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