Add various theorems

HOL-Theorem-Prover · Dec 2, 2023 · 0bbc579 · 0bbc579
1 parent 2a25962
commit 0bbc579
Show file tree

Hide file tree

Showing 4 changed files with 47 additions and 0 deletions.
diff --git a/src/finite_maps/sptreeScript.sml b/src/finite_maps/sptreeScript.sml
@@ -1880,6 +1880,19 @@ Theorem wf_LN[simp]: wf LN
 Proof rw[wf_def]
 QED
 
+Theorem wf_fromList[simp]:
+  wf (fromList ls)
+Proof
+  rw[fromList_def]
+  \\ qmatch_goalsub_abbrev_tac`FOLDL f (0,LN) ls`
+  \\ qho_match_abbrev_tac`P (FOLDL f (0,LN) ls)`
+  \\ `FOLDL f (0,LN) ls = FOLDL f (0,LN) ls /\ P (FOLDL f (0,LN) ls)`
+  suffices_by rw[]
+  \\ irule rich_listTheory.FOLDL_CONG_invariant
+  \\ simp[Abbr`P`, Abbr`f`, pairTheory.FORALL_PROD]
+  \\ rw[wf_insert]
+QED
+
 val splem1 = Q.prove(`
   a <> 0 ==> (a-1) DIV 2 < a`,
   simp[DIV_LT_X]);

diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
@@ -345,6 +345,16 @@ val MAP_FOLDL = Q.store_thm ("MAP_FOLDL",
    THEN GEN_TAC
    THEN REFL_TAC);
 
+Theorem FOLDL_CONG_invariant:
+  !P f1 f2 l e.
+  P e /\
+  (!x a. MEM x l ∧ P a ==> f1 a x = f2 a x /\ P (f2 a x))
+  ==>
+  FOLDL f1 e l = FOLDL f2 e l /\ P (FOLDL f2 e l)
+Proof
+  ntac 3 gen_tac \\ Induct \\ rw[]
+QED
+
 val FILTER_FOLDR = Q.store_thm ("FILTER_FOLDR",
    `!P l. FILTER P l = FOLDR (\x l'. if P x then CONS x l' else l') [] l`,
    BasicProvers.Induct_on `l`

diff --git a/src/num/extra_theories/logrootScript.sml b/src/num/extra_theories/logrootScript.sml
@@ -171,6 +171,12 @@ val LOG_UNIQUE = Q.store_thm("LOG_UNIQUE",
    THEN METIS_TAC [exp_lemma5, DECIDE ``a < b <=> SUC a <= b``, LESS_EQ_TRANS,
                    NOT_LESS, LOG, EXP]);
 
+val LOG_POW = Q.store_thm("LOG_POW",
+  `!b n. 1n < b ==> (LOG b (b ** n) = n)`,
+  REPEAT STRIP_TAC
+  THEN irule LOG_UNIQUE
+  THEN SRW_TAC [ARITH_ss] [EXP]);
+
 val LOG_ADD1 = Q.store_thm("LOG_ADD1",
    `!n a b. 0n < n /\ 1n < a /\ 0 < b ==>
             (LOG a (a ** SUC n * b) = SUC (LOG a (a ** n * b)))`,

diff --git a/src/num/theories/arithmeticScript.sml b/src/num/theories/arithmeticScript.sml
@@ -3785,6 +3785,24 @@ val FUNPOW_1 = store_thm ("FUNPOW_1",
   REWRITE_TAC [FUNPOW, ONE]);
 val _ = export_rewrites ["FUNPOW_1"]
 
+Theorem FUNPOW_CONG:
+  !n x f g.
+  (!m. m < n ==> f (FUNPOW f m x) = g (FUNPOW f m x))
+  ==>
+  FUNPOW f n x = FUNPOW g n x
+Proof
+  INDUCT_TAC \\ SRW_TAC[][FUNPOW_SUC]
+  THEN METIS_TAC[LESS_SUC, LESS_SUC_REFL]
+QED
+
+Theorem FUNPOW_invariant:
+  !m x.
+  P x /\ (!x. P x ==> P (f x)) ==>
+  P (FUNPOW f m x)
+Proof
+  Induct \\ SRW_TAC[][FUNPOW_SUC]
+QED
+
 val NRC_0 = save_thm ("NRC_0", CONJUNCT1 NRC);
 val _ = export_rewrites ["NRC_0"]