[STATEMENT]
lemma deterministic_RP_SomeD:
  assumes "deterministic_RP (N, P, Q, n) = Some R"
  shows "\<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) (N, P, Q, n) = (N', P', Q', n'))
    \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) (N, P, Q, n) = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
proof (induct rule: deterministic_RP.raw_induct[OF _ assms])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>deterministic_RP St Sta. \<lbrakk>\<And>x y. deterministic_RP x = Some y \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) x = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> y = map fst Q'; (if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else deterministic_RP (deterministic_RP_step St)) = Some Sta\<rbrakk> \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> Sta = map fst Q'
[PROOF STEP]
case (1 self_call St R)
[PROOF STATE]
proof (state)
this:
self_call ?x = Some ?y \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) ?x = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> ?y = map fst Q'
(if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else self_call (deterministic_RP_step St)) = Some R

goal (1 subgoal):
 1. \<And>deterministic_RP St Sta. \<lbrakk>\<And>x y. deterministic_RP x = Some y \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) x = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> y = map fst Q'; (if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else deterministic_RP (deterministic_RP_step St)) = Some Sta\<rbrakk> \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> Sta = map fst Q'
[PROOF STEP]
note ih = this(1) and step = this(2)
[PROOF STATE]
proof (state)
this:
self_call ?x = Some ?y \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) ?x = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> ?y = map fst Q'
(if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else self_call (deterministic_RP_step St)) = Some R

goal (1 subgoal):
 1. \<And>deterministic_RP St Sta. \<lbrakk>\<And>x y. deterministic_RP x = Some y \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) x = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> y = map fst Q'; (if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else deterministic_RP (deterministic_RP_step St)) = Some Sta\<rbrakk> \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> Sta = map fst Q'
[PROOF STEP]
obtain N P Q :: "'a dclause list" and n :: nat where
    st: "St = (N, P, Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N P Q n. St = (N, P, Q, n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases St) blast
[PROOF STATE]
proof (state)
this:
St = (N, P, Q, n)

goal (1 subgoal):
 1. \<And>deterministic_RP St Sta. \<lbrakk>\<And>x y. deterministic_RP x = Some y \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) x = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> y = map fst Q'; (if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else deterministic_RP (deterministic_RP_step St)) = Some Sta\<rbrakk> \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> Sta = map fst Q'
[PROOF STEP]
note step = step[unfolded st, simplified]
[PROOF STATE]
proof (state)
this:
(if is_final_dstate (N, P, Q, n) then let (uu_, uu_, Q, uu_) = (N, P, Q, n) in Some (map fst Q) else self_call (deterministic_RP_step (N, P, Q, n))) = Some R

goal (1 subgoal):
 1. \<And>deterministic_RP St Sta. \<lbrakk>\<And>x y. deterministic_RP x = Some y \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) x = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> y = map fst Q'; (if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else deterministic_RP (deterministic_RP_step St)) = Some Sta\<rbrakk> \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> Sta = map fst Q'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
proof (cases "is_final_dstate (N, P, Q, n)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
 2. \<not> is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_final_dstate (N, P, Q, n)

goal (2 subgoals):
 1. is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
 2. \<not> is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_final_dstate (N, P, Q, n)
[PROOF STEP]
have "(deterministic_RP_step ^^ 0) (N, P, Q, n) = (N, P, Q, n)
      \<and> is_final_dstate (N, P, Q, n) \<and> R = map fst Q"
[PROOF STATE]
proof (prove)
using this:
is_final_dstate (N, P, Q, n)

goal (1 subgoal):
 1. (deterministic_RP_step ^^ 0) (N, P, Q, n) = (N, P, Q, n) \<and> is_final_dstate (N, P, Q, n) \<and> R = map fst Q
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
is_final_dstate (N, P, Q, n)
(if is_final_dstate (N, P, Q, n) then let (uu_, uu_, Q, uu_) = (N, P, Q, n) in Some (map fst Q) else self_call (deterministic_RP_step (N, P, Q, n))) = Some R

goal (1 subgoal):
 1. (deterministic_RP_step ^^ 0) (N, P, Q, n) = (N, P, Q, n) \<and> is_final_dstate (N, P, Q, n) \<and> R = map fst Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(deterministic_RP_step ^^ 0) (N, P, Q, n) = (N, P, Q, n) \<and> is_final_dstate (N, P, Q, n) \<and> R = map fst Q

goal (2 subgoals):
 1. is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
 2. \<not> is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(deterministic_RP_step ^^ 0) (N, P, Q, n) = (N, P, Q, n) \<and> is_final_dstate (N, P, Q, n) \<and> R = map fst Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(deterministic_RP_step ^^ 0) (N, P, Q, n) = (N, P, Q, n) \<and> is_final_dstate (N, P, Q, n) \<and> R = map fst Q

goal (1 subgoal):
 1. \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
unfolding st
[PROOF STATE]
proof (prove)
using this:
(deterministic_RP_step ^^ 0) (N, P, Q, n) = (N, P, Q, n) \<and> is_final_dstate (N, P, Q, n) \<and> R = map fst Q

goal (1 subgoal):
 1. \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) (N, P, Q, n) = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'

goal (1 subgoal):
 1. \<not> is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
case nonfinal: False
[PROOF STATE]
proof (state)
this:
\<not> is_final_dstate (N, P, Q, n)

goal (1 subgoal):
 1. \<not> is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
note step = step[simplified nonfinal, simplified]
[PROOF STATE]
proof (state)
this:
self_call (deterministic_RP_step (N, P, Q, n)) = Some R

goal (1 subgoal):
 1. \<not> is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
obtain N' P' Q' :: "'a dclause list" and n' k :: nat where
      "(deterministic_RP_step ^^ k) (deterministic_RP_step (N, P, Q, n)) = (N', P', Q', n')" and
      "is_final_dstate (N', P', Q', n')"
      "R = map fst Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k N' P' Q' n'. \<lbrakk>(deterministic_RP_step ^^ k) (deterministic_RP_step (N, P, Q, n)) = (N', P', Q', n'); is_final_dstate (N', P', Q', n'); R = map fst Q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ih[OF step]
[PROOF STATE]
proof (prove)
using this:
\<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) (deterministic_RP_step (N, P, Q, n)) = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'

goal (1 subgoal):
 1. (\<And>k N' P' Q' n'. \<lbrakk>(deterministic_RP_step ^^ k) (deterministic_RP_step (N, P, Q, n)) = (N', P', Q', n'); is_final_dstate (N', P', Q', n'); R = map fst Q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(deterministic_RP_step ^^ k) (deterministic_RP_step (N, P, Q, n)) = (N', P', Q', n')
is_final_dstate (N', P', Q', n')
R = map fst Q'

goal (1 subgoal):
 1. \<not> is_final_dstate (N, P, Q, n) \<Longrightarrow> \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(deterministic_RP_step ^^ k) (deterministic_RP_step (N, P, Q, n)) = (N', P', Q', n')
is_final_dstate (N', P', Q', n')
R = map fst Q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(deterministic_RP_step ^^ k) (deterministic_RP_step (N, P, Q, n)) = (N', P', Q', n')
is_final_dstate (N', P', Q', n')
R = map fst Q'

goal (1 subgoal):
 1. \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
unfolding st funpow_Suc_right[symmetric, THEN fun_cong, unfolded comp_apply]
[PROOF STATE]
proof (prove)
using this:
(deterministic_RP_step ^^ Suc k) (N, P, Q, n) = (N', P', Q', n')
is_final_dstate (N', P', Q', n')
R = map fst Q'

goal (1 subgoal):
 1. \<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) (N, P, Q, n) = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) St = (N', P', Q', n')) \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma full_deriv_wSts_trancl_weighted_RP: "full_chain (\<leadsto>\<^sub>w\<^sup>+) wSts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. full_chain (\<leadsto>\<^sub>w\<^sup>+) wSts
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. full_chain (\<leadsto>\<^sub>w\<^sup>+) wSts
[PROOF STEP]
have "Sts' = derivation_from St0' \<Longrightarrow> full_chain (\<leadsto>\<^sub>w\<^sup>+) (lmap wstate_of_dstate Sts')"
    for St0' Sts'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sts' = derivation_from St0' \<Longrightarrow> full_chain (\<leadsto>\<^sub>w\<^sup>+) (lmap wstate_of_dstate Sts')
[PROOF STEP]
proof (coinduction arbitrary: St0' Sts' rule: full_chain.coinduct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>St0' Sts'. Sts' = derivation_from St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
case sts': full_chain
[PROOF STATE]
proof (state)
this:
Sts' = derivation_from St0'

goal (1 subgoal):
 1. \<And>St0' Sts'. Sts' = derivation_from St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
proof (cases "is_final_dstate St0'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
 2. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_final_dstate St0'

goal (2 subgoals):
 1. is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
 2. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_final_dstate St0'
[PROOF STEP]
have "ltl (lmap wstate_of_dstate Sts') = LNil"
[PROOF STATE]
proof (prove)
using this:
is_final_dstate St0'

goal (1 subgoal):
 1. ltl (lmap wstate_of_dstate Sts') = LNil
[PROOF STEP]
unfolding sts'
[PROOF STATE]
proof (prove)
using this:
is_final_dstate St0'

goal (1 subgoal):
 1. ltl (lmap wstate_of_dstate (derivation_from St0')) = LNil
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ltl (lmap wstate_of_dstate Sts') = LNil

goal (2 subgoals):
 1. is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
 2. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ltl (lmap wstate_of_dstate Sts') = LNil
[PROOF STEP]
have "lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') LNil"
[PROOF STATE]
proof (prove)
using this:
ltl (lmap wstate_of_dstate Sts') = LNil

goal (1 subgoal):
 1. lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') LNil
[PROOF STEP]
unfolding sts'
[PROOF STATE]
proof (prove)
using this:
ltl (lmap wstate_of_dstate (derivation_from St0')) = LNil

goal (1 subgoal):
 1. lmap wstate_of_dstate (derivation_from St0') = LCons (wstate_of_dstate St0') LNil
[PROOF STEP]
by (subst derivation_from.code, subst (asm) derivation_from.code, auto)
[PROOF STATE]
proof (state)
this:
lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') LNil

goal (2 subgoals):
 1. is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
 2. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') LNil

goal (2 subgoals):
 1. is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
 2. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
have "\<And>St''. \<not> wstate_of_dstate St0' \<leadsto>\<^sub>w St''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>St''. \<not> wstate_of_dstate St0' \<leadsto>\<^sub>w St''
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
is_final_dstate St0'

goal (1 subgoal):
 1. \<And>St''. \<not> wstate_of_dstate St0' \<leadsto>\<^sub>w St''
[PROOF STEP]
by (rule is_final_dstate_imp_not_weighted_RP)
[PROOF STATE]
proof (state)
this:
\<not> wstate_of_dstate St0' \<leadsto>\<^sub>w ?St''

goal (2 subgoals):
 1. is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
 2. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') LNil
\<not> wstate_of_dstate St0' \<leadsto>\<^sub>w ?St''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') LNil
\<not> wstate_of_dstate St0' \<leadsto>\<^sub>w ?St''

goal (1 subgoal):
 1. (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
by (meson tranclpD)
[PROOF STATE]
proof (state)
this:
(\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)

goal (1 subgoal):
 1. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
case nfinal: False
[PROOF STATE]
proof (state)
this:
\<not> is_final_dstate St0'

goal (1 subgoal):
 1. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
have "lmap wstate_of_dstate Sts' =
        LCons (wstate_of_dstate St0') (lmap wstate_of_dstate (ltl Sts'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') (lmap wstate_of_dstate (ltl Sts'))
[PROOF STEP]
unfolding sts'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmap wstate_of_dstate (derivation_from St0') = LCons (wstate_of_dstate St0') (lmap wstate_of_dstate (ltl (derivation_from St0')))
[PROOF STEP]
by (subst derivation_from.code) simp
[PROOF STATE]
proof (state)
this:
lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') (lmap wstate_of_dstate (ltl Sts'))

goal (1 subgoal):
 1. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') (lmap wstate_of_dstate (ltl Sts'))

goal (1 subgoal):
 1. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
have "ltl Sts' = derivation_from (deterministic_RP_step St0')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltl Sts' = derivation_from (deterministic_RP_step St0')
[PROOF STEP]
unfolding sts'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltl (derivation_from St0') = derivation_from (deterministic_RP_step St0')
[PROOF STEP]
using nfinal
[PROOF STATE]
proof (prove)
using this:
\<not> is_final_dstate St0'

goal (1 subgoal):
 1. ltl (derivation_from St0') = derivation_from (deterministic_RP_step St0')
[PROOF STEP]
by (subst derivation_from.code) simp
[PROOF STATE]
proof (state)
this:
ltl Sts' = derivation_from (deterministic_RP_step St0')

goal (1 subgoal):
 1. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ltl Sts' = derivation_from (deterministic_RP_step St0')

goal (1 subgoal):
 1. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
have "wstate_of_dstate St0' \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (lhd (ltl Sts'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St0' \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (lhd (ltl Sts'))
[PROOF STEP]
unfolding sts'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St0' \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (lhd (ltl (derivation_from St0')))
[PROOF STEP]
using nonfinal_deterministic_RP_step[OF nfinal refl] nfinal
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate St0' \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (deterministic_RP_step St0')
\<not> is_final_dstate St0'

goal (1 subgoal):
 1. wstate_of_dstate St0' \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (lhd (ltl (derivation_from St0')))
