theory VSpaceEntries_AI

lemma valid_entries_overwrite_0:
  assumes ve: "valid_entries rg tab"
  assumes disjoint: "\<And>p. \<lbrakk>p \<noteq> x\<rbrakk> \<Longrightarrow> rg v x \<inter> rg (tab p) p = {}"
  shows "valid_entries rg (tab (x := v))" apply (subst valid_entries_def) apply clarsimp apply (intro allI impI conjI) apply clarsimp apply (rule disjoint) apply simp apply clarsimp apply (drule disjoint) apply blast using ve apply (clarsimp simp:valid_entries_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_entries rg (tab(x := v)) proof (prove)
goal (1 subgoal):
 1. \<forall>xa y. xa \<noteq> y \<longrightarrow> rg ((tab(x := v)) xa) xa \<inter> rg ((tab(x := v)) y) y = {} proof (prove)
goal (1 subgoal):
 1. \<And>xa. (xa = x \<longrightarrow> (\<forall>y. x \<noteq> y \<longrightarrow> rg v x \<inter> rg (tab y) y = {})) \<and> (xa \<noteq> x \<longrightarrow> (\<forall>y. (y = x \<longrightarrow> rg (tab xa) xa \<inter> rg v x = {}) \<and> (y \<noteq> x \<longrightarrow> xa \<noteq> y \<longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {}))) proof (prove)
goal (3 subgoals):
 1. \<And>xa y. \<lbrakk>xa = x; x \<noteq> y\<rbrakk> \<Longrightarrow> rg v x \<inter> rg (tab y) y = {}
 2. \<And>xa y. \<lbrakk>xa \<noteq> x; y = x\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg v x = {}
 3. \<And>xa y. \<lbrakk>xa \<noteq> x; y \<noteq> x; xa \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {} proof (prove)
goal (3 subgoals):
 1. \<And>y. x \<noteq> y \<Longrightarrow> rg v x \<inter> rg (tab y) y = {}
 2. \<And>xa y. \<lbrakk>xa \<noteq> x; y = x\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg v x = {}
 3. \<And>xa y. \<lbrakk>xa \<noteq> x; y \<noteq> x; xa \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {} proof (prove)
goal (3 subgoals):
 1. \<And>y. x \<noteq> y \<Longrightarrow> y \<noteq> x
 2. \<And>xa y. \<lbrakk>xa \<noteq> x; y = x\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg v x = {}
 3. \<And>xa y. \<lbrakk>xa \<noteq> x; y \<noteq> x; xa \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {} proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>xa \<noteq> x; y = x\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg v x = {}
 2. \<And>xa y. \<lbrakk>xa \<noteq> x; y \<noteq> x; xa \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {} proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<noteq> x \<Longrightarrow> rg (tab xa) xa \<inter> rg v x = {}
 2. \<And>xa y. \<lbrakk>xa \<noteq> x; y \<noteq> x; xa \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {} proof (prove)
goal (2 subgoals):
 1. \<And>xa. rg v x \<inter> rg (tab xa) xa = {} \<Longrightarrow> rg (tab xa) xa \<inter> rg v x = {}
 2. \<And>xa y. \<lbrakk>xa \<noteq> x; y \<noteq> x; xa \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {} proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa \<noteq> x; y \<noteq> x; xa \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {} proof (prove)
using this:
valid_entries rg tab

goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa \<noteq> x; y \<noteq> x; xa \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {} proof (prove)
goal:
No subgoals!