IArray ignorant of particular representation of nat
authorhaftmann
Wed Feb 13 13:38:52 2013 +0100 (2013-02-13)
changeset 5109484b03c49c223
parent 51093 9d7aa2bb097b
child 51095 7ae79f2e3cc7
IArray ignorant of particular representation of nat
src/HOL/Library/IArray.thy
src/HOL/ex/IArray_Examples.thy
     1.1 --- a/src/HOL/Library/IArray.thy	Wed Feb 13 13:38:52 2013 +0100
     1.2 +++ b/src/HOL/Library/IArray.thy	Wed Feb 13 13:38:52 2013 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  header "Immutable Arrays with Code Generation"
     1.5  
     1.6  theory IArray
     1.7 -imports "~~/src/HOL/Library/Efficient_Nat"
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  text{* Immutable arrays are lists wrapped up in an additional constructor.
    1.12 @@ -15,39 +15,69 @@
    1.13  
    1.14  datatype 'a iarray = IArray "'a list"
    1.15  
    1.16 -fun of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
    1.17 -"of_fun f n = IArray (map f [0..<n])"
    1.18 -hide_const (open) of_fun
    1.19 -
    1.20 -fun length :: "'a iarray \<Rightarrow> nat" where
    1.21 -"length (IArray xs) = List.length xs"
    1.22 -hide_const (open) length
    1.23 -
    1.24 -fun sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
    1.25 -"(IArray as) !! n = as!n"
    1.26 -hide_const (open) sub
    1.27 -
    1.28 -fun list_of :: "'a iarray \<Rightarrow> 'a list" where
    1.29 +primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
    1.30  "list_of (IArray xs) = xs"
    1.31  hide_const (open) list_of
    1.32  
    1.33 +definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
    1.34 +[simp]: "of_fun f n = IArray (map f [0..<n])"
    1.35 +hide_const (open) of_fun
    1.36 +
    1.37 +definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
    1.38 +[simp]: "as !! n = IArray.list_of as ! n"
    1.39 +hide_const (open) sub
    1.40 +
    1.41 +definition length :: "'a iarray \<Rightarrow> nat" where
    1.42 +[simp]: "length as = List.length (IArray.list_of as)"
    1.43 +hide_const (open) length
    1.44 +
    1.45 +lemma list_of_code [code]:
    1.46 +"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
    1.47 +by (cases as) (simp add: map_nth)
    1.48 +
    1.49  
    1.50  subsection "Code Generation"
    1.51  
    1.52 +code_reserved SML Vector
    1.53 +
    1.54  code_type iarray
    1.55    (SML "_ Vector.vector")
    1.56  
    1.57  code_const IArray
    1.58    (SML "Vector.fromList")
    1.59 -code_const IArray.sub
    1.60 -  (SML "Vector.sub(_,_)")
    1.61 -code_const IArray.length
    1.62 +
    1.63 +primrec tabulate :: "code_numeral \<times> (code_numeral \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
    1.64 +"tabulate (n, f) = IArray (map (f \<circ> Code_Numeral.of_nat) [0..<Code_Numeral.nat_of n])"
    1.65 +hide_const (open) tabulate
    1.66 +
    1.67 +lemma [code]:
    1.68 +"IArray.of_fun f n = IArray.tabulate (Code_Numeral.of_nat n, f \<circ> Code_Numeral.nat_of)"
    1.69 +by simp 
    1.70 +
    1.71 +code_const IArray.tabulate
    1.72 +  (SML "Vector.tabulate")
    1.73 +
    1.74 +primrec sub' :: "'a iarray \<times> code_numeral \<Rightarrow> 'a" where
    1.75 +"sub' (as, n) = IArray.list_of as ! Code_Numeral.nat_of n"
    1.76 +hide_const (open) sub'
    1.77 +
    1.78 +lemma [code]:
    1.79 +"as !! n = IArray.sub' (as, Code_Numeral.of_nat n)"
    1.80 +by simp
    1.81 +
    1.82 +code_const IArray.sub'
    1.83 +  (SML "Vector.sub")
    1.84 +
    1.85 +definition length' :: "'a iarray \<Rightarrow> code_numeral" where
    1.86 +[simp]: "length' as = Code_Numeral.of_nat (List.length (IArray.list_of as))"
    1.87 +hide_const (open) length'
    1.88 +
    1.89 +lemma [code]:
    1.90 +"IArray.length as = Code_Numeral.nat_of (IArray.length' as)"
    1.91 +by simp
    1.92 +
    1.93 +code_const IArray.length'
    1.94    (SML "Vector.length")
    1.95 -code_const IArray.of_fun
    1.96 -  (SML "!(fn f => fn n => Vector.tabulate(n,f))")
    1.97 -
    1.98 -lemma list_of_code[code]:
    1.99 -  "IArray.list_of A = map (%n. A!!n) [0..< IArray.length A]"
   1.100 -by (cases A) (simp add: map_nth)
   1.101  
   1.102  end
   1.103 +
     2.1 --- a/src/HOL/ex/IArray_Examples.thy	Wed Feb 13 13:38:52 2013 +0100
     2.2 +++ b/src/HOL/ex/IArray_Examples.thy	Wed Feb 13 13:38:52 2013 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  theory IArray_Examples
     2.5 -imports "~~/src/HOL/Library/IArray"
     2.6 +imports "~~/src/HOL/Library/IArray" "~~/src/HOL/Library/Efficient_Nat"
     2.7  begin
     2.8  
     2.9  lemma "IArray [True,False] !! 1 = False"
    2.10 @@ -24,3 +24,4 @@
    2.11  by eval
    2.12  
    2.13  end
    2.14 +