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: "(⋃x∈paths 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