# HG changeset patch
# User huffman
# Date 1200684671 -3600
# Node ID aa0eca1ccb19bcd20950689db41e76af06f355f3
# Parent  3dc4acca43887a61fb2ed99150df4b01ab04fcd6
pcpodef generates strict_iff lemmas

diff -r 3dc4acca4388 -r aa0eca1ccb19 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Fri Jan 18 20:22:07 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy	Fri Jan 18 20:31:11 2008 +0100
@@ -29,7 +29,6 @@
  apply (erule (1) trans_less)
 done
 
-
 subsection {* Proving a subtype is finite *}
 
 context type_definition
@@ -139,7 +138,6 @@
   thus "\<exists>x. range S <<| x" ..
 qed
 
-
 subsubsection {* Continuity of @{term Rep} and @{term Abs} *}
 
 text {* For any sub-cpo, the @{term Rep} function is continuous. *}
@@ -265,23 +263,37 @@
  apply (rule type_definition.Abs_inverse [OF type UU_in_A])
 done
 
+theorem typedef_Abs_strict_iff:
+  assumes type: "type_definition Rep Abs A"
+    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
+ apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
+ apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
+done
+
+theorem typedef_Rep_strict_iff:
+  assumes type: "type_definition Rep Abs A"
+    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "(Rep x = \<bottom>) = (x = \<bottom>)"
+ apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
+ apply (simp add: type_definition.Rep_inject [OF type])
+done
+
 theorem typedef_Abs_defined:
   assumes type: "type_definition Rep Abs A"
     and less: "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>"
- apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
- apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
-done
+by (simp add: typedef_Abs_strict_iff [OF type less UU_in_A])
 
 theorem typedef_Rep_defined:
   assumes type: "type_definition Rep Abs A"
     and less: "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>"
- apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
- apply (simp add: type_definition.Rep_inject [OF type])
-done
+by (simp add: typedef_Rep_strict_iff [OF type less UU_in_A])
 
 subsection {* Proving a subtype is flat *}
 
diff -r 3dc4acca4388 -r aa0eca1ccb19 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Fri Jan 18 20:22:07 2008 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Fri Jan 18 20:31:11 2008 +0100
@@ -34,6 +34,8 @@
 val cont_Abs = thm "typedef_cont_Abs";
 val Rep_strict = thm "typedef_Rep_strict";
 val Abs_strict = thm "typedef_Abs_strict";
+val Rep_strict_iff = thm "typedef_Rep_strict_iff";
+val Abs_strict_iff = thm "typedef_Abs_strict_iff";
 val Rep_defined = thm "typedef_Rep_defined";
 val Abs_defined = thm "typedef_Abs_defined";
 
@@ -133,6 +135,8 @@
         |> PureThy.add_thms
             ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
               ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),
+              ((Rep_name ^ "_strict_iff", Rep_strict_iff OF pcpo_thms), []),
+              ((Abs_name ^ "_strict_iff", Abs_strict_iff OF pcpo_thms), []),
               ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
               ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
               ])