dedicated computation preprocessing rules for nat, int implemented by target language literals
authorhaftmann
Tue Feb 07 22:15:05 2017 +0100 (2017-02-07)
changeset 64997067a6cca39f0
parent 64996 b316cd527a11
child 64998 d51478d6aae4
dedicated computation preprocessing rules for nat, int implemented by target language literals
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Code_Target_Nat.thy
     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
     2.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 07 22:15:04 2017 +0100
     2.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 07 22:15:05 2017 +0100
     2.3 @@ -44,6 +44,19 @@
     2.4    "nat_of_integer (numeral k) = nat_of_num k"
     2.5    by transfer (simp add: nat_of_num_numeral)
     2.6  
     2.7 +context
     2.8 +begin  
     2.9 +
    2.10 +qualified definition natural :: "num \<Rightarrow> nat"
    2.11 +  where [simp]: "natural = nat_of_num"
    2.12 +
    2.13 +lemma [code_computation_unfold]:
    2.14 +  "numeral = natural"
    2.15 +  "nat_of_num = natural"
    2.16 +  by (simp_all add: nat_of_num_numeral)
    2.17 +
    2.18 +end
    2.19 +
    2.20  lemma [code abstract]:
    2.21    "integer_of_nat (nat_of_num n) = integer_of_num n"
    2.22    by transfer (simp add: nat_of_num_numeral)