theory Retype_C

lemma htd_update_list_not_tag_disj:
  "list_map (typ_slice_t td y)
        \<subseteq>\<^sub>m snd (htd_update_list p xs htd x)
    \<Longrightarrow> x \<in> {p ..+ length xs}
    \<Longrightarrow> y < size_td td
    \<Longrightarrow> length xs < addr_card
    \<Longrightarrow> set xs \<subseteq> list_map ` typ_slice_t td' ` {..< size_td td'}
    \<Longrightarrow> \<not> td \<bottom>\<^sub>t td'" apply (induct xs arbitrary: p htd) apply simp apply (clarsimp simp: intvl_Suc_right) apply (erule disjE) apply clarsimp apply (subst(asm) htd_update_list_same2,
     rule intvl_Suc_nmem'[where n="Suc m" for m, simplified]) apply (simp add: addr_card_def card_word) apply (simp add: list_map_plus_le_not_tag_disj) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}; y < size_td td; length xs < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t td' proof (prove)
goal (2 subgoals):
 1. \<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p [] htd x); x \<in> {p..+length []}; y < size_td td; length [] < addr_card; set [] \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t td'
 2. \<And>x1 xs p htd. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}; y < size_td td; length xs < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t td'; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p (x1 # xs) htd x); x \<in> {p..+length (x1 # xs)}; y < size_td td; length (x1 # xs) < addr_card; set (x1 # xs) \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t td' proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs p htd. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}; y < size_td td; length xs < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t td'; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p (x1 # xs) htd x); x \<in> {p..+length (x1 # xs)}; y < size_td td; length (x1 # xs) < addr_card; set (x1 # xs) \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t td' proof (prove)
goal (1 subgoal):
 1. \<And>xs p htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list (p + 1) xs (htd(p := (True, snd (htd p) ++ list_map (typ_slice_t td' xa)))) x); x = p \<or> x \<in> {p + 1..+length xs}; y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xs p htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list (p + 1) xs (htd(p := (True, snd (htd p) ++ list_map (typ_slice_t td' xa)))) x); y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'; x = p\<rbrakk> \<Longrightarrow> False
 2. \<And>xs p htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list (p + 1) xs (htd(p := (True, snd (htd p) ++ list_map (typ_slice_t td' xa)))) x); y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'; x \<in> {p + 1..+length xs}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xs htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list (x + 1) xs (htd(x := (True, snd (htd x) ++ list_map (typ_slice_t td' xa)))) x); y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'\<rbrakk> \<Longrightarrow> False
 2. \<And>xs p htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list (p + 1) xs (htd(p := (True, snd (htd p) ++ list_map (typ_slice_t td' xa)))) x); y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'; x \<in> {p + 1..+length xs}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>xs htd xa. \<lbrakk>y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'; \<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> Suc (length xs) < 2 ^ LENGTH(32)
 2. \<And>xs htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd ((htd(x := (True, snd (htd x) ++ list_map (typ_slice_t td' xa)))) x); y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'\<rbrakk> \<Longrightarrow> False
 3. \<And>xs p htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list (p + 1) xs (htd(p := (True, snd (htd p) ++ list_map (typ_slice_t td' xa)))) x); y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'; x \<in> {p + 1..+length xs}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xs htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd ((htd(x := (True, snd (htd x) ++ list_map (typ_slice_t td' xa)))) x); y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'\<rbrakk> \<Longrightarrow> False
 2. \<And>xs p htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list (p + 1) xs (htd(p := (True, snd (htd p) ++ list_map (typ_slice_t td' xa)))) x); y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'; x \<in> {p + 1..+length xs}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xs p htd xa. \<lbrakk>\<And>p htd. \<lbrakk>list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p xs htd x); x \<in> {p..+length xs}\<rbrakk> \<Longrightarrow> False; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list (p + 1) xs (htd(p := (True, snd (htd p) ++ list_map (typ_slice_t td' xa)))) x); y < size_td td; Suc (length xs) < addr_card; set xs \<subseteq> list_map ` typ_slice_t td' ` {..<size_td td'}; xa < size_td td'; td \<bottom>\<^sub>t td'; x \<in> {p + 1..+length xs}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!