more lemmas
authornipkow
Thu Dec 22 17:57:09 2005 +0100 (2005-12-22)
changeset 18493343da052b961
parent 18492 b0fe60800623
child 18494 00190b1fa5b3
more lemmas
src/HOL/Equiv_Relations.thy
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Dec 22 14:22:11 2005 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Dec 22 17:57:09 2005 +0100
     1.3 @@ -90,10 +90,6 @@
     1.4    "equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)"
     1.5    by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
     1.6  
     1.7 -lemma eq_equiv_class_iff2:
     1.8 -  "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)"
     1.9 -by(simp add:quotient_def eq_equiv_class_iff)
    1.10 -
    1.11  
    1.12  subsection {* Quotients *}
    1.13  
    1.14 @@ -136,6 +132,10 @@
    1.15    apply (unfold equiv_def sym_def trans_def, blast)
    1.16    done
    1.17  
    1.18 +lemma eq_equiv_class_iff2:
    1.19 +  "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)"
    1.20 +by(simp add:quotient_def eq_equiv_class_iff)
    1.21 +
    1.22  
    1.23  lemma quotient_empty [simp]: "{}//r = {}"
    1.24  by(simp add: quotient_def)
     2.1 --- a/src/HOL/Finite_Set.thy	Thu Dec 22 14:22:11 2005 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Thu Dec 22 17:57:09 2005 +0100
     2.3 @@ -1972,7 +1972,9 @@
     2.4  
     2.5  locale ACIfSL = ACIf +
     2.6    fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
     2.7 +  and strict_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
     2.8    assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
     2.9 +  defines strict_below_def:  "(x \<sqsubset> y) \<equiv> (x \<sqsubseteq> y \<and> x \<noteq> y)"
    2.10  
    2.11  locale ACIfSLlin = ACIfSL +
    2.12    assumes lin: "x\<cdot>y \<in> {x,y}"
    2.13 @@ -2036,6 +2038,17 @@
    2.14  qed
    2.15  
    2.16  
    2.17 +lemma (in ACIfSLlin) strict_below_f_conv[simp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
    2.18 +apply(simp add: strict_below_def)
    2.19 +using lin[of y z] by (auto simp:below_def ACI)
    2.20 +
    2.21 +
    2.22 +lemma (in ACIfSLlin) strict_above_f_conv:
    2.23 + "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)"
    2.24 +apply(simp add: strict_below_def above_f_conv)
    2.25 +using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
    2.26 +
    2.27 +
    2.28  subsubsection{* Lemmas about @{text fold1} *}
    2.29  
    2.30  lemma (in ACf) fold1_Un:
    2.31 @@ -2076,6 +2089,11 @@
    2.32  using A
    2.33  by(induct rule:finite_ne_induct) simp_all
    2.34  
    2.35 +lemma (in ACIfSLlin) strict_below_fold1_iff:
    2.36 +  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<sqsubset> fold1 f A = (\<forall>a\<in>A. x \<sqsubset> a)"
    2.37 +by(induct rule:finite_ne_induct) simp_all
    2.38 +
    2.39 +
    2.40  lemma (in ACIfSL) fold1_belowI:
    2.41  assumes A: "finite A" "A \<noteq> {}"
    2.42  shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
    2.43 @@ -2101,12 +2119,19 @@
    2.44    qed
    2.45  qed
    2.46  
    2.47 +
    2.48  lemma (in ACIfSLlin) fold1_below_iff:
    2.49  assumes A: "finite A" "A \<noteq> {}"
    2.50  shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
    2.51  using A
    2.52  by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
    2.53  
    2.54 +lemma (in ACIfSLlin) fold1_strict_below_iff:
    2.55 +assumes A: "finite A" "A \<noteq> {}"
    2.56 +shows "fold1 f A \<sqsubset> x = (\<exists>a\<in>A. a \<sqsubset> x)"
    2.57 +using A
    2.58 +by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
    2.59 +
    2.60  
    2.61  lemma (in ACIfSLlin) fold1_antimono:
    2.62  assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
    2.63 @@ -2120,7 +2145,7 @@
    2.64    also have "\<dots> = f (fold1 f A) (fold1 f (B-A))"
    2.65    proof -
    2.66      have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
    2.67 -    moreover have "finite(B-A)" by(blast intro:finite_Diff prems)
    2.68 +    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
    2.69      moreover have "(B-A) \<noteq> {}" using prems by blast
    2.70      moreover have "A Int (B-A) = {}" using prems by blast
    2.71      ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
    2.72 @@ -2130,6 +2155,7 @@
    2.73  qed
    2.74  
    2.75  
    2.76 +
    2.77  subsubsection{* Lattices *}
    2.78  
    2.79  locale Lattice = lattice +
    2.80 @@ -2342,25 +2368,27 @@
    2.81  done
    2.82  
    2.83  interpretation min:
    2.84 -  ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
    2.85 +  ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
    2.86 +apply(simp add:order_less_le)
    2.87  apply(rule ACIfSL_axioms.intro)
    2.88  apply(auto simp:min_def)
    2.89  done
    2.90  
    2.91  interpretation min:
    2.92 -  ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
    2.93 +  ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
    2.94  apply(rule ACIfSLlin_axioms.intro)
    2.95  apply(auto simp:min_def)
    2.96  done
    2.97  
    2.98  interpretation max:
    2.99 -  ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
   2.100 +  ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
   2.101 +apply(simp add:order_less_le eq_sym_conv)
   2.102  apply(rule ACIfSL_axioms.intro)
   2.103  apply(auto simp:max_def)
   2.104  done
   2.105  
   2.106  interpretation max:
   2.107 -  ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
   2.108 +  ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
   2.109  apply(rule ACIfSLlin_axioms.intro)
   2.110  apply(auto simp:max_def)
   2.111  done
   2.112 @@ -2424,6 +2452,14 @@
   2.113    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
   2.114  by(simp add: Max_def max.below_fold1_iff)
   2.115  
   2.116 +lemma Min_gr_iff[simp]:
   2.117 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x < Min A) = (\<forall>a\<in>A. x < a)"
   2.118 +by(simp add: Min_def min.strict_below_fold1_iff)
   2.119 +
   2.120 +lemma Max_less_iff[simp]:
   2.121 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A < x) = (\<forall>a\<in>A. a < x)"
   2.122 +by(simp add: Max_def max.strict_below_fold1_iff)
   2.123 +
   2.124  lemma Min_le_iff:
   2.125    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
   2.126  by(simp add: Min_def min.fold1_below_iff)
   2.127 @@ -2432,6 +2468,14 @@
   2.128    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
   2.129  by(simp add: Max_def max.fold1_below_iff)
   2.130  
   2.131 +lemma Min_le_iff:
   2.132 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A < x) = (\<exists>a\<in>A. a < x)"
   2.133 +by(simp add: Min_def min.fold1_strict_below_iff)
   2.134 +
   2.135 +lemma Max_ge_iff:
   2.136 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x < Max A) = (\<exists>a\<in>A. x < a)"
   2.137 +by(simp add: Max_def max.fold1_strict_below_iff)
   2.138 +
   2.139  lemma Min_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
   2.140    \<Longrightarrow> Min (A \<union> B) = min (Min A) (Min B)"
   2.141  by(simp add:Min_def min.f.fold1_Un2)