theory Untyped_DR

lemma free_range_of_untyped_subset'[rule_format]:
  assumes al: "is_aligned ptr sz"
    and sz: "sz < size (ptr)"
  shows "a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr" proof - note no_ov = is_aligned_no_overflow'[OF al] note mono = word_plus_mono_right[OF _ no_ov, simplified field_simps] note sz_len = sz[unfolded word_size] 
(*
  note sz_simp[simp] = unat_2p_sub_1[OF sz_len] unat_power_lower[OF sz_len]
*)
   show ?thesis using sz apply (intro impI psubsetI) apply (rule free_range_of_untyped_subseteq', simp_all add: al) apply (clarsimp simp:free_range_of_untyped_def) apply (strengthen mono word_of_nat_le)+ apply (simp add: sz_len unat_2p_sub_1) apply (intro conjI impI; (clarsimp dest!: le_p2_minus_1)?) apply (drule word_unat.Abs_eqD, simp_all add: unats_def word_size
           less_trans[OF _ power_strict_increasing[OF sz_len]]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr proof (state)
goal (1 subgoal):
 1. a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr proof (state)
this:
ptr \<le> ptr + (2 ^ sz - 1)

goal (1 subgoal):
 1. a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr proof (state)
this:
?y \<le> 2 ^ sz - 1 \<Longrightarrow> ptr + ?y \<le> ptr + 2 ^ sz - 1

goal (1 subgoal):
 1. a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr proof (state)
this:
sz < LENGTH('a)

goal (1 subgoal):
 1. a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr proof (state)
this:
sz < LENGTH('a)

goal (1 subgoal):
 1. a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr proof (prove)
goal (1 subgoal):
 1. a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr proof (prove)
using this:
sz < size ptr

goal (1 subgoal):
 1. a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < size ptr; a < a'; a < 2 ^ sz\<rbrakk> \<Longrightarrow> free_range_of_untyped a' sz ptr \<subseteq> free_range_of_untyped a sz ptr
 2. \<lbrakk>sz < size ptr; a < a'; a < 2 ^ sz\<rbrakk> \<Longrightarrow> free_range_of_untyped a' sz ptr \<noteq> free_range_of_untyped a sz ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < size ptr; a < a'; a < 2 ^ sz\<rbrakk> \<Longrightarrow> free_range_of_untyped a' sz ptr \<noteq> free_range_of_untyped a sz ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < size ptr; a < a'; a < 2 ^ sz\<rbrakk> \<Longrightarrow> (a' \<le> 2 ^ sz - Suc 0 \<longrightarrow> word_of_nat a' \<noteq> word_of_nat a \<and> (ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1 \<or> ptr + word_of_nat a \<le> ptr + 2 ^ sz - 1)) \<and> (\<not> a' \<le> 2 ^ sz - Suc 0 \<longrightarrow> (a \<le> 2 ^ sz - Suc 0 \<longrightarrow> ptr + word_of_nat a \<le> ptr + 2 ^ sz - 1) \<and> a \<le> 2 ^ sz - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < size ptr; a < a'; a < 2 ^ sz\<rbrakk> \<Longrightarrow> (a' \<le> 2 ^ sz - Suc 0 \<longrightarrow> word_of_nat a' \<noteq> word_of_nat a \<and> (a' \<le> unat (2 ^ sz - 1) \<or> a \<le> unat (2 ^ sz - 1))) \<and> (\<not> a' \<le> 2 ^ sz - Suc 0 \<longrightarrow> (a \<le> 2 ^ sz - Suc 0 \<longrightarrow> a \<le> unat (2 ^ sz - 1)) \<and> a \<le> 2 ^ sz - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < size ptr; a < a'; a < 2 ^ sz\<rbrakk> \<Longrightarrow> (a' \<le> 2 ^ sz - Suc 0 \<longrightarrow> word_of_nat a' \<noteq> word_of_nat a) \<and> (\<not> a' \<le> 2 ^ sz - Suc 0 \<longrightarrow> a \<le> 2 ^ sz - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < size ptr; a < a'; a' < 2 ^ sz; word_of_nat a' = word_of_nat a\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>sz < size ptr; a < a'; a < 2 ^ sz; \<not> a' \<le> 2 ^ sz - Suc 0\<rbrakk> \<Longrightarrow> a \<le> 2 ^ sz - Suc 0 proof (prove)
goal:
No subgoals! proof (state)
this:
a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr

goal:
No subgoals!