Theory TTree

theory TTree
imports Main ConstOn "List-Interleavings"
begin

subsubsection ‹Prefix-closed sets of lists›

definition downset :: "'a list set  bool" where
  "downset xss = (x n. x  xss  take n x  xss)"

lemma downsetE[elim]:
  "downset xss   xs  xss  butlast xs  xss"
by (auto simp add: downset_def butlast_conv_take)

lemma downset_appendE[elim]:
  "downset xss  xs@ys  xss  xs  xss"
by (auto simp add: downset_def) (metis append_eq_conv_conj)

lemma downset_hdE[elim]:
  "downset xss  xs  xss  xs  []  [hd xs]  xss"
by (auto simp add: downset_def) (metis take_0 take_Suc)


lemma downsetI[intro]:
  assumes " xs. xs  xss  xs  []  butlast xs  xss"
  shows  "downset xss"
unfolding downset_def
proof(intro impI allI )
  from assms
  have butlast: " xs. xs  xss  butlast xs  xss"
    by (metis butlast.simps(1))

  fix xs n
  assume "xs  xss"
  show "take n xs  xss"
  proof(cases "n  length xs")
  case True
    from this
    show ?thesis
    proof(induction rule: inc_induct)
    case base with xs  xss show ?case by simp
    next
    case (step n')
      from butlast[OF step.IH] step(2)
      show ?case by (simp add: butlast_take)
    qed      
  next
  case False with xs  xss show ?thesis by simp
  qed
qed

lemma [simp]: "downset {[]}" by auto

lemma downset_mapI: "downset xss  downset (map f ` xss)"
  by (fastforce simp add: map_butlast[symmetric])

lemma downset_filter:
  assumes "downset xss"
  shows "downset (filter P ` xss)"
proof(rule, elim imageE, clarsimp)
  fix xs
  assume "xs  xss"
  thus "butlast (filter P xs)  filter P ` xss"
  proof (induction xs rule: rev_induct)
    case Nil thus ?case by force
  next
    case snoc
    thus ?case using downset xss  by (auto intro: snoc.IH)
  qed
qed

lemma downset_set_subset:
  "downset ({xs. set xs  S})"
by (auto dest: in_set_butlastD)

subsubsection ‹The type of infinite labeled trees›

typedef 'a ttree = "{xss :: 'a list set . []  xss  downset xss}" by auto

setup_lifting type_definition_ttree

subsubsection ‹Deconstructors›

lift_definition possible ::"'a ttree  'a  bool"
  is "λ xss x.  xs. x#xs  xss".

lift_definition nxt ::"'a ttree  'a  'a ttree"
  is "λ xss x. insert [] {xs | xs. x#xs  xss}"
  by (auto simp add: downset_def take_Suc_Cons[symmetric] simp del: take_Suc_Cons)

subsubsection ‹Trees as set of paths›

lift_definition paths :: "'a ttree  'a list set" is "(λ x. x)".

lemma paths_inj: "paths t = paths t'  t = t'" by transfer auto

lemma paths_injs_simps[simp]: "paths t = paths t'  t = t'" by transfer auto

lemma paths_Nil[simp]: "[]  paths t" by transfer simp

lemma paths_not_empty[simp]: "(paths t = {})  False" by transfer auto

lemma paths_Cons_nxt:
  "possible t x  xs  paths (nxt t x)  (x#xs)  paths t"
  by transfer auto

lemma paths_Cons_nxt_iff:
  "possible t x  xs  paths (nxt t x)  (x#xs)  paths t"
  by transfer auto

lemma possible_mono:
  "paths t  paths t'  possible t x  possible t' x"
  by transfer auto

lemma nxt_mono:
  "paths t  paths t'  paths (nxt t x)  paths (nxt t' x)"
  by transfer auto

lemma ttree_eqI: "( x xs. x#xs  paths t  x#xs  paths t')  t = t'"
  apply (rule paths_inj)
  apply (rule set_eqI)
  apply (case_tac x)
  apply auto
  done

lemma paths_nxt[elim]:
 assumes "xs  paths (nxt t x)"
 obtains "x#xs  paths t"  | "xs = []"
 using assms by transfer auto

lemma Cons_path: "x # xs  paths t  possible t x  xs  paths (nxt t x)"
 by transfer auto

lemma Cons_pathI[intro]:
  assumes "possible t x  possible t' x"
  assumes "possible t x  possible t' x  xs  paths (nxt t x)  xs  paths (nxt t' x)"
  shows  "x # xs  paths t  x # xs  paths t'"
using assms by (auto simp add: Cons_path)

lemma paths_nxt_eq: "xs  paths (nxt t x)  xs = []  x#xs  paths t"
 by transfer auto

lemma ttree_coinduct:
  assumes "P t t'"
  assumes " t t' x . P t t'  possible t x  possible t' x"
  assumes " t t' x . P t t'  possible t x  possible t' x  P (nxt t x) (nxt t' x)"
  shows "t = t'"
