Tutorial/Embedding_of_logics_deep.ml

   1 let string_INDUCT,string_RECURSION = define_type
   2  "string = String num";;
   3
   4 parse_as_infix("&&",(16,"right"));;
   5 parse_as_infix("||",(15,"right"));;
   6 parse_as_infix("-->",(14,"right"));;
   7 parse_as_infix("<->",(13,"right"));;
   8
   9 parse_as_prefix "Not";;
  10 parse_as_prefix "Box";;
  11 parse_as_prefix "Diamond";;
  12
  13 let form_INDUCT,form_RECURSION = define_type
  14  "form = False
  15        | True
  16        | Atom string
  17        | Not form
  18        | && form form
  19        | || form form
  20        | --> form form
  21        | <-> form form
  22        | Box form
  23        | Diamond form";;
  24
  25 let holds = define
  26  `(holds (W,R) V False w <=> F) /\
  27   (holds (W,R) V True w <=> T) /\
  28   (holds (W,R) V (Atom a) w <=> V a w) /\
  29   (holds (W,R) V (Not p) w <=> ~(holds (W,R) V p w)) /\
  30   (holds (W,R) V (p && q) w <=> holds (W,R) V p w /\ holds (W,R) V q w) /\
  31   (holds (W,R) V (p || q) w <=> holds (W,R) V p w \/ holds (W,R) V q w) /\
  32   (holds (W,R) V (p --> q) w <=> holds (W,R) V p w ==> holds (W,R) V q w) /\
  33   (holds (W,R) V (p <-> q) w <=> holds (W,R) V p w <=> holds (W,R) V q w) /\
  34   (holds (W,R) V (Box p) w <=>
  35         !w'. w' IN W /\ R w w' ==> holds (W,R) V p w') /\
  36   (holds (W,R) V (Diamond p) w <=>
  37         ?w'. w' IN W /\ R w w' /\ holds (W,R) V p w')`;;
  38
  39 let holds_in = new_definition
  40  `holds_in (W,R) p = !V w. w IN W ==> holds (W,R) V p w`;;
  41
  42 parse_as_infix("|=",(11,"right"));;
  43
  44 let valid = new_definition
  45  `L |= p <=> !f. L f ==> holds_in f p`;;
  46
  47 let S4 = new_definition
  48  `S4(W,R) <=> ~(W = {}) /\ (!x y. R x y ==> x IN W /\ y IN W) /\
  49               (!x. x IN W ==> R x x) /\
  50               (!x y z. R x y /\ R y z ==> R x z)`;;
  51
  52 let LTL = new_definition
  53  `LTL(W,R) <=> (W = UNIV) /\ !x y:num. R x y <=> x <= y`;;
  54
  55 let GL = new_definition
  56  `GL(W,R) <=> ~(W = {}) /\ (!x y. R x y ==> x IN W /\ y IN W) /\
  57               WF(\x y. R y x) /\ (!x y z:num. R x y /\ R y z ==> R x z)`;;
  58
  59 let MODAL_TAC =
  60   REWRITE_TAC[valid; FORALL_PAIR_THM; holds_in; holds] THEN MESON_TAC[];;
  61
  62 let MODAL_RULE tm = prove(tm,MODAL_TAC);;
  63
  64 let TAUT_1 = MODAL_RULE `L |= Box True`;;
  65 let TAUT_2 = MODAL_RULE `L |= Box(A --> B) --> Box A --> Box B`;;
  66 let TAUT_3 = MODAL_RULE `L |= Diamond(A --> B) --> Box A --> Diamond B`;;
  67 let TAUT_4 = MODAL_RULE `L |= Box(A --> B) --> Diamond A --> Diamond B`;;
  68 let TAUT_5 = MODAL_RULE `L |= Box(A && B) --> Box A && Box B`;;
  69 let TAUT_6 = MODAL_RULE `L |= Diamond(A || B) --> Diamond A || Diamond B`;;
  70
  71 let HOLDS_FORALL_LEMMA = prove
  72  (`!W R P. (!A V. P(holds (W,R) V A)) <=> (!p:W->bool. P p)`,
  73   REPEAT GEN_TAC THEN EQ_TAC THENL [DISCH_TAC THEN GEN_TAC; SIMP_TAC[]] THEN
  74   POP_ASSUM(MP_TAC o SPECL [`Atom a`; `\a:string. (p:W->bool)`]) THEN
  75   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
  76   REWRITE_TAC[holds] THEN REWRITE_TAC[ETA_AX]);;
  77
  78 let MODAL_SCHEMA_TAC =
  79   REWRITE_TAC[holds_in; holds] THEN MP_TAC HOLDS_FORALL_LEMMA THEN
  80   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
  81   DISCH_THEN(fun th -> REWRITE_TAC[th]);;
  82
  83 let MODAL_REFL = prove
  84  (`!W R. (!w:W. w IN W ==> R w w) <=> !A. holds_in (W,R) (Box A --> A)`,
  85   MODAL_SCHEMA_TAC THEN MESON_TAC[]);;
  86
  87 let MODAL_TRANS = prove
  88  (`!W R. (!w w' w'':W. w IN W /\ w' IN W /\ w'' IN W /\
  89                        R w w' /\ R w' w'' ==> R w w'') <=>
  90          (!A. holds_in (W,R) (Box A --> Box(Box A)))`,
  91   MODAL_SCHEMA_TAC THEN MESON_TAC[]);;
  92
  93 let MODAL_SERIAL = prove
  94  (`!W R. (!w:W. w IN W ==> ?w'. w' IN W /\ R w w') <=>
  95          (!A. holds_in (W,R) (Box A --> Diamond A))`,
  96   MODAL_SCHEMA_TAC THEN MESON_TAC[]);;
  97
  98 let MODAL_SYM = prove
  99  (`!W R. (!w w':W. w IN W /\ w' IN W /\ R w w' ==> R w' w) <=>
 100          (!A. holds_in (W,R) (A --> Box(Diamond A)))`,
 101   MODAL_SCHEMA_TAC THEN EQ_TAC THENL [MESON_TAC[]; REPEAT STRIP_TAC] THEN
 102   FIRST_X_ASSUM(MP_TAC o SPECL [`\v:W. v = w`; `w:W`]) THEN ASM_MESON_TAC[]);;
 103
 104 let MODAL_WFTRANS = prove
 105  (`!W R. (!x y z:W. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z) /\
 106          WF(\x y. x IN W /\ y IN W /\ R y x) <=>
 107          (!A. holds_in (W,R) (Box(Box A --> A) --> Box A))`,
 108   MODAL_SCHEMA_TAC THEN REWRITE_TAC[WF_IND] THEN EQ_TAC THEN
 109   STRIP_TAC THEN REPEAT CONJ_TAC THENL
 110    [REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC;
 111     X_GEN_TAC `w:W` THEN FIRST_X_ASSUM(MP_TAC o SPECL
 112      [`\v:W. v IN W /\ R w v /\ !w''. w'' IN W /\ R v w'' ==> R w w''`; `w:W`]);
 113     X_GEN_TAC `P:W->bool` THEN DISCH_TAC THEN
 114     FIRST_X_ASSUM(MP_TAC o SPEC `\x:W. !w:W. x IN W /\ R w x ==> P x`) THEN
 115     MATCH_MP_TAC MONO_FORALL] THEN
 116   ASM_MESON_TAC[]);;