Theory E_Unification_Examples

✐‹creator "Kevin Kappelmann"›
section ‹E-Unification Examples›
theory E_Unification_Examples
  imports
    Main
    ML_Unification_HOL_Setup
    Unify_Assumption_Tactic
    Unify_Fact_Tactic
    Unify_Resolve_Tactics
begin

paragraph ‹Summary›
text ‹Sample applications of e-unifiers, methods, etc. introduced in this session.›

experiment
begin

subsection ‹Using The Simplifier For Unification.›

inductive_set even :: "nat set" where
zero: "0 ∈ even" |
step: "n ∈ even ⟹ Suc (Suc n) ∈ even"

text ‹Premises of the form @{term "SIMPS_TO_UNIF lhs rhs"} are solved by
@{ML_structure Simplifier_Unification}. It first normalises @{term lhs} and then unifies the
normalisation with @{term rhs}. See also @{theory ML_Unification.ML_Unification_HOL_Setup}.›

lemma [uhint where prio = Prio.LOW]: "n ≠ 0 ⟹ PROP SIMPS_TO_UNIF (n - 1) m ⟹ n ≡ Suc m"
  unfolding SIMPS_TO_UNIF_eq by linarith

text ‹By default, below unification methods use
@{ML Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify}, which is a combination of
various practical unification algorithms.›

schematic_goal "(⋀x. x + 4 = n) ⟹ Suc ?x = n"
  by uassm

lemma "6 ∈ even"
  apply (urule step)
  apply (urule step)
  apply (urule step)
  apply (urule zero)
  done

lemma "(220 + (80 - 2 * 2)) ∈ even"
  apply (urule step)
  apply (urule (rr) step)
  apply (urule zero)
  done

lemma
  assumes "[a,b,c] = [c,b,a]"
  shows "[a] @ [b,c] = [c,b,a]"
  using assms by uassm

lemma "x ∈ ({z, y, x} ∪ S) ∩ {x}"
  by (ufact TrueI)

schematic_goal "(x + (y :: nat))^2 ≤ x^2 + 2*x*y + y^2 + 4 * y + x - y"
  supply power2_sum[simp]
  by (ufact TrueI)

lemma
  assumes "⋀s. P (Suc (Suc 0)) (s(x := (1 :: nat), x := 1 + 1 * 4 - 3))"
  shows "P 2 (s(x := 2))"
  by (ufact assms)

subsection ‹Providing Canonical Solutions With Unification Hints›

lemma sub_self_eq_zero [uhint]: "(n :: nat) - n ≡ 0" by simp

schematic_goal "n - ?m = (0 :: nat)"
  by (ufact refl)

text ‹The following example shows a non-trivial interplay of the simplifier and unification hints:
Using just unification, the hint @{thm sub_self_eq_zero} is not applicable in the following example
since @{term 0} cannot be unified with @{term "length []"}.
However, the simplifier can rewrite @{term "length []"} to @{term 0} and the hint can then be applied.›

(*uncomment to see the trace*)
declare [[ML_map_context ‹Logger.set_log_levels Logger.root Logger.TRACE›]]

schematic_goal "n - ?m = length []"
  by (ufact refl)

text ‹There are also two ways to solve this using only unification hints:
▸ We allow the recursive use of unification hints when unifying @{thm sub_self_eq_zero} and our goal
and register @{term "length [] = 0"} as an additional hint.
▸ We use an alternative for @{thm sub_self_eq_zero} that makes the recursive use of unification
hints explicit and register @{term "length [] = 0"} as an additional hint.›

lemma length_nil_eq [uhint]: "length [] = 0" by simp

text ‹Solution 1: we can use @{attribute rec_uhint} for recursive usages of hints.
Warning: recursive hint applications easily loop.›

schematic_goal "n - ?m = length []"
  supply [[ucombine del = ‹(Standard_Unification_Combine.default_metadata \<^binding>‹simp_unif›)›]]
  (*doesn't work*)
  ― ‹by (ufact refl)›
  supply sub_self_eq_zero[rec_uhint]
  by (ufact refl)

text ‹Solution 2: make the recursion explicit in the hint.›

lemma [uhint]: "k ≡ 0 ⟹ (n :: nat) ≡ m ⟹ n - m ≡ k" by simp

schematic_goal "n - ?m = length []"
  supply [[ucombine del = ‹(Standard_Unification_Combine.default_metadata \<^binding>‹simp_unif›)›]]
  by (ufact refl)

subsection ‹Strenghten Unification With Unification Hints›

lemma
  assumes [uhint]: "n = m"
  shows "n - m = (0 :: nat)"
  by (ufact refl)

lemma
  assumes "x = y"
  shows "y = x"
  supply eq_commute[uhint]
  by (ufact assms)


paragraph ‹Unfolding definitions.›

definition "mysuc n = Suc n"

lemma
  assumes "⋀m. Suc n > mysuc m"
  shows "mysuc n > Suc 3"
  supply mysuc_def[uhint]
  by (ufact assms)


paragraph ‹Discharging meta impliciations with object-level implications›

lemma [uhint]:
  "Trueprop A ≡ A' ⟹ Trueprop B ≡ B' ⟹ Trueprop (A ⟶ B) ≡ (PROP A' ⟹ PROP B')"
  using atomize_imp[symmetric] by simp

lemma
  assumes "A ⟶ (B ⟶ C) ⟶ D"
  shows "A ⟹ (B ⟹ C) ⟹ D"
  using assms by ufact


subsection ‹Better Control Over Meta Variable Instantiations›

text ‹Consider the following type-inference problem.›
schematic_goal
  assumes app_typeI: "⋀f x.  (⋀x. ArgT x ⟹ DomT x (f x)) ⟹ ArgT x ⟹ DomT x (f x)"
  and f_type: "⋀x. ArgT x ⟹ DomT x (f x)"
  and x_type: "ArgT x"
  shows "?T (f x)"
  apply (urule app_typeI) ―‹compare with the following application, creating an (unintuitive) higher-order instantiation›
  (* apply (rule app_typeI) *)
  oops

end

end