# Theory Hoare

Up to index of Isabelle/HOLCF/ex

theory Hoare
imports HOLCF
uses [Hoare.ML]
begin

    (*  Title:      HOLCF/ex/hoare.thy
        ID:         $Id: Hoare.thy,v 1.10 2005/09/06 17:28:59 wenzelm Exp $
        Author:     Franz Regensburger

    Theory for an example by C.A.R. Hoare

    p x = if b1 x
             then p (g x)
             else x fi

    q x = if b1 x orelse b2 x
             then q (g x)
             else x fi

    Prove: for all b1 b2 g .
                q o p  = q

    In order to get a nice notation we fix the functions b1,b2 and g in the
    signature of this example

    *)

    theory Hoare
    imports HOLCF
    begin

    consts
      b1 :: "'a -> tr"
      b2 :: "'a -> tr"
      g :: "'a -> 'a"
      p :: "'a -> 'a"
      q :: "'a -> 'a"

    defs
      p_def:  "p == fix$(LAM f. LAM x.
                     If b1$x then f$(g$x) else x fi)"

      q_def:  "q == fix$(LAM f. LAM x.
                     If b1$x orelse b2$x then f$(g$x) else x fi)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem hoare_lemma2:

      b ≠ TT ==> b = FF ∨ b = UU

theorem hoare_lemma3:

      (∀k. b1·(iterate k g x) = TT) ∨ (∃k. b1·(iterate k g x) ≠ TT)

theorem hoare_lemma4:

      ∃k. b1·(iterate k g x) ≠ TT
      ==> ∃k. b1·(iterate k g x) = FF ∨ b1·(iterate k g x) = UU

theorem hoare_lemma5:

      [| ∃k. b1·(iterate k g x) ≠ TT; k = (LEAST n. b1·(iterate n g x) ≠ TT) |]
      ==> b1·(iterate k g x) = FF ∨ b1·(iterate k g x) = UU

theorem hoare_lemma6:

      b = UU ==> b ≠ TT

theorem hoare_lemma7:

      b = FF ==> b ≠ TT

theorem hoare_lemma8:

      [| ∃k. b1·(iterate k g x) ≠ TT; k = (LEAST n. b1·(iterate n g x) ≠ TT) |]
      ==> ∀m<k. b1·(iterate m g x) = TT

theorem hoare_lemma28:

      f·y = UU ==> f·UU = UU

theorem p_def3:

      p·x = If b1·x then p·(g·x) else x fi

theorem q_def3:

      q·x = If b1·x orelse b2·x then q·(g·x) else x fi

theorem hoare_lemma9:

      (∀m<Suc k. b1·(iterate m g x) = TT) --> p·(iterate k g x) = p·x

theorem hoare_lemma24:

      (∀m<Suc k. b1·(iterate m g x) = TT) --> q·(iterate k g x) = q·x

theorem hoare_lemma11:

      ∃n. b1·(iterate n g x) ≠ TT
      ==> k = (LEAST n. b1·(iterate n g x) ≠ TT) ∧ b1·(iterate k g x) = FF -->
          p·x = iterate k g x

theorem hoare_lemma12:

      ∃n. b1·(iterate n g x) ≠ TT
      ==> k = (LEAST n. b1·(iterate n g x) ≠ TT) ∧ b1·(iterate k g x) = UU -->
          p·x = UU

theorem fernpass_lemma:

      ∀k. b1·(iterate k g x) = TT ==> ∀k. p·(iterate k g x) = UU

theorem hoare_lemma16:

      ∀k. b1·(iterate k g x) = TT ==> p·x = UU

theorem hoare_lemma17:

      ∀k. b1·(iterate k g x) = TT ==> ∀k. q·(iterate k g x) = UU

theorem hoare_lemma18:

      ∀k. b1·(iterate k g x) = TT ==> q·x = UU

theorem hoare_lemma19:

      ∀k. b1·(iterate k g x) = TT ==> b1·UU = UU ∨ (∀y. b1·y = TT)

theorem hoare_lemma20:

      ∀y. b1·y = TT ==> ∀k. q·(iterate k g x) = UU

theorem hoare_lemma21:

      ∀y. b1·y = TT ==> q·x = UU

theorem hoare_lemma22:

      b1·UU = UU ==> q·UU = UU

theorem hoare_lemma26:

      ∃n. b1·(iterate n g x) ≠ TT
      ==> k = (LEAST n. b1·(iterate n g x) ≠ TT) ∧ b1·(iterate k g x) = FF -->
          q·x = q·(iterate k g x)

theorem hoare_lemma27:

      ∃n. b1·(iterate n g x) ≠ TT
      ==> k = (LEAST n. b1·(iterate n g x) ≠ TT) ∧ b1·(iterate k g x) = UU -->
          q·x = UU

theorem hoare_lemma23:

      ∀k. b1·(iterate k g x) = TT ==> q·(p·x) = q·x

theorem hoare_lemma29:

      ∃k. b1·(iterate k g x) ≠ TT ==> q·(p·x) = q·x

theorem hoare_main:

      q oo p = q