import Nat
import Base
union Int{
pos(Nat)
negsuc(Nat)
}
fun abs(x : Int) {
switch x {
case pos(n) { n }
case negsuc(n) { suc(n) }
}
}
union Sign {
positive
negative
}
fun sign(n : Int) {
switch n {
case pos(n') { positive }
case negsuc(n') { negative }
}
}
private fun flip(s : Sign) {
switch s {
case positive { negative }
case negative { positive }
}
}
private fun operator*(s1 : Sign, s2 : Sign) {
switch s1 {
case positive { s2 }
case negative { flip(s2) }
}
}
fun operator -(x : Int) {
switch x {
case pos(n) {
switch n {
case zero { pos(zero) }
case suc(n') { negsuc(n') }
}
}
case negsuc(n){ pos(suc(n)) }
}
}
fun operator -(n:Nat) {
- pos(n)
}
private fun operator*(s : Sign, n : Int) {
switch s {
case positive { n }
case negative { -n }
}
}
fun operator*(s : Sign, n : Nat) { s * pos(n) }
fun operator ⊝(x:Nat, y:Nat) {
if x < y then
-(y - x)
else
pos(x - y)
}
fun operator +(x : Int, m :Int) {
switch x {
case pos(n) {
switch m {
case pos(n') { pos(n + n') }
case negsuc(n') { n ⊝ suc(n') }
}
}
case negsuc(n) {
switch m {
case pos(n') { n' ⊝ suc(n) }
case negsuc(n') { negsuc(suc(n + n')) }
}
}
}
}
fun operator + (n:Nat, m:Int) { pos(n) + m }
fun operator + (n:Int, m:Nat) { n + pos(m) }
fun operator - (n:Int, m:Int) { n + (- m) }
fun operator - (n:Nat, m:Int) { pos(n) - m }
fun operator - (n:Int, m:Nat) { n - pos(m) }
fun operator *(x : Int, y : Int) {
(sign(x) * sign(y)) * (abs(x) * abs(y))
}
fun operator * (n:Nat, m:Int) { pos(n) * m }
fun operator * (n:Int, m:Nat) { n * pos(m) }
fun operator / (n:Int, m:Int) {
(sign(n) * sign(m)) * (abs(n) / abs(m))
}
fun operator / (n:Int, m:Nat) {
sign(n) * (abs(n) / m)
}
fun operator ≤(a : Int, y : Int) {
switch a {
case pos(x) {
switch y {
case pos(y') { x ≤ y' }
case negsuc(y') { false }
}
}
case negsuc(x) {
switch y {
case pos(y') { true }
case negsuc(y') { y' ≤ x }
}
}
}
}
lemma sign_pos: all n:Nat. sign(pos(n)) = positive
proof
arbitrary n:Nat
definition sign
end
lemma sign_negsuc: all n:Nat. sign(negsuc(n)) = negative
proof
arbitrary n:Nat
definition sign
end
lemma sign_neg_pos: all n:Nat. sign(-pos(suc(n))) = negative
proof
arbitrary n:Nat
definition {operator-, sign}
end
lemma mult_pos_any: all s:Sign. positive * s = s
proof
arbitrary s:Sign
definition operator*
end
lemma mult_pos_neg: positive * negative = negative
proof
definition operator*
end
lemma mult_neg_pos: negative * positive = negative
proof
definition {operator*, flip}
end
lemma mult_neg_neg: negative * negative = positive
proof
definition {operator*, flip}
end
lemma mult_pos_nat: all n:Nat. positive * n = pos(n)
proof
arbitrary n:Nat
evaluate
end
lemma mult_neg_nat: all n:Nat. negative * n = - pos(n)
proof
arbitrary n:Nat
evaluate
end
lemma abs_pos: all n:Nat. abs(pos(n)) = n
proof
arbitrary n:Nat
definition abs
end
lemma abs_negsuc: all n:Nat. abs(negsuc(n)) = suc(n)
proof
arbitrary n:Nat
definition abs
end
theorem abs_neg: all n:Int. abs(- n) = abs(n)
proof
arbitrary n:Int
switch n {
case pos(n') {
switch n' {
case 0 {
equations
abs(- pos(0))
= 0 by definition {operator-, abs}
... = #abs(pos(0))# by definition abs
}
case suc(n'') {
equations
abs(- pos(suc(n'')))
= suc(n'') by definition {operator-, abs}
... = #abs(pos(suc(n'')))# by definition abs
}
}
}
case negsuc(n') {
equations
abs(- negsuc(n'))
= suc(n') by definition {operator-, abs}
... = #abs(negsuc(n'))# by definition abs
}
}
end
lemma neg_pos: all n:Nat.
- pos(suc(n)) = negsuc(n)
proof
arbitrary n : Nat
definition operator-
end
lemma neg_suc: all n:Nat.
- suc(n) = negsuc(n)
proof
arbitrary n : Nat
switch n {
case 0 {
definition {operator-, operator-}
}
case suc(n') {
definition {operator-, operator-}
}
}
end
theorem neg_involutive: all n:Int. - - n = n
proof
arbitrary n:Int
switch n {
case pos(n') {
switch n' {
case 0 { definition operator- }
case suc(n'') { definition operator- }
}
}
case negsuc(n') { definition operator- }
}
end
theorem int_zero_add: all n:Int.
+0 + n = n
proof
arbitrary n:Int
switch n {
case pos(n') {
evaluate
}
case negsuc(n') {
evaluate
}
}
end
theorem int_add_zero: all n:Int.
n + +0 = n
proof
arbitrary n:Int
switch n {
case pos(n') {
suffices pos(n' + 0) = pos(n') by evaluate
replace add_zero
}
case negsuc(n') {
suffices - suc(n') = negsuc(n') by evaluate
neg_suc
}
}
end
theorem int_add_commute: all x:Int, y:Int. x + y = y + x
proof
arbitrary x:Int, y:Int
switch x {
case pos(x') {
switch y {
case pos(y') {
suffices pos(x' + y') = pos(y' + x') by definition {operator+}
replace add_commute[x',y']
}
case negsuc(y') {
definition operator+
}
}
}
case negsuc(x') {
switch y {
case pos(y') {
definition operator+
}
case negsuc(y') {
suffices negsuc(suc(x' + y')) = negsuc(suc(y' + x'))
by definition operator+
replace add_commute[x', y']
}
}
}
}
end
lemma zero_subo_neg: all n:Nat. 0 ⊝ suc(n) = negsuc(n)
proof
arbitrary n:Nat
definition {operator⊝, operator<, operator≤, operator≤, operator-, operator-}
end
lemma int_subo_zero: all n:Nat. n ⊝ 0 = pos(n)
proof
arbitrary n:Nat
switch n < 0 for operator⊝ {
case true assume n_neg {
conclude false by definition {operator<, operator≤} in n_neg
}
case false assume n_pos {
replace sub_zero
}
}
end
lemma int_subo_cancel: all n:Nat. n ⊝ n = +0
proof
arbitrary n:Nat
switch n < n {
case true assume nn_true {
conclude false by apply less_irreflexive[n] to replace nn_true
}
case false assume nn_false {
suffices pos(n - n) = +0 by definition {operator ⊝} and replace nn_false
replace sub_cancel
}
}
end
lemma subo_sub: all x:Nat, y:Nat. x ⊝ y = pos(x) - pos(y)
proof
arbitrary x:Nat, y:Nat
switch x {
case 0 {
switch y {
case 0 {
evaluate
}
case suc(y') {
evaluate
}
}
}
case suc(x') {
switch y {
case 0 {
suffices pos(suc(x')) = pos(suc(x' + 0)) by evaluate
replace add_zero
}
case suc(y') {
evaluate
}
}
}
}
end
lemma suc_nat_subo: all x:Nat, y:Nat. suc(x) ⊝ suc(y) = x ⊝ y
proof
arbitrary x:Nat, y:Nat
switch x < y for operator ⊝{
case true assume xy_true {
have: x < y by replace xy_true
have: suc(x) < suc(y) by apply less_suc_iff_suc_less to recall (x < y)
definition {operator-} and replace apply eq_true to recall suc(x) < suc(y)
}
case false assume xy_false {
have: not (suc(x) < suc(y)) by {
assume: suc(x) < suc(y)
have: x < y by apply less_suc_iff_suc_less to recall suc(x) < suc(y)
replace xy_false in recall x < y
}
definition operator - and replace apply eq_false to recall (not (suc(x) < suc(y)))
}
}
end
lemma distrib_left_sub_add: all m:Nat, n:Nat, o:Nat.
(n ⊝ o) + pos(m) = (n + m) ⊝ o
proof
arbitrary m:Nat
induction Nat
case 0 {
arbitrary o:Nat
switch o {
case 0 {
suffices pos(m) = pos(m - 0) by evaluate
replace sub_zero
}
case suc(o') {
suffices negsuc(o') + pos(m) = m ⊝ suc(o') by replace zero_subo_neg | zero_add
definition {operator+}
}
}
}
case suc(n') assume IH {
arbitrary o:Nat
switch o {
case 0 {
suffices pos(suc(n') + m) = pos(suc(n' + m))
by definition {operator+} and replace int_subo_zero
definition operator+
}
case suc(o') {
suffices (n' ⊝ o') + pos(m) = (n' + m) ⊝ o'
by replace suc_add | suc_nat_subo
IH
}
}
}
end
lemma distrib_left_sub_add_neg: all m:Nat, n:Nat, o:Nat.
(n ⊝ o) + negsuc(m) = n ⊝ (suc(o) + m)
proof
arbitrary m:Nat
induction Nat
case 0 {
arbitrary o:Nat
switch o {
case 0 {
evaluate
}
case suc(o') {
suffices negsuc(o') + negsuc(m) = negsuc(suc(o' + m))
by replace suc_add | zero_subo_neg | suc_add
definition {operator+}
}
}
}
case suc(n') assume IH {
arbitrary o:Nat
switch o {
case 0 {
definition {operator+} and replace int_subo_zero | zero_add
}
case suc(o') {
suffices (n' ⊝ o') + negsuc(m) = n' ⊝ (suc(o') + m)
by replace suc_nat_subo | suc_add | suc_nat_subo
IH
}
}
}
end
theorem add_commute_nat_int: all x:Nat, y:Int.
x + y = y + x
proof
arbitrary x:Nat, y:Int
switch y {
case pos(y') {
definition {operator+, operator+} and replace add_commute[x,y']
}
case negsuc(y') {
definition {operator+, operator+}
}
}
end
lemma distrib_right_sub_add: all m:Nat, n:Nat, o:Nat.
pos(m) + (n ⊝ o) = (m + n) ⊝ o
proof
arbitrary m:Nat, n:Nat, o:Nat
equations
pos(m) + (n ⊝ o)
= (n ⊝ o) + pos(m) by int_add_commute
... = (n + m) ⊝ o by distrib_left_sub_add
... = (m + n) ⊝ o by replace add_commute
end
lemma distrib_right_sub_add_neg: all m:Nat, n:Nat, o:Nat.
negsuc(m) + (n ⊝ o) = n ⊝ suc(m + o)
proof
arbitrary m:Nat, n:Nat, o:Nat
equations
negsuc(m) + (n ⊝ o)
= (n ⊝ o) + negsuc(m) by int_add_commute
... = n ⊝ (suc(o) + m) by distrib_left_sub_add_neg[m,n,o]
... = n ⊝ suc(m + o) by replace suc_add | add_commute[o,m]
end
theorem int_add_assoc: all x:Int, y:Int, z:Int. (x + y) + z = x + (y + z)
proof
arbitrary x:Int, y:Int, z:Int
switch x {
case pos(x') {
switch y {
case pos(y') {
switch z {
case pos(z') {
suffices pos((x' + y') + z') = pos(x' + (y' + z'))
by definition {operator+}
.
}
case negsuc(z') {
equations
(pos(x') + pos(y')) + negsuc(z')
= (x' + y') ⊝ suc(z') by definition operator+
... = pos(x') + (y' ⊝ suc(z')) by symmetric distrib_right_sub_add
... = pos(x') + #pos(y') + negsuc(z')# by definition operator+
}
}
}
case negsuc(y') {
switch z {
case pos(z') {
equations
(pos(x') + negsuc(y')) + pos(z')
= (x' ⊝ suc(y')) + pos(z') by evaluate
... = (x' + z') ⊝ suc(y') by distrib_left_sub_add
... = pos(x') + (z' ⊝ suc(y')) by symmetric distrib_right_sub_add
... = pos(x') + #(negsuc(y') + pos(z'))# by definition operator+
}
case negsuc(z') {
equations
(pos(x') + negsuc(y')) + negsuc(z')
= (x' ⊝ suc(y')) + negsuc(z') by evaluate
... = negsuc(z') + (x' ⊝ suc(y')) by int_add_commute
... = x' ⊝ suc(z' + suc(y')) by distrib_right_sub_add_neg
... = x' ⊝ suc(suc(y' + z')) by replace add_suc | add_commute[z',y']
... = #pos(x') + (negsuc(y') + negsuc(z'))# by definition operator+
}
}
}
}
}
case negsuc(x') {
switch y {
case pos(y') {
switch z {
case pos(z') {
equations
(negsuc(x') + pos(y')) + pos(z')
= (y' ⊝ suc(x')) + pos(z') by evaluate
... = (y' + z') ⊝ suc(x') by distrib_left_sub_add
... = #negsuc(x') + (pos(y') + pos(z'))# by definition operator+
}
case negsuc(z') {
equations
(negsuc(x') + pos(y')) + negsuc(z')
= (y' ⊝ suc(x')) + negsuc(z') by evaluate
... = y' ⊝ (suc(suc(x')) + z') by distrib_left_sub_add_neg
... = y' ⊝ suc(suc(x' + z')) by definition {operator+, operator+}
... = y' ⊝ suc(suc(z' + x')) by replace add_commute
... = y' ⊝ #suc(suc(z')) + x'# by definition {operator+, operator+}
... = (y' ⊝ suc(z')) + negsuc(x') by symmetric distrib_left_sub_add_neg
... = negsuc(x') + (y' ⊝ suc(z')) by int_add_commute
... = negsuc(x') + #pos(y') + negsuc(z')# by definition operator+
}
}
}
case negsuc(y') {
switch z {
case pos(z') {
equations
(negsuc(x') + negsuc(y')) + pos(z')
= z' ⊝ suc(suc(x' + y')) by definition operator+
... = z' ⊝ suc(suc(y' + x')) by replace add_commute
... = z' ⊝ #suc(suc(y')) + x'# by definition {operator+, operator+}
... = (z' ⊝ suc(y')) + negsuc(x') by symmetric distrib_left_sub_add_neg
... = negsuc(x') + (z' ⊝ suc(y')) by int_add_commute
... = negsuc(x') + #negsuc(y') + pos(z')# by definition operator+
}
case negsuc(z') {
equations
(negsuc(x') + negsuc(y')) + negsuc(z')
= negsuc(suc(suc(x' + y') + z')) by definition operator+
... = negsuc(suc(suc((x' + y') + z'))) by definition operator+
... = negsuc(suc(x' + suc(y' + z'))) by replace symmetric add_suc[x',y'+z']
... = #negsuc(x') + (negsuc(y') + negsuc(z'))# by definition operator+
}
}
}
}
}
}
end
associative operator+ in Int
theorem int_add_inverse: all x:Int. x + -x = +0
proof
arbitrary x:Int
switch x {
case pos(x') {
switch x' {
case 0 {
definition {operator-, operator+, operator+}
}
case suc(x'') {
suffices suc(x'') ⊝ suc(x'') = +0 by definition {operator-, operator+}
int_subo_cancel
}
}
}
case negsuc(x') {
suffices suc(x') ⊝ suc(x') = +0 by definition {operator-, operator+}
int_subo_cancel
}
}
end
lemma neg_nat: all x:Nat. -x = -pos(x)
proof
arbitrary x:Nat
evaluate
end
lemma neg_subo: all x:Nat, y:Nat. - (x ⊝ y) = y ⊝ x
proof
arbitrary x:Nat, y:Nat
cases trichotomy[x,y]
case: x < y {
have: not (y < x) by apply less_implies_not_greater to (recall x < y)
suffices - (- (y - x)) = pos(y - x)
by definition {operator ⊝}
and replace (apply eq_false to recall not (y < x)) |
(apply eq_true to recall x < y)
replace neg_nat | neg_involutive
}
case: x = y {
suffices - (y ⊝ y) = y ⊝ y by replace recall x = y
suffices - +0 = +0 by replace int_subo_cancel
definition operator-
}
case: y < x {
have: not (x < y) by apply less_implies_not_greater to recall y < x
suffices - pos(x - y) = - (x - y)
by definition operator⊝ and replace (apply eq_true to recall y < x)
| (apply eq_false to recall not (x < y))
definition {operator-, operator-}
}
end
theorem neg_distr_add: all x:Int, y:Int. -(x + y) = (- x) + (- y)
proof
arbitrary x:Int, y:Int
switch x {
case pos(x') {
switch x' {
case 0 {
equations
-(+0 + y)
= -y by replace int_zero_add
... = +0 + -y by symmetric int_zero_add
... = #- +0# + -y by definition operator-
}
case suc(x'') {
switch y {
case pos(y') {
switch y' {
case 0 {
definition {operator+, operator-} and replace add_zero | zero_subo_neg
}
case suc(y'') {
suffices negsuc(x'' + suc(y'')) = negsuc(suc(x'' + y''))
by definition {operator-, operator+, operator+}
replace add_suc
}
}
}
case negsuc(y') {
suffices - (suc(x'') ⊝ suc(y')) = suc(y') ⊝ suc(x'')
by evaluate
suffices - (x'' ⊝ y') = y' ⊝ x'' by replace suc_nat_subo
neg_subo
}
}
}
}
}
case negsuc(x') {
switch y {
case pos(y') {
suffices - (y' ⊝ suc(x')) = - negsuc(x') + - pos(y') by evaluate
equations
- (y' ⊝ suc(x'))
= suc(x') ⊝ y' by neg_subo
... = pos(suc(x')) - pos(y') by subo_sub
... = pos(suc(x')) + - pos(y') by definition operator-
... = #- negsuc(x')# + - pos(y') by definition operator-
}
case negsuc(y') {
suffices pos(suc(suc(x' + y'))) = pos(suc(x') + suc(y'))
by definition {operator+, operator-}
definition operator + and replace add_suc
}
}
}
}
end
theorem int_sub_cancel: all x:Int. x - x = +0
proof
arbitrary x:Int
suffices x + (- x) = +0 by definition operator-
int_add_inverse
end
theorem int_one_mult: all x:Int. +1 * x = x
proof
arbitrary x:Int
switch x {
case pos(x') {
suffices pos(x' + 0) = pos(x') by evaluate
replace add_zero
}
case negsuc(x') {
suffices negsuc(x' + 0) = negsuc(x') by evaluate
replace add_zero
}
}
end
theorem int_zero_mult: all x:Int. +0 * x = +0
proof
arbitrary x:Int
switch x {
case pos(x') { evaluate }
case negsuc(x') { evaluate }
}
end
theorem int_mult_commute: all x:Int, y:Int. x * y = y * x
proof
arbitrary x:Int, y:Int
switch x {
case pos(x') {
switch y {
case pos(y') {
suffices pos(x' * y') = pos(y' * x') by evaluate
replace mult_commute[x',y']
}
case negsuc(y') {
suffices - (x' * suc(y')) = - (suc(y') * x') by evaluate
replace mult_commute[x',suc(y')]
}
}
}
case negsuc(x') {
switch y {
case pos(y') {
suffices - (suc(x') * y') = - (y' * suc(x')) by evaluate
replace mult_commute[suc(x'), y']
}
case negsuc(y') {
suffices pos(suc(x') * suc(y')) = pos(suc(y') * suc(x')) by evaluate
replace mult_commute[suc(x'), suc(y')]
}
}
}
}
end
theorem int_mult_one: all x:Int. x * +1 = x
proof
arbitrary x:Int
equations
x * +1
= +1 * x by int_mult_commute
... = x by int_one_mult
end
theorem int_mult_zero: all x:Int. x * +0 = +0
proof
arbitrary x:Int
equations
x * +0
= +0 * x by int_mult_commute
... = +0 by int_zero_mult
end
lemma mult_assoc_helper: all x:Nat, y:Nat, z:Nat.
z + (y + x * suc(y)) * suc(z)
= (z + y * suc(z)) + x * suc(z + y * suc(z))
proof
arbitrary x:Nat, y:Nat, z:Nat
equations
z + (y + x * suc(y)) * suc(z)
= z + (y + x * (1 + y)) * (1 + z)
by replace suc_one_add[y] | suc_one_add[z]
... = z + (y + x * 1 + x * y) * (1 + z)
by replace dist_mult_add[x]
... = z + (y + x + x * y) * (1 + z)
by replace mult_one
... = z + (y + x + x * y) * 1 + (y + x + x * y) * z
by replace dist_mult_add
... = z + y + x + x * y + (y + x + x * y) * z
by replace mult_one
... = z + y + x + x * y + y*z + x*z + x*y*z
by replace dist_mult_add_right
... = z + y + x + y*z + x*y + x*z + x*y*z
by replace add_commute[x*y, y*z]
... = z + y + x + y*z + x*z + x*y + x*y*z
by replace add_commute[x*y]
... = z + y + y*z + x + x*z + x*y + x*y*z
by replace add_commute[x]
... = #(z + y * suc(z)) + x * suc(z + y * suc(z))#
by replace suc_one_add[(z + y * suc(z))] | suc_one_add[z]
| dist_mult_add | mult_one
end
theorem int_mult_assoc: all x:Int, y:Int, z:Int. (x * y) * z = x * (y * z)
proof
arbitrary x:Int, y:Int, z:Int
switch x {
case pos(x') {
switch x' {
case 0 { replace int_zero_mult | int_zero_mult }
case suc(x'') {
switch y {
case pos(y') {
switch y' {
case 0 { replace int_mult_zero | int_zero_mult | int_mult_zero }
case suc(y'') {
switch z {
case pos(z') {
switch z' {
case 0 { replace int_mult_zero | int_mult_zero }
case suc(z'') {
suffices pos(suc(z'' + (y'' + x'' * suc(y'')) * suc(z'')))
= pos(suc((z'' + y'' * suc(z''))
+ x'' * suc(z'' + y'' * suc(z''))))
by evaluate
replace mult_assoc_helper[x'',y'',z'']
}
}
}
case negsuc(z'') {
suffices negsuc(z'' + (y'' + x'' * suc(y'')) * suc(z''))
= negsuc((z'' + y'' * suc(z'')) + x''*suc(z'' + y''*suc(z'')))
by evaluate
replace mult_assoc_helper[x'',y'',z'']
}
}
}
}
}
case negsuc(y') {
switch z {
case pos(z') {
switch z' {
case 0 { replace int_mult_zero | int_mult_zero }
case suc(z'') {
suffices ─ by definition {operator*} and
replace sign_pos | sign_negsuc | mult_pos_neg
| abs_pos | abs_negsuc | mult_neg_nat | mult_pos_any
| suc_mult | suc_add | neg_pos | sign_negsuc
| mult_neg_nat | mult_neg_pos | abs_negsuc | mult_neg_nat
| neg_pos | sign_negsuc | mult_neg_nat | abs_neg
| suc_mult | abs_pos | suc_add | suc_add
replace mult_assoc_helper[x'',y',z'']
}
}
}
case negsuc(z'') {
suffices ─ by definition operator* and
replace sign_pos | sign_negsuc | abs_pos | abs_negsuc
| mult_pos_neg | mult_neg_nat | suc_mult | suc_add
| neg_pos | sign_negsuc | abs_negsuc | mult_neg_neg
| mult_pos_nat | sign_pos | abs_pos | mult_pos_any
| mult_pos_nat | suc_add | suc_add | suc_mult | suc_add | suc_add
replace mult_assoc_helper[x'',y',z'']
}
}
}
}
}
}
}
case negsuc(x') {
switch y {
case pos(y') {
switch y' {
case 0 { replace int_mult_zero | int_zero_mult | int_mult_zero }
case suc(y'') {
switch z {
case pos(z') {
switch z' {
case 0 { replace int_mult_zero | int_mult_zero }
case suc(z'') {
suffices negsuc(z'' + (y'' + x' * suc(y'')) * suc(z'')) = negsuc((z'' + y'' * suc(z'')) + x' * suc(z'' + y'' * suc(z'')))
by evaluate
replace mult_assoc_helper[x',y'',z'']
}
}
}
case negsuc(z'') {
suffices pos(suc(z'' + (y'' + x' * suc(y'')) * suc(z''))) = pos(suc((z'' + y'' * suc(z'')) + x' * suc(z'' + y'' * suc(z''))))
by evaluate
replace mult_assoc_helper[x',y'',z'']
}
}
}
}
}
case negsuc(y') {
switch z {
case pos(z') {
switch z' {
case 0 { replace int_mult_zero | int_mult_zero }
case suc(z'') {
suffices pos(suc(z'' + (y' + x' * suc(y')) * suc(z''))) = pos(suc((z'' + y' * suc(z'')) + x' * suc(z'' + y' * suc(z'')))) by evaluate
replace mult_assoc_helper[x',y',z'']
}
}
}
case negsuc(z'') {
suffices negsuc(z'' + (y' + x' * suc(y')) * suc(z'')) = negsuc((z'' + y' * suc(z'')) + x' * suc(z'' + y' * suc(z'')))
by evaluate
replace mult_assoc_helper[x',y',z'']
}
}
}
}
}
}
end
associative operator* in Int
theorem int_less_equal_refl: all n:Int. n ≤ n
proof
arbitrary n:Int
switch n {
case pos(n') {
suffices n' ≤ n' by definition operator≤
less_equal_refl
}
case negsuc(n') {
suffices n' ≤ n' by definition operator≤
less_equal_refl
}
}
end
theorem int_less_equal_trans: all m:Int, n:Int, o:Int.
if m ≤ n and n ≤ o then m ≤ o
proof
arbitrary m:Int, n:Int, o:Int
switch m {
case pos(m') {
switch n {
case pos(n') {
switch o {
case pos(o') {
suffices (if (m' ≤ n' and n' ≤ o') then m' ≤ o') by definition operator≤
less_equal_trans
}
case negsuc(o') { definition operator≤ }
}
}
case negsuc(n') { definition operator≤ }
}
}
case negsuc(m') {
switch n {
case pos(n') {
switch o {
case pos(o') { definition operator≤ }
case negsuc(o') { definition operator≤ }
}
}
case negsuc(n') {
switch o {
case pos(o') { definition operator≤ }
case negsuc(o') {
suffices (if (n' ≤ m' and o' ≤ n') then o' ≤ m') by definition operator≤
assume nm_n_on
apply less_equal_trans[o',n',m'] to nm_n_on
}
}
}
}
}
}
end
theorem int_less_equal_antisymmetric:
all x:Int, y:Int.
if x ≤ y and y ≤ x
then x = y
proof
arbitrary x:Int, y:Int
assume xy_n_yx
switch x {
case pos(x') assume x_pos {
switch y {
case pos(y') assume y_pos {
have: x' ≤ y' and y' ≤ x' by definition operator≤ in replace x_pos | y_pos in xy_n_yx
have: x' = y' by apply less_equal_antisymmetric to (recall x' ≤ y' and y' ≤ x')
conclude pos(x') = pos(y') by replace (recall x' = y')
}
case negsuc(y') assume y_neg {
conclude false by definition operator≤ in replace x_pos | y_neg in xy_n_yx
}
}
}
case negsuc(x') assume x_neg {
switch y {
case pos(y') assume y_pos {
conclude false by definition operator≤ in replace x_neg | y_pos in xy_n_yx
}
case negsuc(y') assume y_neg {
have: x' ≤ y' and y' ≤ x' by definition operator≤ in replace x_neg | y_neg in xy_n_yx
have: x' = y' by apply less_equal_antisymmetric to (recall x' ≤ y' and y' ≤ x')
conclude negsuc(x') = negsuc(y') by replace (recall x' = y')
}
}
}
}
end