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))``,
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
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,
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
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 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)
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
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
> >
&
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
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
>
>
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
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
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
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
18 matches
Mail list logo
