1(*
2 * Copyright 1991-1995  University of Cambridge (Author: Monica Nesi)
3 * Copyright 2016-2017  University of Bologna   (Author: Chun Tian)
4 *)
5
6structure StrongEQLib :> StrongEQLib =
7struct
8
9open HolKernel Parse boolLib bossLib;
10
11open IndDefRules;
12open CCSLib CCSTheory CCSSyntax StrongEQTheory;
13
14infixr 0 S_THENC S_ORELSEC;
15
16(******************************************************************************)
17(*                                                                            *)
18(*      Basic functions and conversions for rewriting with                    *)
19(*        the CCS laws for strong equivalence (basic_fun.ml)                  *)
20(*                                                                            *)
21(******************************************************************************)
22
23(* Define S_SYM such that, when given a theorem A |- STRONG_EQUIV t1 t2,
24   returns the theorem A |- STRONG_EQUIV t2 t1. *)
25fun S_SYM thm = MATCH_MP STRONG_EQUIV_SYM thm;
26
27(* Define S_TRANS such that, when given the theorems thm1 and thm2, applies
28   STRONG_EQUIV_TRANS on them, if possible. *)
29fun S_TRANS thm1 thm2 =
30    if rhs_tm thm1 ~~ lhs_tm thm2 then
31       MATCH_MP STRONG_EQUIV_TRANS (CONJ thm1 thm2)
32    else
33       failwith "transitivity of strong equivalence not applicable";
34
35(* When applied to a term "t: CCS", the conversion S_ALL_CONV returns the
36   theorem: |- STRONG_EQUIV t t *)
37fun S_ALL_CONV t = ISPEC t STRONG_EQUIV_REFL;
38
39fun op S_THENC ((c1, c2) :conv * conv) :conv =
40  fn t => let
41      val thm1 = c1 t;
42      val thm2 = c2 (rhs_tm thm1)
43  in
44      S_TRANS thm1 thm2
45  end;
46
47fun op S_ORELSEC ((c1, c2) :conv * conv) :conv =
48  fn t => c1 t handle HOL_ERR _ => c2 t;
49
50fun S_REPEATC (c :conv) (t :term) :thm =
51  ((c S_THENC (S_REPEATC c)) S_ORELSEC S_ALL_CONV) t;
52
53(* Convert a conversion for the application of the laws for STRONG_EQUIV to a tactic. *)
54fun S_LHS_CONV_TAC (c :conv) :tactic =
55  fn (asl, w) => let
56      val (opt, t1, t2) = args_equiv w
57  in
58    if opt ~~ ``STRONG_EQUIV`` then
59      let
60        val thm = c t1
61        val (t1', t') = args_thm thm (* t1' = t1 *)
62      in
63        if t' ~~ t2 then ([], fn _ => S_TRANS thm (ISPEC t' STRONG_EQUIV_REFL))
64        else
65          ([(asl, ``STRONG_EQUIV ^t' ^t2``)],
66           fn ths =>
67              case ths of [thm'] => S_TRANS thm thm'
68                        | _ => failwith "S_LHS_CONV_TAC: weird!")
69      end
70    else
71      failwith "the goal is not a STRONG_EQUIV relation"
72  end;
73
74fun S_RHS_CONV_TAC (c :conv) :tactic =
75  fn (asl, w) => let
76      val (opt, t1, t2) = args_equiv w
77  in
78      if (opt ~~ ``STRONG_EQUIV``) then
79          let val thm = c t2;
80              val (t2', t'') = args_thm thm (* t2' = t2 *)
81          in
82              if t'' ~~ t1 then ([], fn _ => S_SYM thm)
83              else
84                  ([(asl, ``STRONG_EQUIV ^t1 ^t''``)],
85                   fn [thm'] => S_TRANS thm' (S_SYM thm))
86          end
87      else
88          failwith "the goal is not a STRONG_EQUIV relation"
89  end;
90
91(******************************************************************************)
92(*                                                                            *)
93(*          Basic conversions and tactics for applying the laws for           *)
94(*                strong equivalence                                          *)
95(*                                                                            *)
96(******************************************************************************)
97
98fun S_SUB_CONV (c :conv) tm =
99  if is_prefix tm then
100      let val (u, P) = args_prefix tm;
101          val thm = c P
102      in
103          ISPEC u (MATCH_MP STRONG_EQUIV_SUBST_PREFIX thm)
104      end
105  else if is_sum tm then
106      let val (t1, t2) = args_sum tm;
107          val thm1 = c t1
108          and thm2 = c t2
109      in
110          MATCH_MP STRONG_EQUIV_PRESD_BY_SUM (CONJ thm1 thm2)
111      end
112  else if is_par tm then
113      let val (t1, t2) = args_par tm;
114          val thm1 = c t1
115          and thm2 = c t2
116      in
117          MATCH_MP STRONG_EQUIV_PRESD_BY_PAR (CONJ thm1 thm2)
118      end
119  else if is_restr tm then
120      let val (P, L) = args_restr tm;
121          val thm = c P
122      in
123          ISPEC L (MATCH_MP STRONG_EQUIV_SUBST_RESTR thm)
124      end
125  else if is_relab tm then
126      let val (P, rf) = args_relab tm;
127          val thm = c P
128      in
129          ISPEC rf (MATCH_MP STRONG_EQUIV_SUBST_RELAB thm)
130      end
131  else
132      S_ALL_CONV tm;
133
134fun S_DEPTH_CONV (c :conv) t =
135  S_SUB_CONV ((S_DEPTH_CONV c) S_THENC (S_REPEATC c)) t;
136
137fun S_TOP_DEPTH_CONV (c :conv) t =
138   ((S_REPEATC c) S_THENC
139    (S_SUB_CONV (S_TOP_DEPTH_CONV c)) S_THENC
140    ((c S_THENC (S_TOP_DEPTH_CONV c)) S_ORELSEC S_ALL_CONV))
141   t;
142
143(* Define the function S_SUBST for substitution in STRONG_EQUIV terms. *)
144fun S_SUBST thm tm :thm = let
145    val (ti, ti') = args_thm thm
146in
147    if tm ~~ ti then thm
148    else if is_prefix tm then
149        let val (u, t) = args_prefix tm;
150            val thm1 = S_SUBST thm t
151        in
152            ISPEC u (MATCH_MP STRONG_EQUIV_SUBST_PREFIX thm1)
153        end
154    else if is_sum tm then
155        let val (t1, t2) = args_sum tm;
156            val thm1 = S_SUBST thm t1
157            and thm2 = S_SUBST thm t2
158        in
159            MATCH_MP STRONG_EQUIV_PRESD_BY_SUM (CONJ thm1 thm2)
160        end
161    else if is_par tm then
162        let val (t1, t2) = args_par tm;
163            val thm1 = S_SUBST thm t1
164            and thm2 = S_SUBST thm t2
165        in
166            MATCH_MP STRONG_EQUIV_PRESD_BY_PAR (CONJ thm1 thm2)
167        end
168    else if is_restr tm then
169        let val (t, L) = args_restr tm;
170            val thm1 = S_SUBST thm t
171        in
172            ISPEC L (MATCH_MP STRONG_EQUIV_SUBST_RESTR thm1)
173        end
174    else if is_relab tm then
175        let val (t, rf) = args_relab tm;
176            val thm1 = S_SUBST thm t
177        in
178            ISPEC rf (MATCH_MP STRONG_EQUIV_SUBST_RELAB thm1)
179        end
180    else
181        S_ALL_CONV tm
182end;
183
184(* Define the tactic S_LHS_SUBST1_TAC: thm_tactic which substitutes a theorem
185   in the left-hand side of a strong equivalence. *)
186fun S_LHS_SUBST1_TAC thm :tactic =
187  fn (asl, w) => let
188      val (opt, t1, t2) = args_equiv w
189  in
190      if (opt ~~ ``STRONG_EQUIV``) then
191          let val thm' = S_SUBST thm t1;
192              val (t1', t') = args_thm thm' (* t1' = t1 *)
193          in
194              if t' ~~ t2 then
195                  ([], fn [] => S_TRANS thm' (ISPEC t' STRONG_EQUIV_REFL))
196              else
197                  ([(asl, ``STRONG_EQUIV ^t' ^t2``)],
198                   fn [thm''] => S_TRANS thm' thm'')
199          end
200      else
201          failwith "the goal is not a STRONG_EQUIV relation"
202  end;
203
204(* The tactic S_LHS_SUBST_TAC substitutes a list of theorems in the left-hand
205   side of a strong equivalence. *)
206fun S_LHS_SUBST_TAC thmlist = EVERY (map S_LHS_SUBST1_TAC thmlist);
207
208(* The tactic S_RHS_SUBST1_TAC substitutes a theorem in the right-hand side of
209   a strong equivalence. *)
210fun S_RHS_SUBST1_TAC thm =
211    REPEAT GEN_TAC
212 >> RULE_TAC STRONG_EQUIV_SYM
213 >> S_LHS_SUBST1_TAC thm
214 >> RULE_TAC STRONG_EQUIV_SYM;
215
216(* The tactic S_RHS_SUBST_TAC substitutes a list of theorems in the right-hand
217   side of a strong equivalence. *)
218fun S_RHS_SUBST_TAC thmlist =
219    REPEAT GEN_TAC
220 >> RULE_TAC STRONG_EQUIV_SYM
221 >> S_LHS_SUBST_TAC thmlist
222 >> RULE_TAC STRONG_EQUIV_SYM;
223
224(* The tactic S_SUBST1_TAC (S_SUBST_TAC) substitutes a (list of) theorem(s) in
225   both sides of a strong equivalence. *)
226fun S_SUBST1_TAC thm =
227    S_LHS_SUBST1_TAC thm
228 >> S_RHS_SUBST1_TAC thm;
229
230fun S_SUBST_TAC thmlist =
231    S_LHS_SUBST_TAC thmlist
232 >> S_RHS_SUBST_TAC thmlist;
233
234end (* struct *)
235
236(* last updated: May 14, 2017 *)
237