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