As Michael said, higher order is all over the place, even
if first order reasoning is commonplace. One of my favourite
higher order statements is the following encapsulation of
Skolemization:
SKOLEM_THM;
val it =
|- ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x):
thm
Konrad.
On Wed, Nov 18, 201
Some of the definitions are higher-order. For example, the universal
quantifier has to be higher order because it's a function that takes a
predicate as an argument.
Even functions like MAP are higher-order because they take functions as
arguments. Often metis is capable of proving useful fac
Dear all:
HOL is a higher order logic theorem prover, while most of the time, we use
first order lib such as season and metis,
So where is the higher order?
Shen
--
___
hol-in
Which binary relation? What do you mean?
Here's a binary relation that relates natural numbers 1 and 2:
val a_binary_relation_def = Define`a_binary_relation x y <=> (x = 1) /\ (y
= 2)`;
Here's a binary relation that relates two Booleans iff exactly one of them
is true:
val another_binary_relation
I have a query that how can we define a binary relation in HOL with a
specified type?
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lis
Just to be clear, Tactician (only for HOL Light at the moment) goes between
the three styles:
- g and e
- prove with THEN/THENL/etc
- Flyspeck's 'prove_by_refinement', which is a hybrid of the above two
Mark.
on 18/11/15 8:54 AM, Ramana Kumar wrote:
> I usually use ">>" instead of literally
I usually use ">>" instead of literally "THEN". Arguably that's still too
much "shift".
Yes I think you're right about tactician - it's for going back and forth
between those styles.
On 18 November 2015 at 08:41, Freek Wiedijk wrote:
> Hi Ramana,
>
> >Apparently Coq somewhat recently gained the
Hi Ramana,
>Apparently Coq somewhat recently gained the ability to be explicit about
>proof structure:
>http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html
>(Of course that comes naturally when using tacticals like THEN, THEN1, etc.)
Not _very_ recently. It was introduced i
