[STATEMENT]
lemma (in odd_even_clique)
  shows odd_spec: "\<forall>\<sigma>. \<Gamma>\<turnstile>{\<sigma>} \<acute>A :== PROC odd(\<acute>N)
                  \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2 \<rbrace>" (is ?P1)
   and even_spec: "\<forall>\<sigma>. \<Gamma>\<turnstile>{\<sigma>} \<acute>A :== PROC even(\<acute>N)
                  \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2 \<rbrace>" (is ?P2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC odd(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace> &&& \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC even(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC odd(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
 2. \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC even(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
[PROOF STEP]
have "?P1 \<and> ?P2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC odd(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>) \<and> (\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC even(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>)
[PROOF STEP]
apply (hoare_rule ProcRec2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>\<sigma>. \<Gamma>,(\<Union>\<sigma>. {({\<sigma>}, odd_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})}) \<union> (\<Union>\<sigma>. {({\<sigma>}, even_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>A :== 0 ELSE IF \<acute>N = 1 THEN \<acute>A :== CALL even(\<acute>N - 1) ELSE \<acute>A :== CALL odd(\<acute>N - 2) FI FI \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
 2. \<forall>\<sigma>. \<Gamma>,(\<Union>\<sigma>. {({\<sigma>}, odd_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})}) \<union> (\<Union>\<sigma>. {({\<sigma>}, even_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>A :== 1 ELSE IF \<acute>N = 1 THEN \<acute>A :== CALL odd(\<acute>N - 1) ELSE \<acute>A :== CALL even(\<acute>N - 2) FI FI \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
[PROOF STEP]
apply  vcg
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>N. (N = 0 \<longrightarrow> (\<exists>b. N = 2 * b + 0) \<and> 0 < 2) \<and> (N \<noteq> 0 \<longrightarrow> (N = 1 \<longrightarrow> (\<forall>A. (\<exists>b. N - 1 + 1 = 2 * b + A) \<and> A < 2 \<longrightarrow> (\<exists>b. N = 2 * b + A))) \<and> (N \<noteq> 1 \<longrightarrow> (\<forall>A. (\<exists>b. N - 2 = 2 * b + A) \<and> A < 2 \<longrightarrow> (\<exists>b. N = 2 * b + A))))
 2. \<forall>\<sigma>. \<Gamma>,(\<Union>\<sigma>. {({\<sigma>}, odd_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})}) \<union> (\<Union>\<sigma>. {({\<sigma>}, even_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>A :== 1 ELSE IF \<acute>N = 1 THEN \<acute>A :== CALL odd(\<acute>N - 1) ELSE \<acute>A :== CALL even(\<acute>N - 2) FI FI \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
[PROOF STEP]
apply  clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>N A b. \<lbrakk>0 < N; N \<noteq> Suc 0; A < 2; N - 2 = 2 * b + A\<rbrakk> \<Longrightarrow> \<exists>b. N = 2 * b + A
 2. \<forall>\<sigma>. \<Gamma>,(\<Union>\<sigma>. {({\<sigma>}, odd_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})}) \<union> (\<Union>\<sigma>. {({\<sigma>}, even_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>A :== 1 ELSE IF \<acute>N = 1 THEN \<acute>A :== CALL odd(\<acute>N - 1) ELSE \<acute>A :== CALL even(\<acute>N - 2) FI FI \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
[PROOF STEP]
apply  (rule_tac x="b + 1" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>N A b. \<lbrakk>0 < N; N \<noteq> Suc 0; A < 2; N - 2 = 2 * b + A\<rbrakk> \<Longrightarrow> N = 2 * (b + 1) + A
 2. \<forall>\<sigma>. \<Gamma>,(\<Union>\<sigma>. {({\<sigma>}, odd_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})}) \<union> (\<Union>\<sigma>. {({\<sigma>}, even_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>A :== 1 ELSE IF \<acute>N = 1 THEN \<acute>A :== CALL odd(\<acute>N - 1) ELSE \<acute>A :== CALL even(\<acute>N - 2) FI FI \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
[PROOF STEP]
apply  arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,(\<Union>\<sigma>. {({\<sigma>}, odd_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})}) \<union> (\<Union>\<sigma>. {({\<sigma>}, even_'proc, \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>A :== 1 ELSE IF \<acute>N = 1 THEN \<acute>A :== CALL odd(\<acute>N - 1) ELSE \<acute>A :== CALL even(\<acute>N - 2) FI FI \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. (N = 0 \<longrightarrow> (\<exists>b. N + 1 = 2 * b + 1) \<and> 1 < 2) \<and> (N \<noteq> 0 \<longrightarrow> (N = 1 \<longrightarrow> (\<forall>A. (\<exists>b. N - 1 = 2 * b + A) \<and> A < 2 \<longrightarrow> (\<exists>b. N + 1 = 2 * b + A))) \<and> (N \<noteq> 1 \<longrightarrow> (\<forall>A. (\<exists>b. N - 2 + 1 = 2 * b + A) \<and> A < 2 \<longrightarrow> (\<exists>b. N + 1 = 2 * b + A))))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. 0 < N \<Longrightarrow> (N = Suc 0 \<longrightarrow> (\<exists>b. Suc (Suc 0) = 2 * b)) \<and> (N \<noteq> Suc 0 \<longrightarrow> (\<forall>A. (\<exists>b. Suc (N - 2) = 2 * b + A) \<and> A < 2 \<longrightarrow> (\<exists>b. Suc N = 2 * b + A)))
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC odd(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>) \<and> (\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC even(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>)

goal (2 subgoals):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC odd(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
 2. \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC even(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
[PROOF STEP]
thus "?P1" "?P2"
[PROOF STATE]
proof (prove)
using this:
(\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC odd(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>) \<and> (\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC even(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>)

goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC odd(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace> &&& \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC even(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
[PROOF STEP]
by iprover+
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC odd(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>
\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>A :== PROC even(\<acute>N) \<lbrace>(\<exists>b. \<^bsup>\<sigma>\<^esup>N + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in state_space) shows "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
  \<acute>N \<ggreater> n. \<acute>N :== \<acute>N + 1 \<ggreater>
  \<acute>M \<ggreater> m. \<acute>M :== \<acute>M + 1 \<ggreater>
  \<acute>R :== n + m
  \<lbrace>\<acute>R = \<acute>N + \<acute>M - 2\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>N \<ggreater> n. \<acute>N :== \<acute>N + 1\<ggreater> \<acute>M \<ggreater> m. \<acute>M :== \<acute>M + 1\<ggreater> \<acute>R :== n + m \<lbrace>\<acute>R = \<acute>N + \<acute>M - 2\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M N. True \<Longrightarrow> N + M = N + 1 + (M + 1) - 2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Fac_impl) shows
  "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
  CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(\<acute>N) \<ggreater> m.
  \<acute>R :== n + m
  \<lbrace>\<acute>R = fac \<acute>N + fac \<acute>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(\<acute>N) \<ggreater> m. \<acute>R :== n + m \<lbrace>\<acute>R = fac \<acute>N + fac \<acute>N\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(\<acute>N) \<ggreater> m. \<acute>R :== n + m \<lbrace>\<acute>R = fac \<acute>N + fac \<acute>N\<rbrace>
[PROOF STEP]
note Fac_spec = Fac_spec4
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>,?\<Theta>\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(\<acute>N) \<ggreater> m. \<acute>R :== n + m \<lbrace>\<acute>R = fac \<acute>N + fac \<acute>N\<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(\<acute>N) \<ggreater> m. \<acute>R :== n + m \<lbrace>\<acute>R = fac \<acute>N + fac \<acute>N\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(\<acute>N) \<ggreater> m. \<acute>R :== n + m \<lbrace>\<acute>R = fac \<acute>N + fac \<acute>N\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Fac_impl) shows
  "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
  CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(n) \<ggreater> m.
  \<acute>R :== m
  \<lbrace>\<acute>R = fac (fac \<acute>N)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(n) \<ggreater> m. \<acute>R :== m \<lbrace>\<acute>R = fac (fac \<acute>N)\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(n) \<ggreater> m. \<acute>R :== m \<lbrace>\<acute>R = fac (fac \<acute>N)\<rbrace>
[PROOF STEP]
note Fac_spec = Fac_spec4
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>,?\<Theta>\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(n) \<ggreater> m. \<acute>R :== m \<lbrace>\<acute>R = fac (fac \<acute>N)\<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(n) \<ggreater> m. \<acute>R :== m \<lbrace>\<acute>R = fac (fac \<acute>N)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(n) \<ggreater> m. \<acute>R :== m \<lbrace>\<acute>R = fac (fac \<acute>N)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in append_impl) append_spec:
  shows "\<forall>\<sigma> Ps Qs. \<Gamma>\<turnstile>
            \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and>  List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace>
                \<acute>p :== PROC append(\<acute>p,\<acute>q)
            \<lbrace>List \<acute>p \<acute>next (Ps@Qs) \<and> (\<forall>x. x\<notin>set Ps \<longrightarrow> \<acute>next x = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> Ps Qs. \<Gamma>\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace> \<acute>p :== PROC append(\<acute>p,\<acute>q) \<lbrace>List \<acute>p \<acute>next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>
[PROOF STEP]
apply (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> Ps Qs. \<Gamma>,(\<Union>\<sigma> Ps Qs. {(\<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace>, append_'proc, \<lbrace>List \<acute>p \<acute>next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>, {})})\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace> IF \<acute>p = Null THEN \<acute>p :== \<acute>q ELSE \<acute>p\<rightarrow>\<acute>next :== CALL append(\<acute>p\<rightarrow>\<acute>next,\<acute>q) FI \<lbrace>List \<acute>p \<acute>next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ps Qs next p q. \<lbrakk>List p next Ps; List q next Qs; set Ps \<inter> set Qs = {}\<rbrakk> \<Longrightarrow> (p = Null \<longrightarrow> List q next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> next x = next x)) \<and> (p \<noteq> Null \<longrightarrow> (\<exists>Psa. List (next p) next Psa \<and> (\<exists>Qsa. List q next Qsa \<and> set Psa \<inter> set Qsa = {} \<and> (\<forall>nexta pa. List pa nexta (Psa @ Qsa) \<and> (\<forall>x. x \<notin> set Psa \<longrightarrow> nexta x = next x) \<longrightarrow> List p (nexta(p := pa)) (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> (nexta(p := pa)) x = next x)))))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in append_impl) shows "{t. t may_only_modify_globals Z in [next]}
       =
       {t. \<exists>next. globals t=update id id next_' (K_statefun next) (globals Z)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t. t may_only_modify_globals Z in [next]} = {t. \<exists>next. globals t = update id id next_' (K_statefun next) (globals Z)}
[PROOF STEP]
apply (unfold mex_def meq_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t. \<exists>next_'a. globals t = update id id next_' (K_statefun next_'a) (globals Z)} = {t. \<exists>next. globals t = update id id next_' (K_statefun next) (globals Z)}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in append_impl)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>p=Null \<and> \<acute>cont=c\<rbrace> \<acute>p :== CALL append(\<acute>p,Null) \<lbrace>\<acute>cont=c\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>p = Null \<and> \<acute>cont = c\<rbrace> \<acute>p :== CALL append(\<acute>p,Null) \<lbrace>\<acute>cont = c\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cont next p. p = Null \<Longrightarrow> \<exists>Ps. List p next Ps \<and> (\<exists>Qs. List Null next Qs \<and> set Ps \<inter> set Qs = {} \<and> (\<forall>conta nexta p. List p nexta (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> nexta x = next x) \<longrightarrow> conta = cont))
[PROOF STEP]
oops


[STATEMENT]
lemma (in append_impl) append_modifies:
  shows
   "\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC append(\<acute>p,\<acute>q){t. t may_only_modify_globals \<sigma> in [next]}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC append(\<acute>p,\<acute>q) {t. t may_only_modify_globals \<sigma> in [next]}
[PROOF STEP]
apply (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,(\<Union>\<sigma>. {({\<sigma>}, append_'proc, {t. t may_only_modify_globals \<sigma> in [next]}, {})})\<turnstile> {\<sigma>} IF \<acute>p = Null THEN \<acute>p :== \<acute>q ELSE \<acute>p\<rightarrow>\<acute>next :== CALL append(\<acute>p\<rightarrow>\<acute>next,\<acute>q) FI {t. t may_only_modify_globals \<sigma> in [next]}
[PROOF STEP]
apply (vcg spec=modifies)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in append_impl)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>p=Null \<and> \<acute>cont=c\<rbrace> \<acute>p\<rightarrow>\<acute>next :== CALL append(\<acute>p,Null) \<lbrace>\<acute>cont=c\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>p = Null \<and> \<acute>cont = c\<rbrace> \<acute>p\<rightarrow>\<acute>next :== CALL append(\<acute>p,Null) \<lbrace>\<acute>cont = c\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cont next p. p = Null \<Longrightarrow> \<exists>Ps. List p next Ps \<and> (\<exists>Qs. List Null next Qs \<and> set Ps \<inter> set Qs = {} \<and> (\<forall>nexta p. List p nexta (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> nexta x = next x) \<longrightarrow> cont = cont))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in insert_impl) insert_modifies:
  "\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC insert(\<acute>r,\<acute>p){t. t may_only_modify_globals \<sigma> in [next]}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC insert(\<acute>r,\<acute>p) {t. t may_only_modify_globals \<sigma> in [next]}
[PROOF STEP]
apply (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,(\<Union>\<sigma>. {({\<sigma>}, insert_'proc, {t. t may_only_modify_globals \<sigma> in [next]}, {})})\<turnstile> {\<sigma>} IF \<acute>r = Null THEN SKIP ELSE IF \<acute>p = Null THEN \<acute>p :== \<acute>r;; \<acute>p\<rightarrow>\<acute>next :== Null ELSE IF \<acute>r\<rightarrow>\<acute>cont \<le> \<acute>p\<rightarrow>\<acute>cont THEN \<acute>r\<rightarrow>\<acute>next :== \<acute>p;; \<acute>p :== \<acute>r ELSE \<acute>p\<rightarrow>\<acute>next :== CALL insert(\<acute>r,\<acute>p\<rightarrow>\<acute>next) FI FI FI {t. t may_only_modify_globals \<sigma> in [next]}
[PROOF STEP]
apply (vcg spec=modifies)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in insert_impl) insert_spec:
    "\<forall>\<sigma> Ps . \<Gamma>\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and> sorted (\<le>) (map \<acute>cont Ps) \<and>
                  \<acute>r \<noteq> Null \<and> \<acute>r \<notin> set Ps\<rbrace>
         \<acute>p :== PROC insert(\<acute>r,\<acute>p)
   \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont  Qs) \<and>
           set Qs = insert \<^bsup>\<sigma>\<^esup>r (set Ps) \<and>
           (\<forall>x. x \<notin> set Qs \<longrightarrow> \<acute>next x = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> Ps. \<Gamma>\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and> VcgExSP.sorted (\<le>) (map \<acute>cont Ps) \<and> \<acute>r \<noteq> Null \<and> \<acute>r \<notin> set Ps\<rbrace> \<acute>p :== PROC insert(\<acute>r,\<acute>p) \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> VcgExSP.sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont Qs) \<and> set Qs = insert \<^bsup>\<sigma>\<^esup>r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>
[PROOF STEP]
apply (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> Ps. \<Gamma>,(\<Union>\<sigma> Ps. {(\<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and> VcgExSP.sorted (\<le>) (map \<acute>cont Ps) \<and> \<acute>r \<noteq> Null \<and> \<acute>r \<notin> set Ps\<rbrace>, insert_'proc, \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> VcgExSP.sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont Qs) \<and> set Qs = insert \<^bsup>\<sigma>\<^esup>r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>, {})})\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and> VcgExSP.sorted (\<le>) (map \<acute>cont Ps) \<and> \<acute>r \<noteq> Null \<and> \<acute>r \<notin> set Ps\<rbrace> IF \<acute>r = Null THEN SKIP ELSE IF \<acute>p = Null THEN \<acute>p :== \<acute>r;; \<acute>p\<rightarrow>\<acute>next :== Null ELSE IF \<acute>r\<rightarrow>\<acute>cont \<le> \<acute>p\<rightarrow>\<acute>cont THEN \<acute>r\<rightarrow>\<acute>next :== \<acute>p;; \<acute>p :== \<acute>r ELSE \<acute>p\<rightarrow>\<acute>next :== CALL insert(\<acute>r,\<acute>p\<rightarrow>\<acute>next) FI FI FI \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> VcgExSP.sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont Qs) \<and> set Qs = insert \<^bsup>\<sigma>\<^esup>r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps\<rbrakk> \<Longrightarrow> (r = Null \<longrightarrow> (\<exists>Qs. List p next Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> next x = next x))) \<and> (r \<noteq> Null \<longrightarrow> (p = Null \<longrightarrow> (\<exists>Qs. List r (next(r := Null)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (next(r := Null)) x = next x))) \<and> (p \<noteq> Null \<longrightarrow> (cont r \<le> cont p \<longrightarrow> (\<exists>Qs. List r (next(r := p)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (next(r := p)) x = next x))) \<and> (\<not> cont r \<le> cont p \<longrightarrow> (\<exists>Psa. List (next p) next Psa \<and> VcgExSP.sorted (\<le>) (map cont Psa) \<and> r \<noteq> Null \<and> r \<notin> set Psa \<and> (\<forall>nexta pa. (\<exists>Qs. List pa nexta Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Psa) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> nexta x = next x)) \<longrightarrow> (\<exists>Qs. List p (nexta(p := pa)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (nexta(p := pa)) x = next x)))))))
[PROOF STEP]
apply (intro conjI impI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r = Null\<rbrakk> \<Longrightarrow> \<exists>Qs. List p next Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> next x = next x)
 2. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r \<noteq> Null; p = Null\<rbrakk> \<Longrightarrow> \<exists>Qs. List r (next(r := Null)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (next(r := Null)) x = next x)
 3. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r \<noteq> Null; p \<noteq> Null; cont r \<le> cont p\<rbrakk> \<Longrightarrow> \<exists>Qs. List r (next(r := p)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (next(r := p)) x = next x)
 4. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r \<noteq> Null; p \<noteq> Null; \<not> cont r \<le> cont p\<rbrakk> \<Longrightarrow> \<exists>Psa. List (next p) next Psa \<and> VcgExSP.sorted (\<le>) (map cont Psa) \<and> r \<noteq> Null \<and> r \<notin> set Psa \<and> (\<forall>nexta pa. (\<exists>Qs. List pa nexta Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Psa) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> nexta x = next x)) \<longrightarrow> (\<exists>Qs. List p (nexta(p := pa)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (nexta(p := pa)) x = next x)))
[PROOF STEP]
apply    fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r \<noteq> Null; p = Null\<rbrakk> \<Longrightarrow> \<exists>Qs. List r (next(r := Null)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (next(r := Null)) x = next x)
 2. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r \<noteq> Null; p \<noteq> Null; cont r \<le> cont p\<rbrakk> \<Longrightarrow> \<exists>Qs. List r (next(r := p)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (next(r := p)) x = next x)
 3. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r \<noteq> Null; p \<noteq> Null; \<not> cont r \<le> cont p\<rbrakk> \<Longrightarrow> \<exists>Psa. List (next p) next Psa \<and> VcgExSP.sorted (\<le>) (map cont Psa) \<and> r \<noteq> Null \<and> r \<notin> set Psa \<and> (\<forall>nexta pa. (\<exists>Qs. List pa nexta Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Psa) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> nexta x = next x)) \<longrightarrow> (\<exists>Qs. List p (nexta(p := pa)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (nexta(p := pa)) x = next x)))
[PROOF STEP]
apply   fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r \<noteq> Null; p \<noteq> Null; cont r \<le> cont p\<rbrakk> \<Longrightarrow> \<exists>Qs. List r (next(r := p)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (next(r := p)) x = next x)
 2. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r \<noteq> Null; p \<noteq> Null; \<not> cont r \<le> cont p\<rbrakk> \<Longrightarrow> \<exists>Psa. List (next p) next Psa \<and> VcgExSP.sorted (\<le>) (map cont Psa) \<and> r \<noteq> Null \<and> r \<notin> set Psa \<and> (\<forall>nexta pa. (\<exists>Qs. List pa nexta Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Psa) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> nexta x = next x)) \<longrightarrow> (\<exists>Qs. List p (nexta(p := pa)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (nexta(p := pa)) x = next x)))
[PROOF STEP]
apply  fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ps cont next p r. \<lbrakk>List p next Ps; VcgExSP.sorted (\<le>) (map cont Ps); r \<noteq> Null; r \<notin> set Ps; r \<noteq> Null; p \<noteq> Null; \<not> cont r \<le> cont p\<rbrakk> \<Longrightarrow> \<exists>Psa. List (next p) next Psa \<and> VcgExSP.sorted (\<le>) (map cont Psa) \<and> r \<noteq> Null \<and> r \<notin> set Psa \<and> (\<forall>nexta pa. (\<exists>Qs. List pa nexta Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Psa) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> nexta x = next x)) \<longrightarrow> (\<exists>Qs. List p (nexta(p := pa)) Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (set Ps) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> (nexta(p := pa)) x = next x)))
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cont next p r ps nexta pa Qs. \<lbrakk>r \<noteq> Null; p \<noteq> Null; \<not> cont r \<le> cont p; List (next p) next ps; \<forall>x\<in>set ps. cont p \<le> cont x; VcgExSP.sorted (\<le>) (map cont ps); r \<noteq> p; r \<notin> set ps; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert r (set ps); \<forall>x. x \<noteq> r \<and> x \<notin> set ps \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> \<exists>Qs. (\<exists>ps. Qs = p # ps \<and> List pa (nexta(p := pa)) ps) \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = insert r (insert p (set ps)) \<and> (\<forall>x. (x = p \<longrightarrow> p \<notin> set Qs \<longrightarrow> pa = next p) \<and> (x \<noteq> p \<longrightarrow> x \<notin> set Qs \<longrightarrow> nexta x = next x))
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in insertSort_impl) insertSort_modifies:
  shows
   "\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC insertSort(\<acute>p)
              {t. t may_only_modify_globals \<sigma> in [next]}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC insertSort(\<acute>p) {t. t may_only_modify_globals \<sigma> in [next]}
[PROOF STEP]
apply (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,(\<Union>\<sigma>. {({\<sigma>}, insertSort_'proc, {t. t may_only_modify_globals \<sigma> in [next]}, {})})\<turnstile> {\<sigma>} \<acute>r :== Null;; WHILE \<acute>p \<noteq> Null DO \<acute>q :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>r :== CALL insert(\<acute>q,\<acute>r) OD;; \<acute>p :== \<acute>r {t. t may_only_modify_globals \<sigma> in [next]}
[PROOF STEP]
apply (vcg spec=modifies)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in insertSort_impl) insertSort_body_spec:
  shows "\<forall>\<sigma> Ps. \<Gamma>,\<Theta>\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<rbrace>
              \<acute>p :== PROC insertSort(\<acute>p)
          \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont Qs) \<and>
           set Qs = set Ps\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> Ps. \<Gamma>,\<Theta>\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps\<rbrace> \<acute>p :== PROC insertSort(\<acute>p) \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> VcgExSP.sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont Qs) \<and> set Qs = set Ps\<rbrace>
[PROOF STEP]
apply (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> Ps. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma> Ps. {(\<lbrace>\<sigma>. List \<acute>p \<acute>next Ps\<rbrace>, insertSort_'proc, \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> VcgExSP.sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont Qs) \<and> set Qs = set Ps\<rbrace>, {})})\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps\<rbrace> \<acute>r :== Null;; WHILE \<acute>p \<noteq> Null DO \<acute>q :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>r :== CALL insert(\<acute>q,\<acute>r) OD;; \<acute>p :== \<acute>r \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> VcgExSP.sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont Qs) \<and> set Qs = set Ps\<rbrace>
[PROOF STEP]
apply (hoare_rule anno=
         "\<acute>r :== Null;;
         WHILE \<acute>p \<noteq> Null
         INV \<lbrace>\<exists>Qs Rs. List \<acute>p \<acute>next Qs \<and> List \<acute>r \<acute>next Rs \<and>
                  set Qs \<inter> set Rs = {} \<and>
                  sorted (\<le>) (map \<acute>cont Rs) \<and> set Qs \<union> set Rs = set Ps \<and>
                  \<acute>cont = \<^bsup>\<sigma>\<^esup>cont \<rbrace>
          DO \<acute>q :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>r :== CALL insert(\<acute>q,\<acute>r) OD;;
          \<acute>p :== \<acute>r" in HoarePartial.annotateI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> Ps. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma> Ps. {(\<lbrace>\<sigma>. List \<acute>p \<acute>next Ps\<rbrace>, insertSort_'proc, \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> VcgExSP.sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont Qs) \<and> set Qs = set Ps\<rbrace>, {})})\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps\<rbrace> \<acute>r :== Null;; WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>Qs Rs. List \<acute>p \<acute>next Qs \<and> List \<acute>r \<acute>next Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map \<acute>cont Rs) \<and> set Qs \<union> set Rs = set Ps \<and> \<acute>cont = \<^bsup>\<sigma>\<^esup>cont\<rbrace> DO \<acute>q :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>r :== CALL insert(\<acute>q,\<acute>r) OD;; \<acute>p :== \<acute>r \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> VcgExSP.sorted (\<le>) (map \<^bsup>\<sigma>\<^esup>cont Qs) \<and> set Qs = set Ps\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Ps cont next p. List p next Ps \<Longrightarrow> \<exists>Qs Rs. List p next Qs \<and> List Null next Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map cont Rs) \<and> set Qs \<union> set Rs = set Ps \<and> cont = cont
 2. \<And>cont Ps conta next p r. \<lbrakk>\<exists>Qs Rs. List p next Qs \<and> List r next Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont; p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>Psa. List r next Psa \<and> VcgExSP.sorted (\<le>) (map conta Psa) \<and> p \<noteq> Null \<and> p \<notin> set Psa \<and> (\<forall>nexta pa. (\<exists>Qs. List pa nexta Qs \<and> VcgExSP.sorted (\<le>) (map conta Qs) \<and> set Qs = insert p (set Psa) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> nexta x = next x)) \<longrightarrow> (\<exists>Qs. List (next p) nexta Qs \<and> (\<exists>Rs. List pa nexta Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont)))
 3. \<And>cont Ps conta next p r. \<lbrakk>\<exists>Qs Rs. List p next Qs \<and> List r next Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont; \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>Qs. List r next Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = set Ps
[PROOF STEP]
apply   fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>cont Ps conta next p r. \<lbrakk>\<exists>Qs Rs. List p next Qs \<and> List r next Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont; p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>Psa. List r next Psa \<and> VcgExSP.sorted (\<le>) (map conta Psa) \<and> p \<noteq> Null \<and> p \<notin> set Psa \<and> (\<forall>nexta pa. (\<exists>Qs. List pa nexta Qs \<and> VcgExSP.sorted (\<le>) (map conta Qs) \<and> set Qs = insert p (set Psa) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> nexta x = next x)) \<longrightarrow> (\<exists>Qs. List (next p) nexta Qs \<and> (\<exists>Rs. List pa nexta Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont)))
 2. \<And>cont Ps conta next p r. \<lbrakk>\<exists>Qs Rs. List p next Qs \<and> List r next Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont; \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>Qs. List r next Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = set Ps
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>cont Ps conta next p r. \<lbrakk>\<exists>Qs Rs. List p next Qs \<and> List r next Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont; \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>Qs. List r next Qs \<and> VcgExSP.sorted (\<le>) (map cont Qs) \<and> set Qs = set Ps
 2. \<And>cont Ps conta next p r. \<lbrakk>\<exists>Qs Rs. List p next Qs \<and> List r next Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont; p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>Psa. List r next Psa \<and> VcgExSP.sorted (\<le>) (map conta Psa) \<and> p \<noteq> Null \<and> p \<notin> set Psa \<and> (\<forall>nexta pa. (\<exists>Qs. List pa nexta Qs \<and> VcgExSP.sorted (\<le>) (map conta Qs) \<and> set Qs = insert p (set Psa) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> nexta x = next x)) \<longrightarrow> (\<exists>Qs. List (next p) nexta Qs \<and> (\<exists>Rs. List pa nexta Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont)))
[PROOF STEP]
apply  fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cont Ps conta next p r. \<lbrakk>\<exists>Qs Rs. List p next Qs \<and> List r next Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont; p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>Psa. List r next Psa \<and> VcgExSP.sorted (\<le>) (map conta Psa) \<and> p \<noteq> Null \<and> p \<notin> set Psa \<and> (\<forall>nexta pa. (\<exists>Qs. List pa nexta Qs \<and> VcgExSP.sorted (\<le>) (map conta Qs) \<and> set Qs = insert p (set Psa) \<and> (\<forall>x. x \<notin> set Qs \<longrightarrow> nexta x = next x)) \<longrightarrow> (\<exists>Qs. List (next p) nexta Qs \<and> (\<exists>Rs. List pa nexta Rs \<and> set Qs \<inter> set Rs = {} \<and> VcgExSP.sorted (\<le>) (map conta Rs) \<and> set Qs \<union> set Rs = set Ps \<and> conta = cont)))
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> \<exists>Qs. List (next p) nexta Qs \<and> p \<notin> set Qs \<and> set Qs \<inter> set Rs = {} \<and> insert p (set Qs \<union> set Rs) = set Ps
[PROOF STEP]
apply (rule_tac x=ps in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> List (next p) nexta ps \<and> p \<notin> set ps \<and> set ps \<inter> set Rs = {} \<and> insert p (set ps \<union> set Rs) = set Ps
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> List (next p) nexta ps
 2. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> p \<notin> set ps
 3. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> set ps \<inter> set Rs = {}
 4. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> insert p (set ps \<union> set Rs) = set Ps
[PROOF STEP]
apply    (rule heap_eq_ListI1)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> List (next p) (?h161 cont Ps next p r ps Rs nexta pa Qs) ps
 2. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ps. nexta x = ?h161 cont Ps next p r ps Rs nexta pa Qs x
 3. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> p \<notin> set ps
 4. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> set ps \<inter> set Rs = {}
 5. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> insert p (set ps \<union> set Rs) = set Ps
[PROOF STEP]
apply     assumption
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ps. nexta x = next x
 2. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> p \<notin> set ps
 3. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> set ps \<inter> set Rs = {}
 4. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> insert p (set ps \<union> set Rs) = set Ps
[PROOF STEP]
apply    clarsimp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>cont Ps next p r ps Rs nexta pa Qs x. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x; x \<in> set ps\<rbrakk> \<Longrightarrow> nexta x = next x
 2. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> p \<notin> set ps
 3. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> set ps \<inter> set Rs = {}
 4. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> insert p (set ps \<union> set Rs) = set Ps
[PROOF STEP]
apply    (subgoal_tac "x\<noteq>p \<and> x \<notin> set Rs")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>cont Ps next p r ps Rs nexta pa Qs x. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x; x \<in> set ps; x \<noteq> p \<and> x \<notin> set Rs\<rbrakk> \<Longrightarrow> nexta x = next x
 2. \<And>cont Ps next p r ps Rs nexta pa Qs x. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x; x \<in> set ps\<rbrakk> \<Longrightarrow> x \<noteq> p \<and> x \<notin> set Rs
 3. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> p \<notin> set ps
 4. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> set ps \<inter> set Rs = {}
 5. \<And>cont Ps next p r ps Rs nexta pa Qs. \<lbrakk>p \<noteq> Null; List (next p) next ps; List r next Rs; VcgExSP.sorted (\<le>) (map cont Rs); insert p (set ps \<union> set Rs) = set Ps; p \<notin> set Rs; set ps \<inter> set Rs = {}; List pa nexta Qs; VcgExSP.sorted (\<le>) (map cont Qs); set Qs = insert p (set Rs); \<forall>x. x \<noteq> p \<and> x \<notin> set Rs \<longrightarrow> nexta x = next x\<rbrakk> \<Longrightarrow> insert p (set ps \<union> set Rs) = set Ps
[PROOF STEP]
apply     auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in list_alloc)
 shows
  "\<Gamma>,\<Theta>\<turnstile> \<lbrace>\<acute>i = 0 \<and> \<acute>first = Null \<and> n*sz \<le> \<acute>free\<rbrace>
       WHILE \<acute>i < n
       INV \<lbrace>\<exists>Ps. List \<acute>first \<acute>next Ps \<and> length Ps = \<acute>i \<and> \<acute>i \<le> n \<and>
             set Ps \<subseteq> set \<acute>alloc \<and> (n - \<acute>i)*sz \<le> \<acute>free\<rbrace>
       DO
         \<acute>p :== NEW sz [\<acute>cont:==0,\<acute>next:== Null];;
         \<acute>p\<rightarrow>\<acute>next :== \<acute>first;;
         \<acute>first :== \<acute>p;;
         \<acute>i :== \<acute>i+ 1
       OD
       \<lbrace>\<exists>Ps. List \<acute>first \<acute>next  Ps \<and> length Ps = n \<and> set Ps \<subseteq> set \<acute>alloc\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>\<acute>i = 0 \<and> \<acute>first = Null \<and> n * sz \<le> \<acute>free\<rbrace> WHILE \<acute>i < n INV \<lbrace>\<exists>Ps. List \<acute>first \<acute>next Ps \<and> length Ps = \<acute>i \<and> \<acute>i \<le> n \<and> set Ps \<subseteq> set \<acute>alloc \<and> (n - \<acute>i) * sz \<le> \<acute>free\<rbrace> DO \<acute>p :== NEW sz [\<acute>cont :== 0, \<acute>next :== Null];; \<acute>p\<rightarrow>\<acute>next :== \<acute>first;; \<acute>first :== \<acute>p;; \<acute>i :== \<acute>i + 1 OD \<lbrace>\<exists>Ps. List \<acute>first \<acute>next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set \<acute>alloc\<rbrace>
[PROOF STEP]
apply (vcg)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first i. \<lbrakk>i = 0; first = Null; n * sz \<le> free\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free
 2. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; i < n\<rbrakk> \<Longrightarrow> (sz \<le> free \<longrightarrow> (\<exists>Ps. List (new (set alloc)) (next(new (set alloc) := Null, new (set alloc) := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set (new (set alloc) # alloc) \<and> (n - (i + 1)) * sz \<le> free - sz)) \<and> (\<not> sz \<le> free \<longrightarrow> (\<exists>Ps. List Null (next(Null := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - (i + 1)) * sz \<le> free))
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; i < n\<rbrakk> \<Longrightarrow> (sz \<le> free \<longrightarrow> (\<exists>Ps. List (new (set alloc)) (next(new (set alloc) := Null, new (set alloc) := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set (new (set alloc) # alloc) \<and> (n - (i + 1)) * sz \<le> free - sz)) \<and> (\<not> sz \<le> free \<longrightarrow> (\<exists>Ps. List Null (next(Null := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - (i + 1)) * sz \<le> free))
 2. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply  clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> (sz \<le> free \<longrightarrow> (\<exists>Psa. (\<exists>ps. Psa = new (set alloc) # ps \<and> List first (next(new (set alloc) := first)) ps) \<and> length Psa = Suc (length Ps) \<and> set Psa \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz)) \<and> sz \<le> free
 2. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply  (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free \<longrightarrow> (\<exists>Psa. (\<exists>ps. Psa = new (set alloc) # ps \<and> List first (next(new (set alloc) := first)) ps) \<and> length Psa = Suc (length Ps) \<and> set Psa \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz)
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> \<exists>Psa. (\<exists>ps. Psa = new (set alloc) # ps \<and> List first (next(new (set alloc) := first)) ps) \<and> length Psa = Suc (length Ps) \<and> set Psa \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   (rule_tac x="new (set alloc)#Ps" in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> (\<exists>ps. new (set alloc) # Ps = new (set alloc) # ps \<and> List first (next(new (set alloc) := first)) ps) \<and> length (new (set alloc) # Ps) = Suc (length Ps) \<and> set (new (set alloc) # Ps) \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> set Ps \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   (rule conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> set Ps \<subseteq> insert (new (set alloc)) (set alloc)
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> (n - Suc (length Ps)) * sz \<le> free - sz
 3. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 4. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply    fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> (n - Suc (length Ps)) * sz \<le> free - sz
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   (simp add: sz_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 2. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply  (simp add: sz_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in list_alloc)
 shows
  "\<Gamma>\<turnstile> \<lbrace>\<acute>i = 0 \<and> \<acute>first = Null \<and> n*sz \<le> \<acute>free\<rbrace>
       WHILE \<acute>i < n
       INV \<lbrace>\<exists>Ps. List \<acute>first \<acute>next Ps \<and> length Ps = \<acute>i \<and> \<acute>i \<le> n \<and>
             set Ps \<subseteq> set \<acute>alloc \<and> (n - \<acute>i)*sz \<le> \<acute>free\<rbrace>
       DO
         \<acute>p :== NNEW sz [\<acute>cont:==0,\<acute>next:== Null];;
         \<acute>p\<rightarrow>\<acute>next :== \<acute>first;;
         \<acute>first :== \<acute>p;;
         \<acute>i :== \<acute>i+ 1
       OD
       \<lbrace>\<exists>Ps. List \<acute>first \<acute>next  Ps \<and> length Ps = n \<and> set Ps \<subseteq> set \<acute>alloc\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>i = 0 \<and> \<acute>first = Null \<and> n * sz \<le> \<acute>free\<rbrace> WHILE \<acute>i < n INV \<lbrace>\<exists>Ps. List \<acute>first \<acute>next Ps \<and> length Ps = \<acute>i \<and> \<acute>i \<le> n \<and> set Ps \<subseteq> set \<acute>alloc \<and> (n - \<acute>i) * sz \<le> \<acute>free\<rbrace> DO \<acute>p :== NNEW sz [\<acute>cont :== 0, \<acute>next :== Null];; \<acute>p\<rightarrow>\<acute>next :== \<acute>first;; \<acute>first :== \<acute>p;; \<acute>i :== \<acute>i + 1 OD \<lbrace>\<exists>Ps. List \<acute>first \<acute>next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set \<acute>alloc\<rbrace>
[PROOF STEP]
apply (vcg)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first i. \<lbrakk>i = 0; first = Null; n * sz \<le> free\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free
 2. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; i < n\<rbrakk> \<Longrightarrow> (sz \<le> free \<longrightarrow> (\<exists>Ps. List (new (set alloc)) (next(new (set alloc) := Null, new (set alloc) := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set (new (set alloc) # alloc) \<and> (n - (i + 1)) * sz \<le> free - sz)) \<and> (\<not> sz \<le> free \<longrightarrow> (\<exists>Ps. List Null (next(Null := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - (i + 1)) * sz \<le> free) \<and> (\<exists>Ps. List (new (set alloc)) (next(new (set alloc) := Null, new (set alloc) := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set (new (set alloc) # alloc) \<and> (n - (i + 1)) * sz \<le> free - sz))
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; i < n\<rbrakk> \<Longrightarrow> (sz \<le> free \<longrightarrow> (\<exists>Ps. List (new (set alloc)) (next(new (set alloc) := Null, new (set alloc) := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set (new (set alloc) # alloc) \<and> (n - (i + 1)) * sz \<le> free - sz)) \<and> (\<not> sz \<le> free \<longrightarrow> (\<exists>Ps. List Null (next(Null := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - (i + 1)) * sz \<le> free) \<and> (\<exists>Ps. List (new (set alloc)) (next(new (set alloc) := Null, new (set alloc) := first)) Ps \<and> length Ps = i + 1 \<and> i + 1 \<le> n \<and> set Ps \<subseteq> set (new (set alloc) # alloc) \<and> (n - (i + 1)) * sz \<le> free - sz))
 2. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply  clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> (sz \<le> free \<longrightarrow> (\<exists>Psa. (\<exists>ps. Psa = new (set alloc) # ps \<and> List first (next(new (set alloc) := first)) ps) \<and> length Psa = Suc (length Ps) \<and> set Psa \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz)) \<and> sz \<le> free
 2. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply  (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free \<longrightarrow> (\<exists>Psa. (\<exists>ps. Psa = new (set alloc) # ps \<and> List first (next(new (set alloc) := first)) ps) \<and> length Psa = Suc (length Ps) \<and> set Psa \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz)
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> \<exists>Psa. (\<exists>ps. Psa = new (set alloc) # ps \<and> List first (next(new (set alloc) := first)) ps) \<and> length Psa = Suc (length Ps) \<and> set Psa \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   (rule_tac x="new (set alloc)#Ps" in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> (\<exists>ps. new (set alloc) # Ps = new (set alloc) # ps \<and> List first (next(new (set alloc) := first)) ps) \<and> length (new (set alloc) # Ps) = Suc (length Ps) \<and> set (new (set alloc) # Ps) \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> set Ps \<subseteq> insert (new (set alloc)) (set alloc) \<and> (n - Suc (length Ps)) * sz \<le> free - sz
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   (rule conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> set Ps \<subseteq> insert (new (set alloc)) (set alloc)
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> (n - Suc (length Ps)) * sz \<le> free - sz
 3. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 4. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply    fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free; sz \<le> free\<rbrakk> \<Longrightarrow> (n - Suc (length Ps)) * sz \<le> free - sz
 2. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 3. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply   (simp add: sz_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>alloc free next first Ps. \<lbrakk>length Ps < n; List first next Ps; set Ps \<subseteq> set alloc; (n - length Ps) * sz \<le> free\<rbrakk> \<Longrightarrow> sz \<le> free
 2. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply  (simp add: sz_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>alloc free next first i. \<lbrakk>\<exists>Ps. List first next Ps \<and> length Ps = i \<and> i \<le> n \<and> set Ps \<subseteq> set alloc \<and> (n - i) * sz \<le> free; \<not> i < n\<rbrakk> \<Longrightarrow> \<exists>Ps. List first next Ps \<and> length Ps = n \<and> set Ps \<subseteq> set alloc
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in list_alloc) "\<Gamma>,\<Theta>\<turnstile> \<lbrace>True\<rbrace>  \<lbrace>\<acute>p\<noteq>Null\<rbrace>\<longmapsto> \<acute>p\<rightarrow>\<acute>next :== \<acute>p \<lbrace>True\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>True\<rbrace> (False, \<lbrace>\<acute>p \<noteq> Null\<rbrace>)\<longmapsto> \<acute>p\<rightarrow>\<acute>next :== \<acute>p \<lbrace>True\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. True \<Longrightarrow> p \<noteq> Null
[PROOF STEP]
oops


[STATEMENT]
lemma (in list_alloc) "\<Gamma>,\<Theta>\<turnstile> {}  \<lbrace>\<acute>p\<noteq>Null\<rbrace>\<longmapsto> \<acute>p\<rightarrow>\<acute>next :== \<acute>p \<lbrace>True\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> {} (False, \<lbrace>\<acute>p \<noteq> Null\<rbrace>)\<longmapsto> \<acute>p\<rightarrow>\<acute>next :== \<acute>p \<lbrace>True\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in list_alloc)
  shows
  "\<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
       set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
  WHILE \<acute>p \<noteq> Null
  INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next  ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and>
               rev ps @ qs = rev Ps @ Qs \<and>
               set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace>
  DO \<acute>r :== \<acute>p;;
     \<acute>p :== \<acute>p\<rightarrow> \<acute>next;;
     \<acute>r\<rightarrow>\<acute>next :== \<acute>q;;
     \<acute>q :== \<acute>r OD
  \<lbrace>List \<acute>q \<acute>next (rev Ps @ Qs) \<and> set Ps\<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace> WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD \<lbrace>List \<acute>q \<acute>next (rev Ps @ Qs) \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
[PROOF STEP]
apply (vcg)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc next p q. \<lbrakk>List p next Ps; List q next Qs; set Ps \<inter> set Qs = {}; set Ps \<subseteq> set alloc; set Qs \<subseteq> set alloc\<rbrakk> \<Longrightarrow> \<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc
 2. \<And>alloc next p q. \<lbrakk>\<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc; p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. List (next p) (next(p := q)) ps \<and> List p (next(p := q)) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc
 3. \<And>alloc next p q. \<lbrakk>\<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc; \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> List q next (rev Ps @ Qs) \<and> set Ps \<subseteq> set alloc \<and> set Qs \<subseteq> set alloc
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in list_alloc)
  shows
  "\<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
       set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
  WHILE \<acute>p \<noteq> Null
  INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next  ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and>
               rev ps @ qs = rev Ps @ Qs \<and>
               set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace>
  DO \<acute>r :== \<acute>p;;
     \<lbrace>\<acute>p\<noteq>Null \<and> \<acute>p\<in>set \<acute>alloc\<rbrace>\<longmapsto> \<acute>p :== \<acute>p\<rightarrow> \<acute>next;;
     \<lbrace>\<acute>r\<noteq>Null \<and> \<acute>r\<in>set \<acute>alloc\<rbrace>\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;;
     \<acute>q :== \<acute>r OD
 \<lbrace>List \<acute>q \<acute>next (rev Ps @ Qs) \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace> WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (False, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (False, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD \<lbrace>List \<acute>q \<acute>next (rev Ps @ Qs) \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
[PROOF STEP]
apply (vcg)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc next p q. \<lbrakk>List p next Ps; List q next Qs; set Ps \<inter> set Qs = {}; set Ps \<subseteq> set alloc; set Qs \<subseteq> set alloc\<rbrakk> \<Longrightarrow> \<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc
 2. \<And>alloc next p q. \<lbrakk>\<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc; p \<noteq> Null\<rbrakk> \<Longrightarrow> p \<noteq> Null \<and> p \<in> set alloc \<and> p \<noteq> Null \<and> p \<in> set alloc \<and> (\<exists>ps qs. List (next p) (next(p := q)) ps \<and> List p (next(p := q)) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc)
 3. \<And>alloc next p q. \<lbrakk>\<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc; \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> List q next (rev Ps @ Qs) \<and> set Ps \<subseteq> set alloc \<and> set Qs \<subseteq> set alloc
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in list_alloc) rev_noFault:
  shows
  "\<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
       set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
  WHILE \<acute>p \<noteq> Null
  INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next  ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and>
               rev ps @ qs = rev Ps @ Qs \<and>
               set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace>
  DO \<acute>r :== \<acute>p;;
     \<lbrace>\<acute>p\<noteq>Null \<and> \<acute>p\<in>set \<acute>alloc\<rbrace>\<longmapsto> \<acute>p :== \<acute>p\<rightarrow> \<acute>next;;
     \<lbrace>\<acute>r\<noteq>Null \<and> \<acute>r\<in>set \<acute>alloc\<rbrace>\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;;
     \<acute>q :== \<acute>r OD
  UNIV,UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace> WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (False, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (False, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD UNIV,UNIV
[PROOF STEP]
apply (vcg)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc next p q. \<lbrakk>List p next Ps; List q next Qs; set Ps \<inter> set Qs = {}; set Ps \<subseteq> set alloc; set Qs \<subseteq> set alloc\<rbrakk> \<Longrightarrow> \<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc
 2. \<And>alloc next p q. \<lbrakk>\<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc; p \<noteq> Null\<rbrakk> \<Longrightarrow> p \<noteq> Null \<and> p \<in> set alloc \<and> p \<noteq> Null \<and> p \<in> set alloc \<and> (\<exists>ps qs. List (next p) (next(p := q)) ps \<and> List p (next(p := q)) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc)
 3. \<lbrace>(\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc) \<and> \<not> \<acute>p \<noteq> Null\<rbrace> \<subseteq> UNIV
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in list_alloc) rev_moduloGuards:

  shows
  "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{True}\<^esub> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
       set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
  WHILE \<acute>p \<noteq> Null
  INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next  ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and>
               rev ps @ qs = rev Ps @ Qs \<and>
               set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace>
  DO \<acute>r :== \<acute>p;;
     \<lbrace>\<acute>p\<noteq>Null \<and> \<acute>p\<in>set \<acute>alloc\<rbrace>\<surd> \<longmapsto> \<acute>p :== \<acute>p\<rightarrow> \<acute>next;;
     \<lbrace>\<acute>r\<noteq>Null \<and> \<acute>r\<in>set \<acute>alloc\<rbrace>\<surd> \<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;;
     \<acute>q :== \<acute>r OD
 \<lbrace>List \<acute>q \<acute>next (rev Ps @ Qs) \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/{True}\<^esub> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace> WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (True, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (True, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD \<lbrace>List \<acute>q \<acute>next (rev Ps @ Qs) \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>alloc next p q. \<lbrakk>List p next Ps; List q next Qs; set Ps \<inter> set Qs = {}; set Ps \<subseteq> set alloc; set Qs \<subseteq> set alloc\<rbrakk> \<Longrightarrow> \<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc
 2. \<And>alloc next p q. \<lbrakk>\<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc; p \<noteq> Null\<rbrakk> \<Longrightarrow> p \<noteq> Null \<and> p \<in> set alloc \<longrightarrow> p \<noteq> Null \<and> p \<in> set alloc \<longrightarrow> (\<exists>ps qs. List (next p) (next(p := q)) ps \<and> List p (next(p := q)) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc)
 3. \<And>alloc next p q. \<lbrakk>\<exists>ps qs. List p next ps \<and> List q next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set alloc \<and> set qs \<subseteq> set alloc; \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> List q next (rev Ps @ Qs) \<and> set Ps \<subseteq> set alloc \<and> set Qs \<subseteq> set alloc
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma CombineStrip':
  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c' Q,A"
  assumes deriv_strip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c'' UNIV,UNIV"
  assumes c'': "c''= mark_guards False (strip_guards (-F) c')"
  assumes c: "c = mark_guards False c'"
  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> P c Q,A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> P c Q,A
[PROOF STEP]
from deriv_strip [simplified c'']
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>,\<Theta>\<turnstile> P mark_guards False (strip_guards (- F) c') UNIV,UNIV
[PROOF STEP]
have "\<Gamma>,\<Theta>\<turnstile> P (strip_guards (- F) c') UNIV,UNIV"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>,\<Theta>\<turnstile> P mark_guards False (strip_guards (- F) c') UNIV,UNIV

goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> P strip_guards (- F) c' UNIV,UNIV
[PROOF STEP]
by (rule HoarePartialProps.MarkGuardsD)
[PROOF STATE]
proof (state)
this:
\<Gamma>,\<Theta>\<turnstile> P strip_guards (- F) c' UNIV,UNIV

goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> P c Q,A
[PROOF STEP]
with deriv
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P c' Q,A
\<Gamma>,\<Theta>\<turnstile> P strip_guards (- F) c' UNIV,UNIV
[PROOF STEP]
have "\<Gamma>,\<Theta>\<turnstile> P c' Q,A"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P c' Q,A
\<Gamma>,\<Theta>\<turnstile> P strip_guards (- F) c' UNIV,UNIV

goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> P c' Q,A
[PROOF STEP]
by (rule HoarePartialProps.CombineStrip)
[PROOF STATE]
proof (state)
this:
\<Gamma>,\<Theta>\<turnstile> P c' Q,A

goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> P c Q,A
[PROOF STEP]
hence "\<Gamma>,\<Theta>\<turnstile> P mark_guards False c' Q,A"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>,\<Theta>\<turnstile> P c' Q,A

goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> P mark_guards False c' Q,A
[PROOF STEP]
by (rule HoarePartialProps.MarkGuardsI)
[PROOF STATE]
proof (state)
this:
\<Gamma>,\<Theta>\<turnstile> P mark_guards False c' Q,A

goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> P c Q,A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>,\<Theta>\<turnstile> P mark_guards False c' Q,A

goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> P c Q,A
[PROOF STEP]
by (simp add: c)
[PROOF STATE]
proof (state)
this:
\<Gamma>,\<Theta>\<turnstile> P c Q,A

goal:
No subgoals!
[PROOF STEP]
qed