Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Reto Kramer wrote:
by (instantiate_tac [("y31", "fst")]) ;
Actually I've found you get a less flaky proof by the following
which removes the 31 (which is particularly likely to vary after minor
changes in your preceding proof steps)
by (PRIMITIVE standard) ;
by (instantiate_tac [("y", "fst")]) ;
see the reference manual s3.5.1 and s3.1.4
Jeremy
Email Gateway (Aug 17 2022 at 13:27):From: Lucas Dixon <lucas.dixon@ed.ac.uk>
Reto Kramer wrote:
I looked up theorems containing "fst", this included in the list:
Product_Type.fst_conv: fst (?a, ?b) = ?a
This suggests the following applucation of rule:
apply (rule Product_Type.fst_conv[symmetric])
best,
lucas
Email Gateway (Aug 17 2022 at 13:27):From: Makarius <makarius@sketis.net>
On Wed, 12 Oct 2005, Jeremy Dawson wrote:
Reto Kramer wrote:
I find myself with the following subgoal:
!! a b. a = ?y31 (a,b)
How do I tell Isabelle to replace ?y31 with "fst" so that simp will solve
the goal?
Actually I've found you get a less flaky proof by the following
which removes the 31 (which is particularly likely to vary after minor changes
in your preceding proof steps)by (PRIMITIVE standard) ;
by (instantiate_tac [("y", "fst")]) ;
Just note that using standard within a proof is a very bad idea -- its
purpose is to conclude a sequence of reasoning, producing a certain normal
form with some internal rearrangements. Even worse, standard only works
properly in a top-level theory context, but messes up the proof state in
the presence of local assumptions, locales etc.
Functions like prove_goal, prove_goalw_cterm are of the same category, and
are better avoided.
see the reference manual s3.5.1 and s3.1.4
The reference manual is slightly outdated, and will be replaced
eventually.
Makarius
Email Gateway (Aug 17 2022 at 13:27):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Makarius wrote:
On Wed, 12 Oct 2005, Jeremy Dawson wrote:
by (PRIMITIVE standard) ;
by (instantiate_tac [("y", "fst")]) ;Just note that using standard within a proof is a very bad idea -- its
purpose is to conclude a sequence of reasoning, producing a certain normal
form with some internal rearrangements. Even worse, standard only works
properly in a top-level theory context, but messes up the proof state in
the presence of local assumptions, locales etc.Makarius
Alternatively to using standard, do
by (PRIMITIVE zero_var_indexes) ;
This has less effect on the remainder of the proof state,
in particular it doesn't turn hypotheses of the proof state
into premises
Jeremy
Last updated: Nov 21 2024 at 12:39 UTC