[STATEMENT]
lemma rev_length:
  assumes "effect (rev a i j) h h' r"
  shows "Array.length h a = Array.length h' a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.length h a = Array.length h' a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (Imperative_Reverse.rev a i j) h h' r

goal (1 subgoal):
 1. Array.length h a = Array.length h' a
[PROOF STEP]
proof (induct a i j arbitrary: h h' rule: rev.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a i j h h'. \<lbrakk>\<And>x h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a
[PROOF STEP]
case (1 a i j h h'')
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r

goal (1 subgoal):
 1. \<And>a i j h h'. \<lbrakk>\<And>x h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r

goal (1 subgoal):
 1. Array.length h a = Array.length h'' a
[PROOF STEP]
proof (cases "i < j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
 2. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
 2. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
with 1[unfolded rev.simps[of a i j]]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (if i < j then swap a i j \<bind> (\<lambda>_. Imperative_Reverse.rev a (i + 1) (j - 1)) else return ()) h h'' r
i < j
[PROOF STEP]
obtain h' where
      swp: "effect (swap a i j) h h' ()"
      and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (if i < j then swap a i j \<bind> (\<lambda>_. Imperative_Reverse.rev a (i + 1) (j - 1)) else return ()) h h'' r
i < j

goal (1 subgoal):
 1. (\<And>h'. \<lbrakk>effect (swap a i j) h h' (); effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: effect_elims)
[PROOF STATE]
proof (state)
this:
effect (swap a i j) h h' ()
effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()

goal (2 subgoals):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
 2. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
from swp rev 1 True
[PROOF STATE]
proof (chain)
picking this:
effect (swap a i j) h h' ()
effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r
i < j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
effect (swap a i j) h h' ()
effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r
i < j

goal (1 subgoal):
 1. Array.length h a = Array.length h'' a
[PROOF STEP]
unfolding swap.simps
[PROOF STATE]
proof (prove)
using this:
effect (Array.nth a i \<bind> (\<lambda>x. Array.nth a j \<bind> (\<lambda>y. Array.upd i y a \<bind> (\<lambda>_. Array.upd j x a \<bind> (\<lambda>_. return ()))))) h h' ()
effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r
i < j

goal (1 subgoal):
 1. Array.length h a = Array.length h'' a
[PROOF STEP]
by (elim effect_elims) fastforce
[PROOF STATE]
proof (state)
this:
Array.length h a = Array.length h'' a

goal (1 subgoal):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
with 1[unfolded rev.simps[of a i j]]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (if i < j then swap a i j \<bind> (\<lambda>_. Imperative_Reverse.rev a (i + 1) (j - 1)) else return ()) h h'' r
\<not> i < j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (if i < j then swap a i j \<bind> (\<lambda>_. Imperative_Reverse.rev a (i + 1) (j - 1)) else return ()) h h'' r
\<not> i < j

goal (1 subgoal):
 1. Array.length h a = Array.length h'' a
[PROOF STEP]
by (auto elim: effect_elims)
[PROOF STATE]
proof (state)
this:
Array.length h a = Array.length h'' a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Array.length h a = Array.length h'' a

goal:
No subgoals!
[PROOF STEP]
qed