
diff -r 3f617d7a2691 -r 890fbfef6d6b CookBook/Package/Ind_Code.thy
--- a/CookBook/Package/Ind_Code.thy	Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy	Wed Mar 11 01:43:28 2009 +0000
@@ -94,13 +94,14 @@
   The actual definitions are made in Line 7.  
 *}
 
-subsection {* Introduction Rules *}
+
+subsection {* Induction Principles *}
 
 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}.
+  Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}.
 *}
 
 text {*
@@ -110,44 +111,72 @@
 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*})
+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: 
 *}
 
 ML{*fun induction_tac defs prems insts =
-  EVERY1 [ObjectLogic.full_atomize_tac,
+  EVERY1 [K (print_tac "start"),
+          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"
+  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(tactic {* induction_tac [@{thm even_def}, @{thm odd_def}] [@{thm asm}] 
-  [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})
+apply(tactic {* 
+  let
+     val defs = [@{thm even_def}, @{thm odd_def}]
+     val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
+  in 
+    induction_tac defs @{thms prems} insts 
+  end *})
 done
 
-ML %linenosgray{*fun inductions rules defs preds Tss lthy1  =
+text {*
+  While the generic proof is relatively simple, it is a bit harder to
+  set up the goals for the induction principles. 
+*}
+
+
+ML %linenosgray{*fun inductions rules defs preds tyss 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 tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss
+  val newpreds = map Free (newprednames ~~ tyss')
   val cnewpreds = map (cterm_of thy) newpreds
   val rules' = map (subst_free (preds ~~ newpreds)) rules
 
-  fun prove_induction ((pred, newpred), Ts)  =
+  fun prove_induction ((pred, newpred), tys)  =
   let
-    val zs = replicate (length Ts) "z"
+    val zs = replicate (length tys) "z"
     val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
-    val newargs = map Free (newargnames ~~ Ts)
+    val newargs = map Free (newargnames ~~ tys)
 
     val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
     val goal = Logic.list_implies 
@@ -158,26 +187,137 @@
       |> singleton (ProofContext.export lthy3 lthy1)
   end 
 in
-  map prove_induction (preds ~~ newpreds ~~ Tss)
+  map prove_induction (preds ~~ newpreds ~~ tyss)
+end*}
+
+(*
+ML {*
+  let 
+    val rules = [@{term "even 0"},
+                 @{term "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+                 @{term "\<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"}]]
+  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)
+val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}
+
+ML{*fun subproof2 prem params2 prems2 =  
+ SUBPROOF (fn {prems, ...} =>
+   let
+     val prem' = prems MRS prem;
+     val prem'' = 
+       case prop_of prem' of
+           _ $ (Const (@{const_name All}, _) $ _) =>
+             prem' |> all_elims params2 
+                   |> imp_elims prems2
+         | _ => prem';
+   in 
+     rtac prem'' 1 
+   end)*}
+
+ML{*fun subproof1 rules preds i = 
+ SUBPROOF (fn {params, prems, context = ctxt', ...} =>
+   let
+     val (prems1, prems2) = chop (length prems - length rules) prems;
+     val (params1, params2) = chop (length params - length preds) params;
+   in
+     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 
+     THEN
+     EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
+   end)*}
+
+ML{*
+fun introductions_tac defs rules preds i ctxt =
+  EVERY1 [ObjectLogic.rulify_tac,
+          K (rewrite_goals_tac defs),
+          REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
+          subproof1 rules preds i ctxt]*}
+
+ML{*fun introductions rules preds defs lthy = 
+let
+  fun prove_intro (i, goal) =
+    Goal.prove lthy [] [] goal
+      (fn {context, ...} => introductions_tac defs rules preds i context)
+in
+  map_index prove_intro rules
 end*}
 
-ML {* Goal.prove  *}
-ML {* singleton *}
-ML {* ProofContext.export *}
+ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy =
+let
+  val syns = map snd pred_specs
+  val pred_specs' = map fst pred_specs
+  val prednames = map fst pred_specs'
+  val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'
 
-text {*
+  val tyss = map (binder_types o fastype_of) preds   
+  val (attrs, rules) = split_list rule_specs    
+
+  val (defs, lthy') = definitions rules preds prednames syns tyss lthy      
+  val ind_rules = inductions rules defs preds tyss lthy' 	
+  val intro_rules = introductions rules preds defs lthy'
 
-*}
-
-text {*
-  @{ML_chunk [display,gray] subproof1}
-
-  @{ML_chunk [display,gray] subproof2}
-
-  @{ML_chunk [display,gray] intro_rules}
+  val mut_name = space_implode "_" (map Binding.name_of prednames)
+  val case_names = map (Binding.name_of o fst) attrs
+in
+    lthy' 
+    |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
+        ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) 
+    |-> (fn intross => LocalTheory.note Thm.theoremK
+         ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) 
+    |>> snd 
+    ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
+         ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
+          [Attrib.internal (K (RuleCases.case_names case_names)),
+           Attrib.internal (K (RuleCases.consumes 1)),
+           Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
+          (pred_specs ~~ ind_rules)) #>> maps snd) 
+    |> snd
+end*}
 
 
-*}
+ML{*fun read_specification' vars specs lthy =
+let 
+  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
+in   
+  (varst, specst')
+end*}
+
+ML{*fun add_inductive pred_specs rule_specs lthy =
+let
+  val (pred_specs', rule_specs') = 
+    read_specification' pred_specs rule_specs lthy
+in
+  add_inductive_i pred_specs' rule_specs' lthy
+end*} 
+
+ML{*val spec_parser = 
+   OuterParse.opt_target --
+   OuterParse.fixes -- 
+   Scan.optional 
+     (OuterParse.$$$ "where" |--
+        OuterParse.!!! 
+          (OuterParse.enum1 "|" 
+             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+
+ML{*val specification =
+  spec_parser >>
+    (fn ((loc, pred_specs), rule_specs) =>
+      Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*}
+
+ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
+          OuterKeyword.thy_decl specification*}
 
 text {*
   Things to include at the end:
@@ -191,5 +331,11 @@
   
 *}
 
+simple_inductive
+  Even and Odd
+where
+  Even0: "Even 0"
+| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"
+| OddS: "Even n \<Longrightarrow> Odd (Suc n)"
 
 end




