src/HOL/List.thy
changeset 31998 2c7a24f74db9
parent 31930 3107b9af1fb3
child 32005 c369417be055
child 32069 6d28bbd33e2c
     1.1 --- a/src/HOL/List.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -2076,7 +2076,7 @@
     1.4  by(induct xs) simp_all
     1.5  
     1.6  text{* For efficient code generation: avoid intermediate list. *}
     1.7 -lemma foldl_map[code unfold]:
     1.8 +lemma foldl_map[code_unfold]:
     1.9    "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
    1.10  by(induct xs arbitrary:a) simp_all
    1.11  
    1.12 @@ -2198,7 +2198,7 @@
    1.13  
    1.14  text{* For efficient code generation ---
    1.15         @{const listsum} is not tail recursive but @{const foldl} is. *}
    1.16 -lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
    1.17 +lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
    1.18  by(simp add:listsum_foldr foldl_foldr1)
    1.19  
    1.20  lemma distinct_listsum_conv_Setsum:
    1.21 @@ -3746,32 +3746,32 @@
    1.22    show ?case by (induct xs) (auto simp add: Cons aux)
    1.23  qed
    1.24  
    1.25 -lemma mem_iff [code post]:
    1.26 +lemma mem_iff [code_post]:
    1.27    "x mem xs \<longleftrightarrow> x \<in> set xs"
    1.28  by (induct xs) auto
    1.29  
    1.30 -lemmas in_set_code [code unfold] = mem_iff [symmetric]
    1.31 +lemmas in_set_code [code_unfold] = mem_iff [symmetric]
    1.32  
    1.33  lemma empty_null:
    1.34    "xs = [] \<longleftrightarrow> null xs"
    1.35  by (cases xs) simp_all
    1.36  
    1.37 -lemma [code inline]:
    1.38 +lemma [code_inline]:
    1.39    "eq_class.eq xs [] \<longleftrightarrow> null xs"
    1.40  by (simp add: eq empty_null)
    1.41  
    1.42 -lemmas null_empty [code post] =
    1.43 +lemmas null_empty [code_post] =
    1.44    empty_null [symmetric]
    1.45  
    1.46  lemma list_inter_conv:
    1.47    "set (list_inter xs ys) = set xs \<inter> set ys"
    1.48  by (induct xs) auto
    1.49  
    1.50 -lemma list_all_iff [code post]:
    1.51 +lemma list_all_iff [code_post]:
    1.52    "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
    1.53  by (induct xs) auto
    1.54  
    1.55 -lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
    1.56 +lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
    1.57  
    1.58  lemma list_all_append [simp]:
    1.59    "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
    1.60 @@ -3785,11 +3785,11 @@
    1.61    "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
    1.62    unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
    1.63  
    1.64 -lemma list_ex_iff [code post]:
    1.65 +lemma list_ex_iff [code_post]:
    1.66    "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
    1.67  by (induct xs) simp_all
    1.68  
    1.69 -lemmas list_bex_code [code unfold] =
    1.70 +lemmas list_bex_code [code_unfold] =
    1.71    list_ex_iff [symmetric]
    1.72  
    1.73  lemma list_ex_length:
    1.74 @@ -3804,7 +3804,7 @@
    1.75    "map_filter f P xs = map f (filter P xs)"
    1.76  by (induct xs) auto
    1.77  
    1.78 -lemma length_remdups_length_unique [code inline]:
    1.79 +lemma length_remdups_length_unique [code_inline]:
    1.80    "length (remdups xs) = length_unique xs"
    1.81    by (induct xs) simp_all
    1.82  
    1.83 @@ -3813,43 +3813,43 @@
    1.84  
    1.85  text {* Code for bounded quantification and summation over nats. *}
    1.86  
    1.87 -lemma atMost_upto [code unfold]:
    1.88 +lemma atMost_upto [code_unfold]:
    1.89    "{..n} = set [0..<Suc n]"
    1.90  by auto
    1.91  
    1.92 -lemma atLeast_upt [code unfold]:
    1.93 +lemma atLeast_upt [code_unfold]:
    1.94    "{..<n} = set [0..<n]"
    1.95  by auto
    1.96  
    1.97 -lemma greaterThanLessThan_upt [code unfold]:
    1.98 +lemma greaterThanLessThan_upt [code_unfold]:
    1.99    "{n<..<m} = set [Suc n..<m]"
   1.100  by auto
   1.101  
   1.102 -lemma atLeastLessThan_upt [code unfold]:
   1.103 +lemma atLeastLessThan_upt [code_unfold]:
   1.104    "{n..<m} = set [n..<m]"
   1.105  by auto
   1.106  
   1.107 -lemma greaterThanAtMost_upt [code unfold]:
   1.108 +lemma greaterThanAtMost_upt [code_unfold]:
   1.109    "{n<..m} = set [Suc n..<Suc m]"
   1.110  by auto
   1.111  
   1.112 -lemma atLeastAtMost_upt [code unfold]:
   1.113 +lemma atLeastAtMost_upt [code_unfold]:
   1.114    "{n..m} = set [n..<Suc m]"
   1.115  by auto
   1.116  
   1.117 -lemma all_nat_less_eq [code unfold]:
   1.118 +lemma all_nat_less_eq [code_unfold]:
   1.119    "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
   1.120  by auto
   1.121  
   1.122 -lemma ex_nat_less_eq [code unfold]:
   1.123 +lemma ex_nat_less_eq [code_unfold]:
   1.124    "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
   1.125  by auto
   1.126  
   1.127 -lemma all_nat_less [code unfold]:
   1.128 +lemma all_nat_less [code_unfold]:
   1.129    "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
   1.130  by auto
   1.131  
   1.132 -lemma ex_nat_less [code unfold]:
   1.133 +lemma ex_nat_less [code_unfold]:
   1.134    "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
   1.135  by auto
   1.136  
   1.137 @@ -3857,30 +3857,30 @@
   1.138    "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
   1.139  by (induct xs) simp_all
   1.140  
   1.141 -lemma setsum_set_upt_conv_listsum [code unfold]:
   1.142 +lemma setsum_set_upt_conv_listsum [code_unfold]:
   1.143    "setsum f (set [m..<n]) = listsum (map f [m..<n])"
   1.144  by (rule setsum_set_distinct_conv_listsum) simp
   1.145  
   1.146  
   1.147  text {* Code for summation over ints. *}
   1.148  
   1.149 -lemma greaterThanLessThan_upto [code unfold]:
   1.150 +lemma greaterThanLessThan_upto [code_unfold]:
   1.151    "{i<..<j::int} = set [i+1..j - 1]"
   1.152  by auto
   1.153  
   1.154 -lemma atLeastLessThan_upto [code unfold]:
   1.155 +lemma atLeastLessThan_upto [code_unfold]:
   1.156    "{i..<j::int} = set [i..j - 1]"
   1.157  by auto
   1.158  
   1.159 -lemma greaterThanAtMost_upto [code unfold]:
   1.160 +lemma greaterThanAtMost_upto [code_unfold]:
   1.161    "{i<..j::int} = set [i+1..j]"
   1.162  by auto
   1.163  
   1.164 -lemma atLeastAtMost_upto [code unfold]:
   1.165 +lemma atLeastAtMost_upto [code_unfold]:
   1.166    "{i..j::int} = set [i..j]"
   1.167  by auto
   1.168  
   1.169 -lemma setsum_set_upto_conv_listsum [code unfold]:
   1.170 +lemma setsum_set_upto_conv_listsum [code_unfold]:
   1.171    "setsum f (set [i..j::int]) = listsum (map f [i..j])"
   1.172  by (rule setsum_set_distinct_conv_listsum) simp
   1.173