Theory Lambda_Encoding_KBO
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 ">⇩h⇩d" 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) >⇩h⇩d 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