Make the assumption the left-hand-side of an implication (moving it out of the
assumptions), rewrite with the identity that says that
((P /\ Q) ==> R) <=> (P ==> (Q ==> R))
and then move all the implications’ left-hand-sides back into the assumptions.
In HOL4 you could use something like
th |> DISCH_ALL |> REWRITE_RULE [GSYM AND_IMP_INTRO] |> UNDISCH_ALL
The use of the _ALL functions makes this a bit fragile, but it will work in
your case.
You might also find that the discharged theorem works directly as a conditional
rewrite (I don’t know what the HOL Light tools is for this).
My HOL4-informed advice would be to avoid working with theorems that have
assumptions like this: the machinery copes better with theorems that are just
implications. (Of course, goals can have assumptions and the machinery copes
very well with those, but that is a different matter.)
Michael
From: Dylan Melville <dylanmelvi...@gmail.com>
Date: Tuesday, 28 August 2018 at 22:48
To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>,
"hol-info@lists.sourceforge.net" <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions
That's what I figured. How can I separate the assumptions of
second_b13_complete?
On Mon, Aug 27, 2018, 10:32 PM
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote:
The assumption of the rewrite theorem is not present in the assumptions of the
goal and so you get an invalid tactic.
Strictly speaking this is not REWRITE_TAC failing but e. Indeed, you should
find that REWRITE_TAC [second_b13_complete] applied to the goal works just fine.
Michael
From: Dylan Melville <dylanmelvi...@gmail.com<mailto:dylanmelvi...@gmail.com>>
Date: Tuesday, 28 August 2018 at 11:45
To: "hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>"
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
Subject: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions
VERSION: HOL Light QE (augmentation of HOL Light, very similar)
Hello all. Today I’ve been having 2 issues with HOL. The first is that although
the documentation for REWRITE_TAC says that the tactic has no failure
conditions, when I use the following command:
# e (REWRITE_TAC[second_b13_complete]);;
Where second_b13_complete is:
# second_b13_complete;;
val it : thm =
isExprType f (TyBiCons "fun" (TyBase "num") (TyBase "bool")) /\
~isFreeIn (QuoVar "n" (TyBase "num")) f
|- (\n. (\P. P n) (eval (f) to (num->bool))) =
(\P n. P n) (eval (f) to (num->bool))
When used with the following goal already declared:
# p();;
val it : goalstack = 1 subgoal (1 total)
0 [`isExprType f (TyBiCons "fun" (TyVar "num") (TyBase "bool"))`]
1 [`~isFreeIn (QuoVar "n" (TyBase "num")) f`]
2 [`isPeano f`]
`(eval (f) to (num->bool)) 0 /\
(\P. P = (\x. T)) (\n. (\P. P n ==> P (SUC n)) (eval (f) to (num->bool)))
==> (\P. P = (\x. T)) (\n. (\P. P n) (eval (f) to (num->bool)))`
Results in the following error:
# e (REWRITE_TAC[first_b13_complete]);;
Exception: Failure "VALID: Invalid tactic”.
Which is confusing, since not only is the tactic supposed to have no failure
conditions, but the bolded sections of the theorem and the goal are matched
properly, and the two conjuncted antecedents of the theorem are assumptions 0
and 1 of the goal. So, is the reason that the tactic application fails that
antecedents of the theorem are conjuncted? If so, is there a command I’m
missing that can transform the theorem to the proper form?
Thanks in advance.
Dylan Melville | McMaster University, Math and Computer Science
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
