# HG changeset patch # User wenzelm # Date 1325098993 -3600 # Node ID c296c75f4cf40a5ac422b711f5dffd89a987517f # Parent 493d9c4d7ed5b612db70aea6cc633f4ef55e0b5c reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; tuned proofs; diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Algebra/Group.thy Wed Dec 28 20:03:13 2011 +0100 @@ -771,42 +771,36 @@ proof (rule partial_order.complete_lattice_criterion1) show "partial_order ?L" by (rule subgroups_partial_order) next - show "\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 "\G. greatest ?L G (carrier ?L)" .. next fix A assume L: "A \ carrier ?L" and non_empty: "A ~= {}" then have Int_subgroup: "subgroup (\A) G" by (fastforce intro: subgroups_Inter) - show "\I. greatest ?L I (Lower ?L A)" - proof - show "greatest ?L (\A) (Lower ?L A)" - (is "greatest _ ?Int _") - proof (rule greatest_LowerI) - fix H - assume H: "H \ 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 \ H" by fastforce - then show "le ?L ?Int H" by simp - next - fix H - assume H: "H \ Lower ?L A" - with L Int_subgroup show "le ?L H ?Int" - by (fastforce simp: Lower_def intro: Inter_greatest) - next - show "A \ carrier ?L" by (rule L) - next - show "?Int \ carrier ?L" by simp (rule Int_subgroup) - qed + have "greatest ?L (\A) (Lower ?L A)" (is "greatest _ ?Int _") + proof (rule greatest_LowerI) + fix H + assume H: "H \ 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 \ H" by fastforce + then show "le ?L ?Int H" by simp + next + fix H + assume H: "H \ Lower ?L A" + with L Int_subgroup show "le ?L H ?Int" + by (fastforce simp: Lower_def intro: Inter_greatest) + next + show "A \ carrier ?L" by (rule L) + next + show "?Int \ carrier ?L" by simp (rule Int_subgroup) qed + then show "\I. greatest ?L I (Lower ?L A)" .. qed end diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Algebra/Lattice.thy Wed Dec 28 20:03:13 2011 +0100 @@ -1285,22 +1285,18 @@ by default auto next fix B - assume B: "B \ carrier ?L" - show "EX s. least ?L s (Upper ?L B)" - proof - from B show "least ?L (\ B) (Upper ?L B)" - by (fastforce intro!: least_UpperI simp: Upper_def) - qed + assume "B \ carrier ?L" + then have "least ?L (\ 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 \ carrier ?L" - show "EX i. greatest ?L i (Lower ?L B)" - proof - from B show "greatest ?L (\ B \ A) (Lower ?L B)" - txt {* @{term "\ B"} is not the infimum of @{term B}: - @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! *} - by (fastforce intro!: greatest_LowerI simp: Lower_def) - qed + assume "B \ carrier ?L" + then have "greatest ?L (\ B \ A) (Lower ?L B)" + txt {* @{term "\ B"} is not the infimum of @{term B}: + @{term "\ {} = 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, diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Auth/Guard/Analz.thy --- a/src/HOL/Auth/Guard/Analz.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Auth/Guard/Analz.thy Wed Dec 28 20:03:13 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 |] diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Auth/Guard/Extensions.thy --- a/src/HOL/Auth/Guard/Extensions.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Auth/Guard/Extensions.thy Wed Dec 28 20:03:13 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*} diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/HOLCF/FOCUS/Stream_adm.thy --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy Wed Dec 28 20:03:13 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) diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Hoare_Parallel/OG_Hoare.thy --- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Dec 28 20:03:13 2011 +0100 @@ -149,8 +149,7 @@ text {* Strong Soundness for Component Programs:*} -lemma ann_hoare_case_analysis [rule_format]: - defines I: "I \ \C q'. +lemma ann_hoare_case_analysis [rule_format]: "\ C q' \ ((\r f. C = AnnBasic r f \ (\q. r \ {s. f s \ q} \ q \ q')) \ (\c0 c1. C = AnnSeq c0 c1 \ (\q. q \ q' \ \ c0 pre c1 \ \ c1 q)) \ (\r b c1 c2. C = AnnCond1 r b c1 c2 \ (\q. q \ q' \ @@ -160,9 +159,8 @@ (\r i b c. C = AnnWhile r b i c \ (\q. q \ q' \ r \ i \ i \ b \ pre c \ \ c i \ i \ -b \ q)) \ (\r b c. C = AnnAwait r b c \ (\q. q \ q' \ \- (r \ b) c q)))" - shows "\ C q' \ 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) diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Inductive.thy Wed Dec 28 20:03:13 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 diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Isar_Examples/Mutilated_Checkerboard.thy --- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Dec 28 20:03:13 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 \ 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)" . diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Library/Zorn.thy Wed Dec 28 20:03:13 2011 +0100 @@ -58,19 +58,18 @@ lemma Abrial_axiom1: "x \ succ S x" apply (auto simp add: succ_def super_def maxchain_def) apply (rule contrapos_np, assumption) - apply (rule_tac Q="\S. xa \ S" in someI2, blast+) + apply (rule someI2) + apply blast+ done lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI] lemma TFin_induct: - assumes H: "n \ TFin S" - and I: "!!x. x \ TFin S ==> P x ==> P (succ S x)" - "!!Y. Y \ 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 \ TFin S" and + I: "!!x. x \ TFin S ==> P x ==> P (succ S x)" + "!!Y. Y \ TFin S ==> Ball Y P ==> P (Union Y)" + shows "P n" + using H by induct (blast intro: I)+ lemma succ_trans: "x \ y ==> x \ succ S y" apply (erule subset_trans) @@ -160,7 +159,8 @@ lemma select_super: "c \ chain S - maxchain S ==> (\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: "\c. (c :: 'a set set): maxchain S" diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/NSA/Filter.thy --- a/src/HOL/NSA/Filter.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/NSA/Filter.thy Wed Dec 28 20:03:13 2011 +0100 @@ -391,12 +391,10 @@ fix A assume "A \ 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] diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/NSA/StarDef.thy Wed Dec 28 20:03:13 2011 +0100 @@ -17,7 +17,7 @@ lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \" apply (unfold FreeUltrafilterNat_def) -apply (rule someI_ex [where P=freeultrafilter]) +apply (rule someI_ex) apply (rule freeultrafilter_Ex) apply (rule nat_infinite) done diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Nominal/Examples/Class2.thy --- a/src/HOL/Nominal/Examples/Class2.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Nominal/Examples/Class2.thy Wed Dec 28 20:03:13 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) diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Old_Number_Theory/EulerFermat.thy --- a/src/HOL/Old_Number_Theory/EulerFermat.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Wed Dec 28 20:03:13 2011 +0100 @@ -151,7 +151,7 @@ lemma RRset_gcd [rule_format]: "is_RRset A m ==> a \ A --> zgcd a m = 1" apply (unfold is_RRset_def) - apply (rule RsetR.induct [where P="%A. a \ 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 \ A --> b \ A --> a = b" apply (unfold is_RRset_def) - apply (rule RsetR.induct [where P="%A. a \ A --> b \ A --> a = b"]) + apply (rule RsetR.induct) apply (auto simp add: zcong_sym) done diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/UNITY/Simple/Deadlock.thy --- a/src/HOL/UNITY/Simple/Deadlock.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/UNITY/Simple/Deadlock.thy Wed Dec 28 20:03:13 2011 +0100 @@ -16,26 +16,20 @@ (*a simplification step*) lemma Collect_le_Int_equals: "(\i \ atMost n. A(Suc i) \ A i) = (\i \ 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: "(\i \ lessThan n. A i) \ (- A n) \ (\i \ lessThan n. (A i) \ (- 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: "(\i \ lessThan n. -A i \ A (Suc i)) \ (\i \ lessThan n. -A i) \ 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: "(\i \ atMost n. A i) = A 0 \ (\i \ lessThan n. -A i \ 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: "(\i \ atMost (Suc n). A i) = diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/UNITY/Simple/Reach.thy --- a/src/HOL/UNITY/Simple/Reach.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/UNITY/Simple/Reach.thy Wed Dec 28 20:03:13 2011 +0100 @@ -103,7 +103,7 @@ lemma Compl_fixedpoint: "- fixedpoint = (\(u,v)\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 diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/UNITY/Simple/Reachability.thy --- a/src/HOL/UNITY/Simple/Reachability.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/UNITY/Simple/Reachability.thy Wed Dec 28 20:03:13 2011 +0100 @@ -345,7 +345,7 @@ apply (subgoal_tac [2] "({s. (s \ reachable v) = ((root,v) \ REACHABLE) } \ nmsg_eq 0 (v,w)) = ({s. (s \ reachable v) = ( (root,v) \ REACHABLE) } \ (- UNIV \ 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]) diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Word/Bit_Representation.thy --- a/src/HOL/Word/Bit_Representation.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Word/Bit_Representation.thy Wed Dec 28 20:03:13 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) diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/Word/Word.thy Wed Dec 28 20:03:13 2011 +0100 @@ -2407,7 +2407,7 @@ "n = size (w::'a::len0 word) \ ofn = set_bits \ [w, ofn g] = l \ 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) diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/ex/CTL.thy --- a/src/HOL/ex/CTL.thy Wed Dec 28 15:08:12 2011 +0100 +++ b/src/HOL/ex/CTL.thy Wed Dec 28 20:03:13 2011 +0100 @@ -252,8 +252,8 @@ proof - { have "\ (p \ \ p) \ p \ \ p" by (rule AG_fp_1) - moreover have "p \ p \ \ p \ \ p" .. - ultimately have "?lhs \ \ p" by auto + also have "p \ p \ \ p \ \ p" .. + finally have "?lhs \ \ p" by auto } moreover { @@ -261,8 +261,7 @@ also have "\ \ \ \" by (rule AG_fp_2) finally have "?lhs \ \ \ (p \ \ p)" . } - ultimately have "?lhs \ \ p \ \ \ (p \ \ p)" - by (rule Int_greatest) + ultimately have "?lhs \ \ p \ \ \ (p \ \ p)" .. also have "\ = \ ?lhs" by (simp only: AX_int) finally show ?thesis . qed