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