Modified lattice locale
authornipkow
Sun Dec 10 07:12:26 2006 +0100 (2006-12-10)
changeset 21733131dd2a27137
parent 21732 4d4cde714500
child 21734 283461c15fa7
Modified lattice locale
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/LOrder.thy
src/HOL/Lattices.thy
src/HOL/UNITY/Transformers.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Sat Dec 09 18:06:17 2006 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Sun Dec 10 07:12:26 2006 +0100
     1.3 @@ -428,7 +428,7 @@
     1.4  *}
     1.5  
     1.6  consts
     1.7 -  foldSet :: "('a => 'b => 'b) => ('c => 'a) => 'b => ('c set \<times> 'b) set"
     1.8 +  foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
     1.9  
    1.10  inductive "foldSet f g z"
    1.11  intros
    1.12 @@ -440,7 +440,7 @@
    1.13  inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z"
    1.14  
    1.15  constdefs
    1.16 -  fold :: "('a => 'b => 'b) => ('c => 'a) => 'b => 'c set => 'b"
    1.17 +  fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
    1.18    "fold f g z A == THE x. (A, x) : foldSet f g z"
    1.19  
    1.20  text{*A tempting alternative for the definiens is
    1.21 @@ -1211,7 +1211,7 @@
    1.22    proof induct
    1.23      case empty thus ?case by simp
    1.24    next
    1.25 -    case (insert x A) thus ?case by (auto intro: order_trans)
    1.26 +    case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
    1.27    qed
    1.28  next
    1.29    case False thus ?thesis by (simp add: setsum_def)
    1.30 @@ -2213,7 +2213,7 @@
    1.31  apply(rule ACIf.axioms[OF ACIf_inf])
    1.32  apply(rule ACIfSL_axioms.intro)
    1.33  apply(rule iffI)
    1.34 - apply(blast intro: antisym inf_le1 inf_le2 inf_least refl)
    1.35 + apply(blast intro: antisym inf_le1 inf_le2 inf_greatest refl)
    1.36  apply(erule subst)
    1.37  apply(rule inf_le2)
    1.38  done
    1.39 @@ -2226,7 +2226,7 @@
    1.40  apply(rule ACIf.axioms[OF ACIf_sup])
    1.41  apply(rule ACIfSL_axioms.intro)
    1.42  apply(rule iffI)
    1.43 - apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
    1.44 + apply(blast intro: antisym sup_ge1 sup_ge2 sup_least refl)
    1.45  apply(erule subst)
    1.46  apply(rule sup_ge2)
    1.47  done
    1.48 @@ -2247,12 +2247,12 @@
    1.49  lemma (in Lattice) sup_Inf_absorb[simp]:
    1.50    "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
    1.51  apply(subst sup_commute)
    1.52 -apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
    1.53 +apply(simp add:Inf_def sup_absorb2 ACIfSL.fold1_belowI[OF ACIfSL_inf])
    1.54  done
    1.55  
    1.56  lemma (in Lattice) inf_Sup_absorb[simp]:
    1.57    "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
    1.58 -by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
    1.59 +by(simp add:Sup_def inf_absorb1 ACIfSL.fold1_belowI[OF ACIfSL_sup])
    1.60  
    1.61  
    1.62  lemma (in ACIf) hom_fold1_commute:
    1.63 @@ -2289,7 +2289,7 @@
    1.64  next
    1.65    case (insert x A)
    1.66    have finB: "finite {x \<squnion> b |b. b \<in> B}"
    1.67 -    by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
    1.68 +    by(rule finite_surj[where f = "%b. x \<squnion> b", OF B(1)], auto)
    1.69    have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
    1.70    proof -
    1.71      have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
    1.72 @@ -2330,7 +2330,7 @@
    1.73  next
    1.74    case (insert x A)
    1.75    have finB: "finite {x \<sqinter> b |b. b \<in> B}"
    1.76 -    by(fast intro: finite_surj[where f = "%b. x \<sqinter> b", OF B(1)])
    1.77 +    by(rule finite_surj[where f = "%b. x \<sqinter> b", OF B(1)], auto)
    1.78    have finAB: "finite {a \<sqinter> b |a b. a \<in> A \<and> b \<in> B}"
    1.79    proof -
    1.80      have "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<sqinter> b})"
     2.1 --- a/src/HOL/Hyperreal/Lim.thy	Sat Dec 09 18:06:17 2006 +0100
     2.2 +++ b/src/HOL/Hyperreal/Lim.thy	Sun Dec 10 07:12:26 2006 +0100
     2.3 @@ -966,7 +966,7 @@
     2.4      and aux: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (X x - L) < r"
     2.5      by fast
     2.6    from LIMSEQ_D [OF S sgz]
     2.7 -  obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by fast
     2.8 +  obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by blast
     2.9    hence "\<forall>n\<ge>no. norm (X (S n) - L) < r" by (simp add: aux as)
    2.10    thus "\<exists>no. \<forall>n\<ge>no. norm (X (S n) - L) < r" ..
    2.11  qed
     3.1 --- a/src/HOL/LOrder.thy	Sat Dec 09 18:06:17 2006 +0100
     3.2 +++ b/src/HOL/LOrder.thy	Sun Dec 10 07:12:26 2006 +0100
     3.3 @@ -90,63 +90,49 @@
     3.4  lemma join_unique: "(is_join j) = (j = join)"
     3.5  by (insert is_join_join, auto simp add: is_join_unique)
     3.6  
     3.7 -interpretation lattice:
     3.8 -  lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
     3.9 +interpretation meet_semilat:
    3.10 +  lower_semilattice ["op \<le> \<Colon> 'a\<Colon>meet_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet]
    3.11  proof unfold_locales
    3.12 -  fix x y z :: "'a\<Colon>lorder"
    3.13 +  fix x y z :: "'a\<Colon>meet_semilorder"
    3.14    from is_meet_meet have "is_meet meet" by blast
    3.15    note meet = this is_meet_def
    3.16    from meet show "meet x y \<le> x" by blast
    3.17    from meet show "meet x y \<le> y" by blast
    3.18    from meet show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> meet y z" by blast
    3.19 +qed
    3.20 +
    3.21 +interpretation join_semilat:
    3.22 +  upper_semilattice ["op \<le> \<Colon> 'a\<Colon>join_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" join]
    3.23 +proof unfold_locales
    3.24 +  fix x y z :: "'a\<Colon>join_semilorder"
    3.25    from is_join_join have "is_join join" by blast
    3.26    note join = this is_join_def
    3.27    from join show "x \<le> join x y" by blast
    3.28    from join show "y \<le> join x y" by blast
    3.29 -  from join show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> join y z \<le> x" by blast
    3.30 +  from join show "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> join x y \<le> z" by blast
    3.31  qed
    3.32  
    3.33 -lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"
    3.34 -by (insert is_meet_meet, auto simp add: is_meet_def)
    3.35 -
    3.36 -lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
    3.37 -by (insert is_meet_meet, auto simp add: is_meet_def)
    3.38 +declare
    3.39 + join_semilat.antisym_intro[rule del] meet_semilat.antisym_intro[rule del]
    3.40 + join_semilat.less_eq_supE[rule del] meet_semilat.less_eq_infE[rule del]
    3.41  
    3.42 -(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
    3.43 -lemma le_meetI:
    3.44 - "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
    3.45 -by (insert is_meet_meet, auto simp add: is_meet_def)
    3.46 -
    3.47 -lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
    3.48 -by (insert is_join_join, auto simp add: is_join_def)
    3.49 -
    3.50 -lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
    3.51 -by (insert is_join_join, auto simp add: is_join_def)
    3.52 -
    3.53 -lemma join_leI:
    3.54 - "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
    3.55 -by (insert is_join_join, auto simp add: is_join_def)
    3.56 +interpretation meet_join_lat:
    3.57 +  lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
    3.58 +by unfold_locales
    3.59  
    3.60 -lemmas meet_join_le[simp] = meet_left_le meet_right_le join_left_le join_right_le
    3.61 +lemmas meet_left_le = meet_semilat.inf_le1
    3.62 +lemmas meet_right_le = meet_semilat.inf_le2
    3.63 +lemmas le_meetI[rule del] = meet_semilat.less_eq_infI
    3.64 +(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
    3.65 +lemmas join_left_le = join_semilat.sup_ge1
    3.66 +lemmas join_right_le = join_semilat.sup_ge2
    3.67 +lemmas join_leI[rule del] = join_semilat.less_eq_supI
    3.68  
    3.69 -lemma le_meet[simp]: "(x <= meet y z) = (x <= y & x <= z)" (is "?L = ?R")
    3.70 -proof
    3.71 -  assume ?L
    3.72 -  moreover have "meet y z \<le> y" "meet y z <= z" by(simp_all)
    3.73 -  ultimately show ?R by(blast intro:order_trans)
    3.74 -next
    3.75 -  assume ?R thus ?L by (blast intro!:le_meetI)
    3.76 -qed
    3.77 +lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
    3.78  
    3.79 -lemma join_le[simp]: "(join x y <= z) = (x <= z & y <= z)" (is "?L = ?R")
    3.80 -proof
    3.81 -  assume ?L
    3.82 -  moreover have "x \<le> join x y" "y \<le> join x y" by(simp_all)
    3.83 -  ultimately show ?R by(blast intro:order_trans)
    3.84 -next
    3.85 -  assume ?R thus ?L by (blast intro:join_leI)
    3.86 -qed
    3.87 +lemmas le_meet = meet_semilat.less_eq_inf_conv
    3.88  
    3.89 +lemmas le_join = join_semilat.above_sup_conv
    3.90  
    3.91  lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
    3.92  by (auto simp add: is_meet_def min_def)
    3.93 @@ -172,68 +158,22 @@
    3.94  lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
    3.95  by (simp add: is_join_join is_join_max is_join_unique)
    3.96  
    3.97 -lemma meet_idempotent[simp]: "meet x x = x"
    3.98 -by (rule order_antisym, simp_all add: le_meetI)
    3.99 -
   3.100 -lemma join_idempotent[simp]: "join x x = x"
   3.101 -by (rule order_antisym, simp_all add: join_leI)
   3.102 -
   3.103 -lemma meet_comm: "meet x y = meet y x" 
   3.104 -by (rule order_antisym, (simp add: le_meetI)+)
   3.105 -
   3.106 -lemma join_comm: "join x y = join y x"
   3.107 -by (rule order_antisym, (simp add: join_leI)+)
   3.108 -
   3.109 -lemma meet_leI1: "x \<le> z \<Longrightarrow> meet x y \<le> z"
   3.110 -apply(subgoal_tac "meet x y <= x")
   3.111 - apply(blast intro:order_trans)
   3.112 -apply simp
   3.113 -done
   3.114 -
   3.115 -lemma meet_leI2: "y \<le> z \<Longrightarrow> meet x y \<le> z"
   3.116 -apply(subgoal_tac "meet x y <= y")
   3.117 - apply(blast intro:order_trans)
   3.118 -apply simp
   3.119 -done
   3.120 -
   3.121 -lemma le_joinI1: "x \<le> y \<Longrightarrow> x \<le> join y z"
   3.122 -apply(subgoal_tac "y <= join y z")
   3.123 - apply(blast intro:order_trans)
   3.124 -apply simp
   3.125 -done
   3.126 -
   3.127 -lemma le_joinI2: "x \<le> z \<Longrightarrow> x \<le> join y z"
   3.128 -apply(subgoal_tac "z <= join y z")
   3.129 - apply(blast intro:order_trans)
   3.130 -apply simp
   3.131 -done
   3.132 -
   3.133 -lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)"
   3.134 -apply(rule order_antisym)
   3.135 -apply (simp add:meet_leI1 meet_leI2)
   3.136 -apply (simp add:meet_leI1 meet_leI2)
   3.137 -done
   3.138 -
   3.139 -lemma join_assoc: "join (join x y) z = join x (join y z)"
   3.140 -apply(rule order_antisym)
   3.141 -apply (simp add:le_joinI1 le_joinI2)
   3.142 -apply (simp add:le_joinI1 le_joinI2)
   3.143 -done
   3.144 -
   3.145 -lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
   3.146 -by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)
   3.147 -
   3.148 -lemma meet_left_idempotent: "meet y (meet y x) = meet y x"
   3.149 -by (simp add: meet_assoc meet_comm meet_left_comm)
   3.150 -
   3.151 -lemma join_left_comm: "join a (join b c) = join b (join a c)"
   3.152 -by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)
   3.153 -
   3.154 -lemma join_left_idempotent: "join y (join y x) = join y x"
   3.155 -by (simp add: join_assoc join_comm join_left_comm)
   3.156 +lemmas meet_idempotent = meet_semilat.inf_idem
   3.157 +lemmas join_idempotent = join_semilat.sup_idem
   3.158 +lemmas meet_comm = meet_semilat.inf_commute
   3.159 +lemmas join_comm = join_semilat.sup_commute
   3.160 +lemmas meet_leI1[rule del] = meet_semilat.less_eq_infI1
   3.161 +lemmas meet_leI2[rule del] = meet_semilat.less_eq_infI2
   3.162 +lemmas le_joinI1[rule del] = join_semilat.less_eq_supI1
   3.163 +lemmas le_joinI2[rule del] = join_semilat.less_eq_supI2
   3.164 +lemmas meet_assoc = meet_semilat.inf_assoc
   3.165 +lemmas join_assoc = join_semilat.sup_assoc
   3.166 +lemmas meet_left_comm = meet_semilat.inf_left_commute
   3.167 +lemmas meet_left_idempotent = meet_semilat.inf_left_idem
   3.168 +lemmas join_left_comm = join_semilat.sup_left_commute
   3.169 +lemmas join_left_idempotent= join_semilat.sup_left_idem
   3.170      
   3.171  lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
   3.172 -
   3.173  lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
   3.174  
   3.175  lemma le_def_meet: "(x <= y) = (meet x y = x)"
   3.176 @@ -252,17 +192,11 @@
   3.177  apply(simp (no_asm))
   3.178  done
   3.179  
   3.180 -lemma join_absorp2: "a \<le> b \<Longrightarrow> join a b = b" 
   3.181 -by (simp add: le_def_join)
   3.182 -
   3.183 -lemma join_absorp1: "b \<le> a \<Longrightarrow> join a b = a"
   3.184 -by (simp add: le_def_join join_aci)
   3.185 +lemmas join_absorp2 = join_semilat.sup_absorb2
   3.186 +lemmas join_absorp1 = join_semilat.sup_absorb1
   3.187  
   3.188 -lemma meet_absorp1: "a \<le> b \<Longrightarrow> meet a b = a"
   3.189 -by (simp add: le_def_meet)
   3.190 -
   3.191 -lemma meet_absorp2: "b \<le> a \<Longrightarrow> meet a b = b"
   3.192 -by (simp add: le_def_meet meet_aci)
   3.193 +lemmas meet_absorp1 = meet_semilat.inf_absorb1
   3.194 +lemmas meet_absorp2 = meet_semilat.inf_absorb2
   3.195  
   3.196  lemma meet_join_absorp: "meet x (join x y) = x"
   3.197  by(simp add:meet_absorp1)
     4.1 --- a/src/HOL/Lattices.thy	Sat Dec 09 18:06:17 2006 +0100
     4.2 +++ b/src/HOL/Lattices.thy	Sun Dec 10 07:12:26 2006 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     Tobias Nipkow
     4.5  *)
     4.6  
     4.7 -header {* Abstract lattices *}
     4.8 +header {* Lattices via Locales *}
     4.9  
    4.10  theory Lattices
    4.11  imports Orderings
    4.12 @@ -19,67 +19,154 @@
    4.13  locale lower_semilattice = partial_order +
    4.14    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    4.15    assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
    4.16 -  and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    4.17 +  and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    4.18  
    4.19  locale upper_semilattice = partial_order +
    4.20    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    4.21    assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
    4.22 -  and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    4.23 +  and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    4.24  
    4.25  locale lattice = lower_semilattice + upper_semilattice
    4.26  
    4.27 -lemma (in lower_semilattice) inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
    4.28 -by(blast intro: antisym inf_le1 inf_le2 inf_least)
    4.29 +subsubsection{* Intro and elim rules*}
    4.30 +
    4.31 +context lower_semilattice
    4.32 +begin
    4.33  
    4.34 -lemma (in upper_semilattice) sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
    4.35 -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest)
    4.36 +lemmas antisym_intro[intro!] = antisym
    4.37  
    4.38 -lemma (in lower_semilattice) inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    4.39 -by(blast intro: antisym inf_le1 inf_le2 inf_least trans del:refl)
    4.40 +lemma less_eq_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    4.41 +apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
    4.42 + apply(blast intro:trans)
    4.43 +apply simp
    4.44 +done
    4.45  
    4.46 -lemma (in upper_semilattice) sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    4.47 -by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans del:refl)
    4.48 +lemma less_eq_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    4.49 +apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
    4.50 + apply(blast intro:trans)
    4.51 +apply simp
    4.52 +done
    4.53 +
    4.54 +lemma less_eq_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    4.55 +by(blast intro: inf_greatest)
    4.56  
    4.57 -lemma (in lower_semilattice) inf_idem[simp]: "x \<sqinter> x = x"
    4.58 -by(blast intro: antisym inf_le1 inf_le2 inf_least refl)
    4.59 +lemma less_eq_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    4.60 +by(blast intro: trans)
    4.61  
    4.62 -lemma (in upper_semilattice) sup_idem[simp]: "x \<squnion> x = x"
    4.63 -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
    4.64 +lemma less_eq_inf_conv [simp]:
    4.65 + "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    4.66 +by blast
    4.67 +
    4.68 +lemmas below_inf_conv = less_eq_inf_conv
    4.69 +  -- {* a duplicate for backward compatibility *}
    4.70  
    4.71 -lemma (in lower_semilattice) inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    4.72 -by (simp add: inf_assoc[symmetric])
    4.73 +end
    4.74 +
    4.75 +
    4.76 +context upper_semilattice
    4.77 +begin
    4.78  
    4.79 -lemma (in upper_semilattice) sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    4.80 -by (simp add: sup_assoc[symmetric])
    4.81 +lemmas antisym_intro[intro!] = antisym
    4.82  
    4.83 -lemma (in lattice) inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
    4.84 -by(blast intro: antisym inf_le1 inf_least sup_ge1)
    4.85 +lemma less_eq_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    4.86 +apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
    4.87 + apply(blast intro:trans)
    4.88 +apply simp
    4.89 +done
    4.90  
    4.91 -lemma (in lattice) sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
    4.92 -by(blast intro: antisym sup_ge1 sup_greatest inf_le1)
    4.93 +lemma less_eq_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    4.94 +apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
    4.95 + apply(blast intro:trans)
    4.96 +apply simp
    4.97 +done
    4.98 +
    4.99 +lemma less_eq_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
   4.100 +by(blast intro: sup_least)
   4.101  
   4.102 -lemma (in lower_semilattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   4.103 -by(blast intro: antisym inf_le1 inf_least refl)
   4.104 +lemma less_eq_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
   4.105 +by(blast intro: trans)
   4.106  
   4.107 -lemma (in upper_semilattice) sup_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   4.108 -by(blast intro: antisym sup_ge2 sup_greatest refl)
   4.109 +lemma above_sup_conv[simp]:
   4.110 + "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
   4.111 +by blast
   4.112 +
   4.113 +end
   4.114 +
   4.115 +
   4.116 +subsubsection{* Equational laws *}
   4.117  
   4.118  
   4.119 -lemma (in lower_semilattice) less_eq_inf_conv [simp]:
   4.120 - "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
   4.121 -by(blast intro: antisym inf_le1 inf_le2 inf_least refl trans)
   4.122 +context lower_semilattice
   4.123 +begin
   4.124 +
   4.125 +lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
   4.126 +by blast
   4.127 +
   4.128 +lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   4.129 +by blast
   4.130 +
   4.131 +lemma inf_idem[simp]: "x \<sqinter> x = x"
   4.132 +by blast
   4.133 +
   4.134 +lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   4.135 +by blast
   4.136 +
   4.137 +lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   4.138 +by blast
   4.139 +
   4.140 +lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   4.141 +by blast
   4.142 +
   4.143 +lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   4.144 +by blast
   4.145 +
   4.146 +lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
   4.147 +
   4.148 +end
   4.149 +
   4.150 +
   4.151 +context upper_semilattice
   4.152 +begin
   4.153  
   4.154 -lemmas (in lower_semilattice) below_inf_conv = less_eq_inf_conv
   4.155 -  -- {* a duplicate for backward compatibility *}
   4.156 +lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
   4.157 +by blast
   4.158 +
   4.159 +lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   4.160 +by blast
   4.161 +
   4.162 +lemma sup_idem[simp]: "x \<squnion> x = x"
   4.163 +by blast
   4.164 +
   4.165 +lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   4.166 +by blast
   4.167 +
   4.168 +lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   4.169 +by blast
   4.170 +
   4.171 +lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   4.172 +by blast
   4.173  
   4.174 -lemma (in upper_semilattice) above_sup_conv[simp]:
   4.175 - "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
   4.176 -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl trans)
   4.177 +lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   4.178 +by blast
   4.179 +
   4.180 +lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
   4.181 +
   4.182 +end
   4.183  
   4.184 +context lattice
   4.185 +begin
   4.186 +
   4.187 +lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
   4.188 +by(blast intro: antisym inf_le1 inf_greatest sup_ge1)
   4.189 +
   4.190 +lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
   4.191 +by(blast intro: antisym sup_ge1 sup_least inf_le1)
   4.192 +
   4.193 +lemmas (in lattice) ACI = inf_ACI sup_ACI
   4.194  
   4.195  text{* Towards distributivity: if you have one of them, you have them all. *}
   4.196  
   4.197 -lemma (in lattice) distrib_imp1:
   4.198 +lemma distrib_imp1:
   4.199  assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   4.200  shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   4.201  proof-
   4.202 @@ -91,7 +178,7 @@
   4.203    finally show ?thesis .
   4.204  qed
   4.205  
   4.206 -lemma (in lattice) distrib_imp2:
   4.207 +lemma distrib_imp2:
   4.208  assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   4.209  shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   4.210  proof-
   4.211 @@ -103,46 +190,7 @@
   4.212    finally show ?thesis .
   4.213  qed
   4.214  
   4.215 -text{* A package of rewrite rules for deciding equivalence wrt ACI: *}
   4.216 -
   4.217 -lemma (in lower_semilattice) inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   4.218 -proof -
   4.219 -  have "x \<sqinter> (y \<sqinter> z) = (y \<sqinter> z) \<sqinter> x" by (simp only: inf_commute)
   4.220 -  also have "... = y \<sqinter> (z \<sqinter> x)" by (simp only: inf_assoc)
   4.221 -  also have "z \<sqinter> x = x \<sqinter> z" by (simp only: inf_commute)
   4.222 -  finally(back_subst) show ?thesis .
   4.223 -qed
   4.224 -
   4.225 -lemma (in upper_semilattice) sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   4.226 -proof -
   4.227 -  have "x \<squnion> (y \<squnion> z) = (y \<squnion> z) \<squnion> x" by (simp only: sup_commute)
   4.228 -  also have "... = y \<squnion> (z \<squnion> x)" by (simp only: sup_assoc)
   4.229 -  also have "z \<squnion> x = x \<squnion> z" by (simp only: sup_commute)
   4.230 -  finally(back_subst) show ?thesis .
   4.231 -qed
   4.232 -
   4.233 -lemma (in lower_semilattice) inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   4.234 -proof -
   4.235 -  have "x \<sqinter> (x \<sqinter> y) = (x \<sqinter> x) \<sqinter> y" by(simp only:inf_assoc)
   4.236 -  also have "\<dots> = x \<sqinter> y" by(simp)
   4.237 -  finally show ?thesis .
   4.238 -qed
   4.239 -
   4.240 -lemma (in upper_semilattice) sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   4.241 -proof -
   4.242 -  have "x \<squnion> (x \<squnion> y) = (x \<squnion> x) \<squnion> y" by(simp only:sup_assoc)
   4.243 -  also have "\<dots> = x \<squnion> y" by(simp)
   4.244 -  finally show ?thesis .
   4.245 -qed
   4.246 -
   4.247 -
   4.248 -lemmas (in lower_semilattice) inf_ACI =
   4.249 - inf_commute inf_assoc inf_left_commute inf_left_idem
   4.250 -
   4.251 -lemmas (in upper_semilattice) sup_ACI =
   4.252 - sup_commute sup_assoc sup_left_commute sup_left_idem
   4.253 -
   4.254 -lemmas (in lattice) ACI = inf_ACI sup_ACI
   4.255 +end
   4.256  
   4.257  
   4.258  subsection{* Distributive lattices *}
   4.259 @@ -150,21 +198,26 @@
   4.260  locale distrib_lattice = lattice +
   4.261    assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   4.262  
   4.263 -lemma (in distrib_lattice) sup_inf_distrib2:
   4.264 +context distrib_lattice
   4.265 +begin
   4.266 +
   4.267 +lemma sup_inf_distrib2:
   4.268   "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   4.269  by(simp add:ACI sup_inf_distrib1)
   4.270  
   4.271 -lemma (in distrib_lattice) inf_sup_distrib1:
   4.272 +lemma inf_sup_distrib1:
   4.273   "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   4.274  by(rule distrib_imp2[OF sup_inf_distrib1])
   4.275  
   4.276 -lemma (in distrib_lattice) inf_sup_distrib2:
   4.277 +lemma inf_sup_distrib2:
   4.278   "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   4.279  by(simp add:ACI inf_sup_distrib1)
   4.280  
   4.281 -lemmas (in distrib_lattice) distrib =
   4.282 +lemmas distrib =
   4.283    sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   4.284  
   4.285 +end
   4.286 +
   4.287  
   4.288  subsection {* min/max on linear orders as special case of inf/sup *}
   4.289  
   4.290 @@ -178,6 +231,17 @@
   4.291  apply (simp add: max_def linorder_not_le order_less_imp_le)
   4.292  unfolding min_def max_def by auto
   4.293  
   4.294 +text{* Now we have inherited antisymmetry as an intro-rule on all
   4.295 +linear orders. This is a problem because it applies to bool, which is
   4.296 +undesirable. *}
   4.297 +
   4.298 +declare
   4.299 + min_max.antisym_intro[rule del]
   4.300 + min_max.less_eq_infI[rule del] min_max.less_eq_supI[rule del]
   4.301 + min_max.less_eq_supE[rule del] min_max.less_eq_infE[rule del]
   4.302 + min_max.less_eq_supI1[rule del] min_max.less_eq_supI2[rule del]
   4.303 + min_max.less_eq_infI1[rule del] min_max.less_eq_infI2[rule del]
   4.304 +
   4.305  lemmas le_maxI1 = min_max.sup_ge1
   4.306  lemmas le_maxI2 = min_max.sup_ge2
   4.307   
   4.308 @@ -187,4 +251,29 @@
   4.309  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   4.310                 mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
   4.311  
   4.312 +text {* ML legacy bindings *}
   4.313 +
   4.314 +ML {*
   4.315 +val Least_def = thm "Least_def";
   4.316 +val Least_equality = thm "Least_equality";
   4.317 +val min_def = thm "min_def";
   4.318 +val min_of_mono = thm "min_of_mono";
   4.319 +val max_def = thm "max_def";
   4.320 +val max_of_mono = thm "max_of_mono";
   4.321 +val min_leastL = thm "min_leastL";
   4.322 +val max_leastL = thm "max_leastL";
   4.323 +val min_leastR = thm "min_leastR";
   4.324 +val max_leastR = thm "max_leastR";
   4.325 +val le_max_iff_disj = thm "le_max_iff_disj";
   4.326 +val le_maxI1 = thm "le_maxI1";
   4.327 +val le_maxI2 = thm "le_maxI2";
   4.328 +val less_max_iff_disj = thm "less_max_iff_disj";
   4.329 +val max_less_iff_conj = thm "max_less_iff_conj";
   4.330 +val min_less_iff_conj = thm "min_less_iff_conj";
   4.331 +val min_le_iff_disj = thm "min_le_iff_disj";
   4.332 +val min_less_iff_disj = thm "min_less_iff_disj";
   4.333 +val split_min = thm "split_min";
   4.334 +val split_max = thm "split_max";
   4.335 +*}
   4.336 +
   4.337  end
     5.1 --- a/src/HOL/UNITY/Transformers.thy	Sat Dec 09 18:06:17 2006 +0100
     5.2 +++ b/src/HOL/UNITY/Transformers.thy	Sun Dec 10 07:12:26 2006 +0100
     5.3 @@ -444,11 +444,11 @@
     5.4  apply (rule subsetI)  
     5.5  apply (erule wens_set.induct)
     5.6    txt{*Basis*} 
     5.7 -  apply (force simp add: wens_single_finite_def)
     5.8 +  apply (fastsimp simp add: wens_single_finite_def)
     5.9   txt{*Wens inductive step*}
    5.10 - apply (case_tac "acta = Id", simp)   
    5.11 + apply (case_tac "acta = Id", simp)
    5.12   apply (simp add: wens_single_eq)
    5.13 - apply (elim disjE)   
    5.14 + apply (elim disjE)
    5.15   apply (simp add: wens_single_Un_eq)
    5.16   apply (force simp add: wens_single_finite_Un_eq)
    5.17  txt{*Union inductive step*}