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
```