From 2d2cadb86b9a383a5ee209922c9cd1eaa78eaac0 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Tue, 24 Jan 2023 14:55:01 +1100
Subject: [PATCH] lib+proof+tools: move LemmaBucket_C into CParser

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 lib/ROOT                                       | 1 -
 lib/clib/Corres_UL_C.thy                       | 6 +++---
 lib/test/ShowTypes_Test.thy                    | 2 +-
 proof/crefine/ARM/CLevityCatch.thy             | 2 +-
 proof/crefine/ARM_HYP/CLevityCatch.thy         | 2 +-
 proof/crefine/RISCV64/CLevityCatch.thy         | 2 +-
 proof/crefine/X64/CLevityCatch.thy             | 2 +-
 tools/asmrefine/FieldAccessors.thy             | 2 +-
 tools/asmrefine/GraphRefine.thy                | 2 +-
 tools/autocorres/HeapLift.thy                  | 2 +-
 {lib/clib => tools/c-parser}/LemmaBucket_C.thy | 2 +-
 tools/c-parser/ROOT                            | 3 ++-
 12 files changed, 14 insertions(+), 14 deletions(-)
 rename {lib/clib => tools/c-parser}/LemmaBucket_C.thy (99%)

diff --git a/lib/ROOT b/lib/ROOT
index 2b90839bb..9b5a560d4 100644
--- a/lib/ROOT
+++ b/lib/ROOT
@@ -85,7 +85,6 @@ session CLib (lib) in clib = CParser +
     Simpl_Rewrite
     MonadicRewrite_C
     CTranslationNICTA
-    LemmaBucket_C
     SIMPL_Lemmas
     SimplRewrite
     BitFieldProofsLib
diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy
index 486aeb8ee..b3caa4333 100644
--- a/lib/clib/Corres_UL_C.thy
+++ b/lib/clib/Corres_UL_C.thy
@@ -11,9 +11,9 @@
 
 theory Corres_UL_C
 imports
-  "LemmaBucket_C"
-  "Lib.LemmaBucket"
-  "SIMPL_Lemmas"
+  CParser.LemmaBucket_C
+  Lib.LemmaBucket
+  SIMPL_Lemmas
 begin
 
 declare word_neq_0_conv [simp del]
diff --git a/lib/test/ShowTypes_Test.thy b/lib/test/ShowTypes_Test.thy
index ddf7dc758..097c544ab 100644
--- a/lib/test/ShowTypes_Test.thy
+++ b/lib/test/ShowTypes_Test.thy
@@ -7,7 +7,7 @@
 theory ShowTypes_Test
 imports
   Lib.ShowTypes
-  CLib.LemmaBucket_C
+  CParser.LemmaBucket_C
   CParser.CTranslation
 begin
 
diff --git a/proof/crefine/ARM/CLevityCatch.thy b/proof/crefine/ARM/CLevityCatch.thy
index cb74756fc..91d258017 100644
--- a/proof/crefine/ARM/CLevityCatch.thy
+++ b/proof/crefine/ARM/CLevityCatch.thy
@@ -8,7 +8,7 @@ theory CLevityCatch
 imports
   "CBaseRefine.Include_C"
   ArchMove_C
-  "CLib.LemmaBucket_C"
+  "CParser.LemmaBucket_C"
   "Lib.LemmaBucket"
 begin
 
diff --git a/proof/crefine/ARM_HYP/CLevityCatch.thy b/proof/crefine/ARM_HYP/CLevityCatch.thy
index 37a25da20..734f15bc4 100644
--- a/proof/crefine/ARM_HYP/CLevityCatch.thy
+++ b/proof/crefine/ARM_HYP/CLevityCatch.thy
@@ -8,7 +8,7 @@ theory CLevityCatch
 imports
   "CBaseRefine.Include_C"
   ArchMove_C
-  "CLib.LemmaBucket_C"
+  "CParser.LemmaBucket_C"
   "Lib.LemmaBucket"
 begin
 
