# HG changeset patch # User nipkow # Date 1232283497 -3600 # Node ID 7187373c6cb1ff412cc01fd91a2af86a88950e71 # Parent 02a52ae34b7a097a74a13ed570d6b3a2878b132b# Parent f2587922591e39f4682caf669b1a46aa8e3ed24a bug fixes diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOL/Fundamental_Theorem_Algebra.thy --- 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 \ p = 0" - unfolding plength_def by simp +lemma psize_eq_0_iff [simp]: "psize p = 0 \ p = 0" + unfolding psize_def by simp -lemma poly_offset: "\ q. plength q = plength p \ (\x. poly q (x::complex) = poly p (a + x))" +lemma poly_offset: "\ q. psize q = psize p \ (\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 "\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 = (\x y. f x = f y)" -lemma nonconstant_length: "\ (constant (poly p)) \ plength p \ 2" - unfolding constant_def plength_def +lemma nonconstant_length: "\ (constant (poly p)) \ psize p \ 2" + unfolding constant_def psize_def apply (induct p, auto) done @@ -733,9 +733,9 @@ lemma poly_decompose_lemma: assumes nz: "\(\z. z\0 \ poly p z = (0::'a::{recpower,idom}))" - shows "\k a q. a\0 \ Suc (plength q + k) = plength p \ + shows "\k a q. a\0 \ Suc (psize q + k) = psize p \ (\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 "\k a q. a\(0::'a::{recpower,idom}) \ k\0 \ - plength q + k + 1 = plength p \ + psize q + k + 1 = psize p \ (\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 "\z::complex. poly p z = 0" using nc -proof(induct n\ "plength p" arbitrary: p rule: nat_less_induct) +proof(induct n\ "psize p" arbitrary: p rule: nat_less_induct) fix n fix p :: "complex poly" let ?p = "poly p" - assume H: "\mp. \ constant (poly p) \ m = plength p \ (\(z::complex). poly p z = 0)" and nc: "\ constant ?p" and n: "n = plength p" + assume H: "\mp. \ constant (poly p) \ m = psize p \ (\(z::complex). poly p z = 0)" and nc: "\ constant ?p" and n: "n = psize p" let ?ths = "\z. ?p z = 0" from nonconstant_length[OF nc] have n2: "n\ 2" by (simp add: n) @@ -804,7 +804,7 @@ moreover {assume pc0: "?p c \ 0" from poly_offset[of p c] obtain q where - q: "plength q = plength p" "\x. poly q x = ?p (c+x)" by blast + q: "psize q = psize p" "\x. poly q x = ?p (c+x)" by blast {assume h: "constant (poly q)" from q(2) have th: "\x. poly q (x - c) = ?p x" by auto {fix x y @@ -823,8 +823,8 @@ have qr: "\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: "\x y. poly ?r x = poly ?r y" {fix x y @@ -844,7 +844,7 @@ finally have "cmod (poly ?r w) < 1 \ cmod (poly q w) < cmod ?a0" .} note mrmq_eq = this from poly_decompose[OF rnc] obtain k a s where - kas: "a\0" "k\0" "plength s + k + 1 = plength ?r" + kas: "a\0" "k\0" "psize s + k + 1 = psize ?r" "\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 \ 0" - shows "(\x. poly (pCons a p) x = 0 \ poly q x \ 0) \ \ ((pCons a p) dvd (q ^ (plength p)))" + shows "(\x. poly (pCons a p) x = 0 \ poly q x \ 0) \ \ ((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 "(\x. poly (pCons a p) x = 0 \ poly q x \ 0) \ \ ((pCons a p) dvd (q ^ (plength p)))" + show "(\x. poly (pCons a p) x = 0 \ poly q x \ 0) \ \ ((pCons a p) dvd (q ^ (psize p)))" unfolding dp by - (atomize (full), auto) qed diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOL/Polynomial.thy --- 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) \ max (degree p) (degree q)" +lemma degree_add_le_max: "degree (p + q) \ max (degree p) (degree q)" by (rule degree_le, auto simp add: coeff_eq_0) +lemma degree_add_le: + "\degree p \ n; degree q \ n\ \ degree (p + q) \ n" + by (auto intro: order_trans degree_add_le_max) + lemma degree_add_less: "\degree p < n; degree q < n\ \ 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 \ 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) \ max (degree p) (degree q)" +lemma degree_diff_le_max: "degree (p - q) \ max (degree p) (degree q)" using degree_add_le [where p=p and q="-q"] by (simp add: diff_minus) +lemma degree_diff_le: + "\degree p \ n; degree q \ n\ \ degree (p - q) \ n" + by (simp add: diff_minus degree_add_le) + lemma degree_diff_less: "\degree p < n; degree q < n\ \ 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 = (\i\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 \ 'a poly \ 'a poly \ 'a poly \ bool" + pdivmod_rel :: "'a::field poly \ 'a poly \ 'a poly \ 'a poly \ bool" where [code del]: - "divmod_poly_rel x y q r \ + "pdivmod_rel x y q r \ x = q * y + r \ (if y = 0 then q = 0 else r = 0 \ 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 \ 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 \ 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 \ 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 \ degree ?r < degree y" proof (rule eq_zero_or_degree_less) - have "degree ?r \ max (degree (pCons a r)) (degree (smult b y))" - by (rule degree_diff_le) - also have "\ \ degree y" - proof (rule min_max.le_supI) + show "degree ?r \ degree y" + proof (rule degree_diff_le) show "degree (pCons a r) \ degree y" using r by auto show "degree (smult b y) \ degree y" by (rule degree_smult_le) qed - finally show "degree ?r \ degree y" . next show "coeff ?r (degree y) = 0" using `y \ 0` unfolding b by simp qed from 1 2 show ?thesis - unfolding divmod_poly_rel_def + unfolding pdivmod_rel_def using `y \ 0` by simp qed -lemma divmod_poly_rel_exists: "\q r. divmod_poly_rel x y q r" +lemma pdivmod_rel_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 \ 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 \ 0" from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \ 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 \ 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 \ 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. \r. divmod_poly_rel x y q r)" + [code del]: "x div y = (THE q. \r. pdivmod_rel x y q r)" definition mod_poly where - [code del]: "x mod y = (THE r. \q. divmod_poly_rel x y q r)" + [code del]: "x mod y = (THE r. \q. pdivmod_rel x y q r)" lemma div_poly_eq: - "divmod_poly_rel x y q r \ x div y = q" + "pdivmod_rel x y q r \ 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 \ x mod y = r" + "pdivmod_rel x y q r \ 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 \ 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 \ 0 \ x mod y = 0 \ 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 \ 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 \ 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 \ 'a poly \ 'a poly \ 'a poly" + pdivmod :: "'a::field poly \ 'a poly \ 'a poly \ '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 diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/Cfun.thy --- 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 (\x. f x)" assumes t: "cont (\x. t x)" shows "cont (\x. (f x)\(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: "\x. cont (\y. f x y)" assumes f2: "\y. cont (\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 \ 'b::cpo \ 'c::cpo" + assumes f: "cont (\p. f (fst p) (snd p))" + shows "cont (\x. \ y. f x y)" +proof (rule cont2cont_LAM) + fix x :: 'a + have "cont (\y. (x, y))" + by (rule cont_pair2) + with f have "cont (\y. f (fst (x, y)) (snd (x, y)))" + by (rule cont2cont_app3) + thus "cont (\y. f x y)" + by (simp only: fst_conv snd_conv) +next + fix y :: 'b + have "cont (\x. (x, y))" + by (rule cont_pair1) + with f have "cont (\x. f (fst (x, y)) (snd (x, y)))" + by (rule cont2cont_app3) + thus "cont (\x. f x y)" + by (simp only: fst_conv snd_conv) +qed + +lemma cont2cont_LAM_discrete [cont2cont]: + "(\y::'a::discrete_cpo. cont (\x. f x y)) \ cont (\x. \ 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\f\x = (if x = \ then \ else f\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\f\\ = \" by (simp add: strictify_conv_if) diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/Cont.thy --- 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 \ monofun f \ 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 (\x. x)" +lemma cont_id [cont2cont]: "cont (\x. x)" apply (rule contI) apply (erule cpo_lubI) done text {* constant functions are continuous *} -lemma cont_const: "cont (\x. c)" +lemma cont_const [cont2cont]: "cont (\x. c)" apply (rule contI) apply (rule lub_const) done +text {* application of functions is continuous *} + +lemma cont2cont_apply: + fixes f :: "'a::cpo \ 'b::cpo \ 'c::cpo" and t :: "'a \ 'b" + assumes f1: "\y. cont (\x. f x y)" + assumes f2: "\x. cont (\y. f x y)" + assumes t: "cont (\x. t x)" + shows "cont (\x. (f x) (t x))" +proof (rule monocontlub2cont [OF monofunI contlubI]) + fix x y :: "'a" assume "x \ y" + then show "f x (t x) \ f y (t y)" + by (auto intro: cont2monofunE [OF f1] + cont2monofunE [OF f2] + cont2monofunE [OF t] + trans_less) +next + fix Y :: "nat \ 'a" assume "chain Y" + then show "f (\i. Y i) (t (\i. Y i)) = (\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: + "\cont c; cont (\x. f x)\ \ cont (\x. c (f x))" +by (rule cont2cont_apply [OF cont_const]) + text {* if-then-else is continuous *} lemma cont_if [simp]: diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/Cprod.thy --- 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 \ (y::unit) \ 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 \ unit \ 'a" where "unit_when = (\ a _. a)" @@ -39,165 +22,6 @@ lemma unit_when [simp]: "unit_when\a\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 \) \ \p1 p2. (fst p1 \ fst p2 \ snd p1 \ snd p2)" - -instance .. -end - -instance "*" :: (po, po) po -proof - fix x :: "'a \ 'b" - show "x \ x" - unfolding less_cprod_def by simp -next - fix x y :: "'a \ 'b" - assume "x \ y" "y \ x" thus "x = y" - unfolding less_cprod_def Pair_fst_snd_eq - by (fast intro: antisym_less) -next - fix x y z :: "'a \ 'b" - assume "x \ y" "y \ z" thus "x \ z" - unfolding less_cprod_def - by (fast intro: trans_less) -qed - -subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} - -lemma prod_lessI: "\fst p \ fst q; snd p \ snd q\ \ p \ q" -unfolding less_cprod_def by simp - -lemma Pair_less_iff [simp]: "(a, b) \ (c, d) = (a \ c \ b \ d)" -unfolding less_cprod_def by simp - -text {* Pair @{text "(_,_)"} is monotone in both arguments *} - -lemma monofun_pair1: "monofun (\x. (x, y))" -by (simp add: monofun_def) - -lemma monofun_pair2: "monofun (\y. (x, y))" -by (simp add: monofun_def) - -lemma monofun_pair: - "\x1 \ x2; y1 \ y2\ \ (x1, y1) \ (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: - "\range X <<| x; range Y <<| y\ \ range (\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 \ ('a::cpo \ 'b::cpo)" - assumes S: "chain S" - shows "range S <<| (\i. fst (S i), \i. snd (S i))" -proof - - have "chain (\i. fst (S i))" - using monofun_fst S by (rule ch2ch_monofun) - hence 1: "range (\i. fst (S i)) <<| (\i. fst (S i))" - by (rule cpo_lubI) - have "chain (\i. snd (S i))" - using monofun_snd S by (rule ch2ch_monofun) - hence 2: "range (\i. snd (S i)) <<| (\i. snd (S i))" - by (rule cpo_lubI) - show "range S <<| (\i. fst (S i), \i. snd (S i))" - using is_lub_Pair [OF 1 2] by simp -qed - -lemma thelub_cprod: - "chain (S::nat \ 'a::cpo \ 'b::cpo) - \ (\i. S i) = (\i. fst (S i), \i. snd (S i))" -by (rule lub_cprod [THEN thelubI]) - -instance "*" :: (cpo, cpo) cpo -proof - fix S :: "nat \ ('a \ 'b)" - assume "chain S" - hence "range S <<| (\i. fst (S i), \i. snd (S i))" - by (rule lub_cprod) - thus "\x. range S <<| x" .. -qed - -instance "*" :: (finite_po, finite_po) finite_po .. - -instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo -proof - fix x y :: "'a \ 'b" - show "x \ y \ x = y" - unfolding less_cprod_def Pair_fst_snd_eq - by simp -qed - -subsection {* Product type is pointed *} - -lemma minimal_cprod: "(\, \) \ p" -by (simp add: less_cprod_def) - -instance "*" :: (pcpo, pcpo) pcpo -by intro_classes (fast intro: minimal_cprod) - -lemma inst_cprod_pcpo: "\ = (\, \)" -by (rule minimal_cprod [THEN UU_I, symmetric]) - - -subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} - -lemma cont_pair1: "cont (\x. (x, y))" -apply (rule contI) -apply (rule is_lub_Pair) -apply (erule cpo_lubI) -apply (rule lub_const) -done - -lemma cont_pair2: "cont (\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 \ a' \ b \ b')" -by (simp add: cpair_eq_pair less_cprod_def) +by (simp add: cpair_eq_pair) lemma cpair_defined_iff [iff]: "( = \) = (x = \ \ y = \)" -by (simp add: inst_cprod_pcpo cpair_eq_pair) +by (simp add: cpair_eq_pair) lemma cpair_strict [simp]: "\\, \\ = \" by simp @@ -273,10 +97,10 @@ by (simp add: cpair_eq_pair csnd_def cont_snd) lemma cfst_strict [simp]: "cfst\\ = \" -unfolding inst_cprod_pcpo2 by (rule cfst_cpair) +by (simp add: cfst_def) lemma csnd_strict [simp]: "csnd\\ = \" -unfolding inst_cprod_pcpo2 by (rule csnd_cpair) +by (simp add: csnd_def) lemma cpair_cfst_csnd: "\cfst\p, csnd\p\ = p" by (cases p rule: cprodE, simp) @@ -302,19 +126,10 @@ by (rule compactI, simp add: csnd_less_iff) lemma compact_cpair: "\compact x; compact y\ \ compact " -by (rule compactI, simp add: less_cprod) +by (simp add: cpair_eq_pair) lemma compact_cpair_iff [simp]: "compact = (compact x \ 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="\i. Y i" in cprodE, simp) -done +by (simp add: cpair_eq_pair) lemma lub_cprod2: "chain S \ range S <<| <\i. cfst\(S i), \i. csnd\(S i)>" diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/Dsum.thy --- 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 \ y \ case x of - Inl a \ (case y of Inl b \ a \ b | Inr b \ False) | - Inr a \ (case y of Inl b \ False | Inr b \ a \ b)" - -instance .. -end - -lemma Inl_less_iff [simp]: "Inl x \ Inl y = x \ y" -unfolding less_sum_def by simp - -lemma Inr_less_iff [simp]: "Inr x \ Inr y = x \ y" -unfolding less_sum_def by simp - -lemma Inl_less_Inr [simp]: "\ Inl x \ Inr y" -unfolding less_sum_def by simp - -lemma Inr_less_Inl [simp]: "\ Inr x \ Inl y" -unfolding less_sum_def by simp - -lemma Inl_mono: "x \ y \ Inl x \ Inl y" -by simp - -lemma Inr_mono: "x \ y \ Inr x \ Inr y" -by simp - -lemma Inl_lessE: "\Inl a \ x; \b. \x = Inl b; a \ b\ \ R\ \ R" -by (cases x, simp_all) - -lemma Inr_lessE: "\Inr a \ x; \b. \x = Inr b; a \ b\ \ R\ \ R" -by (cases x, simp_all) - -lemmas sum_less_elims = Inl_lessE Inr_lessE - -lemma sum_less_cases: - "\x \ y; - \a b. \x = Inl a; y = Inl b; a \ b\ \ R; - \a b. \x = Inr a; y = Inr b; a \ b\ \ R\ - \ 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 \ x" - by (induct x, simp_all) -next - fix x y :: "'a + 'b" - assume "x \ y" and "y \ x" thus "x = y" - by (induct x, auto elim!: sum_less_elims intro: antisym_less) -next - fix x y z :: "'a + 'b" - assume "x \ y" and "y \ z" thus "x \ z" - by (induct x, auto elim!: sum_less_elims intro: trans_less) -qed - -lemma monofun_inv_Inl: "monofun (\p. THE a. p = Inl a)" -by (rule monofunI, erule sum_less_cases, simp_all) - -lemma monofun_inv_Inr: "monofun (\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: "\A. \chain A; Y = (\i. Inl (A i))\ \ R" - assumes B: "\B. \chain B; Y = (\i. Inr (B i))\ \ 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 \ range (\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 \ range (\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 \ cont (\x. Inl (f x))" -by (fast intro: contI is_lub_Inl elim: contE) - -lemma cont2cont_Inr [simp]: "cont f \ cont (\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: "\a. cont (\x. f x a)" - assumes g: "\b. cont (\x. g x b)" - shows "cont (\x. case y of Inl a \ f x a | Inr b \ g x b)" -by (induct y, simp add: f, simp add: g) - -lemma cont_sum_case2: "\cont f; cont g\ \ 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: "\a. cont (\x. f x a)" and f2: "\x. cont (\a. f x a)" - assumes g1: "\b. cont (\x. g x b)" and g2: "\x. cont (\b. g x b)" - assumes h: "cont (\x. h x)" - shows "cont (\x. case h x of Inl a \ f x a | Inr b \ 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 \ 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 \ 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) \ compact a" -unfolding compact_def -by (drule adm_subst [OF cont_Inl], simp) - -lemma compact_Inr_rev: "compact (Inr a) \ 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 "\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 = - (\n. \ x. case x of Inl a \ Inl (approx n\a) | Inr b \ Inr (approx n\b))" - -lemma approx_Inl [simp]: "approx n\(Inl x) = Inl (approx n\x)" - unfolding approx_sum_def by simp - -lemma approx_Inr [simp]: "approx n\(Inr x) = Inr (approx n\x)" - unfolding approx_sum_def by simp - -instance proof - fix i :: nat and x :: "'a + 'b" - show "chain (approx :: nat \ 'a + 'b \ 'a + 'b)" - unfolding approx_sum_def - by (rule ch2ch_LAM, case_tac x, simp_all) - show "(\i. approx i\x) = x" - by (induct x, simp_all add: lub_Inl lub_Inr) - show "approx i\(approx i\x) = approx i\x" - by (induct x, simp_all) - have "{x::'a + 'b. approx i\x = x} \ - {x::'a. approx i\x = x} <+> {x::'b. approx i\x = x}" - by (rule subsetI, case_tac x, simp_all add: InlI InrI) - thus "finite {x::'a + 'b. approx i\x = x}" - by (rule finite_subset, - intro finite_Plus finite_fixes_approx) -qed - -end - -end diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/Fixrec.thy --- 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\f\r\fail = f" "maybe_when\f\r\(return\x) = r\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 diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/HOLCF.thy --- 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" diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/IsaMakefile --- 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 \ diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/Product_Cpo.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 \ (y::unit) \ 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 \) \ \p1 p2. (fst p1 \ fst p2 \ snd p1 \ snd p2)" + +instance .. +end + +instance "*" :: (po, po) po +proof + fix x :: "'a \ 'b" + show "x \ x" + unfolding less_cprod_def by simp +next + fix x y :: "'a \ 'b" + assume "x \ y" "y \ x" thus "x = y" + unfolding less_cprod_def Pair_fst_snd_eq + by (fast intro: antisym_less) +next + fix x y z :: "'a \ 'b" + assume "x \ y" "y \ z" thus "x \ z" + unfolding less_cprod_def + by (fast intro: trans_less) +qed + +subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} + +lemma prod_lessI: "\fst p \ fst q; snd p \ snd q\ \ p \ q" +unfolding less_cprod_def by simp + +lemma Pair_less_iff [simp]: "(a, b) \ (c, d) \ a \ c \ b \ d" +unfolding less_cprod_def by simp + +text {* Pair @{text "(_,_)"} is monotone in both arguments *} + +lemma monofun_pair1: "monofun (\x. (x, y))" +by (simp add: monofun_def) + +lemma monofun_pair2: "monofun (\y. (x, y))" +by (simp add: monofun_def) + +lemma monofun_pair: + "\x1 \ x2; y1 \ y2\ \ (x1, y1) \ (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: + "\range X <<| x; range Y <<| y\ \ range (\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 \ ('a::cpo \ 'b::cpo)" + assumes S: "chain S" + shows "range S <<| (\i. fst (S i), \i. snd (S i))" +proof - + have "chain (\i. fst (S i))" + using monofun_fst S by (rule ch2ch_monofun) + hence 1: "range (\i. fst (S i)) <<| (\i. fst (S i))" + by (rule cpo_lubI) + have "chain (\i. snd (S i))" + using monofun_snd S by (rule ch2ch_monofun) + hence 2: "range (\i. snd (S i)) <<| (\i. snd (S i))" + by (rule cpo_lubI) + show "range S <<| (\i. fst (S i), \i. snd (S i))" + using is_lub_Pair [OF 1 2] by simp +qed + +lemma thelub_cprod: + "chain (S::nat \ 'a::cpo \ 'b::cpo) + \ (\i. S i) = (\i. fst (S i), \i. snd (S i))" +by (rule lub_cprod [THEN thelubI]) + +instance "*" :: (cpo, cpo) cpo +proof + fix S :: "nat \ ('a \ 'b)" + assume "chain S" + hence "range S <<| (\i. fst (S i), \i. snd (S i))" + by (rule lub_cprod) + thus "\x. range S <<| x" .. +qed + +instance "*" :: (finite_po, finite_po) finite_po .. + +instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo +proof + fix x y :: "'a \ 'b" + show "x \ y \ x = y" + unfolding less_cprod_def Pair_fst_snd_eq + by simp +qed + +subsection {* Product type is pointed *} + +lemma minimal_cprod: "(\, \) \ p" +by (simp add: less_cprod_def) + +instance "*" :: (pcpo, pcpo) pcpo +by intro_classes (fast intro: minimal_cprod) + +lemma inst_cprod_pcpo: "\ = (\, \)" +by (rule minimal_cprod [THEN UU_I, symmetric]) + +lemma Pair_defined_iff [simp]: "(x, y) = \ \ x = \ \ y = \" +unfolding inst_cprod_pcpo by simp + +lemma fst_strict [simp]: "fst \ = \" +unfolding inst_cprod_pcpo by (rule fst_conv) + +lemma csnd_strict [simp]: "snd \ = \" +unfolding inst_cprod_pcpo by (rule snd_conv) + +lemma Pair_strict [simp]: "(\, \) = \" +by simp + +lemma split_strict [simp]: "split f \ = f \ \" +unfolding split_def by simp + +subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} + +lemma cont_pair1: "cont (\x. (x, y))" +apply (rule contI) +apply (rule is_lub_Pair) +apply (erule cpo_lubI) +apply (rule lub_const) +done + +lemma cont_pair2: "cont (\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 (\x. f x)" + assumes g: "cont (\x. g x)" + shows "cont (\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 \ 'b) \ y \ x \ (y, snd x)" +unfolding less_cprod_def by simp + +lemma snd_less_iff: "snd (x::'a \ 'b) \ y = x \ (fst x, y)" +unfolding less_cprod_def by simp + +lemma compact_fst: "compact x \ compact (fst x)" +by (rule compactI, simp add: fst_less_iff) + +lemma compact_snd: "compact x \ compact (snd x)" +by (rule compactI, simp add: snd_less_iff) + +lemma compact_Pair: "\compact x; compact y\ \ compact (x, y)" +by (rule compactI, simp add: less_cprod_def) + +lemma compact_Pair_iff [simp]: "compact (x, y) \ compact x \ 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 "\i. Y i", simp) +done + +end diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/Ssum.thy --- 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\f\g\s = (\. If t then f\x else g\y fi)\(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\f\g\\ = \" unfolding beta_sscase by (simp add: Rep_Ssum_strict) diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/Sum_Cpo.thy --- /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 \ y \ case x of + Inl a \ (case y of Inl b \ a \ b | Inr b \ False) | + Inr a \ (case y of Inl b \ False | Inr b \ a \ b)" + +instance .. +end + +lemma Inl_less_iff [simp]: "Inl x \ Inl y = x \ y" +unfolding less_sum_def by simp + +lemma Inr_less_iff [simp]: "Inr x \ Inr y = x \ y" +unfolding less_sum_def by simp + +lemma Inl_less_Inr [simp]: "\ Inl x \ Inr y" +unfolding less_sum_def by simp + +lemma Inr_less_Inl [simp]: "\ Inr x \ Inl y" +unfolding less_sum_def by simp + +lemma Inl_mono: "x \ y \ Inl x \ Inl y" +by simp + +lemma Inr_mono: "x \ y \ Inr x \ Inr y" +by simp + +lemma Inl_lessE: "\Inl a \ x; \b. \x = Inl b; a \ b\ \ R\ \ R" +by (cases x, simp_all) + +lemma Inr_lessE: "\Inr a \ x; \b. \x = Inr b; a \ b\ \ R\ \ R" +by (cases x, simp_all) + +lemmas sum_less_elims = Inl_lessE Inr_lessE + +lemma sum_less_cases: + "\x \ y; + \a b. \x = Inl a; y = Inl b; a \ b\ \ R; + \a b. \x = Inr a; y = Inr b; a \ b\ \ R\ + \ 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 \ x" + by (induct x, simp_all) +next + fix x y :: "'a + 'b" + assume "x \ y" and "y \ x" thus "x = y" + by (induct x, auto elim!: sum_less_elims intro: antisym_less) +next + fix x y z :: "'a + 'b" + assume "x \ y" and "y \ z" thus "x \ z" + by (induct x, auto elim!: sum_less_elims intro: trans_less) +qed + +lemma monofun_inv_Inl: "monofun (\p. THE a. p = Inl a)" +by (rule monofunI, erule sum_less_cases, simp_all) + +lemma monofun_inv_Inr: "monofun (\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: "\A. \chain A; Y = (\i. Inl (A i))\ \ R" + assumes B: "\B. \chain B; Y = (\i. Inr (B i))\ \ 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 \ range (\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 \ range (\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 \ cont (\x. Inl (f x))" +by (fast intro: contI is_lub_Inl elim: contE) + +lemma cont2cont_Inr [simp]: "cont f \ cont (\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: "\a. cont (\x. f x a)" + assumes g: "\b. cont (\x. g x b)" + shows "cont (\x. case y of Inl a \ f x a | Inr b \ g x b)" +by (induct y, simp add: f, simp add: g) + +lemma cont_sum_case2: "\cont f; cont g\ \ 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: "\a. cont (\x. f x a)" and f2: "\x. cont (\a. f x a)" + assumes g1: "\b. cont (\x. g x b)" and g2: "\x. cont (\b. g x b)" + assumes h: "cont (\x. h x)" + shows "cont (\x. case h x of Inl a \ f x a | Inr b \ 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 \ 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 \ 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) \ compact a" +unfolding compact_def +by (drule adm_subst [OF cont_Inl], simp) + +lemma compact_Inr_rev: "compact (Inr a) \ 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 "\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 = + (\n. \ x. case x of Inl a \ Inl (approx n\a) | Inr b \ Inr (approx n\b))" + +lemma approx_Inl [simp]: "approx n\(Inl x) = Inl (approx n\x)" + unfolding approx_sum_def by simp + +lemma approx_Inr [simp]: "approx n\(Inr x) = Inr (approx n\x)" + unfolding approx_sum_def by simp + +instance proof + fix i :: nat and x :: "'a + 'b" + show "chain (approx :: nat \ 'a + 'b \ 'a + 'b)" + unfolding approx_sum_def + by (rule ch2ch_LAM, case_tac x, simp_all) + show "(\i. approx i\x) = x" + by (induct x, simp_all add: lub_Inl lub_Inr) + show "approx i\(approx i\x) = approx i\x" + by (induct x, simp_all) + have "{x::'a + 'b. approx i\x = x} \ + {x::'a. approx i\x = x} <+> {x::'b. approx i\x = x}" + by (rule subsetI, case_tac x, simp_all add: InlI InrI) + thus "finite {x::'a + 'b. approx i\x = x}" + by (rule finite_subset, + intro finite_Plus finite_fixes_approx) +qed + +end + +end diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/Up.thy --- 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\f\\ = \" -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\f\(up\x) = f\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\up\x = x" by (cases x, simp_all) diff -r 02a52ae34b7a -r 7187373c6cb1 src/HOLCF/ex/Stream.thy --- 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 = (\ f t. case t of x&&xs \ 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\f\\ = \" by (subst smap_unfold, simp) @@ -540,7 +540,7 @@ lemma sfilter_unfold: "sfilter = (\ p s. case s of x && xs \ If p\x then x && sfilter\p\xs else sfilter\p\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\\ = \" apply (rule ext_cfun) diff -r 02a52ae34b7a -r 7187373c6cb1 src/Pure/Isar/class.ML --- 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; - diff -r 02a52ae34b7a -r 7187373c6cb1 src/Pure/Isar/class_target.ML --- 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, diff -r 02a52ae34b7a -r 7187373c6cb1 src/Pure/Isar/locale.ML --- 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 = [];