Theory First_Order_Terms.Subsumption

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
License: LGPL
*)
section ‹Subsumption›

text ‹We define the subsumption relation on terms and prove its well-foundedness.›

theory Subsumption
  imports
    Term
    "Abstract-Rewriting.Seq"
    "HOL-Library.Adhoc_Overloading"
    Fun_More
    Seq_More
begin

consts
  SUBSUMESEQ :: "'a ⇒ 'a ⇒ bool" (infix ‹≤⋅› 50) 
  SUBSUMES :: "'a ⇒ 'a ⇒ bool" (infix ‹<⋅› 50)
  LITSIM :: "'a ⇒ 'a ⇒ bool" (infix ‹≐› 50)

abbreviation (input) INSTANCEQ (infix ‹⋅≥› 50)
  where
    "x ⋅≥ y ≡ y ≤⋅ x"

abbreviation (input) INSTANCE (infix ‹⋅>› 50)
  where
    "x ⋅> y ≡ y <⋅ x"

abbreviation INSTANCEEQ_SET (‹{⋅≥}›)
  where
    "{⋅≥} ≡ {(x, y). y ≤⋅ x}"

abbreviation INSTANCE_SET (‹{⋅>}›)
  where
    "{⋅>} ≡ {(x, y). y <⋅ x}"

abbreviation SUBSUMESEQ_SET (‹{≤⋅}›)
  where
    "{≤⋅} ≡ {(x, y). x ≤⋅ y}"

abbreviation SUBSUMES_SET (‹{<⋅}›)
  where
    "{<⋅} ≡ {(x, y). x <⋅ y}"

abbreviation LITSIM_SET (‹{≐}›)
  where
    "{≐} ≡ {(x, y). x ≐ y}"

locale subsumable =
  fixes subsumeseq :: "'a ⇒ 'a ⇒ bool"
  assumes refl: "subsumeseq x x"
    and trans: "subsumeseq x y ⟹ subsumeseq y z ⟹ subsumeseq x z"
begin

adhoc_overloading
  SUBSUMESEQ subsumeseq

definition "subsumes t s ⟷ t ≤⋅ s ∧ ¬ s ≤⋅ t"

definition "litsim s t ⟷ s ≤⋅ t ∧ t ≤⋅ s"

adhoc_overloading
  SUBSUMES subsumes and
  LITSIM litsim

lemma litsim_refl [simp]:
  "s ≐ s"
  by (auto simp: litsim_def refl)

lemma litsim_sym:
  "s ≐ t ⟹ t ≐ s"
  by (auto simp: litsim_def)

lemma litsim_trans:
  "s ≐ t ⟹ t ≐ u ⟹ s ≐ u"
  by (auto simp: litsim_def dest: trans)

end

sublocale subsumable ⊆ subsumption: preorder "(≤⋅)" "(<⋅)"
  by (unfold_locales) (auto simp: subsumes_def refl elim: trans)

inductive subsumeseq_term :: "('a, 'b) term ⇒ ('a, 'b) term ⇒ bool"
  where
    [intro]: "t = s ⋅ σ ⟹ subsumeseq_term s t"

adhoc_overloading
  SUBSUMESEQ subsumeseq_term

lemma subsumeseq_termE [elim]:
  assumes "s ≤⋅ t"
  obtains σ where "t = s ⋅ σ"
  using assms by (cases)

lemma subsumeseq_term_refl:
  fixes t :: "('a, 'b) term"
  shows "t ≤⋅ t"
  by (rule subsumeseq_term.intros [of t t Var]) simp

lemma subsumeseq_term_trans:
  fixes s t u :: "('a, 'b) term"
  assumes "s ≤⋅ t" and "t ≤⋅ u"
  shows "s ≤⋅ u"
proof -
  obtain σ τ
    where [simp]: "t = s ⋅ σ" "u = t ⋅ τ" using assms by fastforce
  show ?thesis
    by (rule subsumeseq_term.intros [of _ _ "σ ∘⇩s τ"]) simp
qed

interpretation term_subsumable: subsumable subsumeseq_term
  by standard (force simp: subsumeseq_term_refl dest: subsumeseq_term_trans)+

adhoc_overloading
  SUBSUMES term_subsumable.subsumes and
  LITSIM term_subsumable.litsim