diff --git a/proof/crefine/RISCV64/CLevityCatch.thy b/proof/crefine/RISCV64/CLevityCatch.thy
index 1de20de45..6692c171a 100644
--- a/proof/crefine/RISCV64/CLevityCatch.thy
+++ b/proof/crefine/RISCV64/CLevityCatch.thy
@@ -8,7 +8,7 @@ theory CLevityCatch
 imports
   "CBaseRefine.Include_C"
   ArchMove_C
-  "CLib.LemmaBucket_C"
+  "CParser.LemmaBucket_C"
   "Lib.LemmaBucket"
 begin
 
diff --git a/proof/crefine/X64/CLevityCatch.thy b/proof/crefine/X64/CLevityCatch.thy
index 8cc7860ec..878c3126e 100644
--- a/proof/crefine/X64/CLevityCatch.thy
+++ b/proof/crefine/X64/CLevityCatch.thy
@@ -8,7 +8,7 @@ theory CLevityCatch
 imports
   "CBaseRefine.Include_C"
   ArchMove_C
-  "CLib.LemmaBucket_C"
+  "CParser.LemmaBucket_C"
   "Lib.LemmaBucket"
 begin
 
diff --git a/tools/asmrefine/FieldAccessors.thy b/tools/asmrefine/FieldAccessors.thy
index a7a40e9cf..91eebad2f 100644
--- a/tools/asmrefine/FieldAccessors.thy
+++ b/tools/asmrefine/FieldAccessors.thy
@@ -7,7 +7,7 @@
 theory FieldAccessors
   imports
     Lib.Lib
-    CLib.LemmaBucket_C
+    CParser.LemmaBucket_C
 begin
 
 lemma h_val_mono:
diff --git a/tools/asmrefine/GraphRefine.thy b/tools/asmrefine/GraphRefine.thy
index a6ff07c9d..f0da597f8 100644
--- a/tools/asmrefine/GraphRefine.thy
+++ b/tools/asmrefine/GraphRefine.thy
@@ -10,7 +10,7 @@ imports
   TailrecPre
   GraphLangLemmas
   Lib.Lib
-  "CLib.LemmaBucket_C"
+  "CParser.LemmaBucket_C"
   ExtraSpecs
 begin
 
diff --git a/tools/autocorres/HeapLift.thy b/tools/autocorres/HeapLift.thy
index a8a5c46ad..e45ccf6f0 100644
--- a/tools/autocorres/HeapLift.thy
+++ b/tools/autocorres/HeapLift.thy
@@ -11,7 +11,7 @@ imports
   L2Defs
   ExecConcrete
   AbstractArrays
-  "CLib.LemmaBucket_C"
+  "CParser.LemmaBucket_C"
 begin
 
 definition "L2Tcorres st A C = corresXF st (\<lambda>r _. r) (\<lambda>r _. r) \<top> A C"
diff --git a/lib/clib/LemmaBucket_C.thy b/tools/c-parser/LemmaBucket_C.thy
similarity index 99%
rename from lib/clib/LemmaBucket_C.thy
rename to tools/c-parser/LemmaBucket_C.thy
index ab060f581..7a505ca17 100644
--- a/lib/clib/LemmaBucket_C.thy
+++ b/tools/c-parser/LemmaBucket_C.thy
@@ -7,7 +7,7 @@
 theory LemmaBucket_C
 imports
   Basics.CLib
-  CParser.TypHeapLib
+  TypHeapLib
 begin
 
 lemma Ptr_not_null_pointer_not_zero: "(Ptr p \<noteq> NULL)=(p\<noteq>0)"
diff --git a/tools/c-parser/ROOT b/tools/c-parser/ROOT
index 62e1fe7a7..cf43f0868 100644
--- a/tools/c-parser/ROOT
+++ b/tools/c-parser/ROOT
@@ -16,9 +16,10 @@ session CParser = "Simpl-VCG" +
   sessions
     "HOL-Library"
     "ML_Utils"
+    "Basics"
   directories
     "umm_heap"
     "umm_heap/$L4V_ARCH"
   theories
     "CTranslation"
-    "TypHeapLib"
\ No newline at end of file
+    "LemmaBucket_C"
\ No newline at end of file