Email Gateway (Aug 22 2022 at 09:37): Email Gateway (Aug 22 2022 at 09:37):From: Martin Lee <martinchan2016@gmail.com>
Hi sir,
theory Scratch
imports Pure
begin
lemma shows "[P ∨ Q; P ∨ Q] ⇒ Q ∨ P"
apply (auto)
done
lemma shows "A ∨ (B ∨ A) → B ∨ (A ∨ B"
apply (auto)
done
end
Email Gateway (Aug 22 2022 at 09:37):From: Larry Paulson <lp15@cam.ac.uk>
I’m afraid your input syntax is incorrect. See the documentation for details, e.g.
http://isabelle.in.tum.de/dist/Isabelle2014/doc/prog-prove.pdf
And there are plenty of examples in src/HOL/ex/Classical.thy.
Larry Paulson
Email Gateway (Aug 22 2022 at 09:37):From: Lars Noschinski <noschinl@in.tum.de>
You need to import Main. Importing Pure is almost always the wrong thing
to do.
Email Gateway (Aug 22 2022 at 09:40):From: Mandy Martin <tesleft@hotmail.com>
Hi Lars,
After tried, it return inner syntax error, where is wrong?
theory Scratchimports Mainbegin(lemma "A ∨ (B ∨ A) ⇒ B ∨ (A ∨ B)")lemma "A ∨ (B ∨ A) → B ∨ (A ∨ B)"by blastend
Regards,
Martin Lee
Email Gateway (Aug 22 2022 at 09:41):From: Mandy Martin <tesleft@hotmail.com>
Hi ,
i succeed to run after following example,
but the subgoal is the same as the original lemma,
i guess that it proved directly with logic table.
one number can have many kinds of representation of logic
0010 , And(A,Or(B,.... Or(And(A,B..... etc
A -> B , between A and B, there can be many ways. is this the reason that only one subgoal when prove this?
is resolution algorithm for generating subgoals? if not, what algorithm do it used to generate subgoal?
Regards,
Martin Lee
Last updated: Apr 20 2024 at 01:05 UTC