# HG changeset patch # User boehmes # Date 1292880446 -3600 # Node ID b6242168e7faf0f8e09ca9fdaeec4e356cbe1121 # Parent 6792a5c92a580e14344c4144f4fb398d96eafd24# Parent 874dbac157ee50349e99ce9aa52b4d642774e342 merged diff -r 6792a5c92a58 -r b6242168e7fa src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Mon Dec 20 22:02:57 2010 +0100 +++ b/src/HOL/HOLCF/Cfun.thy Mon Dec 20 22:27:26 2010 +0100 @@ -142,16 +142,19 @@ using @{text beta_cfun} as a simp rule. The advantage of the simproc is that it can avoid deeply-nested calls to the simplifier that would otherwise be caused by large continuity side conditions. + + Update: The simproc now uses rule @{text Abs_cfun_inverse2} instead + of @{text beta_cfun}, to avoid problems with eta-contraction. *} -simproc_setup beta_cfun_proc ("Abs_cfun f\x") = {* +simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = {* fn phi => fn ss => fn ct => let val dest = Thm.dest_comb; - val (f, x) = (apfst (snd o dest o snd o dest) o dest) ct; + val f = (snd o dest o snd o dest) ct; val [T, U] = Thm.dest_ctyp (ctyp_of_term f); - val tr = instantiate' [SOME T, SOME U] [SOME f, SOME x] - (mk_meta_eq @{thm beta_cfun}); + val tr = instantiate' [SOME T, SOME U] [SOME f] + (mk_meta_eq @{thm Abs_cfun_inverse2}); val rules = Cont2ContData.get (Simplifier.the_context ss); val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules)); in SOME (perhaps (SINGLE (tac 1)) tr) end @@ -251,10 +254,7 @@ lemma lub_LAM: "\\x. chain (\i. F i x); \i. cont (\x. F i x)\ \ (\i. \ x. F i x) = (\ x. \i. F i x)" -apply (simp add: lub_cfun) -apply (simp add: Abs_cfun_inverse2) -apply (simp add: lub_fun ch2ch_lambda) -done +by (simp add: lub_cfun lub_fun ch2ch_lambda) lemmas lub_distribs = lub_APP lub_LAM diff -r 6792a5c92a58 -r b6242168e7fa src/HOL/HOLCF/Fix.thy --- a/src/HOL/HOLCF/Fix.thy Mon Dec 20 22:02:57 2010 +0100 +++ b/src/HOL/HOLCF/Fix.thy Mon Dec 20 22:27:26 2010 +0100 @@ -148,6 +148,10 @@ apply (rule nat_induct, simp_all) done +lemma cont_fix_ind: + "\cont F; adm P; P \; \x. P x \ P (F x)\ \ P (fix\(Abs_cfun F))" +by (simp add: fix_ind) + lemma def_fix_ind: "\f \ fix\F; adm P; P \; \x. P x \ P (F\x)\ \ P f" by (simp add: fix_ind) @@ -190,6 +194,14 @@ by (simp add: fix_def2) qed +lemma cont_parallel_fix_ind: + assumes "cont F" and "cont G" + assumes "adm (\x. P (fst x) (snd x))" + assumes "P \ \" + assumes "\x y. P x y \ P (F x) (G y)" + shows "P (fix\(Abs_cfun F)) (fix\(Abs_cfun G))" +by (rule parallel_fix_ind, simp_all add: assms) + subsection {* Fixed-points on product types *} text {* diff -r 6792a5c92a58 -r b6242168e7fa src/HOL/HOLCF/Library/List_Predomain.thy --- a/src/HOL/HOLCF/Library/List_Predomain.thy Mon Dec 20 22:02:57 2010 +0100 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy Mon Dec 20 22:27:26 2010 +0100 @@ -96,13 +96,6 @@ subsection {* Lists are a predomain *} -definition udefl :: "udom defl \ udom u defl" - where "udefl = defl_fun1 (strictify\up) (fup\ID) ID" - -lemma cast_udefl: - "cast\(udefl\t) = strictify\up oo cast\t oo fup\ID" -unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up) - definition list_liftdefl :: "udom u defl \ udom u defl" where "list_liftdefl = (\ a. udefl\(slist_defl\(u_defl\a)))" @@ -110,9 +103,6 @@ using isodefl_slist [where fa="cast\a" and da="a"] unfolding isodefl_def by simp -lemma u_emb_bottom: "u_emb\\ = \" -by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u]) - instantiation list :: (predomain) predomain begin @@ -139,37 +129,27 @@ end +subsection {* Configuring domain package to work with list type *} + lemma liftdefl_list [domain_defl_simps]: "LIFTDEFL('a::predomain list) = list_liftdefl\LIFTDEFL('a)" by (rule liftdefl_list_def) -subsection {* Continuous map operation for lists *} - -definition - list_map :: "('a::predomain \ 'b::predomain) \ 'a list \ 'b list" -where - "list_map = (\ f xs. map (\x. f\x) xs)" +abbreviation list_map :: "('a::cpo \ 'b::cpo) \ 'a list \ 'b list" + where "list_map f \ Abs_cfun (map (Rep_cfun f))" -lemma list_map_simps [simp]: - "list_map\f\[] = []" - "list_map\f\(x # xs) = f\x # list_map\f\xs" -unfolding list_map_def by simp_all - -lemma list_map_ID [domain_map_ID]: "list_map\ID = ID" -unfolding list_map_def ID_def -by (simp add: Abs_cfun_inverse cfun_def) +lemma list_map_ID [domain_map_ID]: "list_map ID = ID" +by (simp add: ID_def) lemma deflation_list_map [domain_deflation]: - "deflation d \ deflation (list_map\d)" + "deflation d \ deflation (list_map d)" apply default apply (induct_tac x, simp_all add: deflation.idem) apply (induct_tac x, simp_all add: deflation.below) done -subsection {* Configuring list type to work with domain package *} - lemma encode_list_u_map: - "encode_list_u\(u_map\(list_map\f)\(decode_list_u\xs)) + "encode_list_u\(u_map\(list_map f)\(decode_list_u\xs)) = slist_map\(u_map\f)\xs" apply (induct xs, simp, simp) apply (case_tac a, simp, rename_tac b) @@ -180,7 +160,7 @@ lemma isodefl_list_u [domain_isodefl]: fixes d :: "'a::predomain \ 'a" assumes "isodefl' d t" - shows "isodefl' (list_map\d) (list_liftdefl\t)" + shows "isodefl' (list_map d) (list_liftdefl\t)" using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl) apply (simp add: cfcomp1 encode_list_u_map) diff -r 6792a5c92a58 -r b6242168e7fa src/HOL/HOLCF/Library/Option_Cpo.thy --- a/src/HOL/HOLCF/Library/Option_Cpo.thy Mon Dec 20 22:02:57 2010 +0100 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Mon Dec 20 22:27:26 2010 +0100 @@ -149,6 +149,14 @@ shows "cont (\x. case z of None \ f x | Some a \ g x a)" using assms by (cases z) auto +text {* Continuity rule for map. *} + +lemma cont2cont_option_map [simp, cont2cont]: + assumes f: "cont (\(x, y). f x y)" + assumes g: "cont (\x. g x)" + shows "cont (\x. Option.map (\y. f x y) (g x))" +using assms by (simp add: prod_cont_iff Option.map_def) + subsection {* Compactness and chain-finiteness *} lemma compact_None [simp]: "compact None" @@ -182,7 +190,7 @@ instance option :: (discrete_cpo) discrete_cpo by intro_classes (simp add: below_option_def split: option.split) -subsection {* Using option types with fixrec *} +subsection {* Using option types with Fixrec *} definition "match_None = (\ x k. case x of None \ k | Some a \ Fixrec.fail)" @@ -247,4 +255,38 @@ end +subsection {* Configuring domain package to work with option type *} + +lemma liftdefl_option [domain_defl_simps]: + "LIFTDEFL('a::predomain option) = LIFTDEFL(unit + 'a)" +by (rule liftdefl_option_def) + +abbreviation option_map + where "option_map f \ Abs_cfun (Option.map (Rep_cfun f))" + +lemma option_map_ID [domain_map_ID]: "option_map ID = ID" +by (simp add: ID_def cfun_eq_iff Option.map.identity) + +lemma deflation_option_map [domain_deflation]: + "deflation d \ deflation (option_map d)" +apply default +apply (induct_tac x, simp_all add: deflation.idem) +apply (induct_tac x, simp_all add: deflation.below) +done + +lemma encode_option_option_map: + "encode_option\(Option.map (\x. f\x) (decode_option\x)) = sum_map' ID f\x" +by (induct x, simp_all add: decode_option_def encode_option_def) + +lemma isodefl_option [domain_isodefl]: + assumes "isodefl' d t" + shows "isodefl' (option_map d) (sum_liftdefl\(pdefl\DEFL(unit))\t)" +using isodefl_sum [OF isodefl_LIFTDEFL [where 'a=unit] assms] +unfolding isodefl'_def liftemb_option_def liftprj_option_def liftdefl_eq +by (simp add: cfcomp1 u_map_map encode_option_option_map) + +setup {* + Domain_Take_Proofs.add_rec_type (@{type_name "option"}, [true]) +*} + end diff -r 6792a5c92a58 -r b6242168e7fa src/HOL/HOLCF/Library/Sum_Cpo.thy --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Mon Dec 20 22:02:57 2010 +0100 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Mon Dec 20 22:27:26 2010 +0100 @@ -175,6 +175,18 @@ shows "cont (\x. case h x of Inl a \ f x a | Inr b \ g x b)" using assms by (simp add: cont2cont_sum_case prod_cont_iff) +text {* Continuity of map function. *} + +lemma sum_map_eq: "sum_map f g = sum_case (\a. Inl (f a)) (\b. Inr (g b))" +by (rule ext, case_tac x, simp_all) + +lemma cont2cont_sum_map [simp, cont2cont]: + assumes f: "cont (\(x, y). f x y)" + assumes g: "cont (\(x, y). g x y)" + assumes h: "cont (\x. h x)" + shows "cont (\x. sum_map (\y. f x y) (\y. g x y) (h x))" +using assms by (simp add: sum_map_eq prod_cont_iff) + subsection {* Compactness and chain-finiteness *} lemma compact_Inl: "compact a \ compact (Inl a)" @@ -260,6 +272,11 @@ apply (rename_tac b, case_tac b, simp, simp) done +text {* A deflation combinator for making unpointed types *} + +definition udefl :: "udom defl \ udom u defl" + where "udefl = defl_fun1 (strictify\up) (fup\ID) ID" + lemma ep_pair_strictify_up: "ep_pair (strictify\up) (fup\ID)" apply (rule ep_pair.intro) @@ -267,20 +284,32 @@ apply (case_tac y, simp, simp add: strictify_conv_if) done +lemma cast_udefl: + "cast\(udefl\t) = strictify\up oo cast\t oo fup\ID" +unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up) + +definition sum_liftdefl :: "udom u defl \ udom u defl \ udom u defl" + where "sum_liftdefl = (\ a b. udefl\(ssum_defl\(u_defl\a)\(u_defl\b)))" + +lemma u_emb_bottom: "u_emb\\ = \" +by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u]) + +(* definition sum_liftdefl :: "udom u defl \ udom u defl \ udom u defl" where "sum_liftdefl = defl_fun2 (u_map\emb oo strictify\up) (fup\ID oo u_map\prj) ssum_map" +*) instantiation sum :: (predomain, predomain) predomain begin definition - "liftemb = (u_map\emb oo strictify\up) oo - (ssum_map\liftemb\liftemb oo encode_sum_u)" + "liftemb = (strictify\up oo ssum_emb) oo + (ssum_map\(u_emb oo liftemb)\(u_emb oo liftemb) oo encode_sum_u)" definition - "liftprj = (decode_sum_u oo ssum_map\liftprj\liftprj) oo - (fup\ID oo u_map\prj)" + "liftprj = (decode_sum_u oo ssum_map\(liftprj oo u_prj)\(liftprj oo u_prj)) + oo (ssum_prj oo fup\ID)" definition "liftdefl (t::('a + 'b) itself) = sum_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)" @@ -288,17 +317,56 @@ instance proof show "ep_pair liftemb (liftprj :: udom u \ ('a + 'b) u)" unfolding liftemb_sum_def liftprj_sum_def - by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u_map ep_pair_emb_prj - ep_pair_strictify_up predomain_ep, simp add: ep_pair.intro) + by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u predomain_ep + ep_pair_ssum ep_pair_strictify_up, simp add: ep_pair.intro) show "cast\LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \ ('a + 'b) u)" unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def - apply (subst sum_liftdefl_def, subst cast_defl_fun2) - apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj - ep_pair_strictify_up) - apply (erule (1) finite_deflation_ssum_map) - by (simp add: cast_liftdefl cfcomp1 ssum_map_map) + by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl + cast_liftdefl cfcomp1 ssum_map_map u_emb_bottom) qed end +subsection {* Configuring domain package to work with sum type *} + +lemma liftdefl_sum [domain_defl_simps]: + "LIFTDEFL('a::predomain + 'b::predomain) = + sum_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)" +by (rule liftdefl_sum_def) + +abbreviation sum_map' + where "sum_map' f g \ Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))" + +lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID" +by (simp add: ID_def cfun_eq_iff sum_map.identity) + +lemma deflation_sum_map [domain_deflation]: + "\deflation d1; deflation d2\ \ deflation (sum_map' d1 d2)" +apply default +apply (induct_tac x, simp_all add: deflation.idem) +apply (induct_tac x, simp_all add: deflation.below) +done + +lemma encode_sum_u_sum_map: + "encode_sum_u\(u_map\(sum_map' f g)\(decode_sum_u\x)) + = ssum_map\(u_map\f)\(u_map\g)\x" +apply (induct x, simp add: decode_sum_u_def encode_sum_u_def) +apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def) +apply (case_tac y, simp, simp add: decode_sum_u_def encode_sum_u_def) +done + +lemma isodefl_sum [domain_isodefl]: + fixes d :: "'a::predomain \ 'a" + assumes "isodefl' d1 t1" and "isodefl' d2 t2" + shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\t1\t2)" +using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def +apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl) +apply (simp add: cfcomp1 encode_sum_u_sum_map) +apply (simp add: ssum_map_map u_emb_bottom) +done + +setup {* + Domain_Take_Proofs.add_rec_type (@{type_name "sum"}, [true, true]) +*} + end diff -r 6792a5c92a58 -r b6242168e7fa src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Dec 20 22:02:57 2010 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Dec 20 22:27:26 2010 +0100 @@ -20,6 +20,7 @@ map_consts : term list, map_apply_thms : thm list, map_unfold_thms : thm list, + map_cont_thm : thm, deflation_map_thms : thm list } * theory @@ -135,7 +136,7 @@ fun add_fixdefs (spec : (binding * term) list) - (thy : theory) : (thm list * thm list) * theory = + (thy : theory) : (thm list * thm list * thm) * theory = let val binds = map fst spec val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec) @@ -199,7 +200,7 @@ (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (mk_unfold_thms unfold_binds tuple_unfold_thm) thy in - ((proj_thms, unfold_thms), thy) + ((proj_thms, unfold_thms, cont_thm), thy) end @@ -302,7 +303,7 @@ (* register recursive definition of map functions *) val map_binds = map (Binding.suffix_name "_map") dbinds - val ((map_apply_thms, map_unfold_thms), thy) = + val ((map_apply_thms, map_unfold_thms, map_cont_thm), thy) = add_fixdefs (map_binds ~~ map_specs) thy (* prove deflation theorems for map functions *) @@ -320,13 +321,13 @@ val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns val goals = map mk_goal (map_consts ~~ dom_eqns) val goal = mk_trp (foldr1 HOLogic.mk_conj goals) - val start_thms = - @{thm split_def} :: map_apply_thms val adm_rules = @{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 tuple_rules = + @{thms split_def fst_conv snd_conv} val deflation_rules = @{thms conjI deflation_ID} @ deflation_abs_rep_thms @@ -334,12 +335,11 @@ in Goal.prove_global thy [] assms goal (fn {prems, ...} => EVERY - [simp_tac (HOL_basic_ss addsimps start_thms) 1, - rtac @{thm fix_ind} 1, + [rewrite_goals_tac map_apply_thms, + rtac (map_cont_thm RS @{thm cont_fix_ind}) 1, REPEAT (resolve_tac adm_rules 1), simp_tac (HOL_basic_ss addsimps bottom_rules) 1, - simp_tac beta_ss 1, - simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, + simp_tac (HOL_basic_ss addsimps tuple_rules) 1, REPEAT (etac @{thm conjE} 1), REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)]) end @@ -376,6 +376,7 @@ map_consts = map_consts, map_apply_thms = map_apply_thms, map_unfold_thms = map_unfold_thms, + map_cont_thm = map_cont_thm, deflation_map_thms = deflation_map_thms } in @@ -520,7 +521,7 @@ (* register recursive definition of deflation combinators *) val defl_binds = map (Binding.suffix_name "_defl") dbinds - val ((defl_apply_thms, defl_unfold_thms), thy) = + val ((defl_apply_thms, defl_unfold_thms, defl_cont_thm), thy) = add_fixdefs (defl_binds ~~ defl_specs) thy (* define types using deflation combinators *) @@ -611,7 +612,7 @@ val (map_info, thy) = define_map_functions (dbinds ~~ iso_infos) thy val { map_consts, map_apply_thms, map_unfold_thms, - deflation_map_thms } = map_info + map_cont_thm, deflation_map_thms } = map_info (* prove isodefl rules for map functions *) val isodefl_thm = @@ -635,12 +636,12 @@ val assms = (map mk_assm o snd o hd) defl_flagss val goals = map mk_goal (map_consts ~~ dom_eqns) val goal = mk_trp (foldr1 HOLogic.mk_conj goals) - val start_thms = - @{thm split_def} :: defl_apply_thms @ map_apply_thms val adm_rules = @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id} val bottom_rules = @{thms fst_strict snd_strict isodefl_bottom simp_thms} + val tuple_rules = + @{thms split_def fst_conv snd_conv} val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy val map_ID_simps = map (fn th => th RS sym) map_ID_thms val isodefl_rules = @@ -650,14 +651,12 @@ in Goal.prove_global thy [] assms goal (fn {prems, ...} => EVERY - [simp_tac (HOL_basic_ss addsimps start_thms) 1, - (* FIXME: how reliable is unification here? *) - (* Maybe I should instantiate the rule. *) - rtac @{thm parallel_fix_ind} 1, + [rewrite_goals_tac (defl_apply_thms @ map_apply_thms), + rtac (@{thm cont_parallel_fix_ind} + OF [defl_cont_thm, map_cont_thm]) 1, REPEAT (resolve_tac adm_rules 1), simp_tac (HOL_basic_ss addsimps bottom_rules) 1, - simp_tac beta_ss 1, - simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, + simp_tac (HOL_basic_ss addsimps tuple_rules) 1, simp_tac (HOL_basic_ss addsimps map_ID_simps) 1, REPEAT (etac @{thm conjE} 1), REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])