Theory Resumption

(*  Author:      Andreas Lochbihler
Maintainer:  Andreas Lochbihler
*)
section ‹Manual construction of a resumption codatatype›

theory Resumption imports
"HOL-Library.Old_Datatype"
begin

text ‹
This theory defines the following codatatype:

\begin{verbatim}
codatatype ('a,'b,'c,'d) resumption =
Terminal 'a
| Linear 'b "('a,'b,'c,'d) resumption"
| Branch 'c "'d => ('a,'b,'c,'d) resumption"
\end{verbatim}

›

subsection ‹Auxiliary definitions and lemmata similar to @{theory "HOL-Library.Old_Datatype"}›

lemma Lim_mono: "(⋀d. rs d ⊆ rs' d) ⟹ Old_Datatype.Lim rs ⊆ Old_Datatype.Lim rs'"

lemma Lim_UN1:  "Old_Datatype.Lim (λx. ⋃y. f x y) = (⋃y. Old_Datatype.Lim (λx. f x y))"

text ‹
Inverse for @{term "Old_Datatype.Lim"} like @{term "Old_Datatype.Split"} and @{term "Old_Datatype.Case"}
for @{term "Old_Datatype.Scons"} and @{term "In0"}/@{term "In1"}
›

definition DTBranch :: "(('b ⇒ ('a, 'b) Old_Datatype.dtree) ⇒ 'c) ⇒ ('a, 'b) Old_Datatype.dtree ⇒ 'c"
where "DTBranch f M = (THE u. ∃x. M = Old_Datatype.Lim x ∧ u = f x)"

lemma DTBranch_Lim [simp]: "DTBranch f (Old_Datatype.Lim M) = f M"
by(auto simp add: DTBranch_def dest: Lim_inject)

text ‹Lemmas for @{term Old_Datatype.ntrunc} and @{term "Old_Datatype.Lim"}›

lemma ndepth_Push_Node_Inl_aux:
"case_nat (Inl n) f k = Inr 0 ⟹ Suc (LEAST x. f x = Inr 0) <= k"
apply (induct "k", auto)
apply (erule Least_le)
done

lemma ndepth_Push_Node_Inl:
"ndepth (Push_Node (Inl a) n) = Suc (ndepth n)"
using Rep_Node[of n, unfolded Node_def]
apply(simp add: ndepth_def Push_Node_def Abs_Node_inverse[OF Node_Push_I[OF Rep_Node]])
apply(rule Least_equality)
apply(auto elim: LeastI intro: ndepth_Push_Node_Inl_aux)
done

lemma ntrunc_Lim [simp]: "ntrunc (Suc k) (Old_Datatype.Lim rs) = Old_Datatype.Lim (λx. ntrunc k (rs x))"
unfolding Lim_def ntrunc_def
apply(rule equalityI)
apply clarify
done

subsection ‹Definition for the codatatype universe›

text ‹Constructors›

definition TERMINAL :: "'a ⇒ ('c + 'b + 'a, 'd) Old_Datatype.dtree"
where "TERMINAL a = In0 (Old_Datatype.Leaf (Inr (Inr a)))"

definition LINEAR :: "'b ⇒ ('c + 'b + 'a, 'd) Old_Datatype.dtree ⇒ ('c + 'b + 'a, 'd) Old_Datatype.dtree"
where "LINEAR b r = In1 (In0 (Scons (Old_Datatype.Leaf (Inr (Inl b))) r))"

definition BRANCH :: "'c ⇒ ('d ⇒ ('c + 'b + 'a, 'd) Old_Datatype.dtree) ⇒ ('c + 'b + 'a, 'd) Old_Datatype.dtree"
where "BRANCH c rs = In1 (In1 (Scons (Old_Datatype.Leaf (Inl c)) (Old_Datatype.Lim rs)))"

text ‹case operator›

