Add cv support for finite sets of nums (#1318)

* Add theorem: wf_list_to_num_set

* Add theorem: MEM_fset_REP

* Add support for num fset to cv_stdTheory

Not all operations are included here, but it's enough to get going with.

* Use Num 0 instead of from_unit () in cv_rep thm

* Add cv_rep for fEMPTY: num_set

* Add cv_rep for fUNION and fset_ABS for num fsets

src/finite_maps/sptreeScript.sml

@@ -1937,6 +1937,12 @@ Proof
   \\ rw[wf_insert]
 QED
 
+Theorem wf_list_to_num_set[simp]:
+  !ls. wf (list_to_num_set ls)
+Proof
+  Induct \\ rw[list_to_num_set_def, wf_insert]
+QED
+
 Theorem mapi_fromList:
   mapi f (fromList ls) = fromList (MAPi f ls)
 Proof

src/num/theories/cv_compute/automation/cv_stdScript.sml

@@ -1,11 +1,11 @@
 (*
   Apply cv translator to standard theories list, pair, sptree, etc.
 *)
-open HolKernel Parse boolLib bossLib;
+open HolKernel Parse boolLib bossLib dep_rewrite;
 open cv_typeTheory cvTheory cv_typeLib cv_repLib;
 open arithmeticTheory wordsTheory cv_repTheory cv_primTheory cv_transLib;
 open pairTheory listTheory optionTheory sumTheory alistTheory indexedListsTheory;
-open rich_listTheory sptreeTheory;
+open rich_listTheory sptreeTheory finite_setTheory;
 
 val _ = new_theory "cv_std";
 
@@ -446,6 +446,92 @@ Proof
   \\ rw []
 QED
 
+(*----------------------------------------------------------*
+   num fset
+ *----------------------------------------------------------*)
+
+val from_to_num_set = from_to_thm_for “:num_set”;
+val to_num_set = from_to_num_set |> concl |> rand;
+val from_num_set = from_to_num_set |> concl |> rator |> rand;
+
+Definition to_num_fset_def:
+  to_num_fset cv = fromSet (domain (^to_num_set cv))
+End
+
+Definition from_num_fset_def:
+  from_num_fset fs = ^from_num_set $ list_to_num_set $ fset_REP fs
+End
+
+Theorem from_to_num_fset[cv_from_to]:
+  from_to from_num_fset to_num_fset
+Proof
+  rw[from_to_def, from_num_fset_def, to_num_fset_def]
+  \\ rw[GSYM toSet_11, toSet_fromSet]
+  \\ mp_tac from_to_num_set
+  \\ gs[from_to_def, pred_setTheory.EXTENSION,
+        GSYM fIN_IN, domain_list_to_num_set, fIN_def]
+QED
+
+val from_sptree_sptree_spt_def = definition "from_sptree_sptree_spt_def";
+val cv_insert_thm = theorem "cv_insert_thm";
+val cv_lookup_thm = theorem "cv_lookup_thm";
+val cv_union_thm = theorem "cv_union_thm";
+val cv_list_to_num_set_thm = theorem "cv_list_to_num_set_thm";
+
+Theorem fEMPTY_num_cv_rep[cv_rep]:
+  from_num_fset fEMPTY = Num 0
+Proof
+  rw[from_num_fset_def,
+     Q.ISPEC`from_unit`(CONJUNCT1(GSYM from_sptree_sptree_spt_def))]
+  \\ AP_TERM_TAC
+  \\ DEP_REWRITE_TAC[spt_eq_thm]
+  \\ rw[lookup_list_to_num_set, wf_list_to_num_set, MEM_fset_REP]
+QED
+
+Theorem fINSERT_num_cv_rep[cv_rep]:
+  from_num_fset (fINSERT e s) =
+  cv_insert (Num e) (Num 0) (from_num_fset s)
+Proof
+  rw[from_num_fset_def, GSYM cv_insert_thm, GSYM from_unit_def]
+  \\ AP_TERM_TAC
+  \\ DEP_REWRITE_TAC[spt_eq_thm]
+  \\ rw[wf_insert, wf_list_to_num_set,
+        lookup_list_to_num_set, lookup_insert,
+        MEM_fset_REP]
+  \\ gs[]
+QED
+
+Theorem fIN_num_cv_rep[cv_rep]:
+  b2c (fIN e s) =
+  cv_ispair $ (cv_lookup (Num e) (from_num_fset s))
+Proof
+  rw[from_num_fset_def, GSYM cv_lookup_thm, from_option_def,
+     lookup_list_to_num_set, MEM_fset_REP]
+QED
+
+Theorem fUNION_num_cv_rep[cv_rep]:
+  from_num_fset (fUNION s1 s2) =
+  cv_union (from_num_fset s1) (from_num_fset s2)
+Proof
+  rw[from_num_fset_def, GSYM cv_union_thm]
+  \\ AP_TERM_TAC
+  \\ DEP_REWRITE_TAC[spt_eq_thm]
+  \\ simp[wf_list_to_num_set, wf_union,
+          lookup_list_to_num_set, lookup_union]
+  \\ rw[fUNION_def, MEM_fset_REP] \\ gs[]
+QED
+
+Theorem fset_ABS_num_cv_rep[cv_rep]:
+  from_num_fset (fset_ABS l) =
+  cv_list_to_num_set (from_list Num l)
+Proof
+  rw[from_num_fset_def, GSYM cv_list_to_num_set_thm]
+  \\ AP_TERM_TAC
+  \\ DEP_REWRITE_TAC[spt_eq_thm]
+  \\ simp[wf_list_to_num_set, lookup_list_to_num_set, MEM_fset_REP]
+  \\ simp[GSYM fromSet_set, IN_fromSet]
+QED
+
 (*----------------------------------------------------------*
    Misc.
  *----------------------------------------------------------*)

src/pred_set/src/more_theories/finite_setScript.sml

@@ -1111,6 +1111,19 @@ Proof
   simp[pred_setTheory.EXTENSION, GSYM fIN_IN, IN_fromSet]
 QED
 
+val fset_QUOTIENT = theorem"fset_QUOTIENT";
+
+Theorem fromSet_set:
+  !l. fromSet (set l) = fset_ABS l
+Proof
+  Induct \\ gvs[GSYM fEMPTY_def, fromSet_INSERT]
+  \\ rw[Once fINSERT_def, fsequiv_def]
+  \\ AP_TERM_TAC
+  \\ mp_tac fset_QUOTIENT
+  \\ rewrite_tac[quotientTheory.QUOTIENT_def] \\ strip_tac
+  \\ metis_tac[fsequiv_def]
+QED
+
 Theorem toSet_Qt:
   Qt (λx y. FINITE x /\ x = y) fromSet toSet (λs fs. s = toSet fs)
 Proof
@@ -1149,5 +1162,10 @@ Proof
   simp[FUN_REL_def, sfSETREL_def] >> metis_tac[]
 QED
 
+Theorem MEM_fset_REP:
+  MEM x (fset_REP fs) <=> fIN x fs
+Proof
+  rw[fIN_def]
+QED
 
 val _ = export_theory();