# HG changeset patch # User huffman # Date 1268080586 28800 # Node ID a78bc1930a7a131558275c0df9b4b6e6a8c333e8 # Parent 3d8da9fac424eae374c3af1011611535fcc7cd11 include take_info within take_induct_info type diff -r 3d8da9fac424 -r a78bc1930a7a src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 08 12:21:07 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 08 12:36:26 2010 -0800 @@ -17,7 +17,6 @@ val add_axioms : (binding * (typ * typ)) list -> theory -> (Domain_Take_Proofs.iso_info list - * Domain_Take_Proofs.take_info * Domain_Take_Proofs.take_induct_info) * theory end; @@ -128,7 +127,7 @@ (map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy; in - ((iso_infos, take_info, take_info2), thy) + ((iso_infos, take_info2), thy) end; end; (* struct *) diff -r 3d8da9fac424 -r a78bc1930a7a src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Mar 08 12:21:07 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon Mar 08 12:36:26 2010 -0800 @@ -184,7 +184,7 @@ fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); val repTs : typ list = map mk_eq_typ eqs'; val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs); - val ((iso_infos, take_info, take_info2), thy) = + val ((iso_infos, take_info), thy) = Domain_Axioms.add_axioms dom_eqns thy; val ((rewss, take_rews), theorems_thy) = @@ -192,7 +192,7 @@ |> fold_map (fn ((eq, (x,cs)), info) => Domain_Theorems.theorems (eq, eqs) (Type x, cs) info) (eqs ~~ eqs' ~~ iso_infos) - ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info take_info2; + ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info; in theorems_thy |> Sign.add_path (Long_Name.base_name comp_dnam) @@ -246,7 +246,7 @@ if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); - val ((iso_infos, take_info, take_info2), thy) = thy |> + val ((iso_infos, take_info), thy) = thy |> Domain_Isomorphism.domain_isomorphism (map (fn ((vs, dname, mx, _), eq) => (map fst vs, dname, mx, mk_eq_typ eq, NONE)) @@ -268,7 +268,7 @@ |> fold_map (fn ((eq, (x,cs)), info) => Domain_Theorems.theorems (eq, eqs) (Type x, cs) info) (eqs ~~ eqs' ~~ iso_infos) - ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info take_info2; + ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info; in theorems_thy |> Sign.add_path (Long_Name.base_name comp_dnam) diff -r 3d8da9fac424 -r a78bc1930a7a src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 08 12:21:07 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 08 12:36:26 2010 -0800 @@ -11,7 +11,6 @@ * (binding * binding) option) list -> theory -> (Domain_Take_Proofs.iso_info list - * Domain_Take_Proofs.take_info * Domain_Take_Proofs.take_induct_info) * theory val domain_isomorphism_cmd : @@ -271,7 +270,6 @@ (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list) (thy: theory) : (Domain_Take_Proofs.iso_info list - * Domain_Take_Proofs.take_info * Domain_Take_Proofs.take_induct_info) * theory = let val _ = Theory.requires thy "Representable" "domain isomorphisms"; @@ -656,7 +654,7 @@ Domain_Take_Proofs.add_lub_take_theorems (dom_binds ~~ iso_infos) take_info lub_take_thms thy; in - ((iso_infos, take_info, take_info2), thy) + ((iso_infos, take_info2), thy) end; val domain_isomorphism = gen_domain_isomorphism cert_typ; diff -r 3d8da9fac424 -r a78bc1930a7a src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Mar 08 12:21:07 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Mar 08 12:36:26 2010 -0800 @@ -17,7 +17,8 @@ rep_inverse : thm } type take_info = - { take_consts : term list, + { + take_consts : term list, take_defs : thm list, chain_take_thms : thm list, take_0_thms : thm list, @@ -28,10 +29,19 @@ } type take_induct_info = { - reach_thms : thm list, - take_lemma_thms : thm list, - is_finite : bool, - take_induct_thms : thm list + take_consts : term list, + take_defs : thm list, + chain_take_thms : thm list, + take_0_thms : thm list, + take_Suc_thms : thm list, + deflation_take_thms : thm list, + finite_consts : term list, + finite_defs : thm list, + lub_take_thms : thm list, + reach_thms : thm list, + take_lemma_thms : thm list, + is_finite : bool, + take_induct_thms : thm list } val define_take_functions : (binding * iso_info) list -> theory -> take_info * theory @@ -76,10 +86,19 @@ type take_induct_info = { - reach_thms : thm list, - take_lemma_thms : thm list, - is_finite : bool, - take_induct_thms : thm list + take_consts : term list, + take_defs : thm list, + chain_take_thms : thm list, + take_0_thms : thm list, + take_Suc_thms : thm list, + deflation_take_thms : thm list, + finite_consts : term list, + finite_defs : thm list, + lub_take_thms : thm list, + reach_thms : thm list, + take_lemma_thms : thm list, + is_finite : bool, + take_induct_thms : thm list }; val beta_ss = @@ -596,10 +615,19 @@ val result = { - reach_thms = reach_thms, - take_lemma_thms = take_lemma_thms, - is_finite = is_finite, - take_induct_thms = take_induct_thms + take_consts = #take_consts take_info, + take_defs = #take_defs take_info, + chain_take_thms = #chain_take_thms take_info, + take_0_thms = #take_0_thms take_info, + take_Suc_thms = #take_Suc_thms take_info, + deflation_take_thms = #deflation_take_thms take_info, + finite_consts = #finite_consts take_info, + finite_defs = #finite_defs take_info, + lub_take_thms = lub_take_thms, + reach_thms = reach_thms, + take_lemma_thms = take_lemma_thms, + is_finite = is_finite, + take_induct_thms = take_induct_thms }; in (result, thy) diff -r 3d8da9fac424 -r a78bc1930a7a src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 08 12:21:07 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 08 12:36:26 2010 -0800 @@ -17,7 +17,6 @@ val comp_theorems : bstring * Domain_Library.eq list -> - Domain_Take_Proofs.take_info -> Domain_Take_Proofs.take_induct_info -> theory -> thm list * theory @@ -212,7 +211,7 @@ (take_lemmas : thm list) (axs_reach : thm list) (take_rews : thm list) - (take_info : Domain_Take_Proofs.take_info) + (take_info : Domain_Take_Proofs.take_induct_info) (thy : theory) = let val dnames = map (fst o fst) eqs; @@ -228,14 +227,12 @@ in val axs_rep_iso = map (ga "rep_iso") dnames; val axs_abs_iso = map (ga "abs_iso") dnames; - val axs_chain_take = map (ga "chain_take") dnames; - val lub_take_thms = map (ga "lub_take") dnames; - val axs_finite_def = map (ga "finite_def") dnames; val cases = map (ga "casedist" ) dnames; val con_rews = maps (gts "con_rews" ) dnames; end; - val {take_0_thms, take_Suc_thms, ...} = take_info; + val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info; + val {lub_take_thms, finite_defs, ...} = take_info; fun one_con p (con, args) = let @@ -364,10 +361,10 @@ val goal = mk_trp (%%:(dn^"_finite") $ %:"x"); val tacs = [ rtac @{thm lub_ID_finite} 1, - resolve_tac axs_chain_take 1, + resolve_tac chain_take_thms 1, resolve_tac lub_take_thms 1, rtac decisive_thm 1]; - in pg axs_finite_def goal (K tacs) end; + in pg finite_defs goal (K tacs) end; val _ = trace " Proving finites"; val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma); @@ -378,7 +375,7 @@ fun tacf {prems, context} = let fun finite_tacs (finite, fin_ind) = [ - rtac(rewrite_rule axs_finite_def finite RS exE)1, + rtac(rewrite_rule finite_defs finite RS exE)1, etac subst 1, rtac fin_ind 1, ind_prems_tac prems]; @@ -417,7 +414,7 @@ cut_facts_tac (subthm :: take (length dnames) prems) 1, REPEAT (rtac @{thm conjI} 1 ORELSE EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1, - resolve_tac axs_chain_take 1, + resolve_tac chain_take_thms 1, asm_simp_tac HOL_basic_ss 1]) ] end; @@ -612,8 +609,7 @@ fun comp_theorems (comp_dnam : string, eqs : eq list) - (take_info : Domain_Take_Proofs.take_info) - (take_induct_info : Domain_Take_Proofs.take_induct_info) + (take_info : Domain_Take_Proofs.take_induct_info) (thy : theory) = let val map_tab = Domain_Take_Proofs.get_map_tab thy; @@ -639,8 +635,8 @@ (* theorems about take *) -val take_lemmas = #take_lemma_thms take_induct_info; -val axs_reach = #reach_thms take_induct_info; +val take_lemmas = #take_lemma_thms take_info; +val axs_reach = #reach_thms take_info; val take_rews = maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;