*** empty log message ***
authornipkow
Mon Feb 07 18:20:46 2005 +0100 (2005-02-07)
changeset 155045bc81e50f2c5
parent 15503 38616a65bfbd
child 15505 c929e1cbef88
*** empty log message ***
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Feb 07 08:02:49 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Feb 07 18:20:46 2005 +0100
     1.3 @@ -2083,9 +2083,8 @@
     1.4    and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
     1.5    and sup_ge1: "x \<sqsubseteq> x \<squnion> y" and sup_ge2: "y \<sqsubseteq> x \<squnion> y"
     1.6    and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
     1.7 -(* FIXME *)
     1.8 -  and sup_inf_distrib1: "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
     1.9 -  and sup_inf_distrib2: "x \<sqinter> y \<squnion> z = (x \<squnion> z) \<sqinter> (y \<squnion> z)"
    1.10 +  and inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
    1.11 +  and sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
    1.12    defines "Inf == fold1 inf"  and "Sup == fold1 sup"
    1.13  
    1.14  
    1.15 @@ -2101,12 +2100,53 @@
    1.16  lemma (in Lattice) sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    1.17  by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans)
    1.18  
    1.19 -lemma (in Lattice) inf_idem: "x \<sqinter> x = x"
    1.20 +lemma (in Lattice) inf_idem[simp]: "x \<sqinter> x = x"
    1.21  by(blast intro: antisym inf_le1 inf_le2 inf_least refl)
    1.22  
    1.23 -lemma (in Lattice) sup_idem: "x \<squnion> x = x"
    1.24 +lemma (in Lattice) sup_idem[simp]: "x \<squnion> x = x"
    1.25  by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
    1.26  
    1.27 +lemma (in Lattice) sup_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    1.28 +by(blast intro: antisym sup_ge2 sup_greatest refl)
    1.29 +
    1.30 +lemma (in Lattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    1.31 +by(blast intro: antisym inf_le1 inf_least refl)
    1.32 +
    1.33 +text{* Distributive lattices: *}
    1.34 +
    1.35 +locale DistribLattice = Lattice +
    1.36 +  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.37 +
    1.38 +lemma (in Lattice) distrib_imp1:
    1.39 +assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    1.40 +shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.41 +proof-
    1.42 +  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
    1.43 +  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_comm sup_assoc)
    1.44 +  also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
    1.45 +    by(simp add:inf_sup_absorb inf_comm)
    1.46 +  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    1.47 +  finally show ?thesis .
    1.48 +qed
    1.49 +
    1.50 +lemma (in Lattice) distrib_imp2:
    1.51 +assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.52 +shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    1.53 +proof-
    1.54 +  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
    1.55 +  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_comm inf_assoc)
    1.56 +  also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
    1.57 +    by(simp add:sup_inf_absorb sup_comm)
    1.58 +  also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
    1.59 +  finally show ?thesis .
    1.60 +qed
    1.61 +
    1.62 +
    1.63 +lemma (in DistribLattice) inf_sup_distrib1:
    1.64 + "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    1.65 +by(rule distrib_imp2[OF sup_inf_distrib1])
    1.66 +
    1.67 +
    1.68  text{* Lattices are semilattices *}
    1.69  
    1.70  lemma (in Lattice) ACf_inf: "ACf inf"
    1.71 @@ -2163,7 +2203,18 @@
    1.72  apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
    1.73  done
    1.74  
    1.75 -lemma (in Lattice) sup_Inf1_distrib:
    1.76 +lemma (in Lattice) sup_Inf_absorb:
    1.77 +  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
    1.78 +apply(subst sup_comm)
    1.79 +apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
    1.80 +done
    1.81 +
    1.82 +lemma (in Lattice) inf_Sup_absorb:
    1.83 +  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
    1.84 +by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
    1.85 +
    1.86 +
    1.87 +lemma (in DistribLattice) sup_Inf1_distrib:
    1.88  assumes A: "finite A" "A \<noteq> {}"
    1.89  shows "(x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
    1.90  using A
    1.91 @@ -2184,8 +2235,8 @@
    1.92    finally show ?case .
    1.93  qed
    1.94  
    1.95 -
    1.96 -lemma (in Lattice) sup_Inf2_distrib:
    1.97 +(* FIXME
    1.98 +lemma (in DistribLattice) sup_Inf2_distrib:
    1.99  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   1.100  shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
   1.101  using A
   1.102 @@ -2216,7 +2267,7 @@
   1.103      by blast
   1.104    finally show ?case .
   1.105  qed
   1.106 -
   1.107 +*)
   1.108  
   1.109  
   1.110  subsection{*Min and Max*}
   1.111 @@ -2381,10 +2432,10 @@
   1.112  lemma Min_le_Max:
   1.113    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
   1.114  by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max])
   1.115 -
   1.116 +(* FIXME
   1.117  lemma max_Min2_distrib:
   1.118    "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow>
   1.119    max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}"
   1.120  by(simp add: Min_def Max_def Lattice.sup_Inf2_distrib[OF Lattice_min_max])
   1.121 -
   1.122 +*)
   1.123  end