--- a/NEWS Thu Dec 29 10:47:55 2011 +0100
+++ b/NEWS Thu Dec 29 10:47:55 2011 +0100
@@ -36,10 +36,17 @@
* Ancient code generator for SML and its commands 'code_module',
'code_library', 'consts_code', 'types_code' have been discontinued.
-Use commands of the generic code generator instead. INCOMPATIBILITY.
+Use commands of the generic code generator instead. INCOMPATIBILITY.
* Redundant attribute 'code_inline' has been discontinued. Use
-'code_unfold' instead. INCOMPATIBILITY.
+'code_unfold' instead. INCOMPATIBILITY.
+
+* Dropped attribute 'code_unfold_post' in favor of the its dual 'code_abbrev',
+which yields a common pattern in definitions like
+
+ definition [code_abbrev]: "f = t"
+
+INCOMPATIBILITY.
* Sort constraints are now propagated in simultaneous statements, just
like type constraints. INCOMPATIBILITY in rare situations, where
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Dec 29 10:47:55 2011 +0100
@@ -1783,7 +1783,7 @@
@{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{attribute_def (HOL) code_unfold} & : & @{text attribute} \\
@{attribute_def (HOL) code_post} & : & @{text attribute} \\
- @{attribute_def (HOL) code_unfold_post} & : & @{text attribute} \\
+ @{attribute_def (HOL) code_abbrev} & : & @{text attribute} \\
@{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -1835,7 +1835,7 @@
@@{attribute (HOL) code_post} ( 'del' ) ?
;
- @@{attribute (HOL) code_unfold_post}
+ @@{attribute (HOL) code_abbrev}
;
@@{command (HOL) code_thms} ( constexpr + ) ?
@@ -1940,17 +1940,19 @@
selected code equations and code generator datatypes.
\item @{attribute (HOL) code_unfold} declares (or with option
- ``@{text "del"}'' removes) theorems which are applied as
- rewrite rules to any code equation during preprocessing.
+ ``@{text "del"}'' removes) theorems which during preprocessing
+ are applied as rewrite rules to any code equation or evaluation
+ input.
\item @{attribute (HOL) code_post} declares (or with option ``@{text
"del"}'' removes) theorems which are applied as rewrite rules to any
result of an evaluation.
- \item @{attribute (HOL) code_unfold_post} declares equations which are
- applied as rewrite rules to any code equation during preprocessing,
- and symmetrically to any result of an evaluation.
-
+ \item @{attribute (HOL) code_abbrev} declares equations which are
+ applied as rewrite rules to any result of an evaluation and
+ symmetrically during preprocessing to any code equation or evaluation
+ input.
+
\item @{command (HOL) "print_codeproc"} prints the setup of the code
generator preprocessor.
--- a/src/HOL/Code_Numeral.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/Code_Numeral.thy Thu Dec 29 10:47:55 2011 +0100
@@ -176,16 +176,18 @@
end
-lemma zero_code_numeral_code [code, code_unfold]:
+lemma zero_code_numeral_code [code]:
"(0\<Colon>code_numeral) = Numeral0"
by (simp add: number_of_code_numeral_def Pls_def)
-lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
+
+lemma [code_abbrev]: "Numeral0 = (0\<Colon>code_numeral)"
using zero_code_numeral_code ..
-lemma one_code_numeral_code [code, code_unfold]:
+lemma one_code_numeral_code [code]:
"(1\<Colon>code_numeral) = Numeral1"
by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
-lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
+
+lemma [code_abbrev]: "Numeral1 = (1\<Colon>code_numeral)"
using one_code_numeral_code ..
lemma plus_code_numeral_code [code nbe]:
--- a/src/HOL/IMP/Abs_Int1_ivl.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy Thu Dec 29 10:47:55 2011 +0100
@@ -26,11 +26,7 @@
definition "num_ivl n = {n\<dots>n}"
definition
- "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
-
-lemma in_rep_ivl_contained_in [code_unfold_post]:
- "k \<in> rep_ivl i \<longleftrightarrow> contained_in i k"
- by (simp only: contained_in_def)
+ [code_abbrev]: "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
lemma contained_in_simps [code]:
"contained_in (I (Some l) (Some h)) k \<longleftrightarrow> l \<le> k \<and> k \<le> h"
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Thu Dec 29 10:47:55 2011 +0100
@@ -22,11 +22,7 @@
definition "num_ivl n = I (Some n) (Some n)"
definition
- "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
-
-lemma in_rep_ivl_contained_in [code_unfold_post]:
- "k \<in> rep_ivl i \<longleftrightarrow> contained_in i k"
- by (simp only: contained_in_def)
+ [code_abbrev]: "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
lemma contained_in_simps [code]:
"contained_in (I (Some l) (Some h)) k \<longleftrightarrow> l \<le> k \<and> k \<le> h"
--- a/src/HOL/Library/Efficient_Nat.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Dec 29 10:47:55 2011 +0100
@@ -26,11 +26,11 @@
code_datatype number_nat_inst.number_of_nat
-lemma zero_nat_code [code, code_unfold_post]:
+lemma zero_nat_code [code, code_unfold]:
"0 = (Numeral0 :: nat)"
by simp
-lemma one_nat_code [code, code_unfold_post]:
+lemma one_nat_code [code, code_unfold]:
"1 = (Numeral1 :: nat)"
by simp
@@ -286,8 +286,8 @@
Natural numerals.
*}
-lemma [code_unfold_post]:
- "nat (number_of i) = number_nat_inst.number_of_nat i"
+lemma [code_abbrev]:
+ "number_nat_inst.number_of_nat i = nat (number_of i)"
-- {* this interacts as desired with @{thm nat_number_of_def} *}
by (simp add: number_nat_inst.number_of_nat)
@@ -307,7 +307,7 @@
*}
definition int :: "nat \<Rightarrow> int" where
- [code del]: "int = of_nat"
+ [code del, code_abbrev]: "int = of_nat"
lemma int_code' [code]:
"int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
@@ -317,7 +317,7 @@
"nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
unfolding nat_number_of_def number_of_is_id neg_def by simp
-lemma of_nat_int [code_unfold_post]:
+lemma of_nat_int: (* FIXME delete candidate *)
"of_nat = int" by (simp add: int_def)
lemma of_nat_aux_int [code_unfold]:
--- a/src/HOL/Library/Float.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/Library/Float.thy Thu Dec 29 10:47:55 2011 +0100
@@ -45,10 +45,12 @@
instance ..
end
-lemma number_of_float_Float [code_unfold_post]:
+lemma number_of_float_Float:
"number_of k = Float (number_of k) 0"
by (simp add: number_of_float_def number_of_is_id)
+declare number_of_float_Float [symmetric, code_abbrev]
+
lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
unfolding real_of_float_def using of_float.simps .
--- a/src/HOL/More_Set.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/More_Set.thy Thu Dec 29 10:47:55 2011 +0100
@@ -22,7 +22,7 @@
show ?thesis by (simp only: rem assms minus_fold_remove)
qed
-lemma bounded_Collect_code [code_unfold_post]:
+lemma bounded_Collect_code: (* FIXME delete candidate *)
"{x \<in> A. P x} = Set.project P A"
by (simp add: project_def)
@@ -218,23 +218,15 @@
by (auto simp add: union_set_foldr)
definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
- [simp]: "Inf = Complete_Lattices.Inf"
+ [simp, code_abbrev]: "Inf = Complete_Lattices.Inf"
hide_const (open) Inf
-lemma [code_unfold_post]:
- "Inf = More_Set.Inf"
- by simp
-
definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
- [simp]: "Sup = Complete_Lattices.Sup"
+ [simp, code_abbrev]: "Sup = Complete_Lattices.Sup"
hide_const (open) Sup
-lemma [code_unfold_post]:
- "Sup = More_Set.Sup"
- by simp
-
lemma Inf_code [code]:
"More_Set.Inf (set xs) = foldr inf xs top"
"More_Set.Inf (coset []) = bot"
--- a/src/HOL/Nat.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/Nat.thy Thu Dec 29 10:47:55 2011 +0100
@@ -181,7 +181,7 @@
begin
definition
- One_nat_def [simp]: "1 = Suc 0"
+ One_nat_def [simp, code_post]: "1 = Suc 0"
primrec times_nat where
mult_0: "0 * n = (0\<Colon>nat)"
@@ -1226,9 +1226,7 @@
text {* for code generation *}
definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
- funpow_code_def [code_post]: "funpow = compow"
-
-lemmas [code_unfold] = funpow_code_def [symmetric]
+ funpow_code_def [code_abbrev]: "funpow = compow"
lemma [code]:
"funpow (Suc n) f = f o funpow n f"
--- a/src/HOL/Product_Type.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/Product_Type.thy Thu Dec 29 10:47:55 2011 +0100
@@ -894,14 +894,10 @@
hide_const (open) Times
definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
- "product A B = Sigma A (\<lambda>_. B)"
+ [code_abbrev]: "product A B = Sigma A (\<lambda>_. B)"
hide_const (open) product
-lemma [code_unfold_post]:
- "Sigma A (\<lambda>_. B) = Product_Type.product A B"
- by (simp add: product_def)
-
syntax
"_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
translations
--- a/src/HOL/RealDef.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/RealDef.thy Thu Dec 29 10:47:55 2011 +0100
@@ -1491,11 +1491,10 @@
subsection{*Numerals and Arithmetic*}
-lemma [code_unfold_post]:
- "number_of k = real_of_int (number_of k)"
+lemma [code_abbrev]:
+ "real_of_int (number_of k) = number_of k"
unfolding number_of_is_id number_of_real_def ..
-
text{*Collapse applications of @{term real} to @{term number_of}*}
lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
by (simp add: real_of_int_def)