# HG changeset patch # User wenzelm # Date 1608762111 -3600 # Node ID eac16c76273ee27fc764a8d707c1a3198c1fc85e # Parent 4fc3dc37f4069963db1bd7fd142190537f14d6f9# Parent 055f44891643d94c10d6d1f691f7762df7ab0ffb merged diff -r 4fc3dc37f406 -r eac16c76273e Admin/components/components.sha1 --- 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 diff -r 4fc3dc37f406 -r eac16c76273e Admin/components/main --- 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 diff -r 4fc3dc37f406 -r eac16c76273e NEWS --- 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 *** diff -r 4fc3dc37f406 -r eac16c76273e lib/Tools/java_monitor --- 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 "$@" diff -r 4fc3dc37f406 -r eac16c76273e lib/browser/build --- 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" diff -r 4fc3dc37f406 -r eac16c76273e src/Doc/ROOT --- 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" diff -r 4fc3dc37f406 -r eac16c76273e src/Doc/Tutorial/Inductive/Advanced.thy --- 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 \../../antiquote_setup.ML\ -(*>*) +(*<*)theory Advanced imports Even begin(*>*) text \ The premises of introduction rules may contain universal quantifiers and diff -r 4fc3dc37f406 -r eac16c76273e src/Doc/Tutorial/Inductive/Even.thy --- 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 \../../antiquote_setup.ML\ -(*>*) +(*<*)theory Even imports "../Setup" begin(*>*) section\The Set of Even Numbers\ diff -r 4fc3dc37f406 -r eac16c76273e src/Doc/Tutorial/Protocol/Message.thy --- 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\Theory of Agents and Messages for Security Protocols\ -theory Message imports Main begin -ML_file \../../antiquote_setup.ML\ +theory Message imports "../Setup" begin (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) lemma [simp] : "A \ (B \ A) = B \ A" diff -r 4fc3dc37f406 -r eac16c76273e src/Doc/Tutorial/Setup.thy --- /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 \../antiquote_setup.ML\ +ML_file \../more_antiquote.ML\ + +end diff -r 4fc3dc37f406 -r eac16c76273e src/Doc/Tutorial/Types/Axioms.thy --- 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 \Axioms\ diff -r 4fc3dc37f406 -r eac16c76273e src/Doc/Tutorial/Types/Overloading.thy --- 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 (*>*) diff -r 4fc3dc37f406 -r eac16c76273e src/Doc/Tutorial/Types/Setup.thy --- 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 \../../antiquote_setup.ML\ -ML_file \../../more_antiquote.ML\ - -end diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Arith2.thy --- 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 \More arithmetic\ + theory Arith2 -imports Main + imports Main begin definition cd :: "[nat, nat, nat] \ bool" @@ -21,7 +21,7 @@ | "fac (Suc n) = Suc n * fac n" -subsubsection \cd\ +subsection \cd\ lemma cd_nnn: "0 cd n n n" apply (simp add: cd_def) @@ -48,7 +48,7 @@ done -subsubsection \gcd\ +subsection \gcd\ lemma gcd_nnn: "0 n = gcd n n" apply (unfold gcd_def) @@ -79,7 +79,7 @@ done -subsubsection \pow\ +subsection \pow\ lemma sq_pow_div2 [simp]: "m mod 2 = 0 \ ((n::nat)*n)^(m div 2) = n^m" diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Examples.thy --- 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 \Various examples\ - -theory Examples imports Hoare_Logic Arith2 begin +section \Various examples\ -section \ARITHMETIC\ +theory Examples + imports Hoare_Logic Arith2 +begin -subsection \multiplication by successive addition\ +subsection \Arithmetic\ + +subsubsection \Multiplication by successive addition\ lemma multiply_by_add: "VARS m s a b {a=A \ b=B} @@ -54,7 +56,7 @@ done -subsection \Euclid's algorithm for GCD\ +subsubsection \Euclid's algorithm for GCD\ lemma Euclid_GCD: "VARS a b {0Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\ +subsubsection \Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\ text \ From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474), @@ -112,7 +114,7 @@ done -subsection \Power by iterated squaring and multiplication\ +subsubsection \Power by iterated squaring and multiplication\ lemma power_by_mult: "VARS a b c {a=A & b=B} @@ -132,7 +134,7 @@ done -subsection \Factorial\ +subsubsection \Factorial\ lemma factorial: "VARS a b {a=A} @@ -185,7 +187,7 @@ done -subsection \Square root\ +subsubsection \Square root\ \ \the easy way:\ @@ -221,7 +223,7 @@ done -section \LISTS\ +subsection \Lists\ lemma imperative_reverse: "VARS y x {x=X} @@ -276,9 +278,9 @@ done -section \ARRAYS\ +subsection \Arrays\ -subsection \Search for a key\ +subsubsection \Search for a key\ lemma zero_search: "VARS A i {True} diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/ExamplesAbort.thy --- 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 \Some small examples for programs that may abort\ + +theory ExamplesAbort + imports Hoare_Logic_Abort +begin lemma "VARS x y z::nat {y = z & z \ 0} z \ 0 \ x := y div z {x = 1}" diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/ExamplesTC.thy --- 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 \Examples using Hoare Logic for Total Correctness\ theory ExamplesTC - -imports Hoare_Logic - + imports Hoare_Logic begin text \ diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Heap.thy --- 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 \Pointers, heaps and heap abstractions\ + +text \See the paper by Mehta and Nipkow.\ + +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 \ 'a ref) \ 'a ref \ 'a list \ 'a ref \ bool" where "Path h x [] y \ x = y" @@ -55,7 +58,7 @@ by simp -subsection "Non-repeating paths" +subsubsection "Non-repeating paths" definition distPath :: "('a \ 'a ref) \ 'a ref \ 'a list \ 'a ref \ bool" where "distPath h x as y \ Path h x as y \ 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 \ 'a ref) \ 'a ref \ 'a list \ 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 \ 'a ref) \ 'a ref \ bool" where "islist h p \ (\as. List h p as)" diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/HeapSyntax.thy --- 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 \Heap syntax\ + +theory HeapSyntax + imports Hoare_Logic Heap +begin subsection "Field access and update" diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/HeapSyntaxAbort.thy --- 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 \Heap syntax (abort)\ + +theory HeapSyntaxAbort + imports Hoare_Logic_Abort Heap +begin subsection "Field access and update" diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Hoare.thy --- 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 diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Hoare_Logic.thy --- 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 \Hoare logic\ + theory Hoare_Logic -imports Main + imports Hoare_Syntax Hoare_Tac begin +subsection \Sugared semantic embedding of Hoare logic\ + +text \ + Strictly speaking a shallow embedding (as implemented by Norbert Galm + following Mike Gordon) would suffice. Maybe the datatype com comes in useful + later. +\ + type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" type_synonym 'a var = "'a \ nat" datatype 'a com = Basic "'a \ '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 \ 'a assn \ 'a com \ '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 \ 'a sem" where "Sem (Basic f) s (f s)" -| "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (c1;c2) s s'" -| "s \ b \ Sem c1 s s' \ Sem (IF b THEN c1 ELSE c2 FI) s s'" -| "s \ b \ Sem c2 s s' \ Sem (IF b THEN c1 ELSE c2 FI) s s'" +| "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (Seq c1 c2) s s'" +| "s \ b \ Sem c1 s s' \ Sem (Cond b c1 c2) s s'" +| "s \ b \ Sem c2 s s' \ Sem (Cond b c1 c2) s s'" | "s \ b \ Sem (While b x y c) s s" | "s \ b \ Sem c s s'' \ Sem (While b x y c) s'' s' \ Sem (While b x y c) s s'" +definition Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" + where "Valid p c q \ \s s'. Sem c s s' \ s \ p \ s' \ q" + +definition ValidTC :: "'a bexp \ 'a com \ 'a bexp \ bool" + where "ValidTC p c q \ \s. s \ p \ (\t. Sem c s t \ t \ 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 \ 'a com \ 'a bexp \ bool" - where "Valid p c q \ \s s'. Sem c s s' \ s \ p \ s' \ q" - -definition ValidTC :: "'a bexp \ 'a com \ 'a bexp \ bool" - where "ValidTC p c q \ \s . s \ p \ (\t . Sem c s t \ t \ q)" - lemma tc_implies_pc: "ValidTC p c q \ Valid p c q" by (metis Sem_deterministic Valid_def ValidTC_def) @@ -72,30 +71,6 @@ "ValidTC p c q \ \f . \s . s \ p \ f s \ 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 \hoare_syntax.ML\ -parse_translation \[(\<^syntax_const>\_hoare_vars\, K Hoare_Syntax.hoare_vars_tr)]\ -print_translation \[(\<^const_syntax>\Valid\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare\))]\ - -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 \[(\<^syntax_const>\_hoare_tc_vars\, K Hoare_Syntax.hoare_tc_vars_tr)]\ -print_translation \[(\<^const_syntax>\ValidTC\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_tc\))]\ - lemma SkipRule: "p \ q \ Valid p (Basic id) q" by (auto simp:Valid_def) @@ -103,7 +78,7 @@ lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" by (auto simp:Valid_def) -lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" +lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ 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 "\s s'. Sem c s s' \ s \ I \ s \ b \ s' \ I \ s \ I \ s' \ I \ s' \ 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 \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ 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. \(b x)}" - by blast + +subsubsection \Concrete syntax\ + +setup \ + Hoare_Syntax.setup + {Basic = \<^const_syntax>\Basic\, + Skip = \<^const_syntax>\annskip\, + Seq = \<^const_syntax>\Seq\, + Cond = \<^const_syntax>\Cond\, + While = \<^const_syntax>\While\, + Valid = \<^const_syntax>\Valid\, + ValidTC = \<^const_syntax>\ValidTC\} +\ -lemmas AbortRule = SkipRule \ \dummy version\ -ML_file \hoare_tac.ML\ + +subsubsection \Proof methods: VCG\ + +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 = \ - Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\ "verification condition generator" method_setup vcg_simp = \ Scan.succeed (fn ctxt => - SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ + SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ "verification condition generator plus simplification" method_setup vcg_tc = \ - Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\ "verification condition generator" method_setup vcg_tc_simp = \ Scan.succeed (fn ctxt => - SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ + SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ "verification condition generator plus simplification" end diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Hoare_Logic_Abort.thy --- 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 \Hoare Logic with an Abort statement for modelling run time errors\ + 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 \ '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 \ 'a assn \ 'a com \ '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'' \ Sem c2 s'' s' \ Sem (c1;c2) s s'" -| "Sem (IF b THEN c1 ELSE c2 FI) None None" -| "s \ b \ Sem c1 (Some s) s' \ Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'" -| "s \ b \ Sem c2 (Some s) s' \ Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'" +| "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (Seq c1 c2) s s'" +| "Sem (Cond b c1 c2) None None" +| "s \ b \ Sem c1 (Some s) s' \ Sem (Cond b c1 c2) (Some s) s'" +| "s \ b \ Sem c2 (Some s) s' \ Sem (Cond b c1 c2) (Some s) s'" | "Sem (While b x y c) None None" | "s \ b \ Sem (While b x y c) (Some s) (Some s)" | "s \ b \ Sem c (Some s) s'' \ Sem (While b x y c) s'' s' \ 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 \ \f . \s . s \ p \ f s \ 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 \hoare_syntax.ML\ -parse_translation \[(\<^syntax_const>\_hoare_abort_vars\, K Hoare_Syntax.hoare_vars_tr)]\ -print_translation \[(\<^const_syntax>\Valid\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_abort\))]\ - -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 \[(\<^syntax_const>\_hoare_abort_tc_vars\, K Hoare_Syntax.hoare_tc_vars_tr)]\ -print_translation \[(\<^const_syntax>\ValidTC\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_abort_tc\))]\ - text \The proof rules for partial correctness\ lemma SkipRule: "p \ q \ Valid p (Basic id) q" @@ -106,7 +76,7 @@ lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" by (auto simp:Valid_def) -lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" +lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ 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 "\s s'. Sem c s s' \ s \ Some ` (I \ b) \ s' \ Some ` I \ s \ Some ` I \ s' \ Some ` (I \ -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 \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ 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 \Derivation of the proof rules and, most importantly, the VCG tactic\ - -lemma Compl_Collect: "-(Collect b) = {x. \(b x)}" - by blast - -ML_file \hoare_tac.ML\ - -method_setup vcg = \ - Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\ - "verification condition generator" +subsection \Concrete syntax\ -method_setup vcg_simp = \ - Scan.succeed (fn ctxt => - SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ - "verification condition generator plus simplification" - -method_setup vcg_tc = \ - Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\ - "verification condition generator" - -method_setup vcg_tc_simp = \ - Scan.succeed (fn ctxt => - SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ - "verification condition generator plus simplification" +setup \ + Hoare_Syntax.setup + {Basic = \<^const_syntax>\Basic\, + Skip = \<^const_syntax>\annskip\, + Seq = \<^const_syntax>\Seq\, + Cond = \<^const_syntax>\Cond\, + While = \<^const_syntax>\While\, + Valid = \<^const_syntax>\Valid\, + ValidTC = \<^const_syntax>\ValidTC\} +\ \ \Special syntax for guarded statements and guarded array updates:\ syntax "_guarded_com" :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) "_array_update" :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) translations - "P \ c" == "IF P THEN c ELSE CONST Abort FI" - "a[i] := v" => "(i < CONST length a) \ (a := CONST list_update a i v)" + "P \ c" \ "IF P THEN c ELSE CONST Abort FI" + "a[i] := v" \ "(i < CONST length a) \ (a := CONST list_update a i v)" \ \reverse translation not possible because of duplicate \a\\ text \ @@ -241,4 +199,38 @@ you must write \j < length a \ a[i] := a!j\. \ + +subsection \Proof methods: VCG\ + +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 = \ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\ + "verification condition generator" + +method_setup vcg_simp = \ + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ + "verification condition generator plus simplification" + +method_setup vcg_tc = \ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\ + "verification condition generator" + +method_setup vcg_tc_simp = \ + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ + "verification condition generator plus simplification" + end diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Hoare_Syntax.thy --- /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 \Concrete syntax for Hoare logic, with translations for variables\ + +theory Hoare_Syntax + imports Main +begin + +syntax + "_assign" :: "idt \ 'b \ 'com" ("(2_ :=/ _)" [70, 65] 61) + "_Seq" :: "'com \ 'com \ 'com" ("(_;/ _)" [61,60] 60) + "_Cond" :: "'bexp \ 'com \ 'com \ 'com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) + "_While" :: "'bexp \ 'assn \ 'var \ 'com \ 'com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) + +syntax + "_While0" :: "'bexp \ 'assn \ 'com \ '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" + +syntax + "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \ bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) + "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \ bool" ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) +syntax (output) + "_hoare" :: "['assn, 'com, 'assn] \ bool" ("{_} // _ // {_}" [0,55,0] 50) + "_hoare_tc" :: "['assn, 'com, 'assn] \ bool" ("[_] // _ // [_]" [0,55,0] 50) + +ML_file \hoare_syntax.ML\ + +end diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Hoare_Tac.thy --- /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 \Hoare logic VCG tactic\ + +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. \(b x)}" + by blast + +ML_file \hoare_tac.ML\ + +end + +end diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Pointer_Examples.thy --- 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 \Examples of verifications of pointer programs\ + +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\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 \ List tl q Qs \ set Ps \ set Qs = {} \ size Qs \ 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\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 \ 'a" where "new A = (SOME a. a \ A)" diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Pointer_ExamplesAbort.thy --- 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 \Examples of verifications of pointer programs\ -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:" diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Pointers0.thy --- 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 \Alternative pointers\ + +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 \ 'a) \ 'a \ 'a list \ 'a \ bool" where @@ -68,9 +72,9 @@ lemma [simp]: "\x. u \ set as \ 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 \ 'a) \ 'a \ 'a list \ 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 \ 'a) \ 'a \ bool" where "islist h p \ (\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\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 \ 'a::ref" where "new A = (SOME a. a \ A & a \ Null)" @@ -427,5 +431,4 @@ apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin) done - end diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/SchorrWaite.thy --- 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 \Proof of the Schorr-Waite graph marking algorithm\ -theory SchorrWaite imports HeapSyntax begin +theory SchorrWaite + imports HeapSyntax +begin -section \Machinery for the Schorr-Waite proof\ +subsection \Machinery for the Schorr-Waite proof\ definition \ \Relations induced by a mapping\ @@ -194,8 +195,7 @@ done -section\The Schorr-Waite algorithm\ - +subsection \The Schorr-Waite algorithm\ theorem SchorrWaiteAlgorithm: "VARS c m l r t p q root @@ -573,4 +573,3 @@ qed end - diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/SepLogHeap.thy --- 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 \Heap abstractions for Separation Logic\ + +text \(at the moment only Path and List)\ + theory SepLogHeap -imports Main + imports Main begin type_synonym heap = "(nat \ nat option)" @@ -15,6 +16,7 @@ text\\Some\ means allocated, \None\ means free. Address \0\ serves as the null reference.\ + subsection "Paths in the heap" primrec Path :: "heap \ nat \ nat list \ nat \ bool" diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/Separation.thy --- 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

