src/ZF/Resid/SubUnion.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
permissions -rw-r--r--
expanded tabs
clasohm@1478
     1
(*  Title:      SubUnion.thy
lcp@1048
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Ole Rasmussen
lcp@1048
     4
    Copyright   1995  University of Cambridge
lcp@1048
     5
    Logic Image: ZF
lcp@1048
     6
*)
lcp@1048
     7
lcp@1048
     8
SubUnion = Redex +
lcp@1048
     9
lcp@1048
    10
consts
clasohm@1401
    11
  Ssub,Scomp,Sreg  :: i
clasohm@1401
    12
  "<==","~"        :: [i,i]=>o (infixl 70)
clasohm@1401
    13
  un               :: [i,i]=>i (infixl 70)
clasohm@1478
    14
  regular          :: i=>o
lcp@1048
    15
  
lcp@1048
    16
translations
lcp@1048
    17
  "a<==b"        == "<a,b>:Ssub"
lcp@1048
    18
  "a ~ b"        == "<a,b>:Scomp"
lcp@1048
    19
  "regular(a)"   == "a:Sreg"
lcp@1048
    20
lcp@1048
    21
inductive
lcp@1048
    22
  domains       "Ssub" <= "redexes*redexes"
lcp@1048
    23
  intrs
clasohm@1478
    24
    Sub_Var     "n:nat ==> Var(n)<== Var(n)"
clasohm@1478
    25
    Sub_Fun     "[|u<== v|]==> Fun(u)<== Fun(v)"
clasohm@1478
    26
    Sub_App1    "[|u1<== v1; u2<== v2; b:bool|]==>   
clasohm@1478
    27
                     App(0,u1,u2)<== App(b,v1,v2)"
clasohm@1478
    28
    Sub_App2    "[|u1<== v1; u2<== v2|]==>   
clasohm@1478
    29
                     App(1,u1,u2)<== App(1,v1,v2)"
clasohm@1478
    30
  type_intrs    "redexes.intrs@bool_typechecks"
lcp@1048
    31
lcp@1048
    32
inductive
lcp@1048
    33
  domains       "Scomp" <= "redexes*redexes"
lcp@1048
    34
  intrs
clasohm@1478
    35
    Comp_Var    "n:nat ==> Var(n) ~ Var(n)"
clasohm@1478
    36
    Comp_Fun    "[|u ~ v|]==> Fun(u) ~ Fun(v)"
clasohm@1478
    37
    Comp_App    "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>   
clasohm@1478
    38
                     App(b1,u1,u2) ~ App(b2,v1,v2)"
clasohm@1478
    39
  type_intrs    "redexes.intrs@bool_typechecks"
lcp@1048
    40
lcp@1048
    41
inductive
lcp@1048
    42
  domains       "Sreg" <= "redexes"
lcp@1048
    43
  intrs
clasohm@1478
    44
    Reg_Var     "n:nat ==> regular(Var(n))"
clasohm@1478
    45
    Reg_Fun     "[|regular(u)|]==> regular(Fun(u))"
clasohm@1478
    46
    Reg_App1    "[|regular(Fun(u)); regular(v) 
clasohm@1478
    47
                     |]==>regular(App(1,Fun(u),v))"
clasohm@1478
    48
    Reg_App2    "[|regular(u); regular(v) 
clasohm@1478
    49
                     |]==>regular(App(0,u,v))"
clasohm@1478
    50
  type_intrs    "redexes.intrs@bool_typechecks"
lcp@1048
    51
lcp@1048
    52
defs
clasohm@1155
    53
  union_def  "u un v == redex_rec(u,   
clasohm@1478
    54
         %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),   
clasohm@1155
    55
      %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),   
clasohm@1155
    56
%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,   
clasohm@1478
    57
                                       %c z u. App(b or c, m`z, p`u), t))`v"
lcp@1048
    58
end
lcp@1048
    59