[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

problem with induction

I have problems proving the theorem th. Thus I can't prove it, I think I
did a mistake in my specificaton. 
Actually I wanted to build a finite array. The function t was intended
to manipulate the array in the way, that every book which titel doesn't
match the given string, is replaced by the constant none.
Though the functions seem right to me, i can't prove the theorem by
induction or measure-induct. Perhaps it's a totally wrong approach to
the problem, but all I want is to change a finite array.
Hopefully anyone can help me.

test: THEORY

	max: posnat
	range: TYPE = {x: posnat | x <= max}

	book: TYPE = [# id: posnat, titel: string #]
	book_array: TYPE = [range -> book]

	none: book

	b: VAR book
	str: VAR string
	ba: VAR book_array
	i: VAR range	

	low(str, ba, i): nat = i

	chg(str, ba, i): book_array =
		IF ba(i)`titel /= str THEN ba WITH [(i) := none]
		ELSE ba

	rec(str, ba, i): RECURSIVE book_array =
		IF i = 1 THEN chg(str, ba, i)
		ELSE rec(str, chg(str, ba, i), i - 1)

	t(str, ba): book_array =
		rec(str, ba, max)

		ba(i) = b AND b`titel = str IMPLIES t(str, ba)(i) = b

END test