src/HOL/Quotient.thy
 changeset 44921 58eef4843641 parent 44553 4d39b032a021 child 45680 a61510361b89
```     1.1 --- a/src/HOL/Quotient.thy	Tue Sep 13 08:21:51 2011 -0700
1.2 +++ b/src/HOL/Quotient.thy	Tue Sep 13 17:07:33 2011 -0700
1.3 @@ -85,7 +85,7 @@
1.4    shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
1.5    unfolding set_rel_def
1.6    using equivp_reflp[OF e]
1.7 -  by auto (metis equivp_symp[OF e])+
1.8 +  by auto (metis, metis equivp_symp[OF e])
1.9
1.10  subsection {* Quotient Predicate *}
1.11
1.12 @@ -269,12 +269,12 @@
1.13  lemma ball_reg_right:
1.14    assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
1.15    shows "All P \<longrightarrow> Ball R Q"
1.16 -  using a by (metis Collect_mem_eq)
1.17 +  using a by fast
1.18
1.19  lemma bex_reg_left:
1.20    assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
1.21    shows "Bex R Q \<longrightarrow> Ex P"
1.22 -  using a by (metis Collect_mem_eq)
1.23 +  using a by fast
1.24
1.25  lemma ball_reg_left:
1.26    assumes a: "equivp R"
1.27 @@ -317,25 +317,25 @@
1.28    assumes a: "!x :: 'a. (P x --> Q x)"
1.29    and     b: "All P"
1.30    shows "All Q"
1.31 -  using a b by (metis)
1.32 +  using a b by fast
1.33
1.34  lemma ex_reg:
1.35    assumes a: "!x :: 'a. (P x --> Q x)"
1.36    and     b: "Ex P"
1.37    shows "Ex Q"
1.38 -  using a b by metis
1.39 +  using a b by fast
1.40
1.41  lemma ball_reg:
1.42    assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
1.43    and     b: "Ball R P"
1.44    shows "Ball R Q"
1.45 -  using a b by (metis Collect_mem_eq)
1.46 +  using a b by fast
1.47
1.48  lemma bex_reg:
1.49    assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
1.50    and     b: "Bex R P"
1.51    shows "Bex R Q"
1.52 -  using a b by (metis Collect_mem_eq)
1.53 +  using a b by fast
1.54
1.55
1.56  lemma ball_all_comm:
1.57 @@ -569,7 +569,7 @@
1.58  lemma o_rsp:
1.59    "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
1.60    "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
1.61 -  by (auto intro!: fun_relI elim: fun_relE)
1.62 +  by (force elim: fun_relE)+
1.63
1.64  lemma cond_prs:
1.65    assumes a: "Quotient R absf repf"
1.66 @@ -585,7 +585,7 @@
1.67  lemma if_rsp:
1.68    assumes q: "Quotient R Abs Rep"
1.69    shows "(op = ===> R ===> R ===> R) If If"
1.70 -  by (auto intro!: fun_relI)
1.71 +  by force
1.72
1.73  lemma let_prs:
1.74    assumes q1: "Quotient R1 Abs1 Rep1"
1.75 @@ -596,11 +596,11 @@
1.76
1.77  lemma let_rsp:
1.78    shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
1.79 -  by (auto intro!: fun_relI elim: fun_relE)
1.80 +  by (force elim: fun_relE)
1.81
1.82  lemma id_rsp:
1.83    shows "(R ===> R) id id"
1.84 -  by (auto intro: fun_relI)
1.85 +  by auto
1.86
1.87  lemma id_prs:
1.88    assumes a: "Quotient R Abs Rep"
```