1(*
2 * Copyright 1991-1995  University of Cambridge (Author: Monica Nesi)
3 * Copyright 2016-2017  University of Bologna   (Author: Chun Tian)
4 *)
5
6structure WeakEQLib :> WeakEQLib =
7struct
8
9open HolKernel Parse boolLib bossLib;
10
11open CCSLib CCSTheory StrongEQLib WeakEQTheory;
12
13infix 0 OE_THENC OE_ORELSEC;
14
15(******************************************************************************)
16(*                                                                            *)
17(*              Basic functions and conversions for rewriting                 *)
18(*               with the laws for observational equivalence                  *)
19(*                                                                            *)
20(******************************************************************************)
21
22(* Define OE_SYM such that, when given a theorem A |- WEAK_EQUIV t1 t2,
23   returns the theorem A |- WEAK_EQUIV t2 t1. *)
24fun OE_SYM thm = MATCH_MP WEAK_EQUIV_SYM thm;
25
26(* Define OE_TRANS such that, when given the theorems thm1 and thm2, applies
27   WEAK_EQUIV_TRANS on them, if possible.
28 *)
29fun OE_TRANS thm1 thm2 =
30    if rhs_tm thm1 ~~ lhs_tm thm2 then
31      MATCH_MP WEAK_EQUIV_TRANS (CONJ thm1 thm2)
32    else
33      failwith "transitivity of observation equivalence not applicable";
34
35(* When applied to a term "t: CCS", the conversion OE_ALL_CONV returns the
36   theorem: |- WEAK_EQUIV t t
37 *)
38fun OE_ALL_CONV t = ISPEC t WEAK_EQUIV_REFL;
39
40(* Define the function OE_THENC. *)
41fun op OE_THENC ((c1, c2) :conv * conv) :conv =
42  fn t => let
43      val thm1 = c1 t;
44      val thm2 = c2 (rhs_tm thm1)
45  in OE_TRANS thm1 thm2 end;
46
47(* Define the function OE_ORELSEC. *)
48fun op OE_ORELSEC ((c1, c2) :conv * conv) :conv =
49  fn t => c1 t handle HOL_ERR _ => c2 t;
50
51(* Define the function OE_REPEATC *)
52fun OE_REPEATC (c :conv) (t :term) :thm =
53  ((c OE_THENC (OE_REPEATC c)) OE_ORELSEC OE_ALL_CONV) t;
54
55(* Convert a conversion for the application of the laws for STRONG_EQUIV to a
56   tactic applying the laws for WEAK_EQUIV (i.e. c is a conversion for strong
57   equivalence). *)
58fun OE_LHS_CONV_TAC (c :conv) :tactic =
59  fn (asl, w) => let
60      val (opt, t1, t2) = args_equiv w
61  in
62      if opt ~~ ``WEAK_EQUIV`` then
63          let val thm = MATCH_MP STRONG_IMP_WEAK_EQUIV ((S_DEPTH_CONV c) t1);
64              val (t1', t') = args_thm thm (* t1' = t1 *)
65          in
66              if (t' ~~ t2) then
67                  ([], fn [] => OE_TRANS thm (ISPEC t' WEAK_EQUIV_REFL))
68              else
69                  ([(asl, ``WEAK_EQUIV ^t' ^t2``)],
70                   fn [thm'] => OE_TRANS thm thm')
71          end
72      else
73          failwith "the goal is not an WEAK_EQUIV relation"
74  end;
75
76fun OE_RHS_CONV_TAC (c :conv) :tactic =
77  fn (asl,w) => let
78      val (opt, t1, t2) = args_equiv w
79  in
80      if (opt ~~ ``WEAK_EQUIV``) then
81          let val thm = MATCH_MP STRONG_IMP_WEAK_EQUIV ((S_DEPTH_CONV c) t2);
82              val (t2', t') = args_thm thm (* t2' = t2 *)
83          in
84              if t' ~~ t1 then
85                  ([], fn [] => OE_SYM thm)
86              else
87                  ([(asl, ``WEAK_EQUIV ^t1 ^t'``)],
88                   fn [thm'] => OE_TRANS thm' (OE_SYM thm))
89          end
90      else
91          failwith "the goal is not an WEAK_EQUIV relation"
92  end;
93
94val STRONG_IMP_WEAK_EQUIV_RULE =
95    STRIP_FORALL_RULE (MATCH_MP STRONG_IMP_WEAK_EQUIV);
96
97end (* struct *)
98
99(* last updated: Jun 18, 2017 *)
100