theory BitFieldProofsLib

lemma s_footprint_distinct_helper:
  "h_t_valid htd g (p :: 'a ptr) \<Longrightarrow> typ_uinfo_t TYPE('a :: c_type) \<bottom>\<^sub>t typ_uinfo_t TYPE('b :: c_type)
    \<Longrightarrow> (\<forall>q :: 'b ptr. h_t_valid htd g' q \<longrightarrow> s_footprint p \<inter> s_footprint q = {})" apply clarsimp apply (drule(1) h_t_valid_neq_disjoint) apply (clarsimp simp: sub_typ_proper_def tag_disj_def preorder_class.less_imp_le) apply (clarsimp simp: field_of_t_def) apply (drule field_of_sub) apply (simp add: tag_disj_def) apply (simp add: set_eq_iff ) apply (blast dest: s_footprintD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>htd,g \<Turnstile>\<^sub>t p; typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> \<forall>q. htd,g' \<Turnstile>\<^sub>t q \<longrightarrow> s_footprint p \<inter> s_footprint q = {} proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>htd,g \<Turnstile>\<^sub>t p; typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q\<rbrakk> \<Longrightarrow> s_footprint p \<inter> s_footprint q = {} proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q\<rbrakk> \<Longrightarrow> \<not> TYPE('b) <\<^sub>\<tau> TYPE('a)
 2. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q\<rbrakk> \<Longrightarrow> \<not> field_of_t p q
 3. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q; {ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {}\<rbrakk> \<Longrightarrow> s_footprint p \<inter> s_footprint q = {} proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q\<rbrakk> \<Longrightarrow> \<not> field_of_t p q
 2. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q; {ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {}\<rbrakk> \<Longrightarrow> s_footprint p \<inter> s_footprint q = {} proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q; field_of (ptr_val p - ptr_val q) (typ_uinfo_t TYPE('a)) (typ_uinfo_t TYPE('b))\<rbrakk> \<Longrightarrow> False
 2. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q; {ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {}\<rbrakk> \<Longrightarrow> s_footprint p \<inter> s_footprint q = {} proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q; typ_uinfo_t TYPE('a) \<le> typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> False
 2. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q; {ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {}\<rbrakk> \<Longrightarrow> s_footprint p \<inter> s_footprint q = {} proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q; {ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {}\<rbrakk> \<Longrightarrow> s_footprint p \<inter> s_footprint q = {} proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b); htd,g' \<Turnstile>\<^sub>t q; \<forall>x. x \<in> {ptr_val p..+size_of TYPE('a)} \<longrightarrow> x \<notin> {ptr_val q..+size_of TYPE('b)}\<rbrakk> \<Longrightarrow> \<forall>a b. (a, b) \<in> s_footprint p \<longrightarrow> (a, b) \<notin> s_footprint q proof (prove)
goal:
No subgoals!