diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Package/simple_inductive_package.ML
--- a/CookBook/Package/simple_inductive_package.ML	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,243 +0,0 @@
-(* @chunk SIMPLE_INDUCTIVE_PACKAGE *)
-signature SIMPLE_INDUCTIVE_PACKAGE =
-sig
-  val add_inductive_i:
-    ((Binding.binding * typ) * mixfix) list ->  (*{predicates}*)
-    (Binding.binding * typ) list ->  (*{parameters}*)
-    (Attrib.binding * term) list ->  (*{rules}*)
-    local_theory -> local_theory
-
-  val add_inductive:
-    (Binding.binding * string option * mixfix) list ->  (*{predicates}*)
-    (Binding.binding * string option * mixfix) list ->  (*{parameters}*)
-    (Attrib.binding * string) list ->  (*{rules}*)
-    local_theory -> local_theory
-end;
-(* @end *)
-
-structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
-struct
-
-(* @chunk make_definitions *) 
-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
-(* @end *)
-
-(* @chunk definitions_aux *) 
-fun defs_aux lthy orules preds params (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 (params @ fresh_args) 
-end
-(* @end *)
-
-(* @chunk definitions *) 
-fun definitions rules params preds prednames syns arg_typess lthy =
-let
-  val thy = ProofContext.theory_of lthy
-  val orules = map (ObjectLogic.atomize_term thy) rules
-  val defs = 
-    map (defs_aux lthy orules preds params) (preds ~~ arg_typess) 
-in
-  fold_map make_defs (prednames ~~ syns ~~ defs) lthy
-end
-(* @end *)
-
-fun inst_spec ct = 
-  Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
-
-(* @chunk induction_tac *)
-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]
-(* @end *)
-
-(* @chunk induction_rules *)
-fun inductions rules defs parnames preds Tss lthy1  =
-let
-  val (_, lthy2) = Variable.add_fixes parnames lthy1
-  
-  val Ps = replicate (length preds) "P"
-  val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2
-
-  val thy = ProofContext.theory_of lthy3			      
-
-  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 (newargnames, lthy4) = 
-          Variable.variant_fixes (replicate (length Ts) "z") lthy3;
-    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 lthy4 [] [prem] goal
-      (fn {prems, ...} => induction_tac defs prems cnewpreds)
-      |> singleton (ProofContext.export lthy4 lthy1)
-  end 
-in
-  map prove_induction (preds ~~ newpreds ~~ Tss)
-end
-(* @end *)
-
-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});
-
-
-(* @chunk subproof1 *) 
-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)
-(* @end *)
-
-(* @chunk subproof2 *) 
-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)
-(* @end *)
-
-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]
-
-
-(* @chunk intro_rules *) 
-fun introductions rules parnames preds defs lthy1 = 
-let
-  val (_, lthy2) = Variable.add_fixes parnames lthy1
-
-  fun prove_intro (i, goal) =
-    Goal.prove lthy2 [] [] goal
-       (fn {context, ...} => introductions_tac defs rules preds i context)
-       |> singleton (ProofContext.export lthy2 lthy1)
-in
-  map_index prove_intro rules
-end
-(* @end *)
-
-(* @chunk add_inductive_i *)
-fun add_inductive_i preds params specs lthy =
-let
-  val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params;
-  val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds;
-  val Tss = map (binder_types o fastype_of) preds';   
-  val (ass, rules) = split_list specs;  (* FIXME: ass not used? *)  
-
-  val prednames = map (fst o fst) preds
-  val syns = map snd preds
-  val parnames = map (Binding.name_of o fst) params
-
-  val (defs, lthy1) = definitions rules params' preds' prednames syns Tss lthy;
-      
-  val inducts = inductions rules defs parnames preds' Tss lthy1 	
-  
-  val intros = introductions rules parnames preds' defs lthy1
-
-  val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds);
-  val case_names = map (Binding.name_of o fst o fst) specs
-in
-    lthy1 
-    |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
-        ((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros)) 
-    |-> (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], [])]))
-          (preds ~~ inducts)) #>> maps snd) 
-    |> snd
-end
-(* @end *)
-
-(* @chunk read_specification *)
-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 
-(* @end *)
-
-(* @chunk add_inductive *)
-fun add_inductive preds params specs lthy =
-let
-  val (vars, specs') = read_specification' (preds @ params) specs lthy;
-  val (preds', params') = chop (length preds) vars;
-  val params'' = map fst params'
-in
-  add_inductive_i preds' params'' specs' lthy
-end;
-(* @end *)
-
-(* @chunk parser *)
-val spec_parser = 
-   OuterParse.opt_target --
-   OuterParse.fixes -- 
-   OuterParse.for_fixes --
-   Scan.optional 
-     (OuterParse.$$$ "where" |--
-        OuterParse.!!! 
-          (OuterParse.enum1 "|" 
-             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
-(* @end *)
-
-(* @chunk syntax *)
-val specification =
-  spec_parser >>
-    (fn (((loc, preds), params), specs) =>
-      Toplevel.local_theory loc (add_inductive preds params specs))
-
-val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
-          OuterKeyword.thy_decl specification
-(* @end *)
-
-end;