Theory Lambda_Free_RPO_Optim

(*  Title:       The Optimized Graceful Recursive Path Order for Lambda-Free Higher-Order Terms
    Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹The Optimized Graceful Recursive Path Order for Lambda-Free Higher-Order Terms›

theory Lambda_Free_RPO_Optim
imports Lambda_Free_RPO_Std
begin

text ‹
This theory defines the optimized variant of the graceful recursive path order
(RPO) for ‹λ›-free higher-order terms.
›


subsection ‹Setup›

locale rpo_optim = rpo_basis _ _ arity_sym arity_var
    for
      arity_sym :: "'s ⇒ enat" and
      arity_var :: "'v ⇒ enat" +
  assumes extf_ext_snoc: "ext_snoc (extf f)"
begin

lemmas extf_snoc = ext_snoc.snoc[OF extf_ext_snoc]


subsection ‹Definition of the Order›

definition
  chkargs :: "(('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool) ⇒ ('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool"
where
  [simp]: "chkargs gt t s ⟷ (∀s' ∈ set (args s). gt t s')"

lemma chkargs_mono[mono]: "gt ≤ gt' ⟹ chkargs gt ≤ chkargs gt'"
  by force

inductive gt :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ">t" 50) where
  gt_arg: "ti ∈ set (args t) ⟹ ti >t s ∨ ti = s ⟹ t >t s"
| gt_diff: "head t >hd head s ⟹ chkvar t s ⟹ chkargs (>t) t s ⟹ t >t s"
| gt_same: "head t = head s ⟹ chkargs (>t) t s ⟹
    (∀f ∈ ground_heads (head t). extf f (>t) (args t) (args s)) ⟹ t >t s"

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


subsection ‹Transitivity›

lemma gt_in_args_imp: "ti ∈ set (args t) ⟹ ti >t s ⟹ t >t s"
  by (cases t) (auto intro: gt_arg)

lemma gt_imp_vars: "t >t s ⟹ vars t ⊇ vars s"
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "λ(t, s). size t + size s"
      "λ(t, s). t >t s ⟶ vars t ⊇ vars s" "(t, s)", simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric])
  fix t s
  assume
    ih: "⋀ta sa. size ta + size sa < size t + size s ⟹ ta >t sa ⟹ vars ta ⊇ vars sa" and
    t_gt_s: "t >t s"
  show "vars t ⊇ vars s"
    using t_gt_s
  proof cases
    case (gt_arg ti)
    thus ?thesis
      using ih[of ti s]
      by (metis size_in_args vars_args_subseteq add_mono_thms_linordered_field(1) order_trans)
  next
    case gt_diff
    show ?thesis
    proof (cases s)
      case Hd
      thus ?thesis
        using gt_diff(2) by (auto elim: hd.set_cases(2))
    next
      case (App s1 s2)
      thus ?thesis
        using gt_diff ih
        by simp (metis (no_types) add.assoc gt.simps[unfolded chkargs_def chkvar_def] less_add_Suc1)
    qed
  next
    case gt_same
    thus ?thesis
    proof (cases s rule: tm_exhaust_apps)
      case s: (apps ζ ss)
      thus ?thesis
        using gt_same unfolding chkargs_def s
        by (auto intro!: vars_head_subseteq)
          (metis ih[of t] insert_absorb insert_subset nat_add_left_cancel_less s size_in_args
            tm_collapse_apps tm_inject_apps)
    qed
  qed
qed

