From 3863d2214811727399e1373f795ad1f628530b3a Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Sun, 3 Dec 2023 17:03:26 +0000 Subject: [PATCH] Add fromList_fromAList --- src/finite_maps/sptreeScript.sml | 44 ++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/src/finite_maps/sptreeScript.sml b/src/finite_maps/sptreeScript.sml index 85cb26427a..88a5badd1a 100644 --- a/src/finite_maps/sptreeScript.sml +++ b/src/finite_maps/sptreeScript.sml @@ -1704,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 @@ -2418,6 +2437,31 @@ Proof 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