theory Simple_Separation_Example

lemma "VARS H p q r
  {(list p Ps ** list q Qs) H}
  WHILE p \<noteq> 0
  INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs}
  DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
  {list q (rev Ps @ Qs) H}" apply vcg apply fastforce apply clarsimp apply (case_tac ps, simp) apply (rename_tac p ps') apply (rule_tac x = "ps'" in exI) apply (rule_tac x = "p # qs" in exI) apply clarsimp apply (clarsimp simp: sep_conj_exists sep_conj_ac) apply (rule_tac x = "q" in exI) thm points_to apply (subst (asm) sep_conj_ac) apply (subst (asm) sep_conj_commute) apply (simp add: sep_conj_assoc) apply (frule points_to) apply simp thm maps_to_write apply (subst sep_conj_assoc[symmetric]) apply (subst sep_conj_commute) apply (simp add: sep_conj_assoc) apply (rule maps_to_write) thm maps_to_maps_to_ex apply (drule sep_conj_impl1[rotated]) apply (erule maps_to_maps_to_ex) apply (rule sep_conj_impl1[rotated]) apply (subst sep_conj_ac, assumption) apply assumption apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {(list p Ps \<and>* list q Qs) H}
WHILE p \<noteq> 0 INV {\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs}  VAR {0} 
DO r := p; p := the (H p); H := H(r \<mapsto> q); q := r OD
{list q (rev Ps @ Qs) H} proof (prove)
goal (3 subgoals):
 1. \<And>H p q r. (list p Ps \<and>* list q Qs) H \<Longrightarrow> \<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> 0 \<Longrightarrow> \<exists>ps qs. (list (the (H p)) ps \<and>* list p qs) (H(p \<mapsto> q)) \<and> rev ps @ qs = rev Ps @ Qs
 3. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> 0 \<Longrightarrow> \<exists>ps qs. (list (the (H p)) ps \<and>* list p qs) (H(p \<mapsto> q)) \<and> rev ps @ qs = rev Ps @ Qs
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H p q ps qs. \<lbrakk>0 < p; (list p ps \<and>* list q qs) H; rev ps @ qs = rev Ps @ Qs\<rbrakk> \<Longrightarrow> \<exists>ps qs. (list (the (H p)) ps \<and>* list p qs) (H(p \<mapsto> q)) \<and> rev ps @ qs = rev Ps @ Qs
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H p q ps qs a lista. \<lbrakk>0 < p; (list p ps \<and>* list q qs) H; rev ps @ qs = rev Ps @ Qs; ps = a # lista\<rbrakk> \<Longrightarrow> \<exists>ps qs. (list (the (H p)) ps \<and>* list p qs) (H(p \<mapsto> q)) \<and> rev ps @ qs = rev Ps @ Qs
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q ps qs p ps'. \<lbrakk>0 < pa; (list pa ps \<and>* list q qs) H; rev ps @ qs = rev Ps @ Qs; ps = p # ps'\<rbrakk> \<Longrightarrow> \<exists>ps qs. (list (the (H pa)) ps \<and>* list pa qs) (H(pa \<mapsto> q)) \<and> rev ps @ qs = rev Ps @ Qs
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q ps qs p ps'. \<lbrakk>0 < pa; (list pa ps \<and>* list q qs) H; rev ps @ qs = rev Ps @ Qs; ps = p # ps'\<rbrakk> \<Longrightarrow> \<exists>qs. (list (the (H pa)) ps' \<and>* list pa qs) (H(pa \<mapsto> q)) \<and> rev ps' @ qs = rev Ps @ Qs
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q ps qs p ps'. \<lbrakk>0 < pa; (list pa ps \<and>* list q qs) H; rev ps @ qs = rev Ps @ Qs; ps = p # ps'\<rbrakk> \<Longrightarrow> (list (the (H pa)) ps' \<and>* list pa (p # qs)) (H(pa \<mapsto> q)) \<and> rev ps' @ p # qs = rev Ps @ Qs
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps'. \<lbrakk>0 < pa; ((\<lambda>s. \<exists>x. (pa \<mapsto> x \<and>* list x ps') s) \<and>* list q qs) H; rev ps' @ pa # qs = rev Ps @ Qs\<rbrakk> \<Longrightarrow> (list (the (H pa)) ps' \<and>* (\<lambda>s. \<exists>x. (pa \<mapsto> x \<and>* list x qs) s)) (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* pa \<mapsto> x) H\<rbrakk> \<Longrightarrow> \<exists>x. (list x qs \<and>* pa \<mapsto> x \<and>* list (the (H pa)) ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* pa \<mapsto> x) H\<rbrakk> \<Longrightarrow> (list q qs \<and>* pa \<mapsto> q \<and>* list (the (H pa)) ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* pa \<mapsto> x) H\<rbrakk> \<Longrightarrow> (list q qs \<and>* pa \<mapsto> q \<and>* list (the (H pa)) ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; ((list x ps' \<and>* pa \<mapsto> x) \<and>* list q qs) H\<rbrakk> \<Longrightarrow> (list q qs \<and>* pa \<mapsto> q \<and>* list (the (H pa)) ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; ((pa \<mapsto> x \<and>* list x ps') \<and>* list q qs) H\<rbrakk> \<Longrightarrow> (list q qs \<and>* pa \<mapsto> q \<and>* list (the (H pa)) ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (pa \<mapsto> x \<and>* list x ps' \<and>* list q qs) H\<rbrakk> \<Longrightarrow> (list q qs \<and>* pa \<mapsto> q \<and>* list (the (H pa)) ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (pa \<mapsto> x \<and>* list x ps' \<and>* list q qs) H; the (H pa) = x\<rbrakk> \<Longrightarrow> (list q qs \<and>* pa \<mapsto> q \<and>* list (the (H pa)) ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (pa \<mapsto> x \<and>* list x ps' \<and>* list q qs) H; the (H pa) = x\<rbrakk> \<Longrightarrow> (list q qs \<and>* pa \<mapsto> q \<and>* list x ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (pa \<mapsto> x \<and>* list x ps' \<and>* list q qs) H; the (H pa) = x\<rbrakk> \<Longrightarrow> (list q qs \<and>* pa \<mapsto> q \<and>* list x ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (pa \<mapsto> x \<and>* list x ps' \<and>* list q qs) H; the (H pa) = x\<rbrakk> \<Longrightarrow> ((list q qs \<and>* pa \<mapsto> q) \<and>* list x ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (pa \<mapsto> x \<and>* list x ps' \<and>* list q qs) H; the (H pa) = x\<rbrakk> \<Longrightarrow> ((pa \<mapsto> q \<and>* list q qs) \<and>* list x ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (pa \<mapsto> x \<and>* list x ps' \<and>* list q qs) H; the (H pa) = x\<rbrakk> \<Longrightarrow> (pa \<mapsto> q \<and>* list q qs \<and>* list x ps') (H(pa \<mapsto> q))
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (pa \<mapsto> x \<and>* list x ps' \<and>* list q qs) H; the (H pa) = x\<rbrakk> \<Longrightarrow> (pa \<mapsto> - \<and>* list q qs \<and>* list x ps') H
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; (pa \<mapsto> x \<and>* list x ps' \<and>* list q qs) H; the (H pa) = x\<rbrakk> \<Longrightarrow> (pa \<mapsto> - \<and>* list q qs \<and>* list x ps') H
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (3 subgoals):
 1. \<And>H pa q qs ps' x h. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; the (H pa) = x; (pa \<mapsto> x) h\<rbrakk> \<Longrightarrow> ?I62 H pa q qs ps' x h
 2. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; the (H pa) = x; (?I62 H pa q qs ps' x \<and>* list x ps' \<and>* list q qs) H\<rbrakk> \<Longrightarrow> (pa \<mapsto> - \<and>* list q qs \<and>* list x ps') H
 3. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; the (H pa) = x; (pa \<mapsto> - \<and>* list x ps' \<and>* list q qs) H\<rbrakk> \<Longrightarrow> (pa \<mapsto> - \<and>* list q qs \<and>* list x ps') H
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (3 subgoals):
 1. \<And>H pa q qs ps' x. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; the (H pa) = x; (pa \<mapsto> - \<and>* list x ps' \<and>* list q qs) H\<rbrakk> \<Longrightarrow> (?P66 H pa q qs ps' x \<and>* list q qs \<and>* list x ps') H
 2. \<And>H pa q qs ps' x h. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; the (H pa) = x; (pa \<mapsto> - \<and>* list x ps' \<and>* list q qs) H; ?P66 H pa q qs ps' x h\<rbrakk> \<Longrightarrow> (pa \<mapsto> -) h
 3. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (2 subgoals):
 1. \<And>H pa q qs ps' x h. \<lbrakk>0 < pa; rev ps' @ pa # qs = rev Ps @ Qs; the (H pa) = x; (pa \<mapsto> - \<and>* list x ps' \<and>* list q qs) H; (pa \<mapsto> -) h\<rbrakk> \<Longrightarrow> (pa \<mapsto> -) h
 2. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal (1 subgoal):
 1. \<And>H p q r. (\<exists>ps qs. (list p ps \<and>* list q qs) H \<and> rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> 0 \<Longrightarrow> list q (rev Ps @ Qs) H proof (prove)
goal:
No subgoals!