# Theory Hered

Up to index of Isabelle/CCL

theory Hered
imports Type
uses coinduction.ML [Hered.ML]
begin

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