diff -r 4e2341f6599d -r fb8f22dd8ad0 CookBook/Package/Ind_Code.thy
--- a/CookBook/Package/Ind_Code.thy	Sat Mar 14 00:48:22 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Mon Mar 16 00:12:32 2009 +0100
@@ -7,35 +7,72 @@
 subsection {* Definitions *}
 
 text {*
-  If we give it a term and a constant name, it will define the 
-  constant as the term. 
+  @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
+
+  @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
+
+  @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
+  
+  @{text [display] "ind ::= \<And>zs. pred zs \<Longrightarrow> rules[preds::=Ps] \<Longrightarrow> P zs"}
+
+  @{text [display] "oind ::= \<forall>zs. pred zs \<longrightarrow> orules[preds::=Ps] \<longrightarrow> P zs"}
+  
+  So we have @{text "pred zs"} and @{text "orules[preds::=Ps]"}; have to show
+  @{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\<forall>preds. orules \<longrightarrow> pred zs"}.
+  Instantiating the @{text "preds"} with @{text "Ps"} gives
+  @{text "orules[preds::=Ps] \<longrightarrow> P zs"}. So we can conclude with @{text "P zs"}.
+
+  We have to show @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"};
+  expanding the defs 
+  
+  @{text [display]
+  "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow>  (\<forall>preds. orules \<longrightarrow> pred ts"}
+  
+  so we have @{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},
+  @{text "orules"}; and have to show @{text "pred ts"}
+
+  the @{text "orules"} are of the form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}.
+  
+  using the @{text "As"} we ????
 *}
 
-ML{*fun make_defs ((binding, syn), trm) lthy =
+
+text {*
+  First we have to produce for each predicate its definitions of the form
+
+  @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
+
+  We use the following wrapper function to actually 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.
+*}
+
+ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy =
 let 
-  val arg = ((binding, syn), (Attrib.empty_binding, trm))
+  val arg = ((predname, syn), (Attrib.empty_binding, trm))
   val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
 in 
   (thm, lthy') 
 end*}
 
 text {*
-  Returns the definition and the local theory in which this definition has 
-  been made. The @{ML internalK in Thm} is just a flag attached to the 
+  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}). 
   These flags just classify theorems and have no significant meaning, except 
-  for tools such as finding theorems in the theorem database.
+  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. 
 *}
 
-local_setup {*
-  fn lthy =>
-  let
-    val (def, lthy') = make_defs ((Binding.name "MyTrue", NoSyn), @{term True}) lthy 
-    val _ = warning (str_of_thm lthy' def)
-  in
-    lthy'
-  end
-*}
+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'
+end *}
 
 text {*
   Prints out the theorem @{prop "MyTrue \<equiv> True"}.
@@ -89,8 +126,7 @@
   val arg_tys = [@{typ "nat"}]
   val def = defs_aux lthy orules preds (pred, arg_tys)
 in
-  warning (Syntax.string_of_term lthy def); 
-  lthy
+  warning (Syntax.string_of_term lthy def); lthy
 end*}
 
 text {*
@@ -117,6 +153,22 @@
   The actual definitions are made in Line 7.  
 *}
 
+local_setup {*
+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)"}] 
+  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+  val prednames = [Binding.name "even", Binding.name "odd"] 
+  val syns = [NoSyn, NoSyn] 
+  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
+end*}
+
+
 subsection {* Induction Principles *}
 
 text {* Recall the proof for the induction principle for @{term "even"}: *}
@@ -189,8 +241,22 @@
   set up the goals for the induction principles. 
 *}
 
-ML {* singleton *}
-ML {* ProofContext.export *}
+ML {*
+fun prove_induction lthy2 defs rules cnewpreds ((pred, newpred), tys)  =
+let
+  val zs = replicate (length tys) "z"
+  val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
+  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
+  (fn {prems, ...} => induction_tac defs prems cnewpreds)
+  |> singleton (ProofContext.export lthy3 lthy2)
+end 
+*}
 
 ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =
 let
@@ -204,23 +270,10 @@
   val cnewpreds = map (cterm_of thy) newpreds
   val rules' = map (subst_free (preds ~~ newpreds)) rules
 
-
-  fun prove_induction ((pred, newpred), tys)  =
-  let
-    val zs = replicate (length tys) "z"
-    val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
-    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
-      (fn {prems, ...} => induction_tac defs prems cnewpreds)
-       |> singleton (ProofContext.export lthy3 lthy1)
-  end 
 in
-  map prove_induction (preds ~~ newpreds ~~ tyss)
+  map (prove_induction lthy2 defs rules' cnewpreds) 
+        (preds ~~ newpreds ~~ tyss)
+  |> ProofContext.export lthy2 lthy1
 end*}
 
 ML {*