lemma subsumeseq_term_iff:
  "s ⋅≥ t ⟷ (∃σ. s = t ⋅ σ)"
  by auto

fun num_syms :: "('f, 'v) term ⇒ nat"
  where
    "num_syms (Var x) = 1" |
    "num_syms (Fun f ts) = Suc (sum_list (map num_syms ts))"

fun num_vars :: "('f, 'v) term ⇒ nat"
  where
    "num_vars (Var x) = 1" |
    "num_vars (Fun f ts) = sum_list (map num_vars ts)"

definition num_unique_vars :: "('f, 'v) term ⇒ nat"
  where
    "num_unique_vars t = card (vars_term t)"

lemma num_syms_1: "num_syms t ≥ 1"
  by (induct t) auto

lemma num_syms_subst:
  "num_syms (t ⋅ σ) ≥ num_syms t"
  using num_syms_1
  by (induct t) (auto, metis comp_apply sum_list_mono)


subsection ‹Equality of terms modulo variables›

inductive emv where
  Var [simp, intro!]: "emv (Var x) (Var y)" |
  Fun [intro]: "⟦f = g; length ss = length ts; ∀i < length ts. emv (ss ! i) (ts ! i)⟧ ⟹
    emv (Fun f ss) (Fun g ts)"

lemma sum_list_map_num_syms_subst:
  assumes "sum_list (map (num_syms ∘ (λt. t ⋅ σ)) ts) = sum_list (map num_syms ts)"
  shows "∀i < length ts. num_syms (ts ! i ⋅ σ) = num_syms (ts ! i)"
  using assms
proof (induct ts)
  case (Cons t ts)
  then have "num_syms (t ⋅ σ) + sum_list (map (num_syms ∘ (λt. t ⋅ σ)) ts)
    = num_syms t + sum_list (map num_syms ts)" by (simp add: o_def)
  moreover have "num_syms (t ⋅ σ) ≥ num_syms t" by (metis num_syms_subst)
  moreover have "sum_list (map (num_syms ∘ (λt. t ⋅ σ)) ts) ≥ sum_list (map num_syms ts)"
    using num_syms_subst [of _ σ] by (induct ts) (auto intro: add_mono)
  ultimately show ?case using Cons by (auto) (case_tac i, auto)
qed simp

lemma subst_size_emv:
  assumes "s = t ⋅ τ" and "num_syms s = num_syms t" and "num_funs s = num_funs t"
  shows "emv s t"
  using assms
proof (induct t arbitrary: s)
  case (Var x)
  then show ?case by (force elim: num_funs_0)
next
  case (Fun g ts)
  note IH = this
  show ?case
  proof (cases s)
    case (Var x)
    then show ?thesis using Fun by simp
  next
    case (Fun f ss)
    from IH(2-) [unfolded Fun]
      and sum_list_map_num_syms_subst [of τ ts]
      and sum_list_map_num_funs_subst [of τ ts]
    have "∀i < length ts. num_syms (ts ! i  ⋅ τ) = num_syms (ts ! i)"
      and "∀i < length ts. num_funs (ts ! i ⋅ τ) = num_funs (ts ! i)"
      by auto
    with Fun and IH show ?thesis by auto
  qed
qed

lemma subsumeseq_term_size_emv:
  assumes "s ⋅≥ t" and "num_syms s = num_syms t" and "num_funs s = num_funs t"
  shows "emv s t"
  using assms(1) and subst_size_emv [OF _ assms(2-)] by (cases) simp

lemma emv_subst_vars_term:
  assumes "emv s t"
    and "s = t ⋅ σ"
  shows "vars_term s = (the_Var ∘ σ) ` vars_term t"
  using assms [unfolded subsumeseq_term_iff]
  apply (induct)
   apply (auto simp: in_set_conv_nth iff: image_iff)
   apply (metis nth_mem)
  by (metis comp_apply imageI nth_mem)

lemma emv_subst_imp_num_unique_vars_le:
  assumes "emv s t"
    and "s = t ⋅ σ"
  shows "num_unique_vars s ≤ num_unique_vars t"
  using emv_subst_vars_term [OF assms]
  apply (simp add: num_unique_vars_def)
  by (metis card_image_le finite_vars_term)

