--- a/src/HOL/Big_Operators.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Big_Operators.thy Tue Sep 13 17:07:33 2011 -0700
@@ -1394,7 +1394,7 @@
shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
using A proof (induct rule: finite_ne_induct)
case singleton thus ?case
- by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
+ by(simp add: inf_Sup1_distrib [OF B])
next
case (insert x A)
have finB: "finite {inf x b |b. b \<in> B}"
@@ -1608,11 +1608,7 @@
lemma Max_ge [simp]:
assumes "finite A" and "x \<in> A"
shows "x \<le> Max A"
-proof -
- interpret semilattice_inf max "op \<ge>" "op >"
- by (rule max_lattice)
- from assms show ?thesis by (simp add: Max_def fold1_belowI)
-qed
+ by (simp add: Max_def semilattice_inf.fold1_belowI [OF max_lattice] assms)
lemma Min_ge_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
@@ -1622,11 +1618,7 @@
lemma Max_le_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
-proof -
- interpret semilattice_inf max "op \<ge>" "op >"
- by (rule max_lattice)
- from assms show ?thesis by (simp add: Max_def below_fold1_iff)
-qed
+ by (simp add: Max_def semilattice_inf.below_fold1_iff [OF max_lattice] assms)
lemma Min_gr_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
@@ -1636,12 +1628,8 @@
lemma Max_less_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
-proof -
- interpret dual: linorder "op \<ge>" "op >"
- by (rule dual_linorder)
- from assms show ?thesis
- by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
-qed
+ by (simp add: Max_def linorder.dual_max [OF dual_linorder]
+ linorder.strict_below_fold1_iff [OF dual_linorder] assms)
lemma Min_le_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
@@ -1651,12 +1639,8 @@
lemma Max_ge_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
-proof -
- interpret dual: linorder "op \<ge>" "op >"
- by (rule dual_linorder)
- from assms show ?thesis
- by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
-qed
+ by (simp add: Max_def linorder.dual_max [OF dual_linorder]
+ linorder.fold1_below_iff [OF dual_linorder] assms)
lemma Min_less_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
@@ -1666,12 +1650,8 @@
lemma Max_gr_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
-proof -
- interpret dual: linorder "op \<ge>" "op >"
- by (rule dual_linorder)
- from assms show ?thesis
- by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max])
-qed
+ by (simp add: Max_def linorder.dual_max [OF dual_linorder]
+ linorder.fold1_strict_below_iff [OF dual_linorder] assms)
lemma Min_eqI:
assumes "finite A"
@@ -1705,12 +1685,8 @@
lemma Max_mono:
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Max M \<le> Max N"
-proof -
- interpret dual: linorder "op \<ge>" "op >"
- by (rule dual_linorder)
- from assms show ?thesis
- by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max])
-qed
+ by (simp add: Max_def linorder.dual_max [OF dual_linorder]
+ linorder.fold1_antimono [OF dual_linorder] assms)
lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
assumes fin: "finite A"
--- a/src/HOL/Complete_Lattices.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Complete_Lattices.thy Tue Sep 13 17:07:33 2011 -0700
@@ -84,23 +84,13 @@
lemma INF_foundation_dual [no_atp]:
"complete_lattice.SUPR Inf = INFI"
-proof (rule ext)+
- interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
- by (fact dual_complete_lattice)
- fix f :: "'b \<Rightarrow> 'a" and A
- show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
- by (simp only: dual.SUP_def INF_def)
-qed
+ by (simp add: fun_eq_iff INF_def
+ complete_lattice.SUP_def [OF dual_complete_lattice])
lemma SUP_foundation_dual [no_atp]:
"complete_lattice.INFI Sup = SUPR"
-proof (rule ext)+
- interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
- by (fact dual_complete_lattice)
- fix f :: "'b \<Rightarrow> 'a" and A
- show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
- by (simp only: dual.INF_def SUP_def)
-qed
+ by (simp add: fun_eq_iff SUP_def
+ complete_lattice.INF_def [OF dual_complete_lattice])
lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
by (auto simp add: INF_def intro: Inf_lower)
@@ -330,10 +320,10 @@
by (auto intro: antisym SUP_upper SUP_least)
lemma INF_top [simp]: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
- by (cases "A = {}") (simp_all add: INF_empty)
+ by (cases "A = {}") simp_all
lemma SUP_bot [simp]: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
- by (cases "A = {}") (simp_all add: SUP_empty)
+ by (cases "A = {}") simp_all
lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
by (iprover intro: INF_lower INF_greatest order_trans antisym)
@@ -359,11 +349,11 @@
lemma INF_constant:
"(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
- by (simp add: INF_empty)
+ by simp
lemma SUP_constant:
"(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
- by (simp add: SUP_empty)
+ by simp
lemma less_INF_D:
assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
@@ -385,11 +375,11 @@
lemma INF_UNIV_bool_expand:
"(\<Sqinter>b. A b) = A True \<sqinter> A False"
- by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
+ by (simp add: UNIV_bool INF_insert inf_commute)
lemma SUP_UNIV_bool_expand:
"(\<Squnion>b. A b) = A True \<squnion> A False"
- by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
+ by (simp add: UNIV_bool SUP_insert sup_commute)
end
--- a/src/HOL/Deriv.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Deriv.thy Tue Sep 13 17:07:33 2011 -0700
@@ -451,10 +451,11 @@
\<forall>n. f(n) \<le> g(n) |]
==> Bseq (f :: nat \<Rightarrow> real)"
apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
+apply (rule conjI)
apply (induct_tac "n")
apply (auto intro: order_trans)
-apply (rule_tac y = "g (Suc na)" in order_trans)
-apply (induct_tac [2] "na")
+apply (rule_tac y = "g n" in order_trans)
+apply (induct_tac [2] "n")
apply (auto intro: order_trans)
done
@@ -470,17 +471,7 @@
lemma f_inc_imp_le_lim:
fixes f :: "nat \<Rightarrow> real"
shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
-apply (rule linorder_not_less [THEN iffD1])
-apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
-apply (drule_tac x = "f n - lim f" in spec, clarsimp)
-apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
-apply (subgoal_tac "lim f \<le> f (no + n) ")
-apply (drule_tac no=no and m=n in lemma_f_mono_add)
-apply (auto simp add: add_commute)
-apply (induct_tac "no")
-apply simp
-apply (auto intro: order_trans simp add: diff_minus abs_if)
-done
+ by (rule incseq_le, simp add: incseq_SucI, simp add: convergent_LIMSEQ_iff)
lemma lim_uminus:
fixes g :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -492,10 +483,7 @@
lemma g_dec_imp_lim_le:
fixes g :: "nat \<Rightarrow> real"
shows "\<lbrakk>\<forall>n. g (Suc n) \<le> g(n); convergent g\<rbrakk> \<Longrightarrow> lim g \<le> g n"
-apply (subgoal_tac "- (g n) \<le> - (lim g) ")
-apply (cut_tac [2] f = "%x. - (g x)" in f_inc_imp_le_lim)
-apply (auto simp add: lim_uminus convergent_minus_iff [symmetric])
-done
+ by (rule decseq_le, simp add: decseq_SucI, simp add: convergent_LIMSEQ_iff)
lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
\<forall>n. g(Suc n) \<le> g(n);
@@ -938,7 +926,7 @@
lemma lemma_interval: "[| a < x; x < b |] ==>
\<exists>d::real. 0 < d & (\<forall>y. \<bar>x-y\<bar> < d --> a \<le> y & y \<le> b)"
apply (drule lemma_interval_lt, auto)
-apply (auto intro!: exI)
+apply force
done
text{*Rolle's Theorem.
--- a/src/HOL/Fields.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Fields.thy Tue Sep 13 17:07:33 2011 -0700
@@ -270,7 +270,11 @@
lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
by (simp add: divide_inverse mult_ac)
-text {* These are later declared as simp rules. *}
+text{*It's not obvious whether @{text times_divide_eq} should be
+ simprules or not. Their effect is to gather terms into one big
+ fraction, like a*b*c / x*y*z. The rationale for that is unclear, but
+ many proofs seem to need them.*}
+
lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
lemma add_frac_eq:
@@ -777,15 +781,15 @@
have the same sign*}
lemma divide_strict_left_mono:
"[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
+ by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
lemma divide_left_mono:
"[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
+ by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
lemma divide_strict_left_mono_neg:
"[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
+ by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)
lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
x / y <= z"
@@ -832,11 +836,6 @@
apply simp_all
done
-text{*It's not obvious whether these should be simprules or not.
- Their effect is to gather terms into one big fraction, like
- a*b*c / x*y*z. The rationale for that is unclear, but many proofs
- seem to need them.*}
-
lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
by (simp add: field_simps zero_less_two)
--- a/src/HOL/Fun.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Fun.thy Tue Sep 13 17:07:33 2011 -0700
@@ -610,7 +610,7 @@
by auto
lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
-by (auto intro: ext)
+ by auto
lemma UNION_fun_upd:
"UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
--- a/src/HOL/HOL.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/HOL.thy Tue Sep 13 17:07:33 2011 -0700
@@ -1635,7 +1635,7 @@
apply (rule iffI)
apply (rule_tac a = "%x. THE y. P x y" in ex1I)
apply (fast dest!: theI')
- apply (fast intro: ext the1_equality [symmetric])
+ apply (fast intro: the1_equality [symmetric])
apply (erule ex1E)
apply (rule allI)
apply (rule ex1I)
--- a/src/HOL/Hilbert_Choice.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Hilbert_Choice.thy Tue Sep 13 17:07:33 2011 -0700
@@ -123,7 +123,7 @@
by (simp add:inv_into_f_eq)
lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
-by (blast intro: ext inv_into_f_eq)
+ by (blast intro: inv_into_f_eq)
text{*But is it useful?*}
lemma inj_transfer:
@@ -286,7 +286,7 @@
hence "?f'' a = a'"
using `a \<in> A` 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
moreover have "f a = a'" using assms 2 3
- by (auto simp add: inv_into_f_f bij_betw_def)
+ by (auto simp add: bij_betw_def)
ultimately show "?f'' a = f a" by simp
qed
--- a/src/HOL/Lattices.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Lattices.thy Tue Sep 13 17:07:33 2011 -0700
@@ -180,8 +180,8 @@
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
by (fact inf.left_commute)
-lemma inf_idem [simp]: "x \<sqinter> x = x"
- by (fact inf.idem)
+lemma inf_idem: "x \<sqinter> x = x"
+ by (fact inf.idem) (* already simp *)
lemma inf_left_idem [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
by (fact inf.left_idem)
@@ -219,8 +219,8 @@
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
by (fact sup.left_commute)
-lemma sup_idem [simp]: "x \<squnion> x = x"
- by (fact sup.idem)
+lemma sup_idem: "x \<squnion> x = x"
+ by (fact sup.idem) (* already simp *)
lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
by (fact sup.left_idem)
@@ -311,23 +311,13 @@
lemma less_supI1:
"x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
-proof -
- interpret dual: semilattice_inf sup "op \<ge>" "op >"
- by (fact dual_semilattice)
- assume "x \<sqsubset> a"
- then show "x \<sqsubset> a \<squnion> b"
- by (fact dual.less_infI1)
-qed
+ using dual_semilattice
+ by (rule semilattice_inf.less_infI1)
lemma less_supI2:
"x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
-proof -
- interpret dual: semilattice_inf sup "op \<ge>" "op >"
- by (fact dual_semilattice)
- assume "x \<sqsubset> b"
- then show "x \<sqsubset> a \<squnion> b"
- by (fact dual.less_infI2)
-qed
+ using dual_semilattice
+ by (rule semilattice_inf.less_infI2)
end
@@ -341,16 +331,16 @@
begin
lemma sup_inf_distrib2:
- "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
-by(simp add: inf_sup_aci sup_inf_distrib1)
+ "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
+ by (simp add: sup_commute sup_inf_distrib1)
lemma inf_sup_distrib1:
- "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
-by(rule distrib_imp2[OF sup_inf_distrib1])
+ "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
+ by (rule distrib_imp2 [OF sup_inf_distrib1])
lemma inf_sup_distrib2:
- "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
-by(simp add: inf_sup_aci inf_sup_distrib1)
+ "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
+ by (simp add: inf_commute inf_sup_distrib1)
lemma dual_distrib_lattice:
"class.distrib_lattice sup (op \<ge>) (op >) inf"
@@ -510,11 +500,8 @@
lemma compl_sup [simp]:
"- (x \<squnion> y) = - x \<sqinter> - y"
-proof -
- interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus sup greater_eq greater inf \<top> \<bottom>
- by (rule dual_boolean_algebra)
- then show ?thesis by simp
-qed
+ using dual_boolean_algebra
+ by (rule boolean_algebra.compl_inf)
lemma compl_mono:
"x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
--- a/src/HOL/List.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/List.thy Tue Sep 13 17:07:33 2011 -0700
@@ -1176,7 +1176,7 @@
have "length (filter p (x # xs)) = Suc(card ?S)"
using Cons `p x` by simp
also have "\<dots> = Suc(card(Suc ` ?S))" using fin
- by (simp add: card_image inj_Suc)
+ by (simp add: card_image)
also have "\<dots> = card ?S'" using eq fin
by (simp add:card_insert_if) (simp add:image_def)
finally show ?thesis .
@@ -1187,7 +1187,7 @@
have "length (filter p (x # xs)) = card ?S"
using Cons `\<not> p x` by simp
also have "\<dots> = card(Suc ` ?S)" using fin
- by (simp add: card_image inj_Suc)
+ by (simp add: card_image)
also have "\<dots> = card ?S'" using eq fin
by (simp add:card_insert_if)
finally show ?thesis .
@@ -1529,10 +1529,10 @@
by (induct xs) auto
lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
-by(simp add:last.simps)
+ by simp
lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
-by(simp add:last.simps)
+ by simp
lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
by (induct xs) (auto)
@@ -2627,7 +2627,7 @@
lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
apply (induct n m arbitrary: i rule: diff_induct)
prefer 3 apply (subst map_Suc_upt[symmetric])
-apply (auto simp add: less_diff_conv nth_upt)
+apply (auto simp add: less_diff_conv)
done
lemma nth_take_lemma:
@@ -2647,9 +2647,7 @@
lemma nth_equalityI:
"[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
-apply (frule nth_take_lemma [OF le_refl eq_imp_le])
-apply (simp_all add: take_all)
-done
+ by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
lemma map_nth:
"map (\<lambda>i. xs ! i) [0..<length xs] = xs"
@@ -2666,7 +2664,7 @@
lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
-- {* The famous take-lemma. *}
apply (drule_tac x = "max (length xs) (length ys)" in spec)
-apply (simp add: le_max_iff_disj take_all)
+apply (simp add: le_max_iff_disj)
done
@@ -2880,8 +2878,8 @@
done
lemma length_remdups_concat:
- "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
-by(simp add: set_concat distinct_card[symmetric])
+ "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
+ by (simp add: distinct_card [symmetric])
lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
proof -
@@ -3519,7 +3517,7 @@
"sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
apply (unfold sublist_def)
apply (induct l' rule: rev_induct, simp)
-apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
+apply (simp add: upt_add_eq_append[of 0] sublist_shift_lemma)
apply (simp add: add_commute)
done
@@ -3838,7 +3836,7 @@
by(induct xs)(auto simp:set_insort)
lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
-by(induct xs)(simp_all add:distinct_insort set_sort)
+ by (induct xs) (simp_all add: distinct_insort)
lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
by (induct xs) (auto simp:sorted_Cons set_insort)
--- a/src/HOL/Map.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Map.thy Tue Sep 13 17:07:33 2011 -0700
@@ -265,7 +265,7 @@
lemma map_comp_empty [simp]:
"m \<circ>\<^sub>m empty = empty"
"empty \<circ>\<^sub>m m = empty"
-by (auto simp add: map_comp_def intro: ext split: option.splits)
+by (auto simp add: map_comp_def split: option.splits)
lemma map_comp_simps [simp]:
"m2 k = None \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = None"
@@ -354,7 +354,7 @@
by (simp add: restrict_map_def)
lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
-by (auto simp add: restrict_map_def intro: ext)
+by (auto simp add: restrict_map_def)
lemma restrict_map_empty [simp]: "empty|`D = empty"
by (simp add: restrict_map_def)
@@ -485,7 +485,7 @@
subsection {* @{term [source] dom} *}
lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
-by(auto intro!:ext simp: dom_def)
+ by (auto simp: dom_def)
lemma domI: "m a = Some b ==> a : dom m"
by(simp add:dom_def)
--- a/src/HOL/Orderings.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Orderings.thy Tue Sep 13 17:07:33 2011 -0700
@@ -1309,10 +1309,10 @@
instance "fun" :: (type, preorder) preorder proof
qed (auto simp add: le_fun_def less_fun_def
- intro: order_trans antisym intro!: ext)
+ intro: order_trans antisym)
instance "fun" :: (type, order) order proof
-qed (auto simp add: le_fun_def intro: antisym ext)
+qed (auto simp add: le_fun_def intro: antisym)
instantiation "fun" :: (type, bot) bot
begin
--- a/src/HOL/Product_Type.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Product_Type.thy Tue Sep 13 17:07:33 2011 -0700
@@ -830,10 +830,10 @@
by (simp add: scomp_unfold prod_case_unfold)
lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
- by (simp add: fun_eq_iff scomp_apply)
+ by (simp add: fun_eq_iff)
lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
- by (simp add: fun_eq_iff scomp_apply)
+ by (simp add: fun_eq_iff)
lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
by (simp add: fun_eq_iff scomp_unfold)
@@ -842,7 +842,7 @@
by (simp add: fun_eq_iff scomp_unfold fcomp_def)
lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
- by (simp add: fun_eq_iff scomp_unfold fcomp_apply)
+ by (simp add: fun_eq_iff scomp_unfold)
code_const scomp
(Eval infixl 3 "#->")
@@ -863,7 +863,7 @@
by (simp add: map_pair_def)
enriched_type map_pair: map_pair
- by (auto simp add: split_paired_all intro: ext)
+ by (auto simp add: split_paired_all)
lemma fst_map_pair [simp]:
"fst (map_pair f g x) = f (fst x)"
@@ -1110,10 +1110,10 @@
by auto
lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
- by (auto intro!: image_eqI)
+ by force
lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
- by (auto intro!: image_eqI)
+ by force
lemma insert_times_insert[simp]:
"insert a A \<times> insert b B =
--- a/src/HOL/Quotient.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Quotient.thy Tue Sep 13 17:07:33 2011 -0700
@@ -85,7 +85,7 @@
shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
unfolding set_rel_def
using equivp_reflp[OF e]
- by auto (metis equivp_symp[OF e])+
+ by auto (metis, metis equivp_symp[OF e])
subsection {* Quotient Predicate *}
@@ -269,12 +269,12 @@
lemma ball_reg_right:
assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
shows "All P \<longrightarrow> Ball R Q"
- using a by (metis Collect_mem_eq)
+ using a by fast
lemma bex_reg_left:
assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
shows "Bex R Q \<longrightarrow> Ex P"
- using a by (metis Collect_mem_eq)
+ using a by fast
lemma ball_reg_left:
assumes a: "equivp R"
@@ -317,25 +317,25 @@
assumes a: "!x :: 'a. (P x --> Q x)"
and b: "All P"
shows "All Q"
- using a b by (metis)
+ using a b by fast
lemma ex_reg:
assumes a: "!x :: 'a. (P x --> Q x)"
and b: "Ex P"
shows "Ex Q"
- using a b by metis
+ using a b by fast
lemma ball_reg:
assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
and b: "Ball R P"
shows "Ball R Q"
- using a b by (metis Collect_mem_eq)
+ using a b by fast
lemma bex_reg:
assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
and b: "Bex R P"
shows "Bex R Q"
- using a b by (metis Collect_mem_eq)
+ using a b by fast
lemma ball_all_comm:
@@ -569,7 +569,7 @@
lemma o_rsp:
"((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
"(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
- by (auto intro!: fun_relI elim: fun_relE)
+ by (force elim: fun_relE)+
lemma cond_prs:
assumes a: "Quotient R absf repf"
@@ -585,7 +585,7 @@
lemma if_rsp:
assumes q: "Quotient R Abs Rep"
shows "(op = ===> R ===> R ===> R) If If"
- by (auto intro!: fun_relI)
+ by force
lemma let_prs:
assumes q1: "Quotient R1 Abs1 Rep1"
@@ -596,11 +596,11 @@
lemma let_rsp:
shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
- by (auto intro!: fun_relI elim: fun_relE)
+ by (force elim: fun_relE)
lemma id_rsp:
shows "(R ===> R) id id"
- by (auto intro: fun_relI)
+ by auto
lemma id_prs:
assumes a: "Quotient R Abs Rep"
--- a/src/HOL/Random.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Random.thy Tue Sep 13 17:07:33 2011 -0700
@@ -57,7 +57,7 @@
lemma range:
"k > 0 \<Longrightarrow> fst (range k s) < k"
- by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
+ by (simp add: range_def split_def del: log.simps iterate.simps)
definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
"select xs = range (Code_Numeral.of_nat (length xs))
@@ -73,7 +73,7 @@
then have
"Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
then show ?thesis
- by (simp add: scomp_apply split_beta select_def)
+ by (simp add: split_beta select_def)
qed
primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
@@ -188,4 +188,3 @@
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
end
-
--- a/src/HOL/Relation.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Relation.thy Tue Sep 13 17:07:33 2011 -0700
@@ -420,7 +420,7 @@
by blast
lemma fst_eq_Domain: "fst ` R = Domain R"
-by (auto intro!:image_eqI)
+ by force
lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
by auto
@@ -471,7 +471,7 @@
by blast
lemma snd_eq_Range: "snd ` R = Range R"
-by (auto intro!:image_eqI)
+ by force
subsection {* Field *}
--- a/src/HOL/Rings.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Rings.thy Tue Sep 13 17:07:33 2011 -0700
@@ -1100,7 +1100,7 @@
lemma abs_one [simp]:
"\<bar>1\<bar> = 1"
- by (simp add: abs_if zero_less_one [THEN less_not_sym])
+ by (simp add: abs_if)
end
--- a/src/HOL/Transitive_Closure.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Transitive_Closure.thy Tue Sep 13 17:07:33 2011 -0700
@@ -220,7 +220,7 @@
apply (rename_tac a b)
apply (case_tac "a = b")
apply blast
- apply (blast intro!: r_into_rtrancl)
+ apply blast
done
lemma rtranclp_r_diff_Id: "(inf r op ~=)^** = r^**"
--- a/src/HOL/Wellfounded.thy Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Wellfounded.thy Tue Sep 13 17:07:33 2011 -0700
@@ -190,7 +190,7 @@
"wfP (\<lambda>x y. False)"
proof -
have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
- then show ?thesis by (simp add: bot_fun_def bot_bool_def)
+ then show ?thesis by (simp add: bot_fun_def)
qed
lemma wf_Int1: "wf r ==> wf (r Int r')"
@@ -573,7 +573,7 @@
theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
apply (rule wfPUNIVI)
- apply (induct_tac P x rule: accp_induct)
+ apply (rule_tac P=P in accp_induct)
apply blast
apply blast
done