src/HOL/Code_Numeral.thy
changeset 54489 03ff4d1e6784
parent 53069 d165213e3924
child 55414 eab03e9cee8a
child 55427 ff54d22fe357
     1.1 --- a/src/HOL/Code_Numeral.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -96,10 +96,6 @@
     1.4  qed
     1.5  
     1.6  lemma [transfer_rule]:
     1.7 -  "fun_rel HOL.eq pcr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
     1.8 -  by (unfold neg_numeral_def [abs_def]) transfer_prover
     1.9 -
    1.10 -lemma [transfer_rule]:
    1.11    "fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.12    by (unfold Num.sub_def [abs_def]) transfer_prover
    1.13  
    1.14 @@ -147,10 +143,6 @@
    1.15    "int_of_integer (numeral k) = numeral k"
    1.16    by transfer rule
    1.17  
    1.18 -lemma int_of_integer_neg_numeral [simp]:
    1.19 -  "int_of_integer (neg_numeral k) = neg_numeral k"
    1.20 -  by transfer rule
    1.21 -
    1.22  lemma int_of_integer_sub [simp]:
    1.23    "int_of_integer (Num.sub k l) = Num.sub k l"
    1.24    by transfer rule
    1.25 @@ -253,11 +245,11 @@
    1.26  
    1.27  definition Neg :: "num \<Rightarrow> integer"
    1.28  where
    1.29 -  [simp, code_abbrev]: "Neg = neg_numeral"
    1.30 +  [simp, code_abbrev]: "Neg n = - Pos n"
    1.31  
    1.32  lemma [transfer_rule]:
    1.33 -  "fun_rel HOL.eq pcr_integer neg_numeral Neg"
    1.34 -  by simp transfer_prover
    1.35 +  "fun_rel HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
    1.36 +  by (simp add: Neg_def [abs_def]) transfer_prover
    1.37  
    1.38  code_datatype "0::integer" Pos Neg
    1.39  
    1.40 @@ -272,7 +264,7 @@
    1.41    "dup 0 = 0"
    1.42    "dup (Pos n) = Pos (Num.Bit0 n)"
    1.43    "dup (Neg n) = Neg (Num.Bit0 n)"
    1.44 -  by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
    1.45 +  by (transfer, simp only: numeral_Bit0 minus_add_distrib)+
    1.46  
    1.47  lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
    1.48    is "\<lambda>m n. numeral m - numeral n :: int"