theory Example_Valid_StateH

lemma s0H_pspace_distinct':
  notes pdeBits_def[simp] pteBits_def[simp] objBits_defs[simp]
  shows
  "pspace_distinct' s0H_internal" supply option.case_cong[cong] if_cong[cong] apply (clarsimp simp: pspace_distinct'_def ps_clear_def) apply (rule disjointI) apply clarsimp apply (drule kh0H_SomeD)+ by (simp | erule disjE
        | clarsimp simp: kh0H_dom_sets_distinct[THEN orthD1]
        | clarsimp simp: kh0H_dom_sets_distinct[THEN orthD2]
        | fastforce simp: s0_ptr_defs objBitsKO_def pageBits_def kh0H_obj_def
        | clarsimp simp: irq_node_offs_range_def objBitsKO_def s0_ptr_defs,
          drule_tac x="0xF" in word_plus_strict_mono_right, fastforce, simp add: add.commute,
          drule(1) notE[rotated, OF less_trans, OF _ _ leD, rotated 2], fastforce, simp
        | clarsimp simp: pt_offs_range_def pd_offs_range_def irq_node_offs_range_def cnode_offs_range_def objBitsKO_def archObjSize_def s0_ptr_defs kh0H_obj_def,
          drule(1) aligned_le_sharp, simp add: mask_def,
          drule_tac x="0x3" in word_plus_mono_right, fastforce, simp add: add.commute,
          (drule(1) notE[rotated, OF le_less_trans, OF _ _ leD, rotated 2], fastforce, simp
          | drule(2) notE[rotated, OF le_less_trans, OF _ _ leD[OF order_trans], rotated 2], fastforce, simp)
        | clarsimp simp: objBitsKO_def pageBits_def cnode_offs_range_def pd_offs_range_def pt_offs_range_def irq_node_offs_range_def s0_ptr_defs kh0H_obj_def,
          drule(1) notE[rotated, OF le_less_trans, OF _ _ leD, rotated 2]
                   notE[rotated, OF le_less_trans, OF _ _ leD], fastforce, simp
        | (clarsimp simp: objBitsKO_def pageBits_def cnode_offs_range_def pd_offs_range_def pt_offs_range_def irq_node_offs_range_def s0_ptr_defs kh0H_obj_def Low_cte'_def Low_capsH_def cte_level_bits_def empty_cte_def High_cte'_def High_capsH_def Silc_cte'_def Silc_capsH_def split: if_split_asm,
         (drule(1) aligned_le_sharp, simp add: mask_def,
          drule_tac x="0xF" in word_plus_mono_right, fastforce, simp add: add.commute,
          (drule(1) notE[rotated, OF le_less_trans, OF _ _ leD, rotated 2]
                    notE[rotated, OF le_less_trans, OF _ _ leD], fastforce, simp
          | drule(2) notE[rotated, OF less_trans, OF _ _ leD[OF order_trans], rotated 2]
                     notE[rotated, OF le_less_trans, OF _ _ leD[OF order_trans], rotated 2],
               fastforce, simp))+)[1]
        | clarsimp simp: objBitsKO_def irq_node_offs_range_def cnode_offs_range_def pd_offs_range_def pt_offs_range_def cte_level_bits_def s0_ptr_defs,
          drule_tac x="0xF" in word_plus_strict_mono_right, fastforce, simp add: add.commute,
          drule(2) notE[rotated, OF less_trans, OF _ _ leD[OF order_trans], rotated 2]
                   notE[rotated, OF le_less_trans, OF _ _ leD[OF order_trans], rotated 2],
              fastforce, simp
        | (clarsimp simp: irq_node_offs_range_def cnode_offs_range_def pd_offs_range_def pt_offs_range_def s0_ptr_defs objBitsKO_def archObjSize_def kh0H_obj_def Low_cte'_def Low_capsH_def High_cte'_def High_capsH_def Silc_cte'_def Silc_capsH_def cte_level_bits_def empty_cte_def split: if_split_asm,
          (drule(1) aligned_le_sharp, simp add: mask_neg_add_aligned, fastforce simp: mask_def)+)[1])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_distinct' s0H_internal proof (prove)
goal (1 subgoal):
 1. pspace_distinct' s0H_internal proof (prove)
goal (1 subgoal):
 1. \<And>x y. kh0H x = Some y \<Longrightarrow> ({x..x + 2 ^ objBitsKO y - 1} - {x}) \<inter> dom kh0H = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>kh0H x = Some y; xa \<in> {x..x + 2 ^ objBitsKO y - 1} - {x}; ya \<in> dom kh0H\<rbrakk> \<Longrightarrow> xa \<noteq> ya proof (prove)
goal (1 subgoal):
 1. \<And>x y ya yb. \<lbrakk>kh0H x = Some y; kh0H ya = Some yb; x \<le> ya; ya \<le> x + 2 ^ objBitsKO y - 1; ya \<noteq> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y ya yb. \<lbrakk>x \<le> ya; ya \<le> x + 2 ^ objBitsKO y - 1; ya \<noteq> x; x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x); ya = init_globals_frame \<and> yb = KOUserData \<or> ya = idle_tcb_ptr \<and> yb = KOTCB idle_tcbH \<or> ya = High_tcb_ptr \<and> yb = KOTCB High_tcbH \<or> ya = Low_tcb_ptr \<and> yb = KOTCB Low_tcbH \<or> ya = ntfn_ptr \<and> yb = KONotification ntfnH \<or> ya = irq_cnode_ptr \<and> yb = KOCTE irq_cte \<or> ya \<in> irq_node_offs_range \<and> yb = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> ya \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr ya \<noteq> None \<and> yb = the (Low_cte Low_cnode_ptr ya) \<or> ya \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr ya \<noteq> None \<and> yb = the (High_cte High_cnode_ptr ya) \<or> ya \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr ya \<noteq> None \<and> yb = the (Silc_cte Silc_cnode_ptr ya) \<or> ya \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd ya \<noteq> None \<and> yb = the (global_pdH' init_global_pd ya) \<or> ya \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr ya \<noteq> None \<and> yb = the (High_pdH High_pd_ptr ya) \<or> ya \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr ya \<noteq> None \<and> yb = the (Low_pdH Low_pd_ptr ya) \<or> ya \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr ya \<noteq> None \<and> yb = the (High_ptH High_pt_ptr ya) \<or> ya \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr ya \<noteq> None \<and> yb = the (Low_ptH Low_pt_ptr ya)\<rbrakk> \<Longrightarrow> False