Up to index of Isabelle/CCL
theory Hered(* Title: CCL/Hered.thy ID: $Id: Hered.thy,v 1.5 2005/09/17 15:35:27 wenzelm Exp $ Author: Martin Coen Copyright 1993 University of Cambridge *) header {* Hereditary Termination -- cf. Martin Lo\"f *} theory Hered imports Type uses "coinduction.ML" begin text {* Note that this is based on an untyped equality and so @{text "lam x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"} is. Not so useful for functions! *} consts (*** Predicates ***) HTTgen :: "i set => i set" HTT :: "i set" axioms (*** Definitions of Hereditary Termination ***) HTTgen_def: "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b> & a : R & b : R) | (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}" HTT_def: "HTT == gfp(HTTgen)" ML {* use_legacy_bindings (the_context ()) *} end
theorem lfpI:
[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)
theorem ssubst_single:
[| a = a'; a' : A |] ==> a : A
theorem ssubst_pair:
[| a = a'; b = b'; <a',b'> : A |] ==> <a,b> : A
theorem PO_refl:
<a,a> : PO
theorem EQ_refl:
<a,a> : EQ
theorem HTTgen_mono:
mono(HTTgen)
theorem HTTgenXH:
t : HTTgen(A) <-> t = true ∨ t = false ∨ (∃a b. t = <a,b> ∧ a : A ∧ b : A) ∨ (∃f. t = lam x. f(x) ∧ (∀x. f(x) : A))
theorem HTTXH:
t : HTT <-> t = true ∨ t = false ∨ (∃a b. t = <a,b> ∧ a : HTT ∧ b : HTT) ∨ (∃f. t = lam x. f(x) ∧ (∀x. f(x) : HTT))
theorem HTT_bot:
¬ bot : HTT
theorem HTT_true:
true : HTT
theorem HTT_false:
false : HTT
theorem HTT_pair:
<a,b> : HTT <-> a : HTT ∧ b : HTT
theorem HTT_lam:
lam x. f(x) : HTT <-> (∀x. f(x) : HTT)
theorem HTT_coinduct:
[| t : R; R <= HTTgen(R) |] ==> t : HTT
theorem HTT_coinduct3:
[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT
theorem UnitF:
Unit <= HTT
theorem BoolF:
Bool <= HTT
theorem PlusF:
[| A <= HTT; B <= HTT |] ==> A + B <= HTT
theorem SigmaF:
[| A <= HTT; !!x. x : A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT
theorem NatF:
Nat <= HTT
theorem ListF:
A <= HTT ==> List(A) <= HTT
theorem ListsF:
A <= HTT ==> Lists(A) <= HTT
theorem IListsF:
A <= HTT ==> ILists(A) <= HTT