--- a/CookBook/Package/simple_inductive_package.ML Sun Mar 08 20:53:00 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Tue Mar 10 13:20:46 2009 +0000
@@ -18,107 +18,143 @@
structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
struct
-fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
-
-(* @chunk definitions_aux *)
-fun definitions_aux ((binding, syn), trm) lthy =
+(* @chunk make_definitions *)
+fun make_defs ((binding, syn), trm) lthy =
let
- val ((_, (_, thm)), lthy) =
- LocalTheory.define Thm.internalK ((binding, syn), (Attrib.empty_binding, trm)) lthy
+ 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 params rules preds preds' Tss lthy =
+fun definitions rules params preds prednames syns arg_typess lthy =
let
val thy = ProofContext.theory_of lthy
- val rules' = map (ObjectLogic.atomize_term thy) rules
+ val orules = map (ObjectLogic.atomize_term thy) rules
+ val defs =
+ map (defs_aux lthy orules preds params) (preds ~~ arg_typess)
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
- definitions_aux ((R, syn), t3)
- end) (preds ~~ preds' ~~ Tss) lthy
+ 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 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;
-
- fun prove_indrule ((R, P), Ts) =
+(* @chunk subproof1 *)
+fun subproof2 prem params2 prems2 =
+ SUBPROOF (fn {prems, ...} =>
let
- val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3;
- val zs = map Free (znames ~~ Ts)
+ 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 *)
- val prem = HOLogic.mk_Trueprop (list_comb (R, zs))
- val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs)))
+(* @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
- 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;
-in
- map prove_indrule (preds' ~~ Ps ~~ Tss)
- end
+ rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ THEN
+ EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
+ end)
(* @end *)
(* @chunk intro_rules *)
-fun INTROS rules preds' defs lthy1 lthy2 =
+fun INTROS rules parnames preds defs lthy1 =
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 [@{thm allI},@{thm impI}] 1),
- 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 =>
- 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') prems1)
- end) ctxt 1]) |>
- singleton (ProofContext.export lthy2 lthy1)
+ val (_, lthy2) = Variable.add_fixes parnames lthy1
+
+ fun prove_intro (i, goal) =
+ Goal.prove lthy2 [] [] goal
+ (fn {context = ctxt, ...} =>
+ EVERY1
+ [ObjectLogic.rulify_tac,
+ K (rewrite_goals_tac defs),
+ REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
+ subproof1 rules preds i ctxt])
+ |> singleton (ProofContext.export lthy2 lthy1)
in
map_index prove_intro rules
end
+
(* @end *)
(* @chunk add_inductive_i *)
@@ -129,12 +165,15 @@
val Tss = map (binder_types o fastype_of) preds';
val (ass,rules) = split_list specs;
- val (defs, lthy1) = definitions params' rules preds preds' Tss lthy
- val (_, lthy2) = Variable.add_fixes (map (Binding.name_of o fst) params) lthy1;
+ 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 = INDUCTION rules preds' Tss defs lthy1 lthy2
-
- val intros = INTROS rules preds' defs lthy1 lthy2
+ val inducts = inductions rules defs parnames preds' Tss lthy1
+
+ val intros = INTROS 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