--- a/CookBook/Package/Ind_Code.thy Tue Mar 17 17:32:12 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy Wed Mar 18 03:03:51 2009 +0100
@@ -55,7 +55,7 @@
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
@@ -72,7 +72,7 @@
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}:
@@ -82,17 +82,20 @@
@{text "> MyTrue \<equiv> True"}
\end{isabelle}
- The next two functions construct the terms we need for the definitions, namely
- terms of the form
+ 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] "\<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
- "pred"}; the number of arguments @{text "\<^raw:$zs$>"} of this predicate is
- determined by the number of argument types of @{text "arg_tys"}.
+ 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) =
@@ -112,11 +115,13 @@
end*}
text {*
- The code in Lines 5 to 9 produce 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 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
@@ -132,7 +137,7 @@
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)
@@ -141,15 +146,18 @@
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 function @{ML defs_aux} over all predicates.
+ 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 =
@@ -162,19 +170,16 @@
end*}
text {*
- 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.
-
- The user give the introduction rules using meta-implications and meta-quantifications.
- In line 4 we transform the introduction rules into the object logic (definitions
- cannot use them). To do the 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.
- As the result we obtain a list of theorems and a local theory.
+ 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
*}
@@ -194,6 +199,9 @@
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"}\\
@@ -201,18 +209,16 @@
"> 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
- the induction principles.
-
- Let us now turn to the induction principles. Recall that the proof of the
- induction principle for @{term "even"} was:
+ 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
+lemma man_ind_principle:
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))
@@ -224,32 +230,35 @@
done
text {*
- We have to implement code that constructs the induction principle and then
- a tactic that automatically proves it.
+ 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. This function instantiates the @{text "?x"} in the theorem
- @{thm spec} with a given @{ML_type cterm}.
+ quantifiers.
*}
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
- three quantifiers in the assumption. We use the tactic
+ 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 {*
- 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
@@ -271,8 +280,11 @@
assume_tac]*}
text {*
- We only have to give it as arguments the premises and the instantiations.
- A testcase for the tactic is
+ 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 =
@@ -284,7 +296,7 @@
end*}
text {*
- which indeed proves the induction principle.
+ which indeed proves the induction principle:
*}
lemma
@@ -294,22 +306,23 @@
done
text {*
- While the generic proof for the induction principle is relatively simple,
- it is a bit harder to construct the goals from just the introduction
- rules the user states. In general we have to construct for each predicate
+ 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]
- "\<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$>"}.
- We also need to generate fresh arguments for the predicate @{text "pred"} and
- the @{text "\<^raw:$P$>"} in the conclusion of the induction principle.
+ 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 rules are already appropriately
- substitued. The argument @{text "srules"} stands for these substituted
- introduction rules; @{text cnewpreds} are the certified terms coresponding
+ 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.
@@ -331,64 +344,102 @@
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
- no introduction rules are given, the conclusion of this implications needs
+ 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; then call the tactic for proving the
- induction principle. This tactic expects 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 "\<And>\<^raw:$zs$>"}.
+ 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
+ "\<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)
- (preds ~~ newpreds ~~ tyss)
+ map (prove_induction lthy' defs srules cnewpreds)
+ (preds ~~ newpreds ~~ arg_tyss)
|> ProofContext.export lthy' lthy
end*}
-ML {*
- 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"}]]
- in
- inductions rules defs preds tyss @{context}
- 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 "\<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
*}
-subsection {* Introduction Rules *}
+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})*}
@@ -422,7 +473,7 @@
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:
@@ -491,7 +542,6 @@
end*}
ML{*val spec_parser =
- OuterParse.opt_target --
OuterParse.fixes --
Scan.optional
(OuterParse.$$$ "where" |--
@@ -501,10 +551,9 @@
ML{*val specification =
spec_parser >>
- (fn ((loc, pred_specs), rule_specs) =>
- Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*}
+ (fn ((pred_specs), rule_specs) => add_inductive pred_specs rule_specs)*}
-ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
+ML{*val _ = OuterSyntax.local_theory "simple_inductive" "define inductive predicates"
OuterKeyword.thy_decl specification*}
text {*