author wenzelm Tue, 21 Feb 2012 17:09:53 +0100 changeset 46578 1bc7e91a5c77 parent 46569 1152f98902e7 (current diff) parent 46577 e5438c5797ae (diff) child 46579 fa035a015ea8 child 46580 8d32138811cb
merged
```--- a/src/HOL/Library/Float.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/Library/Float.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -9,8 +9,7 @@
imports Complex_Main Lattice_Algebras
begin

-definition
-  pow2 :: "int \<Rightarrow> real" where
+definition pow2 :: "int \<Rightarrow> real" where
[simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"

datatype float = Float int int
@@ -30,17 +29,20 @@
primrec scale :: "float \<Rightarrow> int" where
"scale (Float a b) = b"

-instantiation float :: zero begin
+instantiation float :: zero
+begin
definition zero_float where "0 = Float 0 0"
instance ..
end

-instantiation float :: one begin
+instantiation float :: one
+begin
definition one_float where "1 = Float 1 0"
instance ..
end

-instantiation float :: number begin
+instantiation float :: number
+begin
definition number_of_float where "number_of n = Float n 0"
instance ..
end
@@ -124,13 +126,13 @@

lemma pow2_int: "pow2 (int c) = 2^c"

-lemma zero_less_pow2[simp]:
-  "0 < pow2 x"
+lemma zero_less_pow2[simp]: "0 < pow2 x"

-lemma normfloat_imp_odd_or_zero: "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
+lemma normfloat_imp_odd_or_zero:
+  "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
proof (induct f rule: normfloat.induct)
case (1 u v)
from 1 have ab: "normfloat (Float u v) = Float a b" by auto
@@ -169,7 +171,7 @@

lemma float_eq_odd_helper:
assumes odd: "odd a'"
-  and floateq: "real (Float a b) = real (Float a' b')"
+    and floateq: "real (Float a b) = real (Float a' b')"
shows "b \<le> b'"
proof -
from odd have "a' \<noteq> 0" by auto
@@ -191,8 +193,8 @@

lemma float_eq_odd:
assumes odd1: "odd a"
-  and odd2: "odd a'"
-  and floateq: "real (Float a b) = real (Float a' b')"
+    and odd2: "odd a'"
+    and floateq: "real (Float a b) = real (Float a' b')"
shows "a = a' \<and> b = b'"
proof -
from
@@ -216,7 +218,7 @@
have ab': "odd a' \<or> (a' = 0 \<and> b' = 0)" by (rule normfloat_imp_odd_or_zero[OF normg])
{
assume odd: "odd a"
-    then have "a \<noteq> 0" by (simp add: even_def, arith)
+    then have "a \<noteq> 0" by (simp add: even_def) arith
with float_eq have "a' \<noteq> 0" by auto
with ab' have "odd a'" by simp
from odd this float_eq have "a = a' \<and> b = b'" by (rule float_eq_odd)
@@ -236,7 +238,8 @@
done
qed

-instantiation float :: plus begin
+instantiation float :: plus
+begin
fun plus_float where
[simp del]: "(Float a_m a_e) + (Float b_m b_e) =
(if a_e \<le> b_e then Float (a_m + b_m * 2^(nat(b_e - a_e))) a_e
@@ -244,17 +247,20 @@
instance ..
end

-instantiation float :: uminus begin
+instantiation float :: uminus
+begin
primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
instance ..
end

-instantiation float :: minus begin
-definition minus_float where [simp del]: "(z::float) - w = z + (- w)"
+instantiation float :: minus
+begin
+definition minus_float where "(z::float) - w = z + (- w)"
instance ..
end

-instantiation float :: times begin
+instantiation float :: times
+begin
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)"
instance ..
end
@@ -265,7 +271,8 @@
primrec float_nprt :: "float \<Rightarrow> float" where
"float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))"

-instantiation float :: ord begin
+instantiation float :: ord
+begin
definition le_float_def: "z \<le> (w :: float) \<equiv> real z \<le> real w"
definition less_float_def: "z < (w :: float) \<equiv> real z < real w"
instance ..
@@ -276,7 +283,7 @@

lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
-  by (cases a) (simp add: uminus_float.simps)
+  by (cases a) simp

lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
by (cases a, cases b) (simp add: minus_float_def)
@@ -285,7 +292,7 @@

lemma real_of_float_0[simp]: "real (0 :: float) = 0"
-  by (auto simp add: zero_float_def float_zero)
+  by (auto simp add: zero_float_def)

lemma real_of_float_1[simp]: "real (1 :: float) = 1"
@@ -1161,16 +1168,20 @@
qed

definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
-"lb_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
-    l = bitlen m - int prec
-  in if l > 0 then Float (m div (2^nat l)) (e + l)
-              else Float m e)"
+  "lb_mult prec x y =
+    (case normfloat (x * y) of Float m e \<Rightarrow>
+      let
+        l = bitlen m - int prec
+      in if l > 0 then Float (m div (2^nat l)) (e + l)
+                  else Float m e)"

definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
-"ub_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
-    l = bitlen m - int prec
-  in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
-              else Float m e)"
+  "ub_mult prec x y =
+    (case normfloat (x * y) of Float m e \<Rightarrow>
+      let
+        l = bitlen m - int prec
+      in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
+                  else Float m e)"

lemma lb_mult: "real (lb_mult prec x y) \<le> real (x * y)"
proof (cases "normfloat (x * y)")
@@ -1225,7 +1236,8 @@
primrec float_abs :: "float \<Rightarrow> float" where
"float_abs (Float m e) = Float \<bar>m\<bar> e"

-instantiation float :: abs begin
+instantiation float :: abs
+begin
definition abs_float_def: "\<bar>x\<bar> = float_abs x"
instance ..
end
@@ -1290,10 +1302,10 @@
declare ceiling_fl.simps[simp del]

definition lb_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
-"lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"
+  "lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"

definition ub_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
-"ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"
+  "ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"

lemma lb_mod: fixes k :: int assumes "0 \<le> real x" and "real k * y \<le> real x" (is "?k * y \<le> ?x")
assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
@@ -1307,7 +1319,9 @@
finally show ?thesis unfolding lb_mod_def real_of_float_sub real_of_float_mult by auto
qed

-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")
+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")
assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
proof -```
```--- a/src/HOL/Library/Fraction_Field.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -2,8 +2,8 @@
Author:     Amine Chaieb, University of Cambridge
*)

-header{* A formalization of the fraction field of any integral domain
-         A generalization of Rat.thy from int to any integral domain *}
+header{* A formalization of the fraction field of any integral domain;
+         generalization of theory Rat from int to any integral domain *}

theory Fraction_Field
imports Main
@@ -14,7 +14,7 @@
subsubsection {* Construction of the type of fractions *}

definition fractrel :: "(('a::idom * 'a ) * ('a * 'a)) set" where
-  "fractrel == {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
+  "fractrel = {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"

lemma fractrel_iff [simp]:
"(x, y) \<in> fractrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
@@ -70,8 +70,7 @@

subsubsection {* Representation and basic operations *}

-definition
-  Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
+definition Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
"Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"

code_datatype Fract
@@ -95,14 +94,11 @@
instantiation fract :: (idom) "{comm_ring_1, power}"
begin

-definition
-  Zero_fract_def [code_unfold]: "0 = Fract 0 1"
+definition Zero_fract_def [code_unfold]: "0 = Fract 0 1"

-definition
-  One_fract_def [code_unfold]: "1 = Fract 1 1"
+definition One_fract_def [code_unfold]: "1 = Fract 1 1"

-definition
"q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"

@@ -117,8 +113,7 @@
qed

-definition
-  minus_fract_def:
+definition minus_fract_def:
"- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})"

lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
@@ -131,16 +126,14 @@
lemma minus_fract_cancel [simp]: "Fract (- a) (- b) = Fract a b"
by (cases "b = 0") (simp_all add: eq_fract)

-definition
-  diff_fract_def: "q - r = q + - (r::'a fract)"
+definition diff_fract_def: "q - r = q + - (r::'a fract)"

lemma diff_fract [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
using assms by (simp add: diff_fract_def diff_minus)

-definition
-  mult_fract_def:
+definition mult_fract_def:
"q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
fractrel``{(fst x * fst y, snd x * snd y)})"

@@ -238,8 +231,7 @@
instantiation fract :: (idom) field_inverse_zero
begin

-definition
-  inverse_fract_def:
+definition inverse_fract_def:
"inverse q = Abs_fract (\<Union>x \<in> Rep_fract q.
fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"

@@ -252,8 +244,7 @@
then show ?thesis by (simp add: Fract_def inverse_fract_def UN_fractrel)
qed

-definition
-  divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
+definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)"

lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
@@ -261,14 +252,15 @@
instance proof
fix q :: "'a fract"
assume "q \<noteq> 0"
-  then show "inverse q * q = 1" apply (cases q rule: Fract_cases_nonzero)
-    by (simp_all add: mult_fract  inverse_fract fract_expand eq_fract mult_commute)
+  then show "inverse q * q = 1"
+    by (cases q rule: Fract_cases_nonzero)
+      (simp_all add: fract_expand eq_fract mult_commute)
next
fix q r :: "'a fract"
show "q / r = q * inverse r" by (simp add: divide_fract_def)
next
-  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
+  show "inverse 0 = (0:: 'a fract)"
qed

end
@@ -292,7 +284,7 @@
have "?le a b c d = ?le (a * x) (b * x) c d"
proof -
from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
-      hence "?le a b c d =
+      then have "?le a b c d =
((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
also have "... = ?le (a * x) (b * x) c d"
@@ -304,7 +296,7 @@
let ?D = "b * d" and ?D' = "b' * d'"
from neq have D: "?D \<noteq> 0" by simp
from neq have "?D' \<noteq> 0" by simp
-  hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
+  then have "?le a b c d = ?le (a * ?D') (b * ?D') c d"
by (rule le_factor)
also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
@@ -320,13 +312,11 @@
instantiation fract :: (linordered_idom) linorder
begin

-definition
-  le_fract_def:
+definition le_fract_def:
"q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
{(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"

-definition
-  less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
+definition less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"

lemma le_fract [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -409,28 +399,25 @@
instantiation fract :: (linordered_idom) "{distrib_lattice, abs_if, sgn_if}"
begin

-definition
-  abs_fract_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"
+definition abs_fract_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"

-definition
-  sgn_fract_def:
-    "sgn (q::'a fract) = (if q=0 then 0 else if 0<q then 1 else - 1)"
+definition sgn_fract_def:
+  "sgn (q::'a fract) = (if q=0 then 0 else if 0<q then 1 else - 1)"

theorem abs_fract [simp]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
by (auto simp add: abs_fract_def Zero_fract_def le_less
eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split)

-definition
-  inf_fract_def:
-    "(inf \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
+definition inf_fract_def:
+  "(inf \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"

-definition
-  sup_fract_def:
-    "(sup \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
+definition sup_fract_def:
+  "(sup \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"

-instance by intro_classes
-  (auto simp add: abs_fract_def sgn_fract_def
-    min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)
+instance
+  by intro_classes
+    (auto simp add: abs_fract_def sgn_fract_def
+      min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)

end

@@ -485,8 +472,8 @@
proof -
fix a::'a and b::'a
assume b: "b < 0"
-    hence "0 < -b" by simp
-    hence "P (Fract (-a) (-b))" by (rule step)
+    then have "0 < -b" by simp
+    then have "P (Fract (-a) (-b))" by (rule step)
thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b])
qed
case (Fract a b)```
```--- a/src/HOL/Library/Function_Algebras.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/Library/Function_Algebras.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -13,9 +13,7 @@
instantiation "fun" :: (type, plus) plus
begin

-definition
-  "f + g = (\<lambda>x. f x + g x)"
-
+definition "f + g = (\<lambda>x. f x + g x)"
instance ..

end
@@ -23,9 +21,7 @@
instantiation "fun" :: (type, zero) zero
begin

-definition
-  "0 = (\<lambda>x. 0)"
-
+definition "0 = (\<lambda>x. 0)"
instance ..

end
@@ -33,9 +29,7 @@
instantiation "fun" :: (type, times) times
begin

-definition
-  "f * g = (\<lambda>x. f x * g x)"
-
+definition "f * g = (\<lambda>x. f x * g x)"
instance ..

end
@@ -43,9 +37,7 @@
instantiation "fun" :: (type, one) one
begin

-definition
-  "1 = (\<lambda>x. 1)"
-
+definition "1 = (\<lambda>x. 1)"
instance ..

end
@@ -53,69 +45,70 @@

+  by default (simp_all add: plus_fun_def fun_eq_iff)

-qed simp
+  by default simp

+  by default (simp_all add: plus_fun_def zero_fun_def)

-qed simp
+  by default simp

-qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
+  by default
+    (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)

+  by default (simp_all add: diff_minus)

text {* Multiplicative structures *}

-instance "fun" :: (type, semigroup_mult) semigroup_mult proof
+instance "fun" :: (type, semigroup_mult) semigroup_mult
+  by default (simp add: times_fun_def mult.assoc)

-instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
+instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
+  by default (simp add: times_fun_def mult.commute)

-instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
+instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
+  by default (simp add: times_fun_def)

-instance "fun" :: (type, monoid_mult) monoid_mult proof
+instance "fun" :: (type, monoid_mult) monoid_mult
+  by default (simp_all add: times_fun_def one_fun_def)

-instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
-qed simp
+instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
+  by default simp

text {* Misc *}

instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..

-instance "fun" :: (type, mult_zero) mult_zero proof
+instance "fun" :: (type, mult_zero) mult_zero
+  by default (simp_all add: zero_fun_def times_fun_def)

-instance "fun" :: (type, zero_neq_one) zero_neq_one proof
-qed (simp add: zero_fun_def one_fun_def fun_eq_iff)
+instance "fun" :: (type, zero_neq_one) zero_neq_one
+  by default (simp add: zero_fun_def one_fun_def fun_eq_iff)

text {* Ring structures *}

-instance "fun" :: (type, semiring) semiring proof
-qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
+instance "fun" :: (type, semiring) semiring
+  by default (simp_all add: plus_fun_def times_fun_def algebra_simps)

-instance "fun" :: (type, comm_semiring) comm_semiring proof
-qed (simp add: plus_fun_def times_fun_def algebra_simps)
+instance "fun" :: (type, comm_semiring) comm_semiring
+  by default (simp add: plus_fun_def times_fun_def algebra_simps)

instance "fun" :: (type, semiring_0) semiring_0 ..

@@ -127,8 +120,7 @@

instance "fun" :: (type, semiring_1) semiring_1 ..

-lemma of_nat_fun:
-  shows "of_nat n = (\<lambda>x::'a. of_nat n)"
+lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
proof -
have comp: "comp = (\<lambda>f g x. f (g x))"
by (rule ext)+ simp
@@ -147,7 +139,8 @@

instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..

-instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
+instance "fun" :: (type, semiring_char_0) semiring_char_0
+proof
from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
by (rule inj_fun)
then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
@@ -168,23 +161,24 @@

text {* Ordereded structures *}

+  by default (simp add: plus_fun_def le_fun_def)

-instance "fun" :: (type, ordered_semiring) ordered_semiring proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
+instance "fun" :: (type, ordered_semiring) ordered_semiring
+  by default
+    (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)

-instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
-qed (fact mult_left_mono)
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
+  by default (fact mult_left_mono)

instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
```
```--- a/src/HOL/Library/Ramsey.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/Library/Ramsey.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -47,11 +47,11 @@
qed
} moreover
{ assume "m\<noteq>0" "n\<noteq>0"
-    hence "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
-    from Suc(1)[OF this(1)] Suc(1)[OF this(2)]
+    then have "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
+    from Suc(1)[OF this(1)] Suc(1)[OF this(2)]
obtain r1 r2 where "r1\<ge>1" "r2\<ge>1" "?R (m - 1) n r1" "?R m (n - 1) r2"
by auto
-    hence "r1+r2 \<ge> 1" by arith
+    then have "r1+r2 \<ge> 1" by arith
moreover
have "?R m n (r1+r2)" (is "ALL V E. _ \<longrightarrow> ?EX V E m n")
proof clarify
@@ -62,12 +62,12 @@
let ?M = "{w : V. w\<noteq>v & {v,w} : E}"
let ?N = "{w : V. w\<noteq>v & {v,w} ~: E}"
have "V = insert v (?M \<union> ?N)" using `v : V` by auto
-      hence "card V = card(insert v (?M \<union> ?N))" by metis
+      then have "card V = card(insert v (?M \<union> ?N))" by metis
also have "\<dots> = card ?M + card ?N + 1" using `finite V`
by(fastforce intro: card_Un_disjoint)
finally have "card V = card ?M + card ?N + 1" .
-      hence "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
-      hence "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
+      then have "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
+      then have "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
moreover
{ assume "r1 \<le> card ?M"
moreover have "finite ?M" using `finite V` by auto
@@ -82,7 +82,7 @@
with `R <= V` have "?EX V E m n" by blast
} moreover
{ assume "?C"
-          hence "clique (insert v R) E" using `R <= ?M`
+          then have "clique (insert v R) E" using `R <= ?M`
by(auto simp:clique_def insert_commute)
moreover have "card(insert v R) = m"
using `?C` `finite R` `v ~: R` `m\<noteq>0` by simp
@@ -102,7 +102,7 @@
with `R <= V` have "?EX V E m n" by blast
} moreover
{ assume "?I"
-          hence "indep (insert v R) E" using `R <= ?N`
+          then have "indep (insert v R) E" using `R <= ?N`
by(auto simp:indep_def insert_commute)
moreover have "card(insert v R) = n"
using `?I` `finite R` `v ~: R` `n\<noteq>0` by simp
@@ -124,17 +124,17 @@
choice_0:   "choice P r 0 = (SOME x. P x)"
| choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"

-lemma choice_n:
+lemma choice_n:
assumes P0: "P x0"
and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
shows "P (choice P r n)"
proof (induct n)
-  case 0 show ?case by (force intro: someI P0)
+  case 0 show ?case by (force intro: someI P0)
next
-  case Suc thus ?case by (auto intro: someI2_ex [OF Pstep])
+  case Suc then show ?case by (auto intro: someI2_ex [OF Pstep])
qed

-lemma dependent_choice:
+lemma dependent_choice:
assumes trans: "trans r"
and P0: "P x0"
and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
@@ -144,7 +144,7 @@
fix n
show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep])
next
-  have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"
+  have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"
using Pstep [OF choice_n [OF P0 Pstep]]
by (auto intro: someI2_ex)
fix n m :: nat
@@ -156,8 +156,7 @@

subsubsection {* Partitions of a Set *}

-definition
-  part :: "nat => nat => 'a set => ('a set => nat) => bool"
+definition part :: "nat => nat => 'a set => ('a set => nat) => bool"
--{*the function @{term f} partitions the @{term r}-subsets of the typically
infinite set @{term Y} into @{term s} distinct categories.*}
where
@@ -165,52 +164,52 @@

text{*For induction, we decrease the value of @{term r} in partitions.*}
lemma part_Suc_imp_part:
-     "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
+     "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
==> part r s (Y - {y}) (%u. f (insert y u))"
apply(drule_tac x="insert y X" in spec)
apply(force)
done

-lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
+lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
unfolding part_def by blast
-
+

subsection {* Ramsey's Theorem: Infinitary Version *}

-lemma Ramsey_induction:
+lemma Ramsey_induction:
fixes s and r::nat
shows
-  "!!(YY::'a set) (f::'a set => nat).
+  "!!(YY::'a set) (f::'a set => nat).
[|infinite YY; part r s YY f|]
-      ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
+      ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
(\<forall>X. X \<subseteq> Y' & finite X & card X = r --> f X = t')"
proof (induct r)
case 0
-  thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
+  then show ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
next
-  case (Suc r)
+  case (Suc r)
show ?case
proof -
from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY" by blast
let ?ramr = "{((y,Y,t),(y',Y',t')). y' \<in> Y & Y' \<subseteq> Y}"
-    let ?propr = "%(y,Y,t).
+    let ?propr = "%(y,Y,t).
y \<in> YY & y \<notin> Y & Y \<subseteq> YY & infinite Y & t < s
& (\<forall>X. X\<subseteq>Y & finite X & card X = r --> (f o insert y) X = t)"
have infYY': "infinite (YY-{yy})" using Suc.prems by auto
have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
by (simp add: o_def part_Suc_imp_part yy Suc.prems)
-    have transr: "trans ?ramr" by (force simp add: trans_def)
+    have transr: "trans ?ramr" by (force simp add: trans_def)
from Suc.hyps [OF infYY' partf']
obtain Y0 and t0
where "Y0 \<subseteq> YY - {yy}"  "infinite Y0"  "t0 < s"
"\<forall>X. X\<subseteq>Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0"
-        by blast
+        by blast
with yy have propr0: "?propr(yy,Y0,t0)" by blast
-    have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
+    have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
proof -
fix x
-      assume px: "?propr x" thus "?thesis x"
+      assume px: "?propr x" then show "?thesis x"
proof (cases x)
case (fields yx Yx tx)
then obtain yx' where yx': "yx' \<in> Yx" using px
@@ -223,7 +222,7 @@
obtain Y' and t'
where Y': "Y' \<subseteq> Yx - {yx'}"  "infinite Y'"  "t' < s"
"\<forall>X. X\<subseteq>Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'"
-            by blast
+            by blast
show ?thesis
proof
show "?propr (yx',Y',t') & (x, (yx',Y',t')) \<in> ?ramr"
@@ -258,51 +257,51 @@
show ?thesis
proof (intro exI conjI)
show "?gy ` {n. ?gt n = s'} \<subseteq> YY" using pg
-        by (auto simp add: Let_def split_beta)
+        by (auto simp add: Let_def split_beta)
show "infinite (?gy ` {n. ?gt n = s'})" using infeqs'
-        by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
+        by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
show "s' < s" by (rule less')
-      show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
+      show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
--> f X = s'"
proof -
-        {fix X
+        {fix X
assume "X \<subseteq> ?gy ` {n. ?gt n = s'}"
and cardX: "finite X" "card X = Suc r"
-         then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
-             by (auto simp add: subset_image_iff)
+         then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
+             by (auto simp add: subset_image_iff)
with cardX have "AA\<noteq>{}" by auto
-         hence AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
+         then have AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
have "f X = s'"
-         proof (cases "g (LEAST x. x \<in> AA)")
+         proof (cases "g (LEAST x. x \<in> AA)")
case (fields ya Ya ta)
-           with AAleast Xeq
-           have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
-           hence "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
-           also have "... = ta"
+           with AAleast Xeq
+           have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
+           then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
+           also have "... = ta"
proof -
have "X - {ya} \<subseteq> Ya"
-             proof
+             proof
fix x assume x: "x \<in> X - {ya}"
-               then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
-                 by (auto simp add: Xeq)
-               hence "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
-               hence lessa': "(LEAST x. x \<in> AA) < a'"
+               then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
+                 by (auto simp add: Xeq)
+               then have "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
+               then have lessa': "(LEAST x. x \<in> AA) < a'"
using Least_le [of "%x. x \<in> AA", OF a'] by arith
show "x \<in> Ya" using xeq fields rg [OF lessa'] by auto
qed
moreover
have "card (X - {ya}) = r"
-             ultimately show ?thesis
+             ultimately show ?thesis
using pg [of "LEAST x. x \<in> AA"] fields cardX
by (clarsimp simp del:insert_Diff_single)
qed
also have "... = s'" using AA AAleast fields by auto
finally show ?thesis .
qed}
-        thus ?thesis by blast
-      qed
-    qed
+        then show ?thesis by blast
+      qed
+    qed
qed
qed

@@ -312,7 +311,7 @@
shows
"[|infinite Z;
\<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]
-  ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
+  ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
& (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"
by (blast intro: Ramsey_induction [unfolded part_def])

@@ -326,7 +325,7 @@
proof -
have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
using part by (fastforce simp add: eval_nat_numeral card_Suc_eq)
-  obtain Y t
+  obtain Y t
where "Y \<subseteq> Z" "infinite Y" "t < s"
"(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
by (insert Ramsey [OF infZ part2]) auto
@@ -342,39 +341,36 @@
\cite{Podelski-Rybalchenko}.
*}

-definition
-  disj_wf         :: "('a * 'a)set => bool"
-where
-  "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
+definition disj_wf :: "('a * 'a)set => bool"
+  where "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"

-definition
-  transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
-where
-  "transition_idx s T A =
-    (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
+definition transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
+  where
+    "transition_idx s T A =
+      (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"

lemma transition_idx_less:
"[|i<j; (s j, s i) \<in> T k; k<n|] ==> transition_idx s T {i,j} < n"
-apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
-apply (simp add: transition_idx_def, blast intro: Least_le)
+apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
+apply (simp add: transition_idx_def, blast intro: Least_le)
done

lemma transition_idx_in:
"[|i<j; (s j, s i) \<in> T k|] ==> (s j, s i) \<in> T (transition_idx s T {i,j})"
-apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
-            cong: conj_cong)
-apply (erule LeastI)
+apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
+            cong: conj_cong)
+apply (erule LeastI)
done

text{*To be equal to the union of some well-founded relations is equivalent
to being the subset of such a union.*}
lemma disj_wf:
"disj_wf(r) = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r \<subseteq> (\<Union>i<n. T i))"
-apply (rule_tac x="%i. T i Int r" in exI)
-apply (rule_tac x=n in exI)
+apply (rule_tac x="%i. T i Int r" in exI)
+apply (rule_tac x=n in exI)
done

theorem trans_disj_wf_implies_wf:
@@ -388,13 +384,13 @@
proof -
fix i and j::nat
assume less: "i<j"
-    thus "(s j, s i) \<in> r"
+    then show "(s j, s i) \<in> r"
proof (rule less_Suc_induct)
-      show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
+      show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
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"
-        using transr by (unfold trans_def, blast)
+        using transr by (unfold trans_def, blast)
qed
-  qed
+  qed
from dwf
obtain T and n::nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
@@ -402,20 +398,20 @@
proof -
fix i and j::nat
assume less: "i<j"
-    hence "(s j, s i) \<in> r" by (rule s [of i j])
-    thus "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
-  qed
+    then have "(s j, s i) \<in> r" by (rule s [of i j])
+    then show "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
+  qed
have trless: "!!i j. i\<noteq>j ==> transition_idx s T {i,j} < n"
-    apply (blast dest: s_in_T transition_idx_less)
-    apply (subst insert_commute)
-    apply (blast dest: s_in_T transition_idx_less)
+    apply (blast dest: s_in_T transition_idx_less)
+    apply (subst insert_commute)
+    apply (blast dest: s_in_T transition_idx_less)
done
have
-   "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
+   "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
(\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
-    by (rule Ramsey2) (auto intro: trless nat_infinite)
-  then obtain K and k
+    by (rule Ramsey2) (auto intro: trless nat_infinite)
+  then obtain K and k
where infK: "infinite K" and less: "k < n" and
allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"
by auto
@@ -424,18 +420,18 @@
fix m::nat
let ?j = "enumerate K (Suc m)"
let ?i = "enumerate K m"
-    have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
-    have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
-    have ij: "?i < ?j" by (simp add: enumerate_step infK)
-    have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
+    have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
+    have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
+    have ij: "?i < ?j" by (simp add: enumerate_step infK)
+    have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
-    obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
+    obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
using s_in_T [OF ij] by blast
-    thus "(s ?j, s ?i) \<in> T k"
-      by (simp add: ijk [symmetric] transition_idx_in ij)
+    then show "(s ?j, s ?i) \<in> T k"
+      by (simp add: ijk [symmetric] transition_idx_in ij)
qed
-  hence "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
-  thus False using wfT less by blast
+  then have "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
+  then show False using wfT less by blast
qed

end```
```--- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -537,8 +537,6 @@

-declare finite_lessThan [iff]
-
text{*Client : <unfolded specification> *}
lemmas client_spec_simps =
client_spec_def client_increasing_def client_bounded_def```
```--- a/src/HOL/UNITY/Comp/Progress.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Comp/Progress.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -13,10 +13,10 @@
text{*Thesis Section 4.4.2*}

definition FF :: "int program" where
-    "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
+    "FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"

definition GG :: "int program" where
-    "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
+    "GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"

subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
```
```--- a/src/HOL/UNITY/ELT.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/ELT.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -166,7 +166,7 @@
prefer 3 apply (blast intro: leadsETo_Union)
prefer 2 apply (blast intro: leadsETo_Trans)
+apply blast
done

@@ -237,7 +237,7 @@
"[| F : A leadsTo[CC] A';  CC <= givenBy v |]
==> F : A leadsTo[givenBy v] A'"

(*Set difference*)
@@ -340,7 +340,7 @@
apply (auto simp add: Diff_eq_empty_iff [THEN iffD2]
-                      Int_Diff ensures_def givenBy_eq_Collect Join_transient)
+                      Int_Diff ensures_def givenBy_eq_Collect)
prefer 3 apply (blast intro: transient_strengthen)
apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
@@ -454,7 +454,7 @@
lemma lel_lemma:
"F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B"
-  apply (blast intro: reachable_ensures leadsETo_Basis)
+  apply (blast intro: reachable_ensures)
apply (subst Int_Union)
@@ -491,7 +491,7 @@
==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]
(extend_set h B)"
-  apply (force intro: leadsETo_Basis subset_imp_ensures
+  apply (force intro: subset_imp_ensures
```--- a/src/HOL/UNITY/Extend.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Extend.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -370,9 +370,7 @@

lemma (in Extend) Allowed_extend:
"Allowed (extend h F) = project h UNIV -` Allowed F"
-apply (simp (no_asm) add: AllowedActs_extend Allowed_def)
-apply blast
-done

lemma (in Extend) extend_SKIP [simp]: "extend h SKIP = SKIP"
apply (unfold SKIP_def)
@@ -634,7 +632,7 @@
"extend h F \<in> AU leadsTo BU
==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
-  apply (blast intro: extend_ensures_slice leadsTo_Basis)
+  apply (blast intro: extend_ensures_slice)
done
@@ -682,7 +680,7 @@
"project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
apply (rule program_equalityI)
- apply (simp add: image_eq_UN UN_Un, auto)
+ apply (auto simp add: image_eq_UN)
done

lemma (in Extend) extend_Join_eq_extend_D:```
```--- a/src/HOL/UNITY/Guar.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Guar.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -17,7 +17,7 @@
begin

instance program :: (type) order
-proof qed (auto simp add: program_less_le dest: component_antisym intro: component_refl component_trans)
+  by default (auto simp add: program_less_le dest: component_antisym intro: component_trans)

text{*Existential and Universal properties.  I formalize the two-program
case, proving equivalence with Chandy and Sanders's n-ary definitions*}```
```--- a/src/HOL/UNITY/Lift_prog.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -120,7 +120,7 @@
else if i<j then insert_map j t (f(i:=s))
else insert_map j t (f(i - Suc 0 := s)))"
apply (rule ext)
txt{*This simplification is VERY slow*}
done

@@ -254,7 +254,7 @@
lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
-apply (simp add: lift_map_def o_def split_def del: split_comp_eq)
+apply (simp add: lift_map_def o_def split_def)
done

lemma delete_map_eqE':
@@ -327,9 +327,9 @@
==> lift i F \<in> preserves (v o sub j o fst) =
(if i=j then F \<in> preserves (v o fst) else True)"
apply (drule subset_preserves_o [THEN subsetD])
-apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
apply (auto cong del: if_weak_cong
-       simp add: lift_map_def eq_commute split_def o_def simp del:split_comp_eq)
+       simp add: lift_map_def eq_commute split_def o_def)
done

@@ -409,10 +409,10 @@

lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"

lemma lift_image_preserves:
"lift i ` preserves v = preserves (v o drop_map i)"
-by (simp add: rename_image_preserves lift_def inv_lift_map_eq)

end```
```--- a/src/HOL/UNITY/ListOrder.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/ListOrder.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -208,7 +208,7 @@
"[| refl r;  (xs,ys) : genPrefix r;  length xs = length ys |]
==>  (xs@zs, ys @ zs) : genPrefix r"
apply (drule genPrefix_take_append, assumption)
+apply simp
done

@@ -301,14 +301,10 @@
(** recursion equations **)

lemma Nil_prefix [iff]: "[] <= xs"
-apply (unfold prefix_def)
-done

lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
-apply (unfold prefix_def)
-done

lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
```--- a/src/HOL/UNITY/PPROD.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -29,7 +29,7 @@

lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
-by (simp add: PLam_def lift_SKIP JN_constant)

lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
by (unfold PLam_def, auto)```
```--- a/src/HOL/UNITY/Rename.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Rename.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -64,7 +64,7 @@
apply (rule surjI)
apply (rule Extend.extend_act_inverse)
-apply (blast intro: bij_imp_bij_inv good_map_bij)
+apply (blast intro: bij_imp_bij_inv)
done

lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))"```
```--- a/src/HOL/UNITY/UNITY.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -58,9 +58,6 @@
"increasing f == \<Inter>z. stable {s. z \<le> f s}"

-text{*Perhaps HOL shouldn't add this in the first place!*}
-declare image_Collect [simp del]
-
subsubsection{*The abstract type of programs*}

lemmas program_typedef =
@@ -73,7 +70,7 @@
done

lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"

lemma Acts_nonempty [simp]: "Acts F \<noteq> {}"
by auto
@@ -84,7 +81,7 @@
done

lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"

subsubsection{*Inspectors for type "program"*}
```
```--- a/src/HOL/UNITY/Union.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Union.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -202,7 +202,7 @@

lemma Join_unless [simp]:
"(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"

(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
@@ -238,12 +238,12 @@
lemma Join_increasing [simp]:
"(F\<squnion>G \<in> increasing f) =
(F \<in> increasing f & G \<in> increasing f)"
-by (simp add: increasing_def Join_stable, blast)

lemma invariant_JoinI:
"[| F \<in> invariant A; G \<in> invariant A |]
==> F\<squnion>G \<in> invariant A"

lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
by (simp add: FP_def JN_stable INTER_eq)
@@ -262,10 +262,10 @@
by (auto simp add: bex_Un transient_def Join_def)

lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A"
+by simp

lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
+by simp

(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
lemma JN_ensures:
@@ -278,7 +278,7 @@
"F\<squnion>G \<in> A ensures B =
(F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &
(F \<in> transient (A-B) | G \<in> transient (A-B)))"
-by (auto simp add: ensures_def Join_transient)

lemma stable_Join_constrains:
"[| F \<in> stable A;  G \<in> A co A' |]  ```
```--- a/src/Pure/PIDE/text.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Pure/PIDE/text.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -74,6 +74,8 @@
{
val empty: Perspective = Perspective(Nil)

+    def full: Perspective = Perspective(List(Range(0, Integer.MAX_VALUE / 2)))
+
def apply(ranges: Seq[Range]): Perspective =
{
val result = new mutable.ListBuffer[Text.Range]```
```--- a/src/Pure/System/session.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Pure/System/session.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -216,7 +216,7 @@

/* delayed command changes */

-    object commands_changed_delay
+    object delay_commands_changed
{
private var changed_nodes: Set[Document.Node.Name] = Set.empty
private var changed_commands: Set[Command] = Set.empty
@@ -299,7 +299,7 @@
//{{{
{
val cmds = global_state.change_yield(_.assign(id, assign))
-      for (cmd <- cmds) commands_changed_delay.invoke(cmd)
+      for (cmd <- cmds) delay_commands_changed.invoke(cmd)
}
//}}}

@@ -359,7 +359,7 @@
case Position.Id(state_id) if !result.is_raw =>
try {
val st = global_state.change_yield(_.accumulate(state_id, result.message))
-            commands_changed_delay.invoke(st.command)
+            delay_commands_changed.invoke(st.command)
}
catch {
@@ -430,8 +430,8 @@
//{{{
var finished = false
while (!finished) {
-        case TIMEOUT => commands_changed_delay.flush()
+        case TIMEOUT => delay_commands_changed.flush()

case Start(timeout, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {```
```--- a/src/Pure/System/swing_thread.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Pure/System/swing_thread.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -53,7 +53,7 @@
val timer = new Timer(time.ms.toInt, listener)
timer.setRepeats(false)

-    def invoke() { now { if (first) timer.start() else timer.restart() } }
+    def invoke() { later { if (first) timer.start() else timer.restart() } }
invoke _
}
```
```--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Feb 21 17:09:53 2012 +0100
@@ -25,6 +25,7 @@
"src/scala_console.scala"
"src/session_dockable.scala"
"src/text_area_painter.scala"
+  "src/text_overview.scala"
"src/token_markup.scala"
)
```
```--- a/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -10,17 +10,16 @@

import isabelle._

-import scala.annotation.tailrec
import scala.collection.mutable
import scala.collection.immutable.SortedMap
import scala.actors.Actor._

import java.lang.System
import java.text.BreakIterator
-import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
+import java.awt.{Color, Graphics2D, Point}
-import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
+import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory}
import javax.swing.event.{CaretListener, CaretEvent}

import org.gjt.sp.util.Log
@@ -348,83 +347,12 @@
}

-  /* overview of command status left of scrollbar */
-
-  private val overview = new JPanel(new BorderLayout)
-  {
-    private val WIDTH = 10
-    private val HEIGHT = 2
-
-    private def lines(): Int = model.buffer.getLineCount max text_area.getVisibleLines
-
-    setPreferredSize(new Dimension(WIDTH, 0))
-
-    setRequestFocusEnabled(false)
-
-      override def mousePressed(event: MouseEvent) {
-        val line = (event.getY * lines()) / getHeight
-        if (line >= 0 && line < text_area.getLineCount)
-          text_area.setCaretPosition(text_area.getLineStartOffset(line))
-      }
-    })
-
-      ToolTipManager.sharedInstance.registerComponent(this)
-    }
-
-    override def removeNotify() {
-      ToolTipManager.sharedInstance.unregisterComponent(this)
-      super.removeNotify
-    }
-
-    override def paintComponent(gfx: Graphics)
-    {
-      super.paintComponent(gfx)
+  /* text status overview left of scrollbar */

-      robust_body(()) {
-        val buffer = model.buffer
-        Isabelle.buffer_lock(buffer) {
-          val snapshot = update_snapshot()
-
-          gfx.setColor(getBackground)
-          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
-
-          val line_count = buffer.getLineCount
-          val char_count = buffer.getLength
-
-          val L = lines()
-          val H = getHeight()
-
-          @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
-          {
-            if (l < line_count && h < H) {
-              val p1 = p + H
-              val q1 = q + HEIGHT * L
-              val (l1, h1) =
-                if (p1 >= q1) (l + 1, h + (p1 - q) / L)
-                else (l + (q1 - p) / H, h + HEIGHT)
-
-              val start = buffer.getLineStartOffset(l)
-              val end =
-                if (l1 < line_count) buffer.getLineStartOffset(l1)
-                else char_count
-
-              Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
-                case None =>
-                case Some(color) =>
-                  gfx.setColor(color)
-                  gfx.fillRect(0, h, getWidth, h1 - h)
-              }
-              paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
-            }
-          }
-          paint_loop(0, 0, 0, 0)
-        }
-      }
-    }
+  private val overview = new Text_Overview(this)
+  {
+    val delay_repaint =
}

@@ -442,7 +370,7 @@
if (updated ||
(changed.nodes.contains(model.name) &&
changed.commands.exists(snapshot.node.commands.contains)))
-              overview.repaint()
+              overview.delay_repaint()

if (updated) invalidate_range(visible)
else {```
```--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -132,7 +132,7 @@
/* resize */

-    val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
+    val delay = Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
override def componentResized(e: ComponentEvent) { delay() }
})
```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/text_overview.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -0,0 +1,97 @@
+/*  Title:      Tools/jEdit/src/text_overview.scala
+    Author:     Makarius
+
+Swing component for text status overview.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.annotation.tailrec
+
+import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension}
+import javax.swing.{JPanel, ToolTipManager}
+
+
+class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout)
+{
+  private val text_area = doc_view.text_area
+  private val buffer = doc_view.model.buffer
+
+  private val WIDTH = 10
+  private val HEIGHT = 2
+
+  private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
+
+  setPreferredSize(new Dimension(WIDTH, 0))
+
+  setRequestFocusEnabled(false)
+
+    override def mousePressed(event: MouseEvent) {
+      val line = (event.getY * lines()) / getHeight
+      if (line >= 0 && line < text_area.getLineCount)
+        text_area.setCaretPosition(text_area.getLineStartOffset(line))
+    }
+  })
+
+    ToolTipManager.sharedInstance.registerComponent(this)
+  }
+
+  override def removeNotify() {
+    ToolTipManager.sharedInstance.unregisterComponent(this)
+    super.removeNotify
+  }
+
+  override def paintComponent(gfx: Graphics)
+  {
+    super.paintComponent(gfx)
+
+    doc_view.robust_body(()) {
+      Isabelle.buffer_lock(buffer) {
+        val snapshot = doc_view.update_snapshot()
+
+        gfx.setColor(getBackground)
+        gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
+
+        val line_count = buffer.getLineCount
+        val char_count = buffer.getLength
+
+        val L = lines()
+        val H = getHeight()
+
+        @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
+        {
+          if (l < line_count && h < H) {
+            val p1 = p + H
+            val q1 = q + HEIGHT * L
+            val (l1, h1) =
+              if (p1 >= q1) (l + 1, h + (p1 - q) / L)
+              else (l + (q1 - p) / H, h + HEIGHT)
+
+            val start = buffer.getLineStartOffset(l)
+            val end =
+              if (l1 < line_count) buffer.getLineStartOffset(l1)
+              else char_count
+
+            Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
+              case None =>
+              case Some(color) =>
+                gfx.setColor(color)
+                gfx.fillRect(0, h, getWidth, h1 - h)
+            }
+            paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
+          }
+        }
+        paint_loop(0, 0, 0, 0)
+      }
+    }
+  }
+}
+```