--- a/CookBook/Package/simple_inductive_package.ML Thu Feb 12 14:15:50 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Thu Feb 12 16:09:42 2009 +0000
@@ -4,12 +4,12 @@
val add_inductive_i:
((Binding.binding * typ) * mixfix) list -> (*{predicates}*)
(Binding.binding * typ) list -> (*{parameters}*)
- (Attrib.binding * term) list -> (*{rules}*)
- local_theory -> (thm list * thm list) * local_theory
+ ((Binding.binding * Attrib.src list) * 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) list list -> (*{rules}*)
+ (Attrib.binding * string) list -> (*{rules}*)
local_theory -> local_theory
end;
(* @end *)
@@ -17,138 +17,159 @@
structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
struct
+
fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
-fun inst_spec ct = Drule.instantiate'
- [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
+fun inst_spec ct =
+ Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
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});
-fun add_inductive_i preds_syn params intrs lthy =
- let
- val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
- val preds = map (fn ((R, T), _) =>
- list_comb (Free (Binding.base_name R, T), params')) preds_syn;
- val Tss = map (binder_types o fastype_of) preds;
-
- (* making the definition *)
+(* @chunk induction_rules *)
+fun INDUCTION rules preds' Tss defs lthy1 lthy2 =
+let
+ 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 rules'' = map (subst_free (preds' ~~ Ps)) rules;
- val intrs' = map
- (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs;
-
- 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.empty_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;
+ fun prove_indrule ((R, P), Ts) =
+ let
+ val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3;
+ val zs = map Free (znames ~~ Ts)
- val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
-
-
- (* proving the induction rules *)
- (* @chunk 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 prove_indrule ((R, P), Ts) =
- let
- val (znames, lthy4) =
- Variable.variant_fixes (replicate (length Ts) "z") lthy3;
- val zs = map Free (znames ~~ Ts)
+ val prem = HOLogic.mk_Trueprop (list_comb (R, zs))
+ val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs)))
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)
+ Goal.prove lthy4 [] [prem] goal
+ (fn {prems, ...} => EVERY1
+ ([ObjectLogic.full_atomize_tac,
+ cut_facts_tac prems,
+ K (rewrite_goals_tac defs)] @
+ map (fn ct => dtac (inst_spec ct)) cPs @
+ [assume_tac])) |>
+ singleton (ProofContext.export lthy4 lthy1)
end;
-
- val indrules = map prove_indrule (preds ~~ Ps ~~ Tss);
- (* @end *)
+in
+ map prove_indrule (preds' ~~ Ps ~~ Tss)
+end
+(* @end *)
- (* proving the introduction rules *)
- (* @chunk intro_rules *)
- fun prove_intr (i, (_, r)) =
+(* @chunk intro_rules *)
+fun INTROS rules preds' defs lthy1 lthy2 =
+let
+ fun prove_intro (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),
+ REPEAT (resolve_tac [@{thm allI},@{thm 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
+ 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
- EVERY (map (fn prem =>
+ rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ THEN
+ EVERY1 (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)
+ prem' |> all_elims params2
+ |> imp_elims prems2
+ | _ => prem';
+ in rtac prem'' 1 end) ctxt') prems1)
end) ctxt 1]) |>
- singleton (ProofContext.export lthy2 lthy1);
-
- val intr_ths = map_index prove_intr intrs;
- (* @end *)
+ singleton (ProofContext.export lthy2 lthy1)
+in
+ map_index prove_intro rules
+end
+(* @end *)
- (* storing the theorems *)
- (* @chunk storing *)
- val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds_syn);
- val case_names = map (Binding.base_name o fst o fst) intrs
- (* @end *)
- in
- lthy1 |>
- LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
- ((Binding.qualify mut_name a, atts), [([th], [])]))
- (intrs ~~ intr_ths)) |->
- (fn intr_thss => LocalTheory.note Thm.theoremK
- ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intr_thss)) |>>
- snd ||>>
- (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
- ((Binding.qualify (Binding.base_name 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_syn ~~ indrules)) #>> maps snd)
- end;
-
-(* @chunk add_inductive *)
-fun add_inductive preds params specs lthy =
- let
- val ((vars, specs'), _) = Specification.read_specification (preds @ params) specs lthy;
- val (preds', params') = chop (length preds) vars;
- val specs'' = map (apsnd the_single) specs'
- val params'' = map fst params'
- in
- snd (add_inductive_i preds' params'' specs'' lthy)
- end;
+(* @chunk definitions *)
+fun define_aux s ((binding, syn), (attr, trm)) lthy =
+let
+ val ((_, (_ , thm)), lthy) = LocalTheory.define s ((binding, syn), (attr, trm)) lthy
+in
+ (thm, lthy)
+end
+
+fun DEFINITION params' rules preds preds' Tss lthy =
+let
+ val rules' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy)) rules
+in
+ fold_map (fn ((((R, _), syn), pred), Ts) =>
+ let
+ val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts))
+
+ val t0 = list_comb (pred, zs);
+ val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0;
+ val t2 = fold_rev mk_all preds' t1;
+ val t3 = fold_rev lambda (params' @ zs) t2;
+ in
+ define_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
+ end) (preds ~~ preds' ~~ Tss) lthy
+end
(* @end *)
+(* @chunk add_inductive_i *)
+fun add_inductive_i preds params specs lthy =
+ let
+ val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
+ val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds;
+ val Tss = map (binder_types o fastype_of) preds';
+ val (ass,rules) = split_list specs;
-(* outer syntax *)
+ val (defs, lthy1) = DEFINITION params' rules preds preds' Tss lthy
+ val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
+
+ val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
+
+ val intros = INTROS rules preds' defs lthy1 lthy2
+
+ val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds);
+ val case_names = map (Binding.base_name o fst o fst) specs
+ in
+ lthy1
+ |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
+ ((Binding.qualify mut_name a, atts), [([th], [])])) (specs ~~ intros))
+ |-> (fn intross => LocalTheory.note Thm.theoremK
+ ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intross))
+ |>> snd
+ ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
+ ((Binding.qualify (Binding.base_name 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 add_inductive *)
+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
+
+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 syntax *)
val parser =
OuterParse.opt_target --
@@ -158,14 +179,12 @@
(OuterParse.$$$ "where" |--
OuterParse.!!!
(OuterParse.enum1 "|"
- ((SpecParse.opt_thm_name ":" --
- (OuterParse.prop >> single)) >> single))) []
-
+ (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
val ind_decl =
- parser >>
+ parser >>
(fn (((loc, preds), params), specs) =>
- Toplevel.local_theory loc (add_inductive preds params specs));
+ Toplevel.local_theory loc (add_inductive preds params specs))
val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
OuterKeyword.thy_decl ind_decl;