Re: [isabelle] thm_deps

Thanks Stefan, your function works exactly as advertised. Please let me know if you decide to add this to the Isabelle repository, so that I use the official version.


On Mar 30, 2006, at 6:55 AM, Stefan Berghofer wrote:

John Matthews wrote:
  lemma test: "(x::int) * 0 + y = y"
  by auto
  ML {* val _ = map (fn str => print str)
(Symtab.keys (Proofterm.thms_of_proof (proof_of (thm "test"))
                                                Symtab.empty)) *}
However, this gave me not only the lemmas used in the proof of test, but the transitive closure of all the lemmas used in the proof of any lemma used by test as well. What I would like is to just get the names of the lemmas directly used in the proof of test itself. [...]

Dear John,

the following variant of thms_of_proof, which is currently not part of
proofterm.ML, should do what you want:

fun thms_of_proof' (Abst (_, _, prf)) = thms_of_proof' prf
  | thms_of_proof' (AbsP (_, _, prf)) = thms_of_proof' prf
| thms_of_proof' (prf1 %% prf2) = thms_of_proof' prf1 #> thms_of_proof' prf2
  | thms_of_proof' (prf % _) = thms_of_proof' prf
  | thms_of_proof' (PThm (("", _), prf, prop, _)) = thms_of_proof' prf
  | thms_of_proof' (prf' as PThm ((s, _), _, prop, _)) = (fn tab =>
      case Symtab.lookup tab s of
        NONE => Symtab.update (s, [(prop, prf')]) tab
      | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
          Symtab.update (s, (prop, prf')::ps) tab)
| thms_of_proof' (MinProof (prfs, _, _)) = fold (thms_of_proof' o Proofterm.proof_of_min_thm) prfs
  | thms_of_proof' _ = I;

With the above function, you can compute the table of lemmas directly used in
the proof of "test" as follows:

thms_of_proof' (Proofterm.strip_thm (proof_of (thm "test"))) Symtab.empty

Note that you have to strip off the outermost PThm constructor first,
otherwise the table of lemmas used in the proof would only consist
of "test" itself.


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.