(* Title: CCL/Fix.thy ID: $Id: Fix.thy,v 1.4 2005/09/17 15:35:27 wenzelm Exp $ Author: Martin Coen Copyright 1993 University of Cambridge *) header {* Tentative attempt at including fixed point induction; justified by Smith *} theory Fix imports Type begin consts idgen :: "[i]=>i" INCL :: "[i=>o]=>o" axioms idgen_def: "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))" INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" po_INCL: "INCL(%x. a(x) [= b(x))" INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))" ML {* use_legacy_bindings (the_context ()) *} end
theorem fix_ind:
[| P(bot); !!x. P(x) ==> P(f(x)); INCL(P) |] ==> P(fix(f))
theorem inclXH:
INCL(P) <-> (∀f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))
theorem inclI:
(!!f. ALL n:Nat. P(f ^ n ` bot) ==> P(fix(f))) ==> INCL(P)
theorem inclD:
[| INCL(P); !!n. n : Nat ==> P(f ^ n ` bot) |] ==> P(fix(f))
theorem inclE:
[| INCL(P); (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)) ==> R |] ==> R
theorem npo_INCL:
INCL(%x. ¬ a(x) [= t)
theorem conj_INCL:
[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) ∧ Q(x))
theorem all_INCL:
(!!a. INCL(P(a))) ==> INCL(%x. ∀a. P(a, x))
theorem ball_INCL:
(!!a. a : A ==> INCL(P(a))) ==> INCL(%x. ALL a:A. P(a, x))
theorem eq_INCL:
INCL(%x. a(x) = b(x))
theorem fix_idgenfp:
idgen(fix(idgen)) = fix(idgen)
theorem id_idgenfp:
idgen(lam x. x) = lam x. x
theorem idgenfp_lam:
idgen(d) = d ==> d = lam x. case(x, true, false, %x y. <d ` x,d ` y>, %u. lam x. d ` u(x))
theorem l_lemma:
[| a = b; a ` t = u |] ==> b ` t = u
theorem po_eta:
[| ∀x. t ` x [= u ` x; ∃f. t = lam x. f(x); ∃f. u = lam x. f(x) |] ==> t [= u
theorem po_eta_lemma:
idgen(d) = d ==> d = lam x. case(x, true, false, %x y. <d ` x,d ` y>, %u. lam x. d ` u(x))
theorem lemma1:
idgen(d) = d ==> {p. ∃a b. p = <a,b> ∧ (∃t. a = fix(idgen) ` t ∧ b = d ` t)} <= POgen({p. ∃a b. p = <a,b> ∧ (∃t. a = fix(idgen) ` t ∧ b = d ` t)})
theorem fix_least_idgen:
idgen(d) = d ==> fix(idgen) [= d
theorem lemma2:
idgen(d) = d ==> {p. ∃a b. p = <a,b> ∧ b = d ` a} <= POgen({p. ∃a b. p = <a,b> ∧ b = d ` a})
theorem id_least_idgen:
idgen(d) = d ==> lam x. x [= d
theorem reachability:
fix(idgen) = lam x. x
theorem id_apply:
f = lam x. x ==> f ` t = t
theorem term_ind:
[| P(bot); P(true); P(false); !!x y. [| P(x); P(y) |] ==> P(<x,y>); !!u. (!!x. P(u(x))) ==> P(lam x. u(x)); INCL(P) |] ==> P(t)