src/HOL/Algebra/Lattice.thy
author haftmann
Fri, 01 Nov 2013 18:51:14 +0100
changeset 54230 b1d955791529
parent 46008 c296c75f4cf4
child 55926 3ef14caf5637
permissions -rw-r--r--
more simplification rules on unary and binary minus
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35849
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     1
(*  Title:      HOL/Algebra/Lattice.thy
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     2
    Author:     Clemens Ballarin, started 7 November 2003
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     3
    Copyright:  Clemens Ballarin
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
     4
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27714
diff changeset
     5
Most congruence rules by Stephan Hohe.
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
     6
*)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
     7
35849
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     8
theory Lattice
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     9
imports Congruence
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
    10
begin
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
    11
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19984
diff changeset
    12
section {* Orders and Lattices *}
14751
0d7850e27fed Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents: 14706
diff changeset
    13
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
    14
subsection {* Partial Orders *}
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
    15
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    16
record 'a gorder = "'a eq_object" +
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
    17
  le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
21041
60e418260b4d Order and lattice structures no longer based on records.
ballarin
parents: 20318
diff changeset
    18
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    19
locale weak_partial_order = equivalence L for L (structure) +
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    20
  assumes le_refl [intro, simp]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    21
      "x \<in> carrier L ==> x \<sqsubseteq> x"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
    22
    and weak_le_antisym [intro]:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    23
      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    24
    and le_trans [trans]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    25
      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    26
    and le_cong:
40293
cd932ab8cb59 Minor reformat.
ballarin
parents: 39990
diff changeset
    27
      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow>
cd932ab8cb59 Minor reformat.
ballarin
parents: 39990
diff changeset
    28
      x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
    29
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
    30
