From f0faa90f8ab7c159b606792a77bd873b4a44ebc5 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 17 Apr 2016 22:40:00 +0200 Subject: [PATCH] lib/spec/proof/tools: fix word change fallout --- lib/AutoLevity.thy | 2 +- lib/AutoLevity_Run.thy | 2 +- lib/Bisim_UL.thy | 2 +- lib/BitFieldProofsLib.thy | 16 +- lib/CTranslationNICTA.thy | 2 +- lib/Crunch_Test.thy | 2 +- lib/Etanercept.thy | 8 +- lib/ExpandAll.thy | 2 +- lib/GenericLib.thy | 2 +- lib/HaskellLib_H.thy | 5 +- lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy | 2 +- lib/LemmaBucket_C.thy | 14 +- lib/Methods.thy | 2 +- lib/Monad_WP/NonDetMonadLemmas.thy | 2 +- lib/Monad_WP/OptionMonad.thy | 3 +- lib/Monad_WP/OptionMonadND.thy | 2 +- lib/Monad_WP/OptionMonadWP.thy | 2 +- lib/MonadicRewrite.thy | 2 +- lib/NonDetMonadLemmaBucket.thy | 2 +- lib/ProvePart.thy | 12 +- lib/Rule_By_Method.thy | 14 +- lib/SimplRewrite.thy | 2 +- lib/StateMonad.thy | 2 +- lib/TSubst.thy | 4 +- lib/Trace_Attribs.thy | 2 +- lib/TypHeapLib.thy | 4 +- lib/{Monad_WP => }/WPTutorial.thy | 2 +- lib/WordSetup.thy | 2 +- lib/Word_Lib/HOL_Lemma_Bucket.thy | 2 +- lib/trace_attribs.ML | 2 +- proof/crefine/CSpace_C.thy | 14 +- proof/crefine/Delete_C.thy | 4 +- proof/crefine/Recycle_C.thy | 18 +-- proof/crefine/Tcb_C.thy | 5 +- proof/crefine/Wellformed_C.thy | 6 +- proof/drefine/Finalise_DR.thy | 4 +- proof/drefine/Untyped_DR.thy | 11 +- .../ARM/ArchLevityCatch_AI.thy | 2 +- .../invariant-abstract/ARM/ArchVSpace_AI.thy | 26 ++-- proof/invariant-abstract/Include_AI.thy | 2 +- proof/invariant-abstract/Untyped_AI.thy | 1 + proof/refine/ADT_H.thy | 6 +- proof/refine/ArchAcc_R.thy | 39 ++--- proof/refine/CNodeInv_R.thy | 2 +- proof/refine/IpcCancel_R.thy | 83 ++++------- proof/refine/Ipc_R.thy | 3 +- proof/refine/PageTableDuplicates.thy | 9 +- proof/refine/Refine.thy | 5 +- proof/refine/Retype_R.thy | 141 ++++++++---------- proof/refine/Schedule_R.thy | 2 +- spec/ROOT | 9 +- spec/abstract/ARM/ArchDecode_A.thy | 1 - spec/abstract/ARM/Machine_A.thy | 4 +- spec/abstract/CSpace_A.thy | 2 +- spec/abstract/Decode_A.thy | 1 - spec/abstract/KernelInit_A.thy | 8 +- spec/abstract/README.md | 4 +- spec/capDL/CSpace_D.thy | 2 - spec/capDL/Intents_D.thy | 2 +- spec/capDL/Monads_D.thy | 2 +- spec/capDL/PageTableUnmap_D.thy | 1 - spec/design/ARM/ArchInvocationLabels_H.thy | 4 +- spec/design/PSpaceStorable_H.thy | 1 - spec/design/m-skel/ARM/MachineTypes.thy | 6 +- .../skel/ARM/ArchInvocationLabels_H.thy | 4 +- spec/design/skel/PSpaceStorable_H.thy | 1 - spec/design/version | 2 +- spec/machine/ARM/MachineOps.thy | 2 - spec/machine/ARM/MachineTypes.thy | 6 +- spec/machine/ARM/Platform.thy | 2 +- spec/take-grant/Confine_S.thy | 2 +- spec/take-grant/System_S.thy | 2 +- tools/c-parser/CTranslation.thy | 31 ++-- tools/c-parser/termstypes.ML | 2 +- tools/c-parser/umm_heap/CTypesBase.thy | 2 +- tools/c-parser/umm_heap/CTypesDefs.thy | 2 - tools/c-parser/umm_heap/Vanilla32.thy | 2 +- 77 files changed, 277 insertions(+), 335 deletions(-) rename lib/{Monad_WP => }/WPTutorial.thy (99%) diff --git a/lib/AutoLevity.thy b/lib/AutoLevity.thy index cf946eab0..d880c8dca 100644 --- a/lib/AutoLevity.thy +++ b/lib/AutoLevity.thy @@ -8,7 +8,7 @@ * @TAG(NICTA_BSD) *) -theory AutoLevity +theory AutoLevity (* FIXME: broken *) imports "./proof_counting/ProofGraph" begin ML {* val infoflow_file = "~~/../lib/proof_counting/Noninterference_Refinement_graphs.xml" *} diff --git a/lib/AutoLevity_Run.thy b/lib/AutoLevity_Run.thy index 71df3d7ea..db828009c 100644 --- a/lib/AutoLevity_Run.thy +++ b/lib/AutoLevity_Run.thy @@ -8,7 +8,7 @@ * @TAG(NICTA_BSD) *) -theory AutoLevity_Run +theory AutoLevity_Run (* FIXME: broken *) imports AutoLevity begin diff --git a/lib/Bisim_UL.thy b/lib/Bisim_UL.thy index 3f862fdc2..ae4858a57 100644 --- a/lib/Bisim_UL.thy +++ b/lib/Bisim_UL.thy @@ -12,7 +12,7 @@ theory Bisim_UL imports - "wp/NonDetMonadVCG" + "Monad_WP/NonDetMonadVCG" Corres_UL EmptyFailLib begin diff --git a/lib/BitFieldProofsLib.thy b/lib/BitFieldProofsLib.thy index 3b724bbda..7c3af70e7 100644 --- a/lib/BitFieldProofsLib.thy +++ b/lib/BitFieldProofsLib.thy @@ -1,7 +1,17 @@ +(* + * Copyright 2016, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + theory BitFieldProofsLib - -imports TypHeapLib - +imports + Eisbach_Methods + TypHeapLib begin lemmas guard_simps = diff --git a/lib/CTranslationNICTA.thy b/lib/CTranslationNICTA.thy index aee2110d4..9e44585a9 100644 --- a/lib/CTranslationNICTA.thy +++ b/lib/CTranslationNICTA.thy @@ -11,7 +11,7 @@ theory CTranslationNICTA imports "../tools/c-parser/CTranslation" - "Word_Lib/WordLib" + "Word_Lib/Word_Lib" begin declare len_of_numeral_defs [simp del] diff --git a/lib/Crunch_Test.thy b/lib/Crunch_Test.thy index 91ec529a3..afe31b85a 100644 --- a/lib/Crunch_Test.thy +++ b/lib/Crunch_Test.thy @@ -9,7 +9,7 @@ *) -theory Crunch_Test +theory Crunch_Test (* FIXME: not tested *) imports Crunch Crunch_Test_Qualified GenericLib Defs begin diff --git a/lib/Etanercept.thy b/lib/Etanercept.thy index 105775078..006800d3d 100644 --- a/lib/Etanercept.thy +++ b/lib/Etanercept.thy @@ -8,11 +8,9 @@ * @TAG(NICTA_BSD) *) -theory Etanercept imports - "~~/src/HOL/Word/Word" - NICTACompat - SignedWords - WordBitwiseSigned +theory Etanercept (* FIXME: broken *) +imports + "Word_Lib/WordBitwise_Signed" "ml-helpers/TermPatternAntiquote" keywords "word_refute" :: diag diff --git a/lib/ExpandAll.thy b/lib/ExpandAll.thy index 75e1cb8a3..0109b4df5 100644 --- a/lib/ExpandAll.thy +++ b/lib/ExpandAll.thy @@ -8,7 +8,7 @@ * @TAG(NICTA_BSD) *) -theory ExpandAll +theory ExpandAll (* FIXME: bitrotted *) imports "~~/src/HOL/Main" begin diff --git a/lib/GenericLib.thy b/lib/GenericLib.thy index 02b2592e9..6978ce433 100644 --- a/lib/GenericLib.thy +++ b/lib/GenericLib.thy @@ -11,7 +11,7 @@ theory GenericLib imports Crunch - "wp/WPEx" + "Monad_WP/wp/WPEx" HaskellLemmaBucket begin diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy index accdd3ff4..3e9dc683c 100644 --- a/lib/HaskellLib_H.thy +++ b/lib/HaskellLib_H.thy @@ -17,14 +17,11 @@ theory HaskellLib_H imports Lib "Monad_WP/NonDetMonadVCG" - "Word_Lib/WordEnum" + "Word_Lib/Word_Enum" begin abbreviation (input) "flip \ swp" -(* add syntax here which conflicts with word shift \ - we can turn off this abbreviation later (with no_notation) - to avoid syntax conflicts *) abbreviation(input) bind_drop :: "('a, 'c) nondet_monad \ ('a, 'b) nondet_monad \ ('a, 'b) nondet_monad" (infixl ">>_" 60) where "bind_drop \ (\x y. bind x (K_bind y))" diff --git a/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy b/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy index f184e67c2..e5128dd53 100644 --- a/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy +++ b/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy @@ -10,7 +10,7 @@ theory Hoare_Sep_Tactics imports - "../wp/NonDetMonadVCG" + "../Monad_WP/NonDetMonadVCG" "../sep_algebra/Sep_Algebra_L4v" begin diff --git a/lib/LemmaBucket_C.thy b/lib/LemmaBucket_C.thy index b25176081..805585acd 100644 --- a/lib/LemmaBucket_C.thy +++ b/lib/LemmaBucket_C.thy @@ -10,9 +10,9 @@ theory LemmaBucket_C imports + Lib TypHeapLib - Aligned - WordLemmaBucket + "Word_Lib/Word_Lemmas_32" "../tools/c-parser/umm_heap/ArrayAssertion" begin @@ -651,13 +651,7 @@ lemma take_drop_foldl_concat: apply (induct x, simp_all)[1] apply simp done - -(* FIXME : Move to WordLib *) -lemma scast_of_nat [simp]: - "scast (of_nat x :: 'a::len signed word) = (of_nat x :: 'a word)" - by (metis (hide_lams, no_types) len_signed scast_def uint_sint - word_of_nat word_ubin.Abs_norm word_ubin.eq_norm) - + definition array_ptr_index :: "(('a :: c_type)['b :: finite]) ptr \ bool \ nat \ 'a ptr" where @@ -926,7 +920,7 @@ lemma h_t_valid_Array_element': apply (clarsimp simp: intvl_def) apply (drule_tac x="offs * size_of TYPE('a) + k" in spec) apply (drule mp) - apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def field_simps of_nat_nat) + apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def field_simps) apply (erule notE) apply (rule_tac y="Suc offs * size_of TYPE('a)" in order_less_le_trans) apply (simp add: size_of_def) diff --git a/lib/Methods.thy b/lib/Methods.thy index 9f2d6836a..b19d45481 100644 --- a/lib/Methods.thy +++ b/lib/Methods.thy @@ -8,7 +8,7 @@ * @TAG(NICTA_BSD) *) -theory Methods +theory Methods (* FIXME: bitrotted *) imports Lib begin diff --git a/lib/Monad_WP/NonDetMonadLemmas.thy b/lib/Monad_WP/NonDetMonadLemmas.thy index 6790dd809..a02795da4 100644 --- a/lib/Monad_WP/NonDetMonadLemmas.thy +++ b/lib/Monad_WP/NonDetMonadLemmas.thy @@ -292,7 +292,7 @@ lemma whileLoopE_unroll: apply (clarsimp simp: lift_def split: sum.splits) apply (subst whileLoop_unroll) apply (subst condition_false) - apply metis + apply fastforce apply (clarsimp simp: throwError_def) done diff --git a/lib/Monad_WP/OptionMonad.thy b/lib/Monad_WP/OptionMonad.thy index a3bceb83c..1809cf93f 100644 --- a/lib/Monad_WP/OptionMonad.thy +++ b/lib/Monad_WP/OptionMonad.thy @@ -7,6 +7,7 @@ * * @TAG(NICTA_BSD) *) + (* * Contributions by: * 2012 Lars Noschinski @@ -14,7 +15,7 @@ *) theory OptionMonad -imports Lib +imports "../Lib" (* FIXME: reduce dependencies *) begin type_synonym ('s,'a) lookup = "'s \ 'a option" diff --git a/lib/Monad_WP/OptionMonadND.thy b/lib/Monad_WP/OptionMonadND.thy index f89bdd3ee..5065acbaa 100644 --- a/lib/Monad_WP/OptionMonadND.thy +++ b/lib/Monad_WP/OptionMonadND.thy @@ -13,7 +13,7 @@ theory OptionMonadND imports OptionMonad - "wp/NonDetMonadLemmas" + NonDetMonadLemmas begin (* FIXME: better concrete syntax? *) diff --git a/lib/Monad_WP/OptionMonadWP.thy b/lib/Monad_WP/OptionMonadWP.thy index a39c3e316..72b4b5368 100644 --- a/lib/Monad_WP/OptionMonadWP.thy +++ b/lib/Monad_WP/OptionMonadWP.thy @@ -60,7 +60,7 @@ lemma obind_wp [wp]: lemma oreturn_wp [wp]: "ovalid (P x) (oreturn x) P" - by (simp add: ovalid_def oreturn_def K_def) + by (simp add: ovalid_def) lemma ocondition_wp [wp]: "\ ovalid L l Q; ovalid R r Q \ diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy index a6261c546..2c751ba87 100644 --- a/lib/MonadicRewrite.thy +++ b/lib/MonadicRewrite.thy @@ -12,7 +12,7 @@ theory MonadicRewrite imports - "wp/NonDetMonadVCG" + "Monad_WP/NonDetMonadVCG" Corres_UL EmptyFailLib LemmaBucket diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy index fbc141774..37891be71 100644 --- a/lib/NonDetMonadLemmaBucket.thy +++ b/lib/NonDetMonadLemmaBucket.thy @@ -11,7 +11,7 @@ theory NonDetMonadLemmaBucket imports "Monad_WP/NonDetMonadVCG" - "Word_Lib/WordLemmas32" + "Word_Lib/Word_Lemmas_32" "MonadEq" "Monad_WP/WhileLoopRulesCompleteness" begin diff --git a/lib/ProvePart.thy b/lib/ProvePart.thy index ef26de3c0..fa6196972 100644 --- a/lib/ProvePart.thy +++ b/lib/ProvePart.thy @@ -1,7 +1,15 @@ +(* + * Copyright 2015, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + theory ProvePart - imports Main - begin text {* Introduces a (sort-of) tactic for proving part of a goal by automatic diff --git a/lib/Rule_By_Method.thy b/lib/Rule_By_Method.thy index dd2b97270..e67578a42 100644 --- a/lib/Rule_By_Method.thy +++ b/lib/Rule_By_Method.thy @@ -1,5 +1,17 @@ +(* + * Copyright 2014, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + theory Rule_By_Method -imports Main "~~/src/HOL/Eisbach/Eisbach_Tools" +imports + Main + "~~/src/HOL/Eisbach/Eisbach_Tools" begin ML \ diff --git a/lib/SimplRewrite.thy b/lib/SimplRewrite.thy index e8551a3a4..f5a7dd480 100644 --- a/lib/SimplRewrite.thy +++ b/lib/SimplRewrite.thy @@ -8,7 +8,7 @@ * @TAG(NICTA_BSD) *) -theory SimplRewrite +theory SimplRewrite (* FIXME: bitrotted *) imports "CTranslationNICTA" "SplitRule" diff --git a/lib/StateMonad.thy b/lib/StateMonad.thy index 9a676b1e3..97b909c93 100644 --- a/lib/StateMonad.thy +++ b/lib/StateMonad.thy @@ -14,7 +14,7 @@ chapter "Monads" -theory StateMonad +theory StateMonad (* FIXME: bitrotted *) imports Lib begin diff --git a/lib/TSubst.thy b/lib/TSubst.thy index 900078b58..db25090f8 100644 --- a/lib/TSubst.thy +++ b/lib/TSubst.thy @@ -8,7 +8,7 @@ * @TAG(NICTA_BSD) *) -theory TSubst +theory TSubst (* FIXME: bitrotted *) imports Main begin @@ -40,7 +40,7 @@ method_setup tsubst = |> Seq.map (singleton (Variable.export ctxt3 ctxt')) end)) ctxt 1))) *} -schematic_lemma +schematic_goal assumes a: "\x y. P x \ P y" fixes x :: 'b shows "\x ::'a :: type. ?Q x \ P x \ ?Q x" diff --git a/lib/Trace_Attribs.thy b/lib/Trace_Attribs.thy index 8a064e059..ce43e7909 100644 --- a/lib/Trace_Attribs.thy +++ b/lib/Trace_Attribs.thy @@ -36,7 +36,7 @@ * a hopefully-sensible set of differences. *) -theory Trace_Attribs +theory Trace_Attribs (* FIXME: bitrotted *) imports HOL keywords "diff_attributes" :: thy_decl diff --git a/lib/TypHeapLib.thy b/lib/TypHeapLib.thy index 0b9765490..1b708ad0e 100644 --- a/lib/TypHeapLib.thy +++ b/lib/TypHeapLib.thy @@ -13,10 +13,10 @@ imports "../tools/c-parser/CTranslation" begin (* This file contains everything you need to know and use for the - day-to-day solving of TypHeap related goals. See KernelState,thy for + day-to-day solving of TypHeap related goals. See KernelState.thy for abbreviations for cslift etc. *) -section "abbreviations and helpers" +section "Abbreviations and helpers" (* The idea here is to make sure that all abbreviations have defs that let you know they are an abbrev. *) definition "is_an_abbreviation \ True" diff --git a/lib/Monad_WP/WPTutorial.thy b/lib/WPTutorial.thy similarity index 99% rename from lib/Monad_WP/WPTutorial.thy rename to lib/WPTutorial.thy index f6ecd0a02..cd0d992ca 100644 --- a/lib/Monad_WP/WPTutorial.thy +++ b/lib/WPTutorial.thy @@ -9,7 +9,7 @@ *) theory WPTutorial -imports Bits_R +imports "../proof/refine/Bits_R" begin text {* diff --git a/lib/WordSetup.thy b/lib/WordSetup.thy index 31fc7b901..d82f7e7b6 100644 --- a/lib/WordSetup.thy +++ b/lib/WordSetup.thy @@ -11,7 +11,7 @@ chapter "Machine Word Setup" theory WordSetup -imports "Word_Lib/Word_Enum" +imports "Word_Lib/Word_Lemmas_32" begin text {* This theory defines the standard platform-specific word size diff --git a/lib/Word_Lib/HOL_Lemma_Bucket.thy b/lib/Word_Lib/HOL_Lemma_Bucket.thy index 7c4a2de53..829309785 100644 --- a/lib/Word_Lib/HOL_Lemma_Bucket.thy +++ b/lib/Word_Lib/HOL_Lemma_Bucket.thy @@ -2179,7 +2179,7 @@ lemma dvd_reduce_multiple: shows "(k dvd k * m + n) = (k dvd n)" by (induct m) (auto simp: add_ac) -lemma image_iff: +lemma image_iff2: "inj f \ f x \ f ` S = (x \ S)" by (rule inj_image_mem_iff) diff --git a/lib/trace_attribs.ML b/lib/trace_attribs.ML index ca01da79f..19ac5640f 100644 --- a/lib/trace_attribs.ML +++ b/lib/trace_attribs.ML @@ -110,7 +110,7 @@ fun ugly_print_term t = (* Render a thm to a string. *) fun render_thm _ thm = - prop_of thm + Thm.prop_of thm |> ugly_print_term |> SHA1.digest |> SHA1.rep diff --git a/proof/crefine/CSpace_C.thy b/proof/crefine/CSpace_C.thy index 0a3db1ed1..a9000f1bd 100644 --- a/proof/crefine/CSpace_C.thy +++ b/proof/crefine/CSpace_C.thy @@ -3862,11 +3862,8 @@ lemma cap_small_frame_cap_set_capFMappedASID_spec: cap_small_frame_cap_CL.capFMappedASIDLow_CL := \<^bsup>s\<^esup>asid && mask asidLowBits \ \ cap_get_tag \ret__struct_cap_C = scast cap_small_frame_cap\" apply vcg - apply (clarsimp simp: Kernel_C.asidLowBits_def word_sle_def - Kernel_C.asidHighBits_def asid_low_bits_def - asid_high_bits_def mask_def) - apply (simp add: word_bw_assocs) - done + by (clarsimp simp: Kernel_C.asidLowBits_def word_sle_def + Kernel_C.asidHighBits_def asid_low_bits_def asid_high_bits_def mask_def) lemma cap_frame_cap_set_capFMappedASID_spec: "\s. \ \ \s. cap_get_tag \<^bsup>s\<^esup>cap = scast cap_frame_cap\ @@ -3877,11 +3874,8 @@ lemma cap_frame_cap_set_capFMappedASID_spec: cap_frame_cap_CL.capFMappedASIDLow_CL := \<^bsup>s\<^esup>asid && mask asidLowBits \ \ cap_get_tag \ret__struct_cap_C = scast cap_frame_cap\" apply vcg - apply (clarsimp simp: Kernel_C.asidLowBits_def word_sle_def - Kernel_C.asidHighBits_def asid_low_bits_def - asid_high_bits_def mask_def) - apply (simp add: word_bw_assocs) - done + by (clarsimp simp: Kernel_C.asidLowBits_def word_sle_def + Kernel_C.asidHighBits_def asid_low_bits_def asid_high_bits_def mask_def) lemma Arch_deriveCap_ccorres: "ccorres (syscall_error_rel \ (ccap_relation \ ArchObjectCap)) deriveCap_xf diff --git a/proof/crefine/Delete_C.thy b/proof/crefine/Delete_C.thy index 4c8be3f69..d5fe438e4 100644 --- a/proof/crefine/Delete_C.thy +++ b/proof/crefine/Delete_C.thy @@ -711,6 +711,8 @@ schematic_goal finaliseSlot_ccorres_induction_helper: done lemma finaliseSlot_ccorres: + notes from_bool_neq_0 [simp del] + shows "ccorres (cintr \ (\(success, irqopt) (success', irq'). success' = from_bool success \ irq_opt_relation irqopt irq')) (liftxf errstate finaliseSlot_ret_C.status_C (\v. (success_C v, finaliseSlot_ret_C.irq_C v)) ret__struct_finaliseSlot_ret_C_') @@ -881,7 +883,7 @@ lemma finaliseSlot_ccorres: apply (clarsimp simp: throwError_def return_def cintr_def) apply vcg apply (wp preemptionPoint_invR) - apply simp + apply simp apply simp apply (rule ccorres_split_throws) apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) diff --git a/proof/crefine/Recycle_C.thy b/proof/crefine/Recycle_C.thy index ed04625ff..dba8f1bc7 100644 --- a/proof/crefine/Recycle_C.thy +++ b/proof/crefine/Recycle_C.thy @@ -695,6 +695,7 @@ lemma arch_recycleCap_ccorres: notes Collect_const [simp del] notes ccorres_if_True_False_simps [simp] notes if_cong[cong] + notes from_bool_neq_0 [simp del] shows "ccorres (ccap_relation o ArchObjectCap) ret__struct_cap_C_' (invs' and valid_cap' (ArchObjectCap cp) and (\s. 2 ^ acapBits cp \ gsMaxObjectSize s) @@ -708,10 +709,9 @@ lemma arch_recycleCap_ccorres: apply (simp add: ARM_H.recycleCap_def cap_get_tag_isCap cap_get_tag_isCap_ArchObject isArchPageCap_ArchObjectCap - del: Collect_const cong: call_ignore_cong) + cong: call_ignore_cong) apply (rule ccorres_if_lhs) - apply (simp add: ccorres_cond_iffs Collect_True - del: Collect_const) + apply (simp add: ccorres_cond_iffs Collect_True) apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_symb_exec_r) apply (rule ccorres_Guard_Seq) @@ -725,9 +725,8 @@ lemma arch_recycleCap_ccorres: apply vcg apply (rule conseqPre, vcg, clarsimp) apply (rule ccorres_if_lhs) - apply (simp add: ccorres_cond_iffs Collect_True Collect_False - Let_def - del: Collect_const cong: call_ignore_cong) + apply (simp add: ccorres_cond_iffs Collect_True Collect_False Let_def + cong: call_ignore_cong) apply (rule ccorres_rhs_assoc)+ apply (csymbr, csymbr, csymbr) apply (subst bind_assoc[symmetric]) @@ -770,8 +769,7 @@ lemma arch_recycleCap_ccorres: ccap_relation_def option_map_Some_eq2) apply (rule ccorres_if_lhs) apply (simp add: ccorres_cond_iffs Collect_True Collect_False - Let_def ARMSectionBits_def - del: Collect_const) + Let_def ARMSectionBits_def) apply (rule ccorres_rhs_assoc)+ apply (csymbr, csymbr) apply (rule ccorres_Guard_Seq)+ @@ -829,7 +827,7 @@ lemma arch_recycleCap_ccorres: update_pde_map_to_pdes carray_map_relation_upd_triv) apply (rule cmap_relation_updI, simp_all)[1] subgoal by (simp add: cpde_relation_def Let_def pde_lift_def - fcp_beta pde_get_tag_def pde_tag_defs) + pde_get_tag_def pde_tag_defs) subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def typ_heap_simps pde_stored_asid_update_valid_offset update_pde_map_tos) @@ -854,7 +852,7 @@ lemma arch_recycleCap_ccorres: apply (rule ccorres_split_nothrowE) apply (ctac add: findPDForASID_ccorres) apply ceqv - apply (simp add: liftE_liftM when_def dc_def[symmetric] del: Collect_const) + apply (simp add: liftE_liftM when_def dc_def[symmetric]) apply (rule ccorres_cond2[where R=\]) apply fastforce apply (ctac add: invalidateTLBByASID_ccorres) diff --git a/proof/crefine/Tcb_C.thy b/proof/crefine/Tcb_C.thy index 9841e7394..4a2b1cec5 100644 --- a/proof/crefine/Tcb_C.thy +++ b/proof/crefine/Tcb_C.thy @@ -2524,8 +2524,9 @@ lemma slotCapLongRunningDelete_ccorres: split: capability.split)[1] apply simp apply (wp hoare_drop_imps isFinalCapability_inv) - apply (clarsimp simp: Collect_const_mem guard_is_UNIV_def - from_bool_0 false_def true_def) + apply (clarsimp simp: Collect_const_mem guard_is_UNIV_def) + apply (rename_tac rv') + apply (case_tac rv'; clarsimp simp: false_def true_def) apply vcg apply (rule conseqPre, vcg, clarsimp) apply (clarsimp simp: cte_wp_at_ctes_of) diff --git a/proof/crefine/Wellformed_C.thy b/proof/crefine/Wellformed_C.thy index ea66f8846..276104fe9 100644 --- a/proof/crefine/Wellformed_C.thy +++ b/proof/crefine/Wellformed_C.thy @@ -282,11 +282,7 @@ lemma to_bool_to_bool_bf: lemma to_bool_bf_mask_1 [simp]: "to_bool_bf (w && mask (Suc 0)) = to_bool_bf w" - apply (simp add: to_bool_bf_def) - apply (rule eq_eqI) - apply (rule word_eqI) - apply simp - done + by (simp add: to_bool_bf_def) lemma to_bool_bf_and [simp]: "to_bool_bf (a && b) = (to_bool_bf a \ to_bool_bf (b::word32))" diff --git a/proof/drefine/Finalise_DR.thy b/proof/drefine/Finalise_DR.thy index f45fb522d..419a5091c 100644 --- a/proof/drefine/Finalise_DR.thy +++ b/proof/drefine/Finalise_DR.thy @@ -1859,7 +1859,7 @@ lemma dcorres_unmap_large_section: apply simp apply (subgoal_tac "0 < (of_nat (slot * 4)::word32)") apply simp - apply (rule le_less_trans[OF _ of_nat_mono_maybe[where Y = 0]]) + apply (rule le_less_trans[OF _ of_nat_mono_maybe[where y = 0]]) apply fastforce apply simp apply fastforce @@ -1971,7 +1971,7 @@ lemma dcorres_unmap_large_page: apply simp apply (subgoal_tac "0 < (of_nat (x * 4)::word32)") apply simp - apply (rule le_less_trans[OF _ of_nat_mono_maybe[where Y = 0]]) + apply (rule le_less_trans[OF _ of_nat_mono_maybe[where y = 0]]) apply fastforce apply simp apply fastforce diff --git a/proof/drefine/Untyped_DR.thy b/proof/drefine/Untyped_DR.thy index 5a91b70d7..b6ebfad95 100644 --- a/proof/drefine/Untyped_DR.thy +++ b/proof/drefine/Untyped_DR.thy @@ -443,14 +443,11 @@ lemma transform_default_object: split: aobject_type.split nat.splits) lemma obj_bits_bound32: - "\type = Structures_A.Untyped \ us < 32; - type = Structures_A.CapTableObject \ us < 28\ - \obj_bits_api type us < WordSetup.word_bits" - apply (case_tac type) - apply (simp_all add:obj_bits_api_def word_bits_def slot_bits_def) + "\type = Structures_A.Untyped \ us < 32; type = Structures_A.CapTableObject \ us < 28\ + \ obj_bits_api type us < word_bits" + apply (case_tac type; simp add:obj_bits_api_def word_bits_def slot_bits_def) apply (rename_tac aobject_type) - apply (case_tac aobject_type) - apply (simp_all add:arch_kobj_size_def default_arch_object_def pageBits_def) + apply (case_tac aobject_type; simp add:arch_kobj_size_def default_arch_object_def pageBits_def) done lemma obj_bits_bound4: diff --git a/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy b/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy index a79e95985..cf228d5af 100644 --- a/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy +++ b/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy @@ -57,7 +57,7 @@ lemma asid_high_bits_of_add: apply (case_tac "na < asid_low_bits") apply (simp add: asid_low_bits_def linorder_not_less word_bits_def) apply (auto dest: test_bit_size - simp: asid_low_bits_def nth_ucast) + simp: asid_low_bits_def word_bits_def nth_ucast) done lemma preemption_point_success [simp,intro]: diff --git a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy index 282848761..3f0860166 100644 --- a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy @@ -56,18 +56,18 @@ lemma asid_low_high_bits: x \ 2 ^ asid_bits - 1; y \ 2 ^ asid_bits - 1 \ \ x = y" apply (rule word_eqI) - apply (simp add: word_less_sub_le upper_bits_unset_is_l2p [symmetric] bang_eq nth_ucast word_size) + apply (simp add: upper_bits_unset_is_l2p_32 [symmetric] bang_eq nth_ucast word_size) apply (clarsimp simp: asid_high_bits_of_def nth_ucast nth_shiftr) apply (simp add: asid_high_bits_def asid_bits_def asid_low_bits_def word_bits_def) subgoal premises prems[rule_format] for n - apply (cases "n < 10") - using prems(1) + apply (cases "n < 10") + using prems(1) apply fastforce - apply (cases "n < 18") - using prems(2)[where n="n - 10"] - apply fastforce - using prems(3-) - by (simp add: linorder_not_less) + apply (cases "n < 18") + using prems(2)[where n="n - 10"] + apply fastforce + using prems(3-) + by (simp add: linorder_not_less) done lemma asid_low_high_bits': @@ -689,7 +689,7 @@ lemma ex_asid_high_bits_plus: apply (simp add: mask_def) apply (rule word_and_le1) apply (subst (asm) mask_def) - apply (simp add: upper_bits_unset_is_l2p [symmetric]) + apply (simp add: upper_bits_unset_is_l2p_32 [symmetric]) apply (subst word_plus_and_or_coroll) apply (rule word_eqI) apply (clarsimp simp: word_size nth_ucast nth_shiftl) @@ -710,7 +710,7 @@ lemma ex_asid_high_bits_plus: lemma asid_high_bits_shl: "\ is_aligned base asid_low_bits; base \ mask asid_bits \ \ ucast (asid_high_bits_of base) << asid_low_bits = base" - apply (simp add: mask_def upper_bits_unset_is_l2p [symmetric]) + apply (simp add: mask_def upper_bits_unset_is_l2p_32 [symmetric]) apply (rule word_eqI) apply (simp add: is_aligned_nth nth_ucast nth_shiftl nth_shiftr asid_low_bits_def asid_high_bits_of_def word_size asid_bits_def word_bits_def) @@ -1802,7 +1802,7 @@ lemma vs_lookup: apply (rule order_trans) apply (rule Image_mono [OF _ order_refl]) apply (rule vs_lookup_trans) - apply (clarsimp simp: rel_comp_Image Un_Image) + apply (clarsimp simp: relcomp_Image Un_Image) done lemma vs_lookup2: @@ -4770,7 +4770,7 @@ lemma new_lookups_rtrancl: lemma vs_lookup: "vs_lookup s' = vs_lookup s \ new_lookups^* `` vs_lookup s" unfolding vs_lookup_def - by (simp add: vs_lookup_trans rel_comp_Image Un_Image) + by (simp add: vs_lookup_trans relcomp_Image Un_Image) lemma vs_lookup2: "vs_lookup s' = vs_lookup s \ (new_lookups `` vs_lookup s)" @@ -4804,7 +4804,7 @@ lemma vs_lookup_pages: "vs_lookup_pages s' = vs_lookup_pages s \ new_lookups^* `` vs_lookup_pages s" unfolding vs_lookup_pages_def - by (simp add: vs_lookup_pages_trans rel_comp_Image Un_Image) + by (simp add: vs_lookup_pages_trans relcomp_Image Un_Image) lemma vs_lookup_pages2: "vs_lookup_pages s' = vs_lookup_pages s \ (new_lookups `` vs_lookup_pages s)" diff --git a/proof/invariant-abstract/Include_AI.thy b/proof/invariant-abstract/Include_AI.thy index 6347e3311..f8ce7e623 100644 --- a/proof/invariant-abstract/Include_AI.thy +++ b/proof/invariant-abstract/Include_AI.thy @@ -12,7 +12,7 @@ theory Include_AI imports BCorres_AI "./$L4V_ARCH/ArchCrunchSetup_AI" - "../../lib/wp/Eisbach_WP" + "../../lib/Monad_WP/wp/Eisbach_WP" "../../spec/abstract/Syscall_A" "../../lib/LemmaBucket" "../../lib/ListLibLemmas" diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index c8d1a39f7..72a16350c 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -1047,6 +1047,7 @@ lemma default_non_Null[simp]: "cap.NullCap \ default_cap tp oref sz" by (cases tp, simp_all) +end locale vo_abs = vmdb_abs + assumes valid_objs: "valid_objs s" diff --git a/proof/refine/ADT_H.thy b/proof/refine/ADT_H.thy index 225c70a66..959513867 100644 --- a/proof/refine/ADT_H.thy +++ b/proof/refine/ADT_H.thy @@ -805,7 +805,7 @@ proof - apply (rule pspace_aligned_distinct_None' [OF pspace_aligned pspace_distinct], simp+) apply (cut_tac x=ya and n="2^10" in - ucast_less_shiftl_helper[simplified word_bits_conv], simp+) + ucast_less_shiftl_helper[where 'a=32,simplified word_bits_conv], simp+) apply (clarsimp simp add: word_gt_0) apply clarsimp apply (subgoal_tac "ucast ya << 2 = 0") @@ -813,7 +813,6 @@ proof - apply (rule ccontr) apply (frule_tac x=y in unaligned_helper, assumption) apply (rule ucast_less_shiftl_helper, simp_all) - apply (simp add: word_bits_conv) apply (rule ext) apply (frule pspace_relation_absD[OF _ pspace_relation]) apply simp @@ -851,7 +850,7 @@ proof - apply (rule pspace_aligned_distinct_None' [OF pspace_aligned pspace_distinct], simp+) apply (cut_tac x=ya and n="2^14" in - ucast_less_shiftl_helper[simplified word_bits_conv], simp+) + ucast_less_shiftl_helper[where 'a=32, simplified word_bits_conv], simp+) apply (clarsimp simp add: word_gt_0) apply clarsimp apply (subgoal_tac "ucast ya << 2 = 0") @@ -859,7 +858,6 @@ proof - apply (rule ccontr) apply (frule_tac x=y in unaligned_helper, assumption) apply (rule ucast_less_shiftl_helper, simp_all) - apply (simp add: word_bits_conv) apply (rule ext) apply (frule pspace_relation_absD[OF _ pspace_relation]) apply simp diff --git a/proof/refine/ArchAcc_R.thy b/proof/refine/ArchAcc_R.thy index 7eafef9c3..0a06480e0 100644 --- a/proof/refine/ArchAcc_R.thy +++ b/proof/refine/ArchAcc_R.thy @@ -388,10 +388,9 @@ lemma get_master_pde_corres: apply (clarsimp simp:pde_relation_aligned_def split:if_splits ARM_H.pde.splits) apply (drule_tac p' = "p && ~~ mask 6" in valid_duplicates'_D[rotated]) - apply (simp add:is_aligned_neg_mask is_aligned_weaken[where y = 2]) - apply (clarsimp simp: vs_ptr_align_def) - apply (simp add:and_not_mask_twice) - apply simp + apply (simp add:is_aligned_neg_mask is_aligned_weaken[where y = 2]) + apply (clarsimp simp: vs_ptr_align_def) + apply (simp add:and_not_mask_twice) apply (drule_tac x = "(ucast ((p && ~~ mask 6) && mask pd_bits >> 2))" in pde_relation_alignedD) apply assumption apply (simp add:expand) @@ -413,10 +412,9 @@ lemma get_master_pde_corres: apply (clarsimp simp:pde_relation_aligned_def split:if_splits ARM_H.pde.splits) apply (drule_tac p' = "p && ~~ mask 6" in valid_duplicates'_D[rotated]) - apply (simp add:is_aligned_neg_mask is_aligned_weaken[where y = 2]) - apply (clarsimp simp: vs_ptr_align_def) - apply (simp add:and_not_mask_twice) - apply simp + apply (simp add:is_aligned_neg_mask is_aligned_weaken[where y = 2]) + apply (clarsimp simp: vs_ptr_align_def) + apply (simp add:and_not_mask_twice) apply (drule_tac x = "(ucast ((p && ~~ mask 6) && mask pd_bits >> 2))" in pde_relation_alignedD) apply assumption apply (simp add: expand) @@ -633,10 +631,9 @@ lemma get_master_pte_corres: apply (clarsimp simp:pte_relation_aligned_def split:if_splits ARM_H.pte.splits) apply (drule_tac p' = "p && ~~ mask 6" in valid_duplicates'_D[rotated]) - apply (simp add:is_aligned_weaken[where y = 2] is_aligned_neg_mask) - apply (clarsimp simp: vs_ptr_align_def) - apply (simp add:and_not_mask_twice) - apply simp + apply (simp add:is_aligned_weaken[where y = 2] is_aligned_neg_mask) + apply (clarsimp simp: vs_ptr_align_def) + apply (simp add:and_not_mask_twice) apply (frule_tac x = "(ucast ((p && ~~ mask 6) && mask pt_bits >> 2))" in pte_relation_alignedD) apply assumption apply (simp add:expand) @@ -671,8 +668,7 @@ lemma get_master_pte_corres: apply assumption apply (rename_tac pte) apply (case_tac pte) - apply (simp_all add:pte_relation_aligned_def - is_aligned_mask[symmetric])+ + apply (simp_all add:pte_relation_aligned_def is_aligned_mask[symmetric]) apply (drule_tac p = "p && ~~ mask 6" and p' = p in valid_duplicates'_D) apply assumption apply simp @@ -694,10 +690,9 @@ lemma get_master_pte_corres: apply (clarsimp simp:pte_relation_aligned_def split:if_splits ARM_H.pte.splits) apply (drule_tac p' = "p && ~~ mask 6" in valid_duplicates'_D[rotated]) - apply (simp add:is_aligned_weaken[where y = 2] is_aligned_neg_mask) - apply (clarsimp simp: vs_ptr_align_def) - apply (simp add:and_not_mask_twice) - apply simp + apply (simp add:is_aligned_weaken[where y = 2] is_aligned_neg_mask) + apply (clarsimp simp: vs_ptr_align_def) + apply (simp add:and_not_mask_twice) apply (drule_tac x = "(ucast ((p && ~~ mask 6) && mask pt_bits >> 2))" in pte_relation_alignedD) apply assumption @@ -1036,8 +1031,7 @@ lemma page_directory_at_state_relation: "\page_directory_at ptr s; pspace_aligned s; (s, sa) \ state_relation;pspace_distinct' sa\ \ page_directory_at' ptr sa" - apply (clarsimp simp:page_directory_at'_def state_relation_def - obj_at_def) + apply (clarsimp simp:page_directory_at'_def state_relation_def obj_at_def) apply (clarsimp simp:pspace_relation_def) apply (drule bspec) apply fastforce @@ -1058,8 +1052,7 @@ lemma page_directory_at_state_relation: apply fastforce apply (thin_tac "dom a = b" for a b) apply (frule(1) pspace_alignedD) - apply (clarsimp simp:ucast_ucast_len - split:if_splits) + apply (clarsimp simp:ucast_ucast_len split:if_splits) apply (drule pde_relation_must_pde) apply (drule(1) pspace_distinctD') apply (clarsimp simp:objBits_simps archObjSize_def) @@ -1162,7 +1155,7 @@ lemma copy_global_mappings_corres: apply (rule corres_guard_imp) apply (rule corres_split [where r'="op =" and P=\ and P'=\]) prefer 2 - apply (clarsimp simp: corres_gets state_relation_def arch_state_relation_def) + apply (clarsimp simp: state_relation_def arch_state_relation_def) apply (rule_tac F = "is_aligned global_pd 6 \ is_aligned pd 6" in corres_gen_asm) apply (rule corres_mapM_x) prefer 5 diff --git a/proof/refine/CNodeInv_R.thy b/proof/refine/CNodeInv_R.thy index c2dc49435..b6805e0bf 100644 --- a/proof/refine/CNodeInv_R.thy +++ b/proof/refine/CNodeInv_R.thy @@ -9027,7 +9027,7 @@ lemma cteMove_valid_pspace' [wp]: apply (simp add: pred_conj_def valid_pspace'_def valid_mdb'_def) apply (wp sch_act_wf_lift valid_queues_lift cur_tcb_lift updateCap_no_0 updateCap_ctes_of_wp getCTE_wp | simp)+ - apply (clarsimp simp: invs'_def valid_state'_def elim!: valid_pspaceE')+ + apply (clarsimp simp: invs'_def valid_state'_def)+ apply (clarsimp dest!: cte_at_cte_wp_atD) apply (rule_tac x = cte in exI) apply clarsimp diff --git a/proof/refine/IpcCancel_R.thy b/proof/refine/IpcCancel_R.thy index 7231abc1c..101add8e3 100644 --- a/proof/refine/IpcCancel_R.thy +++ b/proof/refine/IpcCancel_R.thy @@ -145,9 +145,7 @@ lemma cancelIPC_tcb_at'[wp]: end declare if_weak_cong [cong] - declare delete_remove1 [simp] - declare delete.simps [simp del] lemma invs_weak_sch_act_wf[elim!]: @@ -626,9 +624,7 @@ lemma valid_ep_remove: apply (auto simp add: valid_ep'_def dest: subsetD [OF set_remove1_subset]) done -(* Levity: added (20090201 10:50:13) *) declare cart_singleton_empty [simp] - declare cart_singleton_empty2[simp] crunch ksQ[wp]: setNotification "\s. P (ksReadyQueues s p)" @@ -680,12 +676,15 @@ lemma cancelSignal_invs': apply (rule conjI, erule delta_sym_refs) apply (clarsimp simp: ntfn_bound_refs'_def split: split_if_asm) apply (clarsimp split: split_if_asm) - subgoal by (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def - tcb_bound_refs'_def ntfn_q_refs_of'_def - split: ntfn.splits) - apply (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def + subgoal + by (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def + tcb_bound_refs'_def ntfn_q_refs_of'_def + split: ntfn.splits) + subgoal + by (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def tcb_bound_refs'_def) - apply (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def + subgoal + by (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def tcb_bound_refs'_def ntfn_q_refs_of'_def remove1_empty split: ntfn.splits) apply (rule conjI, clarsimp elim!: if_live_state_refsE) @@ -716,25 +715,14 @@ lemma cancelSignal_invs': lemmas setEndpoint_valid_arch[wp] = valid_arch_state_lift' [OF setEndpoint_typ_at' setEndpoint_ksArchState] -(* Levity: added (20090201 10:50:13) *) declare setEndpoint_ksArch [wp] -lemma setEndpoint_irq_node'[wp]: - "\\s. P (irq_node' s)\ - setEndpoint ep_ptr val - \\_ s. P (irq_node' s)\" - apply (simp add: setEndpoint_def setObject_def split_def) - apply (wp updateObject_default_inv | simp)+ - done - lemma ep_redux_simps3: "ep_q_refs_of' (case xs of [] \ IdleEP | y # ys \ RecvEP (y # ys)) = (set xs \ {EPRecv})" "ep_q_refs_of' (case xs of [] \ IdleEP | y # ys \ SendEP (y # ys)) = (set xs \ {EPSend})" - by (fastforce split: list.splits - simp: valid_ep_def valid_ntfn_def - intro!: ext)+ + by (fastforce split: list.splits simp: valid_ep_def valid_ntfn_def)+ lemma setEndpoint_pde_mappings'[wp]: "\valid_pde_mappings'\ setEndpoint ptr val \\rv. valid_pde_mappings'\" @@ -744,10 +732,7 @@ lemma setEndpoint_pde_mappings'[wp]: apply (clarsimp dest!: updateObject_default_result) done -(* Levity: added (20090126 19:32:18) *) declare setEndpoint_ksMachine [wp] - -(* Levity: added (20090201 10:50:14) *) declare setEndpoint_valid_irq_states' [wp] lemma setEndpoint_vms[wp]: @@ -765,9 +750,9 @@ crunch ksCurDomain[wp]: setEndpoint "\s. P (ksCurDomain s)" lemma setEndpoint_ksDomSchedule[wp]: "\\s. P (ksDomSchedule s)\ setEndpoint ptr ep \\_ s. P (ksDomSchedule s)\" -apply (simp add: setEndpoint_def setObject_def split_def) -apply (wp updateObject_default_inv | simp)+ -done + apply (simp add: setEndpoint_def setObject_def split_def) + apply (wp updateObject_default_inv | simp)+ + done lemma setEndpoint_ct_idle_or_in_cur_domain'[wp]: "\ ct_idle_or_in_cur_domain' \ setEndpoint ptr ep \ \_. ct_idle_or_in_cur_domain' \" @@ -789,9 +774,9 @@ lemma setEndpoint_ct_not_inQ[wp]: lemma setEndpoint_ksDomScheduleIdx[wp]: "\\s. P (ksDomScheduleIdx s)\ setEndpoint ptr ep \\_ s. P (ksDomScheduleIdx s)\" -apply (simp add: setEndpoint_def setObject_def split_def) -apply (wp updateObject_default_inv | simp)+ -done + apply (simp add: setEndpoint_def setObject_def split_def) + apply (wp updateObject_default_inv | simp)+ + done end lemma (in delete_one_conc) cancelIPC_invs[wp]: @@ -866,10 +851,9 @@ proof - cong: list.case_cong) apply (frule_tac x=t in distinct_remove1) apply (frule_tac x=t in set_remove1_eq) - apply (auto elim!: delta_sym_refs - simp: symreftype_inverse' tcb_st_refs_of'_def tcb_bound_refs'_def - split: thread_state.splits split_if_asm) - done + by (auto elim!: delta_sym_refs + simp: symreftype_inverse' tcb_st_refs_of'_def tcb_bound_refs'_def + split: thread_state.splits split_if_asm) have R: "\invs' and tcb_at' t\ do y \ threadSet (\tcb. tcb \ tcbFault := None \) t; @@ -894,12 +878,11 @@ proof - apply (rule hoare_seq_ext [OF _ gts_sp']) apply (case_tac state, simp_all add: isTS_defs) - apply (safe intro!: - hoare_weaken_pre[OF Q] - hoare_weaken_pre[OF R] - hoare_weaken_pre[OF return_wp] - hoare_weaken_pre[OF cancelSignal_invs'] - elim!: invs_valid_objs' pred_tcb'_weakenE) + apply (safe intro!: hoare_weaken_pre[OF Q] + hoare_weaken_pre[OF R] + hoare_weaken_pre[OF return_wp] + hoare_weaken_pre[OF cancelSignal_invs'] + elim!: pred_tcb'_weakenE) apply (auto simp: pred_tcb_at'_def obj_at'_def dest: invs_sch_act_wf') done @@ -936,8 +919,7 @@ lemma (in delete_one_conc_pre) cancelIPC_st_tcb_at: apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def cong: if_cong Structures_H.thread_state.case_cong) apply (rule hoare_seq_ext [OF _ gts_sp']) - apply (case_tac x, simp_all add: isTS_defs list_case_If - isBlockedOnNotification_def) + apply (case_tac x, simp_all add: isTS_defs list_case_If) apply (wp sts_st_tcb_at'_cases delete_one_st_tcb_at threadSet_pred_tcb_no_state cancelSignal_st_tcb_at hoare_drop_imps @@ -1135,7 +1117,7 @@ lemma (in delete_one_conc_pre) cancelIPC_sch_act_not: delete_one_sch_act_not | wpc | simp add: getThreadReplySlot_def o_def if_apply_def2 - split del: if_splits + split del: split_if | rule hoare_drop_imps)+ done @@ -1703,13 +1685,14 @@ lemma sts_invs_minor'_no_valid_queues: apply (drule obj_at_valid_objs') apply (clarsimp simp: valid_pspace'_def) apply (clarsimp simp: valid_obj'_def valid_tcb'_def projectKOs) - apply (fastforce simp: valid_tcb_state'_def - split: Structures_H.thread_state.splits) + subgoal + by (fastforce simp: valid_tcb_state'_def + split: Structures_H.thread_state.splits) apply (clarsimp dest!: st_tcb_at_state_refs_ofD' elim!: rsubst[where P=sym_refs] intro!: ext) apply (fastforce simp: valid_queues_def inQ_def pred_tcb_at' pred_tcb_at'_def - elim!: pred_tcb_at' st_tcb_ex_cap'' obj_at'_weakenE)+ + elim!: st_tcb_ex_cap'' obj_at'_weakenE)+ done crunch ct_idle_or_in_cur_domain'[wp]: tcbSchedDequeue ct_idle_or_in_cur_domain' @@ -1949,13 +1932,8 @@ lemma suspend_makes_inactive: apply (wp threadSet_pred_tcb_no_state setThreadState_st_tcb | simp)+ done -(* Levity: added (20090723 09:16:50) *) declare threadSet_sch_act_sane [wp] - -(* Levity: added (20090721 10:56:34) *) declare sane_update [simp] - -(* Levity: added (20090725 09:07:51) *) declare sts_sch_act_sane [wp] lemma tcbSchedEnqueue_ksQset_weak: @@ -2596,8 +2574,7 @@ lemma cancelAllSignals_unlive: apply (clarsimp simp: pred_tcb_at'_def obj_at'_def projectKOs) apply (simp add: projectKOs projectKO_opt_tcb) apply (fastforce simp: ko_wp_at'_def valid_obj'_def valid_ntfn'_def - obj_at'_def projectKOs - elim: valid_objsE')+ + obj_at'_def projectKOs)+ done crunch ep_at'[wp]: tcbSchedEnqueue "ep_at' epptr" diff --git a/proof/refine/Ipc_R.thy b/proof/refine/Ipc_R.thy index 0b8adf66c..25b35ec5b 100644 --- a/proof/refine/Ipc_R.thy +++ b/proof/refine/Ipc_R.thy @@ -3438,7 +3438,7 @@ lemma sai_invs'[wp]: apply (clarsimp | wp cancelIPC_ct')+ apply (wp set_ntfn_minor_invs' gts_wp' | clarsimp)+ apply (frule pred_tcb_at') - apply (wp set_ntfn_minor_invs' + by (wp set_ntfn_minor_invs' | rule conjI | clarsimp elim!: st_tcb_ex_cap'' | fastforce simp: invs'_def valid_state'_def receiveBlocked_def projectKOs @@ -3448,7 +3448,6 @@ lemma sai_invs'[wp]: | fastforce simp: receiveBlocked_def projectKOs pred_tcb_at'_def obj_at'_def dest!: invs_rct_ct_activatable' split: thread_state.splits)+ - done lemma ncof_invs' [wp]: "\invs'\ nullCapOnFailure (lookupCap t ref) \\rv. invs'\" diff --git a/proof/refine/PageTableDuplicates.thy b/proof/refine/PageTableDuplicates.thy index e7dacd24d..b27bee0f5 100644 --- a/proof/refine/PageTableDuplicates.thy +++ b/proof/refine/PageTableDuplicates.thy @@ -918,15 +918,14 @@ lemma copyGlobalMappings_ksPSpace_concrete: apply simp+ apply (clarsimp split:if_splits) apply (frule_tac x = "(armKSGlobalPD (ksArchState s') + (x && mask pdBits))" - in copyGlobalMappings_ksPSpaceD) + in copyGlobalMappings_ksPSpaceD) apply simp+ apply (drule use_valid[OF _ pd]) apply simp - apply (clarsimp split:if_splits - simp:mask_add_aligned field_simps) + apply (clarsimp split: if_splits simp: field_simps) + apply (clarsimp simp: mask_add_aligned) apply (frule comp) - apply (clarsimp simp:pdBits_def pageBits_def - mask_twice blah) + apply (clarsimp simp:pdBits_def pageBits_def mask_twice blah) apply (drule_tac y = "armKSGlobalPD a + b" for a b in neg_mask_mono_le[where n = 14]) apply (drule_tac x = "armKSGlobalPD a + b" for a b in neg_mask_mono_le[where n = 14]) apply (frule_tac d1 = "x && mask 14" in is_aligned_add_helper[THEN conjunct2]) diff --git a/proof/refine/Refine.thy b/proof/refine/Refine.thy index 20509f9bd..4aa2b7112 100644 --- a/proof/refine/Refine.thy +++ b/proof/refine/Refine.thy @@ -661,11 +661,12 @@ lemma ckernel_invariant: apply (clarsimp simp: ADT_A_def ADT_H_def global_automaton_def) apply (erule_tac P="a \ (\x. b x)" for a b in disjE) - apply ((clarsimp simp: kernel_call_H_def + subgoal + by ((clarsimp simp: kernel_call_H_def | drule use_valid[OF _ valid_corres_combined [OF kernel_entry_invs entry_corres], OF _ kernelEntry_invs'[THEN hoare_weaken_pre]] - | fastforce simp: ex_abs_def sch_act_simple_def ct_running_related sched_act_rct_related)+)[1] + | fastforce simp: ex_abs_def sch_act_simple_def ct_running_related sched_act_rct_related)+) apply (erule_tac P="a \ b" for a b in disjE) apply (clarsimp simp add: do_user_op_H_def monad_to_transition_def) apply (drule use_valid) diff --git a/proof/refine/Retype_R.thy b/proof/refine/Retype_R.thy index 1d7e5db51..2d98577e0 100644 --- a/proof/refine/Retype_R.thy +++ b/proof/refine/Retype_R.thy @@ -177,10 +177,9 @@ lemmas valid_obj_makeObject_rules = lemma makeObjectKO_valid: "makeObjectKO tp = Some v \ valid_obj' v s" - by (clarsimp simp: makeObjectKO_def valid_obj_makeObject_rules - split: sum.splits object_type.splits - apiobject_type.splits kernel_object.splits - arch_kernel_object.splits) + by (clarsimp simp: makeObjectKO_def + split: sum.splits object_type.splits apiobject_type.splits + kernel_object.splits arch_kernel_object.splits) lemma loadObject_cte_same: fixes x :: cte @@ -395,7 +394,7 @@ lemma cte_at_next_slot'': apply(subgoal_tac "next_not_child_dom (p, cdt_list s, cdt s)") prefer 2 apply(simp add: next_not_child_termination valid_mdb_def valid_list_def) - apply(simp add: next_not_child.psimps split: split_if_asm) + apply(simp split: split_if_asm) apply(case_tac "cdt s p") apply(simp) apply(rule descendants_of_cte_at') @@ -722,21 +721,15 @@ lemma null_filter_ctes_retype: done lemma new_cap_addrs_fold: - "\ 0 < n\ \ - map (\p. (ptr + (of_nat p << objBitsKO ko))) - [0.e. n - 1 ] = new_cap_addrs n ptr ko" - apply (simp add: new_cap_addrs_def power_sub[symmetric] - upto_enum_def o_def - unat_power_lower unat_sub word_le_nat_alt - del: upt_Suc) -done + "0 < n \ map (\p. (ptr + (of_nat p << objBitsKO ko))) [0.e. n - 1 ] = new_cap_addrs n ptr ko" + by (simp add: new_cap_addrs_def) lemma new_cap_addrs_aligned: "\ is_aligned ptr (objBitsKO ko) \ \ \x \ set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko)" apply (clarsimp simp: new_cap_addrs_def) apply (erule aligned_add_aligned[OF _ is_aligned_shift]) - apply simp + apply simp done lemma new_cap_addrs_distinct: @@ -878,7 +871,7 @@ lemma new_cap_addrs_subset: apply (rule iffD2[OF word_less_nat_alt]) apply (rule le_less_trans[OF unat_plus_gt]) using range_cover - apply (clarsimp simp:unat_power_lower range_cover_def) + apply (clarsimp simp: range_cover_def) apply (insert range_cover) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask,OF le_refl ]) apply (simp add:range_cover_def)+ @@ -1295,7 +1288,7 @@ proof - done have okov: "objBitsKO ko < word_bits" - by (simp add: objBitsKO_bounded2 objBits_def) + by (simp add: objBits_def) have new_range_disjoint: "\x. x \ set (new_cap_addrs n ptr ko) \ @@ -1439,7 +1432,7 @@ lemma retype_state_relation: note pad' = retype_aligned_distinct' [OF vs' pn' cover'] thus pa': "pspace_aligned' (s'\ksPSpace := ?ps'\)" and pd': "pspace_distinct' (s'\ksPSpace := ?ps'\)" - by (simp_all del: data_map_insert_def) + by simp_all note pa'' = pa'[simplified foldr_upd_app_if[folded data_map_insert_def]] note pd'' = pd'[simplified foldr_upd_app_if[folded data_map_insert_def]] @@ -1513,10 +1506,10 @@ lemma retype_state_relation: from pn2 have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)" by - (rule ext, induct (?al), - simp_all add: cns_of_heap_def default_object_def data_map_insert_def TCBObject) + simp_all add: cns_of_heap_def default_object_def TCBObject) note data_map_insert_def[simp del] from gr show ?thesis - by (simp add: ghost_relation_of_heap fun_upd_apply, simp add: TCBObject update_gs_def fun_upd_apply) + by (simp add: ghost_relation_of_heap, simp add: TCBObject update_gs_def) next case EndpointObject from pn2 @@ -1527,7 +1520,6 @@ lemma retype_state_relation: have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)" by - (rule ext, induct (?al), simp_all add: cns_of_heap_def default_object_def data_map_insert_def EndpointObject) - note data_map_insert_def[simp del] from gr show ?thesis by (simp add: ghost_relation_of_heap, simp add: EndpointObject update_gs_def) @@ -1556,8 +1548,7 @@ lemma retype_state_relation: have [simp]: "cns_of_heap ?ps = (\x. if x \ set ?al then Some us else cns_of_heap (kheap s) x)" by (rule ext, induct (?al), - simp_all add: cns_of_heap_def wf_empty wf_empty_bits wf_unique - default_object_def CapTableObject) + simp_all add: cns_of_heap_def wf_empty_bits wf_unique default_object_def CapTableObject) note data_map_insert_def[simp del] from gr show ?thesis by (simp add: ghost_relation_of_heap, @@ -1568,7 +1559,6 @@ lemma retype_state_relation: have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)" by - (rule ext, induct (?al), simp_all add: cns_of_heap_def data_map_insert_def default_object_def ArchObject) - note data_map_insert_def[simp del] from pn2 gr show ?thesis apply (clarsimp simp add: ghost_relation_of_heap) apply (rule conjI[rotated]) @@ -1980,8 +1970,8 @@ proof - apply (rule arg_cong2[where f=upt, OF refl]) apply (metis mult.commute shiftl_t2n unat_of_nat_shift) using shiftr_not_zero - apply (simp add: shiftl_t2n word_less_1 word_not_le) - apply (metis word_less_1 word_neq_0_conv word_not_le) + apply (simp add: shiftl_t2n) + apply (metis word_less_1 word_not_le) done from aligned @@ -2008,7 +1998,7 @@ proof - obj_bits_api[symmetric] shiftl_t2n upto_enum_red' range_cover.unat_of_nat_n[OF cover]) apply (rule corres_split_nor[OF corres_trivial]) - apply (clarsimp simp: corres_return retype_addrs_fold[symmetric] + apply (clarsimp simp: retype_addrs_fold[symmetric] ptr_add_def upto_enum_red' not_zero' range_cover.unat_of_nat_n[OF cover] word_le_sub1) apply (rename_tac x eps ps) @@ -2410,7 +2400,7 @@ proof - apply (wp createWordObjects_nonzero[OF not_0 ,simplified]) apply (simp add:word_bits_def pageBits_def)+ apply (wp cwo_ret[where v = pageBits, OF _ not_0 ,simplified]) - apply (simp add:pageBits_def ptr word_bits_def ptr)+ + apply (simp add:pageBits_def ptr word_bits_def)+ -- "LargePageObject" apply wp apply (simp add: valid_cap'_def capAligned_def n_less_word_bits @@ -2485,20 +2475,19 @@ proof - proof(cases a) case Untyped with Some cover ct show ?thesis apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) - apply (simp_all add: set_map ARM_H.toAPIType_def - fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def + apply (simp_all add: ARM_H.toAPIType_def fromIntegral_def + toInteger_nat fromInteger_nat APIType_capBits_def split: ARM_H.object_type.splits) apply wp apply (intro ballI) - apply (clarsimp simp: set_map image_def upto_enum_red' valid_cap'_def capAligned_def + apply (clarsimp simp: image_def upto_enum_red' valid_cap'_def capAligned_def split: capability.splits) apply (drule minus_one_helper5[rotated]) apply (rule range_cover_not_zero[OF not_0 cover]) apply (intro conjI) apply (rule is_aligned_add_multI[OF _ le_refl refl]) apply (fastforce simp:range_cover_def word_bits_def)+ - apply (clarsimp simp:valid_untyped'_def ko_wp_at'_def obj_range'_def - del:atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff) + apply (clarsimp simp:valid_untyped'_def ko_wp_at'_def obj_range'_def) apply (drule(1) pspace_no_overlapD'[rotated]) apply (frule(1) range_cover_cell_subset) apply (erule disjE) @@ -2514,7 +2503,7 @@ proof - next case TCBObject with Some cover ct show ?thesis apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) - apply (simp_all add: set_map ARM_H.toAPIType_def + apply (simp_all add: ARM_H.toAPIType_def fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def curDomain_def split: ARM_H.object_type.splits) apply (wp mapM_x_wp' hoare_vcg_const_Ball_lift)+ @@ -2531,7 +2520,7 @@ proof - next case EndpointObject with Some cover ct show ?thesis apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) - apply (simp_all add: set_map ARM_H.toAPIType_def + apply (simp_all add: ARM_H.toAPIType_def fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def split: ARM_H.object_type.splits) apply wp @@ -2548,7 +2537,7 @@ proof - next case NotificationObject with Some cover ct show ?thesis apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) - apply (simp_all add: set_map ARM_H.toAPIType_def + apply (simp_all add: ARM_H.toAPIType_def fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def split: ARM_H.object_type.splits) apply wp @@ -2565,7 +2554,7 @@ proof - next case CapTableObject with Some cover ct show ?thesis apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) - apply (simp_all add: set_map ARM_H.toAPIType_def + apply (simp_all add: ARM_H.toAPIType_def fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def split: ARM_H.object_type.splits) apply wp @@ -2640,13 +2629,11 @@ lemma other_objs_default_relation: lemma captable_relation_retype: "n < word_bits \ obj_relation_retype (default_object Structures_A.CapTableObject n) (KOCTE makeObject)" - apply (clarsimp simp: obj_relation_retype_def default_object_def - wf_empty_bits objBits_simps obj_bits.simps - dom_empty_cnode ex_with_length cte_level_bits_def) + apply (clarsimp simp: obj_relation_retype_def default_object_def wf_empty_bits + objBits_simps dom_empty_cnode ex_with_length cte_level_bits_def) apply (rule conjI) defer - apply (clarsimp simp: cte_relation_def empty_cnode_def - makeObject_cte) + apply (clarsimp simp: cte_relation_def empty_cnode_def makeObject_cte) apply (rule set_eqI, rule iffI) apply (clarsimp simp: cte_map_def) apply (rule_tac x="of_bl y" in exI) @@ -3346,8 +3333,7 @@ lemma valid_untyped'_helper: apply (clarsimp simp:valid_cap'_def retype_ko_wp_at') apply (case_tac "cteCap cte"; simp add: valid_cap'_def cte_wp_at_obj_cases' valid_pspace'_def retype_obj_at_disj' - split: zombie_type.split_asm - del: Int_atLeastAtMost) + split: zombie_type.split_asm) apply (rename_tac arch_capability) apply (case_tac arch_capability; simp add: retype_obj_at_disj' typ_at_to_obj_at_arches @@ -3513,7 +3499,7 @@ proof (intro conjI impI) apply (intro conjI ballI) apply (clarsimp elim!: ranE) apply (rule valid_cap[unfolded foldr_upd_app_if[folded data_map_insert_def]]) - apply (fastforce intro: ranI) + apply (fastforce) apply (rule_tac ptr="x + xa" in cte_wp_at_tcbI', assumption+) apply fastforce apply simp @@ -3665,7 +3651,7 @@ proof - apply (simp add:range_cover_def) apply (fold word_bits_def) using unat_of_nat_shift not_0 - apply (simp add:field_simps shiftl_t2n unat_power_lower32) + apply (simp add:field_simps shiftl_t2n) done have not_0': "(2::word32) ^ (objBitsKO val + gbits) * of_nat n \ 0" apply (rule range_cover_not_zero_shift[OF not_0,unfolded shiftl_t2n,OF _ le_refl]) @@ -3701,7 +3687,7 @@ proof - apply (simp add:range_cover_def word_bits_def) apply (rule less_le_trans[OF mult_less_mono1]) apply (rule unat_mono) - apply (rule_tac Y1= "pa" in of_nat_mono_maybe'[THEN iffD1,rotated -1]) + apply (rule_tac y1= "pa" in of_nat_mono_maybe'[THEN iffD1,rotated -1]) apply (assumption) apply (simp add:word_bits_def) apply (simp add:word_bits_def) @@ -3784,10 +3770,7 @@ lemma createObjects_orig_obj_at2': \ pspace_no_overlap' ptr sz s\ createObjects' ptr n val gbits \\r s. P (obj_at' P' p s)\" unfolding obj_at'_real_def - apply (wp createObjects_orig_ko_wp_at2') - apply (auto intro: conjI) - done - + by (wp createObjects_orig_ko_wp_at2') auto lemma createObjects_orig_cte_wp_at2': "\\s. P (cte_wp_at' P' p s) @@ -3832,7 +3815,7 @@ lemma threadSet_cte_wp_at2'T: apply (subst conj_commute) apply (rule setObject_cte_wp_at2') apply (clarsimp simp: updateObject_default_def projectKOs in_monad objBits_simps - obj_at'_def objBits_simps in_magnitude_check prod_eq_iff) + obj_at'_def in_magnitude_check prod_eq_iff) apply (case_tac tcba, clarsimp simp: bspec_split [OF spec [OF x]]) apply (clarsimp simp: updateObject_default_def in_monad bind_def projectKOs) @@ -5110,7 +5093,7 @@ lemma createNewCaps_vms: createNewCaps ty ptr n us \\archCaps. valid_machine_state'\" apply (clarsimp simp: Arch_createNewCaps_def valid_machine_state'_def - Arch_createNewCaps_def createNewCaps_def pointerInUserData_def + createNewCaps_def pointerInUserData_def typ_at'_def createObjects_def doMachineOp_return_foo) apply (rule hoare_pre) apply (wpc @@ -5769,7 +5752,7 @@ proof - apply clarsimp apply (intro conjI; simp add:valid_pspace'_def objBits_def) apply (fastforce simp add: no_cte no_tcb split_def split: option.splits) - apply (clarsimp simp:invs'_def no_cte no_tcb valid_state'_def no_cte split:option.splits) + apply (clarsimp simp:invs'_def no_tcb valid_state'_def no_cte split:option.splits) done qed @@ -5804,8 +5787,7 @@ lemma corres_retype_update_gsI: _ \ modify (f (set addrs)); return addrs od)" - using corres_retype' - [OF not_zero aligned obj_bits_api check usv ko orr cover] + using corres_retype' [OF not_zero aligned obj_bits_api check usv ko orr cover] by (simp add: f) (*FIXME: Move to Deterministic_AI*) @@ -5815,27 +5797,28 @@ lemma gcd_corres: "corres op = \ \ (gets cur_domain) curDomain" by (simp add: curDomain_def state_relation_def) (* FIXME move *) -lemmas corres_underlying_gets_pre_rhs = corres_symb_exec_r[OF _ _ gets_inv no_fail_pre[OF non_fail_gets TrueI]] +lemmas corres_underlying_gets_pre_rhs = + corres_symb_exec_r[OF _ _ gets_inv no_fail_pre[OF non_fail_gets TrueI]] (* FIXME move *) lemma modify_fold_mapM_x: shows "modify (fold f xs) = mapM_x (\x. modify (f x)) xs" -apply (induct xs) - apply (simp add: mapM_x_Nil id_def return_modify) -apply (simp add: mapM_x_Cons) -apply (drule sym) -apply (simp add: modify_modify o_def) -done + apply (induct xs) + apply (simp add: mapM_x_Nil id_def return_modify) + apply (simp add: mapM_x_Cons) + apply (drule sym) + apply (simp add: modify_modify o_def) + done lemma modify_ekheap_update_ethread_set_futz: - "is_etcb_at t s - \ modify (ekheap_update (\ekh. ekh(t := Some c))) s - = ethread_set (K c) t s" -by (clarsimp simp: ethread_set_def modify_def bind_def return_def gets_the_def put_def set_eobject_def gets_def get_etcb_def get_def assert_opt_def is_etcb_at_def split: option.splits) + "is_etcb_at t s \ modify (ekheap_update (\ekh. ekh(t := Some c))) s = ethread_set (K c) t s" + by (clarsimp simp: ethread_set_def modify_def bind_def return_def gets_the_def put_def + set_eobject_def gets_def get_etcb_def get_def assert_opt_def is_etcb_at_def + split: option.splits) lemma stupid_ekheap_update_ekheap: "ekheap_update (\_. P (ekheap s)) s = ekheap_update (\ekh. P ekh) s" -by simp + by simp lemma retype_region2_extra_ext_mapM_x_corres: shows "corres dc @@ -5846,23 +5829,24 @@ lemma retype_region2_extra_ext_mapM_x_corres: threadSet (tcbDomain_update (\_. cdom)) addr od) addrs)" -apply (rule corres_guard_imp) - apply (simp add: retype_region2_extra_ext_def curDomain_mapM_x_futz[symmetric] when_def) - apply (rule corres_split_eqr[OF _ gcd_corres]) - apply (rule_tac S="Id \ {(x, y). x \ set addrs}" - and P="\s. (\t \ set addrs. tcb_at t s) \ valid_etcbs s" - and P'="\s. \t \ set addrs. tcb_at' t s" - in corres_mapM_x) + apply (rule corres_guard_imp) + apply (simp add: retype_region2_extra_ext_def curDomain_mapM_x_futz[symmetric] when_def) + apply (rule corres_split_eqr[OF _ gcd_corres]) + apply (rule_tac S="Id \ {(x, y). x \ set addrs}" + and P="\s. (\t \ set addrs. tcb_at t s) \ valid_etcbs s" + and P'="\s. \t \ set addrs. tcb_at' t s" + in corres_mapM_x) apply simp apply (rule corres_guard_imp) apply (rule ethread_set_corres, simp_all add: etcb_relation_def non_exst_same_def)[1] apply (case_tac tcb') apply simp - apply auto[2] + apply fastforce + apply fastforce apply (wp hoare_vcg_ball_lift | simp)+ apply auto[1] apply (wp | simp add: curDomain_def)+ -done + done lemma retype_region2_extra_ext_trivial: "ty \ APIType_map2 (Inr (APIObjectType apiobject_type.TCBObject)) @@ -5941,15 +5925,14 @@ lemma corres_retype_region_createNewCaps: apply simp apply (clarsimp simp:range_cover_def) apply (arith+)[4] - -- "TCB, EP, NTFN" - (* suspect indentation here *) + -- "TCB, EP, NTFN" apply (simp_all add: retype_region2_ext_retype_region bind_cong[OF curDomain_mapM_x_futz refl, unfolded bind_assoc])[9] (* not PageDirectoryObject *) apply (rule corres_guard_imp) apply (rule corres_split_eqr) apply (rule corres_split_nor) apply (rule corres_trivial, simp) apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2 - objBits_simps APIType_map2_def) + objBits_simps APIType_map2_def) apply (simp add: APIType_map2_def) apply (rule retype_region2_extra_ext_mapM_x_corres) apply wp[2] diff --git a/proof/refine/Schedule_R.thy b/proof/refine/Schedule_R.thy index 7b62303e4..d11e7d10f 100644 --- a/proof/refine/Schedule_R.thy +++ b/proof/refine/Schedule_R.thy @@ -2271,7 +2271,7 @@ lemma enumPrio_word_div: apply (simp add: maxPriority_def numPriorities_def) apply (clarsimp simp: unat_of_nat_eq) apply (erule conjE) - apply (drule_tac Y="unat v" and X="x" in of_nat_mono_maybe[rotated, where 'a="8"]) + apply (drule_tac y="unat v" and x="x" in of_nat_mono_maybe[rotated, where 'a="8"]) apply (simp add: maxPriority_def numPriorities_def)+ done diff --git a/spec/ROOT b/spec/ROOT index 27c4ef371..46d4a0388 100644 --- a/spec/ROOT +++ b/spec/ROOT @@ -33,18 +33,19 @@ chapter "Specifications" session ASpec in "abstract" = Word + options [document=pdf] theories [document = false] - "../../lib/NICTACompat" "../../lib/Lib" - "../../lib/DistinctProp" + "../../lib/Defs" "../../lib/List_Lib" + "../../lib/WordSetup" theories "Intro_Doc" - "../../lib/wp/NonDetMonad" + "../../lib/Monad_WP/NonDetMonad" theories [document = false] - "../../lib/wp/NonDetMonadLemmas" + "../../lib/Monad_WP/NonDetMonadLemmas" theories "Syscall_A" "Glossary_Doc" + (* "KernelInit_A" *) document_files "VERSION" "root.tex" diff --git a/spec/abstract/ARM/ArchDecode_A.thy b/spec/abstract/ARM/ArchDecode_A.thy index 25834d731..9971ed315 100644 --- a/spec/abstract/ARM/ArchDecode_A.thy +++ b/spec/abstract/ARM/ArchDecode_A.thy @@ -18,7 +18,6 @@ theory ArchDecode_A imports "../Interrupt_A" "../InvocationLabels_A" - "../../../lib/WordLib" begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/Machine_A.thy b/spec/abstract/ARM/Machine_A.thy index 2e80a71ab..70e0ba152 100644 --- a/spec/abstract/ARM/Machine_A.thy +++ b/spec/abstract/ARM/Machine_A.thy @@ -17,9 +17,7 @@ chapter "ARM Machine Instantiation" theory Machine_A imports - "../../../lib/WordSetup" - "../../../lib/wp/NonDetMonad" - "../../machine/MachineExports" + "../../machine/$L4V_ARCH/MachineTypes" begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/CSpace_A.thy b/spec/abstract/CSpace_A.thy index f9274cef5..eaf834cfa 100644 --- a/spec/abstract/CSpace_A.thy +++ b/spec/abstract/CSpace_A.thy @@ -19,7 +19,7 @@ imports "./$L4V_ARCH/ArchVSpace_A" IpcCancel_A "./$L4V_ARCH/ArchCSpace_A" - "../../lib/wp/NonDetMonadLemmas" + "../../lib/Monad_WP/NonDetMonadLemmas" "~~/src/HOL/Library/Prefix_Order" begin diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index 2c0521d58..110e098ab 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -18,7 +18,6 @@ theory Decode_A imports Interrupt_A "./$L4V_ARCH/ArchDecode_A" - "../../lib/WordLib" "../design/InvocationLabels_H" begin diff --git a/spec/abstract/KernelInit_A.thy b/spec/abstract/KernelInit_A.thy index b57be6f5a..4563bb95f 100644 --- a/spec/abstract/KernelInit_A.thy +++ b/spec/abstract/KernelInit_A.thy @@ -8,14 +8,10 @@ * @TAG(GD_GPL) *) -theory KernelInit_A +theory KernelInit_A (* FIXME: unused, out of date *) imports - "../../lib/WordEnum" - "../../lib/Lib" - Structures_A - Exceptions_A Tcb_A - ArchVSpace_A + "./$L4V_ARCH/ArchVSpace_A" begin section {* Generic stuff *} diff --git a/spec/abstract/README.md b/spec/abstract/README.md index 6da3b2f8b..1966f4397 100644 --- a/spec/abstract/README.md +++ b/spec/abstract/README.md @@ -7,8 +7,8 @@ This directory contains the main Isabelle sources of the seL4 abstract specification. The specification draws in additional interface files from `design` and `machine`. -The specification is written in monadic style. See `l4v/lib/wp/NonDetMonad` -for the definition of this monad. +The specification is written in monadic style. See +`l4v/lib/Monad_WP/NonDetMonad` for the definition of this monad. Top-Level Theory ---------------- diff --git a/spec/capDL/CSpace_D.thy b/spec/capDL/CSpace_D.thy index 142002f7f..513fd23ea 100644 --- a/spec/capDL/CSpace_D.thy +++ b/spec/capDL/CSpace_D.thy @@ -15,8 +15,6 @@ theory CSpace_D imports PageTableUnmap_D - "../../lib/WordEnum" - "../../lib/wp/NonDetMonadVCG" begin (* Does the given cap have any children? *) diff --git a/spec/capDL/Intents_D.thy b/spec/capDL/Intents_D.thy index e0090b5ac..8a3960e3a 100644 --- a/spec/capDL/Intents_D.thy +++ b/spec/capDL/Intents_D.thy @@ -28,7 +28,7 @@ theory Intents_D imports - "../../lib/NICTACompat" + "../../lib/WordSetup" "../abstract/CapRights_A" begin diff --git a/spec/capDL/Monads_D.thy b/spec/capDL/Monads_D.thy index 2e0d885d0..94f98b810 100644 --- a/spec/capDL/Monads_D.thy +++ b/spec/capDL/Monads_D.thy @@ -15,7 +15,7 @@ theory Monads_D imports Types_D - "../../lib/wp/NonDetMonad" + "../../lib/Monad_WP/NonDetMonadVCG" begin (* Kernel state monad *) diff --git a/spec/capDL/PageTableUnmap_D.thy b/spec/capDL/PageTableUnmap_D.thy index 8882a37b1..063643460 100644 --- a/spec/capDL/PageTableUnmap_D.thy +++ b/spec/capDL/PageTableUnmap_D.thy @@ -17,7 +17,6 @@ theory PageTableUnmap_D imports Invocations_D KHeap_D - "../../lib/wp/NonDetMonadLemmas" begin -- "Return all slots in the system containing a cap with the given property." diff --git a/spec/design/ARM/ArchInvocationLabels_H.thy b/spec/design/ARM/ArchInvocationLabels_H.thy index 35ec4db49..8678c1067 100644 --- a/spec/design/ARM/ArchInvocationLabels_H.thy +++ b/spec/design/ARM/ArchInvocationLabels_H.thy @@ -11,7 +11,9 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H -imports "../../../lib/Enumeration" "../../machine/ARM/Setup_Locale" +imports + "../../../lib/Word_Lib/Enumeration" + "../../machine/ARM/Setup_Locale" begin context Arch begin global_naming ARM_H diff --git a/spec/design/PSpaceStorable_H.thy b/spec/design/PSpaceStorable_H.thy index cf37f100d..4f6ad0855 100644 --- a/spec/design/PSpaceStorable_H.thy +++ b/spec/design/PSpaceStorable_H.thy @@ -11,7 +11,6 @@ theory PSpaceStorable_H imports Structures_H - "../../lib/wp/NonDetMonad" KernelStateData_H "../../lib/DataMap" begin diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy index 05bdc73ea..5be6d4104 100644 --- a/spec/design/m-skel/ARM/MachineTypes.thy +++ b/spec/design/m-skel/ARM/MachineTypes.thy @@ -12,15 +12,13 @@ chapter "ARM Machine Types" theory MachineTypes imports - "../../../lib/Enumeration" - "../../../lib/WordSetup" - "../../../lib/wp/NonDetMonad" + "../../../lib/Monad_WP/NonDetMonad" Setup_Locale Platform begin context Arch begin global_naming ARM -(* !!! Generated File !!! Skeleton in ../haskell-translator/ARMMachineTypes.thy *) +(* !!! Generated File !!! Skeleton in ../../design/skel-m/ARMMachineTypes.thy *) text {* An implementation of the machine's types, defining register set diff --git a/spec/design/skel/ARM/ArchInvocationLabels_H.thy b/spec/design/skel/ARM/ArchInvocationLabels_H.thy index ff779cd59..b57ed5a43 100644 --- a/spec/design/skel/ARM/ArchInvocationLabels_H.thy +++ b/spec/design/skel/ARM/ArchInvocationLabels_H.thy @@ -11,7 +11,9 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H -imports "../../../lib/Enumeration" "../../machine/ARM/Setup_Locale" +imports + "../../../lib/Word_Lib/Enumeration" + "../../machine/ARM/Setup_Locale" begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/PSpaceStorable_H.thy b/spec/design/skel/PSpaceStorable_H.thy index cf37f100d..4f6ad0855 100644 --- a/spec/design/skel/PSpaceStorable_H.thy +++ b/spec/design/skel/PSpaceStorable_H.thy @@ -11,7 +11,6 @@ theory PSpaceStorable_H imports Structures_H - "../../lib/wp/NonDetMonad" KernelStateData_H "../../lib/DataMap" begin diff --git a/spec/design/version b/spec/design/version index 9f4a2c941..9f2ba2db2 100644 --- a/spec/design/version +++ b/spec/design/version @@ -1,4 +1,4 @@ -Built from git repo at /home/matthewb/verification/arch_split/seL4/haskell by matthewb +Built from git repo at /Users/kleing/verification/seL4/haskell by kleing Generated from changeset: 2f34d63 manual: Corrected introduction of cnode radix diff --git a/spec/machine/ARM/MachineOps.thy b/spec/machine/ARM/MachineOps.thy index 77778e83a..4541ae1f2 100644 --- a/spec/machine/ARM/MachineOps.thy +++ b/spec/machine/ARM/MachineOps.thy @@ -12,8 +12,6 @@ chapter "Machine Operations" theory MachineOps imports - "../../../lib/WordSetup" - "../../../lib/wp/NonDetMonad" "../MachineMonad" begin diff --git a/spec/machine/ARM/MachineTypes.thy b/spec/machine/ARM/MachineTypes.thy index 5b7ad3cb3..ebbb97806 100644 --- a/spec/machine/ARM/MachineTypes.thy +++ b/spec/machine/ARM/MachineTypes.thy @@ -12,15 +12,13 @@ chapter "ARM Machine Types" theory MachineTypes imports - "../../../lib/Enumeration" - "../../../lib/WordSetup" - "../../../lib/wp/NonDetMonad" + "../../../lib/Monad_WP/NonDetMonad" Setup_Locale Platform begin context Arch begin global_naming ARM -(* !!! Generated File !!! Skeleton in ../haskell-translator/ARMMachineTypes.thy *) +(* !!! Generated File !!! Skeleton in ../../design/skel-m/ARMMachineTypes.thy *) text {* An implementation of the machine's types, defining register set diff --git a/spec/machine/ARM/Platform.thy b/spec/machine/ARM/Platform.thy index de6eed1a6..9e6d83365 100644 --- a/spec/machine/ARM/Platform.thy +++ b/spec/machine/ARM/Platform.thy @@ -14,7 +14,7 @@ theory Platform imports "../../../lib/Defs" "../../../lib/Lib" - "../../../lib/WordEnum" + "../../../lib/WordSetup" Setup_Locale begin diff --git a/spec/take-grant/Confine_S.thy b/spec/take-grant/Confine_S.thy index a884935e0..66cb9683f 100644 --- a/spec/take-grant/Confine_S.thy +++ b/spec/take-grant/Confine_S.thy @@ -32,7 +32,7 @@ lemma extra_rights_idem [simp]: lemma extra_rights_image_idem [simp]: "(extra_rights ` (extra_rights ` S)) = (extra_rights ` S)" - by (rule set_eqI, simp add: image_iff) + by (rule set_eqI) (simp add: image_iff) lemma extra_rights_empty_rights_ident [simp]: "extra_rights \ target = e, rights = {} \ = \ target = e, rights = {} \" diff --git a/spec/take-grant/System_S.thy b/spec/take-grant/System_S.thy index d954e3e12..dce201599 100644 --- a/spec/take-grant/System_S.thy +++ b/spec/take-grant/System_S.thy @@ -20,7 +20,7 @@ *) theory System_S -imports "../../lib/NICTACompat" +imports "../../lib/WordSetup" begin (* System entities: Definition of entities that constitute the system diff --git a/tools/c-parser/CTranslation.thy b/tools/c-parser/CTranslation.thy index cdabf0a35..07feb7994 100644 --- a/tools/c-parser/CTranslation.thy +++ b/tools/c-parser/CTranslation.thy @@ -123,22 +123,21 @@ declare typ_info_word [simp del] declare typ_info_ptr [simp del] lemma valid_call_Spec_eq_subset: -"\' procname = Some (Spec R) -\ HoarePartialDef.valid \' NF P (Call procname) Q A -= (P \ fst ` R \ (R \ (- P) \ UNIV \ UNIV \ Q))" -apply (safe, simp_all) -apply (clarsimp simp: HoarePartialDef.valid_def) -apply (rule ccontr) -apply (drule_tac x="Normal x" in spec, elim allE, -drule mp, erule exec.Call, rule exec.SpecStuck) -apply (auto simp: image_def)[2] -apply (clarsimp simp: HoarePartialDef.valid_def) -apply (elim allE, drule mp, erule exec.Call, erule exec.Spec) -apply auto[1] -apply (clarsimp simp: HoarePartialDef.valid_def) -apply (erule exec_Normal_elim_cases, simp_all) -apply (erule exec_Normal_elim_cases, auto) -done + "\' procname = Some (Spec R) \ + HoarePartialDef.valid \' NF P (Call procname) Q A = (P \ fst ` R \ (R \ (- P) \ UNIV \ UNIV \ Q))" + apply (safe, simp_all) + apply (clarsimp simp: HoarePartialDef.valid_def) + apply (rule ccontr) + apply (drule_tac x="Normal x" in spec, elim allE, + drule mp, erule exec.Call, rule exec.SpecStuck) + apply (auto simp: image_def)[2] + apply (clarsimp simp: HoarePartialDef.valid_def) + apply (elim allE, drule mp, erule exec.Call, erule exec.Spec) + apply auto[1] + apply (clarsimp simp: HoarePartialDef.valid_def) + apply (erule exec_Normal_elim_cases, simp_all) + apply (erule exec_Normal_elim_cases, auto) + done lemma creturn_wp [vcg_hoare]: assumes "P \ {s. (exnupd (\_. Return)) (rvupd (\_. v s) s) \ A}" diff --git a/tools/c-parser/termstypes.ML b/tools/c-parser/termstypes.ML index 1d9867412..962bd2984 100644 --- a/tools/c-parser/termstypes.ML +++ b/tools/c-parser/termstypes.ML @@ -20,7 +20,7 @@ val word16 = word_ty @{typ "16"} val word32 = word_ty @{typ "32"} val word64 = word_ty @{typ "64"} -fun sword_ty arg = Type(@{type_name "Word.word"}, [Type (@{type_name "SignedWords.signed"}, [arg])]) +fun sword_ty arg = Type(@{type_name "Word.word"}, [Type (@{type_name "Signed_Words.signed"}, [arg])]) val sword8 = sword_ty @{typ "8"} val sword16 = sword_ty @{typ "16"} val sword32 = sword_ty @{typ "32"} diff --git a/tools/c-parser/umm_heap/CTypesBase.thy b/tools/c-parser/umm_heap/CTypesBase.thy index c30161bb9..08671b714 100644 --- a/tools/c-parser/umm_heap/CTypesBase.thy +++ b/tools/c-parser/umm_heap/CTypesBase.thy @@ -19,7 +19,7 @@ theory CTypesBase imports "./$L4V_ARCH/Addr_Type" "~~/src/HOL/Library/Prefix_Order" - "../../../lib/Word_Lib/SignedWords" + "../../../lib/Word_Lib/Signed_Words" begin section "Type setup" diff --git a/tools/c-parser/umm_heap/CTypesDefs.thy b/tools/c-parser/umm_heap/CTypesDefs.thy index 1c0e013d6..57009f409 100644 --- a/tools/c-parser/umm_heap/CTypesDefs.thy +++ b/tools/c-parser/umm_heap/CTypesDefs.thy @@ -14,8 +14,6 @@ theory CTypesDefs imports - "~~/src/HOL/Library/Prefix_Order" - "../../../lib/Word_Lib/SignedWords" CTypesBase begin diff --git a/tools/c-parser/umm_heap/Vanilla32.thy b/tools/c-parser/umm_heap/Vanilla32.thy index 566db0282..48b335132 100644 --- a/tools/c-parser/umm_heap/Vanilla32.thy +++ b/tools/c-parser/umm_heap/Vanilla32.thy @@ -11,7 +11,7 @@ (* License: BSD, terms see file ./LICENSE *) theory Vanilla32 -imports "../../../lib/Word_Lib/WordLib" CTypes +imports "../../../lib/Word_Lib/Word_Lib" CTypes begin section "Words and Pointers"