Add cv_rep for fUNION and fset_ABS for num fsets

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

@@ -475,6 +475,8 @@ 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
@@ -507,6 +509,29 @@ Proof
      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