--- 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\<cdot>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:
"\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
\<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>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
--- 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:
+ "\<lbrakk>cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>(Abs_cfun F))"
+by (simp add: fix_ind)
+
lemma def_fix_ind:
"\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> 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 (\<lambda>x. P (fst x) (snd x))"
+ assumes "P \<bottom> \<bottom>"
+ assumes "\<And>x y. P x y \<Longrightarrow> P (F x) (G y)"
+ shows "P (fix\<cdot>(Abs_cfun F)) (fix\<cdot>(Abs_cfun G))"
+by (rule parallel_fix_ind, simp_all add: assms)
+
subsection {* Fixed-points on product types *}
text {*
--- 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 \<rightarrow> udom u defl"
- where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID"
-
-lemma cast_udefl:
- "cast\<cdot>(udefl\<cdot>t) = strictify\<cdot>up oo cast\<cdot>t oo fup\<cdot>ID"
-unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up)
-
definition list_liftdefl :: "udom u defl \<rightarrow> udom u defl"
where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_defl\<cdot>a)))"
@@ -110,9 +103,6 @@
using isodefl_slist [where fa="cast\<cdot>a" and da="a"]
unfolding isodefl_def by simp
-lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>"
-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\<cdot>LIFTDEFL('a)"
by (rule liftdefl_list_def)
-subsection {* Continuous map operation for lists *}
-
-definition
- list_map :: "('a::predomain \<rightarrow> 'b::predomain) \<rightarrow> 'a list \<rightarrow> 'b list"
-where
- "list_map = (\<Lambda> f xs. map (\<lambda>x. f\<cdot>x) xs)"
+abbreviation list_map :: "('a::cpo \<rightarrow> 'b::cpo) \<Rightarrow> 'a list \<rightarrow> 'b list"
+ where "list_map f \<equiv> Abs_cfun (map (Rep_cfun f))"
-lemma list_map_simps [simp]:
- "list_map\<cdot>f\<cdot>[] = []"
- "list_map\<cdot>f\<cdot>(x # xs) = f\<cdot>x # list_map\<cdot>f\<cdot>xs"
-unfolding list_map_def by simp_all
-
-lemma list_map_ID [domain_map_ID]: "list_map\<cdot>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 \<Longrightarrow> deflation (list_map\<cdot>d)"
+ "deflation d \<Longrightarrow> 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\<cdot>(u_map\<cdot>(list_map\<cdot>f)\<cdot>(decode_list_u\<cdot>xs))
+ "encode_list_u\<cdot>(u_map\<cdot>(list_map f)\<cdot>(decode_list_u\<cdot>xs))
= slist_map\<cdot>(u_map\<cdot>f)\<cdot>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 \<rightarrow> 'a"
assumes "isodefl' d t"
- shows "isodefl' (list_map\<cdot>d) (list_liftdefl\<cdot>t)"
+ shows "isodefl' (list_map d) (list_liftdefl\<cdot>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)
--- 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 (\<lambda>x. case z of None \<Rightarrow> f x | Some a \<Rightarrow> g x a)"
using assms by (cases z) auto
+text {* Continuity rule for map. *}
+
+lemma cont2cont_option_map [simp, cont2cont]:
+ assumes f: "cont (\<lambda>(x, y). f x y)"
+ assumes g: "cont (\<lambda>x. g x)"
+ shows "cont (\<lambda>x. Option.map (\<lambda>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 = (\<Lambda> x k. case x of None \<Rightarrow> k | Some a \<Rightarrow> 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 \<equiv> 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 \<Longrightarrow> 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\<cdot>(Option.map (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>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\<cdot>(pdefl\<cdot>DEFL(unit))\<cdot>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
--- 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 (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> 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 (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
+by (rule ext, case_tac x, simp_all)
+
+lemma cont2cont_sum_map [simp, cont2cont]:
+ assumes f: "cont (\<lambda>(x, y). f x y)"
+ assumes g: "cont (\<lambda>(x, y). g x y)"
+ assumes h: "cont (\<lambda>x. h x)"
+ shows "cont (\<lambda>x. sum_map (\<lambda>y. f x y) (\<lambda>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 \<Longrightarrow> 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 \<rightarrow> udom u defl"
+ where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID"
+
lemma ep_pair_strictify_up:
"ep_pair (strictify\<cdot>up) (fup\<cdot>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\<cdot>(udefl\<cdot>t) = strictify\<cdot>up oo cast\<cdot>t oo fup\<cdot>ID"
+unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up)
+
+definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
+ where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>b)))"
+
+lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>"
+by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u])
+
+(*
definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
where "sum_liftdefl = defl_fun2 (u_map\<cdot>emb oo strictify\<cdot>up)
(fup\<cdot>ID oo u_map\<cdot>prj) ssum_map"
+*)
instantiation sum :: (predomain, predomain) predomain
begin
definition
- "liftemb = (u_map\<cdot>emb oo strictify\<cdot>up) oo
- (ssum_map\<cdot>liftemb\<cdot>liftemb oo encode_sum_u)"
+ "liftemb = (strictify\<cdot>up oo ssum_emb) oo
+ (ssum_map\<cdot>(u_emb oo liftemb)\<cdot>(u_emb oo liftemb) oo encode_sum_u)"
definition
- "liftprj = (decode_sum_u oo ssum_map\<cdot>liftprj\<cdot>liftprj) oo
- (fup\<cdot>ID oo u_map\<cdot>prj)"
+ "liftprj = (decode_sum_u oo ssum_map\<cdot>(liftprj oo u_prj)\<cdot>(liftprj oo u_prj))
+ oo (ssum_prj oo fup\<cdot>ID)"
definition
"liftdefl (t::('a + 'b) itself) = sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
@@ -288,17 +317,56 @@
instance proof
show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('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\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('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\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
+by (rule liftdefl_sum_def)
+
+abbreviation sum_map'
+ where "sum_map' f g \<equiv> 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]:
+ "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> 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\<cdot>(u_map\<cdot>(sum_map' f g)\<cdot>(decode_sum_u\<cdot>x))
+ = ssum_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>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 \<rightarrow> 'a"
+ assumes "isodefl' d1 t1" and "isodefl' d2 t2"
+ shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>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
--- 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)])