modal.ml

(* ========================================================================= *)
(* Syntax and semantics of modal logic.                                      *)
(*                                                                           *)
(* (c) Copyright, Marco Maggesi, Cosimo Perini Brogi 2020-2022.              *)
(* (c) Copyright, Antonella Bilotta, Marco Maggesi,                          *)
(*                Cosimo Perini Brogi, Leonardo Quartini 2024.               *)
(* (c) Copyright, Antonella Bilotta, Marco Maggesi,                          *)
(*                Cosimo Perini Brogi 2025-2026.                             *)
(*                                                                           *)
(* Part of this code is copied or adapted from                               *)
(*   John Harrison (2017) The HOL Light Tutorial.                            *)
(* ========================================================================= *)

needs "HOLMS/misc.ml";;

(* ------------------------------------------------------------------------- *)
(* Syntax of formulae.                                                       *)
(* ------------------------------------------------------------------------- *)

parse_as_infix("&&",(16,"right"));;
parse_as_infix("||",(15,"right"));;
parse_as_infix("-->",(14,"right"));;
parse_as_infix("<->",(13,"right"));;
parse_as_prefix "Not";;
parse_as_prefix "Box";;

let form_INDUCT,form_RECURSION = define_type
  "form = False
        | True
        | Atom string
        | Not form
        | && form form
        | || form form
        | --> form form
        | <-> form form
        | Box form";;

let form_CASES = prove_cases_thm form_INDUCT;;
let form_DISTINCT = distinctness "form";;
let form_INJ = injectivity "form";;

(* ----------------------------------------------------------------------- *)
(* Further operators.                                                      *)
(* ----------------------------------------------------------------------- *)

parse_as_prefix "Diam";;
parse_as_prefix "Dotbox";;

let diam_DEF = new_definition
  `Diam p = Not Box Not p`;;

let dotbox_DEF = new_definition
  `Dotbox p = (Box p && p)`;;

(* ------------------------------------------------------------------------- *)
(* Constants of modal formulas.                                              *)
(* ------------------------------------------------------------------------- *)

let form_ty = `:form`;;

let modal_atom_tm = `Atom`;;
let modal_true_tm = `True`;;
let modal_false_tm = `False`;;
let modal_not_tm = `(Not)`;;
let modal_conj_tm = `(&&)`;;
let modal_disj_tm = `(||)`;;
let modal_imp_tm = `(-->)`;;
let modal_iff_tm = `(<->)`;;
let modal_box_tm = `(Box)`;;
let modal_diam_tm = `(Diam)`;;
let modal_dotbox_tm = `(Dotbox)`;;

(* ------------------------------------------------------------------------- *)
(* OCaml procedure for analyzing and syntesis of modal formulas.             *)
(* ------------------------------------------------------------------------- *)

let mk_unop ftm = curry mk_comb ftm;;

let dest_unop ftm =
  let errstr = "dest_unop: "^string_of_term ftm in
  fun tm -> try if rator tm <> ftm then fail() else rand tm
            with Failure _ -> failwith errstr;;

let is_unop ftm = can (dest_unop ftm);;

let mk_modal_conj = mk_binop `(&&)`;;
let mk_modal_disj = mk_binop `(||)`;;
let mk_modal_imp = mk_binop `(-->)`;;
let mk_modal_iff = mk_binop `(<->)`;;

let dest_modal_conj = dest_binop `(&&)`;;
let dest_modal_disj = dest_binop `(||)`;;
let dest_modal_imp = dest_binop `(-->)`;;
let dest_modal_iff = dest_binop `(<->)`;;

let is_modal_conj = is_binop `(&&)`;;
let is_modal_disj = is_binop `(||)`;;
let is_modal_imp = is_binop `(-->)`;;
let is_modal_iff = is_binop `(<->)`;;

let mk_modal_atom = mk_unop `Atom`;;
let mk_modal_not = mk_unop `(Not)`;;
let mk_modal_box = mk_unop `(Box)`;;
let mk_modal_diam = mk_unop `(Diam)`;;
let mk_modal_dotbox = mk_unop `(Dotbox)`;;

