Fix more duplicated theorems after breakage caused by 705d331

HOL-Theorem-Prover · Sep 11, 2023 · 44a6680 · 44a6680
1 parent fc9eb64
commit 44a6680
Show file tree

Hide file tree

Showing 9 changed files with 57 additions and 165 deletions.
diff --git a/examples/CCS/ContractionScript.sml b/examples/CCS/ContractionScript.sml
@@ -1703,19 +1703,6 @@ val OBS_contracts_WEAK_TRANS_label' = store_thm (
       MATCH_MP_TAC WEAK_TRANS_AND_EPS \\
       Q.EXISTS_TAC `E1` >> art [] ]);
 
-val OBS_contracts_EPS' = store_thm (
-   "OBS_contracts_EPS'",
-  ``!E E'. OBS_contracts E E' ==> !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``,
-    rpt STRIP_TAC
- >> IMP_RES_TAC EPS_cases1 (* 2 sub-goals here *)
- >- ( Q.EXISTS_TAC `E` >> fs [EPS_REFL] \\
-      IMP_RES_TAC OBS_contracts_IMP_WEAK_EQUIV )
- >> IMP_RES_TAC OBS_contracts_TRANS_RIGHT
- >> IMP_RES_TAC WEAK_EQUIV_EPS'
- >> Q.EXISTS_TAC `E1'` >> art []
- >> IMP_RES_TAC WEAK_TRANS_IMP_EPS
- >> IMP_RES_TAC EPS_TRANS);
-
 (******************************************************************************)
 (*                                                                            *)
 (*      Is OBS_contracts coarsest precongruence contained in `contracts`?     *)

diff --git a/examples/Hoare-for-divergence/std_logic_completenessScript.sml b/examples/Hoare-for-divergence/std_logic_completenessScript.sml
@@ -88,7 +88,7 @@ Proof
   \\ fs [PULL_EXISTS]
   \\ rpt (goal_assum (first_assum o mp_then Any mp_tac))
   \\ ‘∃n. NRC (λs t. guard f s ∧ terminates s c t) n m t ∧ ¬guard f t’ by
-        (match_mp_tac teramintes_While_NRC \\ fs [])
+        (match_mp_tac terminates_While_NRC \\ fs [])
   \\ ‘∀k t1. NRC (λs t. guard f s ∧ terminates s c t) k m t1 ∧ ¬guard f t1 ⇔
              t1 = t ∧ n = k’ by
    (rw [] \\ eq_tac \\ fs [] \\ rw [] \\ fs []

diff --git a/examples/Hoare-for-divergence/while_lang_lemmasScript.sml b/examples/Hoare-for-divergence/while_lang_lemmasScript.sml
@@ -305,21 +305,17 @@ Proof
   \\ simp [Once exec_cases]
 QED
 
-Theorem teramintes_While_NRC:
-  ∀m p t. terminates m p t ⇒
-    ∀c. p = While f c ⇒
-    ∃n. NRC (λs t. guard f s ∧ terminates s c t) n m t ∧ ¬guard f t
+Theorem terminates_While_NRC:
+  ∀m f c t. terminates m (While f c) t ⇒
+            ∃n. NRC (λs t. guard f s ∧ terminates s c t) n m t ∧ ¬guard f t
 Proof
   rewrite_tac [terminates_eq_exec]
-  \\ ho_match_mp_tac exec_strongind \\ rw []
+  \\ Induct_on ‘exec’ \\ rw []
   THEN1 (qexists_tac ‘0’ \\ fs [])
   \\ qexists_tac ‘SUC n’ \\ fs [NRC]
   \\ goal_assum (first_x_assum o mp_then Any mp_tac) \\ fs []
 QED
 
-Theorem teramintes_While_NRC = teramintes_While_NRC
-  |> SIMP_RULE std_ss [PULL_FORALL] |> GEN_ALL;
-
 Theorem not_diverges[simp]:
   ~diverges s Skip l ∧
   ~diverges s (Assign n x) l ∧

diff --git a/examples/PSL/1.01/executable-semantics/ExecuteSemanticsScript.sml b/examples/PSL/1.01/executable-semantics/ExecuteSemanticsScript.sml
@@ -1057,13 +1057,6 @@ val LENGTH_IS_INFINITE = store_thm
    ``!p. IS_INFINITE p ==> (LENGTH p = INFINITY)``,
    METIS_TAC [LENGTH_def, IS_INFINITE_EXISTS]);
 
