Last change
on this file since 223 was
223,
checked in by mulligan, 10 years ago

File for bitvector specific stuff added.

File size:
1.8 KB

Line  

1  (* ===================================== *) 

2  (* Vectors.ma: Fixed length bitvectors, and routine operations on them. *) 

3  (* ===================================== *) 

4  

5  include "logic/pts.ma". 

6  include "basics/eq.ma". 

7  include "basics/bool.ma". 

8  include "arithmetics/nat.ma". 

9  include "nat/plus.ma". 

10  include "nat/minus.ma". 

11  

12  ninductive Vector (A: Type[0]): nat → Type[0] ≝ 

13  Empty: Vector A 0 

14   Cons: ∀n: nat. A → Vector A n → Vector A (n + 1). 

15  

16  nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B) (v: Vector A n) on v ≝ 

17  match v with 

18  [ Empty ⇒ Empty B 

19   Cons n hd tl ⇒ Cons B n (f hd) (map A B n f tl) 

20  ]. 

21  

22  nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat) 

23  (f: A → B → B) (x: B) (v: Vector A n) on v ≝ 

24  match v with 

25  [ Empty ⇒ x 

26   Cons n hd tl ⇒ f hd (fold_right A B n f x tl) 

27  ]. 

28  

29  nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat) 

30  (f: A → B → A) (x: A) (v: Vector B n) on v ≝ 

31  match v with 

32  [ Empty ⇒ x 

33   Cons n hd tl ⇒ f (fold_left A B n f x tl) hd 

34  ]. 

35  

36  nlet rec length (A: Type[0]) (n: nat) (v: Vector A n) on v ≝ 

37  match v with 

38  [ Empty ⇒ 0 

39   Cons n hd tl ⇒ 1 + length A n tl 

40  ]. 

41  

42  (* 

43  nlet rec append (A: Type[0]) (n: nat) (m: nat) 

44  (v: Vector A n) (q: Vector A m) on v ≝ 

45  match v with 

46  [ Empty ⇒ q 

47   Cons n hd tl ⇒ Cons ? n hd (append A n m tl q) 

48  ]. 

49  *) 

50  

51  (* 

52  nlet rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v ≝ 

53  match v with 

54  [ Empty ⇒ Empty A 

55   Cons n hd tl ⇒ append 

56  

57  nlemma length_correct: 

58  ∀A: Type[0]. 

59  ∀n: nat. 

60  ∀v: Vector A n. 

61  length A n v = n. 

62  #A n v; 

63  nelim v. 

64  nnormalize. 

65  @. 

66  #n0 H V H. 

67  nnormalize. 

68  nrewrite > H. 

69  *) 

Note: See
TracBrowser
for help on using the repository browser.