15741

1 
(* Title: HOLCF/Domain.thy


2 
ID: $Id$


3 
Author: Brian Huffman


4 
*)


5 


6 
header {* Domain package *}


7 


8 
theory Domain

16230

9 
imports Ssum Sprod Up One Tr Fixrec

15741

10 
begin


11 


12 
defaultsort pcpo


13 

23376

14 

15741

15 
subsection {* Continuous isomorphisms *}


16 


17 
text {* A locale for continuous isomorphisms *}


18 


19 
locale iso =


20 
fixes abs :: "'a \<rightarrow> 'b"


21 
fixes rep :: "'b \<rightarrow> 'a"


22 
assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"


23 
assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"

23376

24 
begin

15741

25 

23376

26 
lemma swap: "iso rep abs"


27 
by (rule iso.intro [OF rep_iso abs_iso])

15741

28 

23376

29 
lemma abs_less: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"

17835

30 
proof


31 
assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"

23376

32 
then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)


33 
then show "x \<sqsubseteq> y" by simp

17835

34 
next


35 
assume "x \<sqsubseteq> y"

23376

36 
then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)

17835

37 
qed


38 

23376

39 
lemma rep_less: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"


40 
by (rule iso.abs_less [OF swap])

17835

41 

23376

42 
lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"


43 
by (simp add: po_eq_conv abs_less)

17835

44 

23376

45 
lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"


46 
by (rule iso.abs_eq [OF swap])

17835

47 

23376

48 
lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>"

15741

49 
proof 


50 
have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..

23376

51 
then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)


52 
then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp


53 
then show ?thesis by (rule UU_I)

15741

54 
qed


55 

23376

56 
lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"


57 
by (rule iso.abs_strict [OF swap])

15741

58 

23376

59 
lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>"

15741

60 
proof 

17835

61 
have "x = rep\<cdot>(abs\<cdot>x)" by simp


62 
also assume "abs\<cdot>x = \<bottom>"

15741

63 
also note rep_strict

17835

64 
finally show "x = \<bottom>" .

15741

65 
qed


66 

23376

67 
lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"


68 
by (rule iso.abs_defin' [OF swap])

15741

69 

23376

70 
lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"


71 
by (erule contrapos_nn, erule abs_defin')

15741

72 

23376

73 
lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"


74 
by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)

17835

75 

23376

76 
lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"


77 
by (auto elim: abs_defin' intro: abs_strict)

17835

78 

23376

79 
lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"


80 
by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)

15741

81 

17836

82 
lemma (in iso) compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"


83 
proof (unfold compact_def)


84 
assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"


85 
with cont_Rep_CFun2


86 
have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)

23376

87 
then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_less by simp

17836

88 
qed


89 

23376

90 
lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"


91 
by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms)

17836

92 

23376

93 
lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)"


94 
by (rule compact_rep_rev) simp

17836

95 

23376

96 
lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)"


97 
by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms)

17836

98 

23376

99 
lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"

15741

100 
proof


101 
assume "x = abs\<cdot>y"

23376

102 
then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp


103 
then show "rep\<cdot>x = y" by simp

15741

104 
next


105 
assume "rep\<cdot>x = y"

23376

106 
then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp


107 
then show "x = abs\<cdot>y" by simp

15741

108 
qed


109 

23376

110 
end


111 


112 

15741

113 
subsection {* Casedist *}


114 


115 
lemma ex_one_defined_iff:


116 
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"


117 
apply safe


118 
apply (rule_tac p=x in oneE)


119 
apply simp


120 
apply simp


121 
apply force

23376

122 
done

15741

123 


124 
lemma ex_up_defined_iff:


125 
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"


126 
apply safe

16754

127 
apply (rule_tac p=x in upE)

15741

128 
apply simp


129 
apply fast

16320

130 
apply (force intro!: up_defined)

23376

131 
done

15741

132 


133 
lemma ex_sprod_defined_iff:


134 
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) =


135 
(\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"


136 
apply safe


137 
apply (rule_tac p=y in sprodE)


138 
apply simp


139 
apply fast

16217

140 
apply (force intro!: spair_defined)

23376

141 
done

15741

142 


143 
lemma ex_sprod_up_defined_iff:


144 
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) =


145 
(\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"


146 
apply safe


147 
apply (rule_tac p=y in sprodE)


148 
apply simp

16754

149 
apply (rule_tac p=x in upE)

15741

150 
apply simp


151 
apply fast

16217

152 
apply (force intro!: spair_defined)

23376

153 
done

15741

154 


155 
lemma ex_ssum_defined_iff:


156 
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) =


157 
((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>


158 
(\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"


159 
apply (rule iffI)


160 
apply (erule exE)


161 
apply (erule conjE)


162 
apply (rule_tac p=x in ssumE)


163 
apply simp


164 
apply (rule disjI1, fast)


165 
apply (rule disjI2, fast)


166 
apply (erule disjE)

17835

167 
apply force


168 
apply force

23376

169 
done

15741

170 


171 
lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"

23376

172 
by auto

15741

173 


174 
lemmas ex_defined_iffs =


175 
ex_ssum_defined_iff


176 
ex_sprod_up_defined_iff


177 
ex_sprod_defined_iff


178 
ex_up_defined_iff


179 
ex_one_defined_iff


180 


181 
text {* Rules for turning exh into casedist *}


182 


183 
lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)

23376

184 
by auto

15741

185 


186 
lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"

23376

187 
by rule auto

15741

188 


189 
lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"

23376

190 
by rule auto

15741

191 


192 
lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"

23376

193 
by rule auto

15741

194 


195 
lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3


196 


197 


198 
subsection {* Setting up the package *}


199 

16121

200 
ML {*

15741

201 
val iso_intro = thm "iso.intro";


202 
val iso_abs_iso = thm "iso.abs_iso";


203 
val iso_rep_iso = thm "iso.rep_iso";


204 
val iso_abs_strict = thm "iso.abs_strict";


205 
val iso_rep_strict = thm "iso.rep_strict";


206 
val iso_abs_defin' = thm "iso.abs_defin'";


207 
val iso_rep_defin' = thm "iso.rep_defin'";


208 
val iso_abs_defined = thm "iso.abs_defined";


209 
val iso_rep_defined = thm "iso.rep_defined";

17839

210 
val iso_compact_abs = thm "iso.compact_abs";


211 
val iso_compact_rep = thm "iso.compact_rep";

15741

212 
val iso_iso_swap = thm "iso.iso_swap";


213 


214 
val exh_start = thm "exh_start";


215 
val ex_defined_iffs = thms "ex_defined_iffs";


216 
val exh_casedist0 = thm "exh_casedist0";


217 
val exh_casedists = thms "exh_casedists";


218 
*}


219 


220 
end
