author wenzelm Wed Dec 28 22:08:44 2011 +0100 (2011-12-28) changeset 46025 64a19ea435fc parent 46024 b4dcefaa1721 parent 46008 c296c75f4cf4 child 46026 83caa4f4bd56
merged
 src/HOL/Word/Bit_Representation.thy file | annotate | diff | revisions src/HOL/Word/Word.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Dec 28 20:05:52 2011 +0100
1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Dec 28 22:08:44 2011 +0100
1.3 @@ -771,42 +771,36 @@
1.4  proof (rule partial_order.complete_lattice_criterion1)
1.5    show "partial_order ?L" by (rule subgroups_partial_order)
1.6  next
1.7 -  show "\<exists>G. greatest ?L G (carrier ?L)"
1.8 -  proof
1.9 -    show "greatest ?L (carrier G) (carrier ?L)"
1.10 -      by (unfold greatest_def)
1.11 -        (simp add: subgroup.subset subgroup_self)
1.12 -  qed
1.13 +  have "greatest ?L (carrier G) (carrier ?L)"
1.14 +    by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
1.15 +  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
1.16  next
1.17    fix A
1.18    assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
1.19    then have Int_subgroup: "subgroup (\<Inter>A) G"
1.20      by (fastforce intro: subgroups_Inter)
1.21 -  show "\<exists>I. greatest ?L I (Lower ?L A)"
1.22 -  proof
1.23 -    show "greatest ?L (\<Inter>A) (Lower ?L A)"
1.24 -      (is "greatest _ ?Int _")
1.25 -    proof (rule greatest_LowerI)
1.26 -      fix H
1.27 -      assume H: "H \<in> A"
1.28 -      with L have subgroupH: "subgroup H G" by auto
1.29 -      from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
1.30 -        by (rule subgroup_imp_group)
1.31 -      from groupH have monoidH: "monoid ?H"
1.32 -        by (rule group.is_monoid)
1.33 -      from H have Int_subset: "?Int \<subseteq> H" by fastforce
1.34 -      then show "le ?L ?Int H" by simp
1.35 -    next
1.36 -      fix H
1.37 -      assume H: "H \<in> Lower ?L A"
1.38 -      with L Int_subgroup show "le ?L H ?Int"
1.39 -        by (fastforce simp: Lower_def intro: Inter_greatest)
1.40 -    next
1.41 -      show "A \<subseteq> carrier ?L" by (rule L)
1.42 -    next
1.43 -      show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
1.44 -    qed
1.45 +  have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _")
1.46 +  proof (rule greatest_LowerI)
1.47 +    fix H
1.48 +    assume H: "H \<in> A"
1.49 +    with L have subgroupH: "subgroup H G" by auto
1.50 +    from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
1.51 +      by (rule subgroup_imp_group)
1.52 +    from groupH have monoidH: "monoid ?H"
1.53 +      by (rule group.is_monoid)
1.54 +    from H have Int_subset: "?Int \<subseteq> H" by fastforce
1.55 +    then show "le ?L ?Int H" by simp
1.56 +  next
1.57 +    fix H
1.58 +    assume H: "H \<in> Lower ?L A"
1.59 +    with L Int_subgroup show "le ?L H ?Int"
1.60 +      by (fastforce simp: Lower_def intro: Inter_greatest)
1.61 +  next
1.62 +    show "A \<subseteq> carrier ?L" by (rule L)
1.63 +  next
1.64 +    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
1.65    qed
1.66 +  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
1.67  qed
1.68
1.69  end
```
```     2.1 --- a/src/HOL/Algebra/Lattice.thy	Wed Dec 28 20:05:52 2011 +0100
2.2 +++ b/src/HOL/Algebra/Lattice.thy	Wed Dec 28 22:08:44 2011 +0100
2.3 @@ -1285,22 +1285,18 @@
2.4      by default auto
2.5  next
2.6    fix B
2.7 -  assume B: "B \<subseteq> carrier ?L"
2.8 -  show "EX s. least ?L s (Upper ?L B)"
2.9 -  proof
2.10 -    from B show "least ?L (\<Union> B) (Upper ?L B)"
2.11 -      by (fastforce intro!: least_UpperI simp: Upper_def)
2.12 -  qed
2.13 +  assume "B \<subseteq> carrier ?L"
2.14 +  then have "least ?L (\<Union> B) (Upper ?L B)"
2.15 +    by (fastforce intro!: least_UpperI simp: Upper_def)
2.16 +  then show "EX s. least ?L s (Upper ?L B)" ..
2.17  next
2.18    fix B
2.19 -  assume B: "B \<subseteq> carrier ?L"
2.20 -  show "EX i. greatest ?L i (Lower ?L B)"
2.21 -  proof
2.22 -    from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
2.23 -      txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
2.24 -        @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
2.25 -      by (fastforce intro!: greatest_LowerI simp: Lower_def)
2.26 -  qed
2.27 +  assume "B \<subseteq> carrier ?L"
2.28 +  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
2.29 +    txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
2.30 +      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
2.31 +    by (fastforce intro!: greatest_LowerI simp: Lower_def)
2.32 +  then show "EX i. greatest ?L i (Lower ?L B)" ..
2.33  qed
2.34
2.35  text {* An other example, that of the lattice of subgroups of a group,
```
```     3.1 --- a/src/HOL/Auth/Guard/Analz.thy	Wed Dec 28 20:05:52 2011 +0100
3.2 +++ b/src/HOL/Auth/Guard/Analz.thy	Wed Dec 28 22:08:44 2011 +0100
3.3 @@ -236,9 +236,10 @@
3.4
3.5  lemma kparts_insert_synth: "[| Y:parts (insert X G); X:synth (analz G);
3.6  Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Y:parts G"
3.7 -apply (drule parts_insert_substD [where P="%S. Y : S"], clarify)
3.8 +apply (drule parts_insert_substD, clarify)
3.9  apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
3.10 -by (auto dest: Nonce_kparts_synth)
3.11 +apply (auto dest: Nonce_kparts_synth)
3.12 +done
3.13
3.14  lemma Crypt_insert_synth:
3.15    "[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |]
```
```     4.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Wed Dec 28 20:05:52 2011 +0100
4.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Wed Dec 28 22:08:44 2011 +0100
4.3 @@ -198,7 +198,7 @@
4.4
4.5  lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==>
4.6  X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H"
4.7 -by (erule parts.induct, (fastforce dest: parts.Fst parts.Snd parts.Body)+)
4.8 +by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body)
4.9
4.10  lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}"
4.11  by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body)
4.12 @@ -207,10 +207,11 @@
4.13
4.14  lemma Crypt_synth_insert: "[| Crypt K X:parts (insert Y H);
4.15  Y:synth (analz H); Key K ~:analz H |] ==> Crypt K X:parts H"
4.16 -apply (drule parts_insert_substD [where P="%S. Crypt K X : S"], clarify)
4.17 +apply (drule parts_insert_substD, clarify)
4.18  apply (frule in_sub)
4.19  apply (frule parts_mono)
4.20 -by auto
4.21 +apply auto
4.22 +done
4.23
4.24  subsubsection{*greatest nonce used in a message*}
4.25
```
```     5.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Wed Dec 28 20:05:52 2011 +0100
5.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Wed Dec 28 22:08:44 2011 +0100
5.3 @@ -60,7 +60,7 @@
5.4    assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. enat k < #((Y j)::'a::flat stream)|]
5.5    ==> P(LUB i. Y i))"
5.6    shows "P(LUB i. Y i)"
5.7 -apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2])
5.8 +apply (rule increasing_chain_adm_lemma [OF 1 2])
5.9  apply (erule 3, assumption)
5.10  apply (erule thin_rl)
5.11  apply (rule allI)
```
```     6.1 --- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Dec 28 20:05:52 2011 +0100
6.2 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Dec 28 22:08:44 2011 +0100
6.3 @@ -149,8 +149,7 @@
6.4
6.5  text {* Strong Soundness for Component Programs:*}
6.6
6.7 -lemma ann_hoare_case_analysis [rule_format]:
6.8 -  defines I: "I \<equiv> \<lambda>C q'.
6.9 +lemma ann_hoare_case_analysis [rule_format]: "\<turnstile> C q' \<longrightarrow>
6.10    ((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and>
6.11    (\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and>
6.12    (\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and>
6.13 @@ -160,9 +159,8 @@
6.14    (\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow>
6.15    (\<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>
6.16    (\<forall>r b c. C = AnnAwait r b c \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<parallel>- (r \<inter> b) c q)))"
6.17 -  shows "\<turnstile> C q' \<longrightarrow> I C q'"
6.18  apply(rule ann_hoare_induct)
6.20 +apply simp_all
6.21   apply(rule_tac x=q in exI,simp)+
6.22  apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+
6.23  apply(clarify,simp,clarify,rule_tac x=qa in exI,fast)
```
```     7.1 --- a/src/HOL/Inductive.thy	Wed Dec 28 20:05:52 2011 +0100
7.2 +++ b/src/HOL/Inductive.thy	Wed Dec 28 22:08:44 2011 +0100
7.3 @@ -108,7 +108,7 @@
7.4    and P_f: "!!S. P S ==> P(f S)"
7.5    and P_Union: "!!M. !S:M. P S ==> P(Union M)"
7.6    shows "P(lfp f)"
7.7 -  using assms by (rule lfp_ordinal_induct [where P=P])
7.8 +  using assms by (rule lfp_ordinal_induct)
7.9
7.10
7.11  text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
7.12 @@ -210,7 +210,7 @@
7.13  apply (rule Un_least [THEN Un_least])
7.14  apply (rule subset_refl, assumption)
7.15  apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
7.16 -apply (rule monoD [where f=f], assumption)
7.17 +apply (rule monoD, assumption)
7.18  apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
7.19  done
7.20
```
```     8.1 --- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Wed Dec 28 20:05:52 2011 +0100
8.2 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Wed Dec 28 22:08:44 2011 +0100
8.3 @@ -128,7 +128,7 @@
8.4    let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
8.5    have "?B (Suc n) = ?a Un ?B n"
8.6      by (auto simp add: Sigma_Suc Un_assoc)
8.7 -  moreover have "... : ?T"
8.8 +  also have "... : ?T"
8.9    proof (rule tiling.Un)
8.10      have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
8.11        by (rule domino.horiz)
8.12 @@ -137,7 +137,7 @@
8.13      show "?B n : ?T" by (rule Suc)
8.14      show "?a <= - ?B n" by blast
8.15    qed
8.16 -  ultimately show ?case by simp
8.17 +  finally show ?case .
8.18  qed
8.19
8.20  lemma dominoes_tile_matrix:
8.21 @@ -150,13 +150,13 @@
8.22    case (Suc m)
8.23    let ?t = "{m} <*> below (2 * n)"
8.24    have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
8.25 -  moreover have "... : ?T"
8.26 +  also have "... : ?T"
8.27    proof (rule tiling_Un)
8.28      show "?t : ?T" by (rule dominoes_tile_row)
8.29      show "?B m : ?T" by (rule Suc)
8.30      show "?t Int ?B m = {}" by blast
8.31    qed
8.32 -  ultimately show ?case by simp
8.33 +  finally show ?case .
8.34  qed
8.35
8.36  lemma domino_singleton:
8.37 @@ -219,8 +219,8 @@
8.38        have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
8.39        then show ?thesis by (blast intro: that)
8.40      qed
8.41 -    moreover have "... Un ?e t b = insert (i, j) (?e t b)" by simp
8.42 -    moreover have "card ... = Suc (card (?e t b))"
8.43 +    also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
8.44 +    also have "card ... = Suc (card (?e t b))"
8.45      proof (rule card_insert_disjoint)
8.46        from `t \<in> tiling domino` have "finite t"
8.47          by (rule tiling_domino_finite)
8.48 @@ -229,7 +229,7 @@
8.49        from e have "(i, j) : ?e a b" by simp
8.50        with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
8.51      qed
8.52 -    ultimately show "?thesis b" by simp
8.53 +    finally show "?thesis b" .
8.54    qed
8.55    then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
8.56    also from hyp have "card (?e t 0) = card (?e t 1)" .
```
```     9.1 --- a/src/HOL/Library/Zorn.thy	Wed Dec 28 20:05:52 2011 +0100
9.2 +++ b/src/HOL/Library/Zorn.thy	Wed Dec 28 22:08:44 2011 +0100
9.3 @@ -58,19 +58,18 @@
9.4  lemma Abrial_axiom1: "x \<subseteq> succ S x"
9.5    apply (auto simp add: succ_def super_def maxchain_def)
9.6    apply (rule contrapos_np, assumption)
9.7 -  apply (rule_tac Q="\<lambda>S. xa \<in> S" in someI2, blast+)
9.8 +  apply (rule someI2)
9.9 +  apply blast+
9.10    done
9.11
9.12  lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
9.13
9.14  lemma TFin_induct:
9.15 -  assumes H: "n \<in> TFin S"
9.16 -  and I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
9.17 -    "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P(Union Y)"
9.18 -  shows "P n" using H
9.19 -  apply (induct rule: TFin.induct [where P=P])
9.20 -   apply (blast intro: I)+
9.21 -  done
9.22 +  assumes H: "n \<in> TFin S" and
9.23 +    I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
9.24 +      "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P (Union Y)"
9.25 +  shows "P n"
9.26 +  using H by induct (blast intro: I)+
9.27
9.28  lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
9.29    apply (erule subset_trans)
9.30 @@ -160,7 +159,8 @@
9.31  lemma select_super:
9.32       "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
9.33    apply (erule mem_super_Ex [THEN exE])
9.34 -  apply (rule someI2 [where Q="%X. X : super S c"], auto)
9.35 +  apply (rule someI2)
9.36 +  apply auto
9.37    done
9.38
9.39  lemma select_not_equals:
9.40 @@ -185,8 +185,8 @@
9.41    apply (unfold chain_def chain_subset_def)
9.42    apply (rule CollectI, safe)
9.43     apply (drule bspec, assumption)
9.44 -   apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
9.45 -     best+)
9.46 +   apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE])
9.47 +      apply blast+
9.48    done
9.49
9.50  theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
```
```    10.1 --- a/src/HOL/NSA/Filter.thy	Wed Dec 28 20:05:52 2011 +0100
10.2 +++ b/src/HOL/NSA/Filter.thy	Wed Dec 28 22:08:44 2011 +0100
10.3 @@ -391,12 +391,10 @@
10.4      fix A assume "A \<in> U"
10.5      with U show "infinite A" by (rule mem_superfrechet_all_infinite)
10.6    qed
10.7 -  show ?thesis
10.8 -  proof
10.9 -    from fil ultra free show "freeultrafilter U"
10.10 -      by (rule freeultrafilter.intro [OF ultrafilter.intro])
10.11 -      (* FIXME: unfold_locales should use chained facts *)
10.12 -  qed
10.13 +  from fil ultra free have "freeultrafilter U"
10.14 +    by (rule freeultrafilter.intro [OF ultrafilter.intro])
10.15 +    (* FIXME: unfold_locales should use chained facts *)
10.16 +  then show ?thesis ..
10.17  qed
10.18
10.19  lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
```
```    11.1 --- a/src/HOL/NSA/StarDef.thy	Wed Dec 28 20:05:52 2011 +0100
11.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Dec 28 22:08:44 2011 +0100
11.3 @@ -17,7 +17,7 @@
11.4
11.5  lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
11.6  apply (unfold FreeUltrafilterNat_def)
11.7 -apply (rule someI_ex [where P=freeultrafilter])
11.8 +apply (rule someI_ex)
11.9  apply (rule freeultrafilter_Ex)
11.10  apply (rule nat_infinite)
11.11  done
```
```    12.1 --- a/src/HOL/Nominal/Examples/Class2.thy	Wed Dec 28 20:05:52 2011 +0100
12.2 +++ b/src/HOL/Nominal/Examples/Class2.thy	Wed Dec 28 22:08:44 2011 +0100
12.3 @@ -3245,7 +3245,7 @@
12.4    { case 1 show ?case
12.5        apply -
12.7 -      apply(simp add: perm_fun_def [where 'a="ntrm set"])
12.9        apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
12.10        apply(perm_simp)
12.11      done
12.12 @@ -3256,7 +3256,7 @@
12.13        apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
12.16 -      apply(simp add: perm_fun_def [where 'a="ntrm set"])
12.18        apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
12.19        apply(perm_simp)
12.20        done
12.21 @@ -3269,7 +3269,7 @@
12.22      apply -
12.23      apply(simp only: lfp_eqvt)
12.24      apply(simp only: comp_def)
12.25 -    apply(simp only: perm_fun_def [where 'a="ntrm set"])
12.26 +    apply(simp only: perm_fun_def)
12.27      apply(simp only: NEGc.simps NEGn.simps)
12.28      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)
12.30 @@ -3289,7 +3289,7 @@
12.31      apply -
12.32      apply(simp only: lfp_eqvt)
12.33      apply(simp only: comp_def)
12.34 -    apply(simp only: perm_fun_def [where 'a="ntrm set"])
12.35 +    apply(simp only: perm_fun_def)
12.36      apply(simp only: NEGc.simps NEGn.simps)
12.37      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name
12.38                       ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name)
12.39 @@ -3311,7 +3311,7 @@
12.40      apply -
12.41      apply(simp only: lfp_eqvt)
12.42      apply(simp only: comp_def)
12.43 -    apply(simp only: perm_fun_def [where 'a="ntrm set"])
12.44 +    apply(simp only: perm_fun_def)
12.45      apply(simp only: NEGc.simps NEGn.simps)
12.46      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name
12.47                       ORRIGHT2_eqvt_name ORLEFT_eqvt_name)
12.48 @@ -3333,7 +3333,7 @@
12.49      apply -
12.50      apply(simp only: lfp_eqvt)
12.51      apply(simp only: comp_def)
12.52 -    apply(simp only: perm_fun_def [where 'a="ntrm set"])
12.53 +    apply(simp only: perm_fun_def)
12.54      apply(simp only: NEGc.simps NEGn.simps)
12.55      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)
12.56      apply(perm_simp add: ih1 ih2 ih3 ih4)
12.57 @@ -3355,7 +3355,7 @@
12.58    { case 1 show ?case
12.59        apply -
12.61 -      apply(simp add: perm_fun_def [where 'a="ntrm set"])
12.63        apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
12.64        apply(perm_simp)
12.65      done
12.66 @@ -3366,7 +3366,7 @@
12.67        apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
12.70 -      apply(simp add: perm_fun_def [where 'a="ntrm set"])
12.72        apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
12.73        apply(perm_simp)
12.74        done
12.75 @@ -3379,7 +3379,7 @@
12.76      apply -
12.77      apply(simp only: lfp_eqvt)
12.78      apply(simp only: comp_def)
12.79 -    apply(simp only: perm_fun_def [where 'a="ntrm set"])
12.80 +    apply(simp only: perm_fun_def)
12.81      apply(simp only: NEGc.simps NEGn.simps)
12.82      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname
12.83              NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname)
12.84 @@ -3401,7 +3401,7 @@
12.85      apply -
12.86      apply(simp only: lfp_eqvt)
12.87      apply(simp only: comp_def)
12.88 -    apply(simp only: perm_fun_def [where 'a="ntrm set"])
12.89 +    apply(simp only: perm_fun_def)
12.90      apply(simp only: NEGc.simps NEGn.simps)
12.91      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname
12.92                       ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname)
12.93 @@ -3423,7 +3423,7 @@
12.94      apply -
12.95      apply(simp only: lfp_eqvt)
12.96      apply(simp only: comp_def)
12.97 -    apply(simp only: perm_fun_def [where 'a="ntrm set"])
12.98 +    apply(simp only: perm_fun_def)
12.99      apply(simp only: NEGc.simps NEGn.simps)
12.100      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname
12.101                       ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname)
12.102 @@ -3445,7 +3445,7 @@
12.103      apply -
12.104      apply(simp only: lfp_eqvt)
12.105      apply(simp only: comp_def)
12.106 -    apply(simp only: perm_fun_def [where 'a="ntrm set"])
12.107 +    apply(simp only: perm_fun_def)
12.108      apply(simp only: NEGc.simps NEGn.simps)
12.109      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname
12.110           IMPLEFT_eqvt_coname)
```
```    13.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Wed Dec 28 20:05:52 2011 +0100
13.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Wed Dec 28 22:08:44 2011 +0100
13.3 @@ -151,7 +151,7 @@
13.4  lemma RRset_gcd [rule_format]:
13.5      "is_RRset A m ==> a \<in> A --> zgcd a m = 1"
13.6    apply (unfold is_RRset_def)
13.7 -  apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd a m = 1"], auto)
13.8 +  apply (rule RsetR.induct, auto)
13.9    done
13.10
13.11  lemma RsetR_zmult_mono:
13.12 @@ -206,7 +206,7 @@
13.13    "1 < m ==>
13.14      is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
13.15    apply (unfold is_RRset_def)
13.16 -  apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"])
13.17 +  apply (rule RsetR.induct)
13.18      apply (auto simp add: zcong_sym)
13.19    done
13.20
```
```    14.1 --- a/src/HOL/UNITY/Simple/Deadlock.thy	Wed Dec 28 20:05:52 2011 +0100
14.2 +++ b/src/HOL/UNITY/Simple/Deadlock.thy	Wed Dec 28 22:08:44 2011 +0100
14.3 @@ -16,26 +16,20 @@
14.4  (*a simplification step*)
14.5  lemma Collect_le_Int_equals:
14.6       "(\<Inter>i \<in> atMost n. A(Suc i) \<inter> A i) = (\<Inter>i \<in> atMost (Suc n). A i)"
14.7 -apply (induct_tac "n")
14.8 -apply (auto simp add: atMost_Suc)
14.9 -done
14.10 +  by (induct n) (auto simp add: atMost_Suc)
14.11
14.12  (*Dual of the required property.  Converse inclusion fails.*)
14.13  lemma UN_Int_Compl_subset:
14.14       "(\<Union>i \<in> lessThan n. A i) \<inter> (- A n) \<subseteq>
14.15        (\<Union>i \<in> lessThan n. (A i) \<inter> (- A (Suc i)))"
14.16 -apply (induct_tac "n", simp)
14.17 -apply (simp add: lessThan_Suc, blast)
14.18 -done
14.19 +  by (induct n) (auto simp: lessThan_Suc)
14.20
14.21
14.22  (*Converse inclusion fails.*)
14.23  lemma INT_Un_Compl_subset:
14.24       "(\<Inter>i \<in> lessThan n. -A i \<union> A (Suc i))  \<subseteq>
14.25        (\<Inter>i \<in> lessThan n. -A i) \<union> A n"
14.26 -apply (induct_tac "n", simp)
14.27 -apply (simp add: lessThan_Suc, fast)
14.28 -done
14.29 +  by (induct n) (auto simp: lessThan_Suc)
14.30
14.31
14.32  (*Specialized rewriting*)
14.33 @@ -47,10 +41,9 @@
14.34  lemma INT_le_equals_Int:
14.35       "(\<Inter>i \<in> atMost n. A i) =
14.36        A 0 \<inter> (\<Inter>i \<in> lessThan n. -A i \<union> A(Suc i))"
14.37 -apply (induct_tac "n", simp)
14.38 -apply (simp add: Int_ac Int_Un_distrib Int_Un_distrib2
14.39 -                 INT_le_equals_Int_lemma lessThan_Suc atMost_Suc)
14.40 -done
14.41 +  by (induct n)
14.42 +    (simp_all add: Int_ac Int_Un_distrib Int_Un_distrib2
14.43 +      INT_le_equals_Int_lemma lessThan_Suc atMost_Suc)
14.44
14.45  lemma INT_le_Suc_equals_Int:
14.46       "(\<Inter>i \<in> atMost (Suc n). A i) =
```
```    15.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Wed Dec 28 20:05:52 2011 +0100
15.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Wed Dec 28 22:08:44 2011 +0100
15.3 @@ -103,7 +103,7 @@
15.4  lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
15.5  apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def)
15.6  apply (rule subset_antisym)
15.7 -apply (auto simp add: Compl_FP UN_UN_flatten del: subset_antisym)
15.8 +apply (auto simp add: Compl_FP UN_UN_flatten)
15.9   apply (rule fun_upd_idem, force)
15.10  apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
15.11  done
```
```    16.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Wed Dec 28 20:05:52 2011 +0100
16.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Wed Dec 28 22:08:44 2011 +0100
16.3 @@ -345,7 +345,7 @@
16.4  apply (subgoal_tac [2]
16.5       "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) =
16.6        ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))")
16.7 -prefer 2 apply simp
16.8 +prefer 2 apply blast
16.9  prefer 2 apply blast
16.10  apply (rule Stable_reachable_EQ_R_AND_nmsg_0
16.11              [simplified Eq_lemma2 Collect_const])
```
```    17.1 --- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 28 20:05:52 2011 +0100
17.2 +++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 28 22:08:44 2011 +0100
17.3 @@ -235,14 +235,14 @@
17.4      apply safe
17.5      apply (erule rev_mp)
17.6      apply (induct_tac y rule: bin_induct)
17.7 -      apply (safe del: subset_antisym)
17.8 +      apply safe
17.9        apply (drule_tac x=0 in fun_cong, force)
17.10       apply (erule notE, rule ext,
17.11              drule_tac x="Suc x" in fun_cong, force)
17.12      apply (drule_tac x=0 in fun_cong, force simp: BIT_simps)
17.13     apply (erule rev_mp)
17.14     apply (induct_tac y rule: bin_induct)
17.15 -     apply (safe del: subset_antisym)
17.16 +     apply safe
17.17       apply (drule_tac x=0 in fun_cong, force)
17.18      apply (erule notE, rule ext,
17.19             drule_tac x="Suc x" in fun_cong, force)
```
```    18.1 --- a/src/HOL/Word/Word.thy	Wed Dec 28 20:05:52 2011 +0100
18.2 +++ b/src/HOL/Word/Word.thy	Wed Dec 28 22:08:44 2011 +0100
18.3 @@ -2389,7 +2389,7 @@
18.4    "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
18.5      td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
18.6    apply (unfold word_size td_ext_def')
18.7 -  apply (safe del: subset_antisym)
18.8 +  apply safe
18.9       apply (rule_tac [3] ext)
18.10       apply (rule_tac [4] ext)
18.11       apply (unfold word_size of_nth_def test_bit_bl)
```
```    19.1 --- a/src/HOL/ex/CTL.thy	Wed Dec 28 20:05:52 2011 +0100
19.2 +++ b/src/HOL/ex/CTL.thy	Wed Dec 28 22:08:44 2011 +0100
19.3 @@ -252,8 +252,8 @@
19.4        proof -
19.5          {
19.6            have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
19.7 -          moreover have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
19.8 -          ultimately have "?lhs \<subseteq> \<AX> p" by auto
19.9 +          also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
19.10 +          finally have "?lhs \<subseteq> \<AX> p" by auto
19.11          }
19.12          moreover
19.13          {
19.14 @@ -261,8 +261,7 @@
19.15            also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
19.16            finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
19.17          }
19.18 -        ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)"
19.19 -          by (rule Int_greatest)
19.20 +        ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
19.21          also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
19.22          finally show ?thesis .
19.23        qed
```