let dest_modal_atom = dest_unop `Atom`;;
let dest_modal_not = dest_unop `(Not)`;;
let dest_modal_box = dest_unop `(Box)`;;
let dest_modal_diam = dest_unop `(Diam)`;;
let dest_modal_dotbox = dest_unop `(Dotbox)`;;

let is_modal_atom = is_unop `Atom`;;
let is_modal_not = is_unop `(Not)`;;
let is_modal_box = is_unop `(Box)`;;
let is_modal_diam = is_unop `(Diam)`;;
let is_modal_dotbox = is_unop `(Dotbox)`;;

let dest_modal_unop =
  let unops =
    [dest_modal_not; dest_modal_box; dest_modal_diam; dest_modal_dotbox] in
  fun tm -> try tryfind (fun f -> f tm) unops
            with Failure _ -> failwith "dest_modal_unop";;

let dest_modal_binop =
  let binops =
    [dest_modal_conj; dest_modal_disj; dest_modal_imp; dest_modal_iff] in
  fun tm -> try tryfind (fun f -> f tm) binops
            with Failure _ -> failwith "dest_modal_binop";;

let atomicals =
  let rec recur atoms tml =
    match tml with
    | [] -> setify atoms
    | h::t ->
        let atoms',tml' =
          try atoms,dest_modal_unop h::t with Failure _ ->
          try let l,r = dest_modal_binop h in
              atoms,l::r::t
          with Failure _ -> h::atoms,t in
        recur atoms' tml' in
  fun tm -> recur [] [tm];;

(* ------------------------------------------------------------------------- *)
(* Specialized induction tactics for formulas.                               *)
(* ------------------------------------------------------------------------- *)

let FORM_INDUCT_TAC : tactic =
  fun (asl,w) as gl ->
    let q = try let v,_ = dest_forall w in
                if type_of v = form_ty then v else fail()
            with Failure _ -> failwith "FORM_INDUCT_TAC" in
    let s = name_of q in
    let q1 = mk_var(s^"1",form_ty)
    and q2 = mk_var(s^"2",form_ty)
    and a = mk_var(s,string_ty) in
    let lab_tac = LABEL_TAC (s^"_hpind")
    and lab1_tac = LABEL_TAC (s^"1_hpind")
    and lab2_tac = LABEL_TAC (s^"2_hpind") in
    let intro1_tac = X_GEN_TAC q THEN DISCH_THEN lab_tac
    and intro2_tac = X_GEN_TAC q1 THEN X_GEN_TAC q2 THEN
                     DISCH_THEN (CONJUNCTS_THEN2 lab1_tac lab2_tac) in
    let tac =
      MATCH_MP_TAC form_INDUCT THEN REPEAT CONJ_TAC THENL
      [ALL_TAC; (* False *)
       ALL_TAC; (* True *)
       X_GEN_TAC a; (* Atom *)
       intro1_tac; (* Not *)
       intro2_tac; (* && *)
       intro2_tac; (* || *)
       intro2_tac; (* --> *)
       intro2_tac; (* <-> *)
       intro1_tac (* Box *)
      ] in
    tac gl;;

let GEN_FORM_INDUCT_TAC : term -> tactic =
  fun tm ->
    let has_var = partition (free_in tm o concl o snd) in
    let induct_tac = SPEC_TAC(tm,tm) THEN FORM_INDUCT_TAC in
    fun (asl,w) as gl ->
      let l1,l2 = has_var asl in
      if l1 = [] then induct_tac gl else
      (MP_TAC (end_itlist CONJ (map snd l1)) THEN induct_tac) (l2,w);;

