Oak Examples

list.oak

/#

Axioms and results for lists, including linked lists.

#/

###############################################################################
include "set.oak"
###############################################################################

list_def: axiom define List such that for all l in List,
	length[l] is in N and for all x, x is in l iff
		for some i in N where i >= 1 and i <= length[l], l[i] = x

list_literal: axiom define [] such that for all x,a,b,c,d,e,f,g,
	(if x = [a] then
		x is in List and length[x] = 1 and x[1] = a) and
	(if x = [a,b] then
		x is in List and length[x] = 2 and x[1] = a and x[2] = b) and
	(if x = [a,b,c] then
		x is in List and length[x] = 3 and x[1] = a and x[2] = b and x[3] = c) and
	(if x = [a,b,c,d] then
		x is in List and length[x] = 4 and x[1] = a and x[2] = b and x[3] = c and
		x[4] = d) and
	(if x = [a,b,c,d,e] then
		x is in List and length[x] = 5 and x[1] = a and x[2] = b and x[3] = c and
		x[4] = d and x[5] = e) and
	(if x = [a,b,c,d,e,f] then
		x is in List and length[x] = 6 and x[1] = a and x[2] = b and x[3] = c and
		x[4] = d and x[5] = e and x[6] = f) and
	(if x = [a,b,c,d,e,f,g] then
		x is in List and length[x] = 7 and x[1] = a and x[2] = b and x[3] = c and
		x[4] = d and x[5] = e and x[6] = f and x[7] = g)

###############################################################################

tie-in `l[i] is in l` with
	`if l is in List and i is in N and i >= 1 and i <= length[l]
	 then l[i] is in l`
		for all l,i
			by list_def

tie-in `length[l]` with `if l is in List then length[l] is in N` for all l
	by list_def

first_def: define first such that for all l in List,
	if length[l] >= 1 then first[l] = l[1]
proof
	for all l in List, for at most one x in l, x = l[1]
	so for some op, for all l in List and x in l, op[l] = x iff x = l[1]
		by operation22
	so thesis by list_def
end

second_def: define second such that for all l in List,
	if length[l] >= 2 then second[l] = l[2]
proof
	for all l in List, for at most one x in l, x = l[2]
	so for some op, for all l in List and x in l, op[l] = x iff x = l[2]
		by operation22
	so thesis by list_def,1_less_2
end

third_def: define third such that for all l in List,
	if length[l] >= 3 then third[l] = l[3]
proof
	for all l in List, for at most one x in l, x = l[3]
	so for some op, for all l in List and x in l, op[l] = x iff x = l[3]
		by operation22
	so thesis by list_def,1_less_3
end

last_def: define last such that for all l in List,
	if length[l] >= 1 then last[l] = l[length[l]]
proof
	for all l in List, for at most one x in l, x = l[length[l]]
	so for some op, for all l in List and x in l, op[l] = x iff x = l[length[l]]
		by operation22
	so thesis by list_def
end

3_first: for all a,b,c, first[[a,b,c]] = a
	by list_literal,first_def,1_less_3

3_second: for all a,b,c, second[[a,b,c]] = b
	by list_literal,second_def,2_less_3

3_third: for all a,b,c, third[[a,b,c]] = c by list_literal,third_def

tie-in `[a,b,c]` with
	`first[[a,b,c]] = a and second[[a,b,c]] = b and third[[a,b,c]] = c`
		for all a,b,c
			by 3_first,3_second,3_third

index_def: define indexes such that for all l in List,
	for all i, i is in indexes[l] iff i is in N and i >= 1 and i <= length[l]
proof
	for all l in List, for at most one S in Set,
		for all i, i is in S iff i is in N and i >= 1 and i <= length[l]
			by set_equality
	so op_def: for some op, for all l in List and S in Set, op[l] = S iff
		for all i, i is in S iff i is in N and i >= 1 and i <= length[l]
			by operation22
	take any l in List
		for some p, for all i in N, p[i] iff i >= 1 and i <= length[l]
			by property2a
		so for some S in Set, op[l] = S by specify,op_def
	end
	so thesis by op_def
end

tie-in `i is in indexes[l]` with
	`if l is in List and i is in indexes[l] then i is in N`
		for all i,l
			by index_def

index_prop: for all l in List and x,
 	x is in l iff for some i in indexes[l], l[i] = x
		by list_def,index_def

length_member: for all l in List,
	if for some x, x is in l then length[l] >= 1
		by list_def,total_order

