src/HOL/Lattices.thy
changeset 22422 ee19cdb07528
parent 22384 33a46e6c7f04
child 22454 c3654ba76a09
     1.1 --- a/src/HOL/Lattices.thy	Tue Mar 06 16:40:32 2007 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Fri Mar 09 08:45:50 2007 +0100
     1.3 @@ -16,42 +16,47 @@
     1.4  Finite_Set}. In the longer term it may be better to define arbitrary
     1.5  sups and infs via @{text THE}. *}
     1.6  
     1.7 -locale lower_semilattice = order +
     1.8 +class lower_semilattice = order +
     1.9    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    1.10 -  assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
    1.11 +  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    1.12    and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    1.13  
    1.14 -locale upper_semilattice = order +
    1.15 +class upper_semilattice = order +
    1.16    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    1.17 -  assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
    1.18 +  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    1.19    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    1.20  
    1.21 -locale lattice = lower_semilattice + upper_semilattice
    1.22 +class lattice = lower_semilattice + upper_semilattice
    1.23  
    1.24  subsubsection{* Intro and elim rules*}
    1.25  
    1.26  context lower_semilattice
    1.27  begin
    1.28  
    1.29 -lemmas antisym_intro[intro!] = antisym
    1.30 +lemmas antisym_intro [intro!] = antisym
    1.31 +lemmas (in -) [rule del] = antisym_intro
    1.32  
    1.33  lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    1.34  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
    1.35   apply(blast intro: order_trans)
    1.36  apply simp
    1.37  done
    1.38 +lemmas (in -) [rule del] = le_infI1
    1.39  
    1.40  lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    1.41  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
    1.42   apply(blast intro: order_trans)
    1.43  apply simp
    1.44  done
    1.45 +lemmas (in -) [rule del] = le_infI2
    1.46  
    1.47  lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    1.48  by(blast intro: inf_greatest)
    1.49 +lemmas (in -) [rule del] = le_infI
    1.50  
    1.51 -lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.52 -by(blast intro: order_trans)
    1.53 +lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.54 +  by (blast intro: order_trans)
    1.55 +lemmas (in -) [rule del] = le_infE
    1.56  
    1.57  lemma le_inf_iff [simp]:
    1.58   "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    1.59 @@ -66,25 +71,31 @@
    1.60  context upper_semilattice
    1.61  begin
    1.62  
    1.63 -lemmas antisym_intro[intro!] = antisym
    1.64 +lemmas antisym_intro [intro!] = antisym
    1.65 +lemmas (in -) [rule del] = antisym_intro
    1.66  
    1.67  lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.68  apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
    1.69   apply(blast intro: order_trans)
    1.70  apply simp
    1.71  done
    1.72 +lemmas (in -) [rule del] = le_supI1
    1.73  
    1.74  lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.75  apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
    1.76   apply(blast intro: order_trans)
    1.77  apply simp
    1.78  done
    1.79 +lemmas (in -) [rule del] = le_supI2
    1.80  
    1.81  lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    1.82  by(blast intro: sup_least)
    1.83 +lemmas (in -) [rule del] = le_supI
    1.84  
    1.85  lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    1.86 -by(blast intro: order_trans)
    1.87 +  by (blast intro: order_trans)
    1.88 +lemmas (in -) [rule del] = le_supE
    1.89 +
    1.90  
    1.91  lemma ge_sup_conv[simp]:
    1.92   "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
    1.93 @@ -247,25 +258,24 @@
    1.94  apply (simp add: max_def linorder_not_le order_less_imp_le)
    1.95  unfolding min_def max_def by auto
    1.96  
    1.97 -text{* Now we have inherited antisymmetry as an intro-rule on all
    1.98 -linear orders. This is a problem because it applies to bool, which is
    1.99 -undesirable. *}
   1.100 +text {*
   1.101 +  Now we have inherited antisymmetry as an intro-rule on all
   1.102 +  linear orders. This is a problem because it applies to bool, which is
   1.103 +  undesirable.
   1.104 +*}
   1.105  
   1.106 -declare
   1.107 - min_max.antisym_intro[rule del]
   1.108 - min_max.le_infI[rule del] min_max.le_supI[rule del]
   1.109 - min_max.le_supE[rule del] min_max.le_infE[rule del]
   1.110 - min_max.le_supI1[rule del] min_max.le_supI2[rule del]
   1.111 - min_max.le_infI1[rule del] min_max.le_infI2[rule del]
   1.112 +lemmas [rule del] = min_max.antisym_intro  min_max.le_infI min_max.le_supI
   1.113 +  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
   1.114 +  min_max.le_infI1 min_max.le_infI2
   1.115  
   1.116  lemmas le_maxI1 = min_max.sup_ge1
   1.117  lemmas le_maxI2 = min_max.sup_ge2
   1.118   
   1.119  lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   1.120 -               mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
   1.121 +  mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute]
   1.122  
   1.123  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   1.124 -               mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
   1.125 +  mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
   1.126  
   1.127  text {* ML legacy bindings *}
   1.128