Move LT_EXISTS and LE_EXISTS theorems to arithmetic only

Previously, there were variations of these scattered around src
unnecessarily.

There are some minor knock-on changes, but the bulk of the changes in
this commit are me trying to make proofs more robust in the face of
possibly changing LE_EXISTS's existential variable's name from p to
d (for "delta", and matching what is done in LT_EXISTS).

This broke a few things, most annoyingly when the `e + d` or `e + p`
was rewritten by the standard bossLib simplifier. Because this
includes the arithmetic normalisation code, the summands get sorted,
and d sorts to different positions than p.

So, I ended up keeping the old name (p), but I'm happy to also keep
the robustifications included in this commit.

examples/Hoare-for-divergence/while_lang_lemmasScript.sml

@@ -46,7 +46,7 @@ Proof
   \\ fs [LESS_EQ_EXISTS] \\ rw []
   \\ imp_res_tac NRC_ADD_E
   \\ imp_res_tac NRC_step_deterministic
-  \\ res_tac \\ rveq \\ fs []
+  \\ rveq
   \\ ‘∀n t1 t2. NRC step n (Skip,t1) (Skip,t2) ⇒ t1 = t2’ by
      (Induct \\ fs [NRC] \\ rw [] \\ fs [Once step_cases] \\ rveq \\ fs [])
   \\ res_tac \\ rveq \\ fs []
@@ -360,9 +360,11 @@ Theorem lprefix_chain_RTC_step:
   lprefix_chain {fromList out | (∃q t. RTC step x (q,t,out))}
 Proof
   fs [lprefix_lubTheory.lprefix_chain_def] \\ rw []
-  \\ fs [lprefix_lubTheory.lprefix_rel_def,PULL_EXISTS,LPREFIX_fromList,from_toList]
+  \\ fs [lprefix_lubTheory.lprefix_rel_def,PULL_EXISTS,LPREFIX_fromList,
+         from_toList]
   \\ fs [RTC_eq_NRC]
-  \\ ‘n ≤ n' ∨ n' ≤ n’ by fs []
+  \\ rename [‘s1 ≼ s2 ∨ s2 ≼ s1’, ‘NRC _ a _ (_,_,s1)’, ‘NRC _ b _ (_, _, s2)’]
+  \\ ‘a ≤ b ∨ b ≤ a’ by fs []
   \\ fs [LESS_EQ_EXISTS] \\ rw []
   \\ drule NRC_ADD_E \\ strip_tac
   \\ imp_res_tac NRC_step_deterministic
