src/HOL/Lattices.thy
changeset 25062 af5ef0d4d655
parent 24749 151b3758f576
child 25102 db3e412c4cb1
     1.1 --- a/src/HOL/Lattices.thy	Tue Oct 16 23:12:38 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Tue Oct 16 23:12:45 2007 +0200
     1.3 @@ -33,18 +33,20 @@
     1.4  lemmas antisym_intro [intro!] = antisym
     1.5  lemmas (in -) [rule del] = antisym_intro
     1.6  
     1.7 -lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
     1.8 -apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
     1.9 - apply(blast intro: order_trans)
    1.10 -apply simp
    1.11 -done
    1.12 +lemma le_infI1[intro]:
    1.13 +  assumes "a \<sqsubseteq> x"
    1.14 +  shows "a \<sqinter> b \<sqsubseteq> x"
    1.15 +proof (rule order_trans)
    1.16 +  show "a \<sqinter> b \<sqsubseteq> a" and "a \<sqsubseteq> x" using assms by simp
    1.17 +qed
    1.18  lemmas (in -) [rule del] = le_infI1
    1.19  
    1.20 -lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    1.21 -apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
    1.22 - apply(blast intro: order_trans)
    1.23 -apply simp
    1.24 -done
    1.25 +lemma le_infI2[intro]:
    1.26 +  assumes "b \<sqsubseteq> x"
    1.27 +  shows "a \<sqinter> b \<sqsubseteq> x"
    1.28 +proof (rule order_trans)
    1.29 +  show "a \<sqinter> b \<sqsubseteq> b" and "b \<sqsubseteq> x" using assms by simp
    1.30 +qed
    1.31  lemmas (in -) [rule del] = le_infI2
    1.32  
    1.33  lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    1.34 @@ -75,17 +77,11 @@
    1.35  lemmas (in -) [rule del] = antisym_intro
    1.36  
    1.37  lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.38 -apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
    1.39 - apply(blast intro: order_trans)
    1.40 -apply simp
    1.41 -done
    1.42 +  by (rule order_trans) auto
    1.43  lemmas (in -) [rule del] = le_supI1
    1.44  
    1.45  lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.46 -apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
    1.47 - apply(blast intro: order_trans)
    1.48 -apply simp
    1.49 -done
    1.50 +  by (rule order_trans) auto 
    1.51  lemmas (in -) [rule del] = le_supI2
    1.52  
    1.53  lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    1.54 @@ -255,26 +251,26 @@
    1.55  
    1.56  lemma (in lower_semilattice) inf_unique:
    1.57    fixes f (infixl "\<triangle>" 70)
    1.58 -  assumes le1: "\<And>x y. x \<triangle> y \<^loc>\<le> x" and le2: "\<And>x y. x \<triangle> y \<^loc>\<le> y"
    1.59 -  and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z"
    1.60 +  assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
    1.61 +  and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
    1.62    shows "x \<sqinter> y = x \<triangle> y"
    1.63  proof (rule antisym)
    1.64 -  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
    1.65 +  show "x \<triangle> y \<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
    1.66  next
    1.67 -  have leI: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" by (blast intro: greatest)
    1.68 -  show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all
    1.69 +  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
    1.70 +  show "x \<sqinter> y \<le> x \<triangle> y" by (rule leI) simp_all
    1.71  qed
    1.72  
    1.73  lemma (in upper_semilattice) sup_unique:
    1.74    fixes f (infixl "\<nabla>" 70)
    1.75 -  assumes ge1 [simp]: "\<And>x y. x \<^loc>\<le> x \<nabla> y" and ge2: "\<And>x y. y \<^loc>\<le> x \<nabla> y"
    1.76 -  and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x"
    1.77 +  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
    1.78 +  and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
    1.79    shows "x \<squnion> y = x \<nabla> y"
    1.80  proof (rule antisym)
    1.81 -  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
    1.82 +  show "x \<squnion> y \<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
    1.83  next
    1.84 -  have leI: "\<And>x y z. x \<^loc>\<le> z \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<nabla> y \<^loc>\<le> z" by (blast intro: least)
    1.85 -  show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all
    1.86 +  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
    1.87 +  show "x \<nabla> y \<le> x \<squnion> y" by (rule leI) simp_all
    1.88  qed
    1.89    
    1.90  
    1.91 @@ -282,9 +278,9 @@
    1.92    special case of @{const inf}/@{const sup} *}
    1.93  
    1.94  lemma (in linorder) distrib_lattice_min_max:
    1.95 -  "distrib_lattice (op \<^loc>\<le>) (op \<^loc><) min max"
    1.96 +  "distrib_lattice (op \<le>) (op <) min max"
    1.97  proof unfold_locales
    1.98 -  have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
    1.99 +  have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
   1.100      by (auto simp add: less_le antisym)
   1.101    fix x y z
   1.102    show "max x (min y z) = min (max x y) (max x z)"
   1.103 @@ -333,10 +329,10 @@
   1.104       and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
   1.105  begin
   1.106  
   1.107 -lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}"
   1.108 +lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
   1.109    by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
   1.110  
   1.111 -lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
   1.112 +lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
   1.113    by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
   1.114  
   1.115  lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
   1.116 @@ -411,10 +407,10 @@
   1.117  where
   1.118    "bot = Sup {}"
   1.119  
   1.120 -lemma top_greatest [simp]: "x \<^loc>\<le> top"
   1.121 +lemma top_greatest [simp]: "x \<le> top"
   1.122    by (unfold top_def, rule Inf_greatest, simp)
   1.123  
   1.124 -lemma bot_least [simp]: "bot \<^loc>\<le> x"
   1.125 +lemma bot_least [simp]: "bot \<le> x"
   1.126    by (unfold bot_def, rule Sup_least, simp)
   1.127  
   1.128  definition
   1.129 @@ -584,4 +580,16 @@
   1.130  lemmas inf_aci = inf_ACI
   1.131  lemmas sup_aci = sup_ACI
   1.132  
   1.133 +no_notation
   1.134 +  inf (infixl "\<sqinter>" 70)
   1.135 +
   1.136 +no_notation
   1.137 +  sup (infixl "\<squnion>" 65)
   1.138 +
   1.139 +no_notation
   1.140 +  Inf ("\<Sqinter>_" [900] 900)
   1.141 +
   1.142 +no_notation
   1.143 +  Sup ("\<Squnion>_" [900] 900)
   1.144 +
   1.145  end