[STATEMENT]
lemma nth_app_eq3: assumes "tl sl \<noteq> []"
  shows "(sla @ tl sl) ! (length (sla @ tl sl) - (1)) = sl ! (length sl - (1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sla @ tl sl) ! (length (sla @ tl sl) - 1) = sl ! (length sl - 1)
[PROOF STEP]
using assms nth_app_eq nth_tl_length
[PROOF STATE]
proof (prove)
using this:
tl sl \<noteq> []
\<lbrakk>?sl \<noteq> []; ?sl ! (length ?sl - Suc 0) = ?x\<rbrakk> \<Longrightarrow> (?l @ ?sl) ! (length ?l + length ?sl - Suc 0) = ?x
tl ?sl \<noteq> [] \<Longrightarrow> tl ?sl ! (length (tl ?sl) - Suc 0) = ?sl ! (length ?sl - Suc 0)

goal (1 subgoal):
 1. (sla @ tl sl) ! (length (sla @ tl sl) - 1) = sl ! (length sl - 1)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma not_empty_ex: "A \<noteq> {} \<Longrightarrow> ? x. x \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A
[PROOF STEP]
by force


[STATEMENT]
lemma fst_att_eq: "(fst x # sl) ! (0) = fst (attack (al \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst x # sl) ! 0 = fst (attack (al \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>))
[PROOF STEP]
by simp


[STATEMENT]
lemma list_eq1[rule_format]: "sl \<noteq> [] \<longrightarrow>
     (fst x # sl) ! (length (fst x # sl) - (1)) = sl ! (length sl - (1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sl \<noteq> [] \<longrightarrow> (fst x # sl) ! (length (fst x # sl) - 1) = sl ! (length sl - 1)
[PROOF STEP]
by (induction sl, auto)


[STATEMENT]
lemma attack_eq1: "snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) = snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) = snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>))
[PROOF STEP]
by simp


[STATEMENT]
lemma fst_lem1[rule_format]: "\<forall> (a:: 's set) b (c :: 's set) d. (a, c) = (b, d) \<longrightarrow> a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b c d. (a, c) = (b, d) \<longrightarrow> a = b
[PROOF STEP]
by auto


[STATEMENT]
lemma fst_eq1: "(sla ! (0), y) = attack x1 \<Longrightarrow>
       sla ! (0) = fst (attack x1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sla ! 0, y) = attack x1 \<Longrightarrow> sla ! 0 = fst (attack x1)
[PROOF STEP]
by (rule_tac c = y and d = "snd(attack  x1)" in fst_lem1, simp)


[STATEMENT]
lemma base_att_lem1: " y0 \<subseteq> y1 \<Longrightarrow> \<turnstile> \<N>\<^bsub>(y1, y)\<^esub> \<Longrightarrow>\<turnstile> \<N>\<^bsub>(y0, y)\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y0 \<subseteq> y1; \<turnstile>\<N>\<^bsub>(y1, y)\<^esub>\<rbrakk> \<Longrightarrow> \<turnstile>\<N>\<^bsub>(y0, y)\<^esub>
[PROOF STEP]
by (simp add: att_base, blast)


[STATEMENT]
lemma ref_pres_att: "A \<sqsubseteq> A' \<Longrightarrow> attack A = attack A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq> A' \<Longrightarrow> attack A = attack A'
[PROOF STEP]
proof (erule refines_to.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>A l si' si'' l'' si si''' A' l' A''. \<lbrakk>A = l @ [\<N>\<^bsub>(si', si'')\<^esub>] @ l'' \<oplus>\<^sub>\<and>\<^bsup>(si, si''')\<^esup>; A' = l' \<oplus>\<^sub>\<and>\<^bsup>(si', si'')\<^esup>; A'' = l @ l' @ l'' \<oplus>\<^sub>\<and>\<^bsup>(si, si''')\<^esup>\<rbrakk> \<Longrightarrow> attack A = attack A''
 2. \<And>as A s. \<lbrakk>as \<noteq> []; \<forall>A'\<in>set as. (A \<sqsubseteq> A' \<and> attack A = attack A') \<and> attack A = s\<rbrakk> \<Longrightarrow> attack A = attack (as \<oplus>\<^sub>\<or>\<^bsup>s\<^esup>)
 3. \<And>A A' A''. \<lbrakk>A \<sqsubseteq> A'; attack A = attack A'; A' \<sqsubseteq> A''; attack A' = attack A''\<rbrakk> \<Longrightarrow> attack A = attack A''
 4. \<And>A. attack A = attack A
[PROOF STEP]
show "\<And>(A::'a attree) (l::'a attree list) (si'::'a set) (si''::'a set) (l''::'a attree list) (si::'a set)
       (si'''::'a set) (A'::'a attree) (l'::'a attree list) A''::'a attree.
       A = (l @ [\<N>\<^bsub>(si', si'')\<^esub>] @ l'' \<oplus>\<^sub>\<and>\<^bsup>(si, si''')\<^esup>) \<Longrightarrow>
       A' = (l' \<oplus>\<^sub>\<and>\<^bsup>(si', si'')\<^esup>) \<Longrightarrow> A'' = (l @ l' @ l'' \<oplus>\<^sub>\<and>\<^bsup>(si, si''')\<^esup>) \<Longrightarrow> attack A = attack A''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A l si' si'' l'' si si''' A' l' A''. \<lbrakk>A = l @ [\<N>\<^bsub>(si', si'')\<^esub>] @ l'' \<oplus>\<^sub>\<and>\<^bsup>(si, si''')\<^esup>; A' = l' \<oplus>\<^sub>\<and>\<^bsup>(si', si'')\<^esup>; A'' = l @ l' @ l'' \<oplus>\<^sub>\<and>\<^bsup>(si, si''')\<^esup>\<rbrakk> \<Longrightarrow> attack A = attack A''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A = ?l @ [\<N>\<^bsub>(?si', ?si'')\<^esub>] @ ?l'' \<oplus>\<^sub>\<and>\<^bsup>(?si, ?si''')\<^esup>; ?A' = ?l' \<oplus>\<^sub>\<and>\<^bsup>(?si', ?si'')\<^esup>; ?A'' = ?l @ ?l' @ ?l'' \<oplus>\<^sub>\<and>\<^bsup>(?si, ?si''')\<^esup>\<rbrakk> \<Longrightarrow> attack ?A = attack ?A''

goal (3 subgoals):
 1. \<And>as A s. \<lbrakk>as \<noteq> []; \<forall>A'\<in>set as. (A \<sqsubseteq> A' \<and> attack A = attack A') \<and> attack A = s\<rbrakk> \<Longrightarrow> attack A = attack (as \<oplus>\<^sub>\<or>\<^bsup>s\<^esup>)
 2. \<And>A A' A''. \<lbrakk>A \<sqsubseteq> A'; attack A = attack A'; A' \<sqsubseteq> A''; attack A' = attack A''\<rbrakk> \<Longrightarrow> attack A = attack A''
 3. \<And>A. attack A = attack A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>as A s. \<lbrakk>as \<noteq> []; \<forall>A'\<in>set as. (A \<sqsubseteq> A' \<and> attack A = attack A') \<and> attack A = s\<rbrakk> \<Longrightarrow> attack A = attack (as \<oplus>\<^sub>\<or>\<^bsup>s\<^esup>)
 2. \<And>A A' A''. \<lbrakk>A \<sqsubseteq> A'; attack A = attack A'; A' \<sqsubseteq> A''; attack A' = attack A''\<rbrakk> \<Longrightarrow> attack A = attack A''
 3. \<And>A. attack A = attack A
[PROOF STEP]
show "\<And>(as::'a attree list) (A::'a attree) (s::'a set \<times> 'a set).
       as \<noteq> [] \<Longrightarrow>
       (\<forall>A'::'a attree\<in> (set as). ((A \<sqsubseteq> A') \<and> (attack A = attack A')) \<and> attack A = s) \<Longrightarrow>
       attack A = attack (as \<oplus>\<^sub>\<or>\<^bsup>s\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as A s. \<lbrakk>as \<noteq> []; \<forall>A'\<in>set as. (A \<sqsubseteq> A' \<and> attack A = attack A') \<and> attack A = s\<rbrakk> \<Longrightarrow> attack A = attack (as \<oplus>\<^sub>\<or>\<^bsup>s\<^esup>)
[PROOF STEP]
using last_in_set
[PROOF STATE]
proof (prove)
using this:
?as \<noteq> [] \<Longrightarrow> last ?as \<in> set ?as

goal (1 subgoal):
 1. \<And>as A s. \<lbrakk>as \<noteq> []; \<forall>A'\<in>set as. (A \<sqsubseteq> A' \<and> attack A = attack A') \<and> attack A = s\<rbrakk> \<Longrightarrow> attack A = attack (as \<oplus>\<^sub>\<or>\<^bsup>s\<^esup>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?as \<noteq> []; \<forall>A'\<in>set ?as. (?A \<sqsubseteq> A' \<and> attack ?A = attack A') \<and> attack ?A = ?s\<rbrakk> \<Longrightarrow> attack ?A = attack (?as \<oplus>\<^sub>\<or>\<^bsup>?s\<^esup>)

goal (2 subgoals):
 1. \<And>A A' A''. \<lbrakk>A \<sqsubseteq> A'; attack A = attack A'; A' \<sqsubseteq> A''; attack A' = attack A''\<rbrakk> \<Longrightarrow> attack A = attack A''
 2. \<And>A. attack A = attack A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A A' A''. \<lbrakk>A \<sqsubseteq> A'; attack A = attack A'; A' \<sqsubseteq> A''; attack A' = attack A''\<rbrakk> \<Longrightarrow> attack A = attack A''
 2. \<And>A. attack A = attack A
[PROOF STEP]
show "\<And>(A::'a attree) (A'::'a attree) A''::'a attree.
       A \<sqsubseteq> A' \<Longrightarrow> attack A = attack A' \<Longrightarrow> A' \<sqsubseteq> A'' \<Longrightarrow> attack A' = attack A'' \<Longrightarrow> attack A = attack A''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A A' A''. \<lbrakk>A \<sqsubseteq> A'; attack A = attack A'; A' \<sqsubseteq> A''; attack A' = attack A''\<rbrakk> \<Longrightarrow> attack A = attack A''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A \<sqsubseteq> ?A'; attack ?A = attack ?A'; ?A' \<sqsubseteq> ?A''; attack ?A' = attack ?A''\<rbrakk> \<Longrightarrow> attack ?A = attack ?A''

goal (1 subgoal):
 1. \<And>A. attack A = attack A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. attack A = attack A
[PROOF STEP]
show "\<And>A::'a attree. attack A = attack A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. attack A = attack A
[PROOF STEP]
by (rule refl)
[PROOF STATE]
proof (state)
this:
attack ?A = attack ?A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  base_subset:
    assumes "xa \<subseteq> xc"
    shows  "\<turnstile>\<N>\<^bsub>(x, xa)\<^esub> \<Longrightarrow> \<turnstile>\<N>\<^bsub>(x, xc)\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>\<N>\<^bsub>(x, xa)\<^esub> \<Longrightarrow> \<turnstile>\<N>\<^bsub>(x, xc)\<^esub>
[PROOF STEP]
proof (simp add: att_base)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>x. \<exists>xa\<in>xa. x \<rightarrow>\<^sub>i xa \<Longrightarrow> \<forall>x\<in>x. \<exists>xa\<in>xc. x \<rightarrow>\<^sub>i xa
[PROOF STEP]
show " \<forall>x::'a\<in>x. \<exists>xa::'a\<in>xa. x \<rightarrow>\<^sub>i xa \<Longrightarrow> \<forall>x::'a\<in>x. \<exists>xa::'a\<in>xc. x \<rightarrow>\<^sub>i xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>x. \<exists>xa\<in>xa. x \<rightarrow>\<^sub>i xa \<Longrightarrow> \<forall>x\<in>x. \<exists>xa\<in>xc. x \<rightarrow>\<^sub>i xa
[PROOF STEP]
by (meson assms in_mono)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>x. \<exists>xa\<in>xa. x \<rightarrow>\<^sub>i xa \<Longrightarrow> \<forall>x\<in>x. \<exists>xa\<in>xc. x \<rightarrow>\<^sub>i xa

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem AT_EF: assumes " \<turnstile> (A :: ('s :: state) attree)"
               and  "attack A = (I,s)"
               shows "Kripke {s :: ('s :: state). \<exists> i \<in> I. (i \<rightarrow>\<^sub>i* s)} (I :: ('s :: state)set)  \<turnstile> EF s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s
[PROOF STEP]
proof (simp add:check_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I \<subseteq> {sa. (\<exists>i\<in>I. i \<rightarrow>\<^sub>i* sa) \<and> sa \<in> EF s}
[PROOF STEP]
show "I \<subseteq> {sa::('s :: state). (\<exists>i::'s\<in>I. i \<rightarrow>\<^sub>i* sa) \<and> sa \<in> EF s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> {sa. (\<exists>i\<in>I. i \<rightarrow>\<^sub>i* sa) \<and> sa \<in> EF s}
[PROOF STEP]
proof (rule subsetI, rule CollectI, rule conjI, simp add: state_transition_refl_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> I \<Longrightarrow> \<exists>i\<in>I. (i, x) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*
 2. \<And>x. x \<in> I \<Longrightarrow> x \<in> EF s
[PROOF STEP]
show "\<And>x::'s. x \<in> I \<Longrightarrow> \<exists>i::'s\<in>I. (i, x) \<in> {(x::'s, y::'s). x \<rightarrow>\<^sub>i y}\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> I \<Longrightarrow> \<exists>i\<in>I. (i, x) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*
[PROOF STEP]
by (rule_tac x = x in bexI, simp)
[PROOF STATE]
proof (state)
this:
?x \<in> I \<Longrightarrow> \<exists>i\<in>I. (i, ?x) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*

goal (1 subgoal):
 1. \<And>x. x \<in> I \<Longrightarrow> x \<in> EF s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> I \<Longrightarrow> x \<in> EF s
[PROOF STEP]
show "\<And>x::'s. x \<in> I \<Longrightarrow> x \<in> EF s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> I \<Longrightarrow> x \<in> EF s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<turnstile>A
attack A = (I, s)

goal (1 subgoal):
 1. \<And>x. x \<in> I \<Longrightarrow> x \<in> EF s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> I; \<turnstile>A; attack A = (I, s)\<rbrakk> \<Longrightarrow> x \<in> EF s
[PROOF STEP]
have a: "\<forall> x \<in> I. \<exists> y \<in> s. x \<rightarrow>\<^sub>i* y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<turnstile>A
attack A = (I, s)

goal (1 subgoal):
 1. \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile>A; attack A = (I, s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y
[PROOF STEP]
have "\<forall>x::'s\<in>fst (attack A). \<exists>y::'s. y \<in> snd (attack A) \<and> x \<rightarrow>\<^sub>i* y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>fst (attack A). \<exists>y. y \<in> snd (attack A) \<and> x \<rightarrow>\<^sub>i* y
[PROOF STEP]
by (rule att_elem_seq0, rule assms)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>fst (attack A). \<exists>y. y \<in> snd (attack A) \<and> x \<rightarrow>\<^sub>i* y

goal (1 subgoal):
 1. \<lbrakk>\<turnstile>A; attack A = (I, s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y
[PROOF STEP]
thus " \<forall>x::'s\<in>I. \<exists>y::'s\<in>s. x \<rightarrow>\<^sub>i* y"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>fst (attack A). \<exists>y. y \<in> snd (attack A) \<and> x \<rightarrow>\<^sub>i* y

goal (1 subgoal):
 1. \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>fst (attack A). \<exists>y. y \<in> snd (attack A) \<and> x \<rightarrow>\<^sub>i* y
\<turnstile>A
attack A = (I, s)

goal (1 subgoal):
 1. \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> I; \<turnstile>A; attack A = (I, s)\<rbrakk> \<Longrightarrow> x \<in> EF s
[PROOF STEP]
thus "\<And>x::'s. x \<in> I \<Longrightarrow> x \<in> EF s"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y

goal (1 subgoal):
 1. \<And>x. x \<in> I \<Longrightarrow> x \<in> EF s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> I; \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> x \<in> EF s
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> I; \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> x \<in> EF s
[PROOF STEP]
assume b: "x \<in> I"
[PROOF STATE]
proof (state)
this:
x \<in> I

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> I; \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> x \<in> EF s
[PROOF STEP]
have "\<exists>y::'s\<in>s::('s :: state) set. x \<rightarrow>\<^sub>i* y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y
[PROOF STEP]
by (rule_tac x = x and A = I in bspec, rule a, rule b)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>s. x \<rightarrow>\<^sub>i* y

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> I; \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> x \<in> EF s
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>s. x \<rightarrow>\<^sub>i* y
[PROOF STEP]
obtain y where "y \<in> s" and "x \<rightarrow>\<^sub>i* y"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>s. x \<rightarrow>\<^sub>i* y

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> s; x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule bexE)
[PROOF STATE]
proof (state)
this:
y \<in> s
x \<rightarrow>\<^sub>i* y

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> I; \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> x \<in> EF s
[PROOF STEP]
thus "x \<in> EF s"
[PROOF STATE]
proof (prove)
using this:
y \<in> s
x \<rightarrow>\<^sub>i* y

goal (1 subgoal):
 1. x \<in> EF s
[PROOF STEP]
by (erule_tac f = s in EF_step_star)
[PROOF STATE]
proof (state)
this:
x \<in> EF s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> I \<Longrightarrow> ?x \<in> EF s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> I \<Longrightarrow> ?x \<in> EF s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
I \<subseteq> {sa. (\<exists>i\<in>I. i \<rightarrow>\<^sub>i* sa) \<and> sa \<in> EF s}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ATV_EF: "\<lbrakk> \<turnstile>\<^sub>V A; (I,s) = attack A \<rbrakk> \<Longrightarrow>
 (Kripke {s. \<exists> i \<in> I. (i \<rightarrow>\<^sub>i* s) } I  \<turnstile> EF s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile>\<^sub>V A; (I, s) = attack A\<rbrakk> \<Longrightarrow> Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s
[PROOF STEP]
by (metis (full_types) AT_EF ref_pres_att ref_validity_def valid_ref_def)


[STATEMENT]
lemma Compl_step1:
"Kripke {s :: ('s :: state). \<exists> i \<in> I. (i \<rightarrow>\<^sub>i* s)} I  \<turnstile> EF s
\<Longrightarrow> \<forall> x \<in> I. \<exists> y \<in> s. x \<rightarrow>\<^sub>i* y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Kripke {s. \<exists>i\<in>I. i \<rightarrow>\<^sub>i* s} I \<turnstile> EF s \<Longrightarrow> \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y
[PROOF STEP]
by (simp add: EF_step_star_rev valEF_E)


[STATEMENT]
lemma rtrancl_imp_singleton_seq2: "x \<rightarrow>\<^sub>i* y \<Longrightarrow>
          x = y \<or> (\<exists> s. s \<noteq> [] \<and> (tl s \<noteq> []) \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and>
               (\<forall> i < (length s - 1). (s ! i) \<rightarrow>\<^sub>i (s ! (Suc i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<rightarrow>\<^sub>i* y \<Longrightarrow> x = y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
unfolding state_transition_refl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>* \<Longrightarrow> x = y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
proof (induction rule: rtrancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = x \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = x \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
 2. \<And>y z. \<lbrakk>(x, y) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*; (y, z) \<in> {(x, y). x \<rightarrow>\<^sub>i y}; x = y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. x = x \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = x \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
 2. \<And>y z. \<lbrakk>(x, y) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*; (y, z) \<in> {(x, y). x \<rightarrow>\<^sub>i y}; x = y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = x \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = x \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = x \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*; (y, z) \<in> {(x, y). x \<rightarrow>\<^sub>i y}; x = y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*; (y, z) \<in> {(x, y). x \<rightarrow>\<^sub>i y}; x = y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*
(y, z) \<in> {(x, y). x \<rightarrow>\<^sub>i y}
x = y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*; (y, z) \<in> {(x, y). x \<rightarrow>\<^sub>i y}; x = y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
using step.IH
[PROOF STATE]
proof (prove)
using this:
x = y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))

goal (1 subgoal):
 1. x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
proof (elim disjE exE conjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
 2. \<And>s. \<lbrakk>s \<noteq> []; tl s \<noteq> []; s ! 0 = x; s ! (length s - 1) = y; \<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
assume "x=y"
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
 2. \<And>s. \<lbrakk>s \<noteq> []; tl s \<noteq> []; s ! 0 = x; s ! (length s - 1) = y; \<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
with step.hyps
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*
(y, z) \<in> {(x, y). x \<rightarrow>\<^sub>i y}
x = y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*
(y, z) \<in> {(x, y). x \<rightarrow>\<^sub>i y}
x = y

goal (1 subgoal):
 1. x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
by (force intro!: exI [where x="[y,z]"])
[PROOF STATE]
proof (state)
this:
x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<noteq> []; tl s \<noteq> []; s ! 0 = x; s ! (length s - 1) = y; \<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<noteq> []; tl s \<noteq> []; s ! 0 = x; s ! (length s - 1) = y; \<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
show "\<And>s. \<lbrakk>s \<noteq> []; tl s \<noteq> []; s ! 0 = x;
          s ! (length s - 1) = y;
          \<forall>i<length s - 1.
             s ! i \<rightarrow>\<^sub>i s ! Suc i\<rbrakk>
         \<Longrightarrow> x = z \<or>
             (\<exists>s. s \<noteq> [] \<and>
                  tl s \<noteq> [] \<and> s ! 0 = x \<and>
                  s ! (length s - 1) = z \<and>
                  (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<noteq> []; tl s \<noteq> []; s ! 0 = x; s ! (length s - 1) = y; \<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<noteq> []; tl s \<noteq> []; s ! 0 = x; s ! (length s - 1) = y; \<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i\<rbrakk> \<Longrightarrow> \<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i)
[PROOF STEP]
apply (rule_tac x="s @ [z]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<noteq> []; tl s \<noteq> []; s ! 0 = x; s ! (length s - 1) = y; \<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i\<rbrakk> \<Longrightarrow> s @ [z] \<noteq> [] \<and> tl (s @ [z]) \<noteq> [] \<and> (s @ [z]) ! 0 = x \<and> (s @ [z]) ! (length (s @ [z]) - 1) = z \<and> (\<forall>i<length (s @ [z]) - 1. (s @ [z]) ! i \<rightarrow>\<^sub>i (s @ [z]) ! Suc i)
[PROOF STEP]
apply (auto simp: nth_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s i. \<lbrakk>s \<noteq> []; tl s \<noteq> []; \<forall>i<length s - Suc 0. s ! i \<rightarrow>\<^sub>i s ! Suc i; x = s ! 0; y = s ! (length s - Suc 0); \<not> Suc i < length s; i < length s\<rbrakk> \<Longrightarrow> s ! i \<rightarrow>\<^sub>i z
[PROOF STEP]
by (metis One_nat_def Suc_lessI diff_Suc_1 mem_Collect_eq old.prod.case step.hyps(2))
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s \<noteq> []; tl ?s \<noteq> []; ?s ! 0 = x; ?s ! (length ?s - 1) = y; \<forall>i<length ?s - 1. ?s ! i \<rightarrow>\<^sub>i ?s ! Suc i\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = z \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = x \<and> s ! (length s - 1) = z \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tl_nempty_length[rule_format]: "s \<noteq> [] \<longrightarrow> tl s \<noteq> [] \<longrightarrow> 0 < length s - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> [] \<longrightarrow> tl s \<noteq> [] \<longrightarrow> 0 < length s - 1
[PROOF STEP]
by (induction s, simp+)


[STATEMENT]
lemma tl_nempty_length2[rule_format]: "s \<noteq> [] \<longrightarrow> tl s \<noteq> [] \<longrightarrow> Suc 0 < length s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> [] \<longrightarrow> tl s \<noteq> [] \<longrightarrow> Suc 0 < length s
[PROOF STEP]
by (induction s, simp+)


[STATEMENT]
lemma length_last[rule_format]: "(l @ [x]) ! (length (l @ [x]) - 1) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l @ [x]) ! (length (l @ [x]) - 1) = x
[PROOF STEP]
by (induction l, simp+)


[STATEMENT]
lemma Compl_step2: "\<forall> x \<in> I. \<exists> y \<in> s. x \<rightarrow>\<^sub>i* y \<Longrightarrow>
                   ( \<forall> x \<in> I.  x \<in> s \<or> (\<exists> (sl :: ((('s :: state) set)list)).
                  (sl \<noteq> []) \<and> (tl sl \<noteq> []) \<and>
                 (sl ! 0, sl ! (length sl - 1)) = ({x},s) \<and>
                 (\<forall> i < (length sl - 1).  \<turnstile> \<N>\<^bsub>(sl ! i,sl ! (i+1) )\<^esub>
                         )))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>I. \<exists>y\<in>s. x \<rightarrow>\<^sub>i* y \<Longrightarrow> \<forall>x\<in>I. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
proof (rule ballI, drule_tac x = x in bspec, assumption, erule bexE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> I; y \<in> s; x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> I; y \<in> s; x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
assume a: "x \<in> I" and b: "y \<in> s" and  c: "x \<rightarrow>\<^sub>i* y"
[PROOF STATE]
proof (state)
this:
x \<in> I
y \<in> s
x \<rightarrow>\<^sub>i* y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> I; y \<in> s; x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
show "x \<in> s \<or>
       (\<exists>sl::'s set list.
           sl \<noteq> [] \<and>
           tl sl \<noteq> [] \<and>
           (sl ! (0), sl ! (length sl - (1))) = ({x}, s) \<and>
           (\<forall>i<length sl - (1). \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + (1)))\<^esub>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
have d : "x = y \<or>
       (\<exists>s'. s' \<noteq> [] \<and>
           tl s' \<noteq> [] \<and>
           s' ! (0) = x \<and>
           s' ! (length s' - (1)) = y \<and> (\<forall>i<length s' - (1). s' ! i \<rightarrow>\<^sub>i s' ! Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y \<or> (\<exists>s'. s' \<noteq> [] \<and> tl s' \<noteq> [] \<and> s' ! 0 = x \<and> s' ! (length s' - 1) = y \<and> (\<forall>i<length s' - 1. s' ! i \<rightarrow>\<^sub>i s' ! Suc i))
[PROOF STEP]
using c rtrancl_imp_singleton_seq2
[PROOF STATE]
proof (prove)
using this:
x \<rightarrow>\<^sub>i* y
?x \<rightarrow>\<^sub>i* ?y \<Longrightarrow> ?x = ?y \<or> (\<exists>s. s \<noteq> [] \<and> tl s \<noteq> [] \<and> s ! 0 = ?x \<and> s ! (length s - 1) = ?y \<and> (\<forall>i<length s - 1. s ! i \<rightarrow>\<^sub>i s ! Suc i))

goal (1 subgoal):
 1. x = y \<or> (\<exists>s'. s' \<noteq> [] \<and> tl s' \<noteq> [] \<and> s' ! 0 = x \<and> s' ! (length s' - 1) = y \<and> (\<forall>i<length s' - 1. s' ! i \<rightarrow>\<^sub>i s' ! Suc i))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = y \<or> (\<exists>s'. s' \<noteq> [] \<and> tl s' \<noteq> [] \<and> s' ! 0 = x \<and> s' ! (length s' - 1) = y \<and> (\<forall>i<length s' - 1. s' ! i \<rightarrow>\<^sub>i s' ! Suc i))

goal (1 subgoal):
 1. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
thus "x \<in> s \<or>
       (\<exists>sl::'s set list.
           sl \<noteq> [] \<and>
           tl sl \<noteq> [] \<and>
           (sl ! (0), sl ! (length sl - (1))) = ({x}, s) \<and>
           (\<forall>i<length sl - (1). \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + (1)))\<^esub>))"
[PROOF STATE]
proof (prove)
using this:
x = y \<or> (\<exists>s'. s' \<noteq> [] \<and> tl s' \<noteq> [] \<and> s' ! 0 = x \<and> s' ! (length s' - 1) = y \<and> (\<forall>i<length s' - 1. s' ! i \<rightarrow>\<^sub>i s' ! Suc i))

goal (1 subgoal):
 1. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
apply (rule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x = y \<Longrightarrow> x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
 2. \<exists>s'. s' \<noteq> [] \<and> tl s' \<noteq> [] \<and> s' ! 0 = x \<and> s' ! (length s' - 1) = y \<and> (\<forall>i<length s' - 1. s' ! i \<rightarrow>\<^sub>i s' ! Suc i) \<Longrightarrow> x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
y \<in> s

goal (2 subgoals):
 1. x = y \<Longrightarrow> x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
 2. \<exists>s'. s' \<noteq> [] \<and> tl s' \<noteq> [] \<and> s' ! 0 = x \<and> s' ! (length s' - 1) = y \<and> (\<forall>i<length s' - 1. s' ! i \<rightarrow>\<^sub>i s' ! Suc i) \<Longrightarrow> x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s'. s' \<noteq> [] \<and> tl s' \<noteq> [] \<and> s' ! 0 = x \<and> s' ! (length s' - 1) = y \<and> (\<forall>i<length s' - 1. s' ! i \<rightarrow>\<^sub>i s' ! Suc i) \<Longrightarrow> x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))
[PROOF STEP]
apply (rule disjI2, elim conjE exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>s' \<noteq> []; tl s' \<noteq> []; s' ! 0 = x; s' ! (length s' - 1) = y; \<forall>i<length s' - 1. s' ! i \<rightarrow>\<^sub>i s' ! Suc i\<rbrakk> \<Longrightarrow> \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>)
[PROOF STEP]
apply (rule_tac x = "[{s' ! j}. j \<leftarrow> [0..<(length s' - 1)]] @ [s]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>s' \<noteq> []; tl s' \<noteq> []; s' ! 0 = x; s' ! (length s' - 1) = y; \<forall>i<length s' - 1. s' ! i \<rightarrow>\<^sub>i s' ! Suc i\<rbrakk> \<Longrightarrow> map (\<lambda>j. {s' ! j}) [0..<length s' - 1] @ [s] \<noteq> [] \<and> tl (map (\<lambda>j. {s' ! j}) [0..<length s' - 1] @ [s]) \<noteq> [] \<and> ((map (\<lambda>j. {s' ! j}) [0..<length s' - 1] @ [s]) ! 0, (map (\<lambda>j. {s' ! j}) [0..<length s' - 1] @ [s]) ! (length (map (\<lambda>j. {s' ! j}) [0..<length s' - 1] @ [s]) - 1)) = ({x}, s) \<and> (\<forall>i<length (map (\<lambda>j. {s' ! j}) [0..<length s' - 1] @ [s]) - 1. \<turnstile>\<N>\<^bsub>((map (\<lambda>j. {s' ! j}) [0..<length s' - 1] @ [s]) ! i, (map (\<lambda>j. {s' ! j}) [0..<length s' - 1] @ [s]) ! (i + 1))\<^esub>)
[PROOF STEP]
apply (auto simp: nth_append)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s' i. \<lbrakk>s' \<noteq> []; tl s' \<noteq> []; \<forall>i<length s' - Suc 0. s' ! i \<rightarrow>\<^sub>i s' ! Suc i; x = s' ! 0; y = s' ! (length s' - Suc 0); Suc 0 < length s'; Suc i < length s' - Suc 0\<rbrakk> \<Longrightarrow> \<turnstile>\<N>\<^bsub>({s' ! i}, {s' ! Suc i})\<^esub>
 2. \<And>s' i. \<lbrakk>s' \<noteq> []; tl s' \<noteq> []; \<forall>i<length s' - Suc 0. s' ! i \<rightarrow>\<^sub>i s' ! Suc i; x = s' ! 0; y = s' ! (length s' - Suc 0); Suc 0 < length s'; \<not> Suc i < length s' - Suc 0; i < length s' - Suc 0\<rbrakk> \<Longrightarrow> \<turnstile>\<N>\<^bsub>({s' ! i}, s)\<^esub>
 3. \<And>s'. \<lbrakk>s' \<noteq> []; tl s' \<noteq> []; \<forall>i<length s' - Suc 0. s' ! i \<rightarrow>\<^sub>i s' ! Suc i; x = s' ! 0; y = s' ! (length s' - Suc 0)\<rbrakk> \<Longrightarrow> Suc 0 < length s'
[PROOF STEP]
apply (metis AT.att_base Suc_lessD fst_conv prod.sel(2) singletonD singletonI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s' i. \<lbrakk>s' \<noteq> []; tl s' \<noteq> []; \<forall>i<length s' - Suc 0. s' ! i \<rightarrow>\<^sub>i s' ! Suc i; x = s' ! 0; y = s' ! (length s' - Suc 0); Suc 0 < length s'; \<not> Suc i < length s' - Suc 0; i < length s' - Suc 0\<rbrakk> \<Longrightarrow> \<turnstile>\<N>\<^bsub>({s' ! i}, s)\<^esub>
 2. \<And>s'. \<lbrakk>s' \<noteq> []; tl s' \<noteq> []; \<forall>i<length s' - Suc 0. s' ! i \<rightarrow>\<^sub>i s' ! Suc i; x = s' ! 0; y = s' ! (length s' - Suc 0)\<rbrakk> \<Longrightarrow> Suc 0 < length s'
[PROOF STEP]
apply (metis AT.att_base Suc_lessI b fst_conv prod.sel(2) singletonD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>s' \<noteq> []; tl s' \<noteq> []; \<forall>i<length s' - Suc 0. s' ! i \<rightarrow>\<^sub>i s' ! Suc i; x = s' ! 0; y = s' ! (length s' - Suc 0)\<rbrakk> \<Longrightarrow> Suc 0 < length s'
[PROOF STEP]
using tl_nempty_length2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s \<noteq> []; tl ?s \<noteq> []\<rbrakk> \<Longrightarrow> Suc 0 < length ?s

goal (1 subgoal):
 1. \<And>s'. \<lbrakk>s' \<noteq> []; tl s' \<noteq> []; \<forall>i<length s' - Suc 0. s' ! i \<rightarrow>\<^sub>i s' ! Suc i; x = s' ! 0; y = s' ! (length s' - Suc 0)\<rbrakk> \<Longrightarrow> Suc 0 < length s'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_hd_lem[rule_format] : "n > 0 \<longrightarrow> (f 0 #  map (\<lambda>i. f i) [1..<n]) = map  (\<lambda>i. f i) [0..<n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<longrightarrow> f 0 # map f [1..<n] = map f [0..<n]
[PROOF STEP]
by (simp add : hd_map upt_rec)


[STATEMENT]
lemma map_Suc_lem[rule_format] : "n > 0 \<longrightarrow> map (\<lambda> i:: nat. f i)[1..<n] =
                                  map (\<lambda> i:: nat. f(Suc i))[0..<(n - 1)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<longrightarrow> map f [1..<n] = map (\<lambda>i. f (Suc i)) [0..<n - 1]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < n \<longrightarrow> map f [1..<n] = map (\<lambda>i. f (Suc i)) [0..<n - 1]
[PROOF STEP]
have "(f 0 # map (\<lambda>n. f (Suc n)) [0..<n - 1] = f 0 # map f [1..<n]) = (map (\<lambda>n. f (Suc n)) [0..<n - 1] = map f [1..<n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f 0 # map (\<lambda>n. f (Suc n)) [0..<n - 1] = f 0 # map f [1..<n]) = (map (\<lambda>n. f (Suc n)) [0..<n - 1] = map f [1..<n])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(f 0 # map (\<lambda>n. f (Suc n)) [0..<n - 1] = f 0 # map f [1..<n]) = (map (\<lambda>n. f (Suc n)) [0..<n - 1] = map f [1..<n])

goal (1 subgoal):
 1. 0 < n \<longrightarrow> map f [1..<n] = map (\<lambda>i. f (Suc i)) [0..<n - 1]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f 0 # map (\<lambda>n. f (Suc n)) [0..<n - 1] = f 0 # map f [1..<n]) = (map (\<lambda>n. f (Suc n)) [0..<n - 1] = map f [1..<n])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f 0 # map (\<lambda>n. f (Suc n)) [0..<n - 1] = f 0 # map f [1..<n]) = (map (\<lambda>n. f (Suc n)) [0..<n - 1] = map f [1..<n])

goal (1 subgoal):
 1. 0 < n \<longrightarrow> map f [1..<n] = map (\<lambda>i. f (Suc i)) [0..<n - 1]
[PROOF STEP]
by (metis Suc_pred' map_hd_lem map_upt_Suc)
[PROOF STATE]
proof (state)
this:
0 < n \<longrightarrow> map f [1..<n] = map (\<lambda>i. f (Suc i)) [0..<n - 1]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma forall_ex_fun: "finite S \<Longrightarrow> (\<forall> x \<in> S. (\<exists> y. P y x)) \<longrightarrow> (\<exists> f. \<forall> x \<in> S. P (f x) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> (\<forall>x\<in>S. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>S. P (f x) x)
[PROOF STEP]
proof (induction rule: finite.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<forall>x\<in>{}. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>{}. P (f x) x)
 2. \<And>A a. \<lbrakk>finite A; (\<forall>x\<in>A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>A. P (f x) x)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>insert a A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>insert a A. P (f x) x)
[PROOF STEP]
case emptyI
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<forall>x\<in>{}. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>{}. P (f x) x)
 2. \<And>A a. \<lbrakk>finite A; (\<forall>x\<in>A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>A. P (f x) x)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>insert a A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>insert a A. P (f x) x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{}. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>{}. P (f x) x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>{}. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>{}. P (f x) x)

goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; (\<forall>x\<in>A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>A. P (f x) x)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>insert a A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>insert a A. P (f x) x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; (\<forall>x\<in>A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>A. P (f x) x)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>insert a A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>insert a A. P (f x) x)
[PROOF STEP]
case (insertI F x)
[PROOF STATE]
proof (state)
this:
finite F
(\<forall>x\<in>F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>F. P (f x) x)

goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; (\<forall>x\<in>A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>A. P (f x) x)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>insert a A. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>insert a A. P (f x) x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite F
(\<forall>x\<in>F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>F. P (f x) x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite F
(\<forall>x\<in>F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>F. P (f x) x)

goal (1 subgoal):
 1. (\<forall>x\<in>insert x F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>insert x F. P (f x) x)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>finite F; (\<forall>x\<in>F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>F. P (f x) x); \<forall>x\<in>insert x F. \<exists>y. P y x\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>x\<in>insert x F. P (f x) x
[PROOF STEP]
assume d: "(\<forall>x::'a\<in>insert x F. \<exists>y::'b. P y x)"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>insert x F. \<exists>y. P y x

goal (1 subgoal):
 1. \<lbrakk>finite F; (\<forall>x\<in>F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>F. P (f x) x); \<forall>x\<in>insert x F. \<exists>y. P y x\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>x\<in>insert x F. P (f x) x
[PROOF STEP]
have "(\<forall>x::'a\<in>F. \<exists>y::'b. P y x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>F. \<exists>y. P y x
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert x F. \<exists>y. P y x

goal (1 subgoal):
 1. \<forall>x\<in>F. \<exists>y. P y x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>F. \<exists>y. P y x

goal (1 subgoal):
 1. \<lbrakk>finite F; (\<forall>x\<in>F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>F. P (f x) x); \<forall>x\<in>insert x F. \<exists>y. P y x\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>x\<in>insert x F. P (f x) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>F. \<exists>y. P y x
[PROOF STEP]
obtain f where f: "\<forall>x::'a\<in>F. P (f x) x"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>F. \<exists>y. P y x

goal (1 subgoal):
 1. (\<And>f. \<forall>x\<in>F. P (f x) x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insertI.IH
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>F. \<exists>y. P y x
(\<forall>x\<in>F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>F. P (f x) x)

goal (1 subgoal):
 1. (\<And>f. \<forall>x\<in>F. P (f x) x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>F. P (f x) x

goal (1 subgoal):
 1. \<lbrakk>finite F; (\<forall>x\<in>F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>F. P (f x) x); \<forall>x\<in>insert x F. \<exists>y. P y x\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>x\<in>insert x F. P (f x) x
[PROOF STEP]
from d
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>insert x F. \<exists>y. P y x
[PROOF STEP]
obtain y where "P y x"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert x F. \<exists>y. P y x

goal (1 subgoal):
 1. (\<And>y. P y x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P y x

goal (1 subgoal):
 1. \<lbrakk>finite F; (\<forall>x\<in>F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>F. P (f x) x); \<forall>x\<in>insert x F. \<exists>y. P y x\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>x\<in>insert x F. P (f x) x
[PROOF STEP]
thus "(\<exists>f::'a \<Rightarrow> 'b. \<forall>x::'a\<in>insert x F. P (f x) x)"
[PROOF STATE]
proof (prove)
using this:
P y x

goal (1 subgoal):
 1. \<exists>f. \<forall>x\<in>insert x F. P (f x) x
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
P y x
\<forall>x\<in>F. P (f x) x

goal (1 subgoal):
 1. \<exists>f. \<forall>x\<in>insert x F. P (f x) x
[PROOF STEP]
by (rule_tac x = "\<lambda> z. if z = x then y else f z" in exI, simp)
[PROOF STATE]
proof (state)
this:
\<exists>f. \<forall>x\<in>insert x F. P (f x) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>insert x F. \<exists>y. P y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>insert x F. P (f x) x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nodup_all_lem[rule_format]:
  "nodup_all (x1 # a # l) \<longrightarrow> (insert x1 (insert a (set l)) - {x1}) = insert a (set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodup_all (x1 # a # l) \<longrightarrow> insert x1 (insert a (set l)) - {x1} = insert a (set l)
[PROOF STEP]
by (induction l, (simp add: nodup_all_def)+)


[STATEMENT]
lemma nodup_all_tl[rule_format]: "nodup_all (x # l) \<longrightarrow> nodup_all l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodup_all (x # l) \<longrightarrow> nodup_all l
[PROOF STEP]
by (induction l, (simp add: nodup_all_def)+)


[STATEMENT]
lemma finite_nodup: "finite I \<Longrightarrow> \<exists> l. set l = I \<and> nodup_all l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite I \<Longrightarrow> \<exists>l. set l = I \<and> nodup_all l
[PROOF STEP]
proof (induction rule: finite.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>l. set l = {} \<and> nodup_all l
 2. \<And>A a. \<lbrakk>finite A; \<exists>l. set l = A \<and> nodup_all l\<rbrakk> \<Longrightarrow> \<exists>l. set l = insert a A \<and> nodup_all l
[PROOF STEP]
case emptyI
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<exists>l. set l = {} \<and> nodup_all l
 2. \<And>A a. \<lbrakk>finite A; \<exists>l. set l = A \<and> nodup_all l\<rbrakk> \<Longrightarrow> \<exists>l. set l = insert a A \<and> nodup_all l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. set l = {} \<and> nodup_all l
[PROOF STEP]
by (simp add: nodup_all_def)
[PROOF STATE]
proof (state)
this:
\<exists>l. set l = {} \<and> nodup_all l

goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; \<exists>l. set l = A \<and> nodup_all l\<rbrakk> \<Longrightarrow> \<exists>l. set l = insert a A \<and> nodup_all l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; \<exists>l. set l = A \<and> nodup_all l\<rbrakk> \<Longrightarrow> \<exists>l. set l = insert a A \<and> nodup_all l
[PROOF STEP]
case (insertI A a)
[PROOF STATE]
proof (state)
this:
finite A
\<exists>l. set l = A \<and> nodup_all l

goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; \<exists>l. set l = A \<and> nodup_all l\<rbrakk> \<Longrightarrow> \<exists>l. set l = insert a A \<and> nodup_all l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite A
\<exists>l. set l = A \<and> nodup_all l
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite A
\<exists>l. set l = A \<and> nodup_all l

goal (1 subgoal):
 1. \<exists>l. set l = insert a A \<and> nodup_all l
[PROOF STEP]
by (metis insertE insert_absorb list.simps(15) nodup_all_def nodup_step)
[PROOF STATE]
proof (state)
this:
\<exists>l. set l = insert a A \<and> nodup_all l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Compl_step3: "I \<noteq> {} \<Longrightarrow> finite I \<Longrightarrow>
     ( \<forall> x \<in> I.  x \<in> s \<or> (\<exists> (sl :: ((('s :: state) set)list)).
                  (sl \<noteq> []) \<and> (tl sl \<noteq> []) \<and>
                 (sl ! 0, sl ! (length sl - 1)) = ({x},s) \<and>
                 (\<forall> i < (length sl - 1).  \<turnstile> \<N>\<^bsub>(sl ! i,sl ! (i+1) )\<^esub>
                         )) \<Longrightarrow>
     (\<exists> lI. set lI = {x :: 's :: state. 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>
                         ))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; \<forall>x\<in>I. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))\<rbrakk> \<Longrightarrow> \<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>)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; \<forall>x\<in>I. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))\<rbrakk> \<Longrightarrow> \<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>)))
[PROOF STEP]
assume i: "I \<noteq> {}" and f: "finite I" and
      fa: "\<forall>x::'s\<in>I.
       x \<in> s \<or>
       (\<exists>sl::'s set list.
           sl \<noteq> [] \<and>
           tl sl \<noteq> [] \<and>
           (sl ! (0), sl ! (length sl - (1))) = ({x}, s) \<and>
           (\<forall>i<length sl - (1). \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + (1)))\<^esub>))"
[PROOF STATE]
proof (state)
this:
I \<noteq> {}
finite I
\<forall>x\<in>I. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))

goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; \<forall>x\<in>I. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))\<rbrakk> \<Longrightarrow> \<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>)))
[PROOF STEP]
have a: "\<exists> lI. set lI = {x::'s \<in> I. x \<notin> s} \<and> nodup_all lI"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lI. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI
[PROOF STEP]
by (simp add: f finite_nodup)
[PROOF STATE]
proof (state)
this:
\<exists>lI. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI

goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; \<forall>x\<in>I. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))\<rbrakk> \<Longrightarrow> \<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>)))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>lI. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI
[PROOF STEP]
obtain lI where b: "set lI = {x::'s \<in> I. x \<notin> s} \<and> nodup_all lI"
[PROOF STATE]
proof (prove)
using this:
\<exists>lI. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI

goal (1 subgoal):
 1. (\<And>lI. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule exE)
[PROOF STATE]
proof (state)
this:
set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI

goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; finite I; \<forall>x\<in>I. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))\<rbrakk> \<Longrightarrow> \<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>)))
[PROOF STEP]
thus "\<exists>lI::'s list.
       set lI = {x::'s \<in> I. x \<notin> s} \<and>
       (\<exists>Sj::'s 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>)))"
[PROOF STATE]
proof (prove)
using this:
set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI

goal (1 subgoal):
 1. \<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>)))
[PROOF STEP]
apply (rule_tac x = lI in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI \<Longrightarrow> 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>)))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI \<Longrightarrow> set lI = {x \<in> I. x \<notin> s}
 2. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI \<Longrightarrow> \<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>))
[PROOF STEP]
apply (erule conjE, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI \<Longrightarrow> \<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>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI \<Longrightarrow> \<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>))
[PROOF STEP]
have c:  "\<forall> x \<in> set(lI). (\<exists> sl::'s set list.
              sl \<noteq> [] \<and>
              tl sl \<noteq> [] \<and>
              (sl ! (0), sl ! (length sl - (1))) = ({x}, s) \<and>
              (\<forall>i<length sl - (1). \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + (1)))\<^esub>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>)
[PROOF STEP]
using b fa
[PROOF STATE]
proof (prove)
using this:
set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI
\<forall>x\<in>I. x \<in> s \<or> (\<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>))

goal (1 subgoal):
 1. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>)

goal (1 subgoal):
 1. set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI \<Longrightarrow> \<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>))
[PROOF STEP]
thus "\<exists>Sj::'s 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>))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>)

goal (1 subgoal):
 1. \<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>))
[PROOF STEP]
apply (subgoal_tac "finite (set lI)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); finite (set lI)\<rbrakk> \<Longrightarrow> \<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>))
 2. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>) \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply (rotate_tac -1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite (set lI); \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>)\<rbrakk> \<Longrightarrow> \<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>))
 2. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>) \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply (drule forall_ex_fun)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); (\<forall>x\<in>set lI. \<exists>y. ?P2 y x) \<longrightarrow> (\<exists>f. \<forall>x\<in>set lI. ?P2 (f x) x)\<rbrakk> \<Longrightarrow> \<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>))
 2. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>) \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply (drule mp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>) \<Longrightarrow> \<forall>x\<in>set lI. \<exists>y. ?P2 y x
 2. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); \<exists>f. \<forall>x\<in>set lI. ?P2 (f x) x\<rbrakk> \<Longrightarrow> \<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>))
 3. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>) \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); \<exists>f. \<forall>x\<in>set lI. f x \<noteq> [] \<and> tl (f x) \<noteq> [] \<and> (f x ! 0, f x ! (length (f x) - 1)) = ({x}, s) \<and> (\<forall>i<length (f x) - 1. \<turnstile>\<N>\<^bsub>(f x ! i, f x ! (i + 1))\<^esub>)\<rbrakk> \<Longrightarrow> \<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>))
 2. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>) \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); \<forall>x\<in>set lI. f x \<noteq> [] \<and> tl (f x) \<noteq> [] \<and> (f x ! 0, f x ! (length (f x) - 1)) = ({x}, s) \<and> (\<forall>i<length (f x) - 1. \<turnstile>\<N>\<^bsub>(f x ! i, f x ! (i + 1))\<^esub>)\<rbrakk> \<Longrightarrow> \<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>))
 2. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>) \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply (rule_tac x = "[f (lI ! j). j \<leftarrow> [0..<(length lI)]]" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); \<forall>x\<in>set lI. f x \<noteq> [] \<and> tl (f x) \<noteq> [] \<and> (f x ! 0, f x ! (length (f x) - 1)) = ({x}, s) \<and> (\<forall>i<length (f x) - 1. \<turnstile>\<N>\<^bsub>(f x ! i, f x ! (i + 1))\<^esub>)\<rbrakk> \<Longrightarrow> length (map (\<lambda>j. f (lI ! j)) [0..<length lI]) = length lI \<and> nodup_all lI \<and> (\<forall>j<length (map (\<lambda>j. f (lI ! j)) [0..<length lI]). map (\<lambda>j. f (lI ! j)) [0..<length lI] ! j \<noteq> [] \<and> tl (map (\<lambda>j. f (lI ! j)) [0..<length lI] ! j) \<noteq> [] \<and> (map (\<lambda>j. f (lI ! j)) [0..<length lI] ! j ! 0, map (\<lambda>j. f (lI ! j)) [0..<length lI] ! j ! (length (map (\<lambda>j. f (lI ! j)) [0..<length lI] ! j) - 1)) = ({lI ! j}, s) \<and> (\<forall>i<length (map (\<lambda>j. f (lI ! j)) [0..<length lI] ! j) - 1. \<turnstile>\<N>\<^bsub>(map (\<lambda>j. f (lI ! j)) [0..<length lI] ! j ! i, map (\<lambda>j. f (lI ! j)) [0..<length lI] ! j ! (i + 1))\<^esub>))
 2. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>) \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> sl ! 0 = {x} \<and> sl ! (length sl - Suc 0) = s \<and> (\<forall>i<length sl - Suc 0. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! Suc i)\<^esub>); \<forall>x\<in>set lI. f x \<noteq> [] \<and> tl (f x) \<noteq> [] \<and> f x ! 0 = {x} \<and> f x ! (length (f x) - Suc 0) = s \<and> (\<forall>i<length (f x) - Suc 0. \<turnstile>\<N>\<^bsub>(f x ! i, f x ! Suc i)\<^esub>)\<rbrakk> \<Longrightarrow> nodup_all lI
 2. \<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>) \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply (insert b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> sl ! 0 = {x} \<and> sl ! (length sl - Suc 0) = s \<and> (\<forall>i<length sl - Suc 0. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! Suc i)\<^esub>); \<forall>x\<in>set lI. f x \<noteq> [] \<and> tl (f x) \<noteq> [] \<and> f x ! 0 = {x} \<and> f x ! (length (f x) - Suc 0) = s \<and> (\<forall>i<length (f x) - Suc 0. \<turnstile>\<N>\<^bsub>(f x ! i, f x ! Suc i)\<^esub>); set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI\<rbrakk> \<Longrightarrow> nodup_all lI
 2. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI\<rbrakk> \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply (erule conjE, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI\<rbrakk> \<Longrightarrow> finite (set lI)
[PROOF STEP]
apply (rule_tac A = "set lI" and B = I in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI\<rbrakk> \<Longrightarrow> set lI \<subseteq> I
 2. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI\<rbrakk> \<Longrightarrow> finite I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set lI. \<exists>sl. sl \<noteq> [] \<and> tl sl \<noteq> [] \<and> (sl ! 0, sl ! (length sl - 1)) = ({x}, s) \<and> (\<forall>i<length sl - 1. \<turnstile>\<N>\<^bsub>(sl ! i, sl ! (i + 1))\<^esub>); set lI = {x \<in> I. x \<notin> s} \<and> nodup_all lI\<rbrakk> \<Longrightarrow> finite I
[PROOF STEP]
by (rule f)
[PROOF STATE]
proof (state)
this:
\<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>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<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>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_one_tl_empty[rule_format]: "length l = Suc (0 :: nat) \<longrightarrow> tl l = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l = Suc 0 \<longrightarrow> tl l = []
[PROOF STEP]
by (induction l, simp+)


[STATEMENT]
lemma list_two_tl_not_empty[rule_format]: "\<forall> list. length l = Suc (Suc (length list)) \<longrightarrow> tl l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>list. length l = Suc (Suc (length list)) \<longrightarrow> tl l \<noteq> []
[PROOF STEP]
by (induction l, simp+, force)


[STATEMENT]
lemma or_empty: "\<turnstile>([] \<oplus>\<^sub>\<or>\<^bsup>({}, s)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>({}, s)\<^esup>
[PROOF STEP]
by (simp add: att_or)


[STATEMENT]
lemma list_or_upt[rule_format]:
 "\<forall> l . lI \<noteq> [] \<longrightarrow> length l = length lI \<longrightarrow> nodup_all lI \<longrightarrow>
  (\<forall> i < length lI. (\<turnstile> (l ! i)) \<and> (attack (l ! i) = ({lI ! i}, s)))
                \<longrightarrow> ( \<turnstile> (l \<oplus>\<^sub>\<or>\<^bsup>(set lI, s)\<^esup>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l. lI \<noteq> [] \<longrightarrow> length l = length lI \<longrightarrow> nodup_all lI \<longrightarrow> (\<forall>i<length lI. \<turnstile>l ! i \<and> attack (l ! i) = ({lI ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(set lI, s)\<^esup>
[PROOF STEP]
proof (induction lI, simp, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lI l. \<lbrakk>\<forall>l. lI \<noteq> [] \<longrightarrow> length l = length lI \<longrightarrow> nodup_all lI \<longrightarrow> (\<forall>i<length lI. \<turnstile>l ! i \<and> attack (l ! i) = ({lI ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(set lI, s)\<^esup>; a # lI \<noteq> []; length l = length (a # lI); nodup_all (a # lI); \<forall>i<length (a # lI). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # lI) ! i}, s)\<rbrakk> \<Longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(set (a # lI), s)\<^esup>
[PROOF STEP]
fix x1 x2 l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lI l. \<lbrakk>\<forall>l. lI \<noteq> [] \<longrightarrow> length l = length lI \<longrightarrow> nodup_all lI \<longrightarrow> (\<forall>i<length lI. \<turnstile>l ! i \<and> attack (l ! i) = ({lI ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(set lI, s)\<^esup>; a # lI \<noteq> []; length l = length (a # lI); nodup_all (a # lI); \<forall>i<length (a # lI). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # lI) ! i}, s)\<rbrakk> \<Longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(set (a # lI), s)\<^esup>
[PROOF STEP]
show "\<forall>l::'a attree list.
          x2 \<noteq> [] \<longrightarrow>
          length l = length x2 \<longrightarrow>
          nodup_all x2 \<longrightarrow>
          (\<forall>i<length x2. \<turnstile>(l ! i) \<and> attack (l ! i) = ({x2 ! i}, s)) \<longrightarrow> \<turnstile>(l \<oplus>\<^sub>\<or>\<^bsup>(set x2, s)\<^esup>) \<Longrightarrow>
       x1 # x2 \<noteq> [] \<Longrightarrow>
       length l = length (x1 # x2) \<Longrightarrow>
       nodup_all (x1 # x2) \<Longrightarrow>
       \<forall>i<length (x1 # x2). \<turnstile>(l ! i) \<and> attack (l ! i) = ({(x1 # x2) ! i}, s) \<Longrightarrow> \<turnstile>(l \<oplus>\<^sub>\<or>\<^bsup>(set (x1 # x2), s)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>l. x2 \<noteq> [] \<longrightarrow> length l = length x2 \<longrightarrow> nodup_all x2 \<longrightarrow> (\<forall>i<length x2. \<turnstile>l ! i \<and> attack (l ! i) = ({x2 ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(set x2, s)\<^esup>; x1 # x2 \<noteq> []; length l = length (x1 # x2); nodup_all (x1 # x2); \<forall>i<length (x1 # x2). \<turnstile>l ! i \<and> attack (l ! i) = ({(x1 # x2) ! i}, s)\<rbrakk> \<Longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(set (x1 # x2), s)\<^esup>
[PROOF STEP]
apply (case_tac x2, simp, subst att_or, case_tac l, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length l = Suc (Suc (length list)); nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>l ! i \<and> attack (l ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list\<rbrakk> \<Longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)), s)\<^esup>
[PROOF STEP]
text \<open>Case @{text \<open>\<forall>i<Suc (Suc (length list)). \<turnstile>l ! i \<and> attack (l ! i) = ({(x1 # a # list) ! i}, s) \<Longrightarrow>
       x2 = a # list \<Longrightarrow>  \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)), s)\<^esup>\<close>}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length l = Suc (Suc (length list)); nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>l ! i \<and> attack (l ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list\<rbrakk> \<Longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)), s)\<^esup>
[PROOF STEP]
apply (subst att_or, case_tac l, simp, clarify, simp, rename_tac lista, case_tac lista, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> \<turnstile>aa \<and> fst (attack aa) \<subseteq> insert x1 (insert a (set list)) \<and> snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>
[PROOF STEP]
text \<open>Remaining conjunct of three conditions: @{text \<open> \<turnstile>aa \<and>
       fst (attack aa) \<subseteq> insert x1 (insert a (set list)) \<and>
       snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>\<close>}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> \<turnstile>aa \<and> fst (attack aa) \<subseteq> insert x1 (insert a (set list)) \<and> snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> \<turnstile>aa
 2. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> fst (attack aa) \<subseteq> insert x1 (insert a (set list)) \<and> snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>
[PROOF STEP]
text \<open>First condition @{text \<open> \<turnstile>aa\<close>}\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> \<turnstile>aa
 2. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> fst (attack aa) \<subseteq> insert x1 (insert a (set list)) \<and> snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>
[PROOF STEP]
apply (drule_tac x = 0 in spec, drule mp, simp, (erule conjE)+, simp, rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> fst (attack aa) \<subseteq> insert x1 (insert a (set list))
 2. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>
[PROOF STEP]
text \<open>Second condition @{text \<open>fst (attack aa) \<subseteq> insert x1 (insert a (set list))\<close>}\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> fst (attack aa) \<subseteq> insert x1 (insert a (set list))
 2. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>
[PROOF STEP]
apply (drule_tac x = 0 in spec, drule mp, simp, erule conjE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>
[PROOF STEP]
text \<open>The remaining conditions

          @{text \<open>snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>\<close>}

          are solved automatically!\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista ab listb. \<lbrakk>\<forall>l. length l = Suc (length list) \<longrightarrow> nodup_all (a # list) \<longrightarrow> (\<forall>i<Suc (length list). \<turnstile>l ! i \<and> attack (l ! i) = ({(a # list) ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(insert a (set list), s)\<^esup>; length listb = length list; nodup_all (x1 # a # list); \<forall>i<Suc (Suc (length list)). \<turnstile>(aa # ab # listb) ! i \<and> attack ((aa # ab # listb) ! i) = ({(x1 # a # list) ! i}, s); x2 = a # list; l = aa # ab # listb; lista = ab # listb\<rbrakk> \<Longrightarrow> snd (attack aa) \<subseteq> s \<and> \<turnstile>ab # listb \<oplus>\<^sub>\<or>\<^bsup>(insert x1 (insert a (set list)) - fst (attack aa), s)\<^esup>
[PROOF STEP]
by (metis Suc_mono add.right_neutral add_Suc_right list.size(4) nodup_all_lem nodup_all_tl nth_Cons_0 nth_Cons_Suc order_refl prod.sel(1) prod.sel(2) zero_less_Suc)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>l. x2 \<noteq> [] \<longrightarrow> length l = length x2 \<longrightarrow> nodup_all x2 \<longrightarrow> (\<forall>i<length x2. \<turnstile>l ! i \<and> attack (l ! i) = ({x2 ! i}, s)) \<longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(set x2, s)\<^esup>; x1 # x2 \<noteq> []; length l = length (x1 # x2); nodup_all (x1 # x2); \<forall>i<length (x1 # x2). \<turnstile>l ! i \<and> attack (l ! i) = ({(x1 # x2) ! i}, s)\<rbrakk> \<Longrightarrow> \<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(set (x1 # x2), s)\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma app_tl_empty_hd[rule_format]: "tl (l @ [a]) = [] \<longrightarrow> hd (l @ [a]) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (l @ [a]) = [] \<longrightarrow> hd (l @ [a]) = a
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma tl_hd_empty[rule_format]: "tl (l @ [a]) = [] \<longrightarrow> l = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (l @ [a]) = [] \<longrightarrow> l = []
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma tl_hd_not_empty[rule_format]: "tl (l @ [a]) \<noteq> [] \<longrightarrow> l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (l @ [a]) \<noteq> [] \<longrightarrow> l \<noteq> []
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma app_tl_empty_length[rule_format]: "tl (map f [0..<length l] @ [a]) = []
                                        \<Longrightarrow> l = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (map f [0..<length l] @ [a]) = [] \<Longrightarrow> l = []
[PROOF STEP]
by (drule tl_hd_empty, simp)


[STATEMENT]
lemma not_empty_hd_fst[rule_format]: "l \<noteq> [] \<longrightarrow> hd(l @ [a]) = l ! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> [] \<longrightarrow> hd (l @ [a]) = l ! 0
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma app_tl_hd_list[rule_format]: "tl (map f [0..<length l] @ [a]) \<noteq> []
                             \<Longrightarrow> hd(map f [0..<length l] @ [a]) = (map f [0..<length l]) ! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (map f [0..<length l] @ [a]) \<noteq> [] \<Longrightarrow> hd (map f [0..<length l] @ [a]) = map f [0..<length l] ! 0
[PROOF STEP]
by (drule tl_hd_not_empty, erule not_empty_hd_fst)


[STATEMENT]
lemma tl_app_in[rule_format]: "l \<noteq> [] \<longrightarrow>
   map f [0..<(length l - (Suc 0:: nat))] @ [f(length l - (Suc 0 :: nat))] = map f [0..<length l]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> [] \<longrightarrow> map f [0..<length l - Suc 0] @ [f (length l - Suc 0)] = map f [0..<length l]
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma map_fst[rule_format]: "n > 0 \<longrightarrow> map f [0..<n] = f 0 # (map f [1..<n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<longrightarrow> map f [0..<n] = f 0 # map f [1..<n]
[PROOF STEP]
by (induction n) auto