adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib+spec+proof+autocorres: update for renamed Reader_Option_Monad 

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2023-07-07 15:03:17 +10:00 committed by Corey Lewis
parent 26f41e1764
commit 9b90b9e34a
14 changed files with 15 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/HaskellLib_H.thy
View File

@ -14,7 +14,7 @@ imports
Lib Lib
More_Numeral_Type More_Numeral_Type
Monads.NonDetMonadVCG Monads.NonDetMonadVCG
Monads.OptionMonad Monads.Reader_Option_Monad
begin begin
abbreviation (input) "flip \<equiv> swp" abbreviation (input) "flip \<equiv> swp"

2
lib/NonDetMonadLemmaBucket.thy
View File

@ -19,7 +19,7 @@ imports
Injection_Handler Injection_Handler
Monads.WhileLoopRulesCompleteness Monads.WhileLoopRulesCompleteness
"Word_Lib.Distinct_Prop" (* for distinct_tuple_helper *) "Word_Lib.Distinct_Prop" (* for distinct_tuple_helper *)
Monads.OptionMonadWP Monads.Reader_Option_VCG
begin begin
lemma distinct_tuple_helper: lemma distinct_tuple_helper:

2
lib/clib/Corres_UL_C.thy
View File

@ -14,7 +14,7 @@ imports
CParser.LemmaBucket_C CParser.LemmaBucket_C
Lib.LemmaBucket Lib.LemmaBucket
SIMPL_Lemmas SIMPL_Lemmas
Monads.OptionMonadWP Monads.Reader_Option_VCG
begin begin
declare word_neq_0_conv [simp del] declare word_neq_0_conv [simp del]

2
proof/sep-capDL/Lookups_D.thy
View File

@ -7,7 +7,7 @@
theory Lookups_D theory Lookups_D
imports imports
"DSpec.Syscall_D" "DSpec.Syscall_D"
"Monads.OptionMonadND" "Monads.Reader_Option_ND"
begin begin
type_synonym 'a lookup = "cdl_state \<Rightarrow> 'a option" type_synonym 'a lookup = "cdl_state \<Rightarrow> 'a option"

2
spec/design/m-skel/AARCH64/MachineTypes.thy
View File

@ -10,7 +10,7 @@ imports
Word_Lib.WordSetup Word_Lib.WordSetup
Monads.Empty_Fail Monads.Empty_Fail
Monads.No_Fail Monads.No_Fail
Monads.OptionMonadND Monads.Reader_Option_ND
Lib.HaskellLib_H Lib.HaskellLib_H
Platform Platform
begin begin

2
spec/design/m-skel/ARM/MachineTypes.thy
View File

@ -11,7 +11,7 @@ imports
Word_Lib.WordSetup Word_Lib.WordSetup
Monads.Empty_Fail Monads.Empty_Fail
Monads.No_Fail Monads.No_Fail
Monads.OptionMonadND Monads.Reader_Option_ND
Setup_Locale Setup_Locale
Platform Platform
begin begin

2
spec/design/m-skel/ARM_HYP/MachineTypes.thy
View File

@ -11,7 +11,7 @@ imports
Word_Lib.WordSetup Word_Lib.WordSetup
Monads.Empty_Fail Monads.Empty_Fail
Monads.No_Fail Monads.No_Fail
Monads.OptionMonadND Monads.Reader_Option_ND
Setup_Locale Setup_Locale
Platform Platform
begin begin

2
spec/design/m-skel/RISCV64/MachineTypes.thy
View File

@ -11,7 +11,7 @@ imports
Word_Lib.WordSetup Word_Lib.WordSetup
Monads.Empty_Fail Monads.Empty_Fail
Monads.No_Fail Monads.No_Fail
Monads.OptionMonadND Monads.Reader_Option_ND
Lib.HaskellLib_H Lib.HaskellLib_H
Platform Platform
begin begin

2
spec/design/m-skel/X64/MachineTypes.thy
View File

@ -11,7 +11,7 @@ imports
Word_Lib.WordSetup Word_Lib.WordSetup
Monads.Empty_Fail Monads.Empty_Fail
Monads.No_Fail Monads.No_Fail
Monads.OptionMonadND Monads.Reader_Option_ND
Lib.HaskellLib_H Lib.HaskellLib_H
Platform Platform
begin begin

2
tools/autocorres/AutoCorres.thy
View File

@ -21,7 +21,7 @@ imports
TypHeapSimple TypHeapSimple
HeapLift HeapLift
WordAbstract WordAbstract
"Monads.OptionMonadWP" "Monads.Reader_Option_VCG"
"Eisbach_Tools.Apply_Trace" "Eisbach_Tools.Apply_Trace"
AutoCorresSimpset AutoCorresSimpset
"ML_Utils.MkTermAntiquote" "ML_Utils.MkTermAntiquote"

2
tools/autocorres/MonadMono.thy
View File

@ -13,7 +13,7 @@ theory MonadMono
imports imports
NonDetMonadEx NonDetMonadEx
Monads.WhileLoopRulesCompleteness Monads.WhileLoopRulesCompleteness
Monads.OptionMonadWP Monads.Reader_Option_VCG
begin begin
(* (*

4
tools/autocorres/NonDetMonadEx.thy
View File

@ -16,7 +16,7 @@ imports
"Monads.More_NonDetMonadVCG" "Monads.More_NonDetMonadVCG"
"Monads.No_Throw" "Monads.No_Throw"
"Monads.No_Fail" "Monads.No_Fail"
"Monads.OptionMonadND" "Monads.Reader_Option_ND"
begin begin
(* (*
@ -276,7 +276,7 @@ lemma whileLoop_to_fold:
(\<lambda>r. return (Q r)) (\<lambda>r. return (Q r))
i s) = return (if P i \<le> x then fold (\<lambda>i r. (Q r)) [unat (P i) ..< unat x] i else i) s" i s) = return (if P i \<le> x then fold (\<lambda>i r. (Q r)) [unat (P i) ..< unat x] i else i) s"
(is "?LHS s = return (?RHS x) s") (is "?LHS s = return (?RHS x) s")
apply (subst OptionMonadND.gets_the_return [symmetric]) apply (subst Reader_Option_ND.gets_the_return [symmetric])
apply (subst gets_the_whileLoop) apply (subst gets_the_whileLoop)
apply (rule gets_the_to_return) apply (rule gets_the_to_return)
apply (subst owhile_to_fold) apply (subst owhile_to_fold)

2
tools/autocorres/TypeStrengthen.thy
View File

@ -14,7 +14,7 @@
theory TypeStrengthen theory TypeStrengthen
imports imports
L2Defs L2Defs
"Monads.OptionMonadND" "Monads.Reader_Option_ND"
ExecConcrete ExecConcrete
begin begin

2
tools/autocorres/tests/examples/FactorialTest.thy
View File

@ -10,7 +10,7 @@ Termination for recursive functions.
theory FactorialTest theory FactorialTest
imports imports
"AutoCorres.AutoCorres" "AutoCorres.AutoCorres"
"Monads.OptionMonadWP" "Monads.Reader_Option_VCG"
begin begin
external_file "factorial.c" external_file "factorial.c"