# Re: [isabelle] Removing trivial premises

```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 at 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. :)

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.