--- a/src/HOL/Integration.thy Tue Jun 02 18:26:01 2009 +0200
+++ b/src/HOL/Integration.thy Tue Jun 02 18:26:12 2009 +0200
@@ -108,6 +108,86 @@
with `a \<le> b` show ?thesis by auto
qed
+lemma fine_covers_all:
+ assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
+ shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
+ using assms
+proof (induct set: fine)
+ case (2 b c D a t)
+ thus ?case
+ proof (cases "b < x")
+ case True
+ with 2 obtain N where *: "N < length D"
+ and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
+ hence "Suc N < length ((a,t,b)#D) \<and>
+ (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
+ thus ?thesis by auto
+ next
+ case False with 2
+ have "0 < length ((a,t,b)#D) \<and>
+ (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
+ thus ?thesis by auto
+ qed
+qed auto
+
+lemma fine_append_split:
+ assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
+ shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
+ and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
+proof -
+ from assms
+ have "?fine1 \<and> ?fine2"
+ proof (induct arbitrary: D1 D2)
+ case (2 b c D a' x D1 D2)
+ note induct = this
+
+ thus ?case
+ proof (cases D1)
+ case Nil
+ hence "fst (hd D2) = a'" using 2 by auto
+ with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct
+ show ?thesis by (auto intro: fine_Nil)
+ next
+ case (Cons d1 D1')
+ with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8)
+ have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
+ "d1 = (a', x, b)" by auto
+ with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
+ show ?thesis by auto
+ qed
+ qed auto
+ thus ?fine1 and ?fine2 by auto
+qed
+
+lemma fine_\<delta>_expand:
+ assumes "fine \<delta> (a,b) D"
+ and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x"
+ shows "fine \<delta>' (a,b) D"
+using assms proof induct
+ case 1 show ?case by (rule fine_Nil)
+next
+ case (2 b c D a x)
+ show ?case
+ proof (rule fine_Cons)
+ show "fine \<delta>' (b,c) D" using 2 by auto
+ from fine_imp_le[OF 2(1)] 2(6) `x \<le> b`
+ show "b - a < \<delta>' x"
+ using 2(7)[OF `a \<le> x`] by auto
+ qed (auto simp add: 2)
+qed
+
+lemma fine_single_boundaries:
+ assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
+ shows "a = d \<and> b = e"
+using assms proof induct
+ case (2 b c D a x)
+ hence "D = []" and "a = d" and "b = e" by auto
+ moreover
+ from `fine \<delta> (b,c) D` `D = []` have "b = c"
+ by (rule empty_fine_imp_eq)
+ ultimately show ?case by simp
+qed auto
+
subsection {* Riemann sum *}
@@ -133,6 +213,9 @@
lemma rsum_add: "rsum D (\<lambda>x. f x + g x) = rsum D f + rsum D g"
by (induct D, auto simp add: algebra_simps)
+lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
+unfolding rsum_def map_append listsum_append ..
+
subsection {* Gauge integrability (definite) *}
@@ -232,6 +315,144 @@
algebra_simps rsum_right_distrib)
done
+lemma Integral_add:
+ assumes "Integral (a, b) f x1"
+ assumes "Integral (b, c) f x2"
+ assumes "a \<le> b" and "b \<le> c"
+ shows "Integral (a, c) f (x1 + x2)"
+proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI)
+ fix \<epsilon> :: real assume "0 < \<epsilon>"
+ hence "0 < \<epsilon> / 2" by auto
+
+ assume "a < b \<and> b < c"
+ hence "a < b" and "b < c" by auto
+
+ from `Integral (a, b) f x1`[simplified Integral_def split_conv,
+ rule_format, OF `0 < \<epsilon>/2`]
+ obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
+ and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" by auto
+
+ from `Integral (b, c) f x2`[simplified Integral_def split_conv,
+ rule_format, OF `0 < \<epsilon>/2`]
+ obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
+ and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" by auto
+
+ def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
+ else if x = b then min (\<delta>1 b) (\<delta>2 b)
+ else min (\<delta>2 x) (x - b)"
+
+ have "gauge {a..c} \<delta>"
+ using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
+ moreover {
+ fix D :: "(real \<times> real \<times> real) list"
+ assume fine: "fine \<delta> (a,c) D"
+ from fine_covers_all[OF this `a < b` `b \<le> c`]
+ obtain N where "N < length D"
+ and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
+ by auto
+ obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
+ with * have "d < b" and "b \<le> e" by auto
+ have in_D: "(d, t, e) \<in> set D"
+ using D_eq[symmetric] using `N < length D` by auto
+
+ from mem_fine[OF fine in_D]
+ have "d < e" and "d \<le> t" and "t \<le> e" by auto
+
+ have "t = b"
+ proof (rule ccontr)
+ assume "t \<noteq> b"
+ with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def
+ show False by (cases "t < b") auto
+ qed
+
+ let ?D1 = "take N D"
+ let ?D2 = "drop N D"
+ def D1 \<equiv> "take N D @ [(d, t, b)]"
+ def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
+
+ have "D \<noteq> []" using `N < length D` by auto
+ from hd_drop_conv_nth[OF this `N < length D`]
+ have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
+ with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
+ have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
+ using `N < length D` fine by auto
+
+ have "fine \<delta>1 (a,b) D1" unfolding D1_def
+ proof (rule fine_append)
+ show "fine \<delta>1 (a, d) ?D1"
+ proof (rule fine1[THEN fine_\<delta>_expand])
+ fix x assume "a \<le> x" "x \<le> d"
+ hence "x \<le> b" using `d < b` `x \<le> d` by auto
+ thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
+ qed
+
+ have "b - d < \<delta>1 t"
+ using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto
+ from `d < b` `d \<le> t` `t = b` this
+ show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
+ qed
+ note rsum1 = I1[OF this]
+
+ have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
+ using nth_drop'[OF `N < length D`] by simp
+
+ have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
+ proof (cases "drop (Suc N) D = []")
+ case True
+ note * = fine2[simplified drop_split True D_eq append_Nil2]
+ have "e = c" using fine_single_boundaries[OF * refl] by auto
+ thus ?thesis unfolding True using fine_Nil by auto
+ next
+ case False
+ note * = fine_append_split[OF fine2 False drop_split]
+ from fine_single_boundaries[OF *(1)]
+ have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
+ with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
+ thus ?thesis
+ proof (rule fine_\<delta>_expand)
+ fix x assume "e \<le> x" and "x \<le> c"
+ thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto
+ qed
+ qed
+
+ have "fine \<delta>2 (b, c) D2"
+ proof (cases "e = b")
+ case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
+ next
+ case False
+ have "e - b < \<delta>2 b"
+ using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto
+ with False `t = b` `b \<le> e`
+ show ?thesis using D2_def
+ by (auto intro!: fine_append[OF _ fine2] fine_single
+ simp del: append_Cons)
+ qed
+ note rsum2 = I2[OF this]
+
+ have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
+ using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
+ also have "\<dots> = rsum D1 f + rsum D2 f"
+ by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
+ finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
+ using add_strict_mono[OF rsum1 rsum2] by simp
+ }
+ ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
+ (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
+ by blast
+next
+ case False
+ hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto
+ thus ?thesis
+ proof (rule disjE)
+ assume "a = b" hence "x1 = 0"
+ using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto
+ thus ?thesis using `a = b` `Integral (b, c) f x2` by auto
+ next
+ assume "b = c" hence "x2 = 0"
+ using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto
+ thus ?thesis using `b = c` `Integral (a, b) f x1` by auto
+ qed
+qed
text{*Fundamental theorem of calculus (Part I)*}
@@ -339,18 +560,6 @@
lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
by simp
-lemma Integral_add:
- "[| a \<le> b; b \<le> c; Integral(a,b) f' k1; Integral(b,c) f' k2;
- \<forall>x. a \<le> x & x \<le> c --> DERIV f x :> f' x |]
- ==> Integral(a,c) f' (k1 + k2)"
-apply (rule FTC1 [THEN Integral_subst], auto)
-apply (frule FTC1, auto)
-apply (frule_tac a = b in FTC1, auto)
-apply (drule_tac x = x in spec, auto)
-apply (drule_tac ?k2.0 = "f b - f a" in Integral_unique)
-apply (drule_tac [3] ?k2.0 = "f c - f b" in Integral_unique, auto)
-done
-
subsection {* Additivity Theorem of Gauge Integral *}
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Jun 02 18:26:01 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Jun 02 18:26:12 2009 +0200
@@ -329,7 +329,8 @@
lemma fps_const_add [simp]: "fps_const (c::'a\<Colon>monoid_add) + fps_const d = fps_const (c + d)"
by (simp add: fps_ext)
-
+lemma fps_const_sub [simp]: "fps_const (c::'a\<Colon>group_add) - fps_const d = fps_const (c - d)"
+ by (simp add: fps_ext)
lemma fps_const_mult[simp]: "fps_const (c::'a\<Colon>ring) * fps_const d = fps_const (c * d)"
by (simp add: fps_eq_iff fps_mult_nth setsum_0')
@@ -396,6 +397,18 @@
qed (rule number_of_fps_def)
end
+lemma number_of_fps_const: "(number_of k::('a::comm_ring_1) fps) = fps_const (of_int k)"
+
+proof(induct k rule: int_induct[where k=0])
+ case base thus ?case unfolding number_of_fps_def of_int_0 by simp
+next
+ case (step1 i) thus ?case unfolding number_of_fps_def
+ by (simp add: fps_const_add[symmetric] del: fps_const_add)
+next
+ case (step2 i) thus ?case unfolding number_of_fps_def
+ by (simp add: fps_const_sub[symmetric] del: fps_const_sub)
+qed
+
subsection{* Inverses of formal power series *}
declare setsum_cong[fundef_cong]
@@ -956,6 +969,9 @@
"fps_const (a::'a::{comm_ring_1}) oo b = fps_const (a)"
by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
+lemma number_of_compose[simp]: "(number_of k::('a::{comm_ring_1}) fps) oo b = number_of k"
+ unfolding number_of_fps_const by simp
+
lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: ('a :: comm_ring_1) fps)"
by (simp add: fps_eq_iff fps_compose_def mult_delta_left setsum_delta
power_Suc not_le)
@@ -2262,6 +2278,45 @@
show "?dia = inverse ?d" by simp
qed
+lemma fps_inv_idempotent:
+ assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0"
+ shows "fps_inv (fps_inv a) = a"
+proof-
+ let ?r = "fps_inv"
+ have ra0: "?r a $ 0 = 0" by (simp add: fps_inv_def)
+ from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_simps)
+ have X0: "X$0 = 0" by simp
+ from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" .
+ then have "?r (?r a) oo ?r a oo a = X oo a" by simp
+ then have "?r (?r a) oo (?r a oo a) = a"
+ unfolding X_fps_compose_startby0[OF a0]
+ unfolding fps_compose_assoc[OF a0 ra0, symmetric] .
+ then show ?thesis unfolding fps_inv[OF a0 a1] by simp
+qed
+
+lemma fps_ginv_ginv:
+ assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0"
+ and c0: "c$0 = 0" and c1: "c$1 \<noteq> 0"
+ shows "fps_ginv b (fps_ginv c a) = b oo a oo fps_inv c"
+proof-
+ let ?r = "fps_ginv"
+ from c0 have rca0: "?r c a $0 = 0" by (simp add: fps_ginv_def)
+ from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_simps)
+ from fps_ginv[OF rca0 rca1]
+ have "?r b (?r c a) oo ?r c a = b" .
+ then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp
+ then have "?r b (?r c a) oo (?r c a oo a) = b oo a"
+ apply (subst fps_compose_assoc)
+ using a0 c0 by (auto simp add: fps_ginv_def)
+ then have "?r b (?r c a) oo c = b oo a"
+ unfolding fps_ginv[OF a0 a1] .
+ then have "?r b (?r c a) oo c oo fps_inv c= b oo a oo fps_inv c" by simp
+ then have "?r b (?r c a) oo (c oo fps_inv c) = b oo a oo fps_inv c"
+ apply (subst fps_compose_assoc)
+ using a0 c0 by (auto simp add: fps_inv_def)
+ then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp
+qed
+
subsection{* Elementary series *}
subsubsection{* Exponential series *}
@@ -2330,7 +2385,6 @@
lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)"
by (induct n, auto simp add: power_Suc)
-
lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
by (simp add: fps_eq_iff X_fps_compose)
@@ -2348,10 +2402,9 @@
lemma fps_const_inverse:
- "inverse (fps_const (a::'a::{field, division_by_zero})) = fps_const (inverse a)"
+ "a \<noteq> 0 \<Longrightarrow> inverse (fps_const (a::'a::field)) = fps_const (inverse a)"
apply (auto simp add: fps_eq_iff fps_inverse_def) by (case_tac "n", auto)
-
lemma inverse_one_plus_X:
"inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field})^n)"
(is "inverse ?l = ?r")
@@ -2365,21 +2418,45 @@
lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
-subsubsection{* Logarithmic series *}
-definition "(L::'a::field_char_0 fps)
- = Abs_fps (\<lambda>n. (- 1) ^ Suc n / of_nat n)"
+lemma assumes r: "r (Suc k) 1 = 1"
+ shows "fps_radical r (Suc k) (E (c::'a::{field_char_0})) = E (c / of_nat (Suc k))"
+proof-
+ let ?ck = "(c / of_nat (Suc k))"
+ let ?r = "fps_radical r (Suc k)"
+ have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c"
+ by (simp_all del: of_nat_Suc)
+ have th0: "E ?ck ^ (Suc k) = E c" unfolding E_power_mult eq0 ..
+ have th: "r (Suc k) (E c $0) ^ Suc k = E c $ 0"
+ "r (Suc k) (E c $ 0) = E ?ck $ 0" "E c $ 0 \<noteq> 0" using r by simp_all
+ from th0 radical_unique[where r=r and k=k, OF th]
+ show ?thesis by auto
+qed
-lemma fps_deriv_L: "fps_deriv L = inverse (1 + X)"
- unfolding inverse_one_plus_X
- by (simp add: L_def fps_eq_iff power_Suc del: of_nat_Suc)
+lemma Ec_E1_eq:
+ "E (1::'a::{field_char_0}) oo (fps_const c * X) = E c"
+ apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
+ by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong)
+subsubsection{* Logarithmic series *}
-lemma L_nth: "L $ n = (- 1) ^ Suc n / of_nat n"
- by (simp add: L_def)
+lemma Abs_fps_if_0:
+ "Abs_fps(%n. if n=0 then (v::'a::ring_1) else f n) = fps_const v + X * Abs_fps (%n. f (Suc n))"
+ by (auto simp add: fps_eq_iff)
+
+definition L:: "'a::{field_char_0} \<Rightarrow> 'a fps" where
+ "L c \<equiv> fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
+lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)"
+ unfolding inverse_one_plus_X
+ by (simp add: L_def fps_eq_iff del: of_nat_Suc)
+
+lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
+ by (simp add: L_def field_simps)
+
+lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def)
lemma L_E_inv:
- assumes a: "a \<noteq> (0::'a::{field_char_0,division_by_zero})"
- shows "L = fps_const a * fps_inv (E a - 1)" (is "?l = ?r")
+ assumes a: "a\<noteq> (0::'a::{field_char_0})"
+ shows "L a = fps_inv (E a - 1)" (is "?l = ?r")
proof-
let ?b = "E a - 1"
have b0: "?b $ 0 = 0" by simp
@@ -2391,15 +2468,29 @@
finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" .
from fps_inv_deriv[OF b0 b1, unfolded eq]
have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
+ using a
by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult)
- hence "fps_deriv (fps_const a * fps_inv ?b) = inverse (X + 1)"
- using a by (simp add: fps_divide_def field_simps)
hence "fps_deriv ?l = fps_deriv ?r"
- by (simp add: fps_deriv_L add_commute)
+ by (simp add: fps_deriv_L add_commute fps_divide_def divide_inverse)
then show ?thesis unfolding fps_deriv_eq_iff
by (simp add: L_nth fps_inv_def)
qed
+lemma L_mult_add:
+ assumes c0: "c\<noteq>0" and d0: "d\<noteq>0"
+ shows "L c + L d = fps_const (c+d) * L (c*d)"
+ (is "?r = ?l")
+proof-
+ from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
+ have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
+ by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add)
+ also have "\<dots> = fps_deriv ?l"
+ apply (simp add: fps_deriv_L)
+ by (simp add: fps_eq_iff eq)
+ finally show ?thesis
+ unfolding fps_deriv_eq_iff by simp
+qed
+
subsubsection{* Formal trigonometric functions *}
definition "fps_sin (c::'a::field_char_0) =
--- a/src/HOL/List.thy Tue Jun 02 18:26:01 2009 +0200
+++ b/src/HOL/List.thy Tue Jun 02 18:26:12 2009 +0200
@@ -2464,6 +2464,12 @@
case False with d show ?thesis by auto
qed
+lemma distinct_concat:
+ assumes "distinct xs"
+ and "\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys"
+ and "\<And> ys zs. \<lbrakk> ys \<in> set xs ; zs \<in> set xs ; ys \<noteq> zs \<rbrakk> \<Longrightarrow> set ys \<inter> set zs = {}"
+ shows "distinct (concat xs)"
+ using assms by (induct xs) auto
text {* It is best to avoid this indexed version of distinct, but
sometimes it is useful. *}
@@ -2617,6 +2623,10 @@
lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
by (induct n) auto
+lemma map_replicate_const:
+ "map (\<lambda> x. k) lst = replicate (length lst) k"
+ by (induct lst) auto
+
lemma replicate_app_Cons_same:
"(replicate n x) @ (x # xs) = x # replicate n x @ xs"
by (induct n) auto
@@ -2696,6 +2706,9 @@
"map (\<lambda>i. x) [0..<i] = replicate i x"
by (induct i) (simp_all add: replicate_append_same)
+lemma concat_replicate_trivial[simp]:
+ "concat (replicate i []) = []"
+ by (induct i) (auto simp add: map_replicate_const)
lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
by (induct n) auto
--- a/src/HOL/Tools/atp_manager.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML Tue Jun 02 18:26:12 2009 +0200
@@ -81,9 +81,9 @@
fun ord ((a, _), (b, _)) = Time.compare (a, b);
);
-val lookup_thread = AList.lookup Thread.equal;
-val delete_thread = AList.delete Thread.equal;
-val update_thread = AList.update Thread.equal;
+fun lookup_thread xs = AList.lookup Thread.equal xs;
+fun delete_thread xs = AList.delete Thread.equal xs;
+fun update_thread xs = AList.update Thread.equal xs;
(* state of thread manager *)
@@ -104,6 +104,7 @@
val state = Synchronized.var "atp_manager"
(make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
+
(* unregister thread *)
fun unregister (success, message) thread = Synchronized.change state
--- a/src/HOL/Tools/atp_wrapper.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Tue Jun 02 18:26:12 2009 +0200
@@ -113,13 +113,13 @@
fun tptp_prover_opts max_new theory_const =
tptp_prover_opts_full max_new theory_const false;
-val tptp_prover = tptp_prover_opts 60 true;
+fun tptp_prover x = tptp_prover_opts 60 true x;
(*for structured proofs: prover must support TSTP*)
fun full_prover_opts max_new theory_const =
tptp_prover_opts_full max_new theory_const true;
-val full_prover = full_prover_opts 60 true;
+fun full_prover x = full_prover_opts 60 true x;
(* Vampire *)
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 02 18:26:12 2009 +0200
@@ -149,7 +149,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first_coeff = find_first_coeff []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
[@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -238,7 +238,7 @@
val dest_coeff = dest_coeff
val left_distrib = @{thm left_add_mult_distrib} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
@@ -263,7 +263,7 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps
numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -369,7 +369,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first_t []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
@@ -380,7 +380,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
);
structure LessCancelFactor = ExtractCommonTermFun
@@ -388,7 +388,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
);
structure LeCancelFactor = ExtractCommonTermFun
@@ -396,7 +396,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
);
structure DivideCancelFactor = ExtractCommonTermFun
@@ -404,7 +404,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
);
structure DvdCancelFactor = ExtractCommonTermFun
@@ -412,7 +412,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
);
val cancel_factor =
--- a/src/HOL/Tools/numeral_simprocs.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Tue Jun 02 18:26:12 2009 +0200
@@ -232,7 +232,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -310,7 +310,7 @@
val dest_coeff = dest_coeff 1
val left_distrib = @{thm combine_common_factor} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -336,7 +336,7 @@
val dest_coeff = dest_fcoeff 1
val left_distrib = @{thm combine_common_factor} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
fun norm_tac ss =
@@ -387,7 +387,7 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
@@ -533,7 +533,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first_t []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
@@ -545,7 +545,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
- val simp_conv = K (K (SOME @{thm mult_cancel_left}))
+ fun simp_conv _ _ = SOME @{thm mult_cancel_left}
);
(*for ordered rings*)
@@ -574,7 +574,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
- val simp_conv = K (K (SOME @{thm div_mult_mult1_if}))
+ fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
);
structure ModCancelFactor = ExtractCommonTermFun
@@ -582,7 +582,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod}
val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
- val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
+ fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
);
(*for idoms*)
@@ -591,7 +591,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
- val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
+ fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
);
(*Version for all fields, including unordered ones (type complex).*)
@@ -600,7 +600,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
- val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
+ fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
);
val cancel_factors =
--- a/src/Pure/General/secure.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/General/secure.ML Tue Jun 02 18:26:12 2009 +0200
@@ -9,6 +9,7 @@
val set_secure: unit -> unit
val is_secure: unit -> bool
val deny_secure: string -> unit
+ val secure_mltext: unit -> unit
val use_text: use_context -> int * string -> bool -> string -> unit
val use_file: use_context -> bool -> string -> unit
val toplevel_pp: string list -> string -> unit
--- a/src/Pure/IsaMakefile Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/IsaMakefile Tue Jun 02 18:26:12 2009 +0200
@@ -55,19 +55,20 @@
General/table.ML General/url.ML General/xml.ML General/yxml.ML \
Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
- Isar/constdefs.ML Isar/context_rules.ML \
- Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \
- Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \
- Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
- Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \
- Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
- Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
- Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
- Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \
- Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
- Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
- ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
- ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
+ Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
+ Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
+ Isar/local_theory.ML Isar/locale.ML Isar/method.ML \
+ Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
+ Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
+ Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
+ Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
+ Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML \
+ Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
+ Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML \
+ ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
+ ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
+ ML-Systems/install_pp_polyml.ML \
ML-Systems/install_pp_polyml-experimental.ML \
ML-Systems/use_context.ML Proof/extraction.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
--- a/src/Pure/Isar/ROOT.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/Isar/ROOT.ML Tue Jun 02 18:26:12 2009 +0200
@@ -24,6 +24,13 @@
use "outer_parse.ML";
use "value_parse.ML";
use "args.ML";
+
+(*ML support*)
+use "../ML/ml_syntax.ML";
+use "../ML/ml_env.ML";
+if ml_system = "polyml-experimental"
+then use "../ML/ml_compiler_polyml-5.3.ML"
+else use "../ML/ml_compiler.ML";
use "../ML/ml_context.ML";
(*theory sources*)
--- a/src/Pure/Isar/attrib.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Jun 02 18:26:12 2009 +0200
@@ -240,8 +240,7 @@
(* rename_abs *)
-val rename_abs : (Context.generic * thm -> Context.generic * thm) parser =
- Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars');
+fun rename_abs x = (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')) x;
(* unfold / fold definitions *)
--- a/src/Pure/Isar/isar_syn.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Jun 02 18:26:12 2009 +0200
@@ -296,11 +296,11 @@
(* use ML text *)
fun propagate_env (context as Context.Proof lthy) =
- Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+ Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
| propagate_env context = context;
fun propagate_env_prf prf = Proof.map_contexts
- (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
+ (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
val _ =
OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Jun 02 18:26:12 2009 +0200
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/compiler_polyml-5.0.ML
-Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1.
+Runtime compilation for Poly/ML 5.0 and 5.1.
*)
fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
--- a/src/Pure/ML-Systems/polyml_common.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML Tue Jun 02 18:26:12 2009 +0200
@@ -17,6 +17,8 @@
val forget_structure = PolyML.Compiler.forgetStructure;
+val _ = PolyML.Compiler.forgetValue "print";
+
(* Compiler options *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_compiler.ML Tue Jun 02 18:26:12 2009 +0200
@@ -0,0 +1,23 @@
+(* Title: Pure/ML/ml_compiler.ML
+ Author: Makarius
+
+Runtime compilation -- generic version.
+*)
+
+signature ML_COMPILER =
+sig
+ val eval: bool -> Position.T -> ML_Lex.token list -> unit
+end
+
+structure ML_Compiler: ML_COMPILER =
+struct
+
+fun eval verbose pos toks =
+ let
+ val line = the_default 1 (Position.line_of pos);
+ val file = the_default "ML" (Position.file_of pos);
+ val text = ML_Lex.flatten toks;
+ in Secure.use_text ML_Env.local_context (line, file) verbose text end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Jun 02 18:26:12 2009 +0200
@@ -0,0 +1,144 @@
+(* Title: Pure/ML/ml_compiler_polyml-5.3.ML
+ Author: Makarius
+
+Advanced runtime compilation for Poly/ML 5.3 (SVN 762).
+*)
+
+signature ML_COMPILER =
+sig
+ val eval: bool -> Position.T -> ML_Lex.token list -> unit
+end
+
+structure ML_Compiler: ML_COMPILER =
+struct
+
+(* original source positions *)
+
+fun position_of (SOME context) (loc: PolyML.location) =
+ (case pairself (ML_Env.token_position context) (#startPosition loc, #endPosition loc) of
+ (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
+ | (SOME pos, NONE) => pos
+ | _ => Position.line_file (#startLine loc) (#file loc))
+ | position_of NONE (loc: PolyML.location) = Position.line_file (#startLine loc) (#file loc);
+
+
+(* parse trees *)
+
+fun report_parse_tree context depth space =
+ let
+ val pos_of = position_of context;
+ fun report loc (PolyML.PTtype types) =
+ PolyML.NameSpace.displayTypeExpression (types, depth, space)
+ |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+ |> Position.report_text Markup.ML_typing (pos_of loc)
+ | report loc (PolyML.PTdeclaredAt decl) =
+ Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
+ |> Position.report_text Markup.ML_ref (pos_of loc)
+ | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
+ | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
+ | report _ _ = ()
+ and report_tree (loc, props) = List.app (report loc) props;
+ in report_tree end;
+
+
+(* eval ML source tokens *)
+
+fun eval verbose pos toks =
+ let
+ val _ = Secure.secure_mltext ();
+ val {name_space = space, print, error = err, ...} = ML_Env.local_context;
+
+
+ (* input *)
+
+ val input =
+ if is_none (Context.thread_data ()) then map (pair 0) toks
+ else Context.>>> (ML_Env.register_tokens toks);
+ val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
+
+ val current_line = ref (the_default 1 (Position.line_of pos));
+
+ fun get_index () =
+ the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
+
+ fun get () =
+ (case ! input_buffer of
+ [] => NONE
+ | (_, []) :: rest => (input_buffer := rest; get ())
+ | (i, c :: cs) :: rest =>
+ (input_buffer := (i, cs) :: rest;
+ if c = #"\n" then current_line := ! current_line + 1 else ();
+ SOME c));
+
+
+ (* output *)
+
+ val output_buffer = ref Buffer.empty;
+ fun output () = Buffer.content (! output_buffer);
+ fun put s = change output_buffer (Buffer.add s);
+
+ fun put_message {message, hard, location, context = _} =
+ (put (if hard then "Error: " else "Warning: ");
+ put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
+ put (Position.str_of (position_of (Context.thread_data ()) location) ^ "\n"));
+
+
+ (* results *)
+
+ val depth = get_print_depth ();
+
+ fun apply_result {fixes, types, signatures, structures, functors, values} =
+ let
+ fun display disp x =
+ if depth > 0 then
+ (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
+ else ();
+
+ fun apply_fix (a, b) =
+ (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
+ fun apply_type (a, b) =
+ (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
+ fun apply_sig (a, b) =
+ (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
+ fun apply_struct (a, b) =
+ (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
+ fun apply_funct (a, b) =
+ (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
+ fun apply_val (a, b) =
+ (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
+ in
+ List.app apply_fix fixes;
+ List.app apply_type types;
+ List.app apply_sig signatures;
+ List.app apply_struct structures;
+ List.app apply_funct functors;
+ List.app apply_val values
+ end;
+
+ fun result_fun (phase1, phase2) () =
+ (case phase1 of NONE => ()
+ | SOME parse_tree => report_parse_tree (Context.thread_data ()) depth space parse_tree;
+ case phase2 of NONE => err "Static Errors"
+ | SOME code => apply_result (code ())); (* FIXME Toplevel.program *)
+
+
+ (* compiler invocation *)
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPNameSpace space,
+ PolyML.Compiler.CPErrorMessageProc put_message,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
+ PolyML.Compiler.CPLineOffset get_index,
+ PolyML.Compiler.CPCompilerResultFun result_fun];
+ val _ =
+ (while not (List.null (! input_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ err (output ()); raise exn);
+ in if verbose then print (output ()) else () end;
+
+end;
+
--- a/src/Pure/ML/ml_context.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/ML/ml_context.ML Tue Jun 02 18:26:12 2009 +0200
@@ -19,9 +19,6 @@
val the_global_context: unit -> theory
val the_local_context: unit -> Proof.context
val exec: (unit -> unit) -> Context.generic -> Context.generic
- val inherit_env: Context.generic -> Context.generic -> Context.generic
- val name_space: ML_Name_Space.T
- val local_context: use_context
val stored_thms: thm list ref
val ml_store_thm: string * thm -> unit
val ml_store_thms: string * thm list -> unit
@@ -54,78 +51,6 @@
| NONE => error "Missing context after execution");
-(* ML name space *)
-
-structure ML_Env = GenericDataFun
-(
- type T =
- ML_Name_Space.valueVal Symtab.table *
- ML_Name_Space.typeVal Symtab.table *
- ML_Name_Space.fixityVal Symtab.table *
- ML_Name_Space.structureVal Symtab.table *
- ML_Name_Space.signatureVal Symtab.table *
- ML_Name_Space.functorVal Symtab.table;
- val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
- val extend = I;
- fun merge _
- ((val1, type1, fixity1, structure1, signature1, functor1),
- (val2, type2, fixity2, structure2, signature2, functor2)) : T =
- (Symtab.merge (K true) (val1, val2),
- Symtab.merge (K true) (type1, type2),
- Symtab.merge (K true) (fixity1, fixity2),
- Symtab.merge (K true) (structure1, structure2),
- Symtab.merge (K true) (signature1, signature2),
- Symtab.merge (K true) (functor1, functor2));
-);
-
-val inherit_env = ML_Env.put o ML_Env.get;
-
-val name_space: ML_Name_Space.T =
- let
- fun lookup sel1 sel2 name =
- Context.thread_data ()
- |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (ML_Env.get context)) name)
- |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
-
- fun all sel1 sel2 () =
- Context.thread_data ()
- |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (ML_Env.get context)))
- |> append (sel2 ML_Name_Space.global ())
- |> sort_distinct (string_ord o pairself #1);
-
- fun enter ap1 sel2 entry =
- if is_some (Context.thread_data ()) then
- Context.>> (ML_Env.map (ap1 (Symtab.update entry)))
- else sel2 ML_Name_Space.global entry;
- in
- {lookupVal = lookup #1 #lookupVal,
- lookupType = lookup #2 #lookupType,
- lookupFix = lookup #3 #lookupFix,
- lookupStruct = lookup #4 #lookupStruct,
- lookupSig = lookup #5 #lookupSig,
- lookupFunct = lookup #6 #lookupFunct,
- enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
- enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
- enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
- enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
- enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
- enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
- allVal = all #1 #allVal,
- allType = all #2 #allType,
- allFix = all #3 #allFix,
- allStruct = all #4 #allStruct,
- allSig = all #5 #allSig,
- allFunct = all #6 #allFunct}
- end;
-
-val local_context: use_context =
- {tune_source = ML_Parse.fix_ints,
- name_space = name_space,
- str_of_pos = Position.str_of oo Position.line_file,
- print = writeln,
- error = error};
-
-
(* theorem bindings *)
val stored_thms: thm list ref = ref [];
@@ -139,8 +64,8 @@
else if not (ML_Syntax.is_identifier name) then
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
else setmp stored_thms ths' (fn () =>
- use_text local_context (0, "") true
- ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) ();
+ ML_Compiler.eval true Position.none
+ (ML_Lex.tokenize ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);"))) ();
in () end;
val ml_store_thms = ml_store "";
@@ -199,6 +124,7 @@
val struct_name = "Isabelle";
val begin_env = ML_Lex.tokenize ("structure " ^ struct_name ^ " =\nstruct\n");
val end_env = ML_Lex.tokenize "end;";
+val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
in
@@ -240,26 +166,21 @@
fun eval verbose pos txt =
let
- fun eval_raw p = use_text local_context
- (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p));
-
(*prepare source text*)
val _ = Position.report Markup.ML_source pos;
val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
- val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ())
- |>> pairself (implode o map ML_Lex.text_of);
- val _ = if ! trace then tracing (cat_lines [env, body]) else ();
+ val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
+ val _ =
+ if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
+ else ();
(*prepare static ML environment*)
val _ = Context.setmp_thread_data env_ctxt
- (fn () => (eval_raw Position.none false env; Context.thread_data ())) ()
- |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
+ (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) ()
+ |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
- (*eval ML*)
- val _ = eval_raw pos verbose body;
-
- (*reset static ML environment*)
- val _ = eval_raw Position.none false "structure Isabelle = struct end";
+ val _ = ML_Compiler.eval verbose pos body;
+ val _ = ML_Compiler.eval false Position.none reset_env;
in () end;
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_env.ML Tue Jun 02 18:26:12 2009 +0200
@@ -0,0 +1,111 @@
+(* Title: Pure/ML/ml_env.ML
+ Author: Makarius
+
+Local environment of ML sources and results.
+*)
+
+signature ML_ENV =
+sig
+ val inherit: Context.generic -> Context.generic -> Context.generic
+ val register_tokens: ML_Lex.token list -> Context.generic ->
+ (serial * ML_Lex.token) list * Context.generic
+ val token_position: Context.generic -> serial -> Position.T option
+ val name_space: ML_Name_Space.T
+ val local_context: use_context
+end
+
+structure ML_Env: ML_ENV =
+struct
+
+(* context data *)
+
+structure Env = GenericDataFun
+(
+ type T =
+ Position.T Inttab.table *
+ (ML_Name_Space.valueVal Symtab.table *
+ ML_Name_Space.typeVal Symtab.table *
+ ML_Name_Space.fixityVal Symtab.table *
+ ML_Name_Space.structureVal Symtab.table *
+ ML_Name_Space.signatureVal Symtab.table *
+ ML_Name_Space.functorVal Symtab.table);
+ val empty =
+ (Inttab.empty,
+ (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
+ val extend = I;
+ fun merge _
+ ((toks1, (val1, type1, fixity1, structure1, signature1, functor1)),
+ (toks2, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
+ (Inttab.merge (K true) (toks1, toks2),
+ (Symtab.merge (K true) (val1, val2),
+ Symtab.merge (K true) (type1, type2),
+ Symtab.merge (K true) (fixity1, fixity2),
+ Symtab.merge (K true) (structure1, structure2),
+ Symtab.merge (K true) (signature1, signature2),
+ Symtab.merge (K true) (functor1, functor2)));
+);
+
+val inherit = Env.put o Env.get;
+
+
+(* source tokens *)
+
+fun register_tokens toks context =
+ let
+ val regs = map (fn tok => (serial (), tok)) toks;
+ val context' = context
+ |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs));
+ in (regs, context') end;
+
+val token_position = Inttab.lookup o #1 o Env.get;
+
+
+(* results *)
+
+val name_space: ML_Name_Space.T =
+ let
+ fun lookup sel1 sel2 name =
+ Context.thread_data ()
+ |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
+ |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
+
+ fun all sel1 sel2 () =
+ Context.thread_data ()
+ |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
+ |> append (sel2 ML_Name_Space.global ())
+ |> sort_distinct (string_ord o pairself #1);
+
+ fun enter ap1 sel2 entry =
+ if is_some (Context.thread_data ()) then
+ Context.>> (Env.map (apsnd (ap1 (Symtab.update entry))))
+ else sel2 ML_Name_Space.global entry;
+ in
+ {lookupVal = lookup #1 #lookupVal,
+ lookupType = lookup #2 #lookupType,
+ lookupFix = lookup #3 #lookupFix,
+ lookupStruct = lookup #4 #lookupStruct,
+ lookupSig = lookup #5 #lookupSig,
+ lookupFunct = lookup #6 #lookupFunct,
+ enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
+ enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
+ enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
+ enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
+ enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
+ enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
+ allVal = all #1 #allVal,
+ allType = all #2 #allType,
+ allFix = all #3 #allFix,
+ allStruct = all #4 #allStruct,
+ allSig = all #5 #allSig,
+ allFunct = all #6 #allFunct}
+ end;
+
+val local_context: use_context =
+ {tune_source = ML_Parse.fix_ints,
+ name_space = name_space,
+ str_of_pos = Position.str_of oo Position.line_file,
+ print = writeln,
+ error = error};
+
+end;
+
--- a/src/Pure/ML/ml_lex.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/ML/ml_lex.ML Tue Jun 02 18:26:12 2009 +0200
@@ -18,6 +18,7 @@
val kind_of: token -> token_kind
val content_of: token -> string
val text_of: token -> string
+ val flatten: token list -> string
val report_token: token -> unit
val keywords: string list
val source: (Symbol.symbol, 'a) Source.source ->
@@ -73,6 +74,8 @@
Error msg => error msg
| _ => Symbol.escape (content_of tok));
+val flatten = implode o map text_of;
+
fun is_regular (Token (_, (Error _, _))) = false
| is_regular (Token (_, (EOF, _))) = false
| is_regular _ = true;
--- a/src/Pure/ML/ml_test.ML Tue Jun 02 18:26:01 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-(* Title: Pure/ML/ml_test.ML
- Author: Makarius
-
-Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 744).
-*)
-
-signature ML_TEST =
-sig
- val position_of: Proof.context -> PolyML.location -> Position.T
- val eval: bool -> Position.T -> ML_Lex.token list -> unit
-end
-
-structure ML_Test: ML_TEST =
-struct
-
-(* extra ML environment *)
-
-structure Extra_Env = GenericDataFun
-(
- type T = Position.T Inttab.table; (*position of registered tokens*)
- val empty = Inttab.empty;
- val extend = I;
- fun merge _ = Inttab.merge (K true);
-);
-
-fun inherit_env context =
- ML_Context.inherit_env context #>
- Extra_Env.put (Extra_Env.get context);
-
-fun register_tokens toks context =
- let
- val regs = map (fn tok => (serial (), tok)) toks;
- val context' = context
- |> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs);
- in (regs, context') end;
-
-fun position_of ctxt
- ({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) =
- (case pairself (Inttab.lookup (Extra_Env.get (Context.Proof ctxt))) (i, j) of
- (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
- | (SOME pos, NONE) => pos
- | _ => Position.line_file line file);
-
-
-(* parse trees *)
-
-fun report_parse_tree context depth space =
- let
- val pos_of = position_of (Context.proof_of context);
- fun report loc (PolyML.PTtype types) =
- PolyML.NameSpace.displayTypeExpression (types, depth, space)
- |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> Position.report_text Markup.ML_typing (pos_of loc)
- | report loc (PolyML.PTdeclaredAt decl) =
- Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
- |> Position.report_text Markup.ML_ref (pos_of loc)
- | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
- | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
- | report _ _ = ()
- and report_tree (loc, props) = List.app (report loc) props;
- in report_tree end;
-
-
-(* eval ML source tokens *)
-
-fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks =
- let
- (* input *)
-
- val input = Context.>>> (register_tokens toks);
- val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
-
- val current_line = ref (the_default 1 (Position.line_of pos));
-
- fun get_index () =
- the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
-
- fun get () =
- (case ! input_buffer of
- [] => NONE
- | (_, []) :: rest => (input_buffer := rest; get ())
- | (i, c :: cs) :: rest =>
- (input_buffer := (i, cs) :: rest;
- if c = #"\n" then current_line := ! current_line + 1 else ();
- SOME c));
-
-
- (* output *)
-
- val output_buffer = ref Buffer.empty;
- fun output () = Buffer.content (! output_buffer);
- fun put s = change output_buffer (Buffer.add s);
-
- fun put_message {message, hard, location, context = _} =
- (put (if hard then "Error: " else "Warning: ");
- put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
- put (Position.str_of
- (position_of (Context.proof_of (the (Context.thread_data ()))) location) ^ "\n"));
-
-
- (* results *)
-
- val depth = get_print_depth ();
-
- fun apply_result {fixes, types, signatures, structures, functors, values} =
- let
- fun display disp x =
- if depth > 0 then
- (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
- else ();
-
- fun apply_fix (a, b) =
- (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
- fun apply_type (a, b) =
- (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
- fun apply_sig (a, b) =
- (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
- fun apply_struct (a, b) =
- (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
- fun apply_funct (a, b) =
- (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
- fun apply_val (a, b) =
- (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
- in
- List.app apply_fix fixes;
- List.app apply_type types;
- List.app apply_sig signatures;
- List.app apply_struct structures;
- List.app apply_funct functors;
- List.app apply_val values
- end;
-
- fun result_fun (phase1, phase2) () =
- (case phase1 of NONE => ()
- | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth space parse_tree;
- case phase2 of NONE => error "Static Errors"
- | SOME code => apply_result (Toplevel.program code));
-
-
- (* compiler invocation *)
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPNameSpace space,
- PolyML.Compiler.CPErrorMessageProc put_message,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
- PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
- PolyML.Compiler.CPLineOffset get_index,
- PolyML.Compiler.CPCompilerResultFun result_fun];
- val _ =
- (while not (List.null (! input_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
- in if verbose then print (output ()) else () end;
-
-val eval = use_text ML_Context.local_context;
-
-
-(* ML test command *)
-
-fun ML_test (txt, pos) =
- let
- val _ = Position.report Markup.ML_source pos;
- val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
- val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
-
- val _ = Context.setmp_thread_data env_ctxt
- (fn () => (eval false Position.none env; Context.thread_data ())) ()
- |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
- val _ = eval true pos body;
- val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
- in () end;
-
-
-local structure P = OuterParse and K = OuterKeyword in
-
-fun propagate_env (context as Context.Proof lthy) =
- Context.Proof (LocalTheory.map_contexts (inherit_env context) lthy)
- | propagate_env context = context;
-
-val _ =
- OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
- (P.ML_source >> (fn src =>
- Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> propagate_env)));
-
-end;
-
-end;
-
--- a/src/Pure/ROOT.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Pure/ROOT.ML Tue Jun 02 18:26:12 2009 +0200
@@ -46,7 +46,6 @@
use "Syntax/syntax.ML";
use "type_infer.ML";
-use "ML/ml_syntax.ML";
(*core of tactical proof system*)
use "net.ML";
@@ -98,6 +97,5 @@
(*configuration for Proof General*)
cd "ProofGeneral"; use "ROOT.ML"; cd "..";
-if ml_system = "polyml-experimental" then use "ML/ml_test.ML" else ();
use "pure_setup.ML";
--- a/src/Tools/Compute_Oracle/am_compiler.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_compiler.ML Tue Jun 02 18:26:12 2009 +0200
@@ -185,7 +185,7 @@
in
compiled_rewriter := NONE;
- use_text ML_Context.local_context (1, "") false (!buffer);
+ use_text ML_Env.local_context (1, "") false (!buffer);
case !compiled_rewriter of
NONE => raise (Compile "cannot communicate with compiled function")
| SOME r => (compiled_rewriter := NONE; r)
--- a/src/Tools/Compute_Oracle/am_sml.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_sml.ML Tue Jun 02 18:26:12 2009 +0200
@@ -492,7 +492,7 @@
fun writeTextFile name s = File.write (Path.explode name) s
-fun use_source src = use_text ML_Context.local_context (1, "") false src
+fun use_source src = use_text ML_Env.local_context (1, "") false src
fun compile cache_patterns const_arity eqs =
let
--- a/src/Tools/code/code_ml.ML Tue Jun 02 18:26:01 2009 +0200
+++ b/src/Tools/code/code_ml.ML Tue Jun 02 18:26:12 2009 +0200
@@ -1082,7 +1082,7 @@
fun isar_seri_sml module_name =
Code_Target.parse_args (Scan.succeed ())
#> (fn () => serialize_ml target_SML
- (SOME (use_text ML_Context.local_context (1, "generated code") false))
+ (SOME (use_text ML_Env.local_context (1, "generated code") false))
pr_sml_module pr_sml_stmt module_name);
fun isar_seri_ocaml module_name =