src/HOL/Algebra/Lattice.thy
changeset 19783 82f365a14960
parent 19286 83404ccd270a
child 19931 fb32b43e7f80
equal deleted inserted replaced
19782:48c4632e2c28 19783:82f365a14960
    17 subsection {* Partial Orders *}
    17 subsection {* Partial Orders *}
    18 
    18 
    19 record 'a order = "'a partial_object" +
    19 record 'a order = "'a partial_object" +
    20   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    20   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    21 
    21 
    22 locale partial_order = struct L +
    22 locale partial_order =
       
    23   fixes L (structure)
    23   assumes refl [intro, simp]:
    24   assumes refl [intro, simp]:
    24                   "x \<in> carrier L ==> x \<sqsubseteq> x"
    25                   "x \<in> carrier L ==> x \<sqsubseteq> x"
    25     and anti_sym [intro]:
    26     and anti_sym [intro]:
    26                   "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
    27                   "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
    27     and trans [trans]:
    28     and trans [trans]:
    67 lemma Upper_closed [intro, simp]:
    68 lemma Upper_closed [intro, simp]:
    68   "Upper L A \<subseteq> carrier L"
    69   "Upper L A \<subseteq> carrier L"
    69   by (unfold Upper_def) clarify
    70   by (unfold Upper_def) clarify
    70 
    71 
    71 lemma UpperD [dest]:
    72 lemma UpperD [dest]:
    72   includes struct L
    73   fixes L (structure)
    73   shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
    74   shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
    74   by (unfold Upper_def) blast
    75   by (unfold Upper_def) blast
    75 
    76 
    76 lemma Upper_memI:
    77 lemma Upper_memI:
    77   includes struct L
    78   fixes L (structure)
    78   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
    79   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
    79   by (unfold Upper_def) blast
    80   by (unfold Upper_def) blast
    80 
    81 
    81 lemma Upper_antimono:
    82 lemma Upper_antimono:
    82   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
    83   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
    88 lemma Lower_closed [intro, simp]:
    89 lemma Lower_closed [intro, simp]:
    89   "Lower L A \<subseteq> carrier L"
    90   "Lower L A \<subseteq> carrier L"
    90   by (unfold Lower_def) clarify
    91   by (unfold Lower_def) clarify
    91 
    92 
    92 lemma LowerD [dest]:
    93 lemma LowerD [dest]:
    93   includes struct L
    94   fixes L (structure)
    94   shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
    95   shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
    95   by (unfold Lower_def) blast
    96   by (unfold Lower_def) blast
    96 
    97 
    97 lemma Lower_memI:
    98 lemma Lower_memI:
    98   includes struct L
    99   fixes L (structure)
    99   shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   100   shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   100   by (unfold Lower_def) blast
   101   by (unfold Lower_def) blast
   101 
   102 
   102 lemma Lower_antimono:
   103 lemma Lower_antimono:
   103   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   104   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   117 lemma (in partial_order) least_unique:
   118 lemma (in partial_order) least_unique:
   118   "[| least L x A; least L y A |] ==> x = y"
   119   "[| least L x A; least L y A |] ==> x = y"
   119   by (unfold least_def) blast
   120   by (unfold least_def) blast
   120 
   121 
   121 lemma least_le:
   122 lemma least_le:
   122   includes struct L
   123   fixes L (structure)
   123   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   124   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   124   by (unfold least_def) fast
   125   by (unfold least_def) fast
   125 
   126 
   126 lemma least_UpperI:
   127 lemma least_UpperI:
   127   includes struct L
   128   fixes L (structure)
   128   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   129   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   129     and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   130     and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   130     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   131     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   131   shows "least L s (Upper L A)"
   132   shows "least L s (Upper L A)"
   132 proof -
   133 proof -
   150 lemma (in partial_order) greatest_unique:
   151 lemma (in partial_order) greatest_unique:
   151   "[| greatest L x A; greatest L y A |] ==> x = y"
   152   "[| greatest L x A; greatest L y A |] ==> x = y"
   152   by (unfold greatest_def) blast
   153   by (unfold greatest_def) blast
   153 
   154 
   154 lemma greatest_le:
   155 lemma greatest_le:
   155   includes struct L
   156   fixes L (structure)
   156   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   157   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   157   by (unfold greatest_def) fast
   158   by (unfold greatest_def) fast
   158 
   159 
   159 lemma greatest_LowerI:
   160 lemma greatest_LowerI:
   160   includes struct L
   161   fixes L (structure)
   161   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   162   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   162     and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   163     and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   163     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   164     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   164   shows "greatest L i (Lower L A)"
   165   shows "greatest L i (Lower L A)"
   165 proof -
   166 proof -
   177     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   178     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   178     and inf_of_two_exists:
   179     and inf_of_two_exists:
   179     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   180     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   180 
   181 
   181 lemma least_Upper_above:
   182 lemma least_Upper_above:
   182   includes struct L
   183   fixes L (structure)
   183   shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   184   shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   184   by (unfold least_def) blast
   185   by (unfold least_def) blast
   185 
   186 
   186 lemma greatest_Lower_above:
   187 lemma greatest_Lower_above:
   187   includes struct L
   188   fixes L (structure)
   188   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   189   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   189   by (unfold greatest_def) blast
   190   by (unfold greatest_def) blast
   190 
   191 
   191 
   192 
   192 subsubsection {* Supremum *}
   193 subsubsection {* Supremum *}
   209 lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   210 lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   210   "x \<in> carrier L ==> least L x (Upper L {x})"
   211   "x \<in> carrier L ==> least L x (Upper L {x})"
   211   by (rule least_UpperI) fast+
   212   by (rule least_UpperI) fast+
   212 
   213 
   213 lemma (in partial_order) sup_of_singleton [simp]:
   214 lemma (in partial_order) sup_of_singleton [simp]:
   214   includes struct L
   215   "x \<in> carrier L ==> \<Squnion>{x} = x"
   215   shows "x \<in> carrier L ==> \<Squnion>{x} = x"
       
   216   by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
   216   by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
   217 
   217 
   218 
   218 
   219 text {* Condition on @{text A}: supremum exists. *}
   219 text {* Condition on @{text A}: supremum exists. *}
   220 
   220 
   398       (blast intro!: Upper_memI intro: trans join_left join_right join_closed)
   398       (blast intro!: Upper_memI intro: trans join_left join_right join_closed)
   399   qed (simp_all add: L least_carrier [OF sup])
   399   qed (simp_all add: L least_carrier [OF sup])
   400 qed (simp_all add: L)
   400 qed (simp_all add: L)
   401 
   401 
   402 lemma join_comm:
   402 lemma join_comm:
   403   includes struct L
   403   fixes L (structure)
   404   shows "x \<squnion> y = y \<squnion> x"
   404   shows "x \<squnion> y = y \<squnion> x"
   405   by (unfold join_def) (simp add: insert_commute)
   405   by (unfold join_def) (simp add: insert_commute)
   406 
   406 
   407 lemma (in lattice) join_assoc:
   407 lemma (in lattice) join_assoc:
   408   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   408   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   437 lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   437 lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   438   "x \<in> carrier L ==> greatest L x (Lower L {x})"
   438   "x \<in> carrier L ==> greatest L x (Lower L {x})"
   439   by (rule greatest_LowerI) fast+
   439   by (rule greatest_LowerI) fast+
   440 
   440 
   441 lemma (in partial_order) inf_of_singleton [simp]:
   441 lemma (in partial_order) inf_of_singleton [simp]:
   442   includes struct L
   442   "x \<in> carrier L ==> \<Sqinter> {x} = x"
   443   shows "x \<in> carrier L ==> \<Sqinter> {x} = x"
       
   444   by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
   443   by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
   445 
   444 
   446 text {* Condition on A: infimum exists. *}
   445 text {* Condition on A: infimum exists. *}
   447 
   446 
   448 lemma (in lattice) inf_insertI:
   447 lemma (in lattice) inf_insertI:
   627       (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)
   626       (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)
   628   qed (simp_all add: L greatest_carrier [OF inf])
   627   qed (simp_all add: L greatest_carrier [OF inf])
   629 qed (simp_all add: L)
   628 qed (simp_all add: L)
   630 
   629 
   631 lemma meet_comm:
   630 lemma meet_comm:
   632   includes struct L
   631   fixes L (structure)
   633   shows "x \<sqinter> y = y \<sqinter> x"
   632   shows "x \<sqinter> y = y \<sqinter> x"
   634   by (unfold meet_def) (simp add: insert_commute)
   633   by (unfold meet_def) (simp add: insert_commute)
   635 
   634 
   636 lemma (in lattice) meet_assoc:
   635 lemma (in lattice) meet_assoc:
   637   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   636   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"