Okay, I imagine HOL-Light does the same. Thank you > On Jul 3, 2018, at 3:36 PM, Mario Xerxes Castelán Castro > <marioxcc...@yandex.com> wrote: > > Please include the mailing list in your replies. I do not know what you > are doing. Anyway, this does not look like HOL4. Are you using HOL > Light? I only know about HOL4. Removing the quantifier will usually be > done internally by the subsequent tactic that requires using the > proposition with a specific specialization of “n” and there is no need > to specialize the assumption manually. > > On 03/07/18 14:31, Dylan Melville wrote: >> I’m trying to prove a statement about Induction Schemas, after. Breaking >> assumptions into hypotheses I’m left with >> >> 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`] >> 3 [`(eval (f) to (num->bool)) 0`] >> 4 [`!n. (eval (f) to (num->bool)) n ==> (eval (f) to (num->bool)) (SUC >> n)`] >> >> `(eval (f) to (num->bool)) n` >> >> What I need help with only pertains to assumption 4 and the goal. >> >> f was originally universally quantified across the entire original term >> and so was n in all statements where it is free. I assumed that it would >> be easier to manipulate the expressions in the way I want without the >> quantifications, but I am fairly new, so if as you say most theorems / >> tactical handle the universal quantification seamlessly maybe I’m wrong. >> Otherwise, I’d like to strip the forall from the 4th assumption. >> >>> On Jul 3, 2018, at 3:23 PM, Mario Xerxes Castelán Castro >>> <marioxcc...@yandex.com <mailto:marioxcc...@yandex.com>> wrote: >>> >>> An hypothesis of the form “∀x. P” where “x” occurs free in P is stronger >>> than just “P” (that is, the former entails the later). Many tactics have >>> built-in specialization, so it depends on what you want to do. Can you >>> provide more details? >>> >>> On 03/07/18 14:18, Dylan Melville wrote: >>>> Is there any tactical that can take universal quantification off of a >>>> hypothesis like how GEN_TAC does with the goal? >>>> >>>> -Dylan >>>> ------------------------------------------------------------------------------ >>>> Check out the vibrant tech community on one of the world's most >>>> engaging tech sites, Slashdot.org <http://Slashdot.org>! >>>> http://sdm.link/slashdot >>>> _______________________________________________ >>>> hol-info mailing list >>>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> >>>> https://lists.sourceforge.net/lists/listinfo/hol-info >>>> >>> >>> ------------------------------------------------------------------------------ >>> Check out the vibrant tech community on one of the world's most >>> engaging tech sites, Slashdot.org <http://Slashdot.org>! >>> http://sdm.link/slashdot_______________________________________________ >>> hol-info mailing list >>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> >>> https://lists.sourceforge.net/lists/listinfo/hol-info >> > > ------------------------------------------------------------------------------ > 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
------------------------------------------------------------------------------ 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
