diff -r 8939b8fd8603 -r 069d525f8f1d ProgTutorial/Package/Ind_Code.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ProgTutorial/Package/Ind_Code.thy Thu Mar 19 13:28:16 2009 +0100 @@ -0,0 +1,589 @@ +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"} + + \underline{Induction proof} + + After ``objectivication'' we have + @{text "pred zs"} and @{text "orules[preds::=Ps]"}; and 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"}. + + \underline{Intro proof} + + Assume we want to prove the $i$th intro rule. + + We have to show @{text "\xs. As \ (\ys. Bs \ pred ss)\<^isup>* \ pred ts"}; + expanding the defs, gives + + @{text [display] + "\xs. As \ (\ys. Bs \ (\preds. orules \ pred ss))\<^isup>* \ (\preds. orules \ pred ts"} + + applying as many allI and impI as possible + + so we have @{text "As"}, @{text "(\ys. Bs \ (\preds. orules \ pred ss))\<^isup>*"}, + @{text "orules"}; and have to show @{text "pred ts"} + + the $i$th @{text "orule"} is 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