# Theory Wfd

Up to index of Isabelle/CCL

theory Wfd
imports Trancl Type Hered
uses (wfd.ML) (genrec.ML) (typecheck.ML) (eval.ML)
begin

    (*  Title:      CCL/Wfd.thy
        ID:         $Id: Wfd.thy,v 1.6 2005/09/17 15:35:30 wenzelm Exp $
        Author:     Martin Coen, Cambridge University Computer Laboratory
        Copyright   1993  University of Cambridge
    *)

    header {* Well-founded relations in CCL *}

    theory Wfd
    imports Trancl Type Hered
    uses ("wfd.ML") ("genrec.ML") ("typecheck.ML") ("eval.ML")
    begin

    consts
          (*** Predicates ***)
      Wfd        ::       "[i set] => o"
          (*** Relations ***)
      wf         ::       "[i set] => i set"
      wmap       ::       "[i=>i,i set] => i set"
      "**"       ::       "[i set,i set] => i set"      (infixl 70)
      NatPR      ::       "i set"
      ListPR     ::       "i set => i set"

    axioms

      Wfd_def:
      "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"

      wf_def:         "wf(R) == {x. x:R & Wfd(R)}"

      wmap_def:       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
      lex_def:
      "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"

      NatPR_def:      "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
      ListPR_def:     "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"

    ML {* use_legacy_bindings (the_context ()) *}

    use "wfd.ML"
    use "genrec.ML"
    use "typecheck.ML"
    use "eval.ML"

    end

theorem wfd_induct:

      [| Wfd(R); !!x. ∀y. <y,x> : R --> P(y) ==> P(x) |] ==> P(a)

theorem wfd_strengthen_lemma:

      [| !!x y. <x,y> : R ==> Q(x); ∀x. (∀y. <y,x> : R --> y : P) --> x : P;
         !!x. Q(x) ==> x : P |]
      ==> a : P

theorem wf_anti_sym:

      [| Wfd(r); <a,x> : r; <x,a> : r |] ==> P

theorem wf_anti_refl:

      [| Wfd(r); <a,a> : r |] ==> P

theorem trancl_wf:

      Wfd(R) ==> Wfd(R^+)

