# Theory Bot_Terms

```theory Bot_Terms
imports Utils
begin

subsection ‹Bottom terms›

datatype 'f bot_term = Bot | BFun 'f (args: "'f bot_term list")

fun term_to_bot_term :: "('f, 'v) term ⇒ 'f bot_term"  ("_⇧⊥" [80] 80) where
"(Var _)⇧⊥ = Bot"
| "(Fun f ts)⇧⊥ = BFun f (map term_to_bot_term ts)"

fun root_bot where
"root_bot Bot = None" |
"root_bot (BFun f ts) = Some (f, length ts)"

fun funas_bot_term where
"funas_bot_term Bot = {}"
| "funas_bot_term (BFun f ss) = {(f, length ss)} ∪ (⋃ (funas_bot_term ` set ss))"

lemma finite_funas_bot_term:
"finite (funas_bot_term t)"
by (induct t) auto

lemma funas_bot_term_funas_term:
"funas_bot_term (t⇧⊥) = funas_term t"
by (induct t) auto

lemma term_to_bot_term_root_bot [simp]:
"root_bot (t⇧⊥) = root t"
by (induct t) auto

lemma term_to_bot_term_root_bot_comp [simp]:
"root_bot ∘ term_to_bot_term = root"
using term_to_bot_term_root_bot by force

inductive_set mergeP where
base_l [simp]: "(Bot, t) ∈ mergeP"
| base_r [simp]: "(t, Bot) ∈ mergeP"
| step [intro]: "length ss = length ts ⟹ (∀ i < length ts. (ss ! i, ts ! i) ∈ mergeP) ⟹
(BFun f ss, BFun f ts) ∈ mergeP"

lemma merge_refl:
"(s, s) ∈ mergeP"
by (induct s) auto

lemma merge_symmetric:
assumes "(s, t) ∈ mergeP"
shows "(t, s) ∈ mergeP"
using assms by induct auto

fun merge_terms :: "'f bot_term ⇒ 'f bot_term ⇒ 'f bot_term"  (infixr "↑" 67) where
"Bot ↑ s = s"
| "s ↑ Bot = s"
| "(BFun f ss) ↑ (BFun g ts) = (if f = g ∧ length ss = length ts
then BFun f (map (case_prod (↑)) (zip ss ts))
else undefined)"

lemma merge_terms_bot_rhs[simp]:
"s ↑ Bot = s" by (cases s) auto

lemma merge_terms_idem: "s ↑ s = s"
by (induct s) (auto simp add: map_nth_eq_conv)

lemma merge_terms_assoc [ac_simps]:
assumes "(s, t) ∈ mergeP" and "(t, u) ∈ mergeP"
shows "(s ↑ t) ↑ u = s ↑ t ↑ u"
using assms by (induct s t arbitrary: u) (auto elim!: mergeP.cases intro!: nth_equalityI)

lemma merge_terms_commutative [ac_simps]:
shows "s ↑ t = t ↑ s"
by (induct s t rule: merge_terms.induct)
(fastforce simp: in_set_conv_nth intro!: nth_equalityI)+

lemma merge_dist:
assumes "(s, t ↑ u) ∈ mergeP" and "(t, u) ∈ mergeP"
shows "(s, t) ∈ mergeP" using assms
by (induct t arbitrary: s u) (auto elim!: mergeP.cases, metis mergeP.step nth_mem)

lemma megeP_ass:
"(s, t ↑ u) ∈ mergeP ⟹ (t, u) ∈ mergeP ⟹ (s ↑ t, u) ∈ mergeP"
by (induct t arbitrary: s u) (auto simp: mergeP.step elim!: mergeP.cases)

inductive_set bless_eq where
base_l [simp]: "(Bot, t) ∈ bless_eq"
| step [intro]: "length ss = length ts ⟹ (∀ i < length ts. (ss ! i, ts ! i) ∈ bless_eq) ⟹
(BFun f ss, BFun f ts) ∈ bless_eq"

text ‹Infix syntax.›
abbreviation "bless_eq_pred s t ≡ (s, t) ∈ bless_eq"
notation
bless_eq ("{≤⇩b}") and
bless_eq_pred ("(_/ ≤⇩b _)" [56, 56] 55)

