--- 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
--- 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 \<noteq> 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 \<noteq> 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 \<noteq> 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) \<noteq> 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 ***)
--- 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 "(\<lambda>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 "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
proof -
- have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by (simp add: differentiable_const)
- with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by (simp add: differentiable_mult)
+ have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by simp
+ with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by simp
moreover
- have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by (simp add: differentiable_const)
- with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by (simp add: differentiable_mult)
- ultimately show ?thesis by (simp add: differentiable_diff)
+ have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by simp
+ with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by simp
+ ultimately show ?thesis by simp
qed
ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
--- 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\<Colon>nat) mod 2 \<longleftrightarrow> 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
--- 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
--- 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\<noteq>0"
thus ?thesis by (simp add: nonzero_inverse_minus_eq)
@@ -283,13 +283,13 @@
lemma mult_divide_mult_cancel_left:
"c\<noteq>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\<noteq>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 \<le> inverse x) = (0 < x & x \<le> (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 \<le> 0 | 1 < (x::'a::{linordered_field,division_by_zero}))"
--- 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 \<Longrightarrow> finite{B. B \<subseteq> A}"
@@ -634,7 +634,7 @@
from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
let ?hm = "Fun.swap k m h"
have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn
- by (simp add: inj_on_swap_iff inj_on)
+ by (simp add: inj_on)
show ?thesis
proof (intro exI conjI)
show "inj_on ?hm {i. i < m}" using inj_hm
@@ -764,7 +764,7 @@
lemma fold_insert2:
"finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> 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 \<in> 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 \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> 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" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F"
- and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
- from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
+ and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
+ from fTF have fUF: "finite (\<Union>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 (\<lambda>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 @@
(\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
k * card(C) = card (\<Union> 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 _ "\<Union> (insert x F)"])
done
@@ -2285,7 +2285,7 @@
lemma setprod_constant: "finite A ==> (\<Prod>x\<in> 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' \<noteq> {}"
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 \<noteq> 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 \<Longrightarrow> g {a} = a"
-by(simp add:fold1_singleton)
+by simp
lemma (in ab_semigroup_mult) fold1_insert_def:
"\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
--- 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 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> 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 \<noteq> 0" using nz by (simp add: gcd_zero_nat)
+ have "?g \<noteq> 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 \<noteq> 0"
- hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
+ hence zn: "?g ^ n \<noteq> 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 \<noteq> 0"
- hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
+ hence zn: "?g ^ n \<noteq> 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 \<or> (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 \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
\<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> 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
--- 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: "\<not> 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 \<noteq> z"
hence ynz': "y - z \<noteq> 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 \<noteq> z"
hence "y < z \<or> 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 "\<exists>k. y = z + k \<and> 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 \<or> y = z)" by auto
qed
--- 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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"
--- 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) = (\<exists>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)
--- 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 \<longleftrightarrow> 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 \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
proof
assume n1: "\<bar>n\<bar> = 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 "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
--- 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 \<circ> 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
--- 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 *}
--- 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 \<le> 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}*}
--- 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
--- 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 \<le> Fract ?k 1 * (Fract c d)"
proof -
have "?thesis = ((a * d * b * d) \<le> 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)) \<le> 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
--- 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) \<le> (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 \<le> a^n) = (0 \<le> (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
--- 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 \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
--- 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 \<noteq> 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 \<le> 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
--- 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 \<noteq> 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]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
- 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)"
--- 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 \<le> real (n::nat))"
+(* FIXME: duplicates real_of_nat_ge_zero *)
+lemma real_of_nat_ge_zero_cancel_iff: "(0 \<le> 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]
--- 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 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> 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 *)
--- 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]
--- 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 \<Longrightarrow> x dvd z \<Longrightarrow> 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 \<longleftrightarrow> c = 0 \<or> 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 \<longleftrightarrow> c = 0 \<or> 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 \<or> 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 \<or> a = - b"
then show "a * a = b * b" by auto
@@ -764,13 +764,13 @@
lemma mult_left_mono_neg:
"b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> 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 \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> 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 \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
@@ -791,11 +791,10 @@
proof
fix a b
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
- 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 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 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 \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> 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 \<le> a * a"
@@ -1056,11 +1055,11 @@
lemma sgn_1_pos:
"sgn a = 1 \<longleftrightarrow> a > 0"
-unfolding sgn_if by (simp add: neg_equal_zero)
+unfolding sgn_if by simp
lemma sgn_1_neg:
"sgn a = - 1 \<longleftrightarrow> a < 0"
-unfolding sgn_if by (auto simp add: equal_neg_zero)
+unfolding sgn_if by auto
lemma sgn_pos [simp]:
"0 < a \<Longrightarrow> 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 ==>
--- 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
--- 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)..<u}"
@@ -1006,7 +1006,7 @@
shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
proof-
have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)
- also have "\<dots> = ?r" by(simp add: setsum_constant mult_commute)
+ also have "\<dots> = ?r" by(simp add: mult_commute)
finally show ?thesis by auto
qed
@@ -1046,7 +1046,7 @@
lemma geometric_sum:
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
(x ^ n - 1) / (x - 1::'a::{field})"
-by (induct "n") (simp_all add:field_simps power_Suc)
+by (induct "n") (simp_all add: field_simps)
subsection {* The formula for arithmetic sums *}
@@ -1098,7 +1098,7 @@
of_nat(n) * (a + (a + of_nat(n - 1)*d))"
by (rule arith_series_general)
thus ?thesis
- unfolding One_nat_def by (auto simp add: of_nat_id)
+ unfolding One_nat_def by auto
qed
lemma arith_series_int:
--- a/src/HOL/SupInf.thy Thu Feb 18 18:48:07 2010 +0100
+++ b/src/HOL/SupInf.thy Fri Feb 19 09:35:18 2010 +0100
@@ -249,7 +249,7 @@
and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
shows "z \<le> Inf X"
proof -
- have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
+ have "Sup (uminus ` X) \<le> -z" using x z by force
hence "z \<le> - 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. \<forall>x. a \<le> x & x < d --> P x}"], auto)
show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
by (rule SupInf.Sup_upper [where z=b], auto)
- (metis prems real_le_linear real_less_def)
+ (metis `a < b` `\<not> P b` real_le_linear real_less_def)
next
show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
apply (rule SupInf.Sup_least)
--- 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;
--- 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) \<le> r * norm (S n)"
by (simp add: pos_divide_le_eq mult_ac)
thus "norm (S (Suc n)) \<le> 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)) \<le> 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) = (\<Sum>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 \<in> {- 1<..<1}" hence "norm (-x) < 1" by auto
show "summable (\<lambda>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 (\<lambda>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: "\<bar>x / sqrt (x\<twosuperior> + y\<twosuperior>)\<bar> \<le> 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: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
--- 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]
--- 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<y)"
by (simp add: less_than_def less_eq)
--- a/src/HOLCF/FOCUS/Fstream.thy Thu Feb 18 18:48:07 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy Fri Feb 19 09:35:18 2010 +0100
@@ -207,7 +207,7 @@
lemma fsfilter_fscons:
"A(C)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"
--- 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)
--- 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)
--- 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)
--- 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]
--- 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]
--- 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"
--- 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"
--- 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)
--- 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)"
--- 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
--- 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<<x ==> 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"
--- 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") *}
--- 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
--- 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,
--- 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 };
--- 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 = \<bottom>)"
-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 = \<bottom>)"
by (rule stream.casedist [of x], auto)
--- 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)
--- 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 *)
--- 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), []),
--- 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 *)
--- 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;
--- 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;
--- 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
--- 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"),
--- 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) =>
--- 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;
--- 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;
--- 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);