attribute code_abbrev superseedes code_unfold_post; tuned text
authorhaftmann
Thu Dec 29 10:47:55 2011 +0100 (2011-12-29)
changeset 4603051b2f3412a03
parent 46029 4a19e3d147c3
child 46031 ac6bae9fdc2f
attribute code_abbrev superseedes code_unfold_post; tuned text
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Thu Dec 29 10:47:55 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Dec 29 10:47:55 2011 +0100
     1.3 @@ -5017,10 +5017,10 @@
     1.4  subsubsection {* Counterparts for set-related operations *}
     1.5  
     1.6  definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
     1.7 -  [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
     1.8 +  [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
     1.9  
    1.10  text {*
    1.11 -  Only use @{text member} for generating executable code.  Otherwise use
    1.12 +  Use @{text member} only for generating executable code.  Otherwise use
    1.13    @{prop "x \<in> set xs"} instead --- it is much easier to reason about.
    1.14  *}
    1.15  
    1.16 @@ -5029,7 +5029,7 @@
    1.17    "member [] y \<longleftrightarrow> False"
    1.18    by (auto simp add: member_def)
    1.19  
    1.20 -lemma in_set_member [code_unfold]:
    1.21 +lemma in_set_member (* FIXME delete candidate *):
    1.22    "x \<in> set xs \<longleftrightarrow> member xs x"
    1.23    by (simp add: member_def)
    1.24  
    1.25 @@ -5039,18 +5039,18 @@
    1.26  declare set_map [symmetric, code_unfold]
    1.27  
    1.28  definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.29 -  list_all_iff [code_post]: "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
    1.30 +  list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
    1.31  
    1.32  definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.33 -  list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
    1.34 -
    1.35 -definition list_ex1
    1.36 -where
    1.37 -  list_ex1_iff: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
    1.38 +  list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
    1.39 +
    1.40 +definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.41 +  list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
    1.42  
    1.43  text {*
    1.44 -  Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
    1.45 -  over @{const list_all} and @{const list_ex} in specifications.
    1.46 +  Usually you should prefer @{text "\<forall>x\<in>set xs"}, @{text "\<exists>x\<in>set xs"}
    1.47 +  and @{text "\<exists>!x. x\<in>set xs \<and> _"} over @{const list_all}, @{const list_ex}
    1.48 +  and @{const list_ex1} in specifications.
    1.49  *}
    1.50  
    1.51  lemma list_all_simps [simp, code]:
    1.52 @@ -5066,13 +5066,13 @@
    1.53  lemma list_ex1_simps [simp, code]:
    1.54    "list_ex1 P [] = False"
    1.55    "list_ex1 P (x # xs) = (if P x then list_all (\<lambda>y. \<not> P y \<or> x = y) xs else list_ex1 P xs)"
    1.56 -unfolding list_ex1_iff list_all_iff by auto
    1.57 -
    1.58 -lemma Ball_set_list_all [code_unfold]:
    1.59 +  by (auto simp add: list_ex1_iff list_all_iff)
    1.60 +
    1.61 +lemma Ball_set_list_all: (* FIXME delete candidate *)
    1.62    "Ball (set xs) P \<longleftrightarrow> list_all P xs"
    1.63    by (simp add: list_all_iff)
    1.64  
    1.65 -lemma Bex_set_list_ex [code_unfold]:
    1.66 +lemma Bex_set_list_ex: (* FIXME delete candidate *)
    1.67    "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
    1.68    by (simp add: list_ex_iff)
    1.69  
    1.70 @@ -5176,7 +5176,7 @@
    1.71  subsubsection {* Optimizing by rewriting *}
    1.72  
    1.73  definition null :: "'a list \<Rightarrow> bool" where
    1.74 -  [code_post]: "null xs \<longleftrightarrow> xs = []"
    1.75 +  [code_abbrev]: "null xs \<longleftrightarrow> xs = []"
    1.76  
    1.77  text {*
    1.78    Efficient emptyness check is implemented by @{const null}.
    1.79 @@ -5187,7 +5187,7 @@
    1.80    "null [] \<longleftrightarrow> True"
    1.81    by (simp_all add: null_def)
    1.82  
    1.83 -lemma eq_Nil_null [code_unfold]:
    1.84 +lemma eq_Nil_null: (* FIXME delete candidate *)
    1.85    "xs = [] \<longleftrightarrow> null xs"
    1.86    by (simp add: null_def)
    1.87  
    1.88 @@ -5196,7 +5196,7 @@
    1.89    by (simp add: equal eq_Nil_null)
    1.90  
    1.91  definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    1.92 -  [code_post]: "maps f xs = concat (map f xs)"
    1.93 +  [code_abbrev]: "maps f xs = concat (map f xs)"
    1.94  
    1.95  definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    1.96    [code_post]: "map_filter f xs = map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) xs)"
    1.97 @@ -5216,7 +5216,7 @@
    1.98    "map_filter f [] = []"
    1.99    by (simp_all add: map_filter_def split: option.split)
   1.100  
   1.101 -lemma concat_map_maps [code_unfold]:
   1.102 +lemma concat_map_maps: (* FIXME delete candidate *)
   1.103    "concat (map f xs) = maps f xs"
   1.104    by (simp add: maps_def)
   1.105