Theory Lambda_Encoding_KBO

(*  Title:       Properties of Lambda-Free KBO on the Lambda Encoding
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2019
    Maintainer:  Jasmin Blanchette <j.c.blanchette at vu.nl>
*)

section ‹Properties of Lambda-Free KBO on the Lambda Encoding›

theory Lambda_Encoding_KBO
imports Lambda_Free_RPOs.Lambda_Encoding Lambda_Free_KBO_Basic
begin

text ‹
This theory explores the properties of the ‹λ›-free KBO on the proposed encoding of ‹λ›-expressions.
›

locale kbo_lambda_encoding = kbo_basic _ _ _ _ "λ_ :: 'v. UNIV :: 's set" + lambda_encoding lam
  for lam :: 's +
  assumes
    gt_db_db: "j > i ⟹ db j >s db i" and
    wt_db_db: "wt_sym (db j) = wt_sym (db i)"
begin

notation gt (infix ">t" 50)
notation gt_hd (infix ">hd" 50)

abbreviation ge :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix "≥t" 50) where
  "t ≥t s ≡ t >t s ∨ t = s"

lemma wary_raw_db_subst: "wary_subst (raw_db_subst i x)"
  unfolding wary_subst_def by (simp add: arity_def)

lemma wt_subst_db: "wt (subst_db i x s) = wt (subst (raw_db_subst j x) s)"
  by (induct s arbitrary: i j)
    (clarsimp simp: raw_db_subst_def wt_db_db split: hd.splits,
      metis lambda_encoding.subst_db.simps(2) subst.simps(2) wt.simps(2))

lemma subst_db_Suc_ge: "subst_db (Suc i) x s ≥t subst_db i x s"
proof (induct s arbitrary: i)
  case (Hd x)
  then show ?case
    by (auto intro: gt_diff simp: wt_db_db gt_db_db gt_sym_imp_hd)
next
  case (App s1 s2)
  show ?case
    by (simp, safe)
      (metis (full_types) App.hyps(1) App.hyps(2) gt_compat_arg gt_compat_fun gt_trans)+
qed

lemma gt_subst_db: "t >t s ⟹ subst_db i x t >t subst_db i x s"
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "λ(t, s, i). {#size t, size s#}"
        "λ(t, s, i). t >t s ⟶ subst_db i x t >t subst_db i x s" "(t, s, i)",
      simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric] atomize_all[symmetric])
  fix t s :: "('s, 'v) tm" and i :: nat
  assume
    ih: "⋀ta sa i. {#size ta, size sa#} < {#size t, size s#} ⟹ ta >t sa ⟹
      subst_db i x ta >t subst_db i x sa" and
    t_gt_s: "t >t s"

  let ?ρ = "subst_db i x"

  show "?ρ t >t ?ρ s"
  proof (cases "wt (?ρ t) = wt (?ρ s)")
    case wt_ρt_ne_ρs: False

    have vars_s: "vars_mset t ⊇# vars_mset s"
      using gt.cases t_gt_s by blast
    hence vars_ρs: "vars_mset (?ρ t) ⊇# vars_mset (?ρ s)"
      by (simp add: var_mset_subst_db_subseteq)

    have wt_t_ge_s: "wt t ≥ wt s"
      by (metis dual_order.strict_implies_order eq_imp_le gt.cases t_gt_s)

    have "wt (?ρ t) > wt (?ρ s)"
      using wt_ρt_ne_ρs unfolding wt_subst_db
      by (metis (full_types) gt.simps gt_subst t_gt_s wary_raw_db_subst wt_subst_db)
    thus ?thesis
      by (rule gt_wt[OF vars_ρs])
  next
    case wt_ρt_eq_ρs: True
    show ?thesis
      using t_gt_s
    proof cases
      case gt_wt
      hence False
        using wt_ρt_eq_ρs
        by (metis add_less_le_mono kbo_std.extra_wt_subseteq nat_less_le wary_raw_db_subst wt_subst
            wt_subst_db)
      thus ?thesis
        by sat
    next
      case _: gt_diff
      note vars_s = this(1) and hd_t_gt_hd_s = this(3)
      have vars_ρs: "vars_mset (?ρ t) ⊇# vars_mset (?ρ s)"
        by (simp add: var_mset_subst_db_subseteq vars_s)
      term gt_hd
      have "head (?ρ t) >hd head (?ρ s)"
        by (smt Set.set_insert gt_hd_def hd_t_gt_hd_s head_subst_db insert_subset wary_raw_db_subst
            wary_subst_ground_heads)
      thus ?thesis
        by (rule gt_diff[OF vars_ρs wt_ρt_eq_ρs])
    next
      case _: gt_same
      note vars_s = this(1) and hd_s_eq_hd_t = this(3) and extf = this(4)

      have vars_ρs: "vars_mset (?ρ t) ⊇# vars_mset (?ρ s)"
        by (simp add: var_mset_subst_db_subseteq vars_s)
      have hd_ρt: "head (?ρ t) = head (?ρ s)"
        by (simp add: hd_s_eq_hd_t head_subst_db)

      {
        fix f
        assume f_in_grs: "f ∈ ground_heads (head (?ρ s))"

        let ?ρa = "subst_db (if head s = Sym lam then i + 1 else i) x"
        let ?S = "set (args t) ∪ set (args s)"

        have extf_args_s_t: "extf f (>t) (args t) (args s)"
          using extf f_in_grs hd_s_eq_hd_t head_subst_db wary_raw_db_subst wary_subst_ground_heads
          by (metis (no_types, lifting) insert_subset mk_disjoint_insert)
        have "extf f (>t) (map ?ρa (args t)) (map ?ρa (args s))"
        proof (rule extf_map[of ?S, OF _ _ _ _ _ _ extf_args_s_t])
          show "∀x ∈ ?S. ¬ ?ρa x >t ?ρa x"
            using gt_irrefl by blast
        next
          show "∀z ∈ ?S. ∀y ∈ ?S. ∀x ∈ ?S. ?ρa z >t ?ρa y ⟶ ?ρa y >t ?ρa x ⟶ ?ρa z >t ?ρa x"
            using gt_trans by blast
        next
          have sz_a: "∀ta ∈ ?S. ∀sa ∈ ?S. {#size ta, size sa#} < {#size t, size s#}"
            by (fastforce intro: Max_lt_imp_lt_mset dest: size_in_args)
          show "∀y ∈ ?S. ∀x ∈ ?S. y >t x ⟶ ?ρa y >t ?ρa x"
            using ih sz_a by blast
        qed auto
        hence "extf f (>t) (args (?ρ t)) (args (?ρ s))"
          by (simp add: args_subst_db hd_s_eq_hd_t)
      }
      hence "∀f ∈ ground_heads (head (?ρ s)). extf f (>t) (args (?ρ t)) (args (?ρ s))"
        by blast
      thus ?thesis
        by (rule gt_same[OF vars_ρs wt_ρt_eq_ρs hd_ρt])
    qed
  qed
qed

end

end