Email Gateway (Aug 19 2022 at 09:58): Email Gateway (Aug 19 2022 at 09:58):From: Not Sure <kuerzn@googlemail.com>
Hi!
I have two (plus one) questions:
blast, auto, ... are all GREAT!
But is there a way (in ProofGeneral) to see the proofs found by these
tools more detail?
If I have a non-atomic premise like:
[| A ==> B ; ... |] ==> C
how can I "use" it as a rule?
I am looking for somethink like:
apply (rule premise1)
Thanks!
Johannes
Email Gateway (Aug 19 2022 at 09:58):From: Lawrence Paulson <lp15@cam.ac.uk>
You can see some aspects of proofs using proof objects, but it's about as illuminating as reading the assembly language code produced by a compiler.
The answer to your second question is to use a structured proof. Non-atomic premises are all but useless in the apply style. In a structured proof, you can use such a thing exactly like an inference rule.
You will find plenty of Isabelle documentation here: http://isabelle.in.tum.de/documentation.html
Larry Paulson
Email Gateway (Aug 19 2022 at 09:58):From: Peter Lammich <lammich@in.tum.de>
Hi,
On Fr, 2013-01-18 at 12:19 +0000, Lawrence Paulson wrote:
The answer to your second question is to use a structured proof. Non-atomic premises are all but useless in the apply style. In a structured proof, you can use such a thing exactly like an inference rule.
Not an answer for a beginner: I'm frequently using the following code,
that gives you a method rprems, that does exactly the requested thing
(see examples below the code).
We already discussed several times whether we should integrate this
method into Isabelle (see separate post on devel-list)
.. Peter
ML {*
(* Resolve with premises. Copied and adjusted from
Goal.assume_rule_tac. *)
fun rprems_tac ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal, i)
=>
let
fun non_atomic (Const ("==>", _) $ _ $ _) = true
| non_atomic (Const ("all", _) $ _) = true
| non_atomic _ = false;
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
val goal'' = Drule.cterm_rule
(singleton (Variable.export ctxt' ctxt)) goal';
val Rs = filter (non_atomic o Thm.term_of)
(Drule.strip_imp_prems goal'');
val ethms = Rs |> map (fn R =>
(Raw_Simplifier.norm_hhf (Thm.trivial R)));
in eresolve_tac ethms i end
);
(* Resolve with premise. Copied and adjusted from
Goal.assume_rule_tac. *)
fun rprem_tac n ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal,
i) =>
let
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
val goal'' = Drule.cterm_rule
(singleton (Variable.export ctxt' ctxt)) goal';
val R = nth (Drule.strip_imp_prems goal'') (n - 1)
val rl = Raw_Simplifier.norm_hhf (Thm.trivial R)
in
etac rl i
end
);
val setup =
Method.setup @{binding rprems}
(Scan.lift (Scan.option Parse.nat) >> (fn i => fn ctxt =>
SIMPLE_METHOD' (
case i of
NONE => rprems_tac ctxt
| SOME i => rprem_tac i ctxt
))
)
"Resolve with premises"
*}
setup "setup"
(* EXAMPLES: *)
lemma "\<lbrakk> A\<Longrightarrow>B; B\<Longrightarrow>C; A \<rbrakk>
\<Longrightarrow> C"
apply (rprems 2) -- "Explicitely specify number of premise"
apply (rprems 1)
.
lemma "\<lbrakk> A\<Longrightarrow>B; B\<Longrightarrow>C; A \<rbrakk>
\<Longrightarrow> C"
apply (rprems) -- "Resolve with any matching premise,
first to last, backtracking"
apply (rprems)
.
You will find plenty of Isabelle documentation here: http://isabelle.in.tum.de/documentation.html
Larry Paulson
On 18 Jan 2013, at 02:05, Not Sure <kuerzn@googlemail.com> wrote:
Hi!
I have two (plus one) questions:
blast, auto, ... are all GREAT!
But is there a way (in ProofGeneral) to see the proofs found by these
tools more detail?If I have a non-atomic premise like:
[| A ==> B ; ... |] ==> C
how can I "use" it as a rule?
I am looking for somethink like:
apply (rule premise1)
- Where could I have found answers to these questions?
Thanks!
Johannes
Email Gateway (Aug 19 2022 at 10:00):From: Makarius <makarius@sketis.net>
This is what Larry means, when spelled out in Isar:
notepad
begin
assume r: "A ==> C"
have C
proof (rule r)
show A sorry
qed
end
The notepad gives you a structured proof body without an outermost goal
statement getting in the way, so it is usefule for experimentation and
understanding things. If you intent to produce a result eventually, you
can write it like this:
lemma
assumes r: "A ==> C"
shows C
proof (rule r)
show A sorry
qed
If you follow Isar proof structuring the usual way, you should rarely run
into a situation where you get a goal state with the intended rule being
pushed in a goal state too early, and thus prevent its easy manipulation.
(There are ways to do it nonetheless, notably the SUBPROOF and
Subgoal.FOCUS combinators in Isabelle/ML. That is a completely different
story, and not really on-topic for this thread.)
Makarius
Email Gateway (Aug 19 2022 at 10:00):From: Makarius <makarius@sketis.net>
These numbers within proofs scripts are not nice. Many years ago, some
people thinking about structured proofs devised ways to name subgoals and
subgoals premises, instead of numbering them. But I did not find this
very convincing either. It was one of the early achievements of Isar to
manage without that -- and thus continuing the way Larry introduced
elim/dest resolution without physical addressing.
So where are the applications? This thread was started as beginner
questions, to warm up how things are usually done.
Makarius
Email Gateway (Aug 19 2022 at 10:00):From: Makarius <makarius@sketis.net>
Side note: You should definitely try Isabelle/jEdit instead of Proof
General.
I've myself been substantially involved in making Isabelle Proof General
work 13 years ago, but I don't see any reason left to use it today (only
habits of Emacs users that have to be unlearned.)
Makarius
Email Gateway (Aug 19 2022 at 10:00):From: Tobias Nipkow <nipkow@in.tum.de>
AFAIK, jedit does not
The first two are particularly relevant for beginners.
Tobias
Last updated: Apr 25 2024 at 16:19 UTC