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