removed two looping simplifications in SetInterval.thy; deleted the .ML file
authorpaulson
Fri Dec 17 10:15:46 2004 +0100 (2004-12-17)
changeset 15418e28853da5df5
parent 15417 b488b290eccb
child 15419 1d63862c70d9
removed two looping simplifications in SetInterval.thy; deleted the .ML file
src/HOL/IsaMakefile
src/HOL/SetInterval.ML
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Dec 17 10:15:10 2004 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Dec 17 10:15:46 2004 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4    Refute.thy ROOT.ML \
     1.5    Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \
     1.6    Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
     1.7 -  Set.ML Set.thy SetInterval.ML SetInterval.thy \
     1.8 +  Set.ML Set.thy SetInterval.thy \
     1.9    Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
    1.10    Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
    1.11    Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
     2.1 --- a/src/HOL/SetInterval.ML	Fri Dec 17 10:15:10 2004 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,55 +0,0 @@
     2.4 -(*  Title:      HOL/SetInterval.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Clemens Ballarin
     2.7 -    Copyright   2002  TU Muenchen
     2.8 -*)
     2.9 -
    2.10 -(* Legacy ML bindings *)
    2.11 -
    2.12 -val Compl_atLeast = thm "Compl_atLeast";
    2.13 -val Compl_atMost = thm "Compl_atMost";
    2.14 -val Compl_greaterThan = thm "Compl_greaterThan";
    2.15 -val Compl_lessThan = thm "Compl_lessThan";
    2.16 -val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV";
    2.17 -val UN_atLeast_UNIV = thm "UN_atLeast_UNIV";
    2.18 -val UN_atMost_UNIV = thm "UN_atMost_UNIV";
    2.19 -val UN_lessThan_UNIV = thm "UN_lessThan_UNIV";
    2.20 -val atLeastAtMost_def = thm "atLeastAtMost_def";
    2.21 -val atLeastAtMost_iff = thm "atLeastAtMost_iff";
    2.22 -val atLeastLessThan_def  = thm "atLeastLessThan_def";
    2.23 -val atLeastLessThan_iff = thm "atLeastLessThan_iff";
    2.24 -val atLeast_0 = thm "atLeast_0";
    2.25 -val atLeast_Suc = thm "atLeast_Suc";
    2.26 -val atLeast_def      = thm "atLeast_def";
    2.27 -val atLeast_iff = thm "atLeast_iff";
    2.28 -val atMost_0 = thm "atMost_0";
    2.29 -val atMost_Int_atLeast = thm "atMost_Int_atLeast";
    2.30 -val atMost_Suc = thm "atMost_Suc";
    2.31 -val atMost_def       = thm "atMost_def";
    2.32 -val atMost_iff = thm "atMost_iff";
    2.33 -val greaterThanAtMost_def  = thm "greaterThanAtMost_def";
    2.34 -val greaterThanAtMost_iff = thm "greaterThanAtMost_iff";
    2.35 -val greaterThanLessThan_def  = thm "greaterThanLessThan_def";
    2.36 -val greaterThanLessThan_iff = thm "greaterThanLessThan_iff";
    2.37 -val greaterThan_0 = thm "greaterThan_0";
    2.38 -val greaterThan_Suc = thm "greaterThan_Suc";
    2.39 -val greaterThan_def  = thm "greaterThan_def";
    2.40 -val greaterThan_iff = thm "greaterThan_iff";
    2.41 -val ivl_disj_int = thms "ivl_disj_int";
    2.42 -val ivl_disj_int_one = thms "ivl_disj_int_one";
    2.43 -val ivl_disj_int_singleton = thms "ivl_disj_int_singleton";
    2.44 -val ivl_disj_int_two = thms "ivl_disj_int_two";
    2.45 -val ivl_disj_un = thms "ivl_disj_un";
    2.46 -val ivl_disj_un_one = thms "ivl_disj_un_one";
    2.47 -val ivl_disj_un_singleton = thms "ivl_disj_un_singleton";
    2.48 -val ivl_disj_un_two = thms "ivl_disj_un_two";
    2.49 -val lessThan_0 = thm "lessThan_0";
    2.50 -val lessThan_Suc = thm "lessThan_Suc";
    2.51 -val lessThan_Suc_atMost = thm "lessThan_Suc_atMost";
    2.52 -val lessThan_def     = thm "lessThan_def";
    2.53 -val lessThan_iff = thm "lessThan_iff";
    2.54 -val single_Diff_lessThan = thm "single_Diff_lessThan";
    2.55 -
    2.56 -val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
    2.57 -val finite_atMost = thm "finite_atMost";
    2.58 -val finite_lessThan = thm "finite_lessThan";
     3.1 --- a/src/HOL/SetInterval.thy	Fri Dec 17 10:15:10 2004 +0100
     3.2 +++ b/src/HOL/SetInterval.thy	Fri Dec 17 10:15:46 2004 +0100
     3.3 @@ -87,7 +87,7 @@
     3.4  lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
     3.5  by (simp add: lessThan_def)
     3.6  
     3.7 -lemma Compl_lessThan [simp]: 
     3.8 +lemma Compl_lessThan [simp]:
     3.9      "!!k:: 'a::linorder. -lessThan k = atLeast k"
    3.10  apply (auto simp add: lessThan_def atLeast_def)
    3.11  done
    3.12 @@ -98,20 +98,20 @@
    3.13  lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
    3.14  by (simp add: greaterThan_def)
    3.15  
    3.16 -lemma Compl_greaterThan [simp]: 
    3.17 +lemma Compl_greaterThan [simp]:
    3.18      "!!k:: 'a::linorder. -greaterThan k = atMost k"
    3.19  apply (simp add: greaterThan_def atMost_def le_def, auto)
    3.20  done
    3.21  
    3.22  lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
    3.23  apply (subst Compl_greaterThan [symmetric])
    3.24 -apply (rule double_complement) 
    3.25 +apply (rule double_complement)
    3.26  done
    3.27  
    3.28  lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
    3.29  by (simp add: atLeast_def)
    3.30  
    3.31 -lemma Compl_atLeast [simp]: 
    3.32 +lemma Compl_atLeast [simp]:
    3.33      "!!k:: 'a::linorder. -atLeast k = lessThan k"
    3.34  apply (simp add: lessThan_def atLeast_def le_def, auto)
    3.35  done
    3.36 @@ -126,43 +126,43 @@
    3.37  subsection {* Logical Equivalences for Set Inclusion and Equality *}
    3.38  
    3.39  lemma atLeast_subset_iff [iff]:
    3.40 -     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
    3.41 -by (blast intro: order_trans) 
    3.42 +     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
    3.43 +by (blast intro: order_trans)
    3.44  
    3.45  lemma atLeast_eq_iff [iff]:
    3.46 -     "(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
    3.47 +     "(atLeast x = atLeast y) = (x = (y::'a::linorder))"
    3.48  by (blast intro: order_antisym order_trans)
    3.49  
    3.50  lemma greaterThan_subset_iff [iff]:
    3.51 -     "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 
    3.52 -apply (auto simp add: greaterThan_def) 
    3.53 - apply (subst linorder_not_less [symmetric], blast) 
    3.54 +     "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))"
    3.55 +apply (auto simp add: greaterThan_def)
    3.56 + apply (subst linorder_not_less [symmetric], blast)
    3.57  done
    3.58  
    3.59  lemma greaterThan_eq_iff [iff]:
    3.60 -     "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 
    3.61 -apply (rule iffI) 
    3.62 - apply (erule equalityE) 
    3.63 - apply (simp add: greaterThan_subset_iff order_antisym, simp) 
    3.64 +     "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
    3.65 +apply (rule iffI)
    3.66 + apply (erule equalityE)
    3.67 + apply (simp_all add: greaterThan_subset_iff)
    3.68  done
    3.69  
    3.70 -lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" 
    3.71 +lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
    3.72  by (blast intro: order_trans)
    3.73  
    3.74 -lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
    3.75 +lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"
    3.76  by (blast intro: order_antisym order_trans)
    3.77  
    3.78  lemma lessThan_subset_iff [iff]:
    3.79 -     "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 
    3.80 -apply (auto simp add: lessThan_def) 
    3.81 - apply (subst linorder_not_less [symmetric], blast) 
    3.82 +     "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))"
    3.83 +apply (auto simp add: lessThan_def)
    3.84 + apply (subst linorder_not_less [symmetric], blast)
    3.85  done
    3.86  
    3.87  lemma lessThan_eq_iff [iff]:
    3.88 -     "(lessThan x = lessThan y) = (x = (y::'a::linorder))" 
    3.89 -apply (rule iffI) 
    3.90 - apply (erule equalityE) 
    3.91 - apply (simp add: lessThan_subset_iff order_antisym, simp) 
    3.92 +     "(lessThan x = lessThan y) = (x = (y::'a::linorder))"
    3.93 +apply (rule iffI)
    3.94 + apply (erule equalityE)
    3.95 + apply (simp_all add: lessThan_subset_iff)
    3.96  done
    3.97  
    3.98  
    3.99 @@ -279,9 +279,9 @@
   3.100  text{*Not a simprule because the RHS is too messy.*}
   3.101  lemma atLeastLessThanSuc:
   3.102      "{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})"
   3.103 -by (auto simp add: atLeastLessThan_def) 
   3.104 +by (auto simp add: atLeastLessThan_def)
   3.105  
   3.106 -lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
   3.107 +lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}"
   3.108  by (auto simp add: atLeastLessThan_def)
   3.109  
   3.110  lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
   3.111 @@ -293,12 +293,12 @@
   3.112  lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
   3.113    by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
   3.114  
   3.115 -lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"  
   3.116 -  by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
   3.117 +lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"
   3.118 +  by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
   3.119      greaterThanAtMost_def)
   3.120  
   3.121 -lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"  
   3.122 -  by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
   3.123 +lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"
   3.124 +  by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
   3.125      greaterThanLessThan_def)
   3.126  
   3.127  subsubsection {* Finiteness *}
   3.128 @@ -353,10 +353,10 @@
   3.129    apply arith
   3.130    done
   3.131  
   3.132 -lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"  
   3.133 +lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
   3.134    by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
   3.135  
   3.136 -lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l" 
   3.137 +lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"
   3.138    by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
   3.139  
   3.140  lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
   3.141 @@ -367,16 +367,16 @@
   3.142  lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
   3.143    by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
   3.144  
   3.145 -lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"  
   3.146 +lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"
   3.147    by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
   3.148  
   3.149 -lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 
   3.150 -    "{l+1..<u} = {l<..<u::int}"  
   3.151 +lemma atLeastPlusOneLessThan_greaterThanLessThan_int:
   3.152 +    "{l+1..<u} = {l<..<u::int}"
   3.153    by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
   3.154  
   3.155  subsubsection {* Finiteness *}
   3.156  
   3.157 -lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
   3.158 +lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
   3.159      {(0::int)..<u} = int ` {..<nat u}"
   3.160    apply (unfold image_def lessThan_def)
   3.161    apply auto
   3.162 @@ -393,7 +393,7 @@
   3.163    apply auto
   3.164    done
   3.165  
   3.166 -lemma image_atLeastLessThan_int_shift: 
   3.167 +lemma image_atLeastLessThan_int_shift:
   3.168      "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
   3.169    apply (auto simp add: image_def atLeastLessThan_iff)
   3.170    apply (rule_tac x = "x - l" in bexI)
   3.171 @@ -408,13 +408,13 @@
   3.172    apply (rule image_atLeastLessThan_int_shift)
   3.173    done
   3.174  
   3.175 -lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
   3.176 +lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
   3.177    by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
   3.178  
   3.179 -lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 
   3.180 +lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}"
   3.181    by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   3.182  
   3.183 -lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 
   3.184 +lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}"
   3.185    by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
   3.186  
   3.187  subsubsection {* Cardinality *}
   3.188 @@ -441,7 +441,7 @@
   3.189    apply (auto simp add: compare_rls)
   3.190    done
   3.191  
   3.192 -lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" 
   3.193 +lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)"
   3.194    by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   3.195  
   3.196  lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
   3.197 @@ -589,4 +589,56 @@
   3.198  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
   3.199  by (simp add:lessThan_Suc)
   3.200  
   3.201 +
   3.202 +ML
   3.203 +{*
   3.204 +val Compl_atLeast = thm "Compl_atLeast";
   3.205 +val Compl_atMost = thm "Compl_atMost";
   3.206 +val Compl_greaterThan = thm "Compl_greaterThan";
   3.207 +val Compl_lessThan = thm "Compl_lessThan";
   3.208 +val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV";
   3.209 +val UN_atLeast_UNIV = thm "UN_atLeast_UNIV";
   3.210 +val UN_atMost_UNIV = thm "UN_atMost_UNIV";
   3.211 +val UN_lessThan_UNIV = thm "UN_lessThan_UNIV";
   3.212 +val atLeastAtMost_def = thm "atLeastAtMost_def";
   3.213 +val atLeastAtMost_iff = thm "atLeastAtMost_iff";
   3.214 +val atLeastLessThan_def  = thm "atLeastLessThan_def";
   3.215 +val atLeastLessThan_iff = thm "atLeastLessThan_iff";
   3.216 +val atLeast_0 = thm "atLeast_0";
   3.217 +val atLeast_Suc = thm "atLeast_Suc";
   3.218 +val atLeast_def      = thm "atLeast_def";
   3.219 +val atLeast_iff = thm "atLeast_iff";
   3.220 +val atMost_0 = thm "atMost_0";
   3.221 +val atMost_Int_atLeast = thm "atMost_Int_atLeast";
   3.222 +val atMost_Suc = thm "atMost_Suc";
   3.223 +val atMost_def       = thm "atMost_def";
   3.224 +val atMost_iff = thm "atMost_iff";
   3.225 +val greaterThanAtMost_def  = thm "greaterThanAtMost_def";
   3.226 +val greaterThanAtMost_iff = thm "greaterThanAtMost_iff";
   3.227 +val greaterThanLessThan_def  = thm "greaterThanLessThan_def";
   3.228 +val greaterThanLessThan_iff = thm "greaterThanLessThan_iff";
   3.229 +val greaterThan_0 = thm "greaterThan_0";
   3.230 +val greaterThan_Suc = thm "greaterThan_Suc";
   3.231 +val greaterThan_def  = thm "greaterThan_def";
   3.232 +val greaterThan_iff = thm "greaterThan_iff";
   3.233 +val ivl_disj_int = thms "ivl_disj_int";
   3.234 +val ivl_disj_int_one = thms "ivl_disj_int_one";
   3.235 +val ivl_disj_int_singleton = thms "ivl_disj_int_singleton";
   3.236 +val ivl_disj_int_two = thms "ivl_disj_int_two";
   3.237 +val ivl_disj_un = thms "ivl_disj_un";
   3.238 +val ivl_disj_un_one = thms "ivl_disj_un_one";
   3.239 +val ivl_disj_un_singleton = thms "ivl_disj_un_singleton";
   3.240 +val ivl_disj_un_two = thms "ivl_disj_un_two";
   3.241 +val lessThan_0 = thm "lessThan_0";
   3.242 +val lessThan_Suc = thm "lessThan_Suc";
   3.243 +val lessThan_Suc_atMost = thm "lessThan_Suc_atMost";
   3.244 +val lessThan_def     = thm "lessThan_def";
   3.245 +val lessThan_iff = thm "lessThan_iff";
   3.246 +val single_Diff_lessThan = thm "single_Diff_lessThan";
   3.247 +
   3.248 +val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
   3.249 +val finite_atMost = thm "finite_atMost";
   3.250 +val finite_lessThan = thm "finite_lessThan";
   3.251 +*}
   3.252 +
   3.253  end