--- a/CookBook/Package/Ind_Code.thy Tue Mar 17 12:26:34 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy Tue Mar 17 17:32:12 2009 +0100
@@ -4,8 +4,6 @@
section {* Code *}
-subsection {* Definitions *}
-
text {*
@{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
@@ -42,8 +40,8 @@
@{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
- We use the following wrapper function to make the definition via
- @{ML LocalTheory.define}. The function takes a predicate name, a syntax
+ In order to make definitions, we use the following wrapper for
+ @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
annotation and a term representing the right-hand side of the definition.
*}
@@ -56,15 +54,13 @@
end*}
text {*
- It returns the definition (as theorem) and the local theory in which this definition has
+ 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
- theorem (others possibilities are @{ML definitionK in Thm} or @{ML axiomK in Thm}).
+ 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 such as finding theorems in the theorem database. We also
+ 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 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
+ not need to have any theorem attributes. A testcase for this function is
*}
local_setup %gray {* fn lthy =>
@@ -76,23 +72,27 @@
end *}
text {*
- 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.
+ which makes the difinition @{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 function constructs the term for the definition, namely
+ The next two functions construct the terms we need for the definitions, namely
+ terms 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 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.
+ 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"}.
+
+ 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"}.
*}
ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
@@ -112,16 +112,17 @@
end*}
text {*
- 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 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 unique free variables are applied to the predicate (Line 11); 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 (fresh) @{text "\<^raw:$zs$>"}, i.e.~the arguments of the predicate.
+ 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
+ predicate.
A testcase for this function is
*}
@@ -140,16 +141,15 @@
end *}
text {*
- It constructs the term for the predicate @{term "even"}. So we obtain as printout
- the term
+ It constructs the left-hand side for the definition of @{term "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. THis is what the
- next function does.
+ the function @{ML defs_aux} over all predicates.
*}
ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
@@ -162,14 +162,19 @@
end*}
text {*
- The argument @{text "preds"} is the list of predicates as @{ML_type term}s;
+ 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.
+ @{text "arg_tyss"} is the list of argument-type-lists for each predicate.
- 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 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.
A testcase for this function is
*}
@@ -185,29 +190,31 @@
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
+ warning (str_of_thms lthy' defs); lthy'
end *}
text {*
- It prints out the two definitions
+ \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"}
+ \end{isabelle}
- @{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"}:
+ Let us now turn to the induction principles. Recall that the proof of the
+ induction principle for @{term "even"} was:
*}
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"
+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)
@@ -217,27 +224,34 @@
done
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}.
+ We have to implement code that constructs the induction principle and then
+ a tactic that automatically proves it.
+
+ 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}.
*}
ML{*fun inst_spec ctrm =
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
text {*
- For example we can use it to instantiate an assumption:
+ For example we can use it in the following proof to instantiate the
+ three quantifiers in the assumption. We use 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"}.
+ *}
+
lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"
apply (tactic {*
- let
- val ctrms = [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}]
- in
- EVERY1 (map (dtac o inst_spec) ctrms)
- end *})
+ inst_spec_tac [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] 1 *})
txt {*
- where it produces the goal state
+ We obtain the goal state
\begin{minipage}{\textwidth}
@{subgoals}
@@ -245,15 +259,15 @@
(*<*)oops(*>*)
text {*
- Now the tactic for proving the induction rules can be implemented
- as follows
+ Now the complete tactic for proving the induction principles can
+ be implemented as follows:
*}
ML %linenosgray{*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),
+ inst_spec_tac insts,
assume_tac]*}
text {*
@@ -261,43 +275,47 @@
A testcase for the tactic is
*}
+ML{*fun test_tac prems =
+let
+ val defs = [@{thm even_def}, @{thm odd_def}]
+ val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
+in
+ induction_tac defs prems insts
+end*}
+
+text {*
+ 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 {*
- let
- val defs = [@{thm even_def}, @{thm odd_def}]
- val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
- in
- induction_tac defs @{thms prems} insts
- end *})
+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 {*
- 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 for each predicate @{text "pred"}
+ 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
+ @{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$>"}
- where the given predicates @{text preds} are replaced by new distinct
- ones written as @{text "\<^raw:$Ps$>"}, and also need to be applied to
- new variables @{text "\<^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.
The function below expects that the rules are already appropriately
- replaced. The argument @{text "mrules"} stands for these modified
+ substitued. The argument @{text "srules"} stands for these substituted
introduction 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 types of its argument.
+ replacement and @{text "tys"} are the argument types of this predicate.
*}
-ML %linenosgray{* fun prove_induction lthy defs mrules cnewpreds ((pred, newpred), tys) =
+ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), tys) =
let
val zs = replicate (length tys) "z"
val (newargnames, lthy') = Variable.variant_fixes zs lthy;
@@ -305,7 +323,7 @@
val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
val goal = Logic.list_implies
- (mrules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
+ (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
in
Goal.prove lthy' [] [prem] goal
(fn {prems, ...} => induction_tac defs prems cnewpreds)
@@ -313,31 +331,37 @@
end *}
text {*
- In Line 3 we produce a list of names @{text "\<^raw:$zs$>"} according to the type
- list. Line 4 makes these names unique and declare them as \emph{free} (but fixed)
- variables. These variables are free in the new theory @{text "lthy'"}. In Line 5
- we just construct the terms corresponding to the variables. The term variables are
- applied to the predicate in Line 7 (this is the first premise
- @{text "pred \<^raw:$zs$>"} of the induction principle). In Line 8 and 9
- we first the term @{text "\<^raw:$P$>\<^raw:$zs$>"} and then add
- the (modified) introduction rules as premises.
+ In Line 3 we produce a name @{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
+ 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; call the induction tactic in
- Line 13. This returns 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 does contain
- 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; 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$>"}.
- So it is left to produce the modified rules and
+ Now it is left to produce the new predicated with which the introduction
+ rules are substituted.
*}
-ML %linenosgray{*fun inductions rules defs preds tyss lthy1 =
+ML %linenosgray{*fun inductions rules defs preds tyss lthy =
let
val Ps = replicate (length preds) "P"
- val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1
+ val (newprednames, lthy') = Variable.variant_fixes Ps lthy
- val thy = ProofContext.theory_of lthy2
+ val thy = ProofContext.theory_of lthy'
val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss
val newpreds = map Free (newprednames ~~ tyss')
@@ -345,9 +369,9 @@
val rules' = map (subst_free (preds ~~ newpreds)) rules
in
- map (prove_induction lthy2 defs rules' cnewpreds)
+ map (prove_induction lthy' defs rules' cnewpreds)
(preds ~~ newpreds ~~ tyss)
- |> ProofContext.export lthy2 lthy1
+ |> ProofContext.export lthy' lthy
end*}
ML {*
@@ -458,20 +482,10 @@
|> snd
end*}
-ML{*fun read_specification' vars specs lthy =
-let
- 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
-in
- (varst, specst')
-end*}
-
ML{*fun add_inductive pred_specs rule_specs lthy =
let
- val (pred_specs', rule_specs') =
- read_specification' pred_specs rule_specs lthy
+ val ((pred_specs', rule_specs'), _) =
+ Specification.read_spec pred_specs rule_specs lthy
in
add_inductive_i pred_specs' rule_specs' lthy
end*}