
diff -r fb8f22dd8ad0 -r 75381fa516cd CookBook/Package/Ind_Code.thy
--- 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 {*