(* ------------------------------------------------------------------------- *)
(* Kripke's Semantics of formulae.                                           *)
(* ------------------------------------------------------------------------- *)

let holds =
  let pth = prove
    (`(!WP. P WP) <=> (!W:W->bool R:W->W->bool. P (W,R))`,
     MATCH_ACCEPT_TAC FORALL_PAIR_THM) in
  (end_itlist CONJ o map (REWRITE_RULE[pth] o GEN_ALL) o CONJUNCTS o
   new_recursive_definition form_RECURSION)
  `(holds WR V False (w:W) <=> F) /\
   (holds WR V True w <=> T) /\
   (holds WR V (Atom s) w <=> V s w) /\
   (holds WR V (Not p) w <=> ~(holds WR V p w)) /\
   (holds WR V (p && q) w <=> holds WR V p w /\ holds WR V q w) /\
   (holds WR V (p || q) w <=> holds WR V p w \/ holds WR V q w) /\
   (holds WR V (p --> q) w <=> holds WR V p w ==> holds WR V q w) /\
   (holds WR V (p <-> q) w <=> holds WR V p w <=> holds WR V q w) /\
   (holds WR V (Box p) w <=>
    !w'. w' IN FST WR /\ SND WR w w' ==> holds WR V p w')`;;

let holds_in = new_definition
  `holds_in (W,R) p <=> !V w:W. w IN W ==> holds (W,R) V p w`;;

parse_as_infix("|=",(11,"right"));;

let valid = new_definition
  `L |= p <=> !f:(W->bool)#(W->W->bool). f IN L ==> holds_in f p`;;

(* ------------------------------------------------------------------------- *)
(* Some model-theoretic lemmas.                                              *)
(* ------------------------------------------------------------------------- *)

let MODAL_TAC =
  REWRITE_TAC[valid; FORALL_PAIR_THM; holds_in; holds] THEN MESON_TAC[];;

let MODAL_RULE tm = prove(tm,MODAL_TAC);;

let HOLDS_FORALL_LEMMA = prove
 (`!W:W->bool R P. (!p V. P (holds (W,R) V p)) <=> (!U. P U)`,
  REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN
  INTRO_TAC "hp; !U" THEN
  SUBGOAL_THEN `P (\w:W. holds (W,R) (\a. U) (Atom a) w):bool`
    (MP_TAC o REWRITE_RULE[holds]) THEN
  ASM_REWRITE_TAC[ETA_AX]);;

let MODAL_SCHEMA_TAC =
  REWRITE_TAC[holds_in; holds] THEN MP_TAC HOLDS_FORALL_LEMMA THEN
  REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
  DISCH_THEN(fun th -> REWRITE_TAC[th]);;

(* ------------------------------------------------------------------------- *)
(* Subformulas.                                                              *)
(* ------------------------------------------------------------------------- *)

let IN_MINOR_RULES,IN_MINOR_INDUCT,IN_MINOR_CASES = new_inductive_set
  `(!p. p IN MINOR (Not p)) /\
   (!p q. p IN MINOR (p && q)) /\
   (!p q. q IN MINOR (p && q)) /\
   (!p q. p IN MINOR (p || q)) /\
   (!p q. q IN MINOR (p || q)) /\
   (!p q. p IN MINOR (p --> q)) /\
   (!p q. q IN MINOR (p --> q)) /\
   (!p q. p IN MINOR (p <-> q)) /\
   (!p q. q IN MINOR (p <-> q)) /\
   (!p. p IN MINOR (Box p))`;;

let MINOR_CLAUSES = prove
 (`MINOR False = {} /\
   MINOR True = {} /\
   MINOR (Atom s) = {} /\
   (!p. MINOR (Not p) = {p}) /\
   (!p q. MINOR (p && q) = {p,q}) /\
   (!p q. MINOR (p || q) = {p,q}) /\
   (!p q. MINOR (p --> q) = {p,q}) /\
   (!p q. MINOR (p <-> q) = {p,q}) /\
   (!p. MINOR (Box p) = {p})`,
  REWRITE_TAC[EXTENSION; IN_INSERT; NOT_IN_EMPTY; IN_MINOR_CASES;
              distinctness "form"; injectivity "form"] THEN
  MESON_TAC[]);;

parse_as_infix("SUBFORMULA",get_infix_status "SUBSET");;

let SUBFORMULA = new_definition
  `(SUBFORMULA) = RTC (\p q. p IN MINOR q)`;;

let SUBFORMULA_REFL = prove
 (`!p. p SUBFORMULA p`,
  REWRITE_TAC[SUBFORMULA; RTC_REFL]);;

let SUBFORMULA_TRANS = prove
 (`!p q r. p SUBFORMULA q /\ q SUBFORMULA r ==> p SUBFORMULA r`,
  REWRITE_TAC[SUBFORMULA; RTC_TRANS]);;

let SUBFORMULA_CASES_L = prove
 (`!p q. p SUBFORMULA q <=> p = q \/ (?r. p SUBFORMULA r /\ r IN MINOR q)`,
  REWRITE_TAC[SUBFORMULA] THEN MESON_TAC[RTC_CASES_L]);;

let FINITE_SUBFORMULA = prove
 (`!p. FINITE {q | q SUBFORMULA p}`,
  MATCH_MP_TAC form_INDUCT THEN
  REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SUBFORMULA_CASES_L] THEN
  ASM_REWRITE_TAC[MINOR_CLAUSES; IN_INSERT; NOT_IN_EMPTY;
    SET_RULE `{x | x = a} = {a}`;
    SET_RULE `{q | q = a \/ P q} = a INSERT {q | P q}`;
    SET_RULE `{q | ?r. q SUBFORMULA r /\ r = a} = {q | q SUBFORMULA a}`;
    SET_RULE `{q | ?r. q SUBFORMULA r /\ (r = a0 \/ r = a1)} =
                       {q | q SUBFORMULA a0} UNION {q | q SUBFORMULA a1}`;
    EMPTY_GSPEC; FINITE_UNION;  FINITE_INSERT; FINITE_EMPTY]);;

