1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
parse_as_prefix "Not";;
parse_as_infix("&&",(16,"right"));;
parse_as_infix("||",(15,"right"));;
parse_as_infix("-->",(14,"right"));;
parse_as_infix("<->",(13,"right"));;
let false_def = define `False = \t:num. F`;;
let true_def = define `True = \t:num. T`;;
let not_def = define `Not p = \t:num. ~(p t)`;;
let and_def = define `p && q = \t:num. p t /\ q t`;;
let or_def = define `p || q = \t:num. p t \/ q t`;;
let imp_def = define `p --> q = \t:num. p t ==> q t`;;
let iff_def = define `p <-> q = \t:num. p t <=> q t`;;
let forever = define `forever p = \t:num. !t'. t <= t' ==> p t'`;;
let sometime = define `sometime p = \t:num. ?t'. t <= t' /\ p t'`;;
let next = define `next p = \t:num. p(t + 1)`;;
parse_as_infix("until",(17,"right"));;
let until = define
`p until q =
\t:num. ?t'. t <= t' /\ (!t''. t <= t'' /\ t'' < t' ==> p t'') /\ q t'`;;
|
