diff -r 7c09bd3227c5 -r 3da5f3f07d8b CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Fri Mar 13 12:21:44 2009 +0100 +++ b/CookBook/Package/Ind_Code.thy Fri Mar 13 16:57:16 2009 +0100 @@ -1,5 +1,5 @@ theory Ind_Code -imports "../Base" Simple_Inductive_Package Ind_Prelims +imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims begin section {* Code *} @@ -14,24 +14,31 @@ ML{*fun make_defs ((binding, syn), trm) lthy = let val arg = ((binding, syn), (Attrib.empty_binding, trm)) - val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy + val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy in - (thm, lthy) + (thm, lthy') end*} text {* Returns the definition and the local theory in which this definition has - been made. What is @{ML Thm.internalK}? + been made. The @{ML internalK in Thm} is just a flag attached to the + theorem (others flags 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. *} -ML{*let - val lthy = TheoryTarget.init NONE @{theory} -in - make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy -end*} +local_setup {* + fn lthy => + let + val (def, lthy') = make_defs ((Binding.name "MyTrue", NoSyn), @{term True}) lthy + val _ = warning (str_of_thm lthy' def) + in + lthy' + end +*} text {* - Why is the output of MyTrue blue? + Prints out the theorem @{prop "MyTrue \ True"}. *} text {* @@ -41,12 +48,12 @@ term. *} -ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_types) = +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_types + arg_tys |> map (pair "z") |> Variable.variant_frees lthy orules |> map Free @@ -70,18 +77,22 @@ the (fresh) arguments of the predicate. *} -ML{*let - val orules = [@{term "even 0"}, - @{term "\n::nat. odd n \ even (Suc n)"}, - @{term "\n::nat. even n \ odd (Suc n)"}] + +local_setup {* +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"}] + 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 @{context} - (defs_aux @{context} orules preds (@{term "even::nat\bool"}, [@{typ "nat"}]))) + warning (Syntax.string_of_term lthy def); + lthy end*} - text {* The arguments of the main function for the definitions are the intro rules; the predicates and their names, their syntax @@ -108,6 +119,23 @@ subsection {* Induction Principles *} +text {* Recall the proof for the induction principle for @{term "even"}: *} + +lemma + 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 {* We need to be able to instantiate universal quantifiers. *} + ML{*fun inst_spec ct = Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} @@ -120,40 +148,30 @@ *} lemma "\x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \ True" -apply (tactic {* EVERY' (map (dtac o inst_spec) - [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*}) +apply (tactic {* + let + val ctrms = [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}] + in + EVERY1 (map (dtac o inst_spec) ctrms) + end *}) txt {* \begin{minipage}{\textwidth} @{subgoals} \end{minipage}*} (*<*)oops(*>*) - -lemma - assumes "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 tactic for proving the induction rules: + Now the tactic for proving the induction rules: *} ML{*fun induction_tac defs prems insts = - EVERY1 [K (print_tac "start"), - ObjectLogic.full_atomize_tac, + EVERY1 [ObjectLogic.full_atomize_tac, cut_facts_tac prems, K (rewrite_goals_tac defs), EVERY' (map (dtac o inst_spec) insts), assume_tac]*} lemma - assumes "even n" + assumes prems: "even n" shows "P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" apply(tactic {* @@ -165,6 +183,7 @@ end *}) done + text {* While the generic proof is relatively simple, it is a bit harder to set up the goals for the induction principles. @@ -209,12 +228,13 @@ @{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 tyss = [[@{typ "nat"}], [@{typ "nat"}]] in inductions rules defs preds tyss @{context} end *} + subsection {* Introduction Rules *} ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) @@ -266,7 +286,6 @@ end *}) done - ML{*fun introductions rules preds defs lthy = let fun prove_intro (i, goal) = @@ -276,6 +295,8 @@ map_index prove_intro rules end*} +text {* main internal function *} + ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy = let val syns = map snd pred_specs @@ -308,10 +329,9 @@ |> snd end*} - ML{*fun read_specification' vars specs lthy = let - val specs' = map (fn (a, s) => [(a, [s])]) specs + val specs' = map (fn (a, s) => (a, [s])) specs val ((varst, specst), _) = Specification.read_specification vars specs' lthy val specst' = map (apsnd the_single) specst