1.1 --- a/src/HOL/Library/Float.thy Tue Feb 21 13:19:16 2012 +0100
1.2 +++ b/src/HOL/Library/Float.thy Tue Feb 21 17:09:53 2012 +0100
1.3 @@ -9,8 +9,7 @@
1.4 imports Complex_Main Lattice_Algebras
1.5 begin
1.6
1.7 -definition
1.8 - pow2 :: "int \<Rightarrow> real" where
1.9 +definition pow2 :: "int \<Rightarrow> real" where
1.10 [simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
1.11
1.12 datatype float = Float int int
1.13 @@ -30,17 +29,20 @@
1.14 primrec scale :: "float \<Rightarrow> int" where
1.15 "scale (Float a b) = b"
1.16
1.17 -instantiation float :: zero begin
1.18 +instantiation float :: zero
1.19 +begin
1.20 definition zero_float where "0 = Float 0 0"
1.21 instance ..
1.22 end
1.23
1.24 -instantiation float :: one begin
1.25 +instantiation float :: one
1.26 +begin
1.27 definition one_float where "1 = Float 1 0"
1.28 instance ..
1.29 end
1.30
1.31 -instantiation float :: number begin
1.32 +instantiation float :: number
1.33 +begin
1.34 definition number_of_float where "number_of n = Float n 0"
1.35 instance ..
1.36 end
1.37 @@ -124,13 +126,13 @@
1.38 by (auto simp add: pow2_def)
1.39
1.40 lemma pow2_int: "pow2 (int c) = 2^c"
1.41 -by (simp add: pow2_def)
1.42 + by (simp add: pow2_def)
1.43
1.44 -lemma zero_less_pow2[simp]:
1.45 - "0 < pow2 x"
1.46 +lemma zero_less_pow2[simp]: "0 < pow2 x"
1.47 by (simp add: pow2_powr)
1.48
1.49 -lemma normfloat_imp_odd_or_zero: "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
1.50 +lemma normfloat_imp_odd_or_zero:
1.51 + "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
1.52 proof (induct f rule: normfloat.induct)
1.53 case (1 u v)
1.54 from 1 have ab: "normfloat (Float u v) = Float a b" by auto
1.55 @@ -169,7 +171,7 @@
1.56
1.57 lemma float_eq_odd_helper:
1.58 assumes odd: "odd a'"
1.59 - and floateq: "real (Float a b) = real (Float a' b')"
1.60 + and floateq: "real (Float a b) = real (Float a' b')"
1.61 shows "b \<le> b'"
1.62 proof -
1.63 from odd have "a' \<noteq> 0" by auto
1.64 @@ -191,8 +193,8 @@
1.65
1.66 lemma float_eq_odd:
1.67 assumes odd1: "odd a"
1.68 - and odd2: "odd a'"
1.69 - and floateq: "real (Float a b) = real (Float a' b')"
1.70 + and odd2: "odd a'"
1.71 + and floateq: "real (Float a b) = real (Float a' b')"
1.72 shows "a = a' \<and> b = b'"
1.73 proof -
1.74 from
1.75 @@ -216,7 +218,7 @@
1.76 have ab': "odd a' \<or> (a' = 0 \<and> b' = 0)" by (rule normfloat_imp_odd_or_zero[OF normg])
1.77 {
1.78 assume odd: "odd a"
1.79 - then have "a \<noteq> 0" by (simp add: even_def, arith)
1.80 + then have "a \<noteq> 0" by (simp add: even_def) arith
1.81 with float_eq have "a' \<noteq> 0" by auto
1.82 with ab' have "odd a'" by simp
1.83 from odd this float_eq have "a = a' \<and> b = b'" by (rule float_eq_odd)
1.84 @@ -236,7 +238,8 @@
1.85 done
1.86 qed
1.87
1.88 -instantiation float :: plus begin
1.89 +instantiation float :: plus
1.90 +begin
1.91 fun plus_float where
1.92 [simp del]: "(Float a_m a_e) + (Float b_m b_e) =
1.93 (if a_e \<le> b_e then Float (a_m + b_m * 2^(nat(b_e - a_e))) a_e
1.94 @@ -244,17 +247,20 @@
1.95 instance ..
1.96 end
1.97
1.98 -instantiation float :: uminus begin
1.99 +instantiation float :: uminus
1.100 +begin
1.101 primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
1.102 instance ..
1.103 end
1.104
1.105 -instantiation float :: minus begin
1.106 -definition minus_float where [simp del]: "(z::float) - w = z + (- w)"
1.107 +instantiation float :: minus
1.108 +begin
1.109 +definition minus_float where "(z::float) - w = z + (- w)"
1.110 instance ..
1.111 end
1.112
1.113 -instantiation float :: times begin
1.114 +instantiation float :: times
1.115 +begin
1.116 fun times_float where [simp del]: "(Float a_m a_e) * (Float b_m b_e) = Float (a_m * b_m) (a_e + b_e)"
1.117 instance ..
1.118 end
1.119 @@ -265,7 +271,8 @@
1.120 primrec float_nprt :: "float \<Rightarrow> float" where
1.121 "float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))"
1.122
1.123 -instantiation float :: ord begin
1.124 +instantiation float :: ord
1.125 +begin
1.126 definition le_float_def: "z \<le> (w :: float) \<equiv> real z \<le> real w"
1.127 definition less_float_def: "z < (w :: float) \<equiv> real z < real w"
1.128 instance ..
1.129 @@ -276,7 +283,7 @@
1.130 auto simp add: pow2_int[symmetric] pow2_add[symmetric])
1.131
1.132 lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
1.133 - by (cases a) (simp add: uminus_float.simps)
1.134 + by (cases a) simp
1.135
1.136 lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
1.137 by (cases a, cases b) (simp add: minus_float_def)
1.138 @@ -285,7 +292,7 @@
1.139 by (cases a, cases b) (simp add: times_float.simps pow2_add)
1.140
1.141 lemma real_of_float_0[simp]: "real (0 :: float) = 0"
1.142 - by (auto simp add: zero_float_def float_zero)
1.143 + by (auto simp add: zero_float_def)
1.144
1.145 lemma real_of_float_1[simp]: "real (1 :: float) = 1"
1.146 by (auto simp add: one_float_def)
1.147 @@ -1161,16 +1168,20 @@
1.148 qed
1.149
1.150 definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1.151 -"lb_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
1.152 - l = bitlen m - int prec
1.153 - in if l > 0 then Float (m div (2^nat l)) (e + l)
1.154 - else Float m e)"
1.155 + "lb_mult prec x y =
1.156 + (case normfloat (x * y) of Float m e \<Rightarrow>
1.157 + let
1.158 + l = bitlen m - int prec
1.159 + in if l > 0 then Float (m div (2^nat l)) (e + l)
1.160 + else Float m e)"
1.161
1.162 definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1.163 -"ub_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
1.164 - l = bitlen m - int prec
1.165 - in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
1.166 - else Float m e)"
1.167 + "ub_mult prec x y =
1.168 + (case normfloat (x * y) of Float m e \<Rightarrow>
1.169 + let
1.170 + l = bitlen m - int prec
1.171 + in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
1.172 + else Float m e)"
1.173
1.174 lemma lb_mult: "real (lb_mult prec x y) \<le> real (x * y)"
1.175 proof (cases "normfloat (x * y)")
1.176 @@ -1225,7 +1236,8 @@
1.177 primrec float_abs :: "float \<Rightarrow> float" where
1.178 "float_abs (Float m e) = Float \<bar>m\<bar> e"
1.179
1.180 -instantiation float :: abs begin
1.181 +instantiation float :: abs
1.182 +begin
1.183 definition abs_float_def: "\<bar>x\<bar> = float_abs x"
1.184 instance ..
1.185 end
1.186 @@ -1290,10 +1302,10 @@
1.187 declare ceiling_fl.simps[simp del]
1.188
1.189 definition lb_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1.190 -"lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"
1.191 + "lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"
1.192
1.193 definition ub_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1.194 -"ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"
1.195 + "ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"
1.196
1.197 lemma lb_mod: fixes k :: int assumes "0 \<le> real x" and "real k * y \<le> real x" (is "?k * y \<le> ?x")
1.198 assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
1.199 @@ -1307,7 +1319,9 @@
1.200 finally show ?thesis unfolding lb_mod_def real_of_float_sub real_of_float_mult by auto
1.201 qed
1.202
1.203 -lemma ub_mod: fixes k :: int and x :: float assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y")
1.204 +lemma ub_mod:
1.205 + fixes k :: int and x :: float
1.206 + assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y")
1.207 assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
1.208 shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
1.209 proof -
2.1 --- a/src/HOL/Library/Fraction_Field.thy Tue Feb 21 13:19:16 2012 +0100
2.2 +++ b/src/HOL/Library/Fraction_Field.thy Tue Feb 21 17:09:53 2012 +0100
2.3 @@ -2,8 +2,8 @@
2.4 Author: Amine Chaieb, University of Cambridge
2.5 *)
2.6
2.7 -header{* A formalization of the fraction field of any integral domain
2.8 - A generalization of Rat.thy from int to any integral domain *}
2.9 +header{* A formalization of the fraction field of any integral domain;
2.10 + generalization of theory Rat from int to any integral domain *}
2.11
2.12 theory Fraction_Field
2.13 imports Main
2.14 @@ -14,7 +14,7 @@
2.15 subsubsection {* Construction of the type of fractions *}
2.16
2.17 definition fractrel :: "(('a::idom * 'a ) * ('a * 'a)) set" where
2.18 - "fractrel == {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
2.19 + "fractrel = {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
2.20
2.21 lemma fractrel_iff [simp]:
2.22 "(x, y) \<in> fractrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
2.23 @@ -70,8 +70,7 @@
2.24
2.25 subsubsection {* Representation and basic operations *}
2.26
2.27 -definition
2.28 - Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
2.29 +definition Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
2.30 "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
2.31
2.32 code_datatype Fract
2.33 @@ -95,14 +94,11 @@
2.34 instantiation fract :: (idom) "{comm_ring_1, power}"
2.35 begin
2.36
2.37 -definition
2.38 - Zero_fract_def [code_unfold]: "0 = Fract 0 1"
2.39 +definition Zero_fract_def [code_unfold]: "0 = Fract 0 1"
2.40
2.41 -definition
2.42 - One_fract_def [code_unfold]: "1 = Fract 1 1"
2.43 +definition One_fract_def [code_unfold]: "1 = Fract 1 1"
2.44
2.45 -definition
2.46 - add_fract_def:
2.47 +definition add_fract_def:
2.48 "q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
2.49 fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
2.50
2.51 @@ -117,8 +113,7 @@
2.52 with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2)
2.53 qed
2.54
2.55 -definition
2.56 - minus_fract_def:
2.57 +definition minus_fract_def:
2.58 "- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})"
2.59
2.60 lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
2.61 @@ -131,16 +126,14 @@
2.62 lemma minus_fract_cancel [simp]: "Fract (- a) (- b) = Fract a b"
2.63 by (cases "b = 0") (simp_all add: eq_fract)
2.64
2.65 -definition
2.66 - diff_fract_def: "q - r = q + - (r::'a fract)"
2.67 +definition diff_fract_def: "q - r = q + - (r::'a fract)"
2.68
2.69 lemma diff_fract [simp]:
2.70 assumes "b \<noteq> 0" and "d \<noteq> 0"
2.71 shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
2.72 using assms by (simp add: diff_fract_def diff_minus)
2.73
2.74 -definition
2.75 - mult_fract_def:
2.76 +definition mult_fract_def:
2.77 "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
2.78 fractrel``{(fst x * fst y, snd x * snd y)})"
2.79
2.80 @@ -238,8 +231,7 @@
2.81 instantiation fract :: (idom) field_inverse_zero
2.82 begin
2.83
2.84 -definition
2.85 - inverse_fract_def:
2.86 +definition inverse_fract_def:
2.87 "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q.
2.88 fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
2.89
2.90 @@ -252,8 +244,7 @@
2.91 then show ?thesis by (simp add: Fract_def inverse_fract_def UN_fractrel)
2.92 qed
2.93
2.94 -definition
2.95 - divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
2.96 +definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
2.97
2.98 lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
2.99 by (simp add: divide_fract_def)
2.100 @@ -261,14 +252,15 @@
2.101 instance proof
2.102 fix q :: "'a fract"
2.103 assume "q \<noteq> 0"
2.104 - then show "inverse q * q = 1" apply (cases q rule: Fract_cases_nonzero)
2.105 - by (simp_all add: mult_fract inverse_fract fract_expand eq_fract mult_commute)
2.106 + then show "inverse q * q = 1"
2.107 + by (cases q rule: Fract_cases_nonzero)
2.108 + (simp_all add: fract_expand eq_fract mult_commute)
2.109 next
2.110 fix q r :: "'a fract"
2.111 show "q / r = q * inverse r" by (simp add: divide_fract_def)
2.112 next
2.113 - show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
2.114 - (simp add: fract_collapse)
2.115 + show "inverse 0 = (0:: 'a fract)"
2.116 + by (simp add: fract_expand) (simp add: fract_collapse)
2.117 qed
2.118
2.119 end
2.120 @@ -292,7 +284,7 @@
2.121 have "?le a b c d = ?le (a * x) (b * x) c d"
2.122 proof -
2.123 from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
2.124 - hence "?le a b c d =
2.125 + then have "?le a b c d =
2.126 ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
2.127 by (simp add: mult_le_cancel_right)
2.128 also have "... = ?le (a * x) (b * x) c d"
2.129 @@ -304,7 +296,7 @@
2.130 let ?D = "b * d" and ?D' = "b' * d'"
2.131 from neq have D: "?D \<noteq> 0" by simp
2.132 from neq have "?D' \<noteq> 0" by simp
2.133 - hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
2.134 + then have "?le a b c d = ?le (a * ?D') (b * ?D') c d"
2.135 by (rule le_factor)
2.136 also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
2.137 by (simp add: mult_ac)
2.138 @@ -320,13 +312,11 @@
2.139 instantiation fract :: (linordered_idom) linorder
2.140 begin
2.141
2.142 -definition
2.143 - le_fract_def:
2.144 +definition le_fract_def:
2.145 "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
2.146 {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
2.147
2.148 -definition
2.149 - less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
2.150 +definition less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
2.151
2.152 lemma le_fract [simp]:
2.153 assumes "b \<noteq> 0" and "d \<noteq> 0"
2.154 @@ -409,28 +399,25 @@
2.155 instantiation fract :: (linordered_idom) "{distrib_lattice, abs_if, sgn_if}"
2.156 begin
2.157
2.158 -definition
2.159 - abs_fract_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"
2.160 +definition abs_fract_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"
2.161
2.162 -definition
2.163 - sgn_fract_def:
2.164 - "sgn (q::'a fract) = (if q=0 then 0 else if 0<q then 1 else - 1)"
2.165 +definition sgn_fract_def:
2.166 + "sgn (q::'a fract) = (if q=0 then 0 else if 0<q then 1 else - 1)"
2.167
2.168 theorem abs_fract [simp]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
2.169 by (auto simp add: abs_fract_def Zero_fract_def le_less
2.170 eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split)
2.171
2.172 -definition
2.173 - inf_fract_def:
2.174 - "(inf \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
2.175 +definition inf_fract_def:
2.176 + "(inf \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
2.177
2.178 -definition
2.179 - sup_fract_def:
2.180 - "(sup \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
2.181 +definition sup_fract_def:
2.182 + "(sup \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
2.183
2.184 -instance by intro_classes
2.185 - (auto simp add: abs_fract_def sgn_fract_def
2.186 - min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)
2.187 +instance
2.188 + by intro_classes
2.189 + (auto simp add: abs_fract_def sgn_fract_def
2.190 + min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)
2.191
2.192 end
2.193
2.194 @@ -485,8 +472,8 @@
2.195 proof -
2.196 fix a::'a and b::'a
2.197 assume b: "b < 0"
2.198 - hence "0 < -b" by simp
2.199 - hence "P (Fract (-a) (-b))" by (rule step)
2.200 + then have "0 < -b" by simp
2.201 + then have "P (Fract (-a) (-b))" by (rule step)
2.202 thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b])
2.203 qed
2.204 case (Fract a b)
3.1 --- a/src/HOL/Library/Function_Algebras.thy Tue Feb 21 13:19:16 2012 +0100
3.2 +++ b/src/HOL/Library/Function_Algebras.thy Tue Feb 21 17:09:53 2012 +0100
3.3 @@ -13,9 +13,7 @@
3.4 instantiation "fun" :: (type, plus) plus
3.5 begin
3.6
3.7 -definition
3.8 - "f + g = (\<lambda>x. f x + g x)"
3.9 -
3.10 +definition "f + g = (\<lambda>x. f x + g x)"
3.11 instance ..
3.12
3.13 end
3.14 @@ -23,9 +21,7 @@
3.15 instantiation "fun" :: (type, zero) zero
3.16 begin
3.17
3.18 -definition
3.19 - "0 = (\<lambda>x. 0)"
3.20 -
3.21 +definition "0 = (\<lambda>x. 0)"
3.22 instance ..
3.23
3.24 end
3.25 @@ -33,9 +29,7 @@
3.26 instantiation "fun" :: (type, times) times
3.27 begin
3.28
3.29 -definition
3.30 - "f * g = (\<lambda>x. f x * g x)"
3.31 -
3.32 +definition "f * g = (\<lambda>x. f x * g x)"
3.33 instance ..
3.34
3.35 end
3.36 @@ -43,9 +37,7 @@
3.37 instantiation "fun" :: (type, one) one
3.38 begin
3.39
3.40 -definition
3.41 - "1 = (\<lambda>x. 1)"
3.42 -
3.43 +definition "1 = (\<lambda>x. 1)"
3.44 instance ..
3.45
3.46 end
3.47 @@ -53,69 +45,70 @@
3.48
3.49 text {* Additive structures *}
3.50
3.51 -instance "fun" :: (type, semigroup_add) semigroup_add proof
3.52 -qed (simp add: plus_fun_def add.assoc)
3.53 +instance "fun" :: (type, semigroup_add) semigroup_add
3.54 + by default (simp add: plus_fun_def add.assoc)
3.55
3.56 -instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
3.57 -qed (simp_all add: plus_fun_def fun_eq_iff)
3.58 +instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
3.59 + by default (simp_all add: plus_fun_def fun_eq_iff)
3.60
3.61 -instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
3.62 -qed (simp add: plus_fun_def add.commute)
3.63 +instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
3.64 + by default (simp add: plus_fun_def add.commute)
3.65
3.66 -instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
3.67 -qed simp
3.68 +instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
3.69 + by default simp
3.70
3.71 -instance "fun" :: (type, monoid_add) monoid_add proof
3.72 -qed (simp_all add: plus_fun_def zero_fun_def)
3.73 +instance "fun" :: (type, monoid_add) monoid_add
3.74 + by default (simp_all add: plus_fun_def zero_fun_def)
3.75
3.76 -instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
3.77 -qed simp
3.78 +instance "fun" :: (type, comm_monoid_add) comm_monoid_add
3.79 + by default simp
3.80
3.81 instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
3.82
3.83 -instance "fun" :: (type, group_add) group_add proof
3.84 -qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
3.85 +instance "fun" :: (type, group_add) group_add
3.86 + by default
3.87 + (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
3.88
3.89 -instance "fun" :: (type, ab_group_add) ab_group_add proof
3.90 -qed (simp_all add: diff_minus)
3.91 +instance "fun" :: (type, ab_group_add) ab_group_add
3.92 + by default (simp_all add: diff_minus)
3.93
3.94
3.95 text {* Multiplicative structures *}
3.96
3.97 -instance "fun" :: (type, semigroup_mult) semigroup_mult proof
3.98 -qed (simp add: times_fun_def mult.assoc)
3.99 +instance "fun" :: (type, semigroup_mult) semigroup_mult
3.100 + by default (simp add: times_fun_def mult.assoc)
3.101
3.102 -instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
3.103 -qed (simp add: times_fun_def mult.commute)
3.104 +instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
3.105 + by default (simp add: times_fun_def mult.commute)
3.106
3.107 -instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
3.108 -qed (simp add: times_fun_def)
3.109 +instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
3.110 + by default (simp add: times_fun_def)
3.111
3.112 -instance "fun" :: (type, monoid_mult) monoid_mult proof
3.113 -qed (simp_all add: times_fun_def one_fun_def)
3.114 +instance "fun" :: (type, monoid_mult) monoid_mult
3.115 + by default (simp_all add: times_fun_def one_fun_def)
3.116
3.117 -instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
3.118 -qed simp
3.119 +instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
3.120 + by default simp
3.121
3.122
3.123 text {* Misc *}
3.124
3.125 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
3.126
3.127 -instance "fun" :: (type, mult_zero) mult_zero proof
3.128 -qed (simp_all add: zero_fun_def times_fun_def)
3.129 +instance "fun" :: (type, mult_zero) mult_zero
3.130 + by default (simp_all add: zero_fun_def times_fun_def)
3.131
3.132 -instance "fun" :: (type, zero_neq_one) zero_neq_one proof
3.133 -qed (simp add: zero_fun_def one_fun_def fun_eq_iff)
3.134 +instance "fun" :: (type, zero_neq_one) zero_neq_one
3.135 + by default (simp add: zero_fun_def one_fun_def fun_eq_iff)
3.136
3.137
3.138 text {* Ring structures *}
3.139
3.140 -instance "fun" :: (type, semiring) semiring proof
3.141 -qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
3.142 +instance "fun" :: (type, semiring) semiring
3.143 + by default (simp_all add: plus_fun_def times_fun_def algebra_simps)
3.144
3.145 -instance "fun" :: (type, comm_semiring) comm_semiring proof
3.146 -qed (simp add: plus_fun_def times_fun_def algebra_simps)
3.147 +instance "fun" :: (type, comm_semiring) comm_semiring
3.148 + by default (simp add: plus_fun_def times_fun_def algebra_simps)
3.149
3.150 instance "fun" :: (type, semiring_0) semiring_0 ..
3.151
3.152 @@ -127,8 +120,7 @@
3.153
3.154 instance "fun" :: (type, semiring_1) semiring_1 ..
3.155
3.156 -lemma of_nat_fun:
3.157 - shows "of_nat n = (\<lambda>x::'a. of_nat n)"
3.158 +lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
3.159 proof -
3.160 have comp: "comp = (\<lambda>f g x. f (g x))"
3.161 by (rule ext)+ simp
3.162 @@ -147,7 +139,8 @@
3.163
3.164 instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
3.165
3.166 -instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
3.167 +instance "fun" :: (type, semiring_char_0) semiring_char_0
3.168 +proof
3.169 from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
3.170 by (rule inj_fun)
3.171 then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
3.172 @@ -168,23 +161,24 @@
3.173
3.174 text {* Ordereded structures *}
3.175
3.176 -instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
3.177 -qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
3.178 +instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
3.179 + by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
3.180
3.181 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
3.182
3.183 -instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
3.184 -qed (simp add: plus_fun_def le_fun_def)
3.185 +instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
3.186 + by default (simp add: plus_fun_def le_fun_def)
3.187
3.188 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
3.189
3.190 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
3.191
3.192 -instance "fun" :: (type, ordered_semiring) ordered_semiring proof
3.193 -qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
3.194 +instance "fun" :: (type, ordered_semiring) ordered_semiring
3.195 + by default
3.196 + (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
3.197
3.198 -instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
3.199 -qed (fact mult_left_mono)
3.200 +instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
3.201 + by default (fact mult_left_mono)
3.202
3.203 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
3.204
4.1 --- a/src/HOL/Library/Ramsey.thy Tue Feb 21 13:19:16 2012 +0100
4.2 +++ b/src/HOL/Library/Ramsey.thy Tue Feb 21 17:09:53 2012 +0100
4.3 @@ -47,11 +47,11 @@
4.4 qed
4.5 } moreover
4.6 { assume "m\<noteq>0" "n\<noteq>0"
4.7 - hence "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
4.8 - from Suc(1)[OF this(1)] Suc(1)[OF this(2)]
4.9 + then have "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
4.10 + from Suc(1)[OF this(1)] Suc(1)[OF this(2)]
4.11 obtain r1 r2 where "r1\<ge>1" "r2\<ge>1" "?R (m - 1) n r1" "?R m (n - 1) r2"
4.12 by auto
4.13 - hence "r1+r2 \<ge> 1" by arith
4.14 + then have "r1+r2 \<ge> 1" by arith
4.15 moreover
4.16 have "?R m n (r1+r2)" (is "ALL V E. _ \<longrightarrow> ?EX V E m n")
4.17 proof clarify
4.18 @@ -62,12 +62,12 @@
4.19 let ?M = "{w : V. w\<noteq>v & {v,w} : E}"
4.20 let ?N = "{w : V. w\<noteq>v & {v,w} ~: E}"
4.21 have "V = insert v (?M \<union> ?N)" using `v : V` by auto
4.22 - hence "card V = card(insert v (?M \<union> ?N))" by metis
4.23 + then have "card V = card(insert v (?M \<union> ?N))" by metis
4.24 also have "\<dots> = card ?M + card ?N + 1" using `finite V`
4.25 by(fastforce intro: card_Un_disjoint)
4.26 finally have "card V = card ?M + card ?N + 1" .
4.27 - hence "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
4.28 - hence "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
4.29 + then have "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
4.30 + then have "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
4.31 moreover
4.32 { assume "r1 \<le> card ?M"
4.33 moreover have "finite ?M" using `finite V` by auto
4.34 @@ -82,7 +82,7 @@
4.35 with `R <= V` have "?EX V E m n" by blast
4.36 } moreover
4.37 { assume "?C"
4.38 - hence "clique (insert v R) E" using `R <= ?M`
4.39 + then have "clique (insert v R) E" using `R <= ?M`
4.40 by(auto simp:clique_def insert_commute)
4.41 moreover have "card(insert v R) = m"
4.42 using `?C` `finite R` `v ~: R` `m\<noteq>0` by simp
4.43 @@ -102,7 +102,7 @@
4.44 with `R <= V` have "?EX V E m n" by blast
4.45 } moreover
4.46 { assume "?I"
4.47 - hence "indep (insert v R) E" using `R <= ?N`
4.48 + then have "indep (insert v R) E" using `R <= ?N`
4.49 by(auto simp:indep_def insert_commute)
4.50 moreover have "card(insert v R) = n"
4.51 using `?I` `finite R` `v ~: R` `n\<noteq>0` by simp
4.52 @@ -124,17 +124,17 @@
4.53 choice_0: "choice P r 0 = (SOME x. P x)"
4.54 | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
4.55
4.56 -lemma choice_n:
4.57 +lemma choice_n:
4.58 assumes P0: "P x0"
4.59 and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
4.60 shows "P (choice P r n)"
4.61 proof (induct n)
4.62 - case 0 show ?case by (force intro: someI P0)
4.63 + case 0 show ?case by (force intro: someI P0)
4.64 next
4.65 - case Suc thus ?case by (auto intro: someI2_ex [OF Pstep])
4.66 + case Suc then show ?case by (auto intro: someI2_ex [OF Pstep])
4.67 qed
4.68
4.69 -lemma dependent_choice:
4.70 +lemma dependent_choice:
4.71 assumes trans: "trans r"
4.72 and P0: "P x0"
4.73 and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
4.74 @@ -144,7 +144,7 @@
4.75 fix n
4.76 show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep])
4.77 next
4.78 - have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"
4.79 + have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"
4.80 using Pstep [OF choice_n [OF P0 Pstep]]
4.81 by (auto intro: someI2_ex)
4.82 fix n m :: nat
4.83 @@ -156,8 +156,7 @@
4.84
4.85 subsubsection {* Partitions of a Set *}
4.86
4.87 -definition
4.88 - part :: "nat => nat => 'a set => ('a set => nat) => bool"
4.89 +definition part :: "nat => nat => 'a set => ('a set => nat) => bool"
4.90 --{*the function @{term f} partitions the @{term r}-subsets of the typically
4.91 infinite set @{term Y} into @{term s} distinct categories.*}
4.92 where
4.93 @@ -165,52 +164,52 @@
4.94
4.95 text{*For induction, we decrease the value of @{term r} in partitions.*}
4.96 lemma part_Suc_imp_part:
4.97 - "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
4.98 + "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
4.99 ==> part r s (Y - {y}) (%u. f (insert y u))"
4.100 apply(simp add: part_def, clarify)
4.101 apply(drule_tac x="insert y X" in spec)
4.102 apply(force)
4.103 done
4.104
4.105 -lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
4.106 +lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
4.107 unfolding part_def by blast
4.108 -
4.109 +
4.110
4.111 subsection {* Ramsey's Theorem: Infinitary Version *}
4.112
4.113 -lemma Ramsey_induction:
4.114 +lemma Ramsey_induction:
4.115 fixes s and r::nat
4.116 shows
4.117 - "!!(YY::'a set) (f::'a set => nat).
4.118 + "!!(YY::'a set) (f::'a set => nat).
4.119 [|infinite YY; part r s YY f|]
4.120 - ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
4.121 + ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
4.122 (\<forall>X. X \<subseteq> Y' & finite X & card X = r --> f X = t')"
4.123 proof (induct r)
4.124 case 0
4.125 - thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
4.126 + then show ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
4.127 next
4.128 - case (Suc r)
4.129 + case (Suc r)
4.130 show ?case
4.131 proof -
4.132 from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY" by blast
4.133 let ?ramr = "{((y,Y,t),(y',Y',t')). y' \<in> Y & Y' \<subseteq> Y}"
4.134 - let ?propr = "%(y,Y,t).
4.135 + let ?propr = "%(y,Y,t).
4.136 y \<in> YY & y \<notin> Y & Y \<subseteq> YY & infinite Y & t < s
4.137 & (\<forall>X. X\<subseteq>Y & finite X & card X = r --> (f o insert y) X = t)"
4.138 have infYY': "infinite (YY-{yy})" using Suc.prems by auto
4.139 have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
4.140 by (simp add: o_def part_Suc_imp_part yy Suc.prems)
4.141 - have transr: "trans ?ramr" by (force simp add: trans_def)
4.142 + have transr: "trans ?ramr" by (force simp add: trans_def)
4.143 from Suc.hyps [OF infYY' partf']
4.144 obtain Y0 and t0
4.145 where "Y0 \<subseteq> YY - {yy}" "infinite Y0" "t0 < s"
4.146 "\<forall>X. X\<subseteq>Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0"
4.147 - by blast
4.148 + by blast
4.149 with yy have propr0: "?propr(yy,Y0,t0)" by blast
4.150 - have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
4.151 + have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
4.152 proof -
4.153 fix x
4.154 - assume px: "?propr x" thus "?thesis x"
4.155 + assume px: "?propr x" then show "?thesis x"
4.156 proof (cases x)
4.157 case (fields yx Yx tx)
4.158 then obtain yx' where yx': "yx' \<in> Yx" using px
4.159 @@ -223,7 +222,7 @@
4.160 obtain Y' and t'
4.161 where Y': "Y' \<subseteq> Yx - {yx'}" "infinite Y'" "t' < s"
4.162 "\<forall>X. X\<subseteq>Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'"
4.163 - by blast
4.164 + by blast
4.165 show ?thesis
4.166 proof
4.167 show "?propr (yx',Y',t') & (x, (yx',Y',t')) \<in> ?ramr"
4.168 @@ -258,51 +257,51 @@
4.169 show ?thesis
4.170 proof (intro exI conjI)
4.171 show "?gy ` {n. ?gt n = s'} \<subseteq> YY" using pg
4.172 - by (auto simp add: Let_def split_beta)
4.173 + by (auto simp add: Let_def split_beta)
4.174 show "infinite (?gy ` {n. ?gt n = s'})" using infeqs'
4.175 - by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
4.176 + by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
4.177 show "s' < s" by (rule less')
4.178 - show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
4.179 + show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
4.180 --> f X = s'"
4.181 proof -
4.182 - {fix X
4.183 + {fix X
4.184 assume "X \<subseteq> ?gy ` {n. ?gt n = s'}"
4.185 and cardX: "finite X" "card X = Suc r"
4.186 - then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
4.187 - by (auto simp add: subset_image_iff)
4.188 + then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
4.189 + by (auto simp add: subset_image_iff)
4.190 with cardX have "AA\<noteq>{}" by auto
4.191 - hence AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
4.192 + then have AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
4.193 have "f X = s'"
4.194 - proof (cases "g (LEAST x. x \<in> AA)")
4.195 + proof (cases "g (LEAST x. x \<in> AA)")
4.196 case (fields ya Ya ta)
4.197 - with AAleast Xeq
4.198 - have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
4.199 - hence "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
4.200 - also have "... = ta"
4.201 + with AAleast Xeq
4.202 + have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
4.203 + then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
4.204 + also have "... = ta"
4.205 proof -
4.206 have "X - {ya} \<subseteq> Ya"
4.207 - proof
4.208 + proof
4.209 fix x assume x: "x \<in> X - {ya}"
4.210 - then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
4.211 - by (auto simp add: Xeq)
4.212 - hence "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
4.213 - hence lessa': "(LEAST x. x \<in> AA) < a'"
4.214 + then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
4.215 + by (auto simp add: Xeq)
4.216 + then have "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
4.217 + then have lessa': "(LEAST x. x \<in> AA) < a'"
4.218 using Least_le [of "%x. x \<in> AA", OF a'] by arith
4.219 show "x \<in> Ya" using xeq fields rg [OF lessa'] by auto
4.220 qed
4.221 moreover
4.222 have "card (X - {ya}) = r"
4.223 by (simp add: cardX ya)
4.224 - ultimately show ?thesis
4.225 + ultimately show ?thesis
4.226 using pg [of "LEAST x. x \<in> AA"] fields cardX
4.227 by (clarsimp simp del:insert_Diff_single)
4.228 qed
4.229 also have "... = s'" using AA AAleast fields by auto
4.230 finally show ?thesis .
4.231 qed}
4.232 - thus ?thesis by blast
4.233 - qed
4.234 - qed
4.235 + then show ?thesis by blast
4.236 + qed
4.237 + qed
4.238 qed
4.239 qed
4.240
4.241 @@ -312,7 +311,7 @@
4.242 shows
4.243 "[|infinite Z;
4.244 \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]
4.245 - ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
4.246 + ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
4.247 & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"
4.248 by (blast intro: Ramsey_induction [unfolded part_def])
4.249
4.250 @@ -326,7 +325,7 @@
4.251 proof -
4.252 have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
4.253 using part by (fastforce simp add: eval_nat_numeral card_Suc_eq)
4.254 - obtain Y t
4.255 + obtain Y t
4.256 where "Y \<subseteq> Z" "infinite Y" "t < s"
4.257 "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
4.258 by (insert Ramsey [OF infZ part2]) auto
4.259 @@ -342,39 +341,36 @@
4.260 \cite{Podelski-Rybalchenko}.
4.261 *}
4.262
4.263 -definition
4.264 - disj_wf :: "('a * 'a)set => bool"
4.265 -where
4.266 - "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
4.267 +definition disj_wf :: "('a * 'a)set => bool"
4.268 + where "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
4.269
4.270 -definition
4.271 - transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
4.272 -where
4.273 - "transition_idx s T A =
4.274 - (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
4.275 +definition transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
4.276 + where
4.277 + "transition_idx s T A =
4.278 + (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
4.279
4.280
4.281 lemma transition_idx_less:
4.282 "[|i<j; (s j, s i) \<in> T k; k<n|] ==> transition_idx s T {i,j} < n"
4.283 -apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
4.284 -apply (simp add: transition_idx_def, blast intro: Least_le)
4.285 +apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
4.286 +apply (simp add: transition_idx_def, blast intro: Least_le)
4.287 done
4.288
4.289 lemma transition_idx_in:
4.290 "[|i<j; (s j, s i) \<in> T k|] ==> (s j, s i) \<in> T (transition_idx s T {i,j})"
4.291 -apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
4.292 - cong: conj_cong)
4.293 -apply (erule LeastI)
4.294 +apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
4.295 + cong: conj_cong)
4.296 +apply (erule LeastI)
4.297 done
4.298
4.299 text{*To be equal to the union of some well-founded relations is equivalent
4.300 to being the subset of such a union.*}
4.301 lemma disj_wf:
4.302 "disj_wf(r) = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r \<subseteq> (\<Union>i<n. T i))"
4.303 -apply (auto simp add: disj_wf_def)
4.304 -apply (rule_tac x="%i. T i Int r" in exI)
4.305 -apply (rule_tac x=n in exI)
4.306 -apply (force simp add: wf_Int1)
4.307 +apply (auto simp add: disj_wf_def)
4.308 +apply (rule_tac x="%i. T i Int r" in exI)
4.309 +apply (rule_tac x=n in exI)
4.310 +apply (force simp add: wf_Int1)
4.311 done
4.312
4.313 theorem trans_disj_wf_implies_wf:
4.314 @@ -388,13 +384,13 @@
4.315 proof -
4.316 fix i and j::nat
4.317 assume less: "i<j"
4.318 - thus "(s j, s i) \<in> r"
4.319 + then show "(s j, s i) \<in> r"
4.320 proof (rule less_Suc_induct)
4.321 - show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
4.322 + show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
4.323 show "\<And>i j k. \<lbrakk>(s j, s i) \<in> r; (s k, s j) \<in> r\<rbrakk> \<Longrightarrow> (s k, s i) \<in> r"
4.324 - using transr by (unfold trans_def, blast)
4.325 + using transr by (unfold trans_def, blast)
4.326 qed
4.327 - qed
4.328 + qed
4.329 from dwf
4.330 obtain T and n::nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
4.331 by (auto simp add: disj_wf_def)
4.332 @@ -402,20 +398,20 @@
4.333 proof -
4.334 fix i and j::nat
4.335 assume less: "i<j"
4.336 - hence "(s j, s i) \<in> r" by (rule s [of i j])
4.337 - thus "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
4.338 - qed
4.339 + then have "(s j, s i) \<in> r" by (rule s [of i j])
4.340 + then show "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
4.341 + qed
4.342 have trless: "!!i j. i\<noteq>j ==> transition_idx s T {i,j} < n"
4.343 apply (auto simp add: linorder_neq_iff)
4.344 - apply (blast dest: s_in_T transition_idx_less)
4.345 - apply (subst insert_commute)
4.346 - apply (blast dest: s_in_T transition_idx_less)
4.347 + apply (blast dest: s_in_T transition_idx_less)
4.348 + apply (subst insert_commute)
4.349 + apply (blast dest: s_in_T transition_idx_less)
4.350 done
4.351 have
4.352 - "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
4.353 + "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
4.354 (\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
4.355 - by (rule Ramsey2) (auto intro: trless nat_infinite)
4.356 - then obtain K and k
4.357 + by (rule Ramsey2) (auto intro: trless nat_infinite)
4.358 + then obtain K and k
4.359 where infK: "infinite K" and less: "k < n" and
4.360 allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"
4.361 by auto
4.362 @@ -424,18 +420,18 @@
4.363 fix m::nat
4.364 let ?j = "enumerate K (Suc m)"
4.365 let ?i = "enumerate K m"
4.366 - have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
4.367 - have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
4.368 - have ij: "?i < ?j" by (simp add: enumerate_step infK)
4.369 - have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
4.370 + have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
4.371 + have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
4.372 + have ij: "?i < ?j" by (simp add: enumerate_step infK)
4.373 + have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
4.374 by (simp add: allk)
4.375 - obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
4.376 + obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
4.377 using s_in_T [OF ij] by blast
4.378 - thus "(s ?j, s ?i) \<in> T k"
4.379 - by (simp add: ijk [symmetric] transition_idx_in ij)
4.380 + then show "(s ?j, s ?i) \<in> T k"
4.381 + by (simp add: ijk [symmetric] transition_idx_in ij)
4.382 qed
4.383 - hence "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
4.384 - thus False using wfT less by blast
4.385 + then have "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
4.386 + then show False using wfT less by blast
4.387 qed
4.388
4.389 end
5.1 --- a/src/HOL/UNITY/Comp/Alloc.thy Tue Feb 21 13:19:16 2012 +0100
5.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy Tue Feb 21 17:09:53 2012 +0100
5.3 @@ -537,8 +537,6 @@
5.4 declare ask_inv_client_map_drop_map [simp]
5.5
5.6
5.7 -declare finite_lessThan [iff]
5.8 -
5.9 text{*Client : <unfolded specification> *}
5.10 lemmas client_spec_simps =
5.11 client_spec_def client_increasing_def client_bounded_def
6.1 --- a/src/HOL/UNITY/Comp/Progress.thy Tue Feb 21 13:19:16 2012 +0100
6.2 +++ b/src/HOL/UNITY/Comp/Progress.thy Tue Feb 21 17:09:53 2012 +0100
6.3 @@ -13,10 +13,10 @@
6.4 text{*Thesis Section 4.4.2*}
6.5
6.6 definition FF :: "int program" where
6.7 - "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
6.8 + "FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
6.9
6.10 definition GG :: "int program" where
6.11 - "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
6.12 + "GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
6.13
6.14 subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
6.15
7.1 --- a/src/HOL/UNITY/ELT.thy Tue Feb 21 13:19:16 2012 +0100
7.2 +++ b/src/HOL/UNITY/ELT.thy Tue Feb 21 17:09:53 2012 +0100
7.3 @@ -166,7 +166,7 @@
7.4 apply (erule leadsETo_induct)
7.5 prefer 3 apply (blast intro: leadsETo_Union)
7.6 prefer 2 apply (blast intro: leadsETo_Trans)
7.7 -apply (blast intro: leadsETo_Basis)
7.8 +apply blast
7.9 done
7.10
7.11 lemma leadsETo_Trans_Un:
7.12 @@ -237,7 +237,7 @@
7.13 lemma leadsETo_givenBy:
7.14 "[| F : A leadsTo[CC] A'; CC <= givenBy v |]
7.15 ==> F : A leadsTo[givenBy v] A'"
7.16 -by (blast intro: empty_mem_givenBy leadsETo_weaken)
7.17 +by (blast intro: leadsETo_weaken)
7.18
7.19
7.20 (*Set difference*)
7.21 @@ -340,7 +340,7 @@
7.22 apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
7.23 apply (rule leadsETo_Basis)
7.24 apply (auto simp add: Diff_eq_empty_iff [THEN iffD2]
7.25 - Int_Diff ensures_def givenBy_eq_Collect Join_transient)
7.26 + Int_Diff ensures_def givenBy_eq_Collect)
7.27 prefer 3 apply (blast intro: transient_strengthen)
7.28 apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
7.29 apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
7.30 @@ -454,7 +454,7 @@
7.31 lemma lel_lemma:
7.32 "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B"
7.33 apply (erule leadsTo_induct)
7.34 - apply (blast intro: reachable_ensures leadsETo_Basis)
7.35 + apply (blast intro: reachable_ensures)
7.36 apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
7.37 apply (subst Int_Union)
7.38 apply (blast intro: leadsETo_UN)
7.39 @@ -491,7 +491,7 @@
7.40 ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]
7.41 (extend_set h B)"
7.42 apply (erule leadsETo_induct)
7.43 - apply (force intro: leadsETo_Basis subset_imp_ensures
7.44 + apply (force intro: subset_imp_ensures
7.45 simp add: extend_ensures extend_set_Diff_distrib [symmetric])
7.46 apply (blast intro: leadsETo_Trans)
7.47 apply (simp add: leadsETo_UN extend_set_Union)
8.1 --- a/src/HOL/UNITY/Extend.thy Tue Feb 21 13:19:16 2012 +0100
8.2 +++ b/src/HOL/UNITY/Extend.thy Tue Feb 21 17:09:53 2012 +0100
8.3 @@ -370,9 +370,7 @@
8.4
8.5 lemma (in Extend) Allowed_extend:
8.6 "Allowed (extend h F) = project h UNIV -` Allowed F"
8.7 -apply (simp (no_asm) add: AllowedActs_extend Allowed_def)
8.8 -apply blast
8.9 -done
8.10 +by (auto simp add: Allowed_def)
8.11
8.12 lemma (in Extend) extend_SKIP [simp]: "extend h SKIP = SKIP"
8.13 apply (unfold SKIP_def)
8.14 @@ -634,7 +632,7 @@
8.15 "extend h F \<in> AU leadsTo BU
8.16 ==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
8.17 apply (erule leadsTo_induct)
8.18 - apply (blast intro: extend_ensures_slice leadsTo_Basis)
8.19 + apply (blast intro: extend_ensures_slice)
8.20 apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
8.21 apply (simp add: leadsTo_UN slice_Union)
8.22 done
8.23 @@ -682,7 +680,7 @@
8.24 "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
8.25 apply (rule program_equalityI)
8.26 apply (simp add: project_set_extend_set_Int)
8.27 - apply (simp add: image_eq_UN UN_Un, auto)
8.28 + apply (auto simp add: image_eq_UN)
8.29 done
8.30
8.31 lemma (in Extend) extend_Join_eq_extend_D:
9.1 --- a/src/HOL/UNITY/Guar.thy Tue Feb 21 13:19:16 2012 +0100
9.2 +++ b/src/HOL/UNITY/Guar.thy Tue Feb 21 17:09:53 2012 +0100
9.3 @@ -17,7 +17,7 @@
9.4 begin
9.5
9.6 instance program :: (type) order
9.7 -proof qed (auto simp add: program_less_le dest: component_antisym intro: component_refl component_trans)
9.8 + by default (auto simp add: program_less_le dest: component_antisym intro: component_trans)
9.9
9.10 text{*Existential and Universal properties. I formalize the two-program
9.11 case, proving equivalence with Chandy and Sanders's n-ary definitions*}
10.1 --- a/src/HOL/UNITY/Lift_prog.thy Tue Feb 21 13:19:16 2012 +0100
10.2 +++ b/src/HOL/UNITY/Lift_prog.thy Tue Feb 21 17:09:53 2012 +0100
10.3 @@ -120,7 +120,7 @@
10.4 else if i<j then insert_map j t (f(i:=s))
10.5 else insert_map j t (f(i - Suc 0 := s)))"
10.6 apply (rule ext)
10.7 -apply (simp split add: nat_diff_split)
10.8 +apply (simp split add: nat_diff_split)
10.9 txt{*This simplification is VERY slow*}
10.10 done
10.11
10.12 @@ -254,7 +254,7 @@
10.13 lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
10.14 apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
10.15 apply (simp add: lift_def rename_preserves)
10.16 -apply (simp add: lift_map_def o_def split_def del: split_comp_eq)
10.17 +apply (simp add: lift_map_def o_def split_def)
10.18 done
10.19
10.20 lemma delete_map_eqE':
10.21 @@ -327,9 +327,9 @@
10.22 ==> lift i F \<in> preserves (v o sub j o fst) =
10.23 (if i=j then F \<in> preserves (v o fst) else True)"
10.24 apply (drule subset_preserves_o [THEN subsetD])
10.25 -apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
10.26 +apply (simp add: lift_preserves_eq o_def)
10.27 apply (auto cong del: if_weak_cong
10.28 - simp add: lift_map_def eq_commute split_def o_def simp del:split_comp_eq)
10.29 + simp add: lift_map_def eq_commute split_def o_def)
10.30 done
10.31
10.32
10.33 @@ -409,10 +409,10 @@
10.34 by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
10.35
10.36 lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
10.37 -by (simp add: lift_def Allowed_rename)
10.38 +by (simp add: lift_def)
10.39
10.40 lemma lift_image_preserves:
10.41 "lift i ` preserves v = preserves (v o drop_map i)"
10.42 -by (simp add: rename_image_preserves lift_def inv_lift_map_eq)
10.43 +by (simp add: rename_image_preserves lift_def)
10.44
10.45 end
11.1 --- a/src/HOL/UNITY/ListOrder.thy Tue Feb 21 13:19:16 2012 +0100
11.2 +++ b/src/HOL/UNITY/ListOrder.thy Tue Feb 21 17:09:53 2012 +0100
11.3 @@ -208,7 +208,7 @@
11.4 "[| refl r; (xs,ys) : genPrefix r; length xs = length ys |]
11.5 ==> (xs@zs, ys @ zs) : genPrefix r"
11.6 apply (drule genPrefix_take_append, assumption)
11.7 -apply (simp add: take_all)
11.8 +apply simp
11.9 done
11.10
11.11
11.12 @@ -301,14 +301,10 @@
11.13 (** recursion equations **)
11.14
11.15 lemma Nil_prefix [iff]: "[] <= xs"
11.16 -apply (unfold prefix_def)
11.17 -apply (simp add: Nil_genPrefix)
11.18 -done
11.19 +by (simp add: prefix_def)
11.20
11.21 lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
11.22 -apply (unfold prefix_def)
11.23 -apply (simp add: genPrefix_Nil)
11.24 -done
11.25 +by (simp add: prefix_def)
11.26
11.27 lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
11.28 by (simp add: prefix_def)
12.1 --- a/src/HOL/UNITY/PPROD.thy Tue Feb 21 13:19:16 2012 +0100
12.2 +++ b/src/HOL/UNITY/PPROD.thy Tue Feb 21 17:09:53 2012 +0100
12.3 @@ -29,7 +29,7 @@
12.4 by (simp add: PLam_def)
12.5
12.6 lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
12.7 -by (simp add: PLam_def lift_SKIP JN_constant)
12.8 +by (simp add: PLam_def JN_constant)
12.9
12.10 lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
12.11 by (unfold PLam_def, auto)
13.1 --- a/src/HOL/UNITY/Rename.thy Tue Feb 21 13:19:16 2012 +0100
13.2 +++ b/src/HOL/UNITY/Rename.thy Tue Feb 21 17:09:53 2012 +0100
13.3 @@ -64,7 +64,7 @@
13.4 apply (simp add: bij_extend_act_eq_project_act)
13.5 apply (rule surjI)
13.6 apply (rule Extend.extend_act_inverse)
13.7 -apply (blast intro: bij_imp_bij_inv good_map_bij)
13.8 +apply (blast intro: bij_imp_bij_inv)
13.9 done
13.10
13.11 lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))"
14.1 --- a/src/HOL/UNITY/UNITY.thy Tue Feb 21 13:19:16 2012 +0100
14.2 +++ b/src/HOL/UNITY/UNITY.thy Tue Feb 21 17:09:53 2012 +0100
14.3 @@ -58,9 +58,6 @@
14.4 "increasing f == \<Inter>z. stable {s. z \<le> f s}"
14.5
14.6
14.7 -text{*Perhaps HOL shouldn't add this in the first place!*}
14.8 -declare image_Collect [simp del]
14.9 -
14.10 subsubsection{*The abstract type of programs*}
14.11
14.12 lemmas program_typedef =
14.13 @@ -73,7 +70,7 @@
14.14 done
14.15
14.16 lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
14.17 -by (simp add: insert_absorb Id_in_Acts)
14.18 +by (simp add: insert_absorb)
14.19
14.20 lemma Acts_nonempty [simp]: "Acts F \<noteq> {}"
14.21 by auto
14.22 @@ -84,7 +81,7 @@
14.23 done
14.24
14.25 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
14.26 -by (simp add: insert_absorb Id_in_AllowedActs)
14.27 +by (simp add: insert_absorb)
14.28
14.29 subsubsection{*Inspectors for type "program"*}
14.30
15.1 --- a/src/HOL/UNITY/Union.thy Tue Feb 21 13:19:16 2012 +0100
15.2 +++ b/src/HOL/UNITY/Union.thy Tue Feb 21 17:09:53 2012 +0100
15.3 @@ -202,7 +202,7 @@
15.4
15.5 lemma Join_unless [simp]:
15.6 "(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
15.7 -by (simp add: Join_constrains unless_def)
15.8 +by (simp add: unless_def)
15.9
15.10 (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
15.11 reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
15.12 @@ -238,12 +238,12 @@
15.13 lemma Join_increasing [simp]:
15.14 "(F\<squnion>G \<in> increasing f) =
15.15 (F \<in> increasing f & G \<in> increasing f)"
15.16 -by (simp add: increasing_def Join_stable, blast)
15.17 +by (auto simp add: increasing_def)
15.18
15.19 lemma invariant_JoinI:
15.20 "[| F \<in> invariant A; G \<in> invariant A |]
15.21 ==> F\<squnion>G \<in> invariant A"
15.22 -by (simp add: invariant_def, blast)
15.23 +by (auto simp add: invariant_def)
15.24
15.25 lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
15.26 by (simp add: FP_def JN_stable INTER_eq)
15.27 @@ -262,10 +262,10 @@
15.28 by (auto simp add: bex_Un transient_def Join_def)
15.29
15.30 lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A"
15.31 -by (simp add: Join_transient)
15.32 +by simp
15.33
15.34 lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
15.35 -by (simp add: Join_transient)
15.36 +by simp
15.37
15.38 (*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
15.39 lemma JN_ensures:
15.40 @@ -278,7 +278,7 @@
15.41 "F\<squnion>G \<in> A ensures B =
15.42 (F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &
15.43 (F \<in> transient (A-B) | G \<in> transient (A-B)))"
15.44 -by (auto simp add: ensures_def Join_transient)
15.45 +by (auto simp add: ensures_def)
15.46
15.47 lemma stable_Join_constrains:
15.48 "[| F \<in> stable A; G \<in> A co A' |]
16.1 --- a/src/Pure/PIDE/text.scala Tue Feb 21 13:19:16 2012 +0100
16.2 +++ b/src/Pure/PIDE/text.scala Tue Feb 21 17:09:53 2012 +0100
16.3 @@ -74,6 +74,8 @@
16.4 {
16.5 val empty: Perspective = Perspective(Nil)
16.6
16.7 + def full: Perspective = Perspective(List(Range(0, Integer.MAX_VALUE / 2)))
16.8 +
16.9 def apply(ranges: Seq[Range]): Perspective =
16.10 {
16.11 val result = new mutable.ListBuffer[Text.Range]
17.1 --- a/src/Pure/System/session.scala Tue Feb 21 13:19:16 2012 +0100
17.2 +++ b/src/Pure/System/session.scala Tue Feb 21 17:09:53 2012 +0100
17.3 @@ -216,7 +216,7 @@
17.4
17.5 /* delayed command changes */
17.6
17.7 - object commands_changed_delay
17.8 + object delay_commands_changed
17.9 {
17.10 private var changed_nodes: Set[Document.Node.Name] = Set.empty
17.11 private var changed_commands: Set[Command] = Set.empty
17.12 @@ -299,7 +299,7 @@
17.13 //{{{
17.14 {
17.15 val cmds = global_state.change_yield(_.assign(id, assign))
17.16 - for (cmd <- cmds) commands_changed_delay.invoke(cmd)
17.17 + for (cmd <- cmds) delay_commands_changed.invoke(cmd)
17.18 }
17.19 //}}}
17.20
17.21 @@ -359,7 +359,7 @@
17.22 case Position.Id(state_id) if !result.is_raw =>
17.23 try {
17.24 val st = global_state.change_yield(_.accumulate(state_id, result.message))
17.25 - commands_changed_delay.invoke(st.command)
17.26 + delay_commands_changed.invoke(st.command)
17.27 }
17.28 catch {
17.29 case _: Document.State.Fail => bad_result(result)
17.30 @@ -430,8 +430,8 @@
17.31 //{{{
17.32 var finished = false
17.33 while (!finished) {
17.34 - receiveWithin(commands_changed_delay.flush_timeout) {
17.35 - case TIMEOUT => commands_changed_delay.flush()
17.36 + receiveWithin(delay_commands_changed.flush_timeout) {
17.37 + case TIMEOUT => delay_commands_changed.flush()
17.38
17.39 case Start(timeout, args) if prover.isEmpty =>
17.40 if (phase == Session.Inactive || phase == Session.Failed) {
18.1 --- a/src/Pure/System/swing_thread.scala Tue Feb 21 13:19:16 2012 +0100
18.2 +++ b/src/Pure/System/swing_thread.scala Tue Feb 21 17:09:53 2012 +0100
18.3 @@ -53,7 +53,7 @@
18.4 val timer = new Timer(time.ms.toInt, listener)
18.5 timer.setRepeats(false)
18.6
18.7 - def invoke() { now { if (first) timer.start() else timer.restart() } }
18.8 + def invoke() { later { if (first) timer.start() else timer.restart() } }
18.9 invoke _
18.10 }
18.11
19.1 --- a/src/Tools/jEdit/lib/Tools/jedit Tue Feb 21 13:19:16 2012 +0100
19.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Feb 21 17:09:53 2012 +0100
19.3 @@ -25,6 +25,7 @@
19.4 "src/scala_console.scala"
19.5 "src/session_dockable.scala"
19.6 "src/text_area_painter.scala"
19.7 + "src/text_overview.scala"
19.8 "src/token_markup.scala"
19.9 )
19.10
20.1 --- a/src/Tools/jEdit/src/document_view.scala Tue Feb 21 13:19:16 2012 +0100
20.2 +++ b/src/Tools/jEdit/src/document_view.scala Tue Feb 21 17:09:53 2012 +0100
20.3 @@ -10,17 +10,16 @@
20.4
20.5 import isabelle._
20.6
20.7 -import scala.annotation.tailrec
20.8 import scala.collection.mutable
20.9 import scala.collection.immutable.SortedMap
20.10 import scala.actors.Actor._
20.11
20.12 import java.lang.System
20.13 import java.text.BreakIterator
20.14 -import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
20.15 -import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
20.16 +import java.awt.{Color, Graphics2D, Point}
20.17 +import java.awt.event.{MouseMotionAdapter, MouseEvent,
20.18 FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
20.19 -import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
20.20 +import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory}
20.21 import javax.swing.event.{CaretListener, CaretEvent}
20.22
20.23 import org.gjt.sp.util.Log
20.24 @@ -348,83 +347,12 @@
20.25 }
20.26
20.27
20.28 - /* overview of command status left of scrollbar */
20.29 + /* text status overview left of scrollbar */
20.30
20.31 - private val overview = new JPanel(new BorderLayout)
20.32 + private val overview = new Text_Overview(this)
20.33 {
20.34 - private val WIDTH = 10
20.35 - private val HEIGHT = 2
20.36 -
20.37 - private def lines(): Int = model.buffer.getLineCount max text_area.getVisibleLines
20.38 -
20.39 - setPreferredSize(new Dimension(WIDTH, 0))
20.40 -
20.41 - setRequestFocusEnabled(false)
20.42 -
20.43 - addMouseListener(new MouseAdapter {
20.44 - override def mousePressed(event: MouseEvent) {
20.45 - val line = (event.getY * lines()) / getHeight
20.46 - if (line >= 0 && line < text_area.getLineCount)
20.47 - text_area.setCaretPosition(text_area.getLineStartOffset(line))
20.48 - }
20.49 - })
20.50 -
20.51 - override def addNotify() {
20.52 - super.addNotify()
20.53 - ToolTipManager.sharedInstance.registerComponent(this)
20.54 - }
20.55 -
20.56 - override def removeNotify() {
20.57 - ToolTipManager.sharedInstance.unregisterComponent(this)
20.58 - super.removeNotify
20.59 - }
20.60 -
20.61 - override def paintComponent(gfx: Graphics)
20.62 - {
20.63 - super.paintComponent(gfx)
20.64 - Swing_Thread.assert()
20.65 -
20.66 - robust_body(()) {
20.67 - val buffer = model.buffer
20.68 - Isabelle.buffer_lock(buffer) {
20.69 - val snapshot = update_snapshot()
20.70 -
20.71 - gfx.setColor(getBackground)
20.72 - gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
20.73 -
20.74 - val line_count = buffer.getLineCount
20.75 - val char_count = buffer.getLength
20.76 -
20.77 - val L = lines()
20.78 - val H = getHeight()
20.79 -
20.80 - @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
20.81 - {
20.82 - if (l < line_count && h < H) {
20.83 - val p1 = p + H
20.84 - val q1 = q + HEIGHT * L
20.85 - val (l1, h1) =
20.86 - if (p1 >= q1) (l + 1, h + (p1 - q) / L)
20.87 - else (l + (q1 - p) / H, h + HEIGHT)
20.88 -
20.89 - val start = buffer.getLineStartOffset(l)
20.90 - val end =
20.91 - if (l1 < line_count) buffer.getLineStartOffset(l1)
20.92 - else char_count
20.93 -
20.94 - Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
20.95 - case None =>
20.96 - case Some(color) =>
20.97 - gfx.setColor(color)
20.98 - gfx.fillRect(0, h, getWidth, h1 - h)
20.99 - }
20.100 - paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
20.101 - }
20.102 - }
20.103 - paint_loop(0, 0, 0, 0)
20.104 - }
20.105 - }
20.106 - }
20.107 + val delay_repaint =
20.108 + Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
20.109 }
20.110
20.111
20.112 @@ -442,7 +370,7 @@
20.113 if (updated ||
20.114 (changed.nodes.contains(model.name) &&
20.115 changed.commands.exists(snapshot.node.commands.contains)))
20.116 - overview.repaint()
20.117 + overview.delay_repaint()
20.118
20.119 if (updated) invalidate_range(visible)
20.120 else {
21.1 --- a/src/Tools/jEdit/src/output_dockable.scala Tue Feb 21 13:19:16 2012 +0100
21.2 +++ b/src/Tools/jEdit/src/output_dockable.scala Tue Feb 21 17:09:53 2012 +0100
21.3 @@ -132,7 +132,7 @@
21.4 /* resize */
21.5
21.6 addComponentListener(new ComponentAdapter {
21.7 - val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
21.8 + val delay = Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
21.9 override def componentResized(e: ComponentEvent) { delay() }
21.10 })
21.11
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/src/Tools/jEdit/src/text_overview.scala Tue Feb 21 17:09:53 2012 +0100
22.3 @@ -0,0 +1,97 @@
22.4 +/* Title: Tools/jEdit/src/text_overview.scala
22.5 + Author: Makarius
22.6 +
22.7 +Swing component for text status overview.
22.8 +*/
22.9 +
22.10 +package isabelle.jedit
22.11 +
22.12 +
22.13 +import isabelle._
22.14 +
22.15 +import scala.annotation.tailrec
22.16 +
22.17 +import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension}
22.18 +import java.awt.event.{MouseAdapter, MouseEvent}
22.19 +import javax.swing.{JPanel, ToolTipManager}
22.20 +
22.21 +
22.22 +class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout)
22.23 +{
22.24 + private val text_area = doc_view.text_area
22.25 + private val buffer = doc_view.model.buffer
22.26 +
22.27 + private val WIDTH = 10
22.28 + private val HEIGHT = 2
22.29 +
22.30 + private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
22.31 +
22.32 + setPreferredSize(new Dimension(WIDTH, 0))
22.33 +
22.34 + setRequestFocusEnabled(false)
22.35 +
22.36 + addMouseListener(new MouseAdapter {
22.37 + override def mousePressed(event: MouseEvent) {
22.38 + val line = (event.getY * lines()) / getHeight
22.39 + if (line >= 0 && line < text_area.getLineCount)
22.40 + text_area.setCaretPosition(text_area.getLineStartOffset(line))
22.41 + }
22.42 + })
22.43 +
22.44 + override def addNotify() {
22.45 + super.addNotify()
22.46 + ToolTipManager.sharedInstance.registerComponent(this)
22.47 + }
22.48 +
22.49 + override def removeNotify() {
22.50 + ToolTipManager.sharedInstance.unregisterComponent(this)
22.51 + super.removeNotify
22.52 + }
22.53 +
22.54 + override def paintComponent(gfx: Graphics)
22.55 + {
22.56 + super.paintComponent(gfx)
22.57 + Swing_Thread.assert()
22.58 +
22.59 + doc_view.robust_body(()) {
22.60 + Isabelle.buffer_lock(buffer) {
22.61 + val snapshot = doc_view.update_snapshot()
22.62 +
22.63 + gfx.setColor(getBackground)
22.64 + gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
22.65 +
22.66 + val line_count = buffer.getLineCount
22.67 + val char_count = buffer.getLength
22.68 +
22.69 + val L = lines()
22.70 + val H = getHeight()
22.71 +
22.72 + @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
22.73 + {
22.74 + if (l < line_count && h < H) {
22.75 + val p1 = p + H
22.76 + val q1 = q + HEIGHT * L
22.77 + val (l1, h1) =
22.78 + if (p1 >= q1) (l + 1, h + (p1 - q) / L)
22.79 + else (l + (q1 - p) / H, h + HEIGHT)
22.80 +
22.81 + val start = buffer.getLineStartOffset(l)
22.82 + val end =
22.83 + if (l1 < line_count) buffer.getLineStartOffset(l1)
22.84 + else char_count
22.85 +
22.86 + Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
22.87 + case None =>
22.88 + case Some(color) =>
22.89 + gfx.setColor(color)
22.90 + gfx.fillRect(0, h, getWidth, h1 - h)
22.91 + }
22.92 + paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
22.93 + }
22.94 + }
22.95 + paint_loop(0, 0, 0, 0)
22.96 + }
22.97 + }
22.98 + }
22.99 +}
22.100 +