# HG changeset patch # User huffman # Date 1267518866 28800 # Node ID 45c9a8278fafe9e7eb1d78f9218b52f07205d03a # Parent 89b945fa0a3118b55279092ec86cb7d26d0a2719 domain package no longer generates copy functions; all proofs use take functions instead diff -r 89b945fa0a31 -r 45c9a8278faf src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Mon Mar 01 23:54:50 2010 -0800 +++ b/src/HOLCF/Domain.thy Tue Mar 02 00:34:26 2010 -0800 @@ -250,6 +250,27 @@ lemmas sel_defined_iff_rules = cfcomp2 sfst_defined_iff ssnd_defined_iff +lemmas take_con_rules = + ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict + sprod_map_spair' sprod_map_strict u_map_up u_map_strict + +lemma lub_ID_take_lemma: + assumes "chain t" and "(\n. t n) = ID" + assumes "\n. t n\x = t n\y" shows "x = y" +proof - + have "(\n. t n\x) = (\n. t n\y)" + using assms(3) by simp + then have "(\n. t n)\x = (\n. t n)\y" + using assms(1) by (simp add: lub_distribs) + then show "x = y" + using assms(2) by simp +qed + +lemma lub_ID_reach: + assumes "chain t" and "(\n. t n) = ID" + shows "(\n. t n\x) = x" +using assms by (simp add: lub_distribs) + use "Tools/cont_consts.ML" use "Tools/cont_proc.ML" use "Tools/Domain/domain_library.ML" diff -r 89b945fa0a31 -r 45c9a8278faf src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 01 23:54:50 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 02 00:34:26 2010 -0800 @@ -902,15 +902,10 @@ shows "s1< + ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list -> bstring -> Domain_Library.eq list -> theory -> theory end; @@ -67,22 +69,8 @@ val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); - val copy_def = - let fun r i = proj (Bound 0) eqs i; - in - ("copy_def", %%:(dname^"_copy") == /\ "f" - (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep)) - end; - (* ----- axiom and definitions concerning induction ------------------------- *) - val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n - `%x_name === %:x_name)); - val take_def = - ("take_def", - %%:(dname^"_take") == - mk_lam("n",proj - (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); val finite_def = ("finite_def", %%:(dname^"_finite") == @@ -90,9 +78,8 @@ mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); in (dnam, - (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]), - (if definitional then [] else [copy_def]) @ - [take_def, finite_def]) + (if definitional then [] else [abs_iso_ax, rep_iso_ax]), + [finite_def]) end; (* let (calc_axioms) *) @@ -112,14 +99,11 @@ fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; -fun add_axioms definitional comp_dnam (eqs : eq list) thy' = +fun add_axioms definitional eqs' comp_dnam (eqs : eq list) thy' = let val comp_dname = Sign.full_bname thy' comp_dnam; val dnames = map (fst o fst) eqs; val x_name = idx_name dnames "x"; - fun copy_app dname = %%:(dname^"_copy")`Bound 0; - val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == - /\ "f"(mk_ctuple (map copy_app dnames))); fun one_con (con, _, args) = let @@ -165,20 +149,74 @@ fun add_one (dnam, axs, dfs) = Sign.add_path dnam - #> add_defs_infer dfs #> add_axioms_infer axs #> Sign.parent_path; val map_tab = Domain_Isomorphism.get_map_tab thy'; + val axs = mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs; + val thy = thy' |> fold add_one axs; - val thy = thy' - |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs); + fun get_iso_info ((dname, tyvars), cons') = + let + fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t + fun prod (_,args,_) = + case args of [] => oneT + | _ => foldr1 mk_sprodT (map opt_lazy args); + val ax_abs_iso = PureThy.get_thm thy (dname ^ ".abs_iso"); + val ax_rep_iso = PureThy.get_thm thy (dname ^ ".rep_iso"); + val lhsT = Type(dname,tyvars); + val rhsT = foldr1 mk_ssumT (map prod cons'); + val rep_const = Const(dname^"_rep", lhsT ->> rhsT); + val abs_const = Const(dname^"_abs", rhsT ->> lhsT); + in + { + absT = lhsT, + repT = rhsT, + abs_const = abs_const, + rep_const = rep_const, + abs_inverse = ax_abs_iso, + rep_inverse = ax_rep_iso + } + end; + val dom_binds = map (Binding.name o Long_Name.base_name) dnames; + val thy = + if definitional then thy + else snd (Domain_Isomorphism.define_take_functions + (dom_binds ~~ map get_iso_info eqs') thy); + + fun add_one' (dnam, axs, dfs) = + Sign.add_path dnam + #> add_defs_infer dfs + #> Sign.parent_path; + val thy = fold add_one' axs thy; + + (* declare lub_take axioms *) + local + fun ax_lub_take dname = + let + val dnam : string = Long_Name.base_name dname; + val take_const = %%:(dname^"_take"); + val lub = %%: @{const_name lub}; + val image = %%: @{const_name image}; + val UNIV = %%: @{const_name UNIV}; + val lhs = lub $ (image $ take_const $ UNIV); + val ax = mk_trp (lhs === ID); + in + add_one (dnam, [("lub_take", ax)], []) + end + in + val thy = + if definitional then thy + else fold ax_lub_take dnames thy + end; val use_copy_def = length eqs>1 andalso not definitional; in thy - |> Sign.add_path comp_dnam - |> add_defs_infer ((*bisim_def::*)(if use_copy_def then [copy_def] else [])) + |> Sign.add_path comp_dnam +(* + |> add_defs_infer [bisim_def] +*) |> Sign.parent_path end; (* let (add_axioms) *) diff -r 89b945fa0a31 -r 45c9a8278faf src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Mar 01 23:54:50 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 00:34:26 2010 -0800 @@ -164,7 +164,7 @@ ) : cons; val eqs : eq list = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; - val thy = thy' |> Domain_Axioms.add_axioms false comp_dnam eqs; + val thy = thy' |> Domain_Axioms.add_axioms false eqs' comp_dnam eqs; val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn (eq, (x,cs)) => @@ -237,7 +237,7 @@ ) : cons; val eqs : eq list = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; - val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs; + val thy = thy' |> Domain_Axioms.add_axioms true eqs' comp_dnam eqs; val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn (eq, (x,cs)) => diff -r 89b945fa0a31 -r 45c9a8278faf src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 01 23:54:50 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 00:34:26 2010 -0800 @@ -122,6 +122,17 @@ fun mk_deflation t = Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t; +fun mk_lub t = + let + val T = Term.range_type (Term.fastype_of t); + val lub_const = Const (@{const_name lub}, (T --> boolT) --> T); + val UNIV_const = @{term "UNIV :: nat set"}; + val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT; + val image_const = Const (@{const_name image}, image_type); + in + lub_const $ (image_const $ t $ UNIV_const) + end; + (* splits a cterm into the right and lefthand sides of equality *) fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); @@ -424,7 +435,8 @@ fun mk_goal take_const = mk_deflation (take_const $ i); val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)); val adm_rules = - @{thms adm_conj adm_deflation cont2cont_fst cont2cont_snd cont_id}; + @{thms adm_conj adm_subst [OF _ adm_deflation] + cont2cont_fst cont2cont_snd cont_id}; val bottom_rules = take_0_thms @ @{thms deflation_UU simp_thms}; val deflation_rules = @@ -436,8 +448,10 @@ EVERY [rtac @{thm nat.induct} 1, simp_tac (HOL_basic_ss addsimps bottom_rules) 1, - simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1, - REPEAT (resolve_tac deflation_rules 1 ORELSE atac 1)]) + asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1, + REPEAT (etac @{thm conjE} 1 + ORELSE resolve_tac deflation_rules 1 + ORELSE atac 1)]) end; fun conjuncts [] thm = [] | conjuncts (n::[]) thm = [(n, thm)] @@ -795,7 +809,8 @@ val start_thms = @{thm split_def} :: map_apply_thms; val adm_rules = - @{thms adm_conj adm_deflation cont2cont_fst cont2cont_snd cont_id}; + @{thms adm_conj adm_subst [OF _ adm_deflation] + cont2cont_fst cont2cont_snd cont_id}; val bottom_rules = @{thms fst_strict snd_strict deflation_UU simp_thms}; val deflation_rules = @@ -821,115 +836,58 @@ (conjuncts deflation_map_binds deflation_map_thm); val thy = DeflMapData.map (fold Thm.add_thm deflation_map_thms) thy; - (* define copy combinators *) - val new_dts = - map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns; - val copy_arg_type = mk_tupleT (map (fn (T, _) => T ->> T) dom_eqns); - val copy_arg = Free ("f", copy_arg_type); - val copy_args = - let fun mk_copy_args [] t = [] - | mk_copy_args (_::[]) t = [t] - | mk_copy_args (_::xs) t = - mk_fst t :: mk_copy_args xs (mk_snd t); - in mk_copy_args doms copy_arg end; - fun copy_of_dtyp (T, dt) = - if Datatype_Aux.is_rec_type dt - then copy_of_dtyp' (T, dt) - else mk_ID T - and copy_of_dtyp' (T, Datatype_Aux.DtRec i) = nth copy_args i - | copy_of_dtyp' (T, Datatype_Aux.DtTFree a) = mk_ID T - | copy_of_dtyp' (T, Datatype_Aux.DtType (c, ds)) = - case Symtab.lookup map_tab' c of - SOME f => - list_ccomb - (Const (f, mapT T), map copy_of_dtyp (snd (dest_Type T) ~~ ds)) - | NONE => - (warning ("copy_of_dtyp: unknown type constructor " ^ c); mk_ID T); - fun define_copy ((tbind, (rep_const, abs_const)), (lhsT, rhsT)) thy = + (* definitions and proofs related to take functions *) + val (take_info, thy) = + define_take_functions (dom_binds ~~ iso_infos) thy; + val {take_consts, take_defs, chain_take_thms, take_0_thms, + take_Suc_thms, deflation_take_thms} = take_info; + + (* least-upper-bound lemma for take functions *) + val lub_take_lemma = let - val copy_type = copy_arg_type ->> (lhsT ->> lhsT); - val copy_bind = Binding.suffix_name "_copy" tbind; - val (copy_const, thy) = thy |> - Sign.declare_const ((copy_bind, copy_type), NoSyn); - val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT; - val body = copy_of_dtyp (rhsT, dtyp); - val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)); - val rhs = big_lambda copy_arg comp; - val eqn = Logic.mk_equals (copy_const, rhs); - val (copy_def, thy) = - thy - |> Sign.add_path (Binding.name_of tbind) - |> yield_singleton (PureThy.add_defs false o map Thm.no_attributes) - (Binding.name "copy_def", eqn) - ||> Sign.parent_path; - in ((copy_const, copy_def), thy) end; - val ((copy_consts, copy_defs), thy) = thy - |> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns) - |>> ListPair.unzip; - - (* define combined copy combinator *) - val ((c_const, c_def_thms), thy) = - if length doms = 1 - then ((hd copy_consts, []), thy) - else - let - val c_type = copy_arg_type ->> copy_arg_type; - val c_name = space_implode "_" (map Binding.name_of dom_binds); - val c_bind = Binding.name (c_name ^ "_copy"); - val c_body = - mk_tuple (map (mk_capply o rpair copy_arg) copy_consts); - val c_rhs = big_lambda copy_arg c_body; - val (c_const, thy) = - Sign.declare_const ((c_bind, c_type), NoSyn) thy; - val c_eqn = Logic.mk_equals (c_const, c_rhs); - val (c_def_thms, thy) = - thy - |> Sign.add_path c_name - |> (PureThy.add_defs false o map Thm.no_attributes) - [(Binding.name "copy_def", c_eqn)] - ||> Sign.parent_path; - in ((c_const, c_def_thms), thy) end; - - (* fixed-point lemma for combined copy combinator *) - val fix_copy_lemma = - let - fun mk_map_ID (map_const, (T, rhsT)) = - list_ccomb (map_const, map mk_ID (snd (dest_Type T))); + val lhs = mk_tuple (map mk_lub take_consts); + fun mk_map_ID (map_const, (lhsT, rhsT)) = + list_ccomb (map_const, map mk_ID (snd (dest_Type lhsT))); val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns)); - val goal = mk_eqs (mk_fix c_const, rhs); - val rules = - [@{thm pair_collapse}, @{thm split_def}] - @ map_apply_thms - @ c_def_thms @ copy_defs - @ MapIdData.get thy; - val tac = simp_tac (beta_ss addsimps rules) 1; + val goal = mk_trp (mk_eq (lhs, rhs)); + val start_rules = + @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms + @ @{thms pair_collapse split_def} + @ map_apply_thms @ MapIdData.get thy; + val rules0 = + @{thms iterate_0 Pair_strict} @ take_0_thms; + val rules1 = + @{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv} + @ take_Suc_thms; + val tac = + EVERY + [simp_tac (HOL_basic_ss addsimps start_rules) 1, + simp_tac (HOL_basic_ss addsimps @{thms fix_def2}) 1, + rtac @{thm lub_eq} 1, + rtac @{thm nat.induct} 1, + simp_tac (HOL_basic_ss addsimps rules0) 1, + asm_full_simp_tac (beta_ss addsimps rules1) 1]; in Goal.prove_global thy [] [] goal (K tac) end; - (* prove reach lemmas *) - val reach_thm_projs = - let fun mk_projs [] t = [] - | mk_projs (x::[]) t = [(x, t)] - | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); - in mk_projs dom_binds (mk_fix c_const) end; - fun prove_reach_thm (((bind, t), map_ID_thm), (lhsT, rhsT)) thy = + (* prove lub of take equals ID *) + fun prove_lub_take (((bind, take_const), map_ID_thm), (lhsT, rhsT)) thy = let - val x = Free ("x", lhsT); - val goal = mk_eqs (mk_capply (t, x), x); - val rules = - fix_copy_lemma :: map_ID_thm :: @{thms fst_conv snd_conv ID1}; - val tac = simp_tac (HOL_basic_ss addsimps rules) 1; - val reach_thm = Goal.prove_global thy [] [] goal (K tac); + val i = Free ("i", natT); + val goal = mk_eqs (mk_lub (lambda i (take_const $ i)), mk_ID lhsT); + val tac = + EVERY + [rtac @{thm trans} 1, rtac map_ID_thm 2, + cut_facts_tac [lub_take_lemma] 1, + REPEAT (etac @{thm Pair_inject} 1), atac 1]; + val lub_take_thm = Goal.prove_global thy [] [] goal (K tac); in - thy - |> Sign.add_path (Binding.name_of bind) - |> yield_singleton (PureThy.add_thms o map Thm.no_attributes) - (Binding.name "reach", reach_thm) - ||> Sign.parent_path + add_qualified_thm "lub_take" (Binding.name_of bind, lub_take_thm) thy end; - val (reach_thms, thy) = thy |> - fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns); + val (lub_take_thms, thy) = + fold_map prove_lub_take + (dom_binds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy; in (iso_infos, thy) diff -r 89b945fa0a31 -r 45c9a8278faf src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Mon Mar 01 23:54:50 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 00:34:26 2010 -0800 @@ -9,7 +9,6 @@ val calc_syntax: theory -> bool -> - typ -> (string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list -> (binding * typ * mixfix) list @@ -31,7 +30,6 @@ fun calc_syntax thy (definitional : bool) - (dtypeprod : typ) ((dname : string, typevars : typ list), (cons': (binding * (bool * binding option * typ) list * mixfix) list)) : (binding * typ * mixfix) list = @@ -50,18 +48,16 @@ fun dbind s = Binding.name (dnam ^ s); val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn); val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn); - val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn); end; (* ----- constants concerning induction ------------------------------------- *) - val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn); val optional_consts = - if definitional then [] else [const_rep, const_abs, const_copy]; + if definitional then [] else [const_rep, const_abs]; - in (optional_consts @ [const_take, const_finite]) + in (optional_consts @ [const_finite]) end; (* let *) (* ----- putting all the syntax stuff together ------------------------------ *) @@ -75,22 +71,15 @@ let val dtypes = map (Type o fst) eqs'; val boolT = HOLogic.boolT; - val funprod = - foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes); val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes); - val const_copy = - (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn); val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn); val ctt : (binding * typ * mixfix) list list = - map (calc_syntax thy'' definitional funprod) eqs'; + map (calc_syntax thy'' definitional) eqs'; in thy'' |> Cont_Consts.add_consts - (flat ctt @ - (if length eqs'>1 andalso not definitional - then [const_copy] else []) @ - [const_bisim]) + (flat ctt @ [const_bisim]) end; (* let *) end; (* struct *) diff -r 89b945fa0a31 -r 45c9a8278faf src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 01 23:54:50 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 00:34:26 2010 -0800 @@ -120,7 +120,9 @@ in val ax_abs_iso = ga "abs_iso" dname; val ax_rep_iso = ga "rep_iso" dname; - val ax_copy_def = ga "copy_def" dname; + val ax_take_0 = ga "take_0" dname; + val ax_take_Suc = ga "take_Suc" dname; + val ax_take_strict = ga "take_strict" dname; end; (* local *) (* ----- define constructors ------------------------------------------------ *) @@ -177,68 +179,38 @@ (* ----- theorems concerning one induction step ----------------------------- *) -val copy_strict = - let - val _ = trace " Proving copy_strict..."; - val goal = mk_trp (strict (dc_copy `% "f")); - val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts}; - val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; - in - SOME (pg [ax_copy_def] goal (K tacs)) - handle - THM (s, _, _) => (trace s; NONE) - | ERROR s => (trace s; NONE) - end; +local + fun dc_take dn = %%:(dn^"_take"); + val dnames = map (fst o fst) eqs; + fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict"); + val axs_take_strict = map get_take_strict dnames; -local - fun copy_app (con, _, args) = + fun one_take_app (con, _, args) = let - val lhs = dc_copy`%"f"`(con_app con args); + fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; fun one_rhs arg = if Datatype_Aux.is_rec_type (dtyp_of arg) then Domain_Axioms.copy_of_dtyp map_tab - (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg) + mk_take (dtyp_of arg) ` (%# arg) else (%# arg); + val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args); val rhs = con_app2 con one_rhs args; fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg); fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); - val args' = filter_out (fn a => is_rec a orelse is_lazy a) args; - val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts}; - (* FIXME! case_UU_tac *) - fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args'; - val rules = [ax_abs_iso] @ @{thms domain_map_simps}; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; - in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; + val goal = mk_trp (lhs === rhs); + val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}]; + val rules2 = @{thms take_con_rules ID1} @ axs_take_strict; + val tacs = + [simp_tac (HOL_basic_ss addsimps rules) 1, + asm_simp_tac (HOL_basic_ss addsimps rules2) 1]; + in pg con_appls goal (K tacs) end; + val take_apps = map (Drule.export_without_context o one_take_app) cons; in - val _ = trace " Proving copy_apps..."; - val copy_apps = map copy_app cons; + val take_rews = ax_take_0 :: ax_take_strict :: take_apps; end; -local - fun one_strict (con, _, args) = - let - val goal = mk_trp (dc_copy`UU`(con_app con args) === UU); - val rews = the_list copy_strict @ copy_apps @ con_rews; - (* FIXME! case_UU_tac *) - fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @ - [asm_simp_tac (HOLCF_ss addsimps rews) 1]; - in - SOME (pg [] goal tacs) - handle - THM (s, _, _) => (trace s; NONE) - | ERROR s => (trace s; NONE) - end; - - fun has_nonlazy_rec (_, _, args) = exists is_nonlazy_rec args; -in - val _ = trace " Proving copy_stricts..."; - val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons); -end; - -val copy_rews = the_list copy_strict @ copy_apps @ copy_stricts; - in thy |> Sign.add_path (Long_Name.base_name dname) @@ -257,12 +229,12 @@ ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]), ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]), ((Binding.name "injects" , injects ), [Simplifier.simp_add]), - ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]), + ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]), ((Binding.name "match_rews", mat_rews ), [Simplifier.simp_add, Fixrec.fixrec_simp_add])] |> Sign.parent_path |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ - pat_rews @ dist_les @ dist_eqs @ copy_rews) + pat_rews @ dist_les @ dist_eqs) end; (* let *) fun comp_theorems (comp_dnam, eqs: eq list) thy = @@ -282,10 +254,10 @@ local fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); in - val axs_reach = map (ga "reach" ) dnames; val axs_take_def = map (ga "take_def" ) dnames; + val axs_chain_take = map (ga "chain_take") dnames; + val axs_lub_take = map (ga "lub_take" ) dnames; val axs_finite_def = map (ga "finite_def") dnames; - val ax_copy2_def = ga "copy_def" comp_dnam; (* TEMPORARILY DISABLED val ax_bisim_def = ga "bisim_def" comp_dnam; TEMPORARILY DISABLED *) @@ -297,7 +269,6 @@ in val cases = map (gt "casedist" ) dnames; val con_rews = maps (gts "con_rews" ) dnames; - val copy_rews = maps (gts "copy_rews") dnames; end; fun dc_take dn = %%:(dn^"_take"); @@ -307,55 +278,8 @@ (* ----- theorems concerning finite approximation and finite induction ------ *) -local - val iterate_Cprod_ss = global_simpset_of @{theory Fix}; - val copy_con_rews = copy_rews @ con_rews; - val copy_take_defs = - (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; - val _ = trace " Proving take_stricts..."; - fun one_take_strict ((dn, args), _) = - let - val goal = mk_trp (strict (dc_take dn $ %:"n")); - val rules = [ - @{thm monofun_fst [THEN monofunE]}, - @{thm monofun_snd [THEN monofunE]}]; - val tacs = [ - rtac @{thm UU_I} 1, - rtac @{thm below_eq_trans} 1, - resolve_tac axs_reach 2, - rtac @{thm monofun_cfun_fun} 1, - REPEAT (resolve_tac rules 1), - rtac @{thm iterate_below_fix} 1]; - in pg axs_take_def goal (K tacs) end; - val take_stricts = map one_take_strict eqs; - fun take_0 n dn = - let - val goal = mk_trp ((dc_take dn $ @{term "0::nat"}) `% x_name n === UU); - in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end; - val take_0s = mapn take_0 1 dnames; - val _ = trace " Proving take_apps..."; - fun one_take_app dn (con, _, args) = - let - fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; - fun one_rhs arg = - if Datatype_Aux.is_rec_type (dtyp_of arg) - then Domain_Axioms.copy_of_dtyp map_tab - mk_take (dtyp_of arg) ` (%# arg) - else (%# arg); - val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); - val rhs = con_app2 con one_rhs args; - fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg); - fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); - fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); - val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1]; - in pg copy_take_defs goal (K tacs) end; - fun one_take_apps ((dn, _), cons) = map (one_take_app dn) cons; - val take_apps = maps one_take_apps eqs; -in - val take_rews = map Drule.export_without_context - (take_stricts @ take_0s @ take_apps); -end; (* local *) +val take_rews = + maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; local fun one_con p (con, _, args) = @@ -375,7 +299,7 @@ fun ind_term concf = Library.foldr one_eq (mapn (fn n => fn x => (P_name n, x)) 1 conss, mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); - val take_ss = HOL_ss addsimps take_rews; + val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); fun quant_tac ctxt i = EVERY (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); @@ -449,28 +373,15 @@ val _ = trace " Proving take_lemmas..."; val take_lemmas = let - fun take_lemma n (dn, ax_reach) = - let - val lhs = dc_take dn $ Bound 0 `%(x_name n); - val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); - val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); - val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; - val rules = [contlub_fst RS contlubE RS ssubst, - contlub_snd RS contlubE RS ssubst]; - fun tacf {prems, context} = [ - res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, - res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1, - stac fix_def2 1, - REPEAT (CHANGED - (resolve_tac rules 1 THEN chain_tac 1)), - stac contlub_cfun_fun 1, - stac contlub_cfun_fun 2, - rtac lub_equal 3, - chain_tac 1, - rtac allI 1, - resolve_tac prems 1]; - in pg'' thy axs_take_def goal tacf end; - in mapn take_lemma 1 (dnames ~~ axs_reach) end; + fun take_lemma (ax_chain_take, ax_lub_take) = + @{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]; + in map take_lemma (axs_chain_take ~~ axs_lub_take) end; + + val axs_reach = + let + fun reach (ax_chain_take, ax_lub_take) = + @{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]; + in map reach (axs_chain_take ~~ axs_lub_take) end; (* ----- theorems concerning finiteness and induction ----------------------- *) @@ -580,22 +491,28 @@ val cont_rules = [cont_id, cont_const, cont2cont_Rep_CFun, cont2cont_fst, cont2cont_snd]; + val subgoal = + let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n)); + in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end; + val subgoal' = legacy_infer_term thy subgoal; fun tacf {prems, context} = - map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ - quant_tac context 1, - rtac (adm_impl_admw RS wfix_ind) 1, - REPEAT_DETERM (rtac adm_all 1), - REPEAT_DETERM ( - TRY (rtac adm_conj 1) THEN - rtac adm_subst 1 THEN - REPEAT (resolve_tac cont_rules 1) THEN - resolve_tac prems 1), - strip_tac 1, - rtac (rewrite_rule axs_take_def finite_ind) 1, - ind_prems_tac prems]; + let + val subtac = + EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems]; + val subthm = Goal.prove context [] [] subgoal' (K subtac); + in + map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ + 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, + asm_simp_tac HOL_basic_ss 1]) + ] + end; val ind = (pg'' thy [] goal tacf handle ERROR _ => - (warning "Cannot prove infinite induction rule"; TrueI)); + (warning "Cannot prove infinite induction rule"; TrueI) + ); in (finites, ind) end ) handle THM _ => @@ -603,7 +520,6 @@ | ERROR _ => (warning "Cannot prove induction rule"; ([], TrueI)); - end; (* local *) (* ----- theorem concerning coinduction ------------------------------------- *) @@ -667,8 +583,8 @@ in thy |> Sign.add_path comp_dnam |> snd o PureThy.add_thmss [ - ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]), ((Binding.name "take_lemmas", take_lemmas ), []), + ((Binding.name "reach" , axs_reach ), []), ((Binding.name "finites" , finites ), []), ((Binding.name "finite_ind" , [finite_ind]), []), ((Binding.name "ind" , [ind] ), [])(*, diff -r 89b945fa0a31 -r 45c9a8278faf src/HOLCF/ex/Domain_ex.thy --- a/src/HOLCF/ex/Domain_ex.thy Mon Mar 01 23:54:50 2010 -0800 +++ b/src/HOLCF/ex/Domain_ex.thy Tue Mar 02 00:34:26 2010 -0800 @@ -134,7 +134,7 @@ text {* Rules about case combinator *} term tree_when -thm tree.when_def +thm tree.tree_when_def thm tree.when_rews text {* Rules about selectors *} @@ -157,16 +157,17 @@ term match_Node thm tree.match_rews -text {* Rules about copy function *} -term tree_copy -thm tree.copy_def -thm tree.copy_rews - text {* Rules about take function *} term tree_take thm tree.take_def +thm tree.take_0 +thm tree.take_Suc thm tree.take_rews +thm tree.chain_take +thm tree.take_take +thm tree.deflation_take thm tree.take_lemmas +thm tree.reach thm tree.finite_ind text {* Rules about finiteness predicate *} diff -r 89b945fa0a31 -r 45c9a8278faf src/HOLCF/ex/New_Domain.thy --- a/src/HOLCF/ex/New_Domain.thy Mon Mar 01 23:54:50 2010 -0800 +++ b/src/HOLCF/ex/New_Domain.thy Tue Mar 02 00:34:26 2010 -0800 @@ -51,12 +51,12 @@ thm ltree.reach text {* - The definition of the copy function uses map functions associated with + The definition of the take function uses map functions associated with each type constructor involved in the definition. A map function for the lazy list type has been generated by the new domain package. *} -thm ltree.copy_def +thm ltree.take_rews thm llist_map_def lemma ltree_induct: @@ -67,24 +67,24 @@ assumes Branch: "\f l. \x. P (f\x) \ P (Branch\(llist_map\f\l))" shows "P x" proof - - have "\x. P (fix\ltree_copy\x)" - proof (rule fix_ind) - show "adm (\a. \x. P (a\x))" - by (simp add: adm_subst [OF _ adm]) - next - show "\x. P (\\x)" - by (simp add: bot) - next - fix f :: "'a ltree \ 'a ltree" - assume f: "\x. P (f\x)" - show "\x. P (ltree_copy\f\x)" - apply (rule allI) - apply (case_tac x) - apply (simp add: bot) - apply (simp add: Leaf) - apply (simp add: Branch [OF f]) - done - qed + have "P (\i. ltree_take i\x)" + using adm + proof (rule admD) + fix i + show "P (ltree_take i\x)" + proof (induct i arbitrary: x) + case (0 x) + show "P (ltree_take 0\x)" by (simp add: bot) + next + case (Suc n x) + show "P (ltree_take (Suc n)\x)" + apply (cases x) + apply (simp add: bot) + apply (simp add: Leaf) + apply (simp add: Branch Suc) + done + qed + qed (simp add: ltree.chain_take) thus ?thesis by (simp add: ltree.reach) qed diff -r 89b945fa0a31 -r 45c9a8278faf src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Mon Mar 01 23:54:50 2010 -0800 +++ b/src/HOLCF/ex/Stream.thy Tue Mar 02 00:34:26 2010 -0800 @@ -143,16 +143,10 @@ lemma stream_reach2: "(LUB i. stream_take i$s) = s" -apply (insert stream.reach [of s], erule subst) back -apply (simp add: fix_def2 stream.take_def) -apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym]) -by simp +by (rule stream.reach) lemma chain_stream_take: "chain (%i. stream_take i$s)" -apply (rule chainI) -apply (rule monofun_cfun_fun) -apply (simp add: stream.take_def del: iterate_Suc) -by (rule chainE, simp) +by (simp add: stream.chain_take) lemma stream_take_prefix [simp]: "stream_take n$s << s" apply (insert stream_reach2 [of s]) @@ -259,10 +253,9 @@ lemma stream_ind2: "[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s) |] ==> P x" apply (insert stream.reach [of x],erule subst) -apply (frule adm_impl_admw, rule wfix_ind, auto) -apply (rule adm_subst [THEN adm_impl_admw],auto) +apply (erule admD, rule chain_stream_take) apply (insert stream_finite_ind2 [of P]) -by (simp add: stream.take_def) +by simp