--- a/etc/isabelle.css Fri Aug 10 13:33:54 2012 +0200
+++ b/etc/isabelle.css Fri Aug 10 16:29:40 2012 +0200
@@ -42,7 +42,5 @@
.verbatim { color: #00008B; }
.comment { color: #8B0000; }
.control { background-color: #FF6A6A; }
-.malformed { background-color: #FF6A6A; }
+.bad { background-color: #FF6A6A; }
-.malformed_span { background-color: #FF6A6A; }
-
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Aug 10 13:33:54 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Aug 10 16:29:40 2012 +0200
@@ -26,7 +26,8 @@
lemma fps_nth_Abs_fps [simp]: "Abs_fps f $ n = f n"
by (simp add: Abs_fps_inverse)
-text{* Definition of the basic elements 0 and 1 and the basic operations of addition, negation and multiplication *}
+text{* Definition of the basic elements 0 and 1 and the basic operations of addition,
+ negation and multiplication *}
instantiation fps :: (zero) zero
begin
@@ -335,10 +336,12 @@
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')
-lemma fps_const_add_left: "fps_const (c::'a\<Colon>monoid_add) + f = Abs_fps (\<lambda>n. if n = 0 then c + f$0 else f$n)"
+lemma fps_const_add_left: "fps_const (c::'a\<Colon>monoid_add) + f =
+ Abs_fps (\<lambda>n. if n = 0 then c + f$0 else f$n)"
by (simp add: fps_ext)
-lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) = Abs_fps (\<lambda>n. if n = 0 then f$0 + c else f$n)"
+lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) =
+ Abs_fps (\<lambda>n. if n = 0 then f$0 + c else f$n)"
by (simp add: fps_ext)
lemma fps_const_mult_left: "fps_const (c::'a\<Colon>semiring_0) * f = Abs_fps (\<lambda>n. c * f$n)"
@@ -393,7 +396,7 @@
instance fps :: (idom) idom ..
lemma numeral_fps_const: "numeral k = fps_const (numeral k)"
- by (induct k, simp_all only: numeral.simps fps_const_1_eq_1
+ by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1
fps_const_add [symmetric])
lemma neg_numeral_fps_const: "neg_numeral k = fps_const (neg_numeral k)"
@@ -402,7 +405,7 @@
subsection{* The eXtractor series X*}
lemma minus_one_power_iff: "(- (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else - 1)"
- by (induct n, auto)
+ by (induct n) auto
definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
@@ -417,7 +420,8 @@
ultimately show ?thesis by blast
qed
-lemma X_mult_right_nth[simp]: "((f :: ('a::comm_semiring_1) fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
+lemma X_mult_right_nth[simp]:
+ "((f :: ('a::comm_semiring_1) fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
by (metis X_mult_nth mult_commute)
lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)"
@@ -433,13 +437,17 @@
then show ?case by (simp add: fps_eq_iff)
qed
-lemma X_power_mult_nth: "(X^k * (f :: ('a::comm_ring_1) fps)) $n = (if n < k then 0 else f $ (n - k))"
+lemma X_power_mult_nth:
+ "(X^k * (f :: ('a::comm_ring_1) fps)) $n = (if n < k then 0 else f $ (n - k))"
apply (induct k arbitrary: n)
apply (simp)
unfolding power_Suc mult_assoc
- by (case_tac n, auto)
-
-lemma X_power_mult_right_nth: "((f :: ('a::comm_ring_1) fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
+ apply (case_tac n)
+ apply auto
+ done
+
+lemma X_power_mult_right_nth:
+ "((f :: ('a::comm_ring_1) fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
by (metis X_power_mult_nth mult_commute)
@@ -448,10 +456,12 @@
subsection{* Formal Power series form a metric space *}
definition (in dist) ball_def: "ball x r = {y. dist y x < r}"
+
instantiation fps :: (comm_ring_1) dist
begin
-definition dist_fps_def: "dist (a::'a fps) b = (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)"
+definition dist_fps_def:
+ "dist (a::'a fps) b = (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)"
lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
by (simp add: dist_fps_def)
@@ -460,8 +470,11 @@
apply (auto simp add: dist_fps_def)
apply (rule cong[OF refl, where x="(\<lambda>n\<Colon>nat. a $ n \<noteq> b $ n)"])
apply (rule ext)
- by auto
+ apply auto
+ done
+
instance ..
+
end
lemma fps_nonzero_least_unique: assumes a0: "a \<noteq> 0"
@@ -481,10 +494,11 @@
ultimately show ?thesis by blast
qed
-lemma fps_eq_least_unique: assumes ab: "(a::('a::ab_group_add) fps) \<noteq> b"
+lemma fps_eq_least_unique:
+ assumes ab: "(a::('a::ab_group_add) fps) \<noteq> b"
shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> b$n) n"
-using fps_nonzero_least_unique[of "a - b"] ab
-by auto
+ using fps_nonzero_least_unique[of "a - b"] ab
+ by auto
instantiation fps :: (comm_ring_1) metric_space
begin
@@ -497,25 +511,36 @@
show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
by (auto simp add: open_fps_def ball_def subset_eq)
next
-{ fix a b :: "'a fps"
- {assume ab: "a = b"
- then have "\<not> (\<exists>n. a$n \<noteq> b$n)" by simp
- then have "dist a b = 0" by (simp add: dist_fps_def)}
- moreover
- {assume d: "dist a b = 0"
- then have "\<forall>n. a$n = b$n"
- by - (rule ccontr, simp add: dist_fps_def)
- then have "a = b" by (simp add: fps_eq_iff)}
- ultimately show "dist a b =0 \<longleftrightarrow> a = b" by blast}
-note th = this
-from th have th'[simp]: "\<And>a::'a fps. dist a a = 0" by simp
+ {
+ fix a b :: "'a fps"
+ {
+ assume ab: "a = b"
+ then have "\<not> (\<exists>n. a$n \<noteq> b$n)" by simp
+ then have "dist a b = 0" by (simp add: dist_fps_def)
+ }
+ moreover
+ {
+ assume d: "dist a b = 0"
+ then have "\<forall>n. a$n = b$n"
+ by - (rule ccontr, simp add: dist_fps_def)
+ then have "a = b" by (simp add: fps_eq_iff)
+ }
+ ultimately show "dist a b =0 \<longleftrightarrow> a = b" by blast
+ }
+ note th = this
+ from th have th'[simp]: "\<And>a::'a fps. dist a a = 0" by simp
fix a b c :: "'a fps"
- {assume ab: "a = b" then have d0: "dist a b = 0" unfolding th .
+ {
+ assume ab: "a = b" then have d0: "dist a b = 0" unfolding th .
then have "dist a b \<le> dist a c + dist b c"
- using dist_fps_ge0[of a c] dist_fps_ge0[of b c] by simp}
+ using dist_fps_ge0[of a c] dist_fps_ge0[of b c] by simp
+ }
moreover
- {assume c: "c = a \<or> c = b" then have "dist a b \<le> dist a c + dist b c"
- by (cases "c=a", simp_all add: th dist_fps_sym) }
+ {
+ assume c: "c = a \<or> c = b"
+ then have "dist a b \<le> dist a c + dist b c"
+ by (cases "c=a") (simp_all add: th dist_fps_sym)
+ }
moreover
{assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c"
let ?P = "\<lambda>a b n. a$n \<noteq> b$n"
@@ -591,9 +616,12 @@
by (simp add: X_power_iff)
-lemma fps_sum_rep_nth: "(setsum (%i. fps_const(a$i)*X^i) {0..m})$n = (if n \<le> m then a$n else (0::'a::comm_ring_1))"
- apply (auto simp add: fps_eq_iff fps_setsum_nth X_power_nth cond_application_beta cond_value_iff cong del: if_weak_cong)
- by (simp add: setsum_delta')
+lemma fps_sum_rep_nth: "(setsum (%i. fps_const(a$i)*X^i) {0..m})$n =
+ (if n \<le> m then a$n else (0::'a::comm_ring_1))"
+ apply (auto simp add: fps_eq_iff fps_setsum_nth X_power_nth cond_application_beta cond_value_iff
+ cong del: if_weak_cong)
+ apply (simp add: setsum_delta')
+ done
lemma fps_notation:
"(%n. setsum (%i. fps_const(a$i) * X^i) {0..n}) ----> a" (is "?s ----> a")
@@ -702,7 +730,8 @@
ultimately show ?thesis by blast
qed
-lemma fps_inverse_idempotent[intro]: assumes f0: "f$0 \<noteq> (0::'a::field)"
+lemma fps_inverse_idempotent[intro]:
+ assumes f0: "f$0 \<noteq> (0::'a::field)"
shows "inverse (inverse f) = f"
proof-
from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp
@@ -711,7 +740,8 @@
then show ?thesis using f0 unfolding mult_cancel_left by simp
qed
-lemma fps_inverse_unique: assumes f0: "f$0 \<noteq> (0::'a::field)" and fg: "f*g = 1"
+lemma fps_inverse_unique:
+ assumes f0: "f$0 \<noteq> (0::'a::field)" and fg: "f*g = 1"
shows "inverse f = g"
proof-
from inverse_mult_eq_1[OF f0] fg
@@ -748,9 +778,12 @@
definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))"
-lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)" by (simp add: fps_deriv_def)
-
-lemma fps_deriv_linear[simp]: "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_deriv f + fps_const b * fps_deriv g"
+lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)"
+ by (simp add: fps_deriv_def)
+
+lemma fps_deriv_linear[simp]:
+ "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) =
+ fps_const a * fps_deriv f + fps_const b * fps_deriv g"
unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: field_simps)
lemma fps_deriv_mult[simp]:
@@ -821,7 +854,8 @@
lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
by (simp add: fps_ext fps_deriv_def fps_const_def)
-lemma fps_deriv_mult_const_left[simp]: "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
+lemma fps_deriv_mult_const_left[simp]:
+ "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
by simp
lemma fps_deriv_0[simp]: "fps_deriv 0 = 0"
@@ -830,19 +864,24 @@
lemma fps_deriv_1[simp]: "fps_deriv 1 = 0"
by (simp add: fps_deriv_def fps_eq_iff )
-lemma fps_deriv_mult_const_right[simp]: "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
+lemma fps_deriv_mult_const_right[simp]:
+ "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
by simp
-lemma fps_deriv_setsum: "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S"
+lemma fps_deriv_setsum:
+ "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S"
proof-
- {assume "\<not> finite S" hence ?thesis by simp}
+ { assume "\<not> finite S" hence ?thesis by simp }
moreover
- {assume fS: "finite S"
- have ?thesis by (induct rule: finite_induct[OF fS], simp_all)}
+ {
+ assume fS: "finite S"
+ have ?thesis by (induct rule: finite_induct[OF fS]) simp_all
+ }
ultimately show ?thesis by blast
qed
-lemma fps_deriv_eq_0_iff[simp]: "fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f$0 :: 'a::{idom,semiring_char_0}))"
+lemma fps_deriv_eq_0_iff[simp]:
+ "fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f$0 :: 'a::{idom,semiring_char_0}))"
proof-
{assume "f= fps_const (f$0)" hence "fps_deriv f = fps_deriv (fps_const (f$0))" by simp
hence "fps_deriv f = 0" by simp }
@@ -866,60 +905,76 @@
finally show ?thesis by (simp add: field_simps)
qed
-lemma fps_deriv_eq_iff_ex: "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)"
- apply auto unfolding fps_deriv_eq_iff by blast
-
-
-fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps" where
+lemma fps_deriv_eq_iff_ex:
+ "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)"
+ apply auto unfolding fps_deriv_eq_iff
+ apply blast
+ done
+
+
+fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps"
+where
"fps_nth_deriv 0 f = f"
| "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)"
lemma fps_nth_deriv_commute: "fps_nth_deriv (Suc n) f = fps_deriv (fps_nth_deriv n f)"
- by (induct n arbitrary: f, auto)
-
-lemma fps_nth_deriv_linear[simp]: "fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g"
- by (induct n arbitrary: f g, auto simp add: fps_nth_deriv_commute)
-
-lemma fps_nth_deriv_neg[simp]: "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)"
- by (induct n arbitrary: f, simp_all)
-
-lemma fps_nth_deriv_add[simp]: "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
+ by (induct n arbitrary: f) auto
+
+lemma fps_nth_deriv_linear[simp]:
+ "fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) =
+ fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g"
+ by (induct n arbitrary: f g) (auto simp add: fps_nth_deriv_commute)
+
+lemma fps_nth_deriv_neg[simp]:
+ "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)"
+ by (induct n arbitrary: f) simp_all
+
+lemma fps_nth_deriv_add[simp]:
+ "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
using fps_nth_deriv_linear[of n 1 f 1 g] by simp
-lemma fps_nth_deriv_sub[simp]: "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
+lemma fps_nth_deriv_sub[simp]:
+ "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
unfolding diff_minus fps_nth_deriv_add by simp
lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0"
- by (induct n, simp_all )
+ by (induct n) simp_all
lemma fps_nth_deriv_1[simp]: "fps_nth_deriv n 1 = (if n = 0 then 1 else 0)"
- by (induct n, simp_all )
-
-lemma fps_nth_deriv_const[simp]: "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)"
- by (cases n, simp_all)
-
-lemma fps_nth_deriv_mult_const_left[simp]: "fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f"
+ by (induct n) simp_all
+
+lemma fps_nth_deriv_const[simp]:
+ "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)"
+ by (cases n) simp_all
+
+lemma fps_nth_deriv_mult_const_left[simp]:
+ "fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f"
using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp
-lemma fps_nth_deriv_mult_const_right[simp]: "fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c"
+lemma fps_nth_deriv_mult_const_right[simp]:
+ "fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c"
using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult_commute)
-lemma fps_nth_deriv_setsum: "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: ('a::comm_ring_1) fps)) S"
+lemma fps_nth_deriv_setsum:
+ "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: ('a::comm_ring_1) fps)) S"
proof-
- {assume "\<not> finite S" hence ?thesis by simp}
+ { assume "\<not> finite S" hence ?thesis by simp }
moreover
- {assume fS: "finite S"
- have ?thesis by (induct rule: finite_induct[OF fS], simp_all)}
+ {
+ assume fS: "finite S"
+ have ?thesis by (induct rule: finite_induct[OF fS]) simp_all
+ }
ultimately show ?thesis by blast
qed
-lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)"
+lemma fps_deriv_maclauren_0:
+ "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)"
by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult)
subsection {* Powers*}
lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
- by (induct n, auto simp add: expand_fps_eq fps_mult_nth)
+ by (induct n) (auto simp add: expand_fps_eq fps_mult_nth)
lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)$0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
proof(induct n)
@@ -932,19 +987,21 @@
qed
lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n $ 0 = 1"
- by (induct n, auto simp add: fps_mult_nth)
+ by (induct n) (auto simp add: fps_mult_nth)
lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
- by (induct n, auto simp add: fps_mult_nth)
+ by (induct n) (auto simp add: fps_mult_nth)
lemma startsby_power:"a $0 = (v::'a::{comm_ring_1}) \<Longrightarrow> a^n $0 = v^n"
- by (induct n, auto simp add: fps_mult_nth power_Suc)
+ by (induct n) (auto simp add: fps_mult_nth power_Suc)
lemma startsby_zero_power_iff[simp]:
"a^n $0 = (0::'a::{idom}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
apply (rule iffI)
-apply (induct n, auto simp add: power_Suc fps_mult_nth)
-by (rule startsby_zero_power, simp_all)
+apply (induct n)
+apply (auto simp add: fps_mult_nth)
+apply (rule startsby_zero_power, simp_all)
+done
lemma startsby_zero_power_prefix:
assumes a0: "a $0 = (0::'a::idom)"
@@ -1029,9 +1086,13 @@
ultimately show ?thesis by blast
qed
-lemma fps_deriv_power: "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
- apply (induct n, auto simp add: power_Suc field_simps fps_const_add[symmetric] simp del: fps_const_add)
- by (case_tac n, auto simp add: power_Suc field_simps)
+lemma fps_deriv_power:
+ "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
+ apply (induct n)
+ apply (auto simp add: power_Suc field_simps fps_const_add[symmetric] simp del: fps_const_add)
+ apply (case_tac n)
+ apply (auto simp add: power_Suc field_simps)
+ done
lemma fps_inverse_deriv:
fixes a:: "('a :: field) fps"
@@ -1079,8 +1140,8 @@
assumes a0: "a$0 \<noteq> 0"
shows "fps_deriv (inverse a) = - fps_deriv a / a ^ 2"
using fps_inverse_deriv[OF a0]
- unfolding power2_eq_square fps_divide_def
- fps_inverse_mult by simp
+ unfolding power2_eq_square fps_divide_def fps_inverse_mult
+ by simp
lemma inverse_mult_eq_1': assumes f0: "f$0 \<noteq> (0::'a::field)"
shows "f * inverse f= 1"
@@ -1090,7 +1151,8 @@
assumes a0: "b$0 \<noteq> 0"
shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2"
using fps_inverse_deriv[OF a0]
- by (simp add: fps_divide_def field_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
+ by (simp add: fps_divide_def field_simps
+ power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
lemma fps_inverse_gp': "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
@@ -1136,7 +1198,8 @@
definition fps_compose :: "('a::semiring_1) fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55) where
fps_compose_def: "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a$i * (b^i$n)) {0..n})"
-lemma fps_compose_nth: "(a oo b)$n = setsum (\<lambda>i. a$i * (b^i$n)) {0..n}" by (simp add: fps_compose_def)
+lemma fps_compose_nth: "(a oo b)$n = setsum (\<lambda>i. a$i * (b^i$n)) {0..n}"
+ by (simp add: fps_compose_def)
lemma fps_compose_X[simp]: "a oo X = (a :: ('a :: comm_ring_1) fps)"
by (simp add: fps_ext fps_compose_def mult_delta_right setsum_delta')
@@ -1207,7 +1270,7 @@
lemma XDN_linear:
"(XD ^^ n) (fps_const c * a + fps_const d * b) = fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: ('a::comm_ring_1) fps)"
- by (induct n, simp_all)
+ by (induct n) simp_all
lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" by (simp add: fps_eq_iff)
@@ -1296,7 +1359,10 @@
apply (clarsimp simp add: natpermute_def)
unfolding xs' ys'
using mn xs ys
- unfolding natpermute_def by simp}
+ unfolding natpermute_def
+ apply simp
+ done
+ }
moreover
{fix l assume l: "l \<in> natpermute n k"
let ?xs = "take h l"
@@ -1315,7 +1381,9 @@
apply (rule exI[where x = "?ys"])
using ls l
apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id)
- by simp}
+ apply simp
+ done
+ }
ultimately show ?thesis by blast
qed
@@ -1324,7 +1392,8 @@
lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})"
apply (auto simp add: set_replicate_conv_if natpermute_def)
apply (rule nth_equalityI)
- by simp_all
+ apply simp_all
+ done
lemma natpermute_finite: "finite (natpermute n k)"
proof(induct k arbitrary: n)
@@ -1368,7 +1437,8 @@
unfolding nth_list_update[OF i'(1)]
using i zxs
by (case_tac "ia=i", auto simp del: replicate.simps)
- then have "xs \<in> ?B" using i by blast}
+ then have "xs \<in> ?B" using i by blast
+ }
moreover
{fix i assume i: "i \<in> {0..k}"
let ?xs = "replicate (k+1) 0 [i:=n]"
@@ -1383,7 +1453,8 @@
finally
have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def mem_Collect_eq
by blast
- then have "?xs \<in> ?A" using nxs by blast}
+ then have "?xs \<in> ?A" using nxs by blast
+ }
ultimately show ?thesis by auto
qed
@@ -1409,7 +1480,8 @@
unfolding fps_mult_nth H[rule_format, OF km] ..
also have "\<dots> = (\<Sum>v\<in>natpermute n (m + 1). \<Prod>j\<in>{0..m}. a j $ v ! j)"
apply (simp add: k)
- unfolding natpermute_split[of m "m + 1", simplified, of n, unfolded natlist_trivial_1[unfolded One_nat_def] k]
+ unfolding natpermute_split[of m "m + 1", simplified, of n,
+ unfolded natlist_trivial_1[unfolded One_nat_def] k]
apply (subst setsum_UN_disjoint)
apply simp
apply simp
@@ -1428,8 +1500,9 @@
unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k]
apply (clarsimp simp add: natpermute_def nth_append)
done
- finally have "?P m n" .}
- ultimately show "?P m n " by (cases m, auto)
+ finally have "?P m n" .
+ }
+ ultimately show "?P m n " by (cases m) auto
qed
text{* The special form for powers *}
@@ -1474,7 +1547,8 @@
fix n assume H: "\<forall>m<n. b$m = c$m"
{assume n0: "n=0"
from h have "(b oo a)$n = (c oo a)$n" by simp
- hence "b$n = c$n" using n0 by (simp add: fps_compose_nth)}
+ hence "b$n = c$n" using n0 by (simp add: fps_compose_nth)
+ }
moreover
{fix n1 assume n1: "n = Suc n1"
have f: "finite {0 .. n1}" "finite {n}" by simp_all
@@ -1492,10 +1566,12 @@
using startsby_zero_power_nth_same[OF a0]
by simp
from h[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1
- have "b$n = c$n" by auto}
- ultimately show "b$n = c$n" by (cases n, auto)
+ have "b$n = c$n" by auto
+ }
+ ultimately show "b$n = c$n" by (cases n) auto
qed}
- then have ?rhs by (simp add: fps_eq_iff)}
+ then have ?rhs by (simp add: fps_eq_iff)
+ }
ultimately show ?thesis by blast
qed
@@ -1507,7 +1583,10 @@
"radical r 0 a 0 = 1"
| "radical r 0 a (Suc n) = 0"
| "radical r (Suc k) a 0 = r (Suc k) (a$0)"
-| "radical r (Suc k) a (Suc n) = (a$ Suc n - setsum (\<lambda>xs. setprod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k}) {xs. xs \<in> natpermute (Suc n) (Suc k) \<and> Suc n \<notin> set xs}) / (of_nat (Suc k) * (radical r (Suc k) a 0)^k)"
+| "radical r (Suc k) a (Suc n) =
+ (a$ Suc n - setsum (\<lambda>xs. setprod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k})
+ {xs. xs \<in> natpermute (Suc n) (Suc k) \<and> Suc n \<notin> set xs}) /
+ (of_nat (Suc k) * (radical r (Suc k) a 0)^k)"
by pat_completeness auto
termination radical
@@ -1574,7 +1653,8 @@
let ?K = "{0 ..k}"
have fK: "finite ?K" by simp
have fAK: "\<forall>i\<in>?K. finite (?A i)" by auto
- have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow> {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
+ have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow>
+ {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
proof(clarify)
fix i j assume i: "i \<in> ?K" and j: "j\<in> ?K" and ij: "i\<noteq>j"
{assume eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
@@ -1839,13 +1919,13 @@
lemma radical_mult_distrib:
fixes a:: "'a::field_char_0 fps"
- assumes
- k: "k > 0"
- and ra0: "r k (a $ 0) ^ k = a $ 0"
- and rb0: "r k (b $ 0) ^ k = b $ 0"
- and a0: "a$0 \<noteq> 0"
- and b0: "b$0 \<noteq> 0"
- shows "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0) \<longleftrightarrow> fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)"
+ assumes k: "k > 0"
+ and ra0: "r k (a $ 0) ^ k = a $ 0"
+ and rb0: "r k (b $ 0) ^ k = b $ 0"
+ and a0: "a$0 \<noteq> 0"
+ and b0: "b$0 \<noteq> 0"
+ shows "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0) \<longleftrightarrow>
+ fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)"
proof-
{assume r0': "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)"
from r0' have r0: "(r (k) ((a*b)$0)) ^ k = (a*b)$0"
@@ -2095,7 +2175,8 @@
lemma fps_inv_ginv: "fps_inv = fps_ginv X"
apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def)
- apply (induct_tac n rule: nat_less_induct, auto)
+ apply (induct_tac n rule: nat_less_induct)
+ apply auto
apply (case_tac na)
apply simp
apply simp
@@ -2305,7 +2386,7 @@
qed
lemma fps_const_power[simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)"
-by (induct n, auto)
+ by (induct n) auto
lemma fps_compose_radical:
assumes b0: "b$0 = (0::'a::field_char_0)"
@@ -2532,7 +2613,7 @@
qed
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)
+ 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)
@@ -2565,7 +2646,7 @@
qed
lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
- by (induct n, auto simp add: field_simps E_add_mult power_Suc)
+ by (induct n) (auto simp add: field_simps E_add_mult power_Suc)
lemma radical_E:
assumes r: "r (Suc k) 1 = 1"
@@ -3197,10 +3278,10 @@
lemma foldl_mult_start:
"foldl (%r x. r * f x) (v::'a::comm_ring_1) as * x = foldl (%r x. r * f x) (v * x) as "
- by (induct as arbitrary: x v, auto simp add: algebra_simps)
+ by (induct as arbitrary: x v) (auto simp add: algebra_simps)
lemma foldr_mult_foldl: "foldr (%x r. r * f x) as v = foldl (%r x. r * f x) (v :: 'a::comm_ring_1) as"
- by (induct as arbitrary: v, auto simp add: foldl_mult_start)
+ by (induct as arbitrary: v) (auto simp add: foldl_mult_start)
lemma F_nth_alt: "F as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))"
@@ -3224,11 +3305,12 @@
apply simp
apply (subgoal_tac "ALL as. foldl (%(r::'a) (a::'a). r) 1 as = 1")
apply auto
- apply (induct_tac as, auto)
+ apply (induct_tac as)
+ apply auto
done
lemma foldl_prod_prod: "foldl (%(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (%r x. r * g x) w as = foldl (%r x. r * f x * g x) (v*w) as"
- by (induct as arbitrary: v w, auto simp add: algebra_simps)
+ by (induct as arbitrary: v w) (auto simp add: algebra_simps)
lemma F_rec: "F as bs c $ Suc n = ((foldl (%r a. r* (a + of_nat n)) c as)/ (foldl (%r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c $ n"
@@ -3276,7 +3358,7 @@
lemma XDp_foldr_nth[simp]: "foldr (%c r. XDp c o r) cs (%c. XDp c a) c0 $ n =
foldr (%c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n"
- by (induct cs arbitrary: c0, auto simp add: algebra_simps)
+ by (induct cs arbitrary: c0) (auto simp add: algebra_simps)
lemma genric_XDp_foldr_nth:
assumes
@@ -3284,6 +3366,6 @@
shows "foldr (%c r. f c o r) cs (%c. g c a) c0 $ n =
foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
- by (induct cs arbitrary: c0, auto simp add: algebra_simps f)
+ by (induct cs arbitrary: c0) (auto simp add: algebra_simps f)
end
--- a/src/Pure/General/linear_set.scala Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/General/linear_set.scala Fri Aug 10 16:29:40 2012 +0200
@@ -34,8 +34,6 @@
{
override def companion: GenericCompanion[Linear_Set] = Linear_Set
- def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
-
/* relative addressing */
@@ -76,7 +74,7 @@
}
}
- def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+ def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] = // FIXME reverse fold
((hook, this) /: elems) {
case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
}._2
@@ -147,6 +145,10 @@
case Some(stop) => iterator(from).takeWhile(_ != stop)
}
+ def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
+
+ override def last: A = reverse.head
+
def + (elem: A): Linear_Set[A] = insert_after(end, elem)
def - (elem: A): Linear_Set[A] =
--- a/src/Pure/General/scan.scala Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/General/scan.scala Fri Aug 10 16:29:40 2012 +0200
@@ -375,9 +375,9 @@
val recover_delimited =
(quoted_prefix("\"") | (quoted_prefix("`") | (verbatim_prefix | comment_prefix))) ^^
- (x => Token(Token.Kind.UNPARSED, x))
+ (x => Token(Token.Kind.ERROR, x))
- val bad = one(_ => true) ^^ (x => Token(Token.Kind.UNPARSED, x))
+ val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x))
space | (recover_delimited |
(((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
--- a/src/Pure/Isar/token.scala Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/Isar/token.scala Fri Aug 10 16:29:40 2012 +0200
@@ -28,6 +28,7 @@
val VERBATIM = Value("verbatim text")
val SPACE = Value("white space")
val COMMENT = Value("comment text")
+ val ERROR = Value("bad input")
val UNPARSED = Value("unparsed input")
}
@@ -89,8 +90,15 @@
def is_space: Boolean = kind == Token.Kind.SPACE
def is_comment: Boolean = kind == Token.Kind.COMMENT
def is_proper: Boolean = !is_space && !is_comment
+ def is_error: Boolean = kind == Token.Kind.ERROR
def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
+ def is_unfinished: Boolean = is_error &&
+ (source.startsWith("\"") ||
+ source.startsWith("`") ||
+ source.startsWith("{*") ||
+ source.startsWith("(*"))
+
def is_begin: Boolean = is_keyword && source == "begin"
def is_end: Boolean = is_keyword && source == "end"
--- a/src/Pure/ML/ml_lex.ML Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/ML/ml_lex.ML Fri Aug 10 16:29:40 2012 +0200
@@ -115,7 +115,7 @@
| String => Isabelle_Markup.ML_string
| Space => Markup.empty
| Comment => Isabelle_Markup.ML_comment
- | Error _ => Isabelle_Markup.ML_malformed
+ | Error msg => Isabelle_Markup.bad msg
| EOF => Markup.empty;
fun token_markup kind x =
--- a/src/Pure/PIDE/command.scala Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/PIDE/command.scala Fri Aug 10 16:29:40 2012 +0200
@@ -111,8 +111,8 @@
{
val cmds1 = this.commands
val cmds2 = that.commands
- require(cmds1.forall(_.is_defined))
- require(cmds2.forall(_.is_defined))
+ require(!cmds1.exists(_.is_undefined))
+ require(!cmds2.exists(_.is_undefined))
cmds1.length == cmds2.length &&
(cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
}
@@ -128,10 +128,12 @@
{
/* classification */
- def is_defined: Boolean = id != Document.no_id
+ def is_undefined: Boolean = id == Document.no_id
+ val is_unparsed: Boolean = span.exists(_.is_unparsed)
+ val is_unfinished: Boolean = span.exists(_.is_unfinished)
val is_ignored: Boolean = !span.exists(_.is_proper)
- val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed))
+ val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
def is_command: Boolean = !is_ignored && !is_malformed
def name: String =
--- a/src/Pure/PIDE/document.ML Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/PIDE/document.ML Fri Aug 10 16:29:40 2012 +0200
@@ -17,7 +17,7 @@
val print_id: id -> string
type node_header = string * Thy_Header.header * string list
datatype node_edit =
- Clear |
+ Clear | (* FIXME unused !? *)
Edits of (command_id option * command_id option) list |
Deps of node_header |
Perspective of command_id list
--- a/src/Pure/PIDE/isabelle_markup.ML Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Fri Aug 10 16:29:40 2012 +0200
@@ -55,7 +55,6 @@
val ML_charN: string val ML_char: Markup.T
val ML_stringN: string val ML_string: Markup.T
val ML_commentN: string val ML_comment: Markup.T
- val ML_malformedN: string val ML_malformed: Markup.T
val ML_defN: string
val ML_openN: string
val ML_structN: string
@@ -74,11 +73,7 @@
val verbatimN: string val verbatim: Markup.T
val commentN: string val comment: Markup.T
val controlN: string val control: Markup.T
- val malformedN: string val malformed: Markup.T
val tokenN: string val token: Properties.T -> Markup.T
- val command_spanN: string val command_span: string -> Markup.T
- val ignored_spanN: string val ignored_span: Markup.T
- val malformed_spanN: string val malformed_span: Markup.T
val elapsedN: string
val cpuN: string
val gcN: string
@@ -100,7 +95,8 @@
val promptN: string val prompt: Markup.T
val reportN: string val report: Markup.T
val no_reportN: string val no_report: Markup.T
- val badN: string val bad: Markup.T
+ val messageN: string
+ val badN: string val bad: string -> Markup.T
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
@@ -211,7 +207,6 @@
val (ML_charN, ML_char) = markup_elem "ML_char";
val (ML_stringN, ML_string) = markup_elem "ML_string";
val (ML_commentN, ML_comment) = markup_elem "ML_comment";
-val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
val ML_defN = "ML_def";
val ML_openN = "ML_open";
@@ -240,15 +235,10 @@
val (verbatimN, verbatim) = markup_elem "verbatim";
val (commentN, comment) = markup_elem "comment";
val (controlN, control) = markup_elem "control";
-val (malformedN, malformed) = markup_elem "malformed";
val tokenN = "token";
fun token props = (tokenN, props);
-val (command_spanN, command_span) = markup_string "command_span" Markup.nameN;
-val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
-val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
-
(* timing *)
@@ -297,7 +287,11 @@
val (reportN, report) = markup_elem "report";
val (no_reportN, no_report) = markup_elem "no_report";
-val (badN, bad) = markup_elem "bad";
+val messageN = "message"
+val badN = "bad"
+
+fun bad "" = (badN, [])
+ | bad msg = (badN, [(messageN, msg)]);
(* protocol message functions *)
--- a/src/Pure/PIDE/isabelle_markup.scala Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Fri Aug 10 16:29:40 2012 +0200
@@ -132,7 +132,6 @@
val ML_CHAR = "ML_char"
val ML_STRING = "ML_string"
val ML_COMMENT = "ML_comment"
- val ML_MALFORMED = "ML_malformed"
val ML_DEF = "ML_def"
val ML_OPEN = "ML_open"
@@ -150,11 +149,6 @@
val VERBATIM = "verbatim"
val COMMENT = "comment"
val CONTROL = "control"
- val MALFORMED = "malformed"
-
- val COMMAND_SPAN = "command_span"
- val IGNORED_SPAN = "ignored_span"
- val MALFORMED_SPAN = "malformed_span"
/* timing */
@@ -242,6 +236,7 @@
val NO_REPORT = "no_report"
+ val Message = new Properties.String("message")
val BAD = "bad"
--- a/src/Pure/PIDE/protocol.ML Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Aug 10 16:29:40 2012 +0200
@@ -33,7 +33,7 @@
let open XML.Decode in
list (pair string
(variant
- [fn ([], []) => Document.Clear,
+ [fn ([], []) => Document.Clear, (* FIXME unused !? *)
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
fn ([], a) =>
let
--- a/src/Pure/PIDE/protocol.scala Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Aug 10 16:29:40 2012 +0200
@@ -213,7 +213,7 @@
def encode_edit(name: Document.Node.Name)
: T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
variant(List(
- { case Document.Node.Clear() => (Nil, Nil) },
+ { case Document.Node.Clear() => (Nil, Nil) }, // FIXME unused !?
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
{ case Document.Node.Deps(header) =>
val dir = Isabelle_System.posix_path(name.dir)
--- a/src/Pure/Syntax/syntax_phases.ML Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Aug 10 16:29:40 2012 +0200
@@ -318,7 +318,7 @@
fun parse_failed ctxt pos msg kind =
cat_error msg ("Failed to parse " ^ kind ^
Markup.markup Isabelle_Markup.report
- (Context_Position.reported_text ctxt pos Isabelle_Markup.bad ""));
+ (Context_Position.reported_text ctxt pos (Isabelle_Markup.bad "") ""));
fun parse_sort ctxt =
Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
@@ -609,7 +609,7 @@
| token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
| token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
| token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
- | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.malformed, x))
+ | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.bad "", x))
| token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
| token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
| token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
--- a/src/Pure/System/session.scala Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/System/session.scala Fri Aug 10 16:29:40 2012 +0200
@@ -453,7 +453,7 @@
header: Document.Node.Header, perspective: Text.Perspective, text: String)
{
edit(List(header_edit(name, header),
- name -> Document.Node.Clear(), // FIXME diff wrt. existing node
+ name -> Document.Node.Clear(),
name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
name -> Document.Node.Perspective(perspective)))
}
--- a/src/Pure/Thy/thy_syntax.ML Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Fri Aug 10 16:29:40 2012 +0200
@@ -54,7 +54,7 @@
| Token.Space => Markup.empty
| Token.Comment => Isabelle_Markup.comment
| Token.InternalValue => Markup.empty
- | Token.Error _ => Isabelle_Markup.malformed
+ | Token.Error msg => Isabelle_Markup.bad msg
| Token.Sync => Isabelle_Markup.control
| Token.EOF => Isabelle_Markup.control;
@@ -74,7 +74,8 @@
val malformed_symbols =
Symbol_Pos.explode (Token.source_position_of tok)
|> map_filter (fn (sym, pos) =>
- if Symbol.is_malformed sym then SOME (pos, Isabelle_Markup.malformed) else NONE);
+ if Symbol.is_malformed sym
+ then SOME (pos, Isabelle_Markup.bad "Malformed symbol") else NONE);
val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
val reports = (Token.position_of tok, token_markup tok) :: malformed_symbols;
in (is_malformed, reports) end;
@@ -127,18 +128,7 @@
(* present *)
-local
-
-fun kind_markup (Command name) = Isabelle_Markup.command_span name
- | kind_markup Ignored = Isabelle_Markup.ignored_span
- | kind_markup Malformed = Isabelle_Markup.malformed_span;
-
-in
-
-fun present_span span =
- Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
-
-end;
+val present_span = implode o map present_token o span_content;
--- a/src/Pure/Thy/thy_syntax.scala Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Aug 10 16:29:40 2012 +0200
@@ -165,7 +165,7 @@
/** text edits **/
- /* phase 1: edit individual command source */
+ /* edit individual command source */
@tailrec private def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
: Linear_Set[Command] =
@@ -194,7 +194,7 @@
}
- /* phase 2: recover command spans */
+ /* reparse range of command spans */
@tailrec private def chop_common(
cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
@@ -203,69 +203,118 @@
case _ => (cmds, spans)
}
- private def trim_common(
- cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
+ private def reparse_spans(
+ syntax: Outer_Syntax,
+ name: Document.Node.Name,
+ commands: Linear_Set[Command],
+ first: Command, last: Command): Linear_Set[Command] =
{
- val (cmds1, spans1) = chop_common(cmds, spans)
+ val cmds0 = commands.iterator(first, last).toList
+ val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
+
+ val (cmds1, spans1) = chop_common(cmds0, spans0)
+
val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse)
- (rev_cmds2.reverse, rev_spans2.reverse)
+ val cmds2 = rev_cmds2.reverse
+ val spans2 = rev_spans2.reverse
+
+ cmds2 match {
+ case Nil =>
+ assert(spans2.isEmpty)
+ commands
+ case cmd :: _ =>
+ val hook = commands.prev(cmd)
+ val inserted = spans2.map(span => Command(Document.new_id(), name, span))
+ (commands /: cmds2)(_ - _).append_after(hook, inserted)
+ }
}
+
+ /* recover command spans after edits */
+
+ // FIXME somewhat slow
private def recover_spans(
syntax: Outer_Syntax,
- node_name: Document.Node.Name,
+ name: Document.Node.Name,
perspective: Command.Perspective,
- old_commands: Linear_Set[Command]): Linear_Set[Command] =
+ commands: Linear_Set[Command]): Linear_Set[Command] =
{
- val visible = perspective.commands.iterator.filter(_.is_defined).toSet
+ val visible = perspective.commands.toSet
- def next_invisible_command(commands: Linear_Set[Command], from: Command): Command =
- commands.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
- .find(_.is_command) getOrElse commands.last
-
- @tailrec def recover(commands: Linear_Set[Command]): Linear_Set[Command] =
- commands.iterator.find(cmd => !cmd.is_defined) match {
- case Some(first_undefined) =>
- val first = next_invisible_command(commands.reverse, first_undefined)
- val last = next_invisible_command(commands, first_undefined)
+ def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
+ cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
+ .find(_.is_command) getOrElse cmds.last
- val cmds0 = commands.iterator(first, last).toList
- val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
-
- val (cmds, spans) = trim_common(cmds0, spans0)
- val new_commands =
- cmds match {
- case Nil =>
- assert(spans.isEmpty)
- commands
- case cmd :: _ =>
- val hook = commands.prev(cmd)
- val inserted = spans.map(span => Command(Document.new_id(), node_name, span))
- (commands /: cmds)(_ - _).append_after(hook, inserted)
- }
- recover(new_commands)
-
- case None => commands
+ @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
+ cmds.find(_.is_unparsed) match {
+ case Some(first_unparsed) =>
+ val first = next_invisible_command(cmds.reverse, first_unparsed)
+ val last = next_invisible_command(cmds, first_unparsed)
+ recover(reparse_spans(syntax, name, cmds, first, last))
+ case None => cmds
}
- recover(old_commands)
+ recover(commands)
}
- /* phase 3: full reparsing after syntax change */
+ /* consolidate unfinished spans */
- private def reparse_spans(
+ private def consolidate_spans(
syntax: Outer_Syntax,
- node_name: Document.Node.Name,
+ name: Document.Node.Name,
+ perspective: Command.Perspective,
commands: Linear_Set[Command]): Linear_Set[Command] =
{
- val cmds = commands.toList
- val spans1 = parse_spans(syntax.scan(cmds.map(_.source).mkString))
- if (cmds.map(_.span) == spans1) commands
- else Linear_Set(spans1.map(span => Command(Document.new_id(), node_name, span)): _*)
+ if (perspective.commands.isEmpty) commands
+ else {
+ commands.find(_.is_unfinished) match {
+ case Some(first_unfinished) =>
+ val visible = perspective.commands.toSet
+ commands.reverse.find(visible) match {
+ case Some(last_visible) =>
+ reparse_spans(syntax, name, commands, first_unfinished, last_visible)
+ case None => commands
+ }
+ case None => commands
+ }
+ }
}
- /* main phase */
+ /* main */
+
+ private def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
+ : List[(Option[Command], Option[Command])] =
+ {
+ val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
+ val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
+
+ removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) :::
+ inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
+ }
+
+ private def text_edit(syntax: Outer_Syntax,
+ node: Document.Node, edit: Document.Edit_Text): Document.Node =
+ {
+ edit match {
+ case (_, Document.Node.Clear()) => node.clear
+
+ case (name, Document.Node.Edits(text_edits)) =>
+ val commands0 = node.commands
+ val commands1 = edit_text(text_edits, commands0)
+ val commands2 = recover_spans(syntax, name, node.perspective, commands1)
+ node.update_commands(commands2)
+
+ case (_, Document.Node.Deps(_)) => node
+
+ case (name, Document.Node.Perspective(text_perspective)) =>
+ val perspective = command_perspective(node, text_perspective)
+ if (node.perspective same perspective) node
+ else
+ node.update_perspective(perspective)
+ .update_commands(consolidate_spans(syntax, name, perspective, node.commands))
+ }
+ }
def text_edits(
base_syntax: Outer_Syntax,
@@ -279,40 +328,29 @@
var nodes = nodes0
val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
- (edits ::: reparse.map((_, Document.Node.Edits(Nil)))) foreach {
- case (name, Document.Node.Clear()) =>
- doc_edits += (name -> Document.Node.Clear())
- nodes += (name -> nodes(name).clear)
+ val node_edits =
+ (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
+ .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ???
- case (name, Document.Node.Edits(text_edits)) =>
+ node_edits foreach {
+ case (name, edits) =>
val node = nodes(name)
- val commands0 = node.commands
- val commands1 = edit_text(text_edits, commands0)
- val commands2 = recover_spans(syntax, name, node.perspective, commands1) // FIXME somewhat slow
- val commands3 =
- if (reparse_set.contains(name)) reparse_spans(syntax, name, commands2) // slow
- else commands2
-
- val removed_commands = commands0.iterator.filter(!commands3.contains(_)).toList
- val inserted_commands = commands3.iterator.filter(!commands0.contains(_)).toList
+ val commands = node.commands
- val cmd_edits =
- removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
- inserted_commands.map(cmd => (commands3.prev(cmd), Some(cmd)))
-
- doc_edits += (name -> Document.Node.Edits(cmd_edits))
- nodes += (name -> node.update_commands(commands3))
-
- case (name, Document.Node.Deps(_)) =>
+ val node1 =
+ if (reparse_set(name) && !commands.isEmpty)
+ node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
+ else node
+ val node2 = (node1 /: edits)(text_edit(syntax, _, _))
- case (name, Document.Node.Perspective(text_perspective)) =>
- val node = nodes(name)
- val perspective = command_perspective(node, text_perspective)
- if (!(node.perspective same perspective)) {
- doc_edits += (name -> Document.Node.Perspective(perspective))
- nodes += (name -> node.update_perspective(perspective))
- }
+ if (!(node.perspective same node2.perspective))
+ doc_edits += (name -> Document.Node.Perspective(node2.perspective))
+
+ doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+
+ nodes += (name -> node2)
}
+
(doc_edits.toList, Document.Version.make(syntax, nodes))
}
}
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Fri Aug 10 13:33:54 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Aug 10 16:29:40 2012 +0200
@@ -22,7 +22,7 @@
{
/* physical rendering */
- // see http://www.w3schools.com/css/css_colornames.asp
+ // see http://www.w3schools.com/cssref/css_colornames.asp
def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
@@ -104,18 +104,25 @@
}
+ private def tooltip_text(msg: XML.Body): String =
+ Pretty.string_of(msg, margin = Isabelle.Int_Property("tooltip-margin"))
+
def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
{
val msgs =
snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
- Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+ Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
+ Isabelle_Markup.BAD)),
{
- case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
+ case (msgs, Text.Info(_, msg @
+ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
if markup == Isabelle_Markup.WRITELN ||
markup == Isabelle_Markup.WARNING ||
markup == Isabelle_Markup.ERROR =>
- msgs + (serial ->
- Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
+ msgs + (serial -> tooltip_text(List(msg)))
+ case (msgs, Text.Info(_,
+ XML.Elem(Markup(Isabelle_Markup.BAD, Isabelle_Markup.Message(msg)), _))) =>
+ msgs + (0L -> tooltip_text(YXML.parse_body(msg)))
}).toList.flatMap(_.info)
if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
}
@@ -290,7 +297,6 @@
Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
- Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
Isabelle_Markup.ANTIQ -> get_color("blue"))
private val text_color_elements = Set.empty[String] ++ text_colors.keys
@@ -336,7 +342,7 @@
Token.Kind.VERBATIM -> COMMENT3,
Token.Kind.SPACE -> NULL,
Token.Kind.COMMENT -> COMMENT1,
- Token.Kind.UNPARSED -> INVALID
+ Token.Kind.ERROR -> INVALID
).withDefaultValue(NULL)
}