lemma emv_subsumeseq_term_imp_num_unique_vars_le:
  assumes "emv s t"
    and "s ⋅≥ t"
  shows "num_unique_vars s ≤ num_unique_vars t"
  using assms(2) and emv_subst_imp_num_unique_vars_le [OF assms(1)] by (cases) simp

lemma num_syms_geq_num_vars:
  "num_syms t ≥ num_vars t"
proof (induct t)
  case (Fun f ts)
  with sum_list_mono [of ts num_vars num_syms]
  have "sum_list (map num_vars ts) ≤ sum_list (map num_syms ts)" by simp
  then show ?case by simp
qed simp

lemma num_unique_vars_Fun_Cons:
  "num_unique_vars (Fun f (t # ts)) ≤ num_unique_vars t + num_unique_vars (Fun f ts)"
  apply (simp_all add: num_unique_vars_def)
  unfolding card_Un_Int [OF finite_vars_term finite_Union_vars_term]
  apply simp
  done

lemma sum_list_map_unique_vars:
  "sum_list (map num_unique_vars ts) ≥ num_unique_vars (Fun f ts)"
proof (induct ts)
  case (Cons t ts)
  with num_unique_vars_Fun_Cons [of f t ts]
  show ?case by simp
qed (simp add: num_unique_vars_def)

lemma num_unique_vars_Var_1 [simp]:
  "num_unique_vars (Var x) = 1"
  by (simp_all add: num_unique_vars_def)

lemma num_vars_geq_num_unique_vars:
  "num_vars t ≥ num_unique_vars t"
proof -
  note * =
    sum_list_mono [of _ num_unique_vars num_vars, THEN sum_list_map_unique_vars [THEN le_trans]]
  show ?thesis by (induct t) (auto intro: *)
qed

lemma num_syms_ge_num_unique_vars:
  "num_syms t ≥ num_unique_vars t"
  by (metis le_trans num_syms_geq_num_vars num_vars_geq_num_unique_vars)

lemma num_syms_num_unique_vars_clash:
  assumes "∀i. num_syms (f i) = num_syms (f (Suc i))"
    and "∀i. num_unique_vars (f i) < num_unique_vars (f (Suc i))"
  shows False
proof -
  have *: "∀i j. i ≤ j ⟶ num_syms (f i) = num_syms (f j)"
  proof (intro allI impI)
    fix i j :: nat
    assume "i ≤ j"
    then show "num_syms (f i) = num_syms (f j)"
      using assms(1)
      apply (induct "j - i" arbitrary: i)
       apply auto
      by (metis Suc_diff_diff diff_zero less_eq_Suc_le order.not_eq_order_implies_strict)
  qed
  have "∃i. num_unique_vars (f i) ≥ num_syms (f 0)"
    using inc_seq_greater [OF assms(2), of "num_syms (f 0)"] by (metis nat_less_le)
  then obtain i where "num_unique_vars (f i) ≥ num_syms (f 0)" by auto
  with * and assms(2) have "num_unique_vars (f (Suc i)) > num_syms (f (Suc i))"
    by (metis le0 le_antisym num_syms_ge_num_unique_vars)
  then show False
    by (metis less_Suc_eq_le not_less_eq num_syms_ge_num_unique_vars)
qed

lemma emv_subst_imp_is_Var:
  assumes "emv s t"
    and "s = t ⋅ σ"
  shows "∀x ∈ vars_term t. is_Var (σ x)"
  using assms
  apply (induct)
   apply auto
  by (metis in_set_conv_nth)

lemma bij_Var_subst_compose_Var:
  assumes "bij g"
  shows "(Var ∘ g) ∘⇩s (Var ∘ inv g) = Var"
proof
  fix x
  show "((Var ∘ g) ∘⇩s (Var ∘ inv g)) x = Var x"
    using assms
    apply (auto simp: eval_subst_def)
    by (metis UNIV_I bij_is_inj inv_into_f_f)
qed

subsection ‹Well-foundedness›

