reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
authorwenzelm
Wed Dec 28 20:03:13 2011 +0100 (2011-12-28)
changeset 46008c296c75f4cf4
parent 46007 493d9c4d7ed5
child 46025 64a19ea435fc
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
tuned proofs;
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Auth/Guard/Analz.thy
src/HOL/Auth/Guard/Extensions.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/Hoare_Parallel/OG_Hoare.thy
src/HOL/Inductive.thy
src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
src/HOL/Library/Zorn.thy
src/HOL/NSA/Filter.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nominal/Examples/Class2.thy
src/HOL/Old_Number_Theory/EulerFermat.thy
src/HOL/UNITY/Simple/Deadlock.thy
src/HOL/UNITY/Simple/Reach.thy
src/HOL/UNITY/Simple/Reachability.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Word.thy
src/HOL/ex/CTL.thy
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Dec 28 15:08:12 2011 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
     2.2 +++ b/src/HOL/Algebra/Lattice.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
     3.2 +++ b/src/HOL/Auth/Guard/Analz.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
     4.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
     5.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
     6.2 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Dec 28 20:03:13 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.19 -apply (simp_all add: I)
    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 15:08:12 2011 +0100
     7.2 +++ b/src/HOL/Inductive.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
     8.2 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
     9.2 +++ b/src/HOL/Library/Zorn.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
    10.2 +++ b/src/HOL/NSA/Filter.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
    11.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
    12.2 +++ b/src/HOL/Nominal/Examples/Class2.thy	Wed Dec 28 20:03:13 2011 +0100
    12.3 @@ -3245,7 +3245,7 @@
    12.4    { case 1 show ?case 
    12.5        apply -
    12.6        apply(simp add: lfp_eqvt)
    12.7 -      apply(simp add: perm_fun_def [where 'a="ntrm set"])
    12.8 +      apply(simp add: perm_fun_def)
    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.14        apply(simp add: lfp_eqvt)
   12.15        apply(simp add: comp_def)
   12.16 -      apply(simp add: perm_fun_def [where 'a="ntrm set"])
   12.17 +      apply(simp add: perm_fun_def)
   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.29      apply(perm_simp add: ih1 ih2)
   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.60        apply(simp add: lfp_eqvt)
   12.61 -      apply(simp add: perm_fun_def [where 'a="ntrm set"])
   12.62 +      apply(simp add: perm_fun_def)
   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.68        apply(simp add: lfp_eqvt)
   12.69        apply(simp add: comp_def)
   12.70 -      apply(simp add: perm_fun_def [where 'a="ntrm set"])
   12.71 +      apply(simp add: perm_fun_def)
   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 15:08:12 2011 +0100
    13.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
    14.2 +++ b/src/HOL/UNITY/Simple/Deadlock.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
    15.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
    16.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
    17.2 +++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 28 20:03:13 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 15:08:12 2011 +0100
    18.2 +++ b/src/HOL/Word/Word.thy	Wed Dec 28 20:03:13 2011 +0100
    18.3 @@ -2407,7 +2407,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 15:08:12 2011 +0100
    19.2 +++ b/src/HOL/ex/CTL.thy	Wed Dec 28 20:03:13 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