Add various theorems (#1168)

* Add toSortedAList_fromList - thanks to Yong Kiam

* Add size_map thms

* Add more sptree theorems

* Add fromList_fromAList

* Add a couple more sptree thms

src/finite_maps/sptreeScript.sml

@@ -620,6 +620,27 @@ val domain_fromList = store_thm(
   qmatch_assum_rename_tac `nn < SUC (LENGTH l)` >>
   Cases_on `nn` >> fs[] >> metis_tac[ADD1]);
 
+val size_domain = Q.store_thm("size_domain",
+  `!t. size t = CARD (domain t)`,
+  Induct_on `t`
+  >- rw[size_def, domain_def]
+  >- rw[size_def, domain_def]
+  >> rw[CARD_UNION_EQN, CARD_INJ_IMAGE]
+  >-
+   (`IMAGE (\n. 2 * n + 2) (domain t) INTER
+     IMAGE (\n. 2 * n + 1) (domain t') = {}`
+      by (rw[GSYM DISJOINT_DEF, IN_DISJOINT]
+          >> Cases_on `ODD x`
+          >> fs[ODD_EXISTS, ADD1, oddevenlemma])
+    >> simp[]) >>
+  `(({0} INTER IMAGE (\n. 2 * n + 2) (domain t)) = {}) /\
+   (({0} UNION (IMAGE (\n. 2 * n + 2) (domain t)))
+        INTER (IMAGE (\n. 2 * n + 1) (domain t')) = {})`
+  by (rw[GSYM DISJOINT_DEF, IN_DISJOINT]
+      >> Cases_on `ODD x`
+      >> fs[ODD_EXISTS, ADD1, oddevenlemma])
+  >> simp[]);
+
 val ODD_IMP_NOT_ODD = prove(
   ``!k. ODD k ==> ~(ODD (k-1))``,
   Cases >> fs [ODD]);
@@ -948,6 +969,18 @@ val ALL_DISTINCT_MAP_FST_toAList = store_thm("ALL_DISTINCT_MAP_FST_toAList",
   simp[MEM_MAP,PULL_EXISTS,pairTheory.EXISTS_PROD] >>
   metis_tac[ODD_EVEN,lemmas] )
 
+Theorem LENGTH_toAList[simp]:
+  LENGTH (toAList t) = size t
+Proof
+  `LENGTH (toAList t) = LENGTH (MAP FST (toAList t))` by simp[]>>
+  pop_assum SUBST_ALL_TAC>>
+  DEP_REWRITE_TAC[GSYM ALL_DISTINCT_CARD_LIST_TO_SET]>>
+  simp[ALL_DISTINCT_MAP_FST_toAList,size_domain]>>
+  AP_TERM_TAC>>
+  rw[pred_setTheory.EXTENSION]>>
+  simp[MEM_MAP,pairTheory.EXISTS_PROD,MEM_toAList,domain_lookup]
+QED
+
 val _ = remove_ovl_mapping "lrnext" {Name = "lrnext", Thy = "sptree"}
 
 val foldi_FOLDR_toAList_lemma = prove(
@@ -1658,27 +1691,6 @@ val mapi_Alist = Q.store_thm(
   simp[spt_eq_thm, wf_mapi, wf_fromAList, lookup_fromAList] >>
   srw_tac[boolSimps.ETA_ss][lookup_mapi, ALOOKUP_MAP_lemma, ALOOKUP_toAList]);
 
-val size_domain = Q.store_thm("size_domain",
-  `!t. size t = CARD (domain t)`,
-  Induct_on `t`
-  >- rw[size_def, domain_def]
-  >- rw[size_def, domain_def]
-  >> rw[CARD_UNION_EQN, CARD_INJ_IMAGE]
-  >-
-   (`IMAGE (\n. 2 * n + 2) (domain t) INTER
-     IMAGE (\n. 2 * n + 1) (domain t') = {}`
-      by (rw[GSYM DISJOINT_DEF, IN_DISJOINT]
-          >> Cases_on `ODD x`
-          >> fs[ODD_EXISTS, ADD1, oddevenlemma])
-    >> simp[]) >>
-  `(({0} INTER IMAGE (\n. 2 * n + 2) (domain t)) = {}) /\
-   (({0} UNION (IMAGE (\n. 2 * n + 2) (domain t)))
-        INTER (IMAGE (\n. 2 * n + 1) (domain t')) = {})`
-  by (rw[GSYM DISJOINT_DEF, IN_DISJOINT]
-      >> Cases_on `ODD x`
-      >> fs[ODD_EXISTS, ADD1, oddevenlemma])
-  >> simp[]);
-
 val num_set_domain_eq = Q.store_thm("num_set_domain_eq",
   `!t1 t2:unit spt.
      wf t1 /\ wf t2 ==>
@@ -1692,6 +1704,25 @@ val union_num_set_sym = Q.store_thm ("union_num_set_sym",
   `!(t1:unit spt) t2. union t1 t2 = union t2 t1`,
   Induct >> fs[union_def] >> rw[] >> CASE_TAC >> fs[union_def]);
 
+Theorem union_disjoint_sym:
+  !t1 t2.
+  wf t1 /\ wf t2 /\ DISJOINT (domain t1) (domain t2) ==>
+  union t1 t2 = union t2 t1
+Proof
+  Induct
+  >- rw[]
+  >- (
+    rw[union_def]
+    \\ CASE_TAC \\ rw[union_def]
+    \\ fs[] )
+  \\ rw[wf_def] \\ fs[]
+  \\ rw[Once union_def]
+  \\ CASE_TAC \\ rw[Once union_def, SimpRHS] \\ fs[]
+  \\ first_x_assum irule \\ fs[wf_def]
+  \\ gs[pred_setTheory.DISJOINT_IMAGE]
+  \\ simp[pred_setTheory.DISJOINT_SYM]
+QED
+
 Theorem difference_sub:
   (difference a b = LN) ==> (domain a SUBSET domain b)
 Proof
@@ -1880,6 +1911,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]);
@@ -2003,6 +2047,18 @@ Proof
   Induct_on `xs` \\ fs [list_size_def]
 QED
 
+Theorem size_map[simp]:
+  size (map f t) = size t
+Proof
+  rw[size_domain]
+QED
+
+Theorem size_mapi[simp]:
+  size (mapi f t) = size t
+Proof
+  rw[size_domain]
+QED
+
 val spt_size_def = definition "spt_size_def";
 
 Theorem SUM_MAP_same_LE:
@@ -2344,6 +2400,104 @@ Proof
   \\ simp [SORTED_toSortedAList, relationTheory.irreflexive_def]
 QED
 
+Theorem toSortedAList_fromList:
+  toSortedAList (fromList ls) = ZIP (COUNT_LIST (LENGTH ls),ls)
+Proof
+  mp_tac (sortingTheory.SORTED_ALL_DISTINCT_LIST_TO_SET_EQ
+          |> INST_TYPE [alpha |-> ``:num # 'a``]
+          |> Q.SPEC`(\x y. FST x < FST y)`)>>
+  impl_keep_tac >-
+    fs[relationTheory.transitive_def,relationTheory.antisymmetric_def]>>
+  disch_then match_mp_tac>>
+  CONJ_ASM1_TAC
+  >- (
+    match_mp_tac sortingTheory.SORTED_weaken>>
+    irule_at Any (SORTED_toSortedAList |> SIMP_RULE std_ss [sortingTheory.sorted_map])>>
+    simp[])>>
+  CONJ_ASM1_TAC
+  >- (
+    match_mp_tac sortingTheory.SORTED_FST_ZIP>>
+    simp[rich_listTheory.LENGTH_COUNT_LIST,sortingTheory.sorted_lt_count_list])>>
+  rw[]
+  >- (
+    irule sortingTheory.SORTED_ALL_DISTINCT>>
+    first_x_assum (irule_at Any)>>
+    first_x_assum (irule_at Any)>>
+    simp[relationTheory.irreflexive_def])
+  >- (
+    irule sortingTheory.SORTED_ALL_DISTINCT>>
+    first_x_assum (irule_at Any)>>
+    first_x_assum (irule_at Any)>>
+    simp[relationTheory.irreflexive_def])
+  >- (
+    rw[pred_setTheory.EXTENSION]>>
+    Cases_on`x`>>
+    DEP_REWRITE_TAC[MEM_ZIP]>>
+    simp[rich_listTheory.LENGTH_COUNT_LIST,MEM_toSortedAList,lookup_fromList]>>
+    metis_tac[rich_listTheory.EL_COUNT_LIST])
+QED
+
+Theorem fromList_fromAList:
+  !l. fromList l = fromAList (ZIP (COUNT_LIST (LENGTH l), l))
+Proof
+  ho_match_mp_tac SNOC_INDUCT
+  \\ conj_tac >- rw[fromList_def, fromAList_def,
+                    rich_listTheory.COUNT_LIST_def]
+  \\ rw[fromList_def, rich_listTheory.COUNT_LIST_def]
+  \\ rw[FOLDL_SNOC, pairTheory.UNCURRY]
+  \\ rw[GSYM rich_listTheory.COUNT_LIST_def]
+  \\ rw[rich_listTheory.COUNT_LIST_SNOC,
+        rich_listTheory.ZIP_SNOC,
+        rich_listTheory.LENGTH_COUNT_LIST]
+  \\ rw[SNOC_APPEND, fromAList_append]
+  \\ DEP_ONCE_REWRITE_TAC[union_disjoint_sym]
+  \\ simp[union_insert_LN]
+  \\ simp[wf_fromAList, wf_insert, domain_fromAList,
+          MAP_ZIP, rich_listTheory.LENGTH_COUNT_LIST,
+          rich_listTheory.MEM_COUNT_LIST]
+  \\ AP_THM_TAC \\ AP_THM_TAC
+  \\ AP_TERM_TAC
+  \\ qmatch_goalsub_abbrev_tac`FOLDL f e l`
+  \\ `!l e. FST (FOLDL f e l) = FST e + LENGTH l` suffices_by simp[Abbr`e`]
+  \\ Induct \\ rw[Abbr`f`, pairTheory.UNCURRY]
+QED
+
+Theorem ALL_DISTINCT_MAP_FST_toSortedAList:
+  ALL_DISTINCT (MAP FST (toSortedAList t))
+Proof
+  irule sortingTheory.SORTED_ALL_DISTINCT>>
+  irule_at Any (SORTED_toSortedAList)>>
+  simp[relationTheory.irreflexive_def]
+QED
+
+Theorem LENGTH_toSortedAList[simp]:
+  LENGTH (toSortedAList t) = size t
+Proof
+  `LENGTH (toSortedAList t) =
+    LENGTH (MAP FST (toSortedAList t))` by simp[]>>
+  pop_assum SUBST_ALL_TAC>>
+  DEP_REWRITE_TAC[GSYM ALL_DISTINCT_CARD_LIST_TO_SET]>>
+  simp[ALL_DISTINCT_MAP_FST_toSortedAList,size_domain]>>
+  AP_TERM_TAC>>
+  rw[pred_setTheory.EXTENSION]>>
+  simp[MEM_MAP,pairTheory.EXISTS_PROD,MEM_toSortedAList,domain_lookup]
+QED
+
+Theorem set_MAP_FST_toAList_domain:
+  set (MAP FST (toAList t)) = domain t
+Proof
+  rw[EXTENSION]
+  \\ `(ALOOKUP (toAList t) x <> NONE) <=> x IN domain t`
+  suffices_by metis_tac[ALOOKUP_NONE]
+  \\ simp[ALOOKUP_toAList, lookup_NONE_domain]
+QED
+
+Theorem size_fromList[simp]:
+  size (fromList ls) = LENGTH ls
+Proof
+  rw[size_domain, domain_fromList]
+QED
+
 val _ = let
   open sptreepp
 in

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`

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)))`,

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"]
 

src/sort/sortingScript.sml

@@ -1857,4 +1857,19 @@ Proof
   \\ simp[QSORT_SORTED]
 QED
 
+Theorem SORTED_FST_ZIP:
+  !R ls rs.
+  SORTED R ls /\ LENGTH ls = LENGTH rs ==>
+  SORTED (\x y. R (FST x) (FST y)) (ZIP (ls,rs))
+Proof
+  ho_match_mp_tac SORTED_IND>>rw[]
+  >- (Cases_on`rs`>>fs[])>>
+  `?a b rss. rs = a::b::rss` by
+    (Cases_on`rs` \\ fs[] \\
+     metis_tac[list_CASES,LENGTH_NIL,SUC_NOT]) >>
+  fs[]>>
+  first_x_assum(qspec_then`b::rss` mp_tac)>>
+  simp[]
+QED
+
 val _ = export_theory();