-val CAT_SEL_REC_RESTN = store_thm
-  ("CAT_SEL_REC_RESTN",
-   ``!n p. IS_INFINITE p ==> (CAT (SEL_REC n 0 p, RESTN p n) = p)``,
-   Induct
-   >> RW_TAC std_ss [SEL_REC_def, RESTN_def, CAT_def, IS_INFINITE_REST]
-   >> PROVE_TAC [CONS_HEAD_REST, LENGTH_IS_INFINITE, GT]);
-
 (* Safety violations *)
 
 val safety_violation_def = Define

diff --git a/examples/PSL/1.01/official-semantics/PropertiesScript.sml b/examples/PSL/1.01/official-semantics/PropertiesScript.sml
@@ -1526,31 +1526,9 @@ val CONCAT_APPEND =
 * Idempotency  of r[*]: r[*];r[*] = [*]
 ******************************************************************************)
 
-val S_REPEAT_IDEMPOTENT =
- store_thm
-  ("S_REPEAT_IDEMPOTENT",
-   ``!w r. US_SEM w (S_CAT(S_REPEAT r,S_REPEAT r)) = US_SEM w (S_REPEAT r)``,
-   RW_TAC simp_list_ss [US_SEM_def,B_SEM]
-    THEN EQ_TAC
-    THEN RW_TAC simp_list_ss []
-    THENL
-     [Q.EXISTS_TAC `wlist<>wlist'`
-       THEN RW_TAC simp_list_ss [ALL_EL_APPEND,CONCAT_APPEND],
-      Q.EXISTS_TAC `[]` THEN Q.EXISTS_TAC `CONCAT wlist`
-       THEN RW_TAC simp_list_ss []
-       THENL
-        [Q.EXISTS_TAC `[]`
-          THEN RW_TAC simp_list_ss [CONCAT_def],
-         PROVE_TAC[]]]);
-
-(******************************************************************************
-* Idempotency  of r[*]: r[*];r[*] = r[*]
-******************************************************************************)
-
-val S_REPEAT_IDEMPOTENT =
- store_thm
-  ("S_REPEAT_IDEMPOTENT",
-   ``!w r. US_SEM w (S_CAT(S_REPEAT r,S_REPEAT r)) = US_SEM w (S_REPEAT r)``,
+Theorem S_REPEAT_IDEMPOTENT:
+  !w r. US_SEM w (S_CAT(S_REPEAT r,S_REPEAT r)) = US_SEM w (S_REPEAT r)
+Proof
    RW_TAC simp_list_ss [US_SEM_def,B_SEM]
     THEN EQ_TAC
     THEN RW_TAC simp_list_ss []
@@ -1562,7 +1540,7 @@ val S_REPEAT_IDEMPOTENT =
        THENL
         [Q.EXISTS_TAC `[]`
           THEN RW_TAC simp_list_ss [CONCAT_def],
-         PROVE_TAC[]]]);
-
+         PROVE_TAC[]]]
+QED
 
 val _ = export_theory();
diff --git a/examples/PSL/1.01/official-semantics/SyntacticSugarScript.sml b/examples/PSL/1.01/official-semantics/SyntacticSugarScript.sml
@@ -568,14 +568,6 @@ val F_WEAK_WITHIN_INC_def =
   `F_WEAK_WITHIN_INC (r1,b,r2) =
     F_WEAK_IMP(r1, S_AND(r2, S_CAT(S_EQ_REPEAT_ITER b 0, S_BOOL b)))`;
 
-(******************************************************************************
-* within(r1,b){r2} = {r1} |-> {r2&&b[=0];b}
-******************************************************************************)
-val F_WEAK_WITHIN_def =
- Define
-  `F_WEAK_WITHIN (r1,b,r2) =
-    F_WEAK_IMP(r1, S_CAT(S_AND(r2, S_EQ_REPEAT_ITER b 0), S_BOOL b))`;
-
 (******************************************************************************
 * whilenot!(b){r} = within!(T,b){r}
 ******************************************************************************)

diff --git a/examples/PSL/1.1/official-semantics/ProjectionScript.sml b/examples/PSL/1.1/official-semantics/ProjectionScript.sml
@@ -408,15 +408,15 @@ val TAKE_FIRST_NIL =
    Induct
     THEN RW_TAC list_ss [TAKE_FIRST_def,FILTER_APPEND]);
 