theorem lexXH:

      p : ra ** rb <->
      (∃a a' b b'. p = <<a,b>,<a',b'>> ∧ (<a,a'> : ra ∨ a = a' ∧ <b,b'> : rb))

theorem lexI1:

      <a,a'> : ra ==> <<a,b>,<a',b'>> : ra ** rb

theorem lexI2:

      <b,b'> : rb ==> <<a,b>,<a,b'>> : ra ** rb

theorem lexE:

      [| p : ra ** rb; !!a a' b b'. [| <a,a'> : ra; p = <<a,b>,<a',b'>> |] ==> R;
         !!a b b'. [| <b,b'> : rb; p = <<a,b>,<a,b'>> |] ==> R |]
      ==> R

theorem lex_pair:

      [| p : r ** s; !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==> P

theorem lex_wf:

      [| Wfd(R); Wfd(S) |] ==> Wfd(R ** S)

theorem wmapXH:

      p : wmap(f, r) <-> (∃x y. p = <x,y> ∧ <f(x),f(y)> : r)

theorem wmapI:

      <f(a),f(b)> : r ==> <a,b> : wmap(f, r)

theorem wmapE:

      [| p : wmap(f, r); !!a b. [| <f(a),f(b)> : r; p = <a,b> |] ==> R |] ==> R

theorem wmap_wf:

      Wfd(r) ==> Wfd(wmap(f, r))

theorem wfstI:

      <xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst, r)

theorem wsndI:

      <xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd, r)

theorem wthdI:

      <xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd, r)

theorem wfI:

      [| Wfd(r); a : r |] ==> a : wf(r)

theorem Empty_wf:

      Wfd({})

theorem wf_wf:

      Wfd(wf(R))

theorem NatPRXH:

      p : NatPR <-> (EX x:Nat. p = <x,succ(x)>)

theorem ListPRXH:

      p : ListPR(A) <-> (EX h:A. EX t:List(A). p = <t,h $ t>)

theorem NatPR_wf:

      Wfd(NatPR)

theorem ListPR_wf:

      Wfd(ListPR(A))

theorem letrecT:

      [| a : A;
         !!p g. [| p : A; ALL x:{x: A . <x,p> : wf(R)}. g(x) : D(x) |]
                ==> h(p, g) : D(p) |]
      ==> letrec g x be h(x, g) in g(a) : D(a)

theorem SPLITB:

      SPLIT(<a,b>, B) = B(a, b)

theorem letrec2T:

      [| a : A; b : B;
         !!p q g.
            [| p : A; q : B;
               ALL x:A. ALL y:{y: B . <<x,y>,<p,q>> : wf(R)}. g(x, y) : D(x, y) |]
            ==> h(p, q, g) : D(p, q) |]
      ==> letrec g x y be h(x, y, g) in g(a, b) : D(a, b)

theorem lemma:

      SPLIT(<a,<b,c>>, %x xs. SPLIT(xs, B(x))) = B(a, b, c)

theorem letrec3T:

      [| a : A; b : B; c : C;
         !!p q r g.
            [| p : A; q : B; r : C;
               ALL x:A.
               ALL y:B.
               ALL z:{z: C . <<x,<y,z>>,<p,<q,r>>> : wf(R)}.
               g(x, y, z) : D(x, y, z) |]
            ==> h(p, q, r, g) : D(p, q, r) |]
      ==> letrec g x y z be h(x, y, z, g) in g(a, b, c) : D(a, b, c)

theorem rcallT:

      [| ALL x:{x: A . <x,p> : wf(R)}. g(x) : D(x); g(a) : D(a) ==> g(a) : E; a : A;
         <a,p> : wf(R) |]
      ==> g(a) : E

theorem rcall2T:

      [| ALL x:A. ALL y:{y: B . <<x,y>,<p,q>> : wf(R)}. g(x, y) : D(x, y);
         g(a, b) : D(a, b) ==> g(a, b) : E; a : A; b : B; <<a,b>,<p,q>> : wf(R) |]
      ==> g(a, b) : E

theorem rcall3T:

      [| ALL x:A.
         ALL y:B.
         ALL z:{z: C . <<x,<y,z>>,<p,<q,r>>> : wf(R)}. g(x, y, z) : D(x, y, z);
         g(a, b, c) : D(a, b, c) ==> g(a, b, c) : E; a : A; b : B; c : C;
         <<a,<b,c>>,<p,<q,r>>> : wf(R) |]
      ==> g(a, b, c) : E

theorem hyprcallT:

      [| g(a) = b; ALL x:{x: A . <x,p> : wf(R)}. g(x) : D(x);
         [| b = g(a); g(a) : D(a) |] ==> P; a : A; <a,p> : wf(R) |]
      ==> P

theorem hyprcall2T:

      [| g(a, b) = c;
         ALL x:A. ALL y:{y: B . <<x,y>,<p,q>> : wf(R)}. g(x, y) : D(x, y);
         [| c = g(a, b); g(a, b) : D(a, b) |] ==> P; a : A; b : B;
         <<a,b>,<p,q>> : wf(R) |]
      ==> P

theorem hyprcall3T:

      [| g(a, b, c) = d;
         ALL x:A.
         ALL y:B.
         ALL z:{z: C . <<x,<y,z>>,<p,<q,r>>> : wf(R)}. g(x, y, z) : D(x, y, z);
         [| d = g(a, b, c); g(a, b, c) : D(a, b, c) |] ==> P; a : A; b : B; c : C;
         <<a,<b,c>>,<p,<q,r>>> : wf(R) |]
      ==> P

theorem rmIH1:

      [| ALL x:{x: A . <x,p> : wf(R)}. g(x) : D(x); P |] ==> P

theorem rmIH2:

      [| ALL x:A. ALL y:{y: B . <<x,y>,<p,q>> : wf(R)}. g(x, y) : D(x, y); P |] ==> P

theorem rmIH3:

      [| ALL x:A.
         ALL y:B.
         ALL z:{z: C . <<x,<y,z>>,<p,<q,r>>> : wf(R)}. g(x, y, z) : D(x, y, z);
         P |]
      ==> P

theorem letT:

      [| f(t) : B; t ≠ bot |] ==> let x be t in f(x) : B

theorem applyT2:

      [| a : A; f : Pi(A, B) |] ==> f ` a : B(a)

theorem rcall_lemma1:

      [| a : A; a : A ==> P(a) |] ==> a : Subtype(A, P)

theorem rcall_lemma2:

      [| a : Subtype(A, Q); [| a : A; Q(a) |] ==> P(a) |] ==> a : Subtype(A, P)

theorem applyV:

      [| f ---> lam x. b(x); b(a) ---> c |] ==> f ` a ---> c

theorem letV:

      [| t ---> a; f(a) ---> c |] ==> let x be t in f(x) ---> c

theorem fixV:

      f(fix(f)) ---> c ==> fix(f) ---> c

theorem letrecV:

      h(t, %y. letrec g x be h(x, g) in g(y)) ---> c
      ==> letrec g x be h(x, g) in g(t) ---> c