src/HOL/LOrder.thy
author nipkow
Wed, 18 Aug 2004 11:09:40 +0200
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15524 2ef571f80a55
permissions -rw-r--r--
import -> imports
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
     1
(*  Title:   HOL/LOrder.thy
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
     2
    ID:      $Id$
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
     3
    Author:  Steven Obua, TU Muenchen
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
     4
*)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
     5
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
     6
header {* Lattice Orders *}
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
     7
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15010
diff changeset
     8
theory LOrder
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
     9
imports HOL
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15010
diff changeset
    10
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    11
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    12
text {*
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    13
  The theory of lattices developed here is taken from the book:
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    14
  \begin{itemize}
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    15
  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979. 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    16
  \end{itemize}
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    17
*}
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    18
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    19
constdefs
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    20
  is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    21
  "is_meet m == ! a b x. m a b \<le> a \<and> m a b \<le> b \<and> (x \<le> a \<and> x \<le> b \<longrightarrow> x \<le> m a b)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    22
  is_join :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    23
  "is_join j == ! a b x. a \<le> j a b \<and> b \<le> j a b \<and> (a \<le> x \<and> b \<le> x \<longrightarrow> j a b \<le> x)"  
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    24
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    25
lemma is_meet_unique: 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    26
  assumes "is_meet u" "is_meet v" shows "u = v"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    27
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    28
  {
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    29
    fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    30
    assume a: "is_meet a"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    31
    assume b: "is_meet b"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    32
    {
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    33
      fix x y 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    34
      let ?za = "a x y"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    35
      let ?zb = "b x y"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    36
      from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    37
      with b have "?za <= ?zb" by (auto simp add: is_meet_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    38
    }
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    39
  }
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    40
  note f_le = this
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    41
  show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    42
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    43
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    44
lemma is_join_unique: 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    45
  assumes "is_join u" "is_join v" shows "u = v"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    46
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    47
  {
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    48
    fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    49
    assume a: "is_join a"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    50
    assume b: "is_join b"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    51
    {
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    52
      fix x y 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    53
      let ?za = "a x y"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    54
      let ?zb = "b x y"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    55
      from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    56
      with b have "?zb <= ?za" by (auto simp add: is_join_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    57
    }
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    58
  }
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    59
  note f_le = this
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    60
  show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    61
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    62
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    63
axclass join_semilorder < order
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    64
  join_exists: "? j. is_join j"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    65
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    66
axclass meet_semilorder < order
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    67
  meet_exists: "? m. is_meet m"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    68
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    69
axclass lorder < join_semilorder, meet_semilorder
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    70
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    71
constdefs
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    72
  meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    73
  "meet == THE m. is_meet m"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    74
  join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    75
  "join ==  THE j. is_join j"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    76
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    77
lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    78
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    79
  from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    80
  with is_meet_unique[of _ k] show ?thesis
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    81
    by (simp add: meet_def theI[of is_meet])    
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    82
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    83
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    84
lemma meet_unique: "(is_meet m) = (m = meet)" 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    85
by (insert is_meet_meet, auto simp add: is_meet_unique)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    86
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    87
lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    88
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    89
  from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    90
  with is_join_unique[of _ k] show ?thesis
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    91
    by (simp add: join_def theI[of is_join])    
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    92
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    93
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    94
lemma join_unique: "(is_join j) = (j = join)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    95
by (insert is_join_join, auto simp add: is_join_unique)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    96
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    97
lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    98
by (insert is_meet_meet, auto simp add: is_meet_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
    99
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   100
lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   101
by (insert is_meet_meet, auto simp add: is_meet_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   102
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   103
lemma meet_imp_le: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   104
by (insert is_meet_meet, auto simp add: is_meet_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   105
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   106
lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   107
by (insert is_join_join, auto simp add: is_join_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   108
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   109
lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   110
by (insert is_join_join, auto simp add: is_join_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   111
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   112
lemma join_imp_le: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   113
by (insert is_join_join, auto simp add: is_join_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   114
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   115
lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   116
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   117
lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   118
by (auto simp add: is_meet_def min_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   119
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   120
lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   121
by (auto simp add: is_join_def max_def)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   122
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   123
instance linorder \<subseteq> meet_semilorder
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   124
proof
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   125
  from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   126
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   127
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   128
instance linorder \<subseteq> join_semilorder
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   129
proof
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   130
  from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   131
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   132
    
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   133
instance linorder \<subseteq> lorder ..
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   134
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   135
lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))" 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   136
by (simp add: is_meet_meet is_meet_min is_meet_unique)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   137
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   138
lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   139
by (simp add: is_join_join is_join_max is_join_unique)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   140
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   141
lemma meet_idempotent[simp]: "meet x x = x"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   142
by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   143
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   144
lemma join_idempotent[simp]: "join x x = x"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   145
by (rule order_antisym, simp_all add: join_left_le join_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   146
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   147
lemma meet_comm: "meet x y = meet y x" 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   148
by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   149
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   150
lemma join_comm: "join x y = join y x"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   151
by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   152
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   153
lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   154
proof - 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   155
  have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   156
  hence "?l <= x & ?l <= y & ?l <= z" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   157
  hence "?l <= ?r" by (simp add: meet_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   158
  hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   159
  have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)  
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   160
  hence "?r <= x & ?r <= y & ?r <= z" by (auto) 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   161
  hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   162
  hence b:"?r <= ?l" by (simp add: meet_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   163
  from a b show "?l = ?r" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   164
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   165
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   166
lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   167
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   168
  have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   169
  hence "x <= ?l & y <= ?l & z <= ?l" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   170
  hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   171
  hence a:"?r <= ?l" by (simp add: join_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   172
  have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   173
  hence "y <= ?r & z <= ?r & x <= ?r" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   174
  hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   175
  hence b:"?l <= ?r" by (simp add: join_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   176
  from a b show "?l = ?r" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   177
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   178
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   179
lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   180
by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   181
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   182
lemma meet_left_idempotent: "meet y (meet y x) = meet y x"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   183
by (simp add: meet_assoc meet_comm meet_left_comm)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   184
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   185
lemma join_left_comm: "join a (join b c) = join b (join a c)"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   186
by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   187
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   188
lemma join_left_idempotent: "join y (join y x) = join y x"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   189
by (simp add: join_assoc join_comm join_left_comm)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   190
    
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   191
lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   192
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   193
lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   194
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   195
lemma le_def_meet: "(x <= y) = (meet x y = x)" 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   196
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   197
  have u: "x <= y \<longrightarrow> meet x y = x"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   198
  proof 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   199
    assume "x <= y"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   200
    hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   201
    thus "meet x y = x" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   202
  qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   203
  have v:"meet x y = x \<longrightarrow> x <= y" 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   204
  proof 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   205
    have a:"meet x y <= y" by (simp add: meet_right_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   206
    assume "meet x y = x"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   207
    hence "x = meet x y" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   208
    with a show "x <= y" by (auto)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   209
  qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   210
  from u v show ?thesis by blast
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   211
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   212
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   213
lemma le_def_join: "(x <= y) = (join x y = y)" 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   214
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   215
  have u: "x <= y \<longrightarrow> join x y = y"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   216
  proof 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   217
    assume "x <= y"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   218
    hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   219
    thus "join x y = y" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   220
  qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   221
  have v:"join x y = y \<longrightarrow> x <= y" 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   222
  proof 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   223
    have a:"x <= join x y" by (simp add: join_left_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   224
    assume "join x y = y"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   225
    hence "y = join x y" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   226
    with a show "x <= y" by (auto)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   227
  qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   228
  from u v show ?thesis by blast
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   229
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   230
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   231
lemma meet_join_absorp: "meet x (join x y) = x"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   232
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   233
  have a:"meet x (join x y) <= x" by (simp add: meet_left_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   234
  have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   235
  from a b show ?thesis by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   236
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   237
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   238
lemma join_meet_absorp: "join x (meet x y) = x"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   239
proof - 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   240
  have a:"x <= join x (meet x y)" by (simp add: join_left_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   241
  have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   242
  from a b show ?thesis by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   243
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   244
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   245
lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   246
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   247
  assume a: "y <= z"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   248
  have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   249
  with a have "meet x y <= x & meet x y <= z" by auto 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   250
  thus "meet x y <= meet x z" by (simp add: meet_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   251
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   252
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   253
lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   254
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   255
  assume a: "y \<le> z"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   256
  have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   257
  with a have "x <= join x z & y <= join x z" by auto
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   258
  thus "join x y <= join x z" by (simp add: join_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   259
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   260
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   261
lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   262
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   263
  have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   264
  from meet_join_le have b: "meet y z <= ?r" 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   265
    by (rule_tac meet_imp_le, (blast intro: order_trans)+)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   266
  from a b show ?thesis by (simp add: join_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   267
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   268
  
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   269
lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _") 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   270
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   271
  have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   272
  from meet_join_le have b: "?l <= join y z" 
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   273
    by (rule_tac join_imp_le, (blast intro: order_trans)+)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   274
  from a b show ?thesis by (simp add: meet_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   275
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   276
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   277
lemma meet_join_eq_imp_le: "a = c \<or> a = d \<or> b = c \<or> b = d \<Longrightarrow> meet a b \<le> join c d"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   278
by (insert meet_join_le, blast intro: order_trans)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   279
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   280
lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   281
proof -
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   282
  assume a: "x <= z"
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   283
  have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   284
  have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   285
  from b c show ?thesis by (simp add: meet_imp_le)
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   286
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   287
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   288
ML {*
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   289
val is_meet_unique = thm "is_meet_unique";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   290
val is_join_unique = thm "is_join_unique";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   291
val join_exists = thm "join_exists";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   292
val meet_exists = thm "meet_exists";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   293
val is_meet_meet = thm "is_meet_meet";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   294
val meet_unique = thm "meet_unique";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   295
val is_join_join = thm "is_join_join";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   296
val join_unique = thm "join_unique";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   297
val meet_left_le = thm "meet_left_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   298
val meet_right_le = thm "meet_right_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   299
val meet_imp_le = thm "meet_imp_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   300
val join_left_le = thm "join_left_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   301
val join_right_le = thm "join_right_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   302
val join_imp_le = thm "join_imp_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   303
val meet_join_le = thms "meet_join_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   304
val is_meet_min = thm "is_meet_min";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   305
val is_join_max = thm "is_join_max";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   306
val meet_min = thm "meet_min";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   307
val join_max = thm "join_max";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   308
val meet_idempotent = thm "meet_idempotent";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   309
val join_idempotent = thm "join_idempotent";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   310
val meet_comm = thm "meet_comm";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   311
val join_comm = thm "join_comm";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   312
val meet_assoc = thm "meet_assoc";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   313
val join_assoc = thm "join_assoc";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   314
val meet_left_comm = thm "meet_left_comm";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   315
val meet_left_idempotent = thm "meet_left_idempotent";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   316
val join_left_comm = thm "join_left_comm";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   317
val join_left_idempotent = thm "join_left_idempotent";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   318
val meet_aci = thms "meet_aci";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   319
val join_aci = thms "join_aci";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   320
val le_def_meet = thm "le_def_meet";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   321
val le_def_join = thm "le_def_join";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   322
val meet_join_absorp = thm "meet_join_absorp";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   323
val join_meet_absorp = thm "join_meet_absorp";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   324
val meet_mono = thm "meet_mono";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   325
val join_mono = thm "join_mono";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   326
val distrib_join_le = thm "distrib_join_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   327
val distrib_meet_le = thm "distrib_meet_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   328
val meet_join_eq_imp_le = thm "meet_join_eq_imp_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   329
val modular_le = thm "modular_le";
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   330
*}
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents:
diff changeset
   331
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15010
diff changeset
   332
end