adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

ainvs: shorten proof of unique_table_refs_upd_eqD

This commit is contained in:
Rafal Kolanski 2019-07-29 13:33:06 +10:00
parent 95859fd47c
commit 5e2f9bd83b
4 changed files with 16 additions and 148 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
proof/invariant-abstract/ARM/ArchCSpace_AI.thy
View File

@ -131,43 +131,10 @@ lemma unique_table_refs_upd_eqD:
"\<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk>
\<Longrightarrow> unique_table_refs (ms (a \<mapsto> b')) = unique_table_refs ms"
unfolding unique_table_refs_def
apply (rule iffI)
apply (intro allI impI)
apply (case_tac "p=p'")
apply simp
apply (case_tac "a=p")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=b' in allE)
apply simp
apply (case_tac "a=p'")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (intro allI impI)
apply (case_tac "p=p'")
apply (thin_tac " \<forall>p. P p" for P)
apply simp
apply (case_tac "a=p")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=b in allE)
apply simp
apply (case_tac "a=p'")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
done
(* match up p and p' on both sides of equality *)
apply (rule all_cong[where Q=\<top>, simplified])
apply (rule all_cong[where Q=\<top>, simplified])
by auto
lemma set_untyped_cap_as_full_valid_arch_caps [CSpace_AI_assms]:
"\<lbrace>valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace>

41
proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy
View File

@ -130,43 +130,10 @@ lemma unique_table_refs_upd_eqD:
"\<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk>
\<Longrightarrow> unique_table_refs (ms (a \<mapsto> b')) = unique_table_refs ms"
unfolding unique_table_refs_def
apply (rule iffI)
apply (intro allI impI)
apply (case_tac "p=p'")
apply simp
apply (case_tac "a=p")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=b' in allE)
apply simp
apply (case_tac "a=p'")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (intro allI impI)
apply (case_tac "p=p'")
apply (thin_tac " \<forall>p. P p" for P)
apply simp
apply (case_tac "a=p")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=b in allE)
apply simp
apply (case_tac "a=p'")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
done
(* match up p and p' on both sides of equality *)
apply (rule all_cong[where Q=\<top>, simplified])
apply (rule all_cong[where Q=\<top>, simplified])
by auto
lemma set_untyped_cap_as_full_valid_arch_caps [CSpace_AI_assms]:
"\<lbrace>valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace>

41
proof/invariant-abstract/RISCV64/ArchCSpace_AI.thy
View File

@ -24,43 +24,10 @@ lemma unique_table_refs_upd_eqD:
"\<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk>
\<Longrightarrow> unique_table_refs_2 (ms (a \<mapsto> b')) = unique_table_refs_2 ms"
unfolding unique_table_refs_def
apply (rule iffI)
apply (intro allI impI)
apply (case_tac "p=p'")
apply simp
apply (case_tac "a=p")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=b' in allE)
apply simp
apply (case_tac "a=p'")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (intro allI impI)
apply (case_tac "p=p'")
apply (thin_tac " \<forall>p. P p" for P)
apply simp
apply (case_tac "a=p")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=b in allE)
apply simp
apply (case_tac "a=p'")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
done
(* match up p and p' on both sides of equality *)
apply (rule all_cong[where Q=\<top>, simplified])
apply (rule all_cong[where Q=\<top>, simplified])
by auto
lemma cte_at_length_limit:
"\<lbrakk> cte_at p s; valid_objs s \<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits"

41
proof/invariant-abstract/X64/ArchCSpace_AI.thy
View File

@ -133,43 +133,10 @@ lemma unique_table_refs_upd_eqD:
"\<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk>
\<Longrightarrow> unique_table_refs (ms (a \<mapsto> b')) = unique_table_refs ms"
unfolding unique_table_refs_def
apply (rule iffI)
apply (intro allI impI)
apply (case_tac "p=p'")
apply simp
apply (case_tac "a=p")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=b' in allE)
apply simp
apply (case_tac "a=p'")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (intro allI impI)
apply (case_tac "p=p'")
apply (thin_tac " \<forall>p. P p" for P)
apply simp
apply (case_tac "a=p")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=b in allE)
apply simp
apply (case_tac "a=p'")
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply (erule_tac x=cap in allE)
apply simp
done
(* match up p and p' on both sides of equality *)
apply (rule all_cong[where Q=\<top>, simplified])
apply (rule all_cong[where Q=\<top>, simplified])
by auto
lemma set_untyped_cap_as_full_valid_arch_caps [CSpace_AI_assms]:
"\<lbrace>valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace>