# HG changeset patch # User haftmann # Date 1247581652 -7200 # Node ID 6d28bbd33e2cf4ef4214b82c7f6cbbc7e8c61ed8 # Parent 98acc234d683eaa501b9aaca116d67d8119b32cc prefer code_inline over code_unfold; use code_unfold_post where appropriate diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Code_Eval.thy --- a/src/HOL/Code_Eval.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Code_Eval.thy Tue Jul 14 16:27:32 2009 +0200 @@ -32,7 +32,7 @@ \ 'a \ (unit \ term) \ 'b \ (unit \ term)" where "valapp f x = (fst f (fst x), \u. App (snd f ()) (snd x ()))" -lemma valapp_code [code, code_inline]: +lemma valapp_code [code, code_unfold]: "valapp (f, tf) (x, tx) = (f x, \u. App (tf ()) (tx ()))" by (simp only: valapp_def fst_conv snd_conv) diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Code_Numeral.thy Tue Jul 14 16:27:32 2009 +0200 @@ -176,13 +176,13 @@ end -lemma zero_code_numeral_code [code_inline, code]: +lemma zero_code_numeral_code [code, code_unfold]: "(0\code_numeral) = Numeral0" by (simp add: number_of_code_numeral_def Pls_def) lemma [code_post]: "Numeral0 = (0\code_numeral)" using zero_code_numeral_code .. -lemma one_code_numeral_code [code_inline, code]: +lemma one_code_numeral_code [code, code_unfold]: "(1\code_numeral) = Numeral1" by (simp add: number_of_code_numeral_def Pls_def Bit1_def) lemma [code_post]: "Numeral1 = (1\code_numeral)" diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 14 16:27:32 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_unfold]: "raise s = raise_exc (Fail (STR s))" unfolding Fail_def raise_exc_def raise_def .. diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Int.thy --- a/src/HOL/Int.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Int.thy Tue Jul 14 16:27:32 2009 +0200 @@ -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_unfold_post]: "(0\int) = Numeral0" by simp -lemma one_is_num_one [code, code_inline, symmetric, code_post]: +lemma one_is_num_one [code, code_unfold_post]: "(1\int) = Numeral1" by simp diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/IntDiv.thy Tue Jul 14 16:27:32 2009 +0200 @@ -36,7 +36,7 @@ text{*algorithm for the general case @{term "b\0"}*} definition negateSnd :: "int \ int \ int \ int" where - [code_inline]: "negateSnd = apsnd uminus" + [code_unfold]: "negateSnd = apsnd uminus" definition divmod :: "int \ int \ int \ int" where --{*The full division algorithm considers all possible signs for a, b diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Library/Code_Char_chr.thy --- a/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 16:27:32 2009 +0200 @@ -24,11 +24,11 @@ lemmas [code del] = char.recs char.cases char.size -lemma [code, code_inline]: +lemma [code, code_unfold]: "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_unfold]: "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) diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Jul 14 16:27:32 2009 +0200 @@ -26,15 +26,13 @@ code_datatype number_nat_inst.number_of_nat -lemma zero_nat_code [code, code_inline]: +lemma zero_nat_code [code, code_unfold_post]: "0 = (Numeral0 :: nat)" by simp -lemmas [code_post] = zero_nat_code [symmetric] -lemma one_nat_code [code, code_inline]: +lemma one_nat_code [code, code_unfold_post]: "1 = (Numeral1 :: nat)" by simp -lemmas [code_post] = one_nat_code [symmetric] lemma Suc_code [code]: "Suc n = n + 1" @@ -302,7 +300,7 @@ Natural numerals. *} -lemma [code_inline, symmetric, code_post]: +lemma [code_unfold_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 +333,8 @@ "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]: +lemma of_nat_int [code_unfold_post]: "of_nat = int" by (simp add: int_def) -declare of_nat_int [symmetric, code_post] code_const int (SML "_") diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Library/Float.thy Tue Jul 14 16:27:32 2009 +0200 @@ -42,7 +42,7 @@ instance .. end -lemma number_of_float_Float [code_inline, symmetric, code_post]: +lemma number_of_float_Float [code_unfold_post]: "number_of k = Float (number_of k) 0" by (simp add: number_of_float_def number_of_is_id) diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Library/Nat_Infinity.thy --- a/src/HOL/Library/Nat_Infinity.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Library/Nat_Infinity.thy Tue Jul 14 16:27:32 2009 +0200 @@ -40,10 +40,10 @@ "0 = Fin 0" definition - [code_inline]: "1 = Fin 1" + [code_unfold]: "1 = Fin 1" definition - [code_inline, code del]: "number_of k = Fin (number_of k)" + [code_unfold, code del]: "number_of k = Fin (number_of k)" instance .. diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/List.thy --- a/src/HOL/List.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/List.thy Tue Jul 14 16:27:32 2009 +0200 @@ -3756,7 +3756,7 @@ "xs = [] \ null xs" by (cases xs) simp_all -lemma [code_inline]: +lemma [code_unfold]: "eq_class.eq xs [] \ null xs" by (simp add: eq empty_null) @@ -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_unfold]: "length (remdups xs) = length_unique xs" by (induct xs) simp_all diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Nat_Numeral.thy Tue Jul 14 16:27:32 2009 +0200 @@ -20,7 +20,7 @@ begin definition - nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)" + nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)" instance .. diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Option.thy --- a/src/HOL/Option.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Option.thy Tue Jul 14 16:27:32 2009 +0200 @@ -105,7 +105,7 @@ "is_none x \ x = None" by (simp add: is_none_def) -lemma [code_inline]: +lemma [code_unfold]: "eq_class.eq x None \ is_none x" by (simp add: eq is_none_none) diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Rational.thy --- a/src/HOL/Rational.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Rational.thy Tue Jul 14 16:27:32 2009 +0200 @@ -1003,7 +1003,7 @@ definition (in term_syntax) valterm_fract :: "int \ (unit \ Code_Eval.term) \ int \ (unit \ Code_Eval.term) \ rat \ (unit \ Code_Eval.term)" where - [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\} k {\} l" + [code_unfold]: "valterm_fract k l = Code_Eval.valtermify Fract {\} k {\} l" notation fcomp (infixl "o>" 60) notation scomp (infixl "o\" 60) diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/RealDef.thy Tue Jul 14 16:27:32 2009 +0200 @@ -946,7 +946,7 @@ end -lemma [code_unfold, symmetric, code_post]: +lemma [code_unfold_post]: "number_of k = real_of_int (number_of k)" unfolding number_of_is_id real_number_of_def .. @@ -1129,7 +1129,7 @@ definition (in term_syntax) valterm_ratreal :: "rat \ (unit \ Code_Eval.term) \ real \ (unit \ Code_Eval.term)" where - [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\} k" + [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\} k" notation fcomp (infixl "o>" 60) notation scomp (infixl "o\" 60) diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/String.thy --- a/src/HOL/String.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/String.thy Tue Jul 14 16:27:32 2009 +0200 @@ -58,11 +58,11 @@ end *} -lemma char_case_nibble_pair [code, code_inline]: +lemma char_case_nibble_pair [code, code_unfold]: "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_unfold]: "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) diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/ex/Numeral.thy Tue Jul 14 16:27:32 2009 +0200 @@ -758,7 +758,7 @@ code_datatype "0::int" Pls Mns -lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric] +lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric] definition sub :: "num \ num \ 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) \ Numeral0" by simp -lemma [code_inline del]: "(1::int) \ Numeral1" by simp -declare zero_is_num_zero [code_inline del] -declare one_is_num_one [code_inline del] +lemma [code_unfold del]: "(0::int) \ Numeral0" by simp +lemma [code_unfold del]: "(1::int) \ Numeral1" by simp +declare zero_is_num_zero [code_unfold del] +declare one_is_num_one [code_unfold del] hide (open) const sub dup