Tutorial/Embedding_of_logics_shallow.ml

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