# HG changeset patch # User huffman # Date 1265673241 28800 # Node ID 6088dfd5f9c8cfa91b8a8cd45edb8c9f1e56d7e5 # Parent acbc346e53105ae8b461f426b55ba964e997cde6# Parent a5db9779b0263d5204a9a813351e56a1644f1373 merged diff -r a5db9779b026 -r 6088dfd5f9c8 src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Mon Feb 08 21:28:27 2010 +0100 +++ b/src/HOL/Library/Infinite_Set.thy Mon Feb 08 15:54:01 2010 -0800 @@ -192,10 +192,11 @@ by (auto simp add: infinite_nat_iff_unbounded) qed -lemma nat_infinite [simp]: "infinite (UNIV :: nat set)" +(* duplicates Finite_Set.infinite_UNIV_nat *) +lemma nat_infinite: "infinite (UNIV :: nat set)" by (auto simp add: infinite_nat_iff_unbounded) -lemma nat_not_finite [elim]: "finite (UNIV::nat set) \ R" +lemma nat_not_finite: "finite (UNIV::nat set) \ R" by simp text {* diff -r a5db9779b026 -r 6088dfd5f9c8 src/HOLCF/Fix.thy --- a/src/HOLCF/Fix.thy Mon Feb 08 21:28:27 2010 +0100 +++ b/src/HOLCF/Fix.thy Mon Feb 08 15:54:01 2010 -0800 @@ -73,6 +73,10 @@ apply simp done +lemma iterate_below_fix: "iterate n\f\\ \ fix\f" + unfolding fix_def2 + using chain_iterate by (rule is_ub_thelub) + text {* Kleene's fixed point theorems for continuous functions in pointed omega cpo's diff -r a5db9779b026 -r 6088dfd5f9c8 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Feb 08 21:28:27 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Feb 08 15:54:01 2010 -0800 @@ -593,7 +593,12 @@ 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 pg [ax_copy_def] goal (K tacs) end; + in + SOME (pg [ax_copy_def] goal (K tacs)) + handle + THM (s, _, _) => (trace s; NONE) + | ERROR s => (trace s; NONE) + end; local fun copy_app (con, args) = @@ -605,6 +610,9 @@ (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg) else (%# arg); 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}; @@ -621,18 +629,23 @@ fun one_strict (con, args) = let val goal = mk_trp (dc_copy`UU`(con_app con args) === UU); - val rews = copy_strict :: copy_apps @ con_rews; + val rews = the_list copy_strict @ copy_apps @ con_rews; fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @ [asm_simp_tac (HOLCF_ss addsimps rews) 1]; - in pg [] goal tacs end; + 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 one_strict (filter has_nonlazy_rec cons); + val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons); end; -val copy_rews = copy_strict :: copy_apps @ copy_stricts; +val copy_rews = the_list copy_strict @ copy_apps @ copy_stricts; in thy @@ -706,57 +719,48 @@ val copy_take_defs = (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; val _ = trace " Proving take_stricts..."; - val take_stricts = + fun one_take_strict ((dn, args), _) = let - fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n"); - val goal = mk_trp (foldr1 mk_conj (map one_eq eqs)); - fun tacs ctxt = [ - InductTacs.induct_tac ctxt [[SOME "n"]] 1, - simp_tac iterate_Cprod_ss 1, - asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1]; - in pg copy_take_defs goal tacs end; - - val take_stricts' = rewrite_rule copy_take_defs take_stricts; + 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 $ %%: @{const_name Algebras.zero}) `% x_name n === UU); + 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; - fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1; val _ = trace " Proving take_apps..."; - val take_apps = + fun one_take_app dn (con, args) = let - fun mk_eqn 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; - in Library.foldr mk_all (map vname args, lhs === rhs) end; - fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons; - val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs)); - val simps = filter (has_fewer_prems 1) copy_rews; - fun con_tac ctxt (con, args) = - if nonlazy_rec args = [] - then all_tac - else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN - asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1; - fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons; - fun tacs ctxt = - simp_tac iterate_Cprod_ss 1 :: - InductTacs.induct_tac ctxt [[SOME "n"]] 1 :: - simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 :: - asm_full_simp_tac (HOLCF_ss addsimps simps) 1 :: - TRY (safe_tac HOL_cs) :: - maps (eq_tacs ctxt) eqs; - in pg copy_take_defs goal tacs end; + 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 - (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps); + (take_stricts @ take_0s @ take_apps); end; (* local *) local