--- a/NEWS Sat Nov 27 22:02:16 2010 +0100
+++ b/NEWS Sat Nov 27 14:34:54 2010 -0800
@@ -461,6 +461,22 @@
* Case combinators generated by the domain package for type 'foo'
are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
+* Several theorems have been renamed to more accurately reflect the
+names of constants and types involved. INCOMPATIBILITY.
+ thelub_const ~> lub_const
+ lub_const ~> is_lub_const
+ thelubI ~> lub_eqI
+ is_lub_lub ~> is_lubD2
+ lubI ~> is_lub_lub
+ unique_lub ~> is_lub_unique
+ is_ub_lub ~> is_lub_rangeD1
+ lub_bin_chain ~> is_lub_bin_chain
+ thelub_Pair ~> lub_Pair
+ lub_cprod ~> is_lub_prod
+ thelub_cprod ~> lub_prod
+ minimal_cprod ~> minimal_prod
+ inst_cprod_pcpo ~> inst_prod_pcpo
+
* Many legacy theorem names have been discontinued. INCOMPATIBILITY.
sq_ord_less_eq_trans ~> below_eq_trans
sq_ord_eq_less_trans ~> eq_below_trans
--- a/src/HOLCF/Bifinite.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Bifinite.thy Sat Nov 27 14:34:54 2010 -0800
@@ -642,7 +642,7 @@
apply (simp add: contlub_cfun_fun)
apply (simp add: discr_approx_def)
apply (case_tac x, simp)
-apply (rule thelubI)
+apply (rule lub_eqI)
apply (rule is_lubI)
apply (rule ub_rangeI, simp)
apply (drule ub_rangeD)
--- a/src/HOLCF/Cfun.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Cfun.thy Sat Nov 27 14:34:54 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
@@ -209,15 +209,9 @@
lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
by (rule cont_Rep_cfun2 [THEN cont2contlubE])
-lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
-by (rule cont_Rep_cfun2 [THEN contE])
-
lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
by (rule cont_Rep_cfun1 [THEN cont2contlubE])
-lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
-by (rule cont_Rep_cfun1 [THEN contE])
-
text {* monotonicity of application *}
lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
@@ -264,7 +258,7 @@
lemma contlub_LAM:
"\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
\<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
-apply (simp add: thelub_cfun)
+apply (simp add: lub_cfun)
apply (simp add: Abs_cfun_inverse2)
apply (simp add: thelub_fun ch2ch_lambda)
done
@@ -287,7 +281,7 @@
by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
-by (rule lub_cfun [THEN thelubI])
+by (rule lub_cfun [THEN lub_eqI])
subsection {* Continuity simplification procedure *}
@@ -370,7 +364,7 @@
apply (rule allI)
apply (subst contlub_cfun_fun)
apply assumption
-apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
+apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
done
lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
@@ -484,28 +478,28 @@
default_sort pcpo
definition
- strict :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
- "strict = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
+ seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
+ "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
-lemma cont_strict: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
+lemma cont_seq: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
unfolding cont_def is_lub_def is_ub_def ball_simps
by (simp add: lub_eq_bottom_iff)
-lemma strict_conv_if: "strict\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
-unfolding strict_def by (simp add: cont_strict)
+lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
+unfolding seq_def by (simp add: cont_seq)
-lemma strict1 [simp]: "strict\<cdot>\<bottom> = \<bottom>"
-by (simp add: strict_conv_if)
+lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
+by (simp add: seq_conv_if)
-lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID"
-by (simp add: strict_conv_if)
+lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
+by (simp add: seq_conv_if)
-lemma strict3 [simp]: "strict\<cdot>x\<cdot>\<bottom> = \<bottom>"
-by (simp add: strict_conv_if)
+lemma seq3 [simp]: "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
+by (simp add: seq_conv_if)
definition
strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
- "strictify = (\<Lambda> f x. strict\<cdot>x\<cdot>(f\<cdot>x))"
+ "strictify = (\<Lambda> f x. seq\<cdot>x\<cdot>(f\<cdot>x))"
lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
unfolding strictify_def by simp
--- a/src/HOLCF/Completion.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Completion.thy Sat Nov 27 14:34:54 2010 -0800
@@ -55,7 +55,7 @@
lemma lub_image_principal:
assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
-apply (rule thelubI)
+apply (rule lub_eqI)
apply (rule is_lub_maximal)
apply (rule ub_imageI)
apply (simp add: f)
@@ -100,7 +100,7 @@
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
assumes S: "chain S"
shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))"
- and typedef_ideal_rep_contlub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
+ and typedef_ideal_rep_lub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
proof -
have 1: "ideal (\<Union>i. Rep (S i))"
apply (rule ideal_UN)
@@ -117,7 +117,7 @@
apply (simp add: below 2 is_ub_def, fast)
done
hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
- by (rule thelubI)
+ by (rule lub_eqI)
show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
by (simp add: 4 2)
qed
@@ -140,13 +140,13 @@
subsection {* Lemmas about least upper bounds *}
lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
-apply (erule exE, drule lubI)
+apply (erule exE, drule is_lub_lub)
apply (drule is_lubD1)
apply (erule (1) is_ubD)
done
lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
-by (erule exE, drule lubI, erule is_lub_lub)
+by (erule exE, drule is_lub_lub, erule is_lubD2)
subsection {* Locale for ideal completion *}
@@ -154,7 +154,7 @@
fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
assumes ideal_rep: "\<And>x. ideal (rep x)"
- assumes rep_contlub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
+ assumes rep_lub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f"
@@ -162,8 +162,8 @@
lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
apply (frule bin_chain)
-apply (drule rep_contlub)
-apply (simp only: thelubI [OF lub_bin_chain])
+apply (drule rep_lub)
+apply (simp only: lub_eqI [OF is_lub_bin_chain])
apply (rule subsetI, rule UN_I [where a=0], simp_all)
done
@@ -215,7 +215,7 @@
subsubsection {* Principal ideals approximate all elements *}
lemma compact_principal [simp]: "compact (principal a)"
-by (rule compactI2, simp add: principal_below_iff_mem_rep rep_contlub)
+by (rule compactI2, simp add: principal_below_iff_mem_rep rep_lub)
text {* Construct a chain whose lub is the same as a given ideal *}
@@ -285,7 +285,7 @@
have 1: "\<forall>i. enum (X i) \<preceq> enum (X (Suc i))"
by (simp add: X_chain)
have 2: "x = (\<Squnion>n. principal (enum (X n)))"
- apply (simp add: eq_iff rep_contlub 1 rep_principal)
+ apply (simp add: eq_iff rep_lub 1 rep_principal)
apply (auto, rename_tac a)
apply (subgoal_tac "\<exists>i. a = enum i", erule exE)
apply (rule_tac x=i in exI, simp add: X_covers)
@@ -345,7 +345,7 @@
have chain: "chain (\<lambda>i. f (Y i))"
by (rule chainI, simp add: f_mono Y)
have rep_x: "rep x = (\<Union>n. {a. a \<preceq> Y n})"
- by (simp add: x rep_contlub Y rep_principal)
+ by (simp add: x rep_lub Y rep_principal)
have "f ` rep x <<| (\<Squnion>n. f (Y n))"
apply (rule is_lubI)
apply (rule ub_imageI, rename_tac a)
@@ -375,7 +375,7 @@
apply (rule is_ub_thelub_ex [OF lub imageI])
apply (erule (1) subsetD [OF rep_mono])
apply (rule is_lub_thelub_ex [OF lub ub_imageI])
- apply (simp add: rep_contlub, clarify)
+ apply (simp add: rep_lub, clarify)
apply (erule rev_below_trans [OF is_ub_thelub])
apply (erule is_ub_thelub_ex [OF lub imageI])
done
@@ -421,7 +421,7 @@
show "ideal (Rep x)"
using Rep [of x] by simp
show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))"
- using type below by (rule typedef_ideal_rep_contlub)
+ using type below by (rule typedef_ideal_rep_lub)
show "Rep (principal a) = {b. b \<preceq> a}"
by (simp add: principal Abs_inverse ideal_principal)
show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y"
--- a/src/HOLCF/Cont.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Cont.thy Sat Nov 27 14:34:54 2010 -0800
@@ -72,7 +72,7 @@
apply (erule contE)
apply (erule bin_chain)
apply (rule_tac f=f in arg_cong)
-apply (erule lub_bin_chain [THEN thelubI])
+apply (erule is_lub_bin_chain [THEN lub_eqI])
done
text {* continuity implies monotonicity *}
@@ -80,7 +80,7 @@
lemma cont2mono: "cont f \<Longrightarrow> monofun f"
apply (rule monofunI)
apply (drule (1) binchain_cont)
-apply (drule_tac i=0 in is_ub_lub)
+apply (drule_tac i=0 in is_lub_rangeD1)
apply simp
done
@@ -92,7 +92,7 @@
lemma cont2contlubE:
"\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
-apply (rule thelubI [symmetric])
+apply (rule lub_eqI [symmetric])
apply (erule (1) contE)
done
@@ -142,9 +142,7 @@
text {* constant functions are continuous *}
lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)"
-apply (rule contI)
-apply (rule lub_const)
-done
+ using is_lub_const by (rule contI)
text {* application of functions is continuous *}
@@ -235,7 +233,7 @@
lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
apply (rule contI)
apply (drule discrete_chain_const, clarify)
-apply (simp add: lub_const)
+apply (simp add: is_lub_const)
done
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Cpodef.thy Sat Nov 27 14:34:54 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/FOCUS/Fstream.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy Sat Nov 27 14:34:54 2010 -0800
@@ -225,7 +225,7 @@
lemma fstream_lub_lemma1:
"\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
apply (case_tac "max_in_chain i Y")
-apply (drule (1) lub_finch1 [THEN thelubI, THEN sym])
+apply (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
apply (force)
apply (unfold max_in_chain_def)
apply auto
@@ -254,7 +254,7 @@
apply (rule chainI)
apply (fast)
apply (erule chain_shift)
-apply (subst lub_const [THEN thelubI])
+apply (subst lub_const)
apply (subst lub_range_shift)
apply (assumption)
apply (simp)
--- a/src/HOLCF/FOCUS/Fstreams.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy Sat Nov 27 14:34:54 2010 -0800
@@ -246,7 +246,7 @@
apply (drule fstreams_lub_lemma1, auto)
apply (rule_tac x="j" in exI, auto)
apply (case_tac "max_in_chain j Y")
-apply (frule lub_finch1 [THEN thelubI], auto)
+apply (frule lub_finch1 [THEN lub_eqI], auto)
apply (rule_tac x="j" in exI)
apply (erule subst) back back
apply (simp add: below_prod_def sconc_mono)
@@ -266,7 +266,7 @@
lemma lub_Pair_not_UU_lemma:
"[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |]
==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
-apply (frule thelub_cprod, clarsimp)
+apply (frule lub_prod, clarsimp)
apply (drule chain_UU_I_inverse2, clarsimp)
apply (case_tac "Y i", clarsimp)
apply (case_tac "max_in_chain i Y")
@@ -298,7 +298,7 @@
apply (drule fstreams_lub_lemma2, auto)
apply (rule_tac x="j" in exI, auto)
apply (case_tac "max_in_chain j Y")
-apply (frule lub_finch1 [THEN thelubI], auto)
+apply (frule lub_finch1 [THEN lub_eqI], auto)
apply (rule_tac x="j" in exI)
apply (erule subst) back back
apply (simp add: sconc_mono)
@@ -312,7 +312,7 @@
apply (rule sconc_mono)
apply (subgoal_tac "tt ~= tta" "tta << ms")
apply (blast intro: fstreams_chain_lemma)
-apply (frule lub_cprod [THEN thelubI], auto)
+apply (frule lub_prod, auto)
apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
apply (drule fstreams_mono, simp)
apply (rule is_ub_thelub chainI)
--- a/src/HOLCF/FOCUS/Stream_adm.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Sat Nov 27 14:34:54 2010 -0800
@@ -37,7 +37,7 @@
prefer 2 apply fast
apply (unfold finite_chain_def)
apply safe
-apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
+apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst])
apply assumption
apply (erule spec)
done
--- a/src/HOLCF/Fix.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Fix.thy Sat Nov 27 14:34:54 2010 -0800
@@ -183,7 +183,7 @@
hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
by - (rule admD [OF adm'], simp, assumption)
hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
- by (simp add: thelub_Pair)
+ by (simp add: lub_Pair)
hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
by simp
thus "P (fix\<cdot>F) (fix\<cdot>G)"
--- a/src/HOLCF/Fixrec.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Fixrec.thy Sat Nov 27 14:34:54 2010 -0800
@@ -105,9 +105,9 @@
default_sort pcpo
definition
- match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
+ match_bottom :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
where
- "match_UU = (\<Lambda> x k. strict\<cdot>x\<cdot>fail)"
+ "match_bottom = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
definition
match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
@@ -149,10 +149,10 @@
where
"match_FF = (\<Lambda> x k. If x then fail else k)"
-lemma match_UU_simps [simp]:
- "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
- "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
-by (simp_all add: match_UU_def)
+lemma match_bottom_simps [simp]:
+ "match_bottom\<cdot>\<bottom>\<cdot>k = \<bottom>"
+ "x \<noteq> \<bottom> \<Longrightarrow> match_bottom\<cdot>x\<cdot>k = fail"
+by (simp_all add: match_bottom_def)
lemma match_Pair_simps [simp]:
"match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
@@ -244,7 +244,7 @@
(@{const_name ONE}, @{const_name match_ONE}),
(@{const_name TT}, @{const_name match_TT}),
(@{const_name FF}, @{const_name match_FF}),
- (@{const_name UU}, @{const_name match_UU}) ]
+ (@{const_name UU}, @{const_name match_bottom}) ]
*}
hide_const (open) succeed fail run
--- a/src/HOLCF/Fun_Cpo.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Fun_Cpo.thy Sat Nov 27 14:34:54 2010 -0800
@@ -80,7 +80,7 @@
lemma thelub_fun:
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
\<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
-by (rule lub_fun [THEN thelubI])
+by (rule lub_fun [THEN lub_eqI])
instance "fun" :: (type, cpo) cpo
by intro_classes (rule exI, erule lub_fun)
--- a/src/HOLCF/HOLCF.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/HOLCF.thy Sat Nov 27 14:34:54 2010 -0800
@@ -30,5 +30,10 @@
lemmas cont2cont_Rep_CFun = cont2cont_APP
lemmas cont_Rep_CFun_app = cont_APP_app
lemmas cont_Rep_CFun_app_app = cont_APP_app_app
+lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
+lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
+(*
+lemmas thelubI = lub_eqI
+*)
end
--- a/src/HOLCF/IsaMakefile Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/IsaMakefile Sat Nov 27 14:34:54 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/Library/List_Cpo.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Library/List_Cpo.thy Sat Nov 27 14:34:54 2010 -0800
@@ -141,7 +141,7 @@
fix S :: "nat \<Rightarrow> 'a list"
assume "chain S" thus "\<exists>x. range S <<| x"
proof (induct rule: list_chain_induct)
- case Nil thus ?case by (auto intro: lub_const)
+ case Nil thus ?case by (auto intro: is_lub_const)
next
case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI)
qed
@@ -163,7 +163,7 @@
fixes A :: "nat \<Rightarrow> 'a::cpo"
assumes A: "chain A" and B: "chain B"
shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
-by (intro thelubI is_lub_Cons cpo_lubI A B)
+by (intro lub_eqI is_lub_Cons cpo_lubI A B)
lemma cont2cont_list_case:
assumes f: "cont (\<lambda>x. f x)"
@@ -175,7 +175,7 @@
apply (rule cont_apply [OF f])
apply (rule contI)
apply (erule list_chain_cases)
-apply (simp add: lub_const)
+apply (simp add: is_lub_const)
apply (simp add: lub_Cons)
apply (simp add: cont2contlubE [OF h2])
apply (simp add: cont2contlubE [OF h3])
--- a/src/HOLCF/Library/Sum_Cpo.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Library/Sum_Cpo.thy Sat Nov 27 14:34:54 2010 -0800
@@ -98,10 +98,10 @@
lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
apply (rule is_lubI)
apply (rule ub_rangeI)
- apply (simp add: is_ub_lub)
+ apply (simp add: is_lub_rangeD1)
apply (frule ub_rangeD [where i=arbitrary])
apply (erule Inl_belowE, simp)
- apply (erule is_lub_lub)
+ apply (erule is_lubD2)
apply (rule ub_rangeI)
apply (drule ub_rangeD, simp)
done
@@ -109,10 +109,10 @@
lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
apply (rule is_lubI)
apply (rule ub_rangeI)
- apply (simp add: is_ub_lub)
+ apply (simp add: is_lub_rangeD1)
apply (frule ub_rangeD [where i=arbitrary])
apply (erule Inr_belowE, simp)
- apply (erule is_lub_lub)
+ apply (erule is_lubD2)
apply (rule ub_rangeI)
apply (drule ub_rangeD, simp)
done
--- a/src/HOLCF/One.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/One.thy Sat Nov 27 14:34:54 2010 -0800
@@ -54,7 +54,7 @@
definition
one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
- "one_case = (\<Lambda> a x. strict\<cdot>x\<cdot>a)"
+ "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)"
translations
"case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"
--- a/src/HOLCF/Pcpo.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Pcpo.thy Sat Nov 27 14:34:54 2010 -0800
@@ -19,19 +19,19 @@
text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
- by (fast dest: cpo elim: lubI)
+ by (fast dest: cpo elim: is_lub_lub)
lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
- by (blast dest: cpo intro: lubI)
+ by (blast dest: cpo intro: is_lub_lub)
text {* Properties of the lub *}
lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
- by (blast dest: cpo intro: lubI [THEN is_ub_lub])
+ by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
lemma is_lub_thelub:
"\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
- by (blast dest: cpo intro: lubI [THEN is_lub_lub])
+ by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2])
lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
@@ -70,7 +70,7 @@
lemma maxinch_is_thelub:
"chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
apply (rule iffI)
-apply (fast intro!: thelubI lub_finch1)
+apply (fast intro!: lub_eqI lub_finch1)
apply (unfold max_in_chain_def)
apply (safe intro!: below_antisym)
apply (fast elim!: chain_mono)
--- a/src/HOLCF/Pcpodef.thy Sat Nov 27 22:02:16 2010 +0100
+++ /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_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_thelub = typedef_lub [THEN thelubI, 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_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_thelub [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
--- a/src/HOLCF/Porder.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Porder.thy Sat Nov 27 14:34:54 2010 -0800
@@ -126,7 +126,7 @@
lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x"
unfolding is_lub_def by fast
-lemma is_lub_lub: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
+lemma is_lubD2: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
unfolding is_lub_def by fast
lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
@@ -137,40 +137,34 @@
text {* lubs are unique *}
-lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
-apply (unfold is_lub_def is_ub_def)
-apply (blast intro: below_antisym)
-done
+lemma is_lub_unique: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
+ unfolding is_lub_def is_ub_def by (blast intro: below_antisym)
text {* technical lemmas about @{term lub} and @{term is_lub} *}
-lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M"
-apply (unfold lub_def)
-apply (rule theI)
-apply assumption
-apply (erule (1) unique_lub)
-done
+lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M"
+ unfolding lub_def by (rule theI [OF _ is_lub_unique])
-lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
- by (rule unique_lub [OF lubI])
+lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l"
+ by (rule is_lub_unique [OF is_lub_lub])
lemma is_lub_singleton: "{x} <<| x"
by (simp add: is_lub_def)
lemma lub_singleton [simp]: "lub {x} = x"
- by (rule thelubI [OF is_lub_singleton])
+ by (rule is_lub_singleton [THEN lub_eqI])
lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y"
by (simp add: is_lub_def)
lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y"
- by (rule is_lub_bin [THEN thelubI])
+ by (rule is_lub_bin [THEN lub_eqI])
lemma is_lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> S <<| x"
by (erule is_lubI, erule (1) is_ubD)
lemma lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x"
- by (rule is_lub_maximal [THEN thelubI])
+ by (rule is_lub_maximal [THEN lub_eqI])
subsection {* Countable chains *}
@@ -197,7 +191,7 @@
text {* technical lemmas about (least) upper bounds of chains *}
-lemma is_ub_lub: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
+lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
by (rule is_lubD1 [THEN ub_rangeD])
lemma is_ub_range_shift:
@@ -221,11 +215,11 @@
lemma chain_const [simp]: "chain (\<lambda>i. c)"
by (simp add: chainI)
-lemma lub_const: "range (\<lambda>x. c) <<| c"
+lemma is_lub_const: "range (\<lambda>x. c) <<| c"
by (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
-lemma thelub_const [simp]: "(\<Squnion>i. c) = c"
- by (rule lub_const [THEN thelubI])
+lemma lub_const [simp]: "(\<Squnion>i. c) = c"
+ by (rule is_lub_const [THEN lub_eqI])
subsection {* Finite chains *}
@@ -324,7 +318,7 @@
"x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
unfolding max_in_chain_def by simp
-lemma lub_bin_chain:
+lemma is_lub_bin_chain:
"x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"
apply (frule bin_chain)
apply (drule bin_chainmax)
@@ -335,7 +329,7 @@
text {* the maximal element in a chain is its lub *}
lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
- by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
+ by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI)
end
--- a/src/HOLCF/Product_Cpo.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Product_Cpo.thy Sat Nov 27 14:34:54 2010 -0800
@@ -111,46 +111,30 @@
lemma is_lub_Pair:
"\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
-apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: is_ub_lub)
-apply (frule ub2ub_monofun [OF monofun_fst])
-apply (drule ub2ub_monofun [OF monofun_snd])
-apply (simp add: below_prod_def is_lub_lub)
-done
+unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
-lemma thelub_Pair:
+lemma lub_Pair:
"\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
\<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
-by (fast intro: thelubI is_lub_Pair elim: thelubE)
+by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
-lemma lub_cprod:
+lemma is_lub_prod:
fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
assumes S: "chain S"
shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-proof -
- from `chain S` have "chain (\<lambda>i. fst (S i))"
- by (rule ch2ch_fst)
- hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
- by (rule cpo_lubI)
- from `chain S` have "chain (\<lambda>i. snd (S i))"
- by (rule ch2ch_snd)
- hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
- by (rule cpo_lubI)
- show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
- using is_lub_Pair [OF 1 2] by simp
-qed
+using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)
-lemma thelub_cprod:
+lemma lub_prod:
"chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
\<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-by (rule lub_cprod [THEN thelubI])
+by (rule is_lub_prod [THEN lub_eqI])
instance prod :: (cpo, cpo) cpo
proof
fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
assume "chain S"
hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
- by (rule lub_cprod)
+ by (rule is_lub_prod)
thus "\<exists>x. range S <<| x" ..
qed
@@ -164,23 +148,23 @@
subsection {* Product type is pointed *}
-lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
+lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
by (simp add: below_prod_def)
instance prod :: (pcpo, pcpo) pcpo
-by intro_classes (fast intro: minimal_cprod)
+by intro_classes (fast intro: minimal_prod)
-lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_cprod [THEN UU_I, symmetric])
+lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
+by (rule minimal_prod [THEN UU_I, symmetric])
lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
-unfolding inst_cprod_pcpo by simp
+unfolding inst_prod_pcpo by simp
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo by (rule fst_conv)
+unfolding inst_prod_pcpo by (rule fst_conv)
lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo by (rule snd_conv)
+unfolding inst_prod_pcpo by (rule snd_conv)
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
by simp
@@ -194,25 +178,25 @@
apply (rule contI)
apply (rule is_lub_Pair)
apply (erule cpo_lubI)
-apply (rule lub_const)
+apply (rule is_lub_const)
done
lemma cont_pair2: "cont (\<lambda>y. (x, y))"
apply (rule contI)
apply (rule is_lub_Pair)
-apply (rule lub_const)
+apply (rule is_lub_const)
apply (erule cpo_lubI)
done
lemma cont_fst: "cont fst"
apply (rule contI)
-apply (simp add: thelub_cprod)
+apply (simp add: lub_prod)
apply (erule cpo_lubI [OF ch2ch_fst])
done
lemma cont_snd: "cont snd"
apply (rule contI)
-apply (simp add: thelub_cprod)
+apply (simp add: lub_prod)
apply (erule cpo_lubI [OF ch2ch_snd])
done
--- a/src/HOLCF/Sprod.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Sprod.thy Sat Nov 27 14:34:54 2010 -0800
@@ -37,11 +37,11 @@
definition
spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where
- "spair = (\<Lambda> a b. Abs_sprod (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b))"
+ "spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))"
definition
ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
- "ssplit = (\<Lambda> f p. strict\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
+ "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
syntax
"_stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
@@ -54,10 +54,10 @@
subsection {* Case analysis *}
-lemma spair_sprod: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> sprod"
-by (simp add: sprod_def strict_conv_if)
+lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod"
+by (simp add: sprod_def seq_conv_if)
-lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
+lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b)"
by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod)
lemmas Rep_sprod_simps =
@@ -82,16 +82,16 @@
by (simp add: Rep_sprod_simps)
lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
-by (simp add: Rep_sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps seq_conv_if)
lemma spair_below_iff:
"((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
-by (simp add: Rep_sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps seq_conv_if)
lemma spair_eq_iff:
"((:a, b:) = (:c, d:)) =
(a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))"
-by (simp add: Rep_sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps seq_conv_if)
lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
by simp
@@ -177,7 +177,7 @@
by (rule compactI, simp add: ssnd_below_iff)
lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
-by (rule compact_sprod, simp add: Rep_sprod_spair strict_conv_if)
+by (rule compact_sprod, simp add: Rep_sprod_spair seq_conv_if)
lemma compact_spair_iff:
"compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))"
--- a/src/HOLCF/Ssum.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Ssum.thy Sat Nov 27 14:34:54 2010 -0800
@@ -32,22 +32,22 @@
definition
sinl :: "'a \<rightarrow> ('a ++ 'b)" where
- "sinl = (\<Lambda> a. Abs_ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>))"
+ "sinl = (\<Lambda> a. Abs_ssum (seq\<cdot>a\<cdot>TT, a, \<bottom>))"
definition
sinr :: "'b \<rightarrow> ('a ++ 'b)" where
- "sinr = (\<Lambda> b. Abs_ssum (strict\<cdot>b\<cdot>FF, \<bottom>, b))"
+ "sinr = (\<Lambda> b. Abs_ssum (seq\<cdot>b\<cdot>FF, \<bottom>, b))"
-lemma sinl_ssum: "(strict\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
-by (simp add: ssum_def strict_conv_if)
+lemma sinl_ssum: "(seq\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
+by (simp add: ssum_def seq_conv_if)
-lemma sinr_ssum: "(strict\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
-by (simp add: ssum_def strict_conv_if)
+lemma sinr_ssum: "(seq\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
+by (simp add: ssum_def seq_conv_if)
-lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
+lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (seq\<cdot>a\<cdot>TT, a, \<bottom>)"
by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)
-lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
+lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (seq\<cdot>b\<cdot>FF, \<bottom>, b)"
by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)
lemmas Rep_ssum_simps =
@@ -60,16 +60,16 @@
text {* Ordering *}
lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
text {* Equality *}
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 14:34:54 2010 -0800
@@ -711,7 +711,7 @@
val goal = mk_trp (mk_eq (lhs, rhs));
val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy;
val start_rules =
- @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
+ @{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
@ @{thms pair_collapse split_def}
@ map_apply_thms @ map_ID_thms;
val rules0 =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/cpodef.ML Sat Nov 27 14:34:54 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 22:02:16 2010 +0100
+++ b/src/HOLCF/Tools/domaindef.ML Sat Nov 27 14:34:54 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 22:02:16 2010 +0100
+++ /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,
- lub: thm, thelub: 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,
- lub: thm, thelub: 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 lub = make @{thm typedef_lub};
- val thelub = make @{thm typedef_thelub};
- 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 "lub_" name, lub ), []),
- ((Binding.prefix_name "thelub_" name, thelub ), []),
- ((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, lub = lub, thelub = thelub, 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;
--- a/src/HOLCF/Up.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Up.thy Sat Nov 27 14:34:54 2010 -0800
@@ -111,7 +111,7 @@
proof (rule up_chain_lemma)
assume "\<forall>i. S i = Ibottom"
hence "range (\<lambda>i. S i) <<| Ibottom"
- by (simp add: lub_const)
+ by (simp add: is_lub_const)
thus ?thesis ..
next
fix A :: "nat \<Rightarrow> 'a"
@@ -160,7 +160,7 @@
assume A: "\<forall>i. Iup (A i) = Y (i + k)"
assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
- by (simp add: thelubI contlub_cfun_arg)
+ by (simp add: lub_eqI contlub_cfun_arg)
also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
by (simp add: A)
also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
@@ -223,7 +223,7 @@
assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
| A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
apply (rule up_chain_lemma [OF Y])
-apply (simp_all add: inst_up_pcpo up_def cont_Iup thelubI)
+apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
done
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
--- a/src/HOLCF/ex/Domain_Proofs.thy Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy Sat Nov 27 14:34:54 2010 -0800
@@ -467,7 +467,7 @@
lemma lub_take_lemma:
"(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
= (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
-apply (simp only: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms)
+apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
apply (simp only: map_apply_thms pair_collapse)
apply (simp only: fix_def2)
apply (rule lub_eq)