Move namespaceProps up one level

- Scott mentioned that it contains the correct rewrite for namespaceSub
CakeML · Feb 19, 2017 · 5c01e77 · 5c01e77
1 parent ba0206f
commit 5c01e77
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/semantics/proofs/namespacePropsScript.sml → semantics/namespacePropsScript.sml b/semantics/proofs/namespacePropsScript.sml → semantics/namespacePropsScript.sml
@@ -947,15 +947,15 @@ val nsMap_nsAppend = Q.store_thm ("nsMap_nsAppend",
   rw [nsAppend_def, nsMap_def]);
 
 val nsLookupMod_nsMap = Q.store_thm ("nsLookupMod_nsMap",
-  `!n x f. nsLookupMod (nsMap f n) x = lift (nsMap f) (nsLookupMod n x)`,
+  `!n x f. nsLookupMod (nsMap f n) x = OPTION_MAP (nsMap f) (nsLookupMod n x)`,
   ho_match_mp_tac nsLookupMod_ind >>
   rw [nsLookupMod_def, nsMap_def, ALOOKUP_MAP] >>
   every_case_tac >>
   rw [] >>
   fs []);
 
 val nsLookup_nsMap = Q.store_thm ("nsLookup_nsMap",
-  `!n x f. nsLookup (nsMap f n) x = lift f (nsLookup n x)`,
+  `!n x f. nsLookup (nsMap f n) x = OPTION_MAP f (nsLookup n x)`,
   ho_match_mp_tac nsLookup_ind >>
   rw [nsLookup_def, nsMap_def, ALOOKUP_MAP] >>
   every_case_tac >>

diff --git a/semantics/semanticsComputeLib.sml b/semantics/semanticsComputeLib.sml
@@ -20,7 +20,10 @@ open Parse
 val add_namespace_compset = computeLib.extend_compset
   [computeLib.Defs
     [namespaceTheory.mk_id_def
-    ,namespaceTheory.nsSub_def
+    ,namespacePropsTheory.nsSub_compute_thm
+    ,namespacePropsTheory.nsSub_compute_def
+    ,namespacePropsTheory.alistSub_def
+    ,namespacePropsTheory.alist_rel_restr_def
     ,namespaceTheory.nsDomMod_def
     ,namespaceTheory.nsDom_def
     ,namespaceTheory.nsAll2_def