[STATEMENT]
lemma resChainI:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi \<times> pi) set"
  and   lst :: "name list"

  assumes eqvtRel: "eqvt Rel"
  and     Res:     "\<And>R S y. (R, S) \<in> Rel \<Longrightarrow> (<\<nu>y>R, <\<nu>y>S) \<in> Rel"
  and     PRelQ:   "P \<leadsto><Rel> Q"

  shows "(resChain lst) P \<leadsto><Rel> (resChain lst) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resChain lst P \<leadsto><Rel> resChain lst Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. resChain lst P \<leadsto><Rel> resChain lst Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resChain lst P \<leadsto><Rel> resChain lst Q
[PROOF STEP]
proof(induct lst)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. resChain [] P \<leadsto><Rel> resChain [] Q
 2. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
(* Base case *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. resChain [] P \<leadsto><Rel> resChain [] Q
 2. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto><Rel> Q
[PROOF STEP]
show "resChain [] P \<leadsto><Rel> resChain [] Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto><Rel> Q

goal (1 subgoal):
 1. resChain [] P \<leadsto><Rel> resChain [] Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
resChain [] P \<leadsto><Rel> resChain [] Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
(* Inductive step *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
fix a lst
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
assume IH: "(resChain lst P) \<leadsto><Rel> (resChain lst Q)"
[PROOF STATE]
proof (state)
this:
resChain lst P \<leadsto><Rel> resChain lst Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
resChain lst P \<leadsto><Rel> resChain lst Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
from Res
[PROOF STATE]
proof (chain)
picking this:
(?R, ?S) \<in> Rel \<Longrightarrow> (<\<nu>?y>?R, <\<nu>?y>?S) \<in> Rel
[PROOF STEP]
have "\<And>P Q a. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(?R, ?S) \<in> Rel \<Longrightarrow> (<\<nu>?y>?R, <\<nu>?y>?S) \<in> Rel

goal (1 subgoal):
 1. \<And>P Q a. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
have "Rel \<subseteq> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rel \<subseteq> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rel \<subseteq> Rel

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
resChain lst P \<leadsto><Rel> resChain lst Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel
Rel \<subseteq> Rel
[PROOF STEP]
have "<\<nu>a>(resChain lst P) \<leadsto><Rel> <\<nu>a>(resChain lst Q)"
[PROOF STATE]
proof (prove)
using this:
resChain lst P \<leadsto><Rel> resChain lst Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel
Rel \<subseteq> Rel

goal (1 subgoal):
 1. <\<nu>a>resChain lst P \<leadsto><Rel> <\<nu>a>resChain lst Q
[PROOF STEP]
using eqvtRel
[PROOF STATE]
proof (prove)
using this:
resChain lst P \<leadsto><Rel> resChain lst Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel
Rel \<subseteq> Rel
eqvt Rel

goal (1 subgoal):
 1. <\<nu>a>resChain lst P \<leadsto><Rel> <\<nu>a>resChain lst Q
[PROOF STEP]
by(rule_tac resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>a>resChain lst P \<leadsto><Rel> <\<nu>a>resChain lst Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
thus "resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q"
[PROOF STATE]
proof (prove)
using this:
<\<nu>a>resChain lst P \<leadsto><Rel> <\<nu>a>resChain lst Q

goal (1 subgoal):
 1. resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
resChain lst P \<leadsto><Rel> resChain lst Q

goal:
No subgoals!
[PROOF STEP]
qed