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