definition case_RESUMPTION :: "('a ⇒ 'e) ⇒ ('b ⇒ (('c + 'b + 'a, 'd) Old_Datatype.dtree) ⇒ 'e) ⇒ ('c ⇒ ('d ⇒ ('c + 'b + 'a, 'd) Old_Datatype.dtree) ⇒ 'e) ⇒ ('c + 'b + 'a, 'd) Old_Datatype.dtree ⇒ 'e"
where
"case_RESUMPTION t l br =
Old_Datatype.Case (t o inv (Old_Datatype.Leaf o Inr o Inr))
(Old_Datatype.Case (Old_Datatype.Split (λx. l (inv (Old_Datatype.Leaf o Inr o Inl) x)))
(Old_Datatype.Split (λx. DTBranch (br (inv (Old_Datatype.Leaf o Inl) x)))))"

lemma [iff]:
shows TERMINAL_not_LINEAR: "TERMINAL a ≠ LINEAR b r"
and LINEAR_not_TERMINAL: "LINEAR b R ≠ TERMINAL a"
and TERMINAL_not_BRANCH: "TERMINAL a ≠ BRANCH c rs"
and BRANCH_not_TERMINAL: "BRANCH c rs ≠ TERMINAL a"
and LINEAR_not_BRANCH: "LINEAR b r ≠ BRANCH c rs"
and BRANCH_not_LINEAR: "BRANCH c rs ≠ LINEAR b r"
and TERMINAL_inject: "TERMINAL a = TERMINAL a' ⟷ a = a'"
and LINEAR_inject: "LINEAR b r = LINEAR b' r' ⟷ b = b' ∧ r = r'"
and BRANCH_inject: "BRANCH c rs = BRANCH c' rs' ⟷ c = c' ∧ rs = rs'"
by(auto simp add: TERMINAL_def LINEAR_def BRANCH_def dest: Lim_inject)

lemma case_RESUMPTION_simps [simp]:
shows case_RESUMPTION_TERMINAL: "case_RESUMPTION t l br (TERMINAL a) = t a"
and case_RESUMPTION_LINEAR: "case_RESUMPTION t l br (LINEAR b r) = l b r"
and case_RESUMPTION_BRANCH: "case_RESUMPTION t l br (BRANCH c rs) = br c rs"
apply(simp_all add: case_RESUMPTION_def TERMINAL_def LINEAR_def BRANCH_def o_def)
apply(rule arg_cong) back
apply(blast intro: injI inv_f_f)
apply(rule arg_cong) back
apply(blast intro: injI inv_f_f)
apply(rule arg_cong) back
apply(blast intro: injI inv_f_f)
done

lemma LINEAR_mono: "r ⊆ r' ⟹ LINEAR b r ⊆ LINEAR b r'"
by(simp add: LINEAR_def In1_mono In0_mono Scons_mono)

lemma BRANCH_mono: "(⋀d. rs d ⊆ rs' d) ⟹ BRANCH c rs ⊆ BRANCH c rs'"
by(simp add: BRANCH_def In1_mono Scons_mono Lim_mono)

lemma LINEAR_UN: "LINEAR b (⋃x. f x) = (⋃x. LINEAR b (f x))"
by (simp add: LINEAR_def In1_UN1 In0_UN1 Scons_UN1_y)

lemma BRANCH_UN: "BRANCH b (λd. ⋃x. f d x) = (⋃x. BRANCH b (λd. f d x))"
by (simp add: BRANCH_def Lim_UN1 In1_UN1 In0_UN1 Scons_UN1_y)

text ‹The codatatype universe›

coinductive_set resumption :: "('c + 'b + 'a, 'd) Old_Datatype.dtree set"
where
resumption_TERMINAL:
"TERMINAL a ∈ resumption"
| resumption_LINEAR:
"r ∈ resumption ⟹ LINEAR b r ∈ resumption"
| resumption_BRANCH:
"(⋀d. rs d ∈ resumption) ⟹ BRANCH c rs ∈ resumption"

subsection ‹Definition of the codatatype as a type›

