diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Wed Mar 18 23:52:51 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,579 +0,0 @@ -theory Ind_Code -imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims -begin - -section {* Code *} - -text {* - @{text [display] "rule ::= \xs. As \ (\ys. Bs \ pred ss)\<^isup>* \ pred ts"} - - @{text [display] "orule ::= \xs. As \ (\ys. Bs \ pred ss)\<^isup>* \ pred ts"} - - @{text [display] "def ::= pred \ \zs. \preds. orules \ pred zs"} - - @{text [display] "ind ::= \zs. pred zs \ rules[preds::=Ps] \ P zs"} - - @{text [display] "oind ::= \zs. pred zs \ orules[preds::=Ps] \ P zs"} - - So we have @{text "pred zs"} and @{text "orules[preds::=Ps]"}; have to show - @{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\preds. orules \ pred zs"}. - Instantiating the @{text "preds"} with @{text "Ps"} gives - @{text "orules[preds::=Ps] \ P zs"}. So we can conclude with @{text "P zs"}. - - We have to show @{text "\xs. As \ (\ys. Bs \ pred ss)\<^isup>* \ pred ts"}; - expanding the defs - - @{text [display] - "\xs. As \ (\ys. Bs \ (\preds. orules \ pred ss))\<^isup>* \ (\preds. orules \ pred ts"} - - so we have @{text "As"}, @{text "(\ys. Bs \ (\preds. orules \ pred ss))\<^isup>*"}, - @{text "orules"}; and have to show @{text "pred ts"} - - the @{text "orules"} are of the form @{text "\xs. As \ (\ys. Bs \ pred ss)\<^isup>* \ pred ts"}. - - using the @{text "As"} we ???? -*} - - -text {* - First we have to produce for each predicate its definitions of the form - - @{text [display] "pred \ \zs. \preds. orules \ pred zs"} - - In order to make definitions, we use the following wrapper for - @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax - annotation and a term representing the right-hand side of the definition. -*} - -ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy = -let - val arg = ((predname, syn), (Attrib.empty_binding, trm)) - val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy -in - (thm, lthy') -end*} - -text {* - It returns the definition (as a theorem) and the local theory in which this definition has - been made. In Line 4, @{ML internalK in Thm} is a flag attached to the - theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}). - These flags just classify theorems and have no significant meaning, except - for tools that, for example, find theorems in the theorem database. We also - use @{ML empty_binding in Attrib} in Line 3, since the definition does - not need to have any theorem attributes. A testcase for this function is -*} - -local_setup %gray {* fn lthy => -let - val arg = ((@{binding "MyTrue"}, NoSyn), @{term True}) - val (def, lthy') = make_defs arg lthy -in - warning (str_of_thm lthy' def); lthy' -end *} - -text {* - which makes the definition @{prop "MyTrue \ True"} and then prints it out. - Since we are testing the function inside \isacommand{local\_setup}, i.e.~make - changes to the ambient theory, we can query the definition using the usual - command \isacommand{thm}: - - \begin{isabelle} - \isacommand{thm}~@{text "MyTrue_def"}\\ - @{text "> MyTrue \ True"} - \end{isabelle} - - The next two functions construct the terms we need for the definitions for - our \isacommand{simple\_inductive} command. These - terms are of the form - - @{text [display] "\\<^raw:$zs$>. \preds. orules \ pred \<^raw:$zs$>"} - - The variables @{text "\<^raw:$zs$>"} need to be chosen so that they do not occur - in the @{text orules} and also be distinct from the @{text "preds"}. - - The first function constructs the term for one particular predicate, say - @{text "pred"}; the number of arguments of this predicate is - determined by the number of argument types of @{text "arg_tys"}. - So it takes these two parameters as arguments. The other arguments are - all the @{text "preds"} and the @{text "orules"}. -*} - -ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) = -let - fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P - - val fresh_args = - arg_tys - |> map (pair "z") - |> Variable.variant_frees lthy (preds @ orules) - |> map Free -in - list_comb (pred, fresh_args) - |> fold_rev (curry HOLogic.mk_imp) orules - |> fold_rev mk_all preds - |> fold_rev lambda fresh_args -end*} - -text {* - The function in Line 3 is just a helper function for constructing universal - quantifications. The code in Lines 5 to 9 produces the fresh @{text - "\<^raw:$zs$>"}. For this it pairs every argument type with the string - @{text [quotes] "z"} (Line 7); then generates variants for all these strings - so that they are unique w.r.t.~to the @{text "orules"} and the predicates; - in Line 9 it generates the corresponding variable terms for the unique - strings. - - The unique free variables are applied to the predicate (Line 11) using the - function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in - Line 13 we quantify over all predicates; and in line 14 we just abstract - over all the @{text "\<^raw:$zs$>"}, i.e.~the fresh arguments of the - predicate. - - A testcase for this function is -*} - -local_setup %gray{* fn lthy => -let - val orules = [@{prop "even 0"}, - @{prop "\n::nat. odd n \ even (Suc n)"}, - @{prop "\n::nat. even n \ odd (Suc n)"}] - val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}, @{term "z::nat"}] - val pred = @{term "even::nat\bool"} - val arg_tys = [@{typ "nat"}] - val def = defs_aux lthy orules preds (pred, arg_tys) -in - warning (Syntax.string_of_term lthy def); lthy -end *} - -text {* - It constructs the left-hand side for the definition of @{text "even"}. So we obtain - as printout the term - - @{text [display] -"\z. \even odd. (even 0) \ (\n. odd n \ even (Suc n)) - \ (\n. even n \ odd (Suc n)) \ even z"} - - The main function for the definitions now has to just iterate the function - @{ML defs_aux} over all predicates. The argument @{text "preds"} is again - the the list of predicates as @{ML_type term}s; the argument @{text - "prednames"} is the list of names of the predicates; @{text "arg_tyss"} is - the list of argument-type-lists for each predicate. -*} - -ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy = -let - val thy = ProofContext.theory_of lthy - val orules = map (ObjectLogic.atomize_term thy) rules - val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) -in - fold_map make_defs (prednames ~~ syns ~~ defs) lthy -end*} - -text {* - The user will state the introduction rules using meta-implications and - meta-quanti\-fications. In Line 4, we transform these introduction rules into - the object logic (since definitions cannot be stated with - meta-connectives). To do this transformation we have to obtain the theory - behind the local theory (Line 3); with this theory we can use the function - @{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call - to @{ML defs_aux} in Line 5 produces all left-hand sides of the - definitions. The actual definitions are then made in Line 7. The result - of the function is a list of theorems and a local theory. - - - A testcase for this function is -*} - -local_setup %gray {* fn lthy => -let - val rules = [@{prop "even 0"}, - @{prop "\n::nat. odd n \ even (Suc n)"}, - @{prop "\n::nat. even n \ odd (Suc n)"}] - val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}] - val prednames = [@{binding "even"}, @{binding "odd"}] - val syns = [NoSyn, NoSyn] - val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] - val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy -in - warning (str_of_thms lthy' defs); lthy' -end *} - -text {* - where we feed into the functions all parameters corresponding to - the @{text even}-@{text odd} example. The definitions we obtain - are: - - \begin{isabelle} - \isacommand{thm}~@{text "even_def odd_def"}\\ - @{text [break] -"> even \ \z. \even odd. (even 0) \ (\n. odd n \ even (Suc n)) -> \ (\n. even n \ odd (Suc n)) \ even z, -> odd \ \z. \even odd. (even 0) \ (\n. odd n \ even (Suc n)) -> \ (\n. even n \ odd (Suc n)) \ odd z"} - \end{isabelle} - - - This completes the code for making the definitions. Next we deal with - the induction principles. Recall that the proof of the induction principle - for @{text "even"} was: -*} - -lemma man_ind_principle: -assumes prems: "even n" -shows "P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" -apply(atomize (full)) -apply(cut_tac prems) -apply(unfold even_def) -apply(drule spec[where x=P]) -apply(drule spec[where x=Q]) -apply(assumption) -done - -text {* - The code for such induction principles has to accomplish two tasks: - constructing the induction principles from the given introduction - rules and then automatically generating a proof of them using a tactic. - - The tactic will use the following helper function for instantiating universal - quantifiers. -*} - -ML{*fun inst_spec ctrm = - Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*} - -text {* - This helper function instantiates the @{text "?x"} in the theorem - @{thm spec} with a given @{ML_type cterm}. Together with the tactic -*} - -ML{*fun inst_spec_tac ctrms = - EVERY' (map (dtac o inst_spec) ctrms)*} - -text {* - we can use @{ML inst_spec} in the following proof to instantiate the - three quantifiers in the assumption. -*} - -lemma - fixes P::"nat \ nat \ nat \ bool" - shows "\x y z. P x y z \ True" -apply (tactic {* - inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *}) -txt {* - We obtain the goal state - - \begin{minipage}{\textwidth} - @{subgoals} - \end{minipage}*} -(*<*)oops(*>*) - -text {* - Now the complete tactic for proving the induction principles can - be implemented as follows: -*} - -ML %linenosgray{*fun induction_tac defs prems insts = - EVERY1 [ObjectLogic.full_atomize_tac, - cut_facts_tac prems, - K (rewrite_goals_tac defs), - inst_spec_tac insts, - assume_tac]*} - -text {* - We only have to give it as arguments the definitions, the premise - (like @{text "even n"}) - and the instantiations. Compare this with the manual proof given for the - lemma @{thm [source] man_ind_principle}. - A testcase for this tactic is the function -*} - -ML{*fun test_tac prems = -let - val defs = [@{thm even_def}, @{thm odd_def}] - val insts = [@{cterm "P::nat\bool"}, @{cterm "Q::nat\bool"}] -in - induction_tac defs prems insts -end*} - -text {* - which indeed proves the induction principle: -*} - -lemma -assumes prems: "even n" -shows "P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" -apply(tactic {* test_tac @{thms prems} *}) -done - -text {* - While the tactic for the induction principle is relatively simple, - it is a bit harder to construct the goals from the introduction - rules the user provides. In general we have to construct for each predicate - @{text "pred"} a goal of the form - - @{text [display] - "\\<^raw:$zs$>. pred \<^raw:$zs$> \ rules[preds := \<^raw:$Ps$>] \ \<^raw:$P$> \<^raw:$zs$>"} - - where the given predicates @{text preds} are replaced in the introduction - rules by new distinct variables written @{text "\<^raw:$Ps$>"}. - We also need to generate fresh arguments for the predicate @{text "pred"} in - the premise and the @{text "\<^raw:$P$>"} in the conclusion. We achieve - that in two steps. - - The function below expects that the introduction rules are already appropriately - substituted. The argument @{text "srules"} stands for these substituted - rules; @{text cnewpreds} are the certified terms coresponding - to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for - which we prove the introduction principle; @{text "newpred"} is its - replacement and @{text "tys"} are the argument types of this predicate. -*} - -ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), tys) = -let - val zs = replicate (length tys) "z" - val (newargnames, lthy') = Variable.variant_fixes zs lthy; - val newargs = map Free (newargnames ~~ tys) - - val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) - val goal = Logic.list_implies - (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs))) -in - Goal.prove lthy' [] [prem] goal - (fn {prems, ...} => induction_tac defs prems cnewpreds) - |> singleton (ProofContext.export lthy' lthy) -end *} - -text {* - In Line 3 we produce names @{text "\<^raw:$zs$>"} for each type in the - argument type list. Line 4 makes these names unique and declares them as - \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In - Line 5 we just construct the terms corresponding to these variables. - The term variables are applied to the predicate in Line 7 (this corresponds - to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle). - In Line 8 and 9, we first construct the term @{text "\<^raw:$P$>\<^raw:$zs$>"} - and then add the (substituded) introduction rules as premises. In case that - no introduction rules are given, the conclusion of this implication needs - to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal - mechanism will fail. - - In Line 11 we set up the goal to be proved; in the next line call the tactic - for proving the induction principle. This tactic expects definitions, the - premise and the (certified) predicates with which the introduction rules - have been substituted. This will return a theorem. However, it is a theorem - proved inside the local theory @{text "lthy'"}, where the variables @{text - "\<^raw:$zs$>"} are fixed, but free. By exporting this theorem from @{text - "lthy'"} (which contains the @{text "\<^raw:$zs$>"} as free) to @{text - "lthy"} (which does not), we obtain the desired quantifications @{text - "\\<^raw:$zs$>"}. - - (FIXME testcase) - - - Now it is left to produce the new predicates with which the introduction - rules are substituted. -*} - -ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy = -let - val Ps = replicate (length preds) "P" - val (newprednames, lthy') = Variable.variant_fixes Ps lthy - - val thy = ProofContext.theory_of lthy' - - val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss - val newpreds = map Free (newprednames ~~ tyss') - val cnewpreds = map (cterm_of thy) newpreds - val srules = map (subst_free (preds ~~ newpreds)) rules - -in - map (prove_induction lthy' defs srules cnewpreds) - (preds ~~ newpreds ~~ arg_tyss) - |> ProofContext.export lthy' lthy -end*} - -text {* - In Line 3 we generate a string @{text [quotes] "P"} for each predicate. - In Line 4, we use the same trick as in the previous function, that is making the - @{text "\<^raw:$Ps$>"} fresh and declaring them as fixed but free in - the new local theory @{text "lthy'"}. From the local theory we extract - the ambient theory in Line 6. We need this theory in order to certify - the new predicates. In Line 8 we calculate the types of these new predicates - using the argument types. Next we turn them into terms and subsequently - certify them. We can now produce the substituted introduction rules - (Line 11). Line 14 and 15 just iterate the proofs for all predicates. - From this we obtain a list of theorems. Finally we need to export the - fixed variables @{text "\<^raw:$Ps$>"} to obtain the correct quantification - (Line 16). - - A testcase for this function is -*} - -local_setup %gray {* fn lthy => -let - val rules = [@{prop "even (0::nat)"}, - @{prop "\n::nat. odd n \ even (Suc n)"}, - @{prop "\n::nat. even n \ odd (Suc n)"}] - val defs = [@{thm even_def}, @{thm odd_def}] - val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}] - val tyss = [[@{typ "nat"}], [@{typ "nat"}]] - val ind_thms = inductions rules defs preds tyss lthy -in - warning (str_of_thms lthy ind_thms); lthy -end -*} - - -text {* - which prints out - -@{text [display] -"> even z \ -> P 0 \ (\m. Pa m \ P (Suc m)) \ (\m. P m \ Pa (Suc m)) \ P z, -> odd z \ -> P 0 \ (\m. Pa m \ P (Suc m)) \ (\m. P m \ Pa (Suc m)) \ Pa z"} - - - This completes the code for the induction principles. Finally we can - prove the introduction rules. - -*} - -ML {* ObjectLogic.rulify *} - - -ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) -val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} - -ML{*fun subproof2 prem params2 prems2 = - SUBPROOF (fn {prems, ...} => - let - val prem' = prems MRS prem; - val prem'' = - case prop_of prem' of - _ $ (Const (@{const_name All}, _) $ _) => - prem' |> all_elims params2 - |> imp_elims prems2 - | _ => prem'; - in - rtac prem'' 1 - end)*} - -ML{*fun subproof1 rules preds i = - SUBPROOF (fn {params, prems, context = ctxt', ...} => - let - val (prems1, prems2) = chop (length prems - length rules) prems; - val (params1, params2) = chop (length params - length preds) params; - in - rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 - THEN - EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) - end)*} - -ML{* -fun introductions_tac defs rules preds i ctxt = - EVERY1 [ObjectLogic.rulify_tac, - K (rewrite_goals_tac defs), - REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]), - subproof1 rules preds i ctxt]*} - -lemma evenS: - shows "odd m \ even (Suc m)" -apply(tactic {* -let - val rules = [@{prop "even (0::nat)"}, - @{prop "\n::nat. odd n \ even (Suc n)"}, - @{prop "\n::nat. even n \ odd (Suc n)"}] - val defs = [@{thm even_def}, @{thm odd_def}] - val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}] -in - introductions_tac defs rules preds 1 @{context} -end *}) -done - -ML{*fun introductions rules preds defs lthy = -let - fun prove_intro (i, goal) = - Goal.prove lthy [] [] goal - (fn {context, ...} => introductions_tac defs rules preds i context) -in - map_index prove_intro rules -end*} - -text {* main internal function *} - -ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy = -let - val syns = map snd pred_specs - val pred_specs' = map fst pred_specs - val prednames = map fst pred_specs' - val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs' - - val tyss = map (binder_types o fastype_of) preds - val (attrs, rules) = split_list rule_specs - - val (defs, lthy') = definitions rules preds prednames syns tyss lthy - val ind_rules = inductions rules defs preds tyss lthy' - val intro_rules = introductions rules preds defs lthy' - - val mut_name = space_implode "_" (map Binding.name_of prednames) - val case_names = map (Binding.name_of o fst) attrs -in - lthy' - |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => - ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) - |-> (fn intross => LocalTheory.note Thm.theoremK - ((Binding.qualify false mut_name (@{binding "intros"}), []), maps snd intross)) - |>> snd - ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => - ((Binding.qualify false (Binding.name_of R) (@{binding "induct"}), - [Attrib.internal (K (RuleCases.case_names case_names)), - Attrib.internal (K (RuleCases.consumes 1)), - Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) - (pred_specs ~~ ind_rules)) #>> maps snd) - |> snd -end*} - -ML{*fun add_inductive_cmd pred_specs rule_specs lthy = -let - val ((pred_specs', rule_specs'), _) = - Specification.read_spec pred_specs rule_specs lthy -in - add_inductive pred_specs' rule_specs' lthy -end*} - -ML{*val spec_parser = - OuterParse.fixes -- - Scan.optional - (OuterParse.$$$ "where" |-- - OuterParse.!!! - (OuterParse.enum1 "|" - (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} - -ML{*val specification = - spec_parser >> - (fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*} - -ML{*val _ = OuterSyntax.local_theory "simple_inductive" - "define inductive predicates" - OuterKeyword.thy_decl specification*} - -text {* - Things to include at the end: - - \begin{itemize} - \item say something about add-inductive-i to return - the rules - \item say that the induction principle is weaker (weaker than - what the standard inductive package generates) - \end{itemize} - -*} - -simple_inductive - Even and Odd -where - Even0: "Even 0" -| EvenS: "Odd n \ Even (Suc n)" -| OddS: "Even n \ Odd (Suc n)" - -end