opes 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
> Date: Tuesday, 28 August 2018 at 22:48
> To: &quo
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
> *Date: *Tuesday, 28 August 2018 at 11:45
> *To: *"hol-info@lists.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--
As a more concise question: can you use assumptions of the hypothesis to
eliminate the assumptions of a theorem?
On Mon, Aug 20, 2018, 4:51 PM Dylan Melville
wrote:
> Let's say I have a goal,
>
> a /\ b /\ c ==> d
>
> and 2 theorems
>
> a /\ b ==> e
>
> e =
Let's say I have a goal,
a /\ b /\ c ==> d
and 2 theorems
a /\ b ==> e
e ==> f
All I need to do to solve the goal is rewrite using a theorem that states
`f`, however I need to first prove e, which is only probable because the
goal assumes `a`.
The basis of my question, is whether or not I can
Is there anyway to reference a specific assumption of the current goal as a
theorem?
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
__
ou use THENL an give it a list of tactics, where the i-th element the
> list is applied to subgoal i.
>
> Personally, I would recommend using ">-".
>
> Best regards,
>
> Heiko
>
>
> On 08/08/2018 07:24 AM, Dylan Melville wrote:
>> When a goal
When a goal is separated into multiple subgoals during a proof of the form
# prove(thm,tactic);;
Where the last tactic is something like
REPEAT CONJ_TAC
Is there a way to specify that the next tactic should be applied to a specific
subgoal? In the proof I’m working on, it was
How do you concatenate terms in HOL?
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info m
ing
> the theorem. I expect that P might be of type `'a -> bool`. In this case you
> need to instantiate 'a to string first.
>
> Best
>
> Thomas
>
> On 23.07.2018 18:10, Dylan Melville wrote:
>> I have a theorem called EX which returns true when a va
contains “T”. Unfortunately my attempts to use INST
on this theorem haven’t worked. Why doesn’t the following work?
INST [`(\x:string. x = “T")`,`P:(string->bool)`] EX;;
Thank you.
-Dylan Melville (McMaster University)
I have a set of theorems, which state:
let thm1 = A;;
let thm2 = A <=> B;;
And I want a theorem that states B. I tried making B my goal, and using
MESON_TAC[thm1,thm2] but MESON timed out. What’s the proper way to prove B?
-
Thank you!
> On Jul 6, 2018, at 1:04 PM, Mario Xerxes Castelán Castro
> wrote:
>
> This is eta conversion. It is handled in HOL4 by the simplifier and both
> HOL4 and HOL Light have conversions called “ETA_CONV” that are more low
> level.
>
> On 06/07/18 12:01, Dyl
Is there a tactical that shows that a term is equal to the same term with an
added abstraction, for example:
|- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n
Or even more simply
|- f:(num->bool) <=> (\x:num. f:(num->bool) )
--
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 Melvill
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
Also, the version Im using is HOL - Light
> On Jun 28, 2018, at 5:38 PM, Dylan Melville wrote:
>
> Is there a tactic for splitting conjoined assumptions into separate
> assumptions?
--
Check out the
Is there a tactic for splitting conjoined assumptions into separate assumptions?
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
Correcting a mistake: the goldInsc definition was supposed to be
# let goldInsc = new_definition `goldInsc gc <=> ~ gc`;;
> On Jun 26, 2018, at 10:35 AM, Dylan Melville wrote:
>
> I’m working on learning the basics of using HOL to solve logic puzzles, such
> as the ‘Portia
I’m working on learning the basics of using HOL to solve logic puzzles, such as
the ‘Portia’s Suitor’ problem:
Portia has a gold casket and a silver casket and has placed a picture of
herself in one of them. On the caskets, she has written the following
inscriptions:
• Gold: The portra
20 matches
Mail list logo
