src/HOL/Finite_Set.thy
changeset 18493 343da052b961
parent 18423 d7859164447f
child 19279 48b527d0331b
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Dec 22 14:22:11 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Dec 22 17:57:09 2005 +0100
     1.3 @@ -1972,7 +1972,9 @@
     1.4  
     1.5  locale ACIfSL = ACIf +
     1.6    fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
     1.7 +  and strict_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
     1.8    assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
     1.9 +  defines strict_below_def:  "(x \<sqsubset> y) \<equiv> (x \<sqsubseteq> y \<and> x \<noteq> y)"
    1.10  
    1.11  locale ACIfSLlin = ACIfSL +
    1.12    assumes lin: "x\<cdot>y \<in> {x,y}"
    1.13 @@ -2036,6 +2038,17 @@
    1.14  qed
    1.15  
    1.16  
    1.17 +lemma (in ACIfSLlin) strict_below_f_conv[simp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
    1.18 +apply(simp add: strict_below_def)
    1.19 +using lin[of y z] by (auto simp:below_def ACI)
    1.20 +
    1.21 +
    1.22 +lemma (in ACIfSLlin) strict_above_f_conv:
    1.23 + "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)"
    1.24 +apply(simp add: strict_below_def above_f_conv)
    1.25 +using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
    1.26 +
    1.27 +
    1.28  subsubsection{* Lemmas about @{text fold1} *}
    1.29  
    1.30  lemma (in ACf) fold1_Un:
    1.31 @@ -2076,6 +2089,11 @@
    1.32  using A
    1.33  by(induct rule:finite_ne_induct) simp_all
    1.34  
    1.35 +lemma (in ACIfSLlin) strict_below_fold1_iff:
    1.36 +  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<sqsubset> fold1 f A = (\<forall>a\<in>A. x \<sqsubset> a)"
    1.37 +by(induct rule:finite_ne_induct) simp_all
    1.38 +
    1.39 +
    1.40  lemma (in ACIfSL) fold1_belowI:
    1.41  assumes A: "finite A" "A \<noteq> {}"
    1.42  shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
    1.43 @@ -2101,12 +2119,19 @@
    1.44    qed
    1.45  qed
    1.46  
    1.47 +
    1.48  lemma (in ACIfSLlin) fold1_below_iff:
    1.49  assumes A: "finite A" "A \<noteq> {}"
    1.50  shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
    1.51  using A
    1.52  by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
    1.53  
    1.54 +lemma (in ACIfSLlin) fold1_strict_below_iff:
    1.55 +assumes A: "finite A" "A \<noteq> {}"
    1.56 +shows "fold1 f A \<sqsubset> x = (\<exists>a\<in>A. a \<sqsubset> x)"
    1.57 +using A
    1.58 +by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
    1.59 +
    1.60  
    1.61  lemma (in ACIfSLlin) fold1_antimono:
    1.62  assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
    1.63 @@ -2120,7 +2145,7 @@
    1.64    also have "\<dots> = f (fold1 f A) (fold1 f (B-A))"
    1.65    proof -
    1.66      have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
    1.67 -    moreover have "finite(B-A)" by(blast intro:finite_Diff prems)
    1.68 +    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
    1.69      moreover have "(B-A) \<noteq> {}" using prems by blast
    1.70      moreover have "A Int (B-A) = {}" using prems by blast
    1.71      ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
    1.72 @@ -2130,6 +2155,7 @@
    1.73  qed
    1.74  
    1.75  
    1.76 +
    1.77  subsubsection{* Lattices *}
    1.78  
    1.79  locale Lattice = lattice +
    1.80 @@ -2342,25 +2368,27 @@
    1.81  done
    1.82  
    1.83  interpretation min:
    1.84 -  ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
    1.85 +  ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
    1.86 +apply(simp add:order_less_le)
    1.87  apply(rule ACIfSL_axioms.intro)
    1.88  apply(auto simp:min_def)
    1.89  done
    1.90  
    1.91  interpretation min:
    1.92 -  ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
    1.93 +  ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
    1.94  apply(rule ACIfSLlin_axioms.intro)
    1.95  apply(auto simp:min_def)
    1.96  done
    1.97  
    1.98  interpretation max:
    1.99 -  ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
   1.100 +  ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
   1.101 +apply(simp add:order_less_le eq_sym_conv)
   1.102  apply(rule ACIfSL_axioms.intro)
   1.103  apply(auto simp:max_def)
   1.104  done
   1.105  
   1.106  interpretation max:
   1.107 -  ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
   1.108 +  ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
   1.109  apply(rule ACIfSLlin_axioms.intro)
   1.110  apply(auto simp:max_def)
   1.111  done
   1.112 @@ -2424,6 +2452,14 @@
   1.113    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
   1.114  by(simp add: Max_def max.below_fold1_iff)
   1.115  
   1.116 +lemma Min_gr_iff[simp]:
   1.117 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x < Min A) = (\<forall>a\<in>A. x < a)"
   1.118 +by(simp add: Min_def min.strict_below_fold1_iff)
   1.119 +
   1.120 +lemma Max_less_iff[simp]:
   1.121 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A < x) = (\<forall>a\<in>A. a < x)"
   1.122 +by(simp add: Max_def max.strict_below_fold1_iff)
   1.123 +
   1.124  lemma Min_le_iff:
   1.125    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
   1.126  by(simp add: Min_def min.fold1_below_iff)
   1.127 @@ -2432,6 +2468,14 @@
   1.128    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
   1.129  by(simp add: Max_def max.fold1_below_iff)
   1.130  
   1.131 +lemma Min_le_iff:
   1.132 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A < x) = (\<exists>a\<in>A. a < x)"
   1.133 +by(simp add: Min_def min.fold1_strict_below_iff)
   1.134 +
   1.135 +lemma Max_ge_iff:
   1.136 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x < Max A) = (\<exists>a\<in>A. x < a)"
   1.137 +by(simp add: Max_def max.fold1_strict_below_iff)
   1.138 +
   1.139  lemma Min_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
   1.140    \<Longrightarrow> Min (A \<union> B) = min (Min A) (Min B)"
   1.141  by(simp add:Min_def min.f.fold1_Un2)