monomorphic code generation for power operations
authorhaftmann
Thu May 14 15:09:47 2009 +0200 (2009-05-14)
changeset 3115592d8ff6af82c
parent 31154 f919b8e67413
child 31156 90fed3d4430f
monomorphic code generation for power operations
src/HOL/Nat.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Nat.thy	Thu May 14 15:09:47 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Thu May 14 15:09:47 2009 +0200
     1.3 @@ -1199,7 +1199,7 @@
     1.4  definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
     1.5    funpow_code_def [code post]: "funpow = compow"
     1.6  
     1.7 -lemmas [code inline] = funpow_code_def [symmetric]
     1.8 +lemmas [code unfold] = funpow_code_def [symmetric]
     1.9  
    1.10  lemma [code]:
    1.11    "funpow 0 f = id"
     2.1 --- a/src/HOL/Power.thy	Thu May 14 15:09:47 2009 +0200
     2.2 +++ b/src/HOL/Power.thy	Thu May 14 15:09:47 2009 +0200
     2.3 @@ -452,4 +452,13 @@
     2.4    from power_strict_increasing_iff [OF this] less show ?thesis ..
     2.5  qed
     2.6  
     2.7 +
     2.8 +subsection {* Code generator tweak *}
     2.9 +
    2.10 +lemma power_power_power [code, code unfold, code inline del]:
    2.11 +  "power = power.power (1::'a::{power}) (op *)"
    2.12 +  unfolding power_def power.power_def ..
    2.13 +
    2.14 +declare power.power.simps [code]
    2.15 +
    2.16  end