may be a little more
complicated as #n1 may be !x. a -> c /\ d /\ b and I may only want b.
Thanks,
Haitao Zhang
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
I have a theorem that is in a form like !x y z. a ==> b ==> c ==> d and I
would like to match d to the goal. It seems that I need to convert all the
antecedents into a conjunction first. I can (UNDISCH_ALL o SPEC_ALL) to
move everything to the assumptions. But how do I get the conjunctions of
all
ses implicational theorems like this first, and then
> basically applies MATCH_MP_TAC.
>
>
>
> Michael
>
>
>
> *From: *Haitao Zhang
> *Date: *Friday, 1 March 2019 at 11:03
> *To: *hol-info
> *Subject: *[Hol-info] MATCH_MP_TAC and canonical implication form
>
>
You say f is a function. From the context I assume the domain is Nat or f
is a sequence. Mathematically speaking, you should form the partial sums of
f ( sum f from 1 to n), which is a monotonic sequence of nats. Now proof by
contradiction: if your conclusion doesn’t hold, for any m, you can find
llowing a similar path
> > (proof by contradiction), but I don't understand the last step: for any
> > m, the partial sum of f goes up by 1 at n > m, why f must be summable? I
> > think for every monotonic sequence such properties hold.
> >
> > --Chun
> >
&
And even more weird:
> combinTheory;
poly: : error: Value or constructor (combinTheory) has not been declared
Found near combinTheory
Static Errors
> combinTheory.K_DEF;
val it = ⊢ K = (λx y. x): thm
Hmm?!
On Sat, Mar 2, 2019 at 2:34 PM Haitao Zhang wrote:
> For some reason in my ho
On Mon, Feb 25, 2019 at 11:09 AM Haitao Zhang wrote:
> Hi,
>
> I just started HOL and am really enjoying it quite a bit. One difficulty I
> find during interactive tactic proof sessions is to get hold of and
> manipulate assumptions. Right now I find myself using sg to write
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)
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 wrote:
> Sorry Mich
On Tue, Mar 5, 2019 at 10:07 PM 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.)
I think I really like how drule and drule_all work, but is there something
that walks the middle road? I mean drule only discharges one condition; and
drule_all needs all conditions to be discharged. It would be nice to have a
drule that discharges as many as possible and leave the rest as
gt; 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
> *Date: *Wednesday, 6 March 2019 at 18:42
> *To: *"Norrish,
Rules like SYM do not work with top level binders. What is the recommended
way to use them with binders without having to stack up SPEC and GEN?
Thanks,
Haitao
___
hol-info mailing list
hol-info@lists.sourceforge.net
I want to prove ``a <> b`` for some a,b. After stripping I am asked to
prove F. I was able to use the assumptions to prove ``F = T``. At this
point I thought "asm_simp_tac bool_ss []" should finish the proof but it
doesn't. So "pop_assum (fn th => rewrite_tac [th]" actually finished the
work for
It's been about two weeks since I started using HOL. I have been able to
develop a new axiomatization of category theory sufficient enough to prove
Yoneda lemma partially. I want to thank Michael Norrish and Thomas Tuerk
for their generosity in helping me with the learning process. I have gained
oal,
and then use simp_tac bool_ss [] to strip away the conditions that are
dischargable. This is useful when a theorem is used multiple times and
there are multiple assumptions that can be used to instantiate the theorem.
Haitao
On Wed, Mar 6, 2019 at 4:16 PM Haitao Zhang wrote:
> I think I
as:
>
>
> val GEN_IMP_TRANS_conj = (REWRITE_RULE [GSYM satTheory.AND_IMP]
> GEN_IMP_TRANS);
>
> val GEN_IMP_TRANS_conj =
>⊢ ∀P Q R S. (∀x. P x ⇒ Q (R x)) ∧ (∀x. Q x ⇒ S x) ⇒ ∀x. P x ⇒ S (R x):
> thm
>
>
> On Tue, Mar 19, 2019 at 5:30 AM Haitao Zhang wrote:
>
I have two assumptions both in implicative forms with universal
quantification. I would like to obtain an MP in the spirit of the following
theorem:
val GEN_IMP_TRANS = store_thm("GEN_IMP_TRANS",
``!P Q R S. (!x. P x ==> Q (R x)) ==> (!x. Q x ==> S x) ==> (!x. P x
==> S (R x))``,
18 matches
Mail list logo