1.1 --- a/src/HOLCF/Cfun.thy Sat Nov 27 13:12:10 2010 -0800
1.2 +++ b/src/HOLCF/Cfun.thy Sat Nov 27 14:09:03 2010 -0800
1.3 @@ -6,7 +6,7 @@
1.4 header {* The type of continuous functions *}
1.5
1.6 theory Cfun
1.7 -imports Pcpodef Fun_Cpo Product_Cpo
1.8 +imports Cpodef Fun_Cpo Product_Cpo
1.9 begin
1.10
1.11 default_sort cpo
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOLCF/Cpodef.thy Sat Nov 27 14:09:03 2010 -0800
2.3 @@ -0,0 +1,285 @@
2.4 +(* Title: HOLCF/Pcpodef.thy
2.5 + Author: Brian Huffman
2.6 +*)
2.7 +
2.8 +header {* Subtypes of pcpos *}
2.9 +
2.10 +theory Cpodef
2.11 +imports Adm
2.12 +uses ("Tools/cpodef.ML")
2.13 +begin
2.14 +
2.15 +subsection {* Proving a subtype is a partial order *}
2.16 +
2.17 +text {*
2.18 + A subtype of a partial order is itself a partial order,
2.19 + if the ordering is defined in the standard way.
2.20 +*}
2.21 +
2.22 +setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
2.23 +
2.24 +theorem typedef_po:
2.25 + fixes Abs :: "'a::po \<Rightarrow> 'b::type"
2.26 + assumes type: "type_definition Rep Abs A"
2.27 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.28 + shows "OFCLASS('b, po_class)"
2.29 + apply (intro_classes, unfold below)
2.30 + apply (rule below_refl)
2.31 + apply (erule (1) below_trans)
2.32 + apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
2.33 + apply (erule (1) below_antisym)
2.34 +done
2.35 +
2.36 +setup {* Sign.add_const_constraint (@{const_name Porder.below},
2.37 + SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
2.38 +
2.39 +subsection {* Proving a subtype is finite *}
2.40 +
2.41 +lemma typedef_finite_UNIV:
2.42 + fixes Abs :: "'a::type \<Rightarrow> 'b::type"
2.43 + assumes type: "type_definition Rep Abs A"
2.44 + shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
2.45 +proof -
2.46 + assume "finite A"
2.47 + hence "finite (Abs ` A)" by (rule finite_imageI)
2.48 + thus "finite (UNIV :: 'b set)"
2.49 + by (simp only: type_definition.Abs_image [OF type])
2.50 +qed
2.51 +
2.52 +subsection {* Proving a subtype is chain-finite *}
2.53 +
2.54 +lemma ch2ch_Rep:
2.55 + assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.56 + shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
2.57 +unfolding chain_def below .
2.58 +
2.59 +theorem typedef_chfin:
2.60 + fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
2.61 + assumes type: "type_definition Rep Abs A"
2.62 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.63 + shows "OFCLASS('b, chfin_class)"
2.64 + apply intro_classes
2.65 + apply (drule ch2ch_Rep [OF below])
2.66 + apply (drule chfin)
2.67 + apply (unfold max_in_chain_def)
2.68 + apply (simp add: type_definition.Rep_inject [OF type])
2.69 +done
2.70 +
2.71 +subsection {* Proving a subtype is complete *}
2.72 +
2.73 +text {*
2.74 + A subtype of a cpo is itself a cpo if the ordering is
2.75 + defined in the standard way, and the defining subset
2.76 + is closed with respect to limits of chains. A set is
2.77 + closed if and only if membership in the set is an
2.78 + admissible predicate.
2.79 +*}
2.80 +
2.81 +lemma typedef_is_lubI:
2.82 + assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.83 + shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
2.84 +unfolding is_lub_def is_ub_def below by simp
2.85 +
2.86 +lemma Abs_inverse_lub_Rep:
2.87 + fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
2.88 + assumes type: "type_definition Rep Abs A"
2.89 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.90 + and adm: "adm (\<lambda>x. x \<in> A)"
2.91 + shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
2.92 + apply (rule type_definition.Abs_inverse [OF type])
2.93 + apply (erule admD [OF adm ch2ch_Rep [OF below]])
2.94 + apply (rule type_definition.Rep [OF type])
2.95 +done
2.96 +
2.97 +theorem typedef_is_lub:
2.98 + fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
2.99 + assumes type: "type_definition Rep Abs A"
2.100 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.101 + and adm: "adm (\<lambda>x. x \<in> A)"
2.102 + shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
2.103 +proof -
2.104 + assume S: "chain S"
2.105 + hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
2.106 + hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
2.107 + hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
2.108 + by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
2.109 + thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
2.110 + by (rule typedef_is_lubI [OF below])
2.111 +qed
2.112 +
2.113 +lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
2.114 +
2.115 +theorem typedef_cpo:
2.116 + fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
2.117 + assumes type: "type_definition Rep Abs A"
2.118 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.119 + and adm: "adm (\<lambda>x. x \<in> A)"
2.120 + shows "OFCLASS('b, cpo_class)"
2.121 +proof
2.122 + fix S::"nat \<Rightarrow> 'b" assume "chain S"
2.123 + hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
2.124 + by (rule typedef_is_lub [OF type below adm])
2.125 + thus "\<exists>x. range S <<| x" ..
2.126 +qed
2.127 +
2.128 +subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
2.129 +
2.130 +text {* For any sub-cpo, the @{term Rep} function is continuous. *}
2.131 +
2.132 +theorem typedef_cont_Rep:
2.133 + fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
2.134 + assumes type: "type_definition Rep Abs A"
2.135 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.136 + and adm: "adm (\<lambda>x. x \<in> A)"
2.137 + shows "cont Rep"
2.138 + apply (rule contI)
2.139 + apply (simp only: typedef_lub [OF type below adm])
2.140 + apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
2.141 + apply (rule cpo_lubI)
2.142 + apply (erule ch2ch_Rep [OF below])
2.143 +done
2.144 +
2.145 +text {*
2.146 + For a sub-cpo, we can make the @{term Abs} function continuous
2.147 + only if we restrict its domain to the defining subset by
2.148 + composing it with another continuous function.
2.149 +*}
2.150 +
2.151 +theorem typedef_cont_Abs:
2.152 + fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
2.153 + fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
2.154 + assumes type: "type_definition Rep Abs A"
2.155 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.156 + and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
2.157 + and f_in_A: "\<And>x. f x \<in> A"
2.158 + shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
2.159 +unfolding cont_def is_lub_def is_ub_def ball_simps below
2.160 +by (simp add: type_definition.Abs_inverse [OF type f_in_A])
2.161 +
2.162 +subsection {* Proving subtype elements are compact *}
2.163 +
2.164 +theorem typedef_compact:
2.165 + fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
2.166 + assumes type: "type_definition Rep Abs A"
2.167 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.168 + and adm: "adm (\<lambda>x. x \<in> A)"
2.169 + shows "compact (Rep k) \<Longrightarrow> compact k"
2.170 +proof (unfold compact_def)
2.171 + have cont_Rep: "cont Rep"
2.172 + by (rule typedef_cont_Rep [OF type below adm])
2.173 + assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
2.174 + with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
2.175 + thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
2.176 +qed
2.177 +
2.178 +subsection {* Proving a subtype is pointed *}
2.179 +
2.180 +text {*
2.181 + A subtype of a cpo has a least element if and only if
2.182 + the defining subset has a least element.
2.183 +*}
2.184 +
2.185 +theorem typedef_pcpo_generic:
2.186 + fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
2.187 + assumes type: "type_definition Rep Abs A"
2.188 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.189 + and z_in_A: "z \<in> A"
2.190 + and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
2.191 + shows "OFCLASS('b, pcpo_class)"
2.192 + apply (intro_classes)
2.193 + apply (rule_tac x="Abs z" in exI, rule allI)
2.194 + apply (unfold below)
2.195 + apply (subst type_definition.Abs_inverse [OF type z_in_A])
2.196 + apply (rule z_least [OF type_definition.Rep [OF type]])
2.197 +done
2.198 +
2.199 +text {*
2.200 + As a special case, a subtype of a pcpo has a least element
2.201 + if the defining subset contains @{term \<bottom>}.
2.202 +*}
2.203 +
2.204 +theorem typedef_pcpo:
2.205 + fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
2.206 + assumes type: "type_definition Rep Abs A"
2.207 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.208 + and UU_in_A: "\<bottom> \<in> A"
2.209 + shows "OFCLASS('b, pcpo_class)"
2.210 +by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
2.211 +
2.212 +subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
2.213 +
2.214 +text {*
2.215 + For a sub-pcpo where @{term \<bottom>} is a member of the defining
2.216 + subset, @{term Rep} and @{term Abs} are both strict.
2.217 +*}
2.218 +
2.219 +theorem typedef_Abs_strict:
2.220 + assumes type: "type_definition Rep Abs A"
2.221 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.222 + and UU_in_A: "\<bottom> \<in> A"
2.223 + shows "Abs \<bottom> = \<bottom>"
2.224 + apply (rule UU_I, unfold below)
2.225 + apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
2.226 +done
2.227 +
2.228 +theorem typedef_Rep_strict:
2.229 + assumes type: "type_definition Rep Abs A"
2.230 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.231 + and UU_in_A: "\<bottom> \<in> A"
2.232 + shows "Rep \<bottom> = \<bottom>"
2.233 + apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
2.234 + apply (rule type_definition.Abs_inverse [OF type UU_in_A])
2.235 +done
2.236 +
2.237 +theorem typedef_Abs_bottom_iff:
2.238 + assumes type: "type_definition Rep Abs A"
2.239 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.240 + and UU_in_A: "\<bottom> \<in> A"
2.241 + shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
2.242 + apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
2.243 + apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
2.244 +done
2.245 +
2.246 +theorem typedef_Rep_bottom_iff:
2.247 + assumes type: "type_definition Rep Abs A"
2.248 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.249 + and UU_in_A: "\<bottom> \<in> A"
2.250 + shows "(Rep x = \<bottom>) = (x = \<bottom>)"
2.251 + apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
2.252 + apply (simp add: type_definition.Rep_inject [OF type])
2.253 +done
2.254 +
2.255 +theorem typedef_Abs_defined:
2.256 + assumes type: "type_definition Rep Abs A"
2.257 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.258 + and UU_in_A: "\<bottom> \<in> A"
2.259 + shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
2.260 +by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
2.261 +
2.262 +theorem typedef_Rep_defined:
2.263 + assumes type: "type_definition Rep Abs A"
2.264 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.265 + and UU_in_A: "\<bottom> \<in> A"
2.266 + shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
2.267 +by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
2.268 +
2.269 +subsection {* Proving a subtype is flat *}
2.270 +
2.271 +theorem typedef_flat:
2.272 + fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
2.273 + assumes type: "type_definition Rep Abs A"
2.274 + and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
2.275 + and UU_in_A: "\<bottom> \<in> A"
2.276 + shows "OFCLASS('b, flat_class)"
2.277 + apply (intro_classes)
2.278 + apply (unfold below)
2.279 + apply (simp add: type_definition.Rep_inject [OF type, symmetric])
2.280 + apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
2.281 + apply (simp add: ax_flat)
2.282 +done
2.283 +
2.284 +subsection {* HOLCF type definition package *}
2.285 +
2.286 +use "Tools/cpodef.ML"
2.287 +
2.288 +end
3.1 --- a/src/HOLCF/IsaMakefile Sat Nov 27 13:12:10 2010 -0800
3.2 +++ b/src/HOLCF/IsaMakefile Sat Nov 27 14:09:03 2010 -0800
3.3 @@ -43,6 +43,7 @@
3.4 Completion.thy \
3.5 Cont.thy \
3.6 ConvexPD.thy \
3.7 + Cpodef.thy \
3.8 Cprod.thy \
3.9 Discrete.thy \
3.10 Deflation.thy \
3.11 @@ -56,7 +57,6 @@
3.12 LowerPD.thy \
3.13 Map_Functions.thy \
3.14 One.thy \
3.15 - Pcpodef.thy \
3.16 Pcpo.thy \
3.17 Plain_HOLCF.thy \
3.18 Porder.thy \
3.19 @@ -78,9 +78,9 @@
3.20 Tools/Domain/domain_induction.ML \
3.21 Tools/Domain/domain_isomorphism.ML \
3.22 Tools/Domain/domain_take_proofs.ML \
3.23 + Tools/cpodef.ML \
3.24 Tools/domaindef.ML \
3.25 Tools/fixrec.ML \
3.26 - Tools/pcpodef.ML \
3.27 document/root.tex
3.28 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
3.29
4.1 --- a/src/HOLCF/Pcpodef.thy Sat Nov 27 13:12:10 2010 -0800
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,285 +0,0 @@
4.4 -(* Title: HOLCF/Pcpodef.thy
4.5 - Author: Brian Huffman
4.6 -*)
4.7 -
4.8 -header {* Subtypes of pcpos *}
4.9 -
4.10 -theory Pcpodef
4.11 -imports Adm
4.12 -uses ("Tools/pcpodef.ML")
4.13 -begin
4.14 -
4.15 -subsection {* Proving a subtype is a partial order *}
4.16 -
4.17 -text {*
4.18 - A subtype of a partial order is itself a partial order,
4.19 - if the ordering is defined in the standard way.
4.20 -*}
4.21 -
4.22 -setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
4.23 -
4.24 -theorem typedef_po:
4.25 - fixes Abs :: "'a::po \<Rightarrow> 'b::type"
4.26 - assumes type: "type_definition Rep Abs A"
4.27 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.28 - shows "OFCLASS('b, po_class)"
4.29 - apply (intro_classes, unfold below)
4.30 - apply (rule below_refl)
4.31 - apply (erule (1) below_trans)
4.32 - apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
4.33 - apply (erule (1) below_antisym)
4.34 -done
4.35 -
4.36 -setup {* Sign.add_const_constraint (@{const_name Porder.below},
4.37 - SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
4.38 -
4.39 -subsection {* Proving a subtype is finite *}
4.40 -
4.41 -lemma typedef_finite_UNIV:
4.42 - fixes Abs :: "'a::type \<Rightarrow> 'b::type"
4.43 - assumes type: "type_definition Rep Abs A"
4.44 - shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
4.45 -proof -
4.46 - assume "finite A"
4.47 - hence "finite (Abs ` A)" by (rule finite_imageI)
4.48 - thus "finite (UNIV :: 'b set)"
4.49 - by (simp only: type_definition.Abs_image [OF type])
4.50 -qed
4.51 -
4.52 -subsection {* Proving a subtype is chain-finite *}
4.53 -
4.54 -lemma ch2ch_Rep:
4.55 - assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.56 - shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
4.57 -unfolding chain_def below .
4.58 -
4.59 -theorem typedef_chfin:
4.60 - fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
4.61 - assumes type: "type_definition Rep Abs A"
4.62 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.63 - shows "OFCLASS('b, chfin_class)"
4.64 - apply intro_classes
4.65 - apply (drule ch2ch_Rep [OF below])
4.66 - apply (drule chfin)
4.67 - apply (unfold max_in_chain_def)
4.68 - apply (simp add: type_definition.Rep_inject [OF type])
4.69 -done
4.70 -
4.71 -subsection {* Proving a subtype is complete *}
4.72 -
4.73 -text {*
4.74 - A subtype of a cpo is itself a cpo if the ordering is
4.75 - defined in the standard way, and the defining subset
4.76 - is closed with respect to limits of chains. A set is
4.77 - closed if and only if membership in the set is an
4.78 - admissible predicate.
4.79 -*}
4.80 -
4.81 -lemma typedef_is_lubI:
4.82 - assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.83 - shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
4.84 -unfolding is_lub_def is_ub_def below by simp
4.85 -
4.86 -lemma Abs_inverse_lub_Rep:
4.87 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
4.88 - assumes type: "type_definition Rep Abs A"
4.89 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.90 - and adm: "adm (\<lambda>x. x \<in> A)"
4.91 - shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
4.92 - apply (rule type_definition.Abs_inverse [OF type])
4.93 - apply (erule admD [OF adm ch2ch_Rep [OF below]])
4.94 - apply (rule type_definition.Rep [OF type])
4.95 -done
4.96 -
4.97 -theorem typedef_is_lub:
4.98 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
4.99 - assumes type: "type_definition Rep Abs A"
4.100 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.101 - and adm: "adm (\<lambda>x. x \<in> A)"
4.102 - shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
4.103 -proof -
4.104 - assume S: "chain S"
4.105 - hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
4.106 - hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
4.107 - hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
4.108 - by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
4.109 - thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
4.110 - by (rule typedef_is_lubI [OF below])
4.111 -qed
4.112 -
4.113 -lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
4.114 -
4.115 -theorem typedef_cpo:
4.116 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
4.117 - assumes type: "type_definition Rep Abs A"
4.118 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.119 - and adm: "adm (\<lambda>x. x \<in> A)"
4.120 - shows "OFCLASS('b, cpo_class)"
4.121 -proof
4.122 - fix S::"nat \<Rightarrow> 'b" assume "chain S"
4.123 - hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
4.124 - by (rule typedef_is_lub [OF type below adm])
4.125 - thus "\<exists>x. range S <<| x" ..
4.126 -qed
4.127 -
4.128 -subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
4.129 -
4.130 -text {* For any sub-cpo, the @{term Rep} function is continuous. *}
4.131 -
4.132 -theorem typedef_cont_Rep:
4.133 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
4.134 - assumes type: "type_definition Rep Abs A"
4.135 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.136 - and adm: "adm (\<lambda>x. x \<in> A)"
4.137 - shows "cont Rep"
4.138 - apply (rule contI)
4.139 - apply (simp only: typedef_lub [OF type below adm])
4.140 - apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
4.141 - apply (rule cpo_lubI)
4.142 - apply (erule ch2ch_Rep [OF below])
4.143 -done
4.144 -
4.145 -text {*
4.146 - For a sub-cpo, we can make the @{term Abs} function continuous
4.147 - only if we restrict its domain to the defining subset by
4.148 - composing it with another continuous function.
4.149 -*}
4.150 -
4.151 -theorem typedef_cont_Abs:
4.152 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
4.153 - fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
4.154 - assumes type: "type_definition Rep Abs A"
4.155 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.156 - and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
4.157 - and f_in_A: "\<And>x. f x \<in> A"
4.158 - shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
4.159 -unfolding cont_def is_lub_def is_ub_def ball_simps below
4.160 -by (simp add: type_definition.Abs_inverse [OF type f_in_A])
4.161 -
4.162 -subsection {* Proving subtype elements are compact *}
4.163 -
4.164 -theorem typedef_compact:
4.165 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
4.166 - assumes type: "type_definition Rep Abs A"
4.167 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.168 - and adm: "adm (\<lambda>x. x \<in> A)"
4.169 - shows "compact (Rep k) \<Longrightarrow> compact k"
4.170 -proof (unfold compact_def)
4.171 - have cont_Rep: "cont Rep"
4.172 - by (rule typedef_cont_Rep [OF type below adm])
4.173 - assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
4.174 - with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
4.175 - thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
4.176 -qed
4.177 -
4.178 -subsection {* Proving a subtype is pointed *}
4.179 -
4.180 -text {*
4.181 - A subtype of a cpo has a least element if and only if
4.182 - the defining subset has a least element.
4.183 -*}
4.184 -
4.185 -theorem typedef_pcpo_generic:
4.186 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
4.187 - assumes type: "type_definition Rep Abs A"
4.188 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.189 - and z_in_A: "z \<in> A"
4.190 - and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
4.191 - shows "OFCLASS('b, pcpo_class)"
4.192 - apply (intro_classes)
4.193 - apply (rule_tac x="Abs z" in exI, rule allI)
4.194 - apply (unfold below)
4.195 - apply (subst type_definition.Abs_inverse [OF type z_in_A])
4.196 - apply (rule z_least [OF type_definition.Rep [OF type]])
4.197 -done
4.198 -
4.199 -text {*
4.200 - As a special case, a subtype of a pcpo has a least element
4.201 - if the defining subset contains @{term \<bottom>}.
4.202 -*}
4.203 -
4.204 -theorem typedef_pcpo:
4.205 - fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
4.206 - assumes type: "type_definition Rep Abs A"
4.207 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.208 - and UU_in_A: "\<bottom> \<in> A"
4.209 - shows "OFCLASS('b, pcpo_class)"
4.210 -by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
4.211 -
4.212 -subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
4.213 -
4.214 -text {*
4.215 - For a sub-pcpo where @{term \<bottom>} is a member of the defining
4.216 - subset, @{term Rep} and @{term Abs} are both strict.
4.217 -*}
4.218 -
4.219 -theorem typedef_Abs_strict:
4.220 - assumes type: "type_definition Rep Abs A"
4.221 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.222 - and UU_in_A: "\<bottom> \<in> A"
4.223 - shows "Abs \<bottom> = \<bottom>"
4.224 - apply (rule UU_I, unfold below)
4.225 - apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
4.226 -done
4.227 -
4.228 -theorem typedef_Rep_strict:
4.229 - assumes type: "type_definition Rep Abs A"
4.230 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.231 - and UU_in_A: "\<bottom> \<in> A"
4.232 - shows "Rep \<bottom> = \<bottom>"
4.233 - apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
4.234 - apply (rule type_definition.Abs_inverse [OF type UU_in_A])
4.235 -done
4.236 -
4.237 -theorem typedef_Abs_bottom_iff:
4.238 - assumes type: "type_definition Rep Abs A"
4.239 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.240 - and UU_in_A: "\<bottom> \<in> A"
4.241 - shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
4.242 - apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
4.243 - apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
4.244 -done
4.245 -
4.246 -theorem typedef_Rep_bottom_iff:
4.247 - assumes type: "type_definition Rep Abs A"
4.248 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.249 - and UU_in_A: "\<bottom> \<in> A"
4.250 - shows "(Rep x = \<bottom>) = (x = \<bottom>)"
4.251 - apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
4.252 - apply (simp add: type_definition.Rep_inject [OF type])
4.253 -done
4.254 -
4.255 -theorem typedef_Abs_defined:
4.256 - assumes type: "type_definition Rep Abs A"
4.257 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.258 - and UU_in_A: "\<bottom> \<in> A"
4.259 - shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
4.260 -by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
4.261 -
4.262 -theorem typedef_Rep_defined:
4.263 - assumes type: "type_definition Rep Abs A"
4.264 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.265 - and UU_in_A: "\<bottom> \<in> A"
4.266 - shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
4.267 -by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
4.268 -
4.269 -subsection {* Proving a subtype is flat *}
4.270 -
4.271 -theorem typedef_flat:
4.272 - fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
4.273 - assumes type: "type_definition Rep Abs A"
4.274 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
4.275 - and UU_in_A: "\<bottom> \<in> A"
4.276 - shows "OFCLASS('b, flat_class)"
4.277 - apply (intro_classes)
4.278 - apply (unfold below)
4.279 - apply (simp add: type_definition.Rep_inject [OF type, symmetric])
4.280 - apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
4.281 - apply (simp add: ax_flat)
4.282 -done
4.283 -
4.284 -subsection {* HOLCF type definition package *}
4.285 -
4.286 -use "Tools/pcpodef.ML"
4.287 -
4.288 -end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOLCF/Tools/cpodef.ML Sat Nov 27 14:09:03 2010 -0800
5.3 @@ -0,0 +1,383 @@
5.4 +(* Title: HOLCF/Tools/cpodef.ML
5.5 + Author: Brian Huffman
5.6 +
5.7 +Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
5.8 +typedef (see also ~~/src/HOL/Tools/typedef.ML).
5.9 +*)
5.10 +
5.11 +signature CPODEF =
5.12 +sig
5.13 + type cpo_info =
5.14 + { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
5.15 + is_lub: thm, lub: thm, compact: thm }
5.16 + type pcpo_info =
5.17 + { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
5.18 + Rep_defined: thm, Abs_defined: thm }
5.19 +
5.20 + val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
5.21 + term -> (binding * binding) option -> tactic -> theory ->
5.22 + (Typedef.info * thm) * theory
5.23 + val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
5.24 + term -> (binding * binding) option -> tactic * tactic -> theory ->
5.25 + (Typedef.info * cpo_info) * theory
5.26 + val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
5.27 + term -> (binding * binding) option -> tactic * tactic -> theory ->
5.28 + (Typedef.info * cpo_info * pcpo_info) * theory
5.29 +
5.30 + val cpodef_proof: (bool * binding)
5.31 + * (binding * (string * sort) list * mixfix) * term
5.32 + * (binding * binding) option -> theory -> Proof.state
5.33 + val cpodef_proof_cmd: (bool * binding)
5.34 + * (binding * (string * string option) list * mixfix) * string
5.35 + * (binding * binding) option -> theory -> Proof.state
5.36 + val pcpodef_proof: (bool * binding)
5.37 + * (binding * (string * sort) list * mixfix) * term
5.38 + * (binding * binding) option -> theory -> Proof.state
5.39 + val pcpodef_proof_cmd: (bool * binding)
5.40 + * (binding * (string * string option) list * mixfix) * string
5.41 + * (binding * binding) option -> theory -> Proof.state
5.42 +end;
5.43 +
5.44 +structure Cpodef :> CPODEF =
5.45 +struct
5.46 +
5.47 +(** type definitions **)
5.48 +
5.49 +type cpo_info =
5.50 + { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
5.51 + is_lub: thm, lub: thm, compact: thm }
5.52 +
5.53 +type pcpo_info =
5.54 + { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
5.55 + Rep_defined: thm, Abs_defined: thm }
5.56 +
5.57 +(* building terms *)
5.58 +
5.59 +fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
5.60 +fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
5.61 +
5.62 +fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
5.63 +
5.64 +(* manipulating theorems *)
5.65 +
5.66 +fun fold_adm_mem thm NONE = thm
5.67 + | fold_adm_mem thm (SOME set_def) =
5.68 + let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
5.69 + in rule OF [set_def, thm] end;
5.70 +
5.71 +fun fold_UU_mem thm NONE = thm
5.72 + | fold_UU_mem thm (SOME set_def) =
5.73 + let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
5.74 + in rule OF [set_def, thm] end;
5.75 +
5.76 +(* proving class instances *)
5.77 +
5.78 +fun prove_cpo
5.79 + (name: binding)
5.80 + (newT: typ)
5.81 + (Rep_name: binding, Abs_name: binding)
5.82 + (type_definition: thm) (* type_definition Rep Abs A *)
5.83 + (set_def: thm option) (* A == set *)
5.84 + (below_def: thm) (* op << == %x y. Rep x << Rep y *)
5.85 + (admissible: thm) (* adm (%x. x : set) *)
5.86 + (thy: theory)
5.87 + =
5.88 + let
5.89 + val admissible' = fold_adm_mem admissible set_def;
5.90 + val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
5.91 + val (full_tname, Ts) = dest_Type newT;
5.92 + val lhs_sorts = map (snd o dest_TFree) Ts;
5.93 + val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1;
5.94 + val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
5.95 + (* transfer thms so that they will know about the new cpo instance *)
5.96 + val cpo_thms' = map (Thm.transfer thy) cpo_thms;
5.97 + fun make thm = Drule.zero_var_indexes (thm OF cpo_thms');
5.98 + val cont_Rep = make @{thm typedef_cont_Rep};
5.99 + val cont_Abs = make @{thm typedef_cont_Abs};
5.100 + val is_lub = make @{thm typedef_is_lub};
5.101 + val lub = make @{thm typedef_lub};
5.102 + val compact = make @{thm typedef_compact};
5.103 + val (_, thy) =
5.104 + thy
5.105 + |> Sign.add_path (Binding.name_of name)
5.106 + |> Global_Theory.add_thms
5.107 + ([((Binding.prefix_name "adm_" name, admissible'), []),
5.108 + ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []),
5.109 + ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []),
5.110 + ((Binding.prefix_name "is_lub_" name, is_lub ), []),
5.111 + ((Binding.prefix_name "lub_" name, lub ), []),
5.112 + ((Binding.prefix_name "compact_" name, compact ), [])])
5.113 + ||> Sign.parent_path;
5.114 + val cpo_info : cpo_info =
5.115 + { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
5.116 + cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact };
5.117 + in
5.118 + (cpo_info, thy)
5.119 + end;
5.120 +
5.121 +fun prove_pcpo
5.122 + (name: binding)
5.123 + (newT: typ)
5.124 + (Rep_name: binding, Abs_name: binding)
5.125 + (type_definition: thm) (* type_definition Rep Abs A *)
5.126 + (set_def: thm option) (* A == set *)
5.127 + (below_def: thm) (* op << == %x y. Rep x << Rep y *)
5.128 + (UU_mem: thm) (* UU : set *)
5.129 + (thy: theory)
5.130 + =
5.131 + let
5.132 + val UU_mem' = fold_UU_mem UU_mem set_def;
5.133 + val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
5.134 + val (full_tname, Ts) = dest_Type newT;
5.135 + val lhs_sorts = map (snd o dest_TFree) Ts;
5.136 + val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
5.137 + val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
5.138 + val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
5.139 + fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
5.140 + val Rep_strict = make @{thm typedef_Rep_strict};
5.141 + val Abs_strict = make @{thm typedef_Abs_strict};
5.142 + val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff};
5.143 + val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff};
5.144 + val Rep_defined = make @{thm typedef_Rep_defined};
5.145 + val Abs_defined = make @{thm typedef_Abs_defined};
5.146 + val (_, thy) =
5.147 + thy
5.148 + |> Sign.add_path (Binding.name_of name)
5.149 + |> Global_Theory.add_thms
5.150 + ([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []),
5.151 + ((Binding.suffix_name "_strict" Abs_name, Abs_strict), []),
5.152 + ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
5.153 + ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
5.154 + ((Binding.suffix_name "_defined" Rep_name, Rep_defined), []),
5.155 + ((Binding.suffix_name "_defined" Abs_name, Abs_defined), [])])
5.156 + ||> Sign.parent_path;
5.157 + val pcpo_info =
5.158 + { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
5.159 + Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
5.160 + Rep_defined = Rep_defined, Abs_defined = Abs_defined };
5.161 + in
5.162 + (pcpo_info, thy)
5.163 + end;
5.164 +
5.165 +(* prepare_cpodef *)
5.166 +
5.167 +fun declare_type_name a =
5.168 + Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
5.169 +
5.170 +fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
5.171 + let
5.172 + val _ = Theory.requires thy "Cpodef" "cpodefs";
5.173 +
5.174 + (*rhs*)
5.175 + val tmp_ctxt =
5.176 + ProofContext.init_global thy
5.177 + |> fold (Variable.declare_typ o TFree) raw_args;
5.178 + val set = prep_term tmp_ctxt raw_set;
5.179 + val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
5.180 +
5.181 + val setT = Term.fastype_of set;
5.182 + val oldT = HOLogic.dest_setT setT handle TYPE _ =>
5.183 + error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
5.184 +
5.185 + (*lhs*)
5.186 + val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
5.187 + val full_tname = Sign.full_name thy tname;
5.188 + val newT = Type (full_tname, map TFree lhs_tfrees);
5.189 +
5.190 + val morphs = opt_morphs
5.191 + |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
5.192 + in
5.193 + (newT, oldT, set, morphs)
5.194 + end
5.195 +
5.196 +fun add_podef def opt_name typ set opt_morphs tac thy =
5.197 + let
5.198 + val name = the_default (#1 typ) opt_name;
5.199 + val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy
5.200 + |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
5.201 + val oldT = #rep_type (#1 info);
5.202 + val newT = #abs_type (#1 info);
5.203 + val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
5.204 +
5.205 + val RepC = Const (Rep_name, newT --> oldT);
5.206 + val below_eqn = Logic.mk_equals (below_const newT,
5.207 + Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
5.208 + val lthy3 = thy2
5.209 + |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
5.210 + val ((_, (_, below_ldef)), lthy4) = lthy3
5.211 + |> Specification.definition (NONE,
5.212 + ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
5.213 + val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4);
5.214 + val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
5.215 + val thy5 = lthy4
5.216 + |> Class.prove_instantiation_instance
5.217 + (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
5.218 + |> Local_Theory.exit_global;
5.219 + in ((info, below_def), thy5) end;
5.220 +
5.221 +fun prepare_cpodef
5.222 + (prep_term: Proof.context -> 'a -> term)
5.223 + (def: bool)
5.224 + (name: binding)
5.225 + (typ: binding * (string * sort) list * mixfix)
5.226 + (raw_set: 'a)
5.227 + (opt_morphs: (binding * binding) option)
5.228 + (thy: theory)
5.229 + : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
5.230 + let
5.231 + val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
5.232 + prepare prep_term name typ raw_set opt_morphs thy;
5.233 +
5.234 + val goal_nonempty =
5.235 + HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
5.236 + val goal_admissible =
5.237 + HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
5.238 +
5.239 + fun cpodef_result nonempty admissible thy =
5.240 + let
5.241 + val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
5.242 + |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
5.243 + val (cpo_info, thy3) = thy2
5.244 + |> prove_cpo name newT morphs type_definition set_def below_def admissible;
5.245 + in
5.246 + ((info, cpo_info), thy3)
5.247 + end;
5.248 + in
5.249 + (goal_nonempty, goal_admissible, cpodef_result)
5.250 + end
5.251 + handle ERROR msg =>
5.252 + cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
5.253 +
5.254 +fun prepare_pcpodef
5.255 + (prep_term: Proof.context -> 'a -> term)
5.256 + (def: bool)
5.257 + (name: binding)
5.258 + (typ: binding * (string * sort) list * mixfix)
5.259 + (raw_set: 'a)
5.260 + (opt_morphs: (binding * binding) option)
5.261 + (thy: theory)
5.262 + : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
5.263 + let
5.264 + val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
5.265 + prepare prep_term name typ raw_set opt_morphs thy;
5.266 +
5.267 + val goal_UU_mem =
5.268 + HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
5.269 +
5.270 + val goal_admissible =
5.271 + HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
5.272 +
5.273 + fun pcpodef_result UU_mem admissible thy =
5.274 + let
5.275 + val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
5.276 + val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
5.277 + |> add_podef def (SOME name) typ set opt_morphs tac;
5.278 + val (cpo_info, thy3) = thy2
5.279 + |> prove_cpo name newT morphs type_definition set_def below_def admissible;
5.280 + val (pcpo_info, thy4) = thy3
5.281 + |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem;
5.282 + in
5.283 + ((info, cpo_info, pcpo_info), thy4)
5.284 + end;
5.285 + in
5.286 + (goal_UU_mem, goal_admissible, pcpodef_result)
5.287 + end
5.288 + handle ERROR msg =>
5.289 + cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name));
5.290 +
5.291 +
5.292 +(* tactic interface *)
5.293 +
5.294 +fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
5.295 + let
5.296 + val name = the_default (#1 typ) opt_name;
5.297 + val (goal1, goal2, cpodef_result) =
5.298 + prepare_cpodef Syntax.check_term def name typ set opt_morphs thy;
5.299 + val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
5.300 + handle ERROR msg => cat_error msg
5.301 + ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
5.302 + val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
5.303 + handle ERROR msg => cat_error msg
5.304 + ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
5.305 + in cpodef_result thm1 thm2 thy end;
5.306 +
5.307 +fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
5.308 + let
5.309 + val name = the_default (#1 typ) opt_name;
5.310 + val (goal1, goal2, pcpodef_result) =
5.311 + prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy;
5.312 + val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
5.313 + handle ERROR msg => cat_error msg
5.314 + ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
5.315 + val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
5.316 + handle ERROR msg => cat_error msg
5.317 + ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
5.318 + in pcpodef_result thm1 thm2 thy end;
5.319 +
5.320 +
5.321 +(* proof interface *)
5.322 +
5.323 +local
5.324 +
5.325 +fun gen_cpodef_proof prep_term prep_constraint
5.326 + ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
5.327 + let
5.328 + val ctxt = ProofContext.init_global thy;
5.329 + val args = map (apsnd (prep_constraint ctxt)) raw_args;
5.330 + val (goal1, goal2, make_result) =
5.331 + prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
5.332 + fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
5.333 + | after_qed _ = raise Fail "cpodef_proof";
5.334 + in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
5.335 +
5.336 +fun gen_pcpodef_proof prep_term prep_constraint
5.337 + ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
5.338 + let
5.339 + val ctxt = ProofContext.init_global thy;
5.340 + val args = map (apsnd (prep_constraint ctxt)) raw_args;
5.341 + val (goal1, goal2, make_result) =
5.342 + prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
5.343 + fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
5.344 + | after_qed _ = raise Fail "pcpodef_proof";
5.345 + in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
5.346 +
5.347 +in
5.348 +
5.349 +fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x;
5.350 +fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x;
5.351 +
5.352 +fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x;
5.353 +fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x;
5.354 +
5.355 +end;
5.356 +
5.357 +
5.358 +
5.359 +(** outer syntax **)
5.360 +
5.361 +val typedef_proof_decl =
5.362 + Scan.optional (Parse.$$$ "(" |--
5.363 + ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
5.364 + Parse.binding >> (fn s => (true, SOME s)))
5.365 + --| Parse.$$$ ")") (true, NONE) --
5.366 + (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
5.367 + (Parse.$$$ "=" |-- Parse.term) --
5.368 + Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
5.369 +
5.370 +fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
5.371 + (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
5.372 + ((def, the_default t opt_name), (t, args, mx), A, morphs);
5.373 +
5.374 +val _ =
5.375 + Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
5.376 + Keyword.thy_goal
5.377 + (typedef_proof_decl >>
5.378 + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
5.379 +
5.380 +val _ =
5.381 + Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
5.382 + Keyword.thy_goal
5.383 + (typedef_proof_decl >>
5.384 + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
5.385 +
5.386 +end;
6.1 --- a/src/HOLCF/Tools/domaindef.ML Sat Nov 27 13:12:10 2010 -0800
6.2 +++ b/src/HOLCF/Tools/domaindef.ML Sat Nov 27 14:09:03 2010 -0800
6.3 @@ -19,7 +19,7 @@
6.4
6.5 val add_domaindef: bool -> binding option -> binding * (string * sort) list * mixfix ->
6.6 term -> (binding * binding) option -> theory ->
6.7 - (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory
6.8 + (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory
6.9
6.10 val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string
6.11 * (binding * binding) option -> theory -> theory
6.12 @@ -86,7 +86,7 @@
6.13 (raw_defl: 'a)
6.14 (opt_morphs: (binding * binding) option)
6.15 (thy: theory)
6.16 - : (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory =
6.17 + : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
6.18 let
6.19 val _ = Theory.requires thy "Domain" "domaindefs";
6.20
6.21 @@ -118,7 +118,7 @@
6.22 val tac1 = rtac @{thm defl_set_bottom} 1;
6.23 val tac2 = rtac @{thm adm_defl_set} 1;
6.24 val ((info, cpo_info, pcpo_info), thy) = thy
6.25 - |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
6.26 + |> Cpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
6.27
6.28 (*definitions*)
6.29 val Rep_const = Const (#Rep_name (#1 info), newT --> udomT);
7.1 --- a/src/HOLCF/Tools/pcpodef.ML Sat Nov 27 13:12:10 2010 -0800
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,383 +0,0 @@
7.4 -(* Title: HOLCF/Tools/pcpodef.ML
7.5 - Author: Brian Huffman
7.6 -
7.7 -Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
7.8 -typedef (see also ~~/src/HOL/Tools/typedef.ML).
7.9 -*)
7.10 -
7.11 -signature PCPODEF =
7.12 -sig
7.13 - type cpo_info =
7.14 - { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
7.15 - is_lub: thm, lub: thm, compact: thm }
7.16 - type pcpo_info =
7.17 - { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
7.18 - Rep_defined: thm, Abs_defined: thm }
7.19 -
7.20 - val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
7.21 - term -> (binding * binding) option -> tactic -> theory ->
7.22 - (Typedef.info * thm) * theory
7.23 - val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
7.24 - term -> (binding * binding) option -> tactic * tactic -> theory ->
7.25 - (Typedef.info * cpo_info) * theory
7.26 - val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
7.27 - term -> (binding * binding) option -> tactic * tactic -> theory ->
7.28 - (Typedef.info * cpo_info * pcpo_info) * theory
7.29 -
7.30 - val cpodef_proof: (bool * binding)
7.31 - * (binding * (string * sort) list * mixfix) * term
7.32 - * (binding * binding) option -> theory -> Proof.state
7.33 - val cpodef_proof_cmd: (bool * binding)
7.34 - * (binding * (string * string option) list * mixfix) * string
7.35 - * (binding * binding) option -> theory -> Proof.state
7.36 - val pcpodef_proof: (bool * binding)
7.37 - * (binding * (string * sort) list * mixfix) * term
7.38 - * (binding * binding) option -> theory -> Proof.state
7.39 - val pcpodef_proof_cmd: (bool * binding)
7.40 - * (binding * (string * string option) list * mixfix) * string
7.41 - * (binding * binding) option -> theory -> Proof.state
7.42 -end;
7.43 -
7.44 -structure Pcpodef :> PCPODEF =
7.45 -struct
7.46 -
7.47 -(** type definitions **)
7.48 -
7.49 -type cpo_info =
7.50 - { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
7.51 - is_lub: thm, lub: thm, compact: thm }
7.52 -
7.53 -type pcpo_info =
7.54 - { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
7.55 - Rep_defined: thm, Abs_defined: thm }
7.56 -
7.57 -(* building terms *)
7.58 -
7.59 -fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
7.60 -fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
7.61 -
7.62 -fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
7.63 -
7.64 -(* manipulating theorems *)
7.65 -
7.66 -fun fold_adm_mem thm NONE = thm
7.67 - | fold_adm_mem thm (SOME set_def) =
7.68 - let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
7.69 - in rule OF [set_def, thm] end;
7.70 -
7.71 -fun fold_UU_mem thm NONE = thm
7.72 - | fold_UU_mem thm (SOME set_def) =
7.73 - let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
7.74 - in rule OF [set_def, thm] end;
7.75 -
7.76 -(* proving class instances *)
7.77 -
7.78 -fun prove_cpo
7.79 - (name: binding)
7.80 - (newT: typ)
7.81 - (Rep_name: binding, Abs_name: binding)
7.82 - (type_definition: thm) (* type_definition Rep Abs A *)
7.83 - (set_def: thm option) (* A == set *)
7.84 - (below_def: thm) (* op << == %x y. Rep x << Rep y *)
7.85 - (admissible: thm) (* adm (%x. x : set) *)
7.86 - (thy: theory)
7.87 - =
7.88 - let
7.89 - val admissible' = fold_adm_mem admissible set_def;
7.90 - val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
7.91 - val (full_tname, Ts) = dest_Type newT;
7.92 - val lhs_sorts = map (snd o dest_TFree) Ts;
7.93 - val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1;
7.94 - val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
7.95 - (* transfer thms so that they will know about the new cpo instance *)
7.96 - val cpo_thms' = map (Thm.transfer thy) cpo_thms;
7.97 - fun make thm = Drule.zero_var_indexes (thm OF cpo_thms');
7.98 - val cont_Rep = make @{thm typedef_cont_Rep};
7.99 - val cont_Abs = make @{thm typedef_cont_Abs};
7.100 - val is_lub = make @{thm typedef_is_lub};
7.101 - val lub = make @{thm typedef_lub};
7.102 - val compact = make @{thm typedef_compact};
7.103 - val (_, thy) =
7.104 - thy
7.105 - |> Sign.add_path (Binding.name_of name)
7.106 - |> Global_Theory.add_thms
7.107 - ([((Binding.prefix_name "adm_" name, admissible'), []),
7.108 - ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []),
7.109 - ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []),
7.110 - ((Binding.prefix_name "is_lub_" name, is_lub ), []),
7.111 - ((Binding.prefix_name "lub_" name, lub ), []),
7.112 - ((Binding.prefix_name "compact_" name, compact ), [])])
7.113 - ||> Sign.parent_path;
7.114 - val cpo_info : cpo_info =
7.115 - { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
7.116 - cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact };
7.117 - in
7.118 - (cpo_info, thy)
7.119 - end;
7.120 -
7.121 -fun prove_pcpo
7.122 - (name: binding)
7.123 - (newT: typ)
7.124 - (Rep_name: binding, Abs_name: binding)
7.125 - (type_definition: thm) (* type_definition Rep Abs A *)
7.126 - (set_def: thm option) (* A == set *)
7.127 - (below_def: thm) (* op << == %x y. Rep x << Rep y *)
7.128 - (UU_mem: thm) (* UU : set *)
7.129 - (thy: theory)
7.130 - =
7.131 - let
7.132 - val UU_mem' = fold_UU_mem UU_mem set_def;
7.133 - val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
7.134 - val (full_tname, Ts) = dest_Type newT;
7.135 - val lhs_sorts = map (snd o dest_TFree) Ts;
7.136 - val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
7.137 - val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
7.138 - val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
7.139 - fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
7.140 - val Rep_strict = make @{thm typedef_Rep_strict};
7.141 - val Abs_strict = make @{thm typedef_Abs_strict};
7.142 - val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff};
7.143 - val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff};
7.144 - val Rep_defined = make @{thm typedef_Rep_defined};
7.145 - val Abs_defined = make @{thm typedef_Abs_defined};
7.146 - val (_, thy) =
7.147 - thy
7.148 - |> Sign.add_path (Binding.name_of name)
7.149 - |> Global_Theory.add_thms
7.150 - ([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []),
7.151 - ((Binding.suffix_name "_strict" Abs_name, Abs_strict), []),
7.152 - ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
7.153 - ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
7.154 - ((Binding.suffix_name "_defined" Rep_name, Rep_defined), []),
7.155 - ((Binding.suffix_name "_defined" Abs_name, Abs_defined), [])])
7.156 - ||> Sign.parent_path;
7.157 - val pcpo_info =
7.158 - { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
7.159 - Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
7.160 - Rep_defined = Rep_defined, Abs_defined = Abs_defined };
7.161 - in
7.162 - (pcpo_info, thy)
7.163 - end;
7.164 -
7.165 -(* prepare_cpodef *)
7.166 -
7.167 -fun declare_type_name a =
7.168 - Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
7.169 -
7.170 -fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
7.171 - let
7.172 - val _ = Theory.requires thy "Pcpodef" "pcpodefs";
7.173 -
7.174 - (*rhs*)
7.175 - val tmp_ctxt =
7.176 - ProofContext.init_global thy
7.177 - |> fold (Variable.declare_typ o TFree) raw_args;
7.178 - val set = prep_term tmp_ctxt raw_set;
7.179 - val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
7.180 -
7.181 - val setT = Term.fastype_of set;
7.182 - val oldT = HOLogic.dest_setT setT handle TYPE _ =>
7.183 - error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
7.184 -
7.185 - (*lhs*)
7.186 - val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
7.187 - val full_tname = Sign.full_name thy tname;
7.188 - val newT = Type (full_tname, map TFree lhs_tfrees);
7.189 -
7.190 - val morphs = opt_morphs
7.191 - |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
7.192 - in
7.193 - (newT, oldT, set, morphs)
7.194 - end
7.195 -
7.196 -fun add_podef def opt_name typ set opt_morphs tac thy =
7.197 - let
7.198 - val name = the_default (#1 typ) opt_name;
7.199 - val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy
7.200 - |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
7.201 - val oldT = #rep_type (#1 info);
7.202 - val newT = #abs_type (#1 info);
7.203 - val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
7.204 -
7.205 - val RepC = Const (Rep_name, newT --> oldT);
7.206 - val below_eqn = Logic.mk_equals (below_const newT,
7.207 - Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
7.208 - val lthy3 = thy2
7.209 - |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
7.210 - val ((_, (_, below_ldef)), lthy4) = lthy3
7.211 - |> Specification.definition (NONE,
7.212 - ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
7.213 - val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4);
7.214 - val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
7.215 - val thy5 = lthy4
7.216 - |> Class.prove_instantiation_instance
7.217 - (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
7.218 - |> Local_Theory.exit_global;
7.219 - in ((info, below_def), thy5) end;
7.220 -
7.221 -fun prepare_cpodef
7.222 - (prep_term: Proof.context -> 'a -> term)
7.223 - (def: bool)
7.224 - (name: binding)
7.225 - (typ: binding * (string * sort) list * mixfix)
7.226 - (raw_set: 'a)
7.227 - (opt_morphs: (binding * binding) option)
7.228 - (thy: theory)
7.229 - : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
7.230 - let
7.231 - val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
7.232 - prepare prep_term name typ raw_set opt_morphs thy;
7.233 -
7.234 - val goal_nonempty =
7.235 - HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
7.236 - val goal_admissible =
7.237 - HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
7.238 -
7.239 - fun cpodef_result nonempty admissible thy =
7.240 - let
7.241 - val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
7.242 - |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
7.243 - val (cpo_info, thy3) = thy2
7.244 - |> prove_cpo name newT morphs type_definition set_def below_def admissible;
7.245 - in
7.246 - ((info, cpo_info), thy3)
7.247 - end;
7.248 - in
7.249 - (goal_nonempty, goal_admissible, cpodef_result)
7.250 - end
7.251 - handle ERROR msg =>
7.252 - cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
7.253 -
7.254 -fun prepare_pcpodef
7.255 - (prep_term: Proof.context -> 'a -> term)
7.256 - (def: bool)
7.257 - (name: binding)
7.258 - (typ: binding * (string * sort) list * mixfix)
7.259 - (raw_set: 'a)
7.260 - (opt_morphs: (binding * binding) option)
7.261 - (thy: theory)
7.262 - : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
7.263 - let
7.264 - val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
7.265 - prepare prep_term name typ raw_set opt_morphs thy;
7.266 -
7.267 - val goal_UU_mem =
7.268 - HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
7.269 -
7.270 - val goal_admissible =
7.271 - HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
7.272 -
7.273 - fun pcpodef_result UU_mem admissible thy =
7.274 - let
7.275 - val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
7.276 - val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
7.277 - |> add_podef def (SOME name) typ set opt_morphs tac;
7.278 - val (cpo_info, thy3) = thy2
7.279 - |> prove_cpo name newT morphs type_definition set_def below_def admissible;
7.280 - val (pcpo_info, thy4) = thy3
7.281 - |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem;
7.282 - in
7.283 - ((info, cpo_info, pcpo_info), thy4)
7.284 - end;
7.285 - in
7.286 - (goal_UU_mem, goal_admissible, pcpodef_result)
7.287 - end
7.288 - handle ERROR msg =>
7.289 - cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name));
7.290 -
7.291 -
7.292 -(* tactic interface *)
7.293 -
7.294 -fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
7.295 - let
7.296 - val name = the_default (#1 typ) opt_name;
7.297 - val (goal1, goal2, cpodef_result) =
7.298 - prepare_cpodef Syntax.check_term def name typ set opt_morphs thy;
7.299 - val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
7.300 - handle ERROR msg => cat_error msg
7.301 - ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
7.302 - val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
7.303 - handle ERROR msg => cat_error msg
7.304 - ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
7.305 - in cpodef_result thm1 thm2 thy end;
7.306 -
7.307 -fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
7.308 - let
7.309 - val name = the_default (#1 typ) opt_name;
7.310 - val (goal1, goal2, pcpodef_result) =
7.311 - prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy;
7.312 - val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
7.313 - handle ERROR msg => cat_error msg
7.314 - ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
7.315 - val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
7.316 - handle ERROR msg => cat_error msg
7.317 - ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
7.318 - in pcpodef_result thm1 thm2 thy end;
7.319 -
7.320 -
7.321 -(* proof interface *)
7.322 -
7.323 -local
7.324 -
7.325 -fun gen_cpodef_proof prep_term prep_constraint
7.326 - ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
7.327 - let
7.328 - val ctxt = ProofContext.init_global thy;
7.329 - val args = map (apsnd (prep_constraint ctxt)) raw_args;
7.330 - val (goal1, goal2, make_result) =
7.331 - prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
7.332 - fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
7.333 - | after_qed _ = raise Fail "cpodef_proof";
7.334 - in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
7.335 -
7.336 -fun gen_pcpodef_proof prep_term prep_constraint
7.337 - ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
7.338 - let
7.339 - val ctxt = ProofContext.init_global thy;
7.340 - val args = map (apsnd (prep_constraint ctxt)) raw_args;
7.341 - val (goal1, goal2, make_result) =
7.342 - prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
7.343 - fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
7.344 - | after_qed _ = raise Fail "pcpodef_proof";
7.345 - in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
7.346 -
7.347 -in
7.348 -
7.349 -fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x;
7.350 -fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x;
7.351 -
7.352 -fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x;
7.353 -fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x;
7.354 -
7.355 -end;
7.356 -
7.357 -
7.358 -
7.359 -(** outer syntax **)
7.360 -
7.361 -val typedef_proof_decl =
7.362 - Scan.optional (Parse.$$$ "(" |--
7.363 - ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
7.364 - Parse.binding >> (fn s => (true, SOME s)))
7.365 - --| Parse.$$$ ")") (true, NONE) --
7.366 - (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
7.367 - (Parse.$$$ "=" |-- Parse.term) --
7.368 - Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
7.369 -
7.370 -fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
7.371 - (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
7.372 - ((def, the_default t opt_name), (t, args, mx), A, morphs);
7.373 -
7.374 -val _ =
7.375 - Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
7.376 - Keyword.thy_goal
7.377 - (typedef_proof_decl >>
7.378 - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
7.379 -
7.380 -val _ =
7.381 - Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
7.382 - Keyword.thy_goal
7.383 - (typedef_proof_decl >>
7.384 - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
7.385 -
7.386 -end;