equal
deleted
inserted
replaced
3 header {* Complete lattices, with special focus on sets *} |
3 header {* Complete lattices, with special focus on sets *} |
4 |
4 |
5 theory Complete_Lattice |
5 theory Complete_Lattice |
6 imports Set |
6 imports Set |
7 begin |
7 begin |
8 |
|
9 lemma ball_conj_distrib: |
|
10 "(\<forall>x\<in>A. P x \<and> Q x) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<and> (\<forall>x\<in>A. Q x))" |
|
11 by blast |
|
12 |
|
13 lemma bex_disj_distrib: |
|
14 "(\<exists>x\<in>A. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<or> (\<exists>x\<in>A. Q x))" |
|
15 by blast |
|
16 |
8 |
17 notation |
9 notation |
18 less_eq (infix "\<sqsubseteq>" 50) and |
10 less_eq (infix "\<sqsubseteq>" 50) and |
19 less (infix "\<sqsubset>" 50) and |
11 less (infix "\<sqsubset>" 50) and |
20 inf (infixl "\<sqinter>" 70) and |
12 inf (infixl "\<sqinter>" 70) and |