--- a/src/ZF/Resid/SubUnion.thy Mon Dec 28 16:53:24 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* Title: SubUnion.thy
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-SubUnion = Redex +
-
-consts
- Ssub,Scomp,Sreg :: i
- "<==","~" :: [i,i]=>o (infixl 70)
- un :: [i,i]=>i (infixl 70)
- regular :: i=>o
-
-translations
- "a<==b" == "<a,b>:Ssub"
- "a ~ b" == "<a,b>:Scomp"
- "regular(a)" == "a:Sreg"
-
-inductive
- domains "Ssub" <= "redexes*redexes"
- intrs
- Sub_Var "n:nat ==> Var(n)<== Var(n)"
- Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
- Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
- App(0,u1,u2)<== App(b,v1,v2)"
- Sub_App2 "[|u1<== v1; u2<== v2|]==>
- App(1,u1,u2)<== App(1,v1,v2)"
- type_intrs "redexes.intrs@bool_typechecks"
-
-inductive
- domains "Scomp" <= "redexes*redexes"
- intrs
- Comp_Var "n:nat ==> Var(n) ~ Var(n)"
- Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
- Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
- App(b1,u1,u2) ~ App(b2,v1,v2)"
- type_intrs "redexes.intrs@bool_typechecks"
-
-inductive
- domains "Sreg" <= "redexes"
- intrs
- Reg_Var "n:nat ==> regular(Var(n))"
- Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
- Reg_App1 "[|regular(Fun(u)); regular(v)
- |]==>regular(App(1,Fun(u),v))"
- Reg_App2 "[|regular(u); regular(v)
- |]==>regular(App(0,u,v))"
- type_intrs "redexes.intrs@bool_typechecks"
-
-defs
- union_def "u un v == redex_rec(u,
- %i. lam t:redexes. redexes_case(%j. Var(i), %x.0, %b x y.0, t),
- %x m. lam t:redexes. redexes_case(%j.0, %y. Fun(m`y), %b y z.0, t),
-%b x y m p. lam t:redexes. redexes_case(%j.0, %y.0,
- %c z u. App(b or c, m`z, p`u), t))`v"
-end