Theory Loop

Up to index of Isabelle/HOLCF/ex

theory Loop
imports HOLCF
uses [Loop.ML]
begin

(*  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 xb·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 yb·y = TT ∧ g·y ≠ UU --> INV (g·y); ∀y. INV yb·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