src/HOL/HOLCF/Cpodef.thy
changeset 41029 f7d8cfa6e7fc
parent 40834 a1249aeff5b6
child 41182 717404c7d59a
     1.1 --- a/src/HOL/HOLCF/Cpodef.thy	Mon Dec 06 08:43:52 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Mon Dec 06 08:59:58 2010 -0800
     1.3 @@ -250,20 +250,6 @@
     1.4   apply (simp add: type_definition.Rep_inject [OF type])
     1.5  done
     1.6  
     1.7 -theorem typedef_Abs_defined:
     1.8 -  assumes type: "type_definition Rep Abs A"
     1.9 -    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.10 -    and UU_in_A: "\<bottom> \<in> A"
    1.11 -  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
    1.12 -by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
    1.13 -
    1.14 -theorem typedef_Rep_defined:
    1.15 -  assumes type: "type_definition Rep Abs A"
    1.16 -    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.17 -    and UU_in_A: "\<bottom> \<in> A"
    1.18 -  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
    1.19 -by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
    1.20 -
    1.21  subsection {* Proving a subtype is flat *}
    1.22  
    1.23  theorem typedef_flat: