src/HOL/While.thy

+(*  Title:      HOL/While
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   2000 TU Muenchen
+
+Defines a while-combinator "while" and proves
+a) an unrestricted unfolding law (even if while diverges!)
+   (I got this idea from Wolfgang Goerigk)
+b) the invariant rule for reasoning about while
+*)
+
+While = Recdef +
+
+consts while_aux :: "('a => bool) * ('a => 'a) * 'a => 'a"
+recdef while_aux
+ "same_fst (%b. True) (%b. same_fst (%c. True) (%c.
+  {(t,s).  b s & c s = t &
+           ~(? f. f 0 = s & (!i. b(f i) & c(f i) = f(i+1)))}))"
+"while_aux(b,c,s) =
+  (if (? f. f 0 = s & (!i. b(f i) & c(f i) = f(i+1)))
+   then arbitrary
+   else if b s then while_aux(b,c,c s) else s)"
+
+constdefs
+ while :: "('a => bool) => ('a => 'a) => 'a => 'a"
+"while b c s == while_aux(b,c,s)"
+
+end