# [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.*