|
1 (* Title: HOLCF/Domain.thy |
|
2 ID: $Id$ |
|
3 Author: Brian Huffman |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 *) |
|
6 |
|
7 header {* Domain package *} |
|
8 |
|
9 theory Domain |
|
10 imports Ssum Sprod One Up |
|
11 files |
|
12 ("domain/library.ML") |
|
13 ("domain/syntax.ML") |
|
14 ("domain/axioms.ML") |
|
15 ("domain/theorems.ML") |
|
16 ("domain/extender.ML") |
|
17 ("domain/interface.ML") |
|
18 begin |
|
19 |
|
20 defaultsort pcpo |
|
21 |
|
22 subsection {* Continuous isomorphisms *} |
|
23 |
|
24 text {* A locale for continuous isomorphisms *} |
|
25 |
|
26 locale iso = |
|
27 fixes abs :: "'a \<rightarrow> 'b" |
|
28 fixes rep :: "'b \<rightarrow> 'a" |
|
29 assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x" |
|
30 assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y" |
|
31 |
|
32 lemma (in iso) swap: "iso rep abs" |
|
33 by (rule iso.intro [OF rep_iso abs_iso]) |
|
34 |
|
35 lemma (in iso) abs_strict: "abs\<cdot>\<bottom> = \<bottom>" |
|
36 proof - |
|
37 have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" .. |
|
38 hence "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg) |
|
39 hence "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp |
|
40 thus ?thesis by (rule UU_I) |
|
41 qed |
|
42 |
|
43 lemma (in iso) rep_strict: "rep\<cdot>\<bottom> = \<bottom>" |
|
44 by (rule iso.abs_strict [OF swap]) |
|
45 |
|
46 lemma (in iso) abs_defin': "abs\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>" |
|
47 proof - |
|
48 assume A: "abs\<cdot>z = \<bottom>" |
|
49 have "z = rep\<cdot>(abs\<cdot>z)" by simp |
|
50 also have "\<dots> = rep\<cdot>\<bottom>" by (simp only: A) |
|
51 also note rep_strict |
|
52 finally show "z = \<bottom>" . |
|
53 qed |
|
54 |
|
55 lemma (in iso) rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>" |
|
56 by (rule iso.abs_defin' [OF swap]) |
|
57 |
|
58 lemma (in iso) abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>" |
|
59 by (erule contrapos_nn, erule abs_defin') |
|
60 |
|
61 lemma (in iso) rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>" |
|
62 by (erule contrapos_nn, erule rep_defin') |
|
63 |
|
64 lemma (in iso) iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)" |
|
65 proof |
|
66 assume "x = abs\<cdot>y" |
|
67 hence "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp |
|
68 thus "rep\<cdot>x = y" by simp |
|
69 next |
|
70 assume "rep\<cdot>x = y" |
|
71 hence "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp |
|
72 thus "x = abs\<cdot>y" by simp |
|
73 qed |
|
74 |
|
75 subsection {* Casedist *} |
|
76 |
|
77 lemma ex_one_defined_iff: |
|
78 "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE" |
|
79 apply safe |
|
80 apply (rule_tac p=x in oneE) |
|
81 apply simp |
|
82 apply simp |
|
83 apply force |
|
84 done |
|
85 |
|
86 lemma ex_up_defined_iff: |
|
87 "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))" |
|
88 apply safe |
|
89 apply (rule_tac p=x in upE1) |
|
90 apply simp |
|
91 apply fast |
|
92 apply (force intro!: defined_up) |
|
93 done |
|
94 |
|
95 lemma ex_sprod_defined_iff: |
|
96 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
|
97 (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)" |
|
98 apply safe |
|
99 apply (rule_tac p=y in sprodE) |
|
100 apply simp |
|
101 apply fast |
|
102 apply (force intro!: defined_spair) |
|
103 done |
|
104 |
|
105 lemma ex_sprod_up_defined_iff: |
|
106 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
|
107 (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)" |
|
108 apply safe |
|
109 apply (rule_tac p=y in sprodE) |
|
110 apply simp |
|
111 apply (rule_tac p=x in upE1) |
|
112 apply simp |
|
113 apply fast |
|
114 apply (force intro!: defined_spair) |
|
115 done |
|
116 |
|
117 lemma ex_ssum_defined_iff: |
|
118 "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = |
|
119 ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or> |
|
120 (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))" |
|
121 apply (rule iffI) |
|
122 apply (erule exE) |
|
123 apply (erule conjE) |
|
124 apply (rule_tac p=x in ssumE) |
|
125 apply simp |
|
126 apply (rule disjI1, fast) |
|
127 apply (rule disjI2, fast) |
|
128 apply (erule disjE) |
|
129 apply (force intro: defined_sinl) |
|
130 apply (force intro: defined_sinr) |
|
131 done |
|
132 |
|
133 lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)" |
|
134 by auto |
|
135 |
|
136 lemmas ex_defined_iffs = |
|
137 ex_ssum_defined_iff |
|
138 ex_sprod_up_defined_iff |
|
139 ex_sprod_defined_iff |
|
140 ex_up_defined_iff |
|
141 ex_one_defined_iff |
|
142 |
|
143 text {* Rules for turning exh into casedist *} |
|
144 |
|
145 lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *) |
|
146 by auto |
|
147 |
|
148 lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)" |
|
149 by rule auto |
|
150 |
|
151 lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)" |
|
152 by rule auto |
|
153 |
|
154 lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)" |
|
155 by rule auto |
|
156 |
|
157 lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3 |
|
158 |
|
159 |
|
160 subsection {* Setting up the package *} |
|
161 |
|
162 ML_setup {* |
|
163 val iso_intro = thm "iso.intro"; |
|
164 val iso_abs_iso = thm "iso.abs_iso"; |
|
165 val iso_rep_iso = thm "iso.rep_iso"; |
|
166 val iso_abs_strict = thm "iso.abs_strict"; |
|
167 val iso_rep_strict = thm "iso.rep_strict"; |
|
168 val iso_abs_defin' = thm "iso.abs_defin'"; |
|
169 val iso_rep_defin' = thm "iso.rep_defin'"; |
|
170 val iso_abs_defined = thm "iso.abs_defined"; |
|
171 val iso_rep_defined = thm "iso.rep_defined"; |
|
172 val iso_iso_swap = thm "iso.iso_swap"; |
|
173 |
|
174 val exh_start = thm "exh_start"; |
|
175 val ex_defined_iffs = thms "ex_defined_iffs"; |
|
176 val exh_casedist0 = thm "exh_casedist0"; |
|
177 val exh_casedists = thms "exh_casedists"; |
|
178 *} |
|
179 |
|
180 end |