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 >
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
