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 q ps qs p' ps') apply (clarsimp simp: sep_conj_exists sep_conj_ac) apply (subst points_to, sep_solve) apply (rule_tac x = "ps'" in exI) apply (rule_tac x = "p # qs" in exI) apply (simp add: sep_conj_exists sep_conj_ac) apply (rule exI) apply (sep_rule (direct) maps_to_write) \<comment> \<open>note: demonstrates computation\<close> apply (sep_solve add: maps_to_maps_to_ex) 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 p q ps qs p' ps'. \<lbrakk>0 < p; (list p ps \<and>* list q qs) H; rev ps @ qs = rev Ps @ Qs; ps = p' # ps'\<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 qs ps' x. \<lbrakk>0 < p; rev ps' @ p # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* p \<mapsto> x) H\<rbrakk> \<Longrightarrow> \<exists>ps qs. (list p qs \<and>* list (the (H p)) ps) (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 qs ps' x. \<lbrakk>0 < p; rev ps' @ p # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* p \<mapsto> x) H\<rbrakk> \<Longrightarrow> \<exists>ps qs. (list p qs \<and>* list x ps) (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 qs ps' x. \<lbrakk>0 < p; rev ps' @ p # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* p \<mapsto> x) H\<rbrakk> \<Longrightarrow> \<exists>qs. (list p qs \<and>* list x ps') (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 qs ps' x. \<lbrakk>0 < p; rev ps' @ p # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* p \<mapsto> x) H\<rbrakk> \<Longrightarrow> (list p (p # qs) \<and>* list x ps') (H(p \<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 p q qs ps' x. \<lbrakk>0 < p; rev ps' @ p # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* p \<mapsto> x) H\<rbrakk> \<Longrightarrow> \<exists>xa. (list x ps' \<and>* list xa qs \<and>* p \<mapsto> xa) (H(p \<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 p q qs ps' x. \<lbrakk>0 < p; rev ps' @ p # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* p \<mapsto> x) H\<rbrakk> \<Longrightarrow> (list x ps' \<and>* list (?x59 H p q qs ps' x) qs \<and>* p \<mapsto> ?x59 H p q qs ps' x) (H(p \<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 p q qs ps' x. \<lbrakk>0 < p; rev ps' @ p # qs = rev Ps @ Qs; (list q qs \<and>* list x ps' \<and>* p \<mapsto> x) H\<rbrakk> \<Longrightarrow> (p \<mapsto> - \<and>* list x ps' \<and>* list q qs) 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!