Theory Orthogonal_PT
section‹Orthogonal Proof Terms›
theory Orthogonal_PT
imports
Residual_Join_Deletion
begin
inductive orthogonal::"('f, 'v) pterm ⇒ ('f, 'v) pterm ⇒ bool" (infixl "⊥⇩p" 50)
where
"Var x ⊥⇩p Var x"
| "length As = length Bs ⟹ ∀ i < length As. As!i ⊥⇩p Bs!i ⟹ Fun f As ⊥⇩p Fun f Bs"
| "length As = length Bs ⟹ ∀(a,b) ∈ set(zip As Bs). a ⊥⇩p b ⟹ (Prule α As) ⊥⇩p (to_pterm (lhs α)) ⋅ ⟨Bs⟩⇩α"
| "length As = length Bs ⟹ ∀(a,b) ∈ set(zip As Bs). a ⊥⇩p b ⟹ (to_pterm (lhs α)) ⋅ ⟨As⟩⇩α ⊥⇩p (Prule α Bs)"
lemmas orthogonal.intros[intro]
lemma orth_symp: "symp (⊥⇩p)"
proof
{fix A B::"('f, 'v) pterm" assume "A ⊥⇩p B"
then show "B ⊥⇩p A" proof(induct)
case (3 As Bs α)
then show ?case using orthogonal.intros(4)[where α=α and Bs=As and As=Bs]
using zip_symm by fastforce
next
case (4 As Bs α)
then show ?case using orthogonal.intros(3)[where α=α and As=Bs and Bs=As]
using zip_symm by fastforce
qed (simp_all add:orthogonal.intros)
}
qed
lemma equal_imp_orthogonal:
shows "A ⊥⇩p A"
by(induct A) (simp_all add: orthogonal.intros)
lemma source_orthogonal:
assumes "source A = t"
shows "A ⊥⇩p to_pterm t"
using assms proof(induct A arbitrary:t)
case (Prule α As)
then have t:"to_pterm t = (to_pterm (lhs α)) ⋅ ⟨map (to_pterm ∘ source) As⟩⇩α"
by (metis fun_mk_subst list.map_comp source.simps(3) to_pterm.simps(1) to_pterm_subst)
from Prule(1) have "∀(a,b) ∈ set (zip As (map (to_pterm ∘ source) As)). a ⊥⇩p b"
by (metis (mono_tags, lifting) case_prod_beta' comp_def in_set_zip nth_map zip_fst)
with t show ?case
using orthogonal.intros(3) by (metis length_map)
qed (simp_all add:orthogonal.intros)
lemma orth_imp_co_initial:
assumes "A ⊥⇩p B"
shows "co_initial A B"
using assms proof(induct rule: orthogonal.induct)
case (2 As Bs f)
show ?case proof(cases f)
case (Inr g)
with 2 show ?thesis unfolding Inr
by (simp add: nth_map_conv)
next
case (Inl α)
with 2 show ?thesis unfolding Inl
by (metis nth_map_conv source.simps(3))
qed
next
case (3 As Bs α)
then have l:"length (zip As Bs) = length As"
by simp
with 3 have IH:"∀i < length As. source (As!i) = source (Bs!i)"
by (metis (mono_tags, lifting) case_prod_conv nth_mem nth_zip)
have src:"source ((to_pterm (lhs α)) ⋅ ⟨Bs⟩⇩α) = (lhs α) ⋅ ⟨map source Bs⟩⇩α"
by (simp add: source_apply_subst)
from 3(1) l IH show ?case unfolding src source.simps
by (metis nth_map_conv)
next
case (4 As Bs α)
then have l:"length (zip As Bs) = length As"
by simp
with 4 have IH:"∀i < length As. source (As!i) = source (Bs!i)"
by (metis (mono_tags, lifting) case_prod_conv nth_mem nth_zip)
have src:"source ((to_pterm (lhs α)) ⋅ ⟨As⟩⇩α) = (lhs α) ⋅ ⟨map source As⟩⇩α"
by (simp add: source_apply_subst)
from 4(1) l IH show ?case unfolding src source.simps
by (metis nth_map_conv)
qed simp
text‹If two proof terms are orthogonal then residual and join are well-defined.›
lemma orth_imp_residual_defined:
assumes varcond:"⋀l r. (l, r) ∈ R ⟹ is_Fun l" "⋀l r. (l, r) ∈ S ⟹ is_Fun l"
and "A ⊥⇩p B"
and "A ∈ wf_pterm R" and "B ∈ wf_pterm S"
shows "A re B ≠ None"
using assms(3-) proof(induct)
case (2 As Bs f)
from 2(3) have wellAs:"∀a ∈ set As. a ∈ wf_pterm R"
by blast
from 2(4) have wellBs:"∀b ∈ set Bs. b ∈ wf_pterm S"
by blast
from 2(1,2) wellAs wellBs have c:"∀i < length As. (∃C. As!i re Bs!i = Some C)"
by auto
from 2(1) have l:"length As = length (map2 (re) As Bs)"
by simp
from 2(1) have "∀i < length As. As!i re Bs!i = (map2 (re) As Bs)!i"
by simp
with c obtain Cs where "∀i < length As. As!i re Bs!i = Some (Cs!i)" and "length Cs = length As"
using exists_some_list l by (metis (no_types, lifting))
with 2 have *:"those (map2 (re) As Bs) = Some Cs"
by (simp add: those_some)
show ?case proof(cases f)
case (Inr g)
show ?thesis unfolding Inr residual.simps 2(1) * by simp
next
case (Inl α)
show ?thesis unfolding Inl residual.simps 2(1) * by simp
qed
next
case (3 As Bs α)
from 3(3) varcond obtain g ts where g:"lhs α = Fun g ts"
by (metis Inl_inject is_Fun_Fun_conv sum.simps(4) term.distinct(1) term.sel(2) wf_pterm.cases)
then have *:"to_pterm (lhs α) ⋅ ⟨Bs⟩⇩α = Pfun g (map (λt. t ⋅ ⟨Bs⟩⇩α) (map to_pterm ts))"
by simp
from 3(3) have l1:"length As = length (var_rule α)"
using wf_pterm.simps by fastforce
from 3(3) have wellAs:"∀a ∈ set As. a ∈ wf_pterm R"
by blast
from 3(1,4) l1 have wellBs:"∀b ∈ set Bs. b ∈ wf_pterm S"
by (simp add: lhs_subst_args_wf_pterm)
from 3(1) have l2:"length (zip As Bs) = length As"
by simp
with 3(1,2) wellAs wellBs have "∀i < length As. As ! i re Bs ! i ≠ None"
by (metis (mono_tags, lifting) case_prod_conv nth_mem nth_zip)
then have c:"∀i < length As. (∃C. As!i re Bs!i = Some C)"
by blast
from 3(1) have "∀i < length As. As!i re Bs!i = (map2 (re) As Bs)!i"
by simp
with c obtain Cs where "∀i < length As. As!i re Bs!i = Some (Cs!i)" and "length Cs = length As"
using exists_some_list l2 by (metis (no_types, lifting) length_map)
with 3 have cs:"those (map2 (re) As Bs) = Some Cs"
by (simp add: those_some)
have bs:"match (to_pterm (lhs α) ⋅ ⟨Bs⟩⇩α) (to_pterm (lhs α)) = Some (⟨Bs⟩⇩α)"
using lhs_subst_trivial by blast
then have "(map (⟨Bs⟩⇩α) (var_rule α)) = Bs"
using 3(1) l1 apply_lhs_subst_var_rule by force
then show ?case using residual.simps(5) using bs cs g unfolding *
by simp
next
case (4 As Bs α)
from 4(4) varcond obtain g ts where g:"lhs α = Fun g ts"
by (metis Inl_inject is_Fun_Fun_conv sum.simps(4) term.distinct(1) term.sel(2) wf_pterm.cases)
then have *:"to_pterm (lhs α) ⋅ ⟨As⟩⇩α = Pfun g (map (λt. t ⋅ ⟨As⟩⇩α) (map to_pterm ts))"
by simp
from 4(4) have l1:"length Bs = length (var_rule α)"
using wf_pterm.simps by fastforce
from 4(1,3) l1 have wellAs:"∀a ∈ set As. a ∈ wf_pterm R"
by (simp add: lhs_subst_args_wf_pterm)
from 4(4) have wellBs:"∀b ∈ set Bs. b ∈ wf_pterm S"
by blast
from 4(1) have l2:"length (zip As Bs) = length As"
by simp
with 4(1,2) wellAs wellBs have "∀i < length As. As ! i re Bs ! i ≠ None"
by (metis (mono_tags, lifting) case_prod_conv nth_mem nth_zip)
then have c:"∀i < length As. (∃C. As!i re Bs!i = Some C)"
by blast
from 4(1) have "∀i < length As. As!i re Bs!i = (map2 (re) As Bs)!i"
by simp
with c obtain Cs where "∀i < length As. As!i re Bs!i = Some (Cs!i)" and "length Cs = length As"
using exists_some_list l2 by (metis (no_types, lifting) length_map)
with 4 have cs:"those (map2 (re) As Bs) = Some Cs"
by (simp add: those_some)
have bs:"match (to_pterm (lhs α) ⋅ ⟨As⟩⇩α) (to_pterm (lhs α)) = Some (⟨As⟩⇩α)"
using lhs_subst_trivial by blast
have "(map (⟨As⟩⇩α) (var_rule α)) = As"
using 4(1) l1 apply_lhs_subst_var_rule by force
then show ?case using residual.simps(7) using bs cs g unfolding *
by simp
qed simp
lemma orth_imp_join_defined:
assumes varcond:"⋀l r. (l, r) ∈ R ⟹ is_Fun l"
and "A ⊥⇩p B"
and "A ∈ wf_pterm R" and "B ∈ wf_pterm R"
shows "A ⊔ B ≠ None"
using assms(2-) proof(induct)
case (2 As Bs f)
from 2(3) have wellAs:"∀a ∈ set As. a ∈ wf_pterm R"
by blast
from 2(4) have wellBs:"∀b ∈ set Bs. b ∈ wf_pterm R"
by blast
from 2(1,2) wellAs wellBs have c:"∀i < length As. (∃C. As!i ⊔ Bs!i = Some C)"
by auto
from 2(1) have l:"length As = length (map2 (⊔) As Bs)"
by simp
from 2(1) have "∀i < length As. As!i ⊔ Bs!i = (map2 (⊔) As Bs)!i"
by simp
with c obtain Cs where "∀i < length As. As!i ⊔ Bs!i = Some (Cs!i)" and "length Cs = length As"
using exists_some_list l by (metis (no_types, lifting))
with 2 have *:"those (map2 (⊔) As Bs) = Some Cs"
by (simp add: those_some)
show ?case proof(cases f)
case (Inr g)
show ?thesis unfolding Inr join.simps 2(1) * by simp
next
case (Inl α)
show ?thesis unfolding Inl join.simps 2(1) * by simp
qed
next
case (3 As Bs α)
from 3(3) varcond obtain g ts where g:"lhs α = Fun g ts"
by (metis Inl_inject is_Fun_Fun_conv sum.simps(4) term.distinct(1) term.sel(2) wf_pterm.cases)
then have *:"to_pterm (lhs α) ⋅ ⟨Bs⟩⇩α = Pfun g (map (λt. t ⋅ ⟨Bs⟩⇩α) (map to_pterm ts))"
by simp
from 3(3) have l1:"length As = length (var_rule α)"
using wf_pterm.simps by fastforce
from 3(3) have wellAs:"∀a ∈ set As. a ∈ wf_pterm R"
by blast
from 3(1,4) l1 have wellBs:"∀b ∈ set Bs. b ∈ wf_pterm R"
by (simp add: lhs_subst_args_wf_pterm)
from 3(1) have l2:"length (zip As Bs) = length As"
by simp
with 3(1,2) wellAs wellBs have "∀i < length As. As ! i ⊔ Bs ! i ≠ None"
by (metis (mono_tags, lifting) case_prod_conv nth_mem nth_zip)
then have c:"∀i < length As. (∃C. As!i ⊔ Bs!i = Some C)"
by blast
from 3(1) have "∀i < length As. As!i ⊔ Bs!i = (map2 (⊔) As Bs)!i"
by simp
with c obtain Cs where "∀i < length As. As!i ⊔ Bs!i = Some (Cs!i)" and "length Cs = length As"
using exists_some_list l2 by (metis (no_types, lifting) length_map)
with 3 have cs:"those (map2 (⊔) As Bs) = Some Cs"
by (simp add: those_some)
have bs:"match (to_pterm (lhs α) ⋅ ⟨Bs⟩⇩α) (to_pterm (lhs α)) = Some (⟨Bs⟩⇩α)"
using lhs_subst_trivial by blast
then have "(map (⟨Bs⟩⇩α) (var_rule α)) = Bs"
using 3(1) l1 apply_lhs_subst_var_rule by force
then show ?case using residual.simps(5) using bs cs g unfolding *
by simp
next
case (4 As Bs α)
from 4(4) varcond obtain g ts where g:"lhs α = Fun g ts"
by (metis Inl_inject is_Fun_Fun_conv sum.simps(4) term.distinct(1) term.sel(2) wf_pterm.cases)
then have *:"to_pterm (lhs α) ⋅ ⟨As⟩⇩α = Pfun g (map (λt. t ⋅ ⟨As⟩⇩α) (map to_pterm ts))"
by simp
from 4(4) have l1:"length Bs = length (var_rule α)"
using wf_pterm.simps by fastforce
from 4(1,3) l1 have wellAs:"∀a ∈ set As. a ∈ wf_pterm R"
by (simp add: lhs_subst_args_wf_pterm)
from 4(4) have wellBs:"∀b ∈ set Bs. b ∈ wf_pterm R"
by blast
from 4(1) have l2:"length (zip As Bs) = length As"
by simp
with 4(1,2) wellAs wellBs have "∀i < length As. As ! i ⊔ Bs ! i ≠ None"
by (metis (mono_tags, lifting) case_prod_conv nth_mem nth_zip)
then have c:"∀i < length As. (∃C. As!i ⊔ Bs!i = Some C)"
by blast
from 4(1) have "∀i < length As. As!i ⊔ Bs!i = (map2 (⊔) As Bs)!i"
by simp
with c obtain Cs where "∀i < length As. As!i ⊔ Bs!i = Some (Cs!i)" and "length Cs = length As"
using exists_some_list l2 by (metis (no_types, lifting) length_map)
with 4 have cs:"those (map2 (⊔) As Bs) = Some Cs"
by (simp add: those_some)
have bs:"match (to_pterm (lhs α) ⋅ ⟨As⟩⇩α) (to_pterm (lhs α)) = Some (⟨As⟩⇩α)"
using lhs_subst_trivial by blast
have "(map (⟨As⟩⇩α) (var_rule α)) = As"
using 4(1) l1 apply_lhs_subst_var_rule by force
then show ?case using residual.simps(7) using bs cs g unfolding *
by simp
qed simp
context no_var_lhs
begin
lemma orth_imp_residual_defined:
assumes "A ⊥⇩p B" and "A ∈ wf_pterm R" and "B ∈ wf_pterm R"
shows "A re B ≠ None"
using orth_imp_residual_defined assms no_var_lhs by fastforce
lemma orth_imp_join_defined:
assumes "A ⊥⇩p B" and "A ∈ wf_pterm R" and "B ∈ wf_pterm R"
shows "A ⊔ B ≠ None"
using orth_imp_join_defined assms no_var_lhs by fastforce
lemma orthogonal_ctxt:
assumes "C⟨A⟩ ⊥⇩p C⟨B⟩" "C ∈ wf_pterm_ctxt R"
shows "A ⊥⇩p B"
using assms proof(induct C)
case (Cfun f ss1 C ss2)
from Cfun(2) have "∀i<length (ss1 @ C⟨A⟩ # ss2). (ss1 @ C⟨A⟩ # ss2) ! i ⊥⇩p (ss1 @ C⟨B⟩ # ss2) ! i"
unfolding intp_actxt.simps using orthogonal.simps by (smt (verit) is_Prule.simps(1) is_Prule.simps(3) term.distinct(1) term.sel(4))
then have "C⟨A⟩ ⊥⇩p C⟨B⟩"
by (metis append.right_neutral length_append length_greater_0_conv length_nth_simps(1) list.discI nat_add_left_cancel_less nth_append_length)
with Cfun(1,3) show ?case by auto
next
case (Crule α ss1 C ss2)
from Crule(3) obtain f ts where "lhs α = Fun f ts"
using no_var_lhs by (smt (verit, del_insts) Inl_inject Inr_not_Inl case_prodD actxt.distinct(1) actxt.inject term.collapse(2) wf_pterm_ctxt.simps)
with Crule(2) have "∀i<length (ss1 @ C⟨A⟩ # ss2). (ss1 @ C⟨A⟩ # ss2) ! i ⊥⇩p (ss1 @ C⟨B⟩ # ss2) ! i"
unfolding intp_actxt.simps using orthogonal.simps
by (smt (verit, ccfv_threshold) Inl_inject Inr_not_Inl eval_term.simps(2) term.distinct(1) term.inject(2) to_pterm.simps(2))
then have "C⟨A⟩ ⊥⇩p C⟨B⟩"
by (metis intp_actxt.simps(2) hole_pos.simps(2) hole_pos_poss nth_append_length poss_Cons_poss term.sel(4))
with Crule(1,3) show ?case by auto
qed simp
end
context left_lin_no_var_lhs
begin
lemma orthogonal_subst:
assumes "A ⋅ σ ⊥⇩p B ⋅ σ" "source A = source B"
and "A ∈ wf_pterm R" "B ∈ wf_pterm R"
shows "A ⊥⇩p B"
using assms(3,4,1,2) proof(induct A arbitrary:B rule:subterm_induct)
case (subterm A)
show ?case proof(cases A)
case (Var x)
with subterm no_var_lhs have "B = Var x"
by (metis Inl_inject Inr_not_Inl case_prodD co_initial_Var is_VarI term.distinct(1) term.inject(2) wf_pterm.simps)
then show ?thesis
unfolding Var by (simp add: orthogonal.intros(1))
next
case (Pfun f As)
with subterm(5) show ?thesis proof(cases B)
case (Pfun g Bs)
from subterm(5) have f:"f = g"
unfolding ‹A = Pfun f As› Pfun by simp
from subterm(5) have l:"length As = length Bs"
unfolding ‹A = Pfun f As› Pfun using map_eq_imp_length_eq by auto
{fix i assume i:"i < length As"
with subterm(4) have "As!i ⋅ σ ⊥⇩p Bs!i ⋅ σ"
unfolding ‹A = Pfun f As› Pfun eval_term.simps f
by (smt (verit) is_Prule.simps(1) is_Prule.simps(3) length_map nth_map orthogonal.simps term.distinct(1) term.sel(4))
moreover from i subterm(5) have "source (As!i) = source (Bs!i)"
unfolding ‹A = Pfun f As› Pfun eval_term.simps f by (simp add: map_equality_iff)
moreover from i l subterm(2,3) have "As!i ∈ wf_pterm R" "Bs!i ∈ wf_pterm R"
unfolding ‹A = Pfun f As› Pfun by auto
moreover from i have "As!i ⊲ A"
unfolding ‹A = Pfun f As› by simp
ultimately have "As!i ⊥⇩p Bs!i"
using subterm(1) by simp
}
with l show ?thesis
unfolding f ‹A = Pfun f As› Pfun by (simp add: orthogonal.intros(2))
next
case (Prule β Bs)
with subterm(3) have lin:"linear_term (lhs β)"
using left_lin left_linear_trs_def wf_pterm.cases by fastforce
from subterm(3) obtain g ts where lhs:"lhs β = Fun g ts"
unfolding Prule using no_var_lhs by (metis Inl_inject case_prodD is_FunE is_Prule.simps(1) is_Prule.simps(3) term.distinct(1) term.inject(2) wf_pterm.simps)
with subterm(4) obtain τ1 where "A ⋅ σ = to_pterm (lhs β) ⋅ τ1"
unfolding Prule Pfun eval_term.simps using orthogonal.simps by (smt (verit, ccfv_SIG) Inl_inject Inr_not_Inl term.inject(2))
with subterm(4,5) obtain τ where τ2:"A = to_pterm (lhs β) ⋅ τ"
unfolding Prule Pfun source.simps using simple_pterm_match lin by (metis matches_iff source.simps(2))
let ?As="map τ (var_rule β)"
have l:"length Bs = length (var_rule β)"
using Prule subterm.prems(2) wf_pterm.simps by fastforce
from τ2 have A:"A = to_pterm (lhs β) ⋅ ⟨?As⟩⇩β"
by (metis lhs_subst_var_rule set_vars_term_list subsetI vars_to_pterm)
{fix i assume i:"i < length Bs"
have subt:"?As!i ⊲ A"
using i l by (metis (no_types, lifting) τ2 comp_apply lhs nth_map nth_mem set_remdups set_rev set_vars_term_list subst_image_subterm to_pterm.simps(2) vars_to_pterm)
have wf:"?As!i ∈ wf_pterm R"
using i l by (metis A length_map lhs_subst_args_wf_pterm nth_mem subterm.prems(1))
have l':"length (var_rule β) = length ?As"
by simp
from subterm(4) A Prule lhs have orth:"?As!i ⋅ σ ⊥⇩p Bs!i ⋅ σ" proof(cases)
case (4 As' Bs' β')
then have Bs':"Bs' = map (λs. s ⋅ σ) Bs" and β':"β' = β"
unfolding Prule by simp_all
have As':"As' = map (λs. s ⋅ σ) ?As" proof-
have l'':"length As' = length ?As" using 4(3) l unfolding Bs' length_map by simp
{fix j assume j:"j < length As'" and neq:"As'!j ≠ map (λs. s ⋅ σ) ?As ! j"
let ?x="var_rule β!j"
from j have x:"?x ∈ vars_term (lhs β)"
by (metis comp_apply l' l'' nth_mem set_remdups set_rev set_vars_term_list)
then obtain p where p:"p ∈ poss (lhs β)" "lhs β |_p = Var ?x"
by (meson vars_term_poss_subt_at)
from j have 1:"(⟨As'⟩⇩β') ?x = As'!j"
using β' l'' lhs_subst_var_i by force
from j have 2:"(⟨map (λs. s ⋅ σ) ?As⟩⇩β) ?x = map (λs. s ⋅ σ) ?As ! j"
using lhs_subst_var_i by (metis l'' length_map)
then have False using 4(1) 1 2 p unfolding A eval_lhs_subst[OF l'] β'
by (smt (verit, del_insts) x neq set_vars_term_list term_subst_eq_rev vars_to_pterm)
}
then show ?thesis
using l'' by (metis (mono_tags, lifting) map_nth_eq_conv nth_map)
qed
have i':"i < length (zip (map (λa. a ⋅ σ) (map τ (var_rule β))) (map (λb. b ⋅ σ) Bs))"
using i l by simp
from 4(4) have "map (λa. a ⋅ σ) (map τ (var_rule β)) ! i ⊥⇩p map (λb. b ⋅ σ) Bs !i"
unfolding As' Bs' using i' by (metis case_prodD i l length_map nth_mem nth_zip)
then show ?thesis
using i l by auto
qed simp_all
have co_init:"source (?As!i) = source (Bs!i)" proof(rule ccontr)
assume neq:"source (?As!i) ≠ source (Bs!i)"
let ?x="var_rule β!i"
from i l have x:"?x ∈ vars_term (lhs β)"
by (metis comp_apply nth_mem set_remdups set_rev set_vars_term_list)
then obtain p where p:"p ∈ poss (lhs β)" "lhs β |_p = Var ?x"
by (meson vars_term_poss_subt_at)
from i have 1:"(⟨map source ?As⟩⇩β) ?x = source (?As!i)"
using l lhs_subst_var_i by (metis length_map nth_map)
from i have 2:"(⟨map source Bs⟩⇩β) ?x = source (Bs!i)"
using l lhs_subst_var_i by (metis length_map nth_map)
from subterm(5) show False using neq 1 2 p
unfolding Prule A source.simps source_apply_subst[OF to_pterm_wf_pterm[of "lhs β"]] source_to_pterm
using term_subst_eq_rev x by fastforce
qed
from subterm(1) subt wf orth co_init have "?As!i ⊥⇩p Bs!i"
using i subterm(3) unfolding Prule by (meson fun_well_arg nth_mem)
}
then show ?thesis unfolding A Prule
by (smt (verit, best) case_prodI2 in_set_idx l length_map length_zip min_less_iff_conj nth_zip orthogonal.intros(4) prod.sel(1) snd_conv)
qed simp
next
case (Prule α As)
with subterm(2) have lin:"linear_term (lhs α)"
using left_lin left_linear_trs_def wf_pterm.cases by fastforce
from subterm(2) obtain f ts where lhs:"lhs α = Fun f ts"
by (metis Inr_not_Inl Prule case_prodD is_FunE no_var_lhs sum.inject(1) term.distinct(1) term.inject(2) wf_pterm.simps)
with subterm(5) show ?thesis proof(cases B)
case (Var x)
then show ?thesis
using source_orthogonal subterm.prems(4) by fastforce
next
case (Pfun g Bs)
with subterm(4) obtain τ1 where "B ⋅ σ = to_pterm (lhs α) ⋅ τ1"
unfolding Prule Pfun eval_term.simps using orthogonal.simps by (smt (verit, ccfv_SIG) Inl_inject Inr_not_Inl term.inject(2))
with subterm(4,5) obtain τ where τ2:"B = to_pterm (lhs α) ⋅ τ"
unfolding Prule Pfun source.simps using simple_pterm_match lin by (metis matches_iff source.simps(2))
let ?Bs="map τ (var_rule α)"
have l:"length As = length (var_rule α)"
using Prule subterm.prems(1) wf_pterm.simps by fastforce
from τ2 have B:"B = to_pterm (lhs α) ⋅ ⟨?Bs⟩⇩α"
by (metis lhs_subst_var_rule set_vars_term_list subsetI vars_to_pterm)
have l':"length (var_rule α) = length ?Bs"
by simp
{fix i assume i:"i < length As"
from subterm(4) B Prule lhs have orth:"As!i ⋅ σ ⊥⇩p ?Bs!i ⋅ σ" proof(cases)
case (3 As' Bs' α')
then have As':"As' = map (λs. s ⋅ σ) As" and α':"α' = α"
unfolding Prule by simp_all
have Bs':"Bs' = map (λs. s ⋅ σ) ?Bs" proof-
have l'':"length Bs' = length ?Bs" using 3(3) l unfolding As' length_map by simp
{fix j assume j:"j < length Bs'" and neq:"Bs'!j ≠ map (λs. s ⋅ σ) ?Bs ! j"
let ?x="var_rule α!j"
from j have x:"?x ∈ vars_term (lhs α)"
by (metis comp_apply l'' length_map nth_mem set_remdups set_rev set_vars_term_list)
then obtain p where p:"p ∈ poss (lhs α)" "lhs α |_p = Var ?x"
by (meson vars_term_poss_subt_at)
from j have 1:"(⟨Bs'⟩⇩α') ?x = Bs'!j"
using α' l'' lhs_subst_var_i by force
from j have 2:"(⟨map (λs. s ⋅ σ) ?Bs⟩⇩α) ?x = map (λs. s ⋅ σ) ?Bs ! j"
using lhs_subst_var_i by (metis l'' length_map)
then have False using 3(1) 1 2 p unfolding B eval_lhs_subst[OF l'] α'
by (smt (verit, ccfv_SIG) "3"(2) B α' eval_lhs_subst l' map_eq_conv neq set_vars_term_list term_subst_eq_rev vars_to_pterm x)
}
then show ?thesis
using l'' by (metis (mono_tags, lifting) map_nth_eq_conv nth_map)
qed
have i':"i < length (zip (map (λb. b ⋅ σ) As) (map (λa. a ⋅ σ) (map τ (var_rule α))))"
using i l by simp
from 3(4) have "map (λb. b ⋅ σ) As ! i ⊥⇩p map (λa. a ⋅ σ) (map τ (var_rule α)) ! i "
unfolding As' Bs' using i' by (metis case_prodD i l length_map nth_mem nth_zip)
then show ?thesis
using i l by auto
qed simp_all
have co_init:"source (As!i) = source (?Bs!i)" proof(rule ccontr)
assume neq:"source (As!i) ≠ source (?Bs!i)"
let ?x="var_rule α!i"
from i l have x:"?x ∈ vars_term (lhs α)"
by (metis comp_apply nth_mem set_remdups set_rev set_vars_term_list)
then obtain p where p:"p ∈ poss (lhs α)" "lhs α |_p = Var ?x"
by (meson vars_term_poss_subt_at)
from i have 1:"(⟨map source ?Bs⟩⇩α) ?x = source (?Bs!i)"
using l lhs_subst_var_i by (metis length_map nth_map)
from i have 2:"(⟨map source As⟩⇩α) ?x = source (As!i)"
using l lhs_subst_var_i by (metis length_map nth_map)
from subterm(5) show False using neq 1 2 p
unfolding Prule B source.simps source_apply_subst[OF to_pterm_wf_pterm[of "lhs α"]] source_to_pterm
using term_subst_eq_rev x by fastforce
qed
from subterm(1,2,3) co_init have "As!i ⊥⇩p ?Bs!i"
using i l' orth unfolding Prule by (metis B fun_well_arg l lhs_subst_args_wf_pterm nth_mem orth supt.arg)
}
then show ?thesis unfolding B Prule
by (smt (verit, best) case_prodI2 fst_conv in_set_zip l l' orthogonal.intros(3) snd_conv)
next
case (Prule β Bs)
from subterm(4) have α:"α = β"
unfolding Prule ‹A = Prule α As› eval_term.simps using orthogonal.simps
by (smt (verit) Inl_inject Prule eval_term.simps(2) is_Prule.simps(1) is_Prule.simps(3) lhs no_var_lhs.lhs_is_Fun
no_var_lhs_axioms subterm.prems(2) term.collapse(2) term.sel(2) to_pterm.simps(2))
from subterm(2,3) have l:"length As = length Bs"
unfolding ‹A = Prule α As› Prule using α length_args_well_Prule by blast
{fix i assume i:"i < length As"
with subterm(4) have "As!i ⋅ σ ⊥⇩p Bs!i ⋅ σ"
unfolding ‹A = Prule α As› Prule eval_term.simps α by (smt (verit, ccfv_threshold) Inl_inject
Inr_not_Inl α eval_term.simps(2) length_map lhs nth_map orthogonal.simps term.distinct(1) term.inject(2) to_pterm.simps(2))
moreover from i subterm(5) have "source (As!i) = source (Bs!i)"
using Prule α ‹A = Prule α As› co_init_prule subterm.prems(1) subterm.prems(2) by blast
moreover from i l subterm(2,3) have "As!i ∈ wf_pterm R" "Bs!i ∈ wf_pterm R"
unfolding Prule ‹A = Prule α As› by auto
moreover from i have "As!i ⊲ A"
unfolding ‹A = Prule α As› by simp
ultimately have "As!i ⊥⇩p Bs!i"
using subterm(1) by simp
}
with l show ?thesis
unfolding α ‹A = Prule α As› Prule by (simp add: orthogonal.intros(2))
qed
qed
qed
end
end