82 |
82 |
83 text \<open>Temporarily relax type constraints.\<close> |
83 text \<open>Temporarily relax type constraints.\<close> |
84 |
84 |
85 setup \<open> |
85 setup \<open> |
86 fold Sign.add_const_constraint |
86 fold Sign.add_const_constraint |
87 [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"}) |
87 [ (\<^const_name>\<open>defl\<close>, SOME \<^typ>\<open>'a::pcpo itself \<Rightarrow> udom defl\<close>) |
88 , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) |
88 , (\<^const_name>\<open>emb\<close>, SOME \<^typ>\<open>'a::pcpo \<rightarrow> udom\<close>) |
89 , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) |
89 , (\<^const_name>\<open>prj\<close>, SOME \<^typ>\<open>udom \<rightarrow> 'a::pcpo\<close>) |
90 , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom u defl"}) |
90 , (\<^const_name>\<open>liftdefl\<close>, SOME \<^typ>\<open>'a::pcpo itself \<Rightarrow> udom u defl\<close>) |
91 , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom u"}) |
91 , (\<^const_name>\<open>liftemb\<close>, SOME \<^typ>\<open>'a::pcpo u \<rightarrow> udom u\<close>) |
92 , (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::pcpo u"}) ] |
92 , (\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::pcpo u\<close>) ] |
93 \<close> |
93 \<close> |
94 |
94 |
95 lemma typedef_domain_class: |
95 lemma typedef_domain_class: |
96 fixes Rep :: "'a::pcpo \<Rightarrow> udom" |
96 fixes Rep :: "'a::pcpo \<Rightarrow> udom" |
97 fixes Abs :: "udom \<Rightarrow> 'a::pcpo" |
97 fixes Abs :: "udom \<Rightarrow> 'a::pcpo" |
140 |
140 |
141 text \<open>Restore original typing constraints.\<close> |
141 text \<open>Restore original typing constraints.\<close> |
142 |
142 |
143 setup \<open> |
143 setup \<open> |
144 fold Sign.add_const_constraint |
144 fold Sign.add_const_constraint |
145 [(@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"}), |
145 [(\<^const_name>\<open>defl\<close>, SOME \<^typ>\<open>'a::domain itself \<Rightarrow> udom defl\<close>), |
146 (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"}), |
146 (\<^const_name>\<open>emb\<close>, SOME \<^typ>\<open>'a::domain \<rightarrow> udom\<close>), |
147 (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"}), |
147 (\<^const_name>\<open>prj\<close>, SOME \<^typ>\<open>udom \<rightarrow> 'a::domain\<close>), |
148 (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"}), |
148 (\<^const_name>\<open>liftdefl\<close>, SOME \<^typ>\<open>'a::predomain itself \<Rightarrow> udom u defl\<close>), |
149 (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}), |
149 (\<^const_name>\<open>liftemb\<close>, SOME \<^typ>\<open>'a::predomain u \<rightarrow> udom u\<close>), |
150 (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"})] |
150 (\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::predomain u\<close>)] |
151 \<close> |
151 \<close> |
152 |
152 |
153 ML_file "Tools/domaindef.ML" |
153 ML_file "Tools/domaindef.ML" |
154 |
154 |
155 subsection \<open>Isomorphic deflations\<close> |
155 subsection \<open>Isomorphic deflations\<close> |