diff -r fb8f22dd8ad0 -r 75381fa516cd CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Mon Mar 16 00:12:32 2009 +0100 +++ b/CookBook/Package/Ind_Code.thy Mon Mar 16 03:02:56 2009 +0100 @@ -42,7 +42,7 @@ @{text [display] "pred \ \zs. \preds. orules \ pred zs"} - We use the following wrapper function to actually make the definition via + We use the following wrapper function to make the definition via @{ML LocalTheory.define}. The function takes a predicate name, a syntax annotation and a term representing the right-hand side of the definition. *} @@ -56,33 +56,43 @@ end*} text {* - Returns the definition (as theorem) and the local theory in which this definition has - been made. The @{ML internalK in Thm} in Line 4 is just a flag attached to the - theorem (others flags are @{ML definitionK in Thm} or @{ML axiomK in Thm}). + It returns the definition (as theorem) and the local theory in which this definition has + been made. In Line 4 @{ML internalK in Thm} is just a flag attached to the + theorem (others possibilities are @{ML definitionK in Thm} or @{ML axiomK in Thm}). These flags just classify theorems and have no significant meaning, except for tools such as finding theorems in the theorem database. We also - use @{ML empty_binding in Attrib} in Line 3, since the definition does not need any - theorem attributes. + use @{ML empty_binding in Attrib} in Line 3, since the definition does + not need any theorem attributes. Note the definition has not yet been + stored in the theorem database. So at the moment we can only refer to it + via the return value. A testcase for this functions is *} local_setup %gray {* fn lthy => let val arg = ((Binding.name "MyTrue", NoSyn), @{term True}) val (def, lthy') = make_defs arg lthy - val _ = warning (str_of_thm lthy' def) in - lthy' + warning (str_of_thm lthy' def); lthy' end *} text {* - Prints out the theorem @{prop "MyTrue \ True"}. -*} + which prints out the theorem @{prop "MyTrue \ True"}. Since we are + testing the function inside \isacommand{local\_setup} we have also + access to theorem associated with this definition. + + \begin{isabelle} + \isacommand{thm}~@{text "MyTrue_def"}\\ + @{text "> MyTrue \ True"} + \end{isabelle} -text {* - Constructs the term for the definition: the main arguments are a predicate - and the types of the arguments, it also expects orules which are the - intro rules in the object logic; preds which are all predicates. returns the - term. + The next function constructs the term for the definition, namely + + @{text [display] "\\<^raw:$zs$>. \preds. orules \ pred \<^raw:$zs$>"} + + The variables @{text "\<^raw:$zs$>"} need to be chosen so to not occur + in the @{text orules} and also be distinct from @{text "pred"}. The function + constructs the term for one particular predicate @{text "pred"}; the number + of @{text "\<^raw:$zs$>"} is determined by the nunber of types. *} ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) = @@ -92,7 +102,7 @@ val fresh_args = arg_tys |> map (pair "z") - |> Variable.variant_frees lthy orules + |> Variable.variant_frees lthy (preds @ orules) |> map Free in list_comb (pred, fresh_args) @@ -102,21 +112,21 @@ end*} text {* - The lines 5-9 produce fresh arguments with which the predicate can be applied. - For this it pairs every type with a string @{text [quotes] "z"} (Line 7); then - generates variants for all these strings (names) so that they are unique w.r.t.~to - the intro rules; in Line 9 it generates the corresponding variable terms for these - unique names. + The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"} with which the + predicate is applied. For this it pairs every type with a string @{text [quotes] "z"} + (Line 7); then generates variants for all these strings (names) so that they are + unique w.r.t.~to the orules and predicates; in Line 9 it generates the corresponding + variable terms for the unique names. The unique free variables are applied to the predicate (Line 11); then - the intro rules are attached as preconditions (Line 12); in Line 13 we + 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 (fresh) arguments of the predicate. + the (fresh) @{text "\<^raw:$zs$>"}, i.e.~the arguments of the predicate. + + A testcase for this function is *} - -local_setup {* -fn lthy => +local_setup %gray{* fn lthy => let val orules = [@{prop "even 0"}, @{prop "\n::nat. odd n \ even (Suc n)"}, @@ -127,14 +137,19 @@ val def = defs_aux lthy orules preds (pred, arg_tys) in warning (Syntax.string_of_term lthy def); lthy -end*} +end *} text {* - The arguments of the main function for the definitions are - the intro rules; the predicates and their names, their syntax - annotations and the argument types of each predicate. It - returns a theorem list (the definitions) and a local - theory where the definitions are made + It constructs the term for the predicate @{term "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. THis is what the + next function does. *} ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy = @@ -147,18 +162,23 @@ end*} text {* + The argument @{text "preds"} is 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. + In line 4 we generate the intro rules in the object logic; for this we have to obtain the theory behind the local theory (Line 3); with this we can call @{ML defs_aux} to generate the terms for the left-hand sides. - The actual definitions are made in Line 7. + The actual definitions are made in Line 7. + + A testcase for this function is *} -local_setup {* -fn lthy => +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)"}] + @{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.name "even", Binding.name "odd"] val syns = [NoSyn, NoSyn] @@ -166,12 +186,23 @@ val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy in warning (str_of_thms lthy' defs); lthy -end*} +end *} +text {* + + It prints out the two definitions -subsection {* Induction Principles *} + @{text [display] +"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"} -text {* Recall the proof for the induction principle for @{term "even"}: *} + This completes the code concerning the definitions. Next comes the code for + the induction principles. + + Recall the proof for the induction principle for @{term "even"}: +*} lemma assumes prems: "even n" @@ -185,34 +216,37 @@ apply(assumption) done - -text {* We need to be able to instantiate universal quantifiers. *} +text {* + To automate this proof we need to be able to instantiate universal + quantifiers. For this we use the following helper function. It + instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}. +*} -ML{*fun inst_spec ct = - Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} +ML{*fun inst_spec ctrm = + Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*} text {* - Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}. + For example we can use it to instantiate an assumption: *} -text {* - Instantiates universal qantifications in the premises -*} - -lemma "\x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \ True" +lemma "\x1 x2 x3. P (x1::nat) (x2::nat) (x3::nat) \ True" apply (tactic {* let - val ctrms = [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}] + val ctrms = [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] in EVERY1 (map (dtac o inst_spec) ctrms) end *}) -txt {* \begin{minipage}{\textwidth} - @{subgoals} - \end{minipage}*} +txt {* + where it produces the goal state + + \begin{minipage}{\textwidth} + @{subgoals} + \end{minipage}*} (*<*)oops(*>*) text {* - Now the tactic for proving the induction rules: + Now the tactic for proving the induction rules can be implemented + as follows *} ML{*fun induction_tac defs prems insts = @@ -222,6 +256,11 @@ EVERY' (map (dtac o inst_spec) insts), assume_tac]*} +text {* + We only have to give it as arguments the premises and the instantiations. + A testcase for the tactic is +*} + lemma assumes prems: "even n" shows "P 0 \ @@ -237,26 +276,36 @@ text {* - While the generic proof is relatively simple, it is a bit harder to - set up the goals for the induction principles. + which indeed proves the lemma. + + While the generic proof for the induction principle is relatively simple, + it is a bit harder to set up the goals just from the given introduction + rules. For this we have to construct + + @{text [display] + "\\<^raw:$zs$>. pred \<^raw:$zs$> \ rules[preds := \<^raw:$Ps$>] \ \<^raw:$P$> \<^raw:$zs$>"} + + where the given predicates are replaced by new ones written + as @{text "\<^raw:$Ps$>"}, and also generate new variables + @{text "\<^raw:$zs$>"}. *} -ML {* -fun prove_induction lthy2 defs rules cnewpreds ((pred, newpred), tys) = +ML %linenosgray{* fun prove_induction lthy defs rules cnewpreds ((pred, newpred), tys) = let val zs = replicate (length tys) "z" - val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; + 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 (rules, HOLogic.mk_Trueprop (list_comb (newpred, newargs))) in - Goal.prove lthy3 [] [prem] goal + Goal.prove lthy' [] [prem] goal (fn {prems, ...} => induction_tac defs prems cnewpreds) - |> singleton (ProofContext.export lthy3 lthy2) -end -*} + |> singleton (ProofContext.export lthy' lthy) +end *} + +text {* *} ML %linenosgray{*fun inductions rules defs preds tyss lthy1 = let @@ -273,7 +322,7 @@ in map (prove_induction lthy2 defs rules' cnewpreds) (preds ~~ newpreds ~~ tyss) - |> ProofContext.export lthy2 lthy1 + |> ProofContext.export lthy2 lthy1 end*} ML {*