15741

1 
(* Title: HOLCF/Domain.thy


2 
ID: $Id$


3 
Author: Brian Huffman


4 
*)


5 


6 
header {* Domain package *}


7 


8 
theory Domain


9 
imports Ssum Sprod One Up


10 
files


11 
("domain/library.ML")


12 
("domain/syntax.ML")


13 
("domain/axioms.ML")


14 
("domain/theorems.ML")


15 
("domain/extender.ML")


16 
("domain/interface.ML")


17 
begin


18 


19 
defaultsort pcpo


20 


21 
subsection {* Continuous isomorphisms *}


22 


23 
text {* A locale for continuous isomorphisms *}


24 


25 
locale iso =


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


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


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


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


30 


31 
lemma (in iso) swap: "iso rep abs"


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


33 


34 
lemma (in iso) abs_strict: "abs\<cdot>\<bottom> = \<bottom>"


35 
proof 


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


37 
hence "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)


38 
hence "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp


39 
thus ?thesis by (rule UU_I)


40 
qed


41 


42 
lemma (in iso) rep_strict: "rep\<cdot>\<bottom> = \<bottom>"


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


44 


45 
lemma (in iso) abs_defin': "abs\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"


46 
proof 


47 
assume A: "abs\<cdot>z = \<bottom>"


48 
have "z = rep\<cdot>(abs\<cdot>z)" by simp


49 
also have "\<dots> = rep\<cdot>\<bottom>" by (simp only: A)


50 
also note rep_strict


51 
finally show "z = \<bottom>" .


52 
qed


53 


54 
lemma (in iso) rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"


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


56 


57 
lemma (in iso) abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"


58 
by (erule contrapos_nn, erule abs_defin')


59 


60 
lemma (in iso) rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"


61 
by (erule contrapos_nn, erule rep_defin')


62 


63 
lemma (in iso) iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"


64 
proof


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


66 
hence "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp


67 
thus "rep\<cdot>x = y" by simp


68 
next


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


70 
hence "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp


71 
thus "x = abs\<cdot>y" by simp


72 
qed


73 


74 
subsection {* Casedist *}


75 


76 
lemma ex_one_defined_iff:


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


78 
apply safe


79 
apply (rule_tac p=x in oneE)


80 
apply simp


81 
apply simp


82 
apply force


83 
done


84 


85 
lemma ex_up_defined_iff:


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


87 
apply safe


88 
apply (rule_tac p=x in upE1)


89 
apply simp


90 
apply fast


91 
apply (force intro!: defined_up)


92 
done


93 


94 
lemma ex_sprod_defined_iff:


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


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


97 
apply safe


98 
apply (rule_tac p=y in sprodE)


99 
apply simp


100 
apply fast

16217

101 
apply (force intro!: spair_defined)

15741

102 
done


103 


104 
lemma ex_sprod_up_defined_iff:


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


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


107 
apply safe


108 
apply (rule_tac p=y in sprodE)


109 
apply simp


110 
apply (rule_tac p=x in upE1)


111 
apply simp


112 
apply fast

16217

113 
apply (force intro!: spair_defined)

15741

114 
done


115 


116 
lemma ex_ssum_defined_iff:


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


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


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


120 
apply (rule iffI)


121 
apply (erule exE)


122 
apply (erule conjE)


123 
apply (rule_tac p=x in ssumE)


124 
apply simp


125 
apply (rule disjI1, fast)


126 
apply (rule disjI2, fast)


127 
apply (erule disjE)

16217

128 
apply (force intro: sinl_defined)


129 
apply (force intro: sinr_defined)

15741

130 
done


131 


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


133 
by auto


134 


135 
lemmas ex_defined_iffs =


136 
ex_ssum_defined_iff


137 
ex_sprod_up_defined_iff


138 
ex_sprod_defined_iff


139 
ex_up_defined_iff


140 
ex_one_defined_iff


141 


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


143 


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


145 
by auto


146 


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


148 
by rule auto


149 


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


151 
by rule auto


152 


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


154 
by rule auto


155 


156 
lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3


157 


158 


159 
subsection {* Setting up the package *}


160 

16121

161 
ML {*

15741

162 
val iso_intro = thm "iso.intro";


163 
val iso_abs_iso = thm "iso.abs_iso";


164 
val iso_rep_iso = thm "iso.rep_iso";


165 
val iso_abs_strict = thm "iso.abs_strict";


166 
val iso_rep_strict = thm "iso.rep_strict";


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


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


169 
val iso_abs_defined = thm "iso.abs_defined";


170 
val iso_rep_defined = thm "iso.rep_defined";


171 
val iso_iso_swap = thm "iso.iso_swap";


172 


173 
val exh_start = thm "exh_start";


174 
val ex_defined_iffs = thms "ex_defined_iffs";


175 
val exh_casedist0 = thm "exh_casedist0";


176 
val exh_casedists = thms "exh_casedists";


177 
*}


178 


179 
end