which stands for P H. No more compact, but avoids the funny H. - *) -theory Separation imports Hoare_Logic_Abort SepLogHeap begin +section \Separation logic\ + +theory Separation + imports Hoare_Logic_Abort SepLogHeap +begin text\The semantic definition of a few connectives:\ diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/document/root.tex --- 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} diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/hoare_syntax.ML --- 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>\_assign\, _) $ x $ e) xs = - Syntax.const \<^const_syntax>\Basic\ $ mk_fexp x e xs - | com_tr (Const (\<^const_syntax>\Basic\,_) $ f) _ = Syntax.const \<^const_syntax>\Basic\ $ f - | com_tr (Const (\<^const_syntax>\Seq\,_) $ c1 $ c2) xs = - Syntax.const \<^const_syntax>\Seq\ $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (\<^const_syntax>\Cond\,_) $ b $ c1 $ c2) xs = - Syntax.const \<^const_syntax>\Cond\ $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (\<^const_syntax>\While\,_) $ b $ I $ V $ c) xs = - Syntax.const \<^const_syntax>\While\ $ 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>\_assign\, _) $ x $ e) xs = + syntax_const ctxt #Basic $ mk_fexp x e xs + | tr (Const (\<^syntax_const>\_Seq\,_) $ c1 $ c2) xs = + syntax_const ctxt #Seq $ tr c1 xs $ tr c2 xs + | tr (Const (\<^syntax_const>\_Cond\,_) $ b $ c1 $ c2) xs = + syntax_const ctxt #Cond $ bexp_tr b xs $ tr c1 xs $ tr c2 xs + | tr (Const (\<^syntax_const>\_While\,_) $ 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>\_idts\, _) $ 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>\Valid\ $ - 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>\ValidTC\ $ - 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>\_assign\ $ fst which $ snd which - else Syntax.const \<^const_syntax>\annskip\ + then Syntax.const \<^syntax_const>\_assign\ $ a $ b + else syntax_const ctxt #Skip end; -fun com_tr' (Const (\<^const_syntax>\Basic\, _) $ f) = - if is_f f then mk_assign f - else Syntax.const \<^const_syntax>\Basic\ $ f - | com_tr' (Const (\<^const_syntax>\Seq\,_) $ c1 $ c2) = - Syntax.const \<^const_syntax>\Seq\ $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (\<^const_syntax>\Cond\, _) $ b $ c1 $ c2) = - Syntax.const \<^const_syntax>\Cond\ $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (\<^const_syntax>\While\, _) $ b $ I $ V $ c) = - Syntax.const \<^const_syntax>\While\ $ 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>\_Seq\ $ 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>\_Cond\ $ + 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>\_While\ $ + 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>\_hoare_vars\, hoare_vars_tr), + (\<^syntax_const>\_hoare_vars_tc\, hoare_tc_vars_tr)] #> + Sign.print_translation + [(#Valid consts, spec_tr' \<^syntax_const>\_hoare\), + (#ValidTC consts, spec_tr' \<^syntax_const>\_hoare_tc\)]; + end; - diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Hoare/hoare_tac.ML --- 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>\Orderings.less_eq\, [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>\SeqRule\) 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>\SkipRule\) i, + resolve_tac ctxt (get_thms \<^named_theorems>\AbortRule\) i, EVERY [ - resolve_tac ctxt @{thms BasicRule} i, + resolve_tac ctxt (get_thms \<^named_theorems>\BasicRule\) 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>\CondRule\) 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>\WhileRule\) 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>\SeqRuleTC\) 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>\SkipRuleTC\) i, EVERY [ - resolve_tac ctxt @{thms BasicRuleTC} i, + resolve_tac ctxt (get_thms \<^named_theorems>\BasicRuleTC\) 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>\CondRuleTC\) 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>\WhileRuleTC\) 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; - diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Isar_Examples/Hoare.thy --- 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 \Hoare Logic\ theory Hoare - imports Main + imports "HOL-Hoare.Hoare_Tac" begin subsection \Abstract syntax and semantics\ @@ -397,22 +397,16 @@ apply blast done -lemma Compl_Collect: "- Collect b = {x. \ b x}" - by blast - -lemmas AbortRule = SkipRule \ \dummy version\ -lemmas SeqRuleTC = SkipRule \ \dummy version\ -lemmas SkipRuleTC = SkipRule \ \dummy version\ -lemmas BasicRuleTC = SkipRule \ \dummy version\ -lemmas CondRuleTC = SkipRule \ \dummy version\ -lemmas WhileRuleTC = SkipRule \ \dummy version\ - -ML_file \~~/src/HOL/Hoare/hoare_tac.ML\ +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 = \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"}] )))))\ "verification condition generator for Hoare logic" diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/ROOT --- 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 diff -r 4fc3dc37f406 -r eac16c76273e src/HOL/Tools/etc/options --- 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 diff -r 4fc3dc37f406 -r eac16c76273e src/Pure/Admin/isabelle_cronjob.scala --- 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" + diff -r 4fc3dc37f406 -r eac16c76273e src/Pure/GUI/desktop_app.scala --- /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)) +} diff -r 4fc3dc37f406 -r eac16c76273e src/Pure/Thy/presentation.scala --- 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)) } diff -r 4fc3dc37f406 -r eac16c76273e src/Pure/Tools/build.scala --- 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 = diff -r 4fc3dc37f406 -r eac16c76273e src/Pure/Tools/java_monitor.scala --- 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() diff -r 4fc3dc37f406 -r eac16c76273e src/Pure/build-jars --- 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 diff -r 4fc3dc37f406 -r eac16c76273e src/Tools/jEdit/patches/panel_font --- /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); + } //}}}