Re: [isabelle] quoting definitions in latex

* Peter Sewell <Peter.Sewell at> [2007-12-14 12:51]:
> I'd like to write an expository document based on some Isabelle, and
> so need to quote selected definitions, not necessarily in the order
> they appear in the main .thy.

I had a similar problem for my diploma thesis, which I wanted to write
in LaTeX, but quoting many lemmas and definitions.

The attached crude perl script takes a number of theory files as input,
parses them (well, not really, but enough for my purposes) and creates
text_raw {* *} blocks in which it defines appropriate LaTeX commands.

So if you have a constdef foo it defines two LaTeX commands: \fooDef and
\fooDefInline (with different display options).

I put the output of the script into a new theory file with dependencies
on the original theories, processed it with Isabelle into a .tex file
and \included the resulting file into my main .tex file (after removing
the preamble and other unneeded stuff).

Worked very well for me.

#!/usr/bin/perl -w
# (C) 2007 Thomas Bleher <ThomasBleher at>
# Released under the same license as Isabelle (ie BSD)
# Parse theories and create LaTeX commands from all definitions and lemmata.

sub remove_ {
	# only chars are allowed in latex command names, so we substitute numbers and single quotes;
	# all other chars are simply removed, but the char following a removed char is uppercased
	# Example: my_lemma1 becomes myLemmaOne
	my (%replacements) = (0 => "Zero", 1 => "One", 2 => "Two", 3 => "Three", 4 => "Four", 5 => "Five", 6 => "Six", 7 => "Seven", 8 => "Eight", 9 => "Nine", "'" => "SQuote");

	my $text = shift;
	$text =~ s/\Q$_\E/$replacements{$_}_/g for (keys %replacements);
	my @parts = split /[^a-zA-Z0-9]/, $text;
	return (shift @parts).(join '', map {ucfirst} @parts);

my %thms;
sub print_format {
	my ($thyname, $thmname, $locale) = @_;
	if ($locale ne '') {
		$locale =~ /\(in (\w+)\)/ or die "Locale-Error: found '$locale'";
		$thmname = "$1.$thmname";
	if ($thms{$thmname}++) {
		$thmname = "$thyname.$thmname";
		die "Multiple theorems named $thmname" if $thms{$thmname}++;
	my $latexname = remove_ $thmname;
	print "text_raw{*\n\\newcommand{\\${latexname}Inline}{\ at {thm $thmname [no_vars]}}\n*}\n";
	print "text_raw{*\n\\newcommand{\\$latexname}{\n\ at {thm [display] $thmname [no_vars]}\n}\n*}\n\n";

my @files = @ARGV;

my (%done) = map {$_ => 1} @files;
while (@files) {
	my $file = shift @files;
	next if {"Main.thy"=>1,"LaTeXsugar.thy"=>1}->{$file}; # these are the base files, don't process them
	open FILE, "<", $file or do { warn "Could not open file '$file'!"; next; };
	$state = 0;
	print "\n\n(* Reading file $file... *)\n\n";
	local $/ = undef;
	my $data = <FILE>;
	$data =~ s/\(\*.*?\*\)//gs; # remove comments
	my $thyname = ($data =~ /^\s*theory\s+(\w+)(?:\s|$)/ms)[0];
	for (split /\n/, $data) { # crudely parse the theory
		if (/(?:theory\s+\w+\s+|^)imports\s+(.+?)(?:\s+begin|$)/) {
			($imports = $1) =~ s/"//g;
			for (map { $_.".thy" } split /\s+/, $imports) {
				push @files, $_ unless $done{$_};
				$done{$_} = 1;

		# lemmas and theorems can be parsed without much state info
		/^(?:lemma|theorem)\s+(\(in \w+\)\s+|)("?)([\w']+)\2(?:\s+\[[a-z,!_ ]+\])?:/ and print_format($thyname, $3, $1);
		# locale parsing is still *very* rudimentary...
		/^locale\s+("?)(\w+)\1\s*=/ and print_format($thyname, $2."_def",'');

		# constdefs, by contrast, need some more state info:
		/^(?:constdefs)(\s+|$)/ and $state = 1;
		/^(?:defs)(\s+|$)/      and $state = 2;
		/^(?:axioms)(\s+|$)/    and $state = 3;

		/^(?:consts|record|lemma|theorem|primrec|declare|recdef|datatype|text|locale)(\s+|$)/ and $state = 0;

		$state == 0 and /^\s*inductive\s+"?(\w+)\s/ and print_format($thyname, $1.".intros",'');
		$state == 1 and /("?)([\w']+)\1\s+::\s/ and print_format($thyname, $2."_def",'');
		$state  > 1 and /("?)([\w']+)\1\s*:\s+"/ and print_format($thyname, $2,'');

		# still missing: named primrec definitions, locale assumes, lots of more esoteric stuff
	close FILE;

Attachment: signature.asc
Description: Digital signature

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