proof(rule paths_inj, rule set_eqI)
  fix xs
  from assms(1)
  show "xs  paths t  xs  paths t'"
  proof (induction xs arbitrary: t t')
  case Nil thus ?case by simp
  next
  case (Cons x xs t t')
    show ?case
    proof (rule Cons_pathI)
      from P t t'
      show "possible t x  possible t' x" by (rule assms(2))
    next
      assume "possible t x" and "possible t' x"
      with P t t'
      have "P (nxt t x) (nxt t' x)" by (rule assms(3))
      thus "xs  paths (nxt t x)  xs  paths (nxt t' x)" by (rule Cons.IH)
    qed
  qed
qed

subsubsection ‹The carrier of a tree›

lift_definition carrier :: "'a ttree  'a set" is "λ xss. (set ` xss)".

lemma carrier_mono: "paths t  paths t'  carrier t  carrier t'" by transfer auto

lemma carrier_possible:
  "possible t x  x  carrier t" by transfer force

lemma carrier_possible_subset:
   "carrier t  A  possible t x  x  A" by transfer force

lemma carrier_nxt_subset:
  "carrier (nxt t x)  carrier t"
  by transfer auto

lemma Union_paths_carrier: "(xpaths t. set x) = carrier t"
  by transfer auto


subsubsection ‹Repeatable trees›

definition repeatable where "repeatable t = (x . possible t x  nxt t x = t)"

lemma nxt_repeatable[simp]: "repeatable t  possible t x  nxt t x = t"
  unfolding repeatable_def by auto

subsubsection ‹Simple trees›

lift_definition empty :: "'a ttree" is "{[]}" by auto

lemma possible_empty[simp]: "possible empty x'  False"
  by transfer auto

lemma nxt_not_possible[simp]: "¬ possible t x  nxt t x = empty"
  by transfer auto

lemma paths_empty[simp]: "paths empty = {[]}" by transfer auto

lemma carrier_empty[simp]: "carrier empty = {}" by transfer auto

lemma repeatable_empty[simp]: "repeatable empty" unfolding repeatable_def by transfer auto
  

lift_definition single :: "'a  'a ttree" is "λ x. {[], [x]}"
  by auto

lemma possible_single[simp]: "possible (single x) x'  x = x'"
  by transfer auto

lemma nxt_single[simp]: "nxt (single x) x' =  empty"
  by transfer auto

lemma carrier_single[simp]: "carrier (single y) = {y}"
  by transfer auto

lemma paths_single[simp]: "paths (single x) = {[], [x]}"
  by transfer auto

lift_definition many_calls :: "'a  'a ttree" is "λ x. range (λ n. replicate n x)"
  by (auto simp add: downset_def)

lemma possible_many_calls[simp]: "possible (many_calls x) x'  x = x'"
  by transfer (force simp add: Cons_replicate_eq)

lemma nxt_many_calls[simp]: "nxt (many_calls x) x' = (if x' =  x then many_calls x else empty)"
  by transfer (force simp add: Cons_replicate_eq)

lemma repeatable_many_calls: "repeatable (many_calls x)"
  unfolding repeatable_def by auto

lemma carrier_many_calls[simp]: "carrier (many_calls x) = {x}" by transfer auto

lift_definition anything :: "'a ttree" is "UNIV"
  by auto

lemma possible_anything[simp]: "possible anything x'  True"
  by transfer auto

lemma nxt_anything[simp]: "nxt anything x = anything"
  by  transfer auto

lemma paths_anything[simp]:
  "paths anything = UNIV" by transfer auto

lemma carrier_anything[simp]:
  "carrier anything = UNIV" 
  apply (auto simp add: Union_paths_carrier[symmetric])
  apply (rule_tac x = "[x]" in exI)
  apply simp
  done

lift_definition many_among :: "'a set  'a ttree" is "λ S. {xs . set xs  S}"
  by (auto intro: downset_set_subset)

lemma carrier_many_among[simp]: "carrier (many_among S) = S"
 by transfer (auto, metis List.set_insert bot.extremum insertCI insert_subset list.set(1))

subsubsection ‹Intersection of two trees›

lift_definition intersect :: "'a ttree  'a ttree  'a ttree" (infixl "∩∩" 80)
  is "(∩)"
  by (auto simp add: downset_def)

lemma paths_intersect[simp]: "paths (t ∩∩ t') = paths t  paths t'"
  by transfer auto

lemma carrier_intersect: "carrier (t ∩∩ t')  carrier t  carrier t'"
  unfolding Union_paths_carrier[symmetric]
  by auto
  

subsubsection ‹Disjoint union of trees›

lift_definition either :: "'a ttree  'a ttree  'a ttree" (infixl "⊕⊕" 80)
  is "(∪)"
  by (auto simp add: downset_def)
  
lemma either_empty1[simp]: "empty ⊕⊕ t = t"
  by transfer auto
lemma either_empty2[simp]: "t ⊕⊕ empty = t"
  by transfer auto
lemma either_sym[simp]: "t ⊕⊕ t2 = t2 ⊕⊕ t"
  by transfer auto
lemma either_idem[simp]: "t ⊕⊕ t = t"
  by transfer auto

lemma possible_either[simp]: "possible (t ⊕⊕ t') x  possible t x  possible t' x"
  by transfer auto

lemma nxt_either[simp]: "nxt (t ⊕⊕ t') x = nxt t x ⊕⊕ nxt t' x"
  by transfer auto

lemma paths_either[simp]: "paths (t ⊕⊕ t') = paths t  paths t'"
  by transfer simp

lemma carrier_either[simp]:
  "carrier (t ⊕⊕ t') = carrier t  carrier t'"
  by transfer simp

lemma either_contains_arg1: "paths t  paths (t ⊕⊕ t')"
  by transfer fastforce

lemma either_contains_arg2: "paths t'  paths (t ⊕⊕ t')"
  by transfer fastforce

lift_definition Either :: "'a ttree set  'a ttree"  is "λ S. insert [] (S)"
  by (auto simp add: downset_def)

lemma paths_Either: "paths (Either ts) = insert [] ((paths ` ts))"
  by transfer auto

subsubsection ‹Merging of trees›

lemma ex_ex_eq_hint: "(x. (xs ys. x = f xs ys  P xs ys)  Q x)  (xs ys. Q (f xs ys)  P xs ys)"
  by auto

lift_definition both :: "'a ttree  'a ttree  'a ttree" (infixl "⊗⊗" 86)
  is "λ xss yss .  {xs  ys | xs ys. xs  xss  ys  yss}"
  by (force simp: ex_ex_eq_hint dest: interleave_butlast)

lemma both_assoc[simp]: "t ⊗⊗ (t' ⊗⊗ t'') = (t ⊗⊗ t') ⊗⊗ t''"
  apply transfer
  apply auto
  apply (metis interleave_assoc2)
  apply (metis interleave_assoc1)
  done

lemma both_comm: "t ⊗⊗ t' = t' ⊗⊗ t"
  by transfer (auto, (metis interleave_comm)+)

lemma both_empty1[simp]: "empty ⊗⊗ t = t"
  by transfer auto

lemma both_empty2[simp]: "t ⊗⊗ empty = t"
  by transfer auto

lemma paths_both: "xs  paths (t ⊗⊗ t')  ( ys  paths t.  zs  paths t'. xs  ys  zs)"
  by transfer fastforce

lemma both_contains_arg1: "paths t  paths (t ⊗⊗ t')"
  by transfer fastforce

lemma both_contains_arg2: "paths t'  paths (t ⊗⊗ t')"
  by transfer fastforce

lemma both_mono1:
  "paths t  paths t'  paths (t ⊗⊗ t'')  paths (t' ⊗⊗ t'')"
  by transfer auto

lemma both_mono2:
  "paths t  paths t'  paths (t'' ⊗⊗ t)  paths (t'' ⊗⊗ t')"
  by transfer auto

lemma possible_both[simp]: "possible (t ⊗⊗ t') x  possible t x  possible t' x"
proof
  assume "possible (t ⊗⊗ t') x"
  then obtain xs where "x#xs  paths (t ⊗⊗ t')"
    by transfer auto
  
  from x#xs  paths (t ⊗⊗ t')
  obtain ys zs where "ys  paths t" and "zs  paths t'" and "x#xs  ys  zs"
    by transfer auto

  from x#xs  ys  zs
  have "ys  []  hd ys = x   zs  []  hd zs = x"
    by (auto elim: interleave_cases)
  thus "possible t x  possible t' x"
    using  ys  paths t   zs  paths t'
    by transfer auto
next
  assume "possible t x  possible t' x"
  then obtain xs where "x#xs paths t  x#xs paths t'"
    by transfer auto
  from this have "x#xs  paths (t ⊗⊗ t')" by (auto dest: subsetD[OF both_contains_arg1]  subsetD[OF both_contains_arg2])
  thus "possible (t ⊗⊗ t') x" by transfer auto
qed

lemma nxt_both:
    "nxt (t' ⊗⊗ t) x = (if possible t' x  possible t x then nxt t' x ⊗⊗ t ⊕⊕ t' ⊗⊗ nxt t x else
                           if possible t' x then nxt t' x ⊗⊗ t else
                           if possible t x then t' ⊗⊗ nxt t x else
                           empty)"
  by (transfer, auto 4 4 intro: interleave_intros)

lemma Cons_both:
    "x # xs  paths (t' ⊗⊗ t)  (if possible t' x  possible t x then xs  paths (nxt t' x ⊗⊗ t)  xs  paths (t' ⊗⊗ nxt t x) else
                           if possible t' x then xs  paths (nxt t' x ⊗⊗ t) else
                           if possible t x then xs  paths (t' ⊗⊗ nxt t x) else
                           False)"
  apply (auto simp add: paths_Cons_nxt_iff[symmetric] nxt_both)
  by (metis paths.rep_eq possible.rep_eq possible_both)

