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