theory ArchVSpace_AI

lemma valid_pte_lift3:
  assumes x: "(\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>)"
  shows "\<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>" apply (insert bool_function_four_cases[where f=P]) apply (erule disjE) apply (cases pte) apply (simp add: data_at_def | wp hoare_vcg_const_imp_lift x)+ apply (erule disjE) apply (cases pte) apply (simp add: data_at_def | wp hoare_vcg_disj_lift hoare_vcg_const_imp_lift x)+ apply (erule disjE) apply (simp | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. P = Not \<or> P = id \<or> P = (\<lambda>_. True) \<or> P = (\<lambda>_. False) \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. P = Not \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
 2. P = id \<or> P = (\<lambda>_. True) \<or> P = (\<lambda>_. False) \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>P = Not; pte = InvalidPTE\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
 2. \<And>x21 x22 x23. \<lbrakk>P = Not; pte = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
 3. \<And>x31 x32 x33. \<lbrakk>P = Not; pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
 4. P = id \<or> P = (\<lambda>_. True) \<or> P = (\<lambda>_. False) \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. P = id \<or> P = (\<lambda>_. True) \<or> P = (\<lambda>_. False) \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. P = id \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
 2. P = (\<lambda>_. True) \<or> P = (\<lambda>_. False) \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>P = id; pte = InvalidPTE\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
 2. \<And>x21 x22 x23. \<lbrakk>P = id; pte = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
 3. \<And>x31 x32 x33. \<lbrakk>P = id; pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
 4. P = (\<lambda>_. True) \<or> P = (\<lambda>_. False) \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. P = (\<lambda>_. True) \<or> P = (\<lambda>_. False) \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. P = (\<lambda>_. True) \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
 2. P = (\<lambda>_. False) \<Longrightarrow> \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace> proof (prove)
goal:
No subgoals!