lemma gt_trans: "u >t t ⟹ t >t s ⟹ u >t s"
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "λ(u, t, s). {#size u, size t, size s#}"
        "λ(u, t, s). u >t t ⟶ t >t s ⟶ u >t s" "(u, t, s)",
      simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric])
  fix u t s
  assume
    ih: "⋀ua ta sa. {#size ua, size ta, size sa#} < {#size u, size t, size s#} ⟹
      ua >t ta ⟹ ta >t sa ⟹ ua >t sa" and
    u_gt_t: "u >t t" and t_gt_s: "t >t s"

  have chkvar: "chkvar u s"
    by clarsimp (meson u_gt_t t_gt_s gt_imp_vars hd.set_sel(2) vars_head_subseteq subsetCE)

  have chk_u_s_if: "chkargs (>t) u s" if chk_t_s: "chkargs (>t) t s"
  proof (clarsimp simp only: chkargs_def)
    fix s'
    assume "s' ∈ set (args s)"
    thus "u >t s'"
      using chk_t_s by (auto intro!: ih[of _ _ s', OF _ u_gt_t] size_in_args)
  qed

  have u_gt_s_if_ui: "ui ≥t t ⟹ u >t s" if ui_in: "ui ∈ set (args u)" for ui
    using ih[of ui t s, simplified, OF size_in_args[OF ui_in] _ t_gt_s]
      gt_in_args_imp[OF ui_in, of s] t_gt_s by blast

  show "u >t s"
    using t_gt_s
  proof cases
    case gt_arg_t_s: (gt_arg ti)
    have u_gt_s_if_chk_u_t: ?thesis if chk_u_t: "chkargs (>t) u t"
      using ih[of u ti s] gt_arg_t_s chk_u_t size_in_args by force
    show ?thesis
      using u_gt_t by cases (auto intro: u_gt_s_if_ui u_gt_s_if_chk_u_t)
  next
    case gt_diff_t_s: gt_diff
    show ?thesis
      using u_gt_t
    proof cases
      case gt_diff_u_t: gt_diff
      have "head u >hd head s"
        using gt_diff_u_t(1) gt_diff_t_s(1) by (auto intro: gt_hd_trans)
      thus ?thesis
        by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_diff_t_s(3)]])
    next
      case gt_same_u_t: gt_same
      have "head u >hd head s"
        using gt_diff_t_s(1) gt_same_u_t(1) by auto
      thus ?thesis
        by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_diff_t_s(3)]])
    qed (auto intro: u_gt_s_if_ui)
  next
    case gt_same_t_s: gt_same
    show ?thesis
      using u_gt_t
    proof cases
      case gt_diff_u_t: gt_diff
      have "head u >hd head s"
        using gt_diff_u_t(1) gt_same_t_s(1) by simp
      thus ?thesis
        by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_same_t_s(2)]])
    next
      case gt_same_u_t: gt_same
      have hd_u_s: "head u = head s"
        using gt_same_u_t(1) gt_same_t_s(1) by simp

      let ?S = "set (args u) ∪ set (args t) ∪ set (args s)"

      have gt_trans_args: "∀ua ∈ ?S. ∀ta ∈ ?S. ∀sa ∈ ?S. ua >t ta ⟶ ta >t sa ⟶ ua >t sa"
      proof clarify
        fix sa ta ua
        assume
          ua_in: "ua ∈ ?S" and ta_in: "ta ∈ ?S" and sa_in: "sa ∈ ?S" and
          ua_gt_ta: "ua >t ta" and ta_gt_sa: "ta >t sa"
        show "ua >t sa"
          by (auto intro!: ih[OF Max_lt_imp_lt_mset ua_gt_ta ta_gt_sa])
            (meson ua_in ta_in sa_in Un_iff max.strict_coboundedI1 max.strict_coboundedI2
               size_in_args)+
      qed

      have "∀f ∈ ground_heads (head u). extf f (>t) (args u) (args s)"
      proof (clarify, rule extf_trans[OF _ _ _ gt_trans_args])
        fix f
        assume f_in_grounds: "f ∈ ground_heads (head u)"
        show "extf f (>t) (args u) (args t)"
          using f_in_grounds gt_same_u_t(3) by blast
        show "extf f (>t) (args t) (args s)"
          using f_in_grounds gt_same_t_s(3) unfolding gt_same_u_t(1) by blast
      qed auto
      thus ?thesis
        by (rule gt_same[OF hd_u_s chk_u_s_if[OF gt_same_t_s(2)]])
    qed (auto intro: u_gt_s_if_ui)
  qed
qed

lemma gt_sub_fun: "App s t >t s"
  by (rule gt_same) (auto intro: extf_snoc gt_arg[of _ "App s t"])

end


subsection ‹Conditional Equivalence with Unoptimized Version›

context rpo
begin

context
  assumes extf_ext_snoc: "⋀f. ext_snoc (extf f)"
begin