lemma wf_subsumes:
  "wf ({<⋅} :: ('f, 'v) term rel)"
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain f :: "('f, 'v) term seq"
    where strict: "∀i. f i ⋅> f (Suc i)"
    by (metis mem_Collect_eq case_prodD wf_iff_no_infinite_down_chain)
  then have *: "∀i. f i ⋅≥ f (Suc i)" by (metis term_subsumable.subsumption.less_imp_le)
  then have "∀i. num_syms (f i) ≥ num_syms (f (Suc i))"
    by (auto simp: subsumeseq_term_iff) (metis num_syms_subst)
  from down_chain_imp_eq [OF this] obtain N
    where N_syms: "∀i > N. num_syms (f i) = num_syms (f (Suc i))" ..
  define g where "g i = f (i + N)" for i
  from * have "∀i. num_funs (g i) ≥ num_funs (g (Suc i))"
    by (auto simp: subsumeseq_term_iff g_def) (metis num_funs_subst)
  from down_chain_imp_eq [OF this] obtain K
    where K_funs: "∀i > K. num_funs (g i) = num_funs (g (Suc i))" ..
  define M where "M = max K N"
  have strict_g: "∀i > M. g i ⋅> g (Suc i)" using strict by (simp add: g_def M_def)
  have g: "∀i > M. g i ⋅≥ g (Suc i)" using * by (simp add: g_def M_def)
  moreover have "∀i > M. num_funs (g i) = num_funs (g (Suc i))"
    using K_funs unfolding M_def by (metis max_less_iff_conj)
  moreover have syms: "∀i > M. num_syms (g i) = num_syms (g (Suc i))"
    using N_syms unfolding M_def g_def
    by (metis add_Suc_right add_lessD1 add_strict_left_mono add.commute)
  ultimately have emv: "∀i > M. emv (g i) (g (Suc i))" by (metis subsumeseq_term_size_emv)
  then have "∀i > M. num_unique_vars (g (Suc i)) ≥ num_unique_vars (g i)"
    using emv_subsumeseq_term_imp_num_unique_vars_le and g by fast
  then obtain i where "i > M"
    and nuv: "num_unique_vars (g (Suc i)) = num_unique_vars (g i)"
    using num_syms_num_unique_vars_clash [of "λi. g (i + Suc M)"] and syms
    by (metis add_Suc_right add_Suc_shift le_eq_less_or_eq less_add_Suc2)
  define s and t where "s = g i" and "t = g (Suc i)"
  from nuv have card: "card (vars_term s) = card (vars_term t)"
    by (simp add: num_unique_vars_def s_def t_def)
  from g [THEN spec, THEN mp, OF ‹i > M›] obtain σ
    where "s = t ⋅ σ" by (cases) (auto simp: s_def t_def)
  then have "emv s t" and "vars_term s = (the_Var ∘ σ) ` vars_term t"
    using emv_subst_vars_term [of s t σ] and emv and ‹i > M› by (auto simp: s_def t_def)
  with card have "card ((the_Var ∘ σ) ` vars_term t) = card (vars_term t)" by simp
  from finite_card_eq_imp_bij_betw [OF finite_vars_term this]
  have "bij_betw (the_Var ∘ σ) (vars_term t) ((the_Var ∘ σ) ` vars_term t)" .

  from bij_betw_extend [OF this, of UNIV]
  obtain h where *: "∀x∈vars_term t. h x = (the_Var ∘ σ) x"
    and "finite {x. h x ≠ x}"
    and "bij h" by auto
  have "∀x∈vars_term t. (Var ∘ h) x = σ x"
  proof
    fix x
    assume "x ∈ vars_term t"
    with * have "h x = (the_Var ∘ σ) x" by simp
    with emv_subst_imp_is_Var [OF ‹emv s t› ‹s = t ⋅ σ›] ‹x ∈ vars_term t›
    show "(Var ∘ h) x = σ x" by simp
  qed
  then have "t ⋅ (Var ∘ h) = s"
    using ‹s = t ⋅ σ› by (auto simp: term_subst_eq_conv)
  then have "t ⋅ (Var ∘ h) ∘⇩s (Var ∘ inv h) = s ⋅ (Var ∘ inv h)" by auto
  then have "t = s ⋅ (Var ∘ inv h)"
    unfolding bij_Var_subst_compose_Var [OF ‹bij h›] by simp
  then have "t ⋅≥ s" by auto
  with strict_g and ‹i > M› show False by (auto simp: s_def t_def term_subsumable.subsumes_def)
qed

end