--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Package/simple_inductive_package.ML Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,243 @@
+(* @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;