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>
Date: Tuesday, 28 August 2018 at 11:45
To: "hol-info@lists.sourceforge.net" <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
