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

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size:
2.2 KB

Line  

1  include "Cartesian.ma". 

2  include "Maybe.ma". 

3  include "Bool.ma". 

4  

5  include "logic/pts.ma". 

6  include "Plogic/equality.ma". 

7  

8  ninductive Nat: Type[0] ≝ 

9  Z: Nat 

10   S: Nat → Nat. 

11  

12  nlet rec plus (n: Nat) (o: Nat) on n ≝ 

13  match n with 

14  [ Z ⇒ o 

15   S p ⇒ S (plus p o) 

16  ]. 

17  

18  notation "n break + m" 

19  right associative with precedence 52 

20  for @{ 'plus $n $m }. 

21  

22  interpretation "Nat plus" 'plus n m = (plus n m). 

23  

24  nlet rec minus (n: Nat) (o: Nat) on n ≝ 

25  match n with 

26  [ Z ⇒ Z 

27   S p ⇒ 

28  match o with 

29  [ Z ⇒ S p 

30   S q ⇒ minus p q 

31  ] 

32  ]. 

33  

34  notation "n break  m" 

35  right associative with precedence 47 

36  for @{ 'minus $n $m }. 

37  

38  interpretation "Nat minus" 'minus n m = (minus n m). 

39  

40  nlet rec multiplication (n: Nat) (o: Nat) on n ≝ 

41  match n with 

42  [ Z ⇒ Z 

43   S p ⇒ o + (multiplication p o) 

44  ]. 

45  

46  notation "n break * m" 

47  right associative with precedence 47 

48  for @{ 'multiplication $n $m }. 

49  

50  interpretation "Nat multiplication" 'times n m = (multiplication n m). 

51  

52  nlemma plus_zero: 

53  ∀n: Nat. 

54  n + Z = n. 

55  #n. 

56  nelim n. 

57  nnormalize. 

58  @. 

59  #N H. 

60  nnormalize. 

61  nrewrite > H. 

62  @. 

63  nqed. 

64  

65  nlemma plus_associative: 

66  ∀m, n, o: Nat. 

67  (m + n) + o = m + (n + o). 

68  #m n o. 

69  nelim m. 

70  nnormalize. 

71  @. 

72  #N H. 

73  nnormalize. 

74  nrewrite > H. 

75  @. 

76  nqed. 

77  

78  nlemma succ_plus: 

79  ∀m, n: Nat. 

80  S(m + n) = m + S(n). 

81  #m n. 

82  nelim m. 

83  nnormalize. 

84  @. 

85  #N H. 

86  nnormalize. 

87  nrewrite > H. 

88  @. 

89  nqed. 

90  

91  nlemma plus_symmetrical: 

92  ∀m, n: Nat. 

93  m + n = n + m. 

94  #m n. 

95  nelim m. 

96  nnormalize. 

97  nelim n. 

98  nnormalize. 

99  @. 

100  #N H. 

101  nnormalize. 

102  nrewrite < H. 

103  @. 

104  #N H. 

105  nnormalize. 

106  nrewrite > H. 

107  napplyS succ_plus. 

108  nqed. 

109  

110  nlemma multiplication_zero: 

111  ∀m: Nat. 

112  m * Z = Z. 

113  #m. 

114  nelim m. 

115  nnormalize. 

116  @. 

117  #N H. 

118  nnormalize. 

119  nrewrite > H. 

120  @. 

121  nqed. 

122  

123  nlemma multiplication_succ: 

124  ∀m, n: Nat. 

125  m * S(n) = m + (m * n). 

126  #m n. 

127  nelim m. 

128  nnormalize. 

129  @. 

130  #N H. 

131  nnormalize. 

132  napplyS plus_symmetrical. 

133  nqed. 

134  

135  nlemma multiplication_symmetrical: 

136  ∀m, n: Nat. 

137  m * n = n * m. 

138  #m n. 

139  nelim m. 

140  nnormalize. 

141  nelim n. 

142  nnormalize. 

143  @. 

144  #N H. 

145  nnormalize. 

146  nrewrite < H. 

147  @. 

148  #N H. 

149  nnormalize. 

150  nrewrite > H. 

151  napplyS multiplication_succ. 

152  nqed. 

153  

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