src/HOL/HOLCF/Cpodef.thy
 changeset 41430 1aa23e9f2c87 parent 41182 717404c7d59a child 42151 4da4fc77664b
     1.1 --- a/src/HOL/HOLCF/Cpodef.thy	Tue Jan 04 15:03:27 2011 -0800
1.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Tue Jan 04 15:32:56 2011 -0800
1.3 @@ -203,9 +203,9 @@
1.4    fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
1.5    assumes type: "type_definition Rep Abs A"
1.6      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.7 -    and UU_in_A: "\<bottom> \<in> A"
1.8 +    and bottom_in_A: "\<bottom> \<in> A"
1.9    shows "OFCLASS('b, pcpo_class)"
1.10 -by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
1.11 +by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
1.12
1.13  subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
1.14
1.15 @@ -217,36 +217,36 @@
1.16  theorem typedef_Abs_strict:
1.17    assumes type: "type_definition Rep Abs A"
1.18      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.19 -    and UU_in_A: "\<bottom> \<in> A"
1.20 +    and bottom_in_A: "\<bottom> \<in> A"
1.21    shows "Abs \<bottom> = \<bottom>"
1.22 - apply (rule UU_I, unfold below)
1.23 - apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
1.24 + apply (rule bottomI, unfold below)
1.25 + apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])
1.26  done
1.27
1.28  theorem typedef_Rep_strict:
1.29    assumes type: "type_definition Rep Abs A"
1.30      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.31 -    and UU_in_A: "\<bottom> \<in> A"
1.32 +    and bottom_in_A: "\<bottom> \<in> A"
1.33    shows "Rep \<bottom> = \<bottom>"
1.34 - apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
1.35 - apply (rule type_definition.Abs_inverse [OF type UU_in_A])
1.36 + apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
1.37 + apply (rule type_definition.Abs_inverse [OF type bottom_in_A])
1.38  done
1.39
1.40  theorem typedef_Abs_bottom_iff:
1.41    assumes type: "type_definition Rep Abs A"
1.42      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.43 -    and UU_in_A: "\<bottom> \<in> A"
1.44 +    and bottom_in_A: "\<bottom> \<in> A"
1.45    shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
1.46 - apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
1.47 - apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
1.48 + apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
1.49 + apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)
1.50  done
1.51
1.52  theorem typedef_Rep_bottom_iff:
1.53    assumes type: "type_definition Rep Abs A"
1.54      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.55 -    and UU_in_A: "\<bottom> \<in> A"
1.56 +    and bottom_in_A: "\<bottom> \<in> A"
1.57    shows "(Rep x = \<bottom>) = (x = \<bottom>)"
1.58 - apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
1.59 + apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
1.60   apply (simp add: type_definition.Rep_inject [OF type])
1.61  done
1.62
1.63 @@ -256,12 +256,12 @@
1.64    fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
1.65    assumes type: "type_definition Rep Abs A"
1.66      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.67 -    and UU_in_A: "\<bottom> \<in> A"
1.68 +    and bottom_in_A: "\<bottom> \<in> A"
1.69    shows "OFCLASS('b, flat_class)"
1.70   apply (intro_classes)
1.71   apply (unfold below)
1.72   apply (simp add: type_definition.Rep_inject [OF type, symmetric])
1.73 - apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
1.74 + apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])