tuned list comprehension, added lemma
authornipkow
Sun Jun 03 16:57:51 2007 +0200 (2007-06-03)
changeset 2321282881b1ae9c6
parent 23211 4d56ad10b5e8
child 23213 43553703267c
tuned list comprehension, added lemma
src/HOL/List.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/List.thy	Sun Jun 03 15:44:35 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Sun Jun 03 16:57:51 2007 +0200
     1.3 @@ -256,9 +256,9 @@
     1.4  
     1.5  translations
     1.6  "[e. p\<leftarrow>xs]" => "map (%p. e) xs"
     1.7 -"_listcompr e p xs (_lc_gen q ys GT)" =>
     1.8 - "concat (map (%p. _listcompr e q ys GT) xs)"
     1.9 -"_listcompr e p xs (_lc_test P GT)" => "_listcompr e p (filter (%p. P) xs) GT"
    1.10 +"_listcompr e p xs (_lc_gen q ys Q)" =>
    1.11 + "concat (map (%p. _listcompr e q ys Q) xs)"
    1.12 +"_listcompr e p xs (_lc_test P Q)" => "_listcompr e p (filter (%p. P) xs) Q"
    1.13  
    1.14  (* Some examples:
    1.15  term "[(x,y). x \<leftarrow> xs, x<y]"
     2.1 --- a/src/HOL/Orderings.thy	Sun Jun 03 15:44:35 2007 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Sun Jun 03 16:57:51 2007 +0200
     2.3 @@ -99,94 +99,94 @@
     2.4  
     2.5  lemma eq_refl: "x = y \<Longrightarrow> x \<^loc>\<le> y"
     2.6      -- {* This form is useful with the classical reasoner. *}
     2.7 -  by (erule ssubst) (rule order_refl)
     2.8 +by (erule ssubst) (rule order_refl)
     2.9  
    2.10  lemma less_irrefl [iff]: "\<not> x \<^loc>< x"
    2.11 -  by (simp add: less_le)
    2.12 +by (simp add: less_le)
    2.13  
    2.14  lemma le_less: "x \<^loc>\<le> y \<longleftrightarrow> x \<^loc>< y \<or> x = y"
    2.15      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
    2.16 -  by (simp add: less_le) blast
    2.17 +by (simp add: less_le) blast
    2.18  
    2.19  lemma le_imp_less_or_eq: "x \<^loc>\<le> y \<Longrightarrow> x \<^loc>< y \<or> x = y"
    2.20 -  unfolding less_le by blast
    2.21 +unfolding less_le by blast
    2.22  
    2.23  lemma less_imp_le: "x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y"
    2.24 -  unfolding less_le by blast
    2.25 +unfolding less_le by blast
    2.26  
    2.27  lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
    2.28 -  by (erule contrapos_pn, erule subst, rule less_irrefl)
    2.29 +by (erule contrapos_pn, erule subst, rule less_irrefl)
    2.30  
    2.31  
    2.32  text {* Useful for simplification, but too risky to include by default. *}
    2.33  
    2.34  lemma less_imp_not_eq: "x \<^loc>< y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
    2.35 -  by auto
    2.36 +by auto
    2.37  
    2.38  lemma less_imp_not_eq2: "x \<^loc>< y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
    2.39 -  by auto
    2.40 +by auto
    2.41  
    2.42  
    2.43  text {* Transitivity rules for calculational reasoning *}
    2.44  
    2.45  lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<^loc>\<le> b \<Longrightarrow> a \<^loc>< b"
    2.46 -  by (simp add: less_le)
    2.47 +by (simp add: less_le)
    2.48  
    2.49  lemma le_neq_trans: "a \<^loc>\<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<^loc>< b"
    2.50 -  by (simp add: less_le)
    2.51 +by (simp add: less_le)
    2.52  
    2.53  
    2.54  text {* Asymmetry. *}
    2.55  
    2.56  lemma less_not_sym: "x \<^loc>< y \<Longrightarrow> \<not> (y \<^loc>< x)"
    2.57 -  by (simp add: less_le antisym)
    2.58 +by (simp add: less_le antisym)
    2.59  
    2.60  lemma less_asym: "x \<^loc>< y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<^loc>< x) \<Longrightarrow> P"
    2.61 -  by (drule less_not_sym, erule contrapos_np) simp
    2.62 +by (drule less_not_sym, erule contrapos_np) simp
    2.63  
    2.64  lemma eq_iff: "x = y \<longleftrightarrow> x \<^loc>\<le> y \<and> y \<^loc>\<le> x"
    2.65 -  by (blast intro: antisym)
    2.66 +by (blast intro: antisym)
    2.67  
    2.68  lemma antisym_conv: "y \<^loc>\<le> x \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
    2.69 -  by (blast intro: antisym)
    2.70 +by (blast intro: antisym)
    2.71  
    2.72  lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
    2.73 -  by (erule contrapos_pn, erule subst, rule less_irrefl)
    2.74 +by (erule contrapos_pn, erule subst, rule less_irrefl)
    2.75  
    2.76  
    2.77  text {* Transitivity. *}
    2.78  
    2.79  lemma less_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
    2.80 -  by (simp add: less_le) (blast intro: order_trans antisym)
    2.81 +by (simp add: less_le) (blast intro: order_trans antisym)
    2.82  
    2.83  lemma le_less_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
    2.84 -  by (simp add: less_le) (blast intro: order_trans antisym)
    2.85 +by (simp add: less_le) (blast intro: order_trans antisym)
    2.86  
    2.87  lemma less_le_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>< z"
    2.88 -  by (simp add: less_le) (blast intro: order_trans antisym)
    2.89 +by (simp add: less_le) (blast intro: order_trans antisym)
    2.90  
    2.91  
    2.92  text {* Useful for simplification, but too risky to include by default. *}
    2.93  
    2.94  lemma less_imp_not_less: "x \<^loc>< y \<Longrightarrow> (\<not> y \<^loc>< x) \<longleftrightarrow> True"
    2.95 -  by (blast elim: less_asym)
    2.96 +by (blast elim: less_asym)
    2.97  
    2.98  lemma less_imp_triv: "x \<^loc>< y \<Longrightarrow> (y \<^loc>< x \<longrightarrow> P) \<longleftrightarrow> True"
    2.99 -  by (blast elim: less_asym)
   2.100 +by (blast elim: less_asym)
   2.101  
   2.102  
   2.103  text {* Transitivity rules for calculational reasoning *}
   2.104  
   2.105  lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P"
   2.106 -  by (rule less_asym)
   2.107 +by (rule less_asym)
   2.108  
   2.109  
   2.110  text {* Reverse order *}
   2.111  
   2.112  lemma order_reverse:
   2.113    "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
   2.114 -  by unfold_locales
   2.115 -    (simp add: less_le, auto intro: antisym order_trans)
   2.116 +by unfold_locales
   2.117 +   (simp add: less_le, auto intro: antisym order_trans)
   2.118  
   2.119  end
   2.120  
   2.121 @@ -198,97 +198,103 @@
   2.122  begin
   2.123  
   2.124  lemma less_linear: "x \<^loc>< y \<or> x = y \<or> y \<^loc>< x"
   2.125 -  unfolding less_le using less_le linear by blast 
   2.126 +unfolding less_le using less_le linear by blast
   2.127  
   2.128  lemma le_less_linear: "x \<^loc>\<le> y \<or> y \<^loc>< x"
   2.129 -  by (simp add: le_less less_linear)
   2.130 +by (simp add: le_less less_linear)
   2.131  
   2.132  lemma le_cases [case_names le ge]:
   2.133    "(x \<^loc>\<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>\<le> x \<Longrightarrow> P) \<Longrightarrow> P"
   2.134 -  using linear by blast
   2.135 +using linear by blast
   2.136  
   2.137  lemma linorder_cases [case_names less equal greater]:
   2.138 -    "(x \<^loc>< y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> P) \<Longrightarrow> P"
   2.139 -  using less_linear by blast
   2.140 +  "(x \<^loc>< y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> P) \<Longrightarrow> P"
   2.141 +using less_linear by blast
   2.142  
   2.143  lemma not_less: "\<not> x \<^loc>< y \<longleftrightarrow> y \<^loc>\<le> x"
   2.144 -  apply (simp add: less_le)
   2.145 -  using linear apply (blast intro: antisym)
   2.146 -  done
   2.147 +apply (simp add: less_le)
   2.148 +using linear apply (blast intro: antisym)
   2.149 +done
   2.150 +
   2.151 +lemma not_less_iff_gr_or_eq:
   2.152 + "\<not>(x \<^loc>< y) \<longleftrightarrow> (x \<^loc>> y | x = y)"
   2.153 +apply(simp add:not_less le_less)
   2.154 +apply blast
   2.155 +done
   2.156  
   2.157  lemma not_le: "\<not> x \<^loc>\<le> y \<longleftrightarrow> y \<^loc>< x"
   2.158 -  apply (simp add: less_le)
   2.159 -  using linear apply (blast intro: antisym)
   2.160 -  done
   2.161 +apply (simp add: less_le)
   2.162 +using linear apply (blast intro: antisym)
   2.163 +done
   2.164  
   2.165  lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<^loc>< y \<or> y \<^loc>< x"
   2.166 -  by (cut_tac x = x and y = y in less_linear, auto)
   2.167 +by (cut_tac x = x and y = y in less_linear, auto)
   2.168  
   2.169  lemma neqE: "x \<noteq> y \<Longrightarrow> (x \<^loc>< y \<Longrightarrow> R) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> R) \<Longrightarrow> R"
   2.170 -  by (simp add: neq_iff) blast
   2.171 +by (simp add: neq_iff) blast
   2.172  
   2.173  lemma antisym_conv1: "\<not> x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
   2.174 -  by (blast intro: antisym dest: not_less [THEN iffD1])
   2.175 +by (blast intro: antisym dest: not_less [THEN iffD1])
   2.176  
   2.177  lemma antisym_conv2: "x \<^loc>\<le> y \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
   2.178 -  by (blast intro: antisym dest: not_less [THEN iffD1])
   2.179 +by (blast intro: antisym dest: not_less [THEN iffD1])
   2.180  
   2.181  lemma antisym_conv3: "\<not> y \<^loc>< x \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
   2.182 -  by (blast intro: antisym dest: not_less [THEN iffD1])
   2.183 +by (blast intro: antisym dest: not_less [THEN iffD1])
   2.184  
   2.185  text{*Replacing the old Nat.leI*}
   2.186  lemma leI: "\<not> x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x"
   2.187 -  unfolding not_less .
   2.188 +unfolding not_less .
   2.189  
   2.190  lemma leD: "y \<^loc>\<le> x \<Longrightarrow> \<not> x \<^loc>< y"
   2.191 -  unfolding not_less .
   2.192 +unfolding not_less .
   2.193  
   2.194  (*FIXME inappropriate name (or delete altogether)*)
   2.195  lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y"
   2.196 -  unfolding not_le .
   2.197 +unfolding not_le .
   2.198  
   2.199  
   2.200  text {* Reverse order *}
   2.201  
   2.202  lemma linorder_reverse:
   2.203    "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
   2.204 -  by unfold_locales
   2.205 -    (simp add: less_le, auto intro: antisym order_trans simp add: linear)
   2.206 +by unfold_locales
   2.207 +  (simp add: less_le, auto intro: antisym order_trans simp add: linear)
   2.208  
   2.209  
   2.210  text {* min/max properties *}
   2.211  
   2.212  lemma min_le_iff_disj:
   2.213    "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
   2.214 -  unfolding min_def using linear by (auto intro: order_trans)
   2.215 +unfolding min_def using linear by (auto intro: order_trans)
   2.216  
   2.217  lemma le_max_iff_disj:
   2.218    "z \<^loc>\<le> max x y \<longleftrightarrow> z \<^loc>\<le> x \<or> z \<^loc>\<le> y"
   2.219 -  unfolding max_def using linear by (auto intro: order_trans)
   2.220 +unfolding max_def using linear by (auto intro: order_trans)
   2.221  
   2.222  lemma min_less_iff_disj:
   2.223    "min x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<or> y \<^loc>< z"
   2.224 -  unfolding min_def le_less using less_linear by (auto intro: less_trans)
   2.225 +unfolding min_def le_less using less_linear by (auto intro: less_trans)
   2.226  
   2.227  lemma less_max_iff_disj:
   2.228    "z \<^loc>< max x y \<longleftrightarrow> z \<^loc>< x \<or> z \<^loc>< y"
   2.229 -  unfolding max_def le_less using less_linear by (auto intro: less_trans)
   2.230 +unfolding max_def le_less using less_linear by (auto intro: less_trans)
   2.231  
   2.232  lemma min_less_iff_conj [simp]:
   2.233    "z \<^loc>< min x y \<longleftrightarrow> z \<^loc>< x \<and> z \<^loc>< y"
   2.234 -  unfolding min_def le_less using less_linear by (auto intro: less_trans)
   2.235 +unfolding min_def le_less using less_linear by (auto intro: less_trans)
   2.236  
   2.237  lemma max_less_iff_conj [simp]:
   2.238    "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z"
   2.239 -  unfolding max_def le_less using less_linear by (auto intro: less_trans)
   2.240 +unfolding max_def le_less using less_linear by (auto intro: less_trans)
   2.241  
   2.242  lemma split_min:
   2.243    "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)"
   2.244 -  by (simp add: min_def)
   2.245 +by (simp add: min_def)
   2.246  
   2.247  lemma split_max:
   2.248    "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)"
   2.249 -  by (simp add: max_def)
   2.250 +by (simp add: max_def)
   2.251  
   2.252  end
   2.253  
   2.254 @@ -564,16 +570,16 @@
   2.255  subsection {* Transitivity reasoning *}
   2.256  
   2.257  lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
   2.258 -  by (rule subst)
   2.259 +by (rule subst)
   2.260  
   2.261  lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
   2.262 -  by (rule ssubst)
   2.263 +by (rule ssubst)
   2.264  
   2.265  lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
   2.266 -  by (rule subst)
   2.267 +by (rule subst)
   2.268  
   2.269  lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
   2.270 -  by (rule ssubst)
   2.271 +by (rule ssubst)
   2.272  
   2.273  lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
   2.274    (!!x y. x < y ==> f x < f y) ==> f a < c"
   2.275 @@ -812,16 +818,16 @@
   2.276    by intro_classes (auto simp add: le_bool_def less_bool_def)
   2.277  
   2.278  lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
   2.279 -  by (simp add: le_bool_def)
   2.280 +by (simp add: le_bool_def)
   2.281  
   2.282  lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
   2.283 -  by (simp add: le_bool_def)
   2.284 +by (simp add: le_bool_def)
   2.285  
   2.286  lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   2.287 -  by (simp add: le_bool_def)
   2.288 +by (simp add: le_bool_def)
   2.289  
   2.290  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
   2.291 -  by (simp add: le_bool_def)
   2.292 +by (simp add: le_bool_def)
   2.293  
   2.294  lemma [code func]:
   2.295    "False \<le> b \<longleftrightarrow> True"
   2.296 @@ -850,41 +856,41 @@
   2.297        !!y. P y ==> x <= y;
   2.298        !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
   2.299     ==> Q (Least P)"
   2.300 -  apply (unfold Least_def)
   2.301 -  apply (rule theI2)
   2.302 -    apply (blast intro: order_antisym)+
   2.303 -  done
   2.304 +apply (unfold Least_def)
   2.305 +apply (rule theI2)
   2.306 +  apply (blast intro: order_antisym)+
   2.307 +done
   2.308  
   2.309  lemma Least_equality:
   2.310 -    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   2.311 -  apply (simp add: Least_def)
   2.312 -  apply (rule the_equality)
   2.313 -  apply (auto intro!: order_antisym)
   2.314 -  done
   2.315 +  "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   2.316 +apply (simp add: Least_def)
   2.317 +apply (rule the_equality)
   2.318 +apply (auto intro!: order_antisym)
   2.319 +done
   2.320  
   2.321  lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
   2.322 -  by (simp add: min_def)
   2.323 +by (simp add: min_def)
   2.324  
   2.325  lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
   2.326 -  by (simp add: max_def)
   2.327 +by (simp add: max_def)
   2.328  
   2.329  lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
   2.330 -  apply (simp add: min_def)
   2.331 -  apply (blast intro: order_antisym)
   2.332 -  done
   2.333 +apply (simp add: min_def)
   2.334 +apply (blast intro: order_antisym)
   2.335 +done
   2.336  
   2.337  lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
   2.338 -  apply (simp add: max_def)
   2.339 -  apply (blast intro: order_antisym)
   2.340 -  done
   2.341 +apply (simp add: max_def)
   2.342 +apply (blast intro: order_antisym)
   2.343 +done
   2.344  
   2.345  lemma min_of_mono:
   2.346 -    "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
   2.347 -  by (simp add: min_def)
   2.348 +  "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
   2.349 +by (simp add: min_def)
   2.350  
   2.351  lemma max_of_mono:
   2.352 -    "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
   2.353 -  by (simp add: max_def)
   2.354 +  "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
   2.355 +by (simp add: max_def)
   2.356  
   2.357  
   2.358  subsection {* legacy ML bindings *}