# Theory WhileLangLemmas

```section "Lemmas about the While language"

theory WhileLangLemmas imports WhileLang Coinductive.Coinductive_List_Prefix begin

lemma NRC_step_deterministic:
"star_n step n x y ⟹ star_n step n x z ⟹ y = z"
proof (induct rule: star_n.induct)
case (refl_n x)
then show ?case
apply -
by (erule star_n.cases; simp)
next
case (step_n x y n z)
then show ?case
apply (rotate_tac 3)
apply (erule star_n.cases, simp)
apply simp
apply (drule (1) step_deterministic)
by simp
qed

inductive exec where
exec_skip:   "exec s Skip s"
| exec_assign: "exec s (Assign n x) (subst n x s)"
| exec_print:  "exec s (Print x) (print x s)"
| exec_seq:    "exec s0 p s1 ⟹ exec s1 q s2 ⟹  exec s0 (Seq p q) s2"
| exec_if:     "exec s (if guard x s then p else q) s1 ⟹ exec s (If x p q) s1"
| exec_while1: "¬guard x s ⟹ exec s (While x p) s"
| exec_while2: "guard x s ⟹ exec s p s1 ⟹ exec s1 (While x p) s2
⟹ exec s (While x p) s2"

declare exec.intros[intro!]

lemma NRC_step[simp]:
"star_n step n (Skip,s) (Skip,t) ⟹ s = t"
by (induct n "(Skip, s)" "(Skip, t)" arbitrary: s t rule: star_n.induct; clarsimp)

lemma terminates_Skip:
"terminates s Skip t ⟷ s = t"
by (fastforce simp: terminates.simps star_eq_star_n)

lemma NRC_assign[simp]:
"star_n step n (Assign n' x,s) (Skip, t) ⟹ t = subst n' x s"
by (induct n "(Assign n' x,s)" "(Skip, t)" arbitrary: n' x s t rule: star_n.induct)
(fastforce dest: NRC_step)

lemma terminates_Assign:
"terminates s (Assign n x) t ⟷ t = subst n x s"
by (fastforce simp: terminates.simps star_eq_star_n)

lemma NRC_print[simp]:
"star_n step n (Print x,s) (Skip, t) ⟹ t = print x s"
by (induct n "(Print x,s)" "(Skip, t)" arbitrary: x s t rule: star_n.induct)
(fastforce dest: NRC_step)

lemma terminates_Print:
"terminates s (Print x) t ⟷ t = print x s"
by (fastforce simp: terminates.simps star_eq_star_n)

lemma terminates_If:
"terminates s (If x p q) t ⟷ terminates s (if guard x s then p else q) t"
proof -
have NRC_if1:
"star_n step n (prog.If x p q, s) (Skip, t) ⟹
∃n. star_n step n (if guard x s then p else q, s) (Skip, t)" for n
by (induct n "(If x p q,s)" "(Skip, t)" arbitrary: x p q s t rule: star_n.induct)
fastforce
have NRC_if2:
"star_n step n (if guard x s then p else q, s) (Skip, t) ⟹
∃n. star_n step n (prog.If x p q, s) (Skip, t)" for n
proof (induct n "(if guard x s then p else q, s)" "(Skip, t)"
arbitrary: x p q s t rule: star_n.induct)
case refl_n
then show ?case by (fastforce split: if_split_asm)
next
case (step_n y n)
then show ?case by (fastforce split: if_split_asm)
qed
show ?thesis
by (fastforce dest: NRC_if1 NRC_if2 simp: star_eq_star_n terminates.simps)
qed

lemma terminates_While:
"terminates s (While f c) t ⟷ terminates s (If f (Seq c (While f c)) Skip) t"
proof -
have NRC_while1:
"star_n step n (While f c, s) (Skip, t) ⟹
∃n. star_n step n (prog.If f (Seq c (While f c)) Skip, s) (Skip, t)" for n
by (induct n "(While f c,s)" "(Skip, t)" arbitrary: f c s t rule: star_n.induct)
fastforce

have NRC_while2:
"star_n step n (prog.If f (Seq c (While f c)) Skip, s) (Skip, t) ⟹
∃n. star_n step n (While f c, s) (Skip, t)" for n
by (induct n "(If f (Seq c (While f c)) Skip, s)" "(Skip, t)"
arbitrary: f c s t rule: star_n.induct)
fastforce
show ?thesis
by (fastforce dest: NRC_while1 NRC_while2 simp: star_eq_star_n terminates.simps)
qed

definition real_step where
"real_step ≡ λ(p, s) qt. p ≠ Skip ∧ step (p,s) qt"

lemma terminates:
"terminates s p t ⟷ star real_step (p,s) (Skip,t)"
proof -
have P1: "star_n step n (p, s) (Skip, t) ⟹
∃n. star_n (λ(p, s) qt. p ≠ Skip ∧ step (p, s) qt) n (p, s) (Skip, t)" for n
proof (induct n "(p, s)" "(Skip, t)" arbitrary: p s t rule: star_n.induct)
case refl_n
then show ?case by fastforce
next
case (step_n y n)
then show ?case
apply (drule_tac x="fst y" and y="snd y" in meta_spec2)
apply simp
by blast
qed
have P2: "star_n (λ(p, s) qt. p ≠ Skip ∧ step (p, s) qt) n (p, s) (Skip, t) ⟹
∃n. star_n step n (p, s) (Skip, t)" for n
by (induct n "(p, s)" "(Skip, t)" arbitrary: p s t rule: star_n.induct) fastforce+
show ?thesis
by (fastforce dest: P1 P2 simp: real_step_def star_eq_star_n terminates.simps)
qed

lemma NRC_real_step_Skip[simp]:
"star_n real_step n (Skip,s) (Skip,t) ⟷ n = 0 ∧ s = t"
apply (rule iffI; simp?)
by (induct n "(Skip, s)" "(Skip, t)" arbitrary: s t rule: star_n.induct)

lemma NRC_real_step_not_Skip:
"p ≠ Skip ⟹
(star_n real_step n (p,s) (Skip,t) ⟷
(∃k m. real_step (p,s) m ∧ star_n real_step k m (Skip,t) ∧ n = k + 1))"
apply (rule iffI; rotate_tac)
by (induct n "(p, s)" "(Skip, t)" arbitrary: p s t rule: star_n.induct, simp)
fastforce+

lemma real_step_seqE:
"real_step (Seq p q, s) x ⟹
(x = (q, s) ⟹ p = Skip ⟹ P) ⟹
(⋀p' s'. x = (Seq p' q, s') ⟹  real_step (p, s) (p', s') ⟹ p ≠ Skip ⟹ P)
⟹ P"
by (clarsimp simp: real_step_def) (erule seqE; clarsimp)

lemma real_steps_Seq:
"star_n real_step n (Seq p q,s) (Skip,t) ⟷
(∃n1 n2 m.
star_n real_step n1 (p,s) (Skip,m) ∧
star_n real_step n2 (q,m) (Skip,t) ∧ n = n1 + n2 + 1)"
proof
assume H: "star_n real_step n (Seq p q, s) (Skip, t)"
show "∃n1 n2 m.
star_n real_step n1 (p, s) (Skip, m) ∧
star_n real_step n2 (q, m) (Skip, t) ∧ n = n1 + n2 + 1" using H
proof (induct n "(Seq p q,s)" "(Skip,t)" arbitrary: p q s t rule: star_n.induct)
fix y n p q s t
assume P1: "real_step (Seq p q, s) y"
and P2: "star_n real_step n y (Skip, t)"
and IH: "⋀p q s. y = (Seq p q, s) ⟹
(∃n1 n2 r. star_n real_step n1 (p, s) (Skip, r) ∧
star_n real_step n2 (q, r) (Skip, t) ∧
n = n1 + n2 + 1)"
then show "∃n1 n2 r. star_n real_step n1 (p, s) (Skip, r) ∧
star_n real_step n2 (q, r) (Skip, t) ∧ Suc n = n1 + n2 + 1"
by (fastforce elim!: real_step_seqE)
qed
next
assume H: "∃n1 n2 m.
star_n real_step n1 (p, s) (Skip, m) ∧
star_n real_step n2 (q, m) (Skip, t) ∧ n = n1 + n2 + 1"
show "star_n real_step n (Seq p q, s) (Skip, t)"
using H
apply -
apply (case_tac "p=Skip", clarsimp)
apply (rule step_n[rotated], simp)
apply (clarsimp simp: real_step_def)
apply (elim exE conjE)
proof -
have H: "star_n real_step n1 (p, s) (Skip, m) ⟹
star_n real_step n2 (q, m) (Skip, t) ⟹
p ≠ Skip ⟹
star_n real_step (n1 + n2 + 1) (Seq p q, s) (Skip, t)" for n1 n2 m
apply (induct n1 "(p, s)" "(Skip, m)" arbitrary: s p m rule: star_n.induct)
apply (clarsimp simp: real_step_def)
apply (rename_tac y n s p m)
apply (subgoal_tac "real_step (Seq p q, s) (Seq (fst y) q, snd y)")
prefer 2
apply (clarsimp simp: real_step_def)
apply (case_tac "fst y = Skip")
apply (subgoal_tac "⋀a b. fst a = b ⟹ (∃c. a = (b, c) ∧ c = snd a)")
prefer 2
apply clarsimp
apply (drule_tac x="y" and y="Skip" in meta_spec2)
apply (drule (1) meta_mp)
apply (elim exE conjE)
apply (rename_tac c)
apply (thin_tac "c = snd y")
apply simp
apply (erule step_n)
apply (rule step_n[rotated])
apply simp
apply (clarsimp simp: real_step_def)
apply clarsimp
done
thus "⋀n1 n2 m.
p ≠ Skip ⟹
star_n real_step n1 (p, s) (Skip, m) ⟹
star_n real_step n2 (q, m) (Skip, t) ⟹
n = n1 + n2 + 1 ⟹
star_n real_step n (Seq p q, s) (Skip, t)" by blast
qed
qed

lemma terminates_Seq:
"terminates s (Seq p q) t ⟷ (∃m. terminates s p m ∧ terminates m q t)"
by (fastforce simp: terminates star_eq_star_n real_steps_Seq)

lemma terminates_eq_exec:
"terminates s p t ⟷ exec s p t"
proof -
have P1: "star_n real_step n (p, s) (Skip, t) ⟹ exec s p t" for n
proof (induct n arbitrary: p s t rule: nat_less_induct)
case (1 n)
then show ?case
apply -
apply (case_tac p; clarsimp)
apply (erule star_n.cases;
clarsimp simp: real_step_def NRC_real_step_Skip[simplified real_step_def])
apply (drule sym[where s="subst _ _ _"], clarsimp)
apply (erule star_n.cases;
clarsimp simp: real_step_def NRC_real_step_Skip[simplified real_step_def])
apply (drule sym[where s="print _ _"], clarsimp)
apply (clarsimp simp: real_steps_Seq)
apply (erule star_n.cases;
clarsimp simp: real_step_def NRC_real_step_Skip[simplified real_step_def]
split: if_split_asm)
apply fastforce
apply fastforce
apply (erule star_n.cases; clarsimp simp: real_step_def)
apply (erule whileE, clarsimp)
apply (erule star_n.cases;
clarsimp split: if_split_asm simp: NRC_real_step_Skip[simplified real_step_def])
defer
apply fastforce
apply (clarsimp simp: real_steps_Seq[simplified real_step_def])
qed
then have P1': "terminates s p t ⟹ exec s p t"
by (clarsimp simp: terminates star_eq_star_n)
have P2: "exec s p t ⟹ terminates s p t"
proof (induct s p t rule: exec.induct; clarsimp)
case (exec_skip s)
then show ?case by (clarsimp simp: terminates_Skip)
next
case (exec_assign s n x)
then show ?case by (clarsimp simp: terminates_Assign)
next
case (exec_print s x)
then show ?case by (clarsimp simp: terminates_Print)
next
case (exec_seq s0 p s1 q s2)
then show ?case by (cases s1; fastforce simp: terminates_Seq)
next
case (exec_if s x p q s1)
then show ?case by (cases s1; fastforce simp: terminates_If)
next
case (exec_while1 x s p)
then show ?case by (clarsimp simp: terminates_While terminates_If terminates_Skip)
next
case (exec_while2 x s p s1 s2)
then show ?case
apply (simp (no_asm) add: terminates_While terminates_If terminates_Skip)
by (cases s1; fastforce simp: terminates_Seq)
qed
show ?thesis using P1' P2 by auto
qed

lemma terminates_While_NRC:
assumes "terminates m p t"
assumes "p = While f c"
shows "∃n. star_n (λs t. guard f s ∧ terminates s c t) n m t ∧ ¬guard f t"
using assms
by (induct m "While f c" t arbitrary: f c rule: exec.induct; clarsimp; fastforce)

lemma not_diverges[simp]:
"~diverges s Skip l"
"~diverges s (Assign n x) l"
"~diverges s (Print x) l"
by (clarsimp simp: diverges.simps terminates_Skip terminates_Assign terminates_Print;
metis surj_pair)+

lemma star_n_Skip:
"star_n step n (Skip, s) (c', t) ⟹ c' = Skip ∧ t = s"
apply (induct n)
apply (erule star_n.cases; clarsimp)+
done

lemma star_n_Seq:
"star_n step n (c, s) (c', t) ⟹
∃n. star_n step n (Seq c p, s) (Seq c' p, t) "
apply (case_tac "c=Skip")
apply (fastforce dest!: star_n_Skip)
apply (induct n arbitrary: c s)
apply (erule star_n.cases; simp; rename_tac x; case_tac x; rule_tac x=0 in exI, clarsimp)
apply (erule star_n.cases, simp)
apply (rename_tac y na z)
apply (drule_tac x="fst y" and y="snd y" in meta_spec2)
apply clarsimp
apply (rename_tac ac ad bb na af bc)
apply (case_tac "ac=Skip", simp)
apply (fastforce dest!: star_n_Skip)
apply clarsimp
apply fastforce
done

lemma RTC_Seq:
"star step (c,s) (c',t) ⟹
star step (Seq c p, s) (Seq c' p,t)"
apply (clarsimp simp: star_eq_star_n star_n_Seq)
done

lemma step_output_mono:
"step s t ⟹ prefix (output_of (snd s)) (output_of (snd t))"
by (induct rule: step.induct; simp add: subst_def print_def split_def output_of_def)

lemma NRC_step_output_mono:
"star_n step k (c,s) (c',s') ⟹ prefix (output_of s) (output_of s')"
apply (induct k arbitrary: c s c' s')
apply (erule star_n.cases; clarsimp)
apply (erule star_n.cases; clarsimp)
apply (drule step_output_mono)
apply fastforce
done

lemma lprefix_chain_RTC_step':
"Complete_Partial_Order.chain lprefix {llist_of out | out. (∃q t. step x (q,t,out))}"
apply (rule chainI)
apply simp
apply (elim exE impE conjE)
by (metis lprefix_down_linear lprefix_llist_ofI prod.inject step_deterministic)

lemma star_n_step_decompose:
"star_n step n x y ⟹ star_n step n' x z ⟹ n' < n
⟹ star_n step (n - n') z y"
by (fastforce elim!: star_n_decompose step_deterministic NRC_step_deterministic)

lemma lprefix_chain_NRC_step':
"star_n step n x (q, t, out) ⟹
star_n step n' x (q', t', out') ⟹
lprefix (llist_of out) (llist_of out') ∨ lprefix (llist_of out') (llist_of out)"
apply (insert less_linear[of n n'])
apply (elim disjE)
defer 2
apply (drule (2) star_n_step_decompose,
metis NRC_step_output_mono internal_case_prod_conv internal_case_prod_def
lprefix_llist_of output_of_def)+
apply simp
apply (drule (1) NRC_step_deterministic)
by fastforce

lemma lprefix_chain_NRC_step:
"Complete_Partial_Order.chain lprefix {llist_of out | out. (∃q t. star_n step n x (q,t,out))}"
by (rule chainI) (force dest: lprefix_chain_NRC_step')

lemma lprefix_chain_RTC_step:
"Complete_Partial_Order.chain lprefix {llist_of out | out. (∃q t. star step x (q,t,out))}"
by (rule chainI) (force dest: lprefix_chain_NRC_step' star_star_n)

lemma lprefix_chain_NRC_step_ex:
"Complete_Partial_Order.chain lprefix {llist_of out | out. (∃q t n. star_n step n x (q,t,out))}"
by (subst star_eq_star_n[symmetric]) (rule lprefix_chain_RTC_step)

definition lprefix_rel where
"lprefix_rel ls ls' ≡ ∀l ∈ ls. ∃l' ∈ ls'. lprefix l l'"

lemma diverges_unique:
"diverges s p l ⟹ ∀l'. diverges s p l' ⟶ l' = l"
using diverges_deterministic by blast

lemma terminates_unique:
"terminates s p t ⟹ ∀t'. terminates s p t' ⟶ t' = t"
using terminates_deterministic by blast

(* diverges lemmas *)

lemma star_n_real_step_Seq_exact:
"star_n real_step n (c, s) (Skip, t) ⟹ star_n step n (Seq c c', s) (Seq Skip c', t)"
by (induct "(c, s)" "(Skip, t)" arbitrary: c s t rule: star_n.induct) (auto simp: real_step_def)

lemma star_n_real_step_Seq_exact':
"star_n real_step n (c, s) (Skip, t) ⟹ star_n real_step n (Seq c c', s) (Seq Skip c', t)"
by (induct "(c, s)" "(Skip, t)" arbitrary: c s t rule: star_n.induct) (auto simp: real_step_def)

lemma div_Seq1_always_Seq:
"⟦ star_n step n (Seq c c', s) (q, s'); c ≠ Skip;
∀a b n. ¬ star_n step n (c, s) (Skip, a, b)⟧
⟹ ∃u. q = Seq u c' ∧ u ≠ Skip"
proof (induct "(Seq c c', s)" "(q, s')" arbitrary: c c' q s s' rule: star_n.induct)
case (step_n y n)
then show ?case
by cases fastforce+
qed clarsimp

lemma div_Seq1_steps:
"⟦star_n step n (Seq c c', s) (Seq u c', s'); c ≠ Skip;
∀a b n. ¬ star_n step n (c, s) (Skip, a, b)⟧
⟹ star_n step n (c, s) (u, s')"
proof (induct "(Seq c c', s)" "(Seq u c', s')" arbitrary: c c' u s s' rule: star_n.induct)
case (step_n y n)
then show ?case by cases fastforce+
qed fastforce

lemma div_Seq1_lSup_eq:
"∀t. ¬ terminates s c t
⟹ lSup {llist_of out |out. ∃q t. star step (c, s) (q, t, out)} =
lSup {llist_of out |out. ∃q t. star step (Seq c c', s) (q, t, out)}"
apply (rule lprefix_antisym)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply (clarsimp simp: terminates star_eq_star_n)
apply (drule star_n_Seq)
apply fastforce
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply clarsimp
apply (clarsimp simp: terminates.simps star_eq_star_n)
apply (frule div_Seq1_always_Seq)
apply (metis (no_types, opaque_lifting) star_n.simps surj_pair)
apply simp
apply (erule star_n.cases, fastforce)
by (metis (mono_tags, opaque_lifting) div_Seq1_steps prod.collapse refl_n step_n)

lemma star_n_real_step_step:
"star_n real_step n x y ⟹ star_n step n x y"
by (induct rule: star_n.induct; clarsimp)
(metis (no_types, lifting) prod.simps(2) real_step_def star_n.simps)

lemma div_Seq2_steps:
"⟦ star_n real_step n' (c, s) (Skip, s'); n' < n;
∀t' n. ¬ star_n real_step n (c', s') (Skip, t');
star_n step n (Seq c c', s) (q, t, out)⟧
⟹ ∃m q t'. star_n step m (c', s') (q, t', out)"
apply (drule star_n_real_step_Seq_exact[where c'=c'])
apply (drule (2) star_n_step_decompose)
apply (erule_tac ?a1.0="n - n'" in star_n.cases)
apply clarsimp
apply clarsimp
apply (erule step.cases; clarsimp)
apply fastforce
done

lemma div_Seq2_lSub_eq:
"⟦terminates s c s'; ∀t. ¬ terminates s' c' t⟧
⟹ lSup {llist_of out |out. ∃q t. star step (Seq c c', s) (q, t, out)} =
lSup {llist_of out |out. ∃q t. star step (c', s') (q, t, out)}"
apply (rule lprefix_antisym)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply clarsimp
apply (clarsimp simp: terminates star_eq_star_n)
apply (rename_tac n na)
apply (cases s; cases s'; simp)
apply (case_tac "n < na")
apply (rule chain_lprefix_lSup[OF lprefix_chain_NRC_step_ex])
apply (drule (1) div_Seq2_steps; fastforce)
apply (clarsimp simp: not_less)
apply (drule star_n_real_step_Seq_exact[where c'=c'])
apply (rename_tac aa ba)
apply (subgoal_tac "lprefix (llist_of ba)
(lSup {llist_of out |out. ∃q t n. star_n step n (c', aa, ba) (q, t, out)})")
prefer 2
apply (rule chain_lprefix_lSup[OF lprefix_chain_NRC_step_ex])
apply fastforce
apply (case_tac "n=na"; simp?)
apply (drule (1) NRC_step_deterministic)
apply clarsimp
apply (drule le_neq_trans, clarsimp, simp)
apply (frule_tac n=n and n'=na in star_n_step_decompose; simp?)
apply (drule_tac k="n-na" in NRC_step_output_mono)
apply (clarsimp simp: output_of_def)
apply (meson lprefix_llist_of lprefix_trans)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply (clarsimp simp: terminates star_eq_star_n)
apply (drule star_n_real_step_Seq_exact[where c'=c'])
apply (subgoal_tac "step (Seq Skip c', s') (c', s')")
apply (drule (1) step_n_rev)
apply (clarsimp dest!: star_n_star simp: star_eq_star_n[symmetric])
apply (drule (1) star_trans)
apply fastforce
apply clarsimp
done

lemma diverges_Seq:
"diverges s (Seq c c') l ⟷ diverges s c l ∨ (∃t. terminates s c t ∧ diverges t c' l)"
apply (rule iffI)
apply (case_tac "∃t. terminates s c t"; simp)
prefer 2
apply (erule diverges.cases)
apply (rule diverges.intros)
apply (clarsimp simp: terminates.simps star_eq_star_n)
apply (metis (no_types, opaque_lifting) div_Seq1_steps div_Seq1_always_Seq refl_n star_n_Seq)
apply (rule disjI2, clarsimp)
apply (rename_tac a b)
apply (rule_tac x=a in exI, rule_tac x=b in exI, clarsimp)
apply (clarsimp simp: diverges.simps terminates_Seq)
apply (drule_tac x=a and y=b in spec2)
apply clarsimp
apply (drule div_Seq2_lSub_eq; fastforce)
apply (erule disjE)
apply (rule diverges.intros, clarsimp)
apply (rule conjI; clarsimp?)
apply (erule diverges.cases, clarsimp)
apply (fastforce simp: div_Seq1_lSup_eq diverges.simps)
apply clarsimp
apply (erule diverges.cases, clarsimp)
apply (rule diverges.intros, clarsimp)
apply (rule conjI; clarsimp?)
using terminates_Seq terminates_deterministic apply blast
apply (drule div_Seq2_lSub_eq)
by simp+

lemma div_true_If_lSup_eq:
"⟦∀t. ¬ terminates s p t; guard f s⟧
⟹ lSup {llist_of out |out. ∃qa t. star step (prog.If f p q, s) (qa, t, out)} =
lSup {llist_of out |out. ∃q t. star step (p, s) (q, t, out)}"
apply (rule lprefix_antisym)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply clarsimp
apply (erule star.cases; fastforce)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply clarsimp
apply (subgoal_tac "step (If f p q, s) (if guard f s then p else q, s)")
apply simp
apply (drule (1) step[where r=step])
apply fastforce
apply (rule step_if)
done

lemma div_false_If_lSup_Eq:
"⟦∀t. ¬ terminates s q t; ¬ guard f s⟧
⟹ lSup
{llist_of out |out. ∃qa t. star step (prog.If f p q, s) (qa, t, out)} =
lSup {llist_of out |out. ∃q' t. star step (q, s) (q', t, out)}"
apply (rule lprefix_antisym)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply clarsimp
apply (erule star.cases; fastforce)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply clarsimp
apply (subgoal_tac "step (If f p q, s) (if guard f s then p else q, s)")
apply simp
apply (drule (1) step[where r=step])
apply fastforce
apply (rule step_if)
done

lemma diverges_If:
"diverges s (If f p q) l = diverges s (if guard f s then p else q) l"
by (fastforce simp: diverges.simps terminates_If
div_true_If_lSup_eq div_false_If_lSup_Eq)

"⟦star_n real_step n (c, s) (Skip, s'); guard g s⟧
⟹ star_n real_step (n + 3) (While g c, s) (While g c, s')"
apply (drule star_n_real_step_Seq_exact'[where c'="While g c"])
apply (subgoal_tac "real_step (Seq Skip (While g c), s') (While g c, s')")
apply (drule (1) step_n_rev)
apply (thin_tac "real_step _ _")
apply (subgoal_tac "real_step (If g (Seq c (While g c)) Skip, s)
(if guard g s then Seq c (While g c) else Skip, s)")
apply (simp only: if_True)
apply (drule (1) step_n[rotated])
apply (thin_tac "real_step _ _")
apply (subgoal_tac "real_step (While g c, s) (If g (Seq c (While g c)) Skip, s)")
apply (drule (1) step_n[rotated])
apply (thin_tac "real_step _ _")
apply (fastforce simp: real_step_def)+
apply (fastforce simp: real_step_def)
done

lemma div_body_While_lSup_eq:
"⟦guard g s; ∀t. ¬ terminates s c t⟧
⟹ lSup {llist_of out |out. ∃q t. star step (c, s) (q, t, out)} =
lSup {llist_of out |out. ∃q t. star step (While g c, s) (q, t, out)}"
apply (rule lprefix_antisym)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply clarsimp
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply (clarsimp simp:  star_eq_star_n)
apply (subgoal_tac "step (If g (Seq c (While g c)) Skip, s)
(if guard g s then (Seq c (While g c)) else Skip, s)")
prefer 2
apply (rule step_if)
apply simp
apply (subgoal_tac "step (While g c, s) (If g (Seq c (While g c)) Skip, s)")
prefer 2
apply (rule step_while)
apply (drule star_n_Seq[where p="While g c"])
apply (elim exE)
apply fastforce
apply (frule div_Seq1_lSup_eq[where c'="While g c"])
apply (frule div_true_If_lSup_eq[where p="Seq c (While g c)" and q=Skip, rotated, THEN sym])
apply (clarsimp simp: terminates_Seq)
apply simp
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply (clarsimp simp: star_eq_star_n)
apply (erule star_n.cases)
apply fastforce
apply clarsimp
apply (erule step.cases; simp)
apply clarsimp
apply fastforce
done

lemma inf_loop_While_steps:
"⟦ star_n real_step n' (c, s) (Skip, s'); n' + 3 < n; guard g s;
star_n step n (While g c, s) (q, t, out)⟧
⟹ ∃q' t' n. star_n step n (While g c, s') (q', t', out)"

lemma inf_loop_While_lSup_eq:
"⟦guard g s; terminates s c (a, b); ∀aa ba. ¬ terminates (a, b) (While g c) (aa, ba)⟧
⟹ lSup {llist_of out |out. ∃q t. star step (While g c, a, b) (q, t, out)} =
lSup {llist_of out |out. ∃q t. star step (While g c, s) (q, t, out)}"
apply (rule lprefix_antisym)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply (rule chain_lprefix_lSup[OF lprefix_chain_RTC_step])
apply clarsimp
apply (clarsimp simp: terminates star_eq_star_n)
apply (drule (1) star_n_trans, fastforce)
apply (rule chain_lSup_lprefix[OF lprefix_chain_RTC_step])
apply clarsimp
apply (clarsimp simp: terminates star_eq_star_n)
apply (rename_tac n na)
apply (case_tac "n + 3 < na")
apply (rule chain_lprefix_lSup[OF lprefix_chain_NRC_step_ex])
apply (fastforce dest!: inf_loop_While_steps)
apply (clarsimp simp: not_less)
apply (rule lprefix_trans[of _ "llist_of b"])
apply clarsimp
apply (case_tac "na = n + 3"; simp?)
apply (drule (1) NRC_step_deterministic)
apply clarsimp
apply (drule le_neq_trans, clarsimp, simp)
apply (frule_tac n="n+3" and n'=na in star_n_step_decompose; simp?)
apply (drule_tac k="n+3-na" in NRC_step_output_mono)
apply (clarsimp simp: output_of_def)
apply (rule chain_lprefix_lSup[OF lprefix_chain_NRC_step_ex])
apply fastforce
done

lemma diverges_While:
"diverges s (While g c) l ⟷ diverges s (If g (Seq c (While g c)) Skip) l"
apply (rule iffI; clarsimp simp: diverges_If diverges_Seq)
defer
apply (case_tac "guard g s"; simp)
apply (clarsimp simp: diverges_Seq)
apply (erule disjE; clarsimp?)
apply (clarsimp simp: diverges.simps terminates_While terminates_If terminates_Seq)
apply (fastforce simp: div_body_While_lSup_eq)
apply (simp (no_asm) add: diverges.simps terminates_While terminates_If)
apply clarsimp
apply (simp only: terminates_Seq del: )
apply (rule conjI)
apply (clarsimp, drule (1) terminates_deterministic, clarsimp simp: diverges.simps)
apply (clarsimp simp: diverges.simps)
apply (fastforce simp: inf_loop_While_lSup_eq)
apply (case_tac "guard g s"; simp)
apply (subgoal_tac "diverges s (While g c) l ⟹ guard g s
⟹ (∀a b. ¬ terminates s (Seq c (While g c)) (a, b))")
prefer 2
apply (clarsimp simp: diverges.simps terminates_While terminates_If)
apply (clarsimp simp: terminates_Seq diverges.simps)
apply (rule context_conjI)
prefer 2
apply (fastforce simp: div_body_While_lSup_eq)
apply clarsimp
apply (rename_tac a b)
apply (drule_tac x=a and y=b in spec2)
apply clarsimp
apply (rotate_tac 2)
apply (drule_tac x=a and y=b in spec2)
apply clarsimp
apply (erule notE)
apply (fastforce simp: inf_loop_While_lSup_eq)
apply (clarsimp simp: diverges.simps terminates_While terminates_If)
apply (clarsimp simp: terminates.simps)
by (metis star.refl surj_pair)

lemma NRC_terminates:
assumes "star_n (λx y. terminates x c y) i s t"
shows "∀t1. star_n (λx y. terminates x c y) i s t1 ⟷ (t = t1)"
proof -
have "⋀a b. star_n (λx. terminates x c) i s (a, b) ⟹ t = (a, b)" using assms
proof(induct i arbitrary: s t)
case 0
show ?case using 0
by cases (erule star_n.cases; simp)
next
case (Suc i)
show ?case using Suc.prems
apply cases
apply(erule star_n.cases; simp)
by(blast dest: terminates_deterministic Suc.hyps)
qed
thus ?thesis using assms by fastforce
qed

lemma step_output_append:
"step (c, a, b) (c', a', b') ⟹ ∃new. b' = b @ new"
by (induct c arbitrary: c' a a' b; fastforce simp: subst_def print_def dest!: seqE whileE)

lemma step_output_extend':
"step (c, a, b) (c', a', b @ new) ⟹ ∀xs. step (c, a, xs) (c', a', xs @ new)"
apply (induct c arbitrary: c' a a' b)
apply clarsimp
apply clarsimp
apply (rename_tac x1 x2 a a' b xs)
apply (cases new; simp)
apply (subgoal_tac "(a', xs) = subst x1 x2 (a, xs)")
apply clarsimp
apply (clarsimp simp: subst_def)
apply (clarsimp simp: subst_def)
apply clarsimp
apply (rename_tac x a a' b xs)
apply (subgoal_tac "(a', xs @ new) = print x (a, xs)")
apply clarsimp
apply (clarsimp simp: print_def)
apply (erule seqE)
apply fastforce
apply fastforce
apply (erule ifE)
apply (erule Pair_inject)
apply (erule Pair_inject)
apply (simp only: append_self_conv append.right_neutral)
apply (rule allI)
apply (rename_tac x1 c1 c2 c' a a' b xs)
apply (subgoal_tac "guard x1 (a, b) = guard x1 (a, xs)")
prefer 2
apply force
apply (erule whileE)
apply (erule Pair_inject)
apply (erule Pair_inject)
apply (simp only: append_self_conv append.right_neutral)
apply (rule allI)
apply (rename_tac x1 c c' a a' b xs)
apply (subgoal_tac "guard x1 (a, b) = guard x1 (a, xs)")
prefer 2
apply force
done

lemma step_output_extend:
"step (c, a, b) (c', a', b') ⟹ ∃new. b' = b @ new ∧ (∀xs. step (c, a, xs) (c', a', xs @ new))"
by (metis step_output_append step_output_extend')

lemma star_n_real_step_output_extend:
"star_n real_step n (c, s) (Skip, t) ⟹
∃new. snd t = snd s @ new ∧
(∀xs. ∃n. star_n real_step n (c, fst s, xs)
(Skip, fst t, xs @ new)) "
apply (induct n arbitrary: c s t)
apply (erule star_n.cases; fastforce)
apply clarsimp
apply (erule star_n.cases; simp)
apply clarsimp
apply (rename_tac c a b c' a0 b0 n a' b')
apply (drule_tac x=c' in meta_spec)
apply (drule_tac x=a0 and y=b0 in meta_spec2)
apply (drule_tac x=a' and y=b' in meta_spec2)
apply clarsimp
apply (subgoal_tac "c ≠ Skip ∧ step (c, a, b) (c', a0, b0)")
prefer 2
apply (clarsimp simp: real_step_def)
apply clarsimp
apply (drule step_output_extend)
apply clarsimp
apply (rotate_tac -1)
apply (rename_tac new newa xs)
apply (drule_tac x=xs in spec)
apply (drule_tac x="xs@newa" in spec)
apply clarsimp
apply (thin_tac "real_step _ _")
apply (subgoal_tac "real_step (c, a, xs) (c', a0, xs @ newa)")
prefer 2
apply (clarsimp simp: real_step_def)
apply (rename_tac na)
apply (rule_tac x="Suc na" in exI)
apply fastforce
done

lemma terminates_history:
"terminates s c t ⟹
∃new. snd t = snd s @ new ∧
(∀xs. terminates (fst s,xs) c (fst t,xs @ new))"
apply (clarsimp simp: terminates star_eq_star_n)
using star_n_real_step_output_extend by auto

lemma terminates_ignores_history:
"terminates (s, out1) c (t, out2) ⟹
terminates (s, []) c (t, drop (length out1) out2)"
by (metis append.simps(1) append_eq_conv_conj prod.sel(1) prod.sel(2) terminates_history)

end```