If you really need to instantiate a theorem by hand, using Q.SPEC_THEN and Q.ISPEC_THEN is usually better. The first is also available under the name qspec_then.
E.g., you can do qspec_then `a` mp_tac mytheorem If you need to do lots of specialisations you can use the list forms: qspecl_then [`a`, `b`, `c`] mp_tac mytheorem If you want to specialise an assumption (rather than mytheorem), use first_x_assum or similar to pull that assumption out of the assumptions: first_x_assum (qspecl_then [`a+6`, `f b`] mp_tac) The big advantage of Q.SPEC_THEN and friends is that the arguments are parsed in the context of the goal (so something like `f b` above will ensure that f and b get the right types rather than `’a->’b` and `’a`). Michael From: Haitao Zhang <zhtp...@gmail.com> Date: Wednesday, 6 March 2019 at 18:42 To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au> Cc: hol-info <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] HOL difficulty with this subgoal I should also add that simp [..] would take a step in the wrong direction as I have an equality on the assumptions list that I used earlier in the other direction (through SYM). simp_tac does not do anything as assumptions are required. And as I can see now the step does not actually depend on FUNSET_ID as there is already a fact proved using it in the assumptions. I was using FUNSET_ID in the earlier solution because I was manually instantiating the antecedent (instead of searching for it among the assumptions). Haitao On Tue, Mar 5, 2019 at 11:30 PM Haitao Zhang <zhtp...@gmail.com<mailto:zhtp...@gmail.com>> wrote: Sorry Michael I cut and pasted the wrong goal for some reason. Here is the corrected one: scf (A :mor -> bool) A (λ(x :mor). x) c sce A (a :mor) = sce A ((λ(x :mor). x) a) ------------------------------------ 0. homset (A :mor -> bool) 4. (A :mor -> bool) (a :mor) It doesn't depend on scr. I also found out that writing out in this non beta-reduced form I can solve it with irule SC_EV >> asm_simp_tac bool_ss [], but not in the beta reduced form. metis_tac and prove_tac still fails on both (beta-reduced or not reduced). Sorry for the confusion. Haitao On Tue, Mar 5, 2019 at 10:07 PM <michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote: 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<mailto:zhtp...@gmail.com>> Date: Wednesday, 6 March 2019 at 16:57 To: hol-info <hol-info@lists.sourceforge.net<mailto: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<mailto:hol-info@lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
