1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11theory ArchBits_AI
12imports "../Invariants_AI"
13begin
14
15context Arch begin global_naming ARM
16
17lemma invs_unique_table_caps[elim!]:
18  "invs s \<Longrightarrow> unique_table_caps (caps_of_state s)"
19  by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)
20
21lemma invs_unique_refs[elim!]:
22  "invs s \<Longrightarrow> unique_table_refs (caps_of_state s)"
23  by (simp add: invs_def valid_state_def valid_arch_caps_def)
24
25
26lemma invs_pd_caps:
27  "invs s \<Longrightarrow> valid_table_caps s"
28  by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)
29
30lemma invs_valid_vs_lookup[elim!]:
31  "invs s \<Longrightarrow> valid_vs_lookup s "
32  by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)
33
34lemma pbfs_atleast_pageBits:
35  "pageBits \<le> pageBitsForSize sz"
36  by (cases sz) (auto simp: pageBits_def)
37
38lemmas is_cap_simps = is_cap_simps is_arch_cap_simps
39lemmas valid_cap_def = valid_cap_def[simplified valid_arch_cap_def]
40
41lemmas valid_cap_simps =
42  valid_cap_def[split_simps cap.split arch_cap.split]
43
44end
45
46end
47