Re: [isabelle] Embeding theories in existing latex document



I do this all the time. You just have to grab the generated TeX output and insert it into your TeX file, within the brackets \begin {isabelle}...\end{isabelle} or \isa{...}.

The generated TeX is verbose because it refers to virtually all symbols via macros. I attach a Perl script that replaces these macros by the corresponding characters.

If you want to edit this TeX further, I advise you to use a TeX gui (such as TeXShop) that maps between the typeset output and the corresponding place in the source.

All of this is completely unsupported. I seem to be the only person who wants to write papers directly in LaTeX rather than using Isabelle markup.

Larry


On 18 Jan 2007, at 11:47, Martin Klebermaß wrote:

i have a separate latex document where i want to present my theories, and want to extract some of the definitions and proofs out of my isabelle scripts and embed them into my document.

Is this somehow possible. I have only seen it the other way round embedding latex code into the isabelle documents.

#!/usr/bin/perl
#simplify the output of an Isar proof presentation

sub replaceisa {
    my ($file) = @_;

    open (FILE, $file) || die $!;
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
    close FILE || die $!;

    $_ = $text;

    s/}% *\n/}\n/g;    #can't use the $ anchor because text is one string!
    s/\\isamarkuptrue%\n//g;
    s/\\isamarkupfalse%\n//g;
    s/{\\isadigit{(\w+)}}/\1/g;
    s/{isabellebody}/{isabelle}/g;
    s/{\\isacharquery}/?/g;
    s/{\\isacharbang}/!/g;
    s/{\\isachardot}/./g;
    s/{\\isacharsemicolon}/;/g;
    s/{\\isacharhash}/\\#/g;
    s/{\\isachardollar}/\\\$/g;
    s/{\\isacharpercent}/\\%/g;
    s/{\\isacharampersand}/\\&/g;
    s/{\\isacharprime}/'/g;
    s/{\\isacharparenleft}/(/g;
    s/{\\isacharparenright}/)/g;
    s/{\\isacharasterisk}/*/g;
    s/{\\isacharat}/@/g;
    s!{\\isacharslash}!/!g;
    s/{\\isacharminus}/-/g;
    s/{\\isacharplus}/+/g;
    s/{\\isacharless}/</g;
    s/{\\isachargreater}/>/g;
    s/{\\isacharbrackleft}/[/g;
    s/{\\isacharbrackright}/]/g;
    s/{\\isachardoublequote}/"/g;
    s/{\\isacharunderscore}/\\_/g;
    s/{\\isacharbar}/|/g;
    s/{\\isacharcolon}/:/g;
    s/{\\isasymColon}/::/g;
    s/{\\isacharcomma}/,/g;
    s/{\\isacharequal}/=/g;
    s/{\\isacharbackquote}/`/g;
    s/{\\isacharminus}/-/g;
    s/{\\isacharasterisk}/*/g;

# remove superfluous {...} that remain
    s/{(\\\w+)}/\1 /g;
    s/{}(\S-)/\1/g;

# here the string to be replaced extends over two lines!
    s/\\end{isabelle} *\n(\\rulename{[^{}]+})/\1\n\\end{isabelle}/g;

    $result = $_;

    if ($text ne $result) {
	print STDERR "converting $file\n";
        if (! -f "$file~~") {
	    rename $file, "$file~~" || die $!;
        }
	open (FILE, "> $file") || die $!;
	print FILE $result;
	close FILE || die $!;
    }
}


## main

foreach $file (@ARGV) {
  eval { &replaceisa($file); };
  if ($@) { print STDERR "*** replaceisa $file: ", $@, "\n"; }
}


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