theory Sep_Eq

lemma sep_disj_addI1':
  "disjoint x (sep_add' y z) \<Longrightarrow> disjoint y z \<Longrightarrow> disjoint (sep_add' x y) z" apply (clarsimp simp: disjoint_def sep_add'_def) apply (rule conjI) apply clarsimp apply (frule lift_to_add2, assumption) apply (simp add: add_assoc) apply (clarsimp simp: lift2_def add_comm) apply clarsimp apply (frule lift_to_add2, assumption) apply (simp add: add_assoc) apply (clarsimp simp: lift2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x ## sep_add' y z; y ## z\<rbrakk> \<Longrightarrow> sep_add' x y ## z proof (prove)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> ((\<exists>ya. x \<oplus> y = Some ya) \<longrightarrow> (\<exists>ya. the (x \<oplus> y) \<oplus> z = Some ya)) \<and> (x \<oplus> y = None \<longrightarrow> (\<exists>y. undefined \<oplus> z = Some y)) proof (prove)
goal (2 subgoals):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> (\<exists>ya. x \<oplus> y = Some ya) \<longrightarrow> (\<exists>ya. the (x \<oplus> y) \<oplus> z = Some ya)
 2. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> x \<oplus> y = None \<longrightarrow> (\<exists>y. undefined \<oplus> z = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>ya yaa yb. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa; x \<oplus> y = Some yb\<rbrakk> \<Longrightarrow> \<exists>y. yb \<oplus> z = Some y
 2. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> x \<oplus> y = None \<longrightarrow> (\<exists>y. undefined \<oplus> z = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>ya yaa yb. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa; x \<oplus> y = Some yb; Some x ++ Some y ++ Some z = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. yb \<oplus> z = Some y
 2. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> x \<oplus> y = None \<longrightarrow> (\<exists>y. undefined \<oplus> z = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>ya yaa yb. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa; x \<oplus> y = Some yb; (Some x ++ Some y) ++ Some z = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. yb \<oplus> z = Some y
 2. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> x \<oplus> y = None \<longrightarrow> (\<exists>y. undefined \<oplus> z = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> x \<oplus> y = None \<longrightarrow> (\<exists>y. undefined \<oplus> z = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa; x \<oplus> y = None\<rbrakk> \<Longrightarrow> \<exists>y. undefined \<oplus> z = Some y proof (prove)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa; x \<oplus> y = None; Some x ++ Some y ++ Some z = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. undefined \<oplus> z = Some y proof (prove)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa; x \<oplus> y = None; (Some x ++ Some y) ++ Some z = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. undefined \<oplus> z = Some y proof (prove)
goal:
No subgoals!