Email Gateway (Aug 22 2022 at 13:23): Email Gateway (Aug 22 2022 at 13:23):From: Michael Färber <michael.faerber@uibk.ac.at>
Dear mailing list,
when I resolve theorems, I sometimes obtain trivial premises such as in
this case:
val th1 = Thm.assume @{cprop "P ==> Q"}
val th2 = Thm.assume @{cprop "(P ==> Q) ==> R"}
val th3 = th2 OF [th1]
This produces a th3 with proposition "(P ==> P) ==> R".
However, I would like to obtain only "R".
My ad-hoc solution was to create a function that strips away the first
premise if it is trivial,
and to apply it multiple times on a theorem (via funpow) if the
theorem contains multiple trivial premises.
fun remove_trivial_prem th =
let
val prem = case Thm.prems_of th of x::_ => x | _ => raise Fail "no
premises"
val (l, r) = Logic.dest_implies prem
val _ = @{assert} (l = r)
val ctxt = Thm.theory_of_thm th |> Defs.global_context |> fst
val triv = Thm.trivial (Thm.cterm_of ctxt l)
in Thm.implies_elim th triv
end
val th4 = remove_trivial_prem th3
This now yields a th3 with proposition "R".
However, I feel that this is a bad way to treat trivial premises, among
others because I have to manually determine how many trivial premises
are present in the theorem.
So what is the canonical way to deal with trivial premises?
Cheers,
Michael
P.S.: I know that in Isar, trivial premises can be eliminated when
closing a proof with ".", but I do not know how to do that in ML.
Reading the source for hours unfortunately did not bring me
enlightenment yet. :)
Email Gateway (Aug 22 2022 at 13:23):From: Jeremy Dawson <jeremy.dawson@anu.edu.au>
In an older version of Isabelle you would just use
TRYALL atac th3
and take the head of the resulting sequence
This may no longer be possible of course
Jeremy
Sent from my NOOK
Michael Färber <michael.faerber@uibk.ac.at> wrote:
Dear mailing list,
when I resolve theorems, I sometimes obtain trivial premises such as in
this case:
val th1 = Thm.assume @{cprop "P ==> Q"}
val th2 = Thm.assume @{cprop "(P ==> Q) ==> R"}
val th3 = th2 OF [th1]
This produces a th3 with proposition "(P ==> P) ==> R".
However, I would like to obtain only "R".
My ad-hoc solution was to create a function that strips away the first
premise if it is trivial,
and to apply it multiple times on a theorem (via funpow) if the
theorem contains multiple trivial premises.
fun remove_trivial_prem th =
let
val prem = case Thm.prems_of th of x::_ => x | _ => raise Fail "no
premises"
val (l, r) = Logic.dest_implies prem
val _ = @{assert} (l = r)
val ctxt = Thm.theory_of_thm th |> Defs.global_context |> fst
val triv = Thm.trivial (Thm.cterm_of ctxt l)
in Thm.implies_elim th triv
end
val th4 = remove_trivial_prem th3
This now yields a th3 with proposition "R".
However, I feel that this is a bad way to treat trivial premises, among
others because I have to manually determine how many trivial premises
are present in the theorem.
So what is the canonical way to deal with trivial premises?
Cheers,
Michael
P.S.: I know that in Isar, trivial premises can be eliminated when
closing a proof with ".", but I do not know how to do that in ML.
Reading the source for hours unfortunately did not bring me
enlightenment yet. :)
Email Gateway (Aug 22 2022 at 13:24):From: Makarius <makarius@sketis.net>
On 19/05/16 21:20, Michael Färber wrote:
when I resolve theorems, I sometimes obtain trivial premises such as in
this case:~~~
val th1 = Thm.assume @{cprop "P ==> Q"}
val th2 = Thm.assume @{cprop "(P ==> Q) ==> R"}
val th3 = th2 OF [th1]
~~~This produces a th3 with proposition "(P ==> P) ==> R".
However, I would like to obtain only "R".
Larry Paulson introduced the concept of "elim-resolution" for that
around 1989. Apart from the original papers from that time, it is also
briefly explained in the "implementation" manual in section 4.2.1 – for
tactical backwards proof.
In principle, it is possible to make elim versions of the forward proof
combinators (RS, OF), but it is not done, because backwards proof scales
better to real applications.
So what is the canonical way to deal with trivial premises?
The canonical way is to avoid getting them in the first place, i.e. via
elim-resolution.
P.S.: I know that in Isar, trivial premises can be eliminated when
closing a proof with ".", but I do not know how to do that in ML.
Reading the source for hours unfortunately did not bring me
enlightenment yet. :)
Reading sources is important, but one needs to have an idea about the
general concepts behind them. Apart from the original published
literature (which is naturally a bit outdated), the canonical entry
points are the "implementation" manual and the "isar-ref" manual.
The Prover IDE also helps a lot to navigate around, e.g. to find the
Isabelle/ML definitions of Isabelle/Isar commands.
The implicit finishing of the left-over proof state in structured Isar
proofs is defined in src/Pure/Isar/method.ML as "finish". This is very
specific for how Isar works. It is unlikely to make much sense in a
different context.
Makarius
Last updated: Apr 16 2024 at 08:18 UTC