isabelle: src/HOL/While.thy@33fe2d701ddd (annotated)

9448 755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	1	(* Title: HOL/While
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	2	ID: $Id$
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	3	Author: Tobias Nipkow
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	4	Copyright 2000 TU Muenchen
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	5
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	6	Defines a while-combinator "while" and proves
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	7	a) an unrestricted unfolding law (even if while diverges!)
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	8	(I got this idea from Wolfgang Goerigk)
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	9	b) the invariant rule for reasoning about while
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	10	*)
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	11
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	12	While = Recdef +
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	13
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	14	consts while_aux :: "('a => bool) * ('a => 'a) * 'a => 'a"
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	15	recdef while_aux
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	16	"same_fst (%b. True) (%b. same_fst (%c. True) (%c.
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	17	{(t,s). b s & c s = t &
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	18	~(? f. f 0 = s & (!i. b(f i) & c(f i) = f(i+1)))}))"
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	19	"while_aux(b,c,s) =
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	20	(if (? f. f 0 = s & (!i. b(f i) & c(f i) = f(i+1)))
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	21	then arbitrary
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	22	else if b s then while_aux(b,c,c s) else s)"
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	23
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	24	constdefs
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	25	while :: "('a => bool) => ('a => 'a) => 'a => 'a"
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	26	"while b c s == while_aux(b,c,s)"
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	27
755330e55e18 While functional for defining tail-recursive functions nipkow parents: diff changeset	28	end

author	nipkow
	Thu, 12 Oct 2000 18:38:23 +0200
changeset 10212	33fe2d701ddd
parent 9448	755330e55e18
permissions	-rw-r--r--