theory ArchVSpace_AI

lemma vs_lookup_Cons_eq:
  "(ref \<rhd> p) s \<Longrightarrow> ((v # ref) \<rhd> p') s = ((ref, p) \<rhd>1 (v # ref, p')) s" apply (rule iffI) apply (clarsimp simp: vs_lookup_def vs_asid_refs_def
                  dest!: graph_ofD) apply (frule vs_lookup1_trans_is_append[where ys=ref]) apply (frule vs_lookup1_trans_is_append[where ys="v # ref"]) apply (clarsimp dest!: vs_lookup1_rtrancl_iterations vs_lookup1D) apply (clarsimp simp add: up_ucast_inj_eq) apply (drule(1) vs_lookup1_inj) apply (simp add: vs_lookup1I) apply (erule vs_lookup_trancl_step) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ref \<rhd> p) s \<Longrightarrow> ((v # ref) \<rhd> p') s = (((ref, p), v # ref, p') \<in> vs_lookup1 s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(ref \<rhd> p) s; ((v # ref) \<rhd> p') s\<rbrakk> \<Longrightarrow> ((ref, p), v # ref, p') \<in> vs_lookup1 s
 2. \<lbrakk>(ref \<rhd> p) s; ((ref, p), v # ref, p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((v # ref) \<rhd> p') s proof (prove)
goal (2 subgoals):
 1. \<And>ab bb ac bc. \<lbrakk>(([VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), ref, p) \<in> (vs_lookup1 s)\<^sup>*; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bc), v # ref, p') \<in> (vs_lookup1 s)\<^sup>*; asid_table s ab = Some bb; asid_table s ac = Some bc\<rbrakk> \<Longrightarrow> ((ref, p), v # ref, p') \<in> vs_lookup1 s
 2. \<lbrakk>(ref \<rhd> p) s; ((ref, p), v # ref, p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((v # ref) \<rhd> p') s proof (prove)
goal (2 subgoals):
 1. \<And>ab bb ac bc. \<lbrakk>(([VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), ref, p) \<in> (vs_lookup1 s)\<^sup>*; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bc), v # ref, p') \<in> (vs_lookup1 s)\<^sup>*; asid_table s ab = Some bb; asid_table s ac = Some bc; \<exists>zs. ref = zs @ [VSRef (UCAST(7 \<rightarrow> 32) ab) None]\<rbrakk> \<Longrightarrow> ((ref, p), v # ref, p') \<in> vs_lookup1 s
 2. \<lbrakk>(ref \<rhd> p) s; ((ref, p), v # ref, p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((v # ref) \<rhd> p') s proof (prove)
goal (2 subgoals):
 1. \<And>ab bb ac bc. \<lbrakk>(([VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), ref, p) \<in> (vs_lookup1 s)\<^sup>*; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bc), v # ref, p') \<in> (vs_lookup1 s)\<^sup>*; asid_table s ab = Some bb; asid_table s ac = Some bc; \<exists>zs. ref = zs @ [VSRef (UCAST(7 \<rightarrow> 32) ab) None]; \<exists>zs. v # ref = zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None]\<rbrakk> \<Longrightarrow> ((ref, p), v # ref, p') \<in> vs_lookup1 s
 2. \<lbrakk>(ref \<rhd> p) s; ((ref, p), v # ref, p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((v # ref) \<rhd> p') s proof (prove)
goal (2 subgoals):
 1. \<And>ab bb ac zs b pa ko. \<lbrakk>asid_table s ab = Some bb; asid_table s ac = Some b; ref = zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None]; UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) ac; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bb), zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], p) \<in> vs_lookup1 s ^^ length zs; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], b), zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], pa) \<in> vs_lookup1 s ^^ length zs; ko_at ko pa s; (v, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], p), v # zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], p') \<in> vs_lookup1 s
 2. \<lbrakk>(ref \<rhd> p) s; ((ref, p), v # ref, p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((v # ref) \<rhd> p') s proof (prove)
goal (2 subgoals):
 1. \<And>bb ac zs pa ko. \<lbrakk>asid_table s ac = Some bb; ref = zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None]; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bb), zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], p) \<in> vs_lookup1 s ^^ length zs; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bb), zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], pa) \<in> vs_lookup1 s ^^ length zs; ko_at ko pa s; (v, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], p), v # zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], p') \<in> vs_lookup1 s
 2. \<lbrakk>(ref \<rhd> p) s; ((ref, p), v # ref, p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((v # ref) \<rhd> p') s proof (prove)
goal (2 subgoals):
 1. \<And>bb ac zs pa ko. \<lbrakk>asid_table s ac = Some bb; ref = zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None]; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bb), zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], pa) \<in> vs_lookup1 s ^^ length zs; ko_at ko pa s; (v, p') \<in> vs_refs ko; p = pa\<rbrakk> \<Longrightarrow> ((zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], p), v # zs @ [VSRef (UCAST(7 \<rightarrow> 32) ac) None], p') \<in> vs_lookup1 s
 2. \<lbrakk>(ref \<rhd> p) s; ((ref, p), v # ref, p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((v # ref) \<rhd> p') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; ((ref, p), v # ref, p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((v # ref) \<rhd> p') s proof (prove)
goal (1 subgoal):
 1. ((ref, p), v # ref, p') \<in> vs_lookup1 s \<Longrightarrow> ((ref, p), v # ref, p') \<in> (vs_lookup1 s)\<^sup>+ proof (prove)
goal:
No subgoals!