I had great difficulty to have HOL prove the following subgoal (I turned on
typing for debugging, ``$c`` is a composition operator like ``$o``):

   scf (A :mor -> bool) A (λ(x :mor). x) c sce A (a :mor) = scr A c sce A a
     0.  homset (A :mor -> bool)
     4.  (A :mor -> bool) (a :mor)

Which should be directly derived from two theorems below and assumptions
0,4 (I removed other ones to reduce clutter) :

val it = ⊢ ∀(A :α -> bool). FUNSET A A (λ(x :α). x): thm
> SC_EV;
val it =
   ⊢ ∀(A :mor -> bool) (B :mor -> bool) (f :mor -> mor) (a :mor).
         homset A ⇒
         homset B ⇒
         FUNSET A B f ⇒
         A a ⇒
         (scf A B f c sce A a = sce B (f a)): thm

Eventually I need to manually instantiate everything to solve it:

> e (mp_tac (BETA_RULE (MATCH_MP ((UNDISCH o UNDISCH o SPEC ``a:mor`` o
SPEC ``\x.(x:mor)`` o Q.SPEC `A` o Q.SPEC `A`) SC_EV) (ISPEC
``A:mor->bool`` FUNSET_ID))) >> asm_simp_tac bool_ss []);

It seems the main obstacle was "ground const vs. polymorphic const" based
on the error messages I got during various trials. It was important that I
spelled out all type correctly for it to work.

hol-info mailing list

Reply via email to