[STATEMENT]
lemma step_lem[rule_format]:  "l \<noteq> [] \<Longrightarrow>
       tl (map (\<lambda> i. f((x1 # a # l) ! i)((a # l) ! i)) [0..<length l]) =
       map (\<lambda>i. f((a # l) ! i)(l ! i)) [0..<length l - (1)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> tl (map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l]) = map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - 1]
[PROOF STEP]
proof (simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> tl (map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l]) = map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - Suc 0]
[PROOF STEP]
assume l: "l \<noteq> []"
[PROOF STATE]
proof (state)
this:
l \<noteq> []

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> tl (map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l]) = map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - Suc 0]
[PROOF STEP]
have a: "map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] =
                 (f(x1)(a) # (map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<(length l - 1)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f x1 a # map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - 1]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f x1 a # map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - 1]
[PROOF STEP]
have b : "map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] =
                     f ((x1 # a # l) ! 0) ((a # l) ! 0) #
                     (map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [1..<length l])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f ((x1 # a # l) ! 0) ((a # l) ! 0) # map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [1..<length l]
[PROOF STEP]
by (rule map_fst, simp, rule l)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f ((x1 # a # l) ! 0) ((a # l) ! 0) # map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [1..<length l]

goal (1 subgoal):
 1. map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f x1 a # map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - 1]
[PROOF STEP]
have c: "map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [Suc (0)..<length l] =
                map (\<lambda>i. f ((x1 # a # l) ! Suc i) ((a # l) ! Suc i)) [(0)..<(length l - 1)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [Suc 0..<length l] = map (\<lambda>i. f ((x1 # a # l) ! Suc i) ((a # l) ! Suc i)) [0..<length l - 1]
[PROOF STEP]
by (subgoal_tac "[Suc (0)..<length l] = map Suc [0..<(length l - 1)]",
             simp, simp add: map_Suc_upt l)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [Suc 0..<length l] = map (\<lambda>i. f ((x1 # a # l) ! Suc i) ((a # l) ! Suc i)) [0..<length l - 1]

goal (1 subgoal):
 1. map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f x1 a # map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - 1]
[PROOF STEP]
thus "map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] =
             f x1 a # map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - (1)]"
[PROOF STATE]
proof (prove)
using this:
map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [Suc 0..<length l] = map (\<lambda>i. f ((x1 # a # l) ! Suc i) ((a # l) ! Suc i)) [0..<length l - 1]

goal (1 subgoal):
 1. map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f x1 a # map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - 1]
[PROOF STEP]
by (simp add: b c)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f x1 a # map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - 1]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f x1 a # map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - 1]

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> tl (map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l]) = map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - Suc 0]
[PROOF STEP]
thus "l \<noteq> [] \<Longrightarrow>
    tl (map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l]) =
    map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - Suc (0)]"
[PROOF STATE]
proof (prove)
using this:
map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] = f x1 a # map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - 1]

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> tl (map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l]) = map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - Suc 0]
[PROOF STEP]
by (subst a, simp)
[PROOF STATE]
proof (state)
this:
l \<noteq> [] \<Longrightarrow> tl (map (\<lambda>i. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l]) = map (\<lambda>i. f ((a # l) ! i) (l ! i)) [0..<length l - Suc 0]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_lem2a[rule_format]: "0 < length list \<Longrightarrow> map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>)
        [0..<length list] @
       [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] =
       aa # listb \<longrightarrow> \<N>\<^bsub>((x1, a))\<^esub> = aa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length list \<Longrightarrow> map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] = aa # listb \<longrightarrow> \<N>\<^bsub>(x1, a)\<^esub> = aa
[PROOF STEP]
by (subst map_fst, assumption, simp)


[STATEMENT]
lemma step_lem2b[rule_format]: "0 = length list \<Longrightarrow> map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>)
        [0..<length list] @
       [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] =
       aa # listb \<longrightarrow> \<N>\<^bsub>((x1, a))\<^esub> = aa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = length list \<Longrightarrow> map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] = aa # listb \<longrightarrow> \<N>\<^bsub>(x1, a)\<^esub> = aa
[PROOF STEP]
by simp


[STATEMENT]
lemma step_lem2: "map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>)
        [0..<length list] @
       [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] =
       aa # listb \<Longrightarrow> \<N>\<^bsub>((x1, a))\<^esub> = aa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] = aa # listb \<Longrightarrow> \<N>\<^bsub>(x1, a)\<^esub> = aa
[PROOF STEP]
proof (case_tac "length list", rule step_lem2b, erule sym, assumption)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] = aa # listb; length list = Suc nat\<rbrakk> \<Longrightarrow> \<N>\<^bsub>(x1, a)\<^esub> = aa
[PROOF STEP]
show "\<And>nat.
       map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>) [0..<length list] @
       [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] =
       aa # listb \<Longrightarrow>
       length list = Suc nat \<Longrightarrow> \<N>\<^bsub>(x1, a)\<^esub> = aa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] = aa # listb; length list = Suc nat\<rbrakk> \<Longrightarrow> \<N>\<^bsub>(x1, a)\<^esub> = aa
[PROOF STEP]
by (rule_tac list = list in step_lem2a, simp)
[PROOF STATE]
proof (state)
this:
\<lbrakk>map (\<lambda>i. \<N>\<^bsub>((x1 # a # list) ! i, (a # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((x1 # a # list) ! length list, (a # list) ! length list)\<^esub>] = aa # listb; length list = Suc ?nat\<rbrakk> \<Longrightarrow> \<N>\<^bsub>(x1, a)\<^esub> = aa

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma base_list_and[rule_format]: "Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow>
         (\<forall> li.  Sji ! (0) = li \<longrightarrow>
        Sji! (length (Sji) - 1) = s \<longrightarrow>
       (\<forall>i<length (Sji) - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow>
       \<turnstile> (map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>)
          [0..<length (Sji) - Suc (0)] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow> (\<forall>li. Sji ! 0 = li \<longrightarrow> Sji ! (length Sji - 1) = s \<longrightarrow> (\<forall>i<length Sji - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) [0..<length Sji - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
[PROOF STEP]
proof (induction Sji)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [] \<noteq> [] \<longrightarrow> tl [] \<noteq> [] \<longrightarrow> (\<forall>li. [] ! 0 = li \<longrightarrow> [] ! (length [] - 1) = s \<longrightarrow> (\<forall>i<length [] - 1. \<turnstile>\<N>\<^bsub>([] ! i, [] ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>([] ! i, [] ! Suc i)\<^esub>) [0..<length [] - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
 2. \<And>a Sji. Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow> (\<forall>li. Sji ! 0 = li \<longrightarrow> Sji ! (length Sji - 1) = s \<longrightarrow> (\<forall>i<length Sji - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) [0..<length Sji - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>) \<Longrightarrow> a # Sji \<noteq> [] \<longrightarrow> tl (a # Sji) \<noteq> [] \<longrightarrow> (\<forall>li. (a # Sji) ! 0 = li \<longrightarrow> (a # Sji) ! (length (a # Sji) - 1) = s \<longrightarrow> (\<forall>i<length (a # Sji) - 1. \<turnstile>\<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) [0..<length (a # Sji) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [] \<noteq> [] \<longrightarrow> tl [] \<noteq> [] \<longrightarrow> (\<forall>li. [] ! 0 = li \<longrightarrow> [] ! (length [] - 1) = s \<longrightarrow> (\<forall>i<length [] - 1. \<turnstile>\<N>\<^bsub>([] ! i, [] ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>([] ! i, [] ! Suc i)\<^esub>) [0..<length [] - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
 2. \<And>a Sji. Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow> (\<forall>li. Sji ! 0 = li \<longrightarrow> Sji ! (length Sji - 1) = s \<longrightarrow> (\<forall>i<length Sji - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) [0..<length Sji - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>) \<Longrightarrow> a # Sji \<noteq> [] \<longrightarrow> tl (a # Sji) \<noteq> [] \<longrightarrow> (\<forall>li. (a # Sji) ! 0 = li \<longrightarrow> (a # Sji) ! (length (a # Sji) - 1) = s \<longrightarrow> (\<forall>i<length (a # Sji) - 1. \<turnstile>\<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) [0..<length (a # Sji) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<noteq> [] \<longrightarrow> tl [] \<noteq> [] \<longrightarrow> (\<forall>li. [] ! 0 = li \<longrightarrow> [] ! (length [] - 1) = s \<longrightarrow> (\<forall>i<length [] - 1. \<turnstile>\<N>\<^bsub>([] ! i, [] ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>([] ! i, [] ! Suc i)\<^esub>) [0..<length [] - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] \<noteq> [] \<longrightarrow> tl [] \<noteq> [] \<longrightarrow> (\<forall>li. [] ! 0 = li \<longrightarrow> [] ! (length [] - 1) = s \<longrightarrow> (\<forall>i<length [] - 1. \<turnstile>\<N>\<^bsub>([] ! i, [] ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>([] ! i, [] ! Suc i)\<^esub>) [0..<length [] - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)

goal (1 subgoal):
 1. \<And>a Sji. Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow> (\<forall>li. Sji ! 0 = li \<longrightarrow> Sji ! (length Sji - 1) = s \<longrightarrow> (\<forall>i<length Sji - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) [0..<length Sji - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>) \<Longrightarrow> a # Sji \<noteq> [] \<longrightarrow> tl (a # Sji) \<noteq> [] \<longrightarrow> (\<forall>li. (a # Sji) ! 0 = li \<longrightarrow> (a # Sji) ! (length (a # Sji) - 1) = s \<longrightarrow> (\<forall>i<length (a # Sji) - 1. \<turnstile>\<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) [0..<length (a # Sji) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Sji. Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow> (\<forall>li. Sji ! 0 = li \<longrightarrow> Sji ! (length Sji - 1) = s \<longrightarrow> (\<forall>i<length Sji - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) [0..<length Sji - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>) \<Longrightarrow> a # Sji \<noteq> [] \<longrightarrow> tl (a # Sji) \<noteq> [] \<longrightarrow> (\<forall>li. (a # Sji) ! 0 = li \<longrightarrow> (a # Sji) ! (length (a # Sji) - 1) = s \<longrightarrow> (\<forall>i<length (a # Sji) - 1. \<turnstile>\<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) [0..<length (a # Sji) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
[PROOF STEP]
case (Cons a Sji)
[PROOF STATE]
proof (state)
this:
Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow> (\<forall>li. Sji ! 0 = li \<longrightarrow> Sji ! (length Sji - 1) = s \<longrightarrow> (\<forall>i<length Sji - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) [0..<length Sji - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)

goal (1 subgoal):
 1. \<And>a Sji. Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow> (\<forall>li. Sji ! 0 = li \<longrightarrow> Sji ! (length Sji - 1) = s \<longrightarrow> (\<forall>i<length Sji - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) [0..<length Sji - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>) \<Longrightarrow> a # Sji \<noteq> [] \<longrightarrow> tl (a # Sji) \<noteq> [] \<longrightarrow> (\<forall>li. (a # Sji) ! 0 = li \<longrightarrow> (a # Sji) ! (length (a # Sji) - 1) = s \<longrightarrow> (\<forall>i<length (a # Sji) - 1. \<turnstile>\<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) [0..<length (a # Sji) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow> (\<forall>li. Sji ! 0 = li \<longrightarrow> Sji ! (length Sji - 1) = s \<longrightarrow> (\<forall>i<length Sji - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) [0..<length Sji - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Sji \<noteq> [] \<longrightarrow> tl Sji \<noteq> [] \<longrightarrow> (\<forall>li. Sji ! 0 = li \<longrightarrow> Sji ! (length Sji - 1) = s \<longrightarrow> (\<forall>i<length Sji - 1. \<turnstile>\<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>(Sji ! i, Sji ! Suc i)\<^esub>) [0..<length Sji - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)

goal (1 subgoal):
 1. a # Sji \<noteq> [] \<longrightarrow> tl (a # Sji) \<noteq> [] \<longrightarrow> (\<forall>li. (a # Sji) ! 0 = li \<longrightarrow> (a # Sji) ! (length (a # Sji) - 1) = s \<longrightarrow> (\<forall>i<length (a # Sji) - 1. \<turnstile>\<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) [0..<length (a # Sji) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)
[PROOF STEP]
apply (subst att_and, case_tac Sji, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>list \<noteq> [] \<longrightarrow> list ! (length list - Suc 0) = s \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, s)\<^esup>; Sji = aa # list\<rbrakk> \<Longrightarrow> (aa # list) ! length list = s \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) \<longrightarrow> (case map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, s)\<^esub>] of [] \<Rightarrow> fst (a, s) \<subseteq> snd (a, s) | [aa] \<Rightarrow> \<turnstile>aa \<and> attack aa = (a, s) | aa # ab # list \<Rightarrow> \<turnstile>aa \<and> fst (attack aa) = fst (a, s) \<and> \<turnstile>ab # list \<oplus>\<^sub>\<and>\<^bsup>(snd (attack aa), snd (a, s))\<^esup>)
[PROOF STEP]
apply (rule impI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>list \<noteq> [] \<longrightarrow> list ! (length list - Suc 0) = s \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, s)\<^esup>; Sji = aa # list; (aa # list) ! length list = s; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>\<rbrakk> \<Longrightarrow> case map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, s)\<^esub>] of [] \<Rightarrow> fst (a, s) \<subseteq> snd (a, s) | [aa] \<Rightarrow> \<turnstile>aa \<and> attack aa = (a, s) | aa # ab # list \<Rightarrow> \<turnstile>aa \<and> fst (attack aa) = fst (a, s) \<and> \<turnstile>ab # list \<oplus>\<^sub>\<and>\<^bsup>(snd (attack aa), snd (a, s))\<^esup>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>list \<noteq> [] \<longrightarrow> list ! (length list - Suc 0) = s \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, s)\<^esup>; Sji = aa # list; (aa # list) ! length list = s; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>\<rbrakk> \<Longrightarrow> case map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, s)\<^esub>] of [] \<Rightarrow> fst (a, s) \<subseteq> snd (a, s) | [aa] \<Rightarrow> \<turnstile>aa \<and> attack aa = (a, s) | aa # ab # list \<Rightarrow> \<turnstile>aa \<and> fst (attack aa) = fst (a, s) \<and> \<turnstile>ab # list \<oplus>\<^sub>\<and>\<^bsup>(snd (attack aa), snd (a, s))\<^esup>
[PROOF STEP]
fix aa list
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>list \<noteq> [] \<longrightarrow> list ! (length list - Suc 0) = s \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, s)\<^esup>; Sji = aa # list; (aa # list) ! length list = s; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>\<rbrakk> \<Longrightarrow> case map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, s)\<^esub>] of [] \<Rightarrow> fst (a, s) \<subseteq> snd (a, s) | [aa] \<Rightarrow> \<turnstile>aa \<and> attack aa = (a, s) | aa # ab # list \<Rightarrow> \<turnstile>aa \<and> fst (attack aa) = fst (a, s) \<and> \<turnstile>ab # list \<oplus>\<^sub>\<and>\<^bsup>(snd (attack aa), snd (a, s))\<^esup>
[PROOF STEP]
show "list \<noteq> [] \<longrightarrow>
       list ! (length list - Suc 0) = s \<longrightarrow>
       (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow>
       \<turnstile>(map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, s)\<^esup>) \<Longrightarrow>
       Sji = aa # list \<Longrightarrow>
       (aa # list) ! length list = s \<Longrightarrow>
       \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub> \<Longrightarrow>
       case map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @
            [\<N>\<^bsub>((a # aa # list) ! length list, s)\<^esub>] of
       [] \<Rightarrow> fst (a, s) \<subseteq> snd (a, s) | [aa] \<Rightarrow> \<turnstile>aa \<and> attack aa = (a, s)
       | aa # ab # list \<Rightarrow>
           \<turnstile>aa \<and> fst (attack aa) = fst (a, s) \<and> \<turnstile>(ab # list \<oplus>\<^sub>\<and>\<^bsup>(snd (attack aa), snd (a, s))\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list \<noteq> [] \<longrightarrow> list ! (length list - Suc 0) = s \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, s)\<^esup>; Sji = aa # list; (aa # list) ! length list = s; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>\<rbrakk> \<Longrightarrow> case map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, s)\<^esub>] of [] \<Rightarrow> fst (a, s) \<subseteq> snd (a, s) | [aa] \<Rightarrow> \<turnstile>aa \<and> attack aa = (a, s) | aa # ab # list \<Rightarrow> \<turnstile>aa \<and> fst (attack aa) = fst (a, s) \<and> \<turnstile>ab # list \<oplus>\<^sub>\<and>\<^bsup>(snd (attack aa), snd (a, s))\<^esup>
[PROOF STEP]
proof (case_tac "map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @
            [\<N>\<^bsub>((a # aa # list) ! length list, s)\<^esub>]", simp, clarify, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ab lista. \<lbrakk>list \<noteq> [] \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # lista; s = (aa # list) ! length list\<rbrakk> \<Longrightarrow> case lista of [] \<Rightarrow> \<turnstile>ab \<and> attack ab = (a, (aa # list) ! length list) | aba # lista \<Rightarrow> \<turnstile>ab \<and> fst (attack ab) = a \<and> \<turnstile>aba # lista \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>
[PROOF STEP]
fix ab lista
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ab lista. \<lbrakk>list \<noteq> [] \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # lista; s = (aa # list) ! length list\<rbrakk> \<Longrightarrow> case lista of [] \<Rightarrow> \<turnstile>ab \<and> attack ab = (a, (aa # list) ! length list) | aba # lista \<Rightarrow> \<turnstile>ab \<and> fst (attack ab) = a \<and> \<turnstile>aba # lista \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>
[PROOF STEP]
have *: "tl (map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list])
                    =  (map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, (list) ! i)\<^esub>) [0..<(length list - 1)])"
        if "list \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list]) = map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list - 1]
[PROOF STEP]
apply (subgoal_tac "tl (map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list])
                    =  (map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, (list) ! i)\<^esub>) [0..<(length list - 1)])")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. tl (map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list]) = map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list - 1] \<Longrightarrow> tl (map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list]) = map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list - 1]
 2. tl (map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list]) = map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list - 1]
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list]) = map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list - 1]
[PROOF STEP]
apply (subst step_lem [OF that])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list - 1] = map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list - 1]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
list \<noteq> [] \<Longrightarrow> tl (map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list]) = map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list - 1]

goal (1 subgoal):
 1. \<And>ab lista. \<lbrakk>list \<noteq> [] \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # lista; s = (aa # list) ! length list\<rbrakk> \<Longrightarrow> case lista of [] \<Rightarrow> \<turnstile>ab \<and> attack ab = (a, (aa # list) ! length list) | aba # lista \<Rightarrow> \<turnstile>ab \<and> fst (attack ab) = a \<and> \<turnstile>aba # lista \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>
[PROOF STEP]
show "list \<noteq> [] \<longrightarrow>
       (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow>
       \<turnstile>(map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>)
          [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>) \<Longrightarrow>
       Sji = aa # list \<Longrightarrow>
       \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub> \<Longrightarrow>
       map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @
       [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] =
       ab # lista \<Longrightarrow>
       s = (aa # list) ! length list \<Longrightarrow>
       case lista of [] \<Rightarrow> \<turnstile>ab \<and> attack ab = (a, (aa # list) ! length list)
       | aba # lista \<Rightarrow>
           \<turnstile>ab \<and> fst (attack ab) = a \<and> \<turnstile>(aba # lista \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list \<noteq> [] \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # lista; s = (aa # list) ! length list\<rbrakk> \<Longrightarrow> case lista of [] \<Rightarrow> \<turnstile>ab \<and> attack ab = (a, (aa # list) ! length list) | aba # lista \<Rightarrow> \<turnstile>ab \<and> fst (attack ab) = a \<and> \<turnstile>aba # lista \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>
[PROOF STEP]
apply (auto simp: split: list.split)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22\<rbrakk> \<Longrightarrow> \<turnstile>ab
 2. \<And>x21 x22 x. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22; x \<in> fst (attack ab)\<rbrakk> \<Longrightarrow> x \<in> a
 3. \<And>x21 x22 x. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22; x \<in> a\<rbrakk> \<Longrightarrow> x \<in> fst (attack ab)
 4. \<And>x21 x22. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22\<rbrakk> \<Longrightarrow> \<turnstile>x21 # x22 \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>
[PROOF STEP]
apply (metis (no_types, lifting) app_tl_hd_list length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 self_append_conv2 upt_0 zero_less_Suc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22; x \<in> fst (attack ab)\<rbrakk> \<Longrightarrow> x \<in> a
 2. \<And>x21 x22 x. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22; x \<in> a\<rbrakk> \<Longrightarrow> x \<in> fst (attack ab)
 3. \<And>x21 x22. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22\<rbrakk> \<Longrightarrow> \<turnstile>x21 # x22 \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>
[PROOF STEP]
apply (metis (no_types, lifting) app_tl_hd_list attack.simps(1) fst_conv length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 self_append_conv2 upt_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22; x \<in> a\<rbrakk> \<Longrightarrow> x \<in> fst (attack ab)
 2. \<And>x21 x22. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22\<rbrakk> \<Longrightarrow> \<turnstile>x21 # x22 \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>
[PROOF STEP]
apply (metis (mono_tags, lifting) app_tl_hd_list attack.simps(1) fst_conv length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 self_append_conv2 upt_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # x21 # x22; s = (aa # list) ! length list; \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; lista = x21 # x22\<rbrakk> \<Longrightarrow> \<turnstile>x21 # x22 \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>
[PROOF STEP]
by (smt * One_nat_def app_tl_hd_list attack.simps(1) length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 nth_Cons_pos self_append_conv2 snd_conv tl_app_in tl_append2 upt_0)
[PROOF STATE]
proof (state)
this:
\<lbrakk>list \<noteq> [] \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, list ! (length list - Suc 0))\<^esup>; Sji = aa # list; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>; map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, (aa # list) ! length list)\<^esub>] = ab # lista; s = (aa # list) ! length list\<rbrakk> \<Longrightarrow> case lista of [] \<Rightarrow> \<turnstile>ab \<and> attack ab = (a, (aa # list) ! length list) | aba # lista \<Rightarrow> \<turnstile>ab \<and> fst (attack ab) = a \<and> \<turnstile>aba # lista \<oplus>\<^sub>\<and>\<^bsup>(snd (attack ab), (aa # list) ! length list)\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>list \<noteq> [] \<longrightarrow> list ! (length list - Suc 0) = s \<longrightarrow> (\<forall>i<length list. \<turnstile>\<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((aa # list) ! i, list ! i)\<^esub>) [0..<length list] \<oplus>\<^sub>\<and>\<^bsup>(aa, s)\<^esup>; Sji = aa # list; (aa # list) ! length list = s; \<forall>i<Suc (length list). \<turnstile>\<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>\<rbrakk> \<Longrightarrow> case map (\<lambda>i. \<N>\<^bsub>((a # aa # list) ! i, (aa # list) ! i)\<^esub>) [0..<length list] @ [\<N>\<^bsub>((a # aa # list) ! length list, s)\<^esub>] of [] \<Rightarrow> fst (a, s) \<subseteq> snd (a, s) | [aa] \<Rightarrow> \<turnstile>aa \<and> attack aa = (a, s) | aa # ab # list \<Rightarrow> \<turnstile>aa \<and> fst (attack aa) = fst (a, s) \<and> \<turnstile>ab # list \<oplus>\<^sub>\<and>\<^bsup>(snd (attack aa), snd (a, s))\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a # Sji \<noteq> [] \<longrightarrow> tl (a # Sji) \<noteq> [] \<longrightarrow> (\<forall>li. (a # Sji) ! 0 = li \<longrightarrow> (a # Sji) ! (length (a # Sji) - 1) = s \<longrightarrow> (\<forall>i<length (a # Sji) - 1. \<turnstile>\<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) \<longrightarrow> \<turnstile>map (\<lambda>i. \<N>\<^bsub>((a # Sji) ! i, (a # Sji) ! Suc i)\<^esub>) [0..<length (a # Sji) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>(li, s)\<^esup>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Compl_step4: "I \<noteq> {} \<Longrightarrow> finite I \<Longrightarrow> \<not> I \<subseteq> s \<Longrightarrow>
(\<exists> lI. set lI = {x. x \<in> I \<and> x \<notin> s} \<and> (\<exists> Sj :: ((('s :: state) set)list) list.
               length Sj = length lI \<and> nodup_all lI \<and>
            (\<forall> j < length Sj. (((Sj ! j)  \<noteq> []) \<and> (tl (Sj ! j) \<noteq> []) \<and>
                 ((Sj ! j) ! 0, (Sj ! j) ! (length (Sj ! j) - 1)) = ({lI ! j},s) \<and>
                 (\<forall> i < (length (Sj ! j) - 1).  \<turnstile> \<N>\<^bsub>((Sj ! j) ! i, (Sj ! j) ! (i+1) )\<^esub>
                         )))))
 \<Longrightarrow>  \<exists> (A :: ('s :: state) attree).  \<turnstile> A \<and> attack A = (I,s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; \<not> I \<subseteq> s; \<exists>lI. set lI = {x \<in> I. x \<notin> s} \<and> (\<exists>Sj. length Sj = length lI \<and> nodup_all lI \<and> (\<forall>j<length Sj. Sj ! j \<noteq> [] \<and> tl (Sj ! j) \<noteq> [] \<and> (Sj ! j ! 0, Sj ! j ! (length (Sj ! j) - 1)) = ({lI ! j}, s) \<and> (\<forall>i<length (Sj ! j) - 1. \<turnstile>\<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>)))\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
proof (erule exE, erule conjE, erule exE, erule conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>lI Sj. \<lbrakk>I \<noteq> {}; finite I; \<not> I \<subseteq> s; set lI = {x \<in> I. x \<notin> s}; length Sj = length lI; nodup_all lI \<and> (\<forall>j<length Sj. Sj ! j \<noteq> [] \<and> tl (Sj ! j) \<noteq> [] \<and> (Sj ! j ! 0, Sj ! j ! (length (Sj ! j) - 1)) = ({lI ! j}, s) \<and> (\<forall>i<length (Sj ! j) - 1. \<turnstile>\<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>))\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
fix lI Sj
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>lI Sj. \<lbrakk>I \<noteq> {}; finite I; \<not> I \<subseteq> s; set lI = {x \<in> I. x \<notin> s}; length Sj = length lI; nodup_all lI \<and> (\<forall>j<length Sj. Sj ! j \<noteq> [] \<and> tl (Sj ! j) \<noteq> [] \<and> (Sj ! j ! 0, Sj ! j ! (length (Sj ! j) - 1)) = ({lI ! j}, s) \<and> (\<forall>i<length (Sj ! j) - 1. \<turnstile>\<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>))\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
assume  a: "I \<noteq> {}" and b: "finite I" and c: "\<not> I \<subseteq> s"
    and d: "set lI = {x::'s \<in> I. x \<notin> s}" and e: "length Sj = length lI"
    and f: "nodup_all lI \<and>
              (\<forall>j<length Sj. Sj ! j \<noteq> [] \<and>
                             tl (Sj ! j) \<noteq> [] \<and>
           (Sj ! j ! (0), Sj ! j ! (length (Sj ! j) - (1))) = ({lI ! j}, s) \<and>
           (\<forall>i<length (Sj ! j) - (1). \<turnstile>\<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + (1)))\<^esub>))"
[PROOF STATE]
proof (state)
this:
I \<noteq> {}
finite I
\<not> I \<subseteq> s
set lI = {x \<in> I. x \<notin> s}
length Sj = length lI
nodup_all lI \<and> (\<forall>j<length Sj. Sj ! j \<noteq> [] \<and> tl (Sj ! j) \<noteq> [] \<and> (Sj ! j ! 0, Sj ! j ! (length (Sj ! j) - 1)) = ({lI ! j}, s) \<and> (\<forall>i<length (Sj ! j) - 1. \<turnstile>\<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>))

goal (1 subgoal):
 1. \<And>lI Sj. \<lbrakk>I \<noteq> {}; finite I; \<not> I \<subseteq> s; set lI = {x \<in> I. x \<notin> s}; length Sj = length lI; nodup_all lI \<and> (\<forall>j<length Sj. Sj ! j \<noteq> [] \<and> tl (Sj ! j) \<noteq> [] \<and> (Sj ! j ! 0, Sj ! j ! (length (Sj ! j) - 1)) = ({lI ! j}, s) \<and> (\<forall>i<length (Sj ! j) - 1. \<turnstile>\<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>))\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
show    "\<exists>A::'s attree. \<turnstile>A \<and> attack A = (I, s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
apply (rule_tac x =
        "[([] \<oplus>\<^sub>\<or>\<^bsup>({x. x \<in> I \<and> x \<in> s}, s)\<^esup>),
    ([[ \<N>\<^bsub>((Sj ! j) ! i, (Sj ! j) ! (i + (1)))\<^esub>.
      i \<leftarrow> [0..<(length (Sj ! j)-(1))]] \<oplus>\<^sub>\<and>\<^bsup>(({lI ! j},s))\<^esup>. j \<leftarrow> [0..<(length Sj)]]
     \<oplus>\<^sub>\<or>\<^bsup>({x. x \<in> I \<and> x \<notin> s},s)\<^esup>)] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup> \<and> attack ([[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>) = (I, s)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<turnstile>[[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>
 2. attack ([[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>) = (I, s)
[PROOF STEP]
show  "\<turnstile>([[] \<oplus>\<^sub>\<or>\<^bsup>({x::'s \<in> I. x \<in> s}, s)\<^esup>,
       map (\<lambda>j.
               ((map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + (1)))\<^esub>)
                [0..<length (Sj ! j) - (1)]) \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>))
       [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x::'s \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile>[[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>
[PROOF STEP]
have g: "I - {x::'s \<in> I. x \<in> s} = {x::'s \<in> I. x \<notin> s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s}

goal (1 subgoal):
 1. \<turnstile>[[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>
[PROOF STEP]
thus "\<turnstile>([[] \<oplus>\<^sub>\<or>\<^bsup>({x::'s \<in> I. x \<in> s}, s)\<^esup>,
       (map (\<lambda>j.
               ((map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + (1)))\<^esub>)
                [0..<length (Sj ! j) - (1)]) \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>))
       [0..<length Sj]) \<oplus>\<^sub>\<or>\<^bsup>({x::'s \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>)"
[PROOF STATE]
proof (prove)
using this:
I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s}

goal (1 subgoal):
 1. \<turnstile>[[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>
[PROOF STEP]
apply (subst att_or, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup> \<and> \<turnstile>[map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>
 2. I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>
[PROOF STEP]
show "I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>([] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>
[PROOF STEP]
by (metis (no_types, lifting) CollectD att_or_empty_back subsetI)
[PROOF STATE]
proof (state)
this:
I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>

goal (1 subgoal):
 1. I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>
[PROOF STEP]
show "I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow>
    \<turnstile>([map (\<lambda>j. ((map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0]) \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>))
        [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>
[PROOF STEP]
text \<open>Use lemma @{text \<open>list_or_upt\<close>} to distribute attack validity  over list lI\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>
[PROOF STEP]
proof (erule ssubst, subst att_or, simp, rule subst, rule d, rule_tac lI = lI in list_or_upt)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. lI \<noteq> []
 2. length (map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj]) = length lI
 3. nodup_all lI
 4. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! i \<and> attack (map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! i) = ({lI ! i}, s)
[PROOF STEP]
show "lI \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lI \<noteq> []
[PROOF STEP]
using c d
[PROOF STATE]
proof (prove)
using this:
\<not> I \<subseteq> s
set lI = {x \<in> I. x \<notin> s}

goal (1 subgoal):
 1. lI \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lI \<noteq> []

goal (3 subgoals):
 1. length (map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj]) = length lI
 2. nodup_all lI
 3. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! i \<and> attack (map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! i) = ({lI ! i}, s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. length (map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj]) = length lI
 2. nodup_all lI
 3. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! i \<and> attack (map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! i) = ({lI ! i}, s)
[PROOF STEP]
show "\<And>i.
       i < length lI \<Longrightarrow>
       \<turnstile>(map (\<lambda>j.
                 ((map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>)
                  [0..<length (Sj ! j) - Suc (0)]) \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>))
          [0..<length Sj] !
         i) \<and>
       (attack
        (map (\<lambda>j.
                 ((map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>)
                  [0..<length (Sj ! j) - Suc (0)]) \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>))
          [0..<length Sj] !
         i) =
       ({lI ! i}, s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! i \<and> attack (map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! i) = ({lI ! i}, s)
[PROOF STEP]
proof (simp add: a b c d e f)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>ia. \<N>\<^bsub>(Sj ! i ! ia, Sj ! i ! Suc ia)\<^esub>) [0..<length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>
[PROOF STEP]
show "\<And>i.
                i < length lI \<Longrightarrow>
                \<turnstile>(map (\<lambda>ia. \<N>\<^bsub>(Sj ! i ! ia, Sj ! i ! Suc ia)\<^esub>)
                [0..<length (Sj ! i) - Suc (0)] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>ia. \<N>\<^bsub>(Sj ! i ! ia, Sj ! i ! Suc ia)\<^esub>) [0..<length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>ia. \<N>\<^bsub>(Sj ! i ! ia, Sj ! i ! Suc ia)\<^esub>) [0..<length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>
[PROOF STEP]
fix i :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>ia. \<N>\<^bsub>(Sj ! i ! ia, Sj ! i ! Suc ia)\<^esub>) [0..<length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>
[PROOF STEP]
assume a1: "i < length lI"
[PROOF STATE]
proof (state)
this:
i < length lI

goal (1 subgoal):
 1. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>ia. \<N>\<^bsub>(Sj ! i ! ia, Sj ! i ! Suc ia)\<^esub>) [0..<length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>
[PROOF STEP]
have "\<forall>n. \<turnstile>map (\<lambda>na. \<N>\<^bsub>(Sj ! n ! na, Sj ! n ! Suc na)\<^esub>) [0..< length (Sj ! n) - 1] \<oplus>\<^sub>\<and>\<^bsup>(Sj ! n ! 0, Sj ! n ! (length (Sj ! n) - 1))\<^esup> \<or> \<not> n < length Sj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. \<turnstile>map (\<lambda>na. \<N>\<^bsub>(Sj ! n ! na, Sj ! n ! Suc na)\<^esub>) [0..<length (Sj ! n) - 1] \<oplus>\<^sub>\<and>\<^bsup>(Sj ! n ! 0, Sj ! n ! (length (Sj ! n) - 1))\<^esup> \<or> \<not> n < length Sj
[PROOF STEP]
by (metis (no_types) One_nat_def add.right_neutral add_Suc_right base_list_and f)
[PROOF STATE]
proof (state)
this:
\<forall>n. \<turnstile>map (\<lambda>na. \<N>\<^bsub>(Sj ! n ! na, Sj ! n ! Suc na)\<^esub>) [0..<length (Sj ! n) - 1] \<oplus>\<^sub>\<and>\<^bsup>(Sj ! n ! 0, Sj ! n ! (length (Sj ! n) - 1))\<^esup> \<or> \<not> n < length Sj

goal (1 subgoal):
 1. \<And>i. i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>ia. \<N>\<^bsub>(Sj ! i ! ia, Sj ! i ! Suc ia)\<^esub>) [0..<length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. \<turnstile>map (\<lambda>na. \<N>\<^bsub>(Sj ! n ! na, Sj ! n ! Suc na)\<^esub>) [0..<length (Sj ! n) - 1] \<oplus>\<^sub>\<and>\<^bsup>(Sj ! n ! 0, Sj ! n ! (length (Sj ! n) - 1))\<^esup> \<or> \<not> n < length Sj
[PROOF STEP]
show "\<turnstile>map (\<lambda>n. \<N>\<^bsub>(Sj ! i ! n, Sj ! i ! Suc n)\<^esub>) [0..< length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<turnstile>map (\<lambda>na. \<N>\<^bsub>(Sj ! n ! na, Sj ! n ! Suc na)\<^esub>) [0..<length (Sj ! n) - 1] \<oplus>\<^sub>\<and>\<^bsup>(Sj ! n ! 0, Sj ! n ! (length (Sj ! n) - 1))\<^esup> \<or> \<not> n < length Sj

goal (1 subgoal):
 1. \<turnstile>map (\<lambda>n. \<N>\<^bsub>(Sj ! i ! n, Sj ! i ! Suc n)\<^esub>) [0..<length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<turnstile>map (\<lambda>na. \<N>\<^bsub>(Sj ! n ! na, Sj ! n ! Suc na)\<^esub>) [0..<length (Sj ! n) - 1] \<oplus>\<^sub>\<and>\<^bsup>(Sj ! n ! 0, Sj ! n ! (length (Sj ! n) - 1))\<^esup> \<or> \<not> n < length Sj
i < length lI

goal (1 subgoal):
 1. \<turnstile>map (\<lambda>n. \<N>\<^bsub>(Sj ! i ! n, Sj ! i ! Suc n)\<^esub>) [0..<length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>
[PROOF STEP]
by (metis (no_types) One_nat_def e f)
[PROOF STATE]
proof (state)
this:
\<turnstile>map (\<lambda>n. \<N>\<^bsub>(Sj ! i ! n, Sj ! i ! Suc n)\<^esub>) [0..<length (Sj ! i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! i}, s)\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>ia. \<N>\<^bsub>(Sj ! ?i ! ia, Sj ! ?i ! Suc ia)\<^esub>) [0..<length (Sj ! ?i) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! ?i}, s)\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i < length lI \<Longrightarrow> \<turnstile>map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! ?i \<and> attack (map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] ! ?i) = ({lI ! ?i}, s)

goal (2 subgoals):
 1. length (map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj]) = length lI
 2. nodup_all lI
[PROOF STEP]
qed (auto simp add: e f)
[PROOF STATE]
proof (state)
this:
I - {x \<in> I. x \<in> s} = {x \<in> I. x \<notin> s} \<Longrightarrow> \<turnstile>[map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! Suc i)\<^esub>) [0..<length (Sj ! j) - Suc 0] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile>[[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile>[[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>

goal (1 subgoal):
 1. attack ([[] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<in> s}, s)\<^esup>, map (\<lambda>j. map (\<lambda>i. \<N>\<^bsub>(Sj ! j ! i, Sj ! j ! (i + 1))\<^esub>) [0..<length (Sj ! j) - 1] \<oplus>\<^sub>\<and>\<^bsup>({lI ! j}, s)\<^esup>) [0..<length Sj] \<oplus>\<^sub>\<or>\<^bsup>({x \<in> I. x \<notin> s}, s)\<^esup>] \<oplus>\<^sub>\<or>\<^bsup>(I, s)\<^esup>) = (I, s)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<exists>A. \<turnstile>A \<and> attack A = (I, s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Completeness: "I \<noteq> {} \<Longrightarrow> finite I \<Longrightarrow>
Kripke {s :: ('s :: state). \<exists> i \<in> I. (i \<rightarrow>\<^sub>i* s)} (I :: ('s :: state)set)  \<turnstile> EF s
\<Longrightarrow> \<exists> (A :: ('s :: state) attree). \<turnstile> A \<and> attack A = (I,s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
proof (case_tac "I \<subseteq> s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; I \<subseteq> s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
 2. \<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; \<not> I \<subseteq> s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
show "I \<noteq> {} \<Longrightarrow> finite I \<Longrightarrow>
    Kripke {s::'s. \<exists>i::'s\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s \<Longrightarrow> I \<subseteq> s \<Longrightarrow> \<exists>A::'s attree. \<turnstile>A \<and> attack A = (I, s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; I \<subseteq> s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
using att_or_empty_back attack.simps(3)
[PROOF STATE]
proof (prove)
using this:
?s' \<subseteq> ?s'' \<Longrightarrow> \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>(?s', ?s'')\<^esup>
attack (?as \<oplus>\<^sub>\<or>\<^bsup>?s\<^esup>) = ?s

goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; I \<subseteq> s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; I \<subseteq> s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)

goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; \<not> I \<subseteq> s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; \<not> I \<subseteq> s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
show "I \<noteq> {} \<Longrightarrow> finite I \<Longrightarrow>
    Kripke {s::'s. \<exists>i::'s\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s \<Longrightarrow> \<not> I \<subseteq> s
   \<Longrightarrow> \<exists>A::'s attree. \<turnstile>A \<and> attack A = (I, s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; \<not> I \<subseteq> s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)
[PROOF STEP]
by (iprover intro: Compl_step1 Compl_step2 Compl_step3 Compl_step4 elim: )
[PROOF STATE]
proof (state)
this:
\<lbrakk>I \<noteq> {}; finite I; Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; \<not> I \<subseteq> s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (I, s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contrapos_compl:
  "I \<noteq> {} \<Longrightarrow> finite I \<Longrightarrow>
  (\<not> (\<exists> (A :: ('s :: state) attree). \<turnstile> A \<and> attack A = (I, - s))) \<Longrightarrow>
\<not> (Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF (- s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; \<nexists>A. \<turnstile>A \<and> attack A = (I, - s)\<rbrakk> \<Longrightarrow> \<not> Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF (- s)
[PROOF STEP]
using Completeness
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?I \<noteq> {}; finite ?I; Kripke {s. \<exists>i\<in>?I. i \<rightarrow>\<^sub>i* s} ?I \<turnstile> EF ?s\<rbrakk> \<Longrightarrow> \<exists>A. \<turnstile>A \<and> attack A = (?I, ?s)

goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; \<nexists>A. \<turnstile>A \<and> attack A = (I, - s)\<rbrakk> \<Longrightarrow> \<not> Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF (- s)
[PROOF STEP]
by auto


[STATEMENT]
lemma contrapos_corr:
"(\<not>(Kripke {s :: ('s :: state). \<exists> i \<in> I. (i \<rightarrow>\<^sub>i* s)} I  \<turnstile> EF s))
\<Longrightarrow> attack A = (I,s)
\<Longrightarrow> \<not> (\<turnstile> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; attack A = (I, s)\<rbrakk> \<Longrightarrow> \<not> \<turnstile>A
[PROOF STEP]
using AT_EF
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<turnstile>?A; attack ?A = (?I, ?s)\<rbrakk> \<Longrightarrow> Kripke {s. \<exists>i\<in>?I. i \<rightarrow>\<^sub>i* s} ?I \<turnstile> EF ?s

goal (1 subgoal):
 1. \<lbrakk>\<not> Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s; attack A = (I, s)\<rbrakk> \<Longrightarrow> \<not> \<turnstile>A
[PROOF STEP]
by blast


[STATEMENT]
lemma bird_unfold:
  "bird = Node (1, 1) (pure recip \<diamondop> (pure succ \<diamondop> bird)) (pure succ \<diamondop> (pure recip \<diamondop> bird))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bird = Node (1, 1) (pure recip \<diamondop> (pure succ \<diamondop> bird)) (pure succ \<diamondop> (pure recip \<diamondop> bird))
[PROOF STEP]
using bird.code
[PROOF STATE]
proof (prove)
using this:
bird = Node (1, 1) (map_tree recip (map_tree succ bird)) (map_tree succ (map_tree recip bird))

goal (1 subgoal):
 1. bird = Node (1, 1) (pure recip \<diamondop> (pure succ \<diamondop> bird)) (pure succ \<diamondop> (pure recip \<diamondop> bird))
[PROOF STEP]
unfolding map_tree_ap_tree_pure_tree[symmetric]
[PROOF STATE]
proof (prove)
using this:
bird = Node (1, 1) (pure recip \<diamondop> (pure succ \<diamondop> bird)) (pure succ \<diamondop> (pure recip \<diamondop> bird))

goal (1 subgoal):
 1. bird = Node (1, 1) (pure recip \<diamondop> (pure succ \<diamondop> bird)) (pure succ \<diamondop> (pure recip \<diamondop> bird))
[PROOF STEP]
.


[STATEMENT]
lemma bird_simps [simp]:
  "root bird = (1, 1)"
  "left bird = pure recip \<diamondop> (pure succ \<diamondop> bird)"
  "right bird = pure succ \<diamondop> (pure recip \<diamondop> bird)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root bird = (1, 1) &&& left bird = pure recip \<diamondop> (pure succ \<diamondop> bird) &&& right bird = pure succ \<diamondop> (pure recip \<diamondop> bird)
[PROOF STEP]
by(subst bird_unfold, simp)+


[STATEMENT]
lemma mirror_bird: "mirror bird = pure recip \<diamondop> bird" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mirror bird = pure recip \<diamondop> bird
[PROOF STEP]
proof(rule sym)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pure recip \<diamondop> bird = mirror bird
[PROOF STEP]
let ?F = "\<lambda>t. Node (1, 1) (map_tree succ (map_tree recip t)) (map_tree recip (map_tree succ t))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pure recip \<diamondop> bird = mirror bird
[PROOF STEP]
have *: "mirror bird = ?F (mirror bird)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mirror bird = Node (1, 1) (map_tree succ (map_tree recip (mirror bird))) (map_tree recip (map_tree succ (mirror bird)))
[PROOF STEP]
by(rule tree.expand; simp add: mirror_ap_tree mirror_pure map_tree_ap_tree_pure_tree[symmetric])
[PROOF STATE]
proof (state)
this:
mirror bird = Node (1, 1) (map_tree succ (map_tree recip (mirror bird))) (map_tree recip (map_tree succ (mirror bird)))

goal (1 subgoal):
 1. pure recip \<diamondop> bird = mirror bird
[PROOF STEP]
show "t = mirror bird" when "t = ?F t" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = mirror bird
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
t = Node (1, 1) (map_tree succ (map_tree recip t)) (map_tree recip (map_tree succ t))

goal (1 subgoal):
 1. t = mirror bird
[PROOF STEP]
by corec_unique (fact *)
[PROOF STATE]
proof (state)
this:
?t = Node (1, 1) (map_tree succ (map_tree recip ?t)) (map_tree recip (map_tree succ ?t)) \<Longrightarrow> ?t = mirror bird

goal (1 subgoal):
 1. pure recip \<diamondop> bird = Node (1, 1) (map_tree succ (map_tree recip (pure recip \<diamondop> bird))) (map_tree recip (map_tree succ (pure recip \<diamondop> bird)))
[PROOF STEP]
show "pure recip \<diamondop> bird = ?F (pure recip \<diamondop> bird)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure recip \<diamondop> bird = Node (1, 1) (map_tree succ (map_tree recip (pure recip \<diamondop> bird))) (map_tree recip (map_tree succ (pure recip \<diamondop> bird)))
[PROOF STEP]
by(rule tree.expand; simp add: map_tree_ap_tree_pure_tree; applicative_lifting; simp add: split_beta)
[PROOF STATE]
proof (state)
this:
pure recip \<diamondop> bird = Node (1, 1) (map_tree succ (map_tree recip (pure recip \<diamondop> bird))) (map_tree recip (map_tree succ (pure recip \<diamondop> bird)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma even_mirror_simps [simp]:
  "root (even_mirror t) = root t"
  "left (even_mirror t) = odd_mirror (right t)"
  "right (even_mirror t) = odd_mirror (left t)"
  and odd_mirror_simps [simp]:
  "root (odd_mirror t) = root t"
  "left (odd_mirror t) = even_mirror (left t)"
  "right (odd_mirror t) = even_mirror (right t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (root (even_mirror t) = root t &&& left (even_mirror t) = odd_mirror (right t) &&& right (even_mirror t) = odd_mirror (left t)) &&& root (odd_mirror t) = root t &&& left (odd_mirror t) = even_mirror (left t) &&& right (odd_mirror t) = even_mirror (right t)
[PROOF STEP]
by(simp_all add: even_mirror_def odd_mirror_def)


[STATEMENT]
lemma even_odd_mirror_pure [simp]: fixes even shows
  "even_odd_mirror even (pure_tree x) = pure_tree x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even_odd_mirror even (pure x) = pure x
[PROOF STEP]
by(coinduction arbitrary: even) auto


[STATEMENT]
lemma even_odd_mirror_ap_tree [simp]: fixes even shows
  "even_odd_mirror even (f \<diamondop> x) = even_odd_mirror even f \<diamondop> even_odd_mirror even x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even_odd_mirror even (f \<diamondop> x) = even_odd_mirror even f \<diamondop> even_odd_mirror even x
[PROOF STEP]
by(coinduction arbitrary: even f x) auto


[STATEMENT]
lemma [simp]:
  shows even_mirror_pure: "even_mirror (pure_tree x) = pure_tree x"
  and odd_mirror_pure: "odd_mirror (pure_tree x) = pure_tree x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even_mirror (pure x) = pure x &&& odd_mirror (pure x) = pure x
[PROOF STEP]
by(simp_all add: even_mirror_def odd_mirror_def)


[STATEMENT]
lemma [simp]:
  shows even_mirror_ap_tree: "even_mirror (f \<diamondop> x) = even_mirror f \<diamondop> even_mirror x"
  and odd_mirror_ap_tree: "odd_mirror (f \<diamondop> x) = odd_mirror f \<diamondop> odd_mirror x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even_mirror (f \<diamondop> x) = even_mirror f \<diamondop> even_mirror x &&& odd_mirror (f \<diamondop> x) = odd_mirror f \<diamondop> odd_mirror x
[PROOF STEP]
by(simp_all add: even_mirror_def odd_mirror_def)


[STATEMENT]
lemma even_mirror_traverse_tree [simp]:
  "root (traverse_tree path (even_mirror t)) = root (traverse_tree (even_mirror_path path) t)"
  and odd_mirror_traverse_tree [simp]:
  "root (traverse_tree path (odd_mirror t)) = root (traverse_tree (odd_mirror_path path) t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (traverse_tree path (even_mirror t)) = root (traverse_tree (even_mirror_path path) t) &&& root (traverse_tree path (odd_mirror t)) = root (traverse_tree (odd_mirror_path path) t)
[PROOF STEP]
by (induct path arbitrary: t) (simp_all split: dir.splits)


[STATEMENT]
lemma even_odd_mirror_path_involution [simp]:
  "even_mirror_path (even_mirror_path path) = path"
  "odd_mirror_path (odd_mirror_path path) = path"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even_mirror_path (even_mirror_path path) = path &&& odd_mirror_path (odd_mirror_path path) = path
[PROOF STEP]
by (induct path) (simp_all split: dir.splits)


[STATEMENT]
lemma even_odd_mirror_path_injective [simp]:
  "even_mirror_path path = even_mirror_path path' \<longleftrightarrow> path = path'"
  "odd_mirror_path path = odd_mirror_path path' \<longleftrightarrow> path = path'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (even_mirror_path path = even_mirror_path path') = (path = path') &&& (odd_mirror_path path = odd_mirror_path path') = (path = path')
[PROOF STEP]
by (induct path arbitrary: path') (case_tac path', simp_all split: dir.splits)+


[STATEMENT]
lemma odd_mirror_bird_stern_brocot:
  "odd_mirror bird = stern_brocot_recurse"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_mirror bird = stern_brocot_recurse
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd_mirror bird = stern_brocot_recurse
[PROOF STEP]
let ?rsrs = "map_tree (recip \<circ> succ \<circ> recip \<circ> succ)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd_mirror bird = stern_brocot_recurse
[PROOF STEP]
let ?rssr = "map_tree (recip \<circ> succ \<circ> succ \<circ> recip)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd_mirror bird = stern_brocot_recurse
[PROOF STEP]
let ?srrs = "map_tree (succ \<circ> recip \<circ> recip \<circ> succ)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd_mirror bird = stern_brocot_recurse
[PROOF STEP]
let ?srsr = "map_tree (succ \<circ> recip \<circ> succ \<circ> recip)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd_mirror bird = stern_brocot_recurse
[PROOF STEP]
let ?R = "\<lambda>t. Node (1, 1) (Node (1, 2) (?rssr t) (?rsrs t)) (Node (2, 1) (?srsr t) (?srrs t))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd_mirror bird = stern_brocot_recurse
[PROOF STEP]
have *: "stern_brocot_recurse = ?R stern_brocot_recurse"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stern_brocot_recurse = Node (1, 1) (Node (1, 2) (map_tree (recip \<circ> succ \<circ> succ \<circ> recip) stern_brocot_recurse) (map_tree (recip \<circ> succ \<circ> recip \<circ> succ) stern_brocot_recurse)) (Node (2, 1) (map_tree (succ \<circ> recip \<circ> succ \<circ> recip) stern_brocot_recurse) (map_tree (succ \<circ> recip \<circ> recip \<circ> succ) stern_brocot_recurse))
[PROOF STEP]
by(rule tree.expand; simp; intro conjI; rule tree.expand; simp; intro conjI) \<comment> \<open>Expand the tree twice\<close>
      (applicative_lifting, simp add: split_beta)+
[PROOF STATE]
proof (state)
this:
stern_brocot_recurse = Node (1, 1) (Node (1, 2) (map_tree (recip \<circ> succ \<circ> succ \<circ> recip) stern_brocot_recurse) (map_tree (recip \<circ> succ \<circ> recip \<circ> succ) stern_brocot_recurse)) (Node (2, 1) (map_tree (succ \<circ> recip \<circ> succ \<circ> recip) stern_brocot_recurse) (map_tree (succ \<circ> recip \<circ> recip \<circ> succ) stern_brocot_recurse))

goal (1 subgoal):
 1. odd_mirror bird = stern_brocot_recurse
[PROOF STEP]
show "f = stern_brocot_recurse" when "f = ?R f" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = stern_brocot_recurse
[PROOF STEP]
using that *
[PROOF STATE]
proof (prove)
using this:
f = Node (1, 1) (Node (1, 2) (map_tree (recip \<circ> succ \<circ> succ \<circ> recip) f) (map_tree (recip \<circ> succ \<circ> recip \<circ> succ) f)) (Node (2, 1) (map_tree (succ \<circ> recip \<circ> succ \<circ> recip) f) (map_tree (succ \<circ> recip \<circ> recip \<circ> succ) f))
stern_brocot_recurse = Node (1, 1) (Node (1, 2) (map_tree (recip \<circ> succ \<circ> succ \<circ> recip) stern_brocot_recurse) (map_tree (recip \<circ> succ \<circ> recip \<circ> succ) stern_brocot_recurse)) (Node (2, 1) (map_tree (succ \<circ> recip \<circ> succ \<circ> recip) stern_brocot_recurse) (map_tree (succ \<circ> recip \<circ> recip \<circ> succ) stern_brocot_recurse))

goal (1 subgoal):
 1. f = stern_brocot_recurse
[PROOF STEP]
by corec_unique
[PROOF STATE]
proof (state)
this:
?f = Node (1, 1) (Node (1, 2) (map_tree (recip \<circ> succ \<circ> succ \<circ> recip) ?f) (map_tree (recip \<circ> succ \<circ> recip \<circ> succ) ?f)) (Node (2, 1) (map_tree (succ \<circ> recip \<circ> succ \<circ> recip) ?f) (map_tree (succ \<circ> recip \<circ> recip \<circ> succ) ?f)) \<Longrightarrow> ?f = stern_brocot_recurse

goal (1 subgoal):
 1. odd_mirror bird = Node (1, 1) (Node (1, 2) (map_tree (recip \<circ> succ \<circ> succ \<circ> recip) (odd_mirror bird)) (map_tree (recip \<circ> succ \<circ> recip \<circ> succ) (odd_mirror bird))) (Node (2, 1) (map_tree (succ \<circ> recip \<circ> succ \<circ> recip) (odd_mirror bird)) (map_tree (succ \<circ> recip \<circ> recip \<circ> succ) (odd_mirror bird)))
[PROOF STEP]
show "odd_mirror bird = ?R (odd_mirror bird)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_mirror bird = Node (1, 1) (Node (1, 2) (map_tree (recip \<circ> succ \<circ> succ \<circ> recip) (odd_mirror bird)) (map_tree (recip \<circ> succ \<circ> recip \<circ> succ) (odd_mirror bird))) (Node (2, 1) (map_tree (succ \<circ> recip \<circ> succ \<circ> recip) (odd_mirror bird)) (map_tree (succ \<circ> recip \<circ> recip \<circ> succ) (odd_mirror bird)))
[PROOF STEP]
by(rule tree.expand; simp; intro conjI; rule tree.expand; simp; intro conjI) \<comment> \<open>Expand the tree twice\<close>
      (applicative_lifting; simp)+
[PROOF STATE]
proof (state)
this:
odd_mirror bird = Node (1, 1) (Node (1, 2) (map_tree (recip \<circ> succ \<circ> succ \<circ> recip) (odd_mirror bird)) (map_tree (recip \<circ> succ \<circ> recip \<circ> succ) (odd_mirror bird))) (Node (2, 1) (map_tree (succ \<circ> recip \<circ> succ \<circ> recip) (odd_mirror bird)) (map_tree (succ \<circ> recip \<circ> recip \<circ> succ) (odd_mirror bird)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem bird_rationals:
  assumes "m > 0" "n > 0"
  shows "root (traverse_tree (odd_mirror_path (mk_path m n)) (pure rat_of \<diamondop> bird)) = Fract (int m) (int n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (traverse_tree (odd_mirror_path (mk_path m n)) (pure rat_of \<diamondop> bird)) = Fract (int m) (int n)
[PROOF STEP]
using stern_brocot_rationals[OF assms]
[PROOF STATE]
proof (prove)
using this:
root (traverse_tree (mk_path m n) (pure rat_of \<diamondop> stern_brocot_recurse)) = Fract (int m) (int n)

goal (1 subgoal):
 1. root (traverse_tree (odd_mirror_path (mk_path m n)) (pure rat_of \<diamondop> bird)) = Fract (int m) (int n)
[PROOF STEP]
by (simp add: odd_mirror_bird_stern_brocot[symmetric])


[STATEMENT]
theorem bird_rationals_not_repeated:
  "root (traverse_tree path (pure rat_of \<diamondop> bird)) = root (traverse_tree path' (pure rat_of \<diamondop> bird))
  \<Longrightarrow> path = path'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (traverse_tree path (pure rat_of \<diamondop> bird)) = root (traverse_tree path' (pure rat_of \<diamondop> bird)) \<Longrightarrow> path = path'
[PROOF STEP]
using stern_brocot_rationals_not_repeated[where path="odd_mirror_path path" and path'="odd_mirror_path path'"]
[PROOF STATE]
proof (prove)
using this:
root (traverse_tree (odd_mirror_path path) (pure rat_of \<diamondop> stern_brocot_recurse)) = root (traverse_tree (odd_mirror_path path') (pure rat_of \<diamondop> stern_brocot_recurse)) \<Longrightarrow> odd_mirror_path path = odd_mirror_path path'

goal (1 subgoal):
 1. root (traverse_tree path (pure rat_of \<diamondop> bird)) = root (traverse_tree path' (pure rat_of \<diamondop> bird)) \<Longrightarrow> path = path'
[PROOF STEP]
by (simp add: odd_mirror_bird_stern_brocot[symmetric])


[STATEMENT]
lemma a_d_zero [simp]: "ad x \<cdot> d x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> d x = 0
[PROOF STEP]
by (metis am1 am2 a_zero_def am_d_def)


[STATEMENT]
lemma a_d_one [simp]: "d x \<oplus> ad x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<oplus> ad x = (1::'a)
[PROOF STEP]
by (metis am1 am3 mult_1_right am_d_def am_add_op_def)


[STATEMENT]
lemma n_annil [simp]: "0 \<cdot> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<cdot> x = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<cdot> x = 0
[PROOF STEP]
have "0 \<cdot> x = d x \<cdot> ad x \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<cdot> x = d x \<cdot> ad x \<cdot> x
[PROOF STEP]
by (simp add: a_zero_def am_d_def)
[PROOF STATE]
proof (state)
this:
0 \<cdot> x = d x \<cdot> ad x \<cdot> x

goal (1 subgoal):
 1. 0 \<cdot> x = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<cdot> x = d x \<cdot> ad x \<cdot> x

goal (1 subgoal):
 1. 0 \<cdot> x = 0
[PROOF STEP]
have "... = d x \<cdot> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> ad x \<cdot> x = d x \<cdot> 0
[PROOF STEP]
by (metis am1 mult_assoc a_zero_def)
[PROOF STATE]
proof (state)
this:
d x \<cdot> ad x \<cdot> x = d x \<cdot> 0

goal (1 subgoal):
 1. 0 \<cdot> x = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d x \<cdot> ad x \<cdot> x = d x \<cdot> 0

goal (1 subgoal):
 1. 0 \<cdot> x = 0
[PROOF STEP]
by (metis am1 am2 am3 mult_assoc a_zero_def)
[PROOF STATE]
proof (state)
this:
0 \<cdot> x = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_mult_idem [simp]: "ad x \<cdot> ad x = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
have "ad x \<cdot> ad x = ad (1 \<cdot> x) \<cdot> 1 \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad x = ad ((1::'a) \<cdot> x) \<cdot> (1::'a) \<cdot> ad x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad x = ad ((1::'a) \<cdot> x) \<cdot> (1::'a) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad x = ad ((1::'a) \<cdot> x) \<cdot> (1::'a) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
have "... = ad (1 \<cdot> x) \<cdot> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad ((1::'a) \<cdot> x) \<cdot> (1::'a) \<cdot> ad x = ad ((1::'a) \<cdot> x) \<cdot> (1::'a)
[PROOF STEP]
using am5
[PROOF STATE]
proof (prove)
using this:
ad (?x \<cdot> ?y) \<cdot> ?x \<cdot> ad ?y = ad (?x \<cdot> ?y) \<cdot> ?x

goal (1 subgoal):
 1. ad ((1::'a) \<cdot> x) \<cdot> (1::'a) \<cdot> ad x = ad ((1::'a) \<cdot> x) \<cdot> (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ad ((1::'a) \<cdot> x) \<cdot> (1::'a) \<cdot> ad x = ad ((1::'a) \<cdot> x) \<cdot> (1::'a)

goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ad x \<cdot> ad x = ad ((1::'a) \<cdot> x) \<cdot> (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> ad x = ad ((1::'a) \<cdot> x) \<cdot> (1::'a)

goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad x = ad x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_add_idem [simp]: "ad x \<oplus> ad x = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<oplus> ad x = ad x
[PROOF STEP]
by (metis am1 am3 am4 mult_1_right am_add_op_def)


[STATEMENT]
lemma a_add_comm: "x \<oplus> y = y \<oplus> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<oplus> y = y \<oplus> x
[PROOF STEP]
using am2 am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<cdot> ad ?y = ad ?y \<cdot> ad ?x
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. x \<oplus> y = y \<oplus> x
[PROOF STEP]
by auto


[STATEMENT]
lemma a_add_assoc: "x \<oplus> (y \<oplus> z) = (x \<oplus> y) \<oplus> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<oplus> (y \<oplus> z) = x \<oplus> y \<oplus> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<oplus> (y \<oplus> z) = x \<oplus> y \<oplus> z
[PROOF STEP]
have "\<And>x y. ad x \<cdot> ad (x \<cdot> y) = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. ad x \<cdot> ad (x \<cdot> y) = ad x
[PROOF STEP]
by (metis a_mult_idem am2 am4 mult_assoc)
[PROOF STATE]
proof (state)
this:
ad ?x \<cdot> ad (?x \<cdot> ?y) = ad ?x

goal (1 subgoal):
 1. x \<oplus> (y \<oplus> z) = x \<oplus> y \<oplus> z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ad ?x \<cdot> ad (?x \<cdot> ?y) = ad ?x

goal (1 subgoal):
 1. x \<oplus> (y \<oplus> z) = x \<oplus> y \<oplus> z
[PROOF STEP]
by (metis a_add_comm am_add_op_def local.am3 local.am4 mult_assoc)
[PROOF STATE]
proof (state)
this:
x \<oplus> (y \<oplus> z) = x \<oplus> y \<oplus> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma huntington [simp]: "ad (x \<oplus> y) \<oplus> ad (x \<oplus> ad y) = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<oplus> y) \<oplus> ad (x \<oplus> ad y) = ad x
[PROOF STEP]
using a_add_idem am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. ad (x \<oplus> y) \<oplus> ad (x \<oplus> ad y) = ad x
[PROOF STEP]
by auto


[STATEMENT]
lemma a_absorb1 [simp]: "(ad x \<oplus> ad y) \<cdot> ad x = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> ad x = ad x
[PROOF STEP]
by (metis a_add_idem a_mult_idem am4 mult_assoc am_add_op_def)


[STATEMENT]
lemma a_absorb2 [simp]: "ad x \<oplus> ad x \<cdot> ad y = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<oplus> ad x \<cdot> ad y = ad x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<oplus> ad x \<cdot> ad y = ad x
[PROOF STEP]
have "ad (ad x) \<cdot> ad (ad x \<cdot> ad y) = ad (ad x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad x) \<cdot> ad (ad x \<cdot> ad y) = ad (ad x)
[PROOF STEP]
by (metis (no_types) a_mult_idem local.am4 local.mult.semigroup_axioms semigroup.assoc)
[PROOF STATE]
proof (state)
this:
ad (ad x) \<cdot> ad (ad x \<cdot> ad y) = ad (ad x)

goal (1 subgoal):
 1. ad x \<oplus> ad x \<cdot> ad y = ad x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad x) \<cdot> ad (ad x \<cdot> ad y) = ad (ad x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (ad x) \<cdot> ad (ad x \<cdot> ad y) = ad (ad x)

goal (1 subgoal):
 1. ad x \<oplus> ad x \<cdot> ad y = ad x
[PROOF STEP]
using a_add_idem am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad (ad x) \<cdot> ad (ad x \<cdot> ad y) = ad (ad x)
ad ?x \<oplus> ad ?x = ad ?x
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. ad x \<oplus> ad x \<cdot> ad y = ad x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad x \<oplus> ad x \<cdot> ad y = ad x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod_split [simp]: "ad x \<cdot> ad y \<oplus> ad x \<cdot> d y = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y \<oplus> ad x \<cdot> d y = ad x
[PROOF STEP]
using a_add_idem am_d_def am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
d ?x = ad (ad ?x)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. ad x \<cdot> ad y \<oplus> ad x \<cdot> d y = ad x
[PROOF STEP]
by auto


[STATEMENT]
lemma sum_split [simp]: "(ad x \<oplus> ad y) \<cdot> (ad x \<oplus> d y) = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> d y) = ad x
[PROOF STEP]
using a_add_idem am_d_def am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
d ?x = ad (ad ?x)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> d y) = ad x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma a_comp_simp [simp]: "(ad x \<oplus> ad y) \<cdot> d x = ad y \<cdot> d x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> d x = ad y \<cdot> d x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> d x = ad y \<cdot> d x
[PROOF STEP]
have f1: "(ad x \<oplus> ad y) \<cdot> d x = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad x) \<cdot> ad (ad (ad y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> d x = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad x) \<cdot> ad (ad (ad y))
[PROOF STEP]
by (simp add: am_add_op_def am_d_def)
[PROOF STATE]
proof (state)
this:
(ad x \<oplus> ad y) \<cdot> d x = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad x) \<cdot> ad (ad (ad y))

goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> d x = ad y \<cdot> d x
[PROOF STEP]
have f2: "ad y = ad (ad (ad y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad y = ad (ad (ad y))
[PROOF STEP]
using a_add_idem am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

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

goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> d x = ad y \<cdot> d x
[PROOF STEP]
have "ad y = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad y = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad y
[PROOF STEP]
by (metis (no_types) a_absorb1 a_add_comm am_add_op_def)
[PROOF STATE]
proof (state)
this:
ad y = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad y

goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> d x = ad y \<cdot> d x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad y = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad y = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad y

goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> d x = ad y \<cdot> d x
[PROOF STEP]
using f2 f1
[PROOF STATE]
proof (prove)
using this:
ad y = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad y
ad y = ad (ad (ad y))
(ad x \<oplus> ad y) \<cdot> d x = ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad x) \<cdot> ad (ad (ad y))

goal (1 subgoal):
 1. (ad x \<oplus> ad y) \<cdot> d x = ad y \<cdot> d x
[PROOF STEP]
by (simp add: am_d_def local.am2 local.mult.semigroup_axioms semigroup.assoc)
[PROOF STATE]
proof (state)
this:
(ad x \<oplus> ad y) \<cdot> d x = ad y \<cdot> d x

goal:
No subgoals!
[PROOF STEP]
qed