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"