equal
deleted
inserted
replaced
159 class finite_distrib_lattice_complete = |
159 class finite_distrib_lattice_complete = |
160 distrib_lattice + finite_lattice_complete |
160 distrib_lattice + finite_lattice_complete |
161 |
161 |
162 lemma finite_distrib_lattice_complete_sup_Inf: |
162 lemma finite_distrib_lattice_complete_sup_Inf: |
163 "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)" |
163 "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)" |
164 apply (rule finite_induct) |
164 using finite by (induct A rule: finite_induct) |
165 apply (metis finite_code) |
165 (simp_all add: sup_inf_distrib1) |
166 apply (metis INF_empty Inf_empty sup_top_right) |
|
167 apply (metis INF_insert Inf_insert sup_inf_distrib1) |
|
168 done |
|
169 |
166 |
170 lemma finite_distrib_lattice_complete_inf_Sup: |
167 lemma finite_distrib_lattice_complete_inf_Sup: |
171 "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)" |
168 "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)" |
172 apply (rule finite_induct) |
169 apply (rule finite_induct) |
173 apply (metis finite_code) |
170 apply (metis finite_code) |