diff -r 2319cff107f0 -r 3f617d7a2691 CookBook/Package/simple_inductive_package.ML --- 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