theory ArchUntyped_AI

lemma init_arch_objects_descendants_range[wp,Untyped_AI_assms]:
  "\<lbrace>\<lambda>(s::'state_ext::state_ext state). descendants_range x cref s \<rbrace> init_arch_objects ty ptr n us y
          \<lbrace>\<lambda>rv s. descendants_range x cref s\<rbrace>" apply (simp add:descendants_range_def) apply (rule hoare_pre) apply (wp retype_region_mdb init_arch_objects_hoare_lift) apply (wps do_machine_op_mdb) apply (wp hoare_vcg_ball_lift) apply (rule hoare_pre) apply (wps store_pde_mdb_inv) apply wp apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>descendants_range x cref\<rbrace> init_arch_objects ty ptr n us y \<lbrace>\<lambda>rv. descendants_range x cref\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s\<rbrace> init_arch_objects ty ptr n us y \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> init_arch_objects ty ptr n us y \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s\<rbrace>
 2. \<And>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>oper. \<lbrace>?P4\<rbrace> do_machine_op oper \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s\<rbrace>
 2. \<And>ptr val. \<lbrace>?P4\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv. ?P4\<rbrace>
 3. \<And>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s \<Longrightarrow> (?P4 and (\<lambda>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s)) s proof (prove)
goal (3 subgoals):
 1. \<And>oper prev_s. \<lbrace>?P7 prev_s\<rbrace> do_machine_op oper \<lbrace>\<lambda>rv s'. \<forall>p'\<in>descendants_of cref (cdt prev_s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' prev_s\<rbrace>
 2. \<And>ptr val. \<lbrace>\<lambda>s. ?P7 s s\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. ?P7 s s\<rbrace>
 3. \<And>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s \<Longrightarrow> ((\<lambda>s. ?P7 s s) and (\<lambda>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s)) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr val. \<lbrace>\<lambda>s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s\<rbrace>
 2. \<And>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s \<Longrightarrow> ((\<lambda>s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s) and (\<lambda>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s)) s proof (prove)
goal (3 subgoals):
 1. \<And>ptr val. \<lbrace>?Q20 ptr val\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s\<rbrace>
 2. \<And>ptr val s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s \<Longrightarrow> ?Q20 ptr val s
 3. \<And>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s \<Longrightarrow> ((\<lambda>s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s) and (\<lambda>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s)) s proof (prove)
goal (3 subgoals):
 1. \<And>ptr val prev_s. \<lbrace>?P23 ptr val prev_s\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s'. \<forall>xa\<in>descendants_of cref (cdt prev_s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa prev_s\<rbrace>
 2. \<And>ptr val s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s \<Longrightarrow> ?P23 ptr val s s
 3. \<And>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s \<Longrightarrow> ((\<lambda>s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s) and (\<lambda>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s)) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr val s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s \<Longrightarrow> \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s
 2. \<And>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s \<Longrightarrow> ((\<lambda>s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s) and (\<lambda>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s \<Longrightarrow> ((\<lambda>s. \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s) and (\<lambda>s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s)) s proof (prove)
goal:
No subgoals!