Logosphere.
A Formal Digital Library.
Department of Computer Science
Yale University
51 Prospect St.
New Haven, CT 06520-8285
U.S.A.
|
Home |
|
|
Publications |
|
|
Logics Resolution Paramodulation HOL Nuprl PVS |
|
|
Examples |
% File: pvs-0.1.elf
% Encoding of PVS in Twelf
% following "Sam Owre, Natarajan Shankar. The Formal Semantics of PVS"
% Author: Carsten Schuermann
level : type.
1 : level.
2 : level.
term : type. %name term T x.
% Pretypes
TYPE : level -> term.
uni1 = TYPE 1.
uni2 = TYPE 2.
fun : term -> (term -> term) -> term.
sig : term -> (term -> term) -> term.
set : term -> (term -> term) -> term.
def : term -> term -> (term -> term) -> term.
unit : term.
=> : term -> term -> term
= [A][B] fun A ([x] B). %infix right 10 =>.
& : term -> term -> term
= [A][B] sig A ([x] B). %infix right 11 &.
&* : term -> term -> term -> term
= [A][M][B] def A M ([x] B).
% Preterms
@ : term -> term -> term. %infix left 13 @.
lam : term -> (term -> term) -> term.
fst : term -> term.
snd : term -> term.
, : term -> term -> term. %infix right 11 ,.
* : term.
% Base type and constants
bool : term.
true : term.
false : term.
if : term.
eq : term.
% Notational Definitions
=== : term -> term -> type. %infix left 6 ===.
%mode === +T -T'.
boolop : term.
d-boolop : boolop === ((bool & bool) => bool).
% Theories
theory-real0 = sig (uni1) [real] real & ((real & real) => bool).
real :term.
d-real : real === (lam theory-real0 [t :term] fst t).
zero :term.
d-zero : zero === (lam theory-real0 [t :term] fst (snd t)).
<= :term.
d-<= : <= === (lam theory-real0 [t :term] snd (snd t)).
theory-ifdef = fun uni1 [T] (bool & T & T) => T.
theory-equality = fun uni1 [T] T & T => bool.
d-if : if === lam theory-ifdef [x] lam uni1 [T] x @ T.
d-eq : eq === lam theory-equality [x] lam uni1 [T] x @ T.
t-if : term.
t-eq : term.
neg = lam bool [x] (eq @ t-eq @ bool) @ (x , false).
and = lam (bool & bool) [x] (if @ t-if @ bool) @ (fst x , snd x , false).
or = lam (bool & bool) [x] (if @ t-if @ bool) @ (fst x , true , (snd x)).
imp = lam (bool & bool) [x] (if @ t-if @ bool) @ (fst x , snd x , true).
all : term -> (term -> term) -> term
= [A][M] eq @ t-eq @ (A => bool)
@ (lam A ([x] M x) , lam A ([x] true)).
% Example 2.1
ex-2-1a : term
= bool.
ex-2-1b : term
= real.
ex-2-1c : term
= (bool , real).
ex-2-1d : term
= (real , bool) => bool.
% Example 2.2
ex-2-2a : term
= true.
ex-2-2b : term
= neg @ true.
ex-2-2c : term
= lam bool [x] neg @ x.
ex-2-2d : term
= snd (true , false).
ex-2-2e : term
= (true , lam bool [x] neg @ (neg @ x)).
% Defintion expansion
delta : term -> term -> type. %mode delta +A -B.
d-bool : delta bool bool.
d-false : delta false false.
d-true : delta true true.
d-t-if : delta t-if t-if.
d-t-eq : delta t-eq t-eq.
d-type : delta (TYPE L) (TYPE L).
d-* : delta * *.
d-=== : delta A A''
<- A === A'
<- delta A' A''.
d-fun : delta (fun A B) (fun A' B')
<- delta A A'
<- ({x:term} delta x x
-> delta (B x) (B' x)).
d-sig : delta (sig A B) (sig A' B')
<- delta A A'
<- ({x:term} delta x x
-> delta (B x) (B' x)).
d-def : delta (def A M B) (def A' M' B')
<- delta A A'
<- delta M M'
<- ({x:term} delta x M'
-> delta (B x) (B' x)).
d-set : delta (set A M) (set A' M)
<- delta A A'.
d-, : delta (M1 , M2) (M1' , M2')
<- delta M1 M1'
<- delta M2 M2'.
d-fst : delta (fst M) (fst M')
<- delta M M'.
d-snd : delta (snd M) (snd M')
<- delta M M'.
d-lam : delta (lam A M) (lam A' M')
<- delta A A'
<- ({x:term} delta x x
-> delta (M x) (M' x)).
d-app : delta (M1 @ M2) (M1' @ M2')
<- delta M1 M1'
<- delta M2 M2'.
%block defexp : some {M:term -> term}
block {x:term}
{d:delta x (M x)}.
%worlds (defexp) (=== _ _ ) (delta _ _).
% Example 2.19
ex-2-19b : delta boolop (fun (sig bool ([x:term] bool)) ([x:term] bool))
= d-===
(d-fun
([x:term] [x1:delta x x] d-bool)
(d-sig
([x:term] [x1:delta x x] d-bool)
d-bool))
d-boolop.
%solve ex-2-19c : delta or _.
ex-2-19c :
delta or
(lam (sig bool ([x:term] bool))
([x:term]
lam
(fun uni1
([x1:term]
fun (sig bool ([x2:term] sig x1 ([x3:term] x1)))
([x2:term] x1)))
([x1:term] lam uni1 ([x2:term] x1 @ x2))
@ t-if @ bool @ (fst x , true , snd x)))
= d-lam
([x:term] [x2:delta x x]
d-app (d-, (d-, (d-snd x2) d-true) (d-fst x2))
(d-app d-bool
(d-app d-t-if
(d-===
(d-lam
([x15:term] [x16:delta x15 x15]
d-lam
([x17:term] [x18:delta x17 x17]
d-app x18 x16) d-type)
(d-fun
([x7:term] [x8:delta x7 x7]
d-fun ([x13:term] [x14:delta x13 x13] x8)
(d-sig
([x9:term] [x10:delta x9 x9]
d-sig
([x11:term]
[x12:delta x11 x11] x8)
x8)
d-bool))
d-type))
d-if))))
(d-sig ([x:term] [x1:delta x x] d-bool) d-bool).
% Maximal Supertypes.
% Definition 4.4
con : term -> term -> term -> type. %mode con +T +M -T'.
con-bool : con bool _ bool.
con-t-if : con t-if _ t-if.
con-t-eq : con t-eq _ t-eq.
con-type : con (TYPE L) _ (TYPE L).
con-set : con (set A M) N (set A [x] and @ (M x , N)).
con-=> : con (A => B) N (A' => B')
<- con A N A'
<- con B N B'.
con-, : con (A & B) N (A' & B')
<- con A N A'
<- con B N B'.
% Definition 3.1, 4.5
mu : term -> term -> type. %mode mu +T -T'.
muX : term -> term -> type. %mode muX +T -T'.
pi : term -> term -> type. %mode pi +T -T'.
piX : term -> term -> type. %mode piX +T -T'.
% Definition 3.2 (direct supertype)
mu0 : term -> term -> type. %mode mu0 +T -T'.
mu0X : term -> term -> type. %mode mu0X +T -T'.
% Base cases
muX-bool : muX bool bool.
muX-t-if : muX t-if t-if.
muX-t-eq : muX t-eq t-eq.
muX-type : muX (TYPE L) (TYPE L).
piX-bool : piX bool (lam bool [x] true).
piX-t-if : piX t-if (lam t-if [x] true).
piX-t-eq : piX t-eq (lam t-eq [x] true).
piX-type : piX (TYPE L) (lam (TYPE L) [x] true).
mu0X-bool : mu0X bool bool.
mu0X-t-if : mu0X t-if t-if.
mu0X-t-eq : mu0X t-eq t-eq.
mu0X-type : mu0X (TYPE L) (TYPE L).
% Inference rules
mu-muX : mu A A''
<- delta A A'
<- muX A' A''.
muX-fun: muX (fun A B) (fun A B')
<- ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A [x] true)
-> mu0X x x
-> muX (B x) (B' x)).
muX-sig: muX (sig A1 A2) (sig A1' A2')
<- muX A1 A1'
<- piX A1 M1
<- ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A1 [x] true)
-> mu0X x x
-> con (A2 x) (M1 @ x) (A2' x)).
muX-set: muX (set A M) A'
<- muX A A'.
pi-piX : pi A A''
<- delta A A'
<- piX A' A''.
piX-fun: piX (fun A B)
(lam (fun A B') [x:term] all A [y:term] (B'' y) @ (x @ y))
<- ({y} delta y y
-> ({N:term} con y N y)
-> muX y y
-> piX y (lam A [x] true)
-> mu0X y y
-> muX (B y) (B' y))
<- ({y} delta y y
-> ({N:term} con y N y)
-> muX y y
-> piX y (lam A [x] true)
-> mu0X y y
-> piX (B y) (B'' y)).
piX-sig: piX (sig A B) (lam (sig A' B') [x:term] and @ (A'' @ (fst x) ,
(B'' (fst x)) @ (snd x)))
<- muX A A'
<- ({y} delta y y
-> ({N:term} con y N y)
-> muX y y
-> piX y (lam A [x] true)
-> mu0X y y
-> muX (B y) (B' y))
<- piX A A''
<- ({y} delta y y
-> ({N:term} con y N y)
-> muX y y
-> piX y (lam A [x] true)
-> mu0X y y
-> piX (B y) (B'' y)).
piX-set: piX (set A M) (lam A' [x] and @ (A'' @ x , M x))
<- muX A A'
<- piX A A''.
mu0-mu0X: mu0 A A''
<- delta A A'
<- mu0X A' A''.
mu0X-fun : mu0X (fun A B) (fun A B).
mu0X-sig : mu0X (sig A1 A2) (sig A1 A2).
mu0X-set : mu0X (set A M) A'
<- mu0X A A'.
%block maxsup : some {M:term -> term} {A:term}
block {x:term}
{d:delta x (M x)}
{n: {N:term} con x N x}
{m: muX x x}
{p: piX x (lam A [x] true)}
{m0: mu0X x x}.
%worlds (maxsup) (con _ _ _) (mu _ _) (muX _ _) (pi _ _) (piX _ _) (mu0 _ _) (mu0X _ _).
% Examples
% Integers as primitives
int : term.
d-int : delta int int.
con-int : con int _ int.
m0-int : mu0 int int .
muX-int : muX int int.
piX-int : piX int (lam int [x] true).
zero-int : term.
d-zero-int : delta zero-int zero-int.
less-int : term.
d-less-int : delta less-int less-int.
nat : term.
d-nat : nat === (set int ([i] less-int @ (zero-int , i))).
natinjection : term.
d-natinjection : natinjection ===
(set (nat => nat) [f]
all (nat & nat) [ij]
imp @ (eq @ t-eq @ nat @ (f @ (fst ij)) @ (f @ (snd ij)))
@ (eq @ t-eq @ nat @ (fst ij) @ (snd ij))).
% Example 3.3
%solve ex-3-3-1 : mu natinjection _.
ex-3-3-1 :
mu natinjection
(fun (set int ([x:term] less-int @ (zero-int , x))) ([x:term] int))
= mu-muX
(muX-set
(muX-fun
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x
(lam (set int ([x4:term] less-int @ (zero-int , x4)))
([x4:term] true))]
[x5:mu0X x x] muX-set muX-int)))
(d-===
(d-set
(d-fun ([x:term] [x1:delta x x] d-=== (d-set d-int) d-nat)
(d-=== (d-set d-int) d-nat)))
d-natinjection).
%solve ex-3-3-2 : mu0 natinjection _.
ex-3-3-2 :
mu0 natinjection
(fun (set int ([x:term] less-int @ (zero-int , x)))
([x:term] set int ([x1:term] less-int @ (zero-int , x1))))
= mu0-mu0X (mu0X-set mu0X-fun)
(d-===
(d-set
(d-fun ([x:term] [x1:delta x x] d-=== (d-set d-int) d-nat)
(d-=== (d-set d-int) d-nat)))
d-natinjection).
% Example 3.5
%solve ex3-5a : pi nat X.
ex3-5a :
pi nat
(lam int
([x:term]
and @ (lam int ([x1:term] true) @ x , less-int @ (zero-int , x))))
= pi-piX (piX-set piX-int muX-int) (d-=== (d-set d-int) d-nat).
%solve ex3-5b : pi (nat => nat) X.
ex3-5b :
pi (nat => nat)
(lam (fun (set int ([x:term] less-int @ (zero-int , x))) ([x:term] int))
([x:term]
all (set int ([x1:term] less-int @ (zero-int , x1)))
([y:term]
lam int
([x1:term]
and
@ (lam int ([x2:term] true) @ x1
, less-int @ (zero-int , x1))) @ (x @ y))))
= pi-piX
(piX-fun
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y
(lam (set int ([x3:term] less-int @ (zero-int , x3)))
([x3:term] true))]
[x4:mu0X y y] piX-set piX-int muX-int)
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y
(lam (set int ([x3:term] less-int @ (zero-int , x3)))
([x4:term] true))]
[x4:mu0X y y] muX-set muX-int))
(d-fun ([x:term] [x1:delta x x] d-=== (d-set d-int) d-nat)
(d-=== (d-set d-int) d-nat)).
%solve ex3-5c : pi (natinjection) X.
ex3-5c :
pi natinjection
(lam (fun (set int ([x:term] less-int @ (zero-int , x))) ([x:term] int))
([x:term]
and
@ (lam
(fun (set int ([x1:term] less-int @ (zero-int , x1)))
([x1:term] int))
([x1:term]
all (set int ([x2:term] less-int @ (zero-int , x2)))
([y:term]
lam int
([x2:term]
and
@ (lam int ([x3:term] true) @ x2
, less-int @ (zero-int , x2)))
@ (x1 @ y)))
@ x
, all (nat & nat)
([ij:term]
imp
@ (eq @ t-eq @ nat @ (x @ fst ij)
@ (x @ snd ij))
@ (eq @ t-eq @ nat @ fst ij @ snd ij)))))
= pi-piX
(piX-set
(piX-fun
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y
(lam (set int ([x3:term] less-int @ (zero-int , x3)))
([x4:term] true))]
[x4:mu0X y y] piX-set piX-int muX-int)
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y
(lam (set int ([x3:term] less-int @ (zero-int , x3)))
([x5:term] true))]
[x4:mu0X y y] muX-set muX-int))
(muX-fun
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x
(lam (set int ([x4:term] less-int @ (zero-int , x4)))
([x6:term] true))]
[x5:mu0X x x] muX-set muX-int)))
(d-===
(d-set
(d-fun ([x:term] [x1:delta x x] d-=== (d-set d-int) d-nat)
(d-=== (d-set d-int) d-nat)))
d-natinjection).
% Type Equivalence
% Definition 3.6 (adjusted according to Defintion 4.6)
tequiv : term -> term -> term -> type.
%mode tequiv +A +B -C.
tequivX : term -> term -> term -> type.
%mode tequivX +A +B -C.
tequivX-bool : tequivX bool bool true.
tequivX-t-eq : tequivX t-eq t-eq true.
tequivX-t-if : tequivX t-if t-if true.
tequivX-type : tequivX (TYPE L) (TYPE L) true.
tequivX-int : tequivX int int true.
tequivX-tequiv : tequiv A B C
<- delta A A'
<- delta B B'
<- tequivX A' B' C.
tequivX-fun : tequivX (fun A B) (fun A' B')
(and @ (and @ (M1 , eq @ t-eq @ (MA => bool) @ (SA , SA')) ,
(all A ([x] M3 x))))
<- muX A MA
<- muX A' MA'
<- tequivX MA MA' M1
<- piX A SA
<- piX A' SA'
<- ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A [x] true)
-> mu0X x x
-> tequivX x x true
-> tequivX (B x) (B' x) (M3 x)).
tequivX-sig : tequivX (sig A B) (sig A' B') (and @ (M1 , all A M2))
<- tequivX A A' M1
<- ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A [x] true)
-> mu0X x x
-> tequivX x x true
-> tequivX (B x) (B' x) (M2 x)).
%block l4 : some {M:term -> term}
{A:term}
block {x:term}
{d:delta x (M x)}
{n:{N:term} con x N x}
{m:muX x x}
{s:piX x (lam A [x] true)}
{m0:mu0X x x}
{t:tequivX x x true}.
%worlds (l4) (tequivX _ _ _) (tequiv _ _ _).
% Definition 4.6
tequiva : term -> term -> term -> term -> type.
%mode tequiva +A +T +B -C.
tequivaX : term -> term -> term -> term -> type.
%mode tequivaX +A +T +B -C.
tequivaX-bool : tequivaX bool _ bool true.
tequivaX-t-eq : tequivaX t-eq _ t-eq true.
tequivaX-t-if : tequivaX t-if _ t-if true.
tequivaX-type : tequivaX (TYPE L) _ (TYPE L) true.
tequivaX-int : tequivaX int _ int true.
tequivaX-tequiva : tequiva A T B C
<- delta A A'
<- delta B B'
<- tequivaX A' T B' C.
tequivaX-fun : tequivaX (fun A B) T (fun A' B')
(and @ (and @ (M1 , eq @ t-eq @ (MA => bool) @ (SA , SA')) ,
all A ([x] M3 x)))
<- muX A MA
<- muX A' MA'
<- tequivX MA MA' M1
<- piX A SA
<- piX A' SA'
<- ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A [x] true)
-> mu0X x x
-> tequivX x x true
-> ({T':term } tequivaX x T' x true)
-> tequivaX (B x) (T @ x) (B' x) (M3 x)).
tequivaX-sig : tequivaX (sig A B) T (sig A' B') (and @ (M1 , M2))
<- tequivaX A (fst T) A' M1
<- tequivaX (B (fst T)) (snd T) (B' (fst T)) M2.
%block l5 : some {M:term -> term}
{A:term}
block {x:term}
{d:delta x (M x)}
{n:{N:term} con x N x}
{m:muX x x}
{s:piX x (lam A [x] true)}
{m0:mu0X x x}
{t: tequivX x x true}
{ta:{T':term } tequivaX x T' x true}.
%worlds (l5) (tequivaX _ _ _ _) (tequiva _ _ _ _).
% Definition 3.8
~ : term -> term -> term -> type.
~base : ~ A B C
<- mu A MA
<- mu B MB
<- tequiv MA MB C.
% Definition 4.6 (next paragraph)
~a : term -> term -> term -> term -> type.
~base : ~a A M B C
<- mu A MA
<- mu B MB
<- tequiva MA M MB C.
%worlds (l5) (~ _ _ _) (~a _ _ _ _).
% Example 3.7
NAT : term.
d-NAT : NAT === (set int ([i] imp @ (less-int @ (i , zero-int) , eq @ t-eq @ int @ (i , zero-int)))).
NATinjection : term.
d-NATinjection : NATinjection ===
(set (NAT => NAT) [f]
all (NAT & NAT) [ij]
imp @ (eq @ t-eq @ NAT @ (f @ (fst ij)) @ (f @ (snd ij)))
@ (eq @ t-eq @ NAT @ (fst ij) @ (snd ij))).
%solve ex3-7-1 : mu (natinjection => natinjection) _.
ex3-7-1 :
mu (natinjection => natinjection)
(fun
(set
(fun (set int ([x:term] less-int @ (zero-int , x)))
([x:term] set int ([x1:term] less-int @ (zero-int , x1))))
([x:term]
all (nat & nat)
([ij:term]
imp @ (eq @ t-eq @ nat @ (x @ fst ij) @ (x @ snd ij))
@ (eq @ t-eq @ nat @ fst ij @ snd ij))))
([x:term]
fun (set int ([x1:term] less-int @ (zero-int , x1)))
([x1:term] int)))
= mu-muX
(muX-fun
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x
(lam
(set
(fun
(set int
([x4:term] less-int @ (zero-int , x4)))
([x4:term]
set int
([x5:term] less-int @ (zero-int , x5))))
([x4:term]
all (nat & nat)
([ij:term]
imp
@ (eq @ t-eq @ nat @ (x4 @ fst ij)
@ (x4 @ snd ij))
@ (eq @ t-eq @ nat @ fst ij
@ snd ij))))
([x4:term] true))]
[x5:mu0X x x]
muX-set
(muX-fun
([x6:term] [x7:delta x6 x6] [x8:{N:term} con x6 N x6]
[x9:muX x6 x6]
[x10:piX x6
(lam
(set int
([x10:term]
less-int @ (zero-int , x10)))
([x10:term] true))]
[x11:mu0X x6 x6] muX-set muX-int))))
(d-fun
([x:term] [x1:delta x x]
d-===
(d-set
(d-fun
([x11:term] [x2:delta x11 x11]
d-=== (d-set d-int) d-nat)
(d-=== (d-set d-int) d-nat))) d-natinjection)
(d-===
(d-set
(d-fun ([x:term] [x1:delta x x] d-=== (d-set d-int) d-nat)
(d-=== (d-set d-int) d-nat)))
d-natinjection)).
ex3-7-1a = (fun
(set
(fun (set int ([x:term] less-int @ (zero-int , x)))
([x:term] set int ([x1:term] less-int @ (zero-int , x1))))
([x:term]
all (nat & nat)
([ij:term]
imp @ (eq @ t-eq @ nat @ (x @ fst ij) @ (x @ snd ij))
@ (eq @ t-eq @ nat @ fst ij @ snd ij))))
([x:term]
fun (set int ([x1:term] less-int @ (zero-int , x1)))
([x1:term] int))).
%solve ex3-7-2 : mu (NATinjection => NATinjection) _.
ex3-7-2 :
mu (NATinjection => NATinjection)
(fun
(set
(fun
(set int
([x:term]
imp
@ (less-int @ (x , zero-int)
, eq @ t-eq @ int @ (x , zero-int))))
([x:term]
set int
([x1:term]
imp
@ (less-int @ (x1 , zero-int)
, eq @ t-eq @ int @ (x1 , zero-int)))))
([x:term]
all (NAT & NAT)
([ij:term]
imp @ (eq @ t-eq @ NAT @ (x @ fst ij) @ (x @ snd ij))
@ (eq @ t-eq @ NAT @ fst ij @ snd ij))))
([x:term]
fun
(set int
([x1:term]
imp
@ (less-int @ (x1 , zero-int)
, eq @ t-eq @ int @ (x1 , zero-int))))
([x1:term] int)))
= mu-muX
(muX-fun
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x
(lam
(set
(fun
(set int
([x4:term]
imp
@ (less-int @ (x4 , zero-int)
, eq @ t-eq @ int
@ (x4 , zero-int))))
([x4:term]
set int
([x5:term]
imp
@ (less-int @ (x5 , zero-int)
, eq @ t-eq @ int
@ (x5 , zero-int)))))
([x4:term]
all (NAT & NAT)
([ij:term]
imp
@ (eq @ t-eq @ NAT @ (x4 @ fst ij)
@ (x4 @ snd ij))
@ (eq @ t-eq @ NAT @ fst ij
@ snd ij))))
([x4:term] true))]
[x5:mu0X x x]
muX-set
(muX-fun
([x6:term] [x7:delta x6 x6] [x8:{N:term} con x6 N x6]
[x9:muX x6 x6]
[x10:piX x6
(lam
(
set int
([x10:term]
imp @ (less-int @ (x10 , zero-int) , eq @ t-eq @ int @ (x10 , zero-int))))
([x10:term] true))]
[x11:mu0X x6 x6] muX-set muX-int))))
(d-fun
([x:term] [x1:delta x x]
d-===
(d-set
(d-fun
([x11:term] [x2:delta x11 x11]
d-=== (d-set d-int) d-NAT)
(d-=== (d-set d-int) d-NAT))) d-NATinjection)
(d-===
(d-set
(d-fun ([x:term] [x1:delta x x] d-=== (d-set d-int) d-NAT)
(d-=== (d-set d-int) d-NAT)))
d-NATinjection)).
ex3-7-2a = (fun
(set
(fun
(set int
([x:term]
imp
@ (less-int @ (x , zero-int)
, eq @ t-eq @ int @ (x , zero-int))))
([x:term]
set int
([x1:term]
imp
@ (less-int @ (x1 , zero-int)
, eq @ t-eq @ int @ (x1 , zero-int)))))
([x:term]
all (NAT & NAT)
([ij:term]
imp @ (eq @ t-eq @ NAT @ (x @ fst ij) @ (x @ snd ij))
@ (eq @ t-eq @ NAT @ fst ij @ snd ij))))
([x:term]
fun
(set int
([x1:term]
imp
@ (less-int @ (x1 , zero-int)
, eq @ t-eq @ int @ (x1 , zero-int))))
([x1:term] int))).
%solve ex3-7-3 : tequiv ex3-7-1a ex3-7-2a X.
ex3-7-3a =(and
@ (and
@ (and
@ (and
@ (true
, eq @ t-eq @ (int => bool)
@
(lam int
([x:term] and @ (lam int ([x1:term] true) @ x , less-int @ (zero-int , x)))
, lam int
([x:term]
and
@ (lam int ([x2:term] true) @ x
, imp
@ (less-int @ (x , zero-int)
, eq @ t-eq @ int @ (x , zero-int))))))
, all (set int ([x:term] less-int @ (zero-int , x)))
([x:term] true))
, eq @ t-eq
@ (fun (set int ([x:term] less-int @ (zero-int , x)))
([x:term] int)
=> bool)
@ (lam
(fun
(set int
([x:term] less-int @ (zero-int , x)))
([x:term] int))
([x:term]
and
@
(lam (fun (set int ([x1:term] less-int @ (zero-int , x1))) ([x1:term] int))
([x3:term]
all (set int ([x1:term] less-int @ (zero-int , x1)))
([y:term]
lam int
([x4:term]
and
@ (lam int ([x5:term] true) @ x4
, less-int @ (zero-int , x4))) @ (x3 @ y))) @ x
, all (nat & nat)
([ij:term]
imp @ (eq @ t-eq @ nat @ (x @ fst ij) @ (x @ snd ij))
@ (eq @ t-eq @ nat @ fst ij @ snd ij))))
, lam
(fun
(set int
([x:term]
imp @ (less-int @ (x , zero-int) , eq @ t-eq @ int @ (x , zero-int))))
([x:term] int))
([x:term]
and
@ (lam
(fun
(set int
([x1:term]
imp
@ (less-int @ (x1 , zero-int)
, eq @ t-eq @ int @ (x1 , zero-int))))
([x1:term] int))
([x6:term]
all
(set int
([x1:term]
imp
@ (less-int @ (x1 , zero-int)
, eq @ t-eq @ int @ (x1 , zero-int))))
([y:term]
lam int
([x7:term]
and
@ (lam int ([x8:term] true) @ x7
, imp
@ (less-int @ (x7 , zero-int)
, eq @ t-eq @ int
@ (x7 , zero-int))))
@ (x6 @ y))) @ x
, all (NAT & NAT)
([ij:term]
imp @ (eq @ t-eq @ NAT @ (x @ fst ij) @ (x @ snd ij))
@ (eq @ t-eq @ NAT @ fst ij @ snd ij))))))
, all
(set
(fun (set int ([x:term] less-int @ (zero-int , x)))
([x:term]
set int ([x1:term] less-int @ (zero-int , x1))))
([x:term]
all (nat & nat)
([ij:term]
imp
@ (eq @ t-eq @ nat @ (x @ fst ij)
@ (x @ snd ij))
@ (eq @ t-eq @ nat @ fst ij @ snd ij))))
([x:term]
and
@ (and
@ (true
,
eq @ t-eq @ (int => bool)
@ (lam int
([x9:term]
and @ (lam int ([x10:term] true) @ x9 , less-int @ (zero-int , x9)))
, lam int
([x11:term]
and
@ (lam int ([x12:term] true) @ x11
, imp
@ (less-int @ (x11 , zero-int)
, eq @ t-eq @ int @ (x11 , zero-int))))))
, all
(set int
([x1:term] less-int @ (zero-int , x1)))
([x13:term] true))))).
%solve ex3-7-4 : pi natinjection PI1'.
ex3-7-4 :
pi natinjection
(lam (fun (set int ([x:term] less-int @ (zero-int , x))) ([x:term] int))
([x:term]
and
@ (lam
(fun (set int ([x1:term] less-int @ (zero-int , x1)))
([x1:term] int))
([x1:term]
all (set int ([x2:term] less-int @ (zero-int , x2)))
([y:term]
lam int
([x2:term]
and
@ (lam int ([x3:term] true) @ x2
, less-int @ (zero-int , x2)))
@ (x1 @ y)))
@ x
, all (nat & nat)
([ij:term]
imp
@ (eq @ t-eq @ nat @ (x @ fst ij)
@ (x @ snd ij))
@ (eq @ t-eq @ nat @ fst ij @ snd ij)))))
= pi-piX
(piX-set
(piX-fun
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y
(lam (set int ([x3:term] less-int @ (zero-int , x3)))
([x4:term] true))]
[x4:mu0X y y] piX-set piX-int muX-int)
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y
(lam (set int ([x3:term] less-int @ (zero-int , x3)))
([x5:term] true))]
[x4:mu0X y y] muX-set muX-int))
(muX-fun
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x
(lam (set int ([x4:term] less-int @ (zero-int , x4)))
([x6:term] true))]
[x5:mu0X x x] muX-set muX-int)))
(d-===
(d-set
(d-fun ([x:term] [x1:delta x x] d-=== (d-set d-int) d-nat)
(d-=== (d-set d-int) d-nat)))
d-natinjection).
%solve ex3-7-5 : pi NATinjection PI2'.
ex3-7-5 :
pi NATinjection
(lam
(fun
(set int
([x:term]
imp
@ (less-int @ (x , zero-int)
, eq @ t-eq @ int @ (x , zero-int))))
([x:term] int))
([x:term]
and
@ (lam
(fun
(set int
([x1:term]
imp
@ (less-int @ (x1 , zero-int)
, eq @ t-eq @ int @ (x1 , zero-int))))
([x1:term] int))
([x1:term]
all
(set int
([x2:term]
imp
@ (less-int @ (x2 , zero-int)
, eq @ t-eq @ int
@ (x2 , zero-int))))
([y:term]
lam int
([x2:term]
and
@ (lam int ([x3:term] true) @ x2
, imp
@ (less-int @ (x2 , zero-int) , eq @ t-eq @ int @ (x2 , zero-int))))
@ (x1 @ y)))
@ x
, all (NAT & NAT)
([ij:term]
imp
@ (eq @ t-eq @ NAT @ (x @ fst ij)
@ (x @ snd ij))
@ (eq @ t-eq @ NAT @ fst ij @ snd ij)))))
= pi-piX
(piX-set
(piX-fun
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y
(lam
(set int
([x3:term]
imp
@ (less-int @ (x3 , zero-int)
, eq @ t-eq @ int
@ (x3 , zero-int))))
([x4:term] true))]
[x4:mu0X y y] piX-set piX-int muX-int)
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y
(lam
(set int
([x3:term]
imp
@ (less-int @ (x3 , zero-int)
, eq @ t-eq @ int
@ (x3 , zero-int))))
([x5:term] true))]
[x4:mu0X y y] muX-set muX-int))
(muX-fun
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x
(lam
(set int
([x4:term]
imp
@ (less-int @ (x4 , zero-int)
, eq @ t-eq @ int
@ (x4 , zero-int))))
([x6:term] true))]
[x5:mu0X x x] muX-set muX-int)))
(d-===
(d-set
(d-fun ([x:term] [x1:delta x x] d-=== (d-set d-int) d-NAT)
(d-=== (d-set d-int) d-NAT)))
d-NATinjection).
%solve ex3-7-6 : tequiv (nat => int) (NAT => int) _.
ex3-7-6a = (and
@ (and
@ (true
, eq @ t-eq @ (int => bool)
@ (lam int
([x:term]
and
@ (lam int ([x1:term] true) @ x
, less-int @ (zero-int , x)))
, lam int
([x:term]
and
@ (lam int ([x2:term] true) @ x
, imp @ (less-int @ (x , zero-int) , eq @ t-eq @ int @ (x , zero-int))))))
, all (set int ([x:term] less-int @ (zero-int , x)))
([x:term] true))).
% Example 4.7
%solve ex4-7-1 : mu (fun int [i] set int [j] less-int @ (i , j)) C.
ex4-7-1 :
mu (fun int ([i:term] set int ([j:term] less-int @ (i , j))))
(fun int ([x:term] int))
= mu-muX
(muX-fun
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x (lam int ([x4:term] true))] [x5:mu0X x x]
muX-set muX-int))
(d-fun ([x:term] [x1:delta x x] d-set d-int) d-int).
%solve ex4-7-2 : pi (fun int [i] set int [j] less-int @ (i , j)) C.
ex4-7-2 :
pi (fun int ([i:term] set int ([j:term] less-int @ (i , j))))
(lam (fun int ([x:term] int))
([x:term]
all int
([y:term]
lam int
([x1:term]
and
@ (lam int ([x2:term] true) @ x1
, less-int @ (y , x1))) @ (x @ y))))
= pi-piX
(piX-fun
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y (lam int ([x3:term] true))] [x4:mu0X y y]
piX-set piX-int muX-int)
([y:term] [x:delta y y] [x1:{N:term} con y N y] [x2:muX y y]
[x3:piX y (lam int ([x4:term] true))] [x4:mu0X y y]
muX-set muX-int))
(d-fun ([x:term] [x1:delta x x] d-set d-int) d-int).
% Typing
% Positive occurrences
|+ : term -> type. %prefix 4 |+.
% Negative occurrences
|- : term -> type. %prefix 4 |-.
% Contradiction
# : type.
of : term -> term -> type.
ofX : term -> term -> type.
% Atomic assumptions
ofX-bool : ofX bool uni1.
ofX-false : ofX false bool.
ofX-true : ofX true bool.
ofX-boolop: ofX boolop uni1.
ofX-t-if : ofX t-if theory-ifdef.
ofX-t-eq : ofX t-eq theory-equality.
ofX-TYPE : ofX uni1 uni2.
ofX-int : ofX int uni1.
ofX-zero-int : ofX zero-int int.
ofX-less-int : ofX less-int ((int & int) => bool).
% Definition Typing
ofbase : of M A
<- delta A A'
<- ofX M A'.
ofXcoerce : ofX M uni2
<- ofX M uni1.
ofXunit : ofX * unit.
ofXset : ofX (set T M) (TYPE L)
<- ofX T (TYPE L)
<- ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam T [x] true)
-> mu0X x x
-> tequivX x x true
-> ({T'} tequivaX x T' x true)
-> ofX x T
-> ofX (M x) bool).
% maybe this should be of (M x) bool. Ask Shankar. depand on d-set.
% it's ok. term level definitions are never expanded --cs Wed Jun 9 16:41:08 2004
ofXfun : ofX (fun A1 A2) (TYPE L)
<- ofX A1 (TYPE L)
<- ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A1 [x] true)
-> mu0X x x
-> tequivX x x true
-> ({T'} tequivaX x T' x true)
-> ofX x A1
-> ofX (A2 x) (TYPE L)).
ofX@ : ofX (M1 @ M2) (B M2)
<- ofX M1 A1
<- ofX M2 A2
<- mu0 A1 (fun A2' B)
<- ~a A2 M2 A2' C
<- (|+ C -> #).
ofXlam : ofX (lam A T) (fun A B)
<- ofX A (TYPE L)
<- ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A [x] true)
-> mu0X x x
-> tequivX x x true
-> ({T'} tequivaX x T' x true)
-> ofX x A
-> ofX (T x) (B x)).
ofXfst : ofX (fst T) A1
<- ofX T T'
<- mu0 T' (sig A1 A2).
ofXsnd : ofX (snd T) (A2 (fst T))
<- ofX T T'
<- mu0 T' (sig A1 A2).
ofX, : ofX (T1 , T2) (sig A1 A2)
<- ofX T1 A1
<- ofX T2 (A2 A1).
ofX,d : ofX (M , T2) (def A1 M A2)
<- ofX T2 (A2 A1).
% Major restriction.
ofXsig : ofX (sig A B) (TYPE L)
<- ofX A (TYPE L)
<- ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A [x] true)
-> mu0X x x
-> tequivX x x true
-> ({T'} tequivaX x T' x true)
-> ofX x A -> ofX (B x) (TYPE L)).
ofXdef : ofX (def A M B) (TYPE L)
<- ofX A (TYPE L)
<- ofX M A
<- ({x:term} delta x M
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A [x] true)
-> mu0X x x
-> tequivX x x true
-> ({T'} tequivaX x T' x true)
-> ofX x A
-> ofX (B x) (TYPE L)).
% Provability. Section 7.
% Section 7.1.1
% This is a higher-order logical framework
% No structural rules necessary
% Section 7.1.2 The Cut Rule
cut : (|- M -> #)
-> (|+ M -> #)
-> of M T
-> ~ M bool C
-> (|+ C -> #)
-> #.
% Section 7.1.3 The Propositional Axioms
ax : (|- A -> |+ A -> #).
falsel : (|- false -> #).
truer : (|+ true -> #).
ctxformula : of A bool -> (|+ A -> #).
ctxdef : M1 === M2 -> (|+ eq @ t-eq @ A @ (M1 , M2) -> #).
ctxl : (|- A -> of A bool -> #)
-> (|- A -> #).
ctxr : (of (neg @ A) bool -> |+ A -> #)
-> (|+ A -> #).
% Works only if the invariant is that |+ |- contain delta expanded formulas.
% Context weakening is automatic.
% Section 7.1.5 The conditional rules.
ifl : (|- A -> |- B -> of A bool -> #)
-> (|- C -> of (neg @ A) bool -> |+ A -> #)
-> (|- (if @ t-if @ bool @ (A , B , C)) -> #).
ifr : (|- A -> of A bool -> |+ B -> #)
-> (of (neg @ A) bool -> |+ A -> |+ C -> #)
-> (|+ (if @ t-if @ bool @ (A , B , C)) -> #).
% Section 7.1.6 The equality rules
refl : of M A -> (|+ eq @ t-eq @ A @ (M , M) -> #).
repl- : (|- (F M) -> #) -> (|- (eq @ t-eq @ A @ M @ N) -> |- (F N) -> #).
repl+ : (|+ (F M) -> #) -> (|- (eq @ t-eq @ A @ M @ N) -> |+ (F N) -> #).
% Section 7.1.7 Boolean equality rules
repltrue : (|- A -> #)
<- (|- eq @ t-eq @ bool @ (A , true) -> #).
replfalse : (|+ A -> #)
<- (|- eq @ t-eq @ bool @ (A , false) -> #).
truefalse : |- eq @ t-eq @ bool @ (true , false) -> #.
% Section 7.1.8 Reduction rules.
beta : |+ eq @ t-eq @ B @ ((lam A [x] M x) @ N , M N) -> #.
left : |+ eq @ t-eq @ B @ (fst (M1 , M2) , M1) -> #.
right : |+ eq @ t-eq @ B @ (snd (M1 , M2) , M2) -> #.
% Section 7.1.9 Existentionality.
funext : ({x:term} delta x x
-> ({N:term} con x N x)
-> muX x x
-> piX x (lam A [x] true)
-> mu0X x x
-> tequivX x x true
-> ({T'} tequivaX x T' x true)
-> ofX x A
-> (|+ eq @ t-eq @ (B x) @ (F @ x , G @ x)))
-> (|+ eq @ t-eq @ (fun A B) @ (F , G) -> #).
tupext : (|+ eq @ t-eq @ A @ (fst M , fst N))
-> (|+ eq @ t-eq @ (B (fst M)) @ (snd M , snd N))
-> (|+ eq @ t-eq @ (sig A B) @ (M , N) -> #).
% Section 7.1.10 Type Constraint rule
typepred : #
<- of M T
<- pi A C
<- (|- A -> #).
% Derived rules of inference added to shrink proof size
andI : (|+ A -> #) -> (|+ B -> #) -> (|+ and @ (A , B) -> #) .
%block typing : some {M:term -> term}
{A:term}
block {x:term}
{d:delta x (M x)}
{n:{N:term} con x N x}
{m:muX x x}
{s:piX x (lam A [x] true)}
{m0:mu0X x x}
{t: tequivX x x true}
{ta:{T':term } tequivaX x T' x true}
{ofx: ofX x A}.
%block negative : some {A:term}
block {n : |- A}.
%block positive : some {A:term}
block {p : |+ A}.
%block assume : some {U:term}
block {u : of U bool}.
%worlds (typing | negative | positive | assume) (ofX _ _) (of _ _) (#) (|+ _) (|- _).
% Examples
% Example 2.5
%solve ex2-5-3 : of ((bool & bool) => bool) uni1.
ex2-5-3 : of (bool & bool => bool) uni1
= ofbase
(ofXfun
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x (lam (sig bool ([x4:term] bool)) ([x4:term] true))]
[x5:mu0X x x] [x6:tequivX x x true]
[x7:{T':term} tequivaX x T' x true]
[x8:ofX x (sig bool ([x8:term] bool))] ofX-bool)
(ofXsig
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x (lam bool ([x5:term] true))] [x5:mu0X x x]
[x6:tequivX x x true] [x7:{T':term} tequivaX x T' x true]
[x8:ofX x bool] ofX-bool)
ofX-bool))
d-type.
%solve ex2-5-4 : of (true , false) (bool & bool).
ex2-5-4 : of (true , false) (bool & bool)
= ofbase (ofX, ofX-false ofX-true)
(d-sig ([x:term] [x1:delta x x] d-bool) d-bool).
%solve ex2-5-5 : of (fst (true , false)) bool.
ex2-5-5 : of (fst (true , false)) bool
= ofbase
(ofXfst (mu0-mu0X mu0X-sig (d-sig ([x:term] [x1:delta x x] x1) d-bool))
(ofX, ofX-false ofX-true))
d-bool.
%solve ex2-5-6 : of (lam bool ([x] true)) (bool => bool).
ex2-5-6 : of (lam bool ([x:term] true)) (bool => bool)
= ofbase
(ofXlam
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x (lam bool ([x4:term] true))] [x5:mu0X x x]
[x6:tequivX x x true] [x7:{T':term} tequivaX x T' x true]
[x8:ofX x bool] ofX-true)
ofX-bool)
(d-fun ([x:term] [x1:delta x x] d-bool) d-bool).
% Example 3.11
%solve ex3-11-0: of (set int [i] true) uni1.
ex3-11-0 : of (set int ([i:term] true)) uni1
= ofbase
(ofXset
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x (lam int ([x4:term] true))] [x5:mu0X x x]
[x6:tequivX x x true] [x7:{T':term} tequivaX x T' x true]
[x8:ofX x int] ofX-true)
ofX-int)
d-type.
%{ex3-11-0 : of (set int ([i:term] true)) TYPE
= ofbase
(ofXset
([x:term] [x1:delta x x] [x2:{N:term} con x N x] [x3:muX x x]
[x4:piX x (lam int ([x4:term] true))] [x5:mu0X x x]
[x6:tequivX x x true] [x7:{T':term} tequivaX x T' x true]
[x8:ofX x int] ofX-true)
ofX-int)
d-type (d-set d-int).
}%
ex3-11-1-a : {i:term} ofX i int -> ofX (i , zero-int) (int & int)
= [i][u] ofX, ofX-zero-int u.
%solve ex3-11-1-b : mu0 (int & int => bool) (T1 => bool).
ex3-11-1-b : mu0 (int & int => bool) (sig int ([x:term] int) => bool)
= mu0-mu0X mu0X-fun
(d-fun ([x:term] [x1:delta x x] d-bool)
(d-sig ([x:term] [x1:delta x x] d-int) d-int)).
%solve ex3-11-1-c : {i:term} ({T'} tequivaX i T' i true)
-> ({N:term} con i N i)
-> ~a (int & int) (i , zero-int) (int & int) T1.
%abbrev
ex3-11-1-c :
{i:term}
({T':term} tequivaX i T' i true) -> ({N:term} con i N i)
-> ~a (int & int) (i , zero-int) (int & int) (and @ (true , true))
= [i:term] [x:{T':term} tequivaX i T' i true] [x1:{N:term} con i N i]
~base
(tequivaX-tequiva (tequivaX-sig tequivaX-int tequivaX-int)
(d-sig ([x2:term] [x3:delta x2 x2] d-int) d-int)
(d-sig ([x3:term] [x2:delta x3 x3] d-int) d-int))
(mu-muX
(muX-sig
([x4:term] [x2:delta x4 x4] [x3:{N:term} con x4 N x4]
[x5:muX x4 x4] [x6:piX x4 (lam int ([x6:term] true))]
[x7:mu0X x4 x4] con-int)
piX-int muX-int)
(d-sig ([x7:term] [x2:delta x7 x7] d-int) d-int))
(mu-muX
(muX-sig
([x8:term] [x2:delta x8 x8] [x3:{N:term} con x8 N x8]
[x4:muX x8 x8] [x5:piX x8 (lam int ([x9:term] true))]
[x6:mu0X x8 x8] con-int)
piX-int muX-int)
(d-sig ([x10:term] [x2:delta x10 x10] d-int) d-int)).
ex3-11-d : (|+ and @ (true , true) -> #)
= andI truer truer.
ex3-11-1: of (set int [i] (less-int @ (i , zero-int))) uni1
= ofbase (ofXset ([x:term] [x2:delta x x] [n][m][p][m0]
[t:tequivX x x true]
[ta:{T'} tequivaX x T' x true][x1:ofX x int]
(ofX@
ex3-11-d
(ex3-11-1-c x ta n)
ex3-11-1-b
(ex3-11-1-a x x1) ofX-less-int )) ofX-int)
d-type.
% Example 4.10
ex-4-10-1b : ofX ((true , true)) (bool & bool)
= ofX, ofX-true ofX-true.
%solve ex-4-10-1c : mu0 ((bool & bool) => bool) ((bool & bool) => bool).
%solve ex-4-10-1-d : {x:term} ({T'} tequivaX x T' x true) -> {x':term} ({T'} tequivaX x' T' x' true) -> ~a (bool & bool) (x , x') (bool & bool) T1.
ex-4-10-1-e : ofX imp (bool & bool => bool). % Change d-set or ofXset
ex-4-10-1 : of (sig bool [x] set bool [y] imp @ (x , y)) uni1
= ofbase (ofXsig ([x][d][n][m][p][m0][t][ta][u]
ofXset ([x'][d'][n'][m'][p'][m0'][t'][ta'] [u']
((ofX@ (andI truer truer)
(ex-4-10-1-d x ta x' ta')
ex-4-10-1c (ofX, u' u) ex-4-10-1-e))) ofX-bool) ofX-bool)
d-type.
%solve ex-4-10-2a : delta (fun bool ([x:term] set bool ([y:term] imp @ (x , y)))) T1.
ex-4-10-2 : of (fun bool [x] set bool [y] imp @ (x , y)) uni1
= ofbase (ofXfun ([x][d][n][m][p][m0][t][ta][u]
ofXset ([x'][d'][n'][m'][p'][m0'][t'][ta'] [u']
(ofX@ (andI truer truer)
(ex-4-10-1-d x ta x' ta')
ex-4-10-1c (ofX, u' u) ex-4-10-1-e)) ofX-bool) ofX-bool)
d-type.
% Example 5.6
theory-reals = sig uni1
[real] sig real
[zero] sig ((real & real) => bool)
[<= : term] def uni1 (set real ([x] <= @ (zero , x)))
[noneg-real] sig noneg-real
[1] *.
% solve X : of theory-reals uni2.
% Constants are not expanded automatically.
%{ Example 5.6, 5.8 Another time.
reals : term.
ofX-reals : ofX reals theory-reals.
d-reals : delta reals reals.
con-reals : con reals _ reals.
muX-reals : muX reals reals.
piX-relas : piX reals (lam reals [x] true).
mu0X-reals: mu0X reals reals.
tequivX-reals : tequivX reals reals true.
tequivaX-reals : tequivaX reals _ reals true.
d-reals : reals === (lam theory-reals [t :term] fst t).
zero-reals : term.
d-zero-reals : zero-reals === (lam theory-reals [t :term] fst (snd t)).
<=-reals : term.
d-<=-reals : <=-reals === (lam theory-reals [t :term] snd (snd t)).
% solve td11 : of (zero @ reals) (fst reals).
% solve td12 : of (<= @ t1) _.
}%
%{ Finish Example 2.19 last part }%
%{ Verify Definition 6.2 }%