tuned
authorhaftmann
Tue Jan 15 16:19:21 2008 +0100 (2008-01-15)
changeset 2591882dd239e0f65
parent 25917 d6c920623afc
child 25919 8b1c0d434824
tuned
src/HOL/Library/Code_Index.thy
     1.1 --- a/src/HOL/Library/Code_Index.thy	Tue Jan 15 16:19:20 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Index.thy	Tue Jan 15 16:19:21 2008 +0100
     1.3 @@ -133,6 +133,20 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma index_of_nat_code [code func]:
     1.8 +  "index_of_nat = of_nat"
     1.9 +proof
    1.10 +  fix n :: nat
    1.11 +  have "of_nat n = index_of_nat n"
    1.12 +    by (induct n) simp_all
    1.13 +  then show "index_of_nat n = of_nat n"
    1.14 +    by (rule sym)
    1.15 +qed
    1.16 +
    1.17 +lemma nat_of_index_code [code func]:
    1.18 +  "nat_of_index n = (if n = 0 then 0 else Suc (nat_of_index (n - 1)))"
    1.19 +  by (induct n) simp
    1.20 +
    1.21  
    1.22  subsection {* ML interface *}
    1.23  
    1.24 @@ -148,18 +162,6 @@
    1.25  
    1.26  subsection {* Code serialization *}
    1.27  
    1.28 -text {* Pecularity for operations with potentially negative result *}
    1.29 -
    1.30 -definition
    1.31 -  minus_index' :: "index \<Rightarrow> index \<Rightarrow> index"
    1.32 -where
    1.33 -  [code func del]: "minus_index' = op -"
    1.34 -
    1.35 -lemma minus_index_code [code func]:
    1.36 -  "n - m = (let q = minus_index' n m
    1.37 -    in if q < 0 then 0 else q)"
    1.38 -  by (simp add: minus_index'_def Let_def)
    1.39 -
    1.40  text {* Implementation of indices by bounded integers *}
    1.41  
    1.42  code_type index
    1.43 @@ -171,26 +173,26 @@
    1.44    (Haskell -)
    1.45  
    1.46  setup {*
    1.47 -  fold (fn target => CodeTarget.add_pretty_numeral target true
    1.48 +  fold (fn target => CodeTarget.add_pretty_numeral target false
    1.49      @{const_name number_index_inst.number_of_index}
    1.50 -    @{const_name Numeral.B0} @{const_name Numeral.B1}
    1.51 -    @{const_name Numeral.Pls} @{const_name Numeral.Min}
    1.52 -    @{const_name Numeral.Bit}
    1.53 +    @{const_name Int.B0} @{const_name Int.B1}
    1.54 +    @{const_name Int.Pls} @{const_name Int.Min}
    1.55 +    @{const_name Int.Bit}
    1.56    ) ["SML", "OCaml", "Haskell"]
    1.57  *}
    1.58  
    1.59 -code_reserved SML int
    1.60 -code_reserved OCaml int
    1.61 +code_reserved SML Int int
    1.62 +code_reserved OCaml Pervasives int
    1.63  
    1.64  code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.65    (SML "Int.+ ((_), (_))")
    1.66    (OCaml "Pervasives.+")
    1.67    (Haskell infixl 6 "+")
    1.68  
    1.69 -code_const "minus_index' \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.70 -  (SML "Int.- ((_), (_))")
    1.71 -  (OCaml "Pervasives.-")
    1.72 -  (Haskell infixl 6 "-")
    1.73 +code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.74 +  (SML "Int.max/ (_/ -/ _,/ 0 : int)")
    1.75 +  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
    1.76 +  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
    1.77  
    1.78  code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.79    (SML "Int.* ((_), (_))")
    1.80 @@ -222,7 +224,4 @@
    1.81    (OCaml "Big'_int.mod'_big'_int")
    1.82    (Haskell "mod")
    1.83  
    1.84 -code_reserved SML Int
    1.85 -code_reserved OCaml Pervasives
    1.86 -
    1.87  end