author huffman Fri Jan 18 20:31:11 2008 +0100 (2008-01-18) changeset 25926 aa0eca1ccb19 parent 25925 3dc4acca4388 child 25927 9c544dac6269
pcpodef generates strict_iff lemmas
 src/HOLCF/Pcpodef.thy file | annotate | diff | revisions src/HOLCF/Tools/pcpodef_package.ML file | annotate | diff | revisions
```     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                ])
```