Theory Bot_Terms

theory Bot_Terms
  imports Utils

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"
  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) 
  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))

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