# HG changeset patch # User Christian Urban # Date 1234454982 0 # Node ID 12533bb49615b0efa304904abab517aeffd9e4ea # Parent b4234e8a0202ecd507b8c2a9ab83474c739ae5cf recovered old version of simple_induct; split the main function into small functions diff -r b4234e8a0202 -r 12533bb49615 CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Thu Feb 12 14:15:50 2009 +0000 +++ b/CookBook/Package/Ind_Code.thy Thu Feb 12 16:09:42 2009 +0000 @@ -14,9 +14,4 @@ *} -text {* - - @{ML_chunk [display,gray] storing} - -*} end diff -r b4234e8a0202 -r 12533bb49615 CookBook/Package/simple_inductive_package.ML --- 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; diff -r b4234e8a0202 -r 12533bb49615 cookbook.pdf Binary file cookbook.pdf has changed