typedef ('a,'b,'c,'d) resumption = "resumption :: ('c + 'b + 'a, 'd) Old_Datatype.dtree set"
proof
show "TERMINAL undefined ∈ ?resumption" by(blast intro: resumption.intros)
qed

text ‹Constructors›

definition Terminal :: "'a ⇒ ('a,'b,'c,'d) resumption"
where "Terminal a = Abs_resumption (TERMINAL a)"

definition Linear :: "'b ⇒ ('a,'b,'c,'d) resumption ⇒ ('a,'b,'c,'d) resumption"
where "Linear b r = Abs_resumption (LINEAR b (Rep_resumption r))"

definition Branch :: "'c ⇒ ('d ⇒ ('a,'b,'c,'d) resumption) ⇒ ('a,'b,'c,'d) resumption"
where "Branch c rs = Abs_resumption (BRANCH c (λd. Rep_resumption (rs d)))"

lemma [iff]:
shows Terminal_not_Linear: "Terminal a ≠ Linear b r"
and Linear_not_Terminal: "Linear b R ≠ Terminal a"
and Termina_not_Branch: "Terminal a ≠ Branch c rs"
and Branch_not_Terminal: "Branch c rs ≠ Terminal a"
and Linear_not_Branch: "Linear b r ≠ Branch c rs"
and Branch_not_Linear: "Branch c rs ≠ Linear b r"
and Terminal_inject: "Terminal a = Terminal a' ⟷ a = a'"
and Linear_inject: "Linear b r = Linear b' r' ⟷ b = b' ∧ r = r'"
and Branch_inject: "Branch c rs = Branch c' rs' ⟷ c = c' ∧ rs = rs'"
apply(auto simp add: Terminal_def Linear_def Branch_def simp add: Rep_resumption resumption.intros Abs_resumption_inject Rep_resumption_inject)
apply(subst (asm) fun_eq_iff, auto simp add: Rep_resumption_inject)
done

lemma Rep_resumption_constructors:
shows Rep_resumption_Terminal: "Rep_resumption (Terminal a) = TERMINAL a"
and Rep_resumption_Linear: "Rep_resumption (Linear b r) = LINEAR b (Rep_resumption r)"
and Rep_resumption_Branch: "Rep_resumption (Branch c rs) = BRANCH c (λd. Rep_resumption (rs d))"
by(simp_all add: Terminal_def Linear_def Branch_def Abs_resumption_inverse resumption.intros Rep_resumption)

text ‹Case operator›

definition case_resumption :: "('a ⇒ 'e) ⇒ ('b ⇒ ('a,'b,'c,'d) resumption ⇒ 'e) ⇒
('c ⇒ ('d ⇒ ('a,'b,'c,'d) resumption) ⇒ 'e) ⇒ ('a,'b,'c,'d) resumption ⇒ 'e"
where [code del]:
"case_resumption t l br r =
case_RESUMPTION t (λb r. l b (Abs_resumption r)) (λc rs. br c (λd. Abs_resumption (rs d))) (Rep_resumption r)"

lemma case_resumption_simps [simp, code]:
shows case_resumption_Terminal: "case_resumption t l br (Terminal a) = t a"
and case_resumption_Linear: "case_resumption t l br (Linear b r) = l b r"
and case_resumption_Branch: "case_resumption t l br (Branch c rs) = br c rs"
by(simp_all add: Terminal_def Linear_def Branch_def case_resumption_def Abs_resumption_inverse resumption.intros Rep_resumption Rep_resumption_inverse)

declare [[case_translation case_resumption Terminal Linear Branch]]

lemma case_resumption_cert:
assumes "CASE ≡ case_resumption t l br"
shows "(CASE (Terminal a) ≡ t a) &&& (CASE (Linear b r) ≡ l b r) &&& (CASE (Branch c rs) ≡ br c rs)"
using assms by simp_all

code_datatype Terminal Linear Branch