lemma rpo_optim: "rpo_optim ground_heads_var (>s) extf arity_sym arity_var"
  unfolding rpo_optim_def rpo_optim_axioms_def using rpo_basis_axioms extf_ext_snoc by auto

abbreviation
  chkargs :: "(('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool) ⇒ ('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool"
where
  "chkargs ≡ rpo_optim.chkargs"

abbreviation gt_optim :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ">to" 50) where
  "(>to) ≡ rpo_optim.gt ground_heads_var (>s) extf"

abbreviation ge_optim :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix "≥to" 50) where
  "(≥to) ≡ rpo_optim.ge ground_heads_var (>s) extf"

theorem gt_iff_optim: "t >t s ⟷ t >to s"
proof (rule measure_induct_rule[of "λ(t, s). size t + size s"
      "λ(t, s). t >t s ⟷ t >to s" "(t, s)", simplified prod.case],
    simp only: split_paired_all prod.case)
  fix t s :: "('s, 'v) tm"
  assume ih: "⋀ta sa. size ta + size sa < size t + size s ⟹ ta >t sa ⟷ ta >to sa"

  show "t >t s ⟷ t >to s"
  proof
    assume t_gt_s: "t >t s"

    have chkargs_if_chksubs: "chkargs (>to) t s" if chksubs: "chksubs (>t) t s"
      unfolding rpo_optim.chkargs_def[OF rpo_optim]
    proof (cases s, simp_all, intro conjI ballI)
      fix s1 s2
      assume s: "s = App s1 s2"

      have t_gt_s2: "t >t s2"
        using chksubs s by simp
      show "t >to s2"
        by (rule ih[THEN iffD1, OF _ t_gt_s2]) (simp add: s)

      {
        fix s1i
        assume s1i_in: "s1i ∈ set (args s1)"

        have "t >t s1"
          using chksubs s by simp
        moreover have "s1 >t s1i"
          using s1i_in gt_proper_sub size_in_args sub_args by fastforce
        ultimately have t_gt_s1i: "t >t s1i"
          by (rule gt_trans)

        have sz_s1i: "size s1i < size s"
          using size_in_args[OF s1i_in] s by simp

        show "t >to s1i"
          by (rule ih[THEN iffD1, OF _ t_gt_s1i]) (simp add: sz_s1i)
      }
    qed

    show "t >to s"
      using t_gt_s
    proof cases
      case gt_sub
      note t_app = this(1) and ti_geo_s = this(2)

      obtain t1 t2 where t: "t = App t1 t2"
        using t_app by (metis tm.collapse(2))

      have t_gto_t1: "t >to t1"
        unfolding t by (rule rpo_optim.gt_sub_fun[OF rpo_optim])
      have t_gto_t2: "t >to t2"
        unfolding t by (rule rpo_optim.gt_arg[OF rpo_optim, of t2]) simp+

      {
        assume t1_gt_s: "t1 >t s"
        have "t1 >to s"
          by (rule ih[THEN iffD1, OF _ t1_gt_s]) (simp add: t)
        hence ?thesis
          by (rule rpo_optim.gt_trans[OF rpo_optim t_gto_t1])
      }
      moreover
      {
        assume t2_gt_s: "t2 >t s"
        have "t2 >to s"
          by (rule ih[THEN iffD1, OF _ t2_gt_s]) (simp add: t)
        hence ?thesis
          by (rule rpo_optim.gt_trans[OF rpo_optim t_gto_t2])
      }
      ultimately show ?thesis
        using t ti_geo_s t_gto_t1 t_gto_t2 by auto
    next
      case gt_diff
      note hd_t_gt_s = this(1) and chkvar = this(2) and chksubs = this(3)
      show ?thesis
        by (rule rpo_optim.gt_diff[OF rpo_optim hd_t_gt_s chkvar chkargs_if_chksubs[OF chksubs]])
    next
      case gt_same
      note hd_t_eq_s = this(1) and chksubs = this(2) and extf = this(3)

      have extf_gto: "∀f ∈ ground_heads (head t). extf f (>to) (args t) (args s)"
      proof (rule ballI, rule extf_mono_strong[of _ _ "(>t)", rule_format])
        fix f
        assume f_in_ground: "f ∈ ground_heads (head t)"

        {
          fix ta sa
          assume ta_in: "ta ∈ set (args t)" and sa_in: "sa ∈ set (args s)" and ta_gt_sa: "ta >t sa"

          show "ta >to sa"
            by (rule ih[THEN iffD1, OF _ ta_gt_sa])
              (simp add: ta_in sa_in add_less_mono size_in_args)
        }

        show "extf f (>t) (args t) (args s)"
          using f_in_ground extf by simp
      qed

      show ?thesis
        by (rule rpo_optim.gt_same[OF rpo_optim hd_t_eq_s chkargs_if_chksubs[OF chksubs] extf_gto])
    qed
  next
    assume t_gto_s: "t >to s"

    have chksubs_if_chkargs: "chksubs (>t) t s" if chkargs: "chkargs (>to) t s"
      unfolding chksubs_def
    proof (cases s, simp_all, rule conjI)
      fix s1 s2
      assume s: "s = App s1 s2"

      have "s >to s1"
        unfolding s by (rule rpo_optim.gt_sub_fun[OF rpo_optim])
      hence t_gto_s1: "t >to s1"
        by (rule rpo_optim.gt_trans[OF rpo_optim t_gto_s])
      show "t >t s1"
        by (rule ih[THEN iffD2, OF _ t_gto_s1]) (simp add: s)

      have t_gto_s2: "t >to s2"
        using chkargs unfolding rpo_optim.chkargs_def[OF rpo_optim] s by simp
      show "t >t s2"
        by (rule ih[THEN iffD2, OF _ t_gto_s2]) (simp add: s)
    qed

    show "t >t s"
    proof (cases rule: rpo_optim.gt.cases[OF rpo_optim t_gto_s,
        case_names gto_arg gto_diff gto_same])
      case (gto_arg ti)
      hence ti_in: "ti ∈ set (args t)" and ti_geo_s: "ti ≥to s"
        by auto
      obtain ζ ts where t: "t = apps (Hd ζ) ts"
        by (fact tm_exhaust_apps)

      {
        assume ti_gto_s: "ti >to s"
        hence ti_gt_s: "ti >t s"
          using ih[of ti s] size_in_args ti_in by auto
        moreover have "t >t ti"
          using sub_args[OF ti_in] gt_proper_sub size_in_args[OF ti_in] by blast
        ultimately have ?thesis
          using gt_trans by blast
      }
      moreover
      {
        assume "ti = s"
        hence ?thesis
          using sub_args[OF ti_in] gt_proper_sub size_in_args[OF ti_in] by blast
      }
      ultimately show ?thesis
        using ti_geo_s by blast
    next
      case gto_diff
      hence hd_t_gt_s: "head t >hd head s" and chkvar: "chkvar t s" and
        chkargs: "chkargs (>to) t s"
        by blast+

      have "chksubs (>t) t s"
        by (rule chksubs_if_chkargs[OF chkargs])
      thus ?thesis
        by (rule gt_diff[OF hd_t_gt_s chkvar])
    next
      case gto_same
      hence hd_t_eq_s: "head t = head s" and chkargs: "chkargs (>to) t s" and
        extf_gto: "∀f ∈ ground_heads (head t). extf f (>to) (args t) (args s)"
        by blast+

      have chksubs: "chksubs (>t) t s"
        by (rule chksubs_if_chkargs[OF chkargs])

      have extf: "∀f ∈ ground_heads (head t). extf f (>t) (args t) (args s)"
      proof (rule ballI, rule extf_mono_strong[of _ _ "(>to)", rule_format])
        fix f
        assume f_in_ground: "f ∈ ground_heads (head t)"

        {
          fix ta sa
          assume ta_in: "ta ∈ set (args t)" and sa_in: "sa ∈ set (args s)" and ta_gto_sa: "ta >to sa"

          show "ta >t sa"
            by (rule ih[THEN iffD2, OF _ ta_gto_sa])
              (simp add: ta_in sa_in add_less_mono size_in_args)
        }

        show "extf f (>to) (args t) (args s)"
          using f_in_ground extf_gto by simp
      qed

      show ?thesis
        by (rule gt_same[OF hd_t_eq_s chksubs extf])
    qed
  qed
qed

end

end

end