Theory 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: subst_compose_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 *: "xvars_term t. h x = (the_Var  σ) x"
    and "finite {x. h x  x}"
    and "bij h" by auto
  have "xvars_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