Stream: Isabelle/ML

Topic: searching for a tactic

Hanna Lachnitt (Jul 26 2025 at 17:22):

I have a goal like this one:

 ∀x≥0. ∀y::int. boo (nat x) y = (x = (2::int) ∧ y = (3::int)) ⟹ ∀x≥0. ∀y::int. lift_boo x y = (x = (2::int) ∧ y = (3::int))

I want to find a tactic in ML that unifies as much as possible, i.e. gets me a new goal:

boo (nat x) y = lift_boo x y

Does anyone know how to do this? It is okay if the goal becomes non-valid, e.g.

∃x. x = (4::int) ==> ∃x. x = (5::int)

would give 4=5.

Mathias Fleury (Jul 26 2025 at 19:09):

I am sure there is a better solution but this might make do:

method my_tac =
   (intro allI impI exI bexI)+;
   (elim allE impE exE bexE)+;
    (assumption+)? (*needs repetition due to assumptions*);
   (erule mysubst2),
   (rule refl)? (*tries to solve the first goal*)

lemma ‹
 ∀x≥0. ∀y::int. boo (nat x) y = (x = (2::int) ∧ y = (3::int)) ⟹ ∀x≥0. ∀y::int. lift_boo x y = (x = (2::int) ∧ y = (3::int))›
  apply my_tac
  sorry

lemma ‹∃x. x = (4::int) ==> ∃x. x = (5::int)›
  apply my_tac
  oops

Hanna Lachnitt (Jul 26 2025 at 23:28):

Thank you so much

Hanna Lachnitt (Jul 26 2025 at 23:47):

I realized that what I am trying to do (which is slightly different than what I described) can best be done with conversions. See this example from the Isabelle cookbook

fun true_conj1_conv ctxt ctrm =
case (Thm.term_of ctrm) of
@{term "op ∧"} $ @{term True} $ _ =>
(Conv.arg_conv (true_conj1_conv ctxt) then_conv
Conv.rewr_conv @{thm true_conj1}) ctrm
| _ $ _ => Conv.comb_conv (true_conj1_conv ctxt) ctrm
| Abs _ => Conv.abs_conv (fn (_, ctxt) => true_conj1_conv ctxt) ctxt ctrm
| _ => Conv.all_conv ctrm

where all occurrences of True ∧ x are rewritten to x

irvin (Jul 28 2025 at 12:53):

Hanna Lachnitt said:

I have a goal like this one:

 ∀x≥0. ∀y::int. boo (nat x) y = (x = (2::int) ∧ y = (3::int)) ⟹ ∀x≥0. ∀y::int. lift_boo x y = (x = (2::int) ∧ y = (3::int))

I want to find a tactic in ML that unifies as much as possible, i.e. gets me a new goal:

boo (nat x) y = lift_boo x y

Does anyone know how to do this? It is okay if the goal becomes non-valid, e.g.

∃x. x = (4::int) ==> ∃x. x = (5::int)

would give 4=5.

If you want to do really unification as much as possible I would highly recommend looking at the https://www.isa-afp.org/entries/ML_Unification.html. See https://www.isa-afp.org/sessions/ml_unification/#E_Unification_Examples.html for some examples

irvin (Jul 28 2025 at 12:56):

There are certain cases where writing proper code would be more efficient but that takes more time

irvin (Jul 28 2025 at 13:20):

I'm just guessing but your example seems like the reification examples https://www.isa-afp.org/sessions/ml_unification/#Unification_Hints_Reification_Examples.html

Hanna Lachnitt (Jul 28 2025 at 16:46):

Thanks @irvin, I will look into it

Last updated: Aug 20 2025 at 20:23 UTC