--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Fri Oct 10 17:13:21 2008 +0200
@@ -0,0 +1,170 @@
+(* @chunk SIMPLE_INDUCTIVE_PACKAGE *)
+signature SIMPLE_INDUCTIVE_PACKAGE =
+sig
+ val add_inductive_i:
+ ((Name.binding * typ) * mixfix) list -> (*{predicates}*)
+ (Name.binding * typ) list -> (*{parameters}*)
+ (Attrib.binding * term) list -> (*{rules}*)
+ local_theory -> (thm list * thm list) * local_theory
+ val add_inductive:
+ (Name.binding * string option * mixfix) list -> (*{predicates}*)
+ (Name.binding * string option * mixfix) list -> (*{parameters}*)
+ (Attrib.binding * string) list -> (*{rules}*)
+ local_theory -> (thm list * thm list) * local_theory
+end;
+(* @end *)
+
+structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
+struct
+
+fun add_inductive_i preds_syn params intrs lthy =
+ let
+ val params' = map (fn (p, T) => Free (Name.name_of p, T)) params;
+ val preds = map (fn ((R, T), _) =>
+ list_comb (Free (Name.name_of R, T), params')) preds_syn;
+ val Tss = map (binder_types o fastype_of) preds;
+
+ (* making the definition *)
+
+ val intrs' = map
+ (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs;
+
+ fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P;
+
+ val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) =>
+ let val zs = map Free (Variable.variant_frees lthy intrs'
+ (map (pair "z") Ts))
+ in
+ LocalTheory.define Thm.internalK
+ ((R, syn), (Attrib.no_binding, fold_rev lambda (params' @ zs)
+ (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp)
+ intrs' (list_comb (pred, zs)))))) #>> snd #>> snd
+ end) (preds_syn ~~ preds ~~ Tss) lthy;
+
+ val (_, lthy2) = Variable.add_fixes (map (Name.name_of o fst) params) lthy1;
+
+
+ (* proving the induction rules *)
+
+ val (Pnames, lthy3) =
+ Variable.variant_fixes (replicate (length preds) "P") lthy2;
+ val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT))
+ (Pnames ~~ Tss);
+ val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps;
+ val intrs'' = map (subst_free (preds ~~ Ps) o snd) intrs;
+
+ fun inst_spec ct = Drule.instantiate'
+ [SOME (ctyp_of_term ct)] [NONE, SOME ct] spec;
+
+ fun prove_indrule ((R, P), Ts) =
+ let
+ val (znames, lthy4) =
+ Variable.variant_fixes (replicate (length Ts) "z") lthy3;
+ val zs = map Free (znames ~~ Ts)
+ in
+ Goal.prove lthy4 []
+ [HOLogic.mk_Trueprop (list_comb (R, zs))]
+ (Logic.list_implies (intrs'',
+ HOLogic.mk_Trueprop (list_comb (P, zs))))
+ (fn {prems, ...} => EVERY
+ ([ObjectLogic.full_atomize_tac 1,
+ cut_facts_tac prems 1,
+ rewrite_goals_tac defs] @
+ map (fn ct => dtac (inst_spec ct) 1) cPs @
+ [assume_tac 1])) |>
+ singleton (ProofContext.export lthy4 lthy1)
+ end;
+
+ val indrules = map prove_indrule (preds ~~ Ps ~~ Tss);
+
+
+ (* proving the introduction rules *)
+
+ val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
+ val imp_elims = fold (fn th => fn th' => [th', th] MRS mp);
+
+ fun prove_intr (i, (_, r)) =
+ Goal.prove lthy2 [] [] r
+ (fn {prems, context = ctxt} => EVERY
+ [ObjectLogic.rulify_tac 1,
+ rewrite_goals_tac defs,
+ REPEAT (resolve_tac [allI, impI] 1),
+ SUBPROOF (fn {params, prems, context = ctxt', ...} =>
+ let
+ val (prems1, prems2) =
+ chop (length prems - length intrs) prems;
+ val (params1, params2) =
+ chop (length params - length preds) params
+ in
+ rtac (ObjectLogic.rulify
+ (all_elims params1 (nth prems2 i))) 1 THEN
+ EVERY (map (fn prem =>
+ SUBPROOF (fn {prems = prems', concl, ...} =>
+ 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) ctxt' 1) prems1)
+ end) ctxt 1]) |>
+ singleton (ProofContext.export lthy2 lthy1);
+
+ val intr_ths = map_index prove_intr intrs;
+
+
+ (* storing the theorems *)
+
+ val mut_name = space_implode "_" (map (Name.name_of o fst o fst) preds_syn);
+ val case_names = map (Name.name_of o fst o fst) intrs
+ in
+ lthy1 |>
+ LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
+ ((Name.qualified mut_name a, atts), [([th], [])]))
+ (intrs ~~ intr_ths)) |->
+ (fn intr_thss => LocalTheory.note Thm.theoremK
+ ((Name.qualified mut_name (Name.binding "intros"), []), maps snd intr_thss)) |>>
+ snd ||>>
+ (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
+ ((Name.qualified (Name.name_of R) (Name.binding "induct"),
+ [Attrib.internal (K (RuleCases.case_names case_names)),
+ Attrib.internal (K (RuleCases.consumes 1)),
+ Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
+ (preds_syn ~~ indrules)) #>> maps snd)
+ end;
+
+(* @chunk add_inductive *)
+fun add_inductive preds_syn params_syn intro_srcs lthy =
+ let
+ val ((vars, specs), _) = Specification.read_specification
+ (preds_syn @ params_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs)
+ lthy;
+ val (preds_syn', params_syn') = chop (length preds_syn) vars;
+ val intrs = map (apsnd the_single) specs
+ in
+ add_inductive_i preds_syn' (map fst params_syn') intrs lthy
+ end;
+(* @end *)
+
+
+(* outer syntax *)
+
+(* @chunk syntax *)
+local structure P = OuterParse and K = OuterKeyword in
+
+val ind_decl =
+ P.opt_target --
+ P.fixes -- P.for_fixes --
+ Scan.optional (P.$$$ "where" |--
+ P.!!! (P.enum1 "|" (SpecParse.opt_thm_name ":" -- P.prop))) [] >>
+ (fn (((loc, preds), params), specs) =>
+ Toplevel.local_theory loc (add_inductive preds params specs #> snd));
+
+val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
+ K.thy_decl ind_decl;
+
+end;
+(* @end *)
+
+end;