src/HOL/Library/Code_Target_Int.thy
changeset 64997 067a6cca39f0
parent 64242 93c6f0da5c70
child 65552 f533820e7248
equal deleted inserted replaced
64996:b316cd527a11 64997:067a6cca39f0
    33   by transfer simp
    33   by transfer simp
    34 
    34 
    35 lemma [code_abbrev]:
    35 lemma [code_abbrev]:
    36   "int_of_integer (- numeral k) = Int.Neg k"
    36   "int_of_integer (- numeral k) = Int.Neg k"
    37   by transfer simp
    37   by transfer simp
    38   
    38 
       
    39 context
       
    40 begin  
       
    41 
       
    42 qualified definition positive :: "num \<Rightarrow> int"
       
    43   where [simp]: "positive = numeral"
       
    44 
       
    45 qualified definition negative :: "num \<Rightarrow> int"
       
    46   where [simp]: "negative = uminus \<circ> numeral"
       
    47 
       
    48 lemma [code_computation_unfold]:
       
    49   "numeral = positive"
       
    50   "Int.Pos = positive"
       
    51   "Int.Neg = negative"
       
    52   by (simp_all add: fun_eq_iff)
       
    53 
       
    54 end
       
    55 
    39 lemma [code, symmetric, code_post]:
    56 lemma [code, symmetric, code_post]:
    40   "0 = int_of_integer 0"
    57   "0 = int_of_integer 0"
    41   by transfer simp
    58   by transfer simp
    42 
    59 
    43 lemma [code, symmetric, code_post]:
    60 lemma [code, symmetric, code_post]: