author | paulson |
Mon, 10 Jul 2000 12:17:34 +0200 | |
changeset 9284 | 85a5355faa91 |
parent 6112 | 5e4871c5136b |
child 9334 | f0c2b71db81b |
permissions | -rw-r--r-- |
9284 | 1 |
(* Title: ZF/Resid/Redex.thy |
1048 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Ole Rasmussen |
1048 | 4 |
Copyright 1995 University of Cambridge |
5 |
Logic Image: ZF |
|
6 |
*) |
|
7 |
||
2874
b1e7e2179597
Datatype declarations now require theory Datatype--NOT in quotes
paulson
parents:
1478
diff
changeset
|
8 |
Redex = Datatype + |
1048 | 9 |
consts |
1401 | 10 |
redexes :: i |
1048 | 11 |
|
12 |
datatype |
|
1478 | 13 |
"redexes" = Var ("n: nat") |
1048 | 14 |
| Fun ("t: redexes") |
15 |
| App ("b:bool" ,"f:redexes" , "a:redexes") |
|
16 |
||
6046 | 17 |
|
1048 | 18 |
consts |
6046 | 19 |
Ssub,Scomp,Sreg :: i |
20 |
"<==","~" :: [i,i]=>o (infixl 70) |
|
21 |
un :: [i,i]=>i (infixl 70) |
|
22 |
union_aux :: i=>i |
|
23 |
regular :: i=>o |
|
24 |
||
9284 | 25 |
translations |
26 |
"a<==b" == "<a,b>:Ssub" |
|
27 |
"a ~ b" == "<a,b>:Scomp" |
|
28 |
"regular(a)" == "a:Sreg" |
|
29 |
||
30 |
||
6046 | 31 |
primrec (*explicit lambda is required because both arguments of "un" vary*) |
32 |
"union_aux(Var(n)) = |
|
33 |
(lam t:redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))" |
|
34 |
||
35 |
"union_aux(Fun(u)) = |
|
9284 | 36 |
(lam t:redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y), |
6046 | 37 |
%b y z. 0, t))" |
38 |
||
39 |
"union_aux(App(b,f,a)) = |
|
40 |
(lam t:redexes. |
|
41 |
redexes_case(%j. 0, %y. 0, |
|
9284 | 42 |
%c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))" |
6046 | 43 |
|
1048 | 44 |
defs |
6046 | 45 |
union_def "u un v == union_aux(u)`v" |
46 |
||
47 |
||
48 |
inductive |
|
49 |
domains "Ssub" <= "redexes*redexes" |
|
50 |
intrs |
|
51 |
Sub_Var "n:nat ==> Var(n)<== Var(n)" |
|
52 |
Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)" |
|
53 |
Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==> |
|
54 |
App(0,u1,u2)<== App(b,v1,v2)" |
|
55 |
Sub_App2 "[|u1<== v1; u2<== v2|]==> |
|
56 |
App(1,u1,u2)<== App(1,v1,v2)" |
|
57 |
type_intrs "redexes.intrs@bool_typechecks" |
|
58 |
||
59 |
inductive |
|
60 |
domains "Scomp" <= "redexes*redexes" |
|
61 |
intrs |
|
62 |
Comp_Var "n:nat ==> Var(n) ~ Var(n)" |
|
63 |
Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)" |
|
64 |
Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==> |
|
65 |
App(b1,u1,u2) ~ App(b2,v1,v2)" |
|
66 |
type_intrs "redexes.intrs@bool_typechecks" |
|
67 |
||
68 |
inductive |
|
69 |
domains "Sreg" <= "redexes" |
|
70 |
intrs |
|
71 |
Reg_Var "n:nat ==> regular(Var(n))" |
|
72 |
Reg_Fun "[|regular(u)|]==> regular(Fun(u))" |
|
73 |
Reg_App1 "[|regular(Fun(u)); regular(v) |
|
74 |
|]==>regular(App(1,Fun(u),v))" |
|
75 |
Reg_App2 "[|regular(u); regular(v) |
|
76 |
|]==>regular(App(0,u,v))" |
|
77 |
type_intrs "redexes.intrs@bool_typechecks" |
|
78 |
||
79 |
||
1048 | 80 |
end |
81 |