attribute code_abbrev superseedes code_unfold_post
authorhaftmann
Thu Dec 29 10:47:55 2011 +0100 (2011-12-29)
changeset 460289f113cdf3d66
parent 46027 ff3c4f2bee01
child 46029 4a19e3d147c3
attribute code_abbrev superseedes code_unfold_post
NEWS
doc-src/IsarRef/Thy/HOL_Specific.thy
src/HOL/Code_Numeral.thy
src/HOL/IMP/Abs_Int1_ivl.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Float.thy
src/HOL/More_Set.thy
src/HOL/Nat.thy
src/HOL/Product_Type.thy
src/HOL/RealDef.thy
     1.1 --- a/NEWS	Thu Dec 29 10:47:55 2011 +0100
     1.2 +++ b/NEWS	Thu Dec 29 10:47:55 2011 +0100
     1.3 @@ -36,10 +36,17 @@
     1.4  
     1.5  * Ancient code generator for SML and its commands 'code_module',
     1.6  'code_library', 'consts_code', 'types_code' have been discontinued.
     1.7 -Use commands of the generic code generator instead. INCOMPATIBILITY.
     1.8 +Use commands of the generic code generator instead.  INCOMPATIBILITY.
     1.9  
    1.10  * Redundant attribute 'code_inline' has been discontinued. Use
    1.11 -'code_unfold' instead. INCOMPATIBILITY.
    1.12 +'code_unfold' instead.  INCOMPATIBILITY.
    1.13 +
    1.14 +* Dropped attribute 'code_unfold_post' in favor of the its dual 'code_abbrev',
    1.15 +which yields a common pattern in definitions like
    1.16 +
    1.17 +  definition [code_abbrev]: "f = t"
    1.18 +
    1.19 +INCOMPATIBILITY.
    1.20  
    1.21  * Sort constraints are now propagated in simultaneous statements, just
    1.22  like type constraints.  INCOMPATIBILITY in rare situations, where
     2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Dec 29 10:47:55 2011 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Dec 29 10:47:55 2011 +0100
     2.3 @@ -1783,7 +1783,7 @@
     2.4      @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     2.5      @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\
     2.6      @{attribute_def (HOL) code_post} & : & @{text attribute} \\
     2.7 -    @{attribute_def (HOL) code_unfold_post} & : & @{text attribute} \\
     2.8 +    @{attribute_def (HOL) code_abbrev} & : & @{text attribute} \\
     2.9      @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.10      @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.11      @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.12 @@ -1835,7 +1835,7 @@
    2.13      @@{attribute (HOL) code_post} ( 'del' ) ?
    2.14      ;
    2.15  
    2.16 -    @@{attribute (HOL) code_unfold_post}
    2.17 +    @@{attribute (HOL) code_abbrev}
    2.18      ;
    2.19  
    2.20      @@{command (HOL) code_thms} ( constexpr + ) ?
    2.21 @@ -1940,17 +1940,19 @@
    2.22    selected code equations and code generator datatypes.
    2.23  
    2.24    \item @{attribute (HOL) code_unfold} declares (or with option
    2.25 -  ``@{text "del"}'' removes) theorems which are applied as
    2.26 -  rewrite rules to any code equation during preprocessing.
    2.27 +  ``@{text "del"}'' removes) theorems which during preprocessing
    2.28 +  are applied as rewrite rules to any code equation or evaluation
    2.29 +  input.
    2.30  
    2.31    \item @{attribute (HOL) code_post} declares (or with option ``@{text
    2.32    "del"}'' removes) theorems which are applied as rewrite rules to any
    2.33    result of an evaluation.
    2.34  
    2.35 -  \item @{attribute (HOL) code_unfold_post} declares equations which are
    2.36 -  applied as rewrite rules to any code equation during preprocessing,
    2.37 -  and symmetrically to any result of an evaluation.
    2.38 -  
    2.39 +  \item @{attribute (HOL) code_abbrev} declares equations which are
    2.40 +  applied as rewrite rules to any result of an evaluation and
    2.41 +  symmetrically during preprocessing to any code equation or evaluation
    2.42 +  input.
    2.43 +
    2.44    \item @{command (HOL) "print_codeproc"} prints the setup of the code
    2.45    generator preprocessor.
    2.46  
     3.1 --- a/src/HOL/Code_Numeral.thy	Thu Dec 29 10:47:55 2011 +0100
     3.2 +++ b/src/HOL/Code_Numeral.thy	Thu Dec 29 10:47:55 2011 +0100
     3.3 @@ -176,16 +176,18 @@
     3.4  
     3.5  end
     3.6  
     3.7 -lemma zero_code_numeral_code [code, code_unfold]:
     3.8 +lemma zero_code_numeral_code [code]:
     3.9    "(0\<Colon>code_numeral) = Numeral0"
    3.10    by (simp add: number_of_code_numeral_def Pls_def)
    3.11 -lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
    3.12 +
    3.13 +lemma [code_abbrev]: "Numeral0 = (0\<Colon>code_numeral)"
    3.14    using zero_code_numeral_code ..
    3.15  
    3.16 -lemma one_code_numeral_code [code, code_unfold]:
    3.17 +lemma one_code_numeral_code [code]:
    3.18    "(1\<Colon>code_numeral) = Numeral1"
    3.19    by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
    3.20 -lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
    3.21 +
    3.22 +lemma [code_abbrev]: "Numeral1 = (1\<Colon>code_numeral)"
    3.23    using one_code_numeral_code ..
    3.24  
    3.25  lemma plus_code_numeral_code [code nbe]:
     4.1 --- a/src/HOL/IMP/Abs_Int1_ivl.thy	Thu Dec 29 10:47:55 2011 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Thu Dec 29 10:47:55 2011 +0100
     4.3 @@ -26,11 +26,7 @@
     4.4  definition "num_ivl n = {n\<dots>n}"
     4.5  
     4.6  definition
     4.7 -  "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
     4.8 -
     4.9 -lemma in_rep_ivl_contained_in [code_unfold_post]:
    4.10 -  "k \<in> rep_ivl i \<longleftrightarrow> contained_in i k"
    4.11 -  by (simp only: contained_in_def)
    4.12 +  [code_abbrev]: "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
    4.13  
    4.14  lemma contained_in_simps [code]:
    4.15    "contained_in (I (Some l) (Some h)) k \<longleftrightarrow> l \<le> k \<and> k \<le> h"
     5.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Thu Dec 29 10:47:55 2011 +0100
     5.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Thu Dec 29 10:47:55 2011 +0100
     5.3 @@ -22,11 +22,7 @@
     5.4  definition "num_ivl n = I (Some n) (Some n)"
     5.5  
     5.6  definition
     5.7 -  "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
     5.8 -
     5.9 -lemma in_rep_ivl_contained_in [code_unfold_post]:
    5.10 -  "k \<in> rep_ivl i \<longleftrightarrow> contained_in i k"
    5.11 -  by (simp only: contained_in_def)
    5.12 +  [code_abbrev]: "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
    5.13  
    5.14  lemma contained_in_simps [code]:
    5.15    "contained_in (I (Some l) (Some h)) k \<longleftrightarrow> l \<le> k \<and> k \<le> h"
     6.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Dec 29 10:47:55 2011 +0100
     6.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Dec 29 10:47:55 2011 +0100
     6.3 @@ -26,11 +26,11 @@
     6.4  
     6.5  code_datatype number_nat_inst.number_of_nat
     6.6  
     6.7 -lemma zero_nat_code [code, code_unfold_post]:
     6.8 +lemma zero_nat_code [code, code_unfold]:
     6.9    "0 = (Numeral0 :: nat)"
    6.10    by simp
    6.11  
    6.12 -lemma one_nat_code [code, code_unfold_post]:
    6.13 +lemma one_nat_code [code, code_unfold]:
    6.14    "1 = (Numeral1 :: nat)"
    6.15    by simp
    6.16  
    6.17 @@ -286,8 +286,8 @@
    6.18    Natural numerals.
    6.19  *}
    6.20  
    6.21 -lemma [code_unfold_post]:
    6.22 -  "nat (number_of i) = number_nat_inst.number_of_nat i"
    6.23 +lemma [code_abbrev]:
    6.24 +  "number_nat_inst.number_of_nat i = nat (number_of i)"
    6.25    -- {* this interacts as desired with @{thm nat_number_of_def} *}
    6.26    by (simp add: number_nat_inst.number_of_nat)
    6.27  
    6.28 @@ -307,7 +307,7 @@
    6.29  *}
    6.30  
    6.31  definition int :: "nat \<Rightarrow> int" where
    6.32 -  [code del]: "int = of_nat"
    6.33 +  [code del, code_abbrev]: "int = of_nat"
    6.34  
    6.35  lemma int_code' [code]:
    6.36    "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
    6.37 @@ -317,7 +317,7 @@
    6.38    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
    6.39    unfolding nat_number_of_def number_of_is_id neg_def by simp
    6.40  
    6.41 -lemma of_nat_int [code_unfold_post]:
    6.42 +lemma of_nat_int: (* FIXME delete candidate *)
    6.43    "of_nat = int" by (simp add: int_def)
    6.44  
    6.45  lemma of_nat_aux_int [code_unfold]:
     7.1 --- a/src/HOL/Library/Float.thy	Thu Dec 29 10:47:55 2011 +0100
     7.2 +++ b/src/HOL/Library/Float.thy	Thu Dec 29 10:47:55 2011 +0100
     7.3 @@ -45,10 +45,12 @@
     7.4  instance ..
     7.5  end
     7.6  
     7.7 -lemma number_of_float_Float [code_unfold_post]:
     7.8 +lemma number_of_float_Float:
     7.9    "number_of k = Float (number_of k) 0"
    7.10    by (simp add: number_of_float_def number_of_is_id)
    7.11  
    7.12 +declare number_of_float_Float [symmetric, code_abbrev]
    7.13 +
    7.14  lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
    7.15    unfolding real_of_float_def using of_float.simps .
    7.16  
     8.1 --- a/src/HOL/More_Set.thy	Thu Dec 29 10:47:55 2011 +0100
     8.2 +++ b/src/HOL/More_Set.thy	Thu Dec 29 10:47:55 2011 +0100
     8.3 @@ -22,7 +22,7 @@
     8.4    show ?thesis by (simp only: rem assms minus_fold_remove)
     8.5  qed
     8.6  
     8.7 -lemma bounded_Collect_code [code_unfold_post]:
     8.8 +lemma bounded_Collect_code: (* FIXME delete candidate *)
     8.9    "{x \<in> A. P x} = Set.project P A"
    8.10    by (simp add: project_def)
    8.11  
    8.12 @@ -218,23 +218,15 @@
    8.13    by (auto simp add: union_set_foldr)
    8.14  
    8.15  definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
    8.16 -  [simp]: "Inf = Complete_Lattices.Inf"
    8.17 +  [simp, code_abbrev]: "Inf = Complete_Lattices.Inf"
    8.18  
    8.19  hide_const (open) Inf
    8.20  
    8.21 -lemma [code_unfold_post]:
    8.22 -  "Inf = More_Set.Inf"
    8.23 -  by simp
    8.24 -
    8.25  definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
    8.26 -  [simp]: "Sup = Complete_Lattices.Sup"
    8.27 +  [simp, code_abbrev]: "Sup = Complete_Lattices.Sup"
    8.28  
    8.29  hide_const (open) Sup
    8.30  
    8.31 -lemma [code_unfold_post]:
    8.32 -  "Sup = More_Set.Sup"
    8.33 -  by simp
    8.34 -
    8.35  lemma Inf_code [code]:
    8.36    "More_Set.Inf (set xs) = foldr inf xs top"
    8.37    "More_Set.Inf (coset []) = bot"
     9.1 --- a/src/HOL/Nat.thy	Thu Dec 29 10:47:55 2011 +0100
     9.2 +++ b/src/HOL/Nat.thy	Thu Dec 29 10:47:55 2011 +0100
     9.3 @@ -181,7 +181,7 @@
     9.4  begin
     9.5  
     9.6  definition
     9.7 -  One_nat_def [simp]: "1 = Suc 0"
     9.8 +  One_nat_def [simp, code_post]: "1 = Suc 0"
     9.9  
    9.10  primrec times_nat where
    9.11    mult_0:     "0 * n = (0\<Colon>nat)"
    9.12 @@ -1226,9 +1226,7 @@
    9.13  text {* for code generation *}
    9.14  
    9.15  definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    9.16 -  funpow_code_def [code_post]: "funpow = compow"
    9.17 -
    9.18 -lemmas [code_unfold] = funpow_code_def [symmetric]
    9.19 +  funpow_code_def [code_abbrev]: "funpow = compow"
    9.20  
    9.21  lemma [code]:
    9.22    "funpow (Suc n) f = f o funpow n f"
    10.1 --- a/src/HOL/Product_Type.thy	Thu Dec 29 10:47:55 2011 +0100
    10.2 +++ b/src/HOL/Product_Type.thy	Thu Dec 29 10:47:55 2011 +0100
    10.3 @@ -894,14 +894,10 @@
    10.4  hide_const (open) Times
    10.5  
    10.6  definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    10.7 -  "product A B = Sigma A (\<lambda>_. B)"
    10.8 +  [code_abbrev]: "product A B = Sigma A (\<lambda>_. B)"
    10.9  
   10.10  hide_const (open) product
   10.11  
   10.12 -lemma [code_unfold_post]:
   10.13 -  "Sigma A (\<lambda>_. B) = Product_Type.product A B"
   10.14 -  by (simp add: product_def)
   10.15 -
   10.16  syntax
   10.17    "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
   10.18  translations
    11.1 --- a/src/HOL/RealDef.thy	Thu Dec 29 10:47:55 2011 +0100
    11.2 +++ b/src/HOL/RealDef.thy	Thu Dec 29 10:47:55 2011 +0100
    11.3 @@ -1491,11 +1491,10 @@
    11.4  
    11.5  subsection{*Numerals and Arithmetic*}
    11.6  
    11.7 -lemma [code_unfold_post]:
    11.8 -  "number_of k = real_of_int (number_of k)"
    11.9 +lemma [code_abbrev]:
   11.10 +  "real_of_int (number_of k) = number_of k"
   11.11    unfolding number_of_is_id number_of_real_def ..
   11.12  
   11.13 -
   11.14  text{*Collapse applications of @{term real} to @{term number_of}*}
   11.15  lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
   11.16  by (simp add: real_of_int_def)