lemma Cons_both_possible_leftE: "possible t x  xs  paths (nxt t x ⊗⊗ t')  x#xs  paths (t ⊗⊗ t')"
  by (auto simp add: Cons_both)
lemma Cons_both_possible_rightE: "possible t' x  xs  paths (t ⊗⊗ nxt t' x)  x#xs  paths (t ⊗⊗ t')"
  by (auto simp add: Cons_both)

lemma either_both_distr[simp]:
  "t' ⊗⊗ t ⊕⊕ t' ⊗⊗ t'' = t' ⊗⊗ (t ⊕⊕ t'')"
  by transfer auto

lemma either_both_distr2[simp]:
  "t' ⊗⊗ t ⊕⊕ t'' ⊗⊗ t = (t' ⊕⊕ t'') ⊗⊗ t"
  by transfer auto

lemma nxt_both_repeatable[simp]:
  assumes [simp]: "repeatable t'"
  assumes [simp]: "possible t' x"
  shows "nxt (t' ⊗⊗ t) x = t' ⊗⊗ (t ⊕⊕ nxt t x)"
  by (auto simp add: nxt_both)

lemma nxt_both_many_calls[simp]: "nxt (many_calls x ⊗⊗ t) x = many_calls x ⊗⊗ (t  ⊕⊕ nxt t x)"
  by (simp add: repeatable_many_calls)

lemma repeatable_both_self[simp]:
  assumes [simp]: "repeatable t"
  shows "t ⊗⊗ t = t"
  apply (intro paths_inj set_eqI)
  apply (induct_tac x)
  apply (auto simp add: Cons_both paths_Cons_nxt_iff[symmetric])
  apply (metis Cons_both both_empty1 possible_empty)+
  done

lemma repeatable_both_both[simp]:
  assumes "repeatable t"
  shows "t ⊗⊗ t' ⊗⊗ t = t ⊗⊗ t'"
  by (metis repeatable_both_self[OF assms]  both_assoc both_comm)

lemma repeatable_both_both2[simp]:
  assumes "repeatable t"
  shows "t' ⊗⊗ t ⊗⊗ t = t' ⊗⊗ t"
  by (metis repeatable_both_self[OF assms]  both_assoc both_comm)


lemma repeatable_both_nxt:
  assumes "repeatable t"
  assumes "possible t' x"
  assumes "t' ⊗⊗ t = t'"
  shows "nxt t' x ⊗⊗ t = nxt t' x"
proof(rule classical)
  assume "nxt t' x ⊗⊗ t  nxt t' x"
  hence "(nxt t' x ⊕⊕ t') ⊗⊗ t  nxt t' x" by (metis (no_types) assms(1) both_assoc repeatable_both_self)
  thus "nxt t' x ⊗⊗ t = nxt t' x"  by (metis (no_types) assms either_both_distr2 nxt_both nxt_repeatable)
qed

lemma repeatable_both_both_nxt:
  assumes "t' ⊗⊗ t = t'"
  shows "t' ⊗⊗ t'' ⊗⊗ t = t' ⊗⊗ t''"
  by (metis assms both_assoc both_comm)


lemma carrier_both[simp]:
  "carrier (t ⊗⊗ t') = carrier t  carrier t'"
proof-
  {
  fix x
  assume "x  carrier (t ⊗⊗ t')"
  then obtain xs where "xs  paths (t ⊗⊗ t')" and "x  set xs" by transfer auto
  then obtain ys zs where "ys  paths t" and "zs  paths t'" and "xs  interleave ys zs"
    by (auto simp add: paths_both)
  from this(3) have "set xs = set ys  set zs" by (rule interleave_set)
  with ys  _ zs  _ x  set xs
  have "x  carrier t  carrier t'"  by transfer auto
  }
  moreover
  note subsetD[OF carrier_mono[OF both_contains_arg1[where t=t and t' = t']]]
       subsetD[OF carrier_mono[OF both_contains_arg2[where t=t and t' = t']]]
  ultimately
  show ?thesis by auto
qed

subsubsection ‹Removing elements from a tree›

lift_definition without :: "'a  'a ttree  'a ttree"
  is "λ x xss. filter (λ x'. x'  x) ` xss"
  by (auto intro: downset_filter)(metis filter.simps(1) imageI)

lemma paths_withoutI:
  assumes "xs  paths t"
  assumes "x  set xs"
  shows "xs  paths (without x t)"
proof-
  from assms(2)
  have "filter (λ x'. x'  x) xs = xs"  by (auto simp add: filter_id_conv)
  with assms(1)
  have "xs  filter (λ x'. x'  x)` paths t" by (metis imageI)
  thus ?thesis by transfer
qed

lemma carrier_without[simp]: "carrier (without x t) = carrier t - {x}"
  by transfer auto

lift_definition ttree_restr :: "'a set  'a ttree  'a ttree" is "λ S xss. filter (λ x'. x'  S) ` xss"
  by (auto intro: downset_filter)(metis filter.simps(1) imageI)

lemma filter_paths_conv_free_restr:
  "filter (λ x' . x'  S) ` paths t = paths (ttree_restr S t)" by transfer auto

lemma filter_paths_conv_free_restr2:
  "filter (λ x' . x'  S) ` paths t = paths (ttree_restr (- S) t)" by transfer auto

lemma filter_paths_conv_free_without:
  "filter (λ x' . x'  y) ` paths t = paths (without y t)" by transfer auto

lemma ttree_restr_is_empty: "carrier t  S = {}  ttree_restr S t = empty"
  apply transfer
  apply (auto del: iffI )
  apply (metis SUP_bot_conv(2) SUP_inf inf_commute inter_set_filter set_empty)
  apply force
  done

lemma ttree_restr_noop: "carrier t  S  ttree_restr S t = t"
  apply transfer
  apply (auto simp add: image_iff)
  apply (metis SUP_le_iff contra_subsetD filter_True)
  apply (rule_tac x = x in bexI)
  apply (metis SUP_upper contra_subsetD filter_True)
  apply assumption
  done

lemma ttree_restr_tree_restr[simp]:
  "ttree_restr S (ttree_restr S' t) = ttree_restr (S'  S) t"
  by transfer (simp add: image_comp comp_def)

lemma ttree_restr_both:
  "ttree_restr S (t ⊗⊗ t') = ttree_restr S t ⊗⊗ ttree_restr S t'"
  by (force simp add: paths_both filter_paths_conv_free_restr[symmetric] intro: paths_inj filter_interleave  elim: interleave_filter)

lemma ttree_restr_nxt_subset: "x  S  paths (ttree_restr S (nxt t x))  paths (nxt (ttree_restr S t) x)"
  by transfer (force simp add: image_iff)

lemma ttree_restr_nxt_subset2: "x  S  paths (ttree_restr S (nxt t x))  paths (ttree_restr S t)"
  apply transfer
  apply auto
  apply force
  by (metis filter.simps(2) imageI)

lemma ttree_restr_possible: "x  S  possible t x  possible (ttree_restr S t) x"
  by transfer force

lemma ttree_restr_possible2: "possible (ttree_restr S t') x  x  S" 
  by transfer (auto, metis filter_eq_Cons_iff)

