--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jul 14 10:54:04 2009 +0200
@@ -1190,7 +1190,13 @@
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
;
- 'code' ( 'inline' ) ? ( 'del' ) ?
+ 'code' ( 'del' ) ?
+ ;
+
+ 'code_unfold' ( 'del' ) ?
+ ;
+
+ 'code_post' ( 'del' ) ?
;
\end{rail}
@@ -1280,11 +1286,15 @@
generation. Usually packages introducing code equations provide
a reasonable default setup for selection.
- \item @{attribute (HOL) code}~@{text inline} declares (or with
+ \item @{attribute (HOL) code_inline} declares (or with
option ``@{text "del"}'' removes) inlining theorems which are
applied as rewrite rules to any code equation during
preprocessing.
+ \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 @{command (HOL) "print_codesetup"} gives an overview on
selected code equations and code generator datatypes.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jul 14 10:53:44 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jul 14 10:54:04 2009 +0200
@@ -1201,7 +1201,13 @@
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
;
- 'code' ( 'inline' ) ? ( 'del' ) ?
+ 'code' ( 'del' ) ?
+ ;
+
+ 'code_unfold' ( 'del' ) ?
+ ;
+
+ 'code_post' ( 'del' ) ?
;
\end{rail}
@@ -1288,11 +1294,15 @@
generation. Usually packages introducing code equations provide
a reasonable default setup for selection.
- \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
+ \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
applied as rewrite rules to any code equation during
preprocessing.
+ \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
+ option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
+ applied as rewrite rules to any result of an evaluation.
+
\item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
selected code equations and code generator datatypes.
--- a/src/HOL/Code_Eval.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Code_Eval.thy Tue Jul 14 10:54:04 2009 +0200
@@ -32,7 +32,7 @@
\<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
"valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
-lemma valapp_code [code, code inline]:
+lemma valapp_code [code, code_inline]:
"valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
by (simp only: valapp_def fst_conv snd_conv)
--- a/src/HOL/Code_Numeral.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Code_Numeral.thy Tue Jul 14 10:54:04 2009 +0200
@@ -176,16 +176,16 @@
end
-lemma zero_code_numeral_code [code inline, code]:
+lemma zero_code_numeral_code [code_inline, 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_post]: "Numeral0 = (0\<Colon>code_numeral)"
using zero_code_numeral_code ..
-lemma one_code_numeral_code [code inline, code]:
+lemma one_code_numeral_code [code_inline, 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_post]: "Numeral1 = (1\<Colon>code_numeral)"
using one_code_numeral_code ..
lemma plus_code_numeral_code [code nbe]:
--- a/src/HOL/Divides.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Divides.thy Tue Jul 14 10:54:04 2009 +0200
@@ -131,7 +131,7 @@
note that ultimately show thesis by blast
qed
-lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
proof
assume "b mod a = 0"
with mod_div_equality [of b a] have "b div a * a = b" by simp
--- a/src/HOL/HOL.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/HOL.thy Tue Jul 14 10:54:04 2009 +0200
@@ -1787,7 +1787,7 @@
assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
begin
-lemma eq [code unfold, code inline del]: "eq = (op =)"
+lemma eq [code_unfold, code_inline del]: "eq = (op =)"
by (rule ext eq_equals)+
lemma eq_refl: "eq x x \<longleftrightarrow> True"
@@ -1796,7 +1796,7 @@
lemma equals_eq: "(op =) \<equiv> eq"
by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
-declare equals_eq [symmetric, code post]
+declare equals_eq [symmetric, code_post]
end
@@ -1847,7 +1847,7 @@
lemmas [code] = Let_def if_True if_False
-lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
+lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
instantiation itself :: (type) eq
begin
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 14 10:54:04 2009 +0200
@@ -283,7 +283,7 @@
where
[code del]: "raise_exc e = raise []"
-lemma raise_raise_exc [code, code inline]:
+lemma raise_raise_exc [code, code_inline]:
"raise s = raise_exc (Fail (STR s))"
unfolding Fail_def raise_exc_def raise_def ..
--- a/src/HOL/Int.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Int.thy Tue Jul 14 10:54:04 2009 +0200
@@ -650,11 +650,11 @@
text {* Removal of leading zeroes *}
-lemma Bit0_Pls [simp, code post]:
+lemma Bit0_Pls [simp, code_post]:
"Bit0 Pls = Pls"
unfolding numeral_simps by simp
-lemma Bit1_Min [simp, code post]:
+lemma Bit1_Min [simp, code_post]:
"Bit1 Min = Min"
unfolding numeral_simps by simp
@@ -2126,11 +2126,11 @@
hide (open) const nat_aux
-lemma zero_is_num_zero [code, code inline, symmetric, code post]:
+lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
"(0\<Colon>int) = Numeral0"
by simp
-lemma one_is_num_one [code, code inline, symmetric, code post]:
+lemma one_is_num_one [code, code_inline, symmetric, code_post]:
"(1\<Colon>int) = Numeral1"
by simp
--- a/src/HOL/IntDiv.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/IntDiv.thy Tue Jul 14 10:54:04 2009 +0200
@@ -36,7 +36,7 @@
text{*algorithm for the general case @{term "b\<noteq>0"}*}
definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
- [code inline]: "negateSnd = apsnd uminus"
+ [code_inline]: "negateSnd = apsnd uminus"
definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--{*The full division algorithm considers all possible signs for a, b
--- a/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 10:54:04 2009 +0200
@@ -24,11 +24,11 @@
lemmas [code del] = char.recs char.cases char.size
-lemma [code, code inline]:
+lemma [code, code_inline]:
"char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)
-lemma [code, code inline]:
+lemma [code, code_inline]:
"char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jul 14 10:54:04 2009 +0200
@@ -26,15 +26,15 @@
code_datatype number_nat_inst.number_of_nat
-lemma zero_nat_code [code, code inline]:
+lemma zero_nat_code [code, code_inline]:
"0 = (Numeral0 :: nat)"
by simp
-lemmas [code post] = zero_nat_code [symmetric]
+lemmas [code_post] = zero_nat_code [symmetric]
-lemma one_nat_code [code, code inline]:
+lemma one_nat_code [code, code_inline]:
"1 = (Numeral1 :: nat)"
by simp
-lemmas [code post] = one_nat_code [symmetric]
+lemmas [code_post] = one_nat_code [symmetric]
lemma Suc_code [code]:
"Suc n = n + 1"
@@ -89,7 +89,7 @@
expression:
*}
-lemma [code, code unfold]:
+lemma [code, code_unfold]:
"nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
@@ -302,7 +302,7 @@
Natural numerals.
*}
-lemma [code inline, symmetric, code post]:
+lemma [code_inline, symmetric, code_post]:
"nat (number_of i) = number_nat_inst.number_of_nat i"
-- {* this interacts as desired with @{thm nat_number_of_def} *}
by (simp add: number_nat_inst.number_of_nat)
@@ -335,9 +335,9 @@
"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]:
+lemma of_nat_int [code_unfold]:
"of_nat = int" by (simp add: int_def)
-declare of_nat_int [symmetric, code post]
+declare of_nat_int [symmetric, code_post]
code_const int
(SML "_")
--- a/src/HOL/Library/Executable_Set.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy Tue Jul 14 10:54:04 2009 +0200
@@ -15,7 +15,7 @@
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
"subset = op \<le>"
-declare subset_def [symmetric, code unfold]
+declare subset_def [symmetric, code_unfold]
lemma [code]:
"subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
@@ -25,7 +25,7 @@
[code del]: "eq_set = op ="
(* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code unfold]
+declare set_eq_subset[code_unfold]
*)
lemma [code]:
@@ -40,7 +40,7 @@
subsection {* Rewrites for primitive operations *}
-declare List_Set.project_def [symmetric, code unfold]
+declare List_Set.project_def [symmetric, code_unfold]
subsection {* code generator setup *}
--- a/src/HOL/Library/Float.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Library/Float.thy Tue Jul 14 10:54:04 2009 +0200
@@ -19,7 +19,7 @@
"of_float (Float a b) = real a * pow2 b"
defs (overloaded)
- real_of_float_def [code unfold]: "real == of_float"
+ real_of_float_def [code_unfold]: "real == of_float"
primrec mantissa :: "float \<Rightarrow> int" where
"mantissa (Float a b) = a"
@@ -42,7 +42,7 @@
instance ..
end
-lemma number_of_float_Float [code inline, symmetric, code post]:
+lemma number_of_float_Float [code_inline, symmetric, code_post]:
"number_of k = Float (number_of k) 0"
by (simp add: number_of_float_def number_of_is_id)
--- a/src/HOL/Library/Fraction_Field.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Tue Jul 14 10:54:04 2009 +0200
@@ -93,10 +93,10 @@
begin
definition
- Zero_fract_def [code, code unfold]: "0 = Fract 0 1"
+ Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
definition
- One_fract_def [code, code unfold]: "1 = Fract 1 1"
+ One_fract_def [code, code_unfold]: "1 = Fract 1 1"
definition
add_fract_def [code del]:
@@ -196,14 +196,14 @@
lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
by (rule of_nat_fract [symmetric])
-lemma fract_collapse [code post]:
+lemma fract_collapse [code_post]:
"Fract 0 k = 0"
"Fract 1 1 = 1"
"Fract k 0 = 0"
by (cases "k = 0")
(simp_all add: Zero_fract_def One_fract_def eq_fract Fract_def)
-lemma fract_expand [code unfold]:
+lemma fract_expand [code_unfold]:
"0 = Fract 0 1"
"1 = Fract 1 1"
by (simp_all add: fract_collapse)
--- a/src/HOL/Library/Nat_Infinity.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Tue Jul 14 10:54:04 2009 +0200
@@ -40,10 +40,10 @@
"0 = Fin 0"
definition
- [code inline]: "1 = Fin 1"
+ [code_inline]: "1 = Fin 1"
definition
- [code inline, code del]: "number_of k = Fin (number_of k)"
+ [code_inline, code del]: "number_of k = Fin (number_of k)"
instance ..
--- a/src/HOL/Library/Polynomial.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy Tue Jul 14 10:54:04 2009 +0200
@@ -1505,7 +1505,7 @@
code_datatype "0::'a::zero poly" pCons
-declare pCons_0_0 [code post]
+declare pCons_0_0 [code_post]
instantiation poly :: ("{zero,eq}") eq
begin
--- a/src/HOL/List.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/List.thy Tue Jul 14 10:54:04 2009 +0200
@@ -2076,7 +2076,7 @@
by(induct xs) simp_all
text{* For efficient code generation: avoid intermediate list. *}
-lemma foldl_map[code unfold]:
+lemma foldl_map[code_unfold]:
"foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
by(induct xs arbitrary:a) simp_all
@@ -2198,7 +2198,7 @@
text{* For efficient code generation ---
@{const listsum} is not tail recursive but @{const foldl} is. *}
-lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
+lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
by(simp add:listsum_foldr foldl_foldr1)
lemma distinct_listsum_conv_Setsum:
@@ -3746,32 +3746,32 @@
show ?case by (induct xs) (auto simp add: Cons aux)
qed
-lemma mem_iff [code post]:
+lemma mem_iff [code_post]:
"x mem xs \<longleftrightarrow> x \<in> set xs"
by (induct xs) auto
-lemmas in_set_code [code unfold] = mem_iff [symmetric]
+lemmas in_set_code [code_unfold] = mem_iff [symmetric]
lemma empty_null:
"xs = [] \<longleftrightarrow> null xs"
by (cases xs) simp_all
-lemma [code inline]:
+lemma [code_inline]:
"eq_class.eq xs [] \<longleftrightarrow> null xs"
by (simp add: eq empty_null)
-lemmas null_empty [code post] =
+lemmas null_empty [code_post] =
empty_null [symmetric]
lemma list_inter_conv:
"set (list_inter xs ys) = set xs \<inter> set ys"
by (induct xs) auto
-lemma list_all_iff [code post]:
+lemma list_all_iff [code_post]:
"list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
by (induct xs) auto
-lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
+lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
lemma list_all_append [simp]:
"list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
@@ -3785,11 +3785,11 @@
"list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
-lemma list_ex_iff [code post]:
+lemma list_ex_iff [code_post]:
"list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
by (induct xs) simp_all
-lemmas list_bex_code [code unfold] =
+lemmas list_bex_code [code_unfold] =
list_ex_iff [symmetric]
lemma list_ex_length:
@@ -3804,7 +3804,7 @@
"map_filter f P xs = map f (filter P xs)"
by (induct xs) auto
-lemma length_remdups_length_unique [code inline]:
+lemma length_remdups_length_unique [code_inline]:
"length (remdups xs) = length_unique xs"
by (induct xs) simp_all
@@ -3813,43 +3813,43 @@
text {* Code for bounded quantification and summation over nats. *}
-lemma atMost_upto [code unfold]:
+lemma atMost_upto [code_unfold]:
"{..n} = set [0..<Suc n]"
by auto
-lemma atLeast_upt [code unfold]:
+lemma atLeast_upt [code_unfold]:
"{..<n} = set [0..<n]"
by auto
-lemma greaterThanLessThan_upt [code unfold]:
+lemma greaterThanLessThan_upt [code_unfold]:
"{n<..<m} = set [Suc n..<m]"
by auto
-lemma atLeastLessThan_upt [code unfold]:
+lemma atLeastLessThan_upt [code_unfold]:
"{n..<m} = set [n..<m]"
by auto
-lemma greaterThanAtMost_upt [code unfold]:
+lemma greaterThanAtMost_upt [code_unfold]:
"{n<..m} = set [Suc n..<Suc m]"
by auto
-lemma atLeastAtMost_upt [code unfold]:
+lemma atLeastAtMost_upt [code_unfold]:
"{n..m} = set [n..<Suc m]"
by auto
-lemma all_nat_less_eq [code unfold]:
+lemma all_nat_less_eq [code_unfold]:
"(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
by auto
-lemma ex_nat_less_eq [code unfold]:
+lemma ex_nat_less_eq [code_unfold]:
"(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
by auto
-lemma all_nat_less [code unfold]:
+lemma all_nat_less [code_unfold]:
"(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
by auto
-lemma ex_nat_less [code unfold]:
+lemma ex_nat_less [code_unfold]:
"(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
by auto
@@ -3857,30 +3857,30 @@
"distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
by (induct xs) simp_all
-lemma setsum_set_upt_conv_listsum [code unfold]:
+lemma setsum_set_upt_conv_listsum [code_unfold]:
"setsum f (set [m..<n]) = listsum (map f [m..<n])"
by (rule setsum_set_distinct_conv_listsum) simp
text {* Code for summation over ints. *}
-lemma greaterThanLessThan_upto [code unfold]:
+lemma greaterThanLessThan_upto [code_unfold]:
"{i<..<j::int} = set [i+1..j - 1]"
by auto
-lemma atLeastLessThan_upto [code unfold]:
+lemma atLeastLessThan_upto [code_unfold]:
"{i..<j::int} = set [i..j - 1]"
by auto
-lemma greaterThanAtMost_upto [code unfold]:
+lemma greaterThanAtMost_upto [code_unfold]:
"{i<..j::int} = set [i+1..j]"
by auto
-lemma atLeastAtMost_upto [code unfold]:
+lemma atLeastAtMost_upto [code_unfold]:
"{i..j::int} = set [i..j]"
by auto
-lemma setsum_set_upto_conv_listsum [code unfold]:
+lemma setsum_set_upto_conv_listsum [code_unfold]:
"setsum f (set [i..j::int]) = listsum (map f [i..j])"
by (rule setsum_set_distinct_conv_listsum) simp
--- a/src/HOL/MicroJava/BV/BVExample.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Tue Jul 14 10:54:04 2009 +0200
@@ -467,7 +467,7 @@
lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
-lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
+lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
code_module BV
contains
--- a/src/HOL/Nat.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Nat.thy Tue Jul 14 10:54:04 2009 +0200
@@ -1200,9 +1200,9 @@
text {* for code generation *}
definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
- funpow_code_def [code post]: "funpow = compow"
+ funpow_code_def [code_post]: "funpow = compow"
-lemmas [code unfold] = funpow_code_def [symmetric]
+lemmas [code_unfold] = funpow_code_def [symmetric]
lemma [code]:
"funpow 0 f = id"
@@ -1265,7 +1265,7 @@
end
-declare of_nat_code [code, code unfold, code inline del]
+declare of_nat_code [code, code_unfold, code_inline del]
text{*Class for unital semirings with characteristic zero.
Includes non-ordered rings like the complex numbers.*}
--- a/src/HOL/Nat_Numeral.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Tue Jul 14 10:54:04 2009 +0200
@@ -20,13 +20,13 @@
begin
definition
- nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
+ nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
instance ..
end
-lemma [code post]:
+lemma [code_post]:
"nat (number_of v) = number_of v"
unfolding nat_number_of_def ..
@@ -316,13 +316,13 @@
lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
by (simp add: nat_number_of_def)
-lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
+lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
by (simp add: nat_number_of_def)
lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
by (simp add: nat_1 nat_number_of_def)
-lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
+lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
by (simp add: nat_numeral_1_eq_1)
--- a/src/HOL/Option.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Option.thy Tue Jul 14 10:54:04 2009 +0200
@@ -94,7 +94,7 @@
subsubsection {* Code generator setup *}
definition is_none :: "'a option \<Rightarrow> bool" where
- [code post]: "is_none x \<longleftrightarrow> x = None"
+ [code_post]: "is_none x \<longleftrightarrow> x = None"
lemma is_none_code [code]:
shows "is_none None \<longleftrightarrow> True"
@@ -105,7 +105,7 @@
"is_none x \<longleftrightarrow> x = None"
by (simp add: is_none_def)
-lemma [code inline]:
+lemma [code_inline]:
"eq_class.eq x None \<longleftrightarrow> is_none x"
by (simp add: eq is_none_none)
--- a/src/HOL/Orderings.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Orderings.thy Tue Jul 14 10:54:04 2009 +0200
@@ -268,13 +268,13 @@
text {* Explicit dictionaries for code generation *}
-lemma min_ord_min [code, code unfold, code inline del]:
+lemma min_ord_min [code, code_unfold, code_inline del]:
"min = ord.min (op \<le>)"
by (rule ext)+ (simp add: min_def ord.min_def)
declare ord.min_def [code]
-lemma max_ord_max [code, code unfold, code inline del]:
+lemma max_ord_max [code, code_unfold, code_inline del]:
"max = ord.max (op \<le>)"
by (rule ext)+ (simp add: max_def ord.max_def)
--- a/src/HOL/Power.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Power.thy Tue Jul 14 10:54:04 2009 +0200
@@ -455,7 +455,7 @@
subsection {* Code generator tweak *}
-lemma power_power_power [code, code unfold, code inline del]:
+lemma power_power_power [code, code_unfold, code_inline del]:
"power = power.power (1::'a::{power}) (op *)"
unfolding power_def power.power_def ..
--- a/src/HOL/Rational.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Rational.thy Tue Jul 14 10:54:04 2009 +0200
@@ -93,10 +93,10 @@
begin
definition
- Zero_rat_def [code, code unfold]: "0 = Fract 0 1"
+ Zero_rat_def [code, code_unfold]: "0 = Fract 0 1"
definition
- One_rat_def [code, code unfold]: "1 = Fract 1 1"
+ One_rat_def [code, code_unfold]: "1 = Fract 1 1"
definition
add_rat_def [code del]:
@@ -211,7 +211,7 @@
end
-lemma rat_number_collapse [code post]:
+lemma rat_number_collapse [code_post]:
"Fract 0 k = 0"
"Fract 1 1 = 1"
"Fract (number_of k) 1 = number_of k"
@@ -219,7 +219,7 @@
by (cases "k = 0")
(simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def)
-lemma rat_number_expand [code unfold]:
+lemma rat_number_expand [code_unfold]:
"0 = Fract 0 1"
"1 = Fract 1 1"
"number_of k = Fract (number_of k) 1"
@@ -291,11 +291,11 @@
lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
by (simp add: Fract_of_int_eq [symmetric])
-lemma Fract_number_of_quotient [code post]:
+lemma Fract_number_of_quotient [code_post]:
"Fract (number_of k) (number_of l) = number_of k / number_of l"
unfolding Fract_of_int_quotient number_of_is_id number_of_eq ..
-lemma Fract_1_number_of [code post]:
+lemma Fract_1_number_of [code_post]:
"Fract 1 (number_of k) = 1 / number_of k"
unfolding Fract_of_int_quotient number_of_eq by simp
@@ -1003,7 +1003,7 @@
definition (in term_syntax)
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+ [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
notation fcomp (infixl "o>" 60)
notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/RealDef.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/RealDef.thy Tue Jul 14 10:54:04 2009 +0200
@@ -559,8 +559,8 @@
real :: "'a => real"
defs (overloaded)
- real_of_nat_def [code unfold]: "real == real_of_nat"
- real_of_int_def [code unfold]: "real == real_of_int"
+ real_of_nat_def [code_unfold]: "real == real_of_nat"
+ real_of_int_def [code_unfold]: "real == real_of_int"
lemma real_eq_of_nat: "real = of_nat"
unfolding real_of_nat_def ..
@@ -946,7 +946,7 @@
end
-lemma [code unfold, symmetric, code post]:
+lemma [code_unfold, symmetric, code_post]:
"number_of k = real_of_int (number_of k)"
unfolding number_of_is_id real_number_of_def ..
@@ -1061,29 +1061,29 @@
code_datatype Ratreal
-lemma Ratreal_number_collapse [code post]:
+lemma Ratreal_number_collapse [code_post]:
"Ratreal 0 = 0"
"Ratreal 1 = 1"
"Ratreal (number_of k) = number_of k"
by simp_all
-lemma zero_real_code [code, code unfold]:
+lemma zero_real_code [code, code_unfold]:
"0 = Ratreal 0"
by simp
-lemma one_real_code [code, code unfold]:
+lemma one_real_code [code, code_unfold]:
"1 = Ratreal 1"
by simp
-lemma number_of_real_code [code unfold]:
+lemma number_of_real_code [code_unfold]:
"number_of k = Ratreal (number_of k)"
by simp
-lemma Ratreal_number_of_quotient [code post]:
+lemma Ratreal_number_of_quotient [code_post]:
"Ratreal (number_of r) / Ratreal (number_of s) = number_of r / number_of s"
by simp
-lemma Ratreal_number_of_quotient2 [code post]:
+lemma Ratreal_number_of_quotient2 [code_post]:
"Ratreal (number_of r / number_of s) = number_of r / number_of s"
unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
@@ -1129,7 +1129,7 @@
definition (in term_syntax)
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+ [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
notation fcomp (infixl "o>" 60)
notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/SetInterval.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/SetInterval.thy Tue Jul 14 10:54:04 2009 +0200
@@ -284,8 +284,8 @@
lemma atLeast0AtMost: "{0..n::nat} = {..n}"
by(simp add:atMost_def atLeastAtMost_def)
-declare atLeast0LessThan[symmetric, code unfold]
- atLeast0AtMost[symmetric, code unfold]
+declare atLeast0LessThan[symmetric, code_unfold]
+ atLeast0AtMost[symmetric, code_unfold]
lemma atLeastLessThan0: "{m..<0::nat} = {}"
by (simp add: atLeastLessThan_def)
--- a/src/HOL/String.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/String.thy Tue Jul 14 10:54:04 2009 +0200
@@ -58,11 +58,11 @@
end
*}
-lemma char_case_nibble_pair [code, code inline]:
+lemma char_case_nibble_pair [code, code_inline]:
"char_case f = split f o nibble_pair_of_char"
by (simp add: expand_fun_eq split: char.split)
-lemma char_rec_nibble_pair [code, code inline]:
+lemma char_rec_nibble_pair [code, code_inline]:
"char_rec f = split f o nibble_pair_of_char"
unfolding char_case_nibble_pair [symmetric]
by (simp add: expand_fun_eq split: char.split)
--- a/src/HOL/Tools/inductive_codegen.ML Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Jul 14 10:54:04 2009 +0200
@@ -697,7 +697,8 @@
val setup =
add_codegen "inductive" inductive_codegen #>
- Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
- Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
+ Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
+ Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
+ "introduction rules for executable predicates";
end;
--- a/src/HOL/Tools/inductive_set.ML Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Tue Jul 14 10:54:04 2009 +0200
@@ -541,8 +541,9 @@
"declare rules for converting between predicate and set notation" #>
Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
- Code.add_attribute ("ind_set",
- Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
+ Attrib.setup @{binding code_ind_set}
+ (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att))
+ "introduction rules for executable predicates" #>
Codegen.add_preprocessor codegen_preproc #>
Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
"declaration of monotonicity rule for set operators" #>
--- a/src/HOL/Tools/recfun_codegen.ML Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Jul 14 10:54:04 2009 +0200
@@ -23,15 +23,13 @@
fun merge _ = Symtab.merge (K true);
);
-fun add_thm NONE thm thy = Code.add_eqn thm thy
- | add_thm (SOME module_name) thm thy =
- let
- val (thm', _) = Code.mk_eqn thy (thm, true)
- in
- thy
- |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
- |> Code.add_eqn thm'
- end;
+fun add_thm_target module_name thm thy =
+ let
+ val (thm', _) = Code.mk_eqn thy (thm, true)
+ in
+ thy
+ |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
+ end;
fun expand_eta thy [] = []
| expand_eta thy (thms as thm :: _) =
@@ -163,15 +161,8 @@
end)
| _ => NONE);
-val setup = let
- fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
- (add_thm opt_module thm) I);
- val del = Thm.declaration_attribute (fn thm => Context.mapping
- (Code.del_eqn thm) I);
-in
+val setup =
add_codegen "recfun" recfun_codegen
- #> Code.add_attribute ("", Args.del |-- Scan.succeed del
- || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)
-end;
+ #> Code.set_code_target_attr add_thm_target;
end;
--- a/src/HOL/ex/Numeral.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/ex/Numeral.thy Tue Jul 14 10:54:04 2009 +0200
@@ -751,14 +751,14 @@
subsection {* Code generator setup for @{typ int} *}
definition Pls :: "num \<Rightarrow> int" where
- [simp, code post]: "Pls n = of_num n"
+ [simp, code_post]: "Pls n = of_num n"
definition Mns :: "num \<Rightarrow> int" where
- [simp, code post]: "Mns n = - of_num n"
+ [simp, code_post]: "Mns n = - of_num n"
code_datatype "0::int" Pls Mns
-lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
+lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
[simp, code del]: "sub m n = (of_num m - of_num n)"
@@ -874,10 +874,10 @@
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
by (simp_all add: of_num_less_iff)
-lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp
-lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp
-declare zero_is_num_zero [code inline del]
-declare one_is_num_one [code inline del]
+lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
+lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
+declare zero_is_num_zero [code_inline del]
+declare one_is_num_one [code_inline del]
hide (open) const sub dup
--- a/src/Pure/Isar/code.ML Tue Jul 14 10:53:44 2009 +0200
+++ b/src/Pure/Isar/code.ML Tue Jul 14 10:54:04 2009 +0200
@@ -62,7 +62,7 @@
val print_codesetup: theory -> unit
(*infrastructure*)
- val add_attribute: string * attribute parser -> theory -> theory
+ val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
val purge_data: theory -> theory
end;
@@ -235,31 +235,6 @@
end;
-(** code attributes **)
-
-structure Code_Attr = TheoryDataFun (
- type T = (string * attribute parser) list;
- val empty = [];
- val copy = I;
- val extend = I;
- fun merge _ = AList.merge (op = : string * string -> bool) (K true);
-);
-
-fun add_attribute (attr as (name, _)) =
- let
- fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
- | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
- in Code_Attr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
- then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
- end;
-
-val _ = Context.>> (Context.map_theory
- (Attrib.setup (Binding.name "code")
- (Scan.peek (fn context =>
- List.foldr op || Scan.fail (map snd (Code_Attr.get (Context.theory_of context)))))
- "declare theorems for code generation"));
-
-
(** data store **)
(* code equations *)
@@ -543,7 +518,7 @@
in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
let
- val _ = if tyco' <> tyco
+ val _ = if (tyco' : string) <> tyco
then error "Different type constructors in constructor set"
else ();
val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
@@ -911,18 +886,32 @@
of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
| NONE => thy;
+structure Code_Attr = TheoryDataFun (
+ type T = (string -> thm -> theory -> theory) option;
+ val empty = NONE;
+ val copy = I;
+ val extend = I;
+ fun merge _ (NONE, f2) = f2
+ | merge _ (f1, _) = f1;
+);
+
+fun set_code_target_attr f = Code_Attr.map (K (SOME f));
+
val _ = Context.>> (Context.map_theory
(let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
- fun add_simple_attribute (name, f) =
- add_attribute (name, Scan.succeed (mk_attribute f));
- fun add_del_attribute (name, (add, del)) =
- add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
- || Scan.succeed (mk_attribute add))
+ val code_attribute_parser =
+ Args.del |-- Scan.succeed (mk_attribute del_eqn)
+ || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
+ || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
+ (fn prefix => mk_attribute (fn thm => fn thy => thy
+ |> add_warning_eqn thm
+ |> the_default ((K o K) I) (Code_Attr.get thy) prefix thm)))
+ || Scan.succeed (mk_attribute add_warning_eqn);
in
Type_Interpretation.init
- #> add_del_attribute ("", (add_warning_eqn, del_eqn))
- #> add_simple_attribute ("nbe", add_nbe_eqn)
+ #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
+ "declare theorems for code generation"
end));
--- a/src/Tools/Code/code_preproc.ML Tue Jul 14 10:53:44 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Tue Jul 14 10:54:04 2009 +0200
@@ -526,14 +526,16 @@
val setup =
let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
- fun add_del_attribute (name, (add, del)) =
- Code.add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
- || Scan.succeed (mk_attribute add))
+ fun add_del_attribute_parser (add, del) =
+ Attrib.add_del (mk_attribute add) (mk_attribute del);
in
- add_del_attribute ("inline", (add_inline, del_inline))
- #> add_del_attribute ("post", (add_post, del_post))
- #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
- (fn thm => Context.mapping (Codegen.add_unfold thm #> add_inline thm) I)))
+ Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
+ "preprocessing equations for code generator"
+ #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
+ "postprocessing equations for code generator"
+ #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
+ (fn thm => Codegen.add_unfold thm #> add_inline thm)))
+ "preprocessing equations for code generators"
end;
val _ =