Update to Isabelle2023

RoboChart/ITree_RoboChart.thy

@@ -1,7 +1,9 @@
 section \<open> RoboChart semantics \<close>
 
 theory ITree_RoboChart
-  imports "Interaction_Trees.ITree_Extraction" "HOL-Library.Numeral_Type" 
+  imports "Interaction_Trees.ITree_Extraction"
+          "Interaction_Trees.ITree_Deadlock"
+          "HOL-Library.Numeral_Type" 
           "ITree_UTP.ITree_CSP_Biased"
 begin
 

RoboChart/RoboChart_Simulation.thy

@@ -12,9 +12,9 @@ begin
 generate_file \<open>code/simulate/Simulate.hs\<close> = \<open>
 module Simulate (simulate) where
 import Interaction_Trees;
-import Partial_Fun;
+import Prelude;
+-- import Partial_Fun;
 import System.IO;
-import qualified Data.List.Split;
 import qualified Data.List;
 
 -- These library functions help us to trim the "_C" strings from pretty printed events
@@ -29,7 +29,7 @@ removeSubstr w "" = "";
 removeSubstr w s@(c:cs) = (if w `isPrefixOf` s then Prelude.drop (Prelude.length w) s else c : removeSubstr w cs);
 
 replace :: String -> String -> String -> String;
-replace old new = Data.List.intercalate new . Data.List.Split.splitOn old;
+replace old new orig = orig;-- Data.List.intercalate new . old;
 
 renameGasEvent :: String -> String;
 renameGasEvent gas = 
@@ -165,7 +165,7 @@ fun simulate model thy =
   let val ctx = Named_Target.theory_init thy
       val ctx' =
         (Code_Target.export_code true [Code.read_const (Local_Theory.exit_global ctx) model] [((("Haskell", ""), SOME ({physical = false}, (Path.explode "simulate", Position.none))), (Token.explode (Thy_Header.get_keywords' @{context}) Position.none "string_classes"))] ctx)
-        |> prep_simulation model (Context.theory_name thy)
+        |> prep_simulation model (Context.theory_name {long = false} thy)
   in run_simulation (Local_Theory.exit_global ctx'); (Local_Theory.exit_global ctx')
   end 
 

RoboChart/examples/Patrol_Robot/Patrol_Robot.thy

@@ -1379,14 +1379,14 @@ export_code
   D__PatrolMod
   in Haskell 
   (* module_name RoboChart_basic *)
-  file_prefix RoboChart_basic_v1 
+  file_prefix Patrol_Robot 
   (string_classes) 
 
 text \<open>A simulation file is generated as a pure Haskell code. \<close>
-generate_file \<open>code/RoboChart_basic_v1/Simulate.hs\<close> = 
+generate_file \<open>code/Patrol_Robot/Simulate.hs\<close> = 
 \<open>module Simulate (simulate) where
 import qualified Interaction_Trees;
-import qualified Partial_Fun;
+-- import qualified Partial_Fun;
 
 isPrefixOf              :: (Eq a) => [a] -> [a] -> Bool;
 isPrefixOf [] _         =  True;
@@ -1406,8 +1406,8 @@ simulate_cnt n (Interaction_Trees.Sil p) =
                             }
                     else simulate_cnt (n + 1) p
      };
-simulate_cnt n (Interaction_Trees.Vis (Partial_Fun.Pfun_of_alist [])) = Prelude.putStrLn "Deadlocked.";
-simulate_cnt n t@(Interaction_Trees.Vis (Partial_Fun.Pfun_of_alist m)) =
+simulate_cnt n (Interaction_Trees.Vis (Interaction_Trees.Pfun_of_alist [])) = Prelude.putStrLn "Deadlocked.";
+simulate_cnt n t@(Interaction_Trees.Vis (Interaction_Trees.Pfun_of_alist m)) =
   do { Prelude.putStrLn ("Events:" ++ Prelude.concat (map (\(n, e) -> " (" ++ Prelude.show n ++ ") " ++ removeSubstr "_C" e ++ ";") (zip [1..] (map (Prelude.show . fst) m))));
        e <- Prelude.getLine;
        case (Prelude.reads e) of
@@ -1427,20 +1427,20 @@ text \<open>The @{verbatim Main.hs} generated below is the main module in the ge
 to compile and build the generated code to an executable file by ghc. We note a compiled version has 
 better performance than the interpreted version by ghci.
 \<close>
-generate_file \<open>code/RoboChart_basic_v1/Main.hs\<close> = 
+generate_file \<open>code/Patrol_Robot/Main.hs\<close> = 
 \<open>import qualified Interaction_Trees;
-import qualified Partial_Fun;
+-- import qualified Partial_Fun;
 import qualified Simulate;
-import qualified RoboChart_basic_v1;
+import qualified Patrol_Robot;
 
 main :: IO ()
 main =
   do
-    Simulate.simulate (RoboChart_basic_v1.d_PatrolMod 0);
+    Simulate.simulate (Patrol_Robot.d_PatrolMod 0);
 \<close>
 
 export_generated_files 
-  \<open>code/RoboChart_basic_v1/Simulate.hs\<close>
-  \<open>code/RoboChart_basic_v1/Main.hs\<close>
+  \<open>code/Patrol_Robot/Simulate.hs\<close>
+  \<open>code/Patrol_Robot/Main.hs\<close>
 
 end

RoboChart/examples/RoboChart_ChemicalDetector_autonomous/RoboChart_ChemicalDetector_autonomous_general.thy

@@ -87,7 +87,9 @@ Sect.~\ref{sec:chem_module}.
 section \<open> General definitions \label{sec:chem_general}\<close>
 
 theory RoboChart_ChemicalDetector_autonomous_general
-  imports "ITree_RoboChart.ITree_RoboChart" "ITree_RoboChart.RoboChart_Simulation"
+  imports "ITree_RoboChart.ITree_RoboChart" 
+          "ITree_Simulation.ITree_Simulation"
+          "ITree_RoboChart.RoboChart_Simulation"
           "Z_Toolkit.Bounded_List"
 begin
 

RoboChart/examples/RoboChart_basic/RoboChart_basic.thy

@@ -34,7 +34,8 @@ This theory, on the contrary, is built from the bottom up because the definition
 relies on the definitions of other processes in the top process. 
 \<close>
 theory RoboChart_basic
-  imports "ITree_RoboChart.ITree_RoboChart" "ITree_Simulation.ITree_Simulation"
+  imports "Interaction_Trees.ITree_Deadlock" 
+          "ITree_RoboChart.ITree_RoboChart" "ITree_Simulation.ITree_Simulation"
 begin
 
 text \<open>We, therefore, structure the theory as follows. In Sect.~\ref{ssec:basic_general}, we give