1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna (Author: Chun Tian) 4 * Copyright 2019 Fondazione Bruno Kessler, Italy (Author: Chun Tian) 5 *) 6 7structure CCSLib :> CCSLib = 8struct 9 10open HolKernel Parse boolLib bossLib; 11 12(******************************************************************************) 13(* *) 14(* Backward compatibility and utility tactic/tacticals (2019) *) 15(* *) 16(******************************************************************************) 17 18(* Tacticals for better expressivity *) 19fun fix ts = MAP_EVERY Q.X_GEN_TAC ts; (* from HOL Light *) 20fun unset ts = MAP_EVERY Q.UNABBREV_TAC ts; (* from HOL mizar mode *) 21fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *) 22val Know = Q_TAC KNOW_TAC; (* from util_prob *) 23val Suff = Q_TAC SUFF_TAC; (* from util_prob *) 24fun K_TAC _ = ALL_TAC; (* from util_prob *) 25val KILL_TAC = POP_ASSUM_LIST K_TAC; (* from util_prob *) 26fun wrap a = [a]; (* from util_prob *) 27val art = ASM_REWRITE_TAC; 28val Rewr = DISCH_THEN (REWRITE_TAC o wrap); (* from util_prob *) 29val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 30val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 31 32fun PRINT_TAC s gl = (* from cardinalTheory *) 33 (print ("** " ^ s ^ "\n"); ALL_TAC gl); 34 35fun COUNT_TAC tac g = (* from Konrad Slind *) 36 let val res as (sg, _) = tac g 37 val _ = print ("subgoals: " ^ Int.toString (List.length sg) ^ "\n") 38 in res end; 39 40local 41 val th = prove (``!a b. a /\ (a ==> b) ==> a /\ b``, PROVE_TAC []) 42in 43 val STRONG_CONJ_TAC :tactic = MATCH_MP_TAC th >> CONJ_TAC 44end; 45 46fun NDISJ_TAC n = (NTAC n DISJ2_TAC) >> TRY DISJ1_TAC; 47 48(******************************************************************************) 49(* *) 50(* Basic rules and tactics for particular forms of rewriting *) 51(* *) 52(******************************************************************************) 53 54(* Rule for rewriting only the right-hand side on an equation once. *) 55val ONCE_REWRITE_RHS_RULE = 56 GEN_REWRITE_RULE (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites; 57 58(* Rule for rewriting only the right-hand side on an equation (pure version). *) 59val PURE_REWRITE_RHS_RULE = 60 GEN_REWRITE_RULE (RAND_CONV o TOP_DEPTH_CONV) empty_rewrites; 61 62(* Rule for rewriting only the right-hand side on an equation 63 (basic rewrites included) *) 64val REWRITE_RHS_RULE = 65 GEN_REWRITE_RULE (RAND_CONV o TOP_DEPTH_CONV) (implicit_rewrites ()); 66 67(* Tactic for rewriting only the right-hand side on an equation once. *) 68val ONCE_REWRITE_RHS_TAC = 69 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites; 70 71(* Tactic for rewriting only the right-hand side on an equation. *) 72val REWRITE_RHS_TAC = 73 GEN_REWRITE_TAC (RAND_CONV o TOP_DEPTH_CONV) (implicit_rewrites ()); 74 75(* Rule for rewriting only the left-hand side on an equation once. *) 76val ONCE_REWRITE_LHS_RULE = 77 GEN_REWRITE_RULE (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites; 78 79(* Rule for rewriting only the left-hand side on an equation (pure version). *) 80val PURE_REWRITE_LHS_RULE = 81 GEN_REWRITE_RULE (RATOR_CONV o TOP_DEPTH_CONV) empty_rewrites; 82 83(* Rule for rewriting only the left-hand side on an equation 84 (basic rewrites included). *) 85val REWRITE_LHS_RULE = 86 GEN_REWRITE_RULE (RATOR_CONV o TOP_DEPTH_CONV) (implicit_rewrites ()); 87 88(* Tactic for rewriting only the left-hand side on an equation once. *) 89val ONCE_REWRITE_LHS_TAC = 90 GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites; 91 92(* Tactic for rewriting only the left-hand side on an equation. *) 93val REWRITE_LHS_TAC = 94 GEN_REWRITE_TAC (RATOR_CONV o TOP_DEPTH_CONV) (implicit_rewrites ()); 95 96(* Rule for rewriting only the left-hand side of an equation once with the 97 assumptions. *) 98fun ONCE_ASM_REWRITE_LHS_RULE thl th = 99 ONCE_REWRITE_LHS_RULE ((map ASSUME (hyp th)) @ thl) th; 100 101(* Tactic for rewriting only the left-hand side of an equation once with the 102 assumptions. *) 103fun ONCE_ASM_REWRITE_LHS_TAC thl = 104 ASSUM_LIST (fn asl => ONCE_REWRITE_LHS_TAC (asl @ thl)); 105 106(* Conversion to swap two universally quantified variables. *) 107fun SWAP_FORALL_CONV tm = let 108 val (v1, body) = dest_forall tm; 109 val v2 = fst (dest_forall body); 110 val tl1 = [v1, v2] and tl2 = [v2, v1]; 111 val th1 = GENL tl2 (SPECL tl1 (ASSUME tm)); 112 val th2 = GENL tl1 (SPECL tl2 (ASSUME (concl th1))) 113in 114 IMP_ANTISYM_RULE (DISCH_ALL th1) (DISCH_ALL th2) 115end; 116 117(* provided by Michael Norrish *) 118fun STRIP_FORALL_RULE f th = 119 let 120 val (vs, _) = strip_forall (concl th) 121 in 122 GENL vs (f (SPEC_ALL th)) 123 end; 124 125(* The rule EQ_IMP_LR returns the implication from left to right of a given 126 equational theorem. *) 127val EQ_IMP_LR = STRIP_FORALL_RULE (fst o EQ_IMP_RULE); 128 129(* The rule EQ_IMP_RL returns the implication from right to left of a given 130 equational theorem. *) 131val EQ_IMP_RL = STRIP_FORALL_RULE (snd o EQ_IMP_RULE); 132 133(* Functions to get the left and right hand side of the equational conclusion 134 of a theorem. *) 135val lconcl = fst o dest_eq o concl o SPEC_ALL; 136val rconcl = snd o dest_eq o concl o SPEC_ALL; 137 138(* Define args_thm as a function that, given a theorem |- f t1 t2, returns (t1, t2). *) 139fun args_thm thm = 140 let 141 val (f, args) = strip_comb (concl thm) 142 in 143 case args of 144 [t1,t2] => (t1, t2) 145 | _ => raise mk_HOL_ERR "CCSLib" "args_thm" "fn doesn't have two args" 146 end; 147 148fun lhs_tm thm = (fst o args_thm) thm; 149fun rhs_tm thm = (snd o args_thm) thm; 150 151(* Define args_equiv as a function that, given a tm "p t1 t2", returns (p, t1, t2) *) 152fun args_equiv tm = 153 let 154 val (p, args) = strip_comb tm 155 in 156 case args of 157 [t1,t2] => (p, t1, t2) 158 | _ => raise mk_HOL_ERR "CCSLib" "args_equiv" "fn doesn't have two args" 159 end; 160 161(* Auxiliary functions (on lists and terms) to find repeated occurrences of a 162 summand to be then deleted by applying the idempotence law for summation. *) 163local 164 fun helper (h:term, nil) = nil 165 | helper (h, t::l) = if h ~~ t then l else t :: (helper (h, l)) 166in 167 fun elim h l = helper (h, l) 168end; 169 170(* Function for applying a list of tactics to a list of subgoals. *) 171fun list_apply_tac _ [] = [] 172 | list_apply_tac (f: 'a -> tactic) (actl : 'a list) : tactic list = 173 (f (hd actl)) :: (list_apply_tac f (tl actl)); 174 175end (* of struct *) 176