-val TAKE_FIRSTN_NIL =
- store_thm
-  ("TAKE_FIRSTN_NIL",
-   ``!P n l. 0 < n ==> (TAKE_FIRSTN P n l = []) ==> (l = [])``,
+Theorem TAKE_FIRSTN_EQ_NIL_E:
+  !P n l. 0 < n ==> (TAKE_FIRSTN P n l = []) ==> (l = [])
+Proof
    GEN_TAC
     THEN Induct
     THEN RW_TAC list_ss []
     THEN FULL_SIMP_TAC list_ss [TAKE_FIRSTN_def]
-    THEN PROVE_TAC[TAKE_FIRST_NIL]);
+    THEN PROVE_TAC[TAKE_FIRST_NIL]
+QED
 
 val HD_TAKE_FIRST =
  store_thm
@@ -1376,7 +1376,8 @@ val S_PROJ_S_FUSION =
        THEN RW_TAC list_ss []
        THEN FULL_SIMP_TAC list_ss []
        THEN `0 < SUC(LENGTH v1)` by DECIDE_TAC
-       THEN `~(TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l = [])` by PROVE_TAC[TAKE_FIRSTN_NIL]
+       THEN `~(TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l = [])`
+         by PROVE_TAC[TAKE_FIRSTN_EQ_NIL_E]
        THEN Q.EXISTS_TAC `BUTLAST(TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)`
        THEN Q.EXISTS_TAC `LASTN (LENGTH l - LENGTH(TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)) l`
        THEN Q.EXISTS_TAC `LAST(TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)`
@@ -2094,27 +2095,15 @@ val LEAST_TAKE_FIRST =
                  LEAST_SUC))
        THEN RW_TAC list_ss []]);
 
-val HD_FILTER_LEAST =
- store_thm
-  ("HD_FILTER_LEAST",
-   ``!P l. (?n. n < LENGTH l /\ P(EL n l))
-           ==>
-           (HD (FILTER P l) = EL (LEAST n. P (EL n l)) l)``,
-   RW_TAC std_ss []
-    THEN IMP_RES_TAC HD_TAKE_FIRST
-    THEN IMP_RES_TAC  LEAST_TAKE_FIRST
-    THEN RW_TAC list_ss []);
-
-val HD_FILTER_LEAST =
- store_thm
-  ("HD_FILTER_LEAST",
-   ``!P l n. n < LENGTH l /\ P(EL n l)
-             ==>
-             (HD (FILTER P l) = EL (LEAST n. P (EL n l)) l)``,
+Theorem HD_FILTER_LEAST:
+  !P l n. n < LENGTH l /\ P(EL n l) ==>
+          (HD (FILTER P l) = EL (LEAST n. P (EL n l)) l)
+Proof
    RW_TAC std_ss []
     THEN IMP_RES_TAC HD_TAKE_FIRST
     THEN IMP_RES_TAC  LEAST_TAKE_FIRST
-    THEN RW_TAC list_ss []);
+    THEN RW_TAC list_ss []
+QED
 
 val IS_LEAST_MIN =
  store_thm
@@ -2866,13 +2855,11 @@ val SEL_BUTFIRSTN =
                   by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``n>(p:num) ==> ~(n=0)``,CONS]
             THEN PROVE_TAC[BUTFIRSTN]]]);
 