@@ -390,7 +392,9 @@ Proof
       \\ drule RTC_Seq
       \\ disch_then (qspec_then ‘c'’ mp_tac)
       \\ simp [RTC_eq_NRC] \\ rw []
-      \\ Cases_on ‘n ≤ n'’ \\ fs []
+      \\ rename [‘NRC step b _ (Seq Skip _, _)’, ‘out ≼ _’,
+                 ‘NRC step a _ (_, _, out)’]
+      \\ Cases_on ‘a ≤ b’ \\ fs []
       THEN1
        (fs [LESS_EQ_EXISTS] \\ rw []
         \\ drule NRC_ADD_E \\ strip_tac
@@ -400,14 +404,14 @@ Proof
         \\ Cases_on ‘t’ \\ fs [output_of_def]
         \\ ‘NRC step 0 (c',q',r) (c',q',r)’ by fs []
         \\ goal_assum (first_assum o mp_then (Pos hd) mp_tac) \\ fs [])
-      \\ qpat_x_assum ‘NRC step n _ _’ assume_tac
+      \\ qpat_x_assum ‘NRC step a _ _’ assume_tac
       \\ rename [‘_ _ _ (x1,x2,x3)’]
       \\ qexists_tac ‘x3’
       \\ qexists_tac ‘x1’
       \\ qexists_tac ‘x2’ \\ fs []
-      \\ qexists_tac ‘n - n' - 1’
-      \\ ‘n = n' + SUC (n − n' - 1)’ by decide_tac
-      \\ ‘NRC step (n' + SUC (n − n' − 1)) (Seq c c',s) (x1,x2,x3)’ by metis_tac []
+      \\ qexists_tac ‘a - b - 1’
+      \\ ‘a = b + SUC (a − b - 1)’ by decide_tac
+      \\ ‘NRC step (b + SUC (a − b − 1)) (Seq c c',s) (x1,x2,x3)’ by metis_tac []
       \\ drule NRC_ADD_E \\ strip_tac
       \\ imp_res_tac NRC_step_deterministic \\ rw []
       \\ pop_assum mp_tac \\ fs [NRC]

examples/PSL/1.01/executable-semantics/ExecuteSemanticsScript.sml

@@ -705,13 +705,13 @@ val SEL_REC0 = store_thm
    ``!n p. SEL_REC (n + 1) 0 p = SEL p (0,n)``,
    RW_TAC arith_ss [SEL_def]);
 
-val S_FLEX_AND_SEL_REC = store_thm
-  ("S_FLEX_AND_SEL_REC",
-   ``!p f g.
-       (?n. US_SEM (SEL_REC n 0 p) (S_FLEX_AND (f,g))) =
-       ?n.
-         US_SEM (SEL_REC n 0 p)
-         (S_AND (S_CAT (f, S_REPEAT S_TRUE), S_CAT (g, S_REPEAT S_TRUE)))``,
+Theorem S_FLEX_AND_SEL_REC:
+  !p f g.
+    (?n. US_SEM (SEL_REC n 0 p) (S_FLEX_AND (f,g))) =
+    ?n.
+      US_SEM (SEL_REC n 0 p)
+             (S_AND (S_CAT (f, S_REPEAT S_TRUE), S_CAT (g, S_REPEAT S_TRUE)))
+Proof
    RW_TAC std_ss [S_FLEX_AND_def, GSYM S_TRUE_def]
    >> EQ_TAC
    >- (CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [US_SEM_def]))
@@ -752,6 +752,7 @@ val S_FLEX_AND_SEL_REC = store_thm
         >> Know `LENGTH w1' + LENGTH w2' = LENGTH w1 + LENGTH w2`
         >- METIS_TAC [listTheory.LENGTH_APPEND, LENGTH_SEL_REC]
         >> STRIP_TAC
+        >> rename [‘LENGTH w1 + p' = LENGTH w1'’]
         >> Know `p' + LENGTH w2' = LENGTH w2`
         >- DECIDE_TAC
         >> POP_ASSUM (K ALL_TAC)
@@ -781,6 +782,7 @@ val S_FLEX_AND_SEL_REC = store_thm
         >> Know `LENGTH w1' + LENGTH w2' = LENGTH w1 + LENGTH w2`
         >- METIS_TAC [listTheory.LENGTH_APPEND, LENGTH_SEL_REC]
         >> STRIP_TAC
+        >> rename [‘LENGTH w1' + p' = LENGTH w1’]
         >> Know `p' + LENGTH w2 = LENGTH w2'`
         >- DECIDE_TAC
         >> POP_ASSUM (K ALL_TAC)
@@ -794,7 +796,8 @@ val S_FLEX_AND_SEL_REC = store_thm
         >> ONCE_REWRITE_TAC [US_SEM_def]
         >> RW_TAC arith_ss
            [US_SEM_REPEAT_TRUE, APPEND_LENGTH_EQ, LENGTH_SEL_REC]
-        >> PROVE_TAC []]);
+        >> PROVE_TAC []]
+QED
 
 val S_FLEX_AND_SEL = store_thm
   ("S_FLEX_AND_SEL",
@@ -1202,9 +1205,9 @@ val boolean_safety_violation = store_thm
 
 (* The basic constraint on simple formulas *)
 
-val simple_safety = store_thm
-  ("simple_safety",
-   ``!f p. simple f /\ IS_INFINITE p ==> (safety_violation p f = ~UF_SEM p f)``,
+Theorem simple_safety:
+   !f p. simple f /\ IS_INFINITE p ==> (safety_violation p f = ~UF_SEM p f)
+Proof
    RW_TAC std_ss []
    >> EQ_TAC >- METIS_TAC [safety_violation_refl]
    >> REPEAT (POP_ASSUM MP_TAC)
@@ -1284,6 +1287,7 @@ val simple_safety = store_thm
        >> RW_TAC std_ss
             [SEL_REC_SPLIT, GSYM CAT_APPEND, RESTN_CAT, LENGTH_SEL_REC]
        >> RW_TAC arith_ss []
+       >> rename [‘j + SUC n = k + p'’]
        >> Cases_on `p'` >- FULL_SIMP_TAC arith_ss []
        >> RW_TAC std_ss [SEL_REC_SUC, CAT_def, HEAD_CONS, ELEM_def],
 
@@ -1305,6 +1309,7 @@ val simple_safety = store_thm
        >> RW_TAC std_ss [safety_violation_def]
        >> Know `n <= n' \/ n' <= n` >- DECIDE_TAC
        >> RW_TAC std_ss [LESS_EQ_EXISTS]
+       >> rename [‘SEL_REC (_ + p')’]
        >| [Q.EXISTS_TAC `n + p'`
            >> RW_TAC std_ss []
            >> ONCE_REWRITE_TAC [ADD_COMM]
@@ -1315,6 +1320,7 @@ val simple_safety = store_thm
            >> ONCE_REWRITE_TAC [ADD_COMM]
            >> RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND]
            >> METIS_TAC [IS_INFINITE_CAT]],
+
        RW_TAC std_ss [safety_violation_def]
        >> Q.PAT_X_ASSUM `~UF_SEM X Y` MP_TAC
        >> ONCE_REWRITE_TAC [UF_SEM_def]
@@ -1332,6 +1338,7 @@ val simple_safety = store_thm
        >> RW_TAC std_ss [safety_violation_def]
        >> Know `n <= n' \/ n' <= n` >- DECIDE_TAC
        >> RW_TAC std_ss [LESS_EQ_EXISTS]
+       >> rename [‘SEL_REC (_ + p')’]
        >| [Q.EXISTS_TAC `n + p'`
            >> RW_TAC std_ss []
            >> ONCE_REWRITE_TAC [ADD_COMM]
@@ -1342,6 +1349,7 @@ val simple_safety = store_thm
            >> ONCE_REWRITE_TAC [ADD_COMM]
            >> RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND]
            >> METIS_TAC [IS_INFINITE_CAT]],
+
        RW_TAC std_ss [safety_violation_def]
        >> Q.PAT_X_ASSUM `~UF_SEM X Y` MP_TAC
        >> ONCE_REWRITE_TAC [UF_SEM_def]
@@ -1359,6 +1367,7 @@ val simple_safety = store_thm
        >> RW_TAC std_ss [safety_violation_def]
        >> Know `n <= n' \/ n' <= n` >- DECIDE_TAC
        >> RW_TAC std_ss [LESS_EQ_EXISTS]
+       >> rename [‘SEL_REC (_ + p')’]
        >| [Q.EXISTS_TAC `n + p'`
            >> RW_TAC std_ss []
            >> ONCE_REWRITE_TAC [ADD_COMM]
@@ -1369,6 +1378,7 @@ val simple_safety = store_thm
            >> ONCE_REWRITE_TAC [ADD_COMM]
            >> RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND]
            >> METIS_TAC [IS_INFINITE_CAT]],
+
        RW_TAC std_ss [safety_violation_def]
        >> Q.PAT_X_ASSUM `~UF_SEM X Y` MP_TAC
        >> ONCE_REWRITE_TAC [UF_SEM_def]
@@ -1386,6 +1396,7 @@ val simple_safety = store_thm
        >> RW_TAC std_ss [safety_violation_def]
        >> Know `n <= n' \/ n' <= n` >- DECIDE_TAC
        >> RW_TAC std_ss [LESS_EQ_EXISTS]
+       >> rename [‘SEL_REC (_ + p')’]
        >| [Q.EXISTS_TAC `n + p'`
            >> RW_TAC std_ss []
            >> ONCE_REWRITE_TAC [ADD_COMM]
@@ -1396,6 +1407,7 @@ val simple_safety = store_thm
            >> ONCE_REWRITE_TAC [ADD_COMM]
            >> RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND]
            >> METIS_TAC [IS_INFINITE_CAT]],
+
        RW_TAC std_ss [safety_violation_def]
        >> Q.PAT_X_ASSUM `~UF_SEM X Y` MP_TAC
        >> ONCE_REWRITE_TAC [UF_SEM_def]
@@ -1413,6 +1425,7 @@ val simple_safety = store_thm
        >> RW_TAC std_ss [safety_violation_def]
        >> Know `n <= n' \/ n' <= n` >- DECIDE_TAC
        >> RW_TAC std_ss [LESS_EQ_EXISTS]
+       >> rename [‘SEL_REC (_ + p')’]
        >| [Q.EXISTS_TAC `n + p'`
            >> RW_TAC std_ss []
            >> ONCE_REWRITE_TAC [ADD_COMM]
@@ -1423,6 +1436,7 @@ val simple_safety = store_thm
            >> ONCE_REWRITE_TAC [ADD_COMM]
            >> RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND]
            >> METIS_TAC [IS_INFINITE_CAT]],
+
        RW_TAC std_ss [safety_violation_def]
        >> Q.PAT_X_ASSUM `~UF_SEM X Y` MP_TAC
        >> ONCE_REWRITE_TAC [UF_SEM_def]
@@ -1440,6 +1454,7 @@ val simple_safety = store_thm
        >> RW_TAC std_ss [safety_violation_def]
        >> Know `n <= n' \/ n' <= n` >- DECIDE_TAC
        >> RW_TAC std_ss [LESS_EQ_EXISTS]
+       >> rename [‘SEL_REC (_ + p')’]
        >| [Q.EXISTS_TAC `n + p'`
            >> RW_TAC std_ss []
            >> ONCE_REWRITE_TAC [ADD_COMM]
@@ -1450,6 +1465,7 @@ val simple_safety = store_thm
            >> ONCE_REWRITE_TAC [ADD_COMM]
            >> RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND]
            >> METIS_TAC [IS_INFINITE_CAT]],
+
        RW_TAC std_ss [safety_violation_def]
        >> Q.PAT_X_ASSUM `~UF_SEM X Y` MP_TAC
        >> ONCE_REWRITE_TAC [UF_SEM_def]
@@ -1467,6 +1483,7 @@ val simple_safety = store_thm
        >> RW_TAC std_ss [safety_violation_def]
        >> Know `n <= n' \/ n' <= n` >- DECIDE_TAC
        >> RW_TAC std_ss [LESS_EQ_EXISTS]
+       >> rename [‘SEL_REC (_ + p')’]
        >| [Q.EXISTS_TAC `n + p'`
            >> RW_TAC std_ss []
            >> ONCE_REWRITE_TAC [ADD_COMM]
@@ -1544,7 +1561,8 @@ val simple_safety = store_thm
        >> Q.SPEC_TAC (`j + 1`,`j`)
        >> Induct
        >> RW_TAC std_ss [SEL_REC_def, CAT_def, HEAD_CONS, REST_CONS]
-       >> PROVE_TAC []]);
+       >> PROVE_TAC []]
+QED
 
 (* The regexp checker *)
 
@@ -1705,9 +1723,8 @@ val checker_CLOCK_FREE = store_thm
                      boolean_checker_CLOCK_FREE, S_FLEX_AND_def, S_FALSE_def]
    >> PROVE_TAC [boolean_def, boolean_checker_CLOCK_FREE]);
 
-val checker_NOT_AND = store_thm
-  ("checker_NOT_AND",
-   ``!f g.
+Theorem checker_NOT_AND:
+   !f g.
        (!p.
           simple (F_NOT f) /\ IS_INFINITE p ==>
           (safety_violation p (F_NOT f) =
@@ -1721,13 +1738,15 @@ val checker_NOT_AND = store_thm
          (safety_violation p (F_NOT (F_AND (f,g))) =
           ?n.
             US_SEM (SEL_REC n 0 p)
-              (S_FLEX_AND (checker (F_NOT f),checker (F_NOT g))))``,
+              (S_FLEX_AND (checker (F_NOT f),checker (F_NOT g))))
+Proof
    RW_TAC std_ss [safety_violation_alt, UF_SEM_def, S_FLEX_AND]
    >> REPEAT (Q.PAT_X_ASSUM `!x. P x` (fn th => RW_TAC std_ss [GSYM th]))
    >> EQ_TAC >- PROVE_TAC []
    >> RW_TAC std_ss []
    >> Know `n <= n' \/ n' <= n` >- DECIDE_TAC
    >> RW_TAC std_ss [LESS_EQ_EXISTS]
+   >> rename [‘SEL_REC (_ + p')’]
    >| [Q.EXISTS_TAC `n + p'`
        >> RW_TAC std_ss []
        >> ONCE_REWRITE_TAC [ADD_COMM]
@@ -1737,7 +1756,8 @@ val checker_NOT_AND = store_thm
        >> RW_TAC std_ss []
        >> ONCE_REWRITE_TAC [ADD_COMM]
        >> RW_TAC arith_ss [SEL_REC_SPLIT, GSYM CAT_APPEND]
-       >> PROVE_TAC [IS_INFINITE_CAT, IS_INFINITE_EXISTS]]);
+       >> PROVE_TAC [IS_INFINITE_CAT, IS_INFINITE_EXISTS]]
+QED
 
 val checker_AND = store_thm
   ("checker_AND",

examples/logic/propositional_logic/PropLogicScript.sml

@@ -642,7 +642,8 @@ Theorem limitbuild_mono:
   ∀m n. m ≤ n ⇒ limitbuild A m ⊆ limitbuild A n
 Proof
   simp[PULL_EXISTS, arithmeticTheory.LESS_EQ_EXISTS] >>
-  Induct_on ‘p’ >> simp[arithmeticTheory.ADD_CLAUSES] >>
+  CONV_TAC SWAP_FORALL_CONV >> Induct >>
+  simp[arithmeticTheory.ADD_CLAUSES] >>
   rw[] >> gs[SUBSET_DEF]
 QED
 

examples/miller/formalize/sequenceScript.sml

@@ -127,12 +127,14 @@ val SDROP_ADD = store_thm
    Induct_on `y` >- RW_TAC list_ss [sdrop_def, I_THM]
    >> RW_TAC std_ss [ADD_CLAUSES, sdrop_def, o_THM]);
 
-val SDROP_EQ_MONO = store_thm
-  ("SDROP_EQ_MONO",
-   ``!m n x y. (sdrop m x = sdrop m y) /\ m <= n ==> (sdrop n x = sdrop n y)``,
+Theorem SDROP_EQ_MONO:
+   !m n x y. (sdrop m x = sdrop m y) /\ m <= n ==> (sdrop n x = sdrop n y)
+Proof
    RW_TAC std_ss [LESS_EQ_EXISTS]
+   >> rename [‘sdrop (m + p) x = sdrop (m + p) y’]
    >> Induct_on `p` >- RW_TAC arith_ss []
-   >> RW_TAC std_ss [ADD_CLAUSES, GSYM STL_o_SDROP, o_THM]);
+   >> RW_TAC std_ss [ADD_CLAUSES, GSYM STL_o_SDROP, o_THM]
+QED
 
 val EVENTUALLY_REFL = store_thm
   ("EVENTUALLY_REFL",

src/float/floatScript.sml

@@ -417,33 +417,31 @@ val ISFINITE = Q.store_thm ("ISFINITE",
 
 (*--------------------------------------*)
 
-val REAL_ABS_INV = Q.prove (
-  `!x. abs (inv x) = inv (abs x)`,
+Theorem REAL_ABS_INV[local]:
+  !x. abs (inv x) = inv (abs x)
+Proof
   gen_tac
   \\ Cases_on `x = 0r`
   \\ simp [REAL_INV_0, REAL_ABS_0, ABS_INV]
-  )
+QED
 
-val REAL_ABS_DIV = Q.prove (
-  `!x y. abs (x / y) = abs x / abs y`,
-  rewrite_tac [real_div, REAL_ABS_INV, REAL_ABS_MUL])
+Theorem REAL_ABS_DIV[local]:
+  !x y. abs (x / y) = abs x / abs y
+Proof
+  rewrite_tac [real_div, REAL_ABS_INV, REAL_ABS_MUL]
+QED
 
-val REAL_POW_LE_1 = Q.prove (
-  `!n x. 1r <= x ==> 1 <= x pow n`,
+Theorem REAL_POW_LE_1[local]:
+  !n x. 1r <= x ==> 1 <= x pow n
+Proof
   Induct
   \\ rw [pow]
   \\ GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID]
   \\ match_mp_tac REAL_LE_MUL2
   \\ simp []
-  )
+QED
 
-val REAL_POW_MONO = Q.prove (
-  `!m n x. 1r <= x /\ m <= n ==> x pow m <= x pow n`,
-  rw [LESS_EQ_EXISTS]
-  \\ simp [REAL_POW_ADD]
-  \\ GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID]
-  \\ metis_tac [REAL_LE_LMUL_IMP, REAL_POW_LE_1, POW_POS, REAL_LE_TRANS,
-                REAL_LE_01])
+Theorem REAL_POW_MONO[local] = realTheory.REAL_POW_MONO
 
 Theorem VAL_FINITE:
   !a. Finite a ==> abs (Val a) <= largest float_format

src/floating-point/lift_ieeeScript.sml

@@ -164,14 +164,7 @@ val REAL_POW_LE_1 = Q.prove(
   \\ simp []
   );
 
-val REAL_POW_MONO = Q.prove(
-  `!m n x. 1r <= x /\ m <= n ==> x pow m <= x pow n`,
-  rw [arithmeticTheory.LESS_EQ_EXISTS]
-  \\ simp [REAL_POW_ADD]
-  \\ Ho_Rewrite.GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID]
-  \\ metis_tac [REAL_LE_LMUL_IMP, REAL_POW_LE_1, POW_POS, REAL_LE_TRANS,
-                REAL_LE_01]
-  );
+val REAL_POW_MONO = realTheory.REAL_POW_MONO
 
 val exponent_le = Q.prove(
   `!e : 'a word. e <> -1w ==> (w2n e <= UINT_MAX (:'a) - 1)`,