theory VSpaceEntries_AI

lemma valid_entries_partial_copy:
  "\<lbrakk> valid_entries rg tab; valid_entries rg tab';
  \<forall>v x. P x \<longrightarrow> (rg v x \<subseteq> S);
  \<forall>v x. \<not> P x \<longrightarrow> (rg v x \<inter> S) = {}\<rbrakk>
       \<Longrightarrow> valid_entries rg (\<lambda>x. if P x then tab x else tab' x)" apply (subst valid_entries_def, simp) apply (intro allI impI conjI) apply (fastforce simp:valid_entries_def) apply (drule_tac x = "tab x" in spec) apply (drule_tac x = x in spec) apply (drule_tac x = "tab' y" in spec) apply (drule_tac x = y in spec) apply clarsimp apply blast apply (fastforce simp:valid_entries_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}\<rbrakk> \<Longrightarrow> valid_entries rg (\<lambda>x. if P x then tab x else tab' x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}\<rbrakk> \<Longrightarrow> \<forall>x. (P x \<longrightarrow> (\<forall>y. (P y \<longrightarrow> x \<noteq> y \<longrightarrow> rg (tab x) x \<inter> rg (tab y) y = {}) \<and> (\<not> P y \<longrightarrow> x \<noteq> y \<longrightarrow> rg (tab x) x \<inter> rg (tab' y) y = {}))) \<and> (\<not> P x \<longrightarrow> (\<forall>y. (P y \<longrightarrow> x \<noteq> y \<longrightarrow> rg (tab' x) x \<inter> rg (tab y) y = {}) \<and> (\<not> P y \<longrightarrow> x \<noteq> y \<longrightarrow> rg (tab' x) x \<inter> rg (tab' y) y = {}))) proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; P x; P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab x) x \<inter> rg (tab y) y = {}
 2. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab x) x \<inter> rg (tab' y) y = {}
 3. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab y) y = {}
 4. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab' y) y = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab x) x \<inter> rg (tab' y) y = {}
 2. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab y) y = {}
 3. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab' y) y = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; P x; \<not> P y; x \<noteq> y; \<forall>xa. P xa \<longrightarrow> rg (tab x) xa \<subseteq> S\<rbrakk> \<Longrightarrow> rg (tab x) x \<inter> rg (tab' y) y = {}
 2. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab y) y = {}
 3. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab' y) y = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; P x; \<not> P y; x \<noteq> y; P x \<longrightarrow> rg (tab x) x \<subseteq> S\<rbrakk> \<Longrightarrow> rg (tab x) x \<inter> rg (tab' y) y = {}
 2. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab y) y = {}
 3. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab' y) y = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; P x; \<not> P y; x \<noteq> y; P x \<longrightarrow> rg (tab x) x \<subseteq> S; \<forall>x. \<not> P x \<longrightarrow> rg (tab' y) x \<inter> S = {}\<rbrakk> \<Longrightarrow> rg (tab x) x \<inter> rg (tab' y) y = {}
 2. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab y) y = {}
 3. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab' y) y = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; P x; \<not> P y; x \<noteq> y; P x \<longrightarrow> rg (tab x) x \<subseteq> S; \<not> P y \<longrightarrow> rg (tab' y) y \<inter> S = {}\<rbrakk> \<Longrightarrow> rg (tab x) x \<inter> rg (tab' y) y = {}
 2. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab y) y = {}
 3. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab' y) y = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; P x; \<not> P y; x \<noteq> y; rg (tab x) x \<subseteq> S; rg (tab' y) y \<inter> S = {}\<rbrakk> \<Longrightarrow> rg (tab x) x \<inter> rg (tab' y) y = {}
 2. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab y) y = {}
 3. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab' y) y = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab y) y = {}
 2. \<And>x y. \<lbrakk>valid_entries rg tab; valid_entries rg tab'; \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}; \<not> P x; \<not> P y; x \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab' x) x \<inter> rg (tab' y) y = {} proof (prove)
goal:
No subgoals!