-val SEL_TAKE_FIRSTN =
- store_thm
-  ("SEL_TAKE_FIRSTN",
-   ``!P n l.
-      LENGTH l > 0
-      ==>
-      (SEL l (0, LENGTH(TAKE_FIRSTN P (SUC n) l)-1) = TAKE_FIRSTN P (SUC n) l)``,
+Theorem SEL_TAKE_FIRSTN:
+  !P n l.
+    LENGTH l > 0 ==>
+    (SEL l (0, LENGTH(TAKE_FIRSTN P (SUC n) l)-1) = TAKE_FIRSTN P (SUC n) l)
+Proof
    GEN_TAC
     THEN Induct
     THEN RW_TAC list_ss [REWRITE_RULE[ONE]TAKE_FIRSTN_1,SEL_TAKE_FIRST]
@@ -2881,35 +2868,44 @@ val SEL_TAKE_FIRSTN =
     THEN `LENGTH (TAKE_FIRST P l) > 0` by PROVE_TAC[LENGTH_TAKE_FIRST_NON_EMPTY]
     THEN Cases_on `BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l = []`
     THEN RW_TAC list_ss [TAKE_FIRSTN_NIL,SEL_TAKE_FIRST]
-    THEN `~(LENGTH(BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)=0)` by PROVE_TAC[LENGTH_NIL]
+    THEN `~(LENGTH(BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)=0)`
+      by PROVE_TAC[LENGTH_NIL]
     THEN `LENGTH(BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l) > 0` by DECIDE_TAC
     THEN `LENGTH(TAKE_FIRST P (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) > 0`
           by PROVE_TAC[LENGTH_TAKE_FIRST_NON_EMPTY]
-    THEN `LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) > 0`
+    THEN `LENGTH(TAKE_FIRSTN P (SUC n)
+                             (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) > 0`
           by PROVE_TAC
-              [LENGTH_TAKE_FIRST_TAKE_FIRSTN,DECIDE``m:num > 0 /\ m <= n:num ==> n > 0``]
+              [LENGTH_TAKE_FIRST_TAKE_FIRSTN,
+               DECIDE``m:num > 0 /\ m <= n:num ==> n > 0``]
     THEN `LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) > 0`
           by PROVE_TAC
               [LENGTH_TAKE_FIRST_TAKE_FIRSTN,LENGTH_TAKE_FIRST_SUC,
                DECIDE``m:num > 0 /\ m <= n:num /\ n <= p:num ==> p > 0``]
-    THEN `LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) <= LENGTH l` by PROVE_TAC[LENGTH_TAKE_FIRSTN]
+    THEN `LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) <= LENGTH l`
+      by PROVE_TAC[LENGTH_TAKE_FIRSTN]
     THEN `LENGTH l > LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) - 1` by DECIDE_TAC
     THEN `LENGTH l > LENGTH (TAKE_FIRST P l)
                      +
-                     LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1`
+                     LENGTH(TAKE_FIRSTN P (SUC n)
+                                   (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1`
           by PROVE_TAC[LENGTH_TAKE_FIRSTN_LEMMA]
     THEN `LENGTH l > (LENGTH (TAKE_FIRST P l) - 1)
                      +
-                     LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l))`
+                     LENGTH(TAKE_FIRSTN P (SUC n)
+                                   (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l))`
           by DECIDE_TAC
     THEN RW_TAC std_ss [DECIDE ``m > 0 ==> (m + n - 1 = (m - 1) + n)``]
     THEN RW_TAC list_ss [SEL_BUTFIRSTN,SEL_TAKE_FIRST]
     THEN `SEL (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)
-              (0,LENGTH (TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1) =
-          TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)`
-          by PROVE_TAC[]
-    THEN `SUC(LENGTH (TAKE_FIRST P l) - 1) = LENGTH(TAKE_FIRST P l)` by DECIDE_TAC
-    THEN RW_TAC list_ss []);
+              (0,LENGTH (TAKE_FIRSTN P (SUC n)
+                               (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1) =
+         TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)`
+      by PROVE_TAC[]
+    THEN `SUC(LENGTH (TAKE_FIRST P l) - 1) = LENGTH(TAKE_FIRST P l)`
+      by DECIDE_TAC
+    THEN RW_TAC list_ss []
+QED
 
 val FIRSTN_SEL =
  store_thm
@@ -2944,52 +2940,6 @@ val FIRSTN_SEL =
           [FIRSTN,ADD1,FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def,
            FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def]);
 
-
-val SEL_TAKE_FIRSTN =
- store_thm
-  ("SEL_TAKE_FIRSTN",
-   ``!P n l.
-      LENGTH l > 0
-      ==>
-      (SEL l (0, LENGTH(TAKE_FIRSTN P (SUC n) l)-1) = TAKE_FIRSTN P (SUC n) l)``,
-   GEN_TAC
-    THEN Induct
-    THEN RW_TAC list_ss [REWRITE_RULE[ONE]TAKE_FIRSTN_1,SEL_TAKE_FIRST]
-    THEN ONCE_REWRITE_TAC[TAKE_FIRSTN_def]
-    THEN RW_TAC list_ss []
-    THEN `LENGTH (TAKE_FIRST P l) > 0` by PROVE_TAC[LENGTH_TAKE_FIRST_NON_EMPTY]
-    THEN Cases_on `BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l = []`
-    THEN RW_TAC list_ss [TAKE_FIRSTN_NIL,SEL_TAKE_FIRST]
-    THEN `~(LENGTH(BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)=0)` by PROVE_TAC[LENGTH_NIL]
-    THEN `LENGTH(BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l) > 0` by DECIDE_TAC
-    THEN `LENGTH(TAKE_FIRST P (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) > 0`
-          by PROVE_TAC[LENGTH_TAKE_FIRST_NON_EMPTY]
-    THEN `LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) > 0`
-          by PROVE_TAC
-              [LENGTH_TAKE_FIRST_TAKE_FIRSTN,DECIDE``m:num > 0 /\ m <= n:num ==> n > 0``]
-    THEN `LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) > 0`
-          by PROVE_TAC
-              [LENGTH_TAKE_FIRST_TAKE_FIRSTN,LENGTH_TAKE_FIRST_SUC,
-               DECIDE``m:num > 0 /\ m <= n:num /\ n <= p:num ==> p > 0``]
-    THEN `LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) <= LENGTH l` by PROVE_TAC[LENGTH_TAKE_FIRSTN]
-    THEN `LENGTH l > LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) - 1` by DECIDE_TAC
-    THEN `LENGTH l > LENGTH (TAKE_FIRST P l)
-                     +
-                     LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1`
-          by PROVE_TAC[LENGTH_TAKE_FIRSTN_LEMMA]
-    THEN `LENGTH l > (LENGTH (TAKE_FIRST P l) - 1)
-                     +
-                     LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l))`
-          by DECIDE_TAC
-    THEN RW_TAC std_ss [DECIDE ``m > 0 ==> (m + n - 1 = (m - 1) + n)``]
-    THEN RW_TAC list_ss [SEL_BUTFIRSTN,SEL_TAKE_FIRST]
-    THEN `SEL (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)
-              (0,LENGTH (TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1) =
-          TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)`
-          by PROVE_TAC[]
-    THEN `SUC(LENGTH (TAKE_FIRST P l) - 1) = LENGTH(TAKE_FIRST P l)` by DECIDE_TAC
-    THEN RW_TAC list_ss []);
-
 val FILTER_SEL =
  store_thm
   ("FILTER_SEL",

diff --git a/examples/PSL/path/PSLPathScript.sml b/examples/PSL/path/PSLPathScript.sml
@@ -279,14 +279,12 @@ val _ = overload_on("<=", ``LE_xnum_xnum``);
 (******************************************************************************
 * Extend greater-than predicate (>) to extended numbers
 ******************************************************************************)
-val GT_num_xnum_def =
- Define `$GT_num_xnum (m:num) (XNUM (n:num)) = (m:num) > (n:num)`;
 
-val GT_num_xnum_def =
- Define
-  `($GT_num_xnum (m:num) (XNUM (n:num)) = (m:num) > (n:num))
+Definition GT_num_xnum_def:
+  ($GT_num_xnum (m:num) (XNUM (n:num)) <=> (m:num) > (n:num))
    /\
