Re: [isabelle] thm_deps



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.

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
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            http://www.in.tum.de/~berghofe





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