setup ‹Code.declare_case_global @{thm case_resumption_cert}›

setup ‹
Nitpick.register_codatatype @{typ "('a,'b,'c,'d) resumption"} @{const_name case_resumption}
(map dest_Const [@{term Terminal}, @{term Linear}, @{term Branch}])
›

lemma resumption_exhaust [cases type: resumption]:
obtains (Terminal) a where "x = Terminal a"
| (Linear) b r where "x = Linear b r"
| (Branch) c rs where "x = Branch c rs"
proof(cases x)
case (Abs_resumption y)
note [simp] = ‹x = Abs_resumption y›
from ‹y ∈ resumption› show thesis
proof(cases rule: resumption.cases)
case resumption_TERMINAL thus ?thesis
by -(rule Terminal, simp add: Terminal_def)
next
case (resumption_LINEAR r b)
from ‹r ∈ resumption› have "Rep_resumption (Abs_resumption r) = r"
hence "y = LINEAR b (Rep_resumption (Abs_resumption r))"
using ‹y = LINEAR b r› by simp
thus ?thesis by -(rule Linear, simp add: Linear_def)
next
case (resumption_BRANCH rs c)
from ‹⋀d. rs d ∈ resumption›
have eq: "rs = (λd. Rep_resumption (Abs_resumption (rs d)))"
by(subst Abs_resumption_inverse) blast+
show ?thesis using ‹y = BRANCH c rs›
by -(rule Branch, simp add: Branch_def, subst eq, simp)
qed
qed

