--- a/src/HOLCF/Cfun.thy Sat Nov 27 13:12:10 2010 -0800
+++ b/src/HOLCF/Cfun.thy Sat Nov 27 14:09:03 2010 -0800
@@ -6,7 +6,7 @@
header {* The type of continuous functions *}
theory Cfun
-imports Pcpodef Fun_Cpo Product_Cpo
+imports Cpodef Fun_Cpo Product_Cpo
begin
default_sort cpo
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Cpodef.thy Sat Nov 27 14:09:03 2010 -0800
@@ -0,0 +1,285 @@
+(* Title: HOLCF/Pcpodef.thy
+ Author: Brian Huffman
+*)
+
+header {* Subtypes of pcpos *}
+
+theory Cpodef
+imports Adm
+uses ("Tools/cpodef.ML")
+begin
+
+subsection {* Proving a subtype is a partial order *}
+
+text {*
+ A subtype of a partial order is itself a partial order,
+ if the ordering is defined in the standard way.
+*}
+
+setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
+
+theorem typedef_po:
+ fixes Abs :: "'a::po \<Rightarrow> 'b::type"
+ assumes type: "type_definition Rep Abs A"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ shows "OFCLASS('b, po_class)"
+ apply (intro_classes, unfold below)
+ apply (rule below_refl)
+ apply (erule (1) below_trans)
+ apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
+ apply (erule (1) below_antisym)
+done
+
+setup {* Sign.add_const_constraint (@{const_name Porder.below},
+ SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
+
+subsection {* Proving a subtype is finite *}
+
+lemma typedef_finite_UNIV:
+ fixes Abs :: "'a::type \<Rightarrow> 'b::type"
+ assumes type: "type_definition Rep Abs A"
+ shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
+proof -
+ assume "finite A"
+ hence "finite (Abs ` A)" by (rule finite_imageI)
+ thus "finite (UNIV :: 'b set)"
+ by (simp only: type_definition.Abs_image [OF type])
+qed
+
+subsection {* Proving a subtype is chain-finite *}
+
+lemma ch2ch_Rep:
+ assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
+unfolding chain_def below .
+
+theorem typedef_chfin:
+ fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
+ assumes type: "type_definition Rep Abs A"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ shows "OFCLASS('b, chfin_class)"
+ apply intro_classes
+ apply (drule ch2ch_Rep [OF below])
+ apply (drule chfin)
+ apply (unfold max_in_chain_def)
+ apply (simp add: type_definition.Rep_inject [OF type])
+done
+
+subsection {* Proving a subtype is complete *}
+
+text {*
+ A subtype of a cpo is itself a cpo if the ordering is
+ defined in the standard way, and the defining subset
+ is closed with respect to limits of chains. A set is
+ closed if and only if membership in the set is an
+ admissible predicate.
+*}
+
+lemma typedef_is_lubI:
+ assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
+unfolding is_lub_def is_ub_def below by simp
+
+lemma Abs_inverse_lub_Rep:
+ fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
+ assumes type: "type_definition Rep Abs A"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and adm: "adm (\<lambda>x. x \<in> A)"
+ shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
+ apply (rule type_definition.Abs_inverse [OF type])
+ apply (erule admD [OF adm ch2ch_Rep [OF below]])
+ apply (rule type_definition.Rep [OF type])
+done
+
+theorem typedef_is_lub:
+ fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
+ assumes type: "type_definition Rep Abs A"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and adm: "adm (\<lambda>x. x \<in> A)"
+ shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
+proof -
+ assume S: "chain S"
+ hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
+ hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
+ hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
+ by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
+ thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
+ by (rule typedef_is_lubI [OF below])
+qed
+
+lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
+
+theorem typedef_cpo:
+ fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
+ assumes type: "type_definition Rep Abs A"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and adm: "adm (\<lambda>x. x \<in> A)"
+ shows "OFCLASS('b, cpo_class)"
+proof
+ fix S::"nat \<Rightarrow> 'b" assume "chain S"
+ hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
+ by (rule typedef_is_lub [OF type below adm])
+ thus "\<exists>x. range S <<| x" ..
+qed
+
+subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
+
+text {* For any sub-cpo, the @{term Rep} function is continuous. *}
+
+theorem typedef_cont_Rep:
+ fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
+ assumes type: "type_definition Rep Abs A"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and adm: "adm (\<lambda>x. x \<in> A)"
+ shows "cont Rep"
+ apply (rule contI)
+ apply (simp only: typedef_lub [OF type below adm])
+ apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
+ apply (rule cpo_lubI)
+ apply (erule ch2ch_Rep [OF below])
+done
+
+text {*
+ For a sub-cpo, we can make the @{term Abs} function continuous
+ only if we restrict its domain to the defining subset by
+ composing it with another continuous function.
+*}
+
+theorem typedef_cont_Abs:
+ fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
+ fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
+ assumes type: "type_definition Rep Abs A"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
+ and f_in_A: "\<And>x. f x \<in> A"
+ shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
+unfolding cont_def is_lub_def is_ub_def ball_simps below
+by (simp add: type_definition.Abs_inverse [OF type f_in_A])
+
+subsection {* Proving subtype elements are compact *}
+
+theorem typedef_compact:
+ fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
+ assumes type: "type_definition Rep Abs A"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and adm: "adm (\<lambda>x. x \<in> A)"
+ shows "compact (Rep k) \<Longrightarrow> compact k"
+proof (unfold compact_def)
+ have cont_Rep: "cont Rep"
+ by (rule typedef_cont_Rep [OF type below adm])
+ assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
+ with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
+ thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
+qed
+
+subsection {* Proving a subtype is pointed *}
+
+text {*
+ A subtype of a cpo has a least element if and only if
+ the defining subset has a least element.
+*}
+
+theorem typedef_pcpo_generic:
+ fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
+ assumes type: "type_definition Rep Abs A"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and z_in_A: "z \<in> A"
+ and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
+ shows "OFCLASS('b, pcpo_class)"
+ apply (intro_classes)
+ apply (rule_tac x="Abs z" in exI, rule allI)
+ apply (unfold below)
+ apply (subst type_definition.Abs_inverse [OF type z_in_A])
+ apply (rule z_least [OF type_definition.Rep [OF type]])
+done
+
+text {*
+ As a special case, a subtype of a pcpo has a least element
+ if the defining subset contains @{term \<bottom>}.
+*}
+
+theorem typedef_pcpo:
+ fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
+ 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 "OFCLASS('b, pcpo_class)"
+by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
+
+subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
+
+text {*
+ For a sub-pcpo where @{term \<bottom>} is a member of the defining
+ subset, @{term Rep} and @{term Abs} are both strict.
+*}
+
+theorem typedef_Abs_strict:
+ 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 "Abs \<bottom> = \<bottom>"
+ apply (rule UU_I, unfold below)
+ apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
+done
+
+theorem typedef_Rep_strict:
+ 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 "Rep \<bottom> = \<bottom>"
+ apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
+ apply (rule type_definition.Abs_inverse [OF type UU_in_A])
+done
+
+theorem typedef_Abs_bottom_iff:
+ 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 \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
+ apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
+ apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
+done
+
+theorem typedef_Rep_bottom_iff:
+ 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 "(Rep x = \<bottom>) = (x = \<bottom>)"
+ apply (rule typedef_Rep_strict [OF type below 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 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:
+ fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
+ 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 "OFCLASS('b, flat_class)"
+ apply (intro_classes)
+ apply (unfold below)
+ apply (simp add: type_definition.Rep_inject [OF type, symmetric])
+ apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
+ apply (simp add: ax_flat)
+done
+
+subsection {* HOLCF type definition package *}
+
+use "Tools/cpodef.ML"
+
+end
--- a/src/HOLCF/IsaMakefile Sat Nov 27 13:12:10 2010 -0800
+++ b/src/HOLCF/IsaMakefile Sat Nov 27 14:09:03 2010 -0800
@@ -43,6 +43,7 @@
Completion.thy \
Cont.thy \
ConvexPD.thy \
+ Cpodef.thy \
Cprod.thy \
Discrete.thy \
Deflation.thy \
@@ -56,7 +57,6 @@
LowerPD.thy \
Map_Functions.thy \
One.thy \
- Pcpodef.thy \
Pcpo.thy \
Plain_HOLCF.thy \
Porder.thy \
@@ -78,9 +78,9 @@
Tools/Domain/domain_induction.ML \
Tools/Domain/domain_isomorphism.ML \
Tools/Domain/domain_take_proofs.ML \
+ Tools/cpodef.ML \
Tools/domaindef.ML \
Tools/fixrec.ML \
- Tools/pcpodef.ML \
document/root.tex
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
--- a/src/HOLCF/Pcpodef.thy Sat Nov 27 13:12:10 2010 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,285 +0,0 @@
-(* Title: HOLCF/Pcpodef.thy
- Author: Brian Huffman
-*)
-
-header {* Subtypes of pcpos *}
-
-theory Pcpodef
-imports Adm
-uses ("Tools/pcpodef.ML")
-begin
-
-subsection {* Proving a subtype is a partial order *}
-
-text {*
- A subtype of a partial order is itself a partial order,
- if the ordering is defined in the standard way.
-*}
-
-setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
-
-theorem typedef_po:
- fixes Abs :: "'a::po \<Rightarrow> 'b::type"
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- shows "OFCLASS('b, po_class)"
- apply (intro_classes, unfold below)
- apply (rule below_refl)
- apply (erule (1) below_trans)
- apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
- apply (erule (1) below_antisym)
-done
-
-setup {* Sign.add_const_constraint (@{const_name Porder.below},
- SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
-
-subsection {* Proving a subtype is finite *}
-
-lemma typedef_finite_UNIV:
- fixes Abs :: "'a::type \<Rightarrow> 'b::type"
- assumes type: "type_definition Rep Abs A"
- shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
-proof -
- assume "finite A"
- hence "finite (Abs ` A)" by (rule finite_imageI)
- thus "finite (UNIV :: 'b set)"
- by (simp only: type_definition.Abs_image [OF type])
-qed
-
-subsection {* Proving a subtype is chain-finite *}
-
-lemma ch2ch_Rep:
- assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
-unfolding chain_def below .
-
-theorem typedef_chfin:
- fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- shows "OFCLASS('b, chfin_class)"
- apply intro_classes
- apply (drule ch2ch_Rep [OF below])
- apply (drule chfin)
- apply (unfold max_in_chain_def)
- apply (simp add: type_definition.Rep_inject [OF type])
-done
-
-subsection {* Proving a subtype is complete *}
-
-text {*
- A subtype of a cpo is itself a cpo if the ordering is
- defined in the standard way, and the defining subset
- is closed with respect to limits of chains. A set is
- closed if and only if membership in the set is an
- admissible predicate.
-*}
-
-lemma typedef_is_lubI:
- assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
-unfolding is_lub_def is_ub_def below by simp
-
-lemma Abs_inverse_lub_Rep:
- fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and adm: "adm (\<lambda>x. x \<in> A)"
- shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
- apply (rule type_definition.Abs_inverse [OF type])
- apply (erule admD [OF adm ch2ch_Rep [OF below]])
- apply (rule type_definition.Rep [OF type])
-done
-
-theorem typedef_is_lub:
- fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and adm: "adm (\<lambda>x. x \<in> A)"
- shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
-proof -
- assume S: "chain S"
- hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
- hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
- hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
- by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
- thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
- by (rule typedef_is_lubI [OF below])
-qed
-
-lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
-
-theorem typedef_cpo:
- fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and adm: "adm (\<lambda>x. x \<in> A)"
- shows "OFCLASS('b, cpo_class)"
-proof
- fix S::"nat \<Rightarrow> 'b" assume "chain S"
- hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
- by (rule typedef_is_lub [OF type below adm])
- thus "\<exists>x. range S <<| x" ..
-qed
-
-subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
-
-text {* For any sub-cpo, the @{term Rep} function is continuous. *}
-
-theorem typedef_cont_Rep:
- fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and adm: "adm (\<lambda>x. x \<in> A)"
- shows "cont Rep"
- apply (rule contI)
- apply (simp only: typedef_lub [OF type below adm])
- apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
- apply (rule cpo_lubI)
- apply (erule ch2ch_Rep [OF below])
-done
-
-text {*
- For a sub-cpo, we can make the @{term Abs} function continuous
- only if we restrict its domain to the defining subset by
- composing it with another continuous function.
-*}
-
-theorem typedef_cont_Abs:
- fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
- fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
- and f_in_A: "\<And>x. f x \<in> A"
- shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
-unfolding cont_def is_lub_def is_ub_def ball_simps below
-by (simp add: type_definition.Abs_inverse [OF type f_in_A])
-
-subsection {* Proving subtype elements are compact *}
-
-theorem typedef_compact:
- fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and adm: "adm (\<lambda>x. x \<in> A)"
- shows "compact (Rep k) \<Longrightarrow> compact k"
-proof (unfold compact_def)
- have cont_Rep: "cont Rep"
- by (rule typedef_cont_Rep [OF type below adm])
- assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
- with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
- thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
-qed
-
-subsection {* Proving a subtype is pointed *}
-
-text {*
- A subtype of a cpo has a least element if and only if
- the defining subset has a least element.
-*}
-
-theorem typedef_pcpo_generic:
- fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and z_in_A: "z \<in> A"
- and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
- shows "OFCLASS('b, pcpo_class)"
- apply (intro_classes)
- apply (rule_tac x="Abs z" in exI, rule allI)
- apply (unfold below)
- apply (subst type_definition.Abs_inverse [OF type z_in_A])
- apply (rule z_least [OF type_definition.Rep [OF type]])
-done
-
-text {*
- As a special case, a subtype of a pcpo has a least element
- if the defining subset contains @{term \<bottom>}.
-*}
-
-theorem typedef_pcpo:
- fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
- 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 "OFCLASS('b, pcpo_class)"
-by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
-
-subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
-
-text {*
- For a sub-pcpo where @{term \<bottom>} is a member of the defining
- subset, @{term Rep} and @{term Abs} are both strict.
-*}
-
-theorem typedef_Abs_strict:
- 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 "Abs \<bottom> = \<bottom>"
- apply (rule UU_I, unfold below)
- apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
-done
-
-theorem typedef_Rep_strict:
- 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 "Rep \<bottom> = \<bottom>"
- apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
- apply (rule type_definition.Abs_inverse [OF type UU_in_A])
-done
-
-theorem typedef_Abs_bottom_iff:
- 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 \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
- apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
-done
-
-theorem typedef_Rep_bottom_iff:
- 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 "(Rep x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Rep_strict [OF type below 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 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:
- fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
- 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 "OFCLASS('b, flat_class)"
- apply (intro_classes)
- apply (unfold below)
- apply (simp add: type_definition.Rep_inject [OF type, symmetric])
- apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
- apply (simp add: ax_flat)
-done
-
-subsection {* HOLCF type definition package *}
-
-use "Tools/pcpodef.ML"
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/cpodef.ML Sat Nov 27 14:09:03 2010 -0800
@@ -0,0 +1,383 @@
+(* Title: HOLCF/Tools/cpodef.ML
+ Author: Brian Huffman
+
+Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
+typedef (see also ~~/src/HOL/Tools/typedef.ML).
+*)
+
+signature CPODEF =
+sig
+ type cpo_info =
+ { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
+ is_lub: 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 }
+
+ val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+ term -> (binding * binding) option -> tactic -> theory ->
+ (Typedef.info * thm) * theory
+ val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+ term -> (binding * binding) option -> tactic * tactic -> theory ->
+ (Typedef.info * cpo_info) * theory
+ val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+ term -> (binding * binding) option -> tactic * tactic -> theory ->
+ (Typedef.info * cpo_info * pcpo_info) * theory
+
+ val cpodef_proof: (bool * binding)
+ * (binding * (string * sort) list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val cpodef_proof_cmd: (bool * binding)
+ * (binding * (string * string option) list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
+ val pcpodef_proof: (bool * binding)
+ * (binding * (string * sort) list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val pcpodef_proof_cmd: (bool * binding)
+ * (binding * (string * string option) list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
+end;
+
+structure Cpodef :> CPODEF =
+struct
+
+(** type definitions **)
+
+type cpo_info =
+ { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
+ is_lub: 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 }
+
+(* building terms *)
+
+fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
+fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
+
+fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
+
+(* manipulating theorems *)
+
+fun fold_adm_mem thm NONE = thm
+ | fold_adm_mem thm (SOME set_def) =
+ let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
+ in rule OF [set_def, thm] end;
+
+fun fold_UU_mem thm NONE = thm
+ | fold_UU_mem thm (SOME set_def) =
+ let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
+ in rule OF [set_def, thm] end;
+
+(* proving class instances *)
+
+fun prove_cpo
+ (name: binding)
+ (newT: typ)
+ (Rep_name: binding, Abs_name: binding)
+ (type_definition: thm) (* type_definition Rep Abs A *)
+ (set_def: thm option) (* A == set *)
+ (below_def: thm) (* op << == %x y. Rep x << Rep y *)
+ (admissible: thm) (* adm (%x. x : set) *)
+ (thy: theory)
+ =
+ let
+ val admissible' = fold_adm_mem admissible set_def;
+ val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
+ val (full_tname, Ts) = dest_Type newT;
+ val lhs_sorts = map (snd o dest_TFree) Ts;
+ val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1;
+ val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
+ (* transfer thms so that they will know about the new cpo instance *)
+ val cpo_thms' = map (Thm.transfer thy) cpo_thms;
+ fun make thm = Drule.zero_var_indexes (thm OF cpo_thms');
+ val cont_Rep = make @{thm typedef_cont_Rep};
+ val cont_Abs = make @{thm typedef_cont_Abs};
+ val is_lub = make @{thm typedef_is_lub};
+ val lub = make @{thm typedef_lub};
+ val compact = make @{thm typedef_compact};
+ val (_, thy) =
+ thy
+ |> Sign.add_path (Binding.name_of name)
+ |> Global_Theory.add_thms
+ ([((Binding.prefix_name "adm_" name, admissible'), []),
+ ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []),
+ ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []),
+ ((Binding.prefix_name "is_lub_" name, is_lub ), []),
+ ((Binding.prefix_name "lub_" name, lub ), []),
+ ((Binding.prefix_name "compact_" name, compact ), [])])
+ ||> Sign.parent_path;
+ val cpo_info : cpo_info =
+ { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
+ cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact };
+ in
+ (cpo_info, thy)
+ end;
+
+fun prove_pcpo
+ (name: binding)
+ (newT: typ)
+ (Rep_name: binding, Abs_name: binding)
+ (type_definition: thm) (* type_definition Rep Abs A *)
+ (set_def: thm option) (* A == set *)
+ (below_def: thm) (* op << == %x y. Rep x << Rep y *)
+ (UU_mem: thm) (* UU : set *)
+ (thy: theory)
+ =
+ let
+ val UU_mem' = fold_UU_mem UU_mem set_def;
+ val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
+ val (full_tname, Ts) = dest_Type newT;
+ val lhs_sorts = map (snd o dest_TFree) Ts;
+ val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
+ val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
+ val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
+ fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
+ val Rep_strict = make @{thm typedef_Rep_strict};
+ 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)
+ |> Global_Theory.add_thms
+ ([((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), [])])
+ ||> 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 };
+ in
+ (pcpo_info, thy)
+ end;
+
+(* prepare_cpodef *)
+
+fun declare_type_name a =
+ Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
+
+fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
+ let
+ val _ = Theory.requires thy "Cpodef" "cpodefs";
+
+ (*rhs*)
+ val tmp_ctxt =
+ ProofContext.init_global thy
+ |> fold (Variable.declare_typ o TFree) raw_args;
+ val set = prep_term tmp_ctxt raw_set;
+ val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
+
+ val setT = Term.fastype_of set;
+ val oldT = HOLogic.dest_setT setT handle TYPE _ =>
+ error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
+
+ (*lhs*)
+ val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
+ val full_tname = Sign.full_name thy tname;
+ val newT = Type (full_tname, map TFree lhs_tfrees);
+
+ val morphs = opt_morphs
+ |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
+ in
+ (newT, oldT, set, morphs)
+ end
+
+fun add_podef def opt_name typ set opt_morphs tac thy =
+ let
+ val name = the_default (#1 typ) opt_name;
+ val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy
+ |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
+ val oldT = #rep_type (#1 info);
+ val newT = #abs_type (#1 info);
+ val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
+
+ val RepC = Const (Rep_name, newT --> oldT);
+ val below_eqn = Logic.mk_equals (below_const newT,
+ Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
+ val lthy3 = thy2
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
+ val ((_, (_, below_ldef)), lthy4) = lthy3
+ |> Specification.definition (NONE,
+ ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
+ val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4);
+ val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
+ val thy5 = lthy4
+ |> Class.prove_instantiation_instance
+ (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
+ |> Local_Theory.exit_global;
+ in ((info, below_def), thy5) end;
+
+fun prepare_cpodef
+ (prep_term: Proof.context -> 'a -> term)
+ (def: bool)
+ (name: binding)
+ (typ: binding * (string * sort) list * mixfix)
+ (raw_set: 'a)
+ (opt_morphs: (binding * binding) option)
+ (thy: theory)
+ : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
+ let
+ val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
+ prepare prep_term name typ raw_set opt_morphs thy;
+
+ val goal_nonempty =
+ HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+ val goal_admissible =
+ HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+
+ fun cpodef_result nonempty admissible thy =
+ let
+ val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
+ |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
+ val (cpo_info, thy3) = thy2
+ |> prove_cpo name newT morphs type_definition set_def below_def admissible;
+ in
+ ((info, cpo_info), thy3)
+ end;
+ in
+ (goal_nonempty, goal_admissible, cpodef_result)
+ end
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
+
+fun prepare_pcpodef
+ (prep_term: Proof.context -> 'a -> term)
+ (def: bool)
+ (name: binding)
+ (typ: binding * (string * sort) list * mixfix)
+ (raw_set: 'a)
+ (opt_morphs: (binding * binding) option)
+ (thy: theory)
+ : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
+ let
+ val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
+ prepare prep_term name typ raw_set opt_morphs thy;
+
+ val goal_UU_mem =
+ HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
+
+ val goal_admissible =
+ HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+
+ fun pcpodef_result UU_mem admissible thy =
+ let
+ val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
+ val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
+ |> add_podef def (SOME name) typ set opt_morphs tac;
+ val (cpo_info, thy3) = thy2
+ |> prove_cpo name newT morphs type_definition set_def below_def admissible;
+ val (pcpo_info, thy4) = thy3
+ |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem;
+ in
+ ((info, cpo_info, pcpo_info), thy4)
+ end;
+ in
+ (goal_UU_mem, goal_admissible, pcpodef_result)
+ end
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name));
+
+
+(* tactic interface *)
+
+fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+ let
+ val name = the_default (#1 typ) opt_name;
+ val (goal1, goal2, cpodef_result) =
+ prepare_cpodef Syntax.check_term def name typ set opt_morphs thy;
+ val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+ handle ERROR msg => cat_error msg
+ ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
+ val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+ handle ERROR msg => cat_error msg
+ ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
+ in cpodef_result thm1 thm2 thy end;
+
+fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+ let
+ val name = the_default (#1 typ) opt_name;
+ val (goal1, goal2, pcpodef_result) =
+ prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy;
+ val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+ handle ERROR msg => cat_error msg
+ ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
+ val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+ handle ERROR msg => cat_error msg
+ ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
+ in pcpodef_result thm1 thm2 thy end;
+
+
+(* proof interface *)
+
+local
+
+fun gen_cpodef_proof prep_term prep_constraint
+ ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
+ let
+ val ctxt = ProofContext.init_global thy;
+ val args = map (apsnd (prep_constraint ctxt)) raw_args;
+ val (goal1, goal2, make_result) =
+ prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
+ fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
+ | after_qed _ = raise Fail "cpodef_proof";
+ in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+
+fun gen_pcpodef_proof prep_term prep_constraint
+ ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
+ let
+ val ctxt = ProofContext.init_global thy;
+ val args = map (apsnd (prep_constraint ctxt)) raw_args;
+ val (goal1, goal2, make_result) =
+ prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
+ fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
+ | after_qed _ = raise Fail "pcpodef_proof";
+ in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+
+in
+
+fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x;
+fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x;
+
+fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x;
+fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x;
+
+end;
+
+
+
+(** outer syntax **)
+
+val typedef_proof_decl =
+ Scan.optional (Parse.$$$ "(" |--
+ ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Parse.binding >> (fn s => (true, SOME s)))
+ --| Parse.$$$ ")") (true, NONE) --
+ (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
+ (Parse.$$$ "=" |-- Parse.term) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
+
+fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
+ (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
+ ((def, the_default t opt_name), (t, args, mx), A, morphs);
+
+val _ =
+ Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
+ Keyword.thy_goal
+ (typedef_proof_decl >>
+ (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
+
+val _ =
+ Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
+ Keyword.thy_goal
+ (typedef_proof_decl >>
+ (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
+
+end;
--- a/src/HOLCF/Tools/domaindef.ML Sat Nov 27 13:12:10 2010 -0800
+++ b/src/HOLCF/Tools/domaindef.ML Sat Nov 27 14:09:03 2010 -0800
@@ -19,7 +19,7 @@
val add_domaindef: bool -> binding option -> binding * (string * sort) list * mixfix ->
term -> (binding * binding) option -> theory ->
- (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory
+ (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory
val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string
* (binding * binding) option -> theory -> theory
@@ -86,7 +86,7 @@
(raw_defl: 'a)
(opt_morphs: (binding * binding) option)
(thy: theory)
- : (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory =
+ : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
let
val _ = Theory.requires thy "Domain" "domaindefs";
@@ -118,7 +118,7 @@
val tac1 = rtac @{thm defl_set_bottom} 1;
val tac2 = rtac @{thm adm_defl_set} 1;
val ((info, cpo_info, pcpo_info), thy) = thy
- |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
+ |> Cpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
(*definitions*)
val Rep_const = Const (#Rep_name (#1 info), newT --> udomT);
--- a/src/HOLCF/Tools/pcpodef.ML Sat Nov 27 13:12:10 2010 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,383 +0,0 @@
-(* Title: HOLCF/Tools/pcpodef.ML
- Author: Brian Huffman
-
-Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
-typedef (see also ~~/src/HOL/Tools/typedef.ML).
-*)
-
-signature PCPODEF =
-sig
- type cpo_info =
- { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
- is_lub: 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 }
-
- val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> tactic -> theory ->
- (Typedef.info * thm) * theory
- val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> tactic * tactic -> theory ->
- (Typedef.info * cpo_info) * theory
- val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> tactic * tactic -> theory ->
- (Typedef.info * cpo_info * pcpo_info) * theory
-
- val cpodef_proof: (bool * binding)
- * (binding * (string * sort) list * mixfix) * term
- * (binding * binding) option -> theory -> Proof.state
- val cpodef_proof_cmd: (bool * binding)
- * (binding * (string * string option) list * mixfix) * string
- * (binding * binding) option -> theory -> Proof.state
- val pcpodef_proof: (bool * binding)
- * (binding * (string * sort) list * mixfix) * term
- * (binding * binding) option -> theory -> Proof.state
- val pcpodef_proof_cmd: (bool * binding)
- * (binding * (string * string option) list * mixfix) * string
- * (binding * binding) option -> theory -> Proof.state
-end;
-
-structure Pcpodef :> PCPODEF =
-struct
-
-(** type definitions **)
-
-type cpo_info =
- { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
- is_lub: 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 }
-
-(* building terms *)
-
-fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
-fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
-
-fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
-
-(* manipulating theorems *)
-
-fun fold_adm_mem thm NONE = thm
- | fold_adm_mem thm (SOME set_def) =
- let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
- in rule OF [set_def, thm] end;
-
-fun fold_UU_mem thm NONE = thm
- | fold_UU_mem thm (SOME set_def) =
- let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
- in rule OF [set_def, thm] end;
-
-(* proving class instances *)
-
-fun prove_cpo
- (name: binding)
- (newT: typ)
- (Rep_name: binding, Abs_name: binding)
- (type_definition: thm) (* type_definition Rep Abs A *)
- (set_def: thm option) (* A == set *)
- (below_def: thm) (* op << == %x y. Rep x << Rep y *)
- (admissible: thm) (* adm (%x. x : set) *)
- (thy: theory)
- =
- let
- val admissible' = fold_adm_mem admissible set_def;
- val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
- val (full_tname, Ts) = dest_Type newT;
- val lhs_sorts = map (snd o dest_TFree) Ts;
- val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1;
- val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
- (* transfer thms so that they will know about the new cpo instance *)
- val cpo_thms' = map (Thm.transfer thy) cpo_thms;
- fun make thm = Drule.zero_var_indexes (thm OF cpo_thms');
- val cont_Rep = make @{thm typedef_cont_Rep};
- val cont_Abs = make @{thm typedef_cont_Abs};
- val is_lub = make @{thm typedef_is_lub};
- val lub = make @{thm typedef_lub};
- val compact = make @{thm typedef_compact};
- val (_, thy) =
- thy
- |> Sign.add_path (Binding.name_of name)
- |> Global_Theory.add_thms
- ([((Binding.prefix_name "adm_" name, admissible'), []),
- ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []),
- ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []),
- ((Binding.prefix_name "is_lub_" name, is_lub ), []),
- ((Binding.prefix_name "lub_" name, lub ), []),
- ((Binding.prefix_name "compact_" name, compact ), [])])
- ||> Sign.parent_path;
- val cpo_info : cpo_info =
- { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
- cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact };
- in
- (cpo_info, thy)
- end;
-
-fun prove_pcpo
- (name: binding)
- (newT: typ)
- (Rep_name: binding, Abs_name: binding)
- (type_definition: thm) (* type_definition Rep Abs A *)
- (set_def: thm option) (* A == set *)
- (below_def: thm) (* op << == %x y. Rep x << Rep y *)
- (UU_mem: thm) (* UU : set *)
- (thy: theory)
- =
- let
- val UU_mem' = fold_UU_mem UU_mem set_def;
- val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
- val (full_tname, Ts) = dest_Type newT;
- val lhs_sorts = map (snd o dest_TFree) Ts;
- val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
- val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
- val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
- fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
- val Rep_strict = make @{thm typedef_Rep_strict};
- 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)
- |> Global_Theory.add_thms
- ([((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), [])])
- ||> 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 };
- in
- (pcpo_info, thy)
- end;
-
-(* prepare_cpodef *)
-
-fun declare_type_name a =
- Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-
-fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
- let
- val _ = Theory.requires thy "Pcpodef" "pcpodefs";
-
- (*rhs*)
- val tmp_ctxt =
- ProofContext.init_global thy
- |> fold (Variable.declare_typ o TFree) raw_args;
- val set = prep_term tmp_ctxt raw_set;
- val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
-
- val setT = Term.fastype_of set;
- val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
-
- (*lhs*)
- val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
- val full_tname = Sign.full_name thy tname;
- val newT = Type (full_tname, map TFree lhs_tfrees);
-
- val morphs = opt_morphs
- |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
- in
- (newT, oldT, set, morphs)
- end
-
-fun add_podef def opt_name typ set opt_morphs tac thy =
- let
- val name = the_default (#1 typ) opt_name;
- val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy
- |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
- val oldT = #rep_type (#1 info);
- val newT = #abs_type (#1 info);
- val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
-
- val RepC = Const (Rep_name, newT --> oldT);
- val below_eqn = Logic.mk_equals (below_const newT,
- Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
- val lthy3 = thy2
- |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
- val ((_, (_, below_ldef)), lthy4) = lthy3
- |> Specification.definition (NONE,
- ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
- val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4);
- val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
- val thy5 = lthy4
- |> Class.prove_instantiation_instance
- (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
- |> Local_Theory.exit_global;
- in ((info, below_def), thy5) end;
-
-fun prepare_cpodef
- (prep_term: Proof.context -> 'a -> term)
- (def: bool)
- (name: binding)
- (typ: binding * (string * sort) list * mixfix)
- (raw_set: 'a)
- (opt_morphs: (binding * binding) option)
- (thy: theory)
- : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
- let
- val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
- prepare prep_term name typ raw_set opt_morphs thy;
-
- val goal_nonempty =
- HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
- val goal_admissible =
- HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
-
- fun cpodef_result nonempty admissible thy =
- let
- val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
- |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
- val (cpo_info, thy3) = thy2
- |> prove_cpo name newT morphs type_definition set_def below_def admissible;
- in
- ((info, cpo_info), thy3)
- end;
- in
- (goal_nonempty, goal_admissible, cpodef_result)
- end
- handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
-
-fun prepare_pcpodef
- (prep_term: Proof.context -> 'a -> term)
- (def: bool)
- (name: binding)
- (typ: binding * (string * sort) list * mixfix)
- (raw_set: 'a)
- (opt_morphs: (binding * binding) option)
- (thy: theory)
- : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
- let
- val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
- prepare prep_term name typ raw_set opt_morphs thy;
-
- val goal_UU_mem =
- HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
-
- val goal_admissible =
- HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
-
- fun pcpodef_result UU_mem admissible thy =
- let
- val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
- val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
- |> add_podef def (SOME name) typ set opt_morphs tac;
- val (cpo_info, thy3) = thy2
- |> prove_cpo name newT morphs type_definition set_def below_def admissible;
- val (pcpo_info, thy4) = thy3
- |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem;
- in
- ((info, cpo_info, pcpo_info), thy4)
- end;
- in
- (goal_UU_mem, goal_admissible, pcpodef_result)
- end
- handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name));
-
-
-(* tactic interface *)
-
-fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
- let
- val name = the_default (#1 typ) opt_name;
- val (goal1, goal2, cpodef_result) =
- prepare_cpodef Syntax.check_term def name typ set opt_morphs thy;
- val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
- handle ERROR msg => cat_error msg
- ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
- val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
- handle ERROR msg => cat_error msg
- ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
- in cpodef_result thm1 thm2 thy end;
-
-fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
- let
- val name = the_default (#1 typ) opt_name;
- val (goal1, goal2, pcpodef_result) =
- prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy;
- val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
- handle ERROR msg => cat_error msg
- ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
- val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
- handle ERROR msg => cat_error msg
- ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
- in pcpodef_result thm1 thm2 thy end;
-
-
-(* proof interface *)
-
-local
-
-fun gen_cpodef_proof prep_term prep_constraint
- ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
- let
- val ctxt = ProofContext.init_global thy;
- val args = map (apsnd (prep_constraint ctxt)) raw_args;
- val (goal1, goal2, make_result) =
- prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
- fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
- | after_qed _ = raise Fail "cpodef_proof";
- in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
-
-fun gen_pcpodef_proof prep_term prep_constraint
- ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
- let
- val ctxt = ProofContext.init_global thy;
- val args = map (apsnd (prep_constraint ctxt)) raw_args;
- val (goal1, goal2, make_result) =
- prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
- fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
- | after_qed _ = raise Fail "pcpodef_proof";
- in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
-
-in
-
-fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x;
-fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x;
-
-fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x;
-fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x;
-
-end;
-
-
-
-(** outer syntax **)
-
-val typedef_proof_decl =
- Scan.optional (Parse.$$$ "(" |--
- ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
- Parse.binding >> (fn s => (true, SOME s)))
- --| Parse.$$$ ")") (true, NONE) --
- (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
- (Parse.$$$ "=" |-- Parse.term) --
- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
-
-fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
- (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
- ((def, the_default t opt_name), (t, args, mx), A, morphs);
-
-val _ =
- Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
- Keyword.thy_goal
- (typedef_proof_decl >>
- (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
-
-val _ =
- Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
- Keyword.thy_goal
- (typedef_proof_decl >>
- (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
-
-end;