theory ArchInvariants_AI

lemma vs_lookup_induct:
  assumes r: "(ref \<rhd> p) s"
  assumes a: "\<And>asid p. \<lbrakk> arm_asid_table (arch_state s) asid = Some p \<rbrakk> \<Longrightarrow> P [VSRef (ucast asid) None] p s"
  assumes s: "\<And>ref p ref' p'. \<lbrakk> (ref \<rhd> p) s; ((ref,p) \<rhd>1 (ref',p')) s; P ref p s \<rbrakk> \<Longrightarrow> P ref' p' s"
  shows "P ref p s" using r apply (clarsimp simp: vs_lookup_def) apply (drule rtranclD) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply (frule a) apply (erule disjE, simp) apply clarsimp apply (drule vs_lookup_atI) apply (erule trancl_induct2) apply (erule (2) s) apply (drule (1) vs_lookup_trancl_step) apply (erule (2) s) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P ref p s proof (prove)
using this:
(ref \<rhd> p) s

goal (1 subgoal):
 1. P ref p s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((a, b), ref, p) \<in> (vs_lookup1 s)\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> P ref p s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); (a, b) = (ref, p) \<or> (a, b) \<noteq> (ref, p) \<and> ((a, b), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> P ref p s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>[VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<and> ba = p \<or> ([VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+; asid_table s aa = Some ba\<rbrakk> \<Longrightarrow> P ref p s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>[VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<and> ba = p \<or> ([VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+; asid_table s aa = Some ba; P [VSRef (UCAST(7 \<rightarrow> 32) aa) None] ba s\<rbrakk> \<Longrightarrow> P ref p s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; P [VSRef (UCAST(7 \<rightarrow> 32) aa) None] ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> P ref p s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; P [VSRef (UCAST(7 \<rightarrow> 32) aa) None] ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> P ref p s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>P [VSRef (UCAST(7 \<rightarrow> 32) aa) None] ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None] \<rhd> ba) s\<rbrakk> \<Longrightarrow> P ref p s proof (prove)
goal (2 subgoals):
 1. \<And>aa ba a b. \<lbrakk>P [VSRef (UCAST(7 \<rightarrow> 32) aa) None] ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None] \<rhd> ba) s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), a, b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> P a b s
 2. \<And>aa ba a b ab bb. \<lbrakk>P [VSRef (UCAST(7 \<rightarrow> 32) aa) None] ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None] \<rhd> ba) s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), a, b) \<in> (vs_lookup1 s)\<^sup>+; ((a, b), ab, bb) \<in> vs_lookup1 s; P a b s\<rbrakk> \<Longrightarrow> P ab bb s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba a b ab bb. \<lbrakk>P [VSRef (UCAST(7 \<rightarrow> 32) aa) None] ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None] \<rhd> ba) s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), a, b) \<in> (vs_lookup1 s)\<^sup>+; ((a, b), ab, bb) \<in> vs_lookup1 s; P a b s\<rbrakk> \<Longrightarrow> P ab bb s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba a b ab bb. \<lbrakk>P [VSRef (UCAST(7 \<rightarrow> 32) aa) None] ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), a, b) \<in> (vs_lookup1 s)\<^sup>+; ((a, b), ab, bb) \<in> vs_lookup1 s; P a b s; (a \<rhd> b) s\<rbrakk> \<Longrightarrow> P ab bb s proof (prove)
goal:
No subgoals!