Theory E_Unification_Examples
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.›
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›)›]]
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 = ‹(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
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)"
apply (urule app_typeI)
oops
end
end