[STATEMENT]
lemma flatten_prec:
  "precise is_flatten_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise is_flatten_list
[PROOF STEP]
apply (intro preciseI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> is_flatten_list a p * F \<and>\<^sub>A is_flatten_list a' p * F' \<Longrightarrow> a = a'
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
case (1 aa b p F F' lsi' ls' lsi'a ls'a)
[PROOF STATE]
proof (state)
this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'
[PROOF STEP]
have *:
      "\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ls'a lsi'a * G \<and>\<^sub>A list_assn is_inner_list ls' lsi' * G'"
[PROOF STATE]
proof (prove)
using this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'

goal (1 subgoal):
 1. \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ls'a lsi'a * G \<and>\<^sub>A list_assn is_inner_list ls' lsi' * G'
[PROOF STEP]
by (smt (z3) assn_aci(10) assn_times_comm)
[PROOF STATE]
proof (state)
this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ls'a lsi'a * G \<and>\<^sub>A list_assn is_inner_list ls' lsi' * G'

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
have "lsi' = lsi'a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsi' = lsi'a
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'

goal (1 subgoal):
 1. lsi' = lsi'a
[PROOF STEP]
by (metis outer_list.precise preciseD star_assoc)
[PROOF STATE]
proof (state)
this:
lsi' = lsi'a

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lsi' = lsi'a

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
have "length ls'a = length lsi'a" "length ls' = length lsi'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ls'a = length lsi'a &&& length ls' = length lsi'
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'

goal (1 subgoal):
 1. length ls'a = length lsi'a &&& length ls' = length lsi'
[PROOF STEP]
by (auto simp add: mod_and_dist dest!: mod_starD list_assn_len)
[PROOF STATE]
proof (state)
this:
length ls'a = length lsi'a
length ls' = length lsi'

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lsi' = lsi'a
length ls'a = length lsi'a
length ls' = length lsi'
[PROOF STEP]
have "length ls' = length lsi'" "length lsi' = length lsi'a" "length lsi'a = length ls'a"
[PROOF STATE]
proof (prove)
using this:
lsi' = lsi'a
length ls'a = length lsi'a
length ls' = length lsi'

goal (1 subgoal):
 1. length ls' = length lsi' &&& length lsi' = length lsi'a &&& length lsi'a = length ls'a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ls' = length lsi'
length lsi' = length lsi'a
length lsi'a = length ls'a

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length ls' = length lsi'
length lsi' = length lsi'a
length lsi'a = length ls'a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length ls' = length lsi'
length lsi' = length lsi'a
length lsi'a = length ls'a

goal (1 subgoal):
 1. concat ls'a = concat ls'
[PROOF STEP]
using * \<open>lsi' = lsi'a\<close>
[PROOF STATE]
proof (prove)
using this:
length ls' = length lsi'
length lsi' = length lsi'a
length lsi'a = length ls'a
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ls'a lsi'a * G \<and>\<^sub>A list_assn is_inner_list ls' lsi' * G'
lsi' = lsi'a

goal (1 subgoal):
 1. concat ls'a = concat ls'
[PROOF STEP]
proof(induction ls' lsi' lsi'a ls'a arbitrary: p rule: list_induct4)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'; [] = []\<rbrakk> \<Longrightarrow> concat [] = concat []
 2. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'
[] = []

goal (2 subgoals):
 1. \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'; [] = []\<rbrakk> \<Longrightarrow> concat [] = concat []
 2. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'
[] = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'
[] = []

goal (1 subgoal):
 1. concat [] = concat []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
concat [] = concat []

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
case (Cons x xs y ys z zs w ws)
[PROOF STATE]
proof (state)
this:
length xs = length ys
length ys = length zs
length zs = length ws
\<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'
y # ys = z # zs

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
length ys = length zs
length zs = length ws
\<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'
y # ys = z # zs
[PROOF STEP]
have "concat ws = concat xs"
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
length ys = length zs
length zs = length ws
\<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'
y # ys = z # zs

goal (1 subgoal):
 1. concat ws = concat xs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ws; length zs = length ws; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs zs * G' \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> is_inner_list w z * list_assn is_inner_list ws zs * G \<and>\<^sub>A is_inner_list x z * list_assn is_inner_list xs zs * G'; y = z \<and> ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs
[PROOF STEP]
by (metis (no_types, opaque_lifting) ab_semigroup_mult_class.mult.left_commute star_assoc)
[PROOF STATE]
proof (state)
this:
concat ws = concat xs

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
concat ws = concat xs

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
have "x = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = w
[PROOF STEP]
using "Cons.prems" preciseD[OF inner_list.precise, where h="(aa,b)"]
[PROOF STATE]
proof (prove)
using this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'
y # ys = z # zs
(aa, b) \<Turnstile> is_inner_list ?a ?p * ?F \<and>\<^sub>A is_inner_list ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'

goal (1 subgoal):
 1. x = w
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> is_inner_list w z * list_assn is_inner_list ws zs * G \<and>\<^sub>A is_inner_list x z * list_assn is_inner_list xs zs * G'; y = z \<and> ys = zs; \<And>a p F a' F'. (aa, b) \<Turnstile> is_inner_list a p * F \<and>\<^sub>A is_inner_list a' p * F' \<Longrightarrow> a = a'\<rbrakk> \<Longrightarrow> x = w
[PROOF STEP]
using assn_times_assoc
[PROOF STATE]
proof (prove)
using this:
?P * ?Q * ?R = ?P * (?Q * ?R)

goal (1 subgoal):
 1. \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> is_inner_list w z * list_assn is_inner_list ws zs * G \<and>\<^sub>A is_inner_list x z * list_assn is_inner_list xs zs * G'; y = z \<and> ys = zs; \<And>a p F a' F'. (aa, b) \<Turnstile> is_inner_list a p * F \<and>\<^sub>A is_inner_list a' p * F' \<Longrightarrow> a = a'\<rbrakk> \<Longrightarrow> x = w
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = w

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
concat ws = concat xs
x = w
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
concat ws = concat xs
x = w

goal (1 subgoal):
 1. concat (w # ws) = concat (x # xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
concat (w # ws) = concat (x # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
concat ls'a = concat ls'

goal:
No subgoals!
[PROOF STEP]
qed