killed a few 'metis' calls
authorblanchet
Thu Mar 13 13:18:13 2014 +0100 (2014-03-13)
changeset 560853d11892ea537
parent 56084 75c154e9f650
child 56086 fb160b829a88
killed a few 'metis' calls
src/HOL/List.thy
src/HOL/Relation.thy
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/List.thy	Thu Mar 13 13:18:13 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Mar 13 13:18:13 2014 +0100
     1.3 @@ -1299,7 +1299,7 @@
     1.4    case (snoc a xs)
     1.5    show ?case
     1.6    proof cases
     1.7 -    assume "x = a" thus ?case using snoc by (metis set_simps(1) emptyE)
     1.8 +    assume "x = a" thus ?case using snoc by (auto intro!: exI)
     1.9    next
    1.10      assume "x \<noteq> a" thus ?case using snoc by fastforce
    1.11    qed
    1.12 @@ -1332,7 +1332,8 @@
    1.13    show ?case
    1.14    proof cases
    1.15      assume "P x"
    1.16 -    thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
    1.17 +    hence "x # xs = [] @ x # xs \<and> P x \<and> (\<forall>y\<in>set []. \<not> P y)" by simp
    1.18 +    thus ?thesis by fast
    1.19    next
    1.20      assume "\<not> P x"
    1.21      hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
    1.22 @@ -1359,7 +1360,7 @@
    1.23    case (snoc x xs)
    1.24    show ?case
    1.25    proof cases
    1.26 -    assume "P x" thus ?thesis by (metis emptyE set_empty)
    1.27 +    assume "P x" thus ?thesis by (auto intro!: exI)
    1.28    next
    1.29      assume "\<not> P x"
    1.30      hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
    1.31 @@ -1375,7 +1376,8 @@
    1.32  lemma split_list_last_prop_iff:
    1.33    "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
    1.34     (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
    1.35 -by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
    1.36 +  by rule (erule split_list_last_prop, auto)
    1.37 +
    1.38  
    1.39  lemma finite_list: "finite A ==> EX xs. set xs = A"
    1.40    by (erule finite_induct) (auto simp add: set_simps(2) [symmetric] simp del: set_simps(2))
    1.41 @@ -1773,7 +1775,7 @@
    1.42  done
    1.43  
    1.44  lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
    1.45 -by(metis length_0_conv length_list_update)
    1.46 +by (simp only: length_0_conv[symmetric] length_list_update)
    1.47  
    1.48  lemma list_update_same_conv:
    1.49  "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
    1.50 @@ -1936,7 +1938,7 @@
    1.51  
    1.52  lemma snoc_eq_iff_butlast:
    1.53    "xs @ [x] = ys \<longleftrightarrow> (ys \<noteq> [] & butlast ys = xs & last ys = x)"
    1.54 -by (metis append_butlast_last_id append_is_Nil_conv butlast_snoc last_snoc not_Cons_self)
    1.55 +by fastforce
    1.56  
    1.57  
    1.58  subsubsection {* @{const take} and @{const drop} *}
    1.59 @@ -2121,8 +2123,7 @@
    1.60    "m >= n \<Longrightarrow> set(drop m xs) <= set(drop n xs)"
    1.61  apply(induct xs arbitrary: m n)
    1.62  apply(auto simp:drop_Cons split:nat.split)
    1.63 -apply (metis set_drop_subset subset_iff)
    1.64 -done
    1.65 +by (metis set_drop_subset subset_iff)
    1.66  
    1.67  lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
    1.68  using set_take_subset by fast
    1.69 @@ -3250,15 +3251,9 @@
    1.70   apply (case_tac j)
    1.71  apply (clarsimp simp add: set_conv_nth, simp)
    1.72  apply (rule conjI)
    1.73 -(*TOO SLOW
    1.74 -apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
    1.75 -*)
    1.76   apply (clarsimp simp add: set_conv_nth)
    1.77   apply (erule_tac x = 0 in allE, simp)
    1.78   apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
    1.79 -(*TOO SLOW
    1.80 -apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
    1.81 -*)
    1.82  apply (erule_tac x = "Suc i" in allE, simp)
    1.83  apply (erule_tac x = "Suc j" in allE, simp)
    1.84  done
    1.85 @@ -3403,8 +3398,7 @@
    1.86  
    1.87  lemma distinct_length_2_or_more:
    1.88  "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
    1.89 -by (metis distinct.simps(2) list.sel(1) hd_in_set list.simps(2) set_ConsD set_rev_mp
    1.90 -      set_subset_Cons)
    1.91 +by force
    1.92  
    1.93  lemma remdups_adj_Cons: "remdups_adj (x # xs) =
    1.94    (case remdups_adj xs of [] \<Rightarrow> [x] | y # xs \<Rightarrow> if x = y then y # xs else x # y # xs)"
    1.95 @@ -3636,8 +3630,8 @@
    1.96    case Nil thus ?case by simp
    1.97  next
    1.98    case (Cons x xs) thus ?case
    1.99 -    by(auto simp: nth_Cons' split: if_splits)
   1.100 -      (metis One_nat_def diff_Suc_1 less_Suc_eq_0_disj)
   1.101 +    apply(auto simp: nth_Cons' split: if_splits)
   1.102 +    using diff_Suc_1[unfolded One_nat_def] less_Suc_eq_0_disj by fastforce
   1.103  qed
   1.104  
   1.105  lemma find_cong[fundef_cong]:
   1.106 @@ -3683,8 +3677,8 @@
   1.107     (case List.extract P xs of
   1.108        None \<Rightarrow> None |
   1.109        Some (ys, y, zs) \<Rightarrow> Some (x#ys, y, zs)))"
   1.110 -by(auto simp add: extract_def split: list.splits)
   1.111 -  (metis comp_def dropWhile_eq_Nil_conv list.distinct(1))
   1.112 +by(auto simp add: extract_def comp_def split: list.splits)
   1.113 +  (metis dropWhile_eq_Nil_conv list.distinct(1))
   1.114  
   1.115  
   1.116  subsubsection {* @{const remove1} *}
   1.117 @@ -3792,7 +3786,7 @@
   1.118  
   1.119  lemma map_removeAll_inj: "inj f \<Longrightarrow>
   1.120    map f (removeAll x xs) = removeAll (f x) (map f xs)"
   1.121 -by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
   1.122 +by (rule map_removeAll_inj_on, erule subset_inj_on, rule subset_UNIV)
   1.123  
   1.124  
   1.125  subsubsection {* @{const replicate} *}
   1.126 @@ -3962,7 +3956,7 @@
   1.127      with * show ?thesis by blast
   1.128    qed
   1.129    then show ?case
   1.130 -    using xs'_def ys'_def by metis
   1.131 +    using xs'_def ys'_def by meson
   1.132  qed
   1.133  
   1.134  lemma comm_append_is_replicate:
   1.135 @@ -3974,7 +3968,7 @@
   1.136  proof -
   1.137    obtain m n zs where "concat (replicate m zs) = xs"
   1.138      and "concat (replicate n zs) = ys"
   1.139 -    using assms by (metis comm_append_are_replicate)
   1.140 +    using comm_append_are_replicate[of xs ys, OF assms] by blast
   1.141    then have "m + n > 1" and "concat (replicate (m+n) zs) = xs @ ys"
   1.142      using `xs \<noteq> []` and `ys \<noteq> []`
   1.143      by (auto simp: replicate_add)
   1.144 @@ -4511,10 +4505,11 @@
   1.145  qed
   1.146  
   1.147  lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
   1.148 -apply(rule notI)
   1.149 -apply(drule finite_maxlen)
   1.150 -apply (metis UNIV_I length_replicate less_not_refl)
   1.151 -done
   1.152 +apply (rule notI)
   1.153 +apply (drule finite_maxlen)
   1.154 +apply clarsimp
   1.155 +apply (erule_tac x = "replicate n undefined" in allE)
   1.156 +by simp
   1.157  
   1.158  
   1.159  subsection {* Sorting *}
   1.160 @@ -4726,7 +4721,7 @@
   1.161    proof(induct rule:list_induct2[OF 1])
   1.162      case 1 show ?case by simp
   1.163    next
   1.164 -    case 2 thus ?case by (simp add:sorted_Cons)
   1.165 +    case 2 thus ?case by (simp add: sorted_Cons)
   1.166         (metis Diff_insert_absorb antisym insertE insert_iff)
   1.167    qed
   1.168  qed
   1.169 @@ -5660,10 +5655,10 @@
   1.170  by (simp add: listrel1_def Cons_eq_append_conv) (blast)
   1.171  
   1.172  lemma listrel1I1: "(x,y) \<in> r \<Longrightarrow> (x # xs, y # xs) \<in> listrel1 r"
   1.173 -by (metis Cons_listrel1_Cons)
   1.174 +by fast
   1.175  
   1.176  lemma listrel1I2: "(xs, ys) \<in> listrel1 r \<Longrightarrow> (x # xs, x # ys) \<in> listrel1 r"
   1.177 -by (metis Cons_listrel1_Cons)
   1.178 +by fast
   1.179  
   1.180  lemma append_listrel1I:
   1.181    "(xs, ys) \<in> listrel1 r \<and> us = vs \<or> xs = ys \<and> (us, vs) \<in> listrel1 r
   1.182 @@ -5757,8 +5752,8 @@
   1.183  done
   1.184  
   1.185  lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
   1.186 -by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff)
   1.187 -
   1.188 +by (auto simp: wf_acc_iff
   1.189 +      intro: lists_accD lists_accI[THEN Cons_in_lists_iff[THEN iffD1, THEN conjunct1]])
   1.190  
   1.191  subsubsection {* Lifting Relations to Lists: all elements *}
   1.192  
   1.193 @@ -5901,7 +5896,7 @@
   1.194        case base show ?case by(auto simp add: listrel_iff_zip set_zip)
   1.195      next
   1.196        case (step ys zs)
   1.197 -      thus ?case  by (metis listrel_reflcl_if_listrel1 listrel_rtrancl_trans)
   1.198 +      thus ?case by (metis listrel_reflcl_if_listrel1 listrel_rtrancl_trans)
   1.199      qed
   1.200    qed
   1.201  qed
     2.1 --- a/src/HOL/Relation.thy	Thu Mar 13 13:18:13 2014 +0100
     2.2 +++ b/src/HOL/Relation.thy	Thu Mar 13 13:18:13 2014 +0100
     2.3 @@ -1135,7 +1135,4 @@
     2.4      (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
     2.5        cong: if_cong)
     2.6  
     2.7 -
     2.8 -
     2.9  end
    2.10 -
     3.1 --- a/src/HOL/Transfer.thy	Thu Mar 13 13:18:13 2014 +0100
     3.2 +++ b/src/HOL/Transfer.thy	Thu Mar 13 13:18:13 2014 +0100
     3.3 @@ -156,10 +156,10 @@
     3.4  by(simp add: bi_unique_def)
     3.5  
     3.6  lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
     3.7 -unfolding right_unique_def by blast
     3.8 +unfolding right_unique_def by fast
     3.9  
    3.10  lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
    3.11 -unfolding right_unique_def by blast
    3.12 +unfolding right_unique_def by fast
    3.13  
    3.14  lemma right_total_alt_def:
    3.15    "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
    3.16 @@ -204,18 +204,18 @@
    3.17    by auto
    3.18  
    3.19  lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)"
    3.20 -  unfolding bi_total_def OO_def by metis
    3.21 +  unfolding bi_total_def OO_def by fast
    3.22  
    3.23  lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)"
    3.24 -  unfolding bi_unique_def OO_def by metis
    3.25 +  unfolding bi_unique_def OO_def by blast
    3.26  
    3.27  lemma right_total_OO:
    3.28    "\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)"
    3.29 -  unfolding right_total_def OO_def by metis
    3.30 +  unfolding right_total_def OO_def by fast
    3.31  
    3.32  lemma right_unique_OO:
    3.33    "\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)"
    3.34 -  unfolding right_unique_def OO_def by metis
    3.35 +  unfolding right_unique_def OO_def by fast
    3.36  
    3.37  
    3.38  subsection {* Properties of relators *}
    3.39 @@ -278,7 +278,7 @@
    3.40  lemma bi_unique_fun [transfer_rule]:
    3.41    "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
    3.42    unfolding bi_total_def bi_unique_def rel_fun_def fun_eq_iff
    3.43 -  by (safe, metis, fast)
    3.44 +  by fast+
    3.45  
    3.46  
    3.47  subsection {* Transfer rules *}
    3.48 @@ -289,7 +289,7 @@
    3.49      (transfer_bforall (Domainp A)) transfer_forall"
    3.50    using assms unfolding right_total_def
    3.51    unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
    3.52 -  by metis
    3.53 +  by fast
    3.54  
    3.55  text {* Transfer rules using implication instead of equality on booleans. *}
    3.56  
    3.57 @@ -300,7 +300,7 @@
    3.58    "bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall"
    3.59    "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
    3.60    unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def
    3.61 -  by metis+
    3.62 +  by fast+
    3.63  
    3.64  lemma transfer_implies_transfer [transfer_rule]:
    3.65    "(op =        ===> op =        ===> op =       ) transfer_implies transfer_implies"
    3.66 @@ -327,13 +327,13 @@
    3.67    assumes "right_total A"
    3.68    shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
    3.69  using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def]
    3.70 -by blast
    3.71 +by fast
    3.72  
    3.73  lemma right_total_All_transfer[transfer_rule]:
    3.74    assumes "right_total A"
    3.75    shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
    3.76  using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
    3.77 -by blast
    3.78 +by fast
    3.79  
    3.80  lemma All_transfer [transfer_rule]:
    3.81    assumes "bi_total A"