-   ($GT_num_xnum (m:num) INFINITY = F)`;
+  ($GT_num_xnum (m:num) INFINITY <=> F)
+End
 
 val GT_xnum_num_def =
  Define
@@ -312,14 +310,12 @@ val _ = overload_on(">", ``GT_xnum_xnum``);
 (******************************************************************************
 * Extend greater-than-or-equal predicate (>=) to extended numbers
 ******************************************************************************)
-val GE_num_xnum_def =
- Define `$GE_num_xnum (m:num) (XNUM (n:num)) = (m:num) >= (n:num)`;
 
-val GE_num_xnum_def =
- Define
-  `($GE_num_xnum (m:num) (XNUM (n:num)) = (m:num) >= (n:num))
+Definition GE_num_xnum_def:
+  ($GE_num_xnum (m:num) (XNUM (n:num)) = (m:num) >= (n:num))
    /\
-   ($GE_num_xnum (m:num) INFINITY = F)`;
+  ($GE_num_xnum (m:num) INFINITY = F)
+End
 
 val GE_xnum_num_def =
  Define

diff --git a/examples/arm/arm6-verification/io_onestepScript.sml b/examples/arm/arm6-verification/io_onestepScript.sml
@@ -1475,7 +1475,7 @@ val ONE_STEP_THMa = save_thm("ONE_STEP_THMa",
 
 (* ------------------------------------------------------------------------- *)
 
-val TCON_IMMERSION = store_thm("TCON_IMMERSION",
+val TCON_IMMERSION_THM = store_thm("TCON_IMMERSION_THM",
   `!f imm strm.
          TCON_IMMERSION f imm strm =
            (let g = \t x. <|state:= (f t x).state; inp := ADVANCE t x.inp|> in