--- 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 @@
by (auto simp add: pow2_def)
lemma pow2_int: "pow2 (int c) = 2^c"
-by (simp add: pow2_def)
+ by (simp add: pow2_def)
-lemma zero_less_pow2[simp]:
- "0 < pow2 x"
+lemma zero_less_pow2[simp]: "0 < pow2 x"
by (simp add: pow2_powr)
-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 @@
auto simp add: pow2_int[symmetric] pow2_add[symmetric])
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 @@
by (cases a, cases b) (simp add: times_float.simps pow2_add)
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"
by (auto simp add: one_float_def)
@@ -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
- add_fract_def:
+definition add_fract_def:
"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 @@
with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2)
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)"
by (simp add: divide_fract_def)
@@ -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)
- (simp add: fract_collapse)
+ show "inverse 0 = (0:: 'a fract)"
+ by (simp add: fract_expand) (simp add: fract_collapse)
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))"
by (simp add: mult_le_cancel_right)
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')"
by (simp add: mult_ac)
@@ -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 @@
text {* Additive structures *}
-instance "fun" :: (type, semigroup_add) semigroup_add proof
-qed (simp add: plus_fun_def add.assoc)
+instance "fun" :: (type, semigroup_add) semigroup_add
+ by default (simp add: plus_fun_def add.assoc)
-instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
-qed (simp_all add: plus_fun_def fun_eq_iff)
+instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
+ by default (simp_all add: plus_fun_def fun_eq_iff)
-instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
-qed (simp add: plus_fun_def add.commute)
+instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
+ by default (simp add: plus_fun_def add.commute)
-instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
-qed simp
+instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
+ by default simp
-instance "fun" :: (type, monoid_add) monoid_add proof
-qed (simp_all add: plus_fun_def zero_fun_def)
+instance "fun" :: (type, monoid_add) monoid_add
+ by default (simp_all add: plus_fun_def zero_fun_def)
-instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
-qed simp
+instance "fun" :: (type, comm_monoid_add) comm_monoid_add
+ by default simp
instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
-instance "fun" :: (type, group_add) group_add proof
-qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
+instance "fun" :: (type, group_add) group_add
+ by default
+ (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
-instance "fun" :: (type, ab_group_add) ab_group_add proof
-qed (simp_all add: diff_minus)
+instance "fun" :: (type, ab_group_add) ab_group_add
+ by default (simp_all add: diff_minus)
text {* Multiplicative structures *}
-instance "fun" :: (type, semigroup_mult) semigroup_mult proof
-qed (simp add: times_fun_def mult.assoc)
+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
-qed (simp add: times_fun_def mult.commute)
+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
-qed (simp add: times_fun_def)
+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
-qed (simp_all add: times_fun_def one_fun_def)
+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
-qed (simp_all add: zero_fun_def times_fun_def)
+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 *}
-instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
-qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
+instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
+ by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
-instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
-qed (simp add: plus_fun_def le_fun_def)
+instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
+ by default (simp add: plus_fun_def le_fun_def)
instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
-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(simp add: part_def, clarify)
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"
by (simp add: cardX ya)
- 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 (auto simp add: disj_wf_def)
-apply (rule_tac x="%i. T i Int r" in exI)
-apply (rule_tac x=n in exI)
-apply (force simp add: wf_Int1)
+apply (auto simp add: disj_wf_def)
+apply (rule_tac x="%i. T i Int r" in exI)
+apply (rule_tac x=n in exI)
+apply (force simp add: wf_Int1)
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)"
by (auto simp add: disj_wf_def)
@@ -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 (auto simp add: linorder_neq_iff)
- 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
by (simp add: allk)
- 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 ask_inv_client_map_drop_map [simp]
-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 @@
apply (erule leadsETo_induct)
prefer 3 apply (blast intro: leadsETo_Union)
prefer 2 apply (blast intro: leadsETo_Trans)
-apply (blast intro: leadsETo_Basis)
+apply blast
done
lemma leadsETo_Trans_Un:
@@ -237,7 +237,7 @@
lemma leadsETo_givenBy:
"[| F : A leadsTo[CC] A'; CC <= givenBy v |]
==> F : A leadsTo[givenBy v] A'"
-by (blast intro: empty_mem_givenBy leadsETo_weaken)
+by (blast intro: leadsETo_weaken)
(*Set difference*)
@@ -340,7 +340,7 @@
apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
apply (rule leadsETo_Basis)
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 (erule leadsTo_induct)
- apply (blast intro: reachable_ensures leadsETo_Basis)
+ apply (blast intro: reachable_ensures)
apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
apply (subst Int_Union)
apply (blast intro: leadsETo_UN)
@@ -491,7 +491,7 @@
==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]
(extend_set h B)"
apply (erule leadsETo_induct)
- apply (force intro: leadsETo_Basis subset_imp_ensures
+ apply (force intro: subset_imp_ensures
simp add: extend_ensures extend_set_Diff_distrib [symmetric])
apply (blast intro: leadsETo_Trans)
apply (simp add: leadsETo_UN extend_set_Union)
--- 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
+by (auto simp add: Allowed_def)
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 (erule leadsTo_induct)
- apply (blast intro: extend_ensures_slice leadsTo_Basis)
+ apply (blast intro: extend_ensures_slice)
apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
apply (simp add: leadsTo_UN slice_Union)
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: project_set_extend_set_Int)
- 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)
-apply (simp split add: nat_diff_split)
+apply (simp split add: nat_diff_split)
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_def rename_preserves)
-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 (simp add: lift_preserves_eq o_def)
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 @@
by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
-by (simp add: lift_def Allowed_rename)
+by (simp add: lift_def)
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)
+by (simp add: rename_image_preserves lift_def)
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 add: take_all)
+apply simp
done
@@ -301,14 +301,10 @@
(** recursion equations **)
lemma Nil_prefix [iff]: "[] <= xs"
-apply (unfold prefix_def)
-apply (simp add: Nil_genPrefix)
-done
+by (simp add: prefix_def)
lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
-apply (unfold prefix_def)
-apply (simp add: genPrefix_Nil)
-done
+by (simp add: prefix_def)
lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
by (simp add: prefix_def)
--- 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 @@
by (simp add: PLam_def)
lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
-by (simp add: PLam_def lift_SKIP JN_constant)
+by (simp add: PLam_def 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 (simp add: bij_extend_act_eq_project_act)
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"
-by (simp add: insert_absorb Id_in_Acts)
+by (simp add: insert_absorb)
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"
-by (simp add: insert_absorb Id_in_AllowedActs)
+by (simp add: insert_absorb)
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)"
-by (simp add: Join_constrains unless_def)
+by (simp add: unless_def)
(*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)
+by (auto simp add: increasing_def)
lemma invariant_JoinI:
"[| F \<in> invariant A; G \<in> invariant A |]
==> F\<squnion>G \<in> invariant A"
-by (simp add: invariant_def, blast)
+by (auto simp add: invariant_def)
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 add: Join_transient)
+by simp
lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
-by (simp add: Join_transient)
+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)
+by (auto simp add: ensures_def)
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 {
case _: Document.State.Fail => bad_result(result)
@@ -430,8 +430,8 @@
//{{{
var finished = false
while (!finished) {
- receiveWithin(commands_changed_delay.flush_timeout) {
- case TIMEOUT => commands_changed_delay.flush()
+ receiveWithin(delay_commands_changed.flush_timeout) {
+ 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.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
+import java.awt.{Color, Graphics2D, Point}
+import java.awt.event.{MouseMotionAdapter, MouseEvent,
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
-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)
-
- addMouseListener(new MouseAdapter {
- 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))
- }
- })
-
- override def addNotify() {
- super.addNotify()
- ToolTipManager.sharedInstance.registerComponent(this)
- }
-
- override def removeNotify() {
- ToolTipManager.sharedInstance.unregisterComponent(this)
- super.removeNotify
- }
-
- override def paintComponent(gfx: Graphics)
- {
- super.paintComponent(gfx)
- Swing_Thread.assert()
+ /* 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 =
+ Swing_Thread.delay_first(Isabelle.session.update_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 */
addComponentListener(new ComponentAdapter {
- 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 java.awt.event.{MouseAdapter, MouseEvent}
+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)
+
+ addMouseListener(new MouseAdapter {
+ 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))
+ }
+ })
+
+ override def addNotify() {
+ super.addNotify()
+ ToolTipManager.sharedInstance.registerComponent(this)
+ }
+
+ override def removeNotify() {
+ ToolTipManager.sharedInstance.unregisterComponent(this)
+ super.removeNotify
+ }
+
+ override def paintComponent(gfx: Graphics)
+ {
+ super.paintComponent(gfx)
+ Swing_Thread.assert()
+
+ 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)
+ }
+ }
+ }
+}
+