theory KHeap_DR

lemma removed_descendants_subset:
  assumes slot: "slot \<in> KHeap_D.descendants_of p s"
  defines "s' \<equiv> s\<lparr>cdl_cdt :=
                     \<lambda>x. if x = slot
                         then None
                         else if cdl_cdt s x = Some slot
                         then cdl_cdt s slot
                         else cdl_cdt s x\<rparr>"
  shows "KHeap_D.descendants_of p s' \<subset> KHeap_D.descendants_of p s" (is "?new \<subset> ?old") proof have "slot \<notin> ?new" apply (clarsimp simp: KHeap_D.descendants_of_def) apply (erule tranclE) apply (clarsimp simp: KHeap_D.cdt_parent_rel_def KHeap_D.is_cdt_parent_def s'_def) apply (clarsimp simp: KHeap_D.cdt_parent_rel_def KHeap_D.is_cdt_parent_def s'_def) done with slot show "?new \<noteq> ?old" by auto { fix p' assume p': "p' \<in> ?new" then have "p' \<in> ?old" unfolding KHeap_D.descendants_of_def apply clarsimp apply (induct rule: trancl_induct) apply (fastforce simp: KHeap_D.cdt_parent_rel_def KHeap_D.is_cdt_parent_def s'_def
                       split: if_split_asm
                       intro: trancl_trans) apply (erule trancl_trans) apply (fastforce simp: KHeap_D.cdt_parent_rel_def KHeap_D.is_cdt_parent_def s'_def
                      split: if_split_asm
                      intro: trancl_trans) done } thus "?new \<subseteq> ?old" by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. KHeap_D.descendants_of p s' \<subset> KHeap_D.descendants_of p s proof (state)
goal (2 subgoals):
 1. KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s
 2. KHeap_D.descendants_of p s' \<noteq> KHeap_D.descendants_of p s proof (prove)
goal (1 subgoal):
 1. slot \<notin> KHeap_D.descendants_of p s' proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> p cdt_parent_of\<^sup>+ slot \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. s' \<turnstile> p cdt_parent_of slot \<Longrightarrow> False
 2. \<And>c. \<lbrakk>s' \<turnstile> p cdt_parent_of\<^sup>+ c; s' \<turnstile> c cdt_parent_of slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>s' \<turnstile> p cdt_parent_of\<^sup>+ c; s' \<turnstile> c cdt_parent_of slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
slot \<notin> KHeap_D.descendants_of p s'

goal (2 subgoals):
 1. KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s
 2. KHeap_D.descendants_of p s' \<noteq> KHeap_D.descendants_of p s proof (chain)
picking this:
slot \<in> KHeap_D.descendants_of p s
slot \<notin> KHeap_D.descendants_of p s' proof (prove)
using this:
slot \<in> KHeap_D.descendants_of p s
slot \<notin> KHeap_D.descendants_of p s'

goal (1 subgoal):
 1. KHeap_D.descendants_of p s' \<noteq> KHeap_D.descendants_of p s proof (state)
this:
KHeap_D.descendants_of p s' \<noteq> KHeap_D.descendants_of p s

goal (1 subgoal):
 1. KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s proof (state)
this:
KHeap_D.descendants_of p s' \<noteq> KHeap_D.descendants_of p s

goal (1 subgoal):
 1. KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s proof (state)
goal (1 subgoal):
 1. KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s proof (state)
this:
p' \<in> KHeap_D.descendants_of p s'

goal (1 subgoal):
 1. KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s proof (chain)
picking this:
p' \<in> KHeap_D.descendants_of p s' proof (prove)
using this:
p' \<in> KHeap_D.descendants_of p s'

goal (1 subgoal):
 1. p' \<in> KHeap_D.descendants_of p s proof (prove)
using this:
p' \<in> {q. s' \<turnstile> p cdt_parent_of\<^sup>+ q}

goal (1 subgoal):
 1. p' \<in> {q. s \<turnstile> p cdt_parent_of\<^sup>+ q} proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> p cdt_parent_of\<^sup>+ p' \<Longrightarrow> s \<turnstile> p cdt_parent_of\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>y. s' \<turnstile> p cdt_parent_of y \<Longrightarrow> s \<turnstile> p cdt_parent_of\<^sup>+ y
 2. \<And>y z. \<lbrakk>s' \<turnstile> p cdt_parent_of\<^sup>+ y; s' \<turnstile> y cdt_parent_of z; s \<turnstile> p cdt_parent_of\<^sup>+ y\<rbrakk> \<Longrightarrow> s \<turnstile> p cdt_parent_of\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>s' \<turnstile> p cdt_parent_of\<^sup>+ y; s' \<turnstile> y cdt_parent_of z; s \<turnstile> p cdt_parent_of\<^sup>+ y\<rbrakk> \<Longrightarrow> s \<turnstile> p cdt_parent_of\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>s' \<turnstile> p cdt_parent_of\<^sup>+ y; s' \<turnstile> y cdt_parent_of z\<rbrakk> \<Longrightarrow> s \<turnstile> y cdt_parent_of\<^sup>+ z proof (prove)
goal:
No subgoals! proof (state)
this:
p' \<in> KHeap_D.descendants_of p s

goal (1 subgoal):
 1. KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s proof (state)
this:
?p'2 \<in> KHeap_D.descendants_of p s' \<Longrightarrow> ?p'2 \<in> KHeap_D.descendants_of p s

goal (1 subgoal):
 1. KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s proof (prove)
using this:
?p'2 \<in> KHeap_D.descendants_of p s' \<Longrightarrow> ?p'2 \<in> KHeap_D.descendants_of p s

goal (1 subgoal):
 1. KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s proof (state)
this:
KHeap_D.descendants_of p s' \<subseteq> KHeap_D.descendants_of p s

goal:
No subgoals!