author ballarin Tue Jul 31 14:18:24 2007 +0200 (2007-07-31) changeset 24087 eb025d149a34 parent 24086 21900a460ba4 child 24088 c2d8270e53a5
Proper interpretation of total orders in lattices.
```     1.1 --- a/src/HOL/Algebra/Lattice.thy	Tue Jul 31 13:31:01 2007 +0200
1.2 +++ b/src/HOL/Algebra/Lattice.thy	Tue Jul 31 14:18:24 2007 +0200
1.3 @@ -656,7 +656,7 @@
1.4
1.5  subsection {* Total Orders *}
1.6
1.7 -locale total_order = lattice +
1.8 +locale total_order = partial_order +
1.9    assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
1.10
1.11  text {* Introduction rule: the usual definition of total order *}
1.12 @@ -664,50 +664,52 @@
1.13  lemma (in partial_order) total_orderI:
1.14    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
1.15    shows "total_order L"
1.16 -proof intro_locales
1.17 -  show "lattice_axioms L"
1.18 -  proof (rule lattice_axioms.intro)
1.19 -    fix x y
1.20 -    assume L: "x \<in> carrier L"  "y \<in> carrier L"
1.21 -    show "EX s. least L s (Upper L {x, y})"
1.22 -    proof -
1.23 -      note total L
1.24 -      moreover
1.25 -      {
1.26 -        assume "x \<sqsubseteq> y"
1.27 -        with L have "least L y (Upper L {x, y})"
1.28 -          by (rule_tac least_UpperI) auto
1.29 -      }
1.30 -      moreover
1.31 -      {
1.32 -        assume "y \<sqsubseteq> x"
1.33 -        with L have "least L x (Upper L {x, y})"
1.34 -          by (rule_tac least_UpperI) auto
1.35 -      }
1.36 -      ultimately show ?thesis by blast
1.37 -    qed
1.38 -  next
1.39 -    fix x y
1.40 -    assume L: "x \<in> carrier L"  "y \<in> carrier L"
1.41 -    show "EX i. greatest L i (Lower L {x, y})"
1.42 -    proof -
1.43 -      note total L
1.44 -      moreover
1.45 -      {
1.46 -        assume "y \<sqsubseteq> x"
1.47 -        with L have "greatest L y (Lower L {x, y})"
1.48 -          by (rule_tac greatest_LowerI) auto
1.49 -      }
1.50 -      moreover
1.51 -      {
1.52 -        assume "x \<sqsubseteq> y"
1.53 -        with L have "greatest L x (Lower L {x, y})"
1.54 -          by (rule_tac greatest_LowerI) auto
1.55 -      }
1.56 -      ultimately show ?thesis by blast
1.57 -    qed
1.58 +  by unfold_locales (rule total)
1.59 +
1.60 +text {* Total orders are lattices. *}
1.61 +
1.62 +interpretation total_order < lattice
1.63 +proof unfold_locales
1.64 +  fix x y
1.65 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
1.66 +  show "EX s. least L s (Upper L {x, y})"
1.67 +  proof -
1.68 +    note total L
1.69 +    moreover
1.70 +    {
1.71 +      assume "x \<sqsubseteq> y"
1.72 +      with L have "least L y (Upper L {x, y})"
1.73 +        by (rule_tac least_UpperI) auto
1.74 +    }
1.75 +    moreover
1.76 +    {
1.77 +      assume "y \<sqsubseteq> x"
1.78 +      with L have "least L x (Upper L {x, y})"
1.79 +        by (rule_tac least_UpperI) auto
1.80 +    }
1.81 +    ultimately show ?thesis by blast
1.82    qed
1.83 -qed (rule total total_order_axioms.intro)+
1.84 +next
1.85 +  fix x y
1.86 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
1.87 +  show "EX i. greatest L i (Lower L {x, y})"
1.88 +  proof -
1.89 +    note total L
1.90 +    moreover
1.91 +    {
1.92 +      assume "y \<sqsubseteq> x"
1.93 +      with L have "greatest L y (Lower L {x, y})"
1.94 +        by (rule_tac greatest_LowerI) auto
1.95 +    }
1.96 +    moreover
1.97 +    {
1.98 +      assume "x \<sqsubseteq> y"
1.99 +      with L have "greatest L x (Lower L {x, y})"
1.100 +        by (rule_tac greatest_LowerI) auto
1.101 +    }
1.102 +    ultimately show ?thesis by blast
1.103 +  qed
1.104 +qed
1.105
1.106
1.107  subsection {* Complete lattices *}
```