--- a/CookBook/Package/Ind_Code.thy Mon Mar 16 00:12:32 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy Mon Mar 16 03:02:56 2009 +0100
@@ -42,7 +42,7 @@
@{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.
*}
@@ -56,33 +56,43 @@
end*}
text {*
- 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
- theorem (others flags are @{ML definitionK in Thm} or @{ML axiomK in Thm}).
+ It returns the definition (as 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}).
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
- theorem attributes.
+ 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
*}
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
- lthy'
+ warning (str_of_thm lthy' def); 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.
+
+ \begin{isabelle}
+ \isacommand{thm}~@{text "MyTrue_def"}\\
+ @{text "> MyTrue \<equiv> True"}
+ \end{isabelle}
-text {*
- Constructs the term for the definition: the main arguments are a predicate
- and the types of the arguments, it also expects orules which are the
- intro rules in the object logic; preds which are all predicates. returns the
- term.
+ 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) =
@@ -92,7 +102,7 @@
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)
@@ -102,21 +112,21 @@
end*}
text {*
- The lines 5-9 produce fresh arguments with which the predicate can be 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 intro rules; in Line 9 it generates the corresponding variable terms for these
- unique names.
+ 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 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)"},
@@ -127,14 +137,19 @@
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
- the intro rules; the predicates and their names, their syntax
- annotations and the argument types of each predicate. It
- returns a theorem list (the definitions) and a local
- theory where the definitions are made
+ It constructs the term for the predicate @{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.
*}
ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
@@ -147,18 +162,23 @@
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.
+ 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)"}]
+ @{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]
@@ -166,12 +186,23 @@
val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
in
warning (str_of_thms lthy' defs); lthy
-end*}
+end *}
+text {*
+
+ It prints out the two definitions
-subsection {* Induction Principles *}
+ @{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"}
-text {* Recall the proof for the induction principle for @{term "even"}: *}
+ 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"
@@ -185,34 +216,37 @@
apply(assumption)
done
-
-text {* We need to be able to instantiate universal quantifiers. *}
+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}.
+*}
-ML{*fun inst_spec ct =
- Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*}
+ML{*fun inst_spec ctrm =
+ Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
text {*
- Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}.
+ For example we can use it to instantiate an assumption:
*}
-text {*
- Instantiates universal qantifications in the premises
-*}
-
-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"
+lemma "\<forall>x1 x2 x3. P (x1::nat) (x2::nat) (x3::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}
- @{subgoals}
- \end{minipage}*}
+txt {*
+ where it produces the goal state
+
+ \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 =
@@ -222,6 +256,11 @@
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>
@@ -237,26 +276,36 @@
text {*
- While the generic proof is relatively simple, it is a bit harder to
- set up the goals for the induction principles.
+ 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
+
+ @{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 {*
-fun prove_induction lthy2 defs rules cnewpreds ((pred, newpred), tys) =
+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)
-end
-*}
+ |> singleton (ProofContext.export lthy' lthy)
+end *}
+
+text {* *}
ML %linenosgray{*fun inductions rules defs preds tyss lthy1 =
let
@@ -273,7 +322,7 @@
in
map (prove_induction lthy2 defs rules' cnewpreds)
(preds ~~ newpreds ~~ tyss)
- |> ProofContext.export lthy2 lthy1
+ |> ProofContext.export lthy2 lthy1
end*}
ML {*