definition
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
    31
  lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
    32
  where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    33
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    34
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    35
subsubsection {* The order relation *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    36
44472
6f2943e34d60 tuned proofs;
wenzelm
parents: 40293
diff changeset
    37
context weak_partial_order
6f2943e34d60 tuned proofs;
wenzelm
parents: 40293
diff changeset
    38
begin
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    39
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    40
lemma le_cong_l [intro, trans]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    41
  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    42
  by (auto intro: le_cong [THEN iffD2])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    43
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    44
lemma le_cong_r [intro, trans]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    45
  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    46
  by (auto intro: le_cong [THEN iffD1])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    47
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
    48
lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    49
  by (simp add: le_cong_l)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    50
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    51
end
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    52
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    53
lemma weak_llessI:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    54
  fixes R (structure)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    55
  assumes "x \<sqsubseteq> y" and "~(x .= y)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    56
  shows "x \<sqsubset> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    57
  using assms unfolding lless_def by simp
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    58
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    59
lemma lless_imp_le:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    60
  fixes R (structure)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    61
  assumes "x \<sqsubset> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    62
  shows "x \<sqsubseteq> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    63
  using assms unfolding lless_def by simp
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    64
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    65
lemma weak_lless_imp_not_eq:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    66
  fixes R (structure)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    67
  assumes "x \<sqsubset> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    68
  shows "\<not> (x .= y)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    69
  using assms unfolding lless_def by simp
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
    70
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    71
lemma weak_llessE:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    72
  fixes R (structure)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    73
  assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    74
  shows "P"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    75
  using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    76
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    77
lemma (in weak_partial_order) lless_cong_l [trans]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    78
  assumes xx': "x .= x'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    79
    and xy: "x' \<sqsubset> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    80
    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    81
  shows "x \<sqsubset> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    82
  using assms unfolding lless_def by (auto intro: trans sym)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    83
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    84
lemma (in weak_partial_order) lless_cong_r [trans]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    85
  assumes xy: "x \<sqsubset> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    86
    and  yy': "y .= y'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    87
    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    88
  shows "x \<sqsubset> y'"
44472
6f2943e34d60 tuned proofs;
wenzelm
parents: 40293
diff changeset
    89
  using assms unfolding lless_def by (auto intro: trans sym)  (*slow*)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    90
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    91
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    92
lemma (in weak_partial_order) lless_antisym:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    93
  assumes "a \<in> carrier L" "b \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    94
    and "a \<sqsubset> b" "b \<sqsubset> a"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    95
  shows "P"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    96
  using assms
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    97
  by (elim weak_llessE) auto
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    98
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
    99
lemma (in weak_partial_order) lless_trans [trans]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   100
  assumes "a \<sqsubset> b" "b \<sqsubset> c"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   101
    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   102
  shows "a \<sqsubset> c"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   103
  using assms unfolding lless_def by (blast dest: le_trans intro: sym)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   104
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   105
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   106
subsubsection {* Upper and lower bounds of a set *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   107
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   108
definition
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   109
  Upper :: "[_, 'a set] => 'a set"
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   110
  where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   111
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   112
definition
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   113
  Lower :: "[_, 'a set] => 'a set"
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   114
  where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   115
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   116
lemma Upper_closed [intro!, simp]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   117
  "Upper L A \<subseteq> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   118
  by (unfold Upper_def) clarify
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   119
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   120
lemma Upper_memD [dest]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   121
  fixes L (structure)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   122
  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   123
  by (unfold Upper_def) blast
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   124
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   125
lemma (in weak_partial_order) Upper_elemD [dest]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   126
  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   127
  unfolding Upper_def elem_def
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   128
  by (blast dest: sym)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   129
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   130
lemma Upper_memI:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   131
  fixes L (structure)
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   132
  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   133
  by (unfold Upper_def) blast
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   134
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   135
lemma (in weak_partial_order) Upper_elemI:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   136
  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   137
  unfolding Upper_def by blast
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   138
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   139
lemma Upper_antimono:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   140
  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   141
  by (unfold Upper_def) blast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   142
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   143
lemma (in weak_partial_order) Upper_is_closed [simp]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   144
  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   145
  by (rule is_closedI) (blast intro: Upper_memI)+
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   146
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   147
lemma (in weak_partial_order) Upper_mem_cong:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   148
  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   149
    and aa': "a .= a'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   150
    and aelem: "a \<in> Upper L A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   151
  shows "a' \<in> Upper L A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   152
proof (rule Upper_memI[OF _ a'carr])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   153
  fix y
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   154
  assume yA: "y \<in> A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   155
  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   156
  also note aa'
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   157
  finally
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   158
      show "y \<sqsubseteq> a'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   159
      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   160
qed
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   161
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   162
lemma (in weak_partial_order) Upper_cong:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   163
  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   164
    and AA': "A {.=} A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   165
  shows "Upper L A = Upper L A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   166
unfolding Upper_def
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   167
apply rule
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   168
 apply (rule, clarsimp) defer 1
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   169
 apply (rule, clarsimp) defer 1
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   170
proof -
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   171
  fix x a'
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   172
  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   173
    and a'A': "a' \<in> A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   174
  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   175
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   176
  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   177
  from this obtain a
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   178
      where aA: "a \<in> A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   179
      and a'a: "a' .= a"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   180
      by auto
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   181
  note [simp] = subsetD[OF Acarr aA] carr
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   182
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   183
  note a'a
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   184
  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   185
  finally show "a' \<sqsubseteq> x" by simp
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   186
next
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   187
  fix x a
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   188
  assume carr: "x \<in> carrier L" "a \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   189
    and aA: "a \<in> A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   190
  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   191
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   192
  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   193
  from this obtain a'
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   194
      where a'A': "a' \<in> A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   195
      and aa': "a .= a'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   196
      by auto
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   197
  note [simp] = subsetD[OF A'carr a'A'] carr
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   198
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   199
  note aa'
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   200
  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   201
  finally show "a \<sqsubseteq> x" by simp
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   202
qed
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   203
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   204
lemma Lower_closed [intro!, simp]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   205
  "Lower L A \<subseteq> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   206
  by (unfold Lower_def) clarify
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   207
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   208
lemma Lower_memD [dest]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   209
  fixes L (structure)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   210
  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   211
  by (unfold Lower_def) blast
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   212
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   213
lemma Lower_memI:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   214
  fixes L (structure)
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   215
  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   216
  by (unfold Lower_def) blast
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   217
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   218
lemma Lower_antimono:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   219
  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   220
  by (unfold Lower_def) blast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   221
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   222
lemma (in weak_partial_order) Lower_is_closed [simp]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   223
  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   224
  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   225
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   226
lemma (in weak_partial_order) Lower_mem_cong:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   227
  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   228
    and aa': "a .= a'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   229
    and aelem: "a \<in> Lower L A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   230
  shows "a' \<in> Lower L A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   231
using assms Lower_closed[of L A]
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   232
by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   233
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   234
lemma (in weak_partial_order) Lower_cong:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   235
  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   236
    and AA': "A {.=} A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   237
  shows "Lower L A = Lower L A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   238
unfolding Lower_def
39990
9b4341366b63 slightly more robust proof
krauss
parents: 35849
diff changeset
   239
apply rule
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   240
 apply clarsimp defer 1
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   241
 apply clarsimp defer 1
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   242
proof -
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   243
  fix x a'
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   244
  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   245
    and a'A': "a' \<in> A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   246
  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   247
  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   248
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   249
  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   250
  from this obtain a
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   251
      where aA: "a \<in> A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   252
      and a'a: "a' .= a"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   253
      by auto
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   254
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   255
  from aA and subsetD[OF Acarr aA]
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   256
      have "x \<sqsubseteq> a" by (rule aLxCond)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   257
  also note a'a[symmetric]
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   258
  finally
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   259
      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   260
next
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   261
  fix x a
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   262
  assume carr: "x \<in> carrier L" "a \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   263
    and aA: "a \<in> A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   264
  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   265
  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   266
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   267
  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   268
  from this obtain a'
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   269
      where a'A': "a' \<in> A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   270
      and aa': "a .= a'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   271
      by auto
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   272
  from a'A' and subsetD[OF A'carr a'A']
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   273
      have "x \<sqsubseteq> a'" by (rule a'LxCond)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   274
  also note aa'[symmetric]
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   275
  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   276
qed
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   277
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   278
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   279
subsubsection {* Least and greatest, as predicate *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   280
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   281
definition
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   282
  least :: "[_, 'a, 'a set] => bool"
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   283
  where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   284
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   285
definition
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   286
  greatest :: "[_, 'a, 'a set] => bool"
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   287
  where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   288
30363
9b8d9b6ef803 proper local context for text with antiquotations;
wenzelm
parents: 29242
diff changeset
   289
text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
9b8d9b6ef803 proper local context for text with antiquotations;
wenzelm
parents: 29242
diff changeset
   290
  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   291
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   292
lemma least_closed [intro, simp]:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   293
  "least L l A ==> l \<in> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   294
  by (unfold least_def) fast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   295
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   296
lemma least_mem:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   297
  "least L l A ==> l \<in> A"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   298
  by (unfold least_def) fast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   299
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   300
lemma (in weak_partial_order) weak_least_unique:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   301
  "[| least L x A; least L y A |] ==> x .= y"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   302
  by (unfold least_def) blast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   303
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   304
lemma least_le:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   305
  fixes L (structure)
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   306
  shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   307
  by (unfold least_def) fast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   308
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   309
lemma (in weak_partial_order) least_cong:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   310
  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   311
  by (unfold least_def) (auto dest: sym)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   312
30363
9b8d9b6ef803 proper local context for text with antiquotations;
wenzelm
parents: 29242
diff changeset
   313
text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for 
9b8d9b6ef803 proper local context for text with antiquotations;
wenzelm
parents: 29242
diff changeset
   314
  @{term "A {.=} A'"} *}
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   315
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   316
lemma (in weak_partial_order) least_Upper_cong_l:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   317
  assumes "x .= x'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   318
    and "x \<in> carrier L" "x' \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   319
    and "A \<subseteq> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   320
  shows "least L x (Upper L A) = least L x' (Upper L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   321
  apply (rule least_cong) using assms by auto
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   322
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   323
lemma (in weak_partial_order) least_Upper_cong_r:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   324
  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   325
    and AA': "A {.=} A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   326
  shows "least L x (Upper L A) = least L x (Upper L A')"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   327
apply (subgoal_tac "Upper L A = Upper L A'", simp)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   328
by (rule Upper_cong) fact+
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   329
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   330
lemma least_UpperI:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   331
  fixes L (structure)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   332
  assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   333
    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   334
    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   335
  shows "least L s (Upper L A)"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   336
proof -
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   337
  have "Upper L A \<subseteq> carrier L" by simp
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   338
  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   339
  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   340
  ultimately show ?thesis by (simp add: least_def)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   341
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   342
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   343
lemma least_Upper_above:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   344
  fixes L (structure)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   345
  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   346
  by (unfold least_def) blast
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   347
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   348
lemma greatest_closed [intro, simp]:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   349
  "greatest L l A ==> l \<in> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   350
  by (unfold greatest_def) fast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   351
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   352
lemma greatest_mem:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   353
  "greatest L l A ==> l \<in> A"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   354
  by (unfold greatest_def) fast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   355
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   356
lemma (in weak_partial_order) weak_greatest_unique:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   357
  "[| greatest L x A; greatest L y A |] ==> x .= y"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   358
  by (unfold greatest_def) blast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   359
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   360
lemma greatest_le:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   361
  fixes L (structure)
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   362
  shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   363
  by (unfold greatest_def) fast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   364
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   365
lemma (in weak_partial_order) greatest_cong:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   366
  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   367
  greatest L x A = greatest L x' A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   368
  by (unfold greatest_def) (auto dest: sym)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   369
30363
9b8d9b6ef803 proper local context for text with antiquotations;
wenzelm
parents: 29242
diff changeset
   370
text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for 
9b8d9b6ef803 proper local context for text with antiquotations;
wenzelm
parents: 29242
diff changeset
   371
  @{term "A {.=} A'"} *}
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   372
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   373
lemma (in weak_partial_order) greatest_Lower_cong_l:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   374
  assumes "x .= x'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   375
    and "x \<in> carrier L" "x' \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   376
    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   377
  shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   378
  apply (rule greatest_cong) using assms by auto
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   379
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   380
lemma (in weak_partial_order) greatest_Lower_cong_r:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   381
  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   382
    and AA': "A {.=} A'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   383
  shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   384
apply (subgoal_tac "Lower L A = Lower L A'", simp)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   385
by (rule Lower_cong) fact+
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   386
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   387
lemma greatest_LowerI:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   388
  fixes L (structure)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   389
  assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   390
    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   391
    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   392
  shows "greatest L i (Lower L A)"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   393
proof -
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   394
  have "Lower L A \<subseteq> carrier L" by simp
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   395
  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   396
  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   397
  ultimately show ?thesis by (simp add: greatest_def)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   398
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   399
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   400
lemma greatest_Lower_below:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   401
  fixes L (structure)
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   402
  shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   403
  by (unfold greatest_def) blast
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   404
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   405
text {* Supremum and infimum *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   406
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   407
definition
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   408
  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   409
  where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   410
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   411
definition
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   412
  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   413
  where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   414
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   415
definition
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   416
  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   417
  where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   418
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   419
definition
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   420
  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   421
  where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   422
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   423
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   424
subsection {* Lattices *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   425
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   426
locale weak_upper_semilattice = weak_partial_order +
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   427
  assumes sup_of_two_exists:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   428
    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   429
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   430
locale weak_lower_semilattice = weak_partial_order +
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   431
  assumes inf_of_two_exists:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   432
    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   433
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   434
locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   435
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   436
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   437
subsubsection {* Supremum *}
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   438
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   439
lemma (in weak_upper_semilattice) joinI:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   440
  "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   441
  ==> P (x \<squnion> y)"
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   442
proof (unfold join_def sup_def)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   443
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   444
    and P: "!!l. least L l (Upper L {x, y}) ==> P l"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   445
  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   446
  with L show "P (SOME l. least L l (Upper L {x, y}))"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   447
    by (fast intro: someI2 P)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   448
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   449
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   450
lemma (in weak_upper_semilattice) join_closed [simp]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   451
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   452
  by (rule joinI) (rule least_closed)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   453
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   454
lemma (in weak_upper_semilattice) join_cong_l:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   455
  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   456
    and xx': "x .= x'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   457
  shows "x \<squnion> y .= x' \<squnion> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   458
proof (rule joinI, rule joinI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   459
  fix a b
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   460
  from xx' carr
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   461
      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   462
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   463
  assume leasta: "least L a (Upper L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   464
  assume "least L b (Upper L {x', y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   465
  with carr
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   466
      have leastb: "least L b (Upper L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   467
      by (simp add: least_Upper_cong_r[OF _ _ seq])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   468
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   469
  from leasta leastb
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   470
      show "a .= b" by (rule weak_least_unique)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   471
qed (rule carr)+
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   472
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   473
lemma (in weak_upper_semilattice) join_cong_r:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   474
  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   475
    and yy': "y .= y'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   476
  shows "x \<squnion> y .= x \<squnion> y'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   477
proof (rule joinI, rule joinI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   478
  fix a b
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   479
  have "{x, y} = {y, x}" by fast
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   480
  also from carr yy'
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   481
      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   482
  also have "{y', x} = {x, y'}" by fast
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   483
  finally
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   484
      have seq: "{x, y} {.=} {x, y'}" .
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   485
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   486
  assume leasta: "least L a (Upper L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   487
  assume "least L b (Upper L {x, y'})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   488
  with carr
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   489
      have leastb: "least L b (Upper L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   490
      by (simp add: least_Upper_cong_r[OF _ _ seq])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   491
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   492
  from leasta leastb
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   493
      show "a .= b" by (rule weak_least_unique)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   494
qed (rule carr)+
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   495
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   496
lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   497
  "x \<in> carrier L ==> least L x (Upper L {x})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   498
  by (rule least_UpperI) auto
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   499
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   500
lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   501
  "x \<in> carrier L ==> \<Squnion>{x} .= x"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   502
  unfolding sup_def
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   503
  by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   504
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   505
lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   506
  "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   507
  unfolding sup_def
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   508
  by (rule someI2) (auto intro: sup_of_singletonI)
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   509
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   510
text {* Condition on @{text A}: supremum exists. *}
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   511
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   512
lemma (in weak_upper_semilattice) sup_insertI:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   513
  "[| !!s. least L s (Upper L (insert x A)) ==> P s;
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   514
  least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   515
  ==> P (\<Squnion>(insert x A))"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   516
proof (unfold sup_def)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   517
  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   518
    and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   519
    and least_a: "least L a (Upper L A)"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   520
  from L least_a have La: "a \<in> carrier L" by simp
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   521
  from L sup_of_two_exists least_a
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   522
  obtain s where least_s: "least L s (Upper L {a, x})" by blast
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   523
  show "P (SOME l. least L l (Upper L (insert x A)))"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   524
  proof (rule someI2)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   525
    show "least L s (Upper L (insert x A))"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   526
    proof (rule least_UpperI)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   527
      fix z
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   528
      assume "z \<in> insert x A"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   529
      then show "z \<sqsubseteq> s"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   530
      proof
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   531
        assume "z = x" then show ?thesis
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   532
          by (simp add: least_Upper_above [OF least_s] L La)
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   533
      next
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   534
        assume "z \<in> A"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   535
        with L least_s least_a show ?thesis
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   536
          by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   537
      qed
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   538
    next
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   539
      fix y
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   540
      assume y: "y \<in> Upper L (insert x A)"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   541
      show "s \<sqsubseteq> y"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   542
      proof (rule least_le [OF least_s], rule Upper_memI)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   543
        fix z
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   544
        assume z: "z \<in> {a, x}"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   545
        then show "z \<sqsubseteq> y"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   546
        proof
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   547
          have y': "y \<in> Upper L A"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   548
            apply (rule subsetD [where A = "Upper L (insert x A)"])
23463
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
   549
             apply (rule Upper_antimono)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   550
             apply blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   551
            apply (rule y)
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   552
            done
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   553
          assume "z = a"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   554
          with y' least_a show ?thesis by (fast dest: least_le)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   555
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   556
          assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   557
          with y L show ?thesis by blast
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   558
        qed
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   559
      qed (rule Upper_closed [THEN subsetD, OF y])
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   560
    next
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   561
      from L show "insert x A \<subseteq> carrier L" by simp
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   562
      from least_s show "s \<in> carrier L" by simp
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   563
    qed
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   564
  qed (rule P)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   565
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   566
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   567
lemma (in weak_upper_semilattice) finite_sup_least:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   568
  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
22265
3c5c6bdf61de Adapted to changes in Finite_Set theory.
berghofe
parents: 22063
diff changeset
   569
proof (induct set: finite)
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   570
  case empty
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   571
  then show ?case by simp
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   572
next
15328
35951e6a7855 mod because of change in finite set induction
nipkow
parents: 14751
diff changeset
   573
  case (insert x A)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   574
  show ?case
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   575
  proof (cases "A = {}")
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   576
    case True
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   577
    with insert show ?thesis
44472
6f2943e34d60 tuned proofs;
wenzelm
parents: 40293
diff changeset
   578
      by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   579
        (* The above step is hairy; least_cong can make simp loop.
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   580
        Would want special version of simp to apply least_cong. *)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   581
  next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   582
    case False
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   583
    with insert have "least L (\<Squnion>A) (Upper L A)" by simp
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   584
    with _ show ?thesis
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   585
      by (rule sup_insertI) (simp_all add: insert [simplified])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   586
  qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   587
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   588
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   589
lemma (in weak_upper_semilattice) finite_sup_insertI:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   590
  assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   591
    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   592
  shows "P (\<Squnion> (insert x A))"
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   593
proof (cases "A = {}")
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   594
  case True with P and xA show ?thesis
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   595
    by (simp add: finite_sup_least)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   596
next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   597
  case False with P and xA show ?thesis
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   598
    by (simp add: sup_insertI finite_sup_least)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   599
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   600
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   601
lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   602
  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
22265
3c5c6bdf61de Adapted to changes in Finite_Set theory.
berghofe
parents: 22063
diff changeset
   603
proof (induct set: finite)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   604
  case empty then show ?case by simp
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   605
next
15328
35951e6a7855 mod because of change in finite set induction
nipkow
parents: 14751
diff changeset
   606
  case insert then show ?case
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   607
    by - (rule finite_sup_insertI, simp_all)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   608
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   609
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   610
lemma (in weak_upper_semilattice) join_left:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   611
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   612
  by (rule joinI [folded join_def]) (blast dest: least_mem)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   613
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   614
lemma (in weak_upper_semilattice) join_right:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   615
  "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   616
  by (rule joinI [folded join_def]) (blast dest: least_mem)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   617
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   618
lemma (in weak_upper_semilattice) sup_of_two_least:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   619
  "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   620
proof (unfold sup_def)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   621
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   622
  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   623
  with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   624
  by (fast intro: someI2 weak_least_unique)  (* blast fails *)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   625
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   626
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   627
lemma (in weak_upper_semilattice) join_le:
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   628
  assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   629
    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   630
  shows "x \<squnion> y \<sqsubseteq> z"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   631
proof (rule joinI [OF _ x y])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   632
  fix s
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   633
  assume "least L s (Upper L {x, y})"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   634
  with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   635
qed
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   636
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   637
lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   638
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   639
  shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   640
proof (rule finite_sup_insertI)
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   641
  -- {* The textbook argument in Jacobson I, p 457 *}
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   642
  fix s
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   643
  assume sup: "least L s (Upper L {x, y, z})"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   644
  show "x \<squnion> (y \<squnion> z) .= s"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   645
  proof (rule weak_le_antisym)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   646
    from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44655
diff changeset
   647
      by (fastforce intro!: join_le elim: least_Upper_above)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   648
  next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   649
    from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   650
    by (erule_tac least_le)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   651
      (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   652
  qed (simp_all add: L least_closed [OF sup])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   653
qed (simp_all add: L)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   654
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   655
text {* Commutativity holds for @{text "="}. *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   656
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   657
lemma join_comm:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   658
  fixes L (structure)
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   659
  shows "x \<squnion> y = y \<squnion> x"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   660
  by (unfold join_def) (simp add: insert_commute)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   661
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   662
lemma (in weak_upper_semilattice) weak_join_assoc:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   663
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   664
  shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   665
proof -
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   666
  (* FIXME: could be simplified by improved simp: uniform use of .=,
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   667
     omit [symmetric] in last step. *)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   668
  have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   669
  also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   670
  also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   671
  also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   672
  finally show ?thesis by (simp add: L)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   673
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   674
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   675
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   676
subsubsection {* Infimum *}
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   677
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   678
lemma (in weak_lower_semilattice) meetI:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   679
  "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   680
  x \<in> carrier L; y \<in> carrier L |]
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   681
  ==> P (x \<sqinter> y)"
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   682
proof (unfold meet_def inf_def)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   683
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   684
    and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   685
  with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   686
  with L show "P (SOME g. greatest L g (Lower L {x, y}))"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   687
  by (fast intro: someI2 weak_greatest_unique P)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   688
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   689
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   690
lemma (in weak_lower_semilattice) meet_closed [simp]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   691
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   692
  by (rule meetI) (rule greatest_closed)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   693
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   694
lemma (in weak_lower_semilattice) meet_cong_l:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   695
  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   696
    and xx': "x .= x'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   697
  shows "x \<sqinter> y .= x' \<sqinter> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   698
proof (rule meetI, rule meetI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   699
  fix a b
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   700
  from xx' carr
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   701
      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   702
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   703
  assume greatesta: "greatest L a (Lower L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   704
  assume "greatest L b (Lower L {x', y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   705
  with carr
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   706
      have greatestb: "greatest L b (Lower L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   707
      by (simp add: greatest_Lower_cong_r[OF _ _ seq])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   708
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   709
  from greatesta greatestb
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   710
      show "a .= b" by (rule weak_greatest_unique)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   711
qed (rule carr)+
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   712
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   713
lemma (in weak_lower_semilattice) meet_cong_r:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   714
  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   715
    and yy': "y .= y'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   716
  shows "x \<sqinter> y .= x \<sqinter> y'"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   717
proof (rule meetI, rule meetI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   718
  fix a b
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   719
  have "{x, y} = {y, x}" by fast
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   720
  also from carr yy'
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   721
      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   722
  also have "{y', x} = {x, y'}" by fast
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   723
  finally
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   724
      have seq: "{x, y} {.=} {x, y'}" .
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   725
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   726
  assume greatesta: "greatest L a (Lower L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   727
  assume "greatest L b (Lower L {x, y'})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   728
  with carr
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   729
      have greatestb: "greatest L b (Lower L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   730
      by (simp add: greatest_Lower_cong_r[OF _ _ seq])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   731
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   732
  from greatesta greatestb
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   733
      show "a .= b" by (rule weak_greatest_unique)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   734
qed (rule carr)+
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   735
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   736
lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   737
  "x \<in> carrier L ==> greatest L x (Lower L {x})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   738
  by (rule greatest_LowerI) auto
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   739
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   740
lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   741
  "x \<in> carrier L ==> \<Sqinter>{x} .= x"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   742
  unfolding inf_def
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   743
  by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   744
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   745
lemma (in weak_partial_order) inf_of_singleton_closed:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   746
  "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   747
  unfolding inf_def
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   748
  by (rule someI2) (auto intro: inf_of_singletonI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   749
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   750
text {* Condition on @{text A}: infimum exists. *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   751
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   752
lemma (in weak_lower_semilattice) inf_insertI:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   753
  "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   754
  greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   755
  ==> P (\<Sqinter>(insert x A))"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   756
proof (unfold inf_def)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   757
  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   758
    and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   759
    and greatest_a: "greatest L a (Lower L A)"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   760
  from L greatest_a have La: "a \<in> carrier L" by simp
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   761
  from L inf_of_two_exists greatest_a
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   762
  obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   763
  show "P (SOME g. greatest L g (Lower L (insert x A)))"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   764
  proof (rule someI2)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   765
    show "greatest L i (Lower L (insert x A))"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   766
    proof (rule greatest_LowerI)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   767
      fix z
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   768
      assume "z \<in> insert x A"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   769
      then show "i \<sqsubseteq> z"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   770
      proof
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   771
        assume "z = x" then show ?thesis
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   772
          by (simp add: greatest_Lower_below [OF greatest_i] L La)
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   773
      next
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   774
        assume "z \<in> A"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   775
        with L greatest_i greatest_a show ?thesis
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   776
          by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   777
      qed
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   778
    next
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   779
      fix y
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   780
      assume y: "y \<in> Lower L (insert x A)"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   781
      show "y \<sqsubseteq> i"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   782
      proof (rule greatest_le [OF greatest_i], rule Lower_memI)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   783
        fix z
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   784
        assume z: "z \<in> {a, x}"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   785
        then show "y \<sqsubseteq> z"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   786
        proof
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   787
          have y': "y \<in> Lower L A"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   788
            apply (rule subsetD [where A = "Lower L (insert x A)"])
23463
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
   789
            apply (rule Lower_antimono)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   790
             apply blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   791
            apply (rule y)
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   792
            done
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   793
          assume "z = a"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   794
          with y' greatest_a show ?thesis by (fast dest: greatest_le)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   795
        next
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   796
          assume "z \<in> {x}"
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   797
          with y L show ?thesis by blast
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   798
        qed
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   799
      qed (rule Lower_closed [THEN subsetD, OF y])
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   800
    next
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   801
      from L show "insert x A \<subseteq> carrier L" by simp
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   802
      from greatest_i show "i \<in> carrier L" by simp
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   803
    qed
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   804
  qed (rule P)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   805
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   806
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   807
lemma (in weak_lower_semilattice) finite_inf_greatest:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   808
  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
22265
3c5c6bdf61de Adapted to changes in Finite_Set theory.
berghofe
parents: 22063
diff changeset
   809
proof (induct set: finite)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   810
  case empty then show ?case by simp
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   811
next
15328
35951e6a7855 mod because of change in finite set induction
nipkow
parents: 14751
diff changeset
   812
  case (insert x A)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   813
  show ?case
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   814
  proof (cases "A = {}")
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   815
    case True
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   816
    with insert show ?thesis
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   817
      by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30363
diff changeset
   818
        inf_of_singleton_closed inf_of_singletonI)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   819
  next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   820
    case False
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   821
    from insert show ?thesis
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   822
    proof (rule_tac inf_insertI)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   823
      from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   824
    qed simp_all
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   825
  qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   826
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   827
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   828
lemma (in weak_lower_semilattice) finite_inf_insertI:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   829
  assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   830
    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   831
  shows "P (\<Sqinter> (insert x A))"
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   832
proof (cases "A = {}")
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   833
  case True with P and xA show ?thesis
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   834
    by (simp add: finite_inf_greatest)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   835
next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   836
  case False with P and xA show ?thesis
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   837
    by (simp add: inf_insertI finite_inf_greatest)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   838
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   839
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   840
lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   841
  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
22265
3c5c6bdf61de Adapted to changes in Finite_Set theory.
berghofe
parents: 22063
diff changeset
   842
proof (induct set: finite)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   843
  case empty then show ?case by simp
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   844
next
15328
35951e6a7855 mod because of change in finite set induction
nipkow
parents: 14751
diff changeset
   845
  case insert then show ?case
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   846
    by (rule_tac finite_inf_insertI) (simp_all)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   847
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   848
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   849
lemma (in weak_lower_semilattice) meet_left:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   850
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   851
  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   852
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   853
lemma (in weak_lower_semilattice) meet_right:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   854
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   855
  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   856
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   857
lemma (in weak_lower_semilattice) inf_of_two_greatest:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   858
  "[| x \<in> carrier L; y \<in> carrier L |] ==>
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   859
  greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   860
proof (unfold inf_def)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   861
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   862
  with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   863
  with L
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   864
  show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   865
  by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   866
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   867
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   868
lemma (in weak_lower_semilattice) meet_le:
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   869
  assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   870
    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   871
  shows "z \<sqsubseteq> x \<sqinter> y"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   872
proof (rule meetI [OF _ x y])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   873
  fix i
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   874
  assume "greatest L i (Lower L {x, y})"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22265
diff changeset
   875
  with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   876
qed
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   877
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   878
lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   879
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   880
  shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   881
proof (rule finite_inf_insertI)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   882
  txt {* The textbook argument in Jacobson I, p 457 *}
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   883
  fix i
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   884
  assume inf: "greatest L i (Lower L {x, y, z})"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   885
  show "x \<sqinter> (y \<sqinter> z) .= i"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   886
  proof (rule weak_le_antisym)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   887
    from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44655
diff changeset
   888
      by (fastforce intro!: meet_le elim: greatest_Lower_below)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   889
  next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   890
    from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   891
    by (erule_tac greatest_le)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   892
      (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
   893
  qed (simp_all add: L greatest_closed [OF inf])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   894
qed (simp_all add: L)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   895
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   896
lemma meet_comm:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   897
  fixes L (structure)
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   898
  shows "x \<sqinter> y = y \<sqinter> x"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   899
  by (unfold meet_def) (simp add: insert_commute)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   900
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   901
lemma (in weak_lower_semilattice) weak_meet_assoc:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   902
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   903
  shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   904
proof -
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   905
  (* FIXME: improved simp, see weak_join_assoc above *)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   906
  have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   907
  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   908
  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   909
  also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   910
  finally show ?thesis by (simp add: L)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   911
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   912
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   913
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   914
subsection {* Total Orders *}
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   915
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   916
locale weak_total_order = weak_partial_order +
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   917
  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   918
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   919
text {* Introduction rule: the usual definition of total order *}
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   920
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   921
lemma (in weak_partial_order) weak_total_orderI:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   922
  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   923
  shows "weak_total_order L"
44655
fe0365331566 tuned proofs;
wenzelm
parents: 44472
diff changeset
   924
  by default (rule total)
24087
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   925
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   926
text {* Total orders are lattices. *}
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   927
29242
e190bc2a5399 More porting to new locales
ballarin
parents: 29237
diff changeset
   928
sublocale weak_total_order < weak: weak_lattice
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 27717
diff changeset
   929
proof
24087
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   930
  fix x y
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   931
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   932
  show "EX s. least L s (Upper L {x, y})"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   933
  proof -
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   934
    note total L
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   935
    moreover
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   936
    {
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   937
      assume "x \<sqsubseteq> y"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   938
      with L have "least L y (Upper L {x, y})"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   939
        by (rule_tac least_UpperI) auto
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   940
    }
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   941
    moreover
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   942
    {
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   943
      assume "y \<sqsubseteq> x"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   944
      with L have "least L x (Upper L {x, y})"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   945
        by (rule_tac least_UpperI) auto
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   946
    }
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   947
    ultimately show ?thesis by blast
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   948
  qed
24087
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   949
next
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   950
  fix x y
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   951
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   952
  show "EX i. greatest L i (Lower L {x, y})"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   953
  proof -
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   954
    note total L
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   955
    moreover
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   956
    {
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   957
      assume "y \<sqsubseteq> x"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   958
      with L have "greatest L y (Lower L {x, y})"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   959
        by (rule_tac greatest_LowerI) auto
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   960
    }
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   961
    moreover
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   962
    {
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   963
      assume "x \<sqsubseteq> y"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   964
      with L have "greatest L x (Lower L {x, y})"
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   965
        by (rule_tac greatest_LowerI) auto
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   966
    }
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   967
    ultimately show ?thesis by blast
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   968
  qed
eb025d149a34 Proper interpretation of total orders in lattices.
ballarin
parents: 23463
diff changeset
   969
qed
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   970
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
   971
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27714
diff changeset
   972
subsection {* Complete Lattices *}
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   973
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   974
locale weak_complete_lattice = weak_lattice +
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   975
  assumes sup_exists:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   976
    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   977
    and inf_exists:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   978
    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
21041
60e418260b4d Order and lattice structures no longer based on records.
ballarin
parents: 20318
diff changeset
   979
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   980
text {* Introduction rule: the usual definition of complete lattice *}
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   981
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   982
lemma (in weak_partial_order) weak_complete_latticeI:
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   983
  assumes sup_exists:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   984
    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   985
    and inf_exists:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   986
    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   987
  shows "weak_complete_lattice L"
44655
fe0365331566 tuned proofs;
wenzelm
parents: 44472
diff changeset
   988
  by default (auto intro: sup_exists inf_exists)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   989
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   990
definition
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   991
  top :: "_ => 'a" ("\<top>\<index>")
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   992
  where "\<top>\<^bsub>L\<^esub> = sup L (carrier L)"
21041
60e418260b4d Order and lattice structures no longer based on records.
ballarin
parents: 20318
diff changeset
   993
35847
19f1f7066917 eliminated old constdefs;
wenzelm
parents: 33657
diff changeset
   994
definition
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
   995
  bottom :: "_ => 'a" ("\<bottom>\<index>")
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35847
diff changeset
   996
  where "\<bottom>\<^bsub>L\<^esub> = inf L (carrier L)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   997
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
   998
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
   999
lemma (in weak_complete_lattice) supI:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1000
  "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
  1001
  ==> P (\<Squnion>A)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1002
proof (unfold sup_def)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1003
  assume L: "A \<subseteq> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1004
    and P: "!!l. least L l (Upper L A) ==> P l"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1005
  with sup_exists obtain s where "least L s (Upper L A)" by blast
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1006
  with L show "P (SOME l. least L l (Upper L A))"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1007
  by (fast intro: someI2 weak_least_unique P)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1008
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1009
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1010
lemma (in weak_complete_lattice) sup_closed [simp]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1011
  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1012
  by (rule supI) simp_all
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1013
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1014
lemma (in weak_complete_lattice) top_closed [simp, intro]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1015
  "\<top> \<in> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1016
  by (unfold top_def) simp
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1017
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1018
lemma (in weak_complete_lattice) infI:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1019
  "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
  1020
  ==> P (\<Sqinter>A)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1021
proof (unfold inf_def)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1022
  assume L: "A \<subseteq> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1023
    and P: "!!l. greatest L l (Lower L A) ==> P l"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1024
  with inf_exists obtain s where "greatest L s (Lower L A)" by blast
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1025
  with L show "P (SOME l. greatest L l (Lower L A))"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1026
  by (fast intro: someI2 weak_greatest_unique P)
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1027
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1028
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1029
lemma (in weak_complete_lattice) inf_closed [simp]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1030
  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1031
  by (rule infI) simp_all
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1032
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1033
lemma (in weak_complete_lattice) bottom_closed [simp, intro]:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1034
  "\<bottom> \<in> carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1035
  by (unfold bottom_def) simp
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1036
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1037
text {* Jacobson: Theorem 8.1 *}
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1038
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1039
lemma Lower_empty [simp]:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1040
  "Lower L {} = carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1041
  by (unfold Lower_def) simp
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1042
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1043
lemma Upper_empty [simp]:
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1044
  "Upper L {} = carrier L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1045
  by (unfold Upper_def) simp
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1046
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1047
theorem (in weak_partial_order) weak_complete_lattice_criterion1:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1048
  assumes top_exists: "EX g. greatest L g (carrier L)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1049
    and inf_exists:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1050
      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1051
  shows "weak_complete_lattice L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1052
proof (rule weak_complete_latticeI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1053
  from top_exists obtain top where top: "greatest L top (carrier L)" ..
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1054
  fix A
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1055
  assume L: "A \<subseteq> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1056
  let ?B = "Upper L A"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1057
  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1058
  then have B_non_empty: "?B ~= {}" by fast
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1059
  have B_L: "?B \<subseteq> carrier L" by simp
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1060
  from inf_exists [OF B_L B_non_empty]
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1061
  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1062
  have "least L b (Upper L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1063
apply (rule least_UpperI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1064
   apply (rule greatest_le [where A = "Lower L ?B"])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1065
    apply (rule b_inf_B)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1066
   apply (rule Lower_memI)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1067
    apply (erule Upper_memD [THEN conjunct1])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1068
     apply assumption
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1069
    apply (rule L)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1070
   apply (fast intro: L [THEN subsetD])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1071
  apply (erule greatest_Lower_below [OF b_inf_B])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1072
  apply simp
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1073
 apply (rule L)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1074
apply (rule greatest_closed [OF b_inf_B])
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1075
done
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1076
  then show "EX s. least L s (Upper L A)" ..
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1077
next
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1078
  fix A
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1079
  assume L: "A \<subseteq> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1080
  show "EX i. greatest L i (Lower L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1081
  proof (cases "A = {}")
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1082
    case True then show ?thesis
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1083
      by (simp add: top_exists)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1084
  next
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1085
    case False with L show ?thesis
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1086
      by (rule inf_exists)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1087
  qed
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1088
qed
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1089
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1090
(* TODO: prove dual version *)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1091
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1092
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1093
subsection {* Orders and Lattices where @{text eq} is the Equality *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1094
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1095
locale partial_order = weak_partial_order +
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1096
  assumes eq_is_equal: "op .= = op ="
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1097
begin
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1098
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
  1099
declare weak_le_antisym [rule del]
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1100
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
  1101
lemma le_antisym [intro]:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1102
  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
  1103
  using weak_le_antisym unfolding eq_is_equal .
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1104
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1105
lemma lless_eq:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1106
  "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1107
  unfolding lless_def by (simp add: eq_is_equal)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1108
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1109
lemma lless_asym:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1110
  assumes "a \<in> carrier L" "b \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1111
    and "a \<sqsubset> b" "b \<sqsubset> a"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1112
  shows "P"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1113
  using assms unfolding lless_eq by auto
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1114
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1115
end
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1116
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1117
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27714
diff changeset
  1118
text {* Least and greatest, as predicate *}
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1119
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1120
lemma (in partial_order) least_unique:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1121
  "[| least L x A; least L y A |] ==> x = y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1122
  using weak_least_unique unfolding eq_is_equal .
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1123
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1124
lemma (in partial_order) greatest_unique:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1125
  "[| greatest L x A; greatest L y A |] ==> x = y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1126
  using weak_greatest_unique unfolding eq_is_equal .
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1127
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1128
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27714
diff changeset
  1129
text {* Lattices *}
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1130
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1131
locale upper_semilattice = partial_order +
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1132
  assumes sup_of_two_exists:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1133
    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1134
29242
e190bc2a5399 More porting to new locales
ballarin
parents: 29237
diff changeset
  1135
sublocale upper_semilattice < weak: weak_upper_semilattice
44655
fe0365331566 tuned proofs;
wenzelm
parents: 44472
diff changeset
  1136
  by default (rule sup_of_two_exists)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1137
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1138
locale lower_semilattice = partial_order +
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1139
  assumes inf_of_two_exists:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1140
    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1141
29242
e190bc2a5399 More porting to new locales
ballarin
parents: 29237
diff changeset
  1142
sublocale lower_semilattice < weak: weak_lower_semilattice
44655
fe0365331566 tuned proofs;
wenzelm
parents: 44472
diff changeset
  1143
  by default (rule inf_of_two_exists)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1144
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1145
locale lattice = upper_semilattice + lower_semilattice
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1146
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1147
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27714
diff changeset
  1148
text {* Supremum *}
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1149
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1150
declare (in partial_order) weak_sup_of_singleton [simp del]
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1151
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1152
lemma (in partial_order) sup_of_singleton [simp]:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1153
  "x \<in> carrier L ==> \<Squnion>{x} = x"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1154
  using weak_sup_of_singleton unfolding eq_is_equal .
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1155
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1156
lemma (in upper_semilattice) join_assoc_lemma:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1157
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1158
  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1159
  using weak_join_assoc_lemma L unfolding eq_is_equal .
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1160
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1161
lemma (in upper_semilattice) join_assoc:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1162
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1163
  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1164
  using weak_join_assoc L unfolding eq_is_equal .
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1165
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1166
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27714
diff changeset
  1167
text {* Infimum *}
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1168
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1169
declare (in partial_order) weak_inf_of_singleton [simp del]
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1170
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1171
lemma (in partial_order) inf_of_singleton [simp]:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1172
  "x \<in> carrier L ==> \<Sqinter>{x} = x"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1173
  using weak_inf_of_singleton unfolding eq_is_equal .
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1174
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1175
text {* Condition on @{text A}: infimum exists. *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1176
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1177
lemma (in lower_semilattice) meet_assoc_lemma:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1178
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1179
  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1180
  using weak_meet_assoc_lemma L unfolding eq_is_equal .
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1181
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1182
lemma (in lower_semilattice) meet_assoc:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1183
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1184
  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 27713
diff changeset
  1185
  using weak_meet_assoc L unfolding eq_is_equal .
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1186
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1187
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27714
diff changeset
  1188
text {* Total Orders *}
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1189
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1190
locale total_order = partial_order +
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 27717
diff changeset
  1191
  assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1192
29242
e190bc2a5399 More porting to new locales
ballarin
parents: 29237
diff changeset
  1193
sublocale total_order < weak: weak_total_order
44655
fe0365331566 tuned proofs;
wenzelm
parents: 44472
diff changeset
  1194
  by default (rule total_order_total)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1195
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1196
text {* Introduction rule: the usual definition of total order *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1197
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1198
lemma (in partial_order) total_orderI:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1199
  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1200
  shows "total_order L"
44655
fe0365331566 tuned proofs;
wenzelm
parents: 44472
diff changeset
  1201
  by default (rule total)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1202
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1203
text {* Total orders are lattices. *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1204
29242
e190bc2a5399 More porting to new locales
ballarin
parents: 29237
diff changeset
  1205
sublocale total_order < weak: lattice
44655
fe0365331566 tuned proofs;
wenzelm
parents: 44472
diff changeset
  1206
  by default (auto intro: sup_of_two_exists inf_of_two_exists)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1207
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1208
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27714
diff changeset
  1209
text {* Complete lattices *}
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1210
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1211
locale complete_lattice = lattice +
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1212
  assumes sup_exists:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1213
    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1214
    and inf_exists:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1215
    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1216
29242
e190bc2a5399 More porting to new locales
ballarin
parents: 29237
diff changeset
  1217
sublocale complete_lattice < weak: weak_complete_lattice
44655
fe0365331566 tuned proofs;
wenzelm
parents: 44472
diff changeset
  1218
  by default (auto intro: sup_exists inf_exists)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1219
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1220
text {* Introduction rule: the usual definition of complete lattice *}
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1221
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1222
lemma (in partial_order) complete_latticeI:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1223
  assumes sup_exists:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1224
    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1225
    and inf_exists:
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1226
    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1227
  shows "complete_lattice L"
44655
fe0365331566 tuned proofs;
wenzelm
parents: 44472
diff changeset
  1228
  by default (auto intro: sup_exists inf_exists)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1229
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1230
theorem (in partial_order) complete_lattice_criterion1:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1231
  assumes top_exists: "EX g. greatest L g (carrier L)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1232
    and inf_exists:
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1233
      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1234
  shows "complete_lattice L"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1235
proof (rule complete_latticeI)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1236
  from top_exists obtain top where top: "greatest L top (carrier L)" ..
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1237
  fix A
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1238
  assume L: "A \<subseteq> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1239
  let ?B = "Upper L A"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1240
  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1241
  then have B_non_empty: "?B ~= {}" by fast
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1242
  have B_L: "?B \<subseteq> carrier L" by simp
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1243
  from inf_exists [OF B_L B_non_empty]
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1244
  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1245
  have "least L b (Upper L A)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1246
apply (rule least_UpperI)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1247
   apply (rule greatest_le [where A = "Lower L ?B"])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1248
    apply (rule b_inf_B)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1249
   apply (rule Lower_memI)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1250
    apply (erule Upper_memD [THEN conjunct1])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1251
     apply assumption
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1252
    apply (rule L)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1253
   apply (fast intro: L [THEN subsetD])
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
  1254
  apply (erule greatest_Lower_below [OF b_inf_B])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1255
  apply simp
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1256
 apply (rule L)
27700
ef4b26efa8b6 Renamed theorems;
ballarin
parents: 26805
diff changeset
  1257
apply (rule greatest_closed [OF b_inf_B])
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1258
done
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1259
  then show "EX s. least L s (Upper L A)" ..
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1260
next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1261
  fix A
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1262
  assume L: "A \<subseteq> carrier L"
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1263
  show "EX i. greatest L i (Lower L A)"
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1264
  proof (cases "A = {}")
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1265
    case True then show ?thesis
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1266
      by (simp add: top_exists)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1267
  next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1268
    case False with L show ?thesis
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1269
      by (rule inf_exists)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1270
  qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1271
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1272
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1273
(* TODO: prove dual version *)
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1274
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19984
diff changeset
  1275
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1276
subsection {* Examples *}
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1277
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27714
diff changeset
  1278
subsubsection {* The Powerset of a Set is a Complete Lattice *}
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1279
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1280
theorem powerset_is_complete_lattice:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27700
diff changeset
  1281
  "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1282
  (is "complete_lattice ?L")
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1283
proof (rule partial_order.complete_latticeI)
22063
717425609192 Reverted to structure representation with records.
ballarin
parents: 21896
diff changeset
  1284
  show "partial_order ?L"
44472
6f2943e34d60 tuned proofs;
wenzelm
parents: 40293
diff changeset
  1285
    by default auto
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1286
next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1287
  fix B
46008
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1288
  assume "B \<subseteq> carrier ?L"
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1289
  then have "least ?L (\<Union> B) (Upper ?L B)"
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1290
    by (fastforce intro!: least_UpperI simp: Upper_def)
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1291
  then show "EX s. least ?L s (Upper ?L B)" ..
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1292
next
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1293
  fix B
46008
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1294
  assume "B \<subseteq> carrier ?L"
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1295
  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1296
    txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1297
      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1298
    by (fastforce intro!: greatest_LowerI simp: Lower_def)
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 44890
diff changeset
  1299
  then show "EX i. greatest ?L i (Lower ?L B)" ..
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1300
qed
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1301
14751
0d7850e27fed Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents: 14706
diff changeset
  1302
text {* An other example, that of the lattice of subgroups of a group,
0d7850e27fed Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents: 14706
diff changeset
  1303
  can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents:
diff changeset
  1304
14693
4deda204e1d8 improved syntax;
wenzelm
parents: 14666
diff changeset
  1305
end