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"
```