src/HOL/SetInterval.thy
changeset 15418 e28853da5df5
parent 15402 97204f3b4705
child 15539 333a88244569
     1.1 --- a/src/HOL/SetInterval.thy	Fri Dec 17 10:15:10 2004 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Fri Dec 17 10:15:46 2004 +0100
     1.3 @@ -87,7 +87,7 @@
     1.4  lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
     1.5  by (simp add: lessThan_def)
     1.6  
     1.7 -lemma Compl_lessThan [simp]: 
     1.8 +lemma Compl_lessThan [simp]:
     1.9      "!!k:: 'a::linorder. -lessThan k = atLeast k"
    1.10  apply (auto simp add: lessThan_def atLeast_def)
    1.11  done
    1.12 @@ -98,20 +98,20 @@
    1.13  lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
    1.14  by (simp add: greaterThan_def)
    1.15  
    1.16 -lemma Compl_greaterThan [simp]: 
    1.17 +lemma Compl_greaterThan [simp]:
    1.18      "!!k:: 'a::linorder. -greaterThan k = atMost k"
    1.19  apply (simp add: greaterThan_def atMost_def le_def, auto)
    1.20  done
    1.21  
    1.22  lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
    1.23  apply (subst Compl_greaterThan [symmetric])
    1.24 -apply (rule double_complement) 
    1.25 +apply (rule double_complement)
    1.26  done
    1.27  
    1.28  lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
    1.29  by (simp add: atLeast_def)
    1.30  
    1.31 -lemma Compl_atLeast [simp]: 
    1.32 +lemma Compl_atLeast [simp]:
    1.33      "!!k:: 'a::linorder. -atLeast k = lessThan k"
    1.34  apply (simp add: lessThan_def atLeast_def le_def, auto)
    1.35  done
    1.36 @@ -126,43 +126,43 @@
    1.37  subsection {* Logical Equivalences for Set Inclusion and Equality *}
    1.38  
    1.39  lemma atLeast_subset_iff [iff]:
    1.40 -     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
    1.41 -by (blast intro: order_trans) 
    1.42 +     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
    1.43 +by (blast intro: order_trans)
    1.44  
    1.45  lemma atLeast_eq_iff [iff]:
    1.46 -     "(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
    1.47 +     "(atLeast x = atLeast y) = (x = (y::'a::linorder))"
    1.48  by (blast intro: order_antisym order_trans)
    1.49  
    1.50  lemma greaterThan_subset_iff [iff]:
    1.51 -     "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 
    1.52 -apply (auto simp add: greaterThan_def) 
    1.53 - apply (subst linorder_not_less [symmetric], blast) 
    1.54 +     "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))"
    1.55 +apply (auto simp add: greaterThan_def)
    1.56 + apply (subst linorder_not_less [symmetric], blast)
    1.57  done
    1.58  
    1.59  lemma greaterThan_eq_iff [iff]:
    1.60 -     "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 
    1.61 -apply (rule iffI) 
    1.62 - apply (erule equalityE) 
    1.63 - apply (simp add: greaterThan_subset_iff order_antisym, simp) 
    1.64 +     "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
    1.65 +apply (rule iffI)
    1.66 + apply (erule equalityE)
    1.67 + apply (simp_all add: greaterThan_subset_iff)
    1.68  done
    1.69  
    1.70 -lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" 
    1.71 +lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
    1.72  by (blast intro: order_trans)
    1.73  
    1.74 -lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
    1.75 +lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"
    1.76  by (blast intro: order_antisym order_trans)
    1.77  
    1.78  lemma lessThan_subset_iff [iff]:
    1.79 -     "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 
    1.80 -apply (auto simp add: lessThan_def) 
    1.81 - apply (subst linorder_not_less [symmetric], blast) 
    1.82 +     "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))"
    1.83 +apply (auto simp add: lessThan_def)
    1.84 + apply (subst linorder_not_less [symmetric], blast)
    1.85  done
    1.86  
    1.87  lemma lessThan_eq_iff [iff]:
    1.88 -     "(lessThan x = lessThan y) = (x = (y::'a::linorder))" 
    1.89 -apply (rule iffI) 
    1.90 - apply (erule equalityE) 
    1.91 - apply (simp add: lessThan_subset_iff order_antisym, simp) 
    1.92 +     "(lessThan x = lessThan y) = (x = (y::'a::linorder))"
    1.93 +apply (rule iffI)
    1.94 + apply (erule equalityE)
    1.95 + apply (simp_all add: lessThan_subset_iff)
    1.96  done
    1.97  
    1.98  
    1.99 @@ -279,9 +279,9 @@
   1.100  text{*Not a simprule because the RHS is too messy.*}
   1.101  lemma atLeastLessThanSuc:
   1.102      "{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})"
   1.103 -by (auto simp add: atLeastLessThan_def) 
   1.104 +by (auto simp add: atLeastLessThan_def)
   1.105  
   1.106 -lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
   1.107 +lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}"
   1.108  by (auto simp add: atLeastLessThan_def)
   1.109  
   1.110  lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
   1.111 @@ -293,12 +293,12 @@
   1.112  lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
   1.113    by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
   1.114  
   1.115 -lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"  
   1.116 -  by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
   1.117 +lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"
   1.118 +  by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
   1.119      greaterThanAtMost_def)
   1.120  
   1.121 -lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"  
   1.122 -  by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
   1.123 +lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"
   1.124 +  by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
   1.125      greaterThanLessThan_def)
   1.126  
   1.127  subsubsection {* Finiteness *}
   1.128 @@ -353,10 +353,10 @@
   1.129    apply arith
   1.130    done
   1.131  
   1.132 -lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"  
   1.133 +lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
   1.134    by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
   1.135  
   1.136 -lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l" 
   1.137 +lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"
   1.138    by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
   1.139  
   1.140  lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
   1.141 @@ -367,16 +367,16 @@
   1.142  lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
   1.143    by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
   1.144  
   1.145 -lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"  
   1.146 +lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"
   1.147    by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
   1.148  
   1.149 -lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 
   1.150 -    "{l+1..<u} = {l<..<u::int}"  
   1.151 +lemma atLeastPlusOneLessThan_greaterThanLessThan_int:
   1.152 +    "{l+1..<u} = {l<..<u::int}"
   1.153    by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
   1.154  
   1.155  subsubsection {* Finiteness *}
   1.156  
   1.157 -lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
   1.158 +lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
   1.159      {(0::int)..<u} = int ` {..<nat u}"
   1.160    apply (unfold image_def lessThan_def)
   1.161    apply auto
   1.162 @@ -393,7 +393,7 @@
   1.163    apply auto
   1.164    done
   1.165  
   1.166 -lemma image_atLeastLessThan_int_shift: 
   1.167 +lemma image_atLeastLessThan_int_shift:
   1.168      "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
   1.169    apply (auto simp add: image_def atLeastLessThan_iff)
   1.170    apply (rule_tac x = "x - l" in bexI)
   1.171 @@ -408,13 +408,13 @@
   1.172    apply (rule image_atLeastLessThan_int_shift)
   1.173    done
   1.174  
   1.175 -lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
   1.176 +lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
   1.177    by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
   1.178  
   1.179 -lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 
   1.180 +lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}"
   1.181    by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   1.182  
   1.183 -lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 
   1.184 +lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}"
   1.185    by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
   1.186  
   1.187  subsubsection {* Cardinality *}
   1.188 @@ -441,7 +441,7 @@
   1.189    apply (auto simp add: compare_rls)
   1.190    done
   1.191  
   1.192 -lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" 
   1.193 +lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)"
   1.194    by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   1.195  
   1.196  lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
   1.197 @@ -589,4 +589,56 @@
   1.198  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
   1.199  by (simp add:lessThan_Suc)
   1.200  
   1.201 +
   1.202 +ML
   1.203 +{*
   1.204 +val Compl_atLeast = thm "Compl_atLeast";
   1.205 +val Compl_atMost = thm "Compl_atMost";
   1.206 +val Compl_greaterThan = thm "Compl_greaterThan";
   1.207 +val Compl_lessThan = thm "Compl_lessThan";
   1.208 +val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV";
   1.209 +val UN_atLeast_UNIV = thm "UN_atLeast_UNIV";
   1.210 +val UN_atMost_UNIV = thm "UN_atMost_UNIV";
   1.211 +val UN_lessThan_UNIV = thm "UN_lessThan_UNIV";
   1.212 +val atLeastAtMost_def = thm "atLeastAtMost_def";
   1.213 +val atLeastAtMost_iff = thm "atLeastAtMost_iff";
   1.214 +val atLeastLessThan_def  = thm "atLeastLessThan_def";
   1.215 +val atLeastLessThan_iff = thm "atLeastLessThan_iff";
   1.216 +val atLeast_0 = thm "atLeast_0";
   1.217 +val atLeast_Suc = thm "atLeast_Suc";
   1.218 +val atLeast_def      = thm "atLeast_def";
   1.219 +val atLeast_iff = thm "atLeast_iff";
   1.220 +val atMost_0 = thm "atMost_0";
   1.221 +val atMost_Int_atLeast = thm "atMost_Int_atLeast";
   1.222 +val atMost_Suc = thm "atMost_Suc";
   1.223 +val atMost_def       = thm "atMost_def";
   1.224 +val atMost_iff = thm "atMost_iff";
   1.225 +val greaterThanAtMost_def  = thm "greaterThanAtMost_def";
   1.226 +val greaterThanAtMost_iff = thm "greaterThanAtMost_iff";
   1.227 +val greaterThanLessThan_def  = thm "greaterThanLessThan_def";
   1.228 +val greaterThanLessThan_iff = thm "greaterThanLessThan_iff";
   1.229 +val greaterThan_0 = thm "greaterThan_0";
   1.230 +val greaterThan_Suc = thm "greaterThan_Suc";
   1.231 +val greaterThan_def  = thm "greaterThan_def";
   1.232 +val greaterThan_iff = thm "greaterThan_iff";
   1.233 +val ivl_disj_int = thms "ivl_disj_int";
   1.234 +val ivl_disj_int_one = thms "ivl_disj_int_one";
   1.235 +val ivl_disj_int_singleton = thms "ivl_disj_int_singleton";
   1.236 +val ivl_disj_int_two = thms "ivl_disj_int_two";
   1.237 +val ivl_disj_un = thms "ivl_disj_un";
   1.238 +val ivl_disj_un_one = thms "ivl_disj_un_one";
   1.239 +val ivl_disj_un_singleton = thms "ivl_disj_un_singleton";
   1.240 +val ivl_disj_un_two = thms "ivl_disj_un_two";
   1.241 +val lessThan_0 = thm "lessThan_0";
   1.242 +val lessThan_Suc = thm "lessThan_Suc";
   1.243 +val lessThan_Suc_atMost = thm "lessThan_Suc_atMost";
   1.244 +val lessThan_def     = thm "lessThan_def";
   1.245 +val lessThan_iff = thm "lessThan_iff";
   1.246 +val single_Diff_lessThan = thm "single_Diff_lessThan";
   1.247 +
   1.248 +val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
   1.249 +val finite_atMost = thm "finite_atMost";
   1.250 +val finite_lessThan = thm "finite_lessThan";
   1.251 +*}
   1.252 +
   1.253  end