--- a/Admin/components/components.sha1 Wed Dec 23 16:25:52 2020 +0000
+++ b/Admin/components/components.sha1 Wed Dec 23 23:21:51 2020 +0100
@@ -183,6 +183,7 @@
b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz
1c753beb93e92e95e99e8ead23a68346bd1af44a jedit_build-20200610.tar.gz
533b1ee6459f59bcbe4f09e214ad2cb990fb6952 jedit_build-20200908.tar.gz
+f9966b5ed26740bb5b8bddbfe947fcefaea43d4d jedit_build-20201223.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
--- a/Admin/components/main Wed Dec 23 16:25:52 2020 +0000
+++ b/Admin/components/main Wed Dec 23 23:21:51 2020 +0100
@@ -6,7 +6,7 @@
e-2.5-1
isabelle_fonts-20190717
jdk-11.0.9+11
-jedit_build-20200908
+jedit_build-20201223
jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6
--- a/NEWS Wed Dec 23 16:25:52 2020 +0000
+++ b/NEWS Wed Dec 23 23:21:51 2020 +0100
@@ -103,8 +103,6 @@
*** HOL ***
-* Session "Hoare" now provides a total correctness logic as well.
-
* An updated version of the veriT solver is now included as Isabelle
component. It can be used in the "smt" proof method via "smt (verit)" or
via "declare [[smt_solver = verit]]" in the context; see also session
@@ -213,6 +211,11 @@
* Syntax for reflected term syntax is organized in bundle term_syntax,
discontinuing previous locale term_syntax. Minor INCOMPATIBILITY.
+* Session "HOL-Hoare": concrete syntax only for Hoare triples, not
+abstract language constructors.
+
+* Session "HOL-Hoare": now provides a total correctness logic as well.
+
*** FOL ***
--- a/lib/Tools/java_monitor Wed Dec 23 16:25:52 2020 +0000
+++ b/lib/Tools/java_monitor Wed Dec 23 23:21:51 2020 +0100
@@ -4,4 +4,4 @@
#
# DESCRIPTION: monitor another Java process
-isabelle java isabelle.Java_Monitor "$@"
+isabelle java "-Dapple.awt.application.name=Java Monitor" isabelle.Java_Monitor "$@"
--- a/lib/browser/build Wed Dec 23 16:25:52 2020 +0000
+++ b/lib/browser/build Wed Dec 23 23:21:51 2020 +0100
@@ -63,7 +63,7 @@
rm -rf classes && mkdir classes
- isabelle_jdk javac -d classes -source 1.6 "${SOURCES[@]}" || \
+ isabelle_jdk javac -d classes -source 7 "${SOURCES[@]}" || \
fail "Failed to compile sources"
isabelle_jdk jar cf "$(platform_path "$TARGET")" -C classes . ||
fail "Failed to produce $TARGET"
--- a/src/Doc/ROOT Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Doc/ROOT Wed Dec 23 23:21:51 2020 +0100
@@ -405,6 +405,8 @@
options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
"Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
+ theories [document = false]
+ Base
theories [threads = 1]
"ToyList/ToyList_Test"
theories [thy_output_indent = 5]
@@ -443,8 +445,6 @@
theories
"Protocol/NS_Public"
"Documents/Documents"
- theories [document = false]
- "Types/Setup"
theories [thy_output_margin = 64, thy_output_indent = 0]
"Types/Numbers"
"Types/Pairs"
--- a/src/Doc/Tutorial/Inductive/Advanced.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Doc/Tutorial/Inductive/Advanced.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,6 +1,4 @@
-(*<*)theory Advanced imports Even begin
-ML_file \<open>../../antiquote_setup.ML\<close>
-(*>*)
+(*<*)theory Advanced imports Even begin(*>*)
text \<open>
The premises of introduction rules may contain universal quantifiers and
--- a/src/Doc/Tutorial/Inductive/Even.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Doc/Tutorial/Inductive/Even.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,6 +1,4 @@
-(*<*)theory Even imports Main begin
-ML_file \<open>../../antiquote_setup.ML\<close>
-(*>*)
+(*<*)theory Even imports "../Setup" begin(*>*)
section\<open>The Set of Even Numbers\<close>
--- a/src/Doc/Tutorial/Protocol/Message.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Doc/Tutorial/Protocol/Message.thy Wed Dec 23 23:21:51 2020 +0100
@@ -7,8 +7,7 @@
section\<open>Theory of Agents and Messages for Security Protocols\<close>
-theory Message imports Main begin
-ML_file \<open>../../antiquote_setup.ML\<close>
+theory Message imports "../Setup" begin
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/Setup.thy Wed Dec 23 23:21:51 2020 +0100
@@ -0,0 +1,10 @@
+(*:maxLineLen=78:*)
+
+theory Setup
+imports Main
+begin
+
+ML_file \<open>../antiquote_setup.ML\<close>
+ML_file \<open>../more_antiquote.ML\<close>
+
+end
--- a/src/Doc/Tutorial/Types/Axioms.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Doc/Tutorial/Types/Axioms.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,4 +1,4 @@
-(*<*)theory Axioms imports Overloading Setup begin(*>*)
+(*<*)theory Axioms imports Overloading "../Setup" begin(*>*)
subsection \<open>Axioms\<close>
--- a/src/Doc/Tutorial/Types/Overloading.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Doc/Tutorial/Types/Overloading.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,4 +1,4 @@
-(*<*)theory Overloading imports Main Setup begin
+(*<*)theory Overloading imports "../Setup" begin
hide_class (open) plus (*>*)
--- a/src/Doc/Tutorial/Types/Setup.thy Wed Dec 23 16:25:52 2020 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-theory Setup
-imports Main
-begin
-
-ML_file \<open>../../antiquote_setup.ML\<close>
-ML_file \<open>../../more_antiquote.ML\<close>
-
-end
--- a/src/HOL/Hoare/Arith2.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/Arith2.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,12 +1,12 @@
(* Title: HOL/Hoare/Arith2.thy
Author: Norbert Galm
Copyright 1995 TUM
-
-More arithmetic. Much of this duplicates ex/Primes.
*)
+section \<open>More arithmetic\<close>
+
theory Arith2
-imports Main
+ imports Main
begin
definition cd :: "[nat, nat, nat] \<Rightarrow> bool"
@@ -21,7 +21,7 @@
| "fac (Suc n) = Suc n * fac n"
-subsubsection \<open>cd\<close>
+subsection \<open>cd\<close>
lemma cd_nnn: "0<n \<Longrightarrow> cd n n n"
apply (simp add: cd_def)
@@ -48,7 +48,7 @@
done
-subsubsection \<open>gcd\<close>
+subsection \<open>gcd\<close>
lemma gcd_nnn: "0<n \<Longrightarrow> n = gcd n n"
apply (unfold gcd_def)
@@ -79,7 +79,7 @@
done
-subsubsection \<open>pow\<close>
+subsection \<open>pow\<close>
lemma sq_pow_div2 [simp]:
"m mod 2 = 0 \<Longrightarrow> ((n::nat)*n)^(m div 2) = n^m"
--- a/src/HOL/Hoare/Examples.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/Examples.thy Wed Dec 23 23:21:51 2020 +0100
@@ -3,13 +3,15 @@
Copyright 1998 TUM
*)
-chapter \<open>Various examples\<close>
-
-theory Examples imports Hoare_Logic Arith2 begin
+section \<open>Various examples\<close>
-section \<open>ARITHMETIC\<close>
+theory Examples
+ imports Hoare_Logic Arith2
+begin
-subsection \<open>multiplication by successive addition\<close>
+subsection \<open>Arithmetic\<close>
+
+subsubsection \<open>Multiplication by successive addition\<close>
lemma multiply_by_add: "VARS m s a b
{a=A \<and> b=B}
@@ -54,7 +56,7 @@
done
-subsection \<open>Euclid's algorithm for GCD\<close>
+subsubsection \<open>Euclid's algorithm for GCD\<close>
lemma Euclid_GCD: "VARS a b
{0<A & 0<B}
@@ -87,7 +89,7 @@
done
-subsection \<open>Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\<close>
+subsubsection \<open>Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\<close>
text \<open>
From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
@@ -112,7 +114,7 @@
done
-subsection \<open>Power by iterated squaring and multiplication\<close>
+subsubsection \<open>Power by iterated squaring and multiplication\<close>
lemma power_by_mult: "VARS a b c
{a=A & b=B}
@@ -132,7 +134,7 @@
done
-subsection \<open>Factorial\<close>
+subsubsection \<open>Factorial\<close>
lemma factorial: "VARS a b
{a=A}
@@ -185,7 +187,7 @@
done
-subsection \<open>Square root\<close>
+subsubsection \<open>Square root\<close>
\<comment> \<open>the easy way:\<close>
@@ -221,7 +223,7 @@
done
-section \<open>LISTS\<close>
+subsection \<open>Lists\<close>
lemma imperative_reverse: "VARS y x
{x=X}
@@ -276,9 +278,9 @@
done
-section \<open>ARRAYS\<close>
+subsection \<open>Arrays\<close>
-subsection \<open>Search for a key\<close>
+subsubsection \<open>Search for a key\<close>
lemma zero_search: "VARS A i
{True}
--- a/src/HOL/Hoare/ExamplesAbort.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/ExamplesAbort.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,11 +1,13 @@
(* Title: HOL/Hoare/ExamplesAbort.thy
Author: Tobias Nipkow
Copyright 1998 TUM
-
-Some small examples for programs that may abort.
*)
-theory ExamplesAbort imports Hoare_Logic_Abort begin
+section \<open>Some small examples for programs that may abort\<close>
+
+theory ExamplesAbort
+ imports Hoare_Logic_Abort
+begin
lemma "VARS x y z::nat
{y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
--- a/src/HOL/Hoare/ExamplesTC.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/ExamplesTC.thy Wed Dec 23 23:21:51 2020 +0100
@@ -5,9 +5,7 @@
section \<open>Examples using Hoare Logic for Total Correctness\<close>
theory ExamplesTC
-
-imports Hoare_Logic
-
+ imports Hoare_Logic
begin
text \<open>
--- a/src/HOL/Hoare/Heap.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/Heap.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,12 +1,15 @@
(* Title: HOL/Hoare/Heap.thy
Author: Tobias Nipkow
Copyright 2002 TUM
-
-Pointers, heaps and heap abstractions.
-See the paper by Mehta and Nipkow.
*)
-theory Heap imports Main begin
+section \<open>Pointers, heaps and heap abstractions\<close>
+
+text \<open>See the paper by Mehta and Nipkow.\<close>
+
+theory Heap
+ imports Main
+begin
subsection "References"
@@ -22,9 +25,9 @@
"addr (Ref a) = a"
-section "The heap"
+subsection "The heap"
-subsection "Paths in the heap"
+subsubsection "Paths in the heap"
primrec Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
"Path h x [] y \<longleftrightarrow> x = y"
@@ -55,7 +58,7 @@
by simp
-subsection "Non-repeating paths"
+subsubsection "Non-repeating paths"
definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
@@ -78,9 +81,9 @@
by (case_tac Ps, auto)
-subsection "Lists on the heap"
+subsubsection "Lists on the heap"
-subsubsection "Relational abstraction"
+paragraph "Relational abstraction"
definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
where "List h x as = Path h x as Null"
@@ -131,7 +134,7 @@
done
-subsection "Functional abstraction"
+subsubsection "Functional abstraction"
definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
--- a/src/HOL/Hoare/HeapSyntax.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/HeapSyntax.thy Wed Dec 23 23:21:51 2020 +0100
@@ -3,7 +3,11 @@
Copyright 2002 TUM
*)
-theory HeapSyntax imports Hoare_Logic Heap begin
+section \<open>Heap syntax\<close>
+
+theory HeapSyntax
+ imports Hoare_Logic Heap
+begin
subsection "Field access and update"
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Dec 23 23:21:51 2020 +0100
@@ -3,7 +3,11 @@
Copyright 2002 TUM
*)
-theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin
+section \<open>Heap syntax (abort)\<close>
+
+theory HeapSyntaxAbort
+ imports Hoare_Logic_Abort Heap
+begin
subsection "Field access and update"
--- a/src/HOL/Hoare/Hoare.thy Wed Dec 23 16:25:52 2020 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(* Author: Tobias Nipkow
- Copyright 1998-2003 TUM
-*)
-
-theory Hoare
-imports Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation
-begin
-
-end
--- a/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 23:21:51 2020 +0100
@@ -2,32 +2,31 @@
Author: Leonor Prensa Nieto & Tobias Nipkow
Copyright 1998 TUM
Author: Walter Guttmann (extension to total-correctness proofs)
-
-Sugared semantic embedding of Hoare logic.
-Strictly speaking a shallow embedding (as implemented by Norbert Galm
-following Mike Gordon) would suffice. Maybe the datatype com comes in useful
-later.
*)
+section \<open>Hoare logic\<close>
+
theory Hoare_Logic
-imports Main
+ imports Hoare_Syntax Hoare_Tac
begin
+subsection \<open>Sugared semantic embedding of Hoare logic\<close>
+
+text \<open>
+ Strictly speaking a shallow embedding (as implemented by Norbert Galm
+ following Mike Gordon) would suffice. Maybe the datatype com comes in useful
+ later.
+\<close>
+
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
type_synonym 'a var = "'a \<Rightarrow> nat"
datatype 'a com =
Basic "'a \<Rightarrow> 'a"
-| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
-| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
-| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
-
-syntax (xsymbols)
- "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-
-translations
- "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD"
+| Seq "'a com" "'a com"
+| Cond "'a bexp" "'a com" "'a com"
+| While "'a bexp" "'a assn" "'a var" "'a com"
abbreviation annskip ("SKIP") where "SKIP == Basic id"
@@ -36,16 +35,22 @@
inductive Sem :: "'a com \<Rightarrow> 'a sem"
where
"Sem (Basic f) s (f s)"
-| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
-| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
-| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
+| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
| "s \<notin> b \<Longrightarrow> Sem (While b x y c) s s"
| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
Sem (While b x y c) s s'"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
+
+definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "ValidTC p c q \<equiv> \<forall>s. s \<in> p \<longrightarrow> (\<exists>t. Sem c s t \<and> t \<in> q)"
+
inductive_cases [elim!]:
- "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
- "Sem (IF b THEN c1 ELSE c2 FI) s s'"
+ "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
+ "Sem (Cond b c1 c2) s s'"
lemma Sem_deterministic:
assumes "Sem c s s1"
@@ -58,12 +63,6 @@
using assms by simp
qed
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
- where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
-
-definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
- where "ValidTC p c q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c s t \<and> t \<in> q)"
-
lemma tc_implies_pc:
"ValidTC p c q \<Longrightarrow> Valid p c q"
by (metis Sem_deterministic Valid_def ValidTC_def)
@@ -72,30 +71,6 @@
"ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
by (metis ValidTC_def)
-syntax
- "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
-
-syntax
- "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax ("" output)
- "_hoare" :: "['a assn,'a com,'a assn] => bool"
- ("{_} // _ // {_}" [0,55,0] 50)
-
-ML_file \<open>hoare_syntax.ML\<close>
-parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
-print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close>
-
-syntax
- "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
-syntax ("" output)
- "_hoare_tc" :: "['a assn,'a com,'a assn] => bool"
- ("[_] // _ // [_]" [0,55,0] 50)
-
-parse_translation \<open>[(\<^syntax_const>\<open>_hoare_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
-print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>))]\<close>
-
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp:Valid_def)
@@ -103,7 +78,7 @@
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
by (auto simp:Valid_def)
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
+lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
by (auto simp:Valid_def)
lemma CondRule:
@@ -112,11 +87,11 @@
by (auto simp:Valid_def)
lemma While_aux:
- assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'"
+ assumes "Sem (While b i v c) s s'"
shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
using assms
- by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto
+ by (induct "While b i v c" s s') auto
lemma WhileRule:
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
@@ -140,7 +115,7 @@
lemma SeqRuleTC:
assumes "ValidTC p c1 q"
and "ValidTC q c2 r"
- shows "ValidTC p (c1;c2) r"
+ shows "ValidTC p (Seq c1 c2) r"
by (meson assms Sem.intros(2) ValidTC_def)
lemma CondRuleTC:
@@ -193,28 +168,51 @@
using assms(1) ValidTC_def by force
qed
-lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
- by blast
+
+subsubsection \<open>Concrete syntax\<close>
+
+setup \<open>
+ Hoare_Syntax.setup
+ {Basic = \<^const_syntax>\<open>Basic\<close>,
+ Skip = \<^const_syntax>\<open>annskip\<close>,
+ Seq = \<^const_syntax>\<open>Seq\<close>,
+ Cond = \<^const_syntax>\<open>Cond\<close>,
+ While = \<^const_syntax>\<open>While\<close>,
+ Valid = \<^const_syntax>\<open>Valid\<close>,
+ ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
+\<close>
-lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close>
-ML_file \<open>hoare_tac.ML\<close>
+
+subsubsection \<open>Proof methods: VCG\<close>
+
+declare BasicRule [Hoare_Tac.BasicRule]
+ and SkipRule [Hoare_Tac.SkipRule]
+ and SeqRule [Hoare_Tac.SeqRule]
+ and CondRule [Hoare_Tac.CondRule]
+ and WhileRule [Hoare_Tac.WhileRule]
+
+declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
+ and SkipRuleTC [Hoare_Tac.SkipRuleTC]
+ and SeqRuleTC [Hoare_Tac.SeqRuleTC]
+ and CondRuleTC [Hoare_Tac.CondRuleTC]
+ and WhileRuleTC [Hoare_Tac.WhileRuleTC]
method_setup vcg = \<open>
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
"verification condition generator"
method_setup vcg_simp = \<open>
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
"verification condition generator plus simplification"
method_setup vcg_tc = \<open>
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\<close>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
"verification condition generator"
method_setup vcg_tc_simp = \<open>
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
"verification condition generator plus simplification"
end
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 23:21:51 2020 +0100
@@ -2,12 +2,12 @@
Author: Leonor Prensa Nieto & Tobias Nipkow
Copyright 2003 TUM
Author: Walter Guttmann (extension to total-correctness proofs)
-
-Like Hoare_Logic.thy, but with an Abort statement for modelling run time errors.
*)
+section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close>
+
theory Hoare_Logic_Abort
-imports Main
+ imports Hoare_Syntax Hoare_Tac
begin
type_synonym 'a bexp = "'a set"
@@ -17,15 +17,9 @@
datatype 'a com =
Basic "'a \<Rightarrow> 'a"
| Abort
-| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
-| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
-| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
-
-syntax (xsymbols)
- "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-
-translations
- "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD"
+| Seq "'a com" "'a com"
+| Cond "'a bexp" "'a com" "'a com"
+| While "'a bexp" "'a assn" "'a var" "'a com"
abbreviation annskip ("SKIP") where "SKIP == Basic id"
@@ -36,18 +30,18 @@
"Sem (Basic f) None None"
| "Sem (Basic f) (Some s) (Some (f s))"
| "Sem Abort s None"
-| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
-| "Sem (IF b THEN c1 ELSE c2 FI) None None"
-| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
-| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
+| "Sem (Cond b c1 c2) None None"
+| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'"
| "Sem (While b x y c) None None"
| "s \<notin> b \<Longrightarrow> Sem (While b x y c) (Some s) (Some s)"
| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
Sem (While b x y c) (Some s) s'"
inductive_cases [elim!]:
- "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
- "Sem (IF b THEN c1 ELSE c2 FI) s s'"
+ "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
+ "Sem (Cond b c1 c2) s s'"
lemma Sem_deterministic:
assumes "Sem c s s1"
@@ -74,30 +68,6 @@
"ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
by (meson ValidTC_def)
-syntax
- "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
-
-syntax
- "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax ("" output)
- "_hoare_abort" :: "['a assn,'a com,'a assn] => bool"
- ("{_} // _ // {_}" [0,55,0] 50)
-
-ML_file \<open>hoare_syntax.ML\<close>
-parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
-print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
-
-syntax
- "_hoare_abort_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
-syntax ("" output)
- "_hoare_abort_tc" :: "['a assn,'a com,'a assn] => bool"
- ("[_] // _ // [_]" [0,55,0] 50)
-
-parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
-print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort_tc\<close>))]\<close>
-
text \<open>The proof rules for partial correctness\<close>
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
@@ -106,7 +76,7 @@
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
by (auto simp:Valid_def)
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
+lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
by (auto simp:Valid_def)
lemma CondRule:
@@ -115,11 +85,11 @@
by (fastforce simp:Valid_def image_def)
lemma While_aux:
- assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'"
+ assumes "Sem (While b i v c) s s'"
shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
using assms
- by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto
+ by (induct "While b i v c" s s') auto
lemma WhileRule:
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
@@ -148,7 +118,7 @@
lemma SeqRuleTC:
assumes "ValidTC p c1 q"
and "ValidTC q c2 r"
- shows "ValidTC p (c1;c2) r"
+ shows "ValidTC p (Seq c1 c2) r"
by (meson assms Sem.intros(4) ValidTC_def)
lemma CondRuleTC:
@@ -202,38 +172,26 @@
qed
-subsection \<open>Derivation of the proof rules and, most importantly, the VCG tactic\<close>
-
-lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
- by blast
-
-ML_file \<open>hoare_tac.ML\<close>
-
-method_setup vcg = \<open>
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
- "verification condition generator"
+subsection \<open>Concrete syntax\<close>
-method_setup vcg_simp = \<open>
- Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
- "verification condition generator plus simplification"
-
-method_setup vcg_tc = \<open>
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\<close>
- "verification condition generator"
-
-method_setup vcg_tc_simp = \<open>
- Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
- "verification condition generator plus simplification"
+setup \<open>
+ Hoare_Syntax.setup
+ {Basic = \<^const_syntax>\<open>Basic\<close>,
+ Skip = \<^const_syntax>\<open>annskip\<close>,
+ Seq = \<^const_syntax>\<open>Seq\<close>,
+ Cond = \<^const_syntax>\<open>Cond\<close>,
+ While = \<^const_syntax>\<open>While\<close>,
+ Valid = \<^const_syntax>\<open>Valid\<close>,
+ ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
+\<close>
\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
syntax
"_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
"_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61)
translations
- "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
- "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
+ "P \<rightarrow> c" \<rightleftharpoons> "IF P THEN c ELSE CONST Abort FI"
+ "a[i] := v" \<rightharpoonup> "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
\<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close>
text \<open>
@@ -241,4 +199,38 @@
you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>.
\<close>
+
+subsection \<open>Proof methods: VCG\<close>
+
+declare BasicRule [Hoare_Tac.BasicRule]
+ and SkipRule [Hoare_Tac.SkipRule]
+ and AbortRule [Hoare_Tac.AbortRule]
+ and SeqRule [Hoare_Tac.SeqRule]
+ and CondRule [Hoare_Tac.CondRule]
+ and WhileRule [Hoare_Tac.WhileRule]
+
+declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
+ and SkipRuleTC [Hoare_Tac.SkipRuleTC]
+ and SeqRuleTC [Hoare_Tac.SeqRuleTC]
+ and CondRuleTC [Hoare_Tac.CondRuleTC]
+ and WhileRuleTC [Hoare_Tac.WhileRuleTC]
+
+method_setup vcg = \<open>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
+ "verification condition generator"
+
+method_setup vcg_simp = \<open>
+ Scan.succeed (fn ctxt =>
+ SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ "verification condition generator plus simplification"
+
+method_setup vcg_tc = \<open>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
+ "verification condition generator"
+
+method_setup vcg_tc_simp = \<open>
+ Scan.succeed (fn ctxt =>
+ SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ "verification condition generator plus simplification"
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Hoare_Syntax.thy Wed Dec 23 23:21:51 2020 +0100
@@ -0,0 +1,32 @@
+(* Title: HOL/Hoare/Hoare_Syntax.thy
+ Author: Leonor Prensa Nieto & Tobias Nipkow
+ Author: Walter Guttmann (extension to total-correctness proofs)
+*)
+
+section \<open>Concrete syntax for Hoare logic, with translations for variables\<close>
+
+theory Hoare_Syntax
+ imports Main
+begin
+
+syntax
+ "_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com" ("(2_ :=/ _)" [70, 65] 61)
+ "_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(_;/ _)" [61,60] 60)
+ "_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
+ "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
+
+syntax
+ "_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
+translations
+ "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
+
+syntax
+ "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
+ "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool" ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
+syntax (output)
+ "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("{_} // _ // {_}" [0,55,0] 50)
+ "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("[_] // _ // [_]" [0,55,0] 50)
+
+ML_file \<open>hoare_syntax.ML\<close>
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Hoare_Tac.thy Wed Dec 23 23:21:51 2020 +0100
@@ -0,0 +1,35 @@
+(* Title: HOL/Hoare/Hoare_Tac.thy
+ Author: Leonor Prensa Nieto & Tobias Nipkow
+ Author: Walter Guttmann (extension to total-correctness proofs)
+*)
+
+section \<open>Hoare logic VCG tactic\<close>
+
+theory Hoare_Tac
+ imports Main
+begin
+
+context
+begin
+
+qualified named_theorems BasicRule
+qualified named_theorems SkipRule
+qualified named_theorems AbortRule
+qualified named_theorems SeqRule
+qualified named_theorems CondRule
+qualified named_theorems WhileRule
+
+qualified named_theorems BasicRuleTC
+qualified named_theorems SkipRuleTC
+qualified named_theorems SeqRuleTC
+qualified named_theorems CondRuleTC
+qualified named_theorems WhileRuleTC
+
+lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
+ by blast
+
+ML_file \<open>hoare_tac.ML\<close>
+
+end
+
+end
--- a/src/HOL/Hoare/Pointer_Examples.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/Pointer_Examples.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,17 +1,20 @@
(* Title: HOL/Hoare/Pointer_Examples.thy
Author: Tobias Nipkow
Copyright 2002 TUM
-
-Examples of verifications of pointer programs.
*)
-theory Pointer_Examples imports HeapSyntax begin
+section \<open>Examples of verifications of pointer programs\<close>
+
+theory Pointer_Examples
+ imports HeapSyntax
+begin
axiomatization where unproven: "PROP A"
-section "Verifications"
-subsection "List reversal"
+subsection "Verifications"
+
+subsubsection "List reversal"
text "A short but unreadable proof:"
@@ -105,7 +108,7 @@
done
-subsection "Searching in a list"
+subsubsection "Searching in a list"
text\<open>What follows is a sequence of successively more intelligent proofs that
a simple loop finds an element in a linked list.
@@ -174,7 +177,8 @@
apply clarsimp
done
-subsection "Splicing two lists"
+
+subsubsection "Splicing two lists"
lemma "VARS tl p q pp qq
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps}
@@ -204,7 +208,7 @@
done
-subsection "Merging two lists"
+subsubsection "Merging two lists"
text"This is still a bit rough, especially the proof."
@@ -392,7 +396,7 @@
text"The proof is automatic, but requires a numbet of special lemmas."
-subsection "Cyclic list reversal"
+subsubsection "Cyclic list reversal"
text\<open>We consider two algorithms for the reversal of circular lists.
@@ -468,7 +472,7 @@
done
-subsection "Storage allocation"
+subsubsection "Storage allocation"
definition new :: "'a set \<Rightarrow> 'a"
where "new A = (SOME a. a \<notin> A)"
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,15 +1,17 @@
(* Title: HOL/Hoare/Pointer_ExamplesAbort.thy
Author: Tobias Nipkow
Copyright 2002 TUM
-
-Examples of verifications of pointer programs
*)
-theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin
+section \<open>Examples of verifications of pointer programs\<close>
-section "Verifications"
+theory Pointer_ExamplesAbort
+ imports HeapSyntaxAbort
+begin
-subsection "List reversal"
+subsection "Verifications"
+
+subsubsection "List reversal"
text "Interestingly, this proof is the same as for the unguarded program:"
--- a/src/HOL/Hoare/Pointers0.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/Pointers0.thy Wed Dec 23 23:21:51 2020 +0100
@@ -9,7 +9,11 @@
- in fact in some case they appear to get (a bit) more complicated.
*)
-theory Pointers0 imports Hoare_Logic begin
+section \<open>Alternative pointers\<close>
+
+theory Pointers0
+ imports Hoare_Logic
+begin
subsection "References"
@@ -40,9 +44,9 @@
by vcg_simp
-section "The heap"
+subsection "The heap"
-subsection "Paths in the heap"
+subsubsection "Paths in the heap"
primrec Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
where
@@ -68,9 +72,9 @@
lemma [simp]: "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
by(induct as, simp, simp add:eq_sym_conv)
-subsection "Lists on the heap"
+subsubsection "Lists on the heap"
-subsubsection "Relational abstraction"
+paragraph "Relational abstraction"
definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
where "List h x as = Path h x as Null"
@@ -118,7 +122,7 @@
apply(fastforce dest:List_hd_not_in_tl)
done
-subsection "Functional abstraction"
+subsubsection "Functional abstraction"
definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
@@ -173,9 +177,9 @@
done
-section "Verifications"
+subsection "Verifications"
-subsection "List reversal"
+subsubsection "List reversal"
text "A short but unreadable proof:"
@@ -256,7 +260,7 @@
done
-subsection "Searching in a list"
+subsubsection "Searching in a list"
text\<open>What follows is a sequence of successively more intelligent proofs that
a simple loop finds an element in a linked list.
@@ -312,7 +316,7 @@
done
-subsection "Merging two lists"
+subsubsection "Merging two lists"
text"This is still a bit rough, especially the proof."
@@ -398,7 +402,7 @@
(* TODO: merging with islist/list instead of List: an improvement?
needs (is)path, which is not so easy to prove either. *)
-subsection "Storage allocation"
+subsubsection "Storage allocation"
definition new :: "'a set \<Rightarrow> 'a::ref"
where "new A = (SOME a. a \<notin> A & a \<noteq> Null)"
@@ -427,5 +431,4 @@
apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
done
-
end
--- a/src/HOL/Hoare/SchorrWaite.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/SchorrWaite.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,14 +1,15 @@
(* Title: HOL/Hoare/SchorrWaite.thy
Author: Farhad Mehta
Copyright 2003 TUM
-
-Proof of the Schorr-Waite graph marking algorithm.
*)
+section \<open>Proof of the Schorr-Waite graph marking algorithm\<close>
-theory SchorrWaite imports HeapSyntax begin
+theory SchorrWaite
+ imports HeapSyntax
+begin
-section \<open>Machinery for the Schorr-Waite proof\<close>
+subsection \<open>Machinery for the Schorr-Waite proof\<close>
definition
\<comment> \<open>Relations induced by a mapping\<close>
@@ -194,8 +195,7 @@
done
-section\<open>The Schorr-Waite algorithm\<close>
-
+subsection \<open>The Schorr-Waite algorithm\<close>
theorem SchorrWaiteAlgorithm:
"VARS c m l r t p q root
@@ -573,4 +573,3 @@
qed
end
-
--- a/src/HOL/Hoare/SepLogHeap.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/SepLogHeap.thy Wed Dec 23 23:21:51 2020 +0100
@@ -1,13 +1,14 @@
(* Title: HOL/Hoare/SepLogHeap.thy
Author: Tobias Nipkow
Copyright 2002 TUM
-
-Heap abstractions (at the moment only Path and List)
-for Separation Logic.
*)
+section \<open>Heap abstractions for Separation Logic\<close>
+
+text \<open>(at the moment only Path and List)\<close>
+
theory SepLogHeap
-imports Main
+ imports Main
begin
type_synonym heap = "(nat \<Rightarrow> nat option)"
@@ -15,6 +16,7 @@
text\<open>\<open>Some\<close> means allocated, \<open>None\<close> means
free. Address \<open>0\<close> serves as the null reference.\<close>
+
subsection "Paths in the heap"
primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
--- a/src/HOL/Hoare/Separation.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/Separation.thy Wed Dec 23 23:21:51 2020 +0100
@@ -9,10 +9,13 @@
into parser and pretty printer, which is not very modular.
Alternative: some syntax like <P> which stands for P H. No more
compact, but avoids the funny H.
-
*)
-theory Separation imports Hoare_Logic_Abort SepLogHeap begin
+section \<open>Separation logic\<close>
+
+theory Separation
+ imports Hoare_Logic_Abort SepLogHeap
+begin
text\<open>The semantic definition of a few connectives:\<close>
--- a/src/HOL/Hoare/document/root.tex Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/document/root.tex Wed Dec 23 23:21:51 2020 +0100
@@ -1,4 +1,4 @@
-\documentclass[11pt,a4paper]{report}
+\documentclass[11pt,a4paper]{article}
\usepackage{graphicx}
\usepackage[english]{babel}
\usepackage{isabelle,isabellesym}
@@ -10,7 +10,12 @@
\begin{document}
\title{Hoare Logic}
-\author{Various}
+\author{
+ Norbert Galm \\
+ Walter Guttmann \\
+ Farhad Mehta \\
+ Tobias Nipkow \\
+ Leonor Prensa Nieto}
\maketitle
\begin{abstract}
@@ -27,7 +32,11 @@
\thispagestyle{empty}
\tableofcontents
-\newpage
+\begin{center}
+ \includegraphics[scale=0.5]{session_graph}
+\end{center}
+
+\clearpage
\input{session}
--- a/src/HOL/Hoare/hoare_syntax.ML Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/hoare_syntax.ML Wed Dec 23 23:21:51 2020 +0100
@@ -7,14 +7,41 @@
signature HOARE_SYNTAX =
sig
- val hoare_vars_tr: term list -> term
- val hoare_tc_vars_tr: term list -> term
- val spec_tr': string -> term list -> term
+ val hoare_vars_tr: Proof.context -> term list -> term
+ val hoare_tc_vars_tr: Proof.context -> term list -> term
+ val spec_tr': string -> Proof.context -> term list -> term
+ val setup:
+ {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
+ Valid: string, ValidTC: string} -> theory -> theory
end;
structure Hoare_Syntax: HOARE_SYNTAX =
struct
+(** theory data **)
+
+structure Data = Theory_Data
+(
+ type T =
+ {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
+ Valid: string, ValidTC: string} option;
+ val empty: T = NONE;
+ val extend = I;
+ fun merge (data1, data2) =
+ if is_some data1 andalso is_some data2 andalso data1 <> data2 then
+ error "Cannot merge syntax from different Hoare Logics"
+ else merge_options (data1, data2);
+);
+
+fun const_syntax ctxt which =
+ (case Data.get (Proof_Context.theory_of ctxt) of
+ SOME consts => which consts
+ | NONE => error "Undefined Hoare syntax consts");
+
+val syntax_const = Syntax.const oo const_syntax;
+
+
+
(** parse translation **)
local
@@ -54,35 +81,33 @@
(* com_tr *)
-fun com_tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs =
- Syntax.const \<^const_syntax>\<open>Basic\<close> $ mk_fexp x e xs
- | com_tr (Const (\<^const_syntax>\<open>Basic\<close>,_) $ f) _ = Syntax.const \<^const_syntax>\<open>Basic\<close> $ f
- | com_tr (Const (\<^const_syntax>\<open>Seq\<close>,_) $ c1 $ c2) xs =
- Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (\<^const_syntax>\<open>Cond\<close>,_) $ b $ c1 $ c2) xs =
- Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (\<^const_syntax>\<open>While\<close>,_) $ b $ I $ V $ c) xs =
- Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ com_tr c xs
- | com_tr t _ = t;
+fun com_tr ctxt =
+ let
+ fun tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs =
+ syntax_const ctxt #Basic $ mk_fexp x e xs
+ | tr (Const (\<^syntax_const>\<open>_Seq\<close>,_) $ c1 $ c2) xs =
+ syntax_const ctxt #Seq $ tr c1 xs $ tr c2 xs
+ | tr (Const (\<^syntax_const>\<open>_Cond\<close>,_) $ b $ c1 $ c2) xs =
+ syntax_const ctxt #Cond $ bexp_tr b xs $ tr c1 xs $ tr c2 xs
+ | tr (Const (\<^syntax_const>\<open>_While\<close>,_) $ b $ I $ V $ c) xs =
+ syntax_const ctxt #While $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ tr c xs
+ | tr t _ = t;
+ in tr end;
fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars
| vars_tr t = [t];
in
-fun hoare_vars_tr [vars, pre, prg, post] =
+fun hoare_vars_tr ctxt [vars, pre, prg, post] =
let val xs = vars_tr vars
- in Syntax.const \<^const_syntax>\<open>Valid\<close> $
- assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
- end
- | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
+ in syntax_const ctxt #Valid $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end
+ | hoare_vars_tr _ ts = raise TERM ("hoare_vars_tr", ts);
-fun hoare_tc_vars_tr [vars, pre, prg, post] =
+fun hoare_tc_vars_tr ctxt [vars, pre, prg, post] =
let val xs = vars_tr vars
- in Syntax.const \<^const_syntax>\<open>ValidTC\<close> $
- assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
- end
- | hoare_tc_vars_tr ts = raise TERM ("hoare_tc_vars_tr", ts);
+ in syntax_const ctxt #ValidTC $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end
+ | hoare_tc_vars_tr _ ts = raise TERM ("hoare_tc_vars_tr", ts);
end;
@@ -139,32 +164,55 @@
(* com_tr' *)
-fun mk_assign f =
+fun mk_assign ctxt f =
let
val (vs, ts) = mk_vts f;
- val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
+ val (ch, (a, b)) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
in
if ch
- then Syntax.const \<^syntax_const>\<open>_assign\<close> $ fst which $ snd which
- else Syntax.const \<^const_syntax>\<open>annskip\<close>
+ then Syntax.const \<^syntax_const>\<open>_assign\<close> $ a $ b
+ else syntax_const ctxt #Skip
end;
-fun com_tr' (Const (\<^const_syntax>\<open>Basic\<close>, _) $ f) =
- if is_f f then mk_assign f
- else Syntax.const \<^const_syntax>\<open>Basic\<close> $ f
- | com_tr' (Const (\<^const_syntax>\<open>Seq\<close>,_) $ c1 $ c2) =
- Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (\<^const_syntax>\<open>Cond\<close>, _) $ b $ c1 $ c2) =
- Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (\<^const_syntax>\<open>While\<close>, _) $ b $ I $ V $ c) =
- Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr' b $ assn_tr' I $ var_tr' V $ com_tr' c
- | com_tr' t = t;
+fun com_tr' ctxt t =
+ let
+ val (head, args) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb t);
+ fun arg k = nth args (k - 1);
+ val n = length args;
+ in
+ (case head of
+ NONE => t
+ | SOME c =>
+ if c = const_syntax ctxt #Basic andalso n = 1 andalso is_f (arg 1) then
+ mk_assign ctxt (arg 1)
+ else if c = const_syntax ctxt #Seq andalso n = 2 then
+ Syntax.const \<^syntax_const>\<open>_Seq\<close> $ com_tr' ctxt (arg 1) $ com_tr' ctxt (arg 2)
+ else if c = const_syntax ctxt #Cond andalso n = 3 then
+ Syntax.const \<^syntax_const>\<open>_Cond\<close> $
+ bexp_tr' (arg 1) $ com_tr' ctxt (arg 2) $ com_tr' ctxt (arg 3)
+ else if c = const_syntax ctxt #While andalso n = 4 then
+ Syntax.const \<^syntax_const>\<open>_While\<close> $
+ bexp_tr' (arg 1) $ assn_tr' (arg 2) $ var_tr' (arg 3) $ com_tr' ctxt (arg 4)
+ else t)
+ end;
in
-fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q;
+fun spec_tr' syn ctxt [p, c, q] =
+ Syntax.const syn $ assn_tr' p $ com_tr' ctxt c $ assn_tr' q;
end;
+
+(** setup **)
+
+fun setup consts =
+ Data.put (SOME consts) #>
+ Sign.parse_translation
+ [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
+ (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)] #>
+ Sign.print_translation
+ [(#Valid consts, spec_tr' \<^syntax_const>\<open>_hoare\<close>),
+ (#ValidTC consts, spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>)];
+
end;
-
--- a/src/HOL/Hoare/hoare_tac.ML Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Hoare/hoare_tac.ML Wed Dec 23 23:21:51 2020 +0100
@@ -5,7 +5,7 @@
Derivation of the proof rules and, most importantly, the VCG tactic.
*)
-signature HOARE =
+signature HOARE_TAC =
sig
val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool ->
int -> tactic
@@ -13,7 +13,7 @@
val hoare_tc_tac: Proof.context -> (int -> tactic) -> int -> tactic
end;
-structure Hoare: HOARE =
+structure Hoare_Tac: HOARE_TAC =
struct
(*** The tactics ***)
@@ -77,7 +77,7 @@
in mk_vars pre end;
fun mk_CollectC tm =
- let val T as Type ("fun",[t,_]) = fastype_of tm;
+ let val Type ("fun",[t,_]) = fastype_of tm;
in HOLogic.Collect_const t $ tm end;
fun inclt ty = Const (\<^const_name>\<open>Orderings.less_eq\<close>, [ty,ty] ---> HOLogic.boolT);
@@ -164,25 +164,26 @@
fun hoare_rule_tac ctxt (vars, Mlem) tac =
let
+ val get_thms = Proof_Context.get_thms ctxt;
val var_names = map (fst o dest_Free) vars;
fun wlp_tac i =
- resolve_tac ctxt @{thms SeqRule} i THEN rule_tac false (i + 1)
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>SeqRule\<close>) i THEN rule_tac false (i + 1)
and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
((wlp_tac i THEN rule_tac pre_cond i)
ORELSE
(FIRST [
- resolve_tac ctxt @{thms SkipRule} i,
- resolve_tac ctxt @{thms AbortRule} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>SkipRule\<close>) i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>AbortRule\<close>) i,
EVERY [
- resolve_tac ctxt @{thms BasicRule} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRule\<close>) i,
resolve_tac ctxt [Mlem] i,
split_simp_tac ctxt i],
EVERY [
- resolve_tac ctxt @{thms CondRule} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>CondRule\<close>) i,
rule_tac false (i + 2),
rule_tac false (i + 1)],
EVERY [
- resolve_tac ctxt @{thms WhileRule} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>WhileRule\<close>) i,
basic_simp_tac ctxt var_names tac (i + 2),
rule_tac true (i + 1)]]
THEN (
@@ -202,24 +203,25 @@
fun hoare_tc_rule_tac ctxt (vars, Mlem) tac =
let
+ val get_thms = Proof_Context.get_thms ctxt;
val var_names = map (fst o dest_Free) vars;
fun wlp_tac i =
- resolve_tac ctxt @{thms SeqRuleTC} i THEN rule_tac false (i + 1)
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>SeqRuleTC\<close>) i THEN rule_tac false (i + 1)
and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
((wlp_tac i THEN rule_tac pre_cond i)
ORELSE
(FIRST [
- resolve_tac ctxt @{thms SkipRuleTC} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>SkipRuleTC\<close>) i,
EVERY [
- resolve_tac ctxt @{thms BasicRuleTC} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRuleTC\<close>) i,
resolve_tac ctxt [Mlem] i,
split_simp_tac ctxt i],
EVERY [
- resolve_tac ctxt @{thms CondRuleTC} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>CondRuleTC\<close>) i,
rule_tac false (i + 2),
rule_tac false (i + 1)],
EVERY [
- resolve_tac ctxt @{thms WhileRuleTC} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>WhileRuleTC\<close>) i,
basic_simp_tac ctxt var_names tac (i + 2),
rule_tac true (i + 1)]]
THEN (
@@ -232,4 +234,3 @@
SELECT_GOAL (hoare_tc_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
end;
-
--- a/src/HOL/Isar_Examples/Hoare.thy Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Isar_Examples/Hoare.thy Wed Dec 23 23:21:51 2020 +0100
@@ -7,7 +7,7 @@
section \<open>Hoare Logic\<close>
theory Hoare
- imports Main
+ imports "HOL-Hoare.Hoare_Tac"
begin
subsection \<open>Abstract syntax and semantics\<close>
@@ -397,22 +397,16 @@
apply blast
done
-lemma Compl_Collect: "- Collect b = {x. \<not> b x}"
- by blast
-
-lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close>
-lemmas SeqRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-lemmas SkipRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-lemmas BasicRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-lemmas CondRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-lemmas WhileRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-
-ML_file \<open>~~/src/HOL/Hoare/hoare_tac.ML\<close>
+declare BasicRule [Hoare_Tac.BasicRule]
+ and SkipRule [Hoare_Tac.SkipRule]
+ and SeqRule [Hoare_Tac.SeqRule]
+ and CondRule [Hoare_Tac.CondRule]
+ and WhileRule [Hoare_Tac.WhileRule]
method_setup hoare =
\<open>Scan.succeed (fn ctxt =>
(SIMPLE_METHOD'
- (Hoare.hoare_tac ctxt
+ (Hoare_Tac.hoare_tac ctxt
(simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] )))))\<close>
"verification condition generator for Hoare logic"
--- a/src/HOL/ROOT Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/ROOT Wed Dec 23 23:21:51 2020 +0100
@@ -311,7 +311,15 @@
Verification of imperative programs (verification conditions are generated
automatically from pre/post conditions and loop invariants).
"
- theories Hoare
+ theories
+ Examples
+ ExamplesAbort
+ ExamplesTC
+ Pointers0
+ Pointer_Examples
+ Pointer_ExamplesAbort
+ SchorrWaite
+ Separation
document_files "root.bib" "root.tex"
session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
@@ -369,6 +377,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009
"
+ options [kodkod_scala]
sessions "HOL-Library"
theories [quick_and_dirty] Nitpick_Examples
@@ -709,6 +718,8 @@
Miscellaneous Isabelle/Isar examples.
"
options [quick_and_dirty]
+ sessions
+ "HOL-Hoare"
theories
Structured_Statements
Basic_Logic
--- a/src/HOL/Tools/etc/options Wed Dec 23 16:25:52 2020 +0000
+++ b/src/HOL/Tools/etc/options Wed Dec 23 23:21:51 2020 +0100
@@ -8,7 +8,7 @@
public option auto_time_limit : real = 2.0
-- "time limit for automatically tried tools (seconds > 0)"
-public option auto_nitpick : bool = true
+public option auto_nitpick : bool = false
-- "run Nitpick automatically"
public option auto_sledgehammer : bool = false
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Dec 23 23:21:51 2020 +0100
@@ -372,7 +372,7 @@
Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true,
proxy_host = "lxbroy10", proxy_user = "i21isatest",
java_heap = "8g",
- options = "-m32 -M1x8 -t AFP" +
+ options = "-m32 -M1x6 -t AFP" +
" -e ISABELLE_GHC=ghc" +
" -e ISABELLE_MLTON=mlton" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/desktop_app.scala Wed Dec 23 23:21:51 2020 +0100
@@ -0,0 +1,22 @@
+/* Title: Pure/GUI/desktop_app.scala
+ Author: Makarius
+
+Support for desktop applications, notably on macOS.
+*/
+
+package isabelle
+
+import java.awt.Desktop
+
+
+object Desktop_App
+{
+ def desktop_action(action: Desktop.Action, f: Desktop => Unit): Unit =
+ if (Desktop.isDesktopSupported) {
+ val desktop = Desktop.getDesktop
+ if (desktop.isSupported(action)) f(desktop)
+ }
+
+ def about_handler(handler: => Unit): Unit =
+ desktop_action(Desktop.Action.APP_ABOUT, _.setAboutHandler(_ => handler))
+}
--- a/src/Pure/Thy/presentation.scala Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Pure/Thy/presentation.scala Wed Dec 23 23:21:51 2020 +0100
@@ -374,6 +374,7 @@
session: String,
deps: Sessions.Deps,
db_context: Sessions.Database_Context,
+ progress: Progress = new Progress,
html_context: HTML_Context,
presentation: Context)
{
@@ -425,49 +426,21 @@
HTML.link(prefix + html_name(name1), body)
}
- val files: List[XML.Body] =
+ val theories: List[XML.Body] =
{
var seen_files = List.empty[(Path, String, Document.Node.Name)]
- (for {
- thy_name <- base.session_theories.iterator
- thy_command <-
- Build_Job.read_theory(db_context, resources, session, thy_name.theory).iterator
- snapshot = Document.State.init.snippet(thy_command)
- (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements).iterator
- if xml.nonEmpty
- } yield {
- val file_title = src_path.implode_short
- val file_name = (files_path + src_path.squash.html).implode
-
- seen_files.find(p => p._1 == src_path || p._2 == file_name) match {
- case None => seen_files ::= (src_path, file_name, thy_name)
- case Some((_, _, thy_name1)) =>
- error("Incoherent use of file name " + src_path + " as " + quote(file_name) +
- " in theory " + thy_name1 + " vs. " + thy_name)
- }
- val file_path = session_dir + Path.explode(file_name)
- html_context.init_fonts(file_path.dir)
-
- val title = "File " + Symbol.cartouche_decoded(file_title)
- HTML.write_document(file_path.dir, file_path.file_name,
- List(HTML.title(title)),
- List(html_context.head(title), html_context.source(html_body(xml))))
+ for (thy_name <- base.session_theories)
+ yield {
+ progress.expose_interrupt()
- List(HTML.link(file_name, HTML.text(file_title)))
- }).toList
- }
-
- val theories =
- for (name <- base.session_theories)
- yield {
- val syntax = base.theory_syntax(name)
+ val syntax = base.theory_syntax(thy_name)
val keywords = syntax.keywords
- val spans = syntax.parse_spans(Symbol.decode(File.read(name.path)))
+ val spans = syntax.parse_spans(Symbol.decode(File.read(thy_name.path)))
val thy_body =
{
- val imports_offset = base.known_theories(name.theory).header.imports_offset
+ val imports_offset = base.known_theories(thy_name.theory).header.imports_offset
var token_offset = 1
spans.flatMap(span =>
{
@@ -489,20 +462,52 @@
})
}
- val title = "Theory " + name.theory_base_name
- HTML.write_document(session_dir, html_name(name),
- List(HTML.title(title)),
- List(html_context.head(title), html_context.source(thy_body)))
+ val files =
+ (for {
+ thy_command <-
+ Build_Job.read_theory(db_context, resources, session, thy_name.theory).iterator
+ snapshot = Document.State.init.snippet(thy_command)
+ (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements).iterator
+ if xml.nonEmpty
+ } yield {
+ progress.expose_interrupt()
+
+ val file_name = (files_path + src_path.squash.html).implode
+
+ seen_files.find(p => p._1 == src_path || p._2 == file_name) match {
+ case None => seen_files ::= (src_path, file_name, thy_name)
+ case Some((_, _, thy_name1)) =>
+ error("Incoherent use of file name " + src_path + " as " + quote(file_name) +
+ " in theory " + thy_name1 + " vs. " + thy_name)
+ }
- List(HTML.link(html_name(name), HTML.text(name.theory_base_name)))
+ val file_path = session_dir + Path.explode(file_name)
+ html_context.init_fonts(file_path.dir)
+
+ val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
+ HTML.write_document(file_path.dir, file_path.file_name,
+ List(HTML.title(file_title)),
+ List(html_context.head(file_title), html_context.source(html_body(xml))))
+
+ List(HTML.link(file_name, HTML.text(file_title)))
+ }).toList
+
+ val thy_title = "Theory " + thy_name.theory_base_name
+ HTML.write_document(session_dir, html_name(thy_name),
+ List(HTML.title(thy_title)),
+ List(html_context.head(thy_title), html_context.source(thy_body)))
+
+ List(HTML.link(html_name(thy_name),
+ HTML.text(thy_name.theory_base_name) :::
+ (if (files.isEmpty) Nil else List(HTML.itemize(files)))))
}
+ }
val title = "Session " + session
HTML.write_document(session_dir, "index.html",
List(HTML.title(title + " (" + Distribution.version + ")")),
html_context.head(title, List(HTML.par(links))) ::
- html_context.contents("Theories", theories) :::
- html_context.contents("Files", files))
+ html_context.contents("Theories", theories))
}
--- a/src/Pure/Tools/build.scala Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Pure/Tools/build.scala Wed Dec 23 23:21:51 2020 +0100
@@ -202,6 +202,7 @@
options +
"completion_limit=0" +
"editor_tracing_messages=0" +
+ "kodkod_scala=false" +
("pide_reports=" + options.bool("build_pide_reports"))
val store = Sessions.store(build_options)
@@ -510,7 +511,7 @@
progress.expose_interrupt()
progress.echo("Presenting " + session_name + " ...")
Presentation.session_html(
- resources, session_name, deps, db_context, html_context, presentation)
+ resources, session_name, deps, db_context, progress, html_context, presentation)
})
val browser_chapters =
--- a/src/Pure/Tools/java_monitor.scala Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Pure/Tools/java_monitor.scala Wed Dec 23 23:21:51 2020 +0100
@@ -9,7 +9,8 @@
import java.awt.Component
import javax.swing.UIManager
-import sun.tools.jconsole.{JConsole, LocalVirtualMachine, VMPanel, ProxyClient}
+import sun.tools.jconsole.{JConsole, LocalVirtualMachine, VMPanel, ProxyClient,
+ Messages, Resources => JConsoleResources}
object Java_Monitor
@@ -40,6 +41,13 @@
System.setProperty("swing.defaultlaf", laf)
}
+ Desktop_App.about_handler {
+ GUI.dialog(null, "Java Monitor",
+ JConsoleResources.format(
+ Messages.JCONSOLE_VERSION, System.getProperty("java.runtime.version"))
+ )
+ }
+
val jconsole = new JConsole(false)
val screen = GUI.mouse_location()
--- a/src/Pure/build-jars Wed Dec 23 16:25:52 2020 +0000
+++ b/src/Pure/build-jars Wed Dec 23 23:21:51 2020 +0100
@@ -45,6 +45,7 @@
src/Pure/Concurrent/par_list.scala
src/Pure/Concurrent/synchronized.scala
src/Pure/GUI/color_value.scala
+ src/Pure/GUI/desktop_app.scala
src/Pure/GUI/gui.scala
src/Pure/GUI/gui_thread.scala
src/Pure/GUI/popup.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/panel_font Wed Dec 23 23:21:51 2020 +0100
@@ -0,0 +1,28 @@
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/PanelWindowContainer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2020-09-03 05:31:02.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2020-12-23 13:16:31.059779643 +0100
+@@ -52,6 +52,7 @@
+ import javax.swing.JComponent;
+ import javax.swing.JPanel;
+ import javax.swing.JPopupMenu;
++import javax.swing.JMenuItem;
+ import javax.swing.JToggleButton;
+ import javax.swing.UIManager;
+ import javax.swing.border.Border;
+@@ -163,6 +164,7 @@
+ {
+ button = new JToggleButton();
+ button.setMargin(new Insets(1,1,1,1));
++ button.setFont(new JMenuItem().getFont());
+ }
+ GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
+ button.setRequestFocusEnabled(false);
+@@ -690,8 +692,6 @@
+ renderHints = new RenderingHints(
+ RenderingHints.KEY_ANTIALIASING,
+ RenderingHints.VALUE_ANTIALIAS_ON);
+- renderHints.put(RenderingHints.KEY_FRACTIONALMETRICS,
+- RenderingHints.VALUE_FRACTIONALMETRICS_ON);
+ renderHints.put(RenderingHints.KEY_RENDERING,
+ RenderingHints.VALUE_RENDER_QUALITY);
+ } //}}}