--- a/src/HOL/Complete_Lattice.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy Mon Aug 08 22:11:00 2011 +0200
@@ -142,14 +142,14 @@
"\<Sqinter>{} = \<top>"
by (auto intro: antisym Inf_greatest)
-lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
+lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
by (simp add: INF_def)
lemma Sup_empty [simp]:
"\<Squnion>{} = \<bottom>"
by (auto intro: antisym Sup_least)
-lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
+lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
by (simp add: SUP_def)
lemma Inf_UNIV [simp]:
@@ -172,6 +172,12 @@
lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
by (simp add: SUP_def Sup_insert)
+lemma INF_image: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
+ by (simp add: INF_def image_image)
+
+lemma SUP_image: "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
+ by (simp add: SUP_def image_image)
+
lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
@@ -684,11 +690,11 @@
lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
by (simp add: Inf_insert)
-lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
- by (fact Inf_empty)
+lemma Inter_empty: "\<Inter>{} = UNIV"
+ by (fact Inf_empty) (* already simp *)
-lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
- by (fact Inf_UNIV)
+lemma Inter_UNIV: "\<Inter>UNIV = {}"
+ by (fact Inf_UNIV) (* already simp *)
lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
by (fact Inf_insert)
@@ -785,8 +791,8 @@
lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
by (fact le_INF_I)
-lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
- by (fact INF_empty)
+lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV"
+ by (fact INF_empty) (* already simp *)
lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
by (fact INF_absorb)
@@ -994,8 +1000,8 @@
lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
by blast
-lemma UN_empty [simp, no_atp]: "(\<Union>x\<in>{}. B x) = {}"
- by (fact SUP_empty)
+lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
+ by (fact SUP_empty) (* already simp *)
lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
by (fact SUP_bot)
--- a/src/HOL/Complex.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Complex.thy Mon Aug 08 22:11:00 2011 +0200
@@ -25,14 +25,12 @@
lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
by (induct z) simp
-lemma complex_equality [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
+lemma complex_eqI [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
by (induct x, induct y) simp
-lemma expand_complex_eq: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
+lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
by (induct x, induct y) simp
-lemmas complex_Re_Im_cancel_iff = expand_complex_eq
-
subsection {* Addition and Subtraction *}
@@ -152,7 +150,7 @@
right_distrib left_distrib right_diff_distrib left_diff_distrib
complex_inverse_def complex_divide_def
power2_eq_square add_divide_distrib [symmetric]
- expand_complex_eq)
+ complex_eq_iff)
end
@@ -190,7 +188,7 @@
lemma Complex_eq_number_of [simp]:
"(Complex a b = number_of w) = (a = number_of w \<and> b = 0)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
subsection {* Scalar Multiplication *}
@@ -215,17 +213,17 @@
proof
fix a b :: real and x y :: complex
show "scaleR a (x + y) = scaleR a x + scaleR a y"
- by (simp add: expand_complex_eq right_distrib)
+ by (simp add: complex_eq_iff right_distrib)
show "scaleR (a + b) x = scaleR a x + scaleR b x"
- by (simp add: expand_complex_eq left_distrib)
+ by (simp add: complex_eq_iff left_distrib)
show "scaleR a (scaleR b x) = scaleR (a * b) x"
- by (simp add: expand_complex_eq mult_assoc)
+ by (simp add: complex_eq_iff mult_assoc)
show "scaleR 1 x = x"
- by (simp add: expand_complex_eq)
+ by (simp add: complex_eq_iff)
show "scaleR a x * y = scaleR a (x * y)"
- by (simp add: expand_complex_eq algebra_simps)
+ by (simp add: complex_eq_iff algebra_simps)
show "x * scaleR a y = scaleR a (x * y)"
- by (simp add: expand_complex_eq algebra_simps)
+ by (simp add: complex_eq_iff algebra_simps)
qed
end
@@ -405,19 +403,19 @@
by (simp add: i_def)
lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_i_not_one [simp]: "ii \<noteq> 1"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_i_not_number_of [simp]: "ii \<noteq> number_of w"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma Complex_mult_i [simp]: "Complex a b * ii = Complex (- b) a"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
by (simp add: i_def complex_of_real_def)
@@ -451,31 +449,31 @@
by (simp add: cnj_def)
lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
by (simp add: cnj_def)
lemma complex_cnj_zero [simp]: "cnj 0 = 0"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_minus: "cnj (- x) = - cnj x"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_one [simp]: "cnj 1 = 1"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)"
by (simp add: complex_inverse_def)
@@ -487,34 +485,34 @@
by (induct n, simp_all add: complex_cnj_mult)
lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_number_of [simp]: "cnj (number_of w) = number_of w"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
by (simp add: complex_norm_def)
lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_cnj_i [simp]: "cnj ii = - ii"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
-by (simp add: expand_complex_eq power2_eq_square)
+by (simp add: complex_eq_iff power2_eq_square)
lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
by (simp add: norm_mult power2_eq_square)
@@ -721,4 +719,10 @@
lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1"
by (simp add: expi_def cis_def)
+text {* Legacy theorem names *}
+
+lemmas expand_complex_eq = complex_eq_iff
+lemmas complex_Re_Im_cancel_iff = complex_eq_iff
+lemmas complex_equality = complex_eqI
+
end
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 08 22:11:00 2011 +0200
@@ -652,7 +652,7 @@
if h aconvc y then false else if h aconvc x then true else earlier t x y;
fun dest_frac ct = case term_of ct of
- Const (@{const_name Rings.divide},_) $ a $ b=>
+ Const (@{const_name Fields.divide},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
| Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| t => Rat.rat_of_int (snd (HOLogic.dest_number t))
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Aug 08 22:11:00 2011 +0200
@@ -2856,7 +2856,7 @@
fun num rT x = HOLogic.mk_number rT x;
fun rrelT rT = [rT,rT] ---> rT;
fun rrT rT = [rT, rT] ---> bT;
-fun divt rT = Const(@{const_name Rings.divide},rrelT rT);
+fun divt rT = Const(@{const_name Fields.divide},rrelT rT);
fun timest rT = Const(@{const_name Groups.times},rrelT rT);
fun plust rT = Const(@{const_name Groups.plus},rrelT rT);
fun minust rT = Const(@{const_name Groups.minus},rrelT rT);
@@ -2884,7 +2884,7 @@
| Const(@{const_name Groups.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
| Const(@{const_name Groups.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
| Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
- | Const(@{const_name Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ | Const(@{const_name Fields.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
| _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1)
handle TERM _ => @{code poly.Bound} (AList.lookup (op aconv) m t |> the));
--- a/src/HOL/Fields.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Fields.thy Mon Aug 08 22:11:00 2011 +0200
@@ -13,6 +13,225 @@
imports Rings
begin
+subsection {* Division rings *}
+
+text {*
+ A division ring is like a field, but without the commutativity requirement.
+*}
+
+class inverse =
+ fixes inverse :: "'a \<Rightarrow> 'a"
+ and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
+
+class division_ring = ring_1 + inverse +
+ assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
+ assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
+ assumes divide_inverse: "a / b = a * inverse b"
+begin
+
+subclass ring_1_no_zero_divisors
+proof
+ fix a b :: 'a
+ assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
+ show "a * b \<noteq> 0"
+ proof
+ assume ab: "a * b = 0"
+ hence "0 = inverse a * (a * b) * inverse b" by simp
+ also have "\<dots> = (inverse a * a) * (b * inverse b)"
+ by (simp only: mult_assoc)
+ also have "\<dots> = 1" using a b by simp
+ finally show False by simp
+ qed
+qed
+
+lemma nonzero_imp_inverse_nonzero:
+ "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
+proof
+ assume ianz: "inverse a = 0"
+ assume "a \<noteq> 0"
+ hence "1 = a * inverse a" by simp
+ also have "... = 0" by (simp add: ianz)
+ finally have "1 = 0" .
+ thus False by (simp add: eq_commute)
+qed
+
+lemma inverse_zero_imp_zero:
+ "inverse a = 0 \<Longrightarrow> a = 0"
+apply (rule classical)
+apply (drule nonzero_imp_inverse_nonzero)
+apply auto
+done
+
+lemma inverse_unique:
+ assumes ab: "a * b = 1"
+ shows "inverse a = b"
+proof -
+ have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
+ moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
+ ultimately show ?thesis by (simp add: mult_assoc [symmetric])
+qed
+
+lemma nonzero_inverse_minus_eq:
+ "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
+by (rule inverse_unique) simp
+
+lemma nonzero_inverse_inverse_eq:
+ "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
+by (rule inverse_unique) simp
+
+lemma nonzero_inverse_eq_imp_eq:
+ assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
+ shows "a = b"
+proof -
+ from `inverse a = inverse b`
+ have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
+ with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
+ by (simp add: nonzero_inverse_inverse_eq)
+qed
+
+lemma inverse_1 [simp]: "inverse 1 = 1"
+by (rule inverse_unique) simp
+
+lemma nonzero_inverse_mult_distrib:
+ assumes "a \<noteq> 0" and "b \<noteq> 0"
+ shows "inverse (a * b) = inverse b * inverse a"
+proof -
+ have "a * (b * inverse b) * inverse a = 1" using assms by simp
+ hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)
+ thus ?thesis by (rule inverse_unique)
+qed
+
+lemma division_ring_inverse_add:
+ "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
+by (simp add: algebra_simps)
+
+lemma division_ring_inverse_diff:
+ "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
+by (simp add: algebra_simps)
+
+lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
+proof
+ assume neq: "b \<noteq> 0"
+ {
+ hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)
+ also assume "a / b = 1"
+ finally show "a = b" by simp
+ next
+ assume "a = b"
+ with neq show "a / b = 1" by (simp add: divide_inverse)
+ }
+qed
+
+lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
+by (simp add: divide_inverse)
+
+lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
+by (simp add: divide_inverse)
+
+lemma divide_zero_left [simp]: "0 / a = 0"
+by (simp add: divide_inverse)
+
+lemma inverse_eq_divide: "inverse a = 1 / a"
+by (simp add: divide_inverse)
+
+lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
+by (simp add: divide_inverse algebra_simps)
+
+lemma divide_1 [simp]: "a / 1 = a"
+ by (simp add: divide_inverse)
+
+lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
+ by (simp add: divide_inverse mult_assoc)
+
+lemma minus_divide_left: "- (a / b) = (-a) / b"
+ by (simp add: divide_inverse)
+
+lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
+ by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
+ by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
+ by (simp add: divide_inverse)
+
+lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
+ by (simp add: diff_minus add_divide_distrib)
+
+lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
+ also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
+ also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
+ by (simp add: divide_inverse mult_assoc)
+
+lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
+ by (drule sym) (simp add: divide_inverse mult_assoc)
+
+end
+
+class division_ring_inverse_zero = division_ring +
+ assumes inverse_zero [simp]: "inverse 0 = 0"
+begin
+
+lemma divide_zero [simp]:
+ "a / 0 = 0"
+ by (simp add: divide_inverse)
+
+lemma divide_self_if [simp]:
+ "a / a = (if a = 0 then 0 else 1)"
+ by simp
+
+lemma inverse_nonzero_iff_nonzero [simp]:
+ "inverse a = 0 \<longleftrightarrow> a = 0"
+ by rule (fact inverse_zero_imp_zero, simp)
+
+lemma inverse_minus_eq [simp]:
+ "inverse (- a) = - inverse a"
+proof cases
+ assume "a=0" thus ?thesis by simp
+next
+ assume "a\<noteq>0"
+ thus ?thesis by (simp add: nonzero_inverse_minus_eq)
+qed
+
+lemma inverse_eq_imp_eq:
+ "inverse a = inverse b \<Longrightarrow> a = b"
+apply (cases "a=0 | b=0")
+ apply (force dest!: inverse_zero_imp_zero
+ simp add: eq_commute [of "0::'a"])
+apply (force dest!: nonzero_inverse_eq_imp_eq)
+done
+
+lemma inverse_eq_iff_eq [simp]:
+ "inverse a = inverse b \<longleftrightarrow> a = b"
+ by (force dest!: inverse_eq_imp_eq)
+
+lemma inverse_inverse_eq [simp]:
+ "inverse (inverse a) = a"
+proof cases
+ assume "a=0" thus ?thesis by simp
+next
+ assume "a\<noteq>0"
+ thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
+qed
+
+end
+
+subsection {* Fields *}
+
class field = comm_ring_1 + inverse +
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
assumes field_divide_inverse: "a / b = a * inverse b"
@@ -249,7 +468,7 @@
end
-text {* Ordered Fields *}
+subsection {* Ordered fields *}
class linordered_field = field + linordered_idom
begin
--- a/src/HOL/HOLCF/Fix.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/HOLCF/Fix.thy Mon Aug 08 22:11:00 2011 +0200
@@ -219,7 +219,7 @@
by (rule trans [symmetric, OF fix_eq], simp)
have 2: "snd (F\<cdot>(?x, ?y)) = ?y"
by (rule trans [symmetric, OF fix_eq], simp)
- from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: Pair_fst_snd_eq)
+ from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
next
fix z assume F_z: "F\<cdot>z = z"
obtain x y where z: "z = (x,y)" by (rule prod.exhaust)
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Mon Aug 08 22:11:00 2011 +0200
@@ -609,7 +609,7 @@
(if a:actions(asig_of(D)) then
(snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
else snd(snd(snd(t)))=snd(snd(snd(s)))))"
- apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq Let_def ioa_projections)
+ apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections)
done
--- a/src/HOL/HOLCF/Product_Cpo.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/HOLCF/Product_Cpo.thy Mon Aug 08 22:11:00 2011 +0200
@@ -46,7 +46,7 @@
next
fix x y :: "'a \<times> 'b"
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
- unfolding below_prod_def Pair_fst_snd_eq
+ unfolding below_prod_def prod_eq_iff
by (fast intro: below_antisym)
next
fix x y z :: "'a \<times> 'b"
@@ -142,7 +142,7 @@
proof
fix x y :: "'a \<times> 'b"
show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
- unfolding below_prod_def Pair_fst_snd_eq
+ unfolding below_prod_def prod_eq_iff
by simp
qed
--- a/src/HOL/HOLCF/Sprod.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/HOLCF/Sprod.thy Mon Aug 08 22:11:00 2011 +0200
@@ -63,7 +63,7 @@
lemmas Rep_sprod_simps =
Rep_sprod_inject [symmetric] below_sprod_def
- Pair_fst_snd_eq below_prod_def
+ prod_eq_iff below_prod_def
Rep_sprod_strict Rep_sprod_spair
lemma sprodE [case_names bottom spair, cases type: sprod]:
--- a/src/HOL/HOLCF/Ssum.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/HOLCF/Ssum.thy Mon Aug 08 22:11:00 2011 +0200
@@ -52,7 +52,7 @@
lemmas Rep_ssum_simps =
Rep_ssum_inject [symmetric] below_ssum_def
- Pair_fst_snd_eq below_prod_def
+ prod_eq_iff below_prod_def
Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr
subsection {* Properties of \emph{sinl} and \emph{sinr} *}
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Aug 08 22:11:00 2011 +0200
@@ -721,7 +721,7 @@
val rules0 =
@{thms iterate_0 Pair_strict} @ take_0_thms
val rules1 =
- @{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv}
+ @{thms iterate_Suc prod_eq_iff fst_conv snd_conv}
@ take_Suc_thms
val tac =
EVERY
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy Mon Aug 08 22:11:00 2011 +0200
@@ -470,7 +470,7 @@
apply (rule lub_eq)
apply (rule nat.induct)
apply (simp only: iterate_0 Pair_strict take_0_thms)
-apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv
+apply (simp only: iterate_Suc prod_eq_iff fst_conv snd_conv
foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
done
--- a/src/HOL/IMP/Big_Step.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/IMP/Big_Step.thy Mon Aug 08 22:11:00 2011 +0200
@@ -113,6 +113,10 @@
qed
qed
+(* Using rule inversion to prove simplification rules: *)
+lemma assign_simp:
+ "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
+ by auto
subsection "Command Equivalence"
--- a/src/HOL/IMP/Comp_Rev.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy Mon Aug 08 22:11:00 2011 +0200
@@ -479,9 +479,7 @@
"ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
by (induct c) auto
-lemma assign [simp]:
- "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
- by auto
+declare assign_simp [simp]
lemma ccomp_exec_n:
"ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Fold.thy Mon Aug 08 22:11:00 2011 +0200
@@ -0,0 +1,413 @@
+header "Constant Folding"
+
+theory Fold imports Sem_Equiv begin
+
+section "Simple folding of arithmetic expressions"
+
+types
+ tab = "name \<Rightarrow> val option"
+
+(* maybe better as the composition of substitution and the existing simp_const(0) *)
+fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
+"simp_const (N n) _ = N n" |
+"simp_const (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
+"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of
+ (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')"
+
+definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"
+
+theorem aval_simp_const[simp]:
+assumes "approx t s"
+shows "aval (simp_const a t) s = aval a s"
+ using assms
+ by (induct a) (auto simp: approx_def split: aexp.split option.split)
+
+theorem aval_simp_const_N:
+assumes "approx t s"
+shows "simp_const a t = N n \<Longrightarrow> aval a s = n"
+ using assms
+ by (induct a arbitrary: n)
+ (auto simp: approx_def split: aexp.splits option.splits)
+
+definition
+ "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
+
+primrec lnames :: "com \<Rightarrow> name set" where
+"lnames SKIP = {}" |
+"lnames (x ::= a) = {x}" |
+"lnames (c1; c2) = lnames c1 \<union> lnames c2" |
+"lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" |
+"lnames (WHILE b DO c) = lnames c"
+
+primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
+"defs SKIP t = t" |
+"defs (x ::= a) t =
+ (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
+"defs (c1;c2) t = (defs c2 o defs c1) t" |
+"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
+"defs (WHILE b DO c) t = t |` (-lnames c)"
+
+primrec fold where
+"fold SKIP _ = SKIP" |
+"fold (x ::= a) t = (x ::= (simp_const a t))" |
+"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))" |
+"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" |
+"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lnames c))"
+
+lemma approx_merge:
+ "approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s"
+ by (fastsimp simp: merge_def approx_def)
+
+lemma approx_map_le:
+ "approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s"
+ by (clarsimp simp: approx_def map_le_def dom_def)
+
+lemma restrict_map_le [intro!, simp]: "t |` S \<subseteq>\<^sub>m t"
+ by (clarsimp simp: restrict_map_def map_le_def)
+
+lemma merge_restrict:
+ assumes "t1 |` S = t |` S"
+ assumes "t2 |` S = t |` S"
+ shows "merge t1 t2 |` S = t |` S"
+proof -
+ from assms
+ have "\<forall>x. (t1 |` S) x = (t |` S) x"
+ and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto
+ thus ?thesis
+ by (auto simp: merge_def restrict_map_def
+ split: if_splits intro: ext)
+qed
+
+
+lemma defs_restrict:
+ "defs c t |` (- lnames c) = t |` (- lnames c)"
+proof (induct c arbitrary: t)
+ case (Semi c1 c2)
+ hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)"
+ by simp
+ hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
+ t |` (- lnames c1) |` (-lnames c2)" by simp
+ moreover
+ from Semi
+ have "defs c2 (defs c1 t) |` (- lnames c2) =
+ defs c1 t |` (- lnames c2)"
+ by simp
+ hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =
+ defs c1 t |` (- lnames c2) |` (- lnames c1)"
+ by simp
+ ultimately
+ show ?case by (clarsimp simp: Int_commute)
+next
+ case (If b c1 c2)
+ hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
+ hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
+ t |` (- lnames c1) |` (-lnames c2)" by simp
+ moreover
+ from If
+ have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
+ hence "defs c2 t |` (- lnames c2) |` (-lnames c1) =
+ t |` (- lnames c2) |` (-lnames c1)" by simp
+ ultimately
+ show ?case by (auto simp: Int_commute intro: merge_restrict)
+qed (auto split: aexp.split)
+
+
+lemma big_step_pres_approx:
+ "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
+proof (induct arbitrary: t rule: big_step_induct)
+ case Skip thus ?case by simp
+next
+ case Assign
+ thus ?case
+ by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
+next
+ case (Semi c1 s1 s2 c2 s3)
+ have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
+ hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4))
+ thus ?case by simp
+next
+ case (IfTrue b s c1 s')
+ hence "approx (defs c1 t) s'" by simp
+ thus ?case by (simp add: approx_merge)
+next
+ case (IfFalse b s c2 s')
+ hence "approx (defs c2 t) s'" by simp
+ thus ?case by (simp add: approx_merge)
+next
+ case WhileFalse
+ thus ?case by (simp add: approx_def restrict_map_def)
+next
+ case (WhileTrue b s1 c s2 s3)
+ hence "approx (defs c t) s2" by simp
+ with WhileTrue
+ have "approx (defs c t |` (-lnames c)) s3" by simp
+ thus ?case by (simp add: defs_restrict)
+qed
+
+corollary approx_defs_inv [simp]:
+ "\<Turnstile> {approx t} c {approx (defs c t)}"
+ by (simp add: hoare_valid_def big_step_pres_approx)
+
+
+lemma big_step_pres_approx_restrict:
+ "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
+proof (induct arbitrary: t rule: big_step_induct)
+ case Assign
+ thus ?case by (clarsimp simp: approx_def)
+next
+ case (Semi c1 s1 s2 c2 s3)
+ hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1"
+ by (simp add: Int_commute)
+ hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
+ by (rule Semi)
+ hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"
+ by (simp add: Int_commute)
+ hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"
+ by (rule Semi)
+ thus ?case by simp
+next
+ case (IfTrue b s c1 s' c2)
+ hence "approx (t |` (-lnames c2) |` (-lnames c1)) s"
+ by (simp add: Int_commute)
+ hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'"
+ by (rule IfTrue)
+ thus ?case by (simp add: Int_commute)
+next
+ case (IfFalse b s c2 s' c1)
+ hence "approx (t |` (-lnames c1) |` (-lnames c2)) s"
+ by simp
+ hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'"
+ by (rule IfFalse)
+ thus ?case by simp
+qed auto
+
+
+lemma approx_restrict_inv:
+ "\<Turnstile> {approx (t |` (-lnames c))} c {approx (t |` (-lnames c))}"
+ by (simp add: hoare_valid_def big_step_pres_approx_restrict)
+
+declare assign_simp [simp]
+
+lemma approx_eq:
+ "approx t \<Turnstile> c \<sim> fold c t"
+proof (induct c arbitrary: t)
+ case SKIP show ?case by simp
+next
+ case Assign
+ show ?case by (simp add: equiv_up_to_def)
+next
+ case Semi
+ thus ?case by (auto intro!: equiv_up_to_semi)
+next
+ case If
+ thus ?case by (auto intro!: equiv_up_to_if_weak)
+next
+ case (While b c)
+ hence "approx (t |` (- lnames c)) \<Turnstile>
+ WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lnames c))"
+ by (auto intro: equiv_up_to_while_weak approx_restrict_inv)
+ thus ?case
+ by (auto intro: equiv_up_to_weaken approx_map_le)
+qed
+
+
+lemma approx_empty [simp]:
+ "approx empty = (\<lambda>_. True)"
+ by (auto intro!: ext simp: approx_def)
+
+lemma equiv_sym:
+ "c \<sim> c' \<longleftrightarrow> c' \<sim> c"
+ by (auto simp add: equiv_def)
+
+theorem constant_folding_equiv:
+ "fold c empty \<sim> c"
+ using approx_eq [of empty c]
+ by (simp add: equiv_up_to_True equiv_sym)
+
+
+
+section {* More ambitious folding including boolean expressions *}
+
+
+fun bsimp_const :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where
+"bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" |
+"bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" |
+"bsimp_const (Not b) t = not(bsimp_const b t)" |
+"bsimp_const (B bv) _ = B bv"
+
+theorem bvalsimp_const [simp]:
+ assumes "approx t s"
+ shows "bval (bsimp_const b t) s = bval b s"
+ using assms by (induct b) auto
+
+lemma not_B [simp]: "not (B v) = B (\<not>v)"
+ by (cases v) auto
+
+lemma not_B_eq [simp]: "(not b = B v) = (b = B (\<not>v))"
+ by (cases b) auto
+
+lemma and_B_eq:
+ "(and a b = B v) = (a = B False \<and> \<not>v \<or>
+ b = B False \<and> \<not>v \<or>
+ (\<exists>v1 v2. a = B v1 \<and> b = B v2 \<and> v = v1 \<and> v2))"
+ by (rule and.induct) auto
+
+lemma less_B_eq [simp]:
+ "(less a b = B v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
+ by (rule less.induct) auto
+
+theorem bvalsimp_const_B:
+assumes "approx t s"
+shows "bsimp_const b t = B v \<Longrightarrow> bval b s = v"
+ using assms
+ by (induct b arbitrary: v)
+ (auto simp: approx_def and_B_eq aval_simp_const_N
+ split: bexp.splits bool.splits)
+
+
+primrec "bdefs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
+"bdefs SKIP t = t" |
+"bdefs (x ::= a) t =
+ (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
+"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |
+"bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
+ B True \<Rightarrow> bdefs c1 t
+ | B False \<Rightarrow> bdefs c2 t
+ | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
+"bdefs (WHILE b DO c) t = t |` (-lnames c)"
+
+
+primrec bfold where
+"bfold SKIP _ = SKIP" |
+"bfold (x ::= a) t = (x ::= (simp_const a t))" |
+"bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" |
+"bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
+ B True \<Rightarrow> bfold c1 t
+ | B False \<Rightarrow> bfold c2 t
+ | _ \<Rightarrow> IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" |
+"bfold (WHILE b DO c) t = (case bsimp_const b t of
+ B False \<Rightarrow> SKIP
+ | _ \<Rightarrow> WHILE bsimp_const b (t |` (-lnames c)) DO bfold c (t |` (-lnames c)))"
+
+
+lemma bdefs_restrict:
+ "bdefs c t |` (- lnames c) = t |` (- lnames c)"
+proof (induct c arbitrary: t)
+ case (Semi c1 c2)
+ hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)"
+ by simp
+ hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
+ t |` (- lnames c1) |` (-lnames c2)" by simp
+ moreover
+ from Semi
+ have "bdefs c2 (bdefs c1 t) |` (- lnames c2) =
+ bdefs c1 t |` (- lnames c2)"
+ by simp
+ hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =
+ bdefs c1 t |` (- lnames c2) |` (- lnames c1)"
+ by simp
+ ultimately
+ show ?case by (clarsimp simp: Int_commute)
+next
+ case (If b c1 c2)
+ hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
+ hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
+ t |` (- lnames c1) |` (-lnames c2)" by simp
+ moreover
+ from If
+ have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
+ hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) =
+ t |` (- lnames c2) |` (-lnames c1)" by simp
+ ultimately
+ show ?case
+ by (auto simp: Int_commute intro: merge_restrict
+ split: bexp.splits bool.splits)
+qed (auto split: aexp.split bexp.split bool.split)
+
+
+lemma big_step_pres_approx_b:
+ "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'"
+proof (induct arbitrary: t rule: big_step_induct)
+ case Skip thus ?case by simp
+next
+ case Assign
+ thus ?case
+ by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
+next
+ case (Semi c1 s1 s2 c2 s3)
+ have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
+ hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4))
+ thus ?case by simp
+next
+ case (IfTrue b s c1 s')
+ hence "approx (bdefs c1 t) s'" by simp
+ thus ?case using `bval b s` `approx t s`
+ by (clarsimp simp: approx_merge bvalsimp_const_B
+ split: bexp.splits bool.splits)
+next
+ case (IfFalse b s c2 s')
+ hence "approx (bdefs c2 t) s'" by simp
+ thus ?case using `\<not>bval b s` `approx t s`
+ by (clarsimp simp: approx_merge bvalsimp_const_B
+ split: bexp.splits bool.splits)
+next
+ case WhileFalse
+ thus ?case
+ by (clarsimp simp: bvalsimp_const_B approx_def restrict_map_def
+ split: bexp.splits bool.splits)
+next
+ case (WhileTrue b s1 c s2 s3)
+ hence "approx (bdefs c t) s2" by simp
+ with WhileTrue
+ have "approx (bdefs c t |` (- lnames c)) s3"
+ by simp
+ thus ?case
+ by (simp add: bdefs_restrict)
+qed
+
+corollary approx_bdefs_inv [simp]:
+ "\<Turnstile> {approx t} c {approx (bdefs c t)}"
+ by (simp add: hoare_valid_def big_step_pres_approx_b)
+
+lemma bfold_equiv:
+ "approx t \<Turnstile> c \<sim> bfold c t"
+proof (induct c arbitrary: t)
+ case SKIP show ?case by simp
+next
+ case Assign
+ thus ?case by (simp add: equiv_up_to_def)
+next
+ case Semi
+ thus ?case by (auto intro!: equiv_up_to_semi)
+next
+ case (If b c1 c2)
+ hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim>
+ IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
+ by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)
+ thus ?case using If
+ by (fastsimp simp: bvalsimp_const_B split: bexp.splits bool.splits
+ intro: equiv_up_to_trans)
+ next
+ case (While b c)
+ hence "approx (t |` (- lnames c)) \<Turnstile>
+ WHILE b DO c \<sim>
+ WHILE bsimp_const b (t |` (- lnames c))
+ DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'")
+ by (auto intro: equiv_up_to_while_weak approx_restrict_inv
+ simp: bequiv_up_to_def)
+ hence "approx t \<Turnstile> ?W \<sim> ?W'"
+ by (auto intro: equiv_up_to_weaken approx_map_le)
+ thus ?case
+ by (auto split: bexp.splits bool.splits
+ intro: equiv_up_to_while_False
+ simp: bvalsimp_const_B)
+qed
+
+
+theorem constant_bfolding_equiv:
+ "bfold c empty \<sim> c"
+ using bfold_equiv [of empty c]
+ by (simp add: equiv_up_to_True equiv_sym)
+
+
+end
--- a/src/HOL/IMP/ROOT.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML Mon Aug 08 22:11:00 2011 +0200
@@ -17,5 +17,6 @@
"Procs_Stat_Vars_Dyn",
"Procs_Stat_Vars_Stat",
"C_like",
- "OO"
+ "OO",
+ "Fold"
];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Sem_Equiv.thy Mon Aug 08 22:11:00 2011 +0200
@@ -0,0 +1,165 @@
+header "Semantic Equivalence up to a Condition"
+
+theory Sem_Equiv
+imports Hoare_Sound_Complete
+begin
+
+definition
+ equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60)
+where
+ "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'"
+
+definition
+ bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60)
+where
+ "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s"
+
+lemma equiv_up_to_True:
+ "((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')"
+ by (simp add: equiv_def equiv_up_to_def)
+
+lemma equiv_up_to_weaken:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> P' \<Turnstile> c \<sim> c'"
+ by (simp add: equiv_up_to_def)
+
+lemma equiv_up_toI:
+ "(\<And>s s'. P s \<Longrightarrow> (c, s) \<Rightarrow> s' = (c', s) \<Rightarrow> s') \<Longrightarrow> P \<Turnstile> c \<sim> c'"
+ by (unfold equiv_up_to_def) blast
+
+lemma equiv_up_toD1:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> (c', s) \<Rightarrow> s'"
+ by (unfold equiv_up_to_def) blast
+
+lemma equiv_up_toD2:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
+ by (unfold equiv_up_to_def) blast
+
+
+lemma equiv_up_to_refl [simp, intro!]:
+ "P \<Turnstile> c \<sim> c"
+ by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_sym:
+ "(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
+ by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_trans [trans]:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
+ by (auto simp: equiv_up_to_def)
+
+
+lemma bequiv_up_to_refl [simp, intro!]:
+ "P \<Turnstile> b <\<sim>> b"
+ by (auto simp: bequiv_up_to_def)
+
+lemma bequiv_up_to_sym:
+ "(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
+ by (auto simp: bequiv_up_to_def)
+
+lemma bequiv_up_to_trans [trans]:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
+ by (auto simp: bequiv_up_to_def)
+
+
+lemma equiv_up_to_hoare:
+ "P' \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
+ unfolding hoare_valid_def equiv_up_to_def by blast
+
+lemma equiv_up_to_hoare_eq:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
+ by (rule equiv_up_to_hoare)
+
+
+lemma equiv_up_to_semi:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
+ P \<Turnstile> (c; d) \<sim> (c'; d')"
+ by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
+
+lemma equiv_up_to_while_lemma:
+ shows "(d,s) \<Rightarrow> s' \<Longrightarrow>
+ P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
+ (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
+ \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
+ P s \<Longrightarrow>
+ d = WHILE b DO c \<Longrightarrow>
+ (WHILE b' DO c', s) \<Rightarrow> s'"
+proof (induct rule: big_step_induct)
+ case (WhileTrue b s1 c s2 s3)
+ note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
+
+ from WhileTrue.prems
+ have "P \<Turnstile> b <\<sim>> b'" by simp
+ with `bval b s1` `P s1`
+ have "bval b' s1" by (simp add: bequiv_up_to_def)
+ moreover
+ from WhileTrue.prems
+ have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp
+ with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2`
+ have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
+ moreover
+ from WhileTrue.prems
+ have "\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" by simp
+ with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2`
+ have "P s2" by (simp add: hoare_valid_def)
+ hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH)
+ ultimately
+ show ?case by blast
+next
+ case WhileFalse
+ thus ?case by (auto simp: bequiv_up_to_def)
+qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
+
+lemma bequiv_context_subst:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
+ by (auto simp: bequiv_up_to_def)
+
+lemma equiv_up_to_while:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
+ \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
+ P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
+ apply (safe intro!: equiv_up_toI)
+ apply (auto intro: equiv_up_to_while_lemma)[1]
+ apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst)
+ apply (drule equiv_up_to_sym [THEN iffD1])
+ apply (drule bequiv_up_to_sym [THEN iffD1])
+ apply (auto intro: equiv_up_to_while_lemma)[1]
+ done
+
+lemma equiv_up_to_while_weak:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow>
+ P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
+ by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken
+ simp: hoare_valid_def)
+
+lemma equiv_up_to_if:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<inter> bval b \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
+ P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
+ by (auto simp: bequiv_up_to_def equiv_up_to_def)
+
+lemma equiv_up_to_if_weak:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
+ P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
+ by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken)
+
+lemma equiv_up_to_if_True [intro!]:
+ "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
+ by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_if_False [intro!]:
+ "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2"
+ by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_while_False [intro!]:
+ "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
+ by (auto simp: equiv_up_to_def)
+
+lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
+ by (induct rule: big_step_induct) auto
+
+lemma equiv_up_to_while_True [intro!,simp]:
+ "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
+ unfolding equiv_up_to_def
+ by (blast dest: while_never)
+
+
+end
\ No newline at end of file
--- a/src/HOL/IOA/IOA.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/IOA/IOA.thy Mon Aug 08 22:11:00 2011 +0200
@@ -317,7 +317,7 @@
(snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
else snd(snd(snd(t)))=snd(snd(snd(s)))))"
(*SLOW*)
- apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq ioa_projections)
+ apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff ioa_projections)
done
lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Mon Aug 08 22:11:00 2011 +0200
@@ -52,7 +52,7 @@
real_ge > HOL4Compat.real_ge
real_lte > Orderings.less_eq :: "[real,real] => bool"
real_sub > Groups.minus :: "[real,real] => real"
- "/" > Rings.divide :: "[real,real] => real"
+ "/" > Fields.divide :: "[real,real] => real"
pow > Power.power :: "[real,nat] => real"
abs > Groups.abs :: "real => real"
real_of_num > RealDef.real :: "nat => real";
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Aug 08 22:11:00 2011 +0200
@@ -162,11 +162,11 @@
MEASURE > HOLLightCompat.MEASURE
(*real_of_num > RealDef.real :: "nat => real"
real_neg > Groups.uminus_class.uminus :: "real => real"
- real_inv > Rings.inverse_class.inverse :: "real => real"
+ real_inv > Fields.inverse_class.inverse :: "real => real"
real_add > Groups.plus_class.plus :: "real => real => real"
real_sub > Groups.minus_class.minus :: "real => real => real"
real_mul > Groups.times_class.times :: "real => real => real"
- real_div > Rings.inverse_class.divide :: "real => real => real"
+ real_div > Fields.inverse_class.divide :: "real => real => real"
real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
real_le > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
real_gt > Orderings.ord_class.greater :: "real \<Rightarrow> real \<Rightarrow> bool"
--- a/src/HOL/Library/Product_Vector.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Library/Product_Vector.thy Mon Aug 08 22:11:00 2011 +0200
@@ -28,13 +28,13 @@
instance proof
fix a b :: real and x y :: "'a \<times> 'b"
show "scaleR a (x + y) = scaleR a x + scaleR a y"
- by (simp add: expand_prod_eq scaleR_right_distrib)
+ by (simp add: prod_eq_iff scaleR_right_distrib)
show "scaleR (a + b) x = scaleR a x + scaleR b x"
- by (simp add: expand_prod_eq scaleR_left_distrib)
+ by (simp add: prod_eq_iff scaleR_left_distrib)
show "scaleR a (scaleR b x) = scaleR (a * b) x"
- by (simp add: expand_prod_eq)
+ by (simp add: prod_eq_iff)
show "scaleR 1 x = x"
- by (simp add: expand_prod_eq)
+ by (simp add: prod_eq_iff)
qed
end
@@ -174,7 +174,7 @@
instance proof
fix x y :: "'a \<times> 'b"
show "dist x y = 0 \<longleftrightarrow> x = y"
- unfolding dist_prod_def expand_prod_eq by simp
+ unfolding dist_prod_def prod_eq_iff by simp
next
fix x y z :: "'a \<times> 'b"
show "dist x y \<le> dist x z + dist y z"
@@ -373,7 +373,7 @@
unfolding norm_prod_def by simp
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_prod_def
- by (simp add: expand_prod_eq)
+ by (simp add: prod_eq_iff)
show "norm (x + y) \<le> norm x + norm y"
unfolding norm_prod_def
apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
@@ -423,7 +423,7 @@
unfolding inner_prod_def
by (intro add_nonneg_nonneg inner_ge_zero)
show "inner x x = 0 \<longleftrightarrow> x = 0"
- unfolding inner_prod_def expand_prod_eq
+ unfolding inner_prod_def prod_eq_iff
by (simp add: add_nonneg_eq_0_iff)
show "norm x = sqrt (inner x x)"
unfolding norm_prod_def inner_prod_def
--- a/src/HOL/Library/Product_plus.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Library/Product_plus.thy Mon Aug 08 22:11:00 2011 +0200
@@ -78,39 +78,36 @@
lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
unfolding uminus_prod_def by simp
-lemmas expand_prod_eq = Pair_fst_snd_eq
-
-
subsection {* Class instances *}
instance prod :: (semigroup_add, semigroup_add) semigroup_add
- by default (simp add: expand_prod_eq add_assoc)
+ by default (simp add: prod_eq_iff add_assoc)
instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
- by default (simp add: expand_prod_eq add_commute)
+ by default (simp add: prod_eq_iff add_commute)
instance prod :: (monoid_add, monoid_add) monoid_add
- by default (simp_all add: expand_prod_eq)
+ by default (simp_all add: prod_eq_iff)
instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
- by default (simp add: expand_prod_eq)
+ by default (simp add: prod_eq_iff)
instance prod ::
(cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
- by default (simp_all add: expand_prod_eq)
+ by default (simp_all add: prod_eq_iff)
instance prod ::
(cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
- by default (simp add: expand_prod_eq)
+ by default (simp add: prod_eq_iff)
instance prod ::
(cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
instance prod :: (group_add, group_add) group_add
- by default (simp_all add: expand_prod_eq diff_minus)
+ by default (simp_all add: prod_eq_iff diff_minus)
instance prod :: (ab_group_add, ab_group_add) ab_group_add
- by default (simp_all add: expand_prod_eq)
+ by default (simp_all add: prod_eq_iff)
lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
by (cases "finite A", induct set: finite, simp_all)
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Aug 08 22:11:00 2011 +0200
@@ -285,7 +285,7 @@
(@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
(@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
(@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
- (@{const_name "Rings.inverse_class.divide"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
(@{const_name "Lattices.semilattice_inf_class.inf"}, @{typ "prop => prop => prop"}),
(@{const_name "Lattices.semilattice_sup_class.sup"}, @{typ "prop => prop => prop"}),
(@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
--- a/src/HOL/Product_Type.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Product_Type.thy Mon Aug 08 22:11:00 2011 +0200
@@ -436,11 +436,11 @@
lemmas surjective_pairing = pair_collapse [symmetric]
-lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
+lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
by (cases s, cases t) simp
lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
- by (simp add: Pair_fst_snd_eq)
+ by (simp add: prod_eq_iff)
lemma split_conv [simp, code]: "split f (a, b) = f a b"
by (fact prod.cases)
@@ -1226,4 +1226,6 @@
lemmas split = split_conv -- {* for backwards compatibility *}
+lemmas Pair_fst_snd_eq = prod_eq_iff
+
end
--- a/src/HOL/Rings.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Rings.thy Mon Aug 08 22:11:00 2011 +0200
@@ -417,217 +417,6 @@
end
-class inverse =
- fixes inverse :: "'a \<Rightarrow> 'a"
- and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
-
-class division_ring = ring_1 + inverse +
- assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
- assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
- assumes divide_inverse: "a / b = a * inverse b"
-begin
-
-subclass ring_1_no_zero_divisors
-proof
- fix a b :: 'a
- assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
- show "a * b \<noteq> 0"
- proof
- assume ab: "a * b = 0"
- hence "0 = inverse a * (a * b) * inverse b" by simp
- also have "\<dots> = (inverse a * a) * (b * inverse b)"
- by (simp only: mult_assoc)
- also have "\<dots> = 1" using a b by simp
- finally show False by simp
- qed
-qed
-
-lemma nonzero_imp_inverse_nonzero:
- "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
-proof
- assume ianz: "inverse a = 0"
- assume "a \<noteq> 0"
- hence "1 = a * inverse a" by simp
- also have "... = 0" by (simp add: ianz)
- finally have "1 = 0" .
- thus False by (simp add: eq_commute)
-qed
-
-lemma inverse_zero_imp_zero:
- "inverse a = 0 \<Longrightarrow> a = 0"
-apply (rule classical)
-apply (drule nonzero_imp_inverse_nonzero)
-apply auto
-done
-
-lemma inverse_unique:
- assumes ab: "a * b = 1"
- shows "inverse a = b"
-proof -
- have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
- moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
- ultimately show ?thesis by (simp add: mult_assoc [symmetric])
-qed
-
-lemma nonzero_inverse_minus_eq:
- "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
-by (rule inverse_unique) simp
-
-lemma nonzero_inverse_inverse_eq:
- "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
-by (rule inverse_unique) simp
-
-lemma nonzero_inverse_eq_imp_eq:
- assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
- shows "a = b"
-proof -
- from `inverse a = inverse b`
- have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
- with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
- by (simp add: nonzero_inverse_inverse_eq)
-qed
-
-lemma inverse_1 [simp]: "inverse 1 = 1"
-by (rule inverse_unique) simp
-
-lemma nonzero_inverse_mult_distrib:
- assumes "a \<noteq> 0" and "b \<noteq> 0"
- shows "inverse (a * b) = inverse b * inverse a"
-proof -
- have "a * (b * inverse b) * inverse a = 1" using assms by simp
- hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)
- thus ?thesis by (rule inverse_unique)
-qed
-
-lemma division_ring_inverse_add:
- "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
-by (simp add: algebra_simps)
-
-lemma division_ring_inverse_diff:
- "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
-by (simp add: algebra_simps)
-
-lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
-proof
- assume neq: "b \<noteq> 0"
- {
- hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)
- also assume "a / b = 1"
- finally show "a = b" by simp
- next
- assume "a = b"
- with neq show "a / b = 1" by (simp add: divide_inverse)
- }
-qed
-
-lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
-by (simp add: divide_inverse)
-
-lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
-by (simp add: divide_inverse)
-
-lemma divide_zero_left [simp]: "0 / a = 0"
-by (simp add: divide_inverse)
-
-lemma inverse_eq_divide: "inverse a = 1 / a"
-by (simp add: divide_inverse)
-
-lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
-by (simp add: divide_inverse algebra_simps)
-
-lemma divide_1 [simp]: "a / 1 = a"
- by (simp add: divide_inverse)
-
-lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
- by (simp add: divide_inverse mult_assoc)
-
-lemma minus_divide_left: "- (a / b) = (-a) / b"
- by (simp add: divide_inverse)
-
-lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
- by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
- by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
- by (simp add: divide_inverse)
-
-lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
- by (simp add: diff_minus add_divide_distrib)
-
-lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
-proof -
- assume [simp]: "c \<noteq> 0"
- have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
- also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
-proof -
- assume [simp]: "c \<noteq> 0"
- have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
- also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
- by (simp add: divide_inverse mult_assoc)
-
-lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
- by (drule sym) (simp add: divide_inverse mult_assoc)
-
-end
-
-class division_ring_inverse_zero = division_ring +
- assumes inverse_zero [simp]: "inverse 0 = 0"
-begin
-
-lemma divide_zero [simp]:
- "a / 0 = 0"
- by (simp add: divide_inverse)
-
-lemma divide_self_if [simp]:
- "a / a = (if a = 0 then 0 else 1)"
- by simp
-
-lemma inverse_nonzero_iff_nonzero [simp]:
- "inverse a = 0 \<longleftrightarrow> a = 0"
- by rule (fact inverse_zero_imp_zero, simp)
-
-lemma inverse_minus_eq [simp]:
- "inverse (- a) = - inverse a"
-proof cases
- assume "a=0" thus ?thesis by simp
-next
- assume "a\<noteq>0"
- thus ?thesis by (simp add: nonzero_inverse_minus_eq)
-qed
-
-lemma inverse_eq_imp_eq:
- "inverse a = inverse b \<Longrightarrow> a = b"
-apply (cases "a=0 | b=0")
- apply (force dest!: inverse_zero_imp_zero
- simp add: eq_commute [of "0::'a"])
-apply (force dest!: nonzero_inverse_eq_imp_eq)
-done
-
-lemma inverse_eq_iff_eq [simp]:
- "inverse a = inverse b \<longleftrightarrow> a = b"
- by (force dest!: inverse_eq_imp_eq)
-
-lemma inverse_inverse_eq [simp]:
- "inverse (inverse a) = a"
-proof cases
- assume "a=0" thus ?thesis by simp
-next
- assume "a\<noteq>0"
- thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
-qed
-
-end
-
text {*
The theory of partially ordered rings is taken from the books:
\begin{itemize}
--- a/src/HOL/Tools/lin_arith.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML Mon Aug 08 22:11:00 2011 +0200
@@ -151,7 +151,7 @@
(SOME t', m'') => (SOME (mC $ s' $ t'), m'')
| (NONE, m'') => (SOME s', m''))
| (NONE, m') => demult (t, m')))
- | demult ((mC as Const (@{const_name Rings.divide}, _)) $ s $ t, m) =
+ | demult ((mC as Const (@{const_name Fields.divide}, _)) $ s $ t, m) =
(* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ? Note that
if we choose to do so here, the simpset used by arith must be able to
@@ -213,7 +213,7 @@
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
- | poly (all as Const (@{const_name Rings.divide}, _) $ _ $ _, m, pi as (p, i)) =
+ | poly (all as Const (@{const_name Fields.divide}, _) $ _ $ _, m, pi as (p, i)) =
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
--- a/src/HOL/Tools/numeral_simprocs.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Aug 08 22:11:00 2011 +0200
@@ -97,7 +97,7 @@
Fractions are reduced later by the cancel_numeral_factor simproc.*)
fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
-val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
+val mk_divide = HOLogic.mk_binop @{const_name Fields.divide};
(*Build term (p / q) * t*)
fun mk_fcoeff ((p, q), t) =
@@ -106,7 +106,7 @@
(*Express t as a product of a fraction with other sorted terms*)
fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
- | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
+ | dest_fcoeff sign (Const (@{const_name Fields.divide}, _) $ t $ u) =
let val (p, t') = dest_coeff sign t
val (q, u') = dest_coeff 1 u
in (mk_frac (p, q), mk_divide (t', u')) end
@@ -391,8 +391,8 @@
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
- val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Fields.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
val cancel = @{thm mult_divide_mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -570,8 +570,8 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
- val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Fields.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
);
@@ -639,13 +639,13 @@
val (l,r) = Thm.dest_binop ct
val T = ctyp_of_term l
in (case (term_of l, term_of r) of
- (Const(@{const_name Rings.divide},_)$_$_, _) =>
+ (Const(@{const_name Fields.divide},_)$_$_, _) =>
let val (x,y) = Thm.dest_binop l val z = r
val _ = map (HOLogic.dest_number o term_of) [x,y,z]
val ynz = prove_nz ss T y
in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
end
- | (_, Const (@{const_name Rings.divide},_)$_$_) =>
+ | (_, Const (@{const_name Fields.divide},_)$_$_) =>
let val (x,y) = Thm.dest_binop r val z = l
val _ = map (HOLogic.dest_number o term_of) [x,y,z]
val ynz = prove_nz ss T y
@@ -655,49 +655,49 @@
end
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
- fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
+ fun is_number (Const(@{const_name Fields.divide},_)$a$b) = is_number a andalso is_number b
| is_number t = can HOLogic.dest_number t
val is_number = is_number o term_of
fun proc3 phi ss ct =
(case term_of ct of
- Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ Const(@{const_name Orderings.less},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ | Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
--- a/src/HOL/Tools/semiring_normalizer.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Mon Aug 08 22:11:00 2011 +0200
@@ -185,14 +185,14 @@
let
fun numeral_is_const ct =
case term_of ct of
- Const (@{const_name Rings.divide},_) $ a $ b =>
+ Const (@{const_name Fields.divide},_) $ a $ b =>
can HOLogic.dest_number a andalso can HOLogic.dest_number b
- | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
+ | Const (@{const_name Fields.inverse},_)$t => can HOLogic.dest_number t
| t => can HOLogic.dest_number t
fun dest_const ct = ((case term_of ct of
- Const (@{const_name Rings.divide},_) $ a $ b=>
+ Const (@{const_name Fields.divide},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
- | Const (@{const_name Rings.inverse},_)$t =>
+ | Const (@{const_name Fields.inverse},_)$t =>
Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
| t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
handle TERM _ => error "ring_dest_const")
--- a/src/HOL/ex/SVC_Oracle.thy Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Mon Aug 08 22:11:00 2011 +0200
@@ -64,7 +64,7 @@
(*abstraction of a real/rational expression*)
fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name Fields.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x)
| rat t = lit t
--- a/src/HOL/ex/svc_funcs.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/HOL/ex/svc_funcs.ML Mon Aug 08 22:11:00 2011 +0200
@@ -173,7 +173,7 @@
| tm (Const(@{const_name Groups.times}, T) $ x $ y) =
if is_numeric_op T then Interp("*", [tm x, tm y])
else fail t
- | tm (Const(@{const_name Rings.inverse}, T) $ x) =
+ | tm (Const(@{const_name Fields.inverse}, T) $ x) =
if domain_type T = HOLogic.realT then
Rat(1, litExp x)
else fail t
--- a/src/Pure/Isar/attrib.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/Pure/Isar/attrib.ML Mon Aug 08 22:11:00 2011 +0200
@@ -444,6 +444,7 @@
register_config Printer.show_structs_raw #>
register_config Printer.show_question_marks_raw #>
register_config Syntax.ambiguity_level_raw #>
+ register_config Syntax.ambiguity_warnings_raw #>
register_config Syntax_Trans.eta_contract_raw #>
register_config Name_Space.names_long_raw #>
register_config Name_Space.names_short_raw #>
--- a/src/Pure/Syntax/syntax.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon Aug 08 22:11:00 2011 +0200
@@ -16,6 +16,8 @@
val ambiguity_level_raw: Config.raw
val ambiguity_level: int Config.T
val ambiguity_limit: int Config.T
+ val ambiguity_warnings_raw: Config.raw
+ val ambiguity_warnings: bool Config.T
val read_token: string -> Symbol_Pos.T list * Position.T
val parse_token: Proof.context -> (XML.tree list -> 'a) ->
Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
@@ -193,6 +195,11 @@
val ambiguity_limit =
Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
+val ambiguity_warnings_raw =
+ Config.declare "syntax_ambiguity_warnings" (fn _ => Config.Bool true);
+val ambiguity_warnings =
+ Config.bool ambiguity_warnings_raw;
+
(* outer syntax token -- with optional YXML content *)
--- a/src/Pure/Syntax/syntax_phases.ML Mon Aug 08 19:30:18 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Aug 08 22:11:00 2011 +0200
@@ -288,15 +288,17 @@
val len = length pts;
val limit = Config.get ctxt Syntax.ambiguity_limit;
+ val warnings = Config.get ctxt Syntax.ambiguity_warnings;
val _ =
if len <= Config.get ctxt Syntax.ambiguity_level then ()
else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
- else
+ else if warnings then
(Context_Position.if_visible ctxt warning (cat_lines
(("Ambiguous input" ^ Position.str_of pos ^
"\nproduces " ^ string_of_int len ^ " parse trees" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
+ map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))))
+ else ();
val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
@@ -353,6 +355,7 @@
val level = Config.get ctxt Syntax.ambiguity_level;
val limit = Config.get ctxt Syntax.ambiguity_limit;
+ val warnings = Config.get ctxt Syntax.ambiguity_warnings;
val ambig_msg =
if ambiguity > 1 andalso ambiguity <= level then
@@ -381,7 +384,7 @@
report_result ctxt pos
[(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
else if len = 1 then
- (if ambiguity > level then
+ (if ambiguity > level andalso warnings then
Context_Position.if_visible ctxt warning
"Fortunately, only one parse tree is type correct.\n\
\You may still want to disambiguate your grammar or your input."