prefer code_inline over code_unfold; use code_unfold_post where appropriate
authorhaftmann
Tue Jul 14 16:27:32 2009 +0200 (2009-07-14)
changeset 320696d28bbd33e2c
parent 32068 98acc234d683
child 32070 c670a31c964c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
src/HOL/Code_Eval.thy
src/HOL/Code_Numeral.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/Library/Code_Char_chr.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Float.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/List.thy
src/HOL/Nat_Numeral.thy
src/HOL/Option.thy
src/HOL/Rational.thy
src/HOL/RealDef.thy
src/HOL/String.thy
src/HOL/ex/Numeral.thy
     1.1 --- a/src/HOL/Code_Eval.thy	Tue Jul 14 16:27:31 2009 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Tue Jul 14 16:27:32 2009 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
     1.5    "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
     1.6  
     1.7 -lemma valapp_code [code, code_inline]:
     1.8 +lemma valapp_code [code, code_unfold]:
     1.9    "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
    1.10    by (simp only: valapp_def fst_conv snd_conv)
    1.11  
     2.1 --- a/src/HOL/Code_Numeral.thy	Tue Jul 14 16:27:31 2009 +0200
     2.2 +++ b/src/HOL/Code_Numeral.thy	Tue Jul 14 16:27:32 2009 +0200
     2.3 @@ -176,13 +176,13 @@
     2.4  
     2.5  end
     2.6  
     2.7 -lemma zero_code_numeral_code [code_inline, code]:
     2.8 +lemma zero_code_numeral_code [code, code_unfold]:
     2.9    "(0\<Colon>code_numeral) = Numeral0"
    2.10    by (simp add: number_of_code_numeral_def Pls_def)
    2.11  lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
    2.12    using zero_code_numeral_code ..
    2.13  
    2.14 -lemma one_code_numeral_code [code_inline, code]:
    2.15 +lemma one_code_numeral_code [code, code_unfold]:
    2.16    "(1\<Colon>code_numeral) = Numeral1"
    2.17    by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
    2.18  lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
     3.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 14 16:27:31 2009 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 14 16:27:32 2009 +0200
     3.3 @@ -283,7 +283,7 @@
     3.4  where
     3.5    [code del]: "raise_exc e = raise []"
     3.6  
     3.7 -lemma raise_raise_exc [code, code_inline]:
     3.8 +lemma raise_raise_exc [code, code_unfold]:
     3.9    "raise s = raise_exc (Fail (STR s))"
    3.10    unfolding Fail_def raise_exc_def raise_def ..
    3.11  
     4.1 --- a/src/HOL/Int.thy	Tue Jul 14 16:27:31 2009 +0200
     4.2 +++ b/src/HOL/Int.thy	Tue Jul 14 16:27:32 2009 +0200
     4.3 @@ -2126,11 +2126,11 @@
     4.4  
     4.5  hide (open) const nat_aux
     4.6  
     4.7 -lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
     4.8 +lemma zero_is_num_zero [code, code_unfold_post]:
     4.9    "(0\<Colon>int) = Numeral0" 
    4.10    by simp
    4.11  
    4.12 -lemma one_is_num_one [code, code_inline, symmetric, code_post]:
    4.13 +lemma one_is_num_one [code, code_unfold_post]:
    4.14    "(1\<Colon>int) = Numeral1" 
    4.15    by simp
    4.16  
     5.1 --- a/src/HOL/IntDiv.thy	Tue Jul 14 16:27:31 2009 +0200
     5.2 +++ b/src/HOL/IntDiv.thy	Tue Jul 14 16:27:32 2009 +0200
     5.3 @@ -36,7 +36,7 @@
     5.4  
     5.5  text{*algorithm for the general case @{term "b\<noteq>0"}*}
     5.6  definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
     5.7 -  [code_inline]: "negateSnd = apsnd uminus"
     5.8 +  [code_unfold]: "negateSnd = apsnd uminus"
     5.9  
    5.10  definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    5.11      --{*The full division algorithm considers all possible signs for a, b
     6.1 --- a/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 16:27:31 2009 +0200
     6.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 16:27:32 2009 +0200
     6.3 @@ -24,11 +24,11 @@
     6.4  
     6.5  lemmas [code del] = char.recs char.cases char.size
     6.6  
     6.7 -lemma [code, code_inline]:
     6.8 +lemma [code, code_unfold]:
     6.9    "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
    6.10    by (cases c) (auto simp add: nibble_pair_of_nat_char)
    6.11  
    6.12 -lemma [code, code_inline]:
    6.13 +lemma [code, code_unfold]:
    6.14    "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
    6.15    by (cases c) (auto simp add: nibble_pair_of_nat_char)
    6.16  
     7.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 16:27:31 2009 +0200
     7.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 16:27:32 2009 +0200
     7.3 @@ -26,15 +26,13 @@
     7.4  
     7.5  code_datatype number_nat_inst.number_of_nat
     7.6  
     7.7 -lemma zero_nat_code [code, code_inline]:
     7.8 +lemma zero_nat_code [code, code_unfold_post]:
     7.9    "0 = (Numeral0 :: nat)"
    7.10    by simp
    7.11 -lemmas [code_post] = zero_nat_code [symmetric]
    7.12  
    7.13 -lemma one_nat_code [code, code_inline]:
    7.14 +lemma one_nat_code [code, code_unfold_post]:
    7.15    "1 = (Numeral1 :: nat)"
    7.16    by simp
    7.17 -lemmas [code_post] = one_nat_code [symmetric]
    7.18  
    7.19  lemma Suc_code [code]:
    7.20    "Suc n = n + 1"
    7.21 @@ -302,7 +300,7 @@
    7.22    Natural numerals.
    7.23  *}
    7.24  
    7.25 -lemma [code_inline, symmetric, code_post]:
    7.26 +lemma [code_unfold_post]:
    7.27    "nat (number_of i) = number_nat_inst.number_of_nat i"
    7.28    -- {* this interacts as desired with @{thm nat_number_of_def} *}
    7.29    by (simp add: number_nat_inst.number_of_nat)
    7.30 @@ -335,9 +333,8 @@
    7.31    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
    7.32    unfolding nat_number_of_def number_of_is_id neg_def by simp
    7.33  
    7.34 -lemma of_nat_int [code_unfold]:
    7.35 +lemma of_nat_int [code_unfold_post]:
    7.36    "of_nat = int" by (simp add: int_def)
    7.37 -declare of_nat_int [symmetric, code_post]
    7.38  
    7.39  code_const int
    7.40    (SML "_")
     8.1 --- a/src/HOL/Library/Float.thy	Tue Jul 14 16:27:31 2009 +0200
     8.2 +++ b/src/HOL/Library/Float.thy	Tue Jul 14 16:27:32 2009 +0200
     8.3 @@ -42,7 +42,7 @@
     8.4  instance ..
     8.5  end
     8.6  
     8.7 -lemma number_of_float_Float [code_inline, symmetric, code_post]:
     8.8 +lemma number_of_float_Float [code_unfold_post]:
     8.9    "number_of k = Float (number_of k) 0"
    8.10    by (simp add: number_of_float_def number_of_is_id)
    8.11  
     9.1 --- a/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 16:27:31 2009 +0200
     9.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 16:27:32 2009 +0200
     9.3 @@ -40,10 +40,10 @@
     9.4    "0 = Fin 0"
     9.5  
     9.6  definition
     9.7 -  [code_inline]: "1 = Fin 1"
     9.8 +  [code_unfold]: "1 = Fin 1"
     9.9  
    9.10  definition
    9.11 -  [code_inline, code del]: "number_of k = Fin (number_of k)"
    9.12 +  [code_unfold, code del]: "number_of k = Fin (number_of k)"
    9.13  
    9.14  instance ..
    9.15  
    10.1 --- a/src/HOL/List.thy	Tue Jul 14 16:27:31 2009 +0200
    10.2 +++ b/src/HOL/List.thy	Tue Jul 14 16:27:32 2009 +0200
    10.3 @@ -3756,7 +3756,7 @@
    10.4    "xs = [] \<longleftrightarrow> null xs"
    10.5  by (cases xs) simp_all
    10.6  
    10.7 -lemma [code_inline]:
    10.8 +lemma [code_unfold]:
    10.9    "eq_class.eq xs [] \<longleftrightarrow> null xs"
   10.10  by (simp add: eq empty_null)
   10.11  
   10.12 @@ -3804,7 +3804,7 @@
   10.13    "map_filter f P xs = map f (filter P xs)"
   10.14  by (induct xs) auto
   10.15  
   10.16 -lemma length_remdups_length_unique [code_inline]:
   10.17 +lemma length_remdups_length_unique [code_unfold]:
   10.18    "length (remdups xs) = length_unique xs"
   10.19    by (induct xs) simp_all
   10.20  
    11.1 --- a/src/HOL/Nat_Numeral.thy	Tue Jul 14 16:27:31 2009 +0200
    11.2 +++ b/src/HOL/Nat_Numeral.thy	Tue Jul 14 16:27:32 2009 +0200
    11.3 @@ -20,7 +20,7 @@
    11.4  begin
    11.5  
    11.6  definition
    11.7 -  nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
    11.8 +  nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
    11.9  
   11.10  instance ..
   11.11  
    12.1 --- a/src/HOL/Option.thy	Tue Jul 14 16:27:31 2009 +0200
    12.2 +++ b/src/HOL/Option.thy	Tue Jul 14 16:27:32 2009 +0200
    12.3 @@ -105,7 +105,7 @@
    12.4    "is_none x \<longleftrightarrow> x = None"
    12.5    by (simp add: is_none_def)
    12.6  
    12.7 -lemma [code_inline]:
    12.8 +lemma [code_unfold]:
    12.9    "eq_class.eq x None \<longleftrightarrow> is_none x"
   12.10    by (simp add: eq is_none_none)
   12.11  
    13.1 --- a/src/HOL/Rational.thy	Tue Jul 14 16:27:31 2009 +0200
    13.2 +++ b/src/HOL/Rational.thy	Tue Jul 14 16:27:32 2009 +0200
    13.3 @@ -1003,7 +1003,7 @@
    13.4  
    13.5  definition (in term_syntax)
    13.6    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
    13.7 -  [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
    13.8 +  [code_unfold]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
    13.9  
   13.10  notation fcomp (infixl "o>" 60)
   13.11  notation scomp (infixl "o\<rightarrow>" 60)
    14.1 --- a/src/HOL/RealDef.thy	Tue Jul 14 16:27:31 2009 +0200
    14.2 +++ b/src/HOL/RealDef.thy	Tue Jul 14 16:27:32 2009 +0200
    14.3 @@ -946,7 +946,7 @@
    14.4  
    14.5  end
    14.6  
    14.7 -lemma [code_unfold, symmetric, code_post]:
    14.8 +lemma [code_unfold_post]:
    14.9    "number_of k = real_of_int (number_of k)"
   14.10    unfolding number_of_is_id real_number_of_def ..
   14.11  
   14.12 @@ -1129,7 +1129,7 @@
   14.13  
   14.14  definition (in term_syntax)
   14.15    valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
   14.16 -  [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
   14.17 +  [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
   14.18  
   14.19  notation fcomp (infixl "o>" 60)
   14.20  notation scomp (infixl "o\<rightarrow>" 60)
    15.1 --- a/src/HOL/String.thy	Tue Jul 14 16:27:31 2009 +0200
    15.2 +++ b/src/HOL/String.thy	Tue Jul 14 16:27:32 2009 +0200
    15.3 @@ -58,11 +58,11 @@
    15.4  end
    15.5  *}
    15.6  
    15.7 -lemma char_case_nibble_pair [code, code_inline]:
    15.8 +lemma char_case_nibble_pair [code, code_unfold]:
    15.9    "char_case f = split f o nibble_pair_of_char"
   15.10    by (simp add: expand_fun_eq split: char.split)
   15.11  
   15.12 -lemma char_rec_nibble_pair [code, code_inline]:
   15.13 +lemma char_rec_nibble_pair [code, code_unfold]:
   15.14    "char_rec f = split f o nibble_pair_of_char"
   15.15    unfolding char_case_nibble_pair [symmetric]
   15.16    by (simp add: expand_fun_eq split: char.split)
    16.1 --- a/src/HOL/ex/Numeral.thy	Tue Jul 14 16:27:31 2009 +0200
    16.2 +++ b/src/HOL/ex/Numeral.thy	Tue Jul 14 16:27:32 2009 +0200
    16.3 @@ -758,7 +758,7 @@
    16.4  
    16.5  code_datatype "0::int" Pls Mns
    16.6  
    16.7 -lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
    16.8 +lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
    16.9  
   16.10  definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   16.11    [simp, code del]: "sub m n = (of_num m - of_num n)"
   16.12 @@ -874,10 +874,10 @@
   16.13    using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
   16.14    by (simp_all add: of_num_less_iff)
   16.15  
   16.16 -lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
   16.17 -lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
   16.18 -declare zero_is_num_zero [code_inline del]
   16.19 -declare one_is_num_one [code_inline del]
   16.20 +lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp
   16.21 +lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp
   16.22 +declare zero_is_num_zero [code_unfold del]
   16.23 +declare one_is_num_one [code_unfold del]
   16.24  
   16.25  hide (open) const sub dup
   16.26