# HG changeset patch # User haftmann # Date 1325152075 -3600 # Node ID 9f113cdf3d667aa92e6ffe08f3dbd5043fffe4cb # Parent ff3c4f2bee01c0102e2458a1b7388ae9a1cdf9dc attribute code_abbrev superseedes code_unfold_post diff -r ff3c4f2bee01 -r 9f113cdf3d66 NEWS --- 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 diff -r ff3c4f2bee01 -r 9f113cdf3d66 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \"} \\ @{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 \"} \\ @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @@ -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. diff -r ff3c4f2bee01 -r 9f113cdf3d66 src/HOL/Code_Numeral.thy --- 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\code_numeral) = Numeral0" by (simp add: number_of_code_numeral_def Pls_def) -lemma [code_post]: "Numeral0 = (0\code_numeral)" + +lemma [code_abbrev]: "Numeral0 = (0\code_numeral)" using zero_code_numeral_code .. -lemma one_code_numeral_code [code, code_unfold]: +lemma one_code_numeral_code [code]: "(1\code_numeral) = Numeral1" by (simp add: number_of_code_numeral_def Pls_def Bit1_def) -lemma [code_post]: "Numeral1 = (1\code_numeral)" + +lemma [code_abbrev]: "Numeral1 = (1\code_numeral)" using one_code_numeral_code .. lemma plus_code_numeral_code [code nbe]: diff -r ff3c4f2bee01 -r 9f113cdf3d66 src/HOL/IMP/Abs_Int1_ivl.thy --- 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\n}" definition - "contained_in i k \ k \ rep_ivl i" - -lemma in_rep_ivl_contained_in [code_unfold_post]: - "k \ rep_ivl i \ contained_in i k" - by (simp only: contained_in_def) + [code_abbrev]: "contained_in i k \ k \ rep_ivl i" lemma contained_in_simps [code]: "contained_in (I (Some l) (Some h)) k \ l \ k \ k \ h" diff -r ff3c4f2bee01 -r 9f113cdf3d66 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy --- 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 \ k \ rep_ivl i" - -lemma in_rep_ivl_contained_in [code_unfold_post]: - "k \ rep_ivl i \ contained_in i k" - by (simp only: contained_in_def) + [code_abbrev]: "contained_in i k \ k \ rep_ivl i" lemma contained_in_simps [code]: "contained_in (I (Some l) (Some h)) k \ l \ k \ k \ h" diff -r ff3c4f2bee01 -r 9f113cdf3d66 src/HOL/Library/Efficient_Nat.thy --- 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 \ 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 \ int) then 0 else number_of l)" @@ -317,7 +317,7 @@ "nat (number_of l) = (if neg (number_of l \ 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]: diff -r ff3c4f2bee01 -r 9f113cdf3d66 src/HOL/Library/Float.thy --- 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 . diff -r ff3c4f2bee01 -r 9f113cdf3d66 src/HOL/More_Set.thy --- 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 \ 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 \ '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 \ '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" diff -r ff3c4f2bee01 -r 9f113cdf3d66 src/HOL/Nat.thy --- 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\nat)" @@ -1226,9 +1226,7 @@ text {* for code generation *} definition funpow :: "nat \ ('a \ 'a) \ 'a \ '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" diff -r ff3c4f2bee01 -r 9f113cdf3d66 src/HOL/Product_Type.thy --- 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 \ 'b set \ ('a \ 'b) set" where - "product A B = Sigma A (\_. B)" + [code_abbrev]: "product A B = Sigma A (\_. B)" hide_const (open) product -lemma [code_unfold_post]: - "Sigma A (\_. 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 diff -r ff3c4f2bee01 -r 9f113cdf3d66 src/HOL/RealDef.thy --- 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)