15 (** Abstract syntax definitions for FOL and ZF **) |
15 (** Abstract syntax definitions for FOL and ZF **) |
16 |
16 |
17 val iT = Type("i",[]) |
17 val iT = Type("i",[]) |
18 and oT = Type("o",[]); |
18 and oT = Type("o",[]); |
19 |
19 |
20 (*Given u expecting arguments of types [T1,...,Tn], create term of |
20 |
21 type T1*...*Tn => i using split*) |
21 (** Logical constants **) |
22 fun ap_split split u [ ] = Abs("null", iT, u) |
|
23 | ap_split split u [_] = u |
|
24 | ap_split split u [_,_] = split $ u |
|
25 | ap_split split u (T::Ts) = |
|
26 split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts)); |
|
27 |
22 |
28 val conj = Const("op &", [oT,oT]--->oT) |
23 val conj = Const("op &", [oT,oT]--->oT) |
29 and disj = Const("op |", [oT,oT]--->oT) |
24 and disj = Const("op |", [oT,oT]--->oT) |
30 and imp = Const("op -->", [oT,oT]--->oT); |
25 and imp = Const("op -->", [oT,oT]--->oT); |
31 |
26 |