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.