src/HOL/Quotient.thy
changeset 55945 e96383acecf9
parent 54867 c21a2465cac1
child 56073 29e308b56d23
     1.1 --- a/src/HOL/Quotient.thy	Thu Mar 06 15:29:18 2014 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Thu Mar 06 15:40:33 2014 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4      using q1 q2 by (simp add: Quotient3_def fun_eq_iff)
     1.5    moreover
     1.6    have "\<And>a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
     1.7 -    by (rule fun_relI)
     1.8 +    by (rule rel_funI)
     1.9        (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
    1.10          simp (no_asm) add: Quotient3_def, simp)
    1.11    
    1.12 @@ -157,17 +157,17 @@
    1.13          (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
    1.14    proof -
    1.15      
    1.16 -    have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding fun_rel_def
    1.17 +    have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding rel_fun_def
    1.18        using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
    1.19        by (metis (full_types) part_equivp_def)
    1.20 -    moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding fun_rel_def
    1.21 +    moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding rel_fun_def
    1.22        using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
    1.23        by (metis (full_types) part_equivp_def)
    1.24      moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r  = (rep1 ---> abs2) s"
    1.25 -      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
    1.26 +      apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
    1.27      moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
    1.28          (rep1 ---> abs2) r  = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s"
    1.29 -      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 
    1.30 +      apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 
    1.31      by (metis map_fun_apply)
    1.32    
    1.33      ultimately show ?thesis by blast
    1.34 @@ -204,7 +204,7 @@
    1.35    assumes q: "Quotient3 R1 Abs1 Rep1"
    1.36    and     a: "(R1 ===> R2) f g" "R1 x y"
    1.37    shows "R2 (f x) (g y)"
    1.38 -  using a by (auto elim: fun_relE)
    1.39 +  using a by (auto elim: rel_funE)
    1.40  
    1.41  lemma apply_rspQ3'':
    1.42    assumes "Quotient3 R Abs Rep"
    1.43 @@ -261,7 +261,7 @@
    1.44    apply(rule iffI)
    1.45    apply(rule allI)
    1.46    apply(drule_tac x="\<lambda>y. f x" in bspec)
    1.47 -  apply(simp add: in_respects fun_rel_def)
    1.48 +  apply(simp add: in_respects rel_fun_def)
    1.49    apply(rule impI)
    1.50    using a equivp_reflp_symp_transp[of "R2"]
    1.51    apply (auto elim: equivpE reflpE)
    1.52 @@ -273,7 +273,7 @@
    1.53    apply(auto)
    1.54    apply(rule_tac x="\<lambda>y. f x" in bexI)
    1.55    apply(simp)
    1.56 -  apply(simp add: Respects_def in_respects fun_rel_def)
    1.57 +  apply(simp add: Respects_def in_respects rel_fun_def)
    1.58    apply(rule impI)
    1.59    using a equivp_reflp_symp_transp[of "R2"]
    1.60    apply (auto elim: equivpE reflpE)
    1.61 @@ -326,10 +326,10 @@
    1.62    assumes q: "Quotient3 R1 Abs1 Rep1"
    1.63    and     a: "(R1 ===> R2) f g"
    1.64    shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
    1.65 -  apply (auto simp add: Babs_def in_respects fun_rel_def)
    1.66 +  apply (auto simp add: Babs_def in_respects rel_fun_def)
    1.67    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
    1.68 -  using a apply (simp add: Babs_def fun_rel_def)
    1.69 -  apply (simp add: in_respects fun_rel_def)
    1.70 +  using a apply (simp add: Babs_def rel_fun_def)
    1.71 +  apply (simp add: in_respects rel_fun_def)
    1.72    using Quotient3_rel[OF q]
    1.73    by metis
    1.74  
    1.75 @@ -349,7 +349,7 @@
    1.76    shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
    1.77    apply(rule iffI)
    1.78    apply(simp_all only: babs_rsp[OF q])
    1.79 -  apply(auto simp add: Babs_def fun_rel_def)
    1.80 +  apply(auto simp add: Babs_def rel_fun_def)
    1.81    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
    1.82    apply(metis Babs_def)
    1.83    apply (simp add: in_respects)
    1.84 @@ -367,17 +367,17 @@
    1.85  lemma ball_rsp:
    1.86    assumes a: "(R ===> (op =)) f g"
    1.87    shows "Ball (Respects R) f = Ball (Respects R) g"
    1.88 -  using a by (auto simp add: Ball_def in_respects elim: fun_relE)
    1.89 +  using a by (auto simp add: Ball_def in_respects elim: rel_funE)
    1.90  
    1.91  lemma bex_rsp:
    1.92    assumes a: "(R ===> (op =)) f g"
    1.93    shows "(Bex (Respects R) f = Bex (Respects R) g)"
    1.94 -  using a by (auto simp add: Bex_def in_respects elim: fun_relE)
    1.95 +  using a by (auto simp add: Bex_def in_respects elim: rel_funE)
    1.96  
    1.97  lemma bex1_rsp:
    1.98    assumes a: "(R ===> (op =)) f g"
    1.99    shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
   1.100 -  using a by (auto elim: fun_relE simp add: Ex1_def in_respects) 
   1.101 +  using a by (auto elim: rel_funE simp add: Ex1_def in_respects) 
   1.102  
   1.103  (* 2 lemmas needed for cleaning of quantifiers *)
   1.104  lemma all_prs:
   1.105 @@ -440,7 +440,7 @@
   1.106  lemma bex1_rel_rsp:
   1.107    assumes a: "Quotient3 R absf repf"
   1.108    shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
   1.109 -  apply (simp add: fun_rel_def)
   1.110 +  apply (simp add: rel_fun_def)
   1.111    apply clarify
   1.112    apply rule
   1.113    apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
   1.114 @@ -519,7 +519,7 @@
   1.115  lemma quot_rel_rsp:
   1.116    assumes a: "Quotient3 R Abs Rep"
   1.117    shows "(R ===> R ===> op =) R R"
   1.118 -  apply(rule fun_relI)+
   1.119 +  apply(rule rel_funI)+
   1.120    apply(rule equals_rsp[OF a])
   1.121    apply(assumption)+
   1.122    done
   1.123 @@ -536,7 +536,7 @@
   1.124  lemma o_rsp:
   1.125    "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
   1.126    "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
   1.127 -  by (force elim: fun_relE)+
   1.128 +  by (force elim: rel_funE)+
   1.129  
   1.130  lemma cond_prs:
   1.131    assumes a: "Quotient3 R absf repf"
   1.132 @@ -563,7 +563,7 @@
   1.133  
   1.134  lemma let_rsp:
   1.135    shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
   1.136 -  by (force elim: fun_relE)
   1.137 +  by (force elim: rel_funE)
   1.138  
   1.139  lemma id_rsp:
   1.140    shows "(R ===> R) id id"
   1.141 @@ -759,7 +759,7 @@
   1.142  ML_file "Tools/Quotient/quotient_info.ML"
   1.143  setup Quotient_Info.setup
   1.144  
   1.145 -declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
   1.146 +declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
   1.147  
   1.148  lemmas [quot_thm] = fun_quotient3
   1.149  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp