isabelle-cookbook: comparison CookBook/Package/Ind

equal deleted inserted replaced

-:fb8f22dd8ad0
+:75381fa516cd
 text {*
 First we have to produce for each predicate its definitions of the form
 @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> 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.
 *}
 ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy =
 in
 (thm, lthy')
 end*}
 text {*
-Returns the definition (as theorem) and the local theory in which this definition has
+It 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
+been made. In Line 4 @{ML internalK in Thm} is just a flag attached to the
-theorem (others flags are @{ML definitionK in Thm} or @{ML axiomK in Thm}).
+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
+use @{ML empty_binding in Attrib} in Line 3, since the definition does
-theorem attributes.
+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
-in
+warning (str_of_thm lthy' def); lthy'
-lthy'
 end *}
 text {*
-Prints out the theorem @{prop "MyTrue \<equiv> True"}.
+which prints out the theorem @{prop "MyTrue \<equiv> True"}. Since we are
-*}
+testing the function inside \isacommand{local\_setup} we have also
+access to theorem associated with this definition.
-text {*
-Constructs the term for the definition: the main arguments are a predicate
+\begin{isabelle}
-and the types of the arguments, it also expects orules which are the
+\isacommand{thm}~@{text "MyTrue_def"}\\
-intro rules in the object logic; preds which are all predicates. returns the
+@{text "> MyTrue \<equiv> True"}
-term.
+\end{isabelle}
+The next function constructs the term for the definition, namely
+@{text [display] "\<lambda>\<^raw:$zs$>. \<forall>preds. orules \<longrightarrow> 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) =
 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 orules
+|> 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 lines 5-9 produce fresh arguments with which the predicate can be applied.
+The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"} with which the
-For this it pairs every type with a string @{text [quotes] "z"} (Line 7); then
+predicate is applied. For this it pairs every type with a string @{text [quotes] "z"}
-generates variants for all these strings (names) so that they are unique w.r.t.~to
+(Line 7); then generates variants for all these strings (names) so that they are
-the intro rules; in Line 9 it generates the corresponding variable terms for these
+unique w.r.t.~to the orules and predicates; in Line 9 it generates the corresponding
-unique names.
+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 "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
 @{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}]
 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
 val pred = @{term "even::nat\<Rightarrow>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*}
+end *}
 text {*
-The arguments of the main function for the definitions are
+It constructs the term for the predicate @{term "even"}. So we obtain as printout
-the intro rules; the predicates and their names, their syntax
+the term
-annotations and the argument types of each predicate. It
-returns a theorem list (the definitions) and a local
+@{text [display]
-theory where the definitions are made
+"\<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
+\<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> 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 =
 let
 val thy = ProofContext.theory_of lthy
 in
 fold_map make_defs (prednames ~~ syns ~~ defs) lthy
 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.
-*}
+A testcase for this function is
-local_setup {*
+*}
-fn lthy =>
+local_setup %gray {* fn lthy =>
 let
 val rules = [@{prop "even 0"},
 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
 val prednames = [Binding.name "even", Binding.name "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*}
+end *}
+text {*
-subsection {* Induction Principles *}
+It prints out the two definitions
-text {* Recall the proof for the induction principle for @{term "even"}: *}
+@{text [display]
+"even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
+\<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,
+odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
+\<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
+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"
 shows "P 0 \<Longrightarrow>
 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
 apply(drule spec[where x=P])
 apply(drule spec[where x=Q])
 apply(assumption)
 done
+text {*
-text {* We need to be able to instantiate universal quantifiers. *}
+To automate this proof we need to be able to instantiate universal
+quantifiers. For this we use the following helper function. It
-ML{*fun inst_spec ct =
+instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}.
-Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*}
+*}
-text {*
+ML{*fun inst_spec ctrm =
-Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}.
+Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
-*}
+text {*
-text {*
+For example we can use it to instantiate an assumption:
-Instantiates universal qantifications in the premises
+*}
-*}
+lemma "\<forall>x1 x2 x3. P (x1::nat) (x2::nat) (x3::nat) \<Longrightarrow> True"
-lemma "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \<Longrightarrow> 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}
+txt {*
-@{subgoals}
+where it produces the goal state
-\end{minipage}*}
+\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 =
 EVERY1 [ObjectLogic.full_atomize_tac,
 cut_facts_tac prems,
 K (rewrite_goals_tac defs),
 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 \<Longrightarrow>
 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
 end *})
 done
 text {*
-While the generic proof is relatively simple, it is a bit harder to
+which indeed proves the lemma.
-set up the goals for the induction principles.
-*}
+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
-ML {*
+rules. For this we have to construct
-fun prove_induction lthy2 defs rules cnewpreds ((pred, newpred), tys)  =
+@{text [display]
+"\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^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 %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)
+|> singleton (ProofContext.export lthy' lthy)
-end
+end *}
-*}
+text {* *}
 ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =
 let
 val Ps = replicate (length preds) "P"
 val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1
 val rules' = map (subst_free (preds ~~ newpreds)) rules
 in
 map (prove_induction lthy2 defs rules' cnewpreds)
 (preds ~~ newpreds ~~ tyss)
 |> ProofContext.export lthy2 lthy1
 end*}
 ML {*
 let
 val rules = [@{prop "even (0::nat)"},

changeset 179	75381fa516cd
parent 178	fb8f22dd8ad0
child 180	9c25418db6f0