src/HOL/Code_Numeral.thy
changeset 64994 6e4c05e8edbb
parent 64848 c50db2128048
child 66190 a41435469559
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Feb 06 20:56:37 2017 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Feb 06 20:56:38 2017 +0100
     1.3 @@ -342,6 +342,26 @@
     1.4  
     1.5  code_datatype "0::integer" Pos Neg
     1.6  
     1.7 +  
     1.8 +text \<open>A further pair of constructors for generated computations\<close>
     1.9 +
    1.10 +context
    1.11 +begin  
    1.12 +
    1.13 +qualified definition positive :: "num \<Rightarrow> integer"
    1.14 +  where [simp]: "positive = numeral"
    1.15 +
    1.16 +qualified definition negative :: "num \<Rightarrow> integer"
    1.17 +  where [simp]: "negative = uminus \<circ> numeral"
    1.18 +
    1.19 +lemma [code_computation_unfold]:
    1.20 +  "numeral = positive"
    1.21 +  "Pos = positive"
    1.22 +  "Neg = negative"
    1.23 +  by (simp_all add: fun_eq_iff)
    1.24 +
    1.25 +end
    1.26 +
    1.27  
    1.28  text \<open>Auxiliary operations\<close>
    1.29