lemma resumption_split:
"P (case_resumption t l br r) ⟷
(∀a. r = Terminal a ⟶ P (t a)) ∧
(∀b r'. r = Linear b r' ⟶ P (l b r')) ∧
(∀c rs. r = Branch c rs ⟶ P (br c rs))"
by(cases r) simp_all

lemma resumption_split_asm:
"P (case_resumption t l br r) ⟷
¬ ((∃a. r = Terminal a ∧ ¬ P (t a)) ∨
(∃b r'. r = Linear b r' ∧ ¬ P (l b r')) ∨
(∃c rs. r = Branch c rs ∧ ¬ P (br c rs)))"
by(cases r) simp_all

lemmas resumption_splits = resumption_split resumption_split_asm

text ‹corecursion operator›

Terminal_corec 'a
| Linear_corec 'b 'e
| Branch_corec 'c "'d ⇒ 'e"
| Resumption_corec "('a, 'b, 'c, 'd) resumption"

primrec RESUMPTION_corec_aux :: "nat ⇒ ('e ⇒ ('a,'b,'c,'d,'e) resumption_corec) ⇒ 'e ⇒ ('c + 'b + 'a,'d) Old_Datatype.dtree"
where
"RESUMPTION_corec_aux 0 f e = {}"
| "RESUMPTION_corec_aux (Suc n) f e =
(case f e of Terminal_corec a ⇒ TERMINAL a
| Linear_corec b e' ⇒ LINEAR b (RESUMPTION_corec_aux n f e')
| Branch_corec c es ⇒ BRANCH c (λd. RESUMPTION_corec_aux n f (es d))
| Resumption_corec r ⇒ Rep_resumption r)"

definition RESUMPTION_corec :: "('e ⇒ ('a,'b,'c,'d,'e) resumption_corec) ⇒ 'e ⇒ ('c + 'b + 'a,'d) Old_Datatype.dtree"
where
"RESUMPTION_corec f e = (⋃n. RESUMPTION_corec_aux n f e)"

lemma RESUMPTION_corec [nitpick_simp]:
"RESUMPTION_corec f e =
(case f e of Terminal_corec a ⇒ TERMINAL a
| Linear_corec b e' ⇒ LINEAR b (RESUMPTION_corec f e')
| Branch_corec c es ⇒ BRANCH c (λd. RESUMPTION_corec f (es d))
| Resumption_corec r ⇒ Rep_resumption r)"
(is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs" unfolding RESUMPTION_corec_def
proof(rule UN_least)
fix n
show "RESUMPTION_corec_aux n f e
⊆ (case f e of Terminal_corec a ⇒ TERMINAL a
| Linear_corec b e' ⇒ LINEAR b (⋃n. RESUMPTION_corec_aux n f e')
| Branch_corec c es ⇒ BRANCH c (λd. ⋃n. RESUMPTION_corec_aux n f (es d))
| Resumption_corec r ⇒ Rep_resumption r)"
apply(cases n, simp_all split: resumption_corec.split)
by(rule conjI strip LINEAR_mono[OF UN_upper] BRANCH_mono[OF UN_upper] UNIV_I)+
qed
next
show "?rhs ⊆ ?lhs" unfolding RESUMPTION_corec_def
apply(simp split: resumption_corec.split add: LINEAR_UN BRANCH_UN)
by safe(rule_tac a="Suc n" for n in UN_I, rule UNIV_I, simp)+
qed

lemma RESUMPTION_corec_type: "RESUMPTION_corec f e ∈ resumption"
proof -
have "∃x. RESUMPTION_corec f e = RESUMPTION_corec f x" by blast
thus ?thesis
proof coinduct
case (resumption x)
then obtain e where x: "x = RESUMPTION_corec f e" by blast
thus ?case
proof(cases "f e")
case (Resumption_corec r)
thus ?thesis using x
by(cases r)(simp_all add: RESUMPTION_corec Rep_resumption_constructors Rep_resumption)
qed
qed

text ‹corecursion operator for the resumption type›

definition resumption_corec :: "('e ⇒ ('a,'b,'c,'d,'e) resumption_corec) ⇒ 'e ⇒ ('a,'b,'c,'d) resumption"
where
"resumption_corec f e = Abs_resumption (RESUMPTION_corec f e)"

lemma resumption_corec:
"resumption_corec f e =
(case f e of Terminal_corec a ⇒ Terminal a
| Linear_corec b e' ⇒ Linear b (resumption_corec f e')
| Branch_corec c es ⇒ Branch c (λd. resumption_corec f (es d))
| Resumption_corec r ⇒ r)"
unfolding resumption_corec_def
apply(subst RESUMPTION_corec)
apply(auto split: resumption_corec.splits simp add: Terminal_def Linear_def Branch_def RESUMPTION_corec_type Abs_resumption_inverse Rep_resumption_inverse)
done

text ‹Equality as greatest fixpoint›

coinductive Eq_RESUMPTION :: "('c+'b+'a, 'd) Old_Datatype.dtree ⇒ ('c+'b+'a, 'd) Old_Datatype.dtree ⇒ bool"
where
EqTERMINAL: "Eq_RESUMPTION (TERMINAL a) (TERMINAL a)"
| EqLINEAR: "Eq_RESUMPTION r r' ⟹ Eq_RESUMPTION (LINEAR b r) (LINEAR b r')"
| EqBRANCH: "(⋀d. Eq_RESUMPTION (rs d) (rs' d)) ⟹ Eq_RESUMPTION (BRANCH c rs) (BRANCH c rs')"

lemma Eq_RESUMPTION_implies_ntrunc_equality:
"Eq_RESUMPTION r r' ⟹ ntrunc k r = ntrunc k r'"
proof(induct k arbitrary: r r' rule: less_induct)
case (less k)
note IH = ‹⋀k' r r'. ⟦k' < k; Eq_RESUMPTION r r'⟧ ⟹ ntrunc k' r = ntrunc k' r'›
from ‹Eq_RESUMPTION r r'› show ?case
proof cases
case EqTERMINAL
thus ?thesis by simp
next
case (EqLINEAR R R' b)
thus ?thesis unfolding LINEAR_def
apply(cases k, simp)
apply(rename_tac k', case_tac k', simp)
apply(rename_tac k'', case_tac k'', simp_all add: IH)
done
next
case (EqBRANCH rs rs' c)
thus ?thesis unfolding BRANCH_def
apply(cases k, simp)
apply(rename_tac k', case_tac k', simp)
apply(rename_tac k'', case_tac k'', simp)
apply(rename_tac k''', case_tac k''', simp_all)
apply(rule arg_cong[where f=Old_Datatype.Lim])
apply(rule ext)
done
qed
qed

lemma Eq_RESUMPTION_refl:
assumes "r ∈ resumption"
shows "Eq_RESUMPTION r r"
proof -
define r' where "r' = r"
with assms have "r = r' ∧ r ∈ resumption" by auto
thus "Eq_RESUMPTION r r'"
proof(coinduct)
case (Eq_RESUMPTION r r')
hence [simp]: "r = r'" and "r ∈ resumption" by auto
from ‹r ∈ resumption› show ?case
by(cases rule: resumption.cases) auto
qed
qed

lemma Eq_RESUMPTION_into_resumption:
assumes "Eq_RESUMPTION r r"
shows "r ∈ resumption"
using assms
proof(coinduct)
case resumption thus ?case by cases auto
qed

lemma Eq_RESUMPTION_eq:
"Eq_RESUMPTION r r' ⟷ r = r' ∧ r ∈ resumption"
proof(rule iffI)
assume "Eq_RESUMPTION r r'"
hence "⋀k. ntrunc k r = ntrunc k r'" by(rule Eq_RESUMPTION_implies_ntrunc_equality)
hence "r = r'" by(rule ntrunc_equality)
moreover with ‹Eq_RESUMPTION r r'› have "r ∈ resumption"
by(auto intro: Eq_RESUMPTION_into_resumption)
ultimately show "r = r' ∧ r ∈ resumption" ..
next
assume "r = r' ∧ r ∈ resumption"
thus "Eq_RESUMPTION r r'" by(blast intro: Eq_RESUMPTION_refl)
qed

lemma Eq_RESUMPTION_I [consumes 1, case_names Eq_RESUMPTION, case_conclusion Eq_RESUMPTION EqTerminal EqLinear EqBranch]:
assumes "X r r'"
and step: "⋀r r'. X r r' ⟹
(∃a. r = TERMINAL a ∧ r' = TERMINAL a) ∨
(∃R R' b. r = LINEAR b R ∧ r' = LINEAR b R' ∧ (X R R' ∨ Eq_RESUMPTION R R')) ∨
(∃rs rs' c. r = BRANCH c rs ∧ r' = BRANCH c rs' ∧ (∀d. X (rs d) (rs' d) ∨ Eq_RESUMPTION (rs d) (rs' d)))"
shows "r = r'"
proof -
from ‹X r r'› have "Eq_RESUMPTION r r'"
by(coinduct)(rule step)
qed

lemma resumption_equalityI [consumes 1, case_names Eq_resumption, case_conclusion Eq_resumption EqTerminal EqLinear EqBranch]:
assumes "X r r'"
and step: "⋀r r'. X r r' ⟹
(∃a. r = Terminal a ∧ r' = Terminal a) ∨
(∃R R' b. r = Linear b R ∧ r' = Linear b R' ∧ (X R R' ∨ R = R')) ∨
(∃rs rs' c. r = Branch c rs ∧ r' = Branch c rs' ∧ (∀d. X (rs d) (rs' d) ∨ rs d = rs' d))"
shows "r = r'"
proof -
define M N where "M = Rep_resumption r" and "N = Rep_resumption r'"
with ‹X r r'› have "∃r r'. M = Rep_resumption r ∧ N = Rep_resumption r' ∧ X r r'" by blast
hence "M = N"
proof(coinduct rule: Eq_RESUMPTION_I)
case (Eq_RESUMPTION M N)
then obtain r r' where [simp]: "M = Rep_resumption r" "N = Rep_resumption r'"
and "X r r'" by blast
{ assume "∃a. r = Terminal a ∧ r' = Terminal a"
hence ?EqTerminal by(auto simp add: Rep_resumption_constructors)
hence ?case .. }
moreover
{ assume "∃R R' b. r = Linear b R ∧ r' = Linear b R' ∧ (X R R' ∨ R = R')"
hence ?EqLinear
by(clarsimp simp add: Rep_resumption_constructors Eq_RESUMPTION_eq Rep_resumption_inject Rep_resumption)
hence ?case by blast }
moreover
{ assume "∃rs rs' c. r = Branch c rs ∧ r' = Branch c rs' ∧ (∀d. X (rs d) (rs' d) ∨ rs d = rs' d)"
hence ?EqBranch
by(clarsimp simp add: Rep_resumption_constructors Eq_RESUMPTION_eq Rep_resumption_inject Rep_resumption)
hence ?case by blast }
ultimately show ?case using step[OF ‹X r r'›] by blast
qed
thus ?thesis unfolding M_def N_def by(simp add: Rep_resumption_inject)
qed

text ‹
Finality of ‹resumption›: Uniqueness of functions defined by corecursion.
›

lemma equals_RESUMPTION_corec:
assumes h: "⋀x. h x = (case f x of Terminal_corec a ⇒ TERMINAL a
| Linear_corec b x' ⇒ LINEAR b (h x')
| Branch_corec c xs ⇒ BRANCH c (λd. h (xs d))
| Resumption_corec r ⇒ Rep_resumption r)"
shows "h = RESUMPTION_corec f"
proof
fix x
define h' where "h' = RESUMPTION_corec f"
have h': "⋀x. h' x = (case f x of Terminal_corec a ⇒ TERMINAL a
| Linear_corec b x' ⇒ LINEAR b (h' x')
| Branch_corec c xs ⇒ BRANCH c (λd. h' (xs d))
| Resumption_corec r ⇒ Rep_resumption r)"
define M N where "M = h x" and "N = h' x"
hence "∃x. M = h x ∧ N = h' x" by blast
thus "M = N"
proof(coinduct rule: Eq_RESUMPTION_I)
case (Eq_RESUMPTION M N)
then obtain x where [simp]: "M = h x" "N = h' x" by blast
show ?case
proof(cases "f x")
case (Terminal_corec a)
with h h' have ?EqTerminal by simp
thus ?thesis ..
next
case (Linear_corec b x')
with h h' have ?EqLinear by auto
thus ?thesis by blast
next
case (Branch_corec c xs)
with h h' have ?EqBranch by auto
thus ?thesis by blast
next
case (Resumption_corec r)
thus ?thesis
by(cases r)(simp_all add: h h' Rep_resumption_constructors Eq_RESUMPTION_refl Rep_resumption)
qed
qed
qed

lemma equals_resumption_corec:
assumes h: "⋀x. h x = (case f x of Terminal_corec a ⇒ Terminal a
| Linear_corec b x' ⇒ Linear b (h x')
| Branch_corec c xs ⇒ Branch c (λd. h (xs d))
| Resumption_corec r ⇒ r)"
shows "h = resumption_corec f"
proof(rule ext)
fix x
{ fix x
from h[of x]
have "Rep_resumption (h x) =
(case f x of Terminal_corec a ⇒ TERMINAL a
| Linear_corec b x' ⇒ LINEAR b (Rep_resumption (h x'))
| Branch_corec c xs ⇒ BRANCH c (λd. Rep_resumption (h (xs d)))
| Resumption_corec r ⇒ Rep_resumption r)"
by(auto split: resumption_corec.split simp add: Rep_resumption_constructors) }
hence eq: "(λx. Rep_resumption (h x)) = RESUMPTION_corec f" by(rule equals_RESUMPTION_corec)
hence "Abs_resumption (Rep_resumption (h x)) = Abs_resumption (RESUMPTION_corec f x)"
by(subst (asm) fun_eq_iff)(auto)
from this[symmetric] show "h x = resumption_corec f x"
qed

end