src/HOL/Algebra/Lattice.thy
 changeset 19783 82f365a14960 parent 19286 83404ccd270a child 19931 fb32b43e7f80
equal 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"`