src/HOL/Library/Quotient_Set.thy
changeset 67399 eab6ce8368fa
parent 62954 c5d0fdc260fa
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
     1.5  
     1.6  lemma rel_vset_eq [id_simps]:
     1.7 -  "rel_vset op = = op ="
     1.8 +  "rel_vset (=) = (=)"
     1.9    by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff rel_vset_def)
    1.10  
    1.11  lemma rel_vset_equivp:
    1.12 @@ -49,55 +49,55 @@
    1.13  
    1.14  lemma collect_rsp[quot_respect]:
    1.15    assumes "Quotient3 R Abs Rep"
    1.16 -  shows "((R ===> op =) ===> rel_vset R) Collect Collect"
    1.17 +  shows "((R ===> (=)) ===> rel_vset R) Collect Collect"
    1.18    by (intro rel_funI) (simp add: rel_fun_def rel_vset_def)
    1.19  
    1.20  lemma collect_prs[quot_preserve]:
    1.21    assumes "Quotient3 R Abs Rep"
    1.22 -  shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
    1.23 +  shows "((Abs ---> id) ---> (-`) Rep) Collect = Collect"
    1.24    unfolding fun_eq_iff
    1.25    by (simp add: Quotient3_abs_rep[OF assms])
    1.26  
    1.27  lemma union_rsp[quot_respect]:
    1.28    assumes "Quotient3 R Abs Rep"
    1.29 -  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<union> op \<union>"
    1.30 +  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) (\<union>) (\<union>)"
    1.31    by (intro rel_funI) (simp add: rel_vset_def)
    1.32  
    1.33  lemma union_prs[quot_preserve]:
    1.34    assumes "Quotient3 R Abs Rep"
    1.35 -  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
    1.36 +  shows "((-`) Abs ---> (-`) Abs ---> (-`) Rep) (\<union>) = (\<union>)"
    1.37    unfolding fun_eq_iff
    1.38    by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
    1.39  
    1.40  lemma diff_rsp[quot_respect]:
    1.41    assumes "Quotient3 R Abs Rep"
    1.42 -  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op - op -"
    1.43 +  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) (-) (-)"
    1.44    by (intro rel_funI) (simp add: rel_vset_def)
    1.45  
    1.46  lemma diff_prs[quot_preserve]:
    1.47    assumes "Quotient3 R Abs Rep"
    1.48 -  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
    1.49 +  shows "((-`) Abs ---> (-`) Abs ---> (-`) Rep) (-) = (-)"
    1.50    unfolding fun_eq_iff
    1.51    by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
    1.52  
    1.53  lemma inter_rsp[quot_respect]:
    1.54    assumes "Quotient3 R Abs Rep"
    1.55 -  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<inter> op \<inter>"
    1.56 +  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) (\<inter>) (\<inter>)"
    1.57    by (intro rel_funI) (auto simp add: rel_vset_def)
    1.58  
    1.59  lemma inter_prs[quot_preserve]:
    1.60    assumes "Quotient3 R Abs Rep"
    1.61 -  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
    1.62 +  shows "((-`) Abs ---> (-`) Abs ---> (-`) Rep) (\<inter>) = (\<inter>)"
    1.63    unfolding fun_eq_iff
    1.64    by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
    1.65  
    1.66  lemma mem_prs[quot_preserve]:
    1.67    assumes "Quotient3 R Abs Rep"
    1.68 -  shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
    1.69 +  shows "(Rep ---> (-`) Abs ---> id) (\<in>) = (\<in>)"
    1.70    by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
    1.71  
    1.72  lemma mem_rsp[quot_respect]:
    1.73 -  shows "(R ===> rel_vset R ===> op =) op \<in> op \<in>"
    1.74 +  shows "(R ===> rel_vset R ===> (=)) (\<in>) (\<in>)"
    1.75    by (intro rel_funI) (simp add: rel_vset_def)
    1.76  
    1.77  end