src/HOL/Algebra/Lattice.thy
changeset 15328 35951e6a7855
parent 14751 0d7850e27fed
child 16325 a6431098a929
equal deleted 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"