Hi Dylan,
1. Your "EX" is basically the same as listTheory.EXISTS_DEF (in HOL4). If
you are in HOL Light, I am sure there is an analogous definition already
available. You should use it, since there are lots of theorems proved about
it already and you will save on work.
2. The problem is likely that you need to first type instantiate the
definition before calling INST.
(Following is HOL4).
First get the definition into your form:
val EXISTS_DEF_0 = LIST_CONJ (map SPEC_ALL (CONJUNCTS
listTheory.EXISTS_DEF));
val EXISTS_DEF_0 =
⊢ (EXISTS P [] ⇔ F) ∧ (EXISTS P (h::t) ⇔ P h ∨ EXISTS P t): thm
Second, type instantiate:
val EXISTS_DEF' = INST_TYPE [alpha |-> ``:string``] EXISTS_DEF_0;
val EXISTS_DEF' = ⊢ (EXISTS P [] ⇔ F) ∧ (EXISTS P (h::t) ⇔ P h ∨ EXISTS P
t): thm
Third, instantiate variable P (now of type ``:string->bool``):
INST [``P:string->bool`` |-> ``(=) "T"``] EXISTS_DEF';
val it =
⊢ (EXISTS ($= "T") [] ⇔ F) ∧
(EXISTS ($= "T") (h::t) ⇔ ("T" = h) ∨ EXISTS ($= "T") t): thm
On Mon, Jul 23, 2018 at 12:41 PM Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> > show_types := true;
> val it = (): unit
> > INFINITY_AX;
> val it = ⊢ ∃(f :ind -> ind). ONE_ONE f ∧ ¬ONTO f: thm
>
> > Il giorno 23 lug 2018, alle ore 18:22, Dylan Melville <
> dylanmelvi...@gmail.com> ha scritto:
> >
> > Is there a way to print theorems with types displayed?
> >
> >> On Jul 23, 2018, at 12:20 PM, Thomas Tuerk <tho...@tuerk-brechen.de>
> wrote:
> >>
> >> Hi,
> >>
> >> hard to say, why it does not work without further details. However, one
> guess is that types do not match. I would recommend showing the types when
> printing 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 value is an
> element of a list. It is defined as:
> >>>
> >>> thm = |- (EX P [] <=> F) /\ (EX P (CONS h t) <=> P h \/ EX P t)
> >>>
> >>> I am trying to use this theorem with `P` being `(\x. x = “T”)` and `t`
> being a long list of strings which 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)
> >>>
> >>>
> >>>
> ------------------------------------------------------------------------------
> >>> 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
> >
> >
> ------------------------------------------------------------------------------
> > 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
>
------------------------------------------------------------------------------
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
