# HG changeset patch
# User huffman
# Date 1291654798 28800
# Node ID f7d8cfa6e7fc6c713aa8ffe6a2343d457630883f
# Parent  0acff85f95c7fe39b2a291cf76185a663841cd62
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead

diff -r 0acff85f95c7 -r f7d8cfa6e7fc src/HOL/HOLCF/Cpodef.thy
--- a/src/HOL/HOLCF/Cpodef.thy	Mon Dec 06 08:43:52 2010 -0800
+++ b/src/HOL/HOLCF/Cpodef.thy	Mon Dec 06 08:59:58 2010 -0800
@@ -250,20 +250,6 @@
  apply (simp add: type_definition.Rep_inject [OF type])
 done
 
-theorem typedef_Abs_defined:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
-by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
-
-theorem typedef_Rep_defined:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
-by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
-
 subsection {* Proving a subtype is flat *}
 
 theorem typedef_flat:
diff -r 0acff85f95c7 -r f7d8cfa6e7fc src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 08:43:52 2010 -0800
+++ b/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 08:59:58 2010 -0800
@@ -36,10 +36,10 @@
 done
 
 lemma succeed_defined [simp]: "succeed\<cdot>x \<noteq> \<bottom>"
-by (simp add: succeed_def cont_Abs_match Abs_match_defined)
+by (simp add: succeed_def cont_Abs_match Abs_match_bottom_iff)
 
 lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
-by (simp add: fail_def Abs_match_defined)
+by (simp add: fail_def Abs_match_bottom_iff)
 
 lemma succeed_eq [simp]: "(succeed\<cdot>x = succeed\<cdot>y) = (x = y)"
 by (simp add: succeed_def cont_Abs_match Abs_match_inject)
diff -r 0acff85f95c7 -r f7d8cfa6e7fc src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Dec 06 08:43:52 2010 -0800
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Dec 06 08:59:58 2010 -0800
@@ -11,8 +11,8 @@
     { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
       lub: thm, compact: thm }
   type pcpo_info =
-    { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
-      Rep_defined: thm, Abs_defined: thm }
+    { Rep_strict: thm, Abs_strict: thm,
+      Rep_bottom_iff: thm, Abs_bottom_iff: thm }
 
   val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic -> theory ->
@@ -48,8 +48,8 @@
     lub: thm, compact: thm }
 
 type pcpo_info =
-  { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
-    Rep_defined: thm, Abs_defined: thm }
+  { Rep_strict: thm, Abs_strict: thm,
+    Rep_bottom_iff: thm, Abs_bottom_iff: thm }
 
 (* building terms *)
 
@@ -136,8 +136,6 @@
     val Abs_strict = make @{thm typedef_Abs_strict}
     val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff}
     val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff}
-    val Rep_defined = make @{thm typedef_Rep_defined}
-    val Abs_defined = make @{thm typedef_Abs_defined}
     val (_, thy) =
       thy
       |> Sign.add_path (Binding.name_of name)
@@ -145,14 +143,11 @@
         ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
           ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
           ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
-          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
-          ((Binding.suffix_name "_defined"    Rep_name, Rep_defined), []),
-          ((Binding.suffix_name "_defined"    Abs_name, Abs_defined), [])])
+          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), [])])
       ||> Sign.parent_path
     val pcpo_info =
       { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
-        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
-        Rep_defined = Rep_defined, Abs_defined = Abs_defined }
+        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff }
   in
     (pcpo_info, thy)
   end