diff -r 53460ac408b5 -r 5bb2d29553c2 CookBook/Package/simple_inductive_package.ML --- /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;