new logical equivalences
authorpaulson
Thu Mar 06 15:03:16 2003 +0100 (2003-03-06)
changeset 138506d1bb3059818
parent 13849 2584233cf3ef
child 13851 f6923453953a
new logical equivalences
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/SetInterval.thy	Thu Mar 06 15:02:51 2003 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Mar 06 15:03:16 2003 +0100
     1.3 @@ -33,7 +33,8 @@
     1.4    atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
     1.5    "{l..u} == {l..} Int {..u}"
     1.6  
     1.7 -(* Setup of transitivity reasoner *)
     1.8 +
     1.9 +subsection {* Setup of transitivity reasoner *}
    1.10  
    1.11  ML {*
    1.12  
    1.13 @@ -73,156 +74,158 @@
    1.14    {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *}
    1.15    {* simple transitivity reasoner *}
    1.16  
    1.17 -(*** lessThan ***)
    1.18  
    1.19 -lemma lessThan_iff: "(i: lessThan k) = (i<k)"
    1.20 +subsection {*lessThan*}
    1.21  
    1.22 -apply (unfold lessThan_def)
    1.23 -apply blast
    1.24 -done
    1.25 -declare lessThan_iff [iff]
    1.26 +lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
    1.27 +by (simp add: lessThan_def)
    1.28  
    1.29 -lemma lessThan_0: "lessThan (0::nat) = {}"
    1.30 -apply (unfold lessThan_def)
    1.31 -apply (simp (no_asm))
    1.32 -done
    1.33 -declare lessThan_0 [simp]
    1.34 +lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
    1.35 +by (simp add: lessThan_def)
    1.36  
    1.37  lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
    1.38 -apply (unfold lessThan_def)
    1.39 -apply (simp (no_asm) add: less_Suc_eq)
    1.40 -apply blast
    1.41 -done
    1.42 +by (simp add: lessThan_def less_Suc_eq, blast)
    1.43  
    1.44  lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
    1.45 -apply (unfold lessThan_def atMost_def)
    1.46 -apply (simp (no_asm) add: less_Suc_eq_le)
    1.47 -done
    1.48 +by (simp add: lessThan_def atMost_def less_Suc_eq_le)
    1.49  
    1.50  lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
    1.51 -apply blast
    1.52 -done
    1.53 +by blast
    1.54  
    1.55 -lemma Compl_lessThan: 
    1.56 +lemma Compl_lessThan [simp]: 
    1.57      "!!k:: 'a::linorder. -lessThan k = atLeast k"
    1.58 -apply (unfold lessThan_def atLeast_def)
    1.59 -apply auto
    1.60 -apply (blast intro: linorder_not_less [THEN iffD1])
    1.61 +apply (auto simp add: lessThan_def atLeast_def)
    1.62 + apply (blast intro: linorder_not_less [THEN iffD1])
    1.63  apply (blast dest: order_le_less_trans)
    1.64  done
    1.65  
    1.66 -lemma single_Diff_lessThan: "!!k:: 'a::order. {k} - lessThan k = {k}"
    1.67 -apply auto
    1.68 -done
    1.69 -declare single_Diff_lessThan [simp]
    1.70 +lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
    1.71 +by auto
    1.72  
    1.73 -(*** greaterThan ***)
    1.74 +subsection {*greaterThan*}
    1.75  
    1.76 -lemma greaterThan_iff: "(i: greaterThan k) = (k<i)"
    1.77 +lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
    1.78 +by (simp add: greaterThan_def)
    1.79  
    1.80 -apply (unfold greaterThan_def)
    1.81 -apply blast
    1.82 -done
    1.83 -declare greaterThan_iff [iff]
    1.84 -
    1.85 -lemma greaterThan_0: "greaterThan 0 = range Suc"
    1.86 -apply (unfold greaterThan_def)
    1.87 +lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
    1.88 +apply (simp add: greaterThan_def)
    1.89  apply (blast dest: gr0_conv_Suc [THEN iffD1])
    1.90  done
    1.91 -declare greaterThan_0 [simp]
    1.92  
    1.93  lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
    1.94 -apply (unfold greaterThan_def)
    1.95 +apply (simp add: greaterThan_def)
    1.96  apply (auto elim: linorder_neqE)
    1.97  done
    1.98  
    1.99  lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
   1.100 -apply blast
   1.101 -done
   1.102 +by blast
   1.103  
   1.104 -lemma Compl_greaterThan: 
   1.105 +lemma Compl_greaterThan [simp]: 
   1.106      "!!k:: 'a::linorder. -greaterThan k = atMost k"
   1.107 -apply (unfold greaterThan_def atMost_def le_def)
   1.108 -apply auto
   1.109 +apply (simp add: greaterThan_def atMost_def le_def, auto)
   1.110  apply (blast intro: linorder_not_less [THEN iffD1])
   1.111  apply (blast dest: order_le_less_trans)
   1.112  done
   1.113  
   1.114 -lemma Compl_atMost: "!!k:: 'a::linorder. -atMost k = greaterThan k"
   1.115 -apply (simp (no_asm) add: Compl_greaterThan [symmetric])
   1.116 +lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
   1.117 +apply (subst Compl_greaterThan [symmetric])
   1.118 +apply (rule double_complement) 
   1.119  done
   1.120  
   1.121 -declare Compl_greaterThan [simp] Compl_atMost [simp]
   1.122  
   1.123 -(*** atLeast ***)
   1.124 -
   1.125 -lemma atLeast_iff: "(i: atLeast k) = (k<=i)"
   1.126 +subsection {*atLeast*}
   1.127  
   1.128 -apply (unfold atLeast_def)
   1.129 -apply blast
   1.130 -done
   1.131 -declare atLeast_iff [iff]
   1.132 +lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
   1.133 +by (simp add: atLeast_def)
   1.134  
   1.135 -lemma atLeast_0: "atLeast (0::nat) = UNIV"
   1.136 -apply (unfold atLeast_def UNIV_def)
   1.137 -apply (simp (no_asm))
   1.138 -done
   1.139 -declare atLeast_0 [simp]
   1.140 +lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
   1.141 +by (unfold atLeast_def UNIV_def, simp)
   1.142  
   1.143  lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
   1.144 -apply (unfold atLeast_def)
   1.145 -apply (simp (no_asm) add: Suc_le_eq)
   1.146 -apply (simp (no_asm) add: order_le_less)
   1.147 -apply blast
   1.148 +apply (simp add: atLeast_def)
   1.149 +apply (simp add: Suc_le_eq)
   1.150 +apply (simp add: order_le_less, blast)
   1.151  done
   1.152  
   1.153  lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
   1.154 -apply blast
   1.155 -done
   1.156 +by blast
   1.157  
   1.158 -lemma Compl_atLeast: 
   1.159 +lemma Compl_atLeast [simp]: 
   1.160      "!!k:: 'a::linorder. -atLeast k = lessThan k"
   1.161 -apply (unfold lessThan_def atLeast_def le_def)
   1.162 -apply auto
   1.163 +apply (simp add: lessThan_def atLeast_def le_def, auto)
   1.164  apply (blast intro: linorder_not_less [THEN iffD1])
   1.165  apply (blast dest: order_le_less_trans)
   1.166  done
   1.167  
   1.168 -declare Compl_lessThan [simp] Compl_atLeast [simp]
   1.169  
   1.170 -(*** atMost ***)
   1.171 -
   1.172 -lemma atMost_iff: "(i: atMost k) = (i<=k)"
   1.173 +subsection {*atMost*}
   1.174  
   1.175 -apply (unfold atMost_def)
   1.176 -apply blast
   1.177 -done
   1.178 -declare atMost_iff [iff]
   1.179 +lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)"
   1.180 +by (simp add: atMost_def)
   1.181  
   1.182 -lemma atMost_0: "atMost (0::nat) = {0}"
   1.183 -apply (unfold atMost_def)
   1.184 -apply (simp (no_asm))
   1.185 -done
   1.186 -declare atMost_0 [simp]
   1.187 +lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
   1.188 +by (simp add: atMost_def)
   1.189  
   1.190  lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
   1.191 -apply (unfold atMost_def)
   1.192 -apply (simp (no_asm) add: less_Suc_eq order_le_less)
   1.193 -apply blast
   1.194 +apply (simp add: atMost_def)
   1.195 +apply (simp add: less_Suc_eq order_le_less, blast)
   1.196  done
   1.197  
   1.198  lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
   1.199 -apply blast
   1.200 +by blast
   1.201 +
   1.202 +
   1.203 +subsection {*Logical Equivalences for Set Inclusion and Equality*}
   1.204 +
   1.205 +lemma atLeast_subset_iff [iff]:
   1.206 +     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
   1.207 +by (blast intro: order_trans) 
   1.208 +
   1.209 +lemma atLeast_eq_iff [iff]:
   1.210 +     "(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
   1.211 +by (blast intro: order_antisym order_trans)
   1.212 +
   1.213 +lemma greaterThan_subset_iff [iff]:
   1.214 +     "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 
   1.215 +apply (auto simp add: greaterThan_def) 
   1.216 + apply (subst linorder_not_less [symmetric], blast) 
   1.217 +apply (blast intro: order_le_less_trans) 
   1.218 +done
   1.219 +
   1.220 +lemma greaterThan_eq_iff [iff]:
   1.221 +     "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 
   1.222 +apply (rule iffI) 
   1.223 + apply (erule equalityE) 
   1.224 + apply (simp add: greaterThan_subset_iff order_antisym, simp) 
   1.225 +done
   1.226 +
   1.227 +lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" 
   1.228 +by (blast intro: order_trans)
   1.229 +
   1.230 +lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
   1.231 +by (blast intro: order_antisym order_trans)
   1.232 +
   1.233 +lemma lessThan_subset_iff [iff]:
   1.234 +     "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 
   1.235 +apply (auto simp add: lessThan_def) 
   1.236 + apply (subst linorder_not_less [symmetric], blast) 
   1.237 +apply (blast intro: order_less_le_trans) 
   1.238 +done
   1.239 +
   1.240 +lemma lessThan_eq_iff [iff]:
   1.241 +     "(lessThan x = lessThan y) = (x = (y::'a::linorder))" 
   1.242 +apply (rule iffI) 
   1.243 + apply (erule equalityE) 
   1.244 + apply (simp add: lessThan_subset_iff order_antisym, simp) 
   1.245  done
   1.246  
   1.247  
   1.248 -(*** Combined properties ***)
   1.249 +subsection {*Combined properties*}
   1.250  
   1.251  lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
   1.252 -apply (blast intro: order_antisym)
   1.253 -done
   1.254 +by (blast intro: order_antisym)
   1.255  
   1.256 -(*** Two-sided intervals ***)
   1.257 +subsection {*Two-sided intervals*}
   1.258  
   1.259  (* greaterThanLessThan *)
   1.260  
   1.261 @@ -252,7 +255,8 @@
   1.262     If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
   1.263     seems to take forever (more than one hour). *)
   1.264  
   1.265 -(*** The following lemmas are useful with the summation operator setsum ***)
   1.266 +subsection {*Lemmas useful with the summation operator setsum*}
   1.267 +
   1.268  (* For examples, see Algebra/poly/UnivPoly.thy *)
   1.269  
   1.270  (** Disjoint Unions **)