let FINITE_SUBSET_SUBFORMULAS_LEMMA = prove
 (`!p. FINITE {A | A SUBSET {q | q SUBFORMULA p} UNION
                            {Not q | q SUBFORMULA p}}`,
  REWRITE_TAC[FINITE_POWERSET_EQ; FINITE_UNION; FINITE_SUBFORMULA] THEN
  REWRITE_TAC[SET_RULE `{Not q | q SUBFORMULA p} =
                        IMAGE (Not) {q | q SUBFORMULA p}`] THEN
  GEN_TAC THEN MATCH_MP_TAC FINITE_IMAGE THEN
  REWRITE_TAC[FINITE_SUBFORMULA]);;

let SUBFORMULA_INVERSION = prove
 (`(!p. p SUBFORMULA False <=> p = False) /\
   (!p. p SUBFORMULA True <=> p = True) /\
   (!p s. p SUBFORMULA (Atom s) <=> p = Atom s) /\
   (!p q. p SUBFORMULA (Not q) <=> p = Not q \/ p SUBFORMULA q) /\
   (!p q r. p SUBFORMULA (q && r) <=>
            p = q && r \/ p SUBFORMULA q \/ p SUBFORMULA r) /\
   (!p q r. p SUBFORMULA (q || r) <=>
            p = q || r \/ p SUBFORMULA q \/ p SUBFORMULA r) /\
   (!p q r. p SUBFORMULA (q --> r) <=>
            p = q --> r \/ p SUBFORMULA q \/ p SUBFORMULA r) /\
   (!p q r. p SUBFORMULA (q <-> r) <=>
            p = q <-> r \/ p SUBFORMULA q \/ p SUBFORMULA r) /\
   (!p q. p SUBFORMULA (Box q) <=> p = Box q \/ p SUBFORMULA q)`,
  REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
  GEN_REWRITE_TAC LAND_CONV [SUBFORMULA_CASES_L] THEN
  REWRITE_TAC[MINOR_CLAUSES; IN_INSERT; NOT_IN_EMPTY] THEN
  MESON_TAC[SUBFORMULA_REFL]);;

let SUBFORMULA_LIST = prove
 (`!p. ?X. NOREPETITION X /\ (!q. MEM q X <=> q SUBFORMULA p)`,
  GEN_TAC THEN EXISTS_TAC `list_of_set {q | q SUBFORMULA p}` THEN
  SIMP_TAC[FINITE_SUBFORMULA; MEM_LIST_OF_SET; IN_ELIM_THM] THEN
  SIMP_TAC[NOREPETITION_LIST_OF_SET; FINITE_SUBFORMULA]);;

(* ------------------------------------------------------------------------- *)
(* Cardinality of the type of formulae.                                      *)
(* ------------------------------------------------------------------------- *)

