--- a/CookBook/Package/Ind_Code.thy	Sun Mar 08 20:53:00 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy	Tue Mar 10 13:20:46 2009 +0000
@@ -1,26 +1,178 @@
 theory Ind_Code
-imports "../Base" Simple_Inductive_Package
+imports "../Base" Simple_Inductive_Package Ind_Prelims
 begin
 
+section {* Code *}
+
+subsection {* Definitions *}
+
+text {*
+  If we give it a term and a constant name, it will define the 
+  constant as the term. 
+*}
+
+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
+in 
+  (thm, lthy) 
+end*}
+
+text {*
+  Returns the definition and the local theory in which this definition has 
+  been made. What is @{ML Thm.internalK}?
+*}
+
+ML {*let
+  val lthy = TheoryTarget.init NONE @{theory}
+in
+  make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy
+end*}
+
+text {*
+  Why is the output of MyTrue blue?
+*}
+
+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.
+*}
+
+ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_types) =
+let 
+  fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
+
+  val fresh_args = 
+        arg_types 
+        |> map (pair "z")
+        |> Variable.variant_frees lthy orules 
+        |> map Free
+in
+  list_comb (pred, fresh_args)
+  |> fold_rev (curry HOLogic.mk_imp) orules
+  |> fold_rev mk_all preds
+  |> fold_rev lambda fresh_args 
+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 unique free variables are applied to the predicate (Line 11); then
+  the intro rules are attached as preconditions (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.
+*}
+
 text {*
-  What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK?
+  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
+*}
+
+ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
+let
+  val thy = ProofContext.theory_of lthy
+  val orules = map (ObjectLogic.atomize_term thy) rules
+  val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) 
+in
+  fold_map make_defs (prednames ~~ syns ~~ defs) lthy
+end*}
+
+text {*
+  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.  
+*}
+
+subsection {* Introduction Rules *}
+
+ML{*fun inst_spec ct = 
+ Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*}
+
+text {*
+  Instantiates the @{text "x"} in @{thm spec[no_vars]} with a @{ML_type cterm}.
+*}
+
+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"
+apply (tactic {* EVERY' (map (dtac o inst_spec) 
+          [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*})
+(*<*)oops(*>*)
+
+text {*
+  The tactic for proving the induction rules: 
 *}
 
+ML{*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),
+          assume_tac]*}
+
+lemma 
+  assumes asm: "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 {* induction_tac [@{thm even_def}, @{thm odd_def}] [@{thm asm}] 
+  [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})
+done
+
+ML %linenosgray{*fun inductions rules defs preds Tss lthy1  =
+let
+  val Ps = replicate (length preds) "P"
+  val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1
+  
+  val thy = ProofContext.theory_of lthy2
+
+  val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss
+  val newpreds = map Free (newprednames ~~ Tss')
+  val cnewpreds = map (cterm_of thy) newpreds
+  val rules' = map (subst_free (preds ~~ newpreds)) rules
+
+  fun prove_induction ((pred, newpred), Ts)  =
+  let
+    val zs = replicate (length Ts) "z"
+    val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
+    val newargs = map Free (newargnames ~~ Ts)
+
+    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 ~~ Tss)
+end*}
+
+ML {* Goal.prove  *}
+ML {* singleton *}
+ML {* ProofContext.export *}
 
 text {*
 
-  @{ML_chunk [display,gray] definitions_aux}
-  @{ML_chunk [display,gray,linenos] definitions}
-
 *}
 
 text {*
-
-  @{ML_chunk [display,gray] induction_rules}
+  @{ML_chunk [display,gray] subproof1}
 
-*}
-
-text {*
+  @{ML_chunk [display,gray] subproof2}
 
   @{ML_chunk [display,gray] intro_rules}