1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* Collects general lemmas in the capDL refinement proof. 8 Those should eventually be moved to Lib. 9 10 Also defines a single entry point for all drefine theories 11 in which global simpset and notation changes can be made. 12*) 13 14theory Lemmas_D 15imports 16 "DBaseRefine.Include_D" 17 MoreHOL 18 MoreCorres 19 "ExecSpec.InvocationLabels_H" 20begin 21 22no_notation bind_drop (infixl ">>" 60) 23 24declare fun_upd_restrict_conv[simp del] 25 26(* FIXME: move *) 27lemma nonempty_pick_in: 28 "a \<noteq> {} \<Longrightarrow> pick a \<in> a" 29 by (metis all_not_in_conv someI_ex) 30 31lemma pick_singleton[simp]: 32 "pick {a} = a" 33 apply (rule ccontr) 34 apply (cut_tac nonempty_pick_in) 35 apply fastforce 36 apply fastforce 37 done 38 39(* FIXME: eventually move to AInvs *) 40lemma is_tcb_TCB[simp]: "is_tcb (TCB t)" 41 by (simp add: is_tcb) 42 43declare dxo_wp_weak[wp del] 44declare is_aligned_no_overflow[simp] 45 46end 47