More additions (REC, I_def, I_NO_TRANS, etc.)

examples/CCS/CCSConv.sml

@@ -1,7 +1,11 @@
-(*
- * Copyright 1991-1995  University of Cambridge (Author: Monica Nesi)
- * Copyright 2016-2017  University of Bologna   (Author: Chun Tian)
- *)
+(* ========================================================================== *)
+(* FILE          : StrongLawsScript.sml                                       *)
+(* DESCRIPTION   : Laws of strong equivalence (STRONG_EQUIV)                  *)
+(*                                                                            *)
+(* COPYRIGHTS    : 1991-1995 University of Cambridge, UK (Monica Nesi)        *)
+(*                 2016-2017 University of Bologna, Italy (Chun Tian)         *)
+(*                 2023-2024 The Australian National University (Chun Tian)   *)
+(******************************************************************************)
 
 structure CCSConv :> CCSConv =
 struct
@@ -535,7 +539,11 @@ fun CCS_TRANS_CONV tm =
           val thmS = SIMP_CONV (srw_ss ()) [CCS_Subst_def] ``CCS_Subst ^P ^tm ^X``;
           val thm = CCS_TRANS_CONV (rconcl thmS)
       in
-          GEN_ALL (REWRITE_CONV [TRANS_REC_EQ, thmS, thm] ``TRANS ^tm u E``)
+          (* NOTE: for the new [REC], CCS_distinct' can be used to eliminate the
+                   extra ‘E <> var X’ generated by TRANS_REC_EQ.
+           *)
+          GEN_ALL (REWRITE_CONV [TRANS_REC_EQ, CCS_distinct', thmS, thm]
+                                ``TRANS ^tm u E``)
       end (* val (X, P) *)
   else (* no need to distinguish on (rconcl thm) *)
       failwith "CCS_TRANS_CONV";
@@ -559,5 +567,3 @@ end; (* local *)
 (* moved to selftest.sml *)
 
 end (* struct *)
-
-(* last updated: May 15, 2017 *)

examples/CCS/CCSScript.sml

@@ -15,6 +15,8 @@ open pred_setTheory pred_setLib relationTheory optionTheory listTheory CCSLib
 
 open generic_termsTheory binderLib nomsetTheory nomdatatype;
 
+local open termTheory; in end; (* for SUB's syntax only *)
+
 val _ = new_theory "CCS";
 
 val set_ss = std_ss ++ PRED_SET_ss;
@@ -803,10 +805,6 @@ Theorem parameter_tm_recursion =
                  ‘dpm’ |-> ‘apm’]
       |> CONV_RULE (REDEPTH_CONV sort_uvars)
 
-val FORALL_ONE = oneTheory.FORALL_ONE;
-val FORALL_ONE_FN = oneTheory.FORALL_ONE_FN;
-val EXISTS_ONE_FN = oneTheory.EXISTS_ONE_FN;
-
 Theorem tm_recursion =
   parameter_tm_recursion
       |> Q.INST_TYPE [‘:'q’ |-> ‘:unit’]
@@ -819,8 +817,8 @@ Theorem tm_recursion =
                   ‘rs’ |-> ‘\r L t u. rsu (r()) L t’,
                   ‘rl’ |-> ‘\r t rf u. rlu (r()) t rf’,
                   ‘re’ |-> ‘\r v t u. reu (r()) v t’]
-      |> SIMP_RULE (srw_ss()) [FORALL_ONE, FORALL_ONE_FN, EXISTS_ONE_FN,
-                               fnpm_def]
+      |> SIMP_RULE (srw_ss()) [oneTheory.FORALL_ONE, oneTheory.FORALL_ONE_FN,
+                               oneTheory.EXISTS_ONE_FN, fnpm_def]
       |> SIMP_RULE (srw_ss() ++ CONJ_ss) [supp_unitfn]
       |> Q.INST [‘vru’ |-> ‘vr’,
                  ‘nlu’ |-> ‘nl’,
@@ -1009,14 +1007,7 @@ val subst_exists =
 
 val SUB_DEF = new_specification("SUB_DEF", ["SUB"], subst_exists);
 
-val _ = add_rule {term_name = "SUB", fixity = Closefix,
-                  pp_elements = [TOK "[", TM, TOK "/", TM, TOK "]"],
-                  paren_style = OnlyIfNecessary,
-                  block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2))};
-
-val _ = TeX_notation { hol = "[", TeX = ("\\ensuremath{[}", 1) };
-val _ = TeX_notation { hol = "/", TeX = ("\\ensuremath{/}", 1) };
-val _ = TeX_notation { hol = "]", TeX = ("\\ensuremath{]}", 1) };
+Overload SUB = “SUB”; (* use the syntax already defined in termTheory *)
 
 val SUB_THMv = prove(
   “([N/x](var x) = (N :'a CCS)) /\ (x <> y ==> [N/y](var x) = var x)”,
@@ -1737,6 +1728,8 @@ Type transition[pp] = “:'a CCS -> 'a Action -> 'a CCS -> bool”
 
 (* Inductive definition of the transition relation TRANS for CCS.
    TRANS: CCS -> Action -> CCS -> bool
+
+   NOTE: added ‘E <> var X’ into [REC] to prove I_NO_TRANS (see below).
  *)
 Inductive TRANS :
     (!E u.                           TRANS (prefix u E) u E) /\         (* PREFIX *)
@@ -1751,7 +1744,7 @@ Inductive TRANS :
                 ==> TRANS (restr L E) u (restr L E')) /\                (* RESTR *)
     (!E u E' rf.    TRANS E u E'
                 ==> TRANS (relab E rf) (relabel rf u) (relab E' rf)) /\ (* RELABELING *)
-    (!E u X E1.     TRANS (CCS_Subst E (rec X E) X) u E1
+    (!E u X E1.     TRANS (CCS_Subst E (rec X E) X) u E1 /\ E <> var X
                 ==> TRANS (rec X E) u E1)                               (* REC *)
 End
 
@@ -1798,10 +1791,77 @@ QED
 (* An recursion variable has no transition.
    !X u E. ~TRANS (var X) u E
  *)
-val VAR_NO_TRANS = save_thm ("VAR_NO_TRANS",
+Theorem VAR_NO_TRANS =
     Q.GENL [`X`, `u`, `E`]
            (REWRITE_RULE [CCS_distinct', CCS_one_one]
-                         (Q.SPECL [`var X`, `u`, `E`] TRANS_cases)));
+                         (Q.SPECL [`var X`, `u`, `E`] TRANS_cases))
+
+val _ = hide "I";
+
+(* cf. chap2Theory (examples/lambda/barendregt) *)
+Definition I_def :
+    I = rec "x" (var "x")
+End
+
+Theorem FV_I[simp] :
+    FV I = {}
+Proof
+    SRW_TAC [][I_def]
+QED
+
+Theorem I_thm :
+    !X. I = rec X (var X)
+Proof
+    Q.X_GEN_TAC ‘x’
+ >> REWRITE_TAC [I_def, Once EQ_SYM_EQ]
+ >> Cases_on ‘x = "x"’ >- rw []
+ >> qabbrev_tac ‘u = var x’
+ >> qabbrev_tac ‘y = "x"’
+ >> ‘y NOTIN FV u’ by rw [Abbr ‘u’]
+ >> Know ‘rec x u = rec y ([var y/x] u)’
+ >- (MATCH_MP_TAC SIMPLE_ALPHA >> art [])
+ >> Rewr'
+ >> Suff ‘[var y/x] u = var y’ >- rw []
+ >> rw [Abbr ‘u’]
+QED
+
+Theorem SUB_I[simp] :
+    [N/v] I = I
+Proof
+    rw [lemma14b]
+QED
+
+Theorem ssub_I :
+    ssub fm I = I
+Proof
+    rw [ssub_value]
+QED
+
+Theorem I_cases :
+    I = rec Y P ==> P = var Y
+Proof
+    rw [I_def]
+ >> qabbrev_tac ‘X = "x"’
+ >> Cases_on ‘X = Y’ >> fs [rec_eq_thm]
+QED
+
+(* NOTE: This proof is only possible under the modified [REC] *)
+Theorem REC_VAR_NO_TRANS :
+    !X u E. ~TRANS (rec X (var X)) u E
+Proof
+    rw [Once TRANS_cases, CCS_Subst]
+ >> DISJ2_TAC
+ >> fs [GSYM I_thm, I_cases]
+QED
+
+(* |- !u E. ~(I --u-> E) *)
+Theorem I_NO_TRANS = REWRITE_RULE [GSYM I_thm] REC_VAR_NO_TRANS
+
+(******************************************************************************)
+(*                                                                            *)
+(*                The transitions of prefixed term                            *)
+(*                                                                            *)
+(******************************************************************************)
 
 (* !u E u' E'. TRANS (prefix u E) u' E' <=> (u' = u) /\ (E' = E) *)
 Theorem TRANS_PREFIX_EQ =
@@ -2164,31 +2224,52 @@ val REC_cases_EQ = save_thm
 
 val REC_cases = save_thm ("REC_cases", EQ_IMP_LR REC_cases_EQ);
 
+Theorem VAR_lemma[local] :
+    X # P ==> var X = [var X/Y] P ==> X <> Y ==> P = var Y
+Proof
+    MP_TAC (Q.SPEC ‘P’ CCS_cases) >> rw []
+ >> fs [] (* 3 subgoals left *)
+ >| [ (* goal 1 (of 3) *)
+      rename1 ‘Z = Y’ >> CCONTR_TAC >> fs [SUB_THM],
+      (* goal 2 (of 3) *)
+      rename1 ‘var X = [var X/Y] (rec Z E)’ \\
+      Q_TAC (NEW_TAC "Z'") ‘{X;Y;Z} UNION FV E’ \\
+      Know ‘rec Z E = rec Z' ([var Z'/Z] E)’
+      >- (MATCH_MP_TAC SIMPLE_ALPHA >> art []) \\
+      DISCH_THEN (fs o wrap),
+      (* goal 3 (of 3) *)
+      Q.PAT_X_ASSUM ‘X = X'’ (fs o wrap o SYM) \\
+      Q_TAC (NEW_TAC "Z") ‘{X;Y} UNION FV E’ \\
+      Know ‘rec X E = rec Z ([var Z/X] E)’
+      >- (MATCH_MP_TAC SIMPLE_ALPHA >> art []) \\
+      DISCH_THEN (fs o wrap) ]
+QED
+
 Theorem TRANS_REC_EQ :
-    !X E u E'. TRANS (rec X E) u E' <=> TRANS (CCS_Subst E (rec X E) X) u E'
+    !X E u E'. TRANS (rec X E) u E' <=> TRANS (CCS_Subst E (rec X E) X) u E' /\ E <> var X
 Proof
     rpt GEN_TAC
  >> reverse EQ_TAC
  >- PURE_ONCE_REWRITE_TAC [REC]
  >> PURE_ONCE_REWRITE_TAC [REC_cases_EQ]
- >> rpt STRIP_TAC
+ >> STRIP_TAC
+ >> rename1 ‘rec X E = rec Y P’
  >> fs [rec_eq_thm, CCS_Subst]
- >> rename1 ‘X <> Y’
- >> rename1 ‘X # P’
- (* stage work *)
- >> rw [fresh_tpm_subst]
+ >> Q.PAT_X_ASSUM ‘E = _’ K_TAC
+ >> simp [fresh_tpm_subst]
  >> Q.ABBREV_TAC ‘E = [var X/Y] P’
  >> Know ‘rec X E = rec Y ([var Y/X] E)’
  >- (MATCH_MP_TAC SIMPLE_ALPHA \\
      rw [Abbr ‘E’, FV_SUB])
  >> Rewr'
- >> rw [Abbr ‘E’]
+ >> simp [Abbr ‘E’]
  >> Know ‘[var Y/X] ([var X/Y] P) = P’
  >- (MATCH_MP_TAC lemma15b >> art [])
  >> Rewr'
- >> Suff ‘[rec Y P/X] ([var X/Y] P) = [rec Y P/Y] P’
- >- rw []
- >> MATCH_MP_TAC lemma15a >> art []
+ >> Know ‘[rec Y P/X] ([var X/Y] P) = [rec Y P/Y] P’
+ >- (MATCH_MP_TAC lemma15a >> art [])
+ >> Rewr' >> art []
+ >> METIS_TAC [VAR_lemma]
 QED
 
 val TRANS_REC = save_thm ("TRANS_REC", EQ_IMP_LR TRANS_REC_EQ);
@@ -2201,8 +2282,7 @@ Proof
  >> TRY (ASM_SET_TAC []) (* 1 - 6 *)
  >> MATCH_MP_TAC SUBSET_TRANS
  >> Q.EXISTS_TAC `FV (CCS_Subst E (rec X E) X)`
- >> POP_ASSUM (REWRITE_TAC o wrap)
- >> REWRITE_TAC [FV_SUBSET_REC']
+ >> ASM_REWRITE_TAC [FV_SUBSET_REC']
 QED
 
 Theorem TRANS_PROC :

examples/CCS/MultivariateScript.sml

@@ -3028,7 +3028,7 @@ Proof
  >> fs [CCS_equation_def, CCS_solution_def, EVERY_MEM, LIST_REL_EL_EQN]
 QED
 
-(* THE FINAL THEOREM (Theorem 3.13 of [3], full version) *)
+(* THE FINAL THEOREM (Theorem 3.16 of [3]) *)
 Theorem unique_solution_of_rooted_contractions :
     !Xs Es Ps Qs.
         CCS_equation Xs Es /\ EVERY (weakly_guarded Xs) Es /\
@@ -3100,11 +3100,8 @@ val _ = html_theory "Multivariate";
      solutions." ACM Transactions on Computational Logic (TOCL) 18.1
      (2017): 4. (DOI: 10.1145/2971339)
 
- [3] Tian, Chun, and Davide Sangiorgi. "Unique Solutions of
-     Contractions, CCS, and their HOL Formalisation." Combined 25th
-     International Workshop on Expressiveness in Concurrency and 15th
-     Workshop on Structural Operational Semantics (EXPRESS/SOS
-     2018). Vol. 276. No. 4. 2018. (DOI: 10.4204/EPTCS.276.10)
+ [3] C. Tian and D. Sangiorgi, “Unique solutions of contractions, CCS, and
+     their HOL formalisation,” Inf. Comput., vol. 275, p. 104606, Dec. 2020.
 
  [4] Gorrieri, R., Versari, C.: Introduction to Concurrency Theory.
      Springer, Cham (2015).