1127668Sbms(* 2127668Sbms * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3127668Sbms * 4127668Sbms * SPDX-License-Identifier: BSD-2-Clause 5127668Sbms *) 6127668Sbms 7127668Sbmschapter Lib 8127668Sbms 9127668Sbmssession Lib (lib) = Word_Lib + 10127668Sbms sessions 11127668Sbms "HOL-Library" 12127668Sbms "HOL-Eisbach" 13127668Sbms directories 14127668Sbms "ml-helpers" 15127668Sbms "subgoal_focus" 16127668Sbms "Monad_WP" 17127668Sbms "Monad_WP/wp" 18127668Sbms theories 19127668Sbms Lib 20127668Sbms Apply_Trace_Cmd 21127668Sbms AddUpdSimps 22127668Sbms EmptyFailLib 23127668Sbms List_Lib 24127668Sbms SubMonadLib 25127668Sbms Simulation 26190207Srpaulo MonadEq 27127668Sbms SimpStrategy 28127668Sbms Extract_Conjunct 29127668Sbms GenericLib 30127668Sbms ProvePart 31127668Sbms Corres_Adjust_Preconds 32127668Sbms Requalify 33127668Sbms Value_Abbreviation 34127668Sbms Eisbach_Methods 35127668Sbms HaskellLib_H 36127668Sbms Eval_Bool 37127668Sbms Bisim_UL 38127668Sbms Extend_Locale 39127668Sbms Solves_Tac 40127668Sbms Crunch 41127668Sbms Crunch_Instances_NonDet 42127668Sbms Crunch_Instances_Trace 43127668Sbms StateMonad 44127668Sbms Corres_UL 45127668Sbms Find_Names 46127668Sbms LemmaBucket 47127668Sbms Try_Methods 48127668Sbms ListLibLemmas 49127668Sbms Time_Methods_Cmd 50127668Sbms Apply_Debug 51127668Sbms MonadicRewrite 52127668Sbms HaskellLemmaBucket 53127668Sbms "ml-helpers/MkTermAntiquote" 54127668Sbms "ml-helpers/TermPatternAntiquote" 55127668Sbms "ml-helpers/TacticAntiquotation" 56127668Sbms "ml-helpers/MLUtils" 57127668Sbms "ml-helpers/TacticTutorial" 58127668Sbms "ml-helpers/MkTermAntiquote_Tests" 59127668Sbms "ml-helpers/TacticAntiquotation_Test" 60127668Sbms "ml-helpers/TermPatternAntiquote_Tests" 61127668Sbms FP_Eval 62127668Sbms "subgoal_focus/Subgoal_Methods" 63127668Sbms Insulin 64127668Sbms ExtraCorres 65127668Sbms NICTATools 66127668Sbms BCorres_UL 67127668Sbms Qualify 68127668Sbms LexordList 69127668Sbms Rule_By_Method 70127668Sbms Defs 71127668Sbms AutoLevity_Hooks 72127668Sbms Distinct_Cmd 73190207Srpaulo Match_Abbreviation 74190207Srpaulo ShowTypes 75190207Srpaulo SpecValid_R 76190207Srpaulo EquivValid 77190207Srpaulo SplitRule 78190207Srpaulo DataMap 79190207Srpaulo FastMap 80190221Srpaulo RangeMap 81190207Srpaulo Corres_Method 82190207Srpaulo Conjuncts 83190207Srpaulo DetWPLib 84190221Srpaulo Guess_ExI 85190207Srpaulo GenericTag 86127668Sbms ML_Goal_Test 87127668Sbms 88127668Sbms (* should really be a separate session, but too entangled atm: *) 89127668Sbms NonDetMonadLemmaBucket 90146773Ssam "Monad_WP/WhileLoopRules" 91146773Ssam "Monad_WP/TraceMonad" 92146773Ssam "Monad_WP/OptionMonadND" 93146773Ssam "Monad_WP/OptionMonadWP" 94146773Ssam "Monad_WP/Strengthen_Demo" 95146773Ssam "Monad_WP/TraceMonadLemmas" 96146773Ssam "Monad_WP/wp/WPBang" 97146773Ssam "Monad_WP/wp/WPFix" 98 "Monad_WP/wp/Eisbach_WP" 99 "Monad_WP/wp/WPI" 100 "Monad_WP/wp/WPC" 101 "Monad_WP/wp/WPEx" 102 "Monad_WP/wp/WP_Pre" 103 "Monad_WP/wp/WP" 104 "Monad_WP/Datatype_Schematic" 105 "Monad_WP/WhileLoopRulesCompleteness" 106 "Monad_WP/Strengthen" 107 "Monad_WP/OptionMonad" 108 "Monad_WP/TraceMonadVCG" 109 "Monad_WP/NonDetMonadVCG" 110 "Monad_WP/NonDetMonad" 111 "Monad_WP/NonDetMonadLemmas" 112 113session CLib (lib) in clib = CParser + 114 sessions 115 "HOL-Library" 116 "HOL-Statespace" 117 "HOL-Eisbach" 118 "Simpl-VCG" 119 Lib 120 theories 121 Corres_UL_C 122 CCorresLemmas 123 CCorres_Rewrite 124 Simpl_Rewrite 125 MonadicRewrite_C 126 CTranslationNICTA 127 LemmaBucket_C 128 SIMPL_Lemmas 129 SimplRewrite 130 TypHeapLib 131 BitFieldProofsLib 132 XPres 133 134session CorresK in "CorresK" = Lib + 135 sessions 136 ASpec 137 ExecSpec 138 theories 139 CorresK_Lemmas 140 141session LibTest (lib) in test = Refine + 142 sessions 143 Lib 144 CLib 145 ASpec 146 ExecSpec 147 theories 148 Crunch_Test_NonDet 149 Crunch_Test_Qualified_NonDet 150 Crunch_Test_Qualified_Trace 151 Crunch_Test_Trace 152 WPTutorial 153 Match_Abbreviation_Test 154 Apply_Debug_Test 155 AutoLevity_Test 156 Insulin_Test 157 ShowTypes_Test 158 Time_Methods_Cmd_Test 159 FastMap_Test 160 RangeMap_Test 161 FP_Eval_Tests 162 Trace_Schematic_Insts_Test 163 Local_Method_Tests 164 Qualify_Test 165 Locale_Abbrev_Test 166 (* use virtual memory function as an example, only makes sense on ARM: *) 167 theories [condition = "L4V_ARCH_IS_ARM"] 168 Corres_Test 169 170session SepTactics (lib) in Hoare_Sep_Tactics = Sep_Algebra + 171 theories 172 Hoare_Sep_Tactics 173 174(* bitrotted 175session AutoLevity (lib) = HOL + 176 theories 177 AutoLevity 178 AutoLevity_Run 179 AutoLevity_Theory_Report 180*) 181 182session Concurrency (lib) in concurrency = HOL + 183 sessions 184 Lib 185 directories 186 "examples" 187 theories 188 Atomicity_Lib 189 Triv_Refinement 190 Prefix_Refinement 191 "examples/Peterson_Atomicity" 192 "examples/Plus2_Prefix" 193