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> 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>
> *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
