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
