equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Quotient_Set.thy |
1 (* Title: HOL/Library/Quotient_Set.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 section {* Quotient infrastructure for the set type *} |
5 section \<open>Quotient infrastructure for the set type\<close> |
6 |
6 |
7 theory Quotient_Set |
7 theory Quotient_Set |
8 imports Main Quotient_Syntax |
8 imports Main Quotient_Syntax |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Contravariant set map (vimage) and set relator, rules for the Quotient package *} |
11 subsection \<open>Contravariant set map (vimage) and set relator, rules for the Quotient package\<close> |
12 |
12 |
13 definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys" |
13 definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys" |
14 |
14 |
15 lemma rel_vset_eq [id_simps]: |
15 lemma rel_vset_eq [id_simps]: |
16 "rel_vset op = = op =" |
16 "rel_vset op = = op =" |