equal
deleted
inserted
replaced
403 apply (fact dual_complete_lattice) |
403 apply (fact dual_complete_lattice) |
404 apply (rule class.complete_distrib_lattice_axioms.intro) |
404 apply (rule class.complete_distrib_lattice_axioms.intro) |
405 apply (simp_all add: inf_Sup sup_Inf)*) |
405 apply (simp_all add: inf_Sup sup_Inf)*) |
406 |
406 |
407 subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice} |
407 subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice} |
408 and proof @{text inf_Sup} and @{text sup_Inf} from that? *} |
408 and prove @{text inf_Sup} and @{text sup_Inf} from that? *} |
409 fix a b c |
409 fix a b c |
410 from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" . |
410 from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" . |
411 then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary) |
411 then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary) |
412 qed |
412 qed |
413 |
413 |