Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unexpected flex-flex pair with FOCUS

view this post on Zulip Email Gateway (Aug 19 2022 at 08:58):

From: Peter Lammich <lammich@in.tum.de>
Hi all,

consider the minimal example below. Why does FOCUS_PARAMS (and,
similarly, FOCUS and FOCUS_PREMS) produce a flex-flex pair here?
I would have expected this not to change the goal at all.

Regards,
Peter

schematic_lemma "?foo x"
apply (tactic {* Subgoal.FOCUS_PARAMS (K all_tac) @{context} 1*})

;
goal (1 subgoal):

  1. ?foo3 x
    flex-flex pairs:
    ?foo3 x =?= ?foo x
    variables:
    x :: 'a
    ?foo, ?foo3 :: 'a \<Rightarrow> bool

Last updated: Nov 21 2024 at 12:39 UTC