--- a/src/HOL/Algebra/Group.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Algebra/Group.thy Wed Dec 28 22:08:44 2011 +0100
@@ -771,42 +771,36 @@
proof (rule partial_order.complete_lattice_criterion1)
show "partial_order ?L" by (rule subgroups_partial_order)
next
- show "\<exists>G. greatest ?L G (carrier ?L)"
- proof
- show "greatest ?L (carrier G) (carrier ?L)"
- by (unfold greatest_def)
- (simp add: subgroup.subset subgroup_self)
- qed
+ have "greatest ?L (carrier G) (carrier ?L)"
+ by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
+ then show "\<exists>G. greatest ?L G (carrier ?L)" ..
next
fix A
assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
then have Int_subgroup: "subgroup (\<Inter>A) G"
by (fastforce intro: subgroups_Inter)
- show "\<exists>I. greatest ?L I (Lower ?L A)"
- proof
- show "greatest ?L (\<Inter>A) (Lower ?L A)"
- (is "greatest _ ?Int _")
- proof (rule greatest_LowerI)
- fix H
- assume H: "H \<in> A"
- with L have subgroupH: "subgroup H G" by auto
- from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
- by (rule subgroup_imp_group)
- from groupH have monoidH: "monoid ?H"
- by (rule group.is_monoid)
- from H have Int_subset: "?Int \<subseteq> H" by fastforce
- then show "le ?L ?Int H" by simp
- next
- fix H
- assume H: "H \<in> Lower ?L A"
- with L Int_subgroup show "le ?L H ?Int"
- by (fastforce simp: Lower_def intro: Inter_greatest)
- next
- show "A \<subseteq> carrier ?L" by (rule L)
- next
- show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
- qed
+ have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _")
+ proof (rule greatest_LowerI)
+ fix H
+ assume H: "H \<in> A"
+ with L have subgroupH: "subgroup H G" by auto
+ from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
+ by (rule subgroup_imp_group)
+ from groupH have monoidH: "monoid ?H"
+ by (rule group.is_monoid)
+ from H have Int_subset: "?Int \<subseteq> H" by fastforce
+ then show "le ?L ?Int H" by simp
+ next
+ fix H
+ assume H: "H \<in> Lower ?L A"
+ with L Int_subgroup show "le ?L H ?Int"
+ by (fastforce simp: Lower_def intro: Inter_greatest)
+ next
+ show "A \<subseteq> carrier ?L" by (rule L)
+ next
+ show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
qed
+ then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
qed
end
--- a/src/HOL/Algebra/Lattice.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Algebra/Lattice.thy Wed Dec 28 22:08:44 2011 +0100
@@ -1285,22 +1285,18 @@
by default auto
next
fix B
- assume B: "B \<subseteq> carrier ?L"
- show "EX s. least ?L s (Upper ?L B)"
- proof
- from B show "least ?L (\<Union> B) (Upper ?L B)"
- by (fastforce intro!: least_UpperI simp: Upper_def)
- qed
+ assume "B \<subseteq> carrier ?L"
+ then have "least ?L (\<Union> B) (Upper ?L B)"
+ by (fastforce intro!: least_UpperI simp: Upper_def)
+ then show "EX s. least ?L s (Upper ?L B)" ..
next
fix B
- assume B: "B \<subseteq> carrier ?L"
- show "EX i. greatest ?L i (Lower ?L B)"
- proof
- from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
- txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
- @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
- by (fastforce intro!: greatest_LowerI simp: Lower_def)
- qed
+ assume "B \<subseteq> carrier ?L"
+ then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
+ txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
+ @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
+ by (fastforce intro!: greatest_LowerI simp: Lower_def)
+ then show "EX i. greatest ?L i (Lower ?L B)" ..
qed
text {* An other example, that of the lattice of subgroups of a group,
--- a/src/HOL/Auth/Guard/Analz.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Auth/Guard/Analz.thy Wed Dec 28 22:08:44 2011 +0100
@@ -236,9 +236,10 @@
lemma kparts_insert_synth: "[| Y:parts (insert X G); X:synth (analz G);
Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Y:parts G"
-apply (drule parts_insert_substD [where P="%S. Y : S"], clarify)
+apply (drule parts_insert_substD, clarify)
apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
-by (auto dest: Nonce_kparts_synth)
+apply (auto dest: Nonce_kparts_synth)
+done
lemma Crypt_insert_synth:
"[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |]
--- a/src/HOL/Auth/Guard/Extensions.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Wed Dec 28 22:08:44 2011 +0100
@@ -198,7 +198,7 @@
lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==>
X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H"
-by (erule parts.induct, (fastforce dest: parts.Fst parts.Snd parts.Body)+)
+by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body)
lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}"
by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body)
@@ -207,10 +207,11 @@
lemma Crypt_synth_insert: "[| Crypt K X:parts (insert Y H);
Y:synth (analz H); Key K ~:analz H |] ==> Crypt K X:parts H"
-apply (drule parts_insert_substD [where P="%S. Crypt K X : S"], clarify)
+apply (drule parts_insert_substD, clarify)
apply (frule in_sub)
apply (frule parts_mono)
-by auto
+apply auto
+done
subsubsection{*greatest nonce used in a message*}
--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy Wed Dec 28 22:08:44 2011 +0100
@@ -60,7 +60,7 @@
assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. enat k < #((Y j)::'a::flat stream)|]
==> P(LUB i. Y i))"
shows "P(LUB i. Y i)"
-apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2])
+apply (rule increasing_chain_adm_lemma [OF 1 2])
apply (erule 3, assumption)
apply (erule thin_rl)
apply (rule allI)
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Dec 28 22:08:44 2011 +0100
@@ -149,8 +149,7 @@
text {* Strong Soundness for Component Programs:*}
-lemma ann_hoare_case_analysis [rule_format]:
- defines I: "I \<equiv> \<lambda>C q'.
+lemma ann_hoare_case_analysis [rule_format]: "\<turnstile> C q' \<longrightarrow>
((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and>
(\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and>
(\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and>
@@ -160,9 +159,8 @@
(\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow>
(\<exists>q. q \<subseteq> q' \<and> r \<subseteq> i \<and> i \<inter> b \<subseteq> pre c \<and> \<turnstile> c i \<and> i \<inter> -b \<subseteq> q)) \<and>
(\<forall>r b c. C = AnnAwait r b c \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<parallel>- (r \<inter> b) c q)))"
- shows "\<turnstile> C q' \<longrightarrow> I C q'"
apply(rule ann_hoare_induct)
-apply (simp_all add: I)
+apply simp_all
apply(rule_tac x=q in exI,simp)+
apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+
apply(clarify,simp,clarify,rule_tac x=qa in exI,fast)
--- a/src/HOL/Inductive.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Inductive.thy Wed Dec 28 22:08:44 2011 +0100
@@ -108,7 +108,7 @@
and P_f: "!!S. P S ==> P(f S)"
and P_Union: "!!M. !S:M. P S ==> P(Union M)"
shows "P(lfp f)"
- using assms by (rule lfp_ordinal_induct [where P=P])
+ using assms by (rule lfp_ordinal_induct)
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
@@ -210,7 +210,7 @@
apply (rule Un_least [THEN Un_least])
apply (rule subset_refl, assumption)
apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
-apply (rule monoD [where f=f], assumption)
+apply (rule monoD, assumption)
apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
done
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Dec 28 22:08:44 2011 +0100
@@ -128,7 +128,7 @@
let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
have "?B (Suc n) = ?a Un ?B n"
by (auto simp add: Sigma_Suc Un_assoc)
- moreover have "... : ?T"
+ also have "... : ?T"
proof (rule tiling.Un)
have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
by (rule domino.horiz)
@@ -137,7 +137,7 @@
show "?B n : ?T" by (rule Suc)
show "?a <= - ?B n" by blast
qed
- ultimately show ?case by simp
+ finally show ?case .
qed
lemma dominoes_tile_matrix:
@@ -150,13 +150,13 @@
case (Suc m)
let ?t = "{m} <*> below (2 * n)"
have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
- moreover have "... : ?T"
+ also have "... : ?T"
proof (rule tiling_Un)
show "?t : ?T" by (rule dominoes_tile_row)
show "?B m : ?T" by (rule Suc)
show "?t Int ?B m = {}" by blast
qed
- ultimately show ?case by simp
+ finally show ?case .
qed
lemma domino_singleton:
@@ -219,8 +219,8 @@
have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
then show ?thesis by (blast intro: that)
qed
- moreover have "... Un ?e t b = insert (i, j) (?e t b)" by simp
- moreover have "card ... = Suc (card (?e t b))"
+ also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
+ also have "card ... = Suc (card (?e t b))"
proof (rule card_insert_disjoint)
from `t \<in> tiling domino` have "finite t"
by (rule tiling_domino_finite)
@@ -229,7 +229,7 @@
from e have "(i, j) : ?e a b" by simp
with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
qed
- ultimately show "?thesis b" by simp
+ finally show "?thesis b" .
qed
then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
also from hyp have "card (?e t 0) = card (?e t 1)" .
--- a/src/HOL/Library/Zorn.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Library/Zorn.thy Wed Dec 28 22:08:44 2011 +0100
@@ -58,19 +58,18 @@
lemma Abrial_axiom1: "x \<subseteq> succ S x"
apply (auto simp add: succ_def super_def maxchain_def)
apply (rule contrapos_np, assumption)
- apply (rule_tac Q="\<lambda>S. xa \<in> S" in someI2, blast+)
+ apply (rule someI2)
+ apply blast+
done
lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
lemma TFin_induct:
- assumes H: "n \<in> TFin S"
- and I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
- "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P(Union Y)"
- shows "P n" using H
- apply (induct rule: TFin.induct [where P=P])
- apply (blast intro: I)+
- done
+ assumes H: "n \<in> TFin S" and
+ I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
+ "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P (Union Y)"
+ shows "P n"
+ using H by induct (blast intro: I)+
lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
apply (erule subset_trans)
@@ -160,7 +159,8 @@
lemma select_super:
"c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
apply (erule mem_super_Ex [THEN exE])
- apply (rule someI2 [where Q="%X. X : super S c"], auto)
+ apply (rule someI2)
+ apply auto
done
lemma select_not_equals:
@@ -185,8 +185,8 @@
apply (unfold chain_def chain_subset_def)
apply (rule CollectI, safe)
apply (drule bspec, assumption)
- apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
- best+)
+ apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE])
+ apply blast+
done
theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
--- a/src/HOL/NSA/Filter.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/NSA/Filter.thy Wed Dec 28 22:08:44 2011 +0100
@@ -391,12 +391,10 @@
fix A assume "A \<in> U"
with U show "infinite A" by (rule mem_superfrechet_all_infinite)
qed
- show ?thesis
- proof
- from fil ultra free show "freeultrafilter U"
- by (rule freeultrafilter.intro [OF ultrafilter.intro])
- (* FIXME: unfold_locales should use chained facts *)
- qed
+ from fil ultra free have "freeultrafilter U"
+ by (rule freeultrafilter.intro [OF ultrafilter.intro])
+ (* FIXME: unfold_locales should use chained facts *)
+ then show ?thesis ..
qed
lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
--- a/src/HOL/NSA/StarDef.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/NSA/StarDef.thy Wed Dec 28 22:08:44 2011 +0100
@@ -17,7 +17,7 @@
lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
apply (unfold FreeUltrafilterNat_def)
-apply (rule someI_ex [where P=freeultrafilter])
+apply (rule someI_ex)
apply (rule freeultrafilter_Ex)
apply (rule nat_infinite)
done
--- a/src/HOL/Nominal/Examples/Class2.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy Wed Dec 28 22:08:44 2011 +0100
@@ -3245,7 +3245,7 @@
{ case 1 show ?case
apply -
apply(simp add: lfp_eqvt)
- apply(simp add: perm_fun_def [where 'a="ntrm set"])
+ apply(simp add: perm_fun_def)
apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
apply(perm_simp)
done
@@ -3256,7 +3256,7 @@
apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
apply(simp add: lfp_eqvt)
apply(simp add: comp_def)
- apply(simp add: perm_fun_def [where 'a="ntrm set"])
+ apply(simp add: perm_fun_def)
apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
apply(perm_simp)
done
@@ -3269,7 +3269,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def [where 'a="ntrm set"])
+ apply(simp only: perm_fun_def)
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)
apply(perm_simp add: ih1 ih2)
@@ -3289,7 +3289,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def [where 'a="ntrm set"])
+ apply(simp only: perm_fun_def)
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name
ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name)
@@ -3311,7 +3311,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def [where 'a="ntrm set"])
+ apply(simp only: perm_fun_def)
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name
ORRIGHT2_eqvt_name ORLEFT_eqvt_name)
@@ -3333,7 +3333,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def [where 'a="ntrm set"])
+ apply(simp only: perm_fun_def)
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)
apply(perm_simp add: ih1 ih2 ih3 ih4)
@@ -3355,7 +3355,7 @@
{ case 1 show ?case
apply -
apply(simp add: lfp_eqvt)
- apply(simp add: perm_fun_def [where 'a="ntrm set"])
+ apply(simp add: perm_fun_def)
apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
apply(perm_simp)
done
@@ -3366,7 +3366,7 @@
apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
apply(simp add: lfp_eqvt)
apply(simp add: comp_def)
- apply(simp add: perm_fun_def [where 'a="ntrm set"])
+ apply(simp add: perm_fun_def)
apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
apply(perm_simp)
done
@@ -3379,7 +3379,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def [where 'a="ntrm set"])
+ apply(simp only: perm_fun_def)
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname
NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname)
@@ -3401,7 +3401,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def [where 'a="ntrm set"])
+ apply(simp only: perm_fun_def)
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname
ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname)
@@ -3423,7 +3423,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def [where 'a="ntrm set"])
+ apply(simp only: perm_fun_def)
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname
ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname)
@@ -3445,7 +3445,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def [where 'a="ntrm set"])
+ apply(simp only: perm_fun_def)
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname
IMPLEFT_eqvt_coname)
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Wed Dec 28 22:08:44 2011 +0100
@@ -151,7 +151,7 @@
lemma RRset_gcd [rule_format]:
"is_RRset A m ==> a \<in> A --> zgcd a m = 1"
apply (unfold is_RRset_def)
- apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd a m = 1"], auto)
+ apply (rule RsetR.induct, auto)
done
lemma RsetR_zmult_mono:
@@ -206,7 +206,7 @@
"1 < m ==>
is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
apply (unfold is_RRset_def)
- apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"])
+ apply (rule RsetR.induct)
apply (auto simp add: zcong_sym)
done
--- a/src/HOL/UNITY/Simple/Deadlock.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/UNITY/Simple/Deadlock.thy Wed Dec 28 22:08:44 2011 +0100
@@ -16,26 +16,20 @@
(*a simplification step*)
lemma Collect_le_Int_equals:
"(\<Inter>i \<in> atMost n. A(Suc i) \<inter> A i) = (\<Inter>i \<in> atMost (Suc n). A i)"
-apply (induct_tac "n")
-apply (auto simp add: atMost_Suc)
-done
+ by (induct n) (auto simp add: atMost_Suc)
(*Dual of the required property. Converse inclusion fails.*)
lemma UN_Int_Compl_subset:
"(\<Union>i \<in> lessThan n. A i) \<inter> (- A n) \<subseteq>
(\<Union>i \<in> lessThan n. (A i) \<inter> (- A (Suc i)))"
-apply (induct_tac "n", simp)
-apply (simp add: lessThan_Suc, blast)
-done
+ by (induct n) (auto simp: lessThan_Suc)
(*Converse inclusion fails.*)
lemma INT_Un_Compl_subset:
"(\<Inter>i \<in> lessThan n. -A i \<union> A (Suc i)) \<subseteq>
(\<Inter>i \<in> lessThan n. -A i) \<union> A n"
-apply (induct_tac "n", simp)
-apply (simp add: lessThan_Suc, fast)
-done
+ by (induct n) (auto simp: lessThan_Suc)
(*Specialized rewriting*)
@@ -47,10 +41,9 @@
lemma INT_le_equals_Int:
"(\<Inter>i \<in> atMost n. A i) =
A 0 \<inter> (\<Inter>i \<in> lessThan n. -A i \<union> A(Suc i))"
-apply (induct_tac "n", simp)
-apply (simp add: Int_ac Int_Un_distrib Int_Un_distrib2
- INT_le_equals_Int_lemma lessThan_Suc atMost_Suc)
-done
+ by (induct n)
+ (simp_all add: Int_ac Int_Un_distrib Int_Un_distrib2
+ INT_le_equals_Int_lemma lessThan_Suc atMost_Suc)
lemma INT_le_Suc_equals_Int:
"(\<Inter>i \<in> atMost (Suc n). A i) =
--- a/src/HOL/UNITY/Simple/Reach.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy Wed Dec 28 22:08:44 2011 +0100
@@ -103,7 +103,7 @@
lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def)
apply (rule subset_antisym)
-apply (auto simp add: Compl_FP UN_UN_flatten del: subset_antisym)
+apply (auto simp add: Compl_FP UN_UN_flatten)
apply (rule fun_upd_idem, force)
apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
done
--- a/src/HOL/UNITY/Simple/Reachability.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy Wed Dec 28 22:08:44 2011 +0100
@@ -345,7 +345,7 @@
apply (subgoal_tac [2]
"({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) =
({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))")
-prefer 2 apply simp
+prefer 2 apply blast
prefer 2 apply blast
apply (rule Stable_reachable_EQ_R_AND_nmsg_0
[simplified Eq_lemma2 Collect_const])
--- a/src/HOL/Word/Bit_Representation.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Wed Dec 28 22:08:44 2011 +0100
@@ -235,14 +235,14 @@
apply safe
apply (erule rev_mp)
apply (induct_tac y rule: bin_induct)
- apply (safe del: subset_antisym)
+ apply safe
apply (drule_tac x=0 in fun_cong, force)
apply (erule notE, rule ext,
drule_tac x="Suc x" in fun_cong, force)
apply (drule_tac x=0 in fun_cong, force simp: BIT_simps)
apply (erule rev_mp)
apply (induct_tac y rule: bin_induct)
- apply (safe del: subset_antisym)
+ apply safe
apply (drule_tac x=0 in fun_cong, force)
apply (erule notE, rule ext,
drule_tac x="Suc x" in fun_cong, force)
--- a/src/HOL/Word/Word.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Word/Word.thy Wed Dec 28 22:08:44 2011 +0100
@@ -2389,7 +2389,7 @@
"n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
apply (unfold word_size td_ext_def')
- apply (safe del: subset_antisym)
+ apply safe
apply (rule_tac [3] ext)
apply (rule_tac [4] ext)
apply (unfold word_size of_nth_def test_bit_bl)
--- a/src/HOL/ex/CTL.thy Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/ex/CTL.thy Wed Dec 28 22:08:44 2011 +0100
@@ -252,8 +252,8 @@
proof -
{
have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
- moreover have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
- ultimately have "?lhs \<subseteq> \<AX> p" by auto
+ also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
+ finally have "?lhs \<subseteq> \<AX> p" by auto
}
moreover
{
@@ -261,8 +261,7 @@
also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
}
- ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)"
- by (rule Int_greatest)
+ ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
finally show ?thesis .
qed