Proper interpretation of total orders in lattices.
authorballarin
Tue Jul 31 14:18:24 2007 +0200 (2007-07-31)
changeset 24087eb025d149a34
parent 24086 21900a460ba4
child 24088 c2d8270e53a5
Proper interpretation of total orders in lattices.
src/HOL/Algebra/Lattice.thy
     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 *}