improved syntax;
authorwenzelm
Sat May 01 22:05:05 2004 +0200 (2004-05-01)
changeset 146934deda204e1d8
parent 14692 b8d6c395c9e2
child 14694 49873d345a39
improved syntax;
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Lattice.thy
     1.1 --- a/src/HOL/Algebra/Group.thy	Sat May 01 22:04:14 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sat May 01 22:05:05 2004 +0200
     1.3 @@ -42,10 +42,10 @@
     1.4    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
     1.5  
     1.6  defs (overloaded)
     1.7 -  nat_pow_def: "pow G a n == nat_rec (one G) (%u b. mult G b a) n"
     1.8 +  nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
     1.9    int_pow_def: "pow G a z ==
    1.10 -    let p = nat_rec (one G) (%u b. mult G b a)
    1.11 -    in if neg z then m_inv G (p (nat (-z))) else p (nat z)"
    1.12 +    let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    1.13 +    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
    1.14  
    1.15  locale magma = struct G +
    1.16    assumes m_closed [intro, simp]:
    1.17 @@ -62,14 +62,15 @@
    1.18      and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
    1.19  
    1.20  lemma monoidI:
    1.21 +  includes struct G
    1.22    assumes m_closed:
    1.23 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
    1.24 -    and one_closed: "one G \<in> carrier G"
    1.25 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    1.26 +    and one_closed: "\<one> \<in> carrier G"
    1.27      and m_assoc:
    1.28        "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.29 -      mult G (mult G x y) z = mult G x (mult G y z)"
    1.30 -    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
    1.31 -    and r_one: "!!x. x \<in> carrier G ==> mult G x (one G) = x"
    1.32 +      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    1.33 +    and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
    1.34 +    and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
    1.35    shows "monoid G"
    1.36    by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
    1.37      semigroup.intro monoid_axioms.intro
    1.38 @@ -80,8 +81,8 @@
    1.39    by (unfold Units_def) fast
    1.40  
    1.41  lemma (in monoid) inv_unique:
    1.42 -  assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>"
    1.43 -    and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
    1.44 +  assumes eq: "y \<otimes> x = \<one>"  "x \<otimes> y' = \<one>"
    1.45 +    and G: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
    1.46    shows "y = y'"
    1.47  proof -
    1.48    from G eq have "y = y \<otimes> (x \<otimes> y')" by simp
    1.49 @@ -129,13 +130,13 @@
    1.50     (x \<otimes> y = x \<otimes> z) = (y = z)"
    1.51  proof
    1.52    assume eq: "x \<otimes> y = x \<otimes> z"
    1.53 -    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
    1.54 +    and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
    1.55    then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
    1.56      by (simp add: m_assoc Units_closed)
    1.57    with G show "y = z" by (simp add: Units_l_inv)
    1.58  next
    1.59    assume eq: "y = z"
    1.60 -    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
    1.61 +    and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
    1.62    then show "x \<otimes> y = x \<otimes> z" by simp
    1.63  qed
    1.64  
    1.65 @@ -152,14 +153,14 @@
    1.66    "inj_on (m_inv G) (Units G)"
    1.67  proof (rule inj_onI)
    1.68    fix x y
    1.69 -  assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y"
    1.70 +  assume G: "x \<in> Units G"  "y \<in> Units G" and eq: "inv x = inv y"
    1.71    then have "inv (inv x) = inv (inv y)" by simp
    1.72    with G show "x = y" by simp
    1.73  qed
    1.74  
    1.75  lemma (in monoid) Units_inv_comm:
    1.76    assumes inv: "x \<otimes> y = \<one>"
    1.77 -    and G: "x \<in> Units G" "y \<in> Units G"
    1.78 +    and G: "x \<in> Units G"  "y \<in> Units G"
    1.79    shows "y \<otimes> x = \<one>"
    1.80  proof -
    1.81    from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed)
    1.82 @@ -200,59 +201,58 @@
    1.83    assumes Units: "carrier G <= Units G"
    1.84  
    1.85  theorem groupI:
    1.86 +  includes struct G
    1.87    assumes m_closed [simp]:
    1.88 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
    1.89 -    and one_closed [simp]: "one G \<in> carrier G"
    1.90 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    1.91 +    and one_closed [simp]: "\<one> \<in> carrier G"
    1.92      and m_assoc:
    1.93        "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.94 -      mult G (mult G x y) z = mult G x (mult G y z)"
    1.95 -    and l_one [simp]: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
    1.96 -    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
    1.97 +      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    1.98 +    and l_one [simp]: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
    1.99 +    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
   1.100    shows "group G"
   1.101  proof -
   1.102    have l_cancel [simp]:
   1.103      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.104 -    (mult G x y = mult G x z) = (y = z)"
   1.105 +    (x \<otimes> y = x \<otimes> z) = (y = z)"
   1.106    proof
   1.107      fix x y z
   1.108 -    assume eq: "mult G x y = mult G x z"
   1.109 -      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.110 +    assume eq: "x \<otimes> y = x \<otimes> z"
   1.111 +      and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   1.112      with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
   1.113 -      and l_inv: "mult G x_inv x = one G" by fast
   1.114 -    from G eq xG have "mult G (mult G x_inv x) y = mult G (mult G x_inv x) z"
   1.115 +      and l_inv: "x_inv \<otimes> x = \<one>" by fast
   1.116 +    from G eq xG have "(x_inv \<otimes> x) \<otimes> y = (x_inv \<otimes> x) \<otimes> z"
   1.117        by (simp add: m_assoc)
   1.118      with G show "y = z" by (simp add: l_inv)
   1.119    next
   1.120      fix x y z
   1.121      assume eq: "y = z"
   1.122 -      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.123 -    then show "mult G x y = mult G x z" by simp
   1.124 +      and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   1.125 +    then show "x \<otimes> y = x \<otimes> z" by simp
   1.126    qed
   1.127    have r_one:
   1.128 -    "!!x. x \<in> carrier G ==> mult G x (one G) = x"
   1.129 +    "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
   1.130    proof -
   1.131      fix x
   1.132      assume x: "x \<in> carrier G"
   1.133      with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
   1.134 -      and l_inv: "mult G x_inv x = one G" by fast
   1.135 -    from x xG have "mult G x_inv (mult G x (one G)) = mult G x_inv x"
   1.136 +      and l_inv: "x_inv \<otimes> x = \<one>" by fast
   1.137 +    from x xG have "x_inv \<otimes> (x \<otimes> \<one>) = x_inv \<otimes> x"
   1.138        by (simp add: m_assoc [symmetric] l_inv)
   1.139 -    with x xG show "mult G x (one G) = x" by simp 
   1.140 +    with x xG show "x \<otimes> \<one> = x" by simp
   1.141    qed
   1.142    have inv_ex:
   1.143 -    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G &
   1.144 -      mult G x y = one G"
   1.145 +    "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
   1.146    proof -
   1.147      fix x
   1.148      assume x: "x \<in> carrier G"
   1.149      with l_inv_ex obtain y where y: "y \<in> carrier G"
   1.150 -      and l_inv: "mult G y x = one G" by fast
   1.151 -    from x y have "mult G y (mult G x y) = mult G y (one G)"
   1.152 +      and l_inv: "y \<otimes> x = \<one>" by fast
   1.153 +    from x y have "y \<otimes> (x \<otimes> y) = y \<otimes> \<one>"
   1.154        by (simp add: m_assoc [symmetric] l_inv r_one)
   1.155 -    with x y have r_inv: "mult G x y = one G"
   1.156 +    with x y have r_inv: "x \<otimes> y = \<one>"
   1.157        by simp
   1.158 -    from x y show "EX y : carrier G. mult G y x = one G &
   1.159 -      mult G x y = one G"
   1.160 +    from x y show "EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
   1.161        by (fast intro: l_inv r_inv)
   1.162    qed
   1.163    then have carrier_subset_Units: "carrier G <= Units G"
   1.164 @@ -265,7 +265,7 @@
   1.165  
   1.166  lemma (in monoid) monoid_groupI:
   1.167    assumes l_inv_ex:
   1.168 -    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
   1.169 +    "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
   1.170    shows "group G"
   1.171    by (rule groupI) (auto intro: m_assoc l_inv_ex)
   1.172  
   1.173 @@ -306,13 +306,13 @@
   1.174     (y \<otimes> x = z \<otimes> x) = (y = z)"
   1.175  proof
   1.176    assume eq: "y \<otimes> x = z \<otimes> x"
   1.177 -    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.178 +    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   1.179    then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
   1.180      by (simp add: m_assoc [symmetric])
   1.181    with G show "y = z" by (simp add: r_inv)
   1.182  next
   1.183    assume eq: "y = z"
   1.184 -    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.185 +    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   1.186    then show "y \<otimes> x = z \<otimes> x" by simp
   1.187  qed
   1.188  
   1.189 @@ -335,7 +335,7 @@
   1.190  lemma (in group) inv_mult_group:
   1.191    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
   1.192  proof -
   1.193 -  assume G: "x \<in> carrier G" "y \<in> carrier G"
   1.194 +  assume G: "x \<in> carrier G"  "y \<in> carrier G"
   1.195    then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
   1.196      by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
   1.197    with G show ?thesis by simp
   1.198 @@ -343,14 +343,14 @@
   1.199  
   1.200  lemma (in group) inv_comm:
   1.201    "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
   1.202 -  by (rule Units_inv_comm) auto                          
   1.203 +  by (rule Units_inv_comm) auto
   1.204  
   1.205  lemma (in group) inv_equality:
   1.206       "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
   1.207  apply (simp add: m_inv_def)
   1.208  apply (rule the_equality)
   1.209 - apply (simp add: inv_comm [of y x]) 
   1.210 -apply (rule r_cancel [THEN iffD1], auto) 
   1.211 + apply (simp add: inv_comm [of y x])
   1.212 +apply (rule r_cancel [THEN iffD1], auto)
   1.213  done
   1.214  
   1.215  text {* Power *}
   1.216 @@ -493,10 +493,10 @@
   1.217  constdefs (structure G and H)
   1.218    DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup"  (infixr "\<times>\<^sub>s" 80)
   1.219    "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
   1.220 -    mult = (%(xg, xh) (yg, yh). (xg \<otimes> yg, xh \<otimes>\<^sub>2 yh)) |)"
   1.221 +    mult = (%(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')) |)"
   1.222  
   1.223    DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid"  (infixr "\<times>\<^sub>g" 80)
   1.224 -  "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>, \<one>\<^sub>2) |)"
   1.225 +  "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>) |)"
   1.226  
   1.227  lemma DirProdSemigroup_magma:
   1.228    includes magma G + magma H
   1.229 @@ -550,18 +550,18 @@
   1.230    by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   1.231  
   1.232  lemma one_DirProdGroup [simp]:
   1.233 -     "one (G \<times>\<^sub>g H) = (one G, one H)"
   1.234 +     "\<one>\<^bsub>(G \<times>\<^sub>g H)\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
   1.235    by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   1.236  
   1.237  lemma mult_DirProdGroup [simp]:
   1.238 -     "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
   1.239 +     "(g, h) \<otimes>\<^bsub>(G \<times>\<^sub>g H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
   1.240    by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   1.241  
   1.242  lemma inv_DirProdGroup [simp]:
   1.243    includes group G + group H
   1.244    assumes g: "g \<in> carrier G"
   1.245        and h: "h \<in> carrier H"
   1.246 -  shows "m_inv (G \<times>\<^sub>g H) (g, h) = (m_inv G g, m_inv H h)"
   1.247 +  shows "m_inv (G \<times>\<^sub>g H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
   1.248    apply (rule group.inv_equality [OF DirProdGroup_group])
   1.249    apply (simp_all add: prems group_def group.l_inv)
   1.250    done
   1.251 @@ -572,7 +572,7 @@
   1.252    hom :: "_ => _ => ('a => 'b) set"
   1.253    "hom G H ==
   1.254      {h. h \<in> carrier G -> carrier H &
   1.255 -      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes> y) = h x \<otimes>\<^sub>2 h y)}"
   1.256 +      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
   1.257  
   1.258  lemma (in semigroup) hom:
   1.259    includes semigroup G
   1.260 @@ -586,9 +586,9 @@
   1.261  qed
   1.262  
   1.263  lemma hom_mult:
   1.264 -  "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |] 
   1.265 -   ==> h (mult G x y) = mult H (h x) (h y)"
   1.266 -  by (simp add: hom_def) 
   1.267 +  "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
   1.268 +   ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
   1.269 +  by (simp add: hom_def)
   1.270  
   1.271  lemma hom_closed:
   1.272    "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
   1.273 @@ -598,9 +598,9 @@
   1.274       "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|]
   1.275        ==> compose (carrier G) h h' \<in> hom G G"
   1.276  apply (simp (no_asm_simp) add: hom_def)
   1.277 -apply (intro conjI) 
   1.278 +apply (intro conjI)
   1.279   apply (force simp add: funcset_compose hom_def)
   1.280 -apply (simp add: compose_def group.axioms hom_mult funcset_mem) 
   1.281 +apply (simp add: compose_def group.axioms hom_mult funcset_mem)
   1.282  done
   1.283  
   1.284  locale group_hom = group G + group H + var h +
   1.285 @@ -613,9 +613,9 @@
   1.286    by simp
   1.287  
   1.288  lemma (in group_hom) hom_one [simp]:
   1.289 -  "h \<one> = \<one>\<^sub>2"
   1.290 +  "h \<one> = \<one>\<^bsub>H\<^esub>"
   1.291  proof -
   1.292 -  have "h \<one> \<otimes>\<^sub>2 \<one>\<^sub>2 = h \<one> \<otimes>\<^sub>2 h \<one>"
   1.293 +  have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^sub>2 h \<one>"
   1.294      by (simp add: hom_mult [symmetric] del: hom_mult)
   1.295    then show ?thesis by (simp del: r_one)
   1.296  qed
   1.297 @@ -625,14 +625,14 @@
   1.298    by simp
   1.299  
   1.300  lemma (in group_hom) hom_inv [simp]:
   1.301 -  "x \<in> carrier G ==> h (inv x) = inv\<^sub>2 (h x)"
   1.302 +  "x \<in> carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)"
   1.303  proof -
   1.304    assume x: "x \<in> carrier G"
   1.305 -  then have "h x \<otimes>\<^sub>2 h (inv x) = \<one>\<^sub>2"
   1.306 +  then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>"
   1.307      by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
   1.308 -  also from x have "... = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)"
   1.309 +  also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
   1.310      by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
   1.311 -  finally have "h x \<otimes>\<^sub>2 h (inv x) = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)" .
   1.312 +  finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
   1.313    with x show ?thesis by simp
   1.314  qed
   1.315  
   1.316 @@ -653,7 +653,7 @@
   1.317    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.318     x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   1.319  proof -
   1.320 -  assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.321 +  assume xyz: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   1.322    from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc)
   1.323    also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm)
   1.324    also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc)
   1.325 @@ -665,15 +665,16 @@
   1.326  locale comm_monoid = comm_semigroup + monoid
   1.327  
   1.328  lemma comm_monoidI:
   1.329 +  includes struct G
   1.330    assumes m_closed:
   1.331 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
   1.332 -    and one_closed: "one G \<in> carrier G"
   1.333 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
   1.334 +    and one_closed: "\<one> \<in> carrier G"
   1.335      and m_assoc:
   1.336        "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.337 -      mult G (mult G x y) z = mult G x (mult G y z)"
   1.338 -    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
   1.339 +      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
   1.340 +    and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
   1.341      and m_comm:
   1.342 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
   1.343 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   1.344    shows "comm_monoid G"
   1.345    using l_one
   1.346    by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
   1.347 @@ -682,20 +683,17 @@
   1.348  
   1.349  lemma (in monoid) monoid_comm_monoidI:
   1.350    assumes m_comm:
   1.351 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
   1.352 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   1.353    shows "comm_monoid G"
   1.354    by (rule comm_monoidI) (auto intro: m_assoc m_comm)
   1.355 -(*
   1.356 -lemma (in comm_monoid) r_one [simp]:
   1.357 +(*lemma (in comm_monoid) r_one [simp]:
   1.358    "x \<in> carrier G ==> x \<otimes> \<one> = x"
   1.359  proof -
   1.360    assume G: "x \<in> carrier G"
   1.361    then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
   1.362    also from G have "... = x" by simp
   1.363    finally show ?thesis .
   1.364 -qed
   1.365 -*)
   1.366 -
   1.367 +qed*)
   1.368  lemma (in comm_monoid) nat_pow_distr:
   1.369    "[| x \<in> carrier G; y \<in> carrier G |] ==>
   1.370    (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
   1.371 @@ -705,22 +703,23 @@
   1.372  
   1.373  lemma (in group) group_comm_groupI:
   1.374    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
   1.375 -      mult G x y = mult G y x"
   1.376 +      x \<otimes> y = y \<otimes> x"
   1.377    shows "comm_group G"
   1.378    by (fast intro: comm_group.intro comm_semigroup_axioms.intro
   1.379      group.axioms prems)
   1.380  
   1.381  lemma comm_groupI:
   1.382 +  includes struct G
   1.383    assumes m_closed:
   1.384 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
   1.385 -    and one_closed: "one G \<in> carrier G"
   1.386 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
   1.387 +    and one_closed: "\<one> \<in> carrier G"
   1.388      and m_assoc:
   1.389        "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.390 -      mult G (mult G x y) z = mult G x (mult G y z)"
   1.391 +      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
   1.392      and m_comm:
   1.393 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
   1.394 -    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
   1.395 -    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
   1.396 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   1.397 +    and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
   1.398 +    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
   1.399    shows "comm_group G"
   1.400    by (fast intro: group.group_comm_groupI groupI prems)
   1.401  
     2.1 --- a/src/HOL/Algebra/Lattice.thy	Sat May 01 22:04:14 2004 +0200
     2.2 +++ b/src/HOL/Algebra/Lattice.thy	Sat May 01 22:05:05 2004 +0200
     2.3 @@ -14,9 +14,7 @@
     2.4  record 'a order = "'a partial_object" +
     2.5    le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
     2.6  
     2.7 -locale order_syntax = struct L
     2.8 -
     2.9 -locale partial_order = order_syntax +
    2.10 +locale partial_order = struct L +
    2.11    assumes refl [intro, simp]:
    2.12                    "x \<in> carrier L ==> x \<sqsubseteq> x"
    2.13      and anti_sym [intro]:
    2.14 @@ -31,19 +29,19 @@
    2.15  
    2.16    -- {* Upper and lower bounds of a set. *}
    2.17    Upper :: "[_, 'a set] => 'a set"
    2.18 -  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> le L x u)} \<inter>
    2.19 +  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>
    2.20                  carrier L"
    2.21  
    2.22    Lower :: "[_, 'a set] => 'a set"
    2.23 -  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> le L l x)} \<inter>
    2.24 +  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>
    2.25                  carrier L"
    2.26  
    2.27    -- {* Least and greatest, as predicate. *}
    2.28    least :: "[_, 'a, 'a set] => bool"
    2.29 -  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. le L l x)"
    2.30 +  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
    2.31  
    2.32    greatest :: "[_, 'a, 'a set] => bool"
    2.33 -  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. le L x g)"
    2.34 +  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
    2.35  
    2.36    -- {* Supremum and infimum *}
    2.37    sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
    2.38 @@ -66,14 +64,14 @@
    2.39    by (unfold Upper_def) clarify
    2.40  
    2.41  lemma UpperD [dest]:
    2.42 -  includes order_syntax
    2.43 +  includes struct L
    2.44    shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
    2.45 -  by (unfold Upper_def) blast 
    2.46 +  by (unfold Upper_def) blast
    2.47  
    2.48  lemma Upper_memI:
    2.49 -  includes order_syntax
    2.50 +  includes struct L
    2.51    shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
    2.52 -  by (unfold Upper_def) blast 
    2.53 +  by (unfold Upper_def) blast
    2.54  
    2.55  lemma Upper_antimono:
    2.56    "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
    2.57 @@ -87,14 +85,14 @@
    2.58    by (unfold Lower_def) clarify
    2.59  
    2.60  lemma LowerD [dest]:
    2.61 -  includes order_syntax
    2.62 +  includes struct L
    2.63    shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
    2.64 -  by (unfold Lower_def) blast 
    2.65 +  by (unfold Lower_def) blast
    2.66  
    2.67  lemma Lower_memI:
    2.68 -  includes order_syntax
    2.69 +  includes struct L
    2.70    shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
    2.71 -  by (unfold Lower_def) blast 
    2.72 +  by (unfold Lower_def) blast
    2.73  
    2.74  lemma Lower_antimono:
    2.75    "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
    2.76 @@ -116,22 +114,21 @@
    2.77    by (unfold least_def) blast
    2.78  
    2.79  lemma least_le:
    2.80 -  includes order_syntax
    2.81 +  includes struct L
    2.82    shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
    2.83    by (unfold least_def) fast
    2.84  
    2.85  lemma least_UpperI:
    2.86 -  includes order_syntax
    2.87 +  includes struct L
    2.88    assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
    2.89      and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
    2.90 -    and L: "A \<subseteq> carrier L" "s \<in> carrier L"
    2.91 +    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
    2.92    shows "least L s (Upper L A)"
    2.93 -proof (unfold least_def, intro conjI)
    2.94 -  show "Upper L A \<subseteq> carrier L" by simp
    2.95 -next
    2.96 -  from above L show "s \<in> Upper L A" by (simp add: Upper_def)
    2.97 -next
    2.98 -  from below show "ALL x : Upper L A. s \<sqsubseteq> x" by fast
    2.99 +proof -
   2.100 +  have "Upper L A \<subseteq> carrier L" by simp
   2.101 +  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
   2.102 +  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
   2.103 +  ultimately show ?thesis by (simp add: least_def)
   2.104  qed
   2.105  
   2.106  
   2.107 @@ -150,24 +147,24 @@
   2.108    by (unfold greatest_def) blast
   2.109  
   2.110  lemma greatest_le:
   2.111 -  includes order_syntax
   2.112 +  includes struct L
   2.113    shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   2.114    by (unfold greatest_def) fast
   2.115  
   2.116  lemma greatest_LowerI:
   2.117 -  includes order_syntax
   2.118 +  includes struct L
   2.119    assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   2.120      and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   2.121 -    and L: "A \<subseteq> carrier L" "i \<in> carrier L"
   2.122 +    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   2.123    shows "greatest L i (Lower L A)"
   2.124 -proof (unfold greatest_def, intro conjI)
   2.125 -  show "Lower L A \<subseteq> carrier L" by simp
   2.126 -next
   2.127 -  from below L show "i \<in> Lower L A" by (simp add: Lower_def)
   2.128 -next
   2.129 -  from above show "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   2.130 +proof -
   2.131 +  have "Lower L A \<subseteq> carrier L" by simp
   2.132 +  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
   2.133 +  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   2.134 +  ultimately show ?thesis by (simp add: greatest_def)
   2.135  qed
   2.136  
   2.137 +
   2.138  subsection {* Lattices *}
   2.139  
   2.140  locale lattice = partial_order +
   2.141 @@ -177,12 +174,12 @@
   2.142      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   2.143  
   2.144  lemma least_Upper_above:
   2.145 -  includes order_syntax
   2.146 +  includes struct L
   2.147    shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   2.148    by (unfold least_def) blast
   2.149  
   2.150  lemma greatest_Lower_above:
   2.151 -  includes order_syntax
   2.152 +  includes struct L
   2.153    shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   2.154    by (unfold greatest_def) blast
   2.155  
   2.156 @@ -193,11 +190,11 @@
   2.157    "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   2.158    ==> P (x \<squnion> y)"
   2.159  proof (unfold join_def sup_def)
   2.160 -  assume L: "x \<in> carrier L" "y \<in> carrier L"
   2.161 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   2.162      and P: "!!l. least L l (Upper L {x, y}) ==> P l"
   2.163    with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   2.164    with L show "P (THE l. least L l (Upper L {x, y}))"
   2.165 -  by (fast intro: theI2 least_unique P)
   2.166 +    by (fast intro: theI2 least_unique P)
   2.167  qed
   2.168  
   2.169  lemma (in lattice) join_closed [simp]:
   2.170 @@ -209,8 +206,8 @@
   2.171    by (rule least_UpperI) fast+
   2.172  
   2.173  lemma (in partial_order) sup_of_singleton [simp]:
   2.174 -  includes order_syntax
   2.175 -  shows "x \<in> carrier L ==> \<Squnion> {x} = x"
   2.176 +  includes struct L
   2.177 +  shows "x \<in> carrier L ==> \<Squnion>{x} = x"
   2.178    by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
   2.179  
   2.180  
   2.181 @@ -219,129 +216,104 @@
   2.182  lemma (in lattice) sup_insertI:
   2.183    "[| !!s. least L s (Upper L (insert x A)) ==> P s;
   2.184    least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   2.185 -  ==> P (\<Squnion> (insert x A))"
   2.186 +  ==> P (\<Squnion>(insert x A))"
   2.187  proof (unfold sup_def)
   2.188 -  assume L: "x \<in> carrier L" "A \<subseteq> carrier L"
   2.189 +  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   2.190      and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   2.191      and least_a: "least L a (Upper L A)"
   2.192    from L least_a have La: "a \<in> carrier L" by simp
   2.193    from L sup_of_two_exists least_a
   2.194    obtain s where least_s: "least L s (Upper L {a, x})" by blast
   2.195    show "P (THE l. least L l (Upper L (insert x A)))"
   2.196 -  proof (rule theI2 [where a = s])
   2.197 +  proof (rule theI2)
   2.198      show "least L s (Upper L (insert x A))"
   2.199      proof (rule least_UpperI)
   2.200        fix z
   2.201 -      assume xA: "z \<in> insert x A"
   2.202 -      show "z \<sqsubseteq> s"
   2.203 -      proof -
   2.204 -	{
   2.205 -	  assume "z = x" then have ?thesis
   2.206 -	    by (simp add: least_Upper_above [OF least_s] L La)
   2.207 -        }
   2.208 -	moreover
   2.209 -        {
   2.210 -	  assume "z \<in> A"
   2.211 -          with L least_s least_a have ?thesis
   2.212 -	    by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
   2.213 -        }
   2.214 -      moreover note xA
   2.215 -      ultimately show ?thesis by blast
   2.216 +      assume "z \<in> insert x A"
   2.217 +      then show "z \<sqsubseteq> s"
   2.218 +      proof
   2.219 +        assume "z = x" then show ?thesis
   2.220 +          by (simp add: least_Upper_above [OF least_s] L La)
   2.221 +      next
   2.222 +        assume "z \<in> A"
   2.223 +        with L least_s least_a show ?thesis
   2.224 +          by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
   2.225 +      qed
   2.226 +    next
   2.227 +      fix y
   2.228 +      assume y: "y \<in> Upper L (insert x A)"
   2.229 +      show "s \<sqsubseteq> y"
   2.230 +      proof (rule least_le [OF least_s], rule Upper_memI)
   2.231 +	fix z
   2.232 +	assume z: "z \<in> {a, x}"
   2.233 +	then show "z \<sqsubseteq> y"
   2.234 +	proof
   2.235 +          have y': "y \<in> Upper L A"
   2.236 +            apply (rule subsetD [where A = "Upper L (insert x A)"])
   2.237 +            apply (rule Upper_antimono) apply clarify apply assumption
   2.238 +            done
   2.239 +          assume "z = a"
   2.240 +          with y' least_a show ?thesis by (fast dest: least_le)
   2.241 +	next
   2.242 +	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
   2.243 +          with y L show ?thesis by blast
   2.244 +	qed
   2.245 +      qed (rule Upper_closed [THEN subsetD])
   2.246 +    next
   2.247 +      from L show "insert x A \<subseteq> carrier L" by simp
   2.248 +      from least_s show "s \<in> carrier L" by simp
   2.249      qed
   2.250    next
   2.251 -    fix y
   2.252 -    assume y: "y \<in> Upper L (insert x A)"
   2.253 -    show "s \<sqsubseteq> y"
   2.254 -    proof (rule least_le [OF least_s], rule Upper_memI)
   2.255 -      fix z
   2.256 -      assume z: "z \<in> {a, x}"
   2.257 -      show "z \<sqsubseteq> y"
   2.258 -      proof -
   2.259 -	{
   2.260 -          have y': "y \<in> Upper L A"
   2.261 -	    apply (rule subsetD [where A = "Upper L (insert x A)"])
   2.262 -	    apply (rule Upper_antimono) apply clarify apply assumption
   2.263 -	    done
   2.264 -	  assume "z = a"
   2.265 -	  with y' least_a have ?thesis by (fast dest: least_le)
   2.266 -        }
   2.267 -	moreover
   2.268 -	{
   2.269 -           assume "z = x"
   2.270 -           with y L have ?thesis by blast
   2.271 -        }
   2.272 -        moreover note z
   2.273 -        ultimately show ?thesis by blast
   2.274 -      qed
   2.275 -    qed (rule Upper_closed [THEN subsetD])
   2.276 -  next
   2.277 -    from L show "insert x A \<subseteq> carrier L" by simp
   2.278 -  next
   2.279 -    from least_s show "s \<in> carrier L" by simp
   2.280 -  qed
   2.281 -next
   2.282      fix l
   2.283      assume least_l: "least L l (Upper L (insert x A))"
   2.284      show "l = s"
   2.285      proof (rule least_unique)
   2.286        show "least L s (Upper L (insert x A))"
   2.287        proof (rule least_UpperI)
   2.288 -	fix z
   2.289 -	assume xA: "z \<in> insert x A"
   2.290 -	show "z \<sqsubseteq> s"
   2.291 -      proof -
   2.292 -	{
   2.293 -	  assume "z = x" then have ?thesis
   2.294 -	    by (simp add: least_Upper_above [OF least_s] L La)
   2.295 -        }
   2.296 -	moreover
   2.297 -        {
   2.298 -	  assume "z \<in> A"
   2.299 -          with L least_s least_a have ?thesis
   2.300 -	    by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
   2.301 -        }
   2.302 -	  moreover note xA
   2.303 -	  ultimately show ?thesis by blast
   2.304 +        fix z
   2.305 +        assume "z \<in> insert x A"
   2.306 +        then show "z \<sqsubseteq> s"
   2.307 +	proof
   2.308 +          assume "z = x" then show ?thesis
   2.309 +            by (simp add: least_Upper_above [OF least_s] L La)
   2.310 +	next
   2.311 +          assume "z \<in> A"
   2.312 +          with L least_s least_a show ?thesis
   2.313 +            by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
   2.314  	qed
   2.315        next
   2.316 -	fix y
   2.317 -	assume y: "y \<in> Upper L (insert x A)"
   2.318 -	show "s \<sqsubseteq> y"
   2.319 -	proof (rule least_le [OF least_s], rule Upper_memI)
   2.320 -	  fix z
   2.321 -	  assume z: "z \<in> {a, x}"
   2.322 -	  show "z \<sqsubseteq> y"
   2.323 -	  proof -
   2.324 -	    {
   2.325 -          have y': "y \<in> Upper L A"
   2.326 -	    apply (rule subsetD [where A = "Upper L (insert x A)"])
   2.327 -	    apply (rule Upper_antimono) apply clarify apply assumption
   2.328 -	    done
   2.329 -	  assume "z = a"
   2.330 -	  with y' least_a have ?thesis by (fast dest: least_le)
   2.331 -        }
   2.332 -	moreover
   2.333 -	{
   2.334 -           assume "z = x"
   2.335 -           with y L have ?thesis by blast
   2.336 -            }
   2.337 -            moreover note z
   2.338 -            ultimately show ?thesis by blast
   2.339 -	  qed
   2.340 -	qed (rule Upper_closed [THEN subsetD])
   2.341 +        fix y
   2.342 +        assume y: "y \<in> Upper L (insert x A)"
   2.343 +        show "s \<sqsubseteq> y"
   2.344 +        proof (rule least_le [OF least_s], rule Upper_memI)
   2.345 +          fix z
   2.346 +          assume z: "z \<in> {a, x}"
   2.347 +          then show "z \<sqsubseteq> y"
   2.348 +          proof
   2.349 +            have y': "y \<in> Upper L A"
   2.350 +	      apply (rule subsetD [where A = "Upper L (insert x A)"])
   2.351 +	      apply (rule Upper_antimono) apply clarify apply assumption
   2.352 +	      done
   2.353 +            assume "z = a"
   2.354 +            with y' least_a show ?thesis by (fast dest: least_le)
   2.355 +	  next
   2.356 +            assume "z \<in> {x}"
   2.357 +            with y L show ?thesis by blast
   2.358 +          qed
   2.359 +        qed (rule Upper_closed [THEN subsetD])
   2.360        next
   2.361 -	from L show "insert x A \<subseteq> carrier L" by simp
   2.362 -      next
   2.363 -	from least_s show "s \<in> carrier L" by simp
   2.364 +        from L show "insert x A \<subseteq> carrier L" by simp
   2.365 +        from least_s show "s \<in> carrier L" by simp
   2.366        qed
   2.367      qed
   2.368    qed
   2.369  qed
   2.370  
   2.371  lemma (in lattice) finite_sup_least:
   2.372 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion> A) (Upper L A)"
   2.373 +  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
   2.374  proof (induct set: Finites)
   2.375 -  case empty then show ?case by simp
   2.376 +  case empty
   2.377 +  then show ?case by simp
   2.378  next
   2.379    case (insert A x)
   2.380    show ?case
   2.381 @@ -350,16 +322,15 @@
   2.382      with insert show ?thesis by (simp add: sup_of_singletonI)
   2.383    next
   2.384      case False
   2.385 -    from insert show ?thesis
   2.386 -    proof (rule_tac sup_insertI)
   2.387 -      from False insert show "least L (\<Squnion> A) (Upper L A)" by simp
   2.388 -    qed simp_all
   2.389 +    with insert have "least L (\<Squnion>A) (Upper L A)" by simp
   2.390 +    with _ show ?thesis
   2.391 +      by (rule sup_insertI) (simp_all add: insert [simplified])
   2.392    qed
   2.393  qed
   2.394  
   2.395  lemma (in lattice) finite_sup_insertI:
   2.396    assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   2.397 -    and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"
   2.398 +    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   2.399    shows "P (\<Squnion> (insert x A))"
   2.400  proof (cases "A = {}")
   2.401    case True with P and xA show ?thesis
   2.402 @@ -370,44 +341,44 @@
   2.403  qed
   2.404  
   2.405  lemma (in lattice) finite_sup_closed:
   2.406 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion> A \<in> carrier L"
   2.407 +  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
   2.408  proof (induct set: Finites)
   2.409    case empty then show ?case by simp
   2.410  next
   2.411    case (insert A x) then show ?case
   2.412 -    by (rule_tac finite_sup_insertI) (simp_all)
   2.413 +    by - (rule finite_sup_insertI, simp_all)
   2.414  qed
   2.415  
   2.416  lemma (in lattice) join_left:
   2.417    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
   2.418 -  by (rule joinI [folded join_def]) (blast dest: least_mem )
   2.419 +  by (rule joinI [folded join_def]) (blast dest: least_mem)
   2.420  
   2.421  lemma (in lattice) join_right:
   2.422    "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
   2.423 -  by (rule joinI [folded join_def]) (blast dest: least_mem )
   2.424 +  by (rule joinI [folded join_def]) (blast dest: least_mem)
   2.425  
   2.426  lemma (in lattice) sup_of_two_least:
   2.427 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion> {x, y}) (Upper L {x, y})"
   2.428 +  "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
   2.429  proof (unfold sup_def)
   2.430 -  assume L: "x \<in> carrier L" "y \<in> carrier L"
   2.431 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   2.432    with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   2.433    with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"
   2.434    by (fast intro: theI2 least_unique)  (* blast fails *)
   2.435  qed
   2.436  
   2.437  lemma (in lattice) join_le:
   2.438 -  assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z"
   2.439 -    and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
   2.440 +  assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
   2.441 +    and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   2.442    shows "x \<squnion> y \<sqsubseteq> z"
   2.443  proof (rule joinI)
   2.444    fix s
   2.445    assume "least L s (Upper L {x, y})"
   2.446    with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
   2.447  qed
   2.448 -  
   2.449 +
   2.450  lemma (in lattice) join_assoc_lemma:
   2.451 -  assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
   2.452 -  shows "x \<squnion> (y \<squnion> z) = \<Squnion> {x, y, z}"
   2.453 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   2.454 +  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
   2.455  proof (rule finite_sup_insertI)
   2.456    -- {* The textbook argument in Jacobson I, p 457 *}
   2.457    fix s
   2.458 @@ -424,21 +395,22 @@
   2.459  qed (simp_all add: L)
   2.460  
   2.461  lemma join_comm:
   2.462 -  includes order_syntax
   2.463 +  includes struct L
   2.464    shows "x \<squnion> y = y \<squnion> x"
   2.465    by (unfold join_def) (simp add: insert_commute)
   2.466  
   2.467  lemma (in lattice) join_assoc:
   2.468 -  assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
   2.469 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   2.470    shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   2.471  proof -
   2.472    have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
   2.473 -  also from L have "... = \<Squnion> {z, x, y}" by (simp add: join_assoc_lemma)
   2.474 -  also from L have "... = \<Squnion> {x, y, z}" by (simp add: insert_commute)
   2.475 +  also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma)
   2.476 +  also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
   2.477    also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma)
   2.478    finally show ?thesis .
   2.479  qed
   2.480  
   2.481 +
   2.482  subsubsection {* Infimum *}
   2.483  
   2.484  lemma (in lattice) meetI:
   2.485 @@ -446,7 +418,7 @@
   2.486    x \<in> carrier L; y \<in> carrier L |]
   2.487    ==> P (x \<sqinter> y)"
   2.488  proof (unfold meet_def inf_def)
   2.489 -  assume L: "x \<in> carrier L" "y \<in> carrier L"
   2.490 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   2.491      and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
   2.492    with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
   2.493    with L show "P (THE g. greatest L g (Lower L {x, y}))"
   2.494 @@ -462,7 +434,7 @@
   2.495    by (rule greatest_LowerI) fast+
   2.496  
   2.497  lemma (in partial_order) inf_of_singleton [simp]:
   2.498 -  includes order_syntax
   2.499 +  includes struct L
   2.500    shows "x \<in> carrier L ==> \<Sqinter> {x} = x"
   2.501    by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
   2.502  
   2.503 @@ -471,127 +443,101 @@
   2.504  lemma (in lattice) inf_insertI:
   2.505    "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
   2.506    greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   2.507 -  ==> P (\<Sqinter> (insert x A))"
   2.508 +  ==> P (\<Sqinter>(insert x A))"
   2.509  proof (unfold inf_def)
   2.510 -  assume L: "x \<in> carrier L" "A \<subseteq> carrier L"
   2.511 +  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   2.512      and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
   2.513      and greatest_a: "greatest L a (Lower L A)"
   2.514    from L greatest_a have La: "a \<in> carrier L" by simp
   2.515    from L inf_of_two_exists greatest_a
   2.516    obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
   2.517    show "P (THE g. greatest L g (Lower L (insert x A)))"
   2.518 -  proof (rule theI2 [where a = i])
   2.519 +  proof (rule theI2)
   2.520      show "greatest L i (Lower L (insert x A))"
   2.521      proof (rule greatest_LowerI)
   2.522        fix z
   2.523 -      assume xA: "z \<in> insert x A"
   2.524 -      show "i \<sqsubseteq> z"
   2.525 -      proof -
   2.526 -	{
   2.527 -	  assume "z = x" then have ?thesis
   2.528 -	    by (simp add: greatest_Lower_above [OF greatest_i] L La)
   2.529 -        }
   2.530 -	moreover
   2.531 -        {
   2.532 -	  assume "z \<in> A"
   2.533 -          with L greatest_i greatest_a have ?thesis
   2.534 -	    by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)
   2.535 -        }
   2.536 -      moreover note xA
   2.537 -      ultimately show ?thesis by blast
   2.538 +      assume "z \<in> insert x A"
   2.539 +      then show "i \<sqsubseteq> z"
   2.540 +      proof
   2.541 +        assume "z = x" then show ?thesis
   2.542 +          by (simp add: greatest_Lower_above [OF greatest_i] L La)
   2.543 +      next
   2.544 +        assume "z \<in> A"
   2.545 +        with L greatest_i greatest_a show ?thesis
   2.546 +          by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)
   2.547 +      qed
   2.548 +    next
   2.549 +      fix y
   2.550 +      assume y: "y \<in> Lower L (insert x A)"
   2.551 +      show "y \<sqsubseteq> i"
   2.552 +      proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   2.553 +	fix z
   2.554 +	assume z: "z \<in> {a, x}"
   2.555 +	then show "y \<sqsubseteq> z"
   2.556 +	proof
   2.557 +          have y': "y \<in> Lower L A"
   2.558 +            apply (rule subsetD [where A = "Lower L (insert x A)"])
   2.559 +            apply (rule Lower_antimono) apply clarify apply assumption
   2.560 +            done
   2.561 +          assume "z = a"
   2.562 +          with y' greatest_a show ?thesis by (fast dest: greatest_le)
   2.563 +	next
   2.564 +          assume "z \<in> {x}"
   2.565 +          with y L show ?thesis by blast
   2.566 +	qed
   2.567 +      qed (rule Lower_closed [THEN subsetD])
   2.568 +    next
   2.569 +      from L show "insert x A \<subseteq> carrier L" by simp
   2.570 +      from greatest_i show "i \<in> carrier L" by simp
   2.571      qed
   2.572    next
   2.573 -    fix y
   2.574 -    assume y: "y \<in> Lower L (insert x A)"
   2.575 -    show "y \<sqsubseteq> i"
   2.576 -    proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   2.577 -      fix z
   2.578 -      assume z: "z \<in> {a, x}"
   2.579 -      show "y \<sqsubseteq> z"
   2.580 -      proof -
   2.581 -	{
   2.582 -          have y': "y \<in> Lower L A"
   2.583 -	    apply (rule subsetD [where A = "Lower L (insert x A)"])
   2.584 -	    apply (rule Lower_antimono) apply clarify apply assumption
   2.585 -	    done
   2.586 -	  assume "z = a"
   2.587 -	  with y' greatest_a have ?thesis by (fast dest: greatest_le)
   2.588 -        }
   2.589 -	moreover
   2.590 -	{
   2.591 -           assume "z = x"
   2.592 -           with y L have ?thesis by blast
   2.593 -        }
   2.594 -        moreover note z
   2.595 -        ultimately show ?thesis by blast
   2.596 -      qed
   2.597 -    qed (rule Lower_closed [THEN subsetD])
   2.598 -  next
   2.599 -    from L show "insert x A \<subseteq> carrier L" by simp
   2.600 -  next
   2.601 -    from greatest_i show "i \<in> carrier L" by simp
   2.602 -  qed
   2.603 -next
   2.604      fix g
   2.605      assume greatest_g: "greatest L g (Lower L (insert x A))"
   2.606      show "g = i"
   2.607      proof (rule greatest_unique)
   2.608        show "greatest L i (Lower L (insert x A))"
   2.609        proof (rule greatest_LowerI)
   2.610 -	fix z
   2.611 -	assume xA: "z \<in> insert x A"
   2.612 -	show "i \<sqsubseteq> z"
   2.613 -      proof -
   2.614 -	{
   2.615 -	  assume "z = x" then have ?thesis
   2.616 -	    by (simp add: greatest_Lower_above [OF greatest_i] L La)
   2.617 -        }
   2.618 -	moreover
   2.619 -        {
   2.620 -	  assume "z \<in> A"
   2.621 -          with L greatest_i greatest_a have ?thesis
   2.622 -	    by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)
   2.623 -        }
   2.624 -	  moreover note xA
   2.625 -	  ultimately show ?thesis by blast
   2.626 -	qed
   2.627 +        fix z
   2.628 +        assume "z \<in> insert x A"
   2.629 +        then show "i \<sqsubseteq> z"
   2.630 +	proof
   2.631 +          assume "z = x" then show ?thesis
   2.632 +            by (simp add: greatest_Lower_above [OF greatest_i] L La)
   2.633 +	next
   2.634 +          assume "z \<in> A"
   2.635 +          with L greatest_i greatest_a show ?thesis
   2.636 +            by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)
   2.637 +        qed
   2.638        next
   2.639 -	fix y
   2.640 -	assume y: "y \<in> Lower L (insert x A)"
   2.641 -	show "y \<sqsubseteq> i"
   2.642 -	proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   2.643 -	  fix z
   2.644 -	  assume z: "z \<in> {a, x}"
   2.645 -	  show "y \<sqsubseteq> z"
   2.646 -	  proof -
   2.647 -	    {
   2.648 -          have y': "y \<in> Lower L A"
   2.649 -	    apply (rule subsetD [where A = "Lower L (insert x A)"])
   2.650 -	    apply (rule Lower_antimono) apply clarify apply assumption
   2.651 -	    done
   2.652 -	  assume "z = a"
   2.653 -	  with y' greatest_a have ?thesis by (fast dest: greatest_le)
   2.654 -        }
   2.655 -	moreover
   2.656 -	{
   2.657 -           assume "z = x"
   2.658 -           with y L have ?thesis by blast
   2.659 -            }
   2.660 -            moreover note z
   2.661 -            ultimately show ?thesis by blast
   2.662 +        fix y
   2.663 +        assume y: "y \<in> Lower L (insert x A)"
   2.664 +        show "y \<sqsubseteq> i"
   2.665 +        proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   2.666 +          fix z
   2.667 +          assume z: "z \<in> {a, x}"
   2.668 +          then show "y \<sqsubseteq> z"
   2.669 +          proof
   2.670 +            have y': "y \<in> Lower L A"
   2.671 +	      apply (rule subsetD [where A = "Lower L (insert x A)"])
   2.672 +	      apply (rule Lower_antimono) apply clarify apply assumption
   2.673 +	      done
   2.674 +            assume "z = a"
   2.675 +            with y' greatest_a show ?thesis by (fast dest: greatest_le)
   2.676 +	  next
   2.677 +            assume "z \<in> {x}"
   2.678 +            with y L show ?thesis by blast
   2.679  	  qed
   2.680 -	qed (rule Lower_closed [THEN subsetD])
   2.681 +        qed (rule Lower_closed [THEN subsetD])
   2.682        next
   2.683 -	from L show "insert x A \<subseteq> carrier L" by simp
   2.684 -      next
   2.685 -	from greatest_i show "i \<in> carrier L" by simp
   2.686 +        from L show "insert x A \<subseteq> carrier L" by simp
   2.687 +        from greatest_i show "i \<in> carrier L" by simp
   2.688        qed
   2.689      qed
   2.690    qed
   2.691  qed
   2.692  
   2.693  lemma (in lattice) finite_inf_greatest:
   2.694 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter> A) (Lower L A)"
   2.695 +  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
   2.696  proof (induct set: Finites)
   2.697    case empty then show ?case by simp
   2.698  next
   2.699 @@ -604,14 +550,14 @@
   2.700      case False
   2.701      from insert show ?thesis
   2.702      proof (rule_tac inf_insertI)
   2.703 -      from False insert show "greatest L (\<Sqinter> A) (Lower L A)" by simp
   2.704 +      from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
   2.705      qed simp_all
   2.706    qed
   2.707  qed
   2.708  
   2.709  lemma (in lattice) finite_inf_insertI:
   2.710    assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
   2.711 -    and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"
   2.712 +    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   2.713    shows "P (\<Sqinter> (insert x A))"
   2.714  proof (cases "A = {}")
   2.715    case True with P and xA show ?thesis
   2.716 @@ -622,7 +568,7 @@
   2.717  qed
   2.718  
   2.719  lemma (in lattice) finite_inf_closed:
   2.720 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter> A \<in> carrier L"
   2.721 +  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
   2.722  proof (induct set: Finites)
   2.723    case empty then show ?case by simp
   2.724  next
   2.725 @@ -632,17 +578,17 @@
   2.726  
   2.727  lemma (in lattice) meet_left:
   2.728    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
   2.729 -  by (rule meetI [folded meet_def]) (blast dest: greatest_mem )
   2.730 +  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   2.731  
   2.732  lemma (in lattice) meet_right:
   2.733    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
   2.734 -  by (rule meetI [folded meet_def]) (blast dest: greatest_mem )
   2.735 +  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   2.736  
   2.737  lemma (in lattice) inf_of_two_greatest:
   2.738    "[| x \<in> carrier L; y \<in> carrier L |] ==>
   2.739    greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
   2.740  proof (unfold inf_def)
   2.741 -  assume L: "x \<in> carrier L" "y \<in> carrier L"
   2.742 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   2.743    with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
   2.744    with L
   2.745    show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"
   2.746 @@ -650,18 +596,18 @@
   2.747  qed
   2.748  
   2.749  lemma (in lattice) meet_le:
   2.750 -  assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y"
   2.751 -    and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
   2.752 +  assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
   2.753 +    and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   2.754    shows "z \<sqsubseteq> x \<sqinter> y"
   2.755  proof (rule meetI)
   2.756    fix i
   2.757    assume "greatest L i (Lower L {x, y})"
   2.758    with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
   2.759  qed
   2.760 -  
   2.761 +
   2.762  lemma (in lattice) meet_assoc_lemma:
   2.763 -  assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
   2.764 -  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter> {x, y, z}"
   2.765 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   2.766 +  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
   2.767  proof (rule finite_inf_insertI)
   2.768    txt {* The textbook argument in Jacobson I, p 457 *}
   2.769    fix i
   2.770 @@ -678,12 +624,12 @@
   2.771  qed (simp_all add: L)
   2.772  
   2.773  lemma meet_comm:
   2.774 -  includes order_syntax
   2.775 +  includes struct L
   2.776    shows "x \<sqinter> y = y \<sqinter> x"
   2.777    by (unfold meet_def) (simp add: insert_commute)
   2.778  
   2.779  lemma (in lattice) meet_assoc:
   2.780 -  assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
   2.781 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   2.782    shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   2.783  proof -
   2.784    have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
   2.785 @@ -693,6 +639,7 @@
   2.786    finally show ?thesis .
   2.787  qed
   2.788  
   2.789 +
   2.790  subsection {* Total Orders *}
   2.791  
   2.792  locale total_order = lattice +
   2.793 @@ -707,47 +654,48 @@
   2.794    show "lattice_axioms L"
   2.795    proof (rule lattice_axioms.intro)
   2.796      fix x y
   2.797 -    assume L: "x \<in> carrier L" "y \<in> carrier L"
   2.798 +    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   2.799      show "EX s. least L s (Upper L {x, y})"
   2.800      proof -
   2.801        note total L
   2.802        moreover
   2.803        {
   2.804 -	assume "x \<sqsubseteq> y"
   2.805 +        assume "x \<sqsubseteq> y"
   2.806          with L have "least L y (Upper L {x, y})"
   2.807 -	  by (rule_tac least_UpperI) auto
   2.808 +          by (rule_tac least_UpperI) auto
   2.809        }
   2.810        moreover
   2.811        {
   2.812 -	assume "y \<sqsubseteq> x"
   2.813 +        assume "y \<sqsubseteq> x"
   2.814          with L have "least L x (Upper L {x, y})"
   2.815 -	  by (rule_tac least_UpperI) auto
   2.816 +          by (rule_tac least_UpperI) auto
   2.817        }
   2.818        ultimately show ?thesis by blast
   2.819      qed
   2.820    next
   2.821      fix x y
   2.822 -    assume L: "x \<in> carrier L" "y \<in> carrier L"
   2.823 +    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   2.824      show "EX i. greatest L i (Lower L {x, y})"
   2.825      proof -
   2.826        note total L
   2.827        moreover
   2.828        {
   2.829 -	assume "y \<sqsubseteq> x"
   2.830 +        assume "y \<sqsubseteq> x"
   2.831          with L have "greatest L y (Lower L {x, y})"
   2.832 -	  by (rule_tac greatest_LowerI) auto
   2.833 +          by (rule_tac greatest_LowerI) auto
   2.834        }
   2.835        moreover
   2.836        {
   2.837 -	assume "x \<sqsubseteq> y"
   2.838 +        assume "x \<sqsubseteq> y"
   2.839          with L have "greatest L x (Lower L {x, y})"
   2.840 -	  by (rule_tac greatest_LowerI) auto
   2.841 +          by (rule_tac greatest_LowerI) auto
   2.842        }
   2.843        ultimately show ?thesis by blast
   2.844      qed
   2.845    qed
   2.846  qed (assumption | rule total_order_axioms.intro)+
   2.847  
   2.848 +
   2.849  subsection {* Complete lattices *}
   2.850  
   2.851  locale complete_lattice = lattice +
   2.852 @@ -766,7 +714,7 @@
   2.853    shows "complete_lattice L"
   2.854  proof (rule complete_lattice.intro)
   2.855    show "lattice_axioms L"
   2.856 -  by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
   2.857 +    by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
   2.858  qed (assumption | rule complete_lattice_axioms.intro)+
   2.859  
   2.860  constdefs (structure L)
   2.861 @@ -789,7 +737,7 @@
   2.862  qed
   2.863  
   2.864  lemma (in complete_lattice) sup_closed [simp]:
   2.865 -  "A \<subseteq> carrier L ==> \<Squnion> A \<in> carrier L"
   2.866 +  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
   2.867    by (rule supI) simp_all
   2.868  
   2.869  lemma (in complete_lattice) top_closed [simp, intro]:
   2.870 @@ -798,7 +746,7 @@
   2.871  
   2.872  lemma (in complete_lattice) infI:
   2.873    "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
   2.874 -  ==> P (\<Sqinter> A)"
   2.875 +  ==> P (\<Sqinter>A)"
   2.876  proof (unfold inf_def)
   2.877    assume L: "A \<subseteq> carrier L"
   2.878      and P: "!!l. greatest L l (Lower L A) ==> P l"
   2.879 @@ -808,7 +756,7 @@
   2.880  qed
   2.881  
   2.882  lemma (in complete_lattice) inf_closed [simp]:
   2.883 -  "A \<subseteq> carrier L ==> \<Sqinter> A \<in> carrier L"
   2.884 +  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
   2.885    by (rule infI) simp_all
   2.886  
   2.887  lemma (in complete_lattice) bottom_closed [simp, intro]:
   2.888 @@ -842,7 +790,7 @@
   2.889    obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
   2.890    have "least L b (Upper L A)"
   2.891  apply (rule least_UpperI)
   2.892 -   apply (rule greatest_le [where A = "Lower L ?B"]) 
   2.893 +   apply (rule greatest_le [where A = "Lower L ?B"])
   2.894      apply (rule b_inf_B)
   2.895     apply (rule Lower_memI)
   2.896      apply (erule UpperD)
   2.897 @@ -942,7 +890,7 @@
   2.898    with subgr [THEN subgroup.m_inv_closed]
   2.899    show "inv x \<in> \<Inter>A" by blast
   2.900  next
   2.901 -  fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A"
   2.902 +  fix x y assume "x \<in> \<Inter>A"  "y \<in> \<Inter>A"
   2.903    with subgr [THEN subgroup.m_closed]
   2.904    show "x \<otimes> y \<in> \<Inter>A" by blast
   2.905  qed
   2.906 @@ -986,4 +934,4 @@
   2.907    then show "EX I. greatest ?L I (Lower ?L A)" ..
   2.908  qed
   2.909  
   2.910 -end
   2.911 \ No newline at end of file
   2.912 +end