Theory Unification_Hints_Reification_Examples

✐‹creator "Kevin Kappelmann"›
✐‹contributor "Paul Bachmann"›
section ‹Examples: Reification Via Unification Hints›
theory Unification_Hints_Reification_Examples
  imports
    HOL.Rat
    ML_Unification_HOL_Setup
    Unify_Fact_Tactic
    Unify_Resolve_Tactics
begin

paragraph ‹Summary›
text ‹Reification via unification hints. For an introduction to unification hints refer
to \<^cite>‹"unif-hints"›. We support a generalisation of unification hints as described
in @{theory ML_Unification.ML_Unification_Hints}.›

subsection ‹Setup›

text ‹One-time setup to obtain a unifier with unification hints for the purpose of reification.
We could also simply use the standard unification hints @{attribute uhint} and
@{attribute rec_uhint}, but having separate instances is a cleaner approach.›

ML‹
  @{functor_instance struct_name = Reification_Unification_Hints
    and functor_name = Term_Index_Unification_Hints
    and id = ‹"reify"›
    and more_args = ‹
      structure TI = Discrimination_Tree
      val init_args = {
        concl_unifier = NONE,
        prems_unifier = NONE,
        normalisers = SOME Higher_Order_Pattern_Unification.norms_unify,
        retrieval = SOME (Term_Index_Unification_Hints_Args.mk_sym_retrieval
          TI.norm_term TI.unifiables),
        hint_preprocessor = SOME (Standard_Unification_Hints.get_hint_preprocessor
          (Context.the_generic_context ()))
      }›}
  val reify_unify = Unification_Combinator.add_fallback_unifier
    (fn unif_theory =>
      Higher_Order_Pattern_Unification.e_unify Unification_Util.unify_types unif_theory unif_theory
      |> Type_Unification.e_unify Unification_Util.unify_types)
    (Reification_Unification_Hints.try_hints
      |> Unification_Combinator.norm_unifier
        (Unification_Util.inst_norm_term' Higher_Order_Pattern_Unification.norms_unify))
›
local_setup ‹Reification_Unification_Hints.setup_attribute NONE›

text ‹Premises of hints should again be unified by the reification unifier.›
declare [[reify_uhint where prems_unifier = reify_unify]]

subsection ‹Formulas with Quantifiers and Environment›

text ‹The following example is taken from HOL-Library.Reflection\_Examples. It is recommended
to compare the approach presented here with the reflection tactic presented in said theory.›

datatype form =
  TrueF
| FalseF
| Less nat nat
| And form form
| Or form form
| Neg form
| ExQ form

primrec interp :: "form ⇒ ('a::ord) list ⇒ bool"
where
  "interp TrueF vs ⟷ True"
| "interp FalseF vs ⟷ False"
| "interp (Less i j) vs ⟷ vs ! i < vs ! j"
| "interp (And f1 f2) vs ⟷ interp f1 vs ∧ interp f2 vs"
| "interp (Or f1 f2) vs ⟷ interp f1 vs ∨ interp f2 vs"
| "interp (Neg f) vs ⟷ ¬ interp f vs"
| "interp (ExQ f) vs ⟷ (∃v. interp f (v # vs))"

paragraph ‹Reification with unification and recursive hint unification for conclusion›

text ‹The following illustrates how to use the equations @{thm interp.simps} directly
as unification hints for reification.›

experiment
begin

text ‹Hints for list lookup.›
declare List.nth_Cons_Suc[reify_uhint where prio = Prio.LOW]
  and List.nth_Cons_0[reify_uhint]

text ‹Hints to reify formulas of type @{type bool} into formulas of type @{type form}.›
declare interp.simps[reify_uhint]

text ‹We have to allow the hint unifier to recursively look for hints during unification of
the hint's conclusion.›
declare [[reify_uhint where concl_unifier = reify_unify]]

(*uncomment the following to see the hint unification process*)
(* declare [[ML_map_context ‹Logger.set_log_levels Unification_Base.logger Logger.DEBUG›]] *)

schematic_goal
  "interp ?f (?vs :: ('a :: ord) list) = (∃(x :: 'a). x < y ∧ ¬(∃(z :: 'a). v < z ∨ ¬False))"
  by (ufact refl where unifier = reify_unify)

text ‹While this all works nicely if set up correctly, it can be rather difficult to
understand and debug the recursive unification process for a hint's conclusion.
In the next paragraph, we present an alternative that is closer to the examples presented
in the original unification hints paper \<^cite>‹"unif-hints"›.›

end

paragraph ‹Reification with matching without recursion for conclusion›

text ‹We disallow the hint unifier to recursively look for hints while unifying the conclusion;
instead, we only allow the hint unifier to match the hint's conclusion against the disagreement terms.›
declare [[reify_uhint where concl_unifier =
  ‹Higher_Order_Pattern_Unification.match |> Type_Unification.e_match Unification_Util.match_types›]]

text ‹However, this also means that we now have to write our hints such that the hint's
conclusion can successfully be matched against the disagreement terms. In particular,
the disagreement terms may still contain meta variables that we want to instantiate with the help
of the unification hints. Essentially, a hint then describes a canonical instantiation for
these meta variables.›

experiment
begin

lemma [reify_uhint where prio = Prio.LOW]:
  "n ≡ Suc n' ⟹ vs ≡ v # vs' ⟹ vs' ! n' ≡ x ⟹ vs ! n ≡ x"
  by simp

lemma [reify_uhint]: "n ≡ 0 ⟹ vs ≡ x # vs' ⟹ vs ! n ≡ x"
  by simp

lemma [reify_uhint]:
  "⟦e ≡ ExQ f; ⋀v. interp f (v # vs) ≡ P v⟧ ⟹ interp e vs ≡ ∃v. P v"
  "⟦e ≡ Less i j; x ≡ vs ! i; y ≡ vs ! j⟧ ⟹ interp e vs ≡ x < y"
  "⟦e ≡ And f1 f2; interp f1 vs ≡ r1; interp f2 vs ≡ r2⟧ ⟹ interp e vs ≡ r1 ∧ r2"
  "⟦e ≡ Or f1 f2; interp f1 vs ≡ r1; interp f2 vs ≡ r2⟧ ⟹ interp e vs ≡ r1 ∨ r2"
  "e ≡ Neg f ⟹ interp f vs ≡ r ⟹ interp e vs ≡ ¬r"
  "e ≡ TrueF ⟹ interp e vs ≡ True"
  "e ≡ FalseF ⟹ interp e vs ≡ False"
  by simp_all

schematic_goal
  "interp ?f (?vs :: ('a :: ord) list) = (∃(x :: 'a). x < y ∧ ¬(∃(z :: 'a). v < z ∨ ¬False))"
  by (urule refl where unifier = reify_unify)

end

text ‹The next examples are modification from \<^cite>‹"unif-hints"›.›

subsection ‹Simple Arithmetic›

datatype add_expr = Var int | Add add_expr add_expr

fun eval_add_expr :: "add_expr ⇒ int" where
  "eval_add_expr (Var i) = i"
| "eval_add_expr (Add ex1 ex2) = eval_add_expr ex1 + eval_add_expr ex2"

lemma eval_add_expr_Var [reify_uhint where prio = Prio.LOW]:
  "e ≡ Var i ⟹ eval_add_expr e ≡ i" by simp

lemma eval_add_expr_add [reify_uhint]:
  "e ≡ Add e1 e2 ⟹ eval_add_expr e1 ≡ m ⟹ eval_add_expr e2 ≡ n ⟹ eval_add_expr e ≡ m + n"
  by simp

ML_command‹
  val t1 = Proof_Context.read_term_pattern @{context} "eval_add_expr ?e"
  val t2 = Proof_Context.read_term_pattern @{context} "1 + (2 + 7) :: int"
  val _ = Unification_Util.log_unif_results @{context} (t1, t2) (reify_unify [])
›

schematic_goal "eval_add_expr ?e = (1 + (2 + 7) :: int)"
  by (urule refl where unifier = reify_unify)


subsection ‹Arithmetic with Environment›

datatype mul_expr =
  Unit
| Var nat
| Mul mul_expr mul_expr
| Inv mul_expr

fun eval_mul_expr :: "mul_expr × rat list ⇒ rat" where
  "eval_mul_expr (Unit, Γ) = 1"
| "eval_mul_expr (Var i, Γ) = Γ ! i"
| "eval_mul_expr (Mul e1 e2, Γ) = eval_mul_expr (e1, Γ) * eval_mul_expr (e2, Γ)"
| "eval_mul_expr (Inv e, Γ) = inverse (eval_mul_expr (e, Γ))"

text ‹Split @{term e} into an expression and an environment.›
lemma [reify_uhint where prio = Prio.VERY_LOW]:
  "e ≡ (e1, Γ) ⟹ eval_mul_expr (e1, Γ) ≡ n ⟹ eval_mul_expr e ≡ n"
  by simp

text ‹Hints for environment lookup.›
lemma [reify_uhint where prio = Prio.LOW]:
  "e ≡ Var (Suc p) ⟹ Γ ≡ s # Δ ⟹ n ≡ eval_mul_expr (Var p, Δ) ⟹ eval_mul_expr (e, Γ) ≡ n"
  by simp

lemma [reify_uhint]: "e ≡ Var 0 ⟹ Γ ≡ n # Θ ⟹ eval_mul_expr (e, Γ) ≡ n"
  by simp

lemma [reify_uhint]:
  "e1 ≡ Inv e2 ⟹ n ≡ eval_mul_expr (e2, Γ) ⟹ eval_mul_expr (e1, Γ) ≡ inverse n"
  "e ≡ Mul e1 e2 ⟹ m ≡ eval_mul_expr (e1, Γ) ⟹ n ≡ eval_mul_expr (e2, Γ) ⟹
    eval_mul_expr (e, Γ) ≡ m * n"
  "e ≡ Unit ⟹ eval_mul_expr (e, Γ) ≡ 1"
  by simp_all

ML_command‹
  val t1 = Proof_Context.read_term_pattern @{context} "eval_mul_expr ?e"
  val t2 = Proof_Context.read_term_pattern @{context} "1 * inverse 3 * 5 :: rat"
  val _ = Unification_Util.log_unif_results' 1 @{context} (t2, t1) (reify_unify [])
›

schematic_goal "eval_mul_expr ?e = (1 * inverse 3 * 5 :: rat)"
  by (ufact refl where unifier = reify_unify)

end