lemma carrier_ttree_restr[simp]:
  "carrier (ttree_restr S t) = S  carrier t"
  by transfer auto

(*
lemma intersect_many_among: "t ∩∩ many_among S = ttree_restr S t"
  apply transfer
  apply auto
*)

subsubsection ‹Multiple variables, each called at most once›

lift_definition singles :: "'a set  'a ttree" is "λ S. {xs.  x  S. length (filter (λ x'. x' = x) xs)  1}"
  apply auto
  apply (rule downsetI)
  apply auto
  apply (subst (asm) append_butlast_last_id[symmetric]) back
  apply simp
  apply (subst (asm) filter_append)
  apply auto
  done

lemma possible_singles[simp]: "possible (singles S) x"
  apply transfer'
  apply (rule_tac x = "[]" in exI)
  apply auto
  done

lemma length_filter_mono[intro]:
  assumes "( x. P x  Q x)"
  shows "length (filter P xs)  length (filter Q xs)"
by (induction xs) (auto dest: assms)

lemma nxt_singles[simp]: "nxt (singles S) x' =  (if x'  S then without x' (singles S) else singles S)"
  apply transfer'
  apply auto
  apply (rule rev_image_eqI[where x = "[]"], auto)[1]
  apply (rule_tac x = x in rev_image_eqI)
  apply (simp, rule ballI, erule_tac x = xa in ballE, auto)[1]
  apply (rule sym)
  apply (simp add: filter_id_conv filter_empty_conv)[1]
  apply (erule_tac x = xb in ballE)
  apply (erule order_trans[rotated])
  apply (rule length_filter_mono)
  apply auto
  done

lemma carrier_singles[simp]:
  "carrier (singles S) = UNIV"
  apply transfer
  apply auto
  apply (rule_tac x = "[x]" in exI)
  apply auto
  done

lemma singles_mono:
  "S  S'  paths (singles S')  paths (singles S)"
by transfer auto


lemma paths_many_calls_subset:
  "paths t  paths (many_calls x ⊗⊗ without x t)"
proof
  fix xs
  assume "xs  paths t"
  
  have "filter (λx'. x' = x) xs = replicate (length (filter (λx'. x' = x) xs)) x"
    by (induction xs) auto
  hence "filter (λx'. x' = x) xs  paths (many_calls x)" by transfer auto
  moreover
  from xs  paths t
  have "filter (λx'. x'  x) xs  paths (without x t)" by transfer auto
  moreover
  have "xs  interleave (filter (λx'. x' = x) xs)  (filter (λx'. x'  x) xs)" by (rule interleave_filtered)
  ultimately show "xs  paths (many_calls x ⊗⊗ without x t)" by transfer auto
qed



subsubsection ‹Substituting trees for every node›

definition f_nxt :: "('a  'a ttree)  'a set  'a  ('a  'a ttree)"
  where "f_nxt f T x = (if x  T then f(x:=empty) else f)"

