*To*: Michael Färber <michael.faerber at uibk.ac.at>*Subject*: Re: [isabelle] Removing trivial premises*From*: Jeremy Dawson <jeremy.dawson at anu.edu.au>*Date*: Fri, 20 May 2016 17:25:42 +1000*Authentication-results*: uibk.ac.at; dkim=none (message not signed) header.d=none; uibk.ac.at; dmarc=none action=none header.from=anu.edu.au;*Cc*: cl-isabelle-users at lists.cam.ac.uk*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:23

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

- Previous by Date: Re: [isabelle] smt method avoidance
- Next by Date: Re: [isabelle] Shortest way to prove an object-level implication via ML
- Previous by Thread: Re: [isabelle] Removing trivial premises
- Next by Thread: [isabelle] smt method avoidance
- Cl-isabelle-users May 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list