src/HOL/Algebra/Lattice.thy
 changeset 15328 35951e6a7855 parent 14751 0d7850e27fed child 16325 a6431098a929
equal inserted replaced
15327:0230a10582d3 15328:35951e6a7855
`   318   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"`
`   318   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"`
`   319 proof (induct set: Finites)`
`   319 proof (induct set: Finites)`
`   320   case empty`
`   320   case empty`
`   321   then show ?case by simp`
`   321   then show ?case by simp`
`   322 next`
`   322 next`
`   323   case (insert A x)`
`   323   case (insert x A)`
`   324   show ?case`
`   324   show ?case`
`   325   proof (cases "A = {}")`
`   325   proof (cases "A = {}")`
`   326     case True`
`   326     case True`
`   327     with insert show ?thesis by (simp add: sup_of_singletonI)`
`   327     with insert show ?thesis by (simp add: sup_of_singletonI)`
`   328   next`
`   328   next`
`   348 lemma (in lattice) finite_sup_closed:`
`   348 lemma (in lattice) finite_sup_closed:`
`   349   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"`
`   349   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"`
`   350 proof (induct set: Finites)`
`   350 proof (induct set: Finites)`
`   351   case empty then show ?case by simp`
`   351   case empty then show ?case by simp`
`   352 next`
`   352 next`
`   353   case (insert A x) then show ?case`
`   353   case insert then show ?case`
`   354     by - (rule finite_sup_insertI, simp_all)`
`   354     by - (rule finite_sup_insertI, simp_all)`
`   355 qed`
`   355 qed`
`   356 `
`   356 `
`   357 lemma (in lattice) join_left:`
`   357 lemma (in lattice) join_left:`
`   358   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"`
`   358   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"`
`   544 lemma (in lattice) finite_inf_greatest:`
`   544 lemma (in lattice) finite_inf_greatest:`
`   545   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"`
`   545   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"`
`   546 proof (induct set: Finites)`
`   546 proof (induct set: Finites)`
`   547   case empty then show ?case by simp`
`   547   case empty then show ?case by simp`
`   548 next`
`   548 next`
`   549   case (insert A x)`
`   549   case (insert x A)`
`   550   show ?case`
`   550   show ?case`
`   551   proof (cases "A = {}")`
`   551   proof (cases "A = {}")`
`   552     case True`
`   552     case True`
`   553     with insert show ?thesis by (simp add: inf_of_singletonI)`
`   553     with insert show ?thesis by (simp add: inf_of_singletonI)`
`   554   next`
`   554   next`
`   575 lemma (in lattice) finite_inf_closed:`
`   575 lemma (in lattice) finite_inf_closed:`
`   576   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"`
`   576   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"`
`   577 proof (induct set: Finites)`
`   577 proof (induct set: Finites)`
`   578   case empty then show ?case by simp`
`   578   case empty then show ?case by simp`
`   579 next`
`   579 next`
`   580   case (insert A x) then show ?case`
`   580   case insert then show ?case`
`   581     by (rule_tac finite_inf_insertI) (simp_all)`
`   581     by (rule_tac finite_inf_insertI) (simp_all)`
`   582 qed`
`   582 qed`
`   583 `
`   583 `
`   584 lemma (in lattice) meet_left:`
`   584 lemma (in lattice) meet_left:`
`   585   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"`
`   585   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"`