fun substitute' :: "('a  'a ttree)  'a set  'a ttree  'a list  bool" where
    substitute'_Nil: "substitute' f T t []  True"
  | substitute'_Cons: "substitute' f T t (x#xs) 
        possible t x  substitute' (f_nxt f T x) T (nxt t x ⊗⊗ f x) xs"

lemma f_nxt_mono1: "( x. paths (f x)  paths (f' x))  paths (f_nxt f T x x')  paths (f_nxt f' T x x')"
  unfolding f_nxt_def by auto
  
lemma f_nxt_empty_set[simp]: "f_nxt f {} x = f" by (simp add: f_nxt_def)

lemma downset_substitute: "downset (Collect (substitute' f T t))"
apply (rule) unfolding mem_Collect_eq
proof-
  fix x
  assume "substitute' f T t x"
  thus "substitute' f T t (butlast x)" by(induction t x rule: substitute'.induct) (auto)
qed

lift_definition substitute :: "('a  'a ttree)  'a set  'a ttree  'a ttree"
  is "λ f T t. Collect (substitute' f T t)"
  by (simp add: downset_substitute)

lemma elim_substitute'[pred_set_conv]: "substitute' f T t xs  xs  paths (substitute f T t)" by transfer auto

lemmas substitute_induct[case_names Nil Cons] = substitute'.induct
lemmas substitute_simps[simp] = substitute'.simps[unfolded elim_substitute']

lemma substitute_mono2: 
  assumes "paths t  paths t'"
  shows "paths (substitute f T t)  paths (substitute f T t')"
proof
  fix xs
  assume "xs  paths (substitute f T t)"
  thus "xs  paths (substitute f T t')"
  using assms
  proof(induction xs arbitrary:f t t')
  case Nil
    thus ?case by simp
  next
  case (Cons x xs)
    from Cons.prems
    show ?case
    by (auto dest: possible_mono elim: Cons.IH intro!:  both_mono1 nxt_mono)
  qed
qed

lemma substitute_mono1: 
  assumes "x. paths (f x)  paths (f' x)"
  shows "paths (substitute f T t)  paths (substitute f' T t)"
proof
  fix xs
  assume "xs  paths (substitute f T t)"
  from this assms
  show "xs  paths (substitute f' T t)"
  proof (induction xs arbitrary: f f' t)
    case Nil
    thus ?case by simp
  next
  case (Cons x xs)
    from Cons.prems
    show ?case
    by (auto elim!: Cons.IH dest: subsetD dest!: subsetD[OF f_nxt_mono1[OF Cons.prems(2)]] subsetD[OF substitute_mono2[OF  both_mono2[OF Cons.prems(2)]]])
  qed
qed

lemma substitute_monoT:
  assumes "T  T'"
  shows "paths (substitute f T' t)  paths (substitute f T t)"
proof
  fix xs
  assume "xs  paths (substitute f T' t)"
  thus "xs  paths (substitute f T t)"
  using assms
  proof(induction f T' t xs arbitrary: T rule: substitute_induct)
  case Nil
    thus ?case by simp
  next
  case (Cons f T' t x xs T)
    from x # xs  paths (substitute f T' t)
    have [simp]: "possible t x" and "xs  paths (substitute (f_nxt f T' x) T' (nxt t x ⊗⊗ f x))" by auto
    from Cons.IH[OF this(2) Cons.prems(2)]
    have "xs  paths (substitute (f_nxt f T' x) T (nxt t x ⊗⊗ f x))".
    hence "xs  paths (substitute (f_nxt f T x) T (nxt t x ⊗⊗ f x))"
      by (rule subsetD[OF substitute_mono1, rotated])
         (auto simp add: f_nxt_def subsetD[OF Cons.prems(2)])
    thus ?case by auto
  qed
qed


lemma substitute_contains_arg: "paths t  paths (substitute f T t)"
proof
  fix xs
  show "xs  paths t  xs  paths (substitute f T t)"
  proof (induction xs arbitrary: f t)
    case Nil
    show ?case by simp
  next
    case (Cons x xs)
    from x # xs  paths t 
    have "possible t x" by transfer auto
    moreover
    from x # xs  paths t have "xs  paths (nxt t x)"
      by (auto simp add: paths_nxt_eq)
    hence "xs  paths (nxt t x ⊗⊗ f x)" by (rule subsetD[OF both_contains_arg1])
    note Cons.IH[OF this]
    ultimately
    show ?case by simp
  qed
qed


lemma possible_substitute[simp]: "possible (substitute f T t) x  possible t x"
  by (metis Cons_both both_empty2 paths_Nil substitute_simps(2))

lemma nxt_substitute[simp]: "possible t x  nxt (substitute f T t) x = substitute (f_nxt f T x) T (nxt t x ⊗⊗ f x)"
  by (rule ttree_eqI) (simp add: paths_nxt_eq)

lemma substitute_either: "substitute f T (t ⊕⊕ t') = substitute f T t ⊕⊕ substitute f T t'"
proof-
  have [simp]: " t t' x . (nxt t x ⊕⊕ nxt t' x) ⊗⊗ f x = nxt t x ⊗⊗ f x ⊕⊕ nxt t' x ⊗⊗ f x" by (metis both_comm either_both_distr)
  {
  fix xs
  have "xs  paths (substitute f T (t ⊕⊕ t'))   xs  paths (substitute f T t)  xs  paths (substitute f T t')"
  proof (induction xs arbitrary: f t t')
    case Nil thus ?case by simp
  next
    case (Cons x xs)
    note IH = Cons.IH[where f = "f_nxt f T x" and t = "nxt t' x ⊗⊗ f x" and t' = "nxt t x ⊗⊗ f x"]
    show ?case
    apply (auto simp del: either_both_distr2 simp add: either_both_distr2[symmetric] IH)
    apply (metis IH both_comm either_both_distr either_empty2 nxt_not_possible)
    apply (metis IH both_comm both_empty1 either_both_distr either_empty1 nxt_not_possible)
    done
  qed
  }
  thus ?thesis by (auto intro: paths_inj)
qed


(*
lemma substitute_both: "substitute f (t ⊗⊗ t') = substitute f t ⊗⊗ substitute f t'"
proof (intro paths_inj set_eqI)
  fix xs
  show "(xs ∈ paths (substitute f (t ⊗⊗ t'))) = (xs ∈ paths (substitute f t ⊗⊗ substitute f t'))"
  proof (induction xs arbitrary: t t')
  case Nil thus ?case by simp
  next
  case (Cons x xs)
    have [simp]: "nxt t x ⊗⊗ t' ⊗⊗ f x = nxt t x ⊗⊗ f x ⊗⊗ t'"
      by (metis both_assoc both_comm)
    have [simp]: "t ⊗⊗ nxt t' x ⊗⊗ f x = t ⊗⊗ (nxt t' x ⊗⊗ f x)"
      by (metis both_assoc both_comm)
    note Cons[where t = "nxt t x ⊗⊗ f x" and t' = t', simp]
    note Cons[where t = t and t' = "nxt t' x ⊗⊗ f x", simp]
    show ?case
      by (auto simp add: Cons_both nxt_both either_both_distr2[symmetric] substitute_either
                  simp del: both_assoc )
  qed
qed
*)

lemma f_nxt_T_delete:
  assumes "f x = empty"
  shows "f_nxt f (T - {x}) x' = f_nxt f T x'"
using assms
by (auto simp add: f_nxt_def)

lemma f_nxt_empty[simp]:
  assumes "f x = empty"
  shows "f_nxt f T x' x = empty"
using assms
by (auto simp add: f_nxt_def)

lemma f_nxt_empty'[simp]:
  assumes "f x = empty"
  shows "f_nxt f T x = f"
using assms
by (auto simp add: f_nxt_def)


lemma substitute_T_delete:
  assumes "f x = empty"
  shows "substitute f (T - {x}) t = substitute f T t"
proof (intro paths_inj  set_eqI)
  fix xs
  from assms
  show "xs  paths (substitute f (T - {x}) t)  xs  paths (substitute f T t)"
  by (induction xs arbitrary: f t) (auto simp add: f_nxt_T_delete )
qed


lemma substitute_only_empty:
  assumes "const_on f (carrier t) empty"
  shows "substitute f T t = t"
proof (intro paths_inj  set_eqI)
  fix xs
  from assms
  show "xs  paths (substitute f T t)  xs  paths t"
  proof (induction xs arbitrary: f t)
  case Nil thus ?case by simp
  case (Cons x xs f t)
  
    note const_onD[OF Cons.prems carrier_possible, where y = x, simp]

    have [simp]: "possible t x  f_nxt f T x = f"
      by (rule f_nxt_empty', rule const_onD[OF Cons.prems carrier_possible, where y = x])

    from Cons.prems carrier_nxt_subset
    have "const_on f (carrier (nxt t x)) empty"
      by (rule const_on_subset)
    hence "const_on (f_nxt f T x) (carrier (nxt t x)) empty"
      by (auto simp add: const_on_def f_nxt_def)
    note Cons.IH[OF this]
    hence [simp]: "possible t x  (xs  paths (substitute f T (nxt t x))) = (xs  paths (nxt t x))"
      by simp

    show ?case by (auto simp add: Cons_path)
  qed
qed

lemma substitute_only_empty_both: "const_on f (carrier t') empty  substitute f T (t ⊗⊗ t') = substitute f T t ⊗⊗ t'"
proof (intro paths_inj set_eqI)
  fix xs
  assume "const_on f (carrier t') TTree.empty"
  thus "(xs  paths (substitute f T (t ⊗⊗ t'))) = (xs  paths (substitute f T t ⊗⊗ t'))"
  proof (induction xs arbitrary: f t t')
  case Nil thus ?case by simp
  next
  case (Cons x xs)
    show ?case
    proof(cases "possible t' x")
      case True 
      hence "x  carrier t'" by (metis carrier_possible)
      with Cons.prems have [simp]: "f x = empty" by auto
      hence [simp]: "f_nxt f T x = f" by (auto simp add: f_nxt_def)

      note Cons.IH[OF Cons.prems, where t = "nxt t x", simp]

      from Cons.prems
      have "const_on f (carrier (nxt t' x)) empty" by (metis carrier_nxt_subset const_on_subset)
      note Cons.IH[OF this, where t = t, simp]

      show ?thesis using True
        by (auto simp add: Cons_both nxt_both  substitute_either)
    next
      case False

      have [simp]: "nxt t x ⊗⊗ t' ⊗⊗ f x = nxt t x ⊗⊗ f x ⊗⊗ t'"
        by (metis both_assoc both_comm)

      from Cons.prems
      have "const_on (f_nxt f T x) (carrier t') empty" 
        by (force simp add: f_nxt_def)
      note Cons.IH[OF this, where t = "nxt t x ⊗⊗ f x", simp]

      show ?thesis using False
        by (auto simp add: Cons_both nxt_both  substitute_either)
    qed
  qed
qed
  
lemma f_nxt_upd_empty[simp]:
  "f_nxt (f(x' := empty)) T x = (f_nxt f T x)(x' := empty)"
  by (auto simp add: f_nxt_def)

lemma repeatable_f_nxt_upd[simp]:
  "repeatable (f x)  repeatable (f_nxt f T x' x)"
  by (auto simp add: f_nxt_def)

lemma substitute_remove_anyways_aux:
  assumes "repeatable (f x)"
  assumes "xs  paths (substitute f T t)"
  assumes "t ⊗⊗ f x = t"
  shows "xs  paths (substitute (f(x := empty)) T t)"
  using assms(2,3) assms(1)
proof (induction f T t xs  rule: substitute_induct)
  case Nil thus ?case by simp
next
  case (Cons f T t x' xs)
  show ?case
  proof(cases "x' = x")
    case False
    hence [simp]: "(f(x := TTree.empty)) x' = f x'" by simp
    have [simp]: "f_nxt f T x' x = f x" using False by (auto simp add: f_nxt_def)
    show ?thesis using Cons by (auto  simp add: repeatable_both_nxt repeatable_both_both_nxt   simp del: fun_upd_apply)
  next
    case True
    hence [simp]: "(f(x := TTree.empty)) x = empty" by simp
    (*  have [simp]: "f_nxt f T x' x = f x" using False by (auto simp add: f_nxt_def) *)

    have *: "(f_nxt f T x) x = f x  (f_nxt f T x) x = empty" by (simp add: f_nxt_def)
    thus ?thesis
      using Cons True
      by (auto  simp add: repeatable_both_nxt repeatable_both_both_nxt   simp del: fun_upd_apply)
  qed
qed
      

lemma substitute_remove_anyways:
  assumes "repeatable t"
  assumes "f x = t"
  shows "substitute f T (t ⊗⊗ t') = substitute (f(x := empty)) T (t ⊗⊗ t')"
proof (rule paths_inj, rule, rule subsetI)
  fix xs
  have "repeatable (f x)" using assms by simp
  moreover
  assume "xs  paths (substitute f T (t ⊗⊗ t'))"
  moreover
  have "t ⊗⊗ t' ⊗⊗ f x = t ⊗⊗ t'"
    by (metis assms both_assoc both_comm repeatable_both_self)
  ultimately
  show "xs  paths (substitute (f(x := empty)) T (t ⊗⊗ t'))"
      by (rule substitute_remove_anyways_aux)
next
  show "paths (substitute (f(x := empty)) T (t ⊗⊗ t'))  paths (substitute f T (t ⊗⊗ t'))"
    by (rule substitute_mono1) auto
qed 

lemma carrier_f_nxt: "carrier (f_nxt f T x x')  carrier (f x')"
  by (simp add: f_nxt_def)

lemma f_nxt_cong: "f x' = f' x'  f_nxt f T x x' = f_nxt f' T x x'"
  by (simp add: f_nxt_def)

lemma substitute_cong':
  assumes "xs  paths (substitute f T t)"
  assumes " x n. x  A  carrier (f x)  A"
  assumes "carrier t  A"
  assumes " x. x  A  f x = f' x"
  shows "xs  paths (substitute f' T t)"
  using assms
proof (induction f T t xs arbitrary: f' rule: substitute_induct )
  case Nil thus ?case by simp
next
  case (Cons f T t x xs)
  hence "possible t x" by auto
  hence "x  carrier t" by (metis carrier_possible)
  hence "x  A" using Cons.prems(3) by auto
  with Cons.prems have [simp]: "f' x = f x" by auto
  have "carrier (f x)  A" using x  A by (rule Cons.prems(2))

  from Cons.prems(1,2) Cons.prems(4)[symmetric]
  show ?case
    by (auto elim!: Cons.IH
          dest!: subsetD[OF carrier_f_nxt] subsetD[OF carrier_nxt_subset] subsetD[OF Cons.prems(3)] subsetD[OF carrier (f x)  A]
          intro: f_nxt_cong
          )
qed


lemma substitute_cong_induct:
  assumes " x. x  A  carrier (f x)  A"
  assumes "carrier t  A"
  assumes " x. x  A  f x = f' x"
  shows "substitute f T t = substitute f' T t"
  apply (rule paths_inj)
  apply (rule set_eqI)
  apply (rule iffI)
  apply (erule (2) substitute_cong'[OF _ assms])
  apply (erule substitute_cong'[OF _ _ assms(2)])
  apply (metis assms(1,3))
  apply (metis assms(3))
  done


lemma carrier_substitute_aux:
  assumes "xs  paths (substitute f T t)"
  assumes "carrier t  A"
  assumes " x. x  A  carrier (f x)  A" 
  shows   "set xs  A"
  using assms
  apply(induction  f T t xs rule: substitute_induct)
  apply auto
  apply (metis carrier_possible_subset)
  apply (metis carrier_f_nxt carrier_nxt_subset carrier_possible_subset contra_subsetD order_trans)
  done

lemma carrier_substitute_below:
  assumes " x. x  A  carrier (f x)  A"
  assumes "carrier t  A"
  shows "carrier (substitute f T t)  A"
proof-
  have " xs. xs  paths (substitute f T t)  set xs  A" by (rule carrier_substitute_aux[OF _ assms(2,1)])
  thus ?thesis by (auto simp add:  Union_paths_carrier[symmetric])
qed

lemma f_nxt_eq_empty_iff:
  "f_nxt f T x x' = empty  f x' = empty  (x' = x  x  T)"
  by (auto simp add: f_nxt_def)

lemma substitute_T_cong':
  assumes "xs  paths (substitute f T t)"
  assumes " x.  (x  T  x  T')  f x = empty"
  shows "xs  paths (substitute f T' t)"
  using assms
proof (induction f T t xs  rule: substitute_induct )
  case Nil thus ?case by simp
next
  case (Cons f T t x xs)
  from Cons.prems(2)[where x = x]
  have [simp]: "f_nxt f T x = f_nxt f T' x"
    by (auto simp add: f_nxt_def)

  from Cons.prems(2)
  have "(x'. (x'  T) = (x'  T')  f_nxt f T x x' = TTree.empty)"
    by (auto simp add: f_nxt_eq_empty_iff)
  from Cons.prems(1) Cons.IH[OF _ this]
  show ?case
    by auto
qed

lemma substitute_cong_T:
  assumes " x.  (x  T  x  T')  f x = empty"
  shows "substitute f T = substitute f T'"
  apply rule
  apply (rule paths_inj)
  apply (rule set_eqI)
  apply (rule iffI)
  apply (erule substitute_T_cong'[OF _ assms])
  apply (erule substitute_T_cong')
  apply (metis assms)
  done

lemma carrier_substitute1: "carrier t  carrier (substitute f T t)"
    by (rule carrier_mono) (rule substitute_contains_arg)

lemma substitute_cong:
  assumes " x. x  carrier (substitute f T t)  f x = f' x"
  shows "substitute f T t = substitute f' T t"
proof(rule substitute_cong_induct[OF _ _ assms])
  show "carrier t  carrier (substitute f T t)"
    by (rule carrier_substitute1)
next
  fix x
  assume "x  carrier (substitute f T t)"
  then obtain xs where "xs  paths (substitute f T t)"  and "x  set xs"  by transfer auto
  thus "carrier (f x)  carrier (substitute f T t)"
  proof (induction xs arbitrary: f t)
  case Nil thus ?case by simp
  next
  case (Cons x' xs f t)
    from x' # xs  paths (substitute f T t)
    have "possible t x'" and "xs  paths (substitute (f_nxt f T x') T (nxt t x' ⊗⊗ f x'))" by auto

    from x  set (x' # xs)
    have "x = x'  (x  x'  x  set xs)" by auto
    hence "carrier (f x)  carrier (substitute (f_nxt f T x') T (nxt t x' ⊗⊗ f x'))"
    proof(elim conjE disjE)
      assume "x = x'"
      have "carrier (f x)  carrier (nxt t x ⊗⊗ f x)" by simp
      also have "  carrier (substitute (f_nxt f T x') T (nxt t x ⊗⊗ f x))" by (rule carrier_substitute1)
      finally show ?thesis unfolding x = x'.
    next
      assume "x  x'"
      hence [simp]: "(f_nxt f T x' x) = f x" by (simp add: f_nxt_def)

      assume "x  set xs" 
      from Cons.IH[OF xs  _ this]
      show "carrier (f x)  carrier (substitute (f_nxt f T x') T (nxt t x' ⊗⊗ f x'))" by simp
    qed
    also
    from possible t x'
    have "carrier (substitute (f_nxt f T x') T (nxt t x' ⊗⊗ f x'))   carrier (substitute f T t)"
      apply transfer
      apply auto
      apply (rule_tac x = "x'#xa" in exI)
      apply auto
      done
    finally show ?case.
  qed
qed

lemma substitute_substitute:
  assumes " x. const_on f' (carrier (f x)) empty"
  shows "substitute f T (substitute f' T t) = substitute (λ x. f x ⊗⊗ f' x) T t"
proof (rule paths_inj, rule set_eqI)
  fix xs
  have [simp]: " f f' x'. f_nxt (λx. f x ⊗⊗ f' x) T x' = (λx. f_nxt f T x' x ⊗⊗ f_nxt f' T x' x)"
    by (auto simp add: f_nxt_def)

  from  assms
  show "xs  paths (substitute f T (substitute f' T t))  xs  paths (substitute (λx. f x ⊗⊗ f' x) T t)"
  proof (induction xs arbitrary: f f' t )
  case Nil thus ?case by simp
  case (Cons x xs)
    thus ?case
    proof (cases "possible t x")
      case True

      from Cons.prems
      have prem': " x'. const_on (f_nxt f' T x) (carrier (f x')) empty"
        by (force simp add: f_nxt_def)
      hence "x'. const_on (f_nxt f' T x) (carrier ((f_nxt f T x) x')) empty" 
        by (metis carrier_empty const_onI emptyE f_nxt_def fun_upd_apply)
      note Cons.IH[where f = "f_nxt f T x" and f' = "f_nxt f' T x", OF this, simp]

      have [simp]: "nxt t x ⊗⊗ f x ⊗⊗ f' x = nxt t x ⊗⊗ f' x ⊗⊗ f x"
        by (metis both_comm both_assoc)

      show ?thesis using True
        by (auto del: iffI simp add: substitute_only_empty_both[OF prem'[where x' = x] , symmetric])
    next
    case False
      thus ?thesis by simp
    qed
  qed
qed


lemma ttree_rest_substitute:
  assumes " x. carrier (f x)  S = {}"
  shows "ttree_restr S (substitute f T t) = ttree_restr S t"
proof(rule paths_inj, rule set_eqI, rule iffI)
  fix xs
  assume "xs  paths (ttree_restr S (substitute f T t))"
  then
  obtain xs' where [simp]: "xs = filter (λ x'. x'  S) xs'" and "xs'  paths (substitute f T t)"
    by (auto simp add: filter_paths_conv_free_restr[symmetric])
  from this(2) assms
  have "filter (λ x'. x'  S) xs'   paths (ttree_restr S t)"
  proof (induction xs' arbitrary: f t)
  case Nil thus ?case by simp
  next
  case (Cons x xs f t)
    from Cons.prems
    have "possible t x" and "xs  paths (substitute (f_nxt f T x) T (nxt t x ⊗⊗ f x))" by auto

    from Cons.prems(2)
    have "(x'. carrier (f_nxt f T x x')  S = {})" by (auto simp add: f_nxt_def)
    
    from  Cons.IH[OF xs  _ this]
    have "[x'xs . x'  S]  paths (ttree_restr S (nxt t x) ⊗⊗ ttree_restr S (f x))" by (simp add: ttree_restr_both)
    hence "[x'xs . x'  S]  paths (ttree_restr S (nxt t x))" by (simp add: ttree_restr_is_empty[OF Cons.prems(2)])
    with possible t x
    show "[x'x#xs . x'  S]  paths (ttree_restr S t)"
      by (cases "x  S") (auto simp add: Cons_path ttree_restr_possible  dest: subsetD[OF ttree_restr_nxt_subset2]  subsetD[OF ttree_restr_nxt_subset])
  qed
  thus "xs  paths (ttree_restr S t)" by simp
next
  fix xs
  assume "xs  paths (ttree_restr S t)"
  then obtain xs' where [simp]:"xs = filter (λ x'. x'  S) xs'" and "xs'  paths t" 
    by (auto simp add: filter_paths_conv_free_restr[symmetric])
  from this(2)
  have "xs'  paths (substitute f T t)" by (rule subsetD[OF substitute_contains_arg])
  thus "xs  paths (ttree_restr S (substitute f T t))"
    by (auto simp add: filter_paths_conv_free_restr[symmetric])
qed

text ‹An alternative characterization of substitution›

inductive substitute'' :: "('a  'a ttree)  'a set  'a list  'a list  bool" where
  substitute''_Nil: "substitute'' f T [] []"
  | substitute''_Cons:
    "zs  paths (f x)  xs'  interleave xs zs  substitute'' (f_nxt f T x) T xs' ys
        substitute'' f T (x#xs) (x#ys)"
inductive_cases substitute''_NilE[elim]: "substitute'' f T xs []"  "substitute'' f T [] xs"
inductive_cases substitute''_ConsE[elim]: "substitute'' f T (x#xs) ys"

lemma substitute_substitute'':
  "xs  paths (substitute f T t)  ( xs'  paths t. substitute'' f T xs' xs)"
proof
  assume "xs  paths (substitute f T t)"
  thus " xs'  paths t. substitute'' f T xs' xs"
  proof(induction xs arbitrary: f t)
    case Nil
    have "substitute'' f T [] []"..
    thus ?case by auto
  next
    case (Cons x xs f t)
    from x # xs  paths (substitute f T t)
    have "possible t x" and "xs  paths (substitute (f_nxt f T x) T (nxt t x ⊗⊗ f x))" by (auto simp add: Cons_path)
    from Cons.IH[OF this(2)]
    obtain xs' where "xs'  paths (nxt t x ⊗⊗ f x)" and "substitute'' (f_nxt f T x) T xs' xs" by auto
    from this(1)
    obtain ys' zs' where "ys'  paths (nxt t x)" and "zs'  paths (f x)" and "xs'  interleave ys' zs'" 
      by (auto simp add: paths_both)
  
    from this(2,3) substitute'' (f_nxt f T x) T xs' xs
    have "substitute'' f T (x # ys') (x # xs)"..
    moreover
    from ys'  paths (nxt t x) possible t x
    have "x # ys'  paths t"  by (simp add: Cons_path)
    ultimately
    show ?case by auto
  qed
next
  assume " xs'  paths t. substitute'' f T xs' xs"
  then obtain xs' where  "substitute'' f T xs' xs" and "xs'  paths t"  by auto
  thus "xs  paths (substitute f T t)"
  proof(induction arbitrary: t rule: substitute''.induct[case_names Nil Cons])
  case Nil thus ?case by simp
  next
  case (Cons zs x xs' xs ys t)
    from Cons.prems Cons.hyps
    show ?case by (force simp add: Cons_path paths_both intro!: Cons.IH)
  qed
qed

lemma paths_substitute_substitute'':
  "paths (substitute f T t) = ((λ xs . Collect (substitute'' f T xs)) ` paths t)"
  by (auto simp add: substitute_substitute'')

lemma ttree_rest_substitute2:
  assumes " x. carrier (f x)  S"
  assumes "const_on f (-S) empty"
  shows "ttree_restr S (substitute f T t) = substitute f T (ttree_restr S t)"
proof(rule paths_inj, rule set_eqI, rule iffI)
  fix xs
  assume "xs  paths (ttree_restr S (substitute f T t))"
  then
  obtain xs' where [simp]: "xs = filter (λ x'. x'  S) xs'" and "xs'  paths (substitute f T t)"
    by (auto simp add: filter_paths_conv_free_restr[symmetric])
  from this(2) assms
  have "filter (λ x'. x'  S) xs'  paths (substitute f T (ttree_restr S t))"
  proof (induction f T t xs' rule: substitute_induct)
  case Nil thus ?case by simp
  next
  case (Cons f T t x xs)
    from Cons.prems(1)
    have "possible t x" and "xs  paths (substitute (f_nxt f T x) T (nxt t x ⊗⊗ f x))" by auto
    note this(2)
    moreover
    from  Cons.prems(2)
    have " x'. carrier (f_nxt f T x x')  S" by (auto simp add: f_nxt_def)
    moreover
    from  Cons.prems(3)
    have "const_on (f_nxt f T x) (-S) empty" by (force simp add: f_nxt_def)
    ultimately
    have "[x'xs . x'  S]  paths (substitute (f_nxt f T x) T (ttree_restr S (nxt t x ⊗⊗ f x)))" by (rule Cons.IH)
    hence *: "[x'xs . x'  S]  paths (substitute (f_nxt f T x) T (ttree_restr S (nxt t x ⊗⊗ f x)))" by (simp add: ttree_restr_both)
    show ?case
    proof (cases "x  S")
      case True
      show ?thesis
        using possible t x Cons.prems(3) * True
        by (auto simp add: ttree_restr_both ttree_restr_noop[OF Cons.prems(2)] intro: ttree_restr_possible
                    dest: subsetD[OF substitute_mono2[OF both_mono1[OF ttree_restr_nxt_subset]]])
    next
      case False
      with const_on f (- S) TTree.empty have [simp]: "f x = empty" by auto
      hence [simp]: "f_nxt f T x = f" by (auto simp add: f_nxt_def)
      show ?thesis
      using * False
      by (auto dest:  subsetD[OF substitute_mono2[OF ttree_restr_nxt_subset2]])
    qed
  qed
  thus "xs  paths (substitute f T (ttree_restr S t))" by simp
next
  fix xs
  assume "xs  paths (substitute f T (ttree_restr S t))"
  then obtain xs' where "xs'  paths t" and "substitute'' f T (filter (λ x'. x'S) xs') xs "
    unfolding substitute_substitute''
    by (auto simp add: filter_paths_conv_free_restr[symmetric])

  from this(2) assms
  have " xs''. xs = filter (λ x'. x'S) xs''  substitute'' f T xs' xs''"
  proof(induction "(xs',xs)" arbitrary: f xs' xs rule: measure_induct_rule[where f = "λ (xs,ys). length (filter (λ x'. x'  S) xs) + length ys"])
  case (less xs ys)
    note substitute'' f T [x'xs . x'  S] ys

    show ?case
    proof(cases xs)
    case Nil with less.prems have "ys = []" by auto
      thus ?thesis using Nil by (auto,  metis filter.simps(1) substitute''_Nil)
    next
    case (Cons x xs')
      show ?thesis
      proof (cases "x  S")
      case True with Cons less.prems
        have "substitute'' f T (x# [x'xs' . x'  S]) ys" by simp
        from substitute''_ConsE[OF this]
        obtain zs xs'' ys' where "ys = x # ys'" and "zs  paths (f x)" and "xs''  interleave [x'xs' . x'  S] zs" and "substitute'' (f_nxt f T x) T xs'' ys'".
        from zs  paths (f x)  less.prems(2)
        have "set zs  S" by (auto simp add: Union_paths_carrier[symmetric])
        hence [simp]: "[x'zs . x'  S] = zs" "[x'zs . x'  S] = []" 
            by (metis UnCI Un_subset_iff eq_iff filter_True,
               metis set zs  S filter_False insert_absorb insert_subset)
        
        from xs''  interleave [x'xs' . x'  S] zs
        have "xs''  interleave [x'xs' . x'  S] [x'zs . x'  S]" by simp
        then obtain xs''' where "xs'' = [x'xs''' . x'  S]" and "xs'''  interleave xs' zs" by (rule interleave_filter)

        from xs'''  interleave xs' zs
        have l: " P. length (filter P xs''') = length (filter P xs') + length (filter P zs)"
          by (induction) auto
        
        from substitute'' (f_nxt f T x) T xs'' ys' xs'' = _
        have "substitute'' (f_nxt f T x) T [x'xs''' . x'  S] ys'" by simp
        moreover
        from less.prems(2)
        have "xa. carrier (f_nxt f T x xa)  S"
          by (auto simp add: f_nxt_def)
        moreover
        from less.prems(3)
        have "const_on (f_nxt f T x) (- S) TTree.empty" by (force simp add: f_nxt_def)
        ultimately
        have "ys''. ys' = [x'ys'' . x'  S]  substitute'' (f_nxt f T x) T xs''' ys''"
            by (rule less.hyps[rotated])
               (auto simp add: ys = _ xs =_ x  S xs'' = _[symmetric] l)[1]
        then obtain ys'' where "ys' = [x'ys'' . x'  S]" and "substitute'' (f_nxt f T x) T xs''' ys''" by blast
        hence "ys = [x'x#ys'' . x'  S]" using x  S ys = _ by simp
        moreover
        from zs  paths (f x) xs'''  interleave xs' zs substitute'' (f_nxt f T x) T xs''' ys''
        have "substitute'' f T (x#xs') (x#ys'')"
          by rule
        ultimately
        show ?thesis unfolding Cons by blast
      next
      case False with Cons less.prems
        have "substitute'' f T ([x'xs' . x'  S]) ys" by simp
        hence "ys'. ys = [x'ys' . x'  S]  substitute'' f T xs' ys'"
            by (rule less.hyps[OF _ _ less.prems(2,3), rotated]) (auto simp add:  xs =_ x   S)
        then obtain ys' where "ys = [x'ys' . x'  S]" and "substitute'' f T xs' ys'" by auto
        
        from this(1)
        have "ys = [x'x#ys' . x'  S]" using x  S ys = _ by simp
        moreover
        have [simp]: "f x = empty" using x  S less.prems(3) by force
        hence "f_nxt f T x = f" by (auto simp add: f_nxt_def)
        with substitute'' f T xs' ys'
        have "substitute'' f T (x#xs') (x#ys')"
          by (auto intro: substitute''.intros)
        ultimately
        show ?thesis unfolding Cons by blast
      qed
    qed
  qed
  then obtain xs'' where "xs = filter (λ x'. x'S) xs''" and "substitute'' f T xs' xs''" by auto
  from this(2) xs'  paths t
  have "xs''  paths (substitute f T t)" by (auto simp add: substitute_substitute'')
  with xs = _
  show "xs  paths (ttree_restr S (substitute f T t))"
    by (auto simp add:  filter_paths_conv_free_restr[symmetric])
qed

end