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'> : raa = 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