index_plus_one: for all l in List and i in indexes[l],
	if i != length[l] then i+1 is in indexes[l]
proof
	take any l in List and i in indexes[l] where i != length[l]
		so i+1 <= length[l] by index_def,less_equal_one
		i+1 >= 1 by index_def,less_equal_one,ineq_add
		so i+1 is in indexes[l] by index_def
	end
end

# LINKED LISTS ################################################################

define next # make it a variable rather than a constant

linked_list_def: define linked_list such that for all l,
	linked_list[l] iff l is in List and for all i in indexes[l],
		(if i != length[l] then next[l[i]] = l[i+1]) and
		(if i = length[l] then for no j in indexes[l], next[l[i]] = l[j])
	by property2

tie-in `linked_list[l]` with `linked_list[l] implies l is in List` for all l
	by linked_list_def

linked_distinct: for all linked_list l and i,j in indexes[l],
	if i != j then l[i] != l[j]
proof
	take any linked_list l
		P_def: for some P, for all n in N,
					   P[n] iff for all i,j in indexes[l] where i >= n and j >= n,
						   if i < j then l[i] != l[j]
			by property2a
		P[length[l]] by index_def,P_def,total_order
		take t: any n in N where n < length[l]
			suppose hyp: P[n+1]
				take 1: any i,j in indexes[l] where i >= n and j >= n and i < j
					suppose i > n
						so i >= n+1 and j >= n+1 by nat_ineq_2,1
						so l[i] != l[j] by hyp,P_def,1
					end
					suppose 2: i = n
						next[l[i]] = l[i+1] by linked_list_def,t,2
						if j = length[l] then next[l[j]] != l[i+1]
							by linked_list_def,2,t,index_plus_one
						suppose 3: j != length[l]
							i+1 is in indexes[l] and j+1 is in indexes[l]
								by index_plus_one,2,3,t
							so l[i+1] != l[j+1] by hyp,P_def,1,ineq_add
							next[l[j]] = l[j+1] by linked_list_def,3
							so next[l[j]] != l[i+1]
						end
						so l[i] != l[j]
					end
				end
				so P[n] by P_def
			end
		end
		so for all n in N where n <= length[l], P[n] by downward_induction
	 	so P[0] by nat_greater_eq_0
	end
	so thesis by P_def,index_def,total_order,0_less_1
end

next_exists: for all linked_list l and x in l,
	if x != last[l] then next[x] is in l and next[x] != first[l]
proof
	take 0: any linked_list l and x in l where x != last[l]
		1: for some i in indexes[l], l[i] = x by index_prop
		1a: i >= 1 and i < length[l] by index_def,last_def,1,0
		2: i+1 is in indexes[l] by index_def,nat_ineq_2,1a,less_equal_one
		3: next[x] = l[i+1] by linked_list_def,1,1a
		length[l] >= 1 by length_member,0
		so next[x] != first[l]
			by first_def,linked_distinct,3,index_def,2,nat_ineq_2,1a
		next[x] is in l by index_prop,2,3
	end
end

prev_exists: for all linked_list l and y in l,
	if y != first[l] then for some x in l, next[x] = y and x != last[l]
proof
	take any linked_list l and y in l where y != first[l]
		1: for some j in indexes[l], l[j] = y by index_prop
		2: so j > 1 and j <= length[l] by index_def,first_def,1
		3: for some i in N, j = i+1 by 2,0_less_1,nat_reduce
		4: i >= 1 and i < length[l] by 2,less_equal_one,3
		5: i is in indexes[l] by index_def,4
		6: for some x in l, x = l[i] by index_prop,5
		next[x] = y by linked_list_def,1,3,5,4,6
		x != last[l] by linked_list_def,3,4,last_def,6,index_def,length_member
	end
end

succ_def: define succ such that for all linked_list l and x,y,
	succ[l,x,y] iff x is in l and x != last[l] and next[x] = y
proof
	for some p, for all l,x,y,
		p[l,x,y] iff linked_list[l] and x is in l and y is in l and
			(x is in l and x != last[l] and next[x] = y)
				by property122
	so thesis by next_exists
end

succ_exists: for all linked_list l,
	for all x in l where x != last[l],
		for some y in l, succ[l,x,y]
			by succ_def,next_exists

pred_exists: for all linked_list l,
	for all y in l where y != first[l],
		for some x in l, succ[l,x,y]
			by succ_def,prev_exists

succ_not_first_last: for all linked_list l,
	for all x,y in l where succ[l,x,y], x != last[l] and y != first[l]
		by succ_def,next_exists