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.›

text ‹Unsolvable unification disagreement pairs are normalised by the simplifier
(cf. @{ML_structure Simplifier_Unification}) and then again passed to the unifier:›

lemma
  assumes "P (map f [])"
  shows "P []"
  (*uncomment to see the trace*)
  (* supply [[ML_map_context ‹Logger.set_log_levels Logger.root Logger.TRACE›]] *)
  by (urule assms)

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

text ‹Premises of the form @{term "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 prio: Prio.LOW]: "n ≠ 0 ⟹ n - 1 ≡⇧?> m ⟹ n ≡ Suc m"
  unfolding SIMPS_TO_UNIF_eq by linarith

text ‹By default, below unification methods use
@{ML Mixed_Comb_Unification.fo_hop_comb_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›]] *)
(*uncomment to see bound variables instead of Skolem variables*)
(* declare [[show_unif_problem_skolem=false]] *)

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: ‹\<^binding>‹simp_unify››]]
  (*doesn't work*)
  ― ‹by (ufact refl)›
  supply sub_self_eq_zero[uhint del, 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: ‹\<^binding>‹simp_unify››]]
  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

lemma
  assumes "A ⟶ ((B ⟶ C) ⟶ D) ⟶ E"
  shows "A ⟹ ((B ⟹ C) ⟹ D) ⟹ E"
  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)" ― ‹we want to infer type ‹?T››
  apply (urule app_typeI)
  ―‹compare with the following application, creating an (unintuitive) higher-order instantiation›
  (* apply (rule app_typeI) *)
  oops

text ‹For synthesis problems, it is sometimes useful to match terms but unify types:›

schematic_goal foo:
  assumes "⋀T x. P T x ⟹ T (x :: 'b)"
  shows "T (x :: ?'b)"
  apply (urule assms unifier: Mixed_Unification.fo_hop_match_type_unify
    normalisers: Unification_Util.beta_eta_short_norms_match_type_unify)
  ―‹Note that the we cannot obtain this result by standard matching:›
  (* apply (tactic ‹match_tac @{context} @{thms assms} 1›) *)
  oops

end

end