--- a/src/HOL/HOLCF/Cpodef.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy Wed Jan 10 15:25:09 2018 +0100
@@ -21,7 +21,7 @@
theorem typedef_po:
fixes Abs :: "'a::po \<Rightarrow> 'b::type"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "OFCLASS('b, po_class)"
apply (intro_classes, unfold below)
apply (rule below_refl)
@@ -51,14 +51,14 @@
subsection \<open>Proving a subtype is chain-finite\<close>
lemma ch2ch_Rep:
- assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
unfolding chain_def below .
theorem typedef_chfin:
fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "OFCLASS('b, chfin_class)"
apply intro_classes
apply (drule ch2ch_Rep [OF below])
@@ -79,14 +79,14 @@
\<close>
lemma typedef_is_lubI:
- assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
by (simp add: is_lub_def is_ub_def below)
lemma Abs_inverse_lub_Rep:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
apply (rule type_definition.Abs_inverse [OF type])
@@ -97,7 +97,7 @@
theorem typedef_is_lub:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
assumes S: "chain S"
shows "range S <<| Abs (\<Squnion>i. Rep (S i))"
@@ -117,7 +117,7 @@
theorem typedef_cpo:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "OFCLASS('b, cpo_class)"
proof
@@ -136,7 +136,7 @@
theorem typedef_cont_Rep:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. Rep (f x))"
apply (erule cont_apply [OF _ _ cont_const])
@@ -157,7 +157,7 @@
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
and f_in_A: "\<And>x. f x \<in> A"
shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
@@ -170,7 +170,7 @@
theorem typedef_compact:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "compact (Rep k) \<Longrightarrow> compact k"
proof (unfold compact_def)
@@ -192,7 +192,7 @@
theorem typedef_pcpo_generic:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and z_in_A: "z \<in> A"
and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
shows "OFCLASS('b, pcpo_class)"
@@ -211,7 +211,7 @@
theorem typedef_pcpo:
fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "OFCLASS('b, pcpo_class)"
by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
@@ -226,7 +226,7 @@
theorem typedef_Abs_strict:
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "Abs \<bottom> = \<bottom>"
apply (rule bottomI, unfold below)
@@ -235,7 +235,7 @@
theorem typedef_Rep_strict:
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "Rep \<bottom> = \<bottom>"
apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
@@ -244,7 +244,7 @@
theorem typedef_Abs_bottom_iff:
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
@@ -253,7 +253,7 @@
theorem typedef_Rep_bottom_iff:
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "(Rep x = \<bottom>) = (x = \<bottom>)"
apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
@@ -266,7 +266,7 @@
theorem typedef_flat:
fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "OFCLASS('b, flat_class)"
apply (intro_classes)