The Theory gst-fun
Parents

gst-ax
Children

gst-listsgst-recgst-fixpgst-sumprod
Constants
$
'a GS 'a GS 'a GS
snd
'a GS 'a GS
fst
'a GS 'a GS
$
'a GS 'a GS 'a GS
$
'a GS 'a GS 'a GS
rel
'a GS BOOL
$o
'a GS 'a GS 'a GS
dom
'a GS 'a GS
ran
'a GS 'a GS
field
'a GS 'a GS
fun
'a GS BOOL
$
'a GS 'a GS 'a GS
$
'a GS 'a GS 'a GS
$g
('a GS 'a GS) 'a GS 'a GS
$g
'a GS 'a GS 'a GS
id
'a GS 'a GS
Fixity



Binder:g Infix 240: Infix 250:og
Definitions
s t u v s t = u v s = u t = v
fst
snd
s t fst (s t) = s snd (s t) = t
s t e
e s t ( l r l s r t e = l r)
s t s t = (s t)
rel
x rel x ( y y x ( s t y = s t))
o
f g
f o g
= Image
( p fst (fst p) snd (snd p))
(Sep (g f) ( p snd (fst p) = fst (snd p)))
dom
x dom x = Image fst x
ran
x ran x = Image snd x
field
s e e field s e dom s e ran s
fun
x
fun x
rel x
( s t u s u x s t x u = t)
s t s t = Sep (s t) fun
s t s t = Sep (s t) ( r dom r = s)
g
f s
$g f s
= Sep (s Image f s) ( p snd p = f (fst p))
g
f x
f g x
= (if y x y f then y x y f else f)
id
s id s = Sep (s s) ( x fst x = snd x)
Theorems
fs_thm
s t p p s t fst p snd p = p
v_thm
p s t p s t fst p s snd p t
_thm
l r s t l r s t l s r t
_thm
s t r r s t r s t
_thm
s t s t
fs_thm1
p r s t p r r s t fst p snd p = p
_thm
p r s t p r r s t fst p s snd p t
rel__thm
rel
dom__thm
dom =
ran__thm
ran =
field__thm
field =
fun__thm
fun
_thm
s t s t
_thm
s t f f s t
_thm
s t t
_thm
s t ( x x t) ( f f s t)
app_thm1
f x (1 y x y f) x f g x f
app_thm2
f x y fun f x y f f g x = y
g_thm
f s t u f s t u dom f f g u t
g_thm1
f s t u f s t u s f g u t
_thm
f s t u f s t f dom f t
id_thm1
s x x id s ( y y s x = y y)
id_ap_thm
s x x s id s g x = x
id_thm1
s t u s t u id s t u
id_thm2
s t u s t id s t t

up quick index © RBJ