equal
deleted
inserted
replaced
11 default_sort bifinite |
11 default_sort bifinite |
12 |
12 |
13 subsection {* Type constructor for finite deflations *} |
13 subsection {* Type constructor for finite deflations *} |
14 |
14 |
15 typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}" |
15 typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}" |
16 by (fast intro: finite_deflation_UU) |
16 by (fast intro: finite_deflation_bottom) |
17 |
17 |
18 instantiation fin_defl :: (bifinite) below |
18 instantiation fin_defl :: (bifinite) below |
19 begin |
19 begin |
20 |
20 |
21 definition below_fin_defl_def: |
21 definition below_fin_defl_def: |
136 |
136 |
137 lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x" |
137 lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x" |
138 apply (induct x rule: defl.principal_induct, simp) |
138 apply (induct x rule: defl.principal_induct, simp) |
139 apply (rule defl.principal_mono) |
139 apply (rule defl.principal_mono) |
140 apply (simp add: below_fin_defl_def) |
140 apply (simp add: below_fin_defl_def) |
141 apply (simp add: Abs_fin_defl_inverse finite_deflation_UU) |
141 apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom) |
142 done |
142 done |
143 |
143 |
144 instance defl :: (bifinite) pcpo |
144 instance defl :: (bifinite) pcpo |
145 by intro_classes (fast intro: defl_minimal) |
145 by intro_classes (fast intro: defl_minimal) |
146 |
146 |
147 lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)" |
147 lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)" |
148 by (rule defl_minimal [THEN UU_I, symmetric]) |
148 by (rule defl_minimal [THEN bottomI, symmetric]) |
149 |
149 |
150 subsection {* Applying algebraic deflations *} |
150 subsection {* Applying algebraic deflations *} |
151 |
151 |
152 definition |
152 definition |
153 cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a" |
153 cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a" |
207 |
207 |
208 lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>" |
208 lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>" |
209 apply (subst inst_defl_pcpo) |
209 apply (subst inst_defl_pcpo) |
210 apply (subst cast_defl_principal) |
210 apply (subst cast_defl_principal) |
211 apply (rule Abs_fin_defl_inverse) |
211 apply (rule Abs_fin_defl_inverse) |
212 apply (simp add: finite_deflation_UU) |
212 apply (simp add: finite_deflation_bottom) |
213 done |
213 done |
214 |
214 |
215 lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>" |
215 lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>" |
216 by (rule cast.below [THEN UU_I]) |
216 by (rule cast.below [THEN bottomI]) |
217 |
217 |
218 subsection {* Deflation combinators *} |
218 subsection {* Deflation combinators *} |
219 |
219 |
220 definition |
220 definition |
221 "defl_fun1 e p f = |
221 "defl_fun1 e p f = |