Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Implementing two ML functions regarding depend...

Email Gateway (Jun 06 2022 at 00:15):

From: qj213@cam.ac.uk
Hi,

I'd like to implement two functions in ML, to extract the lemmas and
definitions certain theorems and definitions depend upon. If someone can give
me some pointers to how they should be implemented I would be very grateful.

1. A function that extracts the lemmas used in a theorem's proof.

Suppose I have the theorem
theorem test: "True"
by simp

I'd like a function that works similarly to 'thm_deps test' that gives me a
list of lemma names that are used in the proof of "test".
Concretely a function of the type Toplevel.state => string => string list. It
takes the current top level state and the name of the theorem as the
arguments, and returns the list ["HOL.TrueI", "Drule.protectD",
"Drule.protectI"].

2. A function that extracts the types and definitions used to state a new
   definition.

Suppose I define a function
fun f :: "nat ⇒ nat" where
"f 0 = 0" |
"f (Suc n) = Suc (f n)"

I'd like a function that has the type Toplevel.state => string => (string * string) list. It takes the current top level state and the name of the
definition as the arguments, and returns the entities used in the definition.
In this case I'd like the function to return
[("nat", "typedef nat = "{n. Nat n}"\n morphisms Rep_Nat Abs_Nat\n using
Nat.Zero_RepI by auto"),
("0", "class zero =\n fixes zero :: 'a ("0")"),
("Suc", "definition Suc :: "nat ⇒ nat"\n where "Suc n = Abs_Nat (Suc_Rep
(Rep_Nat n))"")]

I didn't find anything that is similar to what I'm trying to do here.

Again, many thanks if you can give a hint or point me to the right direction!

Best,
Albert

Email Gateway (Jun 06 2022 at 22:59):

From: Talia Ringer <tringer@cs.washington.edu>
Hi all, talking to each other, we found thm_deps in the Isabelle
documentation. But we aren't sure exactly which dependencies it's
printing---is it just those of the theorem, or those of the theorem and
proof, or just those of the proof?

I'm diving into the ML source code for thm_deps to try to figure out how to
write other functions to get dependencies in different ways. If anyone
knows this code well, guidance is appreciated :)

Talia

Email Gateway (Jun 07 2022 at 09:57):

From: Makarius <makarius@sketis.net>
Instead of diving reductionistically into Isabelle/ML, you should step back
and look holistically at Isabelle/Scala.

The latter has access to formal markup (for occurrences of entities in source
text), and also at foundational theory content.

The latter is accessible via the module Export_Theory in Scala. Here is an
example that makes use of it: https://github.com/Deducteam/isabelle_dedukti

Isabelle/Deducti uses proof terms, but this is not required here (and does not
scale beyond the most basic prefix of Isabelle/HOL).

Makarius

Email Gateway (Jun 07 2022 at 15:37):

From: Talia Ringer <tringer@cs.washington.edu>
Thanks, I'll take a look at Dedukti as well!

Last updated: Jul 15 2022 at 23:21 UTC