# HG changeset patch # User blanchet # Date 1266568518 -3600 # Node ID 5cb63cb4213f20c183e56ec701dcb6d64cdc11a7 # Parent 2bcdae5f4fdb8bee04f507d0c33c268922a83255# Parent 298f729f4fac4ab690a6f33ed16cd7aabe2cef93 merge diff -r 2bcdae5f4fdb -r 5cb63cb4213f Admin/isatest/settings/at64-poly-5.1-para --- a/Admin/isatest/settings/at64-poly-5.1-para Thu Feb 18 18:48:07 2010 +0100 +++ b/Admin/isatest/settings/at64-poly-5.1-para Fri Feb 19 09:35:18 2010 +0100 @@ -1,10 +1,10 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-5.2.1" - ML_SYSTEM="polyml-5.2.1" + POLYML_HOME="/home/polyml/polyml-5.3.0" + ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="x86_64-linux" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="-H 500" + ML_OPTIONS="-H 1000" ISABELLE_HOME_USER=~/isabelle-at64-poly-para-e diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Datatype.thy Fri Feb 19 09:35:18 2010 +0100 @@ -144,11 +144,10 @@ (** Scons vs Atom **) lemma Scons_not_Atom [iff]: "Scons M N \ Atom(a)" -apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def) -apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] +unfolding Atom_def Scons_def Push_Node_def One_nat_def +by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] dest!: Abs_Node_inj elim!: apfst_convE sym [THEN Push_neq_K0]) -done lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard] @@ -199,14 +198,12 @@ (** Injectiveness of Scons **) lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'" -apply (simp add: Scons_def One_nat_def) -apply (blast dest!: Push_Node_inject) -done +unfolding Scons_def One_nat_def +by (blast dest!: Push_Node_inject) lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'" -apply (simp add: Scons_def One_nat_def) -apply (blast dest!: Push_Node_inject) -done +unfolding Scons_def One_nat_def +by (blast dest!: Push_Node_inject) lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'" apply (erule equalityE) @@ -230,14 +227,14 @@ (** Scons vs Leaf **) lemma Scons_not_Leaf [iff]: "Scons M N \ Leaf(a)" -by (simp add: Leaf_def o_def Scons_not_Atom) +unfolding Leaf_def o_def by (rule Scons_not_Atom) lemmas Leaf_not_Scons [iff] = Scons_not_Leaf [THEN not_sym, standard] (** Scons vs Numb **) lemma Scons_not_Numb [iff]: "Scons M N \ Numb(k)" -by (simp add: Numb_def o_def Scons_not_Atom) +unfolding Numb_def o_def by (rule Scons_not_Atom) lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard] @@ -281,14 +278,15 @@ by (auto simp add: Atom_def ntrunc_def ndepth_K0) lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)" -by (simp add: Leaf_def o_def ntrunc_Atom) +unfolding Leaf_def o_def by (rule ntrunc_Atom) lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)" -by (simp add: Numb_def o_def ntrunc_Atom) +unfolding Numb_def o_def by (rule ntrunc_Atom) lemma ntrunc_Scons [simp]: "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)" -by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node) +unfolding Scons_def ntrunc_def One_nat_def +by (auto simp add: ndepth_Push_Node) @@ -351,7 +349,7 @@ (** Injection **) lemma In0_not_In1 [iff]: "In0(M) \ In1(N)" -by (auto simp add: In0_def In1_def One_nat_def) +unfolding In0_def In1_def One_nat_def by auto lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard] @@ -417,10 +415,10 @@ by (simp add: Scons_def, blast) lemma In0_mono: "M<=N ==> In0(M) <= In0(N)" -by (simp add: In0_def subset_refl Scons_mono) +by (simp add: In0_def Scons_mono) lemma In1_mono: "M<=N ==> In1(M) <= In1(N)" -by (simp add: In1_def subset_refl Scons_mono) +by (simp add: In1_def Scons_mono) (*** Split and Case ***) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Deriv.thy Fri Feb 19 09:35:18 2010 +0100 @@ -260,7 +260,7 @@ -- x --> d (f x) * D" by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]]) thus "(\z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D" - by (simp add: d dfx real_scaleR_def) + by (simp add: d dfx) qed text {* @@ -279,7 +279,7 @@ text {* Standard version *} lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db" -by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute) +by (drule (1) DERIV_chain', simp add: o_def mult_commute) lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db" by (auto dest: DERIV_chain simp add: o_def) @@ -290,7 +290,7 @@ lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))" apply (cut_tac DERIV_power [OF DERIV_ident]) -apply (simp add: real_scaleR_def real_of_nat_def) +apply (simp add: real_of_nat_def) done text {* Power of @{text "-1"} *} @@ -1532,12 +1532,12 @@ moreover have "\x. a < x \ x < b \ ?h differentiable x" proof - - have "\x. a < x \ x < b \ (\x. f b - f a) differentiable x" by (simp add: differentiable_const) - with gd have "\x. a < x \ x < b \ (\x. (f b - f a) * g x) differentiable x" by (simp add: differentiable_mult) + have "\x. a < x \ x < b \ (\x. f b - f a) differentiable x" by simp + with gd have "\x. a < x \ x < b \ (\x. (f b - f a) * g x) differentiable x" by simp moreover - have "\x. a < x \ x < b \ (\x. g b - g a) differentiable x" by (simp add: differentiable_const) - with fd have "\x. a < x \ x < b \ (\x. (g b - g a) * f x) differentiable x" by (simp add: differentiable_mult) - ultimately show ?thesis by (simp add: differentiable_diff) + have "\x. a < x \ x < b \ (\x. g b - g a) differentiable x" by simp + with fd have "\x. a < x \ x < b \ (\x. (g b - g a) * f x) differentiable x" by simp + ultimately show ?thesis by simp qed ultimately have "\l z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" by (rule MVT) then obtain l where ldef: "\z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" .. diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Divides.thy Fri Feb 19 09:35:18 2010 +0100 @@ -1090,7 +1090,7 @@ lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2" apply (subgoal_tac "m mod 2 < 2") apply (erule less_2_cases [THEN disjE]) -apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1) +apply (simp_all (no_asm_simp) add: Let_def mod_Suc) done lemma mod2_gr_0 [simp]: "0 < (m\nat) mod 2 \ m mod 2 = 1" @@ -1929,7 +1929,7 @@ apply (rule order_le_less_trans) apply (erule_tac [2] mult_strict_right_mono) apply (rule mult_left_mono_neg) - using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps pos_mod_bound) + using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps) apply (simp) apply (simp) done @@ -1954,7 +1954,7 @@ apply (erule mult_strict_right_mono) apply (rule_tac [2] mult_left_mono) apply simp - using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps pos_mod_bound) + using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps) apply simp done diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Equiv_Relations.thy Fri Feb 19 09:35:18 2010 +0100 @@ -328,7 +328,7 @@ apply assumption apply simp apply(fastsimp simp add:inj_on_def) -apply (simp add:setsum_constant) +apply simp done end diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Fields.thy --- a/src/HOL/Fields.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Fields.thy Fri Feb 19 09:35:18 2010 +0100 @@ -230,7 +230,7 @@ lemma inverse_minus_eq [simp]: "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})" proof cases - assume "a=0" thus ?thesis by (simp add: inverse_zero) + assume "a=0" thus ?thesis by simp next assume "a\0" thus ?thesis by (simp add: nonzero_inverse_minus_eq) @@ -283,13 +283,13 @@ lemma mult_divide_mult_cancel_left: "c\0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})" apply (cases "b = 0") -apply (simp_all add: nonzero_mult_divide_mult_cancel_left) +apply simp_all done lemma mult_divide_mult_cancel_right: "c\0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})" apply (cases "b = 0") -apply (simp_all add: nonzero_mult_divide_mult_cancel_right) +apply simp_all done lemma divide_divide_eq_right [simp,noatp]: @@ -339,7 +339,7 @@ assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::linordered_field)" proof - have "0 < a * inverse a" - by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one) + by (simp add: a_gt_0 [THEN order_less_imp_not_eq2]) thus "0 < inverse a" by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff) qed @@ -524,8 +524,7 @@ lemma one_le_inverse_iff: "(1 \ inverse x) = (0 < x & x \ (1::'a::{linordered_field,division_by_zero}))" -by (force simp add: order_le_less one_less_inverse_iff zero_less_one - eq_commute [of 1]) +by (force simp add: order_le_less one_less_inverse_iff) lemma inverse_less_1_iff: "(inverse x < 1) = (x \ 0 | 1 < (x::'a::{linordered_field,division_by_zero}))" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Finite_Set.thy Fri Feb 19 09:35:18 2010 +0100 @@ -355,7 +355,7 @@ apply (induct set: finite) apply simp_all apply (subst vimage_insert) - apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) + apply (simp add: finite_subset [OF inj_vimage_singleton]) done lemma finite_vimageD: @@ -485,7 +485,7 @@ next assume "finite A" thus "finite (Pow A)" - by induct (simp_all add: finite_UnI finite_imageI Pow_insert) + by induct (simp_all add: Pow_insert) qed lemma finite_Collect_subsets[simp,intro]: "finite A \ finite{B. B \ A}" @@ -634,7 +634,7 @@ from aA obtain k where hkeq: "h k = a" and klessn: "k x \ A \ fold f z (insert x A) = fold f (f x z) A" -by (simp add: fold_insert fold_fun_comm) +by (simp add: fold_fun_comm) lemma fold_rec: assumes "finite A" and "x \ A" @@ -824,8 +824,8 @@ lemma fun_left_comm_idem: "fun_left_comm_idem(op *)" apply unfold_locales - apply (simp add: mult_ac) -apply (simp add: mult_idem mult_assoc[symmetric]) + apply (rule mult_left_commute) +apply (rule mult_left_idem) done end @@ -1366,7 +1366,7 @@ lemma (in comm_monoid_mult) fold_image_1: "finite S \ (\x\S. f x = 1) \ fold_image op * f 1 S = 1" apply (induct set: finite) - apply simp by (auto simp add: fold_image_insert) + apply simp by auto lemma (in comm_monoid_mult) fold_image_Un_one: assumes fS: "finite S" and fT: "finite T" @@ -1412,8 +1412,8 @@ next case (2 T F) then have fTF: "finite T" "\T\F. finite T" "finite F" and TF: "T \ F" - and H: "setsum f (\ F) = setsum (setsum f) F" by (auto simp add: finite_insert) - from fTF have fUF: "finite (\F)" by (auto intro: finite_Union) + and H: "setsum f (\ F) = setsum (setsum f) F" by auto + from fTF have fUF: "finite (\F)" by auto from "2.prems" TF fTF show ?case by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f]) @@ -2056,7 +2056,7 @@ shows "abs (setprod f A) = setprod (\x. abs (f x)) A" proof (cases "finite A") case True thus ?thesis - by induct (auto simp add: field_simps setprod_insert abs_mult) + by induct (auto simp add: field_simps abs_mult) qed auto @@ -2215,7 +2215,7 @@ (\c1 \ C. \c2 \ C. c1 \ c2 --> c1 \ c2 = {}) --> k * card(C) = card (\ C)" apply (erule finite_induct, simp) -apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition +apply (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\ (insert x F)"]) done @@ -2285,7 +2285,7 @@ lemma setprod_constant: "finite A ==> (\x\ A. (y::'a::{comm_monoid_mult})) = y^(card A)" apply (erule finite_induct) -apply (auto simp add: power_Suc) +apply auto done lemma setprod_gen_delta: @@ -2370,7 +2370,7 @@ lemma card_image_le: "finite A ==> card (f ` A) <= card A" apply (induct set: finite) apply simp -apply (simp add: le_SucI finite_imageI card_insert_if) +apply (simp add: le_SucI card_insert_if) done lemma card_image: "inj_on f A ==> card (f ` A) = card A" @@ -2473,7 +2473,7 @@ apply(rotate_tac -1) apply (induct set: finite, simp_all, clarify) apply (subst card_Un_disjoint) - apply (auto simp add: dvd_add disjoint_eq_subset_Compl) + apply (auto simp add: disjoint_eq_subset_Compl) done @@ -2514,7 +2514,7 @@ ultimately have "finite (UNIV::nat set)" by (rule finite_imageD) then show "False" - by (simp add: infinite_UNIV_nat) + by simp qed subsection{* A fold functional for non-empty sets *} @@ -2542,7 +2542,7 @@ lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)" -by (blast intro: fold_graph.intros elim: fold_graph.cases) +by (blast elim: fold_graph.cases) lemma fold1_singleton [simp]: "fold1 f {a} = a" by (unfold fold1_def) blast @@ -2612,9 +2612,9 @@ apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times]) apply (rule sym, clarify) apply (case_tac "Aa=A") - apply (best intro: the_equality fold_graph_determ) + apply (best intro: fold_graph_determ) apply (subgoal_tac "fold_graph times a A x") - apply (best intro: the_equality fold_graph_determ) + apply (best intro: fold_graph_determ) apply (subgoal_tac "insert aa (Aa - {a}) = A") prefer 2 apply (blast elim: equalityE) apply (auto dest: fold_graph_permute_diff [where a=a]) @@ -2658,16 +2658,16 @@ thus ?thesis proof cases assume "A' = {}" - with prems show ?thesis by (simp add: mult_idem) + with prems show ?thesis by simp next assume "A' \ {}" with prems show ?thesis - by (simp add: fold1_insert mult_assoc [symmetric] mult_idem) + by (simp add: fold1_insert mult_assoc [symmetric]) qed next assume "a \ x" with prems show ?thesis - by (simp add: insert_commute fold1_eq_fold fold_insert_idem) + by (simp add: insert_commute fold1_eq_fold) qed qed @@ -2710,7 +2710,7 @@ text{* Now the recursion rules for definitions: *} lemma fold1_singleton_def: "g = fold1 f \ g {a} = a" -by(simp add:fold1_singleton) +by simp lemma (in ab_semigroup_mult) fold1_insert_def: "\ g = fold1 times; finite A; x \ A; A \ {} \ \ g (insert x A) = x * g A" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/GCD.thy Fri Feb 19 09:35:18 2010 +0100 @@ -156,7 +156,7 @@ and "x <= 0 \ y >= 0 \ P (gcd (-x) y)" and "x <= 0 \ y <= 0 \ P (gcd (-x) (-y))" shows "P (gcd x y)" -by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith) +by (insert assms, auto, arith) lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" by (simp add: gcd_int_def) @@ -457,7 +457,7 @@ apply (case_tac "y > 0") apply (subst gcd_non_0_int, auto) apply (insert gcd_non_0_int [of "-y" "-x"]) - apply (auto simp add: gcd_neg1_int gcd_neg2_int) + apply auto done lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n" @@ -557,7 +557,7 @@ then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def) - have "?g \ 0" using nz by (simp add: gcd_zero_nat) + have "?g \ 0" using nz by simp then have gp: "?g > 0" by arith from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" . with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp @@ -824,7 +824,7 @@ {assume "?g = 0" with ab n have ?thesis by auto } moreover {assume z: "?g \ 0" - hence zn: "?g ^ n \ 0" using n by (simp add: neq0_conv) + hence zn: "?g ^ n \ 0" using n by simp from gcd_coprime_exists_nat[OF z] obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast @@ -852,7 +852,7 @@ {assume "?g = 0" with ab n have ?thesis by auto } moreover {assume z: "?g \ 0" - hence zn: "?g ^ n \ 0" using n by (simp add: neq0_conv) + hence zn: "?g ^ n \ 0" using n by simp from gcd_coprime_exists_int[OF z] obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast @@ -1109,7 +1109,7 @@ (a * x = (a + b) * y + d \ (a + b) * x = a * y + d)" using ex apply clarsimp - apply (rule_tac x="d" in exI, simp add: dvd_add) + apply (rule_tac x="d" in exI, simp) apply (case_tac "a * x = b * y + d" , simp_all) apply (rule_tac x="x + y" in exI) apply (rule_tac x="y" in exI) @@ -1124,10 +1124,10 @@ apply(induct a b rule: ind_euclid) apply blast apply clarify - apply (rule_tac x="a" in exI, simp add: dvd_add) + apply (rule_tac x="a" in exI, simp) apply clarsimp apply (rule_tac x="d" in exI) - apply (case_tac "a * x = b * y + d", simp_all add: dvd_add) + apply (case_tac "a * x = b * y + d", simp_all) apply (rule_tac x="x+y" in exI) apply (rule_tac x="y" in exI) apply algebra @@ -1693,8 +1693,7 @@ "inj_on f A \ inj_on g B \ ALL a:A. ALL b:B. coprime (f a) (g b) \ inj_on (%(a,b). f a * g b::nat) (A \ B)" apply(auto simp add:inj_on_def) -apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat - dvd.neq_le_trans dvd_triv_left) +apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left) apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_right mult_commute) done diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Groebner_Basis.thy Fri Feb 19 09:35:18 2010 +0100 @@ -143,16 +143,16 @@ next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr) next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp -next show "mul x x = pwr x 2" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c) +next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c) next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul) next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr) next show "pwr x 0 = r1" using pwr_0 . -next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c) +next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c) next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp -next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr) +next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr) next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))" - by (simp add: nat_number pwr_Suc mul_pwr) + by (simp add: nat_number' pwr_Suc mul_pwr) qed @@ -165,7 +165,7 @@ interpretation class_semiring: gb_semiring "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1" - proof qed (auto simp add: algebra_simps power_Suc) + proof qed (auto simp add: algebra_simps) lemmas nat_arith = add_nat_number_of @@ -175,7 +175,7 @@ less_nat_number_of lemma not_iszero_Numeral1: "\ iszero (Numeral1::'a::number_ring)" - by (simp add: numeral_1_eq_1) + by simp lemmas comp_arith = Let_def arith_simps nat_arith rel_simps neg_simps if_False @@ -350,7 +350,7 @@ interpretation class_ringb: ringb "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus" -proof(unfold_locales, simp add: algebra_simps power_Suc, auto) +proof(unfold_locales, simp add: algebra_simps, auto) fix w x y z ::"'a::{idom,number_ring}" assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" hence ynz': "y - z \ 0" by simp @@ -366,7 +366,7 @@ interpretation natgb: semiringb "op +" "op *" "op ^" "0::nat" "1" -proof (unfold_locales, simp add: algebra_simps power_Suc) +proof (unfold_locales, simp add: algebra_simps) fix w x y z ::"nat" { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" hence "y < z \ y > z" by arith @@ -375,13 +375,13 @@ then obtain k where kp: "k>0" and yz:"z = y + k" by blast from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps) hence "x*k = w*k" by simp - hence "w = x" using kp by (simp add: mult_cancel2) } + hence "w = x" using kp by simp } moreover { assume lt: "y >z" hence "\k. y = z + k \ k>0" by (rule_tac x="y - z" in exI, auto) then obtain k where kp: "k>0" and yz:"y = z + k" by blast from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps) hence "w*k = x*k" by simp - hence "w = x" using kp by (simp add: mult_cancel2)} + hence "w = x" using kp by simp } ultimately have "w=x" by blast } thus "(w * y + x * z = w * z + x * y) = (w = x \ y = z)" by auto qed diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Groups.thy --- a/src/HOL/Groups.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Groups.thy Fri Feb 19 09:35:18 2010 +0100 @@ -347,6 +347,8 @@ lemma eq_iff_diff_eq_0: "a = b \ a - b = 0" by (simp add: algebra_simps) +(* FIXME: duplicates right_minus_eq from class group_add *) +(* but only this one is declared as a simp rule. *) lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \ a = b" by (simp add: algebra_simps) @@ -794,7 +796,7 @@ proof assume assm: "a + a = 0" then have a: "- a = a" by (rule minus_unique) - then show "a = 0" by (simp add: neg_equal_zero) + then show "a = 0" by (simp only: neg_equal_zero) qed simp lemma double_zero_sym [simp]: @@ -807,7 +809,7 @@ assume "0 < a + a" then have "0 - a < a" by (simp only: diff_less_eq) then have "- a < a" by simp - then show "0 < a" by (simp add: neg_less_nonneg) + then show "0 < a" by (simp only: neg_less_nonneg) next assume "0 < a" with this have "0 + 0 < a + a" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Hilbert_Choice.thy Fri Feb 19 09:35:18 2010 +0100 @@ -61,7 +61,7 @@ by (blast intro: someI2) lemma some1_equality: "[| EX!x. P x; P a |] ==> (SOME x. P x) = a" -by (blast intro: some_equality) +by blast lemma some_eq_ex: "P (SOME x. P x) = (\x. P x)" by (blast intro: someI) @@ -108,7 +108,7 @@ done lemma inv_f_f: "inj f ==> inv f (f x) = x" -by (simp add: inv_into_f_f) +by simp lemma f_inv_into_f: "y : f`A ==> f (inv_into A f y) = y" apply (simp add: inv_into_def) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Int.thy --- a/src/HOL/Int.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Int.thy Fri Feb 19 09:35:18 2010 +0100 @@ -391,6 +391,7 @@ lemma nat_int [simp]: "nat (of_nat n) = n" by (simp add: nat int_def) +(* FIXME: duplicates nat_0 *) lemma nat_zero [simp]: "nat 0 = 0" by (simp add: Zero_int_def nat) @@ -626,10 +627,10 @@ lemmas max_number_of [simp] = max_def - [of "number_of u" "number_of v", standard, simp] + [of "number_of u" "number_of v", standard] and min_number_of [simp] = min_def - [of "number_of u" "number_of v", standard, simp] + [of "number_of u" "number_of v", standard] -- {* unfolding @{text minx} and @{text max} on numerals *} lemmas numeral_simps = @@ -1060,7 +1061,7 @@ lemma not_iszero_1: "~ iszero 1" by (simp add: iszero_def eq_commute) -lemma eq_number_of_eq: +lemma eq_number_of_eq [simp]: "((number_of x::'a::number_ring) = number_of y) = iszero (number_of (x + uminus y) :: 'a)" unfolding iszero_def number_of_add number_of_minus @@ -1130,7 +1131,7 @@ by (auto simp add: iszero_def number_of_eq numeral_simps) qed -lemmas iszero_simps = +lemmas iszero_simps [simp] = iszero_0 not_iszero_1 iszero_number_of_Pls nonzero_number_of_Min iszero_number_of_Bit0 iszero_number_of_Bit1 @@ -1218,7 +1219,7 @@ "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \ x = y" unfolding number_of_eq by (rule of_int_eq_iff) -lemmas rel_simps [simp] = +lemmas rel_simps = less_number_of less_bin_simps le_number_of le_bin_simps eq_number_of_eq eq_bin_simps @@ -1240,7 +1241,7 @@ lemma add_number_of_diff1: "number_of v + (number_of w - c) = number_of(v + w) - (c::'a::number_ring)" - by (simp add: diff_minus add_number_of_left) + by (simp add: diff_minus) lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) = @@ -1437,7 +1438,7 @@ text{*Allow 1 on either or both sides*} lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)" -by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq) +by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric]) lemmas add_special = one_add_one_is_two @@ -1558,6 +1559,7 @@ lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp] +(* FIXME: duplicates nat_zero *) lemma nat_0: "nat 0 = 0" by (simp add: nat_eq_iff) @@ -1980,7 +1982,7 @@ lemma minus1_divide [simp]: "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" -by (simp add: divide_inverse inverse_minus_eq) +by (simp add: divide_inverse) lemma half_gt_zero_iff: "(0 < r/2) = (0 < (r::'a::{linordered_field,division_by_zero,number_ring}))" @@ -2098,7 +2100,7 @@ assumes mp:"m \(0::int)" shows "(m * n dvd m) = (\n\ = 1)" proof assume n1: "\n\ = 1" thus "m * n dvd m" - by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff) + by (cases "n >0", auto simp add: minus_equation_iff) next assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp from zdvd_mult_cancel[OF H2 mp] show "\n\ = 1" by (simp only: zdvd1_eq) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/List.thy --- a/src/HOL/List.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/List.thy Fri Feb 19 09:35:18 2010 +0100 @@ -257,9 +257,9 @@ @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\ @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\ -@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\ -@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\ -@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\ +@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\ +@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\ +@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\ @{lemma "listsum [1,2,3::nat] = 6" by simp} \end{tabular}} \caption{Characteristic examples} @@ -720,6 +720,11 @@ lemma map_map [simp]: "map f (map g xs) = map (f \ g) xs" by (induct xs) auto +lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)" +apply(rule ext) +apply(simp) +done + lemma rev_map: "rev (map f xs) = map f (rev xs)" by (induct xs) auto diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Nat.thy Fri Feb 19 09:35:18 2010 +0100 @@ -1356,7 +1356,7 @@ end lemma of_nat_id [simp]: "of_nat n = n" - by (induct n) (auto simp add: One_nat_def) + by (induct n) simp_all lemma of_nat_eq_id [simp]: "of_nat = id" by (auto simp add: expand_fun_eq) @@ -1619,7 +1619,7 @@ lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)" unfolding dvd_def - by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff) + by (force dest: mult_eq_self_implies_10 simp add: mult_assoc) text {* @{term "op dvd"} is a partial order *} diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Nat_Numeral.thy Fri Feb 19 09:35:18 2010 +0100 @@ -211,7 +211,7 @@ "0 \ a ^ (2*n)" proof (induct n) case 0 - show ?case by (simp add: zero_le_one) + show ?case by simp next case (Suc n) have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" @@ -262,7 +262,7 @@ by (simp add: neg_def) lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))" -by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc) +by (simp add: neg_def del: of_nat_Suc) lemmas neg_eq_less_0 = neg_def @@ -275,7 +275,7 @@ by (simp add: One_int_def neg_def) lemma not_neg_1: "~ neg 1" -by (simp add: neg_def linorder_not_less zero_le_one) +by (simp add: neg_def linorder_not_less) lemma neg_nat: "neg z ==> nat z = 0" by (simp add: neg_def order_less_imp_le) @@ -310,7 +310,7 @@ subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*} -declare nat_0 [simp] nat_1 [simp] +declare nat_1 [simp] lemma nat_number_of [simp]: "nat (number_of w) = number_of w" by (simp add: nat_number_of_def) @@ -319,10 +319,10 @@ by (simp add: nat_number_of_def) lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)" -by (simp add: nat_1 nat_number_of_def) +by (simp add: nat_number_of_def) lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0" -by (simp add: nat_numeral_1_eq_1) +by (simp only: nat_numeral_1_eq_1 One_nat_def) subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*} @@ -469,7 +469,7 @@ subsubsection{*Nat *} lemma Suc_pred': "0 < n ==> n = Suc(n - 1)" -by (simp add: numerals) +by simp (*Expresses a natural number constant as the Suc of another one. NOT suitable for rewriting because n recurs in the condition.*) @@ -478,10 +478,10 @@ subsubsection{*Arith *} lemma Suc_eq_plus1: "Suc n = n + 1" -by (simp add: numerals) + unfolding One_nat_def by simp lemma Suc_eq_plus1_left: "Suc n = 1 + n" -by (simp add: numerals) + unfolding One_nat_def by simp (* These two can be useful when m = number_of... *) @@ -563,13 +563,13 @@ "(number_of v <= Suc n) = (let pv = number_of (Int.pred v) in if neg pv then True else nat pv <= n)" -by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric]) +by (simp add: Let_def linorder_not_less [symmetric]) lemma le_Suc_number_of [simp]: "(Suc n <= number_of v) = (let pv = number_of (Int.pred v) in if neg pv then False else n <= nat pv)" -by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric]) +by (simp add: Let_def linorder_not_less [symmetric]) lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min" @@ -660,7 +660,7 @@ power_number_of_odd [of "number_of v", standard] lemma nat_number_of_Pls: "Numeral0 = (0::nat)" - by (simp add: number_of_Pls nat_number_of_def) + by (simp add: nat_number_of_def) lemma nat_number_of_Min: "number_of Int.Min = (0::nat)" apply (simp only: number_of_Min nat_number_of_def nat_zminus_int) @@ -684,6 +684,9 @@ nat_number_of_Pls nat_number_of_Min nat_number_of_Bit0 nat_number_of_Bit1 +lemmas nat_number' = + nat_number_of_Bit0 nat_number_of_Bit1 + lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" by (fact Let_def) @@ -736,7 +739,7 @@ text{*Where K above is a literal*} lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)" -by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split) +by (simp split: nat_diff_split) text {*Now just instantiating @{text n} to @{text "number_of v"} does the right simplification, but with some redundant inequality @@ -761,7 +764,7 @@ done lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" -by (simp add: numerals split add: nat_diff_split) +by (simp split: nat_diff_split) subsubsection{*For @{term nat_case} and @{term nat_rec}*} diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/NthRoot.thy Fri Feb 19 09:35:18 2010 +0100 @@ -566,7 +566,7 @@ done lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u" -by (simp add: divide_less_eq mult_compare_simps) +by (simp add: divide_less_eq) lemma four_x_squared: fixes x::real diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/PReal.thy --- a/src/HOL/PReal.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/PReal.thy Fri Feb 19 09:35:18 2010 +0100 @@ -750,7 +750,7 @@ have frle: "Fract a b \ Fract ?k 1 * (Fract c d)" proof - have "?thesis = ((a * d * b * d) \ c * b * (a * d * b * d))" - by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac) + by (simp add: order_less_imp_not_eq2 mult_ac) moreover have "(1 * (a * d * b * d)) \ c * b * (a * d * b * d)" by (rule mult_mono, @@ -822,7 +822,7 @@ also with ypos have "... = (r/y) * (y + ?d)" by (simp only: algebra_simps divide_inverse, simp) also have "... = r*x" using ypos - by (simp add: times_divide_eq_left) + by simp finally show "r + ?d < r*x" . qed with r notin rdpos diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Parity.thy Fri Feb 19 09:35:18 2010 +0100 @@ -184,7 +184,7 @@ apply (rule conjI) apply simp apply (insert even_zero_nat, blast) - apply (simp add: power_Suc) + apply simp done lemma minus_one_even_power [simp]: @@ -199,7 +199,7 @@ "(even x --> (-1::'a::{number_ring})^x = 1) & (odd x --> (-1::'a)^x = -1)" apply (induct x) - apply (simp, simp add: power_Suc) + apply (simp, simp) done lemma neg_one_even_power [simp]: @@ -214,7 +214,7 @@ "(-x::'a::{comm_ring_1}) ^ n = (if even n then (x ^ n) else -(x ^ n))" apply (induct n) - apply (simp_all split: split_if_asm add: power_Suc) + apply simp_all done lemma zero_le_even_power: "even n ==> @@ -228,7 +228,7 @@ lemma zero_le_odd_power: "odd n ==> (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)" -apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff) +apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff) apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square) done @@ -373,7 +373,7 @@ lemma even_power_le_0_imp_0: "a ^ (2*k) \ (0::'a::{linordered_idom}) ==> a=0" - by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) + by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff) lemma zero_le_power_iff[presburger]: "(0 \ a^n) = (0 \ (a::'a::{linordered_idom}) | even n)" @@ -387,7 +387,7 @@ then obtain k where "n = Suc(2*k)" by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) thus ?thesis - by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power + by (auto simp add: zero_le_mult_iff zero_le_even_power dest!: even_power_le_0_imp_0) qed diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Power.thy --- a/src/HOL/Power.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Power.thy Fri Feb 19 09:35:18 2010 +0100 @@ -332,7 +332,7 @@ lemma abs_power_minus [simp]: "abs ((-a) ^ n) = abs (a ^ n)" - by (simp add: abs_minus_cancel power_abs) + by (simp add: power_abs) lemma zero_less_power_abs_iff [simp, noatp]: "0 < abs a ^ n \ a \ 0 \ n = 0" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Presburger.thy Fri Feb 19 09:35:18 2010 +0100 @@ -199,16 +199,16 @@ hence "P 0" using P Pmod by simp moreover have "P 0 = P(0 - (-1)*d)" using modd by blast ultimately have "P d" by simp - moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff) + moreover have "d : {1..d}" using dpos by simp ultimately show ?RHS .. next assume not0: "x mod d \ 0" - have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) + have "P(x mod d)" using dpos P Pmod by simp moreover have "x mod d : {1..d}" proof - from dpos have "0 \ x mod d" by(rule pos_mod_sign) moreover from dpos have "x mod d < d" by(rule pos_mod_bound) - ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) + ultimately show ?thesis using not0 by simp qed ultimately show ?RHS .. qed diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Rational.thy --- a/src/HOL/Rational.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Rational.thy Fri Feb 19 09:35:18 2010 +0100 @@ -428,7 +428,7 @@ fix q :: rat assume "q \ 0" then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero) - (simp_all add: mult_rat inverse_rat rat_number_expand eq_rat) + (simp_all add: rat_number_expand eq_rat) next fix q r :: rat show "q / r = q * inverse r" by (simp add: divide_rat_def) @@ -592,7 +592,7 @@ abs_rat_def [code del]: "\q\ = (if q < 0 then -q else (q::rat))" lemma abs_rat [simp, code]: "\Fract a b\ = Fract \a\ \b\" - by (auto simp add: abs_rat_def zabs_def Zero_rat_def less_rat not_less le_less minus_rat eq_rat zero_compare_simps) + by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff) definition sgn_rat_def [code del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/RealDef.thy Fri Feb 19 09:35:18 2010 +0100 @@ -767,7 +767,8 @@ lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0" by (simp add: add: real_of_nat_def) -lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \ real (n::nat))" +(* FIXME: duplicates real_of_nat_ge_zero *) +lemma real_of_nat_ge_zero_cancel_iff: "(0 \ real (n::nat))" by (simp add: add: real_of_nat_def) lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)" @@ -951,13 +952,13 @@ text{*Collapse applications of @{term real} to @{term number_of}*} lemma real_number_of [simp]: "real (number_of v :: int) = number_of v" -by (simp add: real_of_int_def of_int_number_of_eq) +by (simp add: real_of_int_def) lemma real_of_nat_number_of [simp]: "real (number_of v :: nat) = (if neg (number_of v :: int) then 0 else (number_of v :: real))" -by (simp add: real_of_int_real_of_nat [symmetric] int_nat_number_of) +by (simp add: real_of_int_real_of_nat [symmetric]) declaration {* K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2] diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/RealPow.thy --- a/src/HOL/RealPow.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/RealPow.thy Fri Feb 19 09:35:18 2010 +0100 @@ -19,8 +19,8 @@ apply (induct "n") apply (auto simp add: real_of_nat_Suc) apply (subst mult_2) -apply (rule add_less_le_mono) -apply (auto simp add: two_realpow_ge_one) +apply (erule add_less_le_mono) +apply (rule two_realpow_ge_one) done lemma realpow_Suc_le_self: "[| 0 \ r; r \ (1::real) |] ==> r ^ Suc n \ r" @@ -57,7 +57,7 @@ lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)" apply (induct "n") -apply (auto simp add: real_of_nat_mult zero_less_mult_iff) +apply (auto simp add: zero_less_mult_iff) done (* used by AFP Integration theory *) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/RealVector.thy --- a/src/HOL/RealVector.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/RealVector.thy Fri Feb 19 09:35:18 2010 +0100 @@ -268,7 +268,7 @@ by (induct n) simp_all lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)" -by (simp add: of_real_def scaleR_cancel_right) +by (simp add: of_real_def) lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified] diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Rings.thy --- a/src/HOL/Rings.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Rings.thy Fri Feb 19 09:35:18 2010 +0100 @@ -315,7 +315,7 @@ qed lemma dvd_diff[simp]: "x dvd y \ x dvd z \ x dvd (y - z)" -by (simp add: diff_minus dvd_minus_iff) +by (simp only: diff_minus dvd_add dvd_minus_iff) end @@ -336,16 +336,16 @@ "a * c = b * c \ c = 0 \ a = b" proof - have "(a * c = b * c) = ((a - b) * c = 0)" - by (simp add: algebra_simps right_minus_eq) - thus ?thesis by (simp add: disj_commute right_minus_eq) + by (simp add: algebra_simps) + thus ?thesis by (simp add: disj_commute) qed lemma mult_cancel_left [simp, noatp]: "c * a = c * b \ c = 0 \ a = b" proof - have "(c * a = c * b) = (c * (a - b) = 0)" - by (simp add: algebra_simps right_minus_eq) - thus ?thesis by (simp add: right_minus_eq) + by (simp add: algebra_simps) + thus ?thesis by simp qed end @@ -382,7 +382,7 @@ then have "(a - b) * (a + b) = 0" by (simp add: algebra_simps) then show "a = b \ a = - b" - by (simp add: right_minus_eq eq_neg_iff_add_eq_0) + by (simp add: eq_neg_iff_add_eq_0) next assume "a = b \ a = - b" then show "a * a = b * b" by auto @@ -764,13 +764,13 @@ lemma mult_left_mono_neg: "b \ a \ c \ 0 \ c * a \ c * b" apply (drule mult_left_mono [of _ _ "uminus c"]) - apply (simp_all add: minus_mult_left [symmetric]) + apply simp_all done lemma mult_right_mono_neg: "b \ a \ c \ 0 \ a * c \ b * c" apply (drule mult_right_mono [of _ _ "uminus c"]) - apply (simp_all add: minus_mult_right [symmetric]) + apply simp_all done lemma mult_nonpos_nonpos: "a \ 0 \ b \ 0 \ 0 \ a * b" @@ -791,11 +791,10 @@ proof fix a b show "\a + b\ \ \a\ + \b\" - by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) - (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric] - neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg, - auto intro!: less_imp_le add_neg_neg) -qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero) + by (auto simp add: abs_if not_less) + (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric], + auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg) +qed (auto simp add: abs_if) end @@ -864,14 +863,14 @@ lemma mult_less_0_iff: "a * b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b" - apply (insert zero_less_mult_iff [of "-a" b]) - apply (force simp add: minus_mult_left[symmetric]) + apply (insert zero_less_mult_iff [of "-a" b]) + apply force done lemma mult_le_0_iff: "a * b \ 0 \ 0 \ a \ b \ 0 \ a \ 0 \ 0 \ b" apply (insert zero_le_mult_iff [of "-a" b]) - apply (force simp add: minus_mult_left[symmetric]) + apply force done lemma zero_le_square [simp]: "0 \ a * a" @@ -1056,11 +1055,11 @@ lemma sgn_1_pos: "sgn a = 1 \ a > 0" -unfolding sgn_if by (simp add: neg_equal_zero) +unfolding sgn_if by simp lemma sgn_1_neg: "sgn a = - 1 \ a < 0" -unfolding sgn_if by (auto simp add: equal_neg_zero) +unfolding sgn_if by auto lemma sgn_pos [simp]: "0 < a \ sgn a = 1" @@ -1116,11 +1115,11 @@ lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1 ==> x * y <= x" -by (auto simp add: mult_compare_simps) +by (auto simp add: mult_le_cancel_left2) lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1 ==> y * x <= x" -by (auto simp add: mult_compare_simps) +by (auto simp add: mult_le_cancel_right2) context linordered_semidom begin @@ -1159,7 +1158,7 @@ begin subclass ordered_ring_abs proof -qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff) +qed (auto simp add: abs_if not_less mult_less_0_iff) lemma abs_mult: "abs (a * b) = abs a * abs b" @@ -1187,7 +1186,7 @@ lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))" apply (simp add: order_less_le abs_le_iff) -apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos) +apply (auto simp add: abs_if) done lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/SEQ.thy Fri Feb 19 09:35:18 2010 +0100 @@ -573,7 +573,7 @@ apply (rule allI, rule impI, rule ext) apply (erule conjE) apply (induct_tac x) -apply (simp add: nat_rec_0) +apply simp apply (erule_tac x="n" in allE) apply (simp) done diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/SetInterval.thy Fri Feb 19 09:35:18 2010 +0100 @@ -539,7 +539,7 @@ apply (rule subset_antisym) apply (rule UN_finite2_subset, blast) apply (rule UN_finite2_subset [where k=k]) - apply (force simp add: atLeastLessThan_add_Un [of 0] UN_Un) + apply (force simp add: atLeastLessThan_add_Un [of 0]) done @@ -613,7 +613,7 @@ apply (unfold image_def lessThan_def) apply auto apply (rule_tac x = "nat x" in exI) - apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym]) + apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) done lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..i. card {j\T. R i j}) S = k * card T" (is "?l = ?r") proof- have "?l = setsum (\i. k) T" by(rule setsum_multicount_gen)(auto simp:assms) - also have "\ = ?r" by(simp add: setsum_constant mult_commute) + also have "\ = ?r" by(simp add: mult_commute) finally show ?thesis by auto qed @@ -1046,7 +1046,7 @@ lemma geometric_sum: "x ~= 1 ==> (\i=0..x. x \ X \ z \ x" shows "z \ Inf X" proof - - have "Sup (uminus ` X) \ -z" using x z by (force intro: Sup_least) + have "Sup (uminus ` X) \ -z" using x z by force hence "z \ - Sup (uminus ` X)" by simp thus ?thesis @@ -306,7 +306,7 @@ case True thus ?thesis by (simp add: min_def) - (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z) + (blast intro: Inf_eq_minimum real_le_refl real_le_trans z) next case False hence 1:"Inf X < a" by simp @@ -441,7 +441,7 @@ proof (rule exI [where x = "Sup {d. \x. a \ x & x < d --> P x}"], auto) show "a \ Sup {d. \c. a \ c \ c < d \ P c}" by (rule SupInf.Sup_upper [where z=b], auto) - (metis prems real_le_linear real_less_def) + (metis `a < b` `\ P b` real_le_linear real_less_def) next show "Sup {d. \c. a \ c \ c < d \ P c} \ b" apply (rule SupInf.Sup_least) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Tools/typedef.ML Fri Feb 19 09:35:18 2010 +0100 @@ -14,10 +14,10 @@ Rep_induct: thm, Abs_induct: thm} val add_typedef: bool -> binding option -> binding * string list * mixfix -> term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory - val typedef: (bool * binding) * (binding * string list * mixfix) * term - * (binding * binding) option -> theory -> Proof.state - val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string - * (binding * binding) option -> theory -> Proof.state + val typedef: (bool * binding) * (binding * string list * mixfix) * term * + (binding * binding) option -> theory -> Proof.state + val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string * + (binding * binding) option -> theory -> Proof.state val get_info: theory -> string -> info option val the_info: theory -> string -> info val interpretation: (string -> theory -> theory) -> theory -> theory @@ -118,9 +118,9 @@ fun add_def theory = if def then theory - |> Sign.add_consts_i [(name, setT', NoSyn)] - |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name) - (Primitive_Defs.mk_defpair (setC, set)))] + |> Sign.add_consts_i [(name, setT', NoSyn)] (* FIXME authentic syntax *) + |> PureThy.add_defs false + [((Binding.map_name Thm.def_name name, Logic.mk_equals (setC, set)), [])] |-> (fn [th] => pair (SOME th)) else (NONE, theory); fun contract_def NONE th = th @@ -164,7 +164,7 @@ [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]), ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}), [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])] - ||> Sign.parent_path; + ||> Sign.restore_naming thy1; val info = {rep_type = oldT, abs_type = newT, Rep_name = full Rep_name, Abs_name = full Abs_name, inhabited = inhabited, type_definition = type_definition, set_def = set_def, @@ -250,24 +250,20 @@ val _ = OuterKeyword.keyword "morphisms"; -val typedef_decl = - Scan.optional (P.$$$ "(" |-- - ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) - --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- - Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); - -fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = - typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs); - val _ = OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" OuterKeyword.thy_goal - (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef))); + (Scan.optional (P.$$$ "(" |-- + ((P.$$$ "open" >> K false) -- Scan.option P.binding || + P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- + (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)) + >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) => + Toplevel.print o Toplevel.theory_to_proof + (typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs)))); end; - val setup = Typedef_Interpretation.init; end; diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Transcendental.thy Fri Feb 19 09:35:18 2010 +0100 @@ -247,7 +247,7 @@ from f[OF this] show ?thesis unfolding n_eq atLeastLessThanSuc_atLeastAtMost . next - case False hence "even (n - 1)" using even_num_iff odd_pos by auto + case False hence "even (n - 1)" by simp from even_nat_div_two_times_two[OF this] have n_eq: "2 * ((n - 1) div 2) = n - 1" unfolding numeral_2_eq_2[symmetric] by auto hence range_eq: "n - 1 + 1 = n" using odd_pos[OF False] by auto @@ -848,7 +848,7 @@ hence "norm (x * S n) / real (Suc n) \ r * norm (S n)" by (simp add: pos_divide_le_eq mult_ac) thus "norm (S (Suc n)) \ r * norm (S n)" - by (simp add: S_Suc norm_scaleR inverse_eq_divide) + by (simp add: S_Suc inverse_eq_divide) qed qed @@ -860,7 +860,7 @@ by (rule summable_exp_generic) next fix n show "norm (x ^ n /\<^sub>R real (fact n)) \ norm x ^ n /\<^sub>R real (fact n)" - by (simp add: norm_scaleR norm_power_ineq) + by (simp add: norm_power_ineq) qed lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)" @@ -957,7 +957,7 @@ by (simp only: scaleR_right.setsum) finally show "S (x + y) (Suc n) = (\i=0..Suc n. S x i * S y (Suc n - i))" - by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc) + by (simp del: setsum_cl_ivl_Suc) qed lemma exp_add: "exp (x + y) = exp x * exp y" @@ -1237,7 +1237,7 @@ { fix x :: real assume "x \ {- 1<..<1}" hence "norm (-x) < 1" by auto show "summable (\n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)" unfolding One_nat_def - by (auto simp del: power_mult_distrib simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`]) + by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`]) } qed hence "DERIV (\x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto @@ -3090,7 +3090,7 @@ lemma cos_x_y_le_one: "\x / sqrt (x\ + y\)\ \ 1" apply (rule power2_le_imp_le [OF _ zero_le_one]) -apply (simp add: abs_divide power_divide divide_le_eq not_sum_power2_lt_zero) +apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero) done lemma cos_arccos_abs: "\y\ \ 1 \ cos (arccos y) = y" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Transitive_Closure.thy Fri Feb 19 09:35:18 2010 +0100 @@ -464,7 +464,7 @@ apply (rule subsetI) apply (simp only: split_tupled_all) apply (erule trancl_induct, blast) - apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans) + apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans) apply (rule subsetI) apply (blast intro: trancl_mono rtrancl_mono [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) @@ -503,7 +503,7 @@ apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major]) apply (rule cases) apply (erule conversepD) - apply (blast intro: prems dest!: tranclp_converseD conversepD) + apply (blast intro: assms dest!: tranclp_converseD) done lemmas converse_trancl_induct = converse_tranclp_induct [to_set] diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOL/Wellfounded.thy Fri Feb 19 09:35:18 2010 +0100 @@ -489,7 +489,7 @@ by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) lemma trans_less_than [iff]: "trans less_than" - by (simp add: less_than_def trans_trancl) + by (simp add: less_than_def) lemma less_than_iff [iff]: "((x,y): less_than) = (x xs = (if x:A then x~> (A(C)xs) else A(C)xs)" apply (unfold fsfilter_def) -apply (simp add: fscons_def2 sfilter_scons If_and_if) +apply (simp add: fscons_def2 If_and_if) done lemma fsfilter_emptys: "{}(C)x = UU" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/FOCUS/Fstreams.thy --- a/src/HOLCF/FOCUS/Fstreams.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/FOCUS/Fstreams.thy Fri Feb 19 09:35:18 2010 +0100 @@ -208,9 +208,6 @@ by (simp add: fsmap_def fsingleton_def2 flift2_def) -declare range_composition[simp del] - - lemma fstreams_chain_lemma[rule_format]: "ALL s x y. stream_take n$(s::'a fstream) << x & x << y & y << s & x ~= y --> stream_take (Suc n)$s << y" apply (induct_tac n, auto) @@ -225,7 +222,7 @@ apply (drule stream_prefix, auto) apply (case_tac "y=UU",auto) apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) -apply (auto simp add: stream.inverts) +apply auto apply (simp add: flat_less_iff) apply (erule_tac x="tt" in allE) apply (erule_tac x="yb" in allE, auto) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/ABP/Correctness.thy --- a/src/HOLCF/IOA/ABP/Correctness.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/ABP/Correctness.thy Fri Feb 19 09:35:18 2010 +0100 @@ -57,10 +57,12 @@ and impl_asigs = sender_asig_def receiver_asig_def declare let_weak_cong [cong] -declare Let_def [simp] ioa_triple_proj [simp] starts_of_par [simp] +declare ioa_triple_proj [simp] starts_of_par [simp] lemmas env_ioas = env_ioa_def env_asig_def env_trans_def -lemmas hom_ioas [simp] = env_ioas impl_ioas impl_trans impl_asigs asig_projections set_lemmas +lemmas hom_ioas = + env_ioas [simp] impl_ioas [simp] impl_trans [simp] impl_asigs [simp] + asig_projections set_lemmas subsection {* lemmas about reduce *} @@ -96,7 +98,7 @@ apply (induct_tac "l") apply (simp (no_asm)) apply (case_tac "list=[]") - apply (simp add: reverse.simps) + apply simp apply (rule impI) apply (simp (no_asm)) apply (cut_tac l = "list" in cons_not_nil) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/NTP/Correctness.thy --- a/src/HOLCF/IOA/NTP/Correctness.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/NTP/Correctness.thy Fri Feb 19 09:35:18 2010 +0100 @@ -50,7 +50,7 @@ apply (simp (no_asm) add: impl_ioas) apply (simp (no_asm) add: impl_asigs) apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections) - apply (simp (no_asm) add: "transitions" unfold_renaming) + apply (simp (no_asm) add: "transitions"(1) unfold_renaming) txt {* 1 *} apply (simp (no_asm) add: impl_ioas) apply (simp (no_asm) add: impl_asigs) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/NTP/Impl.thy --- a/src/HOLCF/IOA/NTP/Impl.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/NTP/Impl.thy Fri Feb 19 09:35:18 2010 +0100 @@ -61,7 +61,7 @@ subsection {* Invariants *} -declare Let_def [simp] le_SucI [simp] +declare le_SucI [simp] lemmas impl_ioas = impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection] diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/Storage/Correctness.thy --- a/src/HOLCF/IOA/Storage/Correctness.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/Storage/Correctness.thy Fri Feb 19 09:35:18 2010 +0100 @@ -18,7 +18,6 @@ in (! l:used. l < k) & b=c}" -declare split_paired_All [simp] declare split_paired_Ex [simp del] diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/meta_theory/CompoExecs.thy --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Fri Feb 19 09:35:18 2010 +0100 @@ -62,7 +62,7 @@ asig_comp sigA sigB))" -lemmas [simp del] = ex_simps all_simps split_paired_All +lemmas [simp del] = split_paired_All section "recursive equations of operators" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Fri Feb 19 09:35:18 2010 +0100 @@ -64,9 +64,6 @@ asig_comp sigA sigB))" -declare surjective_pairing [symmetric, simp] - - subsection "mkex rewrite rules" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/meta_theory/CompoTraces.thy --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Feb 19 09:35:18 2010 +0100 @@ -207,18 +207,18 @@ (* a:A, a:B *) apply simp apply (rule Forall_Conc_impl [THEN mp]) -apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act) +apply (simp add: intA_is_not_actB int_is_act) apply (rule Forall_Conc_impl [THEN mp]) -apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act) +apply (simp add: intA_is_not_actB int_is_act) (* a:A,a~:B *) apply simp apply (rule Forall_Conc_impl [THEN mp]) -apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act) +apply (simp add: intA_is_not_actB int_is_act) apply (case_tac "a:act B") (* a~:A, a:B *) apply simp apply (rule Forall_Conc_impl [THEN mp]) -apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act) +apply (simp add: intA_is_not_actB int_is_act) (* a~:A,a~:B *) apply auto done @@ -230,7 +230,7 @@ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *}) apply auto apply (rule Forall_Conc_impl [THEN mp]) -apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act) +apply (simp add: intA_is_not_actB int_is_act) done lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==> @@ -240,7 +240,7 @@ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *}) apply auto apply (rule Forall_Conc_impl [THEN mp]) -apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act) +apply (simp add: intA_is_not_actB int_is_act) done (* safe-tac makes too many case distinctions with this lemma in the next proof *) @@ -345,14 +345,12 @@ apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a>>y1" in exI) apply (rule_tac x = "y2" in exI) (* elminate all obligations up to two depending on Conc_assoc *) -apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc) +apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc) apply (simp (no_asm) add: Conc_assoc FilterConc) done lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]] -declare FilterConc [simp del] - lemma reduceB_mksch1 [rule_format]: " [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> ! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s & @@ -393,7 +391,7 @@ apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a>>x1" in exI) apply (rule_tac x = "x2" in exI) (* elminate all obligations up to two depending on Conc_assoc *) -apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc) +apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc) apply (simp (no_asm) add: Conc_assoc FilterConc) done @@ -573,7 +571,7 @@ apply (rule take_reduction) (* f A (tw iA) = tw ~eA *) -apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act) +apply (simp add: int_is_act not_ext_is_int_or_not_act) apply (rule refl) apply (simp add: int_is_act not_ext_is_int_or_not_act) apply (rotate_tac -11) @@ -582,7 +580,7 @@ (* assumption Forall tr *) (* assumption schB *) -apply (simp add: Forall_Conc ext_and_act) +apply (simp add: ext_and_act) (* assumption schA *) apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2) apply assumption @@ -595,7 +593,7 @@ (* assumption Forall schA *) apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst) apply assumption -apply (simp add: ForallPTakewhileQ int_is_act) +apply (simp add: int_is_act) (* case x:actions(asig_of A) & x: actions(asig_of B) *) @@ -623,7 +621,7 @@ apply assumption (* f A (tw iA) = tw ~eA *) -apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act) +apply (simp add: int_is_act not_ext_is_int_or_not_act) (* rewrite assumption forall and schB *) apply (rotate_tac 13) @@ -792,7 +790,7 @@ apply (rule take_reduction) (* f B (tw iB) = tw ~eB *) -apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act) +apply (simp add: int_is_act not_ext_is_int_or_not_act) apply (rule refl) apply (simp add: int_is_act not_ext_is_int_or_not_act) apply (rotate_tac -11) @@ -800,7 +798,7 @@ (* now conclusion fulfills induction hypothesis, but assumptions are not ready *) (* assumption schA *) -apply (simp add: Forall_Conc ext_and_act) +apply (simp add: ext_and_act) (* assumption schB *) apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2) apply assumption @@ -813,7 +811,7 @@ (* assumption Forall schB *) apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst) apply assumption -apply (simp add: ForallPTakewhileQ int_is_act) +apply (simp add: int_is_act) (* case x:actions(asig_of A) & x: actions(asig_of B) *) @@ -840,7 +838,7 @@ apply assumption (* f B (tw iB) = tw ~eB *) -apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act) +apply (simp add: int_is_act not_ext_is_int_or_not_act) (* rewrite assumption forall and schB *) apply (rotate_tac 13) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/meta_theory/LiveIOA.thy --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Fri Feb 19 09:35:18 2010 +0100 @@ -43,8 +43,6 @@ ((corresp_ex (fst AM) f exec) |== (snd AM))))" -declare split_paired_Ex [simp del] - lemma live_implements_trans: "!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] ==> live_implements (A,LA) (C,LC)" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/meta_theory/RefCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Fri Feb 19 09:35:18 2010 +0100 @@ -165,7 +165,7 @@ (* --------------------------------------------------- *) lemma mk_traceConc: "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)" -apply (simp add: mk_trace_def filter_act_def FilterConc MapConc) +apply (simp add: mk_trace_def filter_act_def MapConc) done diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/meta_theory/Seq.thy --- a/src/HOLCF/IOA/meta_theory/Seq.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy Fri Feb 19 09:35:18 2010 +0100 @@ -110,7 +110,6 @@ declare Finite.intros [simp] -declare seq.rews [simp] subsection {* recursive equations of operators *} @@ -361,7 +360,7 @@ lemma scons_inject_eq: "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)" -by (simp add: seq.injects) +by simp lemma nil_less_is_nil: "nil< nil=x" apply (rule_tac x="x" in seq.casedist) @@ -447,7 +446,7 @@ apply (intro strip) apply (erule Finite.cases) apply fastsimp -apply (simp add: seq.injects) +apply simp done lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)" @@ -461,7 +460,7 @@ apply (induct arbitrary: y set: Finite) apply (rule_tac x=y in seq.casedist, simp, simp, simp) apply (rule_tac x=y in seq.casedist, simp, simp) -apply (simp add: seq.inverts) +apply simp done lemma adm_Finite [simp]: "adm Finite" diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IOA/meta_theory/TLS.thy --- a/src/HOLCF/IOA/meta_theory/TLS.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy Fri Feb 19 09:35:18 2010 +0100 @@ -87,7 +87,6 @@ lemmas [simp del] = ex_simps all_simps split_paired_Ex -declare Let_def [simp] declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *} diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/IsaMakefile Fri Feb 19 09:35:18 2010 +0100 @@ -113,7 +113,9 @@ HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz -$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \ +$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \ + ex/Stream.thy \ + FOCUS/Fstreams.thy \ FOCUS/Fstream.thy FOCUS/FOCUS.thy \ FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \ FOCUS/Buffer.thy FOCUS/Buffer_adm.thy diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/Tools/pcpodef.ML Fri Feb 19 09:35:18 2010 +0100 @@ -100,7 +100,7 @@ ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []), ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []), ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])]) - ||> Sign.parent_path; + ||> Sign.restore_naming thy2; val cpo_info : cpo_info = { below_def = below_def, adm = admissible', cont_Rep = cont_Rep, cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact }; @@ -139,7 +139,7 @@ ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []), ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []), ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])]) - ||> Sign.parent_path; + ||> Sign.restore_naming thy2; val pcpo_info = { Rep_strict = Rep_strict, Abs_strict = Abs_strict, Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff, diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/Tools/repdef.ML Fri Feb 19 09:35:18 2010 +0100 @@ -139,7 +139,7 @@ |> PureThy.add_thms [((Binding.prefix_name "REP_" name, Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])] - ||> Sign.parent_path; + ||> Sign.restore_naming thy4; val rep_info = { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm }; diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Thu Feb 18 18:48:07 2010 +0100 +++ b/src/HOLCF/ex/Stream.thy Fri Feb 19 09:35:18 2010 +0100 @@ -358,8 +358,7 @@ by (drule stream_finite_lemma1,auto) lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \)" -by (rule stream.casedist [of x], auto simp del: iSuc_Fin - simp add: Fin_0 iSuc_Fin[THEN sym] i0_iless_iSuc iSuc_mono) +by (rule stream.casedist [of x], auto simp add: Fin_0 iSuc_Fin[THEN sym]) lemma slen_empty_eq: "(#x = 0) = (x = \)" by (rule stream.casedist [of x], auto) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/General/binding.ML Fri Feb 19 09:35:18 2010 +0100 @@ -22,6 +22,7 @@ val empty: binding val is_empty: binding -> bool val qualify: bool -> string -> binding -> binding + val qualified: bool -> string -> binding -> binding val qualified_name: string -> binding val qualified_name_of: binding -> string val prefix_of: binding -> (string * bool) list @@ -87,6 +88,10 @@ map_binding (fn (conceal, prefix, qualifier, name, pos) => (conceal, prefix, (qual, mandatory) :: qualifier, name, pos)); +fun qualified mandatory name' = map_binding (fn (conceal, prefix, qualifier, name, pos) => + let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)] + in (conceal, prefix, qualifier', name', pos) end); + fun qualified_name "" = empty | qualified_name s = let val (qualifier, name) = split_last (Long_Name.explode s) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/General/name_space.ML Fri Feb 19 09:35:18 2010 +0100 @@ -43,6 +43,7 @@ val root_path: naming -> naming val parent_path: naming -> naming val mandatory_path: string -> naming -> naming + val qualified_path: bool -> binding -> naming -> naming val transform_binding: naming -> binding -> binding val full_name: naming -> binding -> string val external_names: naming -> string -> string list @@ -261,6 +262,9 @@ val parent_path = map_path (perhaps (try (#1 o split_last))); fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]); +fun qualified_path mandatory binding = map_path (fn path => + path @ #2 (Binding.dest (Binding.qualified mandatory "" binding))); + (* full name *) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/Isar/expression.ML Fri Feb 19 09:35:18 2010 +0100 @@ -681,7 +681,7 @@ |> def_pred abinding parms defs' exts exts'; val (_, thy'') = thy' - |> Sign.mandatory_path (Binding.name_of abinding) + |> Sign.qualified_path true abinding |> PureThy.note_thmss "" [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])] ||> Sign.restore_naming thy'; @@ -695,7 +695,7 @@ |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); val (_, thy'''') = thy''' - |> Sign.mandatory_path (Binding.name_of binding) + |> Sign.qualified_path true binding |> PureThy.note_thmss "" [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]), ((Binding.conceal (Binding.name axiomsN), []), diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Feb 19 09:35:18 2010 +0100 @@ -390,7 +390,7 @@ val _ = OuterSyntax.command "context" "enter local theory context" K.thy_decl (P.name --| P.begin >> (fn name => - Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context name))); + Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name))); (* locales *) diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Feb 19 09:35:18 2010 +0100 @@ -492,7 +492,7 @@ fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u)); in if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t - else Pattern.rewrite_term thy [] [match_abbrev] t + else Pattern.rewrite_term_top thy [] [match_abbrev] t end; diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/Isar/theory_target.ML Fri Feb 19 09:35:18 2010 +0100 @@ -7,12 +7,14 @@ signature THEORY_TARGET = sig - val peek: local_theory -> {target: string, is_locale: bool, - is_class: bool, instantiation: string list * (string * sort) list * sort, + val peek: local_theory -> + {target: string, + is_locale: bool, + is_class: bool, + instantiation: string list * (string * sort) list * sort, overloading: (string * (string * typ) * bool) list} val init: string option -> theory -> local_theory - val begin: string -> Proof.context -> local_theory - val context: xstring -> theory -> local_theory + val context_cmd: xstring -> theory -> local_theory val instantiation: string list * (string * sort) list * sort -> theory -> local_theory val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory val overloading: (string * (string * typ) * bool) list -> theory -> local_theory @@ -305,13 +307,13 @@ in ((lhs, (res_name, res)), lthy4) end; -(* init *) +(* init various targets *) local fun init_target _ NONE = global_target | init_target thy (SOME target) = - if Locale.defined thy (Locale.intern thy target) + if Locale.defined thy target then make_target target true (Class_Target.is_class thy target) ([], [], []) [] else error ("No such locale: " ^ quote target); @@ -349,17 +351,12 @@ in fun init target thy = init_lthy_ctxt (init_target thy target) thy; -fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt; -fun context "-" thy = init NONE thy - | context target thy = init (SOME (Locale.intern thy target)) thy; - - -(* other targets *) +fun context_cmd "-" thy = init NONE thy + | context_cmd target thy = init (SOME (Locale.intern thy target)) thy; fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []); -fun instantiation_cmd raw_arities thy = - instantiation (Class_Target.read_multi_arity thy raw_arities) thy; +fun instantiation_cmd arities thy = instantiation (Class_Target.read_multi_arity thy arities) thy; val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); val overloading_cmd = gen_overloading Syntax.read_term; diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Feb 19 09:35:18 2010 +0100 @@ -104,7 +104,7 @@ type generic_theory = Context.generic; (*theory or local_theory*) -val loc_init = Theory_Target.context; +val loc_init = Theory_Target.context_cmd; val loc_exit = Local_Theory.exit_global; fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/Syntax/syn_trans.ML Fri Feb 19 09:35:18 2010 +0100 @@ -510,7 +510,7 @@ ("_DDDOT", dddot_tr), ("_update_name", update_name_tr), ("_index", index_tr)], - [], + ([]: (string * (term list -> term)) list), [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), ("_pttrns", idtyp_ast_tr' "_pttrns"), diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/axclass.ML Fri Feb 19 09:35:18 2010 +0100 @@ -286,23 +286,25 @@ (* declaration and definition of instances of overloaded constants *) -fun inst_tyco_of thy (c, T) = case get_inst_tyco (Sign.consts_of thy) (c, T) - of SOME tyco => tyco - | NONE => error ("Illegal type for instantiation of class parameter: " - ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T)); +fun inst_tyco_of thy (c, T) = + (case get_inst_tyco (Sign.consts_of thy) (c, T) of + SOME tyco => tyco + | NONE => error ("Illegal type for instantiation of class parameter: " ^ + quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))); fun declare_overloaded (c, T) thy = let - val class = case class_of_param thy c - of SOME class => class - | NONE => error ("Not a class parameter: " ^ quote c); + val class = + (case class_of_param thy c of + SOME class => class + | NONE => error ("Not a class parameter: " ^ quote c)); val tyco = inst_tyco_of thy (c, T); val name_inst = instance_name (tyco, class) ^ "_inst"; val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco; val T' = Type.strip_sorts T; in thy - |> Sign.mandatory_path name_inst + |> Sign.qualified_path true (Binding.name name_inst) |> Sign.declare_const ((Binding.name c', T'), NoSyn) |-> (fn const' as Const (c'', _) => Thm.add_def false true @@ -311,8 +313,8 @@ #-> (fn thm => add_inst_param (c, tyco) (c'', thm) #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), []) #> snd - #> Sign.restore_naming thy #> pair (Const (c, T)))) + ||> Sign.restore_naming thy end; fun define_overloaded b (c, t) thy = @@ -482,7 +484,7 @@ val class_triv = Thm.class_triv def_thy class; val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = def_thy - |> Sign.mandatory_path (Binding.name_of bconst) + |> Sign.qualified_path true bconst |> PureThy.note_thmss "" [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]), ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]), @@ -497,7 +499,7 @@ val result_thy = facts_thy |> fold put_classrel (map (pair class) super ~~ classrel) - |> Sign.add_path (Binding.name_of bconst) + |> Sign.qualified_path false bconst |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd |> Sign.restore_naming facts_thy |> map_axclasses (fn (axclasses, parameters) => diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/display.ML --- a/src/Pure/display.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/display.ML Fri Feb 19 09:35:18 2010 +0100 @@ -125,7 +125,7 @@ fun pretty_full_theory verbose thy = let - val ctxt = ProofContext.init thy; + val ctxt = Syntax.init_pretty_global thy; fun prt_cls c = Syntax.pretty_sort ctxt [c]; fun prt_sort S = Syntax.pretty_sort ctxt S; diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/pattern.ML --- a/src/Pure/pattern.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/pattern.ML Fri Feb 19 09:35:18 2010 +0100 @@ -29,6 +29,7 @@ val pattern: term -> bool val match_rew: theory -> term -> term * term -> (term * term) option val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term + val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term exception Unif exception MATCH exception Pattern @@ -432,7 +433,7 @@ handle MATCH => NONE end; -fun rewrite_term thy rules procs tm = +fun gen_rewrite_term bot thy rules procs tm = let val skel0 = Bound 0; @@ -448,42 +449,53 @@ NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs) | x => x); - fun rew1 bounds (Var _) _ = NONE - | rew1 bounds skel tm = (case rew2 bounds skel tm of - SOME tm1 => (case rew tm1 of - SOME (tm2, skel') => SOME (the_default tm2 (rew1 bounds skel' tm2)) - | NONE => SOME tm1) - | NONE => (case rew tm of - SOME (tm1, skel') => SOME (the_default tm1 (rew1 bounds skel' tm1)) - | NONE => NONE)) - - and rew2 bounds skel (tm1 $ tm2) = (case tm1 of + fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of Abs (_, _, body) => let val tm' = subst_bound (tm2, body) - in SOME (the_default tm' (rew2 bounds skel0 tm')) end + in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end | _ => let val (skel1, skel2) = (case skel of skel1 $ skel2 => (skel1, skel2) | _ => (skel0, skel0)) - in case rew1 bounds skel1 tm1 of - SOME tm1' => (case rew1 bounds skel2 tm2 of + in case r bounds skel1 tm1 of + SOME tm1' => (case r bounds skel2 tm2 of SOME tm2' => SOME (tm1' $ tm2') | NONE => SOME (tm1' $ tm2)) - | NONE => (case rew1 bounds skel2 tm2 of + | NONE => (case r bounds skel2 tm2 of SOME tm2' => SOME (tm1 $ tm2') | NONE => NONE) end) - | rew2 bounds skel (Abs body) = + | rew_sub r bounds skel (Abs body) = let val (abs, tm') = variant_absfree bounds body; val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0) - in case rew1 (bounds + 1) skel' tm' of + in case r (bounds + 1) skel' tm' of SOME tm'' => SOME (abs tm'') | NONE => NONE end - | rew2 _ _ _ = NONE; + | rew_sub _ _ _ _ = NONE; + + fun rew_bot bounds (Var _) _ = NONE + | rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of + SOME tm1 => (case rew tm1 of + SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2)) + | NONE => SOME tm1) + | NONE => (case rew tm of + SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1)) + | NONE => NONE)); - in the_default tm (rew1 0 skel0 tm) end; + fun rew_top bounds _ tm = (case rew tm of + SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of + SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2)) + | NONE => SOME tm1) + | NONE => (case rew_sub rew_top bounds skel0 tm of + SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1)) + | NONE => NONE)); + + in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end; + +val rewrite_term = gen_rewrite_term true; +val rewrite_term_top = gen_rewrite_term false; end; diff -r 2bcdae5f4fdb -r 5cb63cb4213f src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Feb 18 18:48:07 2010 +0100 +++ b/src/Pure/sign.ML Fri Feb 19 09:35:18 2010 +0100 @@ -127,6 +127,7 @@ val root_path: theory -> theory val parent_path: theory -> theory val mandatory_path: string -> theory -> theory + val qualified_path: bool -> binding -> theory -> theory val local_path: theory -> theory val restore_naming: theory -> theory -> theory val hide_class: bool -> string -> theory -> theory @@ -614,6 +615,7 @@ val root_path = map_naming Name_Space.root_path; val parent_path = map_naming Name_Space.parent_path; val mandatory_path = map_naming o Name_Space.mandatory_path; +val qualified_path = map_naming oo Name_Space.qualified_path; fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);