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
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 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 *: "(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