(* 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