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

problem with induction



Hi!
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.

greetings
Chris
test: THEORY
BEGIN

	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
		ENDIF

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

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

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

END test