Theory TD0

section ‹TD0›

theory TD0
  imports Main "HOL.Complete_Lattices" Basics
begin

context 
  fixes T :: "'x ⇒ ('x, 'd::complete_lattice) strategy_tree"
begin

subsection ‹Definitions›

datatype ('a,'b) trace = Node 'a "('a,'b) trace list" 'b

function (domintros) solve :: "('x , 'd) strategy_tree ⇒ 'd" where
  "solve (Answer d) = d" |
  "solve (Query x f) = solve (f (solve (T x)))"
  by pat_completeness auto

function (domintros) solve_trace_rec ::
    "('x , 'd) strategy_tree ⇒ ('x, 'd) trace list ⇒ 'd × ('x, 'd) trace list" where
  "solve_trace_rec (Answer d) tr = (d, List.rev tr)" |
  "solve_trace_rec (Query x f) tr = (let (d, xtr) = solve_trace_rec (T x) []
                                    in solve_trace_rec (f d) ((Node x xtr d) # tr))"
  by pat_completeness auto
(*
 * Note: in principle the second case could be written using solve_trace as:
 * solve_trace_rec (f d) ((solve_trace x) # tr)
 *)
declare solve_trace_rec.domintros [simp]
declare solve_trace_rec.psimps [simp]

definition solve_trace :: "'x ⇒ ('x, 'd) trace" where
  "solve_trace x = (let (d, tr) = solve_trace_rec (T x) [] in Node x tr d)"

(* consistent trace including σ as solution *)
(* consistent_sub_trace *)
fun consistent_sub_trace :: "('x, 'd) trace list ⇒ ('x, 'd) strategy_tree ⇒ 'd ⇒ bool" where
  "consistent_sub_trace [] (Answer d) d' = (d = d')"
| "consistent_sub_trace ((Node x' _ xd) # trs) (Query x f) d =
    (x = x' ∧ consistent_sub_trace trs (f xd) d)"
| "consistent_sub_trace _ _ _ = False"

(* consistent_trace *)
fun consistent_trace :: "('x, 'd) trace ⇒ bool" where
  (*"consistent_trace (Node x [] d) = consistent_sub_trace [] (T x) d"*)(* included in second case *)
  "consistent_trace (Node x xtr d) =
    (consistent_sub_trace xtr (T x) d ∧ list_all (λt. consistent_trace t) xtr)"

(* auxiliary function for proof *)
fun descend_tree ::
    "('x, 'd) strategy_tree ⇒ ('x, 'd) trace list ⇒ ('x, 'd) strategy_tree option" where
  "descend_tree (Answer d) [] = Some (Answer d)"
| "descend_tree (Query x f) [] = Some (Query x f)"
| "descend_tree (Query x f) (Node y _ xd # trs) = (if x = y then descend_tree (f xd) trs else None)"
| "descend_tree _ _ = None"

text‹Induction rule for induction over trace›

thm trace.induct
lemma trace_induct [case_names Leaf Node]:
  assumes "⋀x d. P (Node x [] d)"
    and "⋀x dtrs d. dtrs ≠ [] ⟹ (⋀dtr. dtr ∈ set dtrs ⟹ P dtr) ⟹ P (Node x dtrs d)"
  shows "P t"
  using assms by (metis trace.induct)

text‹Dom lemmas›

thm solve_trace_rec.pinduct

lemma solve_trace_rec_dom_backwards:
  assumes "solve_trace_rec_dom ((Query x f), tr)"
    and "(d, xtr) = solve_trace_rec (T x) []"
  shows "solve_trace_rec_dom (T x, []) ∧ solve_trace_rec_dom (f d, (Node x xtr d) # tr)"
  using assms
proof (induction "Query x f" tr arbitrary: x f d xtr rule: solve_trace_rec.pinduct)
  case (2 x f tr)
  then show ?case
  proof (cases "T x")
    case (Answer d1)
    then show ?thesis
    proof (cases "f d")
      case (Query y g)
      then have "solve_trace_rec_dom (Query y g, Node x xtr d # tr)"
        using "2.hyps"(3) "2.prems" by (cases "solve_trace_rec (T y) []") auto
      then show ?thesis by (simp add: Answer Query)
    qed simp
  next
    case (Query y g)
    then have "solve_trace_rec_dom (Query y g, [])"
      using "2.hyps"(2)
      by (cases "solve_trace_rec (T y) []") auto
    moreover have "solve_trace_rec_dom (f d, Node x xtr d # tr)"
    proof (cases "f d")
      case (Query z h)
      then show ?thesis using "2.hyps"(3) "2.prems"
        by (cases "solve_trace_rec (T z) []") auto
    qed (auto simp add: Query "2.hyps"(2))
    ultimately show ?thesis using Query by auto
  qed
qed

lemma solve_trace_rec_dom_tr_indp: "solve_trace_rec_dom (t,tr) ⟹ solve_trace_rec_dom (t,tr')"
  by (induction t tr arbitrary: tr' rule: solve_trace_rec.pinduct) auto


subsection ‹Helper lemmas›

lemma solve_applied:
  assumes "solve_trace_rec_dom (Query x f, trs)"
  shows "∃xd xtrs. solve_trace_rec (Query x f) trs = solve_trace_rec (f xd) ((Node x xtrs xd) # trs)
          ∧ solve_trace_rec (T x) [] = (xd, xtrs)"
  using assms by (auto split: prod.split)

lemma solve_trace_simp:
  shows "(solve_trace x = Node x xtrs xd) = (solve_trace_rec (T x) [] = (xd, xtrs))"
  using solve_trace_def by (auto split: prod.splits)

corollary solve_applied_trs:
  assumes "solve_trace_rec_dom (Query x f, [])"
    and "solve_trace_rec_dom (Query x f, trs)"
    and "solve_trace_rec (T x) [] = (xd, xtrs)"
  shows "solve_trace_rec (Query x f) trs = solve_trace_rec (f xd) (Node x xtrs xd # trs)"
  using assms by simp

lemma increasing_length:
  assumes "solve_trace_rec_dom (Query x f, trs')"
    and "solve_trace_rec (Query x f) trs' = (d, trs)"
  shows "length trs' < length trs"
proof -
  obtain xd xtrs where D1: "(xd, xtrs) = solve_trace_rec (T x) []"
      and D2: "solve_trace_rec (f xd) ((Node x xtrs xd) # trs') = (d, trs)"
    using assms solve_applied[of x f trs'] by fastforce
  then have f_xd_dom: "solve_trace_rec_dom (f xd, (Node x xtrs xd) # trs')"
    using assms(1) solve_trace_rec_dom_backwards by auto
  have "length trs' < length (snd (solve_trace_rec (f xd) (Node x xtrs xd # trs')))"
    using f_xd_dom
  proof (induction t ≡"f xd" arbitrary: xtrs xd x f trs')
    case (Answer e)
    have "snd (solve_trace_rec (Answer e) ((Node x xtrs xd) # trs')) = rev (Node x xtrs xd # trs')"
      by (simp (no_asm))
    then show ?case using D2 Answer by simp
  next
    case (Query y g)
    define tr where [simp]: "tr = Node x xtrs xd"
    have D: "solve_trace_rec_dom (Query y g, tr # trs')"
      using Query.prems(1) Query.hyps(2) by auto
    then obtain yd and ytrs where y_simp: "solve_trace_rec (Query y g) (tr # trs')
          = solve_trace_rec (g yd) (Node y ytrs yd # Node x xtrs xd # trs')"
        and solve_Ty:"(yd, ytrs) =  solve_trace_rec (T y) []"
      using Query.hyps(2) assms(1) solve_applied[of y g "tr # trs'"]
      by auto
    have "solve_trace_rec_dom ((g yd), Node y ytrs yd # tr # trs')"
      using solve_trace_rec_dom_backwards solve_Ty D by auto
    then have "length trs' < length (snd (solve_trace_rec (g yd) (Node y ytrs yd # tr # trs')))"
      using D Query.hyps(1) solve_applied solve_trace_rec_dom_backwards y_simp by fastforce
    then show ?case using Query.hyps(2) y_simp by auto
  qed
  then show ?thesis using D2 by (cases "solve_trace_rec (f xd) (Node x xtrs xd # trs')") auto
qed

corollary answer_same_length:
  assumes "solve_trace_rec_dom (t, trs)"
    and "length (snd (solve_trace_rec t trs)) = length trs"
  shows " ∃d. t = Answer d"
proof(rule ccontr)
  assume "¬?thesis"
  then obtain y and g where t_simp: "t = Query y g" by (cases t) auto
  have "length trs < length(snd (solve_trace_rec (Query y g) trs))"
    using assms(1) increasing_length[of y g trs] t_simp
    by (cases "solve_trace_rec (Query y g) trs") auto
  then show "False" using t_simp assms(2) by auto
qed

corollary non_empty_result:
  assumes "solve_trace_rec_dom ((Query x f), trs)"
  shows "solve_trace_rec (Query x f) trs ≠ (d, [])"
proof(rule ccontr)
  assume "¬?thesis"
  then have "length trs < length []"
    using assms(1) increasing_length[of x f trs] by auto
  then show "False" by auto
qed

lemma wellformed_trace_aux:
  assumes "solve_trace_rec_dom (qat, trs)"
    and "solve_trace_rec qat trs = (d, trs')"
    and "∀tr ∈ set trs. ∃y. tr = solve_trace y"
    and "tr ∈ set trs'"
  shows "∃y. tr = solve_trace y"
  using assms
proof(induction qat arbitrary: trs trs')
  case (Query x f)
  then obtain xd xtrs where xd_xtrs_def: "solve_trace_rec (T x) [] = (xd, xtrs)"
      and res: "solve_trace_rec (f xd) (Node x xtrs xd # trs) = (d, trs')"
    using solve_applied[of x f trs] by auto
  then have "Node x xtrs xd = solve_trace x" using solve_trace_def by auto
  then have "∀tr ∈ set (Node x xtrs xd # trs). ∃y. tr = solve_trace y"
    using Query.prems(3) by auto
  then show ?case using Query.IH Query.prems(1,4) res solve_trace_rec_dom_backwards xd_xtrs_def
    by (cases "solve_trace_rec (T x) []") (metis rangeI)
qed auto

lemma wellformed_trace:
  assumes "solve_trace_rec_dom (T x, [])"
    and "solve_trace_rec (T x) [] = (xd, xtrs)"
    and "tr ∈ set xtrs"
  shows "∃y ytrs yd. tr = Node y ytrs yd ∧ solve_trace_rec (T y) [] = (yd, ytrs)"
proof -
  obtain y where "tr = solve_trace y" using wellformed_trace_aux[of "T x" "[]"]
    using assms by auto
  then show ?thesis
    using solve_trace_simp by (cases "solve_trace_rec (T y) []") blast
qed

lemma trs_trans:
  assumes "solve_trace_rec_dom (t, [])"
    and "solve_trace_rec t [] = (d, trs')"
  shows "solve_trace_rec t trs = (d, rev trs @ trs')"
  using assms
proof(induction t arbitrary: d trs trs')
  case (Query y g)
  obtain ytrs yd
    where y_simp: "solve_trace_rec (Query y g) [] = solve_trace_rec (g yd) [Node y ytrs yd]"
      and y_solve: "solve_trace_rec (T y) [] = (yd, ytrs)"
    using Query.prems(1) solve_applied solve_trace_simp by blast
  have dom_query_y: "solve_trace_rec_dom ((Query y g), trs)"
    using Query.prems(1) solve_trace_rec_dom_tr_indp by blast
  have "solve_trace_rec_dom (g yd, [Node y ytrs yd])"
    using Query.prems(1) solve_trace_rec_dom_backwards solve_trace_simp y_solve by fastforce
  then have dom_g_yd: "solve_trace_rec_dom (g yd, [])"
    using solve_trace_rec_dom_tr_indp by auto
  obtain d' trs'' where IH: "solve_trace_rec (g yd) [] = (d', trs'')" by fastforce
  then have d_simp: "d = d'" and trs'_def: "trs' = Node y ytrs yd # trs''"
    using Query.prems(2) y_simp Query.IH ‹solve_trace_rec_dom (g yd, [])› by auto
  then have "solve_trace_rec (g yd) (Node y ytrs yd # trs) = (d', rev trs @ Node y ytrs yd # trs'')"
    using IH Query.IH dom_g_yd by auto
  then show ?case using Query.prems(1) d_simp trs'_def dom_query_y solve_applied_trs y_solve by auto
qed auto

subsection ‹Descend lemmas›

lemma descend_query:
  assumes A1: "descend_tree t trs = Some (Query y g)"
  shows "∃x f. t = Query x f"
proof (rule ccontr)
  assume "∄x f. t = Query x f"
  then obtain d where "t = Answer d" by (cases t) auto
  then show False using A1 by (cases trs) auto
qed

lemma descend_downward_step:
  assumes "trs = trs1 @ [Node y ytrs yd]"
    and "descend_tree t trs1 = Some (Query y g)"
  shows "descend_tree t trs = Some (g yd)"
  using assms
proof(induction trs arbitrary: t trs1 y ytrs yd g)
  case Nil
  then show ?case by (auto elim: descend_tree.elims)
next
  case (Cons tr trs'')
  then obtain x f where t_simp: "t = Query x f" using descend_query by blast
  then show ?case using Cons descend_tree.simps
    by (cases trs1; cases tr, cases "g yd") (auto split: if_splits)
qed

lemma descend_tree_append:
  assumes "trs = trs1 @ trs2"
    and "descend_tree t trs1 = Some t1"
  shows "descend_tree t trs = descend_tree t1 trs2"
  using assms
proof (induction trs1 arbitrary: t trs)
  case Nil
  then show ?case using descend_tree.elims by auto
next
  case (Cons tr trs1')
  then show ?case by (cases t; cases tr) auto
qed

lemma descend_tree_append_query:
  assumes "trs = trs1 @ [Node y ytrs yd]"
    and "descend_tree t trs1 = Some (Query y g)"
  shows "descend_tree t trs = Some (g yd)"
  using assms descend_downward_step by auto

lemma descend_tree_cont_some:
  assumes "descend_tree t trs = Some t2"
    and "trs = trs1 @ trs2"
  shows "∃t1. descend_tree t trs1 = Some t1"
  using assms
proof(induction t trs1 arbitrary: trs rule: descend_tree.induct)
  case (3 x f y ytrs yd trs1)
  have [simp]: "x = y" using "3.prems" descend_tree.elims[of "Query x f"] by fastforce
  then show ?case using descend_tree.elims "3.prems" "3.IH" by auto
qed auto

lemma descend_upward_query:
  fixes y ytrs yd
  defines "tr ≡ Node y ytrs yd"
  assumes "descend_tree qat trs = Some t"
    and "trs = trs1 @ tr # trs2"
  shows "∃g. descend_tree qat trs1 = Some (Query y g)
      ∧ descend_tree (Query y g) (tr # trs2) = Some t"
proof -
  obtain t1 where "descend_tree qat trs1 = Some t1" and "descend_tree t1 (tr # trs2) = Some t"
    using assms descend_tree_append descend_tree_cont_some[of qat _ _ trs1 "tr # trs2"] by auto
  note t1_desc = this
  then obtain g where "t1 = Query y g" using tr_def by (cases t1; fastforce)
  then show ?thesis using tr_def t1_desc by simp
qed

lemma dom_descend:
  assumes "solve_trace_rec_dom (T x, [])"
    and "solve_trace_rec (T x) [] = (d, trs)"
    and "trs = trs1 @ trs2"
    and "descend_tree (T x) trs1 = Some t"
  shows "solve_trace_rec_dom (t, ls)"
  using assms
proof(induction trs1 arbitrary: trs2 t ls rule: rev_induct)
  case Nil
    then have "T x = t" by (cases "T x"; simp)
    then show ?case using Nil.prems(1) solve_trace_rec_dom_tr_indp by simp
next
  case (snoc tr trs1)
  obtain z ztrs zd where tr_simp[simp]: "tr = Node z ztrs zd"
    by (cases tr)
  then obtain f where descend_is_query[simp]: "descend_tree (T x) trs1 = Some (Query z f)"
    using snoc.prems(4) descend_upward_query[of "T x" "trs1 @ [tr]" t trs1] by auto
  then have [simp]: "t = f zd"
    using snoc.prems(4) descend_tree_append_query by simp
  then have [simp]: "solve_trace_rec_dom (Query z f, [])"
    using snoc.prems(1-3) snoc.IH(1) by simp
  have "solve_trace_rec (T z) [] = (zd, ztrs)"
    using snoc.prems(1-4) wellformed_trace[of x] by auto
  then have "solve_trace_rec_dom (f zd, [Node z ztrs zd])"
    using solve_trace_rec_dom_backwards[of z f "[]"] by simp
  then show ?case
    using solve_trace_rec_dom_tr_indp by auto
qed

corollary dom_descend_query:
  assumes "solve_trace_rec_dom (T x, [])"
    and "solve_trace_rec (T x) [] = (d, trs)"
    and "trs = trs1 @ trs2"
    and "descend_tree (T x) trs1 = Some (Query y g)"
  shows "solve_trace_rec_dom (T y, ls)"
proof -
  have query_dom: "solve_trace_rec_dom (Query y g, [])"
    using assms dom_descend[where ?t = "Query y g"] by simp
  then obtain yd ytrs where "solve_trace_rec (T y) [] = (yd, ytrs)"
    using solve_applied[of y g "[]"] by auto
  then have "solve_trace_rec_dom (T y, [])"
    using query_dom solve_trace_rec_dom_backwards[of y g "[]" yd ytrs] by auto
  then show "solve_trace_rec_dom (T y, ls)"
    using solve_trace_rec_dom_tr_indp[of "T y" "[]"] by simp
qed

lemma solve_from_descend:
  assumes "solve_trace_rec_dom (T x, [])"
    and "solve_trace_rec (T x) [] = (d, trs)"
    and "trs = trs1' @ trs2'"
    and "Some t = descend_tree (T x) trs1'"
  shows "solve_trace_rec t (rev trs1') = (d, trs)"
  using assms
proof(induction trs1' arbitrary: trs trs2' t d rule: rev_induct)
  case Nil
  then have "t = T x"
    using descend_tree.simps(1) by (auto elim: solve_trace_rec.pelims)
  then show ?case using Nil.prems(2) by simp
next
  case (snoc tr trs'')
  then obtain y ytrs yd where [simp]: "tr = Node y ytrs yd"
    by (cases tr)
  then have solve_y: "solve_trace_rec (T y) [] = (yd, ytrs)"
    using snoc.prems(1-3) wellformed_trace[of x d trs tr] by simp
  then obtain g where desc_trs'': "descend_tree (T x) trs'' = Some (Query y g)"
    using snoc.prems(3-4) descend_upward_query[of "T x" _ t trs'' y ytrs yd "[]"] by auto
  have [simp]: "t = g yd"
    using snoc.prems(4) desc_trs'' descend_downward_step[of _ trs''] by simp
  have "solve_trace_rec_dom (Query y g, [])" and "solve_trace_rec_dom (Query y g, rev trs'')"
    using snoc.prems(1-3) desc_trs'' dom_descend(1) by auto
    note query_dom = this
  have "solve_trace_rec (Query y g) (rev trs'') = (d, trs)"
    using snoc.prems(1-3) desc_trs'' snoc.IH by simp
  then show ?case
    using query_dom solve_y solve_applied[of y g] by simp
qed

lemma descend_some_on_solve_trace:
  assumes "solve_trace_rec_dom (T x, [])"
    and "solve_trace_rec (T x) [] = (d, trs)"
    and "trs = trs1 @ trs2"
  shows "∃t. descend_tree (T x) trs1 = Some t"
  using assms
proof(induction trs1 arbitrary: trs2 rule: rev_induct)
  case Nil
  then show ?case
    by (cases "T x"; auto)
next
  case (snoc tr trs1)
  obtain t where desc_trs1: "descend_tree (T x) trs1 = Some t"
    using snoc.prems snoc.IH by auto
  show ?case
  proof(cases t)
    case (Answer d')
    then have "solve_trace_rec (Answer d') (rev trs1) = (d, trs)"
      using snoc.prems desc_trs1 solve_from_descend by simp
    then show ?thesis using snoc.prems(3) by auto
  next
    case (Query y g)
    then have desc_trs1': "descend_tree (T x) trs1 = Some (Query y g)"
      using desc_trs1 by simp
    then have trs1_dom: "solve_trace_rec_dom (Query y g, rev trs1)"
      using snoc.prems dom_descend by auto
    obtain yd ytrs where [simp]: "solve_trace_rec (T y) [] = (yd, ytrs)"
      by fastforce
    have gyd_dom: "solve_trace_rec_dom (g yd, Node y ytrs yd # rev trs1)"
      using trs1_dom solve_trace_rec_dom_backwards[of y g "rev trs1" yd ytrs] by simp
    then have "solve_trace_rec_dom (g yd, [])"
      using solve_trace_rec_dom_tr_indp by simp

    have r: "(d, trs) = solve_trace_rec (g yd) (Node y ytrs yd # rev trs1)"
      using snoc.prems desc_trs1' dom_descend solve_applied[of y g "rev trs1"] solve_from_descend
      by auto

    obtain d' trs' where "solve_trace_rec (g yd) [] = (d', trs')" by fastforce
    then have [simp]: "tr = Node y ytrs yd"
      using gyd_dom r snoc.prems(3) solve_trace_rec_dom_tr_indp trs_trans by auto
    then show ?thesis
      using desc_trs1' descend_tree_append_query[of "trs1 @ [tr]" trs1 y ytrs yd "T x" g] by simp
  qed
qed

lemma descend_to_node_is_query:
  assumes "solve_trace_rec_dom (T x, [])"
    and "solve_trace_rec (T x) [] = (d, trs)"
    and "trs = trs1 @ Node y ytrs yd # trs2"
  shows "∃g. descend_tree (T x) trs1 = Some (Query y g)"
proof -
  define tr where [simp]:"tr = Node y ytrs yd"
  obtain t where "descend_tree (T x) (trs1 @ [tr]) = Some t"
    using assms descend_some_on_solve_trace[of x d trs "trs1 @ [tr]"] by auto
  then show "∃g. descend_tree (T x) trs1 = Some (Query y g)"
    using descend_upward_query[of "T x" "trs1 @ [tr]" t trs1 y ytrs yd "[]"] by auto
qed

corollary dom_descend_transitive:
  fixes ls2 :: "('x,'d) trace list"
  assumes "solve_trace_rec_dom (T x, [])"
    and "solve_trace_rec (T x) [] = (d, trs)"
    and "trs = trs1 @ Node y ytrs yd # trs2"
  shows "solve_trace_rec_dom (T y, ls2)"
using assms descend_to_node_is_query[of _ _ _ trs1 _ ytrs _ trs2] dom_descend_query by blast

lemma consistent_cascade:
  assumes "consistent_sub_trace trs qat d"
    and "trs = trs1 @ trs2"
    and "descend_tree qat trs1 = Some t"
  shows "consistent_sub_trace trs2 t d"
  using assms
proof(induction trs1 arbitrary: trs qat trs2 t rule: rev_induct)
  case Nil
  then show ?case by (cases qat, auto)
next
  case (snoc tr trs1)
  obtain t' where desc_trs1: "descend_tree qat trs1 = Some t'"
    using snoc.prems(3) descend_tree_cont_some[of qat "trs1 @ [tr]" t] by auto
  then have ih: "consistent_sub_trace (tr # trs2) t' d"
    using snoc.prems snoc.IH[of trs qat "tr # trs2"] by simp
  obtain y ytrs yd where [simp]: "tr = Node y ytrs yd"
    by (cases tr)
  obtain f where [simp]: "t' = Query y f"
    using ih by (cases t'; auto)
  have "consistent_sub_trace trs2 (f yd) d"
    using ih by auto
  then show ?case
    using snoc.prems(2-3) desc_trs1 descend_downward_step by auto
qed

lemma consistent_sub_trace_from_descend:
  assumes "solve_trace_rec (T x) [] = (xd, xtrs)"
    and "solve_trace_rec_dom (T x, [])"
    and "xtrs = xtrs1 @ xtrs2"
    and "Some t = descend_tree (T x) xtrs1"
  shows "consistent_sub_trace xtrs2 t xd"
  using assms(3,4)
proof(induction xtrs2 arbitrary: xtrs1 t)
  case Nil
  have "solve_trace_rec t (rev xtrs1) = (xd, xtrs)"
    using Nil.prems assms(1,2) solve_from_descend by auto
  moreover have "solve_trace_rec_dom (t, rev xtrs1)"
    using assms(1,2) Nil.prems dom_descend[where ?trs2.0 = "[]"] by auto
  ultimately have "t = Answer xd"
    using Nil.prems(1) answer_same_length[of t "rev xtrs1"] by auto
  then show ?case by simp
next
  case (Cons tr xtrs2)
  define xtrs1' where [simp]:"xtrs1' = xtrs1 @ [tr]"
  obtain y ytrs yd where [simp]: "tr = Node y ytrs yd"
    by (cases tr)
  obtain g where [simp]: "t = Query y g"
    using assms(1,2) Cons.prems descend_to_node_is_query[of x xd xtrs xtrs1]
    by auto
  then have "Some (g yd) = descend_tree (T x) xtrs1'"
    using Cons.prems(2) descend_downward_step[of xtrs1' xtrs1 y ytrs yd "T x" g] by simp
  then show ?case using Cons.prems Cons.IH by simp
qed


subsection‹Partial correctness proof›

lemma correctness_trace_1:
  assumes "solve_trace x = tr"
    and "solve_trace_rec_dom (T x, [])"
  shows "consistent_trace tr"
  using assms
proof(induction tr arbitrary: x rule: trace_induct)
  case (Leaf x' xd)
  have [simp]: "x = x'"
    using Leaf.prems(1) solve_trace_def by (auto split: prod.splits)
  then have "T x = Answer xd"
    using Leaf.prems solve_trace_simp non_empty_result
    by (cases "T x"; auto)
  then show ?case by simp
next
  case (Node x' xtrs xd)
  have [simp]: "x = x'" using Node.prems(1) solve_trace_def by (auto split: prod.splits)
  have "consistent_trace tr" if "tr ∈ set xtrs" for tr
  proof -
    obtain y ytrs yd where [simp]: "tr = Node y ytrs yd"
      by (cases tr)
    then have "solve_trace_rec_dom (T y, [])"
      using Node.prems that solve_trace_simp dom_descend_transitive split_list[of tr xtrs] by auto
    moreover have "solve_trace_rec (T y) [] = (yd, ytrs)"
      using Node.prems that solve_trace_simp wellformed_trace[of x xd xtrs] by auto
    ultimately show ?thesis
      using that solve_trace_simp Node.IH[of tr] by auto
  qed
  moreover have "consistent_sub_trace xtrs (T x) xd"
    using consistent_sub_trace_from_descend[of x] Node.prems(1,2) solve_trace_simp
    by (cases "T x") auto
  ultimately show ?case
    using consistent_trace.simps[of x xtrs] Node.hyps Ball_set_list_all by auto
qed


lemma correctness_trace_2:
  assumes "tr = Node x xtrs xd"
    and "consistent_trace tr"
  shows "solve_trace_rec_dom (T x, []) ∧ solve_trace x = tr"
  using assms
proof(induction tr arbitrary: x xtrs xd rule: trace_induct)
  case (Leaf y yd)
  assume "consistent_trace (Node y [] yd)"
  then have Tx_simp: "T y = Answer yd"
    using consistent_sub_trace.elims(1)[of "[]" "T y" yd]
    by auto
  then show ?case using Tx_simp solve_trace_def Leaf.prems(1) by auto
next
  case (Node y ytrs yd)
  then have outer_IH: "solve_trace_rec (T z) [] = (zd, ztrs) ∧ solve_trace_rec_dom (T z, [])"
    if "tr ∈ set ytrs" "tr = Node z ztrs zd"
    for tr z ztrs zd
    using Node.IH solve_trace_simp that by (auto simp add: Ball_set_list_all[symmetric])
  have "solve_trace_rec_dom (qat, rev ytrs1) ∧ solve_trace_rec (qat) (rev ytrs1) = (yd, ytrs)"
    if "ytrs = ytrs1 @ ytrs2" and "Some qat = descend_tree (T y) ytrs1" for ytrs1 ytrs2 qat
    using that
  proof(induction ytrs2 arbitrary: ytrs1 qat)
    case Nil
    then have "consistent_sub_trace [] qat yd"
      using consistent_cascade Node.prems(2) by auto
    then have "qat = Answer yd" by (cases qat) auto
    then show ?case
      using Nil.prems by auto
  next
    case (Cons tr ytrs2)
    obtain z ztrs zd where tr_simp[simp]: "tr = Node z ztrs zd"
      by (cases tr)
    have "consistent_sub_trace (tr # ytrs2) qat yd"
      using assms(1) Cons.prems(1,2) consistent_cascade Node.prems(2) by auto
    then obtain g where qat'_simp: "Query z g = qat" by (cases qat) auto
    then have "descend_tree (T y) (ytrs1 @ [tr]) = Some (g zd)"
      using descend_downward_step Cons.prems(2) by simp
    then have 1: "solve_trace_rec_dom (g zd, tr # rev ytrs1)"
      and "solve_trace_rec (g zd) (rev (ytrs1 @ [tr])) = (yd, ytrs)"
      using assms(1) Cons.prems(1) Cons.IH(1)[of "ytrs1 @ [tr]"] by auto
    then show ?case
      using outer_IH[of tr z ztrs zd] Cons.prems solve_trace_rec.domintros(2) qat'_simp
      by fastforce
  qed
  note this[of "[]" ytrs "T y"]
  then show ?case using solve_trace_simp Node by (cases "T y") auto
qed

theorem correctness_trace:
  shows "consistent_trace (Node x xtr d)
    ⟷ solve_trace_rec_dom (T x, []) ∧ solve_trace x = (Node x xtr d)"
  using correctness_trace_1 correctness_trace_2 by fast

end
end