--- a/src/HOL/Fundamental_Theorem_Algebra.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOL/Fundamental_Theorem_Algebra.thy Sun Jan 18 13:58:17 2009 +0100
@@ -135,15 +135,15 @@
done
definition
- "plength p = (if p = 0 then 0 else Suc (degree p))"
+ "psize p = (if p = 0 then 0 else Suc (degree p))"
-lemma plength_eq_0_iff [simp]: "plength p = 0 \<longleftrightarrow> p = 0"
- unfolding plength_def by simp
+lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
+ unfolding psize_def by simp
-lemma poly_offset: "\<exists> q. plength q = plength p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
+lemma poly_offset: "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
proof (intro exI conjI)
- show "plength (offset_poly p a) = plength p"
- unfolding plength_def
+ show "psize (offset_poly p a) = psize p"
+ unfolding psize_def
by (simp add: offset_poly_eq_0_iff degree_offset_poly)
show "\<forall>x. poly (offset_poly p a) x = poly p (a + x)"
by (simp add: poly_offset_poly)
@@ -719,8 +719,8 @@
text{* Constant function (non-syntactic characterization). *}
definition "constant f = (\<forall>x y. f x = f y)"
-lemma nonconstant_length: "\<not> (constant (poly p)) \<Longrightarrow> plength p \<ge> 2"
- unfolding constant_def plength_def
+lemma nonconstant_length: "\<not> (constant (poly p)) \<Longrightarrow> psize p \<ge> 2"
+ unfolding constant_def psize_def
apply (induct p, auto)
done
@@ -733,9 +733,9 @@
lemma poly_decompose_lemma:
assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
- shows "\<exists>k a q. a\<noteq>0 \<and> Suc (plength q + k) = plength p \<and>
+ shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and>
(\<forall>z. poly p z = z^k * poly (pCons a q) z)"
-unfolding plength_def
+unfolding psize_def
using nz
proof(induct p)
case 0 thus ?case by simp
@@ -761,7 +761,7 @@
lemma poly_decompose:
assumes nc: "~constant(poly p)"
shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
- plength q + k + 1 = plength p \<and>
+ psize q + k + 1 = psize p \<and>
(\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
using nc
proof(induct p)
@@ -781,7 +781,7 @@
apply simp
apply (rule_tac x="q" in exI)
apply (auto simp add: power_Suc)
- apply (auto simp add: plength_def split: if_splits)
+ apply (auto simp add: psize_def split: if_splits)
done
qed
@@ -791,10 +791,10 @@
assumes nc: "~constant(poly p)"
shows "\<exists>z::complex. poly p z = 0"
using nc
-proof(induct n\<equiv> "plength p" arbitrary: p rule: nat_less_induct)
+proof(induct n\<equiv> "psize p" arbitrary: p rule: nat_less_induct)
fix n fix p :: "complex poly"
let ?p = "poly p"
- assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = plength p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = plength p"
+ assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = psize p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = psize p"
let ?ths = "\<exists>z. ?p z = 0"
from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
@@ -804,7 +804,7 @@
moreover
{assume pc0: "?p c \<noteq> 0"
from poly_offset[of p c] obtain q where
- q: "plength q = plength p" "\<forall>x. poly q x = ?p (c+x)" by blast
+ q: "psize q = psize p" "\<forall>x. poly q x = ?p (c+x)" by blast
{assume h: "constant (poly q)"
from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
{fix x y
@@ -823,8 +823,8 @@
have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
by simp
let ?r = "smult (inverse ?a0) q"
- have lgqr: "plength q = plength ?r"
- using a00 unfolding plength_def degree_def
+ have lgqr: "psize q = psize ?r"
+ using a00 unfolding psize_def degree_def
by (simp add: expand_poly_eq)
{assume h: "\<And>x y. poly ?r x = poly ?r y"
{fix x y
@@ -844,7 +844,7 @@
finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .}
note mrmq_eq = this
from poly_decompose[OF rnc] obtain k a s where
- kas: "a\<noteq>0" "k\<noteq>0" "plength s + k + 1 = plength ?r"
+ kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r"
"\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
{assume "k + 1 = n"
with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto
@@ -861,8 +861,8 @@
unfolding constant_def poly_pCons poly_monom
using kas(1) apply simp
by (rule exI[where x=0], rule exI[where x=1], simp)
- from kas(1) kas(2) have th02: "k+1 = plength (pCons 1 (monom a (k - 1)))"
- by (simp add: plength_def degree_monom_eq)
+ from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
+ by (simp add: psize_def degree_monom_eq)
from H[rule_format, OF k1n th01 th02]
obtain w where w: "1 + w^k * a = 0"
unfolding poly_pCons poly_monom
@@ -1353,11 +1353,11 @@
lemma basic_cqe_conv3:
fixes p q :: "complex poly"
assumes l: "p \<noteq> 0"
- shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (plength p)))"
+ shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
proof-
- from l have dp:"degree (pCons a p) = plength p" by (simp add: plength_def)
+ from l have dp:"degree (pCons a p) = psize p" by (simp add: psize_def)
from nullstellensatz_univariate[of "pCons a p" q] l
- show "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (plength p)))"
+ show "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
unfolding dp
by - (atomize (full), auto)
qed
--- a/src/HOL/Polynomial.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOL/Polynomial.thy Sun Jan 18 13:58:17 2009 +0100
@@ -293,6 +293,14 @@
end
+instance poly ::
+ ("{cancel_ab_semigroup_add,comm_monoid_add}") cancel_ab_semigroup_add
+proof
+ fix p q r :: "'a poly"
+ assume "p + q = p + r" thus "q = r"
+ by (simp add: expand_poly_eq)
+qed
+
instantiation poly :: (ab_group_add) ab_group_add
begin
@@ -345,19 +353,22 @@
"pCons a p - pCons b q = pCons (a - b) (p - q)"
by (rule poly_ext, simp add: coeff_pCons split: nat.split)
-lemma degree_add_le: "degree (p + q) \<le> max (degree p) (degree q)"
+lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)"
by (rule degree_le, auto simp add: coeff_eq_0)
+lemma degree_add_le:
+ "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p + q) \<le> n"
+ by (auto intro: order_trans degree_add_le_max)
+
lemma degree_add_less:
"\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n"
- by (auto intro: le_less_trans degree_add_le)
+ by (auto intro: le_less_trans degree_add_le_max)
lemma degree_add_eq_right:
"degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
apply (cases "q = 0", simp)
apply (rule order_antisym)
- apply (rule ord_le_eq_trans [OF degree_add_le])
- apply simp
+ apply (simp add: degree_add_le)
apply (rule le_degree)
apply (simp add: coeff_eq_0)
done
@@ -370,13 +381,17 @@
lemma degree_minus [simp]: "degree (- p) = degree p"
unfolding degree_def by simp
-lemma degree_diff_le: "degree (p - q) \<le> max (degree p) (degree q)"
+lemma degree_diff_le_max: "degree (p - q) \<le> max (degree p) (degree q)"
using degree_add_le [where p=p and q="-q"]
by (simp add: diff_minus)
+lemma degree_diff_le:
+ "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p - q) \<le> n"
+ by (simp add: diff_minus degree_add_le)
+
lemma degree_diff_less:
"\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
- by (auto intro: le_less_trans degree_diff_le)
+ by (simp add: diff_minus degree_add_less)
lemma add_monom: "monom a n + monom b n = monom (a + b) n"
by (rule poly_ext) simp
@@ -534,6 +549,8 @@
end
+instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
+
lemma coeff_mult:
"coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
proof (induct p arbitrary: n)
@@ -575,6 +592,8 @@
end
+instance poly :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
+
lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
unfolding one_poly_def
by (simp add: coeff_pCons split: nat.split)
@@ -647,19 +666,19 @@
subsection {* Long division of polynomials *}
definition
- divmod_poly_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
+ pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
where
[code del]:
- "divmod_poly_rel x y q r \<longleftrightarrow>
+ "pdivmod_rel x y q r \<longleftrightarrow>
x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
-lemma divmod_poly_rel_0:
- "divmod_poly_rel 0 y 0 0"
- unfolding divmod_poly_rel_def by simp
+lemma pdivmod_rel_0:
+ "pdivmod_rel 0 y 0 0"
+ unfolding pdivmod_rel_def by simp
-lemma divmod_poly_rel_by_0:
- "divmod_poly_rel x 0 0 x"
- unfolding divmod_poly_rel_def by simp
+lemma pdivmod_rel_by_0:
+ "pdivmod_rel x 0 0 x"
+ unfolding pdivmod_rel_def by simp
lemma eq_zero_or_degree_less:
assumes "degree p \<le> n" and "coeff p n = 0"
@@ -685,62 +704,59 @@
then show ?thesis ..
qed
-lemma divmod_poly_rel_pCons:
- assumes rel: "divmod_poly_rel x y q r"
+lemma pdivmod_rel_pCons:
+ assumes rel: "pdivmod_rel x y q r"
assumes y: "y \<noteq> 0"
assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
- shows "divmod_poly_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
- (is "divmod_poly_rel ?x y ?q ?r")
+ shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
+ (is "pdivmod_rel ?x y ?q ?r")
proof -
have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
- using assms unfolding divmod_poly_rel_def by simp_all
+ using assms unfolding pdivmod_rel_def by simp_all
have 1: "?x = ?q * y + ?r"
using b x by simp
have 2: "?r = 0 \<or> degree ?r < degree y"
proof (rule eq_zero_or_degree_less)
- have "degree ?r \<le> max (degree (pCons a r)) (degree (smult b y))"
- by (rule degree_diff_le)
- also have "\<dots> \<le> degree y"
- proof (rule min_max.le_supI)
+ show "degree ?r \<le> degree y"
+ proof (rule degree_diff_le)
show "degree (pCons a r) \<le> degree y"
using r by auto
show "degree (smult b y) \<le> degree y"
by (rule degree_smult_le)
qed
- finally show "degree ?r \<le> degree y" .
next
show "coeff ?r (degree y) = 0"
using `y \<noteq> 0` unfolding b by simp
qed
from 1 2 show ?thesis
- unfolding divmod_poly_rel_def
+ unfolding pdivmod_rel_def
using `y \<noteq> 0` by simp
qed
-lemma divmod_poly_rel_exists: "\<exists>q r. divmod_poly_rel x y q r"
+lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r"
apply (cases "y = 0")
-apply (fast intro!: divmod_poly_rel_by_0)
+apply (fast intro!: pdivmod_rel_by_0)
apply (induct x)
-apply (fast intro!: divmod_poly_rel_0)
-apply (fast intro!: divmod_poly_rel_pCons)
+apply (fast intro!: pdivmod_rel_0)
+apply (fast intro!: pdivmod_rel_pCons)
done
-lemma divmod_poly_rel_unique:
- assumes 1: "divmod_poly_rel x y q1 r1"
- assumes 2: "divmod_poly_rel x y q2 r2"
+lemma pdivmod_rel_unique:
+ assumes 1: "pdivmod_rel x y q1 r1"
+ assumes 2: "pdivmod_rel x y q2 r2"
shows "q1 = q2 \<and> r1 = r2"
proof (cases "y = 0")
assume "y = 0" with assms show ?thesis
- by (simp add: divmod_poly_rel_def)
+ by (simp add: pdivmod_rel_def)
next
assume [simp]: "y \<noteq> 0"
from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
- unfolding divmod_poly_rel_def by simp_all
+ unfolding pdivmod_rel_def by simp_all
from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
- unfolding divmod_poly_rel_def by simp_all
+ unfolding pdivmod_rel_def by simp_all
from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
by (simp add: ring_simps)
from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
@@ -761,36 +777,36 @@
qed
qed
-lemmas divmod_poly_rel_unique_div =
- divmod_poly_rel_unique [THEN conjunct1, standard]
+lemmas pdivmod_rel_unique_div =
+ pdivmod_rel_unique [THEN conjunct1, standard]
-lemmas divmod_poly_rel_unique_mod =
- divmod_poly_rel_unique [THEN conjunct2, standard]
+lemmas pdivmod_rel_unique_mod =
+ pdivmod_rel_unique [THEN conjunct2, standard]
instantiation poly :: (field) ring_div
begin
definition div_poly where
- [code del]: "x div y = (THE q. \<exists>r. divmod_poly_rel x y q r)"
+ [code del]: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
definition mod_poly where
- [code del]: "x mod y = (THE r. \<exists>q. divmod_poly_rel x y q r)"
+ [code del]: "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
lemma div_poly_eq:
- "divmod_poly_rel x y q r \<Longrightarrow> x div y = q"
+ "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
unfolding div_poly_def
-by (fast elim: divmod_poly_rel_unique_div)
+by (fast elim: pdivmod_rel_unique_div)
lemma mod_poly_eq:
- "divmod_poly_rel x y q r \<Longrightarrow> x mod y = r"
+ "pdivmod_rel x y q r \<Longrightarrow> x mod y = r"
unfolding mod_poly_def
-by (fast elim: divmod_poly_rel_unique_mod)
+by (fast elim: pdivmod_rel_unique_mod)
-lemma divmod_poly_rel:
- "divmod_poly_rel x y (x div y) (x mod y)"
+lemma pdivmod_rel:
+ "pdivmod_rel x y (x div y) (x mod y)"
proof -
- from divmod_poly_rel_exists
- obtain q r where "divmod_poly_rel x y q r" by fast
+ from pdivmod_rel_exists
+ obtain q r where "pdivmod_rel x y q r" by fast
thus ?thesis
by (simp add: div_poly_eq mod_poly_eq)
qed
@@ -798,26 +814,26 @@
instance proof
fix x y :: "'a poly"
show "x div y * y + x mod y = x"
- using divmod_poly_rel [of x y]
- by (simp add: divmod_poly_rel_def)
+ using pdivmod_rel [of x y]
+ by (simp add: pdivmod_rel_def)
next
fix x :: "'a poly"
- have "divmod_poly_rel x 0 0 x"
- by (rule divmod_poly_rel_by_0)
+ have "pdivmod_rel x 0 0 x"
+ by (rule pdivmod_rel_by_0)
thus "x div 0 = 0"
by (rule div_poly_eq)
next
fix y :: "'a poly"
- have "divmod_poly_rel 0 y 0 0"
- by (rule divmod_poly_rel_0)
+ have "pdivmod_rel 0 y 0 0"
+ by (rule pdivmod_rel_0)
thus "0 div y = 0"
by (rule div_poly_eq)
next
fix x y z :: "'a poly"
assume "y \<noteq> 0"
- hence "divmod_poly_rel (x + z * y) y (z + x div y) (x mod y)"
- using divmod_poly_rel [of x y]
- by (simp add: divmod_poly_rel_def left_distrib)
+ hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
+ using pdivmod_rel [of x y]
+ by (simp add: pdivmod_rel_def left_distrib)
thus "(x + z * y) div y = z + x div y"
by (rule div_poly_eq)
qed
@@ -826,22 +842,22 @@
lemma degree_mod_less:
"y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
- using divmod_poly_rel [of x y]
- unfolding divmod_poly_rel_def by simp
+ using pdivmod_rel [of x y]
+ unfolding pdivmod_rel_def by simp
lemma div_poly_less: "degree x < degree y \<Longrightarrow> x div y = 0"
proof -
assume "degree x < degree y"
- hence "divmod_poly_rel x y 0 x"
- by (simp add: divmod_poly_rel_def)
+ hence "pdivmod_rel x y 0 x"
+ by (simp add: pdivmod_rel_def)
thus "x div y = 0" by (rule div_poly_eq)
qed
lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
proof -
assume "degree x < degree y"
- hence "divmod_poly_rel x y 0 x"
- by (simp add: divmod_poly_rel_def)
+ hence "pdivmod_rel x y 0 x"
+ by (simp add: pdivmod_rel_def)
thus "x mod y = x" by (rule mod_poly_eq)
qed
@@ -852,7 +868,7 @@
shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
unfolding b
apply (rule mod_poly_eq)
-apply (rule divmod_poly_rel_pCons [OF divmod_poly_rel y refl])
+apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
done
@@ -1087,30 +1103,30 @@
text {* code generator setup for div and mod *}
definition
- divmod_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
+ pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
where
- [code del]: "divmod_poly x y = (x div y, x mod y)"
+ [code del]: "pdivmod x y = (x div y, x mod y)"
-lemma div_poly_code [code]: "x div y = fst (divmod_poly x y)"
- unfolding divmod_poly_def by simp
+lemma div_poly_code [code]: "x div y = fst (pdivmod x y)"
+ unfolding pdivmod_def by simp
-lemma mod_poly_code [code]: "x mod y = snd (divmod_poly x y)"
- unfolding divmod_poly_def by simp
+lemma mod_poly_code [code]: "x mod y = snd (pdivmod x y)"
+ unfolding pdivmod_def by simp
-lemma divmod_poly_0 [code]: "divmod_poly 0 y = (0, 0)"
- unfolding divmod_poly_def by simp
+lemma pdivmod_0 [code]: "pdivmod 0 y = (0, 0)"
+ unfolding pdivmod_def by simp
-lemma divmod_poly_pCons [code]:
- "divmod_poly (pCons a x) y =
+lemma pdivmod_pCons [code]:
+ "pdivmod (pCons a x) y =
(if y = 0 then (0, pCons a x) else
- (let (q, r) = divmod_poly x y;
+ (let (q, r) = pdivmod x y;
b = coeff (pCons a r) (degree y) / coeff y (degree y)
in (pCons b q, pCons a r - smult b y)))"
-apply (simp add: divmod_poly_def Let_def, safe)
+apply (simp add: pdivmod_def Let_def, safe)
apply (rule div_poly_eq)
-apply (erule divmod_poly_rel_pCons [OF divmod_poly_rel _ refl])
+apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
apply (rule mod_poly_eq)
-apply (erule divmod_poly_rel_pCons [OF divmod_poly_rel _ refl])
+apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
done
end
--- a/src/HOLCF/Cfun.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOLCF/Cfun.thy Sun Jan 18 13:58:17 2009 +0100
@@ -7,8 +7,7 @@
header {* The type of continuous functions *}
theory Cfun
-imports Pcpodef Ffun
-uses ("Tools/cont_proc.ML")
+imports Pcpodef Ffun Product_Cpo
begin
defaultsort cpo
@@ -301,7 +300,7 @@
text {* cont2cont lemma for @{term Rep_CFun} *}
-lemma cont2cont_Rep_CFun:
+lemma cont2cont_Rep_CFun [cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes t: "cont (\<lambda>x. t x)"
shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
@@ -321,6 +320,11 @@
text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
+text {*
+ Not suitable as a cont2cont rule, because on nested lambdas
+ it causes exponential blow-up in the number of subgoals.
+*}
+
lemma cont2cont_LAM:
assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
@@ -331,17 +335,40 @@
from f2 show "cont f" by (rule cont2cont_lambda)
qed
-text {* continuity simplification procedure *}
+text {*
+ This version does work as a cont2cont rule, since it
+ has only a single subgoal.
+*}
+
+lemma cont2cont_LAM' [cont2cont]:
+ fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
+ assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
+ shows "cont (\<lambda>x. \<Lambda> y. f x y)"
+proof (rule cont2cont_LAM)
+ fix x :: 'a
+ have "cont (\<lambda>y. (x, y))"
+ by (rule cont_pair2)
+ with f have "cont (\<lambda>y. f (fst (x, y)) (snd (x, y)))"
+ by (rule cont2cont_app3)
+ thus "cont (\<lambda>y. f x y)"
+ by (simp only: fst_conv snd_conv)
+next
+ fix y :: 'b
+ have "cont (\<lambda>x. (x, y))"
+ by (rule cont_pair1)
+ with f have "cont (\<lambda>x. f (fst (x, y)) (snd (x, y)))"
+ by (rule cont2cont_app3)
+ thus "cont (\<lambda>x. f x y)"
+ by (simp only: fst_conv snd_conv)
+qed
+
+lemma cont2cont_LAM_discrete [cont2cont]:
+ "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
+by (simp add: cont2cont_LAM)
lemmas cont_lemmas1 =
cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM
-use "Tools/cont_proc.ML";
-setup ContProc.setup;
-
-(*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
-(*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*)
-
subsection {* Miscellaneous *}
text {* Monotonicity of @{term Abs_CFun} *}
@@ -530,7 +557,8 @@
monocontlub2cont [OF monofun_strictify2 contlub_strictify2, standard]
lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
-by (unfold strictify_def, simp add: cont_strictify1 cont_strictify2)
+ unfolding strictify_def
+ by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM)
lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>"
by (simp add: strictify_conv_if)
--- a/src/HOLCF/Cont.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOLCF/Cont.thy Sun Jan 18 13:58:17 2009 +0100
@@ -104,6 +104,8 @@
apply simp
done
+lemmas cont2monofunE = cont2mono [THEN monofunE]
+
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]
text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
@@ -135,22 +137,82 @@
apply (erule cpo_lubI)
done
+subsection {* Continuity simproc *}
+
+ML {*
+structure Cont2ContData = NamedThmsFun
+ ( val name = "cont2cont" val description = "continuity intro rule" )
+*}
+
+setup {* Cont2ContData.setup *}
+
+text {*
+ Given the term @{term "cont f"}, the procedure tries to construct the
+ theorem @{term "cont f == True"}. If this theorem cannot be completely
+ solved by the introduction rules, then the procedure returns a
+ conditional rewrite rule with the unsolved subgoals as premises.
+*}
+
+setup {*
+let
+ fun solve_cont thy ss t =
+ let
+ val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
+ val rules = Cont2ContData.get (Simplifier.the_context ss);
+ val tac = REPEAT_ALL_NEW (match_tac rules);
+ in Option.map fst (Seq.pull (tac 1 tr)) end
+
+ val proc =
+ Simplifier.simproc @{theory} "cont_proc" ["cont f"] solve_cont;
+in
+ Simplifier.map_simpset (fn ss => ss addsimprocs [proc])
+end
+*}
+
subsection {* Continuity of basic functions *}
text {* The identity function is continuous *}
-lemma cont_id: "cont (\<lambda>x. x)"
+lemma cont_id [cont2cont]: "cont (\<lambda>x. x)"
apply (rule contI)
apply (erule cpo_lubI)
done
text {* constant functions are continuous *}
-lemma cont_const: "cont (\<lambda>x. c)"
+lemma cont_const [cont2cont]: "cont (\<lambda>x. c)"
apply (rule contI)
apply (rule lub_const)
done
+text {* application of functions is continuous *}
+
+lemma cont2cont_apply:
+ fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" and t :: "'a \<Rightarrow> 'b"
+ assumes f1: "\<And>y. cont (\<lambda>x. f x y)"
+ assumes f2: "\<And>x. cont (\<lambda>y. f x y)"
+ assumes t: "cont (\<lambda>x. t x)"
+ shows "cont (\<lambda>x. (f x) (t x))"
+proof (rule monocontlub2cont [OF monofunI contlubI])
+ fix x y :: "'a" assume "x \<sqsubseteq> y"
+ then show "f x (t x) \<sqsubseteq> f y (t y)"
+ by (auto intro: cont2monofunE [OF f1]
+ cont2monofunE [OF f2]
+ cont2monofunE [OF t]
+ trans_less)
+next
+ fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
+ then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) = (\<Squnion>i. f (Y i) (t (Y i)))"
+ by (simp only: cont2contlubE [OF t] ch2ch_cont [OF t]
+ cont2contlubE [OF f1] ch2ch_cont [OF f1]
+ cont2contlubE [OF f2] ch2ch_cont [OF f2]
+ diag_lub)
+qed
+
+lemma cont2cont_compose:
+ "\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
+by (rule cont2cont_apply [OF cont_const])
+
text {* if-then-else is continuous *}
lemma cont_if [simp]:
--- a/src/HOLCF/Cprod.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOLCF/Cprod.thy Sun Jan 18 13:58:17 2009 +0100
@@ -12,23 +12,6 @@
subsection {* Type @{typ unit} is a pcpo *}
-instantiation unit :: sq_ord
-begin
-
-definition
- less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
-
-instance ..
-end
-
-instance unit :: discrete_cpo
-by intro_classes simp
-
-instance unit :: finite_po ..
-
-instance unit :: pcpo
-by intro_classes simp
-
definition
unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
"unit_when = (\<Lambda> a _. a)"
@@ -39,165 +22,6 @@
lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
by (simp add: unit_when_def)
-
-subsection {* Product type is a partial order *}
-
-instantiation "*" :: (sq_ord, sq_ord) sq_ord
-begin
-
-definition
- less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
-
-instance ..
-end
-
-instance "*" :: (po, po) po
-proof
- fix x :: "'a \<times> 'b"
- show "x \<sqsubseteq> x"
- unfolding less_cprod_def by simp
-next
- fix x y :: "'a \<times> 'b"
- assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
- unfolding less_cprod_def Pair_fst_snd_eq
- by (fast intro: antisym_less)
-next
- fix x y z :: "'a \<times> 'b"
- assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
- unfolding less_cprod_def
- by (fast intro: trans_less)
-qed
-
-subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
-
-lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
-unfolding less_cprod_def by simp
-
-lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) = (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)"
-unfolding less_cprod_def by simp
-
-text {* Pair @{text "(_,_)"} is monotone in both arguments *}
-
-lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
-by (simp add: monofun_def)
-
-lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
-by (simp add: monofun_def)
-
-lemma monofun_pair:
- "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
-by simp
-
-text {* @{term fst} and @{term snd} are monotone *}
-
-lemma monofun_fst: "monofun fst"
-by (simp add: monofun_def less_cprod_def)
-
-lemma monofun_snd: "monofun snd"
-by (simp add: monofun_def less_cprod_def)
-
-subsection {* Product type is a cpo *}
-
-lemma is_lub_Pair:
- "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
-apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: less_cprod_def is_ub_lub)
-apply (frule ub2ub_monofun [OF monofun_fst])
-apply (drule ub2ub_monofun [OF monofun_snd])
-apply (simp add: less_cprod_def is_lub_lub)
-done
-
-lemma lub_cprod:
- 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 -
- have "chain (\<lambda>i. fst (S i))"
- using monofun_fst S by (rule ch2ch_monofun)
- hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
- by (rule cpo_lubI)
- have "chain (\<lambda>i. snd (S i))"
- using monofun_snd S by (rule ch2ch_monofun)
- 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
-
-lemma thelub_cprod:
- "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])
-
-instance "*" :: (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)
- thus "\<exists>x. range S <<| x" ..
-qed
-
-instance "*" :: (finite_po, finite_po) finite_po ..
-
-instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
-proof
- fix x y :: "'a \<times> 'b"
- show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
- unfolding less_cprod_def Pair_fst_snd_eq
- by simp
-qed
-
-subsection {* Product type is pointed *}
-
-lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
-by (simp add: less_cprod_def)
-
-instance "*" :: (pcpo, pcpo) pcpo
-by intro_classes (fast intro: minimal_cprod)
-
-lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_cprod [THEN UU_I, symmetric])
-
-
-subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
-
-lemma cont_pair1: "cont (\<lambda>x. (x, y))"
-apply (rule contI)
-apply (rule is_lub_Pair)
-apply (erule cpo_lubI)
-apply (rule lub_const)
-done
-
-lemma cont_pair2: "cont (\<lambda>y. (x, y))"
-apply (rule contI)
-apply (rule is_lub_Pair)
-apply (rule lub_const)
-apply (erule cpo_lubI)
-done
-
-lemma contlub_fst: "contlub fst"
-apply (rule contlubI)
-apply (simp add: thelub_cprod)
-done
-
-lemma contlub_snd: "contlub snd"
-apply (rule contlubI)
-apply (simp add: thelub_cprod)
-done
-
-lemma cont_fst: "cont fst"
-apply (rule monocontlub2cont)
-apply (rule monofun_fst)
-apply (rule contlub_fst)
-done
-
-lemma cont_snd: "cont snd"
-apply (rule monocontlub2cont)
-apply (rule monofun_snd)
-apply (rule contlub_snd)
-done
-
subsection {* Continuous versions of constants *}
definition
@@ -245,10 +69,10 @@
by (simp add: cpair_eq_pair)
lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
-by (simp add: cpair_eq_pair less_cprod_def)
+by (simp add: cpair_eq_pair)
lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
-by (simp add: inst_cprod_pcpo cpair_eq_pair)
+by (simp add: cpair_eq_pair)
lemma cpair_strict [simp]: "\<langle>\<bottom>, \<bottom>\<rangle> = \<bottom>"
by simp
@@ -273,10 +97,10 @@
by (simp add: cpair_eq_pair csnd_def cont_snd)
lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo2 by (rule cfst_cpair)
+by (simp add: cfst_def)
lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo2 by (rule csnd_cpair)
+by (simp add: csnd_def)
lemma cpair_cfst_csnd: "\<langle>cfst\<cdot>p, csnd\<cdot>p\<rangle> = p"
by (cases p rule: cprodE, simp)
@@ -302,19 +126,10 @@
by (rule compactI, simp add: csnd_less_iff)
lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
-by (rule compactI, simp add: less_cprod)
+by (simp add: cpair_eq_pair)
lemma compact_cpair_iff [simp]: "compact <x, y> = (compact x \<and> compact y)"
-apply (safe intro!: compact_cpair)
-apply (drule compact_cfst, simp)
-apply (drule compact_csnd, simp)
-done
-
-instance "*" :: (chfin, chfin) chfin
-apply intro_classes
-apply (erule compact_imp_max_in_chain)
-apply (rule_tac p="\<Squnion>i. Y i" in cprodE, simp)
-done
+by (simp add: cpair_eq_pair)
lemma lub_cprod2:
"chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
--- a/src/HOLCF/Dsum.thy Sun Jan 18 13:53:15 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,251 +0,0 @@
-(* Title: HOLCF/Dsum.thy
- Author: Brian Huffman
-*)
-
-header {* The cpo of disjoint sums *}
-
-theory Dsum
-imports Bifinite
-begin
-
-subsection {* Ordering on type @{typ "'a + 'b"} *}
-
-instantiation "+" :: (sq_ord, sq_ord) sq_ord
-begin
-
-definition
- less_sum_def: "x \<sqsubseteq> y \<equiv> case x of
- Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
- Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
-
-instance ..
-end
-
-lemma Inl_less_iff [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
-unfolding less_sum_def by simp
-
-lemma Inr_less_iff [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
-unfolding less_sum_def by simp
-
-lemma Inl_less_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
-unfolding less_sum_def by simp
-
-lemma Inr_less_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
-unfolding less_sum_def by simp
-
-lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
-by simp
-
-lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
-by simp
-
-lemma Inl_lessE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-by (cases x, simp_all)
-
-lemma Inr_lessE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-by (cases x, simp_all)
-
-lemmas sum_less_elims = Inl_lessE Inr_lessE
-
-lemma sum_less_cases:
- "\<lbrakk>x \<sqsubseteq> y;
- \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
- \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
- \<Longrightarrow> R"
-by (cases x, safe elim!: sum_less_elims, auto)
-
-subsection {* Sum type is a complete partial order *}
-
-instance "+" :: (po, po) po
-proof
- fix x :: "'a + 'b"
- show "x \<sqsubseteq> x"
- by (induct x, simp_all)
-next
- fix x y :: "'a + 'b"
- assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
- by (induct x, auto elim!: sum_less_elims intro: antisym_less)
-next
- fix x y z :: "'a + 'b"
- assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
- by (induct x, auto elim!: sum_less_elims intro: trans_less)
-qed
-
-lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
-by (rule monofunI, erule sum_less_cases, simp_all)
-
-lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
-by (rule monofunI, erule sum_less_cases, simp_all)
-
-lemma sum_chain_cases:
- assumes Y: "chain Y"
- assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
- assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"
- shows "R"
- apply (cases "Y 0")
- apply (rule A)
- apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
- apply (rule ext)
- apply (cut_tac j=i in chain_mono [OF Y le0], simp)
- apply (erule Inl_lessE, simp)
- apply (rule B)
- apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
- apply (rule ext)
- apply (cut_tac j=i in chain_mono [OF Y le0], simp)
- apply (erule Inr_lessE, simp)
-done
-
-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 (frule ub_rangeD [where i=arbitrary])
- apply (erule Inl_lessE, simp)
- apply (erule is_lub_lub)
- apply (rule ub_rangeI)
- apply (drule ub_rangeD, simp)
-done
-
-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 (frule ub_rangeD [where i=arbitrary])
- apply (erule Inr_lessE, simp)
- apply (erule is_lub_lub)
- apply (rule ub_rangeI)
- apply (drule ub_rangeD, simp)
-done
-
-instance "+" :: (cpo, cpo) cpo
- apply intro_classes
- apply (erule sum_chain_cases, safe)
- apply (rule exI)
- apply (rule is_lub_Inl)
- apply (erule cpo_lubI)
- apply (rule exI)
- apply (rule is_lub_Inr)
- apply (erule cpo_lubI)
-done
-
-subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
-
-lemma cont2cont_Inl [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inl (f x))"
-by (fast intro: contI is_lub_Inl elim: contE)
-
-lemma cont2cont_Inr [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inr (f x))"
-by (fast intro: contI is_lub_Inr elim: contE)
-
-lemma cont_Inl: "cont Inl"
-by (rule cont2cont_Inl [OF cont_id])
-
-lemma cont_Inr: "cont Inr"
-by (rule cont2cont_Inr [OF cont_id])
-
-lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
-lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
-
-lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
-lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
-
-lemma cont_sum_case1:
- assumes f: "\<And>a. cont (\<lambda>x. f x a)"
- assumes g: "\<And>b. cont (\<lambda>x. g x b)"
- shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-by (induct y, simp add: f, simp add: g)
-
-lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)"
-apply (rule contI)
-apply (erule sum_chain_cases)
-apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
-apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
-done
-
-lemma cont2cont_sum_case [simp]:
- assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
- assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
- assumes h: "cont (\<lambda>x. h x)"
- shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-apply (rule cont2cont_app2 [OF cont2cont_lambda _ h])
-apply (rule cont_sum_case1 [OF f1 g1])
-apply (rule cont_sum_case2 [OF f2 g2])
-done
-
-subsection {* Compactness and chain-finiteness *}
-
-lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
-apply (rule compactI2)
-apply (erule sum_chain_cases, safe)
-apply (simp add: lub_Inl)
-apply (erule (2) compactD2)
-apply (simp add: lub_Inr)
-done
-
-lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
-apply (rule compactI2)
-apply (erule sum_chain_cases, safe)
-apply (simp add: lub_Inl)
-apply (simp add: lub_Inr)
-apply (erule (2) compactD2)
-done
-
-lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
-unfolding compact_def
-by (drule adm_subst [OF cont_Inl], simp)
-
-lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
-unfolding compact_def
-by (drule adm_subst [OF cont_Inr], simp)
-
-lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
-by (safe elim!: compact_Inl compact_Inl_rev)
-
-lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
-by (safe elim!: compact_Inr compact_Inr_rev)
-
-instance "+" :: (chfin, chfin) chfin
-apply intro_classes
-apply (erule compact_imp_max_in_chain)
-apply (case_tac "\<Squnion>i. Y i", simp_all)
-done
-
-instance "+" :: (finite_po, finite_po) finite_po ..
-
-instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: less_sum_def split: sum.split)
-
-subsection {* Sum type is a bifinite domain *}
-
-instantiation "+" :: (profinite, profinite) profinite
-begin
-
-definition
- approx_sum_def: "approx =
- (\<lambda>n. \<Lambda> x. case x of Inl a \<Rightarrow> Inl (approx n\<cdot>a) | Inr b \<Rightarrow> Inr (approx n\<cdot>b))"
-
-lemma approx_Inl [simp]: "approx n\<cdot>(Inl x) = Inl (approx n\<cdot>x)"
- unfolding approx_sum_def by simp
-
-lemma approx_Inr [simp]: "approx n\<cdot>(Inr x) = Inr (approx n\<cdot>x)"
- unfolding approx_sum_def by simp
-
-instance proof
- fix i :: nat and x :: "'a + 'b"
- show "chain (approx :: nat \<Rightarrow> 'a + 'b \<rightarrow> 'a + 'b)"
- unfolding approx_sum_def
- by (rule ch2ch_LAM, case_tac x, simp_all)
- show "(\<Squnion>i. approx i\<cdot>x) = x"
- by (induct x, simp_all add: lub_Inl lub_Inr)
- show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
- by (induct x, simp_all)
- have "{x::'a + 'b. approx i\<cdot>x = x} \<subseteq>
- {x::'a. approx i\<cdot>x = x} <+> {x::'b. approx i\<cdot>x = x}"
- by (rule subsetI, case_tac x, simp_all add: InlI InrI)
- thus "finite {x::'a + 'b. approx i\<cdot>x = x}"
- by (rule finite_subset,
- intro finite_Plus finite_fixes_approx)
-qed
-
-end
-
-end
--- a/src/HOLCF/Fixrec.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOLCF/Fixrec.thy Sun Jan 18 13:58:17 2009 +0100
@@ -55,6 +55,7 @@
"maybe_when\<cdot>f\<cdot>r\<cdot>fail = f"
"maybe_when\<cdot>f\<cdot>r\<cdot>(return\<cdot>x) = r\<cdot>x"
by (simp_all add: return_def fail_def maybe_when_def cont_Rep_maybe
+ cont2cont_LAM
cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
translations
--- a/src/HOLCF/HOLCF.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOLCF/HOLCF.thy Sun Jan 18 13:58:17 2009 +0100
@@ -6,10 +6,11 @@
theory HOLCF
imports
- Domain ConvexPD Algebraic Universal Dsum Main
+ Domain ConvexPD Algebraic Universal Sum_Cpo Main
uses
"holcf_logic.ML"
"Tools/cont_consts.ML"
+ "Tools/cont_proc.ML"
"Tools/domain/domain_library.ML"
"Tools/domain/domain_syntax.ML"
"Tools/domain/domain_axioms.ML"
--- a/src/HOLCF/IsaMakefile Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOLCF/IsaMakefile Sun Jan 18 13:58:17 2009 +0100
@@ -1,5 +1,3 @@
-#
-# $Id$
#
# IsaMakefile for HOLCF
#
@@ -41,7 +39,6 @@
Discrete.thy \
Deflation.thy \
Domain.thy \
- Dsum.thy \
Eventual.thy \
Ffun.thy \
Fixrec.thy \
@@ -54,8 +51,10 @@
Pcpodef.thy \
Pcpo.thy \
Porder.thy \
+ Product_Cpo.thy \
Sprod.thy \
Ssum.thy \
+ Sum_Cpo.thy \
Tr.thy \
Universal.thy \
UpperPD.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Product_Cpo.thy Sun Jan 18 13:58:17 2009 +0100
@@ -0,0 +1,247 @@
+(* Title: HOLCF/Product_Cpo.thy
+ Author: Franz Regensburger
+*)
+
+header {* The cpo of cartesian products *}
+
+theory Product_Cpo
+imports Adm
+begin
+
+defaultsort cpo
+
+subsection {* Type @{typ unit} is a pcpo *}
+
+instantiation unit :: sq_ord
+begin
+
+definition
+ less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
+
+instance ..
+end
+
+instance unit :: discrete_cpo
+by intro_classes simp
+
+instance unit :: finite_po ..
+
+instance unit :: pcpo
+by intro_classes simp
+
+
+subsection {* Product type is a partial order *}
+
+instantiation "*" :: (sq_ord, sq_ord) sq_ord
+begin
+
+definition
+ less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
+
+instance ..
+end
+
+instance "*" :: (po, po) po
+proof
+ fix x :: "'a \<times> 'b"
+ show "x \<sqsubseteq> x"
+ unfolding less_cprod_def by simp
+next
+ fix x y :: "'a \<times> 'b"
+ assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
+ unfolding less_cprod_def Pair_fst_snd_eq
+ by (fast intro: antisym_less)
+next
+ fix x y z :: "'a \<times> 'b"
+ assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
+ unfolding less_cprod_def
+ by (fast intro: trans_less)
+qed
+
+subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
+
+lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
+unfolding less_cprod_def by simp
+
+lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
+unfolding less_cprod_def by simp
+
+text {* Pair @{text "(_,_)"} is monotone in both arguments *}
+
+lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
+by (simp add: monofun_def)
+
+lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
+by (simp add: monofun_def)
+
+lemma monofun_pair:
+ "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
+by simp
+
+text {* @{term fst} and @{term snd} are monotone *}
+
+lemma monofun_fst: "monofun fst"
+by (simp add: monofun_def less_cprod_def)
+
+lemma monofun_snd: "monofun snd"
+by (simp add: monofun_def less_cprod_def)
+
+subsection {* Product type is a cpo *}
+
+lemma is_lub_Pair:
+ "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
+apply (rule is_lubI [OF ub_rangeI])
+apply (simp add: less_cprod_def is_ub_lub)
+apply (frule ub2ub_monofun [OF monofun_fst])
+apply (drule ub2ub_monofun [OF monofun_snd])
+apply (simp add: less_cprod_def is_lub_lub)
+done
+
+lemma lub_cprod:
+ 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 -
+ have "chain (\<lambda>i. fst (S i))"
+ using monofun_fst S by (rule ch2ch_monofun)
+ hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
+ by (rule cpo_lubI)
+ have "chain (\<lambda>i. snd (S i))"
+ using monofun_snd S by (rule ch2ch_monofun)
+ 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
+
+lemma thelub_cprod:
+ "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])
+
+instance "*" :: (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)
+ thus "\<exists>x. range S <<| x" ..
+qed
+
+instance "*" :: (finite_po, finite_po) finite_po ..
+
+instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
+proof
+ fix x y :: "'a \<times> 'b"
+ show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
+ unfolding less_cprod_def Pair_fst_snd_eq
+ by simp
+qed
+
+subsection {* Product type is pointed *}
+
+lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
+by (simp add: less_cprod_def)
+
+instance "*" :: (pcpo, pcpo) pcpo
+by intro_classes (fast intro: minimal_cprod)
+
+lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
+by (rule minimal_cprod [THEN UU_I, symmetric])
+
+lemma Pair_defined_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+unfolding inst_cprod_pcpo by simp
+
+lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
+unfolding inst_cprod_pcpo by (rule fst_conv)
+
+lemma csnd_strict [simp]: "snd \<bottom> = \<bottom>"
+unfolding inst_cprod_pcpo by (rule snd_conv)
+
+lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
+by simp
+
+lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
+unfolding split_def by simp
+
+subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
+
+lemma cont_pair1: "cont (\<lambda>x. (x, y))"
+apply (rule contI)
+apply (rule is_lub_Pair)
+apply (erule cpo_lubI)
+apply (rule lub_const)
+done
+
+lemma cont_pair2: "cont (\<lambda>y. (x, y))"
+apply (rule contI)
+apply (rule is_lub_Pair)
+apply (rule lub_const)
+apply (erule cpo_lubI)
+done
+
+lemma contlub_fst: "contlub fst"
+apply (rule contlubI)
+apply (simp add: thelub_cprod)
+done
+
+lemma contlub_snd: "contlub snd"
+apply (rule contlubI)
+apply (simp add: thelub_cprod)
+done
+
+lemma cont_fst: "cont fst"
+apply (rule monocontlub2cont)
+apply (rule monofun_fst)
+apply (rule contlub_fst)
+done
+
+lemma cont_snd: "cont snd"
+apply (rule monocontlub2cont)
+apply (rule monofun_snd)
+apply (rule contlub_snd)
+done
+
+lemma cont2cont_Pair [cont2cont]:
+ assumes f: "cont (\<lambda>x. f x)"
+ assumes g: "cont (\<lambda>x. g x)"
+ shows "cont (\<lambda>x. (f x, g x))"
+apply (rule cont2cont_apply [OF _ cont_pair1 f])
+apply (rule cont2cont_apply [OF _ cont_pair2 g])
+apply (rule cont_const)
+done
+
+lemmas cont2cont_fst [cont2cont] = cont2cont_compose [OF cont_fst]
+
+lemmas cont2cont_snd [cont2cont] = cont2cont_compose [OF cont_snd]
+
+subsection {* Compactness and chain-finiteness *}
+
+lemma fst_less_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
+unfolding less_cprod_def by simp
+
+lemma snd_less_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y = x \<sqsubseteq> (fst x, y)"
+unfolding less_cprod_def by simp
+
+lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
+by (rule compactI, simp add: fst_less_iff)
+
+lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
+by (rule compactI, simp add: snd_less_iff)
+
+lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
+by (rule compactI, simp add: less_cprod_def)
+
+lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
+apply (safe intro!: compact_Pair)
+apply (drule compact_fst, simp)
+apply (drule compact_snd, simp)
+done
+
+instance "*" :: (chfin, chfin) chfin
+apply intro_classes
+apply (erule compact_imp_max_in_chain)
+apply (case_tac "\<Squnion>i. Y i", simp)
+done
+
+end
--- a/src/HOLCF/Ssum.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOLCF/Ssum.thy Sun Jan 18 13:58:17 2009 +0100
@@ -188,7 +188,7 @@
lemma beta_sscase:
"sscase\<cdot>f\<cdot>g\<cdot>s = (\<Lambda><t, x, y>. If t then f\<cdot>x else g\<cdot>y fi)\<cdot>(Rep_Ssum s)"
-unfolding sscase_def by (simp add: cont_Rep_Ssum)
+unfolding sscase_def by (simp add: cont_Rep_Ssum cont2cont_LAM)
lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
unfolding beta_sscase by (simp add: Rep_Ssum_strict)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Sum_Cpo.thy Sun Jan 18 13:58:17 2009 +0100
@@ -0,0 +1,251 @@
+(* Title: HOLCF/Sum_Cpo.thy
+ Author: Brian Huffman
+*)
+
+header {* The cpo of disjoint sums *}
+
+theory Sum_Cpo
+imports Bifinite
+begin
+
+subsection {* Ordering on type @{typ "'a + 'b"} *}
+
+instantiation "+" :: (sq_ord, sq_ord) sq_ord
+begin
+
+definition
+ less_sum_def: "x \<sqsubseteq> y \<equiv> case x of
+ Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
+ Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
+
+instance ..
+end
+
+lemma Inl_less_iff [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
+unfolding less_sum_def by simp
+
+lemma Inr_less_iff [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
+unfolding less_sum_def by simp
+
+lemma Inl_less_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
+unfolding less_sum_def by simp
+
+lemma Inr_less_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
+unfolding less_sum_def by simp
+
+lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
+by simp
+
+lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
+by simp
+
+lemma Inl_lessE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+by (cases x, simp_all)
+
+lemma Inr_lessE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+by (cases x, simp_all)
+
+lemmas sum_less_elims = Inl_lessE Inr_lessE
+
+lemma sum_less_cases:
+ "\<lbrakk>x \<sqsubseteq> y;
+ \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
+ \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
+ \<Longrightarrow> R"
+by (cases x, safe elim!: sum_less_elims, auto)
+
+subsection {* Sum type is a complete partial order *}
+
+instance "+" :: (po, po) po
+proof
+ fix x :: "'a + 'b"
+ show "x \<sqsubseteq> x"
+ by (induct x, simp_all)
+next
+ fix x y :: "'a + 'b"
+ assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
+ by (induct x, auto elim!: sum_less_elims intro: antisym_less)
+next
+ fix x y z :: "'a + 'b"
+ assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
+ by (induct x, auto elim!: sum_less_elims intro: trans_less)
+qed
+
+lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
+by (rule monofunI, erule sum_less_cases, simp_all)
+
+lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
+by (rule monofunI, erule sum_less_cases, simp_all)
+
+lemma sum_chain_cases:
+ assumes Y: "chain Y"
+ assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
+ assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"
+ shows "R"
+ apply (cases "Y 0")
+ apply (rule A)
+ apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
+ apply (rule ext)
+ apply (cut_tac j=i in chain_mono [OF Y le0], simp)
+ apply (erule Inl_lessE, simp)
+ apply (rule B)
+ apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
+ apply (rule ext)
+ apply (cut_tac j=i in chain_mono [OF Y le0], simp)
+ apply (erule Inr_lessE, simp)
+done
+
+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 (frule ub_rangeD [where i=arbitrary])
+ apply (erule Inl_lessE, simp)
+ apply (erule is_lub_lub)
+ apply (rule ub_rangeI)
+ apply (drule ub_rangeD, simp)
+done
+
+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 (frule ub_rangeD [where i=arbitrary])
+ apply (erule Inr_lessE, simp)
+ apply (erule is_lub_lub)
+ apply (rule ub_rangeI)
+ apply (drule ub_rangeD, simp)
+done
+
+instance "+" :: (cpo, cpo) cpo
+ apply intro_classes
+ apply (erule sum_chain_cases, safe)
+ apply (rule exI)
+ apply (rule is_lub_Inl)
+ apply (erule cpo_lubI)
+ apply (rule exI)
+ apply (rule is_lub_Inr)
+ apply (erule cpo_lubI)
+done
+
+subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
+
+lemma cont2cont_Inl [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inl (f x))"
+by (fast intro: contI is_lub_Inl elim: contE)
+
+lemma cont2cont_Inr [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inr (f x))"
+by (fast intro: contI is_lub_Inr elim: contE)
+
+lemma cont_Inl: "cont Inl"
+by (rule cont2cont_Inl [OF cont_id])
+
+lemma cont_Inr: "cont Inr"
+by (rule cont2cont_Inr [OF cont_id])
+
+lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
+lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
+
+lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
+lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
+
+lemma cont_sum_case1:
+ assumes f: "\<And>a. cont (\<lambda>x. f x a)"
+ assumes g: "\<And>b. cont (\<lambda>x. g x b)"
+ shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
+by (induct y, simp add: f, simp add: g)
+
+lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)"
+apply (rule contI)
+apply (erule sum_chain_cases)
+apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
+apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
+done
+
+lemma cont2cont_sum_case [simp]:
+ assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
+ assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
+ assumes h: "cont (\<lambda>x. h x)"
+ shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
+apply (rule cont2cont_app2 [OF cont2cont_lambda _ h])
+apply (rule cont_sum_case1 [OF f1 g1])
+apply (rule cont_sum_case2 [OF f2 g2])
+done
+
+subsection {* Compactness and chain-finiteness *}
+
+lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
+apply (rule compactI2)
+apply (erule sum_chain_cases, safe)
+apply (simp add: lub_Inl)
+apply (erule (2) compactD2)
+apply (simp add: lub_Inr)
+done
+
+lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
+apply (rule compactI2)
+apply (erule sum_chain_cases, safe)
+apply (simp add: lub_Inl)
+apply (simp add: lub_Inr)
+apply (erule (2) compactD2)
+done
+
+lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
+unfolding compact_def
+by (drule adm_subst [OF cont_Inl], simp)
+
+lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
+unfolding compact_def
+by (drule adm_subst [OF cont_Inr], simp)
+
+lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
+by (safe elim!: compact_Inl compact_Inl_rev)
+
+lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
+by (safe elim!: compact_Inr compact_Inr_rev)
+
+instance "+" :: (chfin, chfin) chfin
+apply intro_classes
+apply (erule compact_imp_max_in_chain)
+apply (case_tac "\<Squnion>i. Y i", simp_all)
+done
+
+instance "+" :: (finite_po, finite_po) finite_po ..
+
+instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
+by intro_classes (simp add: less_sum_def split: sum.split)
+
+subsection {* Sum type is a bifinite domain *}
+
+instantiation "+" :: (profinite, profinite) profinite
+begin
+
+definition
+ approx_sum_def: "approx =
+ (\<lambda>n. \<Lambda> x. case x of Inl a \<Rightarrow> Inl (approx n\<cdot>a) | Inr b \<Rightarrow> Inr (approx n\<cdot>b))"
+
+lemma approx_Inl [simp]: "approx n\<cdot>(Inl x) = Inl (approx n\<cdot>x)"
+ unfolding approx_sum_def by simp
+
+lemma approx_Inr [simp]: "approx n\<cdot>(Inr x) = Inr (approx n\<cdot>x)"
+ unfolding approx_sum_def by simp
+
+instance proof
+ fix i :: nat and x :: "'a + 'b"
+ show "chain (approx :: nat \<Rightarrow> 'a + 'b \<rightarrow> 'a + 'b)"
+ unfolding approx_sum_def
+ by (rule ch2ch_LAM, case_tac x, simp_all)
+ show "(\<Squnion>i. approx i\<cdot>x) = x"
+ by (induct x, simp_all add: lub_Inl lub_Inr)
+ show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+ by (induct x, simp_all)
+ have "{x::'a + 'b. approx i\<cdot>x = x} \<subseteq>
+ {x::'a. approx i\<cdot>x = x} <+> {x::'b. approx i\<cdot>x = x}"
+ by (rule subsetI, case_tac x, simp_all add: InlI InrI)
+ thus "finite {x::'a + 'b. approx i\<cdot>x = x}"
+ by (rule finite_subset,
+ intro finite_Plus finite_fixes_approx)
+qed
+
+end
+
+end
--- a/src/HOLCF/Up.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOLCF/Up.thy Sun Jan 18 13:58:17 2009 +0100
@@ -282,10 +282,10 @@
text {* properties of fup *}
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
-by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
+by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
-by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
+by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
by (cases x, simp_all)
--- a/src/HOLCF/ex/Stream.thy Sun Jan 18 13:53:15 2009 +0100
+++ b/src/HOLCF/ex/Stream.thy Sun Jan 18 13:58:17 2009 +0100
@@ -521,7 +521,7 @@
section "smap"
lemma smap_unfold: "smap = (\<Lambda> f t. case t of x&&xs \<Rightarrow> f$x && smap$f$xs)"
-by (insert smap_def [THEN eq_reflection, THEN fix_eq2], auto)
+by (insert smap_def [where 'a='a and 'b='b, THEN eq_reflection, THEN fix_eq2], auto)
lemma smap_empty [simp]: "smap\<cdot>f\<cdot>\<bottom> = \<bottom>"
by (subst smap_unfold, simp)
@@ -540,7 +540,7 @@
lemma sfilter_unfold:
"sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
-by (insert sfilter_def [THEN eq_reflection, THEN fix_eq2], auto)
+by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
apply (rule ext_cfun)
--- a/src/Pure/Isar/class.ML Sun Jan 18 13:53:15 2009 +0100
+++ b/src/Pure/Isar/class.ML Sun Jan 18 13:58:17 2009 +0100
@@ -24,91 +24,80 @@
open Class_Target;
-(** rule calculation **)
-
-fun calculate_axiom thy sups base_sort assm_axiom param_map class =
- case Locale.intros_of thy class
- of (_, NONE) => assm_axiom
- | (_, SOME intro) =>
- let
- fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
- (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
- (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
- Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
- val axiom_premises = map_filter (fst o rules thy) sups
- @ the_list assm_axiom;
- in intro
- |> instantiate thy [class]
- |> (fn thm => thm OF axiom_premises)
- |> Drule.standard'
- |> Thm.close_derivation
- |> SOME
- end;
-
-fun calculate_morphism thy class sups param_map some_axiom =
- let
- val ctxt = ProofContext.init thy;
- val (([props], [(_, morph1)], export_morph), _) = ctxt
- |> Expression.cert_goal_expression ([(class, (("", false),
- Expression.Named ((map o apsnd) Const param_map)))], []);
- val morph2 = morph1
- $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class));
- val morph3 = case props
- of [prop] => morph2
- $> Element.satisfy_morphism [(Element.prove_witness ctxt prop
- (ALLGOALS (ProofContext.fact_tac (the_list some_axiom))))]
- | [] => morph2;
- val morph4 = morph3 $> Element.eq_morphism thy (these_defs thy sups);
- in (morph3, morph4, export_morph) end;
-
-fun calculate_rules thy morph sups base_sort param_map axiom class =
- let
- fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
- (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
- (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
- Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
- val defs = these_defs thy sups;
- val assm_intro = Locale.intros_of thy class
- |> fst
- |> Option.map (instantiate thy base_sort)
- |> Option.map (MetaSimplifier.rewrite_rule defs)
- |> Option.map Thm.close_derivation;
- val fixate = Thm.instantiate
- (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
- (TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], [])
- val of_class_sups = if null sups
- then map (fixate o Thm.class_triv thy) base_sort
- else map (fixate o snd o rules thy) sups;
- val locale_dests = map Drule.standard' (Locale.axioms_of thy class);
- val num_trivs = case length locale_dests
- of 0 => if is_none axiom then 0 else 1
- | n => n;
- val pred_trivs = if num_trivs = 0 then []
- else the axiom
- |> Thm.prop_of
- |> (map_types o map_atyps o K) (TFree (Name.aT, base_sort))
- |> (Thm.assume o Thm.cterm_of thy)
- |> replicate num_trivs;
- val axclass_intro = (#intro o AxClass.get_info thy) class;
- val of_class = (fixate axclass_intro OF of_class_sups OF locale_dests OF pred_trivs)
- |> Drule.standard'
- |> Thm.close_derivation;
- in (assm_intro, of_class) end;
-
-
(** define classes **)
local
+fun calculate thy class sups base_sort param_map assm_axiom =
+ let
+ val empty_ctxt = ProofContext.init thy;
+
+ (* instantiation of canonical interpretation *)
+ (*FIXME inst_morph should be calculated manually and not instantiate constraint*)
+ val aT = TFree ("'a", base_sort);
+ val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt
+ |> Expression.cert_goal_expression ([(class, (("", false),
+ Expression.Named ((map o apsnd) Const param_map)))], []);
+
+ (* witness for canonical interpretation *)
+ val prop = try the_single props;
+ val wit = Option.map (fn prop => let
+ val sup_axioms = map_filter (fst o rules thy) sups;
+ val loc_intro_tac = case Locale.intros_of thy class
+ of (_, NONE) => all_tac
+ | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
+ val tac = loc_intro_tac
+ THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom))
+ in Element.prove_witness empty_ctxt prop tac end) prop;
+ val axiom = Option.map Element.conclude_witness wit;
+
+ (* canonical interpretation *)
+ val base_morph = inst_morph
+ $> Morphism.binding_morphism
+ (Binding.add_prefix false (class_prefix class))
+ $> Element.satisfy_morphism (the_list wit);
+ val defs = these_defs thy sups;
+ val eq_morph = Element.eq_morphism thy defs;
+ val morph = base_morph $> eq_morph;
+
+ (* assm_intro *)
+ fun prove_assm_intro thm =
+ let
+ val prop = thm |> Thm.prop_of |> Logic.unvarify
+ |> Morphism.term (inst_morph $> eq_morph)
+ |> (map_types o map_atyps) (K aT);
+ fun tac ctxt = LocalDefs.unfold_tac ctxt (map Thm.symmetric defs) (*FIXME*)
+ THEN ALLGOALS (ProofContext.fact_tac [thm]);
+ in Goal.prove_global thy [] [] prop (tac o #context) end;
+ val assm_intro = Option.map prove_assm_intro
+ (fst (Locale.intros_of thy class));
+
+ (* of_class *)
+ val of_class_prop_concl = Logic.mk_inclass (aT, class);
+ val of_class_prop = case prop of NONE => of_class_prop_concl
+ | SOME prop => Logic.mk_implies (Morphism.term inst_morph prop,
+ of_class_prop_concl) |> (map_types o map_atyps) (K aT)
+ val sup_of_classes = map (snd o rules thy) sups;
+ val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
+ val axclass_intro = #intro (AxClass.get_info thy class);
+ val base_sort_trivs = Drule.sort_triv thy (aT, base_sort);
+ val tac = REPEAT (SOMEGOAL
+ (Tactic.match_tac (axclass_intro :: sup_of_classes
+ @ loc_axiom_intros @ base_sort_trivs)
+ ORELSE' Tactic.assume_tac));
+ val of_class = Goal.prove_global thy [] [] of_class_prop (K tac);
+
+ in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
+
fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
let
(*FIXME 2009 simplify*)
val supclasses = map (prep_class thy) raw_supclasses;
val supsort = Sign.minimize_sort thy supclasses;
- val sups = filter (is_class thy) supsort;
+ val (sups, bases) = List.partition (is_class thy) supsort;
val base_sort = if null sups then supsort else
- foldr1 (Sorts.inter_sort (Sign.classes_of thy))
- (map (base_sort thy) sups);
+ Library.foldr (Sorts.inter_sort (Sign.classes_of thy))
+ (map (base_sort thy) sups, bases);
val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
val supparam_names = map fst supparams;
val _ = if has_duplicates (op =) supparam_names
@@ -163,7 +152,7 @@
end;
in
thy
- |> Sign.add_path (Logic.const_of_class bname)
+ |> Sign.add_path (class_prefix class)
|> fold_map add_const raw_params
||> Sign.restore_naming thy
|-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
@@ -205,14 +194,11 @@
|> snd |> LocalTheory.exit_global
|> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
|-> (fn (param_map, params, assm_axiom) =>
- `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
- #-> (fn axiom =>
- `(fn thy => calculate_morphism thy class sups param_map axiom)
- #-> (fn (raw_morph, morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
- #> Locale.activate_global_facts (class, morph $> export_morph)
- #> `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
- #-> (fn (assm_intro, of_class) =>
- register class sups params base_sort raw_morph axiom assm_intro of_class))))
+ `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
+ #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
+ Locale.add_registration (class, (morph, export_morph))
+ #> Locale.activate_global_facts (class, morph $> export_morph)
+ #> register class sups params base_sort base_morph axiom assm_intro of_class))
|> TheoryTarget.init (SOME class)
|> pair class
end;
@@ -286,6 +272,4 @@
end; (*local*)
-
end;
-
--- a/src/Pure/Isar/class_target.ML Sun Jan 18 13:53:15 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Sun Jan 18 13:58:17 2009 +0100
@@ -115,7 +115,7 @@
consts: (string * string) list
(*locale parameter ~> constant name*),
base_sort: sort,
- base_morph: Morphism.morphism
+ base_morph: morphism
(*static part of canonical morphism*),
assm_intro: thm option,
of_class: thm,
--- a/src/Pure/Isar/locale.ML Sun Jan 18 13:53:15 2009 +0100
+++ b/src/Pure/Isar/locale.ML Sun Jan 18 13:58:17 2009 +0100
@@ -37,7 +37,7 @@
thm option * thm option -> thm list ->
(declaration * stamp) list * (declaration * stamp) list ->
((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
- ((string * Morphism.morphism) * stamp) list -> theory -> theory
+ ((string * morphism) * stamp) list -> theory -> theory
(* Locale name space *)
val intern: theory -> xstring -> string
@@ -48,9 +48,10 @@
val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
val intros_of: theory -> string -> thm option * thm option
val axioms_of: theory -> string -> thm list
- val instance_of: theory -> string -> Morphism.morphism -> term list
+ val instance_of: theory -> string -> morphism -> term list
val specification_of: theory -> string -> term option * term list
val declarations_of: theory -> string -> declaration list * declaration list
+ val dependencies_of: theory -> string -> (string * morphism) list
(* Storing results *)
val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -58,13 +59,13 @@
val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
val add_declaration: string -> declaration -> Proof.context -> Proof.context
- val add_dependency: string -> string * Morphism.morphism -> theory -> theory
+ val add_dependency: string -> string * morphism -> theory -> theory
(* Activation *)
- val activate_declarations: theory -> string * Morphism.morphism ->
+ val activate_declarations: theory -> string * morphism ->
Proof.context -> Proof.context
- val activate_global_facts: string * Morphism.morphism -> theory -> theory
- val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
+ val activate_global_facts: string * morphism -> theory -> theory
+ val activate_local_facts: string * morphism -> Proof.context -> Proof.context
val init: string -> theory -> Proof.context
(* Reasoning about locales *)
@@ -74,11 +75,11 @@
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
(* Registrations *)
- val add_registration: string * (Morphism.morphism * Morphism.morphism) ->
+ val add_registration: string * (morphism * morphism) ->
theory -> theory
- val amend_registration: Morphism.morphism -> string * Morphism.morphism ->
+ val amend_registration: morphism -> string * morphism ->
theory -> theory
- val get_registrations: theory -> (string * Morphism.morphism) list
+ val get_registrations: theory -> (string * morphism) list
(* Diagnostic *)
val print_locales: theory -> unit
@@ -128,7 +129,7 @@
(* type and term syntax declarations *)
notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
(* theorem declarations *)
- dependencies: ((string * Morphism.morphism) * stamp) list
+ dependencies: ((string * morphism) * stamp) list
(* locale dependencies (sublocale relation) *)
};
@@ -193,6 +194,9 @@
fun declarations_of thy name = the_locale thy name |>
#decls |> apfst (map fst) |> apsnd (map fst);
+fun dependencies_of thy name = the_locale thy name |>
+ #dependencies |> map fst;
+
(*** Activate context elements of locale ***)
@@ -389,7 +393,7 @@
structure RegistrationsData = TheoryDataFun
(
- type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
+ type T = ((string * (morphism * morphism)) * stamp) list;
(* FIXME mixins need to be stamped *)
(* registrations, in reverse order of declaration *)
val empty = [];