Thank you!
> On Aug 28, 2018, at 8:29 PM, <michael.norr...@data61.csiro.au>
> <michael.norr...@data61.csiro.au> wrote:
>
> 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
