section ‹Lifting root steps to single/parallel root/non-root steps›
theory Lift_Root_Step
imports Basic_Utils
FOR_Certificate
Ground_Terms
TRS.Trs
TRS.Multihole_Context
begin
lemma funas_gterm_of_mctxt_to_funas_mctxt [simp]:
assumes "num_holes C = 0" and "ground_mctxt C"
shows "funas_gterm (gterm_of_term (term_of_mctxt C)) = funas_mctxt C"
using assms unfolding funas_gterm_def by (induct C) auto
lemma funas_gterm_of_mctxt_to_funas_mctxtI [intro]:
assumes "num_holes C = 0" and "ground_mctxt C" and "funas_mctxt C ⊆ ℱ"
shows "funas_gterm (gterm_of_term (term_of_mctxt C)) ⊆ ℱ"
using assms by auto
subsection ‹Rewrite steps›
definition grrstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
"grrstep ℛ = inv_image (rrstep ℛ) term_of_gterm"
definition gnrrstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
"gnrrstep ℛ = inv_image (nrrstep ℛ) term_of_gterm"
definition grstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
"grstep ℛ = inv_image (rstep ℛ) term_of_gterm"
definition gpar_rstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
"gpar_rstep ℛ = inv_image (par_rstep ℛ) term_of_gterm"
subsection ‹Lifting root steps to single/parallel root/non-root steps ($R^{W,X}$)›
text ‹We construct parallel steps, keeping track of whether they are root steps, empty steps, and/or single steps.›
datatype 'f annotated_parallel_step =
aps (aps_step: "'f gterm × 'f gterm") (aps_root: bool) (aps_empty: bool) (aps_single: bool)
inductive_set annotated_parallel_closure ::
"('f × nat) set ⇒ 'f gterm rel ⇒ 'f annotated_parallel_step set" for ℱ R where
aps_root_step: "p ∈ R ⟹
aps p True ― ‹root› False ― ‹¬empty› True ― ‹single› ∈ annotated_parallel_closure ℱ R"
| aps_non_root_step: "(f, n) ∈ ℱ ⟹ length ps = n ⟹
(∀i < length ps. ps ! i ∈ annotated_parallel_closure ℱ R) ⟹
aps (GFun f (map (fst ∘ aps_step) ps), GFun f (map (snd ∘ aps_step) ps))
False ― ‹¬root›
(∀i < length ps. aps_empty (ps ! i)) ― ‹the step is empty if all substeps are empty›
(∃i < length ps. aps_single (ps ! i) ∧ (∀j < length ps. i ≠ j ⟶ aps_empty (ps ! j)))
― ‹it's a single step if one substep is a single step and the rest are empty›
∈ annotated_parallel_closure ℱ R"
definition lift_root_step :: "('f × nat) set ⇒ pos_step ⇒ ext_step ⇒ 'f gterm rel ⇒ 'f gterm rel" where
"lift_root_step ℱ W X R = {aps_step a |a.
a ∈ annotated_parallel_closure ℱ R ∧
(case W of PRoot ⇒ aps_root a ∨ aps_empty a | PNonRoot ⇒ ¬ aps_root a | PAny ⇒ True) ∧
(case X of ESingle ⇒ aps_single a | EParallel ⇒ True | EStrictParallel ⇒ ¬ aps_empty a)
}"
subsection ‹Validation›
lemmas in_inv_image' = in_inv_image[of "fst x" "snd x" for x, unfolded prod.collapse]
text ‹annotated parallel steps are parallel steps›
lemma aps_parallel:
assumes "a ∈ annotated_parallel_closure ℱ (grrstep ℛ)"
shows "aps_step a ∈ gpar_rstep ℛ"
using assms
by induct (auto simp: in_inv_image' gpar_rstep_def grrstep_def rrstep_imp_rstep[THEN rstep_par_rstep[THEN subsetD]])
text ‹@{const aps_empty} implies an empty step (approximated by identity)›
lemma aps_empty':
assumes "a ∈ annotated_parallel_closure ℱ R" "aps_empty a"
shows "aps_step a ∈ Restr Id {t. funas_gterm t ⊆ ℱ}"
using assms unfolding Id_fstsnd_eq Int_iff mem_Times_iff
by induct (auto simp: in_set_conv_nth funas_gterm_def dest!: subsetD)
lemma aps_empty:
assumes "a ∈ annotated_parallel_closure ℱ R" "aps_empty a"
shows "aps_step a ∈ Id"
using aps_empty'[OF assms] by blast
lemma aps_empty_flags:
assumes "a ∈ annotated_parallel_closure ℱ R" "aps_empty a"
shows "¬ aps_root a" "¬ aps_single a"
using assms unfolding Id_fstsnd_eq Int_iff mem_Times_iff
by induct (auto simp: in_set_conv_nth funas_gterm_def dest!: subsetD)
text ‹@{const aps_root} implies a root step›
lemma aps_root:
assumes "a ∈ annotated_parallel_closure ℱ R" "aps_root a"
shows "aps_step a ∈ R"
using assms by cases auto
text ‹@{const aps_single} implies a single step›
lemma aps_single:
assumes "a ∈ annotated_parallel_closure ℱ (grrstep ℛ)" "aps_single a"
shows "aps_step a ∈ grstep ℛ"
using assms
proof (induct)
case (aps_non_root_step f n ps)
obtain i where i: "i < length ps" "aps_single (ps ! i)" "⋀j. j < length ps ⟹ j ≠ i ⟹ aps_empty (ps ! j)"
using aps_non_root_step(2,4) by auto
have "⋀j. j < length ps ⟹ j ≠ i ⟹ fst (aps_step (ps ! j)) = snd (aps_step (ps ! j))"
using i aps_non_root_step(3) by (auto dest!: aps_empty)
then have *: "map (term_of_gterm ∘ (snd ∘ aps_step)) ps = (map (term_of_gterm ∘ (fst ∘ aps_step)) ps)[i := term_of_gterm (snd (aps_step (ps ! i)))]"
using i(1) by (auto intro!: nth_equalityI simp: nth_list_update)
have "aps_step (ps ! i) ∈ grstep ℛ" using i(1,2) aps_non_root_step(3) by blast
then show ?case using i(1)
apply (simp add: grstep_def * upd_conv_take_nth_drop)
apply (subst (1) id_take_nth_drop[of i], simp)
by (rule ctxt_closed_one) (auto simp: in_inv_image')
qed (auto simp: grrstep_def grstep_def rrstep_imp_rstep)
text ‹annotated parallel steps respect the given signature ℱ›
lemma aps_sig':
assumes "a ∈ annotated_parallel_closure ℱ R" "R ⊆ {t. funas_gterm t ⊆ 𝒢} × {t. funas_gterm t ⊆ ℋ}" "ℱ ⊆ 𝒢" "ℱ ⊆ ℋ"
shows "aps_step a ∈ {t. funas_gterm t ⊆ 𝒢} × {t. funas_gterm t ⊆ ℋ}"
using assms by induct (auto 0 3 simp: funas_gterm_def in_set_conv_nth mem_Times_iff)
lemma lift_root_step_sig':
assumes "R ⊆ {t. funas_gterm t ⊆ 𝒢} × {t. funas_gterm t ⊆ ℋ}" "ℱ ⊆ 𝒢" "ℱ ⊆ ℋ"
shows "lift_root_step ℱ W X R ⊆ {t. funas_gterm t ⊆ 𝒢} × {t. funas_gterm t ⊆ ℋ}"
by (fastforce simp: lift_root_step_def dest: aps_sig'[OF _ assms])
lemmas aps_sig = aps_sig'[OF _ _ subset_refl subset_refl]
lemmas lift_root_step_sig = lift_root_step_sig'[OF _ subset_refl subset_refl]
text ‹any parallel step over ℱ is in the annotated parallel closure›
lemma gterm_rel_ground_trs:
"ground_trs (map_both (term_of_gterm :: 'f gterm ⇒ ('f, 'v) term) ` ℛ)"
using ground_trs_def by fastforce
lemma parallel_aps:
fixes ℛ :: "('f, 'v) trs"
assumes "(t, u) ∈ inv_image (sig_step ℱ (par_rstep ℛ)) term_of_gterm"
defines "t' ≡ term_of_gterm t :: ('f, 'v) term" and "u' ≡ term_of_gterm u :: ('f, 'v) term"
shows "∃r e s. aps (t, u) r e s ∈ annotated_parallel_closure ℱ (grrstep ℛ)"
using assms(1)[unfolded in_inv_image, folded u'_def t'_def]
apply (elim sig_stepE)
apply (insert assms(2-))
proof (induct arbitrary: t u rule: par_rstep.induct)
case (root_step t' u' σ)
then have "(t, u) ∈ grrstep ℛ" by (auto simp: grrstep_def intro: rrstepI[where σ = σ])
then show ?case by (auto intro: aps_root_step)
next
case (par_step_fun us' ts' f)
obtain ts us where [simp]: "t = GFun f ts" "u = GFun f us" using par_step_fun(6,7)
by (cases t, cases u) (simp only: term_of_gterm.simps term.simps)
have "∃e r s. aps (ts ! i, us ! i) e r s ∈ annotated_parallel_closure ℱ (grrstep ℛ)" if "i < length ts" for i
apply (rule par_step_fun(2)[of i "ts ! i" "us ! i" for i])
using that par_step_fun(3-)
apply auto
apply fastforce
by (meson SUP_le_iff nth_mem subsetCE)
then obtain rs es ss where
"⋀i. i < length ts ⟹ aps (ts ! i, us ! i) (rs i) (es i) (ss i) ∈ annotated_parallel_closure ℱ (grrstep ℛ)"
by metis
moreover have "length us = length ts" "(f, length ts) ∈ ℱ"
using par_step_fun(3-) by auto
ultimately show ?case using map_nth[of ts] map_nth[of us]
aps_non_root_step[of f "length ts" ℱ "map (λi. aps (ts ! i, us ! i) (rs i) (es i) (ss i)) [0..<length ts]" "grrstep ℛ"]
by (auto simp: comp_def cong: map_cong)
next
case (par_step_var x) then show ?case by (cases t) simp
qed
text ‹any root step is in the annotated parallel closure›
lemma root_aps:
assumes "(t, u) ∈ R"
shows "aps (t, u) True False True ∈ annotated_parallel_closure ℱ R"
using assms by (auto intro: aps_root_step)
text ‹any empty step over ℱ is in the annotated parallel closure›
lemma empty_aps:
assumes "funas_gterm t ⊆ ℱ"
shows "aps (t, t) False True False ∈ annotated_parallel_closure ℱ R"
using assms
proof (induct t)
case (GFun f ts)
have"(f, length ts) ∈ ℱ" using GFun(2) by (auto simp: funas_gterm_def)
moreover have "funas_gterm (ts ! i) ⊆ ℱ" if "i < length ts" for i
using GFun(2) that by (fastforce simp: funas_gterm_def)
ultimately show ?case using GFun(1)[OF nth_mem]
using aps_non_root_step[of f "length ts" ℱ "map (λi. aps (ts ! i, ts ! i) False True False) [0..<length ts]" R]
by (auto simp: comp_def map_nth cong: conj_cong imp_cong)
qed
text ‹any single step over ℱ is in the annotated parallel closure›
lemma helper:
assumes "aps (t, u) r s e ∈ annotated_parallel_closure ℱ ℛ"
and "(f, n) ∈ ℱ" and "⋃(set (map funas_gterm bef)) ⊆ ℱ"
and "⋃(set (map funas_gterm aft)) ⊆ ℱ" and "length (bef @ t # aft) = n"
shows "aps (GFun f (bef @ t # aft), GFun f (bef @ u # aft)) False s e ∈ annotated_parallel_closure ℱ ℛ"
proof -
let ?ts = "bef @ t # aft"
let ?us = "bef @ u # aft"
let ?ps = "map (λi. aps (bef ! i, bef ! i) False True False) [0..<length bef] @
aps (t, u) r s e # map (λi. aps (aft ! i, aft ! i) False True False) [0..<length aft]"
have bef: "⋀i. i < length bef ⟹ aps (bef ! i, bef ! i) False True False ∈ annotated_parallel_closure ℱ ℛ"
and aft: "⋀i. i < length aft ⟹ aps (aft ! i, aft ! i) False True False ∈ annotated_parallel_closure ℱ ℛ"
using assms(3, 4) by (simp add: empty_aps Sup_le_iff)+
{fix i
assume l: "i < length ?ps"
then have "?ps ! i ∈ annotated_parallel_closure ℱ ℛ"
using bef aft assms(1) nth_mem[OF l] by auto}
then have sub:"∀ i < length ?ps. ?ps ! i ∈ annotated_parallel_closure ℱ ℛ" by auto
have s:"(∀ i < length ?ps. aps_empty (?ps ! i)) = s"
by (auto simp add: nth_append_Cons nth_Cons')
have e: "(∃i < length ?ps. aps_single (?ps ! i) ∧ (∀j < length ?ps. i ≠ j ⟶ aps_empty (?ps ! j))) = e"
by (auto simp add: nth_append_Cons nth_Cons')
have r: "GFun f (map (fst ∘ aps_step) ?ps) = GFun f ?ts" "GFun f (map (snd ∘ aps_step) ?ps) = GFun f ?us"
by (auto simp add: map_nth_eq_conv)+
from aps_non_root_step[OF assms(2) _ sub]
show ?thesis using assms(5) unfolding r s e by (auto simp add: map_nth_eq_conv)
qed
lemma single_aps:
fixes ℛ :: "('f, 'v) trs"
assumes "(t, u) ∈ Restr (grstep ℛ) {t. funas_gterm t ⊆ ℱ}"
defines "t' ≡ term_of_gterm t :: ('f, 'v) term" and "u' ≡ term_of_gterm u :: ('f, 'v) term"
shows "∃r. aps (t, u) r False True ∈ annotated_parallel_closure ℱ (Restr (grrstep ℛ) {t. funas_gterm t ⊆ ℱ})"
proof -
from assms(1) have r: "(t, u) ∈ inv_image (sig_step ℱ (rstep ℛ)) term_of_gterm"
unfolding in_inv_image by (auto simp add: grstep_def funas_term_of_gterm_conv sig_stepI)
from r[unfolded in_inv_image, folded u'_def t'_def]
show ?thesis
apply (elim sig_stepE)
apply (insert assms(2-))
proof (induction arbitrary: t u rule: rstep.induct)
case (rstep C σ l r)
then show ?case
proof (induction C arbitrary: t u)
case Hole
then have "(t, u) ∈ (Restr (grrstep ℛ) {t. funas_gterm t ⊆ ℱ})"
unfolding grrstep_def rrstep_def' by auto (metis contra_subsetD funas_term_of_gterm_conv)+
from aps_root_step[OF this] show ?case by auto
next
case (More f bef C aft)
have "ground (term_of_gterm t)" "ground (term_of_gterm u)" using More(3, 4) by auto
then have gr: "∀ x ∈ set bef. ground x" "∀ x ∈ set aft. ground x" using More(3, 4)
by (metis (full_types) ground_ctxt.simps(2) ground_ctxt_apply)+
obtain gBef gAft where bef: "gBef = map gterm_of_term bef" and
aft: "gAft = map gterm_of_term aft" using More(3, 4) by auto
obtain t' u' where t': "t' = gterm_of_term C⟨l ⋅ σ⟩" and u': "u' = gterm_of_term C⟨r ⋅ σ⟩"
using More(3, 4) by auto
have [simp]: "t = GFun f (gBef @ t' # gAft) " "u = GFun f (gBef @ u' # gAft)"
using More(3, 4) bef aft t' u'
by auto (metis (full_types) gterm_of_term.simps list.simps(9) map_append term_of_gterm_inv)+
let ?ts = "(gBef @ t' # gAft)"
let ?us = "(gBef @ u' # gAft)"
have f: "(f, length ?ts) ∈ ℱ" using More(5) by auto
have funas: "funas_term (term_of_gterm t') ⊆ ℱ" "funas_term (term_of_gterm u') ⊆ ℱ"using More(5, 6)
by auto (metis contra_subsetD funas_term_of_gterm_conv)+
have fBef: "⋃ (set (map funas_gterm gBef)) ⊆ ℱ"
using gr bef More(3, 5) by auto (metis SUP_le_iff funas_gterm_gterm_of_term subsetD)
have fAft: "⋃ (set (map funas_gterm gAft)) ⊆ ℱ"
using gr aft More(4, 6) by auto (metis SUP_le_iff funas_gterm_gterm_of_term subsetD)
from More(1)[OF More(2), of t' u'] have "∃r. aps (t', u') r False True ∈ annotated_parallel_closure ℱ (Restr (grrstep ℛ) {t. funas_gterm t ⊆ ℱ})"
using More(3 - 6) funas by (auto simp add: t' u' bef)
then obtain r where "aps (t', u') r False True ∈ annotated_parallel_closure ℱ (Restr (grrstep ℛ) {t. funas_gterm t ⊆ ℱ})" by blast
from helper[OF this f fBef fAft] show ?case by auto
qed
qed
qed
text ‹incrementality and monotonicity of @{const annotated_parallel_closure} and @{const lift_root_step}›
lemma aps_incr:
assumes "R ⊆ S"
shows "annotated_parallel_closure ℱ R ⊆ annotated_parallel_closure ℱ S"
proof (rule)
fix x
assume "x ∈ annotated_parallel_closure ℱ R"
then show "x ∈ annotated_parallel_closure ℱ S" using assms
by (induct) (auto simp add: aps_root_step aps_non_root_step subsetD)
qed
lemma lift_root_step_incr:
assumes "R ⊆ S"
shows "lift_root_step ℱ W X R ⊆ lift_root_step ℱ W X S"
using aps_incr[OF assms] by (auto simp: lift_root_step_def)
lemma aps_mono:
assumes "ℱ ⊆ 𝒢"
shows "annotated_parallel_closure ℱ R ⊆ annotated_parallel_closure 𝒢 R"
proof (intro subsetI, goal_cases LR)
case (LR x)
then show ?case apply (induct rule: annotated_parallel_closure.induct)
by (auto intro!: aps_root_step aps_non_root_step simp: assms[THEN subsetD])
qed
lemma lift_root_step_mono:
assumes "ℱ ⊆ 𝒢"
shows "lift_root_step ℱ W X R ⊆ lift_root_step 𝒢 W X R"
using aps_mono[OF assms] by (auto simp: lift_root_step_def)
lemma grstep_lift_root_step:
"lift_root_step ℱ PAny ESingle (Restr (grrstep ℛ) {t. funas_gterm t ⊆ ℱ}) = Restr (grstep ℛ) {t. funas_gterm t ⊆ ℱ}"
proof (intro equalityI subrelI, goal_cases LR RL)
case (LR x y)
then obtain a where "a ∈ annotated_parallel_closure ℱ (Restr (grrstep ℛ) {t. funas_gterm t ⊆ ℱ})" and
step: "aps_step a = (x, y)" and sin: "aps_single a = True" and funas: "funas_gterm x ⊆ ℱ ∧ funas_gterm y ⊆ ℱ"
unfolding lift_root_step_def apply auto using aps_sig by fastforce
then have w: "a ∈ annotated_parallel_closure ℱ (grrstep ℛ)"
using aps_incr inf.cobounded1 by blast
then show ?case using aps_single[OF w] step sin funas by auto
next
case (RL x y)
from single_aps[OF RL] obtain a where "a ∈ annotated_parallel_closure ℱ (Restr (grrstep ℛ) {t. funas_gterm t ⊆ ℱ})" and
step: "aps_step a = (x, y)" and sin: "aps_single a = True" by auto
then show ?case unfolding lift_root_step_def by auto force
qed
lemma swap_annotated_parallel_step:
assumes "a ∈ annotated_parallel_closure ℱ (prod.swap ` R)"
shows "aps (prod.swap (aps_step a)) (aps_root a) (aps_empty a) (aps_single a) ∈ annotated_parallel_closure ℱ R"
using assms
proof (induct a rule: annotated_parallel_closure.induct)
case (aps_non_root_step f n ps)
then show ?case
using annotated_parallel_closure.aps_non_root_step[of f n ℱ "map (λa. aps (prod.swap (aps_step a)) (aps_root a) (aps_empty a) (aps_single a)) ps" R]
by simp (auto simp: comp_def cong: ex_cong)
qed (auto intro: annotated_parallel_closure.aps_root_step)
lemma swap_lift_root_step:
"lift_root_step ℱ W X (prod.swap ` R) = prod.swap ` lift_root_step ℱ W X R"
proof (intro equalityI subrelI, goal_cases LR RL)
case (LR x y)
then guess a unfolding lift_root_step_def by (elim CollectE exE conjE)
from swap_annotated_parallel_step[OF this(2)] this(1,3,4)
show ?case by (auto 0 0 simp: lift_root_step_def split: pos_step.splits ext_step.splits
intro!: exI[of _ "aps (prod.swap _) _ _ _"] image_eqI[of _ prod.swap, OF swap_swap[symmetric]])
next
case (RL x y)
then guess p a unfolding lift_root_step_def by (elim imageE CollectE exE conjE)
from this(2) this(3) this(1,4,5) swap_annotated_parallel_step[of a ℱ "prod.swap ` R"]
show ?case by (auto 0 0 simp: lift_root_step_def image_comp split: pos_step.splits ext_step.splits
intro!: exI[of _ "aps (prod.swap _) _ _ _"])
qed
lemma converse_lift_root_step:
"(lift_root_step ℱ W X R)¯ = lift_root_step ℱ W X (R¯)"
proof -
have [simp]: "X¯ = prod.swap ` X" for X by auto
show ?thesis using swap_lift_root_step[of ℱ W X R] by simp
qed
lemma aps_sig_transfer:
assumes "a ∈ annotated_parallel_closure ℱ R" "snd ` R ⊆ {t. funas_gterm t ⊆ 𝒢}" "funas_gterm (fst (aps_step a)) ⊆ 𝒢"
shows "a ∈ annotated_parallel_closure 𝒢 R"
using assms
by (induct) (auto intro: aps_root_step aps_non_root_step simp: funas_gterm_def UN_subset_iff)
lemma lift_root_step_sig_transfer:
assumes "p ∈ lift_root_step ℱ W X R" "snd ` R ⊆ {t. funas_gterm t ⊆ 𝒢}" "funas_gterm (fst p) ⊆ 𝒢"
shows "p ∈ lift_root_step 𝒢 W X R"
using assms by (auto 0 0 simp: lift_root_step_def dest!: aps_sig_transfer[of _ ℱ R 𝒢]) blast
lemma lift_root_steps_sig_transfer:
assumes "(s, t) ∈ (lift_root_step ℱ W X R)⇧+" "snd ` R ⊆ {t. funas_gterm t ⊆ 𝒢}" "funas_gterm s ⊆ 𝒢"
shows "(s, t) ∈ (lift_root_step 𝒢 W X R)⇧+"
using assms(1,3)
proof (induct rule: converse_trancl_induct)
case (base s)
show ?case using lift_root_step_sig_transfer[OF base(1) assms(2)] base(2) by (simp add: r_into_trancl)
next
case (step s s')
show ?case using lift_root_step_sig_transfer[OF step(1) assms(2)] step(3,4)
lift_root_step_sig'[of R UNIV 𝒢 𝒢 W X, THEN subsetD, of "(s, s')"] assms(2) by fastforce
qed
lemma lift_root_stepseq_sig_transfer:
assumes "(s, t) ∈ (lift_root_step ℱ W X R)⇧*" "snd ` R ⊆ {t. funas_gterm t ⊆ 𝒢}" "funas_gterm s ⊆ 𝒢"
shows "(s, t) ∈ (lift_root_step 𝒢 W X R)⇧*"
using assms by (auto simp flip: reflcl_trancl simp: lift_root_steps_sig_transfer)
lemmas lift_root_step_sig_transfer' = lift_root_step_sig_transfer[of "prod.swap p" ℱ W X "prod.swap ` R" 𝒢 for p ℱ W X 𝒢 R,
unfolded swap_lift_root_step, OF imageI, THEN imageI [of _ _ prod.swap],
unfolded image_comp comp_def fst_swap snd_swap swap_swap image_ident]
lemmas lift_root_steps_sig_transfer' = lift_root_steps_sig_transfer[of t s ℱ W X "prod.swap ` R" 𝒢 for t s ℱ W X 𝒢 R,
THEN imageI [of _ _ prod.swap], unfolded swap_lift_root_step swap_trancl pair_in_swap_image
image_comp comp_def snd_swap swap_swap swap_simp image_ident]
lemmas lift_root_stepseq_sig_transfer' = lift_root_stepseq_sig_transfer[of t s ℱ W X "prod.swap ` R" 𝒢 for t s ℱ W X 𝒢 R,
THEN imageI [of _ _ prod.swap], unfolded swap_lift_root_step swap_rtrancl pair_in_swap_image
image_comp comp_def snd_swap swap_swap swap_simp image_ident]
lemma lift_root_step_Parallel_conv:
shows "lift_root_step ℱ W EParallel R = lift_root_step ℱ W EStrictParallel R ∪ Restr Id {t. funas_gterm t ⊆ ℱ}"
using aps_empty'[of _ ℱ R] aps_sig[of _ ℱ R] empty_aps[of _ ℱ R]
by (cases W, auto simp: lift_root_step_def) (fastforce intro: exI[of _ "aps _ _ _ _"])+
lemma lift_meta_trancl:
assumes "(⋀s t. (s, t) ∈ A ⟹ (f s, f t) ∈ B)" "(s, t) ∈ A⇧+"
shows "(f s, f t) ∈ B⇧+"
using assms(2,1) by induct force+
lemma relax_pos_lift_root_step:
"lift_root_step ℱ W X R ⊆ lift_root_step ℱ PAny X R"
by (auto simp: lift_root_step_def)
lemma relax_pos_lift_root_steps:
"(lift_root_step ℱ W X R)⇧+ ⊆ (lift_root_step ℱ PAny X R)⇧+"
by (simp add: relax_pos_lift_root_step trancl_mono_set)
lemma relax_ext_lift_root_step:
"lift_root_step ℱ W X R ⊆ lift_root_step ℱ W EParallel R"
by (auto simp: lift_root_step_def)
lemma lift_lift_root_step_Single:
assumes "(f, Suc (length ts + length ts')) ∈ ℱ" "(s, t) ∈ lift_root_step ℱ PAny ESingle R"
"set ts ⊆ {t. funas_gterm t ⊆ ℱ}" "set ts' ⊆ {t. funas_gterm t ⊆ ℱ}"
shows "(GFun f (ts @ s # ts'), GFun f (ts @ t # ts')) ∈ lift_root_step ℱ PNonRoot ESingle R"
proof -
obtain a where a: "a ∈ annotated_parallel_closure ℱ R" "aps_step a = (s, t)" "aps_single a"
using assms(2) by (auto simp: lift_root_step_def)
show ?thesis using a assms(3)[THEN subsetD, OF nth_mem] assms(4)[THEN subsetD, OF nth_mem, of "_ - Suc (length ts)"]
unfolding lift_root_step_def
apply (intro CollectI exI)
by (rule conjI[OF _ conjI[OF aps_non_root_step[OF assms(1), of "map (λt. aps (t, t) False True False) ts @ a # map (λt. aps (t, t) False True False) ts'" R]]])
(auto simp: nth_append_Cons empty_aps set_conv_nth comp_def not_less dest!: le_neq_implies_less)
qed
lemma lift_lift_root_steps_Single:
assumes "(f, Suc (length ts + length ts')) ∈ ℱ" "(s, t) ∈ (lift_root_step ℱ PAny ESingle R)⇧+"
"set ts ⊆ {t. funas_gterm t ⊆ ℱ}" "set ts' ⊆ {t. funas_gterm t ⊆ ℱ}"
shows "(GFun f (ts @ s # ts'), GFun f (ts @ t # ts')) ∈ (lift_root_step ℱ PNonRoot ESingle R)⇧+"
by (rule lift_meta_trancl[OF lift_lift_root_step_Single[OF assms(1) _ assms(3,4)] assms(2)])
lemma lift_root_step_StrictParallel_seq:
assumes "R ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
shows "lift_root_step ℱ PAny EStrictParallel R ⊆ (lift_root_step ℱ PAny ESingle R)⇧+"
proof -
have "aps_step a ∈ (lift_root_step ℱ PAny ESingle R)⇧+" if "a ∈ annotated_parallel_closure ℱ R" "¬ aps_empty a" for a
using that
proof (induct a)
case r: (aps_root_step p)
then show ?case using aps_root_step[of p R ℱ] by (cases p; force simp: lift_root_step_def)
next
case n: (aps_non_root_step f n ps)
have sig: "set (map (fst ∘ aps_step) ps) ⊆ {t. funas_gterm t ⊆ ℱ}"
"set (map (snd ∘ aps_step) ps) ⊆ {t. funas_gterm t ⊆ ℱ}"
using n(3)[rule_format, THEN conjunct1, THEN aps_sig, OF _ assms] by (fastforce simp: set_conv_nth)+
obtain i where i: "i < length ps" "¬ aps_empty (ps ! i)" using n(4) by auto
define tj where "⋀i. tj i = GFun f (take i (map (snd ∘ aps_step) ps) @ drop i (map (fst ∘ aps_step) ps))"
have "(tj 0, tj j) ∈ (lift_root_step ℱ PAny ESingle R)⇧+ ∨ j ≤ i ∧ tj 0 = tj j" if "j ≤ length ps" for j
using that
proof (induct j)
case (Suc j)
moreover have "0 < length ps" using Suc by linarith
then have "(tj j, tj (Suc j)) ∈ (lift_root_step ℱ PAny ESingle R)⇧+ ∨ i ≠ j ∧ tj j = tj (Suc j)"
using Suc(2) n(1) i(2) aps_empty[OF n(3)[rule_format, THEN conjunct1, rule_format, of j]]
using lift_lift_root_steps_Single[of _ _ _ _ "fst p" "snd p" for p, unfolded prod.collapse,
OF _ n(3)[rule_format, THEN conjunct2, rule_format, of j], of f "take j (map (snd ∘ aps_step) ps)"
"drop (Suc j) (map (fst ∘ aps_step) ps)", THEN relax_pos_lift_root_steps[THEN subsetD]]
unfolding tj_def
apply (subst (1 3) Cons_nth_drop_Suc[symmetric], (simp_all)[2])
by (force simp: tj_def take_Suc_conv_app_nth Suc_le_eq min_def
subset_trans[OF set_take_subset sig(2)] subset_trans[OF set_drop_subset sig(1)]
simp flip: n(2))
ultimately show ?case by (auto intro: trancl_trans)
qed simp
from this[of "length ps"] i(1) show ?case by (simp add: tj_def)
qed
then show ?thesis by (auto simp: lift_root_step_def)
qed
lemma lift_root_step_Parallel_seq:
assumes "R ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
shows "lift_root_step ℱ PAny EParallel R ⊆ (lift_root_step ℱ PAny ESingle R)⇧+ ∪ Restr Id {t. funas_gterm t ⊆ ℱ}"
unfolding lift_root_step_Parallel_conv using lift_root_step_StrictParallel_seq[OF assms] by blast
lemma lift_root_step_Single_to_Parallel:
shows "lift_root_step ℱ PAny ESingle R ⊆ lift_root_step ℱ PAny EParallel R"
by (auto simp: lift_root_step_def)
lemma trancl_partial_reflcl:
"(X ∪ Restr Id Y)⇧+ = X⇧+ ∪ Restr Id Y"
proof (intro equalityI subrelI, goal_cases LR RL)
case (LR a b) then show ?case by (induct) (auto dest: trancl_into_trancl)
qed (auto intro: trancl_mono)
lemma lift_root_step_Parallels_single:
assumes "R ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
shows "(lift_root_step ℱ PAny EParallel R)⇧+ = (lift_root_step ℱ PAny ESingle R)⇧+ ∪ Restr Id {t. funas_gterm t ⊆ ℱ}"
using trancl_mono_set[OF lift_root_step_Parallel_seq[OF assms]]
using trancl_mono_set[OF lift_root_step_Single_to_Parallel, of ℱ R]
by (auto simp: lift_root_step_Parallel_conv trancl_partial_reflcl)
lemma lift_root_step_Root_Single [simp]:
"lift_root_step ℱ PRoot ESingle R = R"
using aps_root by (auto simp: lift_root_step_def aps_empty_flags intro!: exI root_aps)
lemma lift_root_Any_Single_eq:
shows "lift_root_step ℱ PAny ESingle R = R ∪ lift_root_step ℱ PNonRoot ESingle R"
by (auto simp add: lift_root_step_def aps_root) (metis aps_root_step annotated_parallel_step.sel(1, 4))
lemma lift_root_Root_EStrict [simp]:
shows "lift_root_step ℱ PRoot EStrictParallel R = R"
by (auto simp add: lift_root_step_def aps_root) (metis aps_root_step annotated_parallel_step.sel(1 - 3))
lemma lift_root_Any_EStrict_eq [simp]:
shows "lift_root_step ℱ PAny EStrictParallel R = R ∪ lift_root_step ℱ PNonRoot EStrictParallel R"
by (auto simp add: lift_root_step_def aps_root) (metis aps_root_step annotated_parallel_step.sel(1, 3))
lemma lift_root_Root_EParallel [simp]:
shows "lift_root_step ℱ PRoot EParallel R = R ∪ Restr Id {t. funas_gterm t ⊆ ℱ}"
unfolding lift_root_step_Parallel_conv by auto
section ‹GTT composition definition and characteristic property.›
definition gcomp_rel :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel ⇒ 'f gterm rel" where
"gcomp_rel ℱ R S = (R O lift_root_step ℱ PAny EParallel S) ∪ (lift_root_step ℱ PAny EParallel R O S)"
lemma gcomp_rel:
"lift_root_step ℱ PAny EParallel (gcomp_rel ℱ R S) = lift_root_step ℱ PAny EParallel R O lift_root_step ℱ PAny EParallel S"
proof -
let ?lift = "lift_root_step ℱ PAny EParallel"
{ fix s u assume "(s, u) ∈ ?lift (gcomp_rel ℱ R S)"
then obtain a where "a ∈ annotated_parallel_closure ℱ (gcomp_rel ℱ R S)" "(s, u) = aps_step a"
by (auto simp: lift_root_step_def)
then have "∃b c t. b ∈ annotated_parallel_closure ℱ R ∧ c ∈ annotated_parallel_closure ℱ S ∧
aps_step b = (s, t) ∧ aps_step c = (t, u)"
proof (induct arbitrary: s u rule: annotated_parallel_closure.induct)
case r: (aps_root_step a) then show ?case
by (force simp: gcomp_rel_def lift_root_step_def dest!: aps_root_step[of _ R ℱ] aps_root_step[of _ S ℱ])
next
case n: (aps_non_root_step f n as)
obtain bs cs ts where [simp]:
"bs i ∈ annotated_parallel_closure ℱ R" "cs i ∈ annotated_parallel_closure ℱ S"
"aps_step (bs i) = (fst (aps_step (as ! i)), ts i)"
"aps_step (cs i) = (ts i, snd (aps_step (as ! i)))" if "i < length as" for i
using n(3)[rule_format, THEN conjunct2, rule_format, OF _ prod.collapse] by metis
show ?case using n(4)
by (auto simp: n(2)[symmetric] Bex_def[symmetric] comp_def intro!: nth_equalityI
aps_non_root_step[OF n(1), of "map bs [0..<n]" R, THEN rev_bexI]
aps_non_root_step[OF n(1), of "map cs [0..<n]" S, THEN rev_bexI])
qed
then have "(s, u) ∈ ?lift R O ?lift S" by (force simp: lift_root_step_def) }
moreover
{ fix s t u assume "(s, t) ∈ ?lift R" "(t, u) ∈ ?lift S"
then obtain b c where "b ∈ annotated_parallel_closure ℱ R" "c ∈ annotated_parallel_closure ℱ S"
"aps_step b = (s, t)" "aps_step c = (t, u)" by (auto simp: lift_root_step_def)
then have "∃a ∈ annotated_parallel_closure ℱ (gcomp_rel ℱ R S). aps_step a = (s, u)"
proof (induct b arbitrary: c s t u rule: annotated_parallel_closure.induct)
case r: (aps_root_step p)
then show ?case
by (force intro!: bexI[OF _ aps_root_step] simp: gcomp_rel_def lift_root_step_def relcomp.simps)
next
case n: (aps_non_root_step f n ps)
show ?case using n(4)
proof (induct rule: annotated_parallel_closure.cases)
case r: (aps_root_step p)
obtain b where "aps_step b = (s, t)" "b ∈ annotated_parallel_closure ℱ R"
using aps_non_root_step[OF n(1,2), of R] n(3,5) by blast
then show ?case using r n(6)
by (force intro!: bexI[OF _ aps_root_step] simp: gcomp_rel_def lift_root_step_def relcomp.simps)
next
case m: (aps_non_root_step g m qs)
have "∃a ∈ annotated_parallel_closure ℱ (gcomp_rel ℱ R S).
aps_step a = (fst (aps_step (ps ! i)), snd (aps_step (qs ! i)))" if "i < n" for i
using n(3)[rule_format, THEN conjunct2, rule_format, OF _ m(4)[rule_format] _ prod.collapse[symmetric],
of i i "fst (aps_step (ps ! i))"] that n(2,5,6) m(1) by (auto simp: map_eq_conv')
then obtain as where "as i ∈ annotated_parallel_closure ℱ (gcomp_rel ℱ R S)"
"aps_step (as i) = (fst (aps_step (ps ! i)), snd (aps_step (qs ! i)))" if "i < n" for i by metis
then show ?case using n(2,5,6) m(1)
by (intro bexI[OF _ aps_non_root_step[OF n(1), of "map as [0..<n]"]]) (auto simp: map_eq_conv')
qed
qed
then have "(s, u) ∈ ?lift (gcomp_rel ℱ R S)" by (force simp: lift_root_step_def) }
ultimately show ?thesis by auto
qed
section ‹GTT transitive closure definition›
definition gtrancl_rel :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel" where
"gtrancl_rel ℱ R = (lift_root_step ℱ PAny ESingle R)⇧* O R O (lift_root_step ℱ PAny ESingle R)⇧*"
lemma aps_empty_term:
assumes "a ∈ annotated_parallel_closure ℱ ℛ" and "aps_empty a"
obtains s where "aps_step a = (s, s)" "funas_gterm s ⊆ ℱ"
using aps_empty'[OF assms] aps_empty[OF assms]
by auto
section ‹Lift Root Step definitions relation to context/multihole context closure›
lemma lift_PNon_Single_to_ctxt:
assumes "(s, t) ∈ lift_root_step ℱ PNonRoot ESingle R"
shows "∃ u v C. gterm_of_term C⟨u⟩ = s ∧ gterm_of_term C⟨v⟩ = t ∧
(gterm_of_term u, gterm_of_term v) ∈ R ∧ funas_ctxt C ⊆ ℱ"
proof -
obtain a where a: "a ∈ annotated_parallel_closure ℱ R" "aps_step a = (s, t)" "aps_single a"
using assms by (auto simp: lift_root_step_def)
then show ?thesis
proof (induct arbitrary: s t)
case (aps_root_step p)
then show ?case by (auto intro!: exI[of _ "term_of_gterm s" for s] exI[of _ Hole])
next
case (aps_non_root_step f n ps) note IS = this
from IS(3 - 5) obtain i u v C where
aps: "ps ! i ∈ annotated_parallel_closure ℱ R" and l: "i < length ps" and
step: "aps_single (ps ! i) ∧ (∀j<length ps. i ≠ j ⟶ aps_empty (ps ! j))" and
wit: "gterm_of_term (C :: ('a, 'b) ctxt) ⟨u⟩ = fst (aps_step (ps ! i)) ∧ gterm_of_term C⟨v⟩ = snd (aps_step (ps ! i)) ∧
(gterm_of_term u, gterm_of_term v) ∈ R ∧ funas_ctxt C ⊆ ℱ"
by auto (metis prod.collapse)
have [simp]: "Suc (min (length ps) i + length ps - Suc i) = length ps"
"gterm_of_term ∘ term_of_gterm = id" using l by linarith auto
have "⋀ j. j < length ps ⟹ j ≠ i ⟹ fst (aps_step (ps ! j)) = snd (aps_step (ps ! j))" and
funas: "⋀ j. j < length ps ⟹ j ≠ i ⟹ funas_gterm (fst (aps_step (ps ! j))) ⊆ ℱ"
by (metis aps_empty_term aps_non_root_step.hyps(3) fst_conv step snd_conv)+
then have eq: "map (fst ∘ aps_step) (take i ps) = map (snd ∘ aps_step) (take i ps)"
"map (fst ∘ aps_step) (drop (Suc i) ps) = map (snd ∘ aps_step) (drop (Suc i) ps)"
by (auto simp add: in_set_conv_nth)
let ?ss = "map (fst ∘ aps_step) (take i ps)"
let ?ts = "map (fst ∘ aps_step) (drop (Suc i) ps)"
have "⋀ j. j < length ps ⟹ (?ss @ fst (aps_step (ps ! i)) # ?ts) ! j = fst (aps_step (ps ! j)) ∧
(?ss @ snd (aps_step (ps ! i)) # ?ts) ! j = snd (aps_step (ps ! j))" using eq l
by (metis (no_types, hide_lams) Cons_nth_drop_Suc append_take_drop_id comp_apply list.simps(9) map_append nth_map)
then have t: "gterm_of_term (More f (map term_of_gterm ?ss) C (map term_of_gterm ?ts))⟨u⟩ = s"
"gterm_of_term (More f (map term_of_gterm ?ss) C (map term_of_gterm ?ts))⟨v⟩ = t"
using wit term_of_gterm_inv IS(4) l
by (auto simp add: comp_assoc[symmetric] intro!: nth_equalityI)
have f: "funas_ctxt (More f (map term_of_gterm ?ss) C (map term_of_gterm ?ts)) ⊆ ℱ"
using funas conjunct2[OF conjunct2[OF conjunct2[OF wit]]] l IS(1, 2)
apply (auto simp add: funas_gterm_def in_set_conv_nth)
apply (metis dual_order.strict_trans funas_term_of_gterm_conv in_mono nat_neq_iff)
by (metis Suc_leI add_Suc funas_term_of_gterm_conv le_add_diff_inverse lessI nat_add_left_cancel_less not_add_less1 subsetD)
show ?case using t conjunct1[OF conjunct2[OF conjunct2[OF wit]]] f
by blast
qed
qed
lemma gctxt_to_lift_PNon_Single:
assumes "(gterm_of_term u, gterm_of_term v) ∈ R" and "C ≠ □"
and "gterm_of_term C⟨u⟩ = s" and "gterm_of_term C⟨v⟩ = t" and "ground_ctxt C" and "funas_ctxt C ⊆ ℱ"
shows "(s, t) ∈ lift_root_step ℱ PNonRoot ESingle R" using assms
proof (induction C arbitrary: u v s t)
case (More f ss C ts)
have f: "(f, Suc (length ss + length ts)) ∈ ℱ" "funas_ctxt C ⊆ ℱ" and cg: "ground_ctxt C"
using More(6, 7) by auto
let ?s = "gterm_of_term C⟨u⟩"
let ?t = "gterm_of_term C⟨v⟩"
let ?P = "λ l x i. x ∈ annotated_parallel_closure ℱ R ∧ aps_step x = (gterm_of_term (l ! i), gterm_of_term (l ! i)) ∧ aps_empty x"
{fix i assume l: "i < length ss"
then have f: "funas_gterm (gterm_of_term (ss ! i)) ⊆ ℱ" using More(6, 7)
by (auto simp add: funas_gterm_gterm_of_term[of "ss ! i"] dest!: subsetD)
from empty_aps[OF f] have "∃ x. ?P ss x i" using annotated_parallel_step.sel(1, 3) by blast}
moreover
{fix i assume l: "i < length ts"
then have f: "funas_gterm (gterm_of_term (ts ! i)) ⊆ ℱ" using More(6, 7)
by (auto simp add: funas_gterm_gterm_of_term[of "ts ! i"] dest!: subsetD)
from empty_aps[OF f] have "∃ x. ?P ts x i" using annotated_parallel_step.sel(1, 3) by blast}
ultimately obtain ss' ts' where len: "length ss = length ss'" "length ts = length ts'" and
prob: "∀i<length ss. ?P ss (ss' ! i) i" "∀i<length ts. ?P ts (ts' ! i) i"
using Ex_list_of_length_P[of "length ss" "?P ss"] Ex_list_of_length_P[of "length ts" "?P ts"]
by auto metis
have "∃ m. m ∈ annotated_parallel_closure ℱ R ∧ aps_step m = (?s, ?t) ∧ aps_single m"
proof (cases "C = □")
case False
then show ?thesis using More(1)[OF More(2) False _ _ cg f(2)]
by (auto simp add: lift_root_step_def) fastforce
qed (auto intro!: aps_root_step[OF More(2)])
then obtain m where m: "m ∈ annotated_parallel_closure ℱ R" "aps_step m = (?s, ?t)" "aps_single m"
by blast
let ?ps = "ss' @ m # ts'"
have "∀i<length ?ps. ?ps ! i ∈ annotated_parallel_closure ℱ R"
"∃ i < length ?ps. (aps_single (?ps ! i) ∧ (∀j < length ?ps. i ≠ j ⟶ aps_empty (?ps ! j)))"
using m prob len by (auto simp add: nth_append_Cons)
from aps_non_root_step[OF f(1) _ this(1)] this(2)
have "aps (GFun f (map (fst ∘ aps_step) ?ps), GFun f (map (snd ∘ aps_step) ?ps)) False
False True ∈ annotated_parallel_closure ℱ R"
by (auto simp add: len) (smt annotated_parallel_step.sel(3, 4) aps_empty_flags(2))
moreover have "GFun f (map (fst ∘ aps_step) ?ps) = s" "GFun f (map (snd ∘ aps_step) ?ps) = t"
using prob m(2) More(4, 5) by (auto simp add: len map_eq_conv')
ultimately show ?case by (auto simp add: lift_root_step_def) force
qed auto
lemma lift_PAny_Single_to_ctxt:
assumes "(s, t) ∈ lift_root_step ℱ PAny ESingle R"
shows "∃ u v C. gterm_of_term C⟨u⟩ = s ∧ gterm_of_term C⟨v⟩ = t ∧
(gterm_of_term u, gterm_of_term v) ∈ R ∧ funas_ctxt C ⊆ ℱ"
proof -
{assume "(s, t) ∈ R"
then have " gterm_of_term □⟨term_of_gterm s⟩ = s ∧ gterm_of_term □⟨term_of_gterm t⟩ = t ∧
(gterm_of_term (term_of_gterm s), gterm_of_term (term_of_gterm t)) ∈ R ∧ funas_ctxt □ ⊆ ℱ"
by auto}
note s = this
show ?thesis using assms lift_PNon_Single_to_ctxt[of s t ℱ R]
unfolding lift_root_Any_Single_eq lift_root_step_Root_Single
apply auto using s by blast
qed
lemma gctxt_to_lift_PAny_Single:
assumes "(gterm_of_term u, gterm_of_term v) ∈ R"
and "gterm_of_term C⟨u⟩ = s" and "gterm_of_term C⟨v⟩ = t" and "ground_ctxt C" and "funas_ctxt C ⊆ ℱ"
shows "(s, t) ∈ lift_root_step ℱ PAny ESingle R"
proof (cases "C = □")
case True
then show ?thesis using assms lift_root_Any_Single_eq by auto
next
case False
show ?thesis using gctxt_to_lift_PNon_Single[OF assms(1) False assms(2-)]
unfolding lift_root_Any_Single_eq by auto
qed
lemma lift_PNon_StrictPar_to_mctxt:
assumes "(s, t) ∈ lift_root_step ℱ PNonRoot EStrictParallel R"
shows "∃ ss ts C. length ss = length ts ∧ 0 < length ts ∧ funas_mctxt C ⊆ ℱ ∧ ground_mctxt C ∧ C ≠ MHole ∧
num_holes C = length ts ∧ gterm_of_term (fill_holes C ss) = s ∧ gterm_of_term (fill_holes C ts) = t ∧
(∀ i < length ts. (gterm_of_term (ss ! i), gterm_of_term (ts ! i)) ∈ R)"
proof -
obtain a where a: "a ∈ annotated_parallel_closure ℱ R" "aps_step a = (s, t)" "¬ aps_root a" "¬ aps_empty a"
using assms unfolding lift_root_step_def by auto
then show ?thesis
proof (induct arbitrary: s t)
case (aps_non_root_step f n ps)
let ?ss = "λ x. fst (fst x)" let ?ts = "λ x. snd (fst x)" let ?C = "λ x. snd x"
let ?P = "λ (x :: ((('a, 'b) term list × ('a, 'b) term list) × ('a, 'b) mctxt)) i. length (?ss x) = length (?ts x) ∧ funas_mctxt (?C x) ⊆ ℱ ∧ ground_mctxt (?C x) ∧
num_holes (?C x) = length (?ts x) ∧
gterm_of_term (fill_holes (?C x) (?ss x)) = fst (aps_step (ps ! i)) ∧
gterm_of_term (fill_holes (?C x) (?ts x)) = snd (aps_step (ps ! i)) ∧
(∀ i < length (?ts x). (gterm_of_term (?ss x ! i), gterm_of_term (?ts x ! i)) ∈ R)"
{fix i assume l: "i < length ps"
then have step: "ps ! i ∈ annotated_parallel_closure ℱ R" using aps_non_root_step by auto
consider (a) "aps_empty (ps ! i) ∧ ¬ aps_root (ps ! i)" | (b) "aps_root (ps ! i)" | (c) "¬ aps_empty (ps ! i) ∧ ¬ aps_root (ps ! i)"
by blast
then have "∃ x. ?P x i ∧ (aps_root (ps ! i) ∨ ¬ aps_empty (ps ! i) ⟶ 0 <num_holes (?C x))"
proof cases
case a
then obtain s where "aps_step (ps ! i) = (s, s)" "funas_gterm s ⊆ ℱ"
using step aps_empty_term by blast
then have "?P (([],[]), mctxt_of_term (term_of_gterm s)) i"
using mctxt_of_term_fill_holes ground_eq_fill[of "term_of_gterm s"]
using ground_term_of_gterm[of s] mctxt_of_term
by (auto simp add: funas_term_of_gterm_conv in_mono)
then show ?thesis using a by blast
next
case b
then obtain u v where "aps_step (ps ! i) = (u, v)" "(u, v) ∈ R"
using step by (metis aps_root surj_pair)
then have "?P (([term_of_gterm u], [term_of_gterm v]), MHole) i ∧ 0 < num_holes MHole" by auto
then show ?thesis using b l
by (intro exI[of _ "(([term_of_gterm u], [term_of_gterm v]), MHole)"]) auto
next
case c
then show ?thesis using step aps_non_root_step(3) l
by auto (metis length_greater_0_conv prod.collapse)
qed}
then obtain m where len: "length m = length ps" and
p: "∀ i < length m. (λ x i. ?P x i ∧ (aps_root (ps ! i) ∨ ¬ aps_empty (ps ! i) ⟶ 0 <num_holes (?C x))) (m ! i) i"
using Ex_list_of_length_P[of "length ps" "λ x i. ?P x i ∧ (aps_root (ps ! i) ∨ ¬ aps_empty (ps ! i) ⟶ 0 <num_holes (?C x))"] by auto
obtain i where w: "i < length ps ∧ (aps_root (ps ! i) ∨ ¬ aps_empty (ps ! i))" using aps_non_root_step(2-) by auto
define sss tss Cs where "sss = map (fst ∘ fst) m" "tss = map (snd ∘ fst) m" "Cs = map snd m"
have len: "length (Cs :: ('a, 'b) mctxt list) = length ps" "length sss = length ps" "length tss = length ps" and
subl: "∀ i < length ps. length (sss ! i) = length (tss ! i)" and
mfg: "∀ i < length ps. funas_mctxt (Cs ! i) ⊆ ℱ ∧ ground_mctxt (Cs ! i)" and
mhl: "∀ i < length ps. num_holes (Cs ! i) = length (sss ! i)" and
mhs: "∀ i < length ps. gterm_of_term (fill_holes (Cs ! i) (sss ! i)) = fst (aps_step (ps ! i))" and
mht: "∀ i < length ps. gterm_of_term (fill_holes (Cs ! i) (tss ! i)) = snd (aps_step (ps ! i))" and
rel: "∀ i < length sss. ∀ j < length (sss ! i). (gterm_of_term (sss ! i ! j), gterm_of_term (tss ! i ! j)) ∈ R" and
h: "0 < num_holes (Cs ! i)"
using len p w unfolding sss_tss_Cs_def by auto
have "gterm_of_term (fill_holes (MFun f Cs) (concat sss)) = s" "gterm_of_term (fill_holes (MFun f Cs) (concat tss)) = t"
using mhs mht aps_non_root_step(4) len
by (auto simp add: map_eq_conv' mhl partition_holes_concat_id subl)
moreover have "∀ i < length (concat sss). (gterm_of_term (concat sss ! i), gterm_of_term (concat tss ! i)) ∈ R"
using rel subl len(2-) by auto (metis nth_concat_two_lists)
moreover have "funas_mctxt (MFun f Cs) ⊆ ℱ" "ground_mctxt (MFun f Cs)"
using mfg aps_non_root_step(1, 2) len(1) by auto (metis in_set_idx subsetD)+
moreover have "MFun f Cs ≠ MHole" "num_holes (MFun f Cs) = length (concat sss)"
using len mhl by auto (metis length_concat map_eq_conv')
moreover have "length (concat sss) = length (concat tss)" using len subl
by (simp add: length_concat) (metis map_eq_conv')
moreover have "0 < length (concat tss)" using len(3) mhl subl conjunct1[OF w] h by auto
ultimately show ?case using len by metis
qed auto
qed
lemma gmctxt_to_lift_PNon_StrictPar:
assumes "∀ i < length ss. (gterm_of_term (ss ! i), gterm_of_term (ts ! i)) ∈ R"
and "num_holes C = length ss" and "num_holes C = length ts" and "0 < length ts"
and "C ≠ MHole" and "ground_mctxt C" and "funas_mctxt C ⊆ ℱ"
shows "(gterm_of_term (fill_holes C ss), gterm_of_term (fill_holes C ts)) ∈
lift_root_step ℱ PNonRoot EStrictParallel R"
using assms(2, 3, 1, 4-)
proof (induct rule: fill_holes_induct2)
case (MFun f Cs ss ts)
let ?s = "λ i. gterm_of_term (fill_holes (Cs ! i) (partition_holes ss Cs ! i))"
let ?t = "λ i. gterm_of_term (fill_holes (Cs ! i) (partition_holes ts Cs ! i))"
have w: "∃ i < length Cs. 0 < length (partition_holes ts Cs ! i)" using MFun
by (metis gr_implies_not_zero gr_zeroI length_partition_holes nth_concat_split)
{fix i assume l: "i < length Cs" and nt: "0 < length (partition_holes ts Cs ! i)"
have "∃ a. aps_step a = (?s i, ?t i) ∧ ¬ aps_empty a ∧ a ∈ annotated_parallel_closure ℱ R"
proof (cases "Cs ! i = MHole")
case True
from True MFun(1, 2, 4) l have "(?s i, ?t i) ∈ R"
using fill_holes_MHole_length[OF _ l(1) True] fill_holes_MHole2[OF _ _ True]
by auto
from aps_root_step[OF this] show ?thesis using annotated_parallel_step.sel(1, 3) by blast
next
case False
have "(?s i, ?t i) ∈ lift_root_step ℱ PNonRoot EStrictParallel R"
using l MFun(3)[OF l _ nt False] MFun(1, 2, 4, 7-)
using partition_by_nth_nth[OF MFun(1), of i] partition_by_nth_nth[OF MFun(2), of i]
by (auto simp add: UN_subset_iff)
then show ?thesis unfolding lift_root_step_def by auto
qed}
moreover
{fix i assume ass: "i < length Cs" "0 = length (partition_holes ts Cs ! i)"
have "∃ a. aps_step a = (?s i, ?t i) ∧ a ∈ annotated_parallel_closure ℱ R"
using ass length_partition_holes_nth[OF MFun(2) ass(1)] gmctxt_no_holes_gterm[of "Cs ! i"]
using empty_aps[of "gterm_of_term (term_of_mctxt (Cs ! i))" ℱ R] MFun(7, 8)
using length_partition_holes_nth[OF MFun(1) ass(1)] length_partition_holes_nth[OF MFun(2) ass(1)]
by auto (meson SUP_le_iff annotated_parallel_step.sel(1) nth_mem)}
ultimately obtain ps where ps: "length ps = length Cs"
"∀ i < length ps. ps ! i ∈ annotated_parallel_closure ℱ R"
"∀ i < length ps. aps_step (ps ! i) = (?s i, ?t i)"
"∃ i < length ps. ¬ aps_empty (ps ! i)"
using w Ex_list_of_length_P[of "length Cs" "λ x i. x ∈ annotated_parallel_closure ℱ R ∧
aps_step x = (?s i, ?t i) ∧ (0 < length (partition_holes ts Cs ! i) ⟶ ¬ aps_empty x)"]
by auto smt
then have "∃ u. aps (GFun f (map (fst ∘ aps_step) ps), GFun f (map (snd ∘ aps_step) ps)) False False u ∈ annotated_parallel_closure ℱ R"
using aps_non_root_step[of f "length Cs" ℱ ps R] MFun(8) by auto smt
moreover have "(gterm_of_term (fill_holes (MFun f Cs) (concat (partition_holes ss Cs))),
gterm_of_term (fill_holes (MFun f Cs) (concat (partition_holes ts Cs)))) =
(GFun f (map (fst ∘ aps_step) ps), GFun f (map (snd ∘ aps_step) ps))"
using MFun(1, 2) ps(1, 3) by (auto simp add: comp_def map_nth map_eq_conv')
ultimately show ?case using ps(1, 2)
by (auto simp add: comp_def lift_root_step_def simp del: fill_holes.simps) force
qed auto
lemma lift_PAny_StrictPar_to_mctxt:
assumes "(s, t) ∈ lift_root_step ℱ PAny EStrictParallel R"
shows "∃ ss ts C. length ss = length ts ∧ 0 < length ts ∧ funas_mctxt C ⊆ ℱ ∧ ground_mctxt C ∧
num_holes C = length ts ∧ gterm_of_term (fill_holes C ss) = s ∧ gterm_of_term (fill_holes C ts) = t ∧
(∀ i < length ts. (gterm_of_term (ss ! i), gterm_of_term (ts ! i)) ∈ R)"
proof -
consider (a) "(s, t) ∈ R" | (b) "(s, t) ∈ lift_root_step ℱ PNonRoot EStrictParallel R"
using assms by auto
then show ?thesis
proof cases
case a
then show ?thesis by (force intro: exI[of _ "[term_of_gterm s]" for s] exI[of _ MHole])
next
case b
from lift_PNon_StrictPar_to_mctxt[OF b] show ?thesis by blast
qed
qed
lemma gmctxt_to_lift_PAny_StrictPar:
assumes "∀ i < length ss. (gterm_of_term (ss ! i), gterm_of_term (ts ! i)) ∈ R"
and "length ss = length ts" and "0 < length ts" and "num_holes C = length ts"
and "ground_mctxt C" and "funas_mctxt C ⊆ ℱ"
shows "(gterm_of_term (fill_holes C ss), gterm_of_term (fill_holes C ts)) ∈
lift_root_step ℱ PAny EStrictParallel R"
proof (cases "C = MHole")
case True
then show ?thesis using assms by (auto simp add: fill_holes_MHole)
next
case False
from gmctxt_to_lift_PNon_StrictPar[OF assms(1) _ _ assms(3) False assms(5-)]
show ?thesis using assms(2, 4) by auto
qed
lemma lift_PNon_Par_to_gmctxt:
assumes "(s, t) ∈ lift_root_step ℱ PNonRoot EParallel R"
shows "∃ ss ts C. length ss = length ts ∧ funas_mctxt C ⊆ ℱ ∧ ground_mctxt C ∧ C ≠ MHole ∧
num_holes C = length ts ∧ gterm_of_term (fill_holes C ss) = s ∧ gterm_of_term (fill_holes C ts) = t ∧
(∀ i < length ts. (gterm_of_term (ss ! i), gterm_of_term (ts ! i)) ∈ R)"
proof -
consider (a) "(s, t) ∈ Restr Id {t. funas_gterm t ⊆ ℱ}" |
(b) "(s, t) ∈ lift_root_step ℱ PNonRoot EStrictParallel R"
using assms lift_root_step_Parallel_conv[of ℱ PNonRoot R] by auto
then show ?thesis proof cases
case a
then show ?thesis using mctxt_of_term ground_eq_fill[of "term_of_gterm t"]
by (intro exI[of _ "[]"] exI[of _ "mctxt_of_term (term_of_gterm t)"])
(auto simp add: funas_term_of_gterm_conv)
next
case b
then show ?thesis using lift_PNon_StrictPar_to_mctxt[OF b] by auto
qed
qed
lemma gmctxt_to_lift_PNon_Par:
assumes "∀ i < length ss. (gterm_of_term (ss ! i), gterm_of_term (ts ! i)) ∈ R"
and "length ss = length ts" and "num_holes C = length ts" and "C ≠ MHole"
and "ground_mctxt C" and "funas_mctxt C ⊆ ℱ"
shows "(gterm_of_term (fill_holes C ss), gterm_of_term (fill_holes C ts)) ∈
lift_root_step ℱ PNonRoot EParallel R"
proof (cases "0 < length ts")
case True
from gmctxt_to_lift_PNon_StrictPar[OF assms(1) _ _ True assms(4-)] assms(2, 3)
show ?thesis unfolding lift_root_step_Parallel_conv[of ℱ PNonRoot R]
by auto
next
case False
then have "(gterm_of_term (fill_holes C ss), gterm_of_term (fill_holes C ts)) ∈ Restr Id {t. funas_gterm t ⊆ ℱ}"
using assms funas_gterm_gterm_of_term ground_eq_fill[OF mctxt_of_term[of "term_of_mctxt C"]] funas_mctxt_mctxt_of_term[of "term_of_mctxt C"]
by auto
then show ?thesis using lift_root_step_Parallel_conv[of ℱ PNonRoot R] by auto
qed
lemma lift_PAny_Par_to_gmctxt:
assumes "(s, t) ∈ lift_root_step ℱ PAny EParallel R"
shows "∃ ss ts C. length ss = length ts ∧ funas_mctxt C ⊆ ℱ ∧ ground_mctxt C ∧
num_holes C = length ts ∧ gterm_of_term (fill_holes C ss) = s ∧ gterm_of_term (fill_holes C ts) = t ∧
(∀ i < length ts. (gterm_of_term (ss ! i), gterm_of_term (ts ! i)) ∈ R)"
proof -
consider (a) "(s, t) ∈ Restr Id {t. funas_gterm t ⊆ ℱ}" |
(b) "(s, t) ∈ lift_root_step ℱ PAny EStrictParallel R"
using assms unfolding lift_root_step_Parallel_conv[of ℱ PAny R] by auto
then show ?thesis proof cases
case a then show ?thesis using mctxt_of_term ground_eq_fill[of "term_of_gterm t"]
by (intro exI[of _ "[]"] exI[of _ "mctxt_of_term (term_of_gterm t)"])
(auto simp add: funas_term_of_gterm_conv)
next
case b
then show ?thesis using lift_PAny_StrictPar_to_mctxt by blast
qed
qed
lemma gmctxt_to_lift_PAny_Par:
assumes "∀ i < length ss. (gterm_of_term (ss ! i), gterm_of_term (ts ! i)) ∈ R"
and "length ss = length ts" and "num_holes C = length ts"
and "ground_mctxt C" and "funas_mctxt C ⊆ ℱ"
shows "(gterm_of_term (fill_holes C ss), gterm_of_term (fill_holes C ts)) ∈
lift_root_step ℱ PAny EParallel R"
proof (cases "0 < length ts")
case True
from gmctxt_to_lift_PAny_StrictPar[OF assms(1, 2) True assms(3-)]
show ?thesis using lift_root_step_Parallel_conv[of ℱ PAny R]
by auto
next
case False
then have "(gterm_of_term (fill_holes C ss), gterm_of_term (fill_holes C ts)) ∈ Restr Id {t. funas_gterm t ⊆ ℱ}"
using assms funas_gterm_gterm_of_term ground_eq_fill[OF mctxt_of_term[of "term_of_mctxt C"]] funas_mctxt_mctxt_of_term[of "term_of_mctxt C"]
by auto
then show ?thesis using lift_root_step_Parallel_conv[of ℱ PAny R] by auto
qed
lemma easy:
"R ⊆ {aps_step a |a. a ∈ annotated_parallel_closure ℱ R ∧ aps_single a}"
apply auto sorry
lemma gtrancl_rel_left1:
assumes "(s, t) ∈ {aps_step a |a. a ∈ annotated_parallel_closure ℱ R ∧ aps_single a}⇧*"
and "(t, u) ∈ R"
and "(u, v) ∈ {aps_step a |a. a ∈ annotated_parallel_closure ℱ R ∧ aps_single a}⇧*"
shows "(s, v) ∈ (aps_step ` annotated_parallel_closure ℱ R)⇧+"
using assms(3)
proof (cases)
case base
from assms(2) have t: "(t, u) ∈ {aps_step a |a. a ∈ annotated_parallel_closure ℱ R ∧ aps_single a}"
using easy by blast
from trancl_mono[OF rtrancl_trancl_trancl[OF assms(1) r_into_trancl[OF t]]]
show ?thesis using base by (simp add: image_mono setcompr_eq_image)
next
case (step y)
from rtrancl_into_trancl1[OF this]
have tr: "(u, v) ∈ {aps_step a |a. a ∈ annotated_parallel_closure ℱ R ∧ aps_single a}⇧+" .
from assms(2) have "(t, u) ∈ {aps_step a |a. a ∈ annotated_parallel_closure ℱ R ∧ aps_single a}"
using easy by blast
from trancl_into_trancl2[OF this tr]
have "(t, v) ∈ {aps_step a |a. a ∈ annotated_parallel_closure ℱ R ∧ aps_single a}⇧+" .
from trancl_mono[OF rtrancl_trancl_trancl[OF assms(1) this]] show ?thesis
by (simp add: image_mono setcompr_eq_image)
qed
lemma gtrancl_rel_inc:
"gtrancl_rel ℱ R ⊆ (aps_step ` annotated_parallel_closure ℱ R)⇧+"
unfolding gtrancl_rel_def lift_root_step_def apply auto
using gtrancl_rel_left1 by blast
lemma gtrancl_rel:
"lift_root_step ℱ PAny EParallel (gtrancl_rel ℱ R) = (lift_root_step ℱ PAny EParallel R)⇧+" (is "?L = ?R")
proof rule
let ?lift = "lift_root_step ℱ PAny EParallel"
{fix s t assume "(s,t) ∈ ?L"
then have "(s, t) ∈ ?lift ((aps_step ` annotated_parallel_closure ℱ R)⇧+)"
unfolding lift_root_step_def using aps_incr gtrancl_rel_inc by blast
then have "(s, t) ∈ ?R" unfolding lift_root_step_def
apply auto
sorry}
then show "?L ⊆ ?R" by auto
next
show "?R ⊆ ?L" sorry
qed
inductive_set parallel_closure ::"('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel" for ℱ ℛ
where root_step[intro]: "(s , t) ∈ ℛ ⟹ (s , t) ∈ parallel_closure ℱ ℛ"
| par_step_fun[intro]: "⟦⋀ i. i < length ts ⟹ (ss ! i,ts ! i) ∈ parallel_closure ℱ ℛ⟧ ⟹ length ss = length ts ⟹
(f, length ts) ∈ ℱ ⟹ (GFun f ss, GFun f ts) ∈ parallel_closure ℱ ℛ"
lemma parallel_impl_aps_annotated:
assumes "(s, t) ∈ parallel_closure ℱ ℛ"
shows "(s, t) ∈ aps_step ` annotated_parallel_closure ℱ ℛ"
using assms
proof induct
case (root_step s t)
then show ?case using aps_root_step image_iff by fastforce
next
case (par_step_fun ts ss f)
let ?P = "λ p i. p ∈ annotated_parallel_closure ℱ ℛ ∧ aps_step p = (ss ! i, ts ! i)"
{fix i assume "i < length ts"
from par_step_fun(2)[OF this] have "∃ p. ?P p i" unfolding image_iff by auto}
from this Ex_list_of_length_P[of _ ?P]
obtain ps where l: "length ps = length ts" and rec :"(∀ i < length ts. ps ! i ∈ annotated_parallel_closure ℱ ℛ ∧
aps_step (ps ! i) = (ss ! i, ts ! i))" by blast
from rec have "GFun f (map (fst ∘ aps_step) ps) = GFun f ss" "GFun f (map (snd ∘ aps_step) ps) = GFun f ts"
by (simp add: l map_nth_eq_conv par_step_fun(3))+
then show ?case using aps_non_root_step[OF par_step_fun(4) l, of ℛ] rec
by (auto simp add: image_iff) force
qed
lemma aps_annotated_impl_parallel:
assumes "(s, t) ∈ aps_step ` annotated_parallel_closure ℱ ℛ"
shows "(s, t) ∈ parallel_closure ℱ ℛ"
using assms
proof
fix x assume aps: "(s, t) = aps_step x"
assume "x ∈ annotated_parallel_closure ℱ ℛ"
then show "(s, t) ∈ parallel_closure ℱ ℛ" using aps
proof (induct arbitrary: s t)
case (aps_non_root_step f n ps)
then have "∀i<length ps. (fst (aps_step (ps ! i)), snd (aps_step (ps ! i))) ∈ parallel_closure ℱ ℛ"
using prod.collapse by blast
then show ?case using aps_non_root_step(1, 2, 4) by auto
qed auto
qed
lemma args_par_rstep_pow_imp_par_rstep_pow:
"length xs = length ys ⟹ ∀i<length xs. (xs ! i, ys ! i) ∈ parallel_closure ℱ R ^^ n ⟹
(f, length xs) ∈ ℱ ⟹ (GFun f xs, GFun f ys) ∈ parallel_closure ℱ R ^^ n"
proof(induct n arbitrary:ys)
case 0
then have "∀i<length xs. (xs ! i = ys ! i)" by simp
with 0 show ?case using relpow_0_I list_eq_iff_nth_eq by metis
next
case (Suc n)
let ?c = "λ z i. (xs ! i, z) ∈ parallel_closure ℱ R ^^ n ∧ (z, ys ! i) ∈ parallel_closure ℱ R"
{ fix i assume "i < length xs"
from relpow_Suc_E[OF Suc(3)[rule_format, OF this]]
have "∃ z. (?c z i)" by metis
}
with choice have "∃ zf. ∀ i < length xs. (?c (zf i) i)" by meson
then obtain zf where a:"∀ i < length xs. (?c (zf i) i)" by auto
let ?zs = "map zf [0..<length xs]"
have len:"length xs = length ?zs" by simp
from a map_nth have "∀i<length xs. (xs ! i, ?zs ! i) ∈ parallel_closure ℱ R ^^ n" by auto
from Suc(1)[OF len this Suc(4)] have n:"(GFun f xs, GFun f ?zs) ∈ parallel_closure ℱ R ^^ n" by auto
from a map_nth have "∀i<length xs. (?zs ! i, ys ! i) ∈ parallel_closure ℱ R" by auto
with par_step_fun len Suc(2, 4) have "(GFun f ?zs, GFun f ys) ∈ parallel_closure ℱ R" by auto
with n show ?case by auto
qed
lemma
"(a, b) ∈ parallel_closure ℱ (inv_image ℛ term_of_gterm) ⟹ (a, b) ∈ gpar_rstep ℛ"
by (induct rule: parallel_closure.induct) (auto simp add: gpar_rstep_def par_rstep_id)
lemma aps_annot_eq_parallel:
"aps_step ` annotated_parallel_closure ℱ ℛ = parallel_closure ℱ ℛ"
using aps_annotated_impl_parallel parallel_impl_aps_annotated by auto fastforce+
lemma R_sub_sig_parallel_sub_sig:
assumes "(s, t) ∈ parallel_closure ℱ ℛ"
and "ℛ ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
shows "funas_gterm s ⊆ ℱ ∧ funas_gterm t ⊆ ℱ"
using assms(1)
proof induct
case (root_step s t)
then show ?case using assms(2) by auto
next
case (par_step_fun ts ss f)
then show ?case unfolding funas_gterm_def by auto (metis in_mono in_set_idx)+
qed
lemma parallel_refl_on_sig:
assumes "funas_gterm a ⊆ ℱ"
shows "(a, a) ∈ parallel_closure ℱ ℛ"
using assms
proof (induct a)
case (GFun f ts)
{fix i assume i: "i < length ts"
then have "(ts ! i, ts ! i) ∈ parallel_closure ℱ ℛ"
using nth_mem[OF i] GFun(1)[of "ts ! i"]
using GFun(2) apply (auto simp add: funas_gterm_def)
using ‹ts ! i ∈ set ts› by blast}
then show ?case using par_step_fun[of ts ts] nth_mem GFun(2)
by (auto simp add: funas_gterm_def)
qed
lemma prallel_comp_incr_suc:
assumes "(a, b) ∈ parallel_closure ℱ ℛ ^^ n" and "0 < n"
and "ℛ ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
shows "(a, b) ∈ parallel_closure ℱ ℛ ^^ (Suc n)"
proof (cases n)
case 0
then show ?thesis using assms(2) by auto
next
case (Suc nat)
then obtain c where f: "(a, c) ∈ parallel_closure ℱ ℛ" and
r: "(c, b) ∈ parallel_closure ℱ ℛ ^^ nat"
using assms by auto (meson relpow_Suc_D2')
then have "funas_gterm a ⊆ ℱ" using assms(3) R_sub_sig_parallel_sub_sig[OF f] by blast
from parallel_refl_on_sig[OF this]
have "(a, a) ∈ parallel_closure ℱ ℛ" by auto
then show ?thesis using assms by auto (metis relcomp.relcompI relpow_commute)
qed
lemma prallel_comp_incr:
assumes "(a, b) ∈ parallel_closure ℱ ℛ ^^ n" and "0 < n" and "n ≤ m"
and "ℛ ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
shows "(a, b) ∈ parallel_closure ℱ ℛ ^^ m"
using assms(3)
proof (induct "m - n" arbitrary: m)
case 0
then show ?case using assms(1) by auto
next
case (Suc x)
then obtain m' where [simp]: "m = Suc m'" and [simp]: "0 < m'"
using gr0_implies_Suc assms(2) gr0I by force
from Suc(1)[of m'] Suc(2, 3) assms(1)
have "(a, b) ∈ parallel_closure ℱ ℛ ^^ m'" by auto
from prallel_comp_incr_suc[OF this _ assms(4)]
show ?case by auto
qed
lemma
assumes "ℛ ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
shows "(a, b) ∈ parallel_closure ℱ ((parallel_closure ℱ ℛ)⇧+) ⟹ (a, b) ∈ (parallel_closure ℱ ℛ)⇧+"
proof (induct rule: parallel_closure.induct)
case (par_step_fun ts ss f)
from par_step_fun(2) Ex_list_of_length_P[of "length ts" "λ n i. (ss ! i, ts ! i) ∈ parallel_closure ℱ ℛ ^^ n ∧ 0 < n"]
obtain xs where len: "length xs = length ts" and rec: "(∀i< length ts. (ss ! i, ts ! i) ∈ parallel_closure ℱ ℛ ^^ xs ! i ∧ 0 < xs ! i)"
unfolding trancl_power by auto
then obtain n where max: "max_list xs = n" by blast
then have "(∀i< length ts. (ss ! i, ts ! i) ∈ parallel_closure ℱ ℛ ^^ n)"
using prallel_comp_incr[OF _ _ _ assms] rec len max_list by auto
then show ?case unfolding trancl_power using par_step_fun(4)
using args_par_rstep_pow_imp_par_rstep_pow[OF par_step_fun(3)] par_step_fun(3)[symmetric]
by auto (metis gr0I le_0_eq len local.rec max max_list nth_mem zero_less_Suc)
qed
lemma parallel_parallel_simp:
assumes "(s, t) ∈ parallel_closure ℱ (parallel_closure ℱ ℛ)"
shows "(s, t) ∈ parallel_closure ℱ ℛ"
using assms
proof induct
case (par_step_fun ts ss f)
then show ?case by (intro parallel_closure.par_step_fun) blast+
qed auto
lemma t:
"gcomp_rel ℱ R S = (R O parallel_closure ℱ S) ∪ (parallel_closure ℱ R O S)"
unfolding gcomp_rel_def lift_root_step_def by (simp add: aps_annot_eq_parallel setcompr_eq_image)
lemma gcomp_rel2:
"lift_root_step ℱ PAny EParallel (gcomp_rel ℱ R S) = lift_root_step ℱ PAny EParallel R O lift_root_step ℱ PAny EParallel S"
proof -
{fix a b assume w: "(a, b) ∈ parallel_closure ℱ (R O parallel_closure ℱ S ∪ parallel_closure ℱ R O S)"
then have "(a, b) ∈ parallel_closure ℱ R O parallel_closure ℱ S"
proof induct
case (par_step_fun ts ss f)
{fix i assume "i < length ts"
then have "∃ u. (ss ! i, u) ∈ parallel_closure ℱ R ∧ (u, ts ! i) ∈ parallel_closure ℱ S"
using par_step_fun(2) by auto}
then obtain us where "(∀i< length ts. (ss ! i, us ! i) ∈ parallel_closure ℱ R ∧ (us ! i, ts ! i) ∈ parallel_closure ℱ S)" and "length us = length ts"
using Ex_list_of_length_P[of _ "λ u i. (ss ! i, u) ∈ parallel_closure ℱ R ∧ (u, ts ! i) ∈ parallel_closure ℱ S"]
by metis
then have "(GFun f ss, GFun f us) ∈ parallel_closure ℱ R ∧ (GFun f us, GFun f ts) ∈ parallel_closure ℱ S"
using par_step_fun(3, 4) by auto
then show ?case by auto
qed auto}
moreover
{fix a b assume "(a, b) ∈ parallel_closure ℱ R O parallel_closure ℱ S"
then obtain c where "(a, c) ∈ parallel_closure ℱ R" and "(c, b) ∈ parallel_closure ℱ S" by auto
then have "(a, b) ∈ parallel_closure ℱ (R O parallel_closure ℱ S ∪ parallel_closure ℱ R O S)"
proof (induct arbitrary: b)
case (par_step_fun ts ss f)
have pr: "(GFun f ss, GFun f ts) ∈ parallel_closure ℱ R"
using par_step_fun(1, 3, 4) by auto
show ?case proof (cases "(GFun f ts, b) ∈ S")
case True
from relcompI[OF pr this]
show ?thesis by (simp add: parallel_closure.root_step)
next
case False
obtain us where [simp]: "b = GFun f us" and len: "length us = length ts"
using par_step_fun(5) False by cases auto
{fix i assume l: "i < length ts"
have "(ss ! i, us ! i) ∈ parallel_closure ℱ (R O parallel_closure ℱ S ∪ parallel_closure ℱ R O S)"
using par_step_fun(5) False l par_step_fun(2)[OF l, of "us ! i"]
by cases auto}
then show ?thesis using par_step_fun(3, 4) len by auto
qed
qed auto}
ultimately show ?thesis unfolding lift_root_step_def t
by (auto simp add: aps_annot_eq_parallel setcompr_eq_image) blast
qed
end