# HG changeset patch # User blanchet # Date 1394713093 -3600 # Node ID 3d11892ea537e42c33d7c19ac79fa5a7eac53553 # Parent 75c154e9f65064ed53d1c533f25fee96f7d2d910 killed a few 'metis' calls diff -r 75c154e9f650 -r 3d11892ea537 src/HOL/List.thy --- a/src/HOL/List.thy Thu Mar 13 13:18:13 2014 +0100 +++ b/src/HOL/List.thy Thu Mar 13 13:18:13 2014 +0100 @@ -1299,7 +1299,7 @@ case (snoc a xs) show ?case proof cases - assume "x = a" thus ?case using snoc by (metis set_simps(1) emptyE) + assume "x = a" thus ?case using snoc by (auto intro!: exI) next assume "x \ a" thus ?case using snoc by fastforce qed @@ -1332,7 +1332,8 @@ show ?case proof cases assume "P x" - thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) + hence "x # xs = [] @ x # xs \ P x \ (\y\set []. \ P y)" by simp + thus ?thesis by fast next assume "\ P x" hence "\x\set xs. P x" using Cons(2) by simp @@ -1359,7 +1360,7 @@ case (snoc x xs) show ?case proof cases - assume "P x" thus ?thesis by (metis emptyE set_empty) + assume "P x" thus ?thesis by (auto intro!: exI) next assume "\ P x" hence "\x\set xs. P x" using snoc(2) by simp @@ -1375,7 +1376,8 @@ lemma split_list_last_prop_iff: "(\x \ set xs. P x) \ (\ys x zs. xs = ys@x#zs \ P x \ (\z \ set zs. \ P z))" -by (metis split_list_last_prop [where P=P] in_set_conv_decomp) + by rule (erule split_list_last_prop, auto) + lemma finite_list: "finite A ==> EX xs. set xs = A" by (erule finite_induct) (auto simp add: set_simps(2) [symmetric] simp del: set_simps(2)) @@ -1773,7 +1775,7 @@ done lemma list_update_nonempty[simp]: "xs[k:=x] = [] \ xs=[]" -by(metis length_0_conv length_list_update) +by (simp only: length_0_conv[symmetric] length_list_update) lemma list_update_same_conv: "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)" @@ -1936,7 +1938,7 @@ lemma snoc_eq_iff_butlast: "xs @ [x] = ys \ (ys \ [] & butlast ys = xs & last ys = x)" -by (metis append_butlast_last_id append_is_Nil_conv butlast_snoc last_snoc not_Cons_self) +by fastforce subsubsection {* @{const take} and @{const drop} *} @@ -2121,8 +2123,7 @@ "m >= n \ set(drop m xs) <= set(drop n xs)" apply(induct xs arbitrary: m n) apply(auto simp:drop_Cons split:nat.split) -apply (metis set_drop_subset subset_iff) -done +by (metis set_drop_subset subset_iff) lemma in_set_takeD: "x : set(take n xs) \ x : set xs" using set_take_subset by fast @@ -3250,15 +3251,9 @@ apply (case_tac j) apply (clarsimp simp add: set_conv_nth, simp) apply (rule conjI) -(*TOO SLOW -apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc) -*) apply (clarsimp simp add: set_conv_nth) apply (erule_tac x = 0 in allE, simp) apply (erule_tac x = "Suc i" in allE, simp, clarsimp) -(*TOO SLOW -apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc) -*) apply (erule_tac x = "Suc i" in allE, simp) apply (erule_tac x = "Suc j" in allE, simp) done @@ -3403,8 +3398,7 @@ lemma distinct_length_2_or_more: "distinct (a # b # xs) \ (a \ b \ distinct (a # xs) \ distinct (b # xs))" -by (metis distinct.simps(2) list.sel(1) hd_in_set list.simps(2) set_ConsD set_rev_mp - set_subset_Cons) +by force lemma remdups_adj_Cons: "remdups_adj (x # xs) = (case remdups_adj xs of [] \ [x] | y # xs \ if x = y then y # xs else x # y # xs)" @@ -3636,8 +3630,8 @@ case Nil thus ?case by simp next case (Cons x xs) thus ?case - by(auto simp: nth_Cons' split: if_splits) - (metis One_nat_def diff_Suc_1 less_Suc_eq_0_disj) + apply(auto simp: nth_Cons' split: if_splits) + using diff_Suc_1[unfolded One_nat_def] less_Suc_eq_0_disj by fastforce qed lemma find_cong[fundef_cong]: @@ -3683,8 +3677,8 @@ (case List.extract P xs of None \ None | Some (ys, y, zs) \ Some (x#ys, y, zs)))" -by(auto simp add: extract_def split: list.splits) - (metis comp_def dropWhile_eq_Nil_conv list.distinct(1)) +by(auto simp add: extract_def comp_def split: list.splits) + (metis dropWhile_eq_Nil_conv list.distinct(1)) subsubsection {* @{const remove1} *} @@ -3792,7 +3786,7 @@ lemma map_removeAll_inj: "inj f \ map f (removeAll x xs) = removeAll (f x) (map f xs)" -by(metis map_removeAll_inj_on subset_inj_on subset_UNIV) +by (rule map_removeAll_inj_on, erule subset_inj_on, rule subset_UNIV) subsubsection {* @{const replicate} *} @@ -3962,7 +3956,7 @@ with * show ?thesis by blast qed then show ?case - using xs'_def ys'_def by metis + using xs'_def ys'_def by meson qed lemma comm_append_is_replicate: @@ -3974,7 +3968,7 @@ proof - obtain m n zs where "concat (replicate m zs) = xs" and "concat (replicate n zs) = ys" - using assms by (metis comm_append_are_replicate) + using comm_append_are_replicate[of xs ys, OF assms] by blast then have "m + n > 1" and "concat (replicate (m+n) zs) = xs @ ys" using `xs \ []` and `ys \ []` by (auto simp: replicate_add) @@ -4511,10 +4505,11 @@ qed lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)" -apply(rule notI) -apply(drule finite_maxlen) -apply (metis UNIV_I length_replicate less_not_refl) -done +apply (rule notI) +apply (drule finite_maxlen) +apply clarsimp +apply (erule_tac x = "replicate n undefined" in allE) +by simp subsection {* Sorting *} @@ -4726,7 +4721,7 @@ proof(induct rule:list_induct2[OF 1]) case 1 show ?case by simp next - case 2 thus ?case by (simp add:sorted_Cons) + case 2 thus ?case by (simp add: sorted_Cons) (metis Diff_insert_absorb antisym insertE insert_iff) qed qed @@ -5660,10 +5655,10 @@ by (simp add: listrel1_def Cons_eq_append_conv) (blast) lemma listrel1I1: "(x,y) \ r \ (x # xs, y # xs) \ listrel1 r" -by (metis Cons_listrel1_Cons) +by fast lemma listrel1I2: "(xs, ys) \ listrel1 r \ (x # xs, x # ys) \ listrel1 r" -by (metis Cons_listrel1_Cons) +by fast lemma append_listrel1I: "(xs, ys) \ listrel1 r \ us = vs \ xs = ys \ (us, vs) \ listrel1 r @@ -5757,8 +5752,8 @@ done lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r" -by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff) - +by (auto simp: wf_acc_iff + intro: lists_accD lists_accI[THEN Cons_in_lists_iff[THEN iffD1, THEN conjunct1]]) subsubsection {* Lifting Relations to Lists: all elements *} @@ -5901,7 +5896,7 @@ case base show ?case by(auto simp add: listrel_iff_zip set_zip) next case (step ys zs) - thus ?case by (metis listrel_reflcl_if_listrel1 listrel_rtrancl_trans) + thus ?case by (metis listrel_reflcl_if_listrel1 listrel_rtrancl_trans) qed qed qed diff -r 75c154e9f650 -r 3d11892ea537 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Thu Mar 13 13:18:13 2014 +0100 +++ b/src/HOL/Relation.thy Thu Mar 13 13:18:13 2014 +0100 @@ -1135,7 +1135,4 @@ (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold cong: if_cong) - - end - diff -r 75c154e9f650 -r 3d11892ea537 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Thu Mar 13 13:18:13 2014 +0100 +++ b/src/HOL/Transfer.thy Thu Mar 13 13:18:13 2014 +0100 @@ -156,10 +156,10 @@ by(simp add: bi_unique_def) lemma right_uniqueI: "(\x y z. \ A x y; A x z \ \ y = z) \ right_unique A" -unfolding right_unique_def by blast +unfolding right_unique_def by fast lemma right_uniqueD: "\ right_unique A; A x y; A x z \ \ y = z" -unfolding right_unique_def by blast +unfolding right_unique_def by fast lemma right_total_alt_def: "right_total R \ ((R ===> op \) ===> op \) All All" @@ -204,18 +204,18 @@ by auto lemma bi_total_OO: "\bi_total A; bi_total B\ \ bi_total (A OO B)" - unfolding bi_total_def OO_def by metis + unfolding bi_total_def OO_def by fast lemma bi_unique_OO: "\bi_unique A; bi_unique B\ \ bi_unique (A OO B)" - unfolding bi_unique_def OO_def by metis + unfolding bi_unique_def OO_def by blast lemma right_total_OO: "\right_total A; right_total B\ \ right_total (A OO B)" - unfolding right_total_def OO_def by metis + unfolding right_total_def OO_def by fast lemma right_unique_OO: "\right_unique A; right_unique B\ \ right_unique (A OO B)" - unfolding right_unique_def OO_def by metis + unfolding right_unique_def OO_def by fast subsection {* Properties of relators *} @@ -278,7 +278,7 @@ lemma bi_unique_fun [transfer_rule]: "\bi_total A; bi_unique B\ \ bi_unique (A ===> B)" unfolding bi_total_def bi_unique_def rel_fun_def fun_eq_iff - by (safe, metis, fast) + by fast+ subsection {* Transfer rules *} @@ -289,7 +289,7 @@ (transfer_bforall (Domainp A)) transfer_forall" using assms unfolding right_total_def unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff - by metis + by fast text {* Transfer rules using implication instead of equality on booleans. *} @@ -300,7 +300,7 @@ "bi_total A \ ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall" "bi_total A \ ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall" unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def - by metis+ + by fast+ lemma transfer_implies_transfer [transfer_rule]: "(op = ===> op = ===> op = ) transfer_implies transfer_implies" @@ -327,13 +327,13 @@ assumes "right_total A" shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex" using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def] -by blast +by fast lemma right_total_All_transfer[transfer_rule]: assumes "right_total A" shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All" using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def] -by blast +by fast lemma All_transfer [transfer_rule]: assumes "bi_total A"