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