theory Retype_C

lemma caps_no_overlap''_le2:
  "\<lbrakk>caps_no_overlap'' ptr sz s;ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz\<rbrakk>
    \<Longrightarrow> caps_no_overlap'' ptr' sz s" apply (clarsimp simp:caps_no_overlap''_def) apply (drule(1) bspec) apply (subgoal_tac  "{ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1}
                      \<subseteq>  {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}") apply (erule impE) apply (rule ccontr) apply clarify apply (drule(1) disjoint_subset2[rotated -1]) apply simp apply (erule subsetD)+ apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_no_overlap'' ptr sz s; ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr' sz s proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>\<forall>cte\<in>ran (ctes_of s). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 2. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 3. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<not> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 3. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<not> False; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 3. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<not> False; untypedRange (cteCap cte) \<inter> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 3. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 2. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> x \<in> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr'..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr' \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!