[STATEMENT]
lemma circular_list_rev_II:
 "\<Gamma>\<turnstile>
 \<lbrace>\<acute>p = r \<and> distPath \<acute>p \<acute>next \<acute>p (r#Ps)\<rbrace>
\<acute>q:==Null;;
WHILE \<acute>p \<noteq> Null
INV
 \<lbrace> ((\<acute>q = Null) \<longrightarrow> (\<exists>ps. distPath \<acute>p \<acute>next r ps  \<and>  ps = r#Ps)) \<and>
  ((\<acute>q \<noteq> Null) \<longrightarrow> (\<exists>ps qs. distPath \<acute>q \<acute>next r qs  \<and> List \<acute>p \<acute>next ps  \<and>
                   set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps@[r])) \<and>
  \<not> (\<acute>p = Null \<and> \<acute>q = Null \<and> r = Null )
   \<rbrace>
DO
  \<acute>tmp :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q:==\<acute>tmp
OD
 \<lbrace>\<acute>q = r \<and> distPath \<acute>q \<acute>next \<acute>q (r # rev Ps)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>p = r \<and> distPath \<acute>p \<acute>next \<acute>p (r # Ps)\<rbrace> \<acute>q :== Null;; WHILE \<acute>p \<noteq> Null INV \<lbrace>(\<acute>q = Null \<longrightarrow> (\<exists>ps. distPath \<acute>p \<acute>next r ps \<and> ps = r # Ps)) \<and> (\<acute>q \<noteq> Null \<longrightarrow> (\<exists>ps qs. distPath \<acute>q \<acute>next r qs \<and> List \<acute>p \<acute>next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (\<acute>p = Null \<and> \<acute>q = Null \<and> r = Null)\<rbrace> DO \<acute>tmp :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>tmp OD \<lbrace>\<acute>q = r \<and> distPath \<acute>q \<acute>next \<acute>q (r # rev Ps)\<rbrace>
[PROOF STEP]
apply (simp only:distPath_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>p = r \<and> Path \<acute>p \<acute>next \<acute>p (r # Ps) \<and> distinct (r # Ps)\<rbrace> \<acute>q :== Null;; WHILE \<acute>p \<noteq> Null INV \<lbrace>(\<acute>q = Null \<longrightarrow> (\<exists>ps. (Path \<acute>p \<acute>next r ps \<and> distinct ps) \<and> ps = r # Ps)) \<and> (\<acute>q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (Path \<acute>q \<acute>next r qs \<and> distinct qs) \<and> List \<acute>p \<acute>next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (\<acute>p = Null \<and> \<acute>q = Null \<and> r = Null)\<rbrace> DO \<acute>tmp :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>tmp OD \<lbrace>\<acute>q = r \<and> Path \<acute>q \<acute>next \<acute>q (r # rev Ps) \<and> distinct (r # rev Ps)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>next p. \<lbrakk>Path p next p (p # Ps); distinct (p # Ps)\<rbrakk> \<Longrightarrow> (Null = Null \<longrightarrow> (\<exists>ps. Path p next p ps \<and> distinct ps \<and> ps = p # Ps)) \<and> (Null \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path Null next p qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [p])) \<and> \<not> (p = Null \<and> Null = Null \<and> p = Null)
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); p \<noteq> Null\<rbrakk> \<Longrightarrow> (p = Null \<longrightarrow> (\<exists>ps. Path (next p) (next(p := q)) r ps \<and> distinct ps \<and> ps = r # Ps)) \<and> (p \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path p (next(p := q)) r qs \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (next p = Null \<and> p = Null \<and> r = Null)
 3. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply   clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); p \<noteq> Null\<rbrakk> \<Longrightarrow> (p = Null \<longrightarrow> (\<exists>ps. Path (next p) (next(p := q)) r ps \<and> distinct ps \<and> ps = r # Ps)) \<and> (p \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path p (next(p := q)) r qs \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (next p = Null \<and> p = Null \<and> r = Null)
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (case_tac "(q = Null)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null; q = Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null; q \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 3. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply   (fastforce intro: path_is_list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null; q \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs psa. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; p \<noteq> Null; q \<noteq> Null; qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps); distinct qs; set (p # psa) \<inter> set qs = {}; rev qs @ p # psa = Ps @ [r]; List (next p) next psa\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (rule_tac x="psa" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs psa. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; p \<noteq> Null; q \<noteq> Null; qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps); distinct qs; set (p # psa) \<inter> set qs = {}; rev qs @ p # psa = Ps @ [r]; List (next p) next psa\<rbrakk> \<Longrightarrow> \<exists>qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) psa \<and> set psa \<inter> set qs = {} \<and> rev qs @ psa = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (rule_tac x=" p # qs" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs psa. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; p \<noteq> Null; q \<noteq> Null; qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps); distinct qs; set (p # psa) \<inter> set qs = {}; rev qs @ p # psa = Ps @ [r]; List (next p) next psa\<rbrakk> \<Longrightarrow> (p # qs = [] \<and> r = p \<or> (\<exists>ps. p # qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct (p # qs) \<and> List (next p) (next(p := q)) psa \<and> set psa \<inter> set (p # qs) = {} \<and> rev (p # qs) @ psa = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done