let COUNTABLE_FORM = prove
 (`COUNTABLE (:form)`,
  (DESTRUCT_TAC "@size. size" o prove_general_recursive_function_exists)
    `?depth.
       depth False = 0 /\
       depth True = 0 /\
       (!a. depth (Atom a) = 0) /\
       (!p. depth (Not p) = depth p + 1) /\
       (!p q. depth (p && q) = MAX (depth p) (depth q) + 1) /\
       (!p q. depth (p || q) = MAX (depth p) (depth q) + 1) /\
       (!p q. depth (p --> q) = MAX (depth p) (depth q) + 1) /\
       (!p q. depth (p <-> q) = MAX (depth p) (depth q) + 1) /\
       (!p. depth (Box p) = depth p + 1)` THEN
  ABBREV_TAC `u n = {p:form | p | size p < n}` THEN
  POP_ASSUM (LABEL_TAC "u") THEN
  SUBGOAL_THEN `(:form) = UNIONS {u n | n | n IN (:num)}` SUBST1_TAC THENL
  [REWRITE_TAC[EXTENSION; IN_UNIV; IN_UNIONS; IN_ELIM_THM] THEN
   X_GEN_TAC `p:form` THEN EXISTS_TAC `u (size (p:form)+1):form->bool` THEN
   REMOVE_THEN "u" (fun th -> REWRITE_TAC[GSYM th]) THEN
   REWRITE_TAC[IN_ELIM_THM; ARITH_RULE `m < m + 1`] THEN MESON_TAC[];
   ALL_TAC] THEN
  MATCH_MP_TAC COUNTABLE_UNIONS THEN CONJ_TAC THENL
  [MATCH_MP_TAC COUNTABLE_SUBSET THEN
   EXISTS_TAC `IMAGE u (:num):(form->bool)->bool` THEN
   SIMP_TAC[NUM_COUNTABLE; COUNTABLE_IMAGE] THEN
   REWRITE_TAC[SUBSET; FORALL_IN_GSPEC; IN_IMAGE; IN_UNIV] THEN
   MESON_TAC[];
   ALL_TAC] THEN
  REWRITE_TAC[FORALL_IN_GSPEC; IN_UNIV] THEN
  INDUCT_TAC THENL
  [REMOVE_THEN "u" (fun th -> REWRITE_TAC[GSYM th]) THEN
   REWRITE_TAC[ARITH_RULE `!n. ~(n < 0)`; EMPTY_GSPEC; COUNTABLE_EMPTY];
   POP_ASSUM (LABEL_TAC "ind")] THEN
  MATCH_MP_TAC COUNTABLE_SUBSET THEN
  EXISTS_TAC
    `u (n:num) UNION
     {True, False} UNION
     IMAGE Atom (:string) UNION
     IMAGE (Not) (u n) UNION
     IMAGE (\(op,p,q). op p q)
           ({(&&),(||),(-->),(<->)} CROSS (u n) CROSS (u n)) UNION
     IMAGE (Box) (u n)` THEN
  CONJ_TAC THENL
  [ASM_REWRITE_TAC[COUNTABLE_UNION; COUNTABLE_INSERT; COUNTABLE_EMPTY] THEN
   ASM_SIMP_TAC[COUNTABLE_IMAGE; COUNTABLE_STRING; COUNTABLE_CROSS;
                COUNTABLE_INSERT; COUNTABLE_EMPTY];
   ALL_TAC] THEN
  USE_THEN "u" (SUBST1_TAC o GSYM o SPEC `SUC n`) THEN
  REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN
  CLAIM_TAC "u_alt" `!p:form n:num. size p < n <=> p IN u n` THENL
  [USE_THEN "u" (fun th -> REWRITE_TAC[GSYM th]) THEN SET_TAC[]; ALL_TAC] THEN
  CLAIM_TAC "max"
    `!p q:form n:num. MAX (size p) (size q) < n <=> p IN u n /\ q IN u n` THENL
  [USE_THEN "u" (fun th -> REWRITE_TAC[GSYM th]) THEN
   SET_TAC[ARITH_RULE `!p q n. MAX p q < n <=> p < n /\ q < n`];
   ALL_TAC] THEN

  GEN_TAC THEN STRUCT_CASES_TAC (SPEC `p:form` (cases "form")) THEN
  HYP REWRITE_TAC "size" [LT_0; IN_UNION; IN_INSERT; NOT_IN_EMPTY;
                          distinctness "form"; GSYM ADD1; LT_SUC] THEN
  HYP REWRITE_TAC "u_alt max" [] THEN
  ASM_SIMP_TAC[FUN_IN_IMAGE; IN_UNIV] THEN
  REWRITE_TAC[IN_IMAGE; EXISTS_PAIR_THM; IN_CROSS; IN_INSERT; NOT_IN_EMPTY;
              distinctness "form"; injectivity "form"] THEN
  MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Bisimulation.                                                             *)