lemma BFun_leq_Bot_False [simp]:
"BFun f ts ≤⇩b Bot ⟷ False"
using bless_eq.cases by auto

lemma BFun_lesseqE [elim]:
assumes "BFun f ts ≤⇩b t"
obtains us where "length ts = length us" "t = BFun f us"
using assms bless_eq.cases by blast

lemma bless_eq_refl: "s ≤⇩b s"
by (induct s) auto

lemma bless_eq_trans [trans]:
assumes "s ≤⇩b t" and "t ≤⇩b u"
shows "s ≤⇩b u" using assms
proof (induct arbitrary: u)
case (step ss ts f)
from step(3) obtain us where [simp]: "u = BFun f us" "length ts = length us" by auto
from step(3, 1, 2) have "i < length ss ⟹ ss ! i ≤⇩b us ! i" for i
by (cases rule: bless_eq.cases) auto
then show ?case using step(1) by auto
qed auto

lemma bless_eq_anti_sym:
"s ≤⇩b t ⟹ t ≤⇩b s ⟹ s = t"
by (induct rule: bless_eq.induct) (auto elim!: bless_eq.cases intro: nth_equalityI)

lemma bless_eq_mergeP:
"s ≤⇩b t ⟹ (s, t) ∈ mergeP"
by (induct s arbitrary: t) (auto elim!: bless_eq.cases)

lemma merge_bot_args_bless_eq_merge:
assumes "(s, t) ∈ mergeP"
shows "s ≤⇩b s ↑ t" using assms
by (induct s arbitrary: t) (auto simp: bless_eq_refl elim!: mergeP.cases intro!: step)

lemma bless_eq_closued_under_merge:
assumes "(s, t) ∈ mergeP" "(u, v) ∈ mergeP" "s ≤⇩b u" "t ≤⇩b v"
shows "s ↑ t ≤⇩b u ↑ v" using assms(3, 4, 1, 2)
proof (induct arbitrary: t v)
case (base_l t)
then show ?case using bless_eq_trans merge_bot_args_bless_eq_merge
by (metis merge_symmetric merge_terms.simps(1) merge_terms_commutative)
next
case (step ss ts f)
then show ?case apply (auto elim!: mergeP.cases intro!: bless_eq.step)
using bless_eq_trans merge_bot_args_bless_eq_merge apply blast
by (metis bless_eq.cases bot_term.distinct(1) bot_term.sel(2))
qed

lemma bless_eq_closued_under_supremum:
assumes "s ≤⇩b u" "t ≤⇩b u"
shows "s ↑ t ≤⇩b u" using assms
by (induct arbitrary: t) (auto elim!: bless_eq.cases intro!: bless_eq.step)

lemma linear_term_comb_subst:
assumes "linear_term (Fun f ss)"
and "length ss = length ts"
and "⋀ i. i < length ts ⟹ ss ! i ⋅ σ i = ts ! i"
shows "∃ σ. Fun f ss ⋅ σ = Fun f ts"
using assms subst_merge[of ss "σ"]
apply auto apply (rule_tac x = σ' in exI)
apply (intro nth_equalityI) apply auto
by (metis term_subst_eq)

lemma bless_eq_to_instance:
assumes "s⇧⊥ ≤⇩b t⇧⊥" and "linear_term s"
shows "∃ σ. s ⋅ σ = t" using assms
proof (induct s arbitrary: t)
case (Fun f ts)
from Fun(2) obtain us where [simp]: "t = Fun f us" "length ts = length us" by (cases t) auto
have "i < length ts ⟹ ∃σ. ts ! i ⋅ σ = us ! i" for i
using Fun(2, 3) Fun(1)[OF nth_mem, of i "us ! i" for i]
by (auto elim: bless_eq.cases)
then show ?case using Ex_list_of_length_P[of "length ts" "λ σ i. ts ! i ⋅ σ = us ! i"]
using linear_term_comb_subst[OF Fun(3)] by auto
qed auto

lemma instance_to_bless_eq:
assumes "s ⋅ σ = t"
shows "s⇧⊥ ≤⇩b t⇧⊥" using assms
proof (induct s arbitrary: t)
case (Fun f ts) then show ?case
by (cases t) auto
qed auto

end```