From dea1bb8f5fce4a203332380c3f434f18a7167767 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Tue, 18 Jul 2023 17:48:26 +1000 Subject: [PATCH] lib: consistent Trace filename prefix Signed-off-by: Corey Lewis --- lib/Crunch_Instances_Trace.thy | 2 +- lib/Monads/Monad_Lib.thy | 2 +- lib/Monads/README.md | 2 +- lib/Monads/ROOT | 6 +++--- lib/Monads/trace/{TraceMonadLemmas.thy => Trace_Lemmas.thy} | 4 ++-- lib/Monads/trace/{TraceMonad.thy => Trace_Monad.thy} | 2 +- lib/Monads/trace/{TraceMonadVCG.thy => Trace_VCG.thy} | 4 ++-- lib/concurrency/Prefix_Refinement.thy | 2 +- lib/concurrency/Triv_Refinement.thy | 2 +- 9 files changed, 13 insertions(+), 13 deletions(-) rename lib/Monads/trace/{TraceMonadLemmas.thy => Trace_Lemmas.thy} (99%) rename lib/Monads/trace/{TraceMonad.thy => Trace_Monad.thy} (99%) rename lib/Monads/trace/{TraceMonadVCG.thy => Trace_VCG.thy} (99%) diff --git a/lib/Crunch_Instances_Trace.thy b/lib/Crunch_Instances_Trace.thy index 49ce6f403c..e7966c63b8 100644 --- a/lib/Crunch_Instances_Trace.thy +++ b/lib/Crunch_Instances_Trace.thy @@ -7,7 +7,7 @@ theory Crunch_Instances_Trace imports Crunch - Monads.TraceMonadVCG + Monads.Trace_VCG begin lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE diff --git a/lib/Monads/Monad_Lib.thy b/lib/Monads/Monad_Lib.thy index 59add57c08..9147968b1c 100644 --- a/lib/Monads/Monad_Lib.thy +++ b/lib/Monads/Monad_Lib.thy @@ -5,7 +5,7 @@ *) (* This theory collects the minimum constant definitions and lemmas for the monad definition - theories (Nondet_Monad, TraceMonad etc). Only things that are necessary for these and needed + theories (Nondet_Monad, Trace_Monad etc). Only things that are necessary for these and needed by more than one of them should go in here. *) theory Monad_Lib diff --git a/lib/Monads/README.md b/lib/Monads/README.md index 4345c6b2ef..28d00f00e1 100644 --- a/lib/Monads/README.md +++ b/lib/Monads/README.md @@ -35,5 +35,5 @@ in weakest-precondition style. [l4v]: https://github.com/seL4/l4v/ [nondet]: ./nondet/Nondet_Monad.thy [option]: ./reader_option/Reader_Option_Monad.thy -[trace]: ./trace/TraceMonad.thy +[trace]: ./trace/Trace_Monad.thy [AutoCorres]: ../../tools/autocorres/ \ No newline at end of file diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT index c13eb42d2f..284039d3ba 100644 --- a/lib/Monads/ROOT +++ b/lib/Monads/ROOT @@ -22,17 +22,17 @@ session Monads (lib) = HOL + theories Nondet_WhileLoopRules - TraceMonad + Trace_Monad Reader_Option_ND Reader_Option_VCG Strengthen_Demo - TraceMonadLemmas + Trace_Lemmas Datatype_Schematic Nondet_WhileLoopRulesCompleteness Strengthen Nondet_Strengthen_Setup Reader_Option_Monad - TraceMonadVCG + Trace_VCG Nondet_In_Monad Nondet_VCG Nondet_Sat diff --git a/lib/Monads/trace/TraceMonadLemmas.thy b/lib/Monads/trace/Trace_Lemmas.thy similarity index 99% rename from lib/Monads/trace/TraceMonadLemmas.thy rename to lib/Monads/trace/Trace_Lemmas.thy index 45e4aedbeb..6b5533d811 100644 --- a/lib/Monads/trace/TraceMonadLemmas.thy +++ b/lib/Monads/trace/Trace_Lemmas.thy @@ -3,8 +3,8 @@ * * SPDX-License-Identifier: BSD-2-Clause *) -theory TraceMonadLemmas -imports TraceMonadVCG +theory Trace_Lemmas +imports Trace_VCG begin lemma mapM_Cons: diff --git a/lib/Monads/trace/TraceMonad.thy b/lib/Monads/trace/Trace_Monad.thy similarity index 99% rename from lib/Monads/trace/TraceMonad.thy rename to lib/Monads/trace/Trace_Monad.thy index 891d17ebec..506f8954ca 100644 --- a/lib/Monads/trace/TraceMonad.thy +++ b/lib/Monads/trace/Trace_Monad.thy @@ -3,7 +3,7 @@ * * SPDX-License-Identifier: BSD-2-Clause *) -theory TraceMonad +theory Trace_Monad imports Monad_Lib Strengthen diff --git a/lib/Monads/trace/TraceMonadVCG.thy b/lib/Monads/trace/Trace_VCG.thy similarity index 99% rename from lib/Monads/trace/TraceMonadVCG.thy rename to lib/Monads/trace/Trace_VCG.thy index fb75b3027e..9bdc420918 100644 --- a/lib/Monads/trace/TraceMonadVCG.thy +++ b/lib/Monads/trace/Trace_VCG.thy @@ -3,9 +3,9 @@ * * SPDX-License-Identifier: BSD-2-Clause *) -theory TraceMonadVCG +theory Trace_VCG imports - TraceMonad + Trace_Monad Fun_Pred_Syntax WPSimp begin diff --git a/lib/concurrency/Prefix_Refinement.thy b/lib/concurrency/Prefix_Refinement.thy index 336f673b89..774d3360f6 100644 --- a/lib/concurrency/Prefix_Refinement.thy +++ b/lib/concurrency/Prefix_Refinement.thy @@ -7,7 +7,7 @@ theory Prefix_Refinement imports Triv_Refinement - "Monads.TraceMonadLemmas" + "Monads.Trace_Lemmas" begin diff --git a/lib/concurrency/Triv_Refinement.thy b/lib/concurrency/Triv_Refinement.thy index 85ef2fd96f..caefd59834 100644 --- a/lib/concurrency/Triv_Refinement.thy +++ b/lib/concurrency/Triv_Refinement.thy @@ -6,7 +6,7 @@ theory Triv_Refinement imports - "Monads.TraceMonadVCG" + "Monads.Trace_VCG" "Monads.Strengthen" begin