
diff -r 7c09bd3227c5 -r 3da5f3f07d8b CookBook/Package/Ind_Code.thy
--- a/CookBook/Package/Ind_Code.thy	Fri Mar 13 12:21:44 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Fri Mar 13 16:57:16 2009 +0100
@@ -1,5 +1,5 @@
 theory Ind_Code
-imports "../Base" Simple_Inductive_Package Ind_Prelims
+imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims
 begin
 
 section {* Code *}
@@ -14,24 +14,31 @@
 ML{*fun make_defs ((binding, syn), trm) lthy =
 let 
   val arg = ((binding, syn), (Attrib.empty_binding, trm))
-  val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy
+  val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
 in 
-  (thm, lthy) 
+  (thm, lthy') 
 end*}
 
 text {*
   Returns the definition and the local theory in which this definition has 
-  been made. What is @{ML Thm.internalK}?
+  been made. The @{ML internalK in Thm} 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.
 *}
 
-ML{*let
-  val lthy = TheoryTarget.init NONE @{theory}
-in
-  make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy
-end*}
+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
+*}
 
 text {*
-  Why is the output of MyTrue blue?
+  Prints out the theorem @{prop "MyTrue \<equiv> True"}.
 *}
 
 text {*
@@ -41,12 +48,12 @@
   term.
 *}
 
-ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_types) =
+ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
 let 
   fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
 
   val fresh_args = 
-        arg_types 
+        arg_tys 
         |> map (pair "z")
         |> Variable.variant_frees lthy orules 
         |> map Free
@@ -70,18 +77,22 @@
   the (fresh) arguments of the predicate.
 *}
 
-ML{*let
-  val orules = [@{term "even 0"},
-                @{term "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
-                @{term "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] 
+
+local_setup {*
+fn lthy =>
+let
+  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 pred = @{term "even::nat\<Rightarrow>bool"}
+  val arg_tys = [@{typ "nat"}]
+  val def = defs_aux lthy orules preds (pred, arg_tys)
 in
-  warning
-    (Syntax.string_of_term @{context} 
-      (defs_aux @{context} orules preds (@{term "even::nat\<Rightarrow>bool"}, [@{typ "nat"}])))
+  warning (Syntax.string_of_term lthy def); 
+  lthy
 end*}
 
-
 text {*
   The arguments of the main function for the definitions are 
   the intro rules; the predicates and their names, their syntax 
@@ -108,6 +119,23 @@
 
 subsection {* Induction Principles *}
 
+text {* Recall the proof for the induction principle for @{term "even"}: *}
+
+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(atomize (full))
+apply(cut_tac prems)
+apply(unfold even_def)
+apply(drule spec[where x=P])
+apply(drule spec[where x=Q])
+apply(assumption)
+done
+
+
+text {* We need to be able to instantiate universal quantifiers. *}
+
 ML{*fun inst_spec ct = 
  Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*}
 
@@ -120,40 +148,30 @@
 *}
 
 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"
-apply (tactic {* EVERY' (map (dtac o inst_spec) 
-          [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*})
+apply (tactic {* 
+  let 
+    val ctrms = [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]
+  in 
+    EVERY1 (map (dtac o inst_spec) ctrms)
+  end *})
 txt {* \begin{minipage}{\textwidth}
        @{subgoals} 
        \end{minipage}*}
 (*<*)oops(*>*)
 
-
-lemma 
-  assumes "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)
-apply(drule spec[where x=P])
-apply(drule spec[where x=Q])
-apply(assumption)
-done
-
 text {*
-  The tactic for proving the induction rules: 
+  Now the tactic for proving the induction rules: 
 *}
 
 ML{*fun induction_tac defs prems insts =
-  EVERY1 [K (print_tac "start"),
-          ObjectLogic.full_atomize_tac,
+  EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prems,
           K (rewrite_goals_tac defs),
           EVERY' (map (dtac o inst_spec) insts),
           assume_tac]*}
 
 lemma 
-  assumes "even 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(tactic {* 
@@ -165,6 +183,7 @@
   end *})
 done
 
+
 text {*
   While the generic proof is relatively simple, it is a bit harder to
   set up the goals for the induction principles. 
@@ -209,12 +228,13 @@
                  @{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 tyss = [[@{typ "nat"}], [@{typ "nat"}]]
   in
     inductions rules defs preds tyss @{context}
   end
 *}
 
+
 subsection {* Introduction Rules *}
 
 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
@@ -266,7 +286,6 @@
 end *})
 done
 
-
 ML{*fun introductions rules preds defs lthy = 
 let
   fun prove_intro (i, goal) =
@@ -276,6 +295,8 @@
   map_index prove_intro rules
 end*}
 
+text {* main internal function *}
+
 ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy =
 let
   val syns = map snd pred_specs
@@ -308,10 +329,9 @@
     |> snd
 end*}
 
-
 ML{*fun read_specification' vars specs lthy =
 let 
-  val specs' = map (fn (a, s) => [(a, [s])]) specs
+  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




