1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7chapter Lib 8 9session Lib (lib) = Word_Lib + 10 sessions 11 "HOL-Library" 12 "HOL-Eisbach" 13 directories 14 "ml-helpers" 15 "subgoal_focus" 16 "Monad_WP" 17 "Monad_WP/wp" 18 theories 19 Lib 20 Apply_Trace_Cmd 21 AddUpdSimps 22 EmptyFailLib 23 List_Lib 24 SubMonadLib 25 Simulation 26 MonadEq 27 SimpStrategy 28 Extract_Conjunct 29 GenericLib 30 ProvePart 31 Corres_Adjust_Preconds 32 Requalify 33 Value_Abbreviation 34 Eisbach_Methods 35 HaskellLib_H 36 Eval_Bool 37 Bisim_UL 38 Extend_Locale 39 Solves_Tac 40 Crunch 41 Crunch_Instances_NonDet 42 Crunch_Instances_Trace 43 StateMonad 44 Corres_UL 45 Find_Names 46 LemmaBucket 47 Try_Methods 48 ListLibLemmas 49 Time_Methods_Cmd 50 Apply_Debug 51 MonadicRewrite 52 HaskellLemmaBucket 53 "ml-helpers/MkTermAntiquote" 54 "ml-helpers/TermPatternAntiquote" 55 "ml-helpers/TacticAntiquotation" 56 "ml-helpers/MLUtils" 57 "ml-helpers/TacticTutorial" 58 "ml-helpers/MkTermAntiquote_Tests" 59 "ml-helpers/TacticAntiquotation_Test" 60 "ml-helpers/TermPatternAntiquote_Tests" 61 FP_Eval 62 "subgoal_focus/Subgoal_Methods" 63 Insulin 64 ExtraCorres 65 NICTATools 66 BCorres_UL 67 Qualify 68 LexordList 69 Rule_By_Method 70 Defs 71 AutoLevity_Hooks 72 Distinct_Cmd 73 Match_Abbreviation 74 ShowTypes 75 SpecValid_R 76 EquivValid 77 SplitRule 78 DataMap 79 FastMap 80 RangeMap 81 Corres_Method 82 Conjuncts 83 DetWPLib 84 Guess_ExI 85 GenericTag 86 ML_Goal_Test 87 88 (* should really be a separate session, but too entangled atm: *) 89 NonDetMonadLemmaBucket 90 "Monad_WP/WhileLoopRules" 91 "Monad_WP/TraceMonad" 92 "Monad_WP/OptionMonadND" 93 "Monad_WP/OptionMonadWP" 94 "Monad_WP/Strengthen_Demo" 95 "Monad_WP/TraceMonadLemmas" 96 "Monad_WP/wp/WPBang" 97 "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