(* ------------------------------------------------------------------------- *)

let BISIMIMULATION = new_definition
  `BISIMIMULATION (W1,R1,V1) (W2,R2,V2) Z <=>
   (!w1:A w2:B.
      Z w1 w2
      ==> w1 IN W1 /\ w2 IN W2 /\
          (!a:string. V1 a w1 <=> V2 a w2) /\
          (!w1'. R1 w1 w1' ==> ?w2'. w2' IN W2 /\ Z w1' w2' /\ R2 w2 w2') /\
          (!w2'. R2 w2 w2' ==> ?w1'. w1' IN W1 /\ Z w1' w2' /\ R1 w1 w1'))`;;

let BISIMIMULATION_HOLDS = prove
 (`!W1 R1 V1 W2 R2 V2 Z p w1:A w2:B.
     BISIMIMULATION (W1,R1,V1) (W2,R2,V2) Z /\
     Z w1 w2
     ==> (holds (W1,R1) V1 p w1 <=> holds (W2,R2) V2 p w2)`,
  SUBGOAL_THEN
    `!W1 R1 V1 W2 R2 V2 Z.
       BISIMIMULATION (W1,R1,V1) (W2,R2,V2) Z
       ==> !p w1:A w2:B.
             Z w1 w2
             ==> (holds (W1,R1) V1 p w1 <=> holds (W2,R2) V2 p w2)`
    (fun th -> MESON_TAC[th]) THEN
  REPEAT GEN_TAC THEN REWRITE_TAC[BISIMIMULATION] THEN DISCH_TAC THEN
  MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[holds] THEN ASM_MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Bisimilarity.                                                             *)
(* ------------------------------------------------------------------------- *)

let BISIMILAR = new_definition
  `BISIMILAR (W1,R1,V1) (W2,R2,V2) (w1:A) (w2:B) <=>
   ?Z. BISIMIMULATION (W1,R1,V1) (W2,R2,V2) Z /\ Z w1 w2`;;

let BISIMILAR_IN = prove
 (`!W1 R1 V1 W2 R2 V2 w1:A w2:B.
     BISIMILAR (W1,R1,V1) (W2,R2,V2) w1 w2 ==> w1 IN W1 /\ w2 IN W2`,
  REWRITE_TAC[BISIMILAR; BISIMIMULATION] THEN MESON_TAC[]);;

let BISIMILAR_HOLDS = prove
 (`!W1 R1 V1 W2 R2 V2 w1:A w2:B.
     BISIMILAR (W1,R1,V1) (W2,R2,V2) w1 w2
     ==> (!p. holds (W1,R1) V1 p w1 <=> holds (W2,R2) V2 p w2)`,
  REWRITE_TAC[BISIMILAR] THEN MESON_TAC[BISIMIMULATION_HOLDS]);;

let BISIMILAR_HOLDS_IN = prove
 (`!W1 R1 W2 R2.
     (!V1 w1:A. ?V2 w2:B. BISIMILAR (W1,R1,V1) (W2,R2,V2) w1 w2)
     ==> (!p. holds_in (W2,R2) p ==> holds_in (W1,R1) p)`,
  REWRITE_TAC[holds_in] THEN MESON_TAC[BISIMILAR_HOLDS; BISIMILAR_IN]);;

let BISIMILAR_VALID = prove
 (`!L1 L2 .
    (!W1 R1 V1 w1:A.
       (W1,R1) IN L1 /\ w1 IN W1
       ==> ?W2 R2 V2 w2:B.
             (W2,R2) IN L2 /\
             BISIMILAR (W1,R1,V1) (W2,R2,V2) w1 w2)
    ==> (!p. L2 |= p ==> L1 |= p)`,
  REWRITE_TAC[valid; holds_in; FORALL_PAIR_THM] THEN
  MESON_TAC[BISIMILAR_HOLDS; BISIMILAR_IN]);;