src/HOL/Lattices.thy
changeset 25510 38c15efe603b
parent 25482 4ed49eccb1eb
child 26014 00c2c3525bef
equal deleted inserted replaced
25509:e537c91b043d 25510:38c15efe603b
   477 end
   477 end
   478 
   478 
   479 
   479 
   480 subsection {* Bool as lattice *}
   480 subsection {* Bool as lattice *}
   481 
   481 
   482 instance bool :: distrib_lattice
   482 instantiation bool :: distrib_lattice
   483   inf_bool_eq: "P \<sqinter> Q \<equiv> P \<and> Q"
   483 begin
   484   sup_bool_eq: "P \<squnion> Q \<equiv> P \<or> Q"
   484 
       
   485 definition
       
   486   inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
       
   487 
       
   488 definition
       
   489   sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
       
   490 
       
   491 instance
   485   by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
   492   by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
   486 
   493 
   487 instance bool :: complete_lattice
   494 end
   488   Inf_bool_def: "\<Sqinter>A \<equiv> \<forall>x\<in>A. x"
   495 
   489   Sup_bool_def: "\<Squnion>A \<equiv> \<exists>x\<in>A. x"
   496 instantiation bool :: complete_lattice
       
   497 begin
       
   498 
       
   499 definition
       
   500   Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
       
   501 
       
   502 definition
       
   503   Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
       
   504 
       
   505 instance
   490   by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
   506   by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
       
   507 
       
   508 end
   491 
   509 
   492 lemma Inf_empty_bool [simp]:
   510 lemma Inf_empty_bool [simp]:
   493   "\<Sqinter>{}"
   511   "\<Sqinter>{}"
   494   unfolding Inf_bool_def by auto
   512   unfolding Inf_bool_def by auto
   495 
   513 
   504   by (iprover intro!: order_antisym le_boolI bot_least)
   522   by (iprover intro!: order_antisym le_boolI bot_least)
   505 
   523 
   506 
   524 
   507 subsection {* Set as lattice *}
   525 subsection {* Set as lattice *}
   508 
   526 
   509 instance set :: (type) distrib_lattice
   527 instantiation set :: (type) distrib_lattice
   510   inf_set_eq: "A \<sqinter> B \<equiv> A \<inter> B"
   528 begin
   511   sup_set_eq: "A \<squnion> B \<equiv> A \<union> B"
   529 
       
   530 definition
       
   531   inf_set_eq [code func del]: "A \<sqinter> B = A \<inter> B"
       
   532 
       
   533 definition
       
   534   sup_set_eq [code func del]: "A \<squnion> B = A \<union> B"
       
   535 
       
   536 instance
   512   by intro_classes (auto simp add: inf_set_eq sup_set_eq)
   537   by intro_classes (auto simp add: inf_set_eq sup_set_eq)
   513 
   538 
   514 lemmas [code func del] = inf_set_eq sup_set_eq
   539 end
   515 
   540 
   516 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   541 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   517   apply (fold inf_set_eq sup_set_eq)
   542   apply (fold inf_set_eq sup_set_eq)
   518   apply (erule mono_inf)
   543   apply (erule mono_inf)
   519   done
   544   done
   521 lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   546 lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   522   apply (fold inf_set_eq sup_set_eq)
   547   apply (fold inf_set_eq sup_set_eq)
   523   apply (erule mono_sup)
   548   apply (erule mono_sup)
   524   done
   549   done
   525 
   550 
   526 instance set :: (type) complete_lattice
   551 instantiation set :: (type) complete_lattice
   527   Inf_set_def: "\<Sqinter>S \<equiv> \<Inter>S"
   552 begin
   528   Sup_set_def: "\<Squnion>S \<equiv> \<Union>S"
   553 
       
   554 definition
       
   555   Inf_set_def [code func del]: "\<Sqinter>S \<equiv> \<Inter>S"
       
   556 
       
   557 definition
       
   558   Sup_set_def [code func del]: "\<Squnion>S \<equiv> \<Union>S"
       
   559 
       
   560 instance
   529   by intro_classes (auto simp add: Inf_set_def Sup_set_def)
   561   by intro_classes (auto simp add: Inf_set_def Sup_set_def)
   530 
   562 
   531 lemmas [code func del] = Inf_set_def Sup_set_def
   563 end
   532 
   564 
   533 lemma top_set_eq: "top = UNIV"
   565 lemma top_set_eq: "top = UNIV"
   534   by (iprover intro!: subset_antisym subset_UNIV top_greatest)
   566   by (iprover intro!: subset_antisym subset_UNIV top_greatest)
   535 
   567 
   536 lemma bot_set_eq: "bot = {}"
   568 lemma bot_set_eq: "bot = {}"
   537   by (iprover intro!: subset_antisym empty_subsetI bot_least)
   569   by (iprover intro!: subset_antisym empty_subsetI bot_least)
   538 
   570 
   539 
   571 
   540 subsection {* Fun as lattice *}
   572 subsection {* Fun as lattice *}
   541 
   573 
   542 instance "fun" :: (type, lattice) lattice
   574 instantiation "fun" :: (type, lattice) lattice
   543   inf_fun_eq: "f \<sqinter> g \<equiv> (\<lambda>x. f x \<sqinter> g x)"
   575 begin
   544   sup_fun_eq: "f \<squnion> g \<equiv> (\<lambda>x. f x \<squnion> g x)"
   576 
       
   577 definition
       
   578   inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
       
   579 
       
   580 definition
       
   581   sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
       
   582 
       
   583 instance
   545 apply intro_classes
   584 apply intro_classes
   546 unfolding inf_fun_eq sup_fun_eq
   585 unfolding inf_fun_eq sup_fun_eq
   547 apply (auto intro: le_funI)
   586 apply (auto intro: le_funI)
   548 apply (rule le_funI)
   587 apply (rule le_funI)
   549 apply (auto dest: le_funD)
   588 apply (auto dest: le_funD)
   550 apply (rule le_funI)
   589 apply (rule le_funI)
   551 apply (auto dest: le_funD)
   590 apply (auto dest: le_funD)
   552 done
   591 done
   553 
   592 
   554 lemmas [code func del] = inf_fun_eq sup_fun_eq
   593 end
   555 
   594 
   556 instance "fun" :: (type, distrib_lattice) distrib_lattice
   595 instance "fun" :: (type, distrib_lattice) distrib_lattice
   557   by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   596   by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   558 
   597 
   559 instance "fun" :: (type, complete_lattice) complete_lattice
   598 instantiation "fun" :: (type, complete_lattice) complete_lattice
   560   Inf_fun_def: "\<Sqinter>A \<equiv> (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   599 begin
   561   Sup_fun_def: "\<Squnion>A \<equiv> (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   600 
       
   601 definition
       
   602   Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
       
   603 
       
   604 definition
       
   605   Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
       
   606 
       
   607 instance
   562   by intro_classes
   608   by intro_classes
   563     (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   609     (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   564       intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   610       intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   565 
   611 
   566 lemmas [code func del] = Inf_fun_def Sup_fun_def
   612 end
   567 
   613 
   568 lemma Inf_empty_fun:
   614 lemma Inf_empty_fun:
   569   "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   615   "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   570   by rule (auto simp add: Inf_fun_def)
   616   by rule (auto simp add: Inf_fun_def)
   571 
   617