[PROOF STEP]
by (subst derivation_from.code) simp
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St0' \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (lhd (ltl Sts'))

goal (1 subgoal):
 1. \<not> is_final_dstate St0' \<Longrightarrow> (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') (lmap wstate_of_dstate (ltl Sts'))
ltl Sts' = derivation_from (deterministic_RP_step St0')
wstate_of_dstate St0' \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (lhd (ltl Sts'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') (lmap wstate_of_dstate (ltl Sts'))
ltl Sts' = derivation_from (deterministic_RP_step St0')
wstate_of_dstate St0' \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (lhd (ltl Sts'))

goal (1 subgoal):
 1. (\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>x. lmap wstate_of_dstate Sts' = LCons x LNil \<and> (\<forall>y. \<not> x \<leadsto>\<^sub>w\<^sup>+ y)) \<or> (\<exists>xs x. lmap wstate_of_dstate Sts' = LCons x xs \<and> ((\<exists>St0' Sts'. xs = lmap wstate_of_dstate Sts' \<and> Sts' = derivation_from St0') \<or> full_chain (\<leadsto>\<^sub>w\<^sup>+) xs) \<and> x \<leadsto>\<^sub>w\<^sup>+ lhd xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?Sts' = derivation_from ?St0' \<Longrightarrow> full_chain (\<leadsto>\<^sub>w\<^sup>+) (lmap wstate_of_dstate ?Sts')

goal (1 subgoal):
 1. full_chain (\<leadsto>\<^sub>w\<^sup>+) wSts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?Sts' = derivation_from ?St0' \<Longrightarrow> full_chain (\<leadsto>\<^sub>w\<^sup>+) (lmap wstate_of_dstate ?Sts')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?Sts' = derivation_from ?St0' \<Longrightarrow> full_chain (\<leadsto>\<^sub>w\<^sup>+) (lmap wstate_of_dstate ?Sts')

goal (1 subgoal):
 1. full_chain (\<leadsto>\<^sub>w\<^sup>+) wSts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
full_chain (\<leadsto>\<^sub>w\<^sup>+) wSts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sswSts:
  "full_chain (\<leadsto>\<^sub>w) sswSts \<and> emb wSts sswSts \<and> lhd sswSts = lhd wSts \<and> llast sswSts = llast wSts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. full_chain (\<leadsto>\<^sub>w) sswSts \<and> emb wSts sswSts \<and> lhd sswSts = lhd wSts \<and> llast sswSts = llast wSts
[PROOF STEP]
unfolding sswSts_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. full_chain (\<leadsto>\<^sub>w) (SOME wSts'. full_chain (\<leadsto>\<^sub>w) wSts' \<and> emb wSts wSts' \<and> lhd wSts' = lhd wSts \<and> llast wSts' = llast wSts) \<and> emb wSts (SOME wSts'. full_chain (\<leadsto>\<^sub>w) wSts' \<and> emb wSts wSts' \<and> lhd wSts' = lhd wSts \<and> llast wSts' = llast wSts) \<and> lhd (SOME wSts'. full_chain (\<leadsto>\<^sub>w) wSts' \<and> emb wSts wSts' \<and> lhd wSts' = lhd wSts \<and> llast wSts' = llast wSts) = lhd wSts \<and> llast (SOME wSts'. full_chain (\<leadsto>\<^sub>w) wSts' \<and> emb wSts wSts' \<and> lhd wSts' = lhd wSts \<and> llast wSts' = llast wSts) = llast wSts
[PROOF STEP]
by (rule someI_ex[OF full_chain_tranclp_imp_exists_full_chain[OF
          full_deriv_wSts_trancl_weighted_RP]])


[STATEMENT]
lemma empty_ssgP0: "wrp.P_of_wstate (lhd sswSts) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrp.P_of_wstate (lhd sswSts) = {}
[PROOF STEP]
unfolding lhd_sswSts
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrp.P_of_wstate (lhd wSts) = {}
[PROOF STEP]
by (subst derivation_from.code) simp


[STATEMENT]
lemma empty_ssgQ0: "wrp.Q_of_wstate (lhd sswSts) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrp.Q_of_wstate (lhd sswSts) = {}
[PROOF STEP]
unfolding lhd_sswSts
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrp.Q_of_wstate (lhd wSts) = {}
[PROOF STEP]
by (subst derivation_from.code) simp


[STATEMENT]
lemma lfinite_Sts: "lfinite Sts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite Sts
[PROOF STEP]
proof (induct rule: deterministic_RP.raw_induct[OF _ drp_some])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>deterministic_RP St Sta. \<lbrakk>\<And>x y. deterministic_RP x = Some y \<Longrightarrow> lfinite (derivation_from x); (if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else deterministic_RP (deterministic_RP_step St)) = Some Sta\<rbrakk> \<Longrightarrow> lfinite (derivation_from St)
[PROOF STEP]
case (1 self_call St St')
[PROOF STATE]
proof (state)
this:
self_call ?x = Some ?y \<Longrightarrow> lfinite (derivation_from ?x)
(if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else self_call (deterministic_RP_step St)) = Some St'

goal (1 subgoal):
 1. \<And>deterministic_RP St Sta. \<lbrakk>\<And>x y. deterministic_RP x = Some y \<Longrightarrow> lfinite (derivation_from x); (if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else deterministic_RP (deterministic_RP_step St)) = Some Sta\<rbrakk> \<Longrightarrow> lfinite (derivation_from St)
[PROOF STEP]
note ih = this(1) and step = this(2)
[PROOF STATE]
proof (state)
this:
self_call ?x = Some ?y \<Longrightarrow> lfinite (derivation_from ?x)
(if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else self_call (deterministic_RP_step St)) = Some St'

goal (1 subgoal):
 1. \<And>deterministic_RP St Sta. \<lbrakk>\<And>x y. deterministic_RP x = Some y \<Longrightarrow> lfinite (derivation_from x); (if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else deterministic_RP (deterministic_RP_step St)) = Some Sta\<rbrakk> \<Longrightarrow> lfinite (derivation_from St)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite (derivation_from St)
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
(if is_final_dstate St then let (uu_, uu_, Q, uu_) = St in Some (map fst Q) else self_call (deterministic_RP_step St)) = Some St'

goal (1 subgoal):
 1. lfinite (derivation_from St)
[PROOF STEP]
by (subst derivation_from.code, auto intro: ih)
[PROOF STATE]
proof (state)
this:
lfinite (derivation_from St)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lfinite_wSts: "lfinite wSts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite wSts
[PROOF STEP]
by (rule lfinite_lmap[THEN iffD2, OF lfinite_Sts])


[STATEMENT]
theorem deterministic_RP_complete: "satisfiable grounded_N0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfiable grounded_N0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> satisfiable grounded_N0 \<Longrightarrow> False
[PROOF STEP]
assume unsat: "\<not> satisfiable grounded_N0"
[PROOF STATE]
proof (state)
this:
\<not> satisfiable grounded_N0

goal (1 subgoal):
 1. \<not> satisfiable grounded_N0 \<Longrightarrow> False
[PROOF STEP]
have unsat_wSts0: "\<not> satisfiable (wrp.grounding_of_wstate (lhd wSts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> satisfiable (grounding_of_clss (wrp.N_of_wstate (lhd wSts) \<union> wrp.P_of_wstate (lhd wSts) \<union> wrp.Q_of_wstate (lhd wSts)))
[PROOF STEP]
using unsat
[PROOF STATE]
proof (prove)
using this:
\<not> satisfiable grounded_N0

goal (1 subgoal):
 1. \<not> satisfiable (grounding_of_clss (wrp.N_of_wstate (lhd wSts) \<union> wrp.P_of_wstate (lhd wSts) \<union> wrp.Q_of_wstate (lhd wSts)))
[PROOF STEP]
by (subst derivation_from.code) (simp add: comp_def)
[PROOF STATE]
proof (state)
this:
\<not> satisfiable (grounding_of_clss (wrp.N_of_wstate (lhd wSts) \<union> wrp.P_of_wstate (lhd wSts) \<union> wrp.Q_of_wstate (lhd wSts)))

goal (1 subgoal):
 1. \<not> satisfiable grounded_N0 \<Longrightarrow> False
[PROOF STEP]
have bot_in_ss: "{#} \<in> Q_of_state (wrp.Liminf_wstate sswSts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#} \<in> Q_of_state (wrp.Liminf_wstate sswSts)
[PROOF STEP]
by (rule wrp.weighted_RP_complete[OF sswSts_thms unsat_wSts0[folded lhd_sswSts]])
[PROOF STATE]
proof (state)
this:
{#} \<in> Q_of_state (wrp.Liminf_wstate sswSts)

goal (1 subgoal):
 1. \<not> satisfiable grounded_N0 \<Longrightarrow> False
[PROOF STEP]
have bot_in_lim: "{#} \<in> Q_of_state (wrp.Liminf_wstate wSts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
proof (cases "lfinite Sts")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfinite Sts \<Longrightarrow> {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
 2. \<not> lfinite Sts \<Longrightarrow> {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
case fin: True
[PROOF STATE]
proof (state)
this:
lfinite Sts

goal (2 subgoals):
 1. lfinite Sts \<Longrightarrow> {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
 2. \<not> lfinite Sts \<Longrightarrow> {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
have "wrp.Liminf_wstate sswSts = wrp.Liminf_wstate wSts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrp.Liminf_wstate sswSts = wrp.Liminf_wstate wSts
[PROOF STEP]
by (rule Liminf_state_fin, simp_all add: fin lfinite_sswSts_iff not_lnull_sswSts,
          subst (1 2) llast_lmap,
          simp_all add: lfinite_sswSts_iff fin not_lnull_sswSts llast_sswSts)
[PROOF STATE]
proof (state)
this:
wrp.Liminf_wstate sswSts = wrp.Liminf_wstate wSts

goal (2 subgoals):
 1. lfinite Sts \<Longrightarrow> {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
 2. \<not> lfinite Sts \<Longrightarrow> {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wrp.Liminf_wstate sswSts = wrp.Liminf_wstate wSts
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wrp.Liminf_wstate sswSts = wrp.Liminf_wstate wSts

goal (1 subgoal):
 1. {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
using bot_in_ss
[PROOF STATE]
proof (prove)
using this:
wrp.Liminf_wstate sswSts = wrp.Liminf_wstate wSts
{#} \<in> Q_of_state (wrp.Liminf_wstate sswSts)

goal (1 subgoal):
 1. {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{#} \<in> Q_of_state (wrp.Liminf_wstate wSts)

goal (1 subgoal):
 1. \<not> lfinite Sts \<Longrightarrow> {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lfinite Sts \<Longrightarrow> {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> lfinite Sts

goal (1 subgoal):
 1. \<not> lfinite Sts \<Longrightarrow> {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> lfinite Sts
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> lfinite Sts

goal (1 subgoal):
 1. {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
using bot_in_ss Q_of_Liminf_state_inf[OF _ emb_lmap[OF emb_sswSts]]
[PROOF STATE]
proof (prove)
using this:
\<not> lfinite Sts
{#} \<in> Q_of_state (wrp.Liminf_wstate sswSts)
\<not> lfinite (lmap ?f1 wSts) \<Longrightarrow> Q_of_state (Liminf_state (lmap ?f1 sswSts)) \<subseteq> Q_of_state (Liminf_state (lmap ?f1 wSts))

goal (1 subgoal):
 1. {#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#} \<in> Q_of_state (wrp.Liminf_wstate wSts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{#} \<in> Q_of_state (wrp.Liminf_wstate wSts)

goal (1 subgoal):
 1. \<not> satisfiable grounded_N0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{#} \<in> Q_of_state (wrp.Liminf_wstate wSts)
[PROOF STEP]
obtain k :: nat where
    k_lt: "enat k < llength Sts" and
    emp_in: "{#} \<in> wrp.Q_of_wstate (lnth wSts k)"
[PROOF STATE]
proof (prove)
using this:
{#} \<in> Q_of_state (wrp.Liminf_wstate wSts)

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>enat k < llength Sts; {#} \<in> wrp.Q_of_wstate (lnth wSts k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Liminf_state_def Liminf_llist_def
[PROOF STATE]
proof (prove)
using this:
{#} \<in> Q_of_state (\<Union>i\<in>{i. enat i < llength (lmap N_of_state (lmap state_of_wstate wSts))}. \<Inter> (lnth (lmap N_of_state (lmap state_of_wstate wSts)) ` {j. i \<le> j \<and> enat j < llength (lmap N_of_state (lmap state_of_wstate wSts))}), \<Union>i\<in>{i. enat i < llength (lmap P_of_state (lmap state_of_wstate wSts))}. \<Inter> (lnth (lmap P_of_state (lmap state_of_wstate wSts)) ` {j. i \<le> j \<and> enat j < llength (lmap P_of_state (lmap state_of_wstate wSts))}), \<Union>i\<in>{i. enat i < llength (lmap Q_of_state (lmap state_of_wstate wSts))}. \<Inter> (lnth (lmap Q_of_state (lmap state_of_wstate wSts)) ` {j. i \<le> j \<and> enat j < llength (lmap Q_of_state (lmap state_of_wstate wSts))}))

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>enat k < llength Sts; {#} \<in> wrp.Q_of_wstate (lnth wSts k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enat k < llength Sts
{#} \<in> wrp.Q_of_wstate (lnth wSts k)

goal (1 subgoal):
 1. \<not> satisfiable grounded_N0 \<Longrightarrow> False
[PROOF STEP]
have emp_in: "{#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))
[PROOF STEP]
have "enat k < llength Sts' \<Longrightarrow> Sts' = derivation_from St0' \<Longrightarrow>
      {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k) \<Longrightarrow>
      {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0'))" for St0' Sts' k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0'))
[PROOF STEP]
proof (induction k arbitrary: St0' Sts')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>St0' Sts'. \<lbrakk>enat 0 < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') 0)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ 0) St0'))
 2. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
enat 0 < llength Sts'
Sts' = derivation_from St0'
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') 0)

goal (2 subgoals):
 1. \<And>St0' Sts'. \<lbrakk>enat 0 < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') 0)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ 0) St0'))
 2. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
enat 0 < llength Sts'
Sts' = derivation_from St0'
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
enat 0 < llength Sts'
Sts' = derivation_from St0'
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') 0)

goal (1 subgoal):
 1. {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ 0) St0'))
[PROOF STEP]
by (subst (asm) derivation_from.code, cases St0', auto simp: comp_def)
[PROOF STATE]
proof (state)
this:
{#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ 0) St0'))

goal (1 subgoal):
 1. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>enat k < llength ?Sts'; ?Sts' = derivation_from ?St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate ?Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) ?St0'))
enat (Suc k) < llength Sts'
Sts' = derivation_from St0'
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))

goal (1 subgoal):
 1. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
note ih = this(1) and sk_lt = this(2) and sts' = this(3) and emp_in_sk = this(4)
[PROOF STATE]
proof (state)
this:
\<lbrakk>enat k < llength ?Sts'; ?Sts' = derivation_from ?St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate ?Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) ?St0'))
enat (Suc k) < llength Sts'
Sts' = derivation_from St0'
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))

goal (1 subgoal):
 1. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
have k_lt: "enat k < llength (ltl Sts')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat k < llength (ltl Sts')
[PROOF STEP]
using sk_lt
[PROOF STATE]
proof (prove)
using this:
enat (Suc k) < llength Sts'

goal (1 subgoal):
 1. enat k < llength (ltl Sts')
[PROOF STEP]
by (cases Sts') (auto simp: Suc_ile_eq)
[PROOF STATE]
proof (state)
this:
enat k < llength (ltl Sts')

goal (1 subgoal):
 1. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enat k < llength (ltl Sts')

goal (1 subgoal):
 1. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
have "ltl Sts' = derivation_from (deterministic_RP_step St0')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltl Sts' = derivation_from (deterministic_RP_step St0')
[PROOF STEP]
using sts' k_lt
[PROOF STATE]
proof (prove)
using this:
Sts' = derivation_from St0'
enat k < llength (ltl Sts')

goal (1 subgoal):
 1. ltl Sts' = derivation_from (deterministic_RP_step St0')
[PROOF STEP]
by (cases Sts') auto
[PROOF STATE]
proof (state)
this:
ltl Sts' = derivation_from (deterministic_RP_step St0')

goal (1 subgoal):
 1. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ltl Sts' = derivation_from (deterministic_RP_step St0')

goal (1 subgoal):
 1. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
have "{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)
[PROOF STEP]
using emp_in_sk k_lt
[PROOF STATE]
proof (prove)
using this:
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))
enat k < llength (ltl Sts')

goal (1 subgoal):
 1. {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)
[PROOF STEP]
by (cases Sts') auto
[PROOF STATE]
proof (state)
this:
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)

goal (1 subgoal):
 1. \<And>k St0' Sts'. \<lbrakk>\<And>St0' Sts'. \<lbrakk>enat k < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0')); enat (Suc k) < llength Sts'; Sts' = derivation_from St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') (Suc k))\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enat k < llength (ltl Sts')
ltl Sts' = derivation_from (deterministic_RP_step St0')
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
enat k < llength (ltl Sts')
ltl Sts' = derivation_from (deterministic_RP_step St0')
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)

goal (1 subgoal):
 1. {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
using ih[of "ltl Sts'" "deterministic_RP_step St0'"]
[PROOF STATE]
proof (prove)
using this:
enat k < llength (ltl Sts')
ltl Sts' = derivation_from (deterministic_RP_step St0')
{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)
\<lbrakk>enat k < llength (ltl Sts'); ltl Sts' = derivation_from (deterministic_RP_step St0'); {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) (deterministic_RP_step St0')))

goal (1 subgoal):
 1. {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))
[PROOF STEP]
by (simp add: funpow_swap1)
[PROOF STATE]
proof (state)
this:
{#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ Suc k) St0'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>enat ?k < llength ?Sts'; ?Sts' = derivation_from ?St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate ?Sts') ?k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ ?k) ?St0'))

goal (1 subgoal):
 1. {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>enat ?k < llength ?Sts'; ?Sts' = derivation_from ?St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate ?Sts') ?k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ ?k) ?St0'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>enat ?k < llength ?Sts'; ?Sts' = derivation_from ?St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate ?Sts') ?k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ ?k) ?St0'))

goal (1 subgoal):
 1. {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))
[PROOF STEP]
using k_lt emp_in
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>enat ?k < llength ?Sts'; ?Sts' = derivation_from ?St0'; {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate ?Sts') ?k)\<rbrakk> \<Longrightarrow> {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ ?k) ?St0'))
enat k < llength Sts
{#} \<in> wrp.Q_of_wstate (lnth wSts k)

goal (1 subgoal):
 1. {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))

goal (1 subgoal):
 1. \<not> satisfiable grounded_N0 \<Longrightarrow> False
[PROOF STEP]
have "deterministic_RP St0 \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deterministic_RP St0 \<noteq> None
[PROOF STEP]
by (rule is_final_dstate_funpow_imp_deterministic_RP_neq_None[of "Suc k"],
        cases "(deterministic_RP_step ^^ k) St0",
        use emp_in in \<open>force simp: deterministic_RP_step.simps is_final_dstate.simps\<close>)
[PROOF STATE]
proof (state)
this:
deterministic_RP St0 \<noteq> None

goal (1 subgoal):
 1. \<not> satisfiable grounded_N0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deterministic_RP St0 \<noteq> None
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
deterministic_RP St0 \<noteq> None

goal (1 subgoal):
 1. False
[PROOF STEP]
using drp_none
[PROOF STATE]
proof (prove)
using this:
deterministic_RP St0 \<noteq> None
deterministic_RP St0 = None

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uexpr_eq_iff:
  "e = f \<longleftrightarrow> (\<forall> b. \<lbrakk>e\<rbrakk>\<^sub>e b = \<lbrakk>f\<rbrakk>\<^sub>e b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e = f) = (\<forall>b. \<lbrakk>e\<rbrakk>\<^sub>e b = \<lbrakk>f\<rbrakk>\<^sub>e b)
[PROOF STEP]
using Rep_uexpr_inject[of e f, THEN sym]
[PROOF STATE]
proof (prove)
using this:
(e = f) = (\<lbrakk>e\<rbrakk>\<^sub>e = \<lbrakk>f\<rbrakk>\<^sub>e)

goal (1 subgoal):
 1. (e = f) = (\<forall>b. \<lbrakk>e\<rbrakk>\<^sub>e b = \<lbrakk>f\<rbrakk>\<^sub>e b)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma lit_ueval [ueval]: "\<lbrakk>\<guillemotleft>x\<guillemotright>\<rbrakk>\<^sub>eb = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>x\<guillemotright>\<rbrakk>\<^sub>e b = x
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma var_ueval [ueval]: "\<lbrakk>var x\<rbrakk>\<^sub>eb = get\<^bsub>x\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<rbrakk>\<^sub>e b = get\<^bsub>x\<^esub> b
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma uop_ueval [ueval]: "\<lbrakk>uop f x\<rbrakk>\<^sub>eb = f (\<lbrakk>x\<rbrakk>\<^sub>eb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uop f x\<rbrakk>\<^sub>e b = f (\<lbrakk>x\<rbrakk>\<^sub>e b)
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma bop_ueval [ueval]: "\<lbrakk>bop f x y\<rbrakk>\<^sub>eb = f (\<lbrakk>x\<rbrakk>\<^sub>eb) (\<lbrakk>y\<rbrakk>\<^sub>eb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bop f x y\<rbrakk>\<^sub>e b = f (\<lbrakk>x\<rbrakk>\<^sub>e b) (\<lbrakk>y\<rbrakk>\<^sub>e b)
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma trop_ueval [ueval]: "\<lbrakk>trop f x y z\<rbrakk>\<^sub>eb = f (\<lbrakk>x\<rbrakk>\<^sub>eb) (\<lbrakk>y\<rbrakk>\<^sub>eb) (\<lbrakk>z\<rbrakk>\<^sub>eb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trop f x y z\<rbrakk>\<^sub>e b = f (\<lbrakk>x\<rbrakk>\<^sub>e b) (\<lbrakk>y\<rbrakk>\<^sub>e b) (\<lbrakk>z\<rbrakk>\<^sub>e b)
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma qtop_ueval [ueval]: "\<lbrakk>qtop f x y z w\<rbrakk>\<^sub>eb = f (\<lbrakk>x\<rbrakk>\<^sub>eb) (\<lbrakk>y\<rbrakk>\<^sub>eb) (\<lbrakk>z\<rbrakk>\<^sub>eb) (\<lbrakk>w\<rbrakk>\<^sub>eb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qtop f x y z w\<rbrakk>\<^sub>e b = f (\<lbrakk>x\<rbrakk>\<^sub>e b) (\<lbrakk>y\<rbrakk>\<^sub>e b) (\<lbrakk>z\<rbrakk>\<^sub>e b) (\<lbrakk>w\<rbrakk>\<^sub>e b)
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma uop_const [simp]: "uop id u = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uop id u = u
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma bop_const_1 [simp]: "bop (\<lambda>x y. y) u v = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bop (\<lambda>x y. y) u v = v
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma bop_const_2 [simp]: "bop (\<lambda>x y. x) u v = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bop (\<lambda>x y. x) u v = u
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma uexpr_fst [simp]: "\<pi>\<^sub>1((e, f)\<^sub>u) = e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>1((e, f)\<^sub>u) = e
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma uexpr_snd [simp]: "\<pi>\<^sub>2((e, f)\<^sub>u) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>2((e, f)\<^sub>u) = f
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma lit_fun_simps [lit_simps]:
  "\<guillemotleft>i x y z u\<guillemotright> = qtop i \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright> \<guillemotleft>z\<guillemotright> \<guillemotleft>u\<guillemotright>"
  "\<guillemotleft>h x y z\<guillemotright> = trop h \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright> \<guillemotleft>z\<guillemotright>"
  "\<guillemotleft>g x y\<guillemotright> = bop g \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright>"
  "\<guillemotleft>f x\<guillemotright> = uop f \<guillemotleft>x\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<guillemotleft>i x y z u\<guillemotright> = qtop i \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright> \<guillemotleft>z\<guillemotright> \<guillemotleft>u\<guillemotright> &&& \<guillemotleft>h x y z\<guillemotright> = trop h \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright> \<guillemotleft>z\<guillemotright>) &&& \<guillemotleft>g x y\<guillemotright> = bop g \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright> &&& \<guillemotleft>f x\<guillemotright> = uop f \<guillemotleft>x\<guillemotright>
[PROOF STEP]
by (transfer, simp)+


[STATEMENT]
lemma numeral_uexpr_rep_eq [ueval]: "\<lbrakk>numeral x\<rbrakk>\<^sub>e b = numeral x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>numeral x\<rbrakk>\<^sub>e b = numeral x
[PROOF STEP]
apply (induct x)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Numeral1\<rbrakk>\<^sub>e b = Numeral1
 2. \<And>x. \<lbrakk>numeral x\<rbrakk>\<^sub>e b = numeral x \<Longrightarrow> \<lbrakk>numeral (num.Bit0 x)\<rbrakk>\<^sub>e b = numeral (num.Bit0 x)
 3. \<And>x. \<lbrakk>numeral x\<rbrakk>\<^sub>e b = numeral x \<Longrightarrow> \<lbrakk>numeral (num.Bit1 x)\<rbrakk>\<^sub>e b = numeral (num.Bit1 x)
[PROOF STEP]
apply (simp add: lit.rep_eq one_uexpr_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>numeral x\<rbrakk>\<^sub>e b = numeral x \<Longrightarrow> \<lbrakk>numeral (num.Bit0 x)\<rbrakk>\<^sub>e b = numeral (num.Bit0 x)
 2. \<And>x. \<lbrakk>numeral x\<rbrakk>\<^sub>e b = numeral x \<Longrightarrow> \<lbrakk>numeral (num.Bit1 x)\<rbrakk>\<^sub>e b = numeral (num.Bit1 x)
[PROOF STEP]
apply (simp add: bop.rep_eq numeral_Bit0 plus_uexpr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>numeral x\<rbrakk>\<^sub>e b = numeral x \<Longrightarrow> \<lbrakk>numeral (num.Bit1 x)\<rbrakk>\<^sub>e b = numeral (num.Bit1 x)
[PROOF STEP]
apply (simp add: bop.rep_eq lit.rep_eq numeral_code(3) one_uexpr_def plus_uexpr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma numeral_uexpr_simp: "numeral x = \<guillemotleft>numeral x\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. numeral x = \<guillemotleft>numeral x\<guillemotright>
[PROOF STEP]
by (simp add: uexpr_eq_iff numeral_uexpr_rep_eq lit.rep_eq)


[STATEMENT]
lemma lit_zero [lit_simps]: "\<guillemotleft>0\<guillemotright> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>0::'a\<guillemotright> = 0
[PROOF STEP]
by (simp add:uexpr_defs)


[STATEMENT]
lemma lit_one [lit_simps]: "\<guillemotleft>1\<guillemotright> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>1::'a\<guillemotright> = 1
[PROOF STEP]
by (simp add: uexpr_defs)


[STATEMENT]
lemma lit_plus [lit_simps]: "\<guillemotleft>x + y\<guillemotright> = \<guillemotleft>x\<guillemotright> + \<guillemotleft>y\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>x + y\<guillemotright> = \<guillemotleft>x\<guillemotright> + \<guillemotleft>y\<guillemotright>
[PROOF STEP]
by (simp add: uexpr_defs, transfer, simp)


[STATEMENT]
lemma lit_numeral [lit_simps]: "\<guillemotleft>numeral n\<guillemotright> = numeral n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>numeral n\<guillemotright> = numeral n
[PROOF STEP]
by (simp add: numeral_uexpr_simp)


[STATEMENT]
lemma lit_numeral_1: "uop numeral x = Abs_uexpr (\<lambda>b. numeral (\<lbrakk>x\<rbrakk>\<^sub>e b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uop numeral x = mk\<^sub>e (\<lambda>b. numeral (\<lbrakk>x\<rbrakk>\<^sub>e b))
[PROOF STEP]
by (simp add: uop_def)


[STATEMENT]
lemma lit_numeral_2: "Abs_uexpr (\<lambda> b. numeral v) = numeral v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk\<^sub>e (\<lambda>b. numeral v) = numeral v
[PROOF STEP]
by (metis lit.abs_eq lit_numeral)


[STATEMENT]
lemma "(1::(int, '\<alpha>) uexpr) + \<guillemotleft>2\<guillemotright> = 4 \<longleftrightarrow> \<guillemotleft>3\<guillemotright> = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + \<guillemotleft>2\<guillemotright> = 4) = (\<guillemotleft>3::'a\<guillemotright> = 4)
[PROOF STEP]
apply (literalise)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<guillemotleft>1 + 2\<guillemotright> = \<guillemotleft>4\<guillemotright>) = (\<guillemotleft>3::'a\<guillemotright> = \<guillemotleft>4::'a\<guillemotright>)
[PROOF STEP]
apply (uexpr_simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (3 = 4) = (3 = 4)
[PROOF STEP]
oops


[STATEMENT]
lemma tag_both: "\<lbrakk> (Let x f,Let x' f')\<in>R \<rbrakk> \<Longrightarrow> (f x,f' x')\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Let x f, Let x' f') \<in> R \<Longrightarrow> (f x, f' x') \<in> R
[PROOF STEP]
by simp


[STATEMENT]
lemma tag_rhs: "\<lbrakk> (c,Let x f)\<in>R \<rbrakk> \<Longrightarrow> (c,f x)\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, Let x f) \<in> R \<Longrightarrow> (c, f x) \<in> R
[PROOF STEP]
by simp


[STATEMENT]
lemma tag_lhs: "\<lbrakk> (Let x f,a)\<in>R \<rbrakk> \<Longrightarrow> (f x,a)\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Let x f, a) \<in> R \<Longrightarrow> (f x, a) \<in> R
[PROOF STEP]
by simp


[STATEMENT]
lemma tagged_fun_relD_both:
    "\<lbrakk> (f,f')\<in>A\<rightarrow>B; (x,x')\<in>A \<rbrakk> \<Longrightarrow> (Let x f,Let x' f')\<in>B"
    and tagged_fun_relD_rhs: "\<lbrakk> (f,f')\<in>A\<rightarrow>B; (x,x')\<in>A \<rbrakk> \<Longrightarrow> (f x,Let x' f')\<in>B"
    and tagged_fun_relD_lhs: "\<lbrakk> (f,f')\<in>A\<rightarrow>B; (x,x')\<in>A \<rbrakk> \<Longrightarrow> (Let x f,f' x')\<in>B"
    and tagged_fun_relD_none: "\<lbrakk> (f,f')\<in>A\<rightarrow>B; (x,x')\<in>A \<rbrakk> \<Longrightarrow> (f x,f' x')\<in>B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>(f, f') \<in> A \<rightarrow> B; (x, x') \<in> A\<rbrakk> \<Longrightarrow> (Let x f, Let x' f') \<in> B) &&& (\<lbrakk>(f, f') \<in> A \<rightarrow> B; (x, x') \<in> A\<rbrakk> \<Longrightarrow> (f x, Let x' f') \<in> B)) &&& (\<lbrakk>(f, f') \<in> A \<rightarrow> B; (x, x') \<in> A\<rbrakk> \<Longrightarrow> (Let x f, f' x') \<in> B) &&& (\<lbrakk>(f, f') \<in> A \<rightarrow> B; (x, x') \<in> A\<rbrakk> \<Longrightarrow> (f x, f' x') \<in> B)
[PROOF STEP]
by (simp_all add: fun_relD)


[STATEMENT]
lemma fmapU_eq_fmap: "fmapU = fmap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmapU = fmap
[PROOF STEP]
by (simp add: fmap_def eta_cfun)


[STATEMENT]
lemma fmap_eq_fmapU: "fmap = fmapU"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap = fmapU
[PROOF STEP]
by (simp only: fmapU_eq_fmap)


[STATEMENT]
lemma cast_TC:
  "cast\<cdot>(TC('f)\<cdot>t) = emb oo fmapU\<cdot>(cast\<cdot>t) oo PRJ(udom\<cdot>'f::prefunctor)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast\<cdot>(TC('f)\<cdot>t) = EMB(udom\<cdot>'f) oo fmapU\<cdot>(cast\<cdot>t) oo PRJ(udom\<cdot>'f)
[PROOF STEP]
by (rule isodefl_fmapU [unfolded isodefl_def])


[STATEMENT]
lemma isodefl_cast: "isodefl (cast\<cdot>t) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isodefl (cast\<cdot>t) t
[PROOF STEP]
by (simp add: isodefl_def)


[STATEMENT]
lemma cast_cast_below1: "A \<sqsubseteq> B \<Longrightarrow> cast\<cdot>A\<cdot>(cast\<cdot>B\<cdot>x) = cast\<cdot>A\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq> B \<Longrightarrow> cast\<cdot>A\<cdot>(cast\<cdot>B\<cdot>x) = cast\<cdot>A\<cdot>x
[PROOF STEP]
by (intro deflation_below_comp1 deflation_cast monofun_cfun_arg)


[STATEMENT]
lemma cast_cast_below2: "A \<sqsubseteq> B \<Longrightarrow> cast\<cdot>B\<cdot>(cast\<cdot>A\<cdot>x) = cast\<cdot>A\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq> B \<Longrightarrow> cast\<cdot>B\<cdot>(cast\<cdot>A\<cdot>x) = cast\<cdot>A\<cdot>x
[PROOF STEP]
by (intro deflation_below_comp2 deflation_cast monofun_cfun_arg)


[STATEMENT]
lemma isodefl_fmap:
  assumes "isodefl d t"
  shows "isodefl (fmap\<cdot>d :: 'a\<cdot>'f \<rightarrow> _) (TC('f::functor)\<cdot>t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isodefl (fmap\<cdot>d) (TC('f)\<cdot>t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isodefl (fmap\<cdot>d) (TC('f)\<cdot>t)
[PROOF STEP]
have deflation_d: "deflation d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deflation d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isodefl d t

goal (1 subgoal):
 1. deflation d
[PROOF STEP]
by (rule isodefl_imp_deflation)
[PROOF STATE]
proof (state)
this:
deflation d

goal (1 subgoal):
 1. isodefl (fmap\<cdot>d) (TC('f)\<cdot>t)
[PROOF STEP]
have cast_t: "cast\<cdot>t = emb oo d oo prj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast\<cdot>t = EMB('a) oo d oo PRJ('a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isodefl d t

goal (1 subgoal):
 1. cast\<cdot>t = EMB('a) oo d oo PRJ('a)
[PROOF STEP]
unfolding isodefl_def
[PROOF STATE]
proof (prove)
using this:
cast\<cdot>t = EMB('a) oo d oo PRJ('a)

goal (1 subgoal):
 1. cast\<cdot>t = EMB('a) oo d oo PRJ('a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cast\<cdot>t = EMB('a) oo d oo PRJ('a)

goal (1 subgoal):
 1. isodefl (fmap\<cdot>d) (TC('f)\<cdot>t)
[PROOF STEP]
have t_below: "t \<sqsubseteq> DEFL('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<sqsubseteq> DEFL('a)
[PROOF STEP]
apply (rule cast_below_imp_below)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast\<cdot>t \<sqsubseteq> cast\<cdot>DEFL('a)
[PROOF STEP]
apply (simp only: cast_t cast_DEFL)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EMB('a) oo d oo PRJ('a) \<sqsubseteq> EMB('a) oo PRJ('a)
[PROOF STEP]
apply (simp add: cfun_below_iff deflation.below [OF deflation_d])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
t \<sqsubseteq> DEFL('a)

goal (1 subgoal):
 1. isodefl (fmap\<cdot>d) (TC('f)\<cdot>t)
[PROOF STEP]
have fmap_eq: "fmap\<cdot>d = PRJ('a\<cdot>'f) oo cast\<cdot>(TC('f)\<cdot>t) oo emb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>d = PRJ('a\<cdot>'f) oo cast\<cdot>(TC('f)\<cdot>t) oo EMB('a\<cdot>'f)
[PROOF STEP]
by (simp add: fmap_def coerce_cfun cast_TC cast_t prj_emb cfcomp1)
[PROOF STATE]
proof (state)
this:
fmap\<cdot>d = PRJ('a\<cdot>'f) oo cast\<cdot>(TC('f)\<cdot>t) oo EMB('a\<cdot>'f)

goal (1 subgoal):
 1. isodefl (fmap\<cdot>d) (TC('f)\<cdot>t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isodefl (fmap\<cdot>d) (TC('f)\<cdot>t)
[PROOF STEP]
apply (simp add: fmap_eq isodefl_def cfun_eq_iff emb_prj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. cast\<cdot>(TC('f)\<cdot>t)\<cdot>x = cast\<cdot>DEFL('a\<cdot>'f)\<cdot>(cast\<cdot>(TC('f)\<cdot>t)\<cdot>(cast\<cdot>DEFL('a\<cdot>'f)\<cdot>x))
[PROOF STEP]
apply (simp add: DEFL_app)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. cast\<cdot>(TC('f)\<cdot>t)\<cdot>x = cast\<cdot>(TC('f)\<cdot>DEFL('a))\<cdot>(cast\<cdot>(TC('f)\<cdot>t)\<cdot>(cast\<cdot>(TC('f)\<cdot>DEFL('a))\<cdot>x))
[PROOF STEP]
apply (simp add: cast_cast_below1 monofun_cfun t_below)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. cast\<cdot>(TC('f)\<cdot>t)\<cdot>x = cast\<cdot>(TC('f)\<cdot>DEFL('a))\<cdot>(cast\<cdot>(TC('f)\<cdot>t)\<cdot>x)
[PROOF STEP]
apply (simp add: cast_cast_below2 monofun_cfun t_below)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
isodefl (fmap\<cdot>d) (TC('f)\<cdot>t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fmap_ID [simp]: "fmap\<cdot>ID = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>ID = ID
[PROOF STEP]
apply (rule isodefl_DEFL_imp_ID)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isodefl (fmap\<cdot>ID) DEFL('a\<cdot>'b)
[PROOF STEP]
apply (subst DEFL_app)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isodefl (fmap\<cdot>ID) (TC('b)\<cdot>DEFL('a))
[PROOF STEP]
apply (rule isodefl_fmap)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isodefl ID DEFL('a)
[PROOF STEP]
apply (rule isodefl_ID_DEFL)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fmap_ident [simp]: "fmap\<cdot>(\<Lambda> x. x) = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>(\<Lambda> x. x) = ID
[PROOF STEP]
by (simp add: ID_def [symmetric])


[STATEMENT]
lemma coerce_coerce_eq_fmapU_cast [coerce_simp]:
  fixes xs :: "udom\<cdot>'f::functor"
  shows "COERCE('a\<cdot>'f, udom\<cdot>'f)\<cdot>(COERCE(udom\<cdot>'f, 'a\<cdot>'f)\<cdot>xs) =
    fmapU\<cdot>(cast\<cdot>DEFL('a))\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE('a\<cdot>'f, udom\<cdot>'f)\<cdot>(COERCE(udom\<cdot>'f, 'a\<cdot>'f)\<cdot>xs) = fmapU\<cdot>(cast\<cdot>DEFL('a))\<cdot>xs
[PROOF STEP]
by (simp add: coerce_def emb_prj DEFL_app cast_TC)


[STATEMENT]
lemma fmap_fmap:
  fixes xs :: "'a\<cdot>'f::functor" and g :: "'a \<rightarrow> 'b" and f :: "'b \<rightarrow> 'c"
  shows "fmap\<cdot>f\<cdot>(fmap\<cdot>g\<cdot>xs) = fmap\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>(fmap\<cdot>g\<cdot>xs) = fmap\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs
[PROOF STEP]
unfolding fmap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE((udom \<rightarrow> udom) \<rightarrow> udom\<cdot>'f \<rightarrow> udom\<cdot>'f, ('b \<rightarrow> 'c) \<rightarrow> 'b\<cdot>'f \<rightarrow> 'c\<cdot>'f)\<cdot>fmapU\<cdot>f\<cdot>(COERCE((udom \<rightarrow> udom) \<rightarrow> udom\<cdot>'f \<rightarrow> udom\<cdot>'f, ('a \<rightarrow> 'b) \<rightarrow> 'a\<cdot>'f \<rightarrow> 'b\<cdot>'f)\<cdot>fmapU\<cdot>g\<cdot>xs) = COERCE((udom \<rightarrow> udom) \<rightarrow> udom\<cdot>'f \<rightarrow> udom\<cdot>'f, ('a \<rightarrow> 'c) \<rightarrow> 'a\<cdot>'f \<rightarrow> 'c\<cdot>'f)\<cdot>fmapU\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs
[PROOF STEP]
by (simp add: coerce_simp)


[STATEMENT]
lemma fmap_cfcomp: "fmap\<cdot>(f oo g) = fmap\<cdot>f oo fmap\<cdot>g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>(f oo g) = fmap\<cdot>f oo fmap\<cdot>g
[PROOF STEP]
by (simp add: cfcomp1 fmap_fmap eta_cfun)


[STATEMENT]
lemma deflation_fmap:
  "deflation d \<Longrightarrow> deflation (fmap\<cdot>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deflation d \<Longrightarrow> deflation (fmap\<cdot>d)
[PROOF STEP]
apply (rule deflation.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. deflation d \<Longrightarrow> fmap\<cdot>d\<cdot>(fmap\<cdot>d\<cdot>x) = fmap\<cdot>d\<cdot>x
 2. \<And>x. deflation d \<Longrightarrow> fmap\<cdot>d\<cdot>x \<sqsubseteq> x
[PROOF STEP]
apply (simp add: fmap_fmap deflation.idem eta_cfun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. deflation d \<Longrightarrow> fmap\<cdot>d\<cdot>x \<sqsubseteq> x
[PROOF STEP]
apply (subgoal_tac "fmap\<cdot>d\<cdot>x \<sqsubseteq> fmap\<cdot>ID\<cdot>x", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. deflation d \<Longrightarrow> fmap\<cdot>d\<cdot>x \<sqsubseteq> fmap\<cdot>ID\<cdot>x
[PROOF STEP]
apply (rule monofun_cfun_fun, rule monofun_cfun_arg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. deflation d \<Longrightarrow> d \<sqsubseteq> ID
[PROOF STEP]
apply (erule deflation.below_ID)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ep_pair_fmap:
  "ep_pair e p \<Longrightarrow> ep_pair (fmap\<cdot>e) (fmap\<cdot>p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ep_pair e p \<Longrightarrow> ep_pair (fmap\<cdot>e) (fmap\<cdot>p)
[PROOF STEP]
apply (rule ep_pair.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. ep_pair e p \<Longrightarrow> fmap\<cdot>p\<cdot>(fmap\<cdot>e\<cdot>x) = x
 2. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>e\<cdot>(fmap\<cdot>p\<cdot>y) \<sqsubseteq> y
[PROOF STEP]
apply (simp add: fmap_fmap ep_pair.e_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>e\<cdot>(fmap\<cdot>p\<cdot>y) \<sqsubseteq> y
[PROOF STEP]
apply (simp add: fmap_fmap)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>(\<Lambda> x. e\<cdot>(p\<cdot>x))\<cdot>y \<sqsubseteq> y
[PROOF STEP]
apply (rule_tac y="fmap\<cdot>ID\<cdot>y" in below_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>(\<Lambda> x. e\<cdot>(p\<cdot>x))\<cdot>y \<sqsubseteq> fmap\<cdot>ID\<cdot>y
 2. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>ID\<cdot>y \<sqsubseteq> y
[PROOF STEP]
apply (rule monofun_cfun_fun)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>(\<Lambda> x. e\<cdot>(p\<cdot>x)) \<sqsubseteq> fmap\<cdot>ID
 2. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>ID\<cdot>y \<sqsubseteq> y
[PROOF STEP]
apply (rule monofun_cfun_arg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. ep_pair e p \<Longrightarrow> (\<Lambda> x. e\<cdot>(p\<cdot>x)) \<sqsubseteq> ID
 2. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>ID\<cdot>y \<sqsubseteq> y
[PROOF STEP]
apply (rule cfun_belowI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. ep_pair e p \<Longrightarrow> e\<cdot>(p\<cdot>x) \<sqsubseteq> x
 2. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>ID\<cdot>y \<sqsubseteq> y
[PROOF STEP]
apply (erule ep_pair.e_p_below)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. ep_pair e p \<Longrightarrow> fmap\<cdot>ID\<cdot>y \<sqsubseteq> y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fmap_strict:
  fixes f :: "'a \<rightarrow> 'b"
  assumes "f\<cdot>\<bottom> = \<bottom>" shows "fmap\<cdot>f\<cdot>\<bottom> = (\<bottom>::'b\<cdot>'f::functor)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
proof (rule bottomI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
have "fmap\<cdot>f\<cdot>(\<bottom>::'a\<cdot>'f) \<sqsubseteq> fmap\<cdot>f\<cdot>(fmap\<cdot>\<bottom>\<cdot>(\<bottom>::'b\<cdot>'f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fmap\<cdot>f\<cdot>(fmap\<cdot>\<bottom>\<cdot>\<bottom>)
[PROOF STEP]
by (simp add: monofun_cfun)
[PROOF STATE]
proof (state)
this:
fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fmap\<cdot>f\<cdot>(fmap\<cdot>\<bottom>\<cdot>\<bottom>)

goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fmap\<cdot>f\<cdot>(fmap\<cdot>\<bottom>\<cdot>\<bottom>)

goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
have "... = fmap\<cdot>(\<Lambda> x. f\<cdot>(\<bottom>\<cdot>x))\<cdot>(\<bottom>::'b\<cdot>'f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>(fmap\<cdot>\<bottom>\<cdot>\<bottom>) = fmap\<cdot>(\<Lambda> x. f\<cdot>(\<bottom>\<cdot>x))\<cdot>\<bottom>
[PROOF STEP]
by (simp add: fmap_fmap)
[PROOF STATE]
proof (state)
this:
fmap\<cdot>f\<cdot>(fmap\<cdot>\<bottom>\<cdot>\<bottom>) = fmap\<cdot>(\<Lambda> x. f\<cdot>(\<bottom>\<cdot>x))\<cdot>\<bottom>

goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fmap\<cdot>f\<cdot>(fmap\<cdot>\<bottom>\<cdot>\<bottom>) = fmap\<cdot>(\<Lambda> x. f\<cdot>(\<bottom>\<cdot>x))\<cdot>\<bottom>

goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
have "... \<sqsubseteq> fmap\<cdot>ID\<cdot>\<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>(\<Lambda> x. f\<cdot>(\<bottom>\<cdot>x))\<cdot>\<bottom> \<sqsubseteq> fmap\<cdot>ID\<cdot>\<bottom>
[PROOF STEP]
by (simp add: monofun_cfun assms del: fmap_ID)
[PROOF STATE]
proof (state)
this:
fmap\<cdot>(\<Lambda> x. f\<cdot>(\<bottom>\<cdot>x))\<cdot>\<bottom> \<sqsubseteq> fmap\<cdot>ID\<cdot>\<bottom>

goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fmap\<cdot>(\<Lambda> x. f\<cdot>(\<bottom>\<cdot>x))\<cdot>\<bottom> \<sqsubseteq> fmap\<cdot>ID\<cdot>\<bottom>

goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
have "... = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>ID\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fmap\<cdot>ID\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
show "fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> (\<bottom>::'b\<cdot>'f::functor)"
[PROOF STATE]
proof (prove)
using this:
fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>

goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fmap\<cdot>f\<cdot>\<bottom> \<sqsubseteq> \<bottom>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fmapU_cast_eq:
  "fmapU\<cdot>(cast\<cdot>A) =
    PRJ(udom\<cdot>'f) oo cast\<cdot>(TC('f::functor)\<cdot>A) oo emb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmapU\<cdot>(cast\<cdot>A) = PRJ(udom\<cdot>'f) oo cast\<cdot>(TC('f)\<cdot>A) oo EMB(udom\<cdot>'f)
[PROOF STEP]
by (subst cast_TC, rule cfun_eqI, simp)


[STATEMENT]
lemma fmapU_cast_DEFL:
  "fmapU\<cdot>(cast\<cdot>DEFL('a)) =
    PRJ(udom\<cdot>'f) oo cast\<cdot>DEFL('a\<cdot>'f::functor) oo emb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmapU\<cdot>(cast\<cdot>DEFL('a)) = PRJ(udom\<cdot>'f) oo cast\<cdot>DEFL('a\<cdot>'f) oo EMB(udom\<cdot>'f)
[PROOF STEP]
by (simp add: fmapU_cast_eq DEFL_app)


[STATEMENT]
lemma coerce_functor: "COERCE('a\<cdot>'f, 'b\<cdot>'f::functor) = fmap\<cdot>coerce"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE('a\<cdot>'f, 'b\<cdot>'f) = fmap\<cdot>COERCE('a, 'b)
[PROOF STEP]
apply (rule cfun_eqI, rename_tac xs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. COERCE('a\<cdot>'f, 'b\<cdot>'f)\<cdot>xs = fmap\<cdot>COERCE('a, 'b)\<cdot>xs
[PROOF STEP]
apply (simp add: fmap_def coerce_cfun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. COERCE('a\<cdot>'f, 'b\<cdot>'f)\<cdot>xs = COERCE(udom\<cdot>'f, 'b\<cdot>'f)\<cdot>(fmapU\<cdot>(EMB('b) oo COERCE('a, 'b) oo PRJ('a))\<cdot>(COERCE('a\<cdot>'f, udom\<cdot>'f)\<cdot>xs))
[PROOF STEP]
apply (simp add: coerce_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. PRJ('b\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs) = PRJ('b\<cdot>'f)\<cdot>(EMB(udom\<cdot>'f)\<cdot>(fmapU\<cdot>(EMB('b) oo (PRJ('b) oo EMB('a)) oo PRJ('a))\<cdot>(PRJ(udom\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs))))
[PROOF STEP]
apply (simp add: cfcomp1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. PRJ('b\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs) = PRJ('b\<cdot>'f)\<cdot>(EMB(udom\<cdot>'f)\<cdot>(fmapU\<cdot>(\<Lambda> x. EMB('b)\<cdot>(PRJ('b)\<cdot>(EMB('a)\<cdot>(PRJ('a)\<cdot>x))))\<cdot>(PRJ(udom\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs))))
[PROOF STEP]
apply (simp only: emb_prj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. PRJ('b\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs) = PRJ('b\<cdot>'f)\<cdot>(EMB(udom\<cdot>'f)\<cdot>(fmapU\<cdot>(\<Lambda> x. cast\<cdot>DEFL('b)\<cdot>(cast\<cdot>DEFL('a)\<cdot>x))\<cdot>(PRJ(udom\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs))))
[PROOF STEP]
apply (subst fmapU_fmapU [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. PRJ('b\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs) = PRJ('b\<cdot>'f)\<cdot>(EMB(udom\<cdot>'f)\<cdot>(fmapU\<cdot>(cast\<cdot>DEFL('b))\<cdot>(fmapU\<cdot>(cast\<cdot>DEFL('a))\<cdot>(PRJ(udom\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs)))))
[PROOF STEP]
apply (simp add: fmapU_cast_DEFL)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. PRJ('b\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs) = PRJ('b\<cdot>'f)\<cdot>(EMB(udom\<cdot>'f)\<cdot>(PRJ(udom\<cdot>'f)\<cdot>(cast\<cdot>DEFL('b\<cdot>'f)\<cdot>(EMB(udom\<cdot>'f)\<cdot>(PRJ(udom\<cdot>'f)\<cdot>(cast\<cdot>DEFL('a\<cdot>'f)\<cdot>(EMB(udom\<cdot>'f)\<cdot>(PRJ(udom\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs)))))))))
[PROOF STEP]
apply (simp add: emb_prj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. PRJ('b\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs) = PRJ('b\<cdot>'f)\<cdot>(cast\<cdot>DEFL(udom\<cdot>'f)\<cdot>(cast\<cdot>DEFL('b\<cdot>'f)\<cdot>(cast\<cdot>DEFL(udom\<cdot>'f)\<cdot>(cast\<cdot>DEFL('a\<cdot>'f)\<cdot>(cast\<cdot>DEFL(udom\<cdot>'f)\<cdot>(EMB('a\<cdot>'f)\<cdot>xs))))))
[PROOF STEP]
apply (simp add: cast_cast_below1 cast_cast_below2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fmapU_cast_coerce [coerce_simp]:
  fixes m :: "'a\<cdot>'f::functor"
  shows "fmapU\<cdot>(cast\<cdot>DEFL('a))\<cdot>(COERCE('a\<cdot>'f, udom\<cdot>'f)\<cdot>m) =
    COERCE('a\<cdot>'f, udom\<cdot>'f)\<cdot>m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmapU\<cdot>(cast\<cdot>DEFL('a))\<cdot>(COERCE('a\<cdot>'f, udom\<cdot>'f)\<cdot>m) = COERCE('a\<cdot>'f, udom\<cdot>'f)\<cdot>m
[PROOF STEP]
by (simp add: coerce_functor cast_DEFL fmapU_eq_fmap fmap_fmap eta_cfun)


[STATEMENT]
lemma coerce_fmap [coerce_simp]:
  fixes xs :: "'a\<cdot>'f::functor" and f :: "'a \<rightarrow> 'b"
  shows "COERCE('b\<cdot>'f, 'c\<cdot>'f)\<cdot>(fmap\<cdot>f\<cdot>xs) = fmap\<cdot>(\<Lambda> x. COERCE('b,'c)\<cdot>(f\<cdot>x))\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE('b\<cdot>'f, 'c\<cdot>'f)\<cdot>(fmap\<cdot>f\<cdot>xs) = fmap\<cdot>(\<Lambda> x. COERCE('b, 'c)\<cdot>(f\<cdot>x))\<cdot>xs
[PROOF STEP]
by (simp add: coerce_functor fmap_fmap)


[STATEMENT]
lemma fmap_coerce [coerce_simp]:
  fixes xs :: "'a\<cdot>'f::functor" and f :: "'b \<rightarrow> 'c"
  shows "fmap\<cdot>f\<cdot>(COERCE('a\<cdot>'f, 'b\<cdot>'f)\<cdot>xs) = fmap\<cdot>(\<Lambda> x. f\<cdot>(COERCE('a,'b)\<cdot>x))\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>(COERCE('a\<cdot>'f, 'b\<cdot>'f)\<cdot>xs) = fmap\<cdot>(\<Lambda> x. f\<cdot>(COERCE('a, 'b)\<cdot>x))\<cdot>xs
[PROOF STEP]
by (simp add: coerce_functor fmap_fmap)


[STATEMENT]
lemma show_law_complex [show_law_intros]:
  "show_law showsp_complex r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. show_law showsp_complex r
[PROOF STEP]
by (rule show_lawI) (simp add: showsp_complex_def show_law_simps)


[STATEMENT]
lemma showsp_complex_append [show_law_simps]:
  "showsp_complex p r (x @ y) = showsp_complex p r x @ y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. showsp_complex p r (x @ y) = showsp_complex p r x @ y
[PROOF STEP]
by (intro show_lawD show_law_intros)


[STATEMENT]
lemma pick[simp]: "x \<in> X \<Longrightarrow> pick X \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X \<Longrightarrow> pick X \<in> X
[PROOF STEP]
unfolding pick_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X \<Longrightarrow> (SOME x. x \<in> X) \<in> X
[PROOF STEP]
by (metis someI_ex)


[STATEMENT]
lemma pick_NE[simp]: "X \<noteq> {} \<Longrightarrow> pick X \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> pick X \<in> X
[PROOF STEP]
by auto


[STATEMENT]
lemma clinear_compose: "clinear f \<Longrightarrow> clinear g \<Longrightarrow> clinear (g \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>clinear f; clinear g\<rbrakk> \<Longrightarrow> clinear (g \<circ> f)
[PROOF STEP]
unfolding clinear_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Vector_Spaces.linear (*\<^sub>C) (*\<^sub>C) f; Vector_Spaces.linear (*\<^sub>C) (*\<^sub>C) g\<rbrakk> \<Longrightarrow> Vector_Spaces.linear (*\<^sub>C) (*\<^sub>C) (g \<circ> f)
[PROOF STEP]
by (rule Vector_Spaces.linear_compose)


[STATEMENT]
lemma divideC_field_simps[field_simps]: (* In Real_Vector_Spaces, these lemmas are unnamed *)
  "c \<noteq> 0 \<Longrightarrow> a = b /\<^sub>C c \<longleftrightarrow> c *\<^sub>C a = b"
  "c \<noteq> 0 \<Longrightarrow> b /\<^sub>C c = a \<longleftrightarrow> b = c *\<^sub>C a"
  "c \<noteq> 0 \<Longrightarrow> a + b /\<^sub>C c = (c *\<^sub>C a + b) /\<^sub>C c"
  "c \<noteq> 0 \<Longrightarrow> a /\<^sub>C c + b = (a + c *\<^sub>C b) /\<^sub>C c"
  "c \<noteq> 0 \<Longrightarrow> a - b /\<^sub>C c = (c *\<^sub>C a - b) /\<^sub>C c"
  "c \<noteq> 0 \<Longrightarrow> a /\<^sub>C c - b = (a - c *\<^sub>C b) /\<^sub>C c"
  "c \<noteq> 0 \<Longrightarrow> - (a /\<^sub>C c) + b = (- a + c *\<^sub>C b) /\<^sub>C c"
  "c \<noteq> 0 \<Longrightarrow> - (a /\<^sub>C c) - b = (- a - c *\<^sub>C b) /\<^sub>C c"
  for a b :: "'a :: complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((c \<noteq> 0 \<Longrightarrow> (a = b /\<^sub>C c) = (c *\<^sub>C a = b)) &&& (c \<noteq> 0 \<Longrightarrow> (b /\<^sub>C c = a) = (b = c *\<^sub>C a))) &&& (c \<noteq> 0 \<Longrightarrow> a + b /\<^sub>C c = (c *\<^sub>C a + b) /\<^sub>C c) &&& (c \<noteq> 0 \<Longrightarrow> a /\<^sub>C c + b = (a + c *\<^sub>C b) /\<^sub>C c)) &&& ((c \<noteq> 0 \<Longrightarrow> a - b /\<^sub>C c = (c *\<^sub>C a - b) /\<^sub>C c) &&& (c \<noteq> 0 \<Longrightarrow> a /\<^sub>C c - b = (a - c *\<^sub>C b) /\<^sub>C c)) &&& (c \<noteq> 0 \<Longrightarrow> - (a /\<^sub>C c) + b = (- a + c *\<^sub>C b) /\<^sub>C c) &&& (c \<noteq> 0 \<Longrightarrow> - (a /\<^sub>C c) - b = (- a - c *\<^sub>C b) /\<^sub>C c)
[PROOF STEP]
by (auto simp add: scaleC_add_right scaleC_add_left scaleC_diff_right scaleC_diff_left)


[STATEMENT]
lemma scaleC_minus1_left [simp]: "scaleC (-1) x = - x"
  for x :: "'a::complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 *\<^sub>C x = - x
[PROOF STEP]
using scaleC_minus_left [of 1 x]
[PROOF STATE]
proof (prove)
using this:
- 1 *\<^sub>C x = - (1 *\<^sub>C x)

goal (1 subgoal):
 1. - 1 *\<^sub>C x = - x
[PROOF STEP]
by simp


[STATEMENT]
lemma scaleC_2:
  fixes x :: "'a::complex_vector"
  shows "scaleC 2 x = x + x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 *\<^sub>C x = x + x
[PROOF STEP]
unfolding one_add_one [symmetric] scaleC_add_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 *\<^sub>C x + 1 *\<^sub>C x = x + x
[PROOF STEP]
by simp


[STATEMENT]
lemma scaleC_half_double [simp]:
  fixes a :: "'a::complex_vector"
  shows "(1 / 2) *\<^sub>C (a + a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 / 2) *\<^sub>C (a + a) = a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1 / 2) *\<^sub>C (a + a) = a
[PROOF STEP]
have "\<And>r. r *\<^sub>C (a + a) = (r * 2) *\<^sub>C a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r *\<^sub>C (a + a) = (r * 2) *\<^sub>C a
[PROOF STEP]
by (metis scaleC_2 scaleC_scaleC)
[PROOF STATE]
proof (state)
this:
?r *\<^sub>C (a + a) = (?r * 2) *\<^sub>C a

goal (1 subgoal):
 1. (1 / 2) *\<^sub>C (a + a) = a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?r *\<^sub>C (a + a) = (?r * 2) *\<^sub>C a

goal (1 subgoal):
 1. (1 / 2) *\<^sub>C (a + a) = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 / 2) *\<^sub>C (a + a) = a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clinear_scale_complex:
  fixes c::complex shows "clinear f \<Longrightarrow> f (c * b) = c * f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear f \<Longrightarrow> f (c * b) = c * f b
[PROOF STEP]
using complex_vector.linear_scale
[PROOF STATE]
proof (prove)
using this:
clinear ?f \<Longrightarrow> ?f (?r *\<^sub>C ?b) = ?r *\<^sub>C ?f ?b

goal (1 subgoal):
 1. clinear f \<Longrightarrow> f (c * b) = c * f b
[PROOF STEP]
by fastforce


[STATEMENT]
lemma nonzero_inverse_scaleC_distrib:
  "a \<noteq> 0 \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> inverse (scaleC a x) = scaleC (inverse a) (inverse x)"
  for x :: "'a::complex_div_algebra"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 0; x \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> inverse (a *\<^sub>C x) = inverse x /\<^sub>C a
[PROOF STEP]
by (rule inverse_unique) simp


[STATEMENT]
lemma inverse_scaleC_distrib: "inverse (scaleC a x) = scaleC (inverse a) (inverse x)"
  for x :: "'a::{complex_div_algebra,division_ring}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (a *\<^sub>C x) = inverse x /\<^sub>C a
[PROOF STEP]
by (metis inverse_zero nonzero_inverse_scaleC_distrib complex_vector.scale_eq_0_iff)


[STATEMENT]
lemma complex_add_divide_simps[vector_add_divide_simps]:  (* In Real_Vector_Spaces, these lemmas are unnamed *)
  "v + (b / z) *\<^sub>C w = (if z = 0 then v else (z *\<^sub>C v + b *\<^sub>C w) /\<^sub>C z)"
  "a *\<^sub>C v + (b / z) *\<^sub>C w = (if z = 0 then a *\<^sub>C v else ((a * z) *\<^sub>C v + b *\<^sub>C w) /\<^sub>C z)"
  "(a / z) *\<^sub>C v + w = (if z = 0 then w else (a *\<^sub>C v + z *\<^sub>C w) /\<^sub>C z)"
  "(a / z) *\<^sub>C v + b *\<^sub>C w = (if z = 0 then b *\<^sub>C w else (a *\<^sub>C v + (b * z) *\<^sub>C w) /\<^sub>C z)"
  "v - (b / z) *\<^sub>C w = (if z = 0 then v else (z *\<^sub>C v - b *\<^sub>C w) /\<^sub>C z)"
  "a *\<^sub>C v - (b / z) *\<^sub>C w = (if z = 0 then a *\<^sub>C v else ((a * z) *\<^sub>C v - b *\<^sub>C w) /\<^sub>C z)"
  "(a / z) *\<^sub>C v - w = (if z = 0 then -w else (a *\<^sub>C v - z *\<^sub>C w) /\<^sub>C z)"
  "(a / z) *\<^sub>C v - b *\<^sub>C w = (if z = 0 then -b *\<^sub>C w else (a *\<^sub>C v - (b * z) *\<^sub>C w) /\<^sub>C z)"
  for v :: "'a :: complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v + (b / z) *\<^sub>C w = (if z = 0 then v else (z *\<^sub>C v + b *\<^sub>C w) /\<^sub>C z) &&& a *\<^sub>C v + (b / z) *\<^sub>C w = (if z = 0 then a *\<^sub>C v else ((a * z) *\<^sub>C v + b *\<^sub>C w) /\<^sub>C z)) &&& (a / z) *\<^sub>C v + w = (if z = 0 then w else (a *\<^sub>C v + z *\<^sub>C w) /\<^sub>C z) &&& (a / z) *\<^sub>C v + b *\<^sub>C w = (if z = 0 then b *\<^sub>C w else (a *\<^sub>C v + (b * z) *\<^sub>C w) /\<^sub>C z)) &&& (v - (b / z) *\<^sub>C w = (if z = 0 then v else (z *\<^sub>C v - b *\<^sub>C w) /\<^sub>C z) &&& a *\<^sub>C v - (b / z) *\<^sub>C w = (if z = 0 then a *\<^sub>C v else ((a * z) *\<^sub>C v - b *\<^sub>C w) /\<^sub>C z)) &&& (a / z) *\<^sub>C v - w = (if z = 0 then - w else (a *\<^sub>C v - z *\<^sub>C w) /\<^sub>C z) &&& (a / z) *\<^sub>C v - b *\<^sub>C w = (if z = 0 then - b *\<^sub>C w else (a *\<^sub>C v - (b * z) *\<^sub>C w) /\<^sub>C z)
[PROOF STEP]
by (simp_all add: divide_inverse_commute scaleC_add_right scaleC_diff_right)


[STATEMENT]
lemma ceq_vector_fraction_iff [vector_add_divide_simps]:
  fixes x :: "'a :: complex_vector"
  shows "(x = (u / v) *\<^sub>C a) \<longleftrightarrow> (if v=0 then x = 0 else v *\<^sub>C x = u *\<^sub>C a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = (u / v) *\<^sub>C a) = (if v = 0 then x = (0::'a) else v *\<^sub>C x = u *\<^sub>C a)
[PROOF STEP]
by auto (metis (no_types) divide_eq_1_iff divide_inverse_commute scaleC_one scaleC_scaleC)


[STATEMENT]
lemma cvector_fraction_eq_iff [vector_add_divide_simps]:
  fixes x :: "'a :: complex_vector"
  shows "((u / v) *\<^sub>C a = x) \<longleftrightarrow> (if v=0 then x = 0 else u *\<^sub>C a = v *\<^sub>C x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((u / v) *\<^sub>C a = x) = (if v = 0 then x = (0::'a) else u *\<^sub>C a = v *\<^sub>C x)
[PROOF STEP]
by (metis ceq_vector_fraction_iff)