Move some theorems out of keccakScript.sml

HOL-Theorem-Prover · Oct 12, 2024 · fa42645 · fa42645
1 parent daa2bab
commit fa42645
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 37 deletions.
diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
@@ -10,43 +10,6 @@ val _ = new_theory "keccak";
 
 val _ = numLib.temp_prefer_num();
 
-(* TODO: move *)
-Theorem FUNPOW_COMPOSE_INV:
-  !n x f g h.
-  (!m. m < n ==> h(g(FUNPOW f m x)) = FUNPOW f m x)
-  ==>
-  FUNPOW (g o f o h) n (g x) =
-  g (FUNPOW f n x)
-Proof
-  Induct \\ rw[]
-  \\ rw[FUNPOW_SUC]
-QED
-
-(* TODO: move *)
-Theorem FUNPOW_invariant_index:
-  !m x.
-  P x /\
-  (!n. n < m ==> R (FUNPOW f n x)) /\
-  (!x. P x /\ R x ==> P (f x)) ==>
-  P (FUNPOW f m x)
-Proof
-  Induct>>rw[FUNPOW_SUC]
-QED
-
-(* TODO: move *)
-Theorem WHILE_FUNPOW:
-  (?n. ~P (FUNPOW f n s))
-  ==> WHILE P f s = FUNPOW f (LEAST n. ~P (FUNPOW f n s)) s
-Proof
-  strip_tac
-  \\ `~!n. P (FUNPOW f n s)` by PROVE_TAC[]
-  \\ `?x. OWHILE P f s = SOME x` by PROVE_TAC[OWHILE_EQ_NONE, option_CASES]
-  \\ irule OWHILE_WHILE
-  \\ rewrite_tac[OWHILE_def]
-  \\ IF_CASES_TAC
-  \\ fsrw_tac[][]
-QED
-
 Datatype:
   state_array =
   <| w: num

diff --git a/src/num/theories/arithmeticScript.sml b/src/num/theories/arithmeticScript.sml
@@ -3968,6 +3968,21 @@ Proof
   Induct \\ SRW_TAC[][FUNPOW_SUC]
 QED
 
+Theorem FUNPOW_invariant_index:
+  !m x.
+  P x /\
+  (!n. n < m ==> R (FUNPOW f n x)) /\
+  (!x. P x /\ R x ==> P (f x)) ==>
+  P (FUNPOW f m x)
+Proof
+  Induct >> SRW_TAC[][FUNPOW_SUC]
+  \\ first_assum irule
+  \\ `m < SUC m` by SRW_TAC[][LESS_SUC_REFL]
+  \\ SRW_TAC[][]
+  \\ first_assum irule \\ SRW_TAC[][]
+  \\ first_assum irule \\ SRW_TAC[][LESS_SUC]
+QED
+
 (* Theorem: FUNPOW f m (FUNPOW f n x) = FUNPOW f n (FUNPOW f m x) *)
 (* Proof: by FUNPOW_ADD, ADD_COMM *)
 Theorem FUNPOW_COMM:

diff --git a/src/num/theories/whileScript.sml b/src/num/theories/whileScript.sml
@@ -424,6 +424,19 @@ val OWHILE_IND = store_thm(
   THEN IMP_RES_TAC prim_recTheory.LESS_MONO THEN RES_TAC
   THEN FULL_SIMP_TAC bool_ss [FUNPOW]);
 
+Theorem WHILE_FUNPOW:
+  (?n. ~P (FUNPOW f n s))
+  ==> WHILE P f s = FUNPOW f (LEAST n. ~P (FUNPOW f n s)) s
+Proof
+  strip_tac
+  \\ `~!n. P (FUNPOW f n s)` by PROVE_TAC[]
+  \\ `?x. OWHILE P f s = SOME x` by PROVE_TAC[OWHILE_EQ_NONE, option_CASES]
+  \\ irule OWHILE_WHILE
+  \\ rewrite_tac[OWHILE_def]
+  \\ IF_CASES_TAC
+  \\ FULL_SIMP_TAC(srw_ss())[]
+QED
+
 Theorem TAILREC_EXISTS[local]:
   ?tailrec.
     !(f:'a -> 'a + 'b) (x:'a).