# 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>\