# HG changeset patch # User haftmann # Date 1312834260 -7200 # Node ID caac24afcadb89747c161bb0601a088a0f05555d # Parent cebb7abb54b18bcac5705320cbd11e5d70b80a74# Parent 9f8790f8e589d108da50cbf7cebee4fd531b8208 merged diff -r 9f8790f8e589 -r caac24afcadb src/HOL/Complete_Lattice.thy --- 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 @@ "\{} = \" by (auto intro: antisym Inf_greatest) -lemma INF_empty: "(\x\{}. f x) = \" +lemma INF_empty [simp]: "(\x\{}. f x) = \" by (simp add: INF_def) lemma Sup_empty [simp]: "\{} = \" by (auto intro: antisym Sup_least) -lemma SUP_empty: "(\x\{}. f x) = \" +lemma SUP_empty [simp]: "(\x\{}. f x) = \" by (simp add: SUP_def) lemma Inf_UNIV [simp]: @@ -172,6 +172,12 @@ lemma SUP_insert: "(\x\insert a A. f x) = f a \ SUPR A f" by (simp add: SUP_def Sup_insert) +lemma INF_image: "(\x\f`A. g x) = (\x\A. g (f x))" + by (simp add: INF_def image_image) + +lemma SUP_image: "(\x\f`A. g x) = (\x\A. g (f x))" + by (simp add: SUP_def image_image) + lemma Inf_Sup: "\A = \{b. \a \ A. b \ a}" by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) @@ -684,11 +690,11 @@ lemma Int_eq_Inter: "A \ B = \{A, B}" by (simp add: Inf_insert) -lemma Inter_empty [simp]: "\{} = UNIV" - by (fact Inf_empty) +lemma Inter_empty: "\{} = UNIV" + by (fact Inf_empty) (* already simp *) -lemma Inter_UNIV [simp]: "\UNIV = {}" - by (fact Inf_UNIV) +lemma Inter_UNIV: "\UNIV = {}" + by (fact Inf_UNIV) (* already simp *) lemma Inter_insert [simp]: "\(insert a B) = a \ \B" by (fact Inf_insert) @@ -785,8 +791,8 @@ lemma INT_greatest: "(\x. x \ A \ C \ B x) \ C \ (\x\A. B x)" by (fact le_INF_I) -lemma INT_empty [simp]: "(\x\{}. B x) = UNIV" - by (fact INF_empty) +lemma INT_empty: "(\x\{}. B x) = UNIV" + by (fact INF_empty) (* already simp *) lemma INT_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)" by (fact INF_absorb) @@ -994,8 +1000,8 @@ lemma UN_insert_distrib: "u \ A \ (\x\A. insert a (B x)) = insert a (\x\A. B x)" by blast -lemma UN_empty [simp, no_atp]: "(\x\{}. B x) = {}" - by (fact SUP_empty) +lemma UN_empty [no_atp]: "(\x\{}. B x) = {}" + by (fact SUP_empty) (* already simp *) lemma UN_empty2 [simp]: "(\x\A. {}) = {}" by (fact SUP_bot) diff -r 9f8790f8e589 -r caac24afcadb src/HOL/Complex.thy --- 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?]: "\Re x = Re y; Im x = Im y\ \ x = y" +lemma complex_eqI [intro?]: "\Re x = Re y; Im x = Im y\ \ x = y" by (induct x, induct y) simp -lemma expand_complex_eq: "x = y \ Re x = Re y \ Im x = Im y" +lemma complex_eq_iff: "x = y \ Re x = Re y \ 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 \ 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 \ 0" -by (simp add: expand_complex_eq) +by (simp add: complex_eq_iff) lemma complex_i_not_one [simp]: "ii \ 1" -by (simp add: expand_complex_eq) +by (simp add: complex_eq_iff) lemma complex_i_not_number_of [simp]: "ii \ 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)\ + (Im z)\)" -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)\" 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 diff -r 9f8790f8e589 -r caac24afcadb src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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)) diff -r 9f8790f8e589 -r caac24afcadb src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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)); diff -r 9f8790f8e589 -r caac24afcadb src/HOL/Fields.thy --- 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 \ 'a" + and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) + +class division_ring = ring_1 + inverse + + assumes left_inverse [simp]: "a \ 0 \ inverse a * a = 1" + assumes right_inverse [simp]: "a \ 0 \ 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 \ 0" and b: "b \ 0" + show "a * b \ 0" + proof + assume ab: "a * b = 0" + hence "0 = inverse a * (a * b) * inverse b" by simp + also have "\ = (inverse a * a) * (b * inverse b)" + by (simp only: mult_assoc) + also have "\ = 1" using a b by simp + finally show False by simp + qed +qed + +lemma nonzero_imp_inverse_nonzero: + "a \ 0 \ inverse a \ 0" +proof + assume ianz: "inverse a = 0" + assume "a \ 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 \ 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 \ 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 \ 0 \ inverse (- a) = - inverse a" +by (rule inverse_unique) simp + +lemma nonzero_inverse_inverse_eq: + "a \ 0 \ inverse (inverse a) = a" +by (rule inverse_unique) simp + +lemma nonzero_inverse_eq_imp_eq: + assumes "inverse a = inverse b" and "a \ 0" and "b \ 0" + shows "a = b" +proof - + from `inverse a = inverse b` + have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong) + with `a \ 0` and `b \ 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 \ 0" and "b \ 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 \ 0 \ b \ 0 \ inverse a + inverse b = inverse a * (a + b) * inverse b" +by (simp add: algebra_simps) + +lemma division_ring_inverse_diff: + "a \ 0 \ b \ 0 \ inverse a - inverse b = inverse a * (b - a) * inverse b" +by (simp add: algebra_simps) + +lemma right_inverse_eq: "b \ 0 \ a / b = 1 \ a = b" +proof + assume neq: "b \ 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 \ 0 \ inverse a = 1 / a" +by (simp add: divide_inverse) + +lemma divide_self [simp]: "a \ 0 \ 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 \ 0 ==> - (a / b) = a / (- b)" + by (simp add: divide_inverse nonzero_inverse_minus_eq) + +lemma nonzero_minus_divide_divide: "b \ 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 \ 0 \ a = b / c \ a * c = b" +proof - + assume [simp]: "c \ 0" + have "a = b / c \ a * c = (b / c) * c" by simp + also have "... \ a * c = b" by (simp add: divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma nonzero_divide_eq_eq [field_simps]: "c \ 0 \ b / c = a \ b = a * c" +proof - + assume [simp]: "c \ 0" + have "b / c = a \ (b / c) * c = a * c" by simp + also have "... \ b = a * c" by (simp add: divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma divide_eq_imp: "c \ 0 \ b = a * c \ b / c = a" + by (simp add: divide_inverse mult_assoc) + +lemma eq_divide_imp: "c \ 0 \ a * c = b \ 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 \ 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\0" + thus ?thesis by (simp add: nonzero_inverse_minus_eq) +qed + +lemma inverse_eq_imp_eq: + "inverse a = inverse b \ 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 \ 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\0" + thus ?thesis by (simp add: nonzero_inverse_inverse_eq) +qed + +end + +subsection {* Fields *} + class field = comm_ring_1 + inverse + assumes field_inverse: "a \ 0 \ 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 diff -r 9f8790f8e589 -r caac24afcadb src/HOL/HOLCF/Fix.thy --- 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\(?x, ?y)) = ?y" by (rule trans [symmetric, OF fix_eq], simp) - from 1 2 show "F\(?x, ?y) = (?x, ?y)" by (simp add: Pair_fst_snd_eq) + from 1 2 show "F\(?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff) next fix z assume F_z: "F\z = z" obtain x y where z: "z = (x,y)" by (rule prod.exhaust) diff -r 9f8790f8e589 -r caac24afcadb src/HOL/HOLCF/IOA/meta_theory/Automata.thy --- 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 diff -r 9f8790f8e589 -r caac24afcadb src/HOL/HOLCF/Product_Cpo.thy --- 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 \ 'b" assume "x \ y" "y \ 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 \ 'b" @@ -142,7 +142,7 @@ proof fix x y :: "'a \ 'b" show "x \ y \ x = y" - unfolding below_prod_def Pair_fst_snd_eq + unfolding below_prod_def prod_eq_iff by simp qed diff -r 9f8790f8e589 -r caac24afcadb src/HOL/HOLCF/Sprod.thy --- 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]: diff -r 9f8790f8e589 -r caac24afcadb src/HOL/HOLCF/Ssum.thy --- 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} *} diff -r 9f8790f8e589 -r caac24afcadb src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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 diff -r 9f8790f8e589 -r caac24afcadb src/HOL/HOLCF/ex/Domain_Proofs.thy --- 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 diff -r 9f8790f8e589 -r caac24afcadb src/HOL/IMP/Big_Step.thy --- 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) \ s' \ (s' = s(x := aval a s))" + by auto subsection "Command Equivalence" diff -r 9f8790f8e589 -r caac24afcadb src/HOL/IMP/Comp_Rev.thy --- 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 = [] \ (c,s) \ s" by (induct c) auto -lemma assign [simp]: - "(x ::= a,s) \ s' \ (s' = s(x := aval a s))" - by auto +declare assign_simp [simp] lemma ccomp_exec_n: "ccomp c \ (0,s,stk) \^n (isize(ccomp c),t,stk') diff -r 9f8790f8e589 -r caac24afcadb src/HOL/IMP/Fold.thy --- /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 \ val option" + +(* maybe better as the composition of substitution and the existing simp_const(0) *) +fun simp_const :: "aexp \ tab \ aexp" where +"simp_const (N n) _ = N n" | +"simp_const (V x) t = (case t x of None \ V x | Some k \ N k)" | +"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of + (N n1, N n2) \ N(n1+n2) | (e1',e2') \ Plus e1' e2')" + +definition "approx t s \ (ALL x k. t x = Some k \ 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 \ aval a s = n" + using assms + by (induct a arbitrary: n) + (auto simp: approx_def split: aexp.splits option.splits) + +definition + "merge t1 t2 = (\m. if t1 m = t2 m then t1 m else None)" + +primrec lnames :: "com \ name set" where +"lnames SKIP = {}" | +"lnames (x ::= a) = {x}" | +"lnames (c1; c2) = lnames c1 \ lnames c2" | +"lnames (IF b THEN c1 ELSE c2) = lnames c1 \ lnames c2" | +"lnames (WHILE b DO c) = lnames c" + +primrec "defs" :: "com \ tab \ tab" where +"defs SKIP t = t" | +"defs (x ::= a) t = + (case simp_const a t of N k \ t(x \ k) | _ \ 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 \ approx t2 s \ approx (merge t1 t2) s" + by (fastsimp simp: merge_def approx_def) + +lemma approx_map_le: + "approx t2 s \ t1 \\<^sub>m t2 \ approx t1 s" + by (clarsimp simp: approx_def map_le_def dom_def) + +lemma restrict_map_le [intro!, simp]: "t |` S \\<^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 "\x. (t1 |` S) x = (t |` S) x" + and "\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) \ s' \ approx t s \ 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]: + "\ {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) \ s' \ approx (t |` (-lnames c)) s \ 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: + "\ {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 \ c \ 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)) \ + WHILE b DO c \ 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 = (\_. True)" + by (auto intro!: ext simp: approx_def) + +lemma equiv_sym: + "c \ c' \ c' \ c" + by (auto simp add: equiv_def) + +theorem constant_folding_equiv: + "fold c empty \ 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 \ tab \ 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 (\v)" + by (cases v) auto + +lemma not_B_eq [simp]: "(not b = B v) = (b = B (\v))" + by (cases b) auto + +lemma and_B_eq: + "(and a b = B v) = (a = B False \ \v \ + b = B False \ \v \ + (\v1 v2. a = B v1 \ b = B v2 \ v = v1 \ v2))" + by (rule and.induct) auto + +lemma less_B_eq [simp]: + "(less a b = B v) = (\n1 n2. a = N n1 \ b = N n2 \ v = (n1 < n2))" + by (rule less.induct) auto + +theorem bvalsimp_const_B: +assumes "approx t s" +shows "bsimp_const b t = B v \ 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 \ tab \ tab" where +"bdefs SKIP t = t" | +"bdefs (x ::= a) t = + (case simp_const a t of N k \ t(x \ k) | _ \ 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 \ bdefs c1 t + | B False \ bdefs c2 t + | _ \ 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 \ bfold c1 t + | B False \ bfold c2 t + | _ \ 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 \ SKIP + | _ \ 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) \ s' \ approx t s \ 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 `\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]: + "\ {approx t} c {approx (bdefs c t)}" + by (simp add: hoare_valid_def big_step_pres_approx_b) + +lemma bfold_equiv: + "approx t \ c \ 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 \ IF b THEN c1 ELSE c2 \ + 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)) \ + WHILE b DO c \ + WHILE bsimp_const b (t |` (- lnames c)) + DO bfold c (t |` (- lnames c))" (is "_ \ ?W \ ?W'") + by (auto intro: equiv_up_to_while_weak approx_restrict_inv + simp: bequiv_up_to_def) + hence "approx t \ ?W \ ?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 \ c" + using bfold_equiv [of empty c] + by (simp add: equiv_up_to_True equiv_sym) + + +end diff -r 9f8790f8e589 -r caac24afcadb src/HOL/IMP/ROOT.ML --- 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" ]; diff -r 9f8790f8e589 -r caac24afcadb src/HOL/IMP/Sem_Equiv.thy --- /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 \ com \ com \ bool" ("_ \ _ \ _" [60,0,10] 60) +where + "P \ c \ c' \ \s s'. P s \ (c,s) \ s' \ (c',s) \ s'" + +definition + bequiv_up_to :: "assn \ bexp \ bexp \ bool" ("_ \ _ <\> _" [60,0,10] 60) +where + "P \ b <\> b' \ \s. P s \ bval b s = bval b' s" + +lemma equiv_up_to_True: + "((\_. True) \ c \ c') = (c \ c')" + by (simp add: equiv_def equiv_up_to_def) + +lemma equiv_up_to_weaken: + "P \ c \ c' \ (\s. P' s \ P s) \ P' \ c \ c'" + by (simp add: equiv_up_to_def) + +lemma equiv_up_toI: + "(\s s'. P s \ (c, s) \ s' = (c', s) \ s') \ P \ c \ c'" + by (unfold equiv_up_to_def) blast + +lemma equiv_up_toD1: + "P \ c \ c' \ P s \ (c, s) \ s' \ (c', s) \ s'" + by (unfold equiv_up_to_def) blast + +lemma equiv_up_toD2: + "P \ c \ c' \ P s \ (c', s) \ s' \ (c, s) \ s'" + by (unfold equiv_up_to_def) blast + + +lemma equiv_up_to_refl [simp, intro!]: + "P \ c \ c" + by (auto simp: equiv_up_to_def) + +lemma equiv_up_to_sym: + "(P \ c \ c') = (P \ c' \ c)" + by (auto simp: equiv_up_to_def) + +lemma equiv_up_to_trans [trans]: + "P \ c \ c' \ P \ c' \ c'' \ P \ c \ c''" + by (auto simp: equiv_up_to_def) + + +lemma bequiv_up_to_refl [simp, intro!]: + "P \ b <\> b" + by (auto simp: bequiv_up_to_def) + +lemma bequiv_up_to_sym: + "(P \ b <\> b') = (P \ b' <\> b)" + by (auto simp: bequiv_up_to_def) + +lemma bequiv_up_to_trans [trans]: + "P \ b <\> b' \ P \ b' <\> b'' \ P \ b <\> b''" + by (auto simp: bequiv_up_to_def) + + +lemma equiv_up_to_hoare: + "P' \ c \ c' \ (\s. P s \ P' s) \ (\ {P} c {Q}) = (\ {P} c' {Q})" + unfolding hoare_valid_def equiv_up_to_def by blast + +lemma equiv_up_to_hoare_eq: + "P \ c \ c' \ (\ {P} c {Q}) = (\ {P} c' {Q})" + by (rule equiv_up_to_hoare) + + +lemma equiv_up_to_semi: + "P \ c \ c' \ Q \ d \ d' \ \ {P} c {Q} \ + P \ (c; d) \ (c'; d')" + by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast + +lemma equiv_up_to_while_lemma: + shows "(d,s) \ s' \ + P \ b <\> b' \ + (\s. P s \ bval b s) \ c \ c' \ + \ {\s. P s \ bval b s} c {P} \ + P s \ + d = WHILE b DO c \ + (WHILE b' DO c', s) \ 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 \ b <\> 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 "(\s. P s \ bval b s) \ c \ c'" by simp + with `bval b s1` `P s1` `(c, s1) \