src/HOL/Code_Evaluation.thy
changeset 40883 b37dca06477f
parent 40638 6b137c96df07
child 40884 3113fd4810bd
     1.1 --- a/src/HOL/Code_Evaluation.thy	Thu Dec 02 08:34:23 2010 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Thu Dec 02 13:53:36 2010 +0100
     1.3 @@ -138,30 +138,39 @@
     1.4  
     1.5  subsubsection {* Numeric types *}
     1.6  
     1.7 -definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
     1.8 -  "term_of_num two = (\<lambda>_. dummy_term)"
     1.9 +definition term_of_num_semiring :: "'a\<Colon>semiring_div \<Rightarrow> 'a \<Rightarrow> term" where
    1.10 +  "term_of_num_semiring two = (\<lambda>_. dummy_term)"
    1.11  
    1.12 -lemma (in term_syntax) term_of_num_code [code]:
    1.13 -  "term_of_num two k = (if k = 0 then termify Int.Pls
    1.14 +lemma (in term_syntax) term_of_num_semiring_code [code]:
    1.15 +  "term_of_num_semiring two k = (if k = 0 then termify Int.Pls
    1.16      else (if k mod two = 0
    1.17 -      then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
    1.18 -      else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
    1.19 -  by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
    1.20 +      then termify Int.Bit0 <\<cdot>> term_of_num_semiring two (k div two)
    1.21 +      else termify Int.Bit1 <\<cdot>> term_of_num_semiring two (k div two)))"
    1.22 +  by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def Let_def)
    1.23  
    1.24  lemma (in term_syntax) term_of_nat_code [code]:
    1.25 -  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
    1.26 -  by (simp only: term_of_anything)
    1.27 -
    1.28 -lemma (in term_syntax) term_of_int_code [code]:
    1.29 -  "term_of (k::int) = (if k = 0 then termify (0 :: int)
    1.30 -    else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
    1.31 -      else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
    1.32 +  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n"
    1.33    by (simp only: term_of_anything)
    1.34  
    1.35  lemma (in term_syntax) term_of_code_numeral_code [code]:
    1.36    "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
    1.37    by (simp only: term_of_anything)
    1.38  
    1.39 +definition term_of_num_ring :: "'a\<Colon>ring_div \<Rightarrow> 'a \<Rightarrow> term" where
    1.40 +  "term_of_num_ring two = (\<lambda>_. dummy_term)"
    1.41 +
    1.42 +lemma (in term_syntax) term_of_num_ring_code [code]:
    1.43 +  "term_of_num_ring two k = (if k = 0 then termify Int.Pls
    1.44 +    else if k = -1 then termify Int.Min
    1.45 +    else if k mod two = 0 then termify Int.Bit0 <\<cdot>> term_of_num_ring two (k div two)
    1.46 +    else termify Int.Bit1 <\<cdot>> term_of_num_ring two (k div two))"
    1.47 +  by (auto simp add: term_of_anything Const_def App_def term_of_num_ring_def Let_def)
    1.48 +
    1.49 +lemma (in term_syntax) term_of_int_code [code]:
    1.50 +  "term_of (k::int) = (if k = 0 then termify (0 :: int)
    1.51 +    else termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num_ring (2::int) k)"
    1.52 +  by (simp only: term_of_anything)
    1.53 +
    1.54  
    1.55  subsubsection {* Obfuscation *}
    1.56  
    1.57 @@ -188,6 +197,6 @@
    1.58  
    1.59  
    1.60  hide_const dummy_term valapp
    1.61 -hide_const (open) Const App Abs termify valtermify term_of term_of_num tracing
    1.62 +hide_const (open) Const App Abs termify valtermify term_of term_of_num_semiring term_of_num_ring tracing
    1.63  
    1.64  end