src/HOL/Library/Code_Target_Int.thy
changeset 64997 067a6cca39f0
parent 64242 93c6f0da5c70
child 65552 f533820e7248
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Tue Feb 07 22:15:04 2017 +0100
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Tue Feb 07 22:15:05 2017 +0100
     1.3 @@ -35,7 +35,24 @@
     1.4  lemma [code_abbrev]:
     1.5    "int_of_integer (- numeral k) = Int.Neg k"
     1.6    by transfer simp
     1.7 -  
     1.8 +
     1.9 +context
    1.10 +begin  
    1.11 +
    1.12 +qualified definition positive :: "num \<Rightarrow> int"
    1.13 +  where [simp]: "positive = numeral"
    1.14 +
    1.15 +qualified definition negative :: "num \<Rightarrow> int"
    1.16 +  where [simp]: "negative = uminus \<circ> numeral"
    1.17 +
    1.18 +lemma [code_computation_unfold]:
    1.19 +  "numeral = positive"
    1.20 +  "Int.Pos = positive"
    1.21 +  "Int.Neg = negative"
    1.22 +  by (simp_all add: fun_eq_iff)
    1.23 +
    1.24 +end
    1.25 +
    1.26  lemma [code, symmetric, code_post]:
    1.27    "0 = int_of_integer 0"
    1.28    by transfer simp