(* Title: HOLCF/ex/Loop.thy ID: $Id: Loop.thy,v 1.11 2005/09/06 17:28:59 wenzelm Exp $ Author: Franz Regensburger *) header {* Theory for a loop primitive like while *} theory Loop imports HOLCF begin constdefs step :: "('a -> tr)->('a -> 'a)->'a->'a" "step == (LAM b g x. If b$x then g$x else x fi)" while :: "('a -> tr)->('a -> 'a)->'a->'a" "while == (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))" ML {* use_legacy_bindings (the_context ()) *} end
theorem step_def2:
step·b·g·x = If b·x then g·x else x fi
theorem while_def2:
while·b·g = (FIX f. LAM x. If b·x then f·(g·x) else x fi)
theorem while_unfold:
while·b·g·x = If b·x then while·b·g·(g·x) else x fi
theorem while_unfold2:
∀x. while·b·g·x = while·b·g·(iterate k (step·b·g) x)
theorem while_unfold3:
while·b·g·x = while·b·g·(step·b·g·x)
theorem loop_lemma1:
[| ∃y. b·y = FF; iterate k (step·b·g) x = UU |] ==> iterate (Suc k) (step·b·g) x = UU
theorem loop_lemma2:
[| ∃y. b·y = FF; iterate (Suc k) (step·b·g) x ≠ UU |] ==> iterate k (step·b·g) x ≠ UU
theorem loop_lemma3:
[| ∀x. INV x ∧ b·x = TT ∧ g·x ≠ UU --> INV (g·x); ∃y. b·y = FF; INV x; iterate k (step·b·g) x ≠ UU |] ==> INV (iterate k (step·b·g) x)
theorem loop_lemma4:
b·(iterate k (step·b·g) x) = FF ==> while·b·g·x = iterate k (step·b·g) x
theorem loop_lemma5:
∀k. b·(iterate k (step·b·g) x) ≠ FF ==> while·b·g·(iterate m (step·b·g) x) = UU
theorem loop_lemma6:
∀k. b·(iterate k (step·b·g) x) ≠ FF ==> while·b·g·x = UU
theorem loop_lemma7:
while·b·g·x ≠ UU ==> ∃k. b·(iterate k (step·b·g) x) = FF
theorem loop_inv2:
[| ∀y. INV y ∧ b·y = TT ∧ g·y ≠ UU --> INV (g·y); ∀y. INV y ∧ b·y = FF --> Q y; INV x; while·b·g·x ≠ UU |] ==> Q (while·b·g·x)
theorem loop_inv:
[| P x; !!y. P y ==> INV y; !!y. [| INV y; b·y = TT; g·y ≠ UU |] ==> INV (g·y); !!y. [| INV y; b·y = FF |] ==> Q y; while·b·g·x ≠ UU |] ==> Q (while·b·g·x)
theorem loeckx_sieber:
Ifix F = (LUB i. (%G. iterate i G UU)) F
theorem cont_Ifix2':
cont Ifix
theorem fix_lemma1:
(%i. iterate i f UU) = (%j. (LAM f. iterate j f UU)·f)
theorem fix_lemma2:
Ifix = (%f. LUB j. (LAM f. iterate j f UU)·f)
theorem cont_Ifix2'':
cont Ifix