# 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 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