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])
    1.75   apply (simp add: ax_flat)
    1.76  done
    1.77