# [isabelle] Removing trivial premises

```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.