theory CSpace_AI

lemma descendants:
  "descendants_of p m' =
  (if p = src
   then {}
   else if p = dest
   then descendants_of src m
   else descendants_of p m - {src} \<union>
        (if src \<in> descendants_of p m then {dest} else {}))" (is "?d = ?d'") proof  (rule set_eqI) fix x show "(x \<in> ?d) = (x \<in> ?d')" apply (simp add: descendants_of_def) apply safe apply (fastforce simp: parent_m'_m) apply (fastforce simp: parent_m_m') apply (fastforce simp: parent_m_m') apply (erule src_dest) apply (erule dest_src) apply (fastforce dest!: parent_m'_m split: if_split_asm) apply (fastforce simp: parent_m_m') done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of p m' = (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of p m') = (x \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {}))) proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of p m') = (x \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {}))) proof (prove)
goal (1 subgoal):
 1. (x \<in> descendants_of p m') = (x \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {}))) proof (prove)
goal (1 subgoal):
 1. (m \<Turnstile> p \<rightarrow> src \<longrightarrow> (p = dest \<longrightarrow> m' \<Turnstile> dest \<rightarrow> x = m \<Turnstile> src \<rightarrow> x) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> m' \<Turnstile> p \<rightarrow> x = (m \<Turnstile> p \<rightarrow> x \<and> x \<noteq> src \<or> x = dest))) \<and> ((p, src) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> (p = dest \<longrightarrow> m' \<Turnstile> dest \<rightarrow> x = m \<Turnstile> src \<rightarrow> x) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> m' \<Turnstile> p \<rightarrow> x = (m \<Turnstile> p \<rightarrow> x \<and> x \<noteq> src))) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> src; p \<noteq> dest; p \<noteq> src; m' \<Turnstile> p \<rightarrow> x; x \<noteq> dest\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> src; p \<noteq> dest; p \<noteq> src; m \<Turnstile> p \<rightarrow> x; x \<noteq> src\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> x
 3. \<lbrakk>m \<Turnstile> p \<rightarrow> src; p \<noteq> dest; p \<noteq> src; x = dest\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> dest
 4. \<lbrakk>p = dest; \<not> False; m' \<Turnstile> dest \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> x
 5. \<lbrakk>p = dest; \<not> False; m \<Turnstile> src \<rightarrow> x\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> x
 6. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m' \<Turnstile> p \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x
 7. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m \<Turnstile> p \<rightarrow> x; x \<noteq> src\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> x proof (prove)
goal (6 subgoals):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> src; p \<noteq> dest; p \<noteq> src; m \<Turnstile> p \<rightarrow> x; x \<noteq> src\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> x
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> src; p \<noteq> dest; p \<noteq> src; x = dest\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> dest
 3. \<lbrakk>p = dest; \<not> False; m' \<Turnstile> dest \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> x
 4. \<lbrakk>p = dest; \<not> False; m \<Turnstile> src \<rightarrow> x\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> x
 5. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m' \<Turnstile> p \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x
 6. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m \<Turnstile> p \<rightarrow> x; x \<noteq> src\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> x proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> src; p \<noteq> dest; p \<noteq> src; x = dest\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> dest
 2. \<lbrakk>p = dest; \<not> False; m' \<Turnstile> dest \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> x
 3. \<lbrakk>p = dest; \<not> False; m \<Turnstile> src \<rightarrow> x\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> x
 4. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m' \<Turnstile> p \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x
 5. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m \<Turnstile> p \<rightarrow> x; x \<noteq> src\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> x proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p = dest; \<not> False; m' \<Turnstile> dest \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> x
 2. \<lbrakk>p = dest; \<not> False; m \<Turnstile> src \<rightarrow> x\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> x
 3. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m' \<Turnstile> p \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x
 4. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m \<Turnstile> p \<rightarrow> x; x \<noteq> src\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = dest; \<not> False; m \<Turnstile> src \<rightarrow> x\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> x
 2. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m' \<Turnstile> p \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x
 3. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m \<Turnstile> p \<rightarrow> x; x \<noteq> src\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m' \<Turnstile> p \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x
 2. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m \<Turnstile> p \<rightarrow> x; x \<noteq> src\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p, src) \<notin> (cdt_parent_rel m)\<^sup>+; p \<noteq> dest; p \<noteq> src; m \<Turnstile> p \<rightarrow> x; x \<noteq> src\<rbrakk> \<Longrightarrow> m' \<Turnstile> p \<rightarrow> x proof (prove)
goal:
No subgoals! proof (state)
this:
(x \<in> descendants_of p m') = (x \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})))

goal:
No subgoals!