What did simp[FUNSET_ID, SC_EV] do to this goal, if anything?
I’d expect it to change the goal to
sce A a = scr A c sce A a
(You haven’t shown us any assumptions/theorems about scr.)
Michael
From: Haitao Zhang <zhtp...@gmail.com>
Date: Wednesday, 6 March 2019 at 16:57
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] HOL difficulty with this subgoal
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) :
> FUNSET_ID;
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.
Haitao
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
