isabelle-cookbook: comparison CookBook/Package/Ind

equal deleted inserted replaced

-:8bb4eaa2ec92
+:c7f04a008c9c
 (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 just a flag attached to the
+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
 in
 warning (str_of_thm lthy' def); lthy'
 end *}
 text {*
-which makes the difinition @{prop "MyTrue \<equiv> True"} and then prints it out.
+which makes the definition @{prop "MyTrue \<equiv> 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 \<equiv> True"}
 \end{isabelle}
-The next two functions construct the terms we need for the definitions, namely
+The next two functions construct the terms we need for the definitions for
-terms of the form
+our \isacommand{simple\_inductive} command. These
+terms are of the form
 @{text [display] "\<lambda>\<^raw:$zs$>. \<forall>preds. orules \<longrightarrow> 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 @{text "preds"}.
+in the @{text orules} and also be distinct from the @{text "preds"}.
-The first function constructs the term for one particular predicate @{text
+The first function constructs the term for one particular predicate, say
-"pred"}; the number of arguments @{text "\<^raw:$zs$>"} of this predicate is
+@{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
 |> fold_rev mk_all preds
 |> fold_rev lambda fresh_args
 end*}
 text {*
-The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"}. For this
+The function in Line 3 is just a helper function for constructing universal
-it pairs every argument type with the string @{text [quotes] "z"} (Line 7);
+quantifications. The code in Lines 5 to 9 produces the fresh @{text
-then generates variants for all these strings so that they are unique
+"\<^raw:$zs$>"}. For this it pairs every argument type with the string
-w.r.t.~to the @{text "orules"} and the predicates; in Line 9 it generates the
+@{text [quotes] "z"} (Line 7); then generates variants for all these strings
-corresponding variable terms for the unique 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
 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 preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}, @{term "z::nat"}]
 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 *}
 text {*
-It constructs the left-hand side for the definition of @{term "even"}. So we obtain
+It constructs the left-hand side for the definition of @{text "even"}. So we obtain
 as printout the term
 @{text [display]
 "\<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 main function for the definitions now has to just iterate the function
-the function @{ML defs_aux} over all predicates.
+@{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
 in
 fold_map make_defs (prednames ~~ syns ~~ defs) lthy
 end*}
 text {*
-The argument @{text "preds"} is again the the list of predicates as
+The user will state the introduction rules using meta-implications and
-@{ML_type term}s;
+meta-quanti\-fications. In Line 4, we transform these introduction rules into
-the argument @{text "prednames"} is the list of names of the predicates;
+the object logic (since definitions cannot be stated with
-@{text "arg_tyss"} is the list of argument-type-lists for each predicate.
+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
-The user give the introduction rules using meta-implications and meta-quantifications.
+@{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call
-In line 4 we transform the introduction rules into the object logic (definitions
+to @{ML defs_aux} in Line 5 produces all left-hand sides of the
-cannot use them). To do the transformation we have to
+definitions. The actual definitions are then made in Line 7.  The result
-obtain the theory behind the local theory (Line 3); with this theory
+of the function is a list of theorems and a local 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.
-As the result we obtain a list of theorems and a local theory.
 A testcase for this function is
 *}
 local_setup %gray {* fn 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 \<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"}
+>                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
 \end{isabelle}
-This completes the code concerning the definitions. Next comes the code for
+This completes the code for making the definitions. Next we deal with
-the induction principles.
+the induction principles. Recall that the proof of the induction principle
+for @{text "even"} was:
-Let us now turn to the induction principles. Recall that the proof of the
+*}
-induction principle for @{term "even"} was:
-*}
+lemma man_ind_principle:
-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(atomize (full))
 apply(cut_tac prems)
 apply(unfold even_def)
 apply(drule spec[where x=Q])
 apply(assumption)
 done
 text {*
-We have to implement code that constructs the induction principle and then
+The code for such induction principles has to accomplish two tasks:
-a tactic that automatically proves it.
+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. This function instantiates the @{text "?x"} in the theorem
+quantifiers.
-@{thm spec} with a given @{ML_type cterm}.
 *}
 ML{*fun inst_spec ctrm =
 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
 text {*
-For example we can use it in the following proof to instantiate the
+This helper function instantiates the @{text "?x"} in the theorem
-three quantifiers in the assumption. We use the tactic
+@{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 {*
-and then apply use it with the @{ML_type cterm}s @{text "y1\<dots>y3"}.
+we can use @{ML inst_spec} in the following proof to instantiate the
-*}
+three quantifiers in the assumption.
+*}
-lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"
+lemma
+fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+shows "\<forall>x y z. P x y z \<Longrightarrow> True"
 apply (tactic {*
-inst_spec_tac  [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] 1 *})
+inst_spec_tac  [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
 txt {*
 We obtain the goal state
 \begin{minipage}{\textwidth}
 @{subgoals}
 K (rewrite_goals_tac defs),
 inst_spec_tac insts,
 assume_tac]*}
 text {*
-We only have to give it as arguments the premises and the instantiations.
+We only have to give it as arguments the definitions, the premise
-A testcase for the tactic is
+(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}]
 in
 induction_tac defs prems insts
 end*}
 text {*
-which indeed proves the induction principle.
+which indeed proves the induction principle:
 *}
 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(tactic {* test_tac @{thms prems} *})
 done
 text {*
-While the generic proof for the induction principle is relatively simple,
+While the tactic for the induction principle is relatively simple,
-it is a bit harder to construct the goals from just the introduction
+it is a bit harder to construct the goals from the introduction
-rules the user states. In general we have to construct for each predicate
+rules the user provides. In general we have to construct for each predicate
 @{text "pred"} a goal of the form
 @{text [display]
-"\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$>\<^raw:$zs$>"}
+"\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$> \<^raw:$zs$>"}
 where the given predicates @{text preds} are replaced in the introduction
-rule @{text "rules"} by new distinct variables written as @{text "\<^raw:$Ps$>"}.
+rules by new distinct variables written @{text "\<^raw:$Ps$>"}.
-We also need to generate fresh arguments for the predicate @{text "pred"} and
+We also need to generate fresh arguments for the predicate @{text "pred"} in
-the @{text "\<^raw:$P$>"} in the conclusion of the induction principle.
+the premise and the @{text "\<^raw:$P$>"} in the conclusion. We achieve
+that in two steps.
-The function below expects that the rules are already appropriately
-substitued. The argument @{text "srules"} stands for these substituted
+The function below expects that the introduction rules are already appropriately
-introduction rules; @{text cnewpreds} are the certified terms coresponding
+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.
 *}
 (fn {prems, ...} => induction_tac defs prems cnewpreds)
 |> singleton (ProofContext.export lthy' lthy)
 end *}
 text {*
-In Line 3 we produce a name @{text "\<^raw:$zs$>"} for each type in the
+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 (modified) introduction rules as premises. In case that
+and then add the (substituded) introduction rules as premises. In case that
-no introduction rules are given, the conclusion of this implications needs
+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; then call the tactic for proving the
+In Line 11 we set up the goal to be proved; in the next line call the tactic
-induction principle. This tactic expects the (certified) predicates with which
+for proving the induction principle. This tactic expects definitions, the
-the introduction rules have been substituted. This will return a theorem.
+premise and the (certified) predicates with which the introduction rules
-However, it is a theorem proved inside the local theory @{text "lthy'"} where
+have been substituted. This will return a theorem. However, it is a theorem
-the variables @{text "\<^raw:$zs$>"} are fixed, but free. By exporting this
+proved inside the local theory @{text "lthy'"}, where the variables @{text
-theorem from @{text "lthy'"} (which contains the  @{text "\<^raw:$zs$>"}
+"\<^raw:$zs$>"} are fixed, but free. By exporting this theorem from @{text
-as free) to @{text "lthy"} (which does not), we obtain the desired quantifications
+"lthy'"} (which contains the @{text "\<^raw:$zs$>"} as free) to @{text
-@{text "\<And>\<^raw:$zs$>"}.
+"lthy"} (which does not), we obtain the desired quantifications @{text
+"\<And>\<^raw:$zs$>"}.
-Now it is left to produce the new predicated with which the introduction
+(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 tyss lthy  =
+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) tyss
+val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss
 val newpreds = map Free (newprednames ~~ tyss')
 val cnewpreds = map (cterm_of thy) newpreds
-val rules' = map (subst_free (preds ~~ newpreds)) rules
+val srules = map (subst_free (preds ~~ newpreds)) rules
 in
-map (prove_induction lthy' defs rules' cnewpreds)
+map (prove_induction lthy' defs srules cnewpreds)
-(preds ~~ newpreds ~~ tyss)
+(preds ~~ newpreds ~~ arg_tyss)
 |> ProofContext.export lthy' lthy
 end*}
-ML {*
+text {*
-let
+In Line 3 we generate a string @{text [quotes] "P"} for each predicate.
-val rules = [@{prop "even (0::nat)"},
+In Line 4, we use the same trick as in the previous function, that is making the
-@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+@{text "\<^raw:$Ps$>"} fresh and declaring them as fixed but free in
-@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
+the new local theory @{text "lthy'"}. From the local theory we extract
-val defs = [@{thm even_def}, @{thm odd_def}]
+the ambient theory in Line 6. We need this theory in order to certify
-val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+the new predicates. In Line 8 we calculate the types of these new predicates
-val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
+using the argument types. Next we turn them into terms and subsequently
-in
+certify them. We can now produce the substituted introduction rules
-inductions rules defs preds tyss @{context}
+(Line 11). Line 14 and 15 just iterate the proofs for all predicates.
-end
+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).
-subsection {* Introduction Rules *}
+A testcase for this function is
+*}
+local_setup %gray {* fn lthy =>
+let
+val rules = [@{prop "even (0::nat)"},
+@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
+val defs = [@{thm even_def}, @{thm odd_def}]
+val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>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 \<Longrightarrow>
+>  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> P z,
+> odd z \<Longrightarrow>
+>  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> 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 =
 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}]),
+REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
 subproof1 rules preds i ctxt]*}
 lemma evenS:
 shows "odd m \<Longrightarrow> even (Suc m)"
 apply(tactic {*
 in
 add_inductive_i pred_specs' rule_specs' lthy
 end*}
 ML{*val spec_parser =
-OuterParse.opt_target --
 OuterParse.fixes --
 Scan.optional
 (OuterParse.$$$ "where" |--
 OuterParse.!!!
 (OuterParse.enum1 "|"
 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 ML{*val specification =
 spec_parser >>
-(fn ((loc, pred_specs), rule_specs) =>
+(fn ((pred_specs), rule_specs) => add_inductive pred_specs rule_specs)*}
-Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*}
+ML{*val _ = OuterSyntax.local_theory "simple_inductive" "define inductive predicates"
-ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
 OuterKeyword.thy_decl specification*}
 text {*
 Things to include at the end:

changeset 184	c7f04a008c9c
parent 183	8bb4eaa2ec92
child 185	043ef82000b4