[STATEMENT]
lemma rtrancl_finite_relpow:
  "(a, b) \<in> (set rel)\<^sup>* \<longleftrightarrow> (\<exists> n \<le> length rel. (a, b) \<in> set rel ^^ n)" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a, b) \<in> (set rel)\<^sup>*) = (\<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
 2. \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n \<Longrightarrow> (a, b) \<in> (set rel)\<^sup>*
[PROOF STEP]
assume ?r
[PROOF STATE]
proof (state)
this:
\<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n

goal (2 subgoals):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
 2. \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n \<Longrightarrow> (a, b) \<in> (set rel)\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
show ?l
[PROOF STATE]
proof (prove)
using this:
\<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n

goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>*
[PROOF STEP]
unfolding rtrancl_power
[PROOF STATE]
proof (prove)
using this:
\<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n

goal (1 subgoal):
 1. \<exists>n. (a, b) \<in> set rel ^^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a, b) \<in> (set rel)\<^sup>*

goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
assume ?l
[PROOF STATE]
proof (state)
this:
(a, b) \<in> (set rel)\<^sup>*

goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
from this [unfolded rtrancl_power]
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. (a, b) \<in> set rel ^^ n
[PROOF STEP]
obtain n where ab: "(a,b) \<in> set rel ^^ n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. (a, b) \<in> set rel ^^ n

goal (1 subgoal):
 1. (\<And>n. (a, b) \<in> set rel ^^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(a, b) \<in> set rel ^^ n

goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
obtain l where l: "l = (LEAST n. (a,b) \<in> set rel ^^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. l = (LEAST n. (a, b) \<in> set rel ^^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = (LEAST n. (a, b) \<in> set rel ^^ n)

goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
have ab: "(a, b) \<in> set rel ^^ l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> set rel ^^ l
[PROOF STEP]
unfolding l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> set rel ^^ (LEAST n. (a, b) \<in> set rel ^^ n)
[PROOF STEP]
by (intro LeastI, rule ab)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> set rel ^^ l

goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
from this [unfolded relpow_fun_conv]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. f 0 = a \<and> f l = b \<and> (\<forall>i<l. (f i, f (Suc i)) \<in> set rel)
[PROOF STEP]
obtain f where a: "f 0 = a" and b: "f l = b"
    and steps: "\<And> i. i < l \<Longrightarrow> (f i, f (Suc i)) \<in> set rel"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. f 0 = a \<and> f l = b \<and> (\<forall>i<l. (f i, f (Suc i)) \<in> set rel)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = a; f l = b; \<And>i. i < l \<Longrightarrow> (f i, f (Suc i)) \<in> set rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f 0 = a
f l = b
?i < l \<Longrightarrow> (f ?i, f (Suc ?i)) \<in> set rel

goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
let ?hits = "map (\<lambda> i. f (Suc i)) [0 ..< l]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
from steps
[PROOF STATE]
proof (chain)
picking this:
?i < l \<Longrightarrow> (f ?i, f (Suc ?i)) \<in> set rel
[PROOF STEP]
have subset: "set ?hits \<subseteq> snd ` set rel"
[PROOF STATE]
proof (prove)
using this:
?i < l \<Longrightarrow> (f ?i, f (Suc ?i)) \<in> set rel

goal (1 subgoal):
 1. set (map (\<lambda>i. f (Suc i)) [0..<l]) \<subseteq> snd ` set rel
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set (map (\<lambda>i. f (Suc i)) [0..<l]) \<subseteq> snd ` set rel

goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
have "l \<le> length rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> length rel
[PROOF STEP]
proof (cases "distinct ?hits")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
distinct (map (\<lambda>i. f (Suc i)) [0..<l])

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
have "l = length ?hits"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = length (map (\<lambda>i. f (Suc i)) [0..<l])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l = length (map (\<lambda>i. f (Suc i)) [0..<l])

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
l = length (map (\<lambda>i. f (Suc i)) [0..<l])

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
have "... = card (set ?hits)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (\<lambda>i. f (Suc i)) [0..<l]) = card (set (map (\<lambda>i. f (Suc i)) [0..<l]))
[PROOF STEP]
unfolding distinct_card [OF True]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (\<lambda>i. f (Suc i)) [0..<l]) = length (map (\<lambda>i. f (Suc i)) [0..<l])
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
length (map (\<lambda>i. f (Suc i)) [0..<l]) = card (set (map (\<lambda>i. f (Suc i)) [0..<l]))

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (map (\<lambda>i. f (Suc i)) [0..<l]) = card (set (map (\<lambda>i. f (Suc i)) [0..<l]))

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
have "... \<le> card (snd ` set rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set (map (\<lambda>i. f (Suc i)) [0..<l])) \<le> card (snd ` set rel)
[PROOF STEP]
by (rule card_mono [OF _ subset], auto)
[PROOF STATE]
proof (state)
this:
card (set (map (\<lambda>i. f (Suc i)) [0..<l])) \<le> card (snd ` set rel)

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (set (map (\<lambda>i. f (Suc i)) [0..<l])) \<le> card (snd ` set rel)

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
have "... = card (set (map snd rel))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (snd ` set rel) = card (set (map snd rel))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (snd ` set rel) = card (set (map snd rel))

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (snd ` set rel) = card (set (map snd rel))

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
have "... \<le> length (map snd rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set (map snd rel)) \<le> length (map snd rel)
[PROOF STEP]
by (rule card_length)
[PROOF STATE]
proof (state)
this:
card (set (map snd rel)) \<le> length (map snd rel)

goal (2 subgoals):
 1. distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
 2. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
l \<le> length (map snd rel)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l \<le> length (map snd rel)

goal (1 subgoal):
 1. l \<le> length rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<le> length rel

goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l])

goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
from this [unfolded distinct_conv_nth]
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>i<length (map (\<lambda>i. f (Suc i)) [0..<l]). \<forall>j<length (map (\<lambda>i. f (Suc i)) [0..<l]). i \<noteq> j \<longrightarrow> map (\<lambda>i. f (Suc i)) [0..<l] ! i \<noteq> map (\<lambda>i. f (Suc i)) [0..<l] ! j)
[PROOF STEP]
obtain i j where i: "i < l" and j: "j < l" and ij: "i \<noteq> j" and fij: "f (Suc i) = f (Suc j)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i<length (map (\<lambda>i. f (Suc i)) [0..<l]). \<forall>j<length (map (\<lambda>i. f (Suc i)) [0..<l]). i \<noteq> j \<longrightarrow> map (\<lambda>i. f (Suc i)) [0..<l] ! i \<noteq> map (\<lambda>i. f (Suc i)) [0..<l] ! j)

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < l; j < l; i \<noteq> j; f (Suc i) = f (Suc j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < l
j < l
i \<noteq> j
f (Suc i) = f (Suc j)

goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
let ?i = "min i j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
let ?j = "max i j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
have i: "?i < l" and j: "?j < l" and fij: "f (Suc ?i) = f (Suc ?j)"
      and ij: "?i < ?j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (min i j < l &&& max i j < l) &&& f (Suc (min i j)) = f (Suc (max i j)) &&& min i j < max i j
[PROOF STEP]
using i j ij fij
[PROOF STATE]
proof (prove)
using this:
i < l
j < l
i \<noteq> j
f (Suc i) = f (Suc j)

goal (1 subgoal):
 1. (min i j < l &&& max i j < l) &&& f (Suc (min i j)) = f (Suc (max i j)) &&& min i j < max i j
[PROOF STEP]
unfolding min_def max_def
[PROOF STATE]
proof (prove)
using this:
i < l
j < l
i \<noteq> j
f (Suc i) = f (Suc j)

goal (1 subgoal):
 1. ((if i \<le> j then i else j) < l &&& (if i \<le> j then j else i) < l) &&& f (Suc (if i \<le> j then i else j)) = f (Suc (if i \<le> j then j else i)) &&& (if i \<le> j then i else j) < (if i \<le> j then j else i)
[PROOF STEP]
by (cases "i \<le> j", auto)
[PROOF STATE]
proof (state)
this:
min i j < l
max i j < l
f (Suc (min i j)) = f (Suc (max i j))
min i j < max i j

goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
from i j fij ij
[PROOF STATE]
proof (chain)
picking this:
min i j < l
max i j < l
f (Suc (min i j)) = f (Suc (max i j))
min i j < max i j
[PROOF STEP]
obtain i j where i: "i < l" and j: "j < l" and ij: "i < j" and fij: "f (Suc i) = f (Suc j)"
[PROOF STATE]
proof (prove)
using this:
min i j < l
max i j < l
f (Suc (min i j)) = f (Suc (max i j))
min i j < max i j

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < l; j < l; i < j; f (Suc i) = f (Suc j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i < l
j < l
i < j
f (Suc i) = f (Suc j)

goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
let ?g = "\<lambda> n. if n \<le> i then f n else f (n + (j - i))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
let ?l = "l - (j - i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
have abl: "(a,b) \<in> set rel ^^ ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> set rel ^^ (l - (j - i))
[PROOF STEP]
unfolding relpow_fun_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. f 0 = a \<and> f (l - (j - i)) = b \<and> (\<forall>i<l - (j - i). (f i, f (Suc i)) \<in> set rel)
[PROOF STEP]
proof (rule exI [of _ ?g], intro conjI impI allI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (if 0 \<le> i then f 0 else f (0 + (j - i))) = a
 2. (if l - (j - i) \<le> i then f (l - (j - i)) else f (l - (j - i) + (j - i))) = b
 3. \<And>i. i < l - (j - i) \<Longrightarrow> (if i \<le> i then f i else f (i + (j - i)), if Suc i \<le> i then f (Suc i) else f (Suc i + (j - i))) \<in> set rel
[PROOF STEP]
show "?g ?l = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if l - (j - i) \<le> i then f (l - (j - i)) else f (l - (j - i) + (j - i))) = b
[PROOF STEP]
unfolding b [symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if l - (j - i) \<le> i then f (l - (j - i)) else f (l - (j - i) + (j - i))) = f l
[PROOF STEP]
using j ij
[PROOF STATE]
proof (prove)
using this:
j < l
i < j

goal (1 subgoal):
 1. (if l - (j - i) \<le> i then f (l - (j - i)) else f (l - (j - i) + (j - i))) = f l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if l - (j - i) \<le> i then f (l - (j - i)) else f (l - (j - i) + (j - i))) = b

goal (2 subgoals):
 1. (if 0 \<le> i then f 0 else f (0 + (j - i))) = a
 2. \<And>i. i < l - (j - i) \<Longrightarrow> (if i \<le> i then f i else f (i + (j - i)), if Suc i \<le> i then f (Suc i) else f (Suc i + (j - i))) \<in> set rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (if 0 \<le> i then f 0 else f (0 + (j - i))) = a
 2. \<And>i. i < l - (j - i) \<Longrightarrow> (if i \<le> i then f i else f (i + (j - i)), if Suc i \<le> i then f (Suc i) else f (Suc i + (j - i))) \<in> set rel
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (if 0 \<le> i then f 0 else f (0 + (j - i))) = a
 2. \<And>i. i < l - (j - i) \<Longrightarrow> (if i \<le> i then f i else f (i + (j - i)), if Suc i \<le> i then f (Suc i) else f (Suc i + (j - i))) \<in> set rel
[PROOF STEP]
assume k: "k < ?l"
[PROOF STATE]
proof (state)
this:
k < l - (j - i)

goal (2 subgoals):
 1. (if 0 \<le> i then f 0 else f (0 + (j - i))) = a
 2. \<And>i. i < l - (j - i) \<Longrightarrow> (if i \<le> i then f i else f (i + (j - i)), if Suc i \<le> i then f (Suc i) else f (Suc i + (j - i))) \<in> set rel
[PROOF STEP]
show "(?g k, ?g (Suc k)) \<in> set rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
proof (cases "k < i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
 2. \<not> k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k < i

goal (2 subgoals):
 1. k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
 2. \<not> k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i < l
k < i
[PROOF STEP]
have "k < l"
[PROOF STATE]
proof (prove)
using this:
i < l
k < i

goal (1 subgoal):
 1. k < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < l

goal (2 subgoals):
 1. k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
 2. \<not> k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
from steps [OF this]
[PROOF STATE]
proof (chain)
picking this:
(f k, f (Suc k)) \<in> set rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f k, f (Suc k)) \<in> set rel

goal (1 subgoal):
 1. (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(f k, f (Suc k)) \<in> set rel
k < i

goal (1 subgoal):
 1. (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel

goal (1 subgoal):
 1. \<not> k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> k < i

goal (1 subgoal):
 1. \<not> k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> k < i
[PROOF STEP]
have ik: "i \<le> k"
[PROOF STATE]
proof (prove)
using this:
\<not> k < i

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

goal (1 subgoal):
 1. \<not> k < i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
proof (cases "k = i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
 2. k \<noteq> i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k = i

goal (2 subgoals):
 1. k = i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
 2. k \<noteq> i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k = i

goal (1 subgoal):
 1. (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
using ij fij steps [OF i]
[PROOF STATE]
proof (prove)
using this:
k = i
i < j
f (Suc i) = f (Suc j)
(f i, f (Suc i)) \<in> set rel

goal (1 subgoal):
 1. (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<noteq> i

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
with ik
[PROOF STATE]
proof (chain)
picking this:
i \<le> k
k \<noteq> i
[PROOF STEP]
have ik: "i < k"
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k \<noteq> i

goal (1 subgoal):
 1. i < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < k

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < k
[PROOF STEP]
have small: "k + (j - i) < l"
[PROOF STATE]
proof (prove)
using this:
i < k

goal (1 subgoal):
 1. k + (j - i) < l
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
i < k
k < l - (j - i)

goal (1 subgoal):
 1. k + (j - i) < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k + (j - i) < l

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
using steps[OF small] ik
[PROOF STATE]
proof (prove)
using this:
(f (k + (j - i)), f (Suc (k + (j - i)))) \<in> set rel
i < k

goal (1 subgoal):
 1. (if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if k \<le> i then f k else f (k + (j - i)), if Suc k \<le> i then f (Suc k) else f (Suc k + (j - i))) \<in> set rel

goal (1 subgoal):
 1. (if 0 \<le> i then f 0 else f (0 + (j - i))) = a
[PROOF STEP]
qed (simp add: a)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> set rel ^^ (l - (j - i))

goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
from ij i
[PROOF STATE]
proof (chain)
picking this:
i < j
i < l
[PROOF STEP]
have ll: "?l < l"
[PROOF STATE]
proof (prove)
using this:
i < j
i < l

goal (1 subgoal):
 1. l - (j - i) < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l - (j - i) < l

goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
have "l \<le> ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> l - (j - i)
[PROOF STEP]
unfolding l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. (a, b) \<in> set rel ^^ n) \<le> (LEAST n. (a, b) \<in> set rel ^^ n) - (j - i)
[PROOF STEP]
by (rule Least_le, rule abl [unfolded l])
[PROOF STATE]
proof (state)
this:
l \<le> l - (j - i)

goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
with ll
[PROOF STATE]
proof (chain)
picking this:
l - (j - i) < l
l \<le> l - (j - i)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
l - (j - i) < l
l \<le> l - (j - i)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> distinct (map (\<lambda>i. f (Suc i)) [0..<l]) \<Longrightarrow> l \<le> length rel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. l \<le> length rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<le> length rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<le> length rel

goal (1 subgoal):
 1. (a, b) \<in> (set rel)\<^sup>* \<Longrightarrow> \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
with ab
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> set rel ^^ l
l \<le> length rel
[PROOF STEP]
show ?r
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> set rel ^^ l
l \<le> length rel

goal (1 subgoal):
 1. \<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n\<le>length rel. (a, b) \<in> set rel ^^ n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rtrancl_impl:
  "set_of (rtrancl_i rel as) = {b. (\<exists> a \<in> set as. (a, b) \<in> (set rel)\<^sup>*)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (rtrancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>*}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_of (rtrancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>*}
[PROOF STEP]
interpret set_access_succ set_of memb empty un "gen_succ rel" "set rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_access_succ set_of memb empty un (gen_succ rel) (set rel)
[PROOF STEP]
by (unfold_locales, insert gen_succ, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_of (rtrancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>*}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (rtrancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>*}
[PROOF STEP]
unfolding rtrancl_impl_def Let_def relpow_impl
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set as \<and> m \<le> length rel \<and> (a, b) \<in> set rel ^^ m} = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>*}
[PROOF STEP]
by (auto simp: rtrancl_finite_relpow)
[PROOF STATE]
proof (state)
this:
set_of (rtrancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>*}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trancl_impl:
  "set_of (trancl_i rel as) = {b. (\<exists> a \<in> set as. (a, b) \<in> (set rel)\<^sup>+)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (trancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>+}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_of (trancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>+}
[PROOF STEP]
interpret set_access_succ set_of memb empty un "gen_succ rel" "set rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_access_succ set_of memb empty un (gen_succ rel) (set rel)
[PROOF STEP]
by (unfold_locales, insert gen_succ, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_of (trancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>+}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (trancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>+}
[PROOF STEP]
unfolding trancl_impl_def Let_def relpow_impl trancl_unfold_left relcomp_unfold rtrancl_finite_relpow succ
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>a b m. uu_ = b \<and> a \<in> {b. \<exists>a\<in>set as. (a, b) \<in> set rel} \<and> m \<le> length rel \<and> (a, b) \<in> set rel ^^ m} = {b. \<exists>a\<in>set as. (a, b) \<in> {(x, z). \<exists>y. (x, y) \<in> set rel \<and> (\<exists>n\<le>length rel. (y, z) \<in> set rel ^^ n)}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_of (trancl_i rel as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set rel)\<^sup>+}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma D_extRetJ [intro!]: "\<D> e A \<Longrightarrow> \<D> (extRet2J e va) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D> e A \<Longrightarrow> \<D> (extRet2J e va) A
[PROOF STEP]
by(cases va) simp_all


[STATEMENT]
lemma blocks_defass [iff]: "\<And>A. \<lbrakk> length Vs = length Ts; length vs = length Ts\<rbrakk> \<Longrightarrow>
 \<D> (blocks Vs Ts vs e) A = \<D> e (A \<squnion> \<lfloor>set Vs\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>length Vs = length Ts; length vs = length Ts\<rbrakk> \<Longrightarrow> \<D> (blocks Vs Ts vs e) A = \<D> e (A \<squnion> \<lfloor>set Vs\<rfloor>)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>length Vs = length Ts; length vs = length Ts\<rbrakk> \<Longrightarrow> \<D> (blocks Vs Ts vs e) A = \<D> e (A \<squnion> \<lfloor>set Vs\<rfloor>)
[PROOF STEP]
apply(induct Vs Ts vs e rule:blocks.induct)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>V Vs T Ts v vs e A. \<lbrakk>\<And>A. \<lbrakk>length Vs = length Ts; length vs = length Ts\<rbrakk> \<Longrightarrow> \<D> (blocks Vs Ts vs e) A = \<D> e (A \<squnion> \<lfloor>set Vs\<rfloor>); length (V # Vs) = length (T # Ts); length (v # vs) = length (T # Ts)\<rbrakk> \<Longrightarrow> \<D> (blocks (V # Vs) (T # Ts) (v # vs) e) A = \<D> e (A \<squnion> \<lfloor>set (V # Vs)\<rfloor>)
 2. \<And>e A. \<lbrakk>length [] = length []; length [] = length []\<rbrakk> \<Longrightarrow> \<D> (blocks [] [] [] e) A = \<D> e (A \<squnion> \<lfloor>set []\<rfloor>)
 3. \<And>v va c d A. \<lbrakk>length [] = length (v # va); length c = length (v # va)\<rbrakk> \<Longrightarrow> \<D> (blocks [] (v # va) c d) A = \<D> d (A \<squnion> \<lfloor>set []\<rfloor>)
 4. \<And>b v va d A. \<lbrakk>length [] = length b; length (v # va) = length b\<rbrakk> \<Longrightarrow> \<D> (blocks [] b (v # va) d) A = \<D> d (A \<squnion> \<lfloor>set []\<rfloor>)
 5. \<And>v va c d A. \<lbrakk>length (v # va) = length []; length c = length []\<rbrakk> \<Longrightarrow> \<D> (blocks (v # va) [] c d) A = \<D> d (A \<squnion> \<lfloor>set (v # va)\<rfloor>)
 6. \<And>a v va d A. \<lbrakk>length a = length []; length (v # va) = length []\<rbrakk> \<Longrightarrow> \<D> (blocks a [] (v # va) d) A = \<D> d (A \<squnion> \<lfloor>set a\<rfloor>)
 7. \<And>v va b d A. \<lbrakk>length (v # va) = length b; length [] = length b\<rbrakk> \<Longrightarrow> \<D> (blocks (v # va) b [] d) A = \<D> d (A \<squnion> \<lfloor>set (v # va)\<rfloor>)
 8. \<And>a v va d A. \<lbrakk>length a = length (v # va); length [] = length (v # va)\<rbrakk> \<Longrightarrow> \<D> (blocks a (v # va) [] d) A = \<D> d (A \<squnion> \<lfloor>set a\<rfloor>)
[PROOF STEP]
apply(simp_all add:hyperset_defs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done