pcpodef generates strict_iff lemmas
authorhuffman
Fri Jan 18 20:31:11 2008 +0100 (2008-01-18)
changeset 25926aa0eca1ccb19
parent 25925 3dc4acca4388
child 25927 9c544dac6269
pcpodef generates strict_iff lemmas
src/HOLCF/Pcpodef.thy
src/HOLCF/Tools/pcpodef_package.ML
     1.1 --- a/src/HOLCF/Pcpodef.thy	Fri Jan 18 20:22:07 2008 +0100
     1.2 +++ b/src/HOLCF/Pcpodef.thy	Fri Jan 18 20:31:11 2008 +0100
     1.3 @@ -29,7 +29,6 @@
     1.4   apply (erule (1) trans_less)
     1.5  done
     1.6  
     1.7 -
     1.8  subsection {* Proving a subtype is finite *}
     1.9  
    1.10  context type_definition
    1.11 @@ -139,7 +138,6 @@
    1.12    thus "\<exists>x. range S <<| x" ..
    1.13  qed
    1.14  
    1.15 -
    1.16  subsubsection {* Continuity of @{term Rep} and @{term Abs} *}
    1.17  
    1.18  text {* For any sub-cpo, the @{term Rep} function is continuous. *}
    1.19 @@ -265,23 +263,37 @@
    1.20   apply (rule type_definition.Abs_inverse [OF type UU_in_A])
    1.21  done
    1.22  
    1.23 +theorem typedef_Abs_strict_iff:
    1.24 +  assumes type: "type_definition Rep Abs A"
    1.25 +    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.26 +    and UU_in_A: "\<bottom> \<in> A"
    1.27 +  shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
    1.28 + apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
    1.29 + apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
    1.30 +done
    1.31 +
    1.32 +theorem typedef_Rep_strict_iff:
    1.33 +  assumes type: "type_definition Rep Abs A"
    1.34 +    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.35 +    and UU_in_A: "\<bottom> \<in> A"
    1.36 +  shows "(Rep x = \<bottom>) = (x = \<bottom>)"
    1.37 + apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
    1.38 + apply (simp add: type_definition.Rep_inject [OF type])
    1.39 +done
    1.40 +
    1.41  theorem typedef_Abs_defined:
    1.42    assumes type: "type_definition Rep Abs A"
    1.43      and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.44      and UU_in_A: "\<bottom> \<in> A"
    1.45    shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
    1.46 - apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
    1.47 - apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
    1.48 -done
    1.49 +by (simp add: typedef_Abs_strict_iff [OF type less UU_in_A])
    1.50  
    1.51  theorem typedef_Rep_defined:
    1.52    assumes type: "type_definition Rep Abs A"
    1.53      and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.54      and UU_in_A: "\<bottom> \<in> A"
    1.55    shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
    1.56 - apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
    1.57 - apply (simp add: type_definition.Rep_inject [OF type])
    1.58 -done
    1.59 +by (simp add: typedef_Rep_strict_iff [OF type less UU_in_A])
    1.60  
    1.61  subsection {* Proving a subtype is flat *}
    1.62  
     2.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Fri Jan 18 20:22:07 2008 +0100
     2.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Fri Jan 18 20:31:11 2008 +0100
     2.3 @@ -34,6 +34,8 @@
     2.4  val cont_Abs = thm "typedef_cont_Abs";
     2.5  val Rep_strict = thm "typedef_Rep_strict";
     2.6  val Abs_strict = thm "typedef_Abs_strict";
     2.7 +val Rep_strict_iff = thm "typedef_Rep_strict_iff";
     2.8 +val Abs_strict_iff = thm "typedef_Abs_strict_iff";
     2.9  val Rep_defined = thm "typedef_Rep_defined";
    2.10  val Abs_defined = thm "typedef_Abs_defined";
    2.11  
    2.12 @@ -133,6 +135,8 @@
    2.13          |> PureThy.add_thms
    2.14              ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
    2.15                ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),
    2.16 +              ((Rep_name ^ "_strict_iff", Rep_strict_iff OF pcpo_thms), []),
    2.17 +              ((Abs_name ^ "_strict_iff", Abs_strict_iff OF pcpo_thms), []),
    2.18                ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
    2.19                ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
    2.20                ])