-
-NB: the formalization is not completely sound! It does not enforce
-distinctness of variable names in contexts!
[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
Author's PhD thesis, 1999.
-
Frederic Blanqui has contributed a theory of guardedness, which is
demonstrated by proofs of some roving agent protocols.
-
-
-The distribution contains simulation relations, temporal logic, and an abstraction theory.
-Everything is based upon a domain-theoretic model of finite and infinite sequences.
-
-
-This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
-following H. Heuser, Funktionalanalysis, p. 228 -232.
-The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis.
-It is a conclusion of Zorn's lemma.
-
-Two different formaulations of the theorem are presented, one for general real vectorspaces
-and its application to normed vectorspaces.
-
-The theorem says, that every continous linearform, defined on arbitrary subspaces
-(not only one-dimensional subspaces), can be extended to a continous linearform on
-the whole vectorspace.
-
-
-
-
-This directory contains a formalization of the meta theory of I/O automata in HOL.
-This formalization has been significantly changed and extended. The new version
-is available in the subdirectory HOLCF/IOA. There are also the proofs of two
-communication protocols which formerly have been here.
-
-
-
diff -r f4c82c165f58 -r 2aea76fe9c73 src/HOL/Induct/README.html
--- a/src/HOL/Induct/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-
-
-
-
-
- This directory is a collection of small examples to demonstrate
-Isabelle/HOL's (co)inductive definitions package. Large examples appear on
-many other directories, such as Auth, IMP and Lambda.
-
-
Last modified 20.5.2000
-
-
-
diff -r f4c82c165f58 -r 2aea76fe9c73 src/HOL/README.html
--- a/src/HOL/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-
-
-
-
-
- \n" + sessions.map(session_entry(_)).mkString + "
") +
+ end_document
+ }
}
diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Thy/present.ML Tue Mar 12 22:24:01 2013 +0100
@@ -14,9 +14,8 @@
include BASIC_PRESENT
val session_name: theory -> string
val read_variant: string -> string * string
- val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
- string list -> string -> bool * string -> Url.T option * bool -> bool ->
- theory list -> unit (*not thread-safe!*)
+ val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
+ string * string -> bool * string -> bool -> theory list -> unit (*not thread-safe!*)
val finish: unit -> unit (*not thread-safe!*)
val init_theory: string -> unit
val theory_source: string -> (unit -> HTML.text) -> unit
@@ -45,15 +44,6 @@
val graph_pdf_path = Path.basic "session_graph.pdf";
val graph_eps_path = Path.basic "session_graph.eps";
-val session_path = Path.basic ".session";
-val session_entries_path = Path.explode ".session/entries";
-val pre_index_path = Path.explode ".session/pre-index";
-
-fun mk_rel_path [] ys = Path.make ys
- | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
- | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
- Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
-
fun show_path path = Path.implode (Path.append (File.pwd ()) path);
@@ -62,37 +52,48 @@
structure Browser_Info = Theory_Data
(
- type T = {name: string, session: string list, is_local: bool};
- val empty = {name = "", session = [], is_local = false}: T;
+ type T = {chapter: string, name: string};
+ val empty = {chapter = Context.PureN, name = Context.PureN}: T;
fun extend _ = empty;
fun merge _ = empty;
);
-val put_info = Browser_Info.put;
-val get_info = Browser_Info.get;
-val session_name = #name o get_info;
+val session_name = #name o Browser_Info.get;
+val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
(** graphs **)
fun ID_of sess s = space_implode "/" (sess @ [s]);
-fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy);
+fun ID_of_thy thy = ID_of (session_chapter_name thy) (Context.theory_name thy);
+fun theory_link (curr_chapter, curr_session) thy =
+ let
+ val {chapter, name = session} = Browser_Info.get thy;
+ val link = html_path (Context.theory_name thy);
+ in
+ if curr_session = session then SOME link
+ else if curr_chapter = chapter then
+ SOME (Path.appends [Path.parent, Path.basic session, link])
+ else if chapter = Context.PureN then NONE
+ else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
+ end;
(*retrieve graph data from initial collection of theories*)
-fun init_graph remote_path curr_sess = rev o map (fn thy =>
+fun init_graph (curr_chapter, curr_session) = rev o map (fn thy =>
let
- val name = Context.theory_name thy;
- val {name = sess_name, session, is_local} = get_info thy;
+ val {chapter, name = session_name} = Browser_Info.get thy;
+ val thy_name = Context.theory_name thy;
+ val path =
+ (case theory_link (curr_chapter, curr_session) thy of
+ NONE => ""
+ | SOME p => Path.implode p);
val entry =
- {name = name, ID = ID_of session name, dir = sess_name,
- path =
- if null session then "" else
- if is_some remote_path andalso not is_local then
- Url.implode (Url.append (the remote_path) (Url.File
- (Path.append (Path.make session) (html_path name))))
- else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
+ {name = thy_name,
+ ID = ID_of [chapter, session_name] thy_name,
+ dir = session_name,
+ path = path,
unfold = false,
parents = map ID_of_thy (Theory.parents_of thy),
content = []};
@@ -130,8 +131,8 @@
val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
-fun init_browser_info remote_path curr_sess thys = make_browser_info
- (Symtab.empty, [], [], [], init_graph remote_path curr_sess thys);
+fun init_browser_info session thys =
+ make_browser_info (Symtab.empty, [], [], [], init_graph session thys);
fun map_browser_info f {theories, files, tex_index, html_index, graph} =
make_browser_info (f (theories, files, tex_index, html_index, graph));
@@ -189,54 +190,30 @@
(* session_info *)
type session_info =
- {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
+ {name: string, chapter: string, info_path: Path.T,
info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
- documents: (string * string) list, doc_dump: (bool * string), remote_path: Url.T option,
- verbose: bool, readme: Path.T option};
+ documents: (string * string) list, doc_dump: (bool * string), verbose: bool,
+ readme: Path.T option};
fun make_session_info
- (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output,
- documents, doc_dump, remote_path, verbose, readme) =
- {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
- info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
- documents = documents, doc_dump = doc_dump, remote_path = remote_path,
- verbose = verbose, readme = readme}: session_info;
+ (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
+ documents, doc_dump, verbose, readme) =
+ {name = name, chapter = chapter, info_path = info_path, info = info,
+ doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
+ documents = documents, doc_dump = doc_dump, verbose = verbose,
+ readme = readme}: session_info;
(* state *)
val session_info = Unsynchronized.ref (NONE: session_info option);
-fun session_default x f = (case ! session_info of NONE => x | SOME info => f info);
+fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
(** document preparation **)
-(* maintain session index *)
-
-val session_entries =
- HTML.session_entries o
- map (fn name => (Url.File (Path.append (Path.basic name) index_path), name));
-
-fun get_entries dir =
- split_lines (File.read (Path.append dir session_entries_path));
-
-fun put_entries entries dir =
- File.write (Path.append dir session_entries_path) (cat_lines entries);
-
-
-fun create_index dir =
- File.read (Path.append dir pre_index_path) ^
- session_entries (get_entries dir) ^ HTML.end_document
- |> File.write (Path.append dir index_path);
-
-fun update_index dir name =
- (case try get_entries dir of
- NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir)
- | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
-
-
(* document variants *)
fun read_variant str =
@@ -248,19 +225,14 @@
(* init session *)
-fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
-
-fun init build info info_path doc doc_graph document_output doc_variants path name
- (doc_dump as (_, dump_prefix)) (remote_path, first_time) verbose thys =
+fun init build info info_path doc doc_graph document_output doc_variants
+ (chapter, name) (doc_dump as (_, dump_prefix)) verbose thys =
if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
(browser_info := empty_browser_info; session_info := NONE)
else
let
- val parent_name = name_of_session (take (length path - 1) path);
- val session_name = name_of_session path;
- val sess_prefix = Path.make path;
- val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
- val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output);
+ val doc_output =
+ if document_output = "" then NONE else SOME (Path.explode document_output);
val documents =
if doc = "" then []
@@ -269,11 +241,6 @@
else (); [])
else doc_variants;
- val parent_index_path = Path.append Path.parent index_path;
- val index_up_lnk =
- if first_time then
- Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
- else Url.File parent_index_path;
val readme =
if File.exists readme_html_path then SOME readme_html_path
else if File.exists readme_path then SOME readme_path
@@ -282,14 +249,12 @@
val docs =
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
- val index_text = HTML.begin_index (index_up_lnk, parent_name)
- (Url.File index_path, session_name) docs (Url.explode "medium.html");
in
session_info :=
- SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc,
- doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme));
- browser_info := init_browser_info remote_path path thys;
- add_html_index (0, index_text)
+ SOME (make_session_info (name, chapter, info_path, info, doc,
+ doc_graph, doc_output, documents, doc_dump, verbose, readme));
+ browser_info := init_browser_info (chapter, name) thys;
+ add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
end;
@@ -337,15 +302,18 @@
fun finish () =
- session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output,
- documents, doc_dump = (dump_copy, dump_prefix), path, verbose, readme, ...} =>
+ with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output,
+ documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} =>
let
val {theories, files, tex_index, html_index, graph} = ! browser_info;
val thys = Symtab.dest theories;
- val parent_html_prefix = Path.append html_prefix Path.parent;
+
+ val chapter_prefix = Path.append info_path (Path.basic chapter);
+ val session_prefix = Path.append chapter_prefix (Path.basic name);
fun finish_html (a, {html, ...}: theory_info) =
- File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
+ File.write_buffer (Path.append session_prefix (html_path a))
+ (Buffer.add HTML.end_document html);
val sorted_graph = sorted_index graph;
val opt_graphs =
@@ -355,21 +323,19 @@
val _ =
if info then
- (Isabelle_System.mkdirs (Path.append html_prefix session_path);
- File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
- File.write (Path.append html_prefix session_entries_path) "";
- create_index html_prefix;
- if length path > 1 then update_index parent_html_prefix name else ();
- (case readme of NONE => () | SOME path => File.copy path html_prefix);
- Graph_Display.write_graph_browser (Path.append html_prefix graph_path) sorted_graph;
+ (Isabelle_System.mkdirs session_prefix;
+ File.write_buffer (Path.append session_prefix index_path)
+ (index_buffer html_index |> Buffer.add HTML.end_document);
+ (case readme of NONE => () | SOME path => File.copy path session_prefix);
+ Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph;
Isabelle_System.isabelle_tool "browser" "-b";
- File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
- List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
+ File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
+ List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt)
(HTML.applet_pages name (Url.File index_path, name));
- File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
+ File.copy (Path.explode "~~/etc/isabelle.css") session_prefix;
List.app finish_html thys;
List.app (uncurry File.write) files;
- if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
+ if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
else ())
else ();
@@ -415,7 +381,7 @@
val jobs =
(if info orelse is_none doc_output then
- map (document_job html_prefix true) documents
+ map (document_job session_prefix true) documents
else []) @
(case doc_output of
NONE => []
@@ -430,33 +396,23 @@
(* theory elements *)
-fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info);
+fun init_theory name = with_session_info () (fn _ => init_theory_info name empty_theory_info);
fun theory_source name mk_text =
- session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
+ with_session_info () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
fun theory_output name s =
- session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s));
+ with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s));
-fun parent_link remote_path curr_session thy =
- let
- val {name = _, session, is_local} = get_info thy;
- val name = Context.theory_name thy;
- val link =
- if null session then NONE
- else SOME
- (if is_some remote_path andalso not is_local then
- Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name)))
- else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
- in (link, name) end;
-
fun begin_theory update_time dir thy =
- session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
+ with_session_info thy (fn {name = session_name, chapter, info_path, ...} =>
let
val name = Context.theory_name thy;
val parents = Theory.parents_of thy;
- val parent_specs = map (parent_link remote_path path) parents;
+ val parent_specs = parents |> map (fn parent =>
+ (Option.map Url.File (theory_link (chapter, session_name) parent),
+ (Context.theory_name parent)));
val files = []; (* FIXME *)
val files_html = files |> map (fn (raw_path, loadit) =>
@@ -464,18 +420,22 @@
val path = File.check_file (File.full_path dir raw_path);
val base = Path.base path;
val base_html = html_ext base;
- val _ = add_file (Path.append html_prefix base_html,
- HTML.external_file (Url.File base) (File.read path));
+ (* FIXME retain file path!? *)
+ val session_prefix = Path.appends [info_path, Path.basic chapter, Path.basic name];
+ val _ =
+ add_file (Path.append session_prefix base_html,
+ HTML.external_file (Url.File base) (File.read path));
in (Url.File base_html, Url.File raw_path, loadit) end);
fun prep_html_source (tex_source, html_source, html) =
- let
- val txt = HTML.begin_theory (Url.File index_path, session)
- name parent_specs files_html (Buffer.content html_source)
+ let val txt = HTML.begin_theory name parent_specs files_html (Buffer.content html_source)
in (tex_source, Buffer.empty, Buffer.add txt html) end;
val entry =
- {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
+ {name = name,
+ ID = ID_of [chapter, session_name] name,
+ dir = session_name,
+ unfold = true,
path = Path.implode (html_path name),
parents = map ID_of_thy parents,
content = []};
@@ -484,7 +444,7 @@
add_graph_entry (update_time, entry);
add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
add_tex_index (update_time, Latex.theory_entry name);
- put_info {name = sess_name, session = path, is_local = is_some remote_path} thy
+ Browser_Info.put {chapter = chapter, name = session_name} thy
end);
diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Thy/present.scala Tue Mar 12 22:24:01 2013 +0100
@@ -7,35 +7,41 @@
package isabelle
+import scala.collection.immutable.SortedMap
+
+
object Present
{
- /* maintain session index -- NOT thread-safe */
+ /* maintain chapter index -- NOT thread-safe */
private val index_path = Path.basic("index.html")
- private val session_entries_path = Path.explode(".session/entries")
- private val pre_index_path = Path.explode(".session/pre-index")
+ private val sessions_path = Path.basic(".sessions")
- private def get_entries(dir: Path): List[String] =
- split_lines(File.read(dir + session_entries_path))
+ private def read_sessions(dir: Path): List[(String, String)] =
+ {
+ import XML.Decode._
+ list(pair(string, string))(YXML.parse_body(File.read(dir + sessions_path)))
+ }
- private def put_entries(entries: List[String], dir: Path): Unit =
- File.write(dir + session_entries_path, cat_lines(entries))
+ private def write_sessions(dir: Path, sessions: List[(String, String)])
+ {
+ import XML.Encode._
+ File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
+ }
- def create_index(dir: Path): Unit =
- File.write(dir + index_path,
- File.read(dir + pre_index_path) +
- HTML.session_entries(get_entries(dir)) +
- HTML.end_document)
+ def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)])
+ {
+ val dir = info_path + Path.basic(chapter)
+ Isabelle_System.mkdirs(dir)
- def update_index(dir: Path, names: List[String]): Unit =
- try {
- put_entries(get_entries(dir).filterNot(names.contains) ::: names, dir)
- create_index(dir)
- }
- catch {
- case ERROR(msg) =>
- java.lang.System.err.println(
- "### " + msg + "\n### Browser info: failed to update session index of " + dir)
- }
+ val sessions0 =
+ try { read_sessions(dir + sessions_path) }
+ catch { case ERROR(_) => Nil case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
+
+ val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
+
+ write_sessions(dir, sessions)
+ File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
+ }
}
diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Tools/build.ML Tue Mar 12 22:24:01 2013 +0100
@@ -109,11 +109,12 @@
fun build args_file = Command_Line.tool (fn () =>
let
val (command_timings, (do_output, (options, (verbose, (browser_info,
- (parent_name, (name, theories))))))) =
+ (parent_name, (chapter, (name, theories)))))))) =
File.read (Path.explode args_file) |> YXML.parse_body |>
let open XML.Decode in
pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
- (pair string (pair string ((list (pair Options.decode (list string))))))))))
+ (pair string (pair string (pair string
+ ((list (pair Options.decode (list string)))))))))))
end;
val document_variants =
@@ -125,18 +126,15 @@
val _ = writeln ("\fSession.name = " ^ name);
val _ =
- (case Session.path () of
- [] => ()
- | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
- val _ =
- Session.init do_output false
- (Options.bool options "browser_info") browser_info
+ Session.init do_output
+ (Options.bool options "browser_info")
+ (Path.explode browser_info)
(Options.string options "document")
(Options.bool options "document_graph")
(Options.string options "document_output")
document_variants
- parent_name name
- (false, "") ""
+ parent_name (chapter, name)
+ (false, "")
verbose;
val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Tools/build.scala Tue Mar 12 22:24:01 2013 +0100
@@ -14,6 +14,7 @@
import java.util.zip.GZIPInputStream
import scala.collection.SortedSet
+import scala.collection.mutable
import scala.annotation.tailrec
@@ -46,6 +47,8 @@
/** session information **/
// external version
+ abstract class Entry
+ sealed case class Chapter(name: String) extends Entry
sealed case class Session_Entry(
pos: Position.T,
name: String,
@@ -55,10 +58,11 @@
description: String,
options: List[Options.Spec],
theories: List[(List[Options.Spec], List[String])],
- files: List[String])
+ files: List[String]) extends Entry
// internal version
sealed case class Session_Info(
+ chapter: String,
select: Boolean,
pos: Position.T,
groups: List[String],
@@ -72,8 +76,8 @@
def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
- def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
- : (String, Session_Info) =
+ def session_info(options: Options, select: Boolean, dir: Path,
+ chapter: String, entry: Session_Entry): (String, Session_Info) =
try {
val name = entry.name
@@ -87,10 +91,11 @@
entry.theories.map({ case (opts, thys) =>
(session_options ++ opts, thys.map(Path.explode(_))) })
val files = entry.files.map(Path.explode(_))
- val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
+ val entry_digest =
+ SHA1.digest((chapter, name, entry.parent, entry.options, entry.theories).toString)
val info =
- Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
+ Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
entry.parent, entry.description, session_options, theories, files, entry_digest)
(name, info)
@@ -180,6 +185,9 @@
/* parser */
+ val chapter_default = "Unsorted"
+
+ private val CHAPTER = "chapter"
private val SESSION = "session"
private val IN = "in"
private val DESCRIPTION = "description"
@@ -189,10 +197,20 @@
lazy val root_syntax =
Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
- (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
+ (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
+ IN + DESCRIPTION + OPTIONS + THEORIES + FILES
private object Parser extends Parse.Parser
{
+ def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos)
+
+ def chapter(pos: Position.T): Parser[Chapter] =
+ {
+ val chapter_name = atom("chapter name", _.is_name)
+
+ command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
+ }
+
def session_entry(pos: Position.T): Parser[Session_Entry] =
{
val session_name = atom("session name", _.is_name)
@@ -219,11 +237,19 @@
Session_Entry(pos, a, b, c, d, e, f, g, h) }
}
- def parse_entries(root: Path): List[Session_Entry] =
+ def parse_entries(root: Path): List[(String, Session_Entry)] =
{
val toks = root_syntax.scan(File.read(root))
- parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
- case Success(result, _) => result
+
+ parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match {
+ case Success(result, _) =>
+ var chapter = chapter_default
+ val entries = new mutable.ListBuffer[(String, Session_Entry)]
+ result.foreach {
+ case Chapter(name) => chapter = name
+ case session_entry: Session_Entry => entries += ((chapter, session_entry))
+ }
+ entries.toList
case bad => error(bad.toString)
}
}
@@ -250,7 +276,8 @@
def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
{
val root = dir + ROOT
- if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
+ if (root.is_file)
+ Parser.parse_entries(root).map(p => session_info(options, select, dir, p._1, p._2))
else Nil
}
@@ -398,7 +425,7 @@
val groups =
if (info.groups.isEmpty) ""
else info.groups.mkString(" (", " ", ")")
- progress.echo("Session " + name + groups)
+ progress.echo("Session " + info.chapter + "/" + name + groups)
}
val thy_deps =
@@ -470,9 +497,10 @@
{
import XML.Encode._
pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
- pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+ pair(string, pair(string, pair(string,
+ list(pair(Options.encode, list(Path.encode)))))))))))(
(command_timings, (do_output, (info.options, (verbose, (browser_info,
- (parent, (name, info.theories))))))))
+ (parent, (info.chapter, (name, info.theories)))))))))
}))
private val env =
@@ -568,7 +596,6 @@
private def log_gz(name: String): Path = log(name).ext("gz")
private val SESSION_NAME = "\fSession.name = "
- private val SESSION_PARENT_PATH = "\fSession.parent_path = "
sealed case class Log_Info(
@@ -727,7 +754,7 @@
}
// scheduler loop
- case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int)
+ case class Result(current: Boolean, heap: String, rc: Int)
def sleep(): Unit = Thread.sleep(500)
@@ -748,7 +775,7 @@
val res = job.join
progress.echo(res.err)
- val (parent_path, heap) =
+ val heap =
if (res.rc == 0) {
(output_dir + log(name)).file.delete
@@ -757,13 +784,7 @@
File.write_gzip(output_dir + log_gz(name),
sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out)
- val parent_path =
- if (job.info.options.bool("browser_info"))
- res.out_lines.find(_.startsWith(SESSION_PARENT_PATH))
- .map(_.substring(SESSION_PARENT_PATH.length))
- else None
-
- (parent_path, heap)
+ heap
}
else {
(output_dir + Path.basic(name)).file.delete
@@ -778,10 +799,10 @@
progress.echo("\n" + cat_lines(tail))
}
- (None, no_heap)
+ no_heap
}
loop(pending - name, running - name,
- results + (name -> Result(false, parent_path, heap, res.rc)))
+ results + (name -> Result(false, heap, res.rc)))
//}}}
case None if (running.size < (max_jobs max 1)) =>
//{{{ check/start next job
@@ -789,7 +810,7 @@
case Some((name, info)) =>
val parent_result =
info.parent match {
- case None => Result(true, None, no_heap, 0)
+ case None => Result(true, no_heap, 0)
case Some(parent) => results(parent)
}
val output = output_dir + Path.basic(name)
@@ -812,10 +833,10 @@
val all_current = current && parent_result.current
if (all_current)
- loop(pending - name, running, results + (name -> Result(true, None, heap, 0)))
+ loop(pending - name, running, results + (name -> Result(true, heap, 0)))
else if (no_build) {
if (verbose) progress.echo("Skipping " + name + " ...")
- loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
+ loop(pending - name, running, results + (name -> Result(false, heap, 1)))
}
else if (parent_result.rc == 0 && !progress.stopped) {
progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
@@ -826,7 +847,7 @@
}
else {
progress.echo(name + " CANCELLED")
- loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
+ loop(pending - name, running, results + (name -> Result(false, heap, 1)))
}
case None => sleep(); loop(pending, running, results)
}
@@ -847,11 +868,11 @@
else loop(queue, Map.empty, Map.empty)
val session_entries =
- (for ((name, res) <- results.iterator if res.parent_path.isDefined)
- yield (res.parent_path.get, name)).toList.groupBy(_._1).map(
- { case (p, es) => (p, es.map(_._2).sorted) })
- for ((p, names) <- session_entries)
- Present.update_index(browser_info + Path.explode(p), names)
+ (for { (name, res) <- results.iterator; info = full_tree(name) }
+ yield (info.chapter, (name, info.description))).toList.groupBy(_._1).map(
+ { case (chapter, es) => (chapter, es.map(_._2)) })
+ for ((chapter, entries) <- session_entries)
+ Present.update_chapter_index(browser_info, chapter, entries)
val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
if (rc != 0 && (verbose || !no_build)) {
diff -r f4c82c165f58 -r 2aea76fe9c73 src/Sequents/README.html
--- a/src/Sequents/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-
-
-
-
-
-
-
Sequents/README
-
-
-
-
-
Sequents: Various Sequent Calculi
-
-This directory contains the ML sources of the Isabelle system for
-various Sequent, Linear, and Modal Logic.
-
-The subdirectories ex, ex/LK, ex/ILL,
-ex/Modal contain some examples.
-
-Much of the work in Modal logic was done by Martin Coen. Thanks to
-Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
-reorganized the files and supplied Linear Logic. Jacob Frost provided
-some improvements to the syntax of sequents.
-
-
Useful references on sequent calculi:
-
-
-- Steve Reeves and Michael Clarke,
- Logic for Computer Science (Addison-Wesley, 1990)
- - G. Takeuti,
- Proof Theory (North Holland, 1987)
-
-
-Useful references on Modal Logics:
-
-- Melvin C Fitting,
- Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
-
- - Lincoln A. Wallen,
- Automated Deduction in Nonclassical Logics (MIT Press, 1990)
-
-
-Useful references on Linear Logic:
-
-- A. S. Troelstra
- Lectures on Linear Logic (CSLI, 1992)
-
- - S. Kalvala and V. de Paiva
- Linear Logic in Isabelle (in TR 379, University of Cambridge
- Computer Lab, 1995, ed L. Paulson)
-
-
-
diff -r f4c82c165f58 -r 2aea76fe9c73 src/Sequents/ROOT
--- a/src/Sequents/ROOT Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Sequents/ROOT Tue Mar 12 22:24:01 2013 +0100
@@ -1,9 +1,41 @@
+chapter Sequents
+
session Sequents = Pure +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
- Classical Sequent Calculus based on Pure Isabelle.
+ Various Sequent Calculi for Classical, Linear, and Modal Logic.
+
+ Much of the work in Modal logic was done by Martin Coen. Thanks to Rajeev
+ Gore' for supplying the inference system for S43. Sara Kalvala reorganized
+ the files and supplied Linear Logic. Jacob Frost provided some improvements
+ to the syntax of sequents.
+
+
+ Useful references on sequent calculi:
+
+ Steve Reeves and Michael Clarke, Logic for Computer Science
+ (Addison-Wesley, 1990)
+
+ G. Takeuti, Proof Theory (North Holland, 1987)
+
+
+ Useful references on Modal Logics:
+
+ Melvin C Fitting, Proof Methods for Modal and Intuitionistic Logics
+ (Reidel, 1983)
+
+ Lincoln A. Wallen, Automated Deduction in Nonclassical Logics (MIT Press,
+ 1990)
+
+
+ Useful references on Linear Logic:
+
+ A. S. Troelstra, Lectures on Linear Logic (CSLI, 1992)
+
+ S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
+ of Cambridge Computer Lab, 1995, ed L. Paulson)
*}
options [document = false]
theories
diff -r f4c82c165f58 -r 2aea76fe9c73 src/ZF/AC/README.html
--- a/src/ZF/AC/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-
-
-
-
-
-
-
ZF/AC/README
-
-
-
-
-
AC -- Equivalents of the Axiom of Choice
-
-Krzysztof Grabczewski has mechanized the first two chapters of the book
-
-
-
-@book{rubin&rubin,
- author = "Herman Rubin and Jean E. Rubin",
- title = "Equivalents of the Axiom of Choice, {II}",
- publisher = "North-Holland",
- year = 1985}
-
-
-
-The report
-Mechanizing Set Theory,
-by Paulson and Grabczewski, describes both this development and ZF's theories
-of cardinals.
-
-
-
diff -r f4c82c165f58 -r 2aea76fe9c73 src/ZF/Coind/README.html
--- a/src/ZF/Coind/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-
-
-
-
-
-
ZF/Coind/README
-
-
-
-
-
Coind -- A Coinduction Example
-
-Jacob Frost has mechanized the proofs from the article
-
-
-
-@Article{milner-coind,
- author = "Robin Milner and Mads Tofte",
- title = "Co-induction in Relational Semantics",
- journal = TCS,
- year = 1991,
- volume = 87,
- pages = "209--220"}
-
-
-
It involves proving the consistency of the dynamic and static semantics
-for a small functional language. A codatatype definition specifies values and
-value environments in mutual recursion: non-well-founded values represent
-recursive functions; value environments are variant functions from variables
-into values.
-
-
-Frost's
-report describes this development.
-
-
-
diff -r f4c82c165f58 -r 2aea76fe9c73 src/ZF/Constructible/README.html
--- a/src/ZF/Constructible/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-
-
-
-
-
-
ZF/Constructible/README
-
-
-
-
Constructible--Relative Consistency of the Axiom of Choice
-
-Gödel's proof of the relative consistency of the axiom of choice is
-mechanized using Isabelle/ZF. The proof builds upon a previous mechanization
-of the
-
reflection
-theorem. The heavy reliance on metatheory in the original proof makes the
-formalization unusually long, and not entirely satisfactory: two parts of the
-proof do not fit together. It seems impossible to solve these problems
-without formalizing the metatheory. However, the present development follows
-a standard textbook, Kunen's
Set Theory, and could support the
-formalization of further material from that book. It also serves as an
-example of what to expect when deep mathematics is formalized.
-
-A paper describing this development is
-
available.
-
-
-
-
-
-Last modified $Date$
-
-
-Larry Paulson,
-lcp@cl.cam.ac.uk
-
-
-
diff -r f4c82c165f58 -r 2aea76fe9c73 src/ZF/IMP/README.html
--- a/src/ZF/IMP/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-
-
-
-
-
-
-
ZF/IMP/README
-
-
-
-
-
IMP -- A while-language and two semantics
-
-The formalization of the denotational and operational semantics of a simple
-while-language together with an equivalence proof between the two semantics.
-The whole development essentially formalizes/transcribes chapters 2 and 5 of
-
-
-@book{Winskel,
- author = {Glynn Winskel},
- title = {The Formal Semantics of Programming Languages},
- publisher = {MIT Press},
- year = 1993}.
-
-
-There is a
-report
-by Lötzbeyer and Sandner.
-
-A much extended version of this development is found in
-HOL/IMP.
-
diff -r f4c82c165f58 -r 2aea76fe9c73 src/ZF/README.html
--- a/src/ZF/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-
-
-
-
-
-
-
ZF/README
-
-
-
-
-
ZF: Zermelo-Fraenkel Set Theory
-
-This directory contains the ML sources of the Isabelle system for
-ZF Set Theory, based on FOL.
-
-There are several subdirectories of examples:
-
-- AC
-
- subdirectory containing proofs from the book "Equivalents of the Axiom
-of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof
-Gr`abczewski.
-
-
- Coind
-
- subdirectory containing a large example of proof by co-induction. It
-is by Jacob Frost following a paper by Robin Milner and Mads Tofte.
-
-
- IMP
-
- subdirectory containing a semantics equivalence proof between
-operational and denotational definitions of a simple programming language.
-Thanks to Heiko Loetzbeyer & Robert Sandner.
-
-
- Resid
-
- subdirectory containing a proof of the Church-Rosser Theorem. It is
-by Ole Rasmussen, following the Coq proof by G�ard Huet.
-
-
- ex
-
- subdirectory containing various examples.
-
-
-Isabelle/ZF formalizes the greater part of elementary set theory,
-including relations, functions, injections, surjections, ordinals and
-cardinals. Results proved include Cantor's Theorem, the Recursion
-Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the
-Wellordering Theorem.
-
-Isabelle/ZF also provides theories of lists, trees, etc., for
-formalizing computational notions. It supports inductive definitions
-of infinite-branching trees for any cardinality of branching.
-
-Useful references for Isabelle/ZF:
-
-
-- Lawrence C. Paulson,
- Set theory for verification: I. From foundations to functions.
- J. Automated Reasoning 11 (1993), 353-389.
-
- - Lawrence C. Paulson,
- Set theory for verification: II. Induction and recursion.
- Report 312, Computer Lab (1993).
-
- - Lawrence C. Paulson,
- A fixedpoint approach to implementing (co)inductive definitions.
- In: A. Bundy (editor),
- CADE-12: 12th International Conference on Automated Deduction,
- (Springer LNAI 814, 1994), 148-161.
-
-
-Useful references on ZF set theory:
-
-
-- Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
-
-
- Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
-
-
- Keith J. Devlin,
- Fundamentals of Contemporary Set Theory (Springer, 1979)
-
- - Kenneth Kunen
- Set Theory: An Introduction to Independence Proofs
- (North-Holland, 1980)
-
-
-
diff -r f4c82c165f58 -r 2aea76fe9c73 src/ZF/ROOT
--- a/src/ZF/ROOT Tue Mar 12 19:55:17 2013 +0100
+++ b/src/ZF/ROOT Tue Mar 12 22:24:01 2013 +0100
@@ -1,11 +1,46 @@
+chapter ZF
+
session ZF (main) = Pure +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
- Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
+ Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen,
+ Philippe Noel and Lawrence Paulson.
+
+ Isabelle/ZF formalizes the greater part of elementary set theory, including
+ relations, functions, injections, surjections, ordinals and cardinals.
+ Results proved include Cantor's Theorem, the Recursion Theorem, the
+ Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem.
+
+ Isabelle/ZF also provides theories of lists, trees, etc., for formalizing
+ computational notions. It supports inductive definitions of
+ infinite-branching trees for any cardinality of branching.
+
+
+ Useful references for Isabelle/ZF:
+
+ Lawrence C. Paulson, Set theory for verification: I. From foundations to
+ functions. J. Automated Reasoning 11 (1993), 353-389.
- This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
+ Lawrence C. Paulson, Set theory for verification: II. Induction and
+ recursion. Report 312, Computer Lab (1993).
+
+ Lawrence C. Paulson, A fixedpoint approach to implementing (co)inductive
+ definitions. In: A. Bundy (editor), CADE-12: 12th International
+ Conference on Automated Deduction, (Springer LNAI 814, 1994), 148-161.
+
+
+ Useful references on ZF set theory:
+
+ Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
+
+ Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
+
+ Keith J. Devlin, Fundamentals of Contemporary Set Theory (Springer, 1979)
+
+ Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
+ (North-Holland, 1980)
*}
options [document_graph]
theories
@@ -19,6 +54,14 @@
Copyright 1995 University of Cambridge
Proofs of AC-equivalences, due to Krzysztof Grabczewski.
+
+ See also the book "Equivalents of the Axiom of Choice, II" by H. Rubin and
+ J.E. Rubin, 1985.
+
+ The report
+ http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
+ "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
+ development and ZF's theories of cardinals.
*}
options [document_graph]
theories
@@ -41,6 +84,12 @@
Coind -- A Coinduction Example.
+ It involves proving the consistency of the dynamic and static semantics for
+ a small functional language. A codatatype definition specifies values and
+ value environments in mutual recursion: non-well-founded values represent
+ recursive functions; value environments are variant functions from
+ variables into values.
+
Based upon the article
Robin Milner and Mads Tofte,
Co-induction in Relational Semantics,
@@ -49,12 +98,31 @@
Written up as
Jacob Frost, A Case Study of Co_induction in Isabelle
Report, Computer Lab, University of Cambridge (1995).
+ http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
*}
options [document = false]
theories ECR
session "ZF-Constructible" in Constructible = ZF +
- description {* Inner Models, Absoluteness and Consistency Proofs. *}
+ description {*
+ Relative Consistency of the Axiom of Choice:
+ Inner Models, Absoluteness and Consistency Proofs.
+
+ Gödel's proof of the relative consistency of the axiom of choice is
+ mechanized using Isabelle/ZF. The proof builds upon a previous
+ mechanization of the reflection theorem (see
+ http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf). The heavy
+ reliance on metatheory in the original proof makes the formalization
+ unusually long, and not entirely satisfactory: two parts of the proof do
+ not fit together. It seems impossible to solve these problems without
+ formalizing the metatheory. However, the present development follows a
+ standard textbook, Kunen's Set Theory, and could support the formalization
+ of further material from that book. It also serves as an example of what to
+ expect when deep mathematics is formalized.
+
+ A paper describing this development is
+ http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
+ *}
options [document_graph]
theories DPow_absolute AC_in_L Rank_Separation
files "document/root.tex" "document/root.bib"
@@ -120,6 +188,10 @@
Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development.
J. Functional Programming 4(3) 1994, 371-394.
+
+ See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
+ Porting Experiment.
+ http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
*}
options [document = false]
theories Confluence
@@ -148,6 +220,15 @@
Copyright 1993 University of Cambridge
Miscellaneous examples for Zermelo-Fraenkel Set Theory.
+
+ Includes a simple form of Ramsey's theorem. A report is available:
+ http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z
+
+ Several (co)inductive and (co)datatype definitions are presented. The
+ report http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz
+ describes the theoretical foundations of datatypes while
+ href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
+ describes the package that automates their declaration.
*}
options [document = false]
theories
diff -r f4c82c165f58 -r 2aea76fe9c73 src/ZF/Resid/README.html
--- a/src/ZF/Resid/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-
-
-
-
-
-
-
ZF/Resid/README
-
-
-
-
-
Resid -- A theory of residuals
-
-Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the
-article
-
-
-
-
-@Article{huet-residual,
- author = "{G\'erard} Huet",
- title = "Residual Theory in $\lambda$-Calculus: A Formal Development",
- journal = JFP,
- year = 1994,
- volume = 4,
- number = 3,
- pages = "371--394"}
-
-
-See Rasmussen's report
The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment.
-
-
-
diff -r f4c82c165f58 -r 2aea76fe9c73 src/ZF/ex/README.html
--- a/src/ZF/ex/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-
-
-
-
-
-
-
ZF/ex/README
-
-
-
-
-
ZF general examples
-
-Examples on this directory include a simple form of Ramsey's theorem. A
report is available.
-
-
-
-Several (co)inductive and (co)datatype definitions are presented. One report describes the theoretical foundations of datatypes while another describes the package that automates their declaration.
-
-
-