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