From f8b1c7d5ae75043f38e35a4c3339b48a9b8d99e5 Mon Sep 17 00:00:00 2001 From: Matthew Brecknell Date: Tue, 25 Oct 2016 11:23:16 +1100 Subject: [PATCH] Isabelle2016-1: update Simpl --- tools/c-parser/Simpl/AlternativeSmallStep.thy | 120 ++- tools/c-parser/Simpl/DPC0Expressions.thy | 2 +- tools/c-parser/Simpl/DPC0Library.thy | 18 +- tools/c-parser/Simpl/HeapList.thy | 18 +- tools/c-parser/Simpl/Hoare.thy | 8 +- tools/c-parser/Simpl/HoarePartial.thy | 32 +- tools/c-parser/Simpl/HoarePartialDef.thy | 34 +- tools/c-parser/Simpl/HoarePartialProps.thy | 44 +- tools/c-parser/Simpl/HoareTotal.thy | 34 +- tools/c-parser/Simpl/HoareTotalDef.thy | 18 +- tools/c-parser/Simpl/HoareTotalProps.thy | 42 +- tools/c-parser/Simpl/Language.thy | 70 +- tools/c-parser/Simpl/ROOT | 1 + tools/c-parser/Simpl/Semantic.thy | 28 +- tools/c-parser/Simpl/Simpl.thy | 30 +- tools/c-parser/Simpl/Simpl_Heap.thy | 6 +- tools/c-parser/Simpl/SmallStep.thy | 52 +- tools/c-parser/Simpl/StateSpace.thy | 4 +- tools/c-parser/Simpl/SyntaxTest.thy | 2 +- tools/c-parser/Simpl/Termination.thy | 74 +- tools/c-parser/Simpl/UserGuide.thy | 704 +++++++++--------- tools/c-parser/Simpl/Vcg.thy | 70 +- tools/c-parser/Simpl/XVcg.thy | 8 +- tools/c-parser/Simpl/ex/Closure.thy | 4 +- tools/c-parser/Simpl/ex/ClosureEx.thy | 2 +- tools/c-parser/Simpl/ex/Compose.thy | 24 +- tools/c-parser/Simpl/ex/Quicksort.thy | 2 +- tools/c-parser/Simpl/ex/VcgEx.thy | 350 ++++----- tools/c-parser/Simpl/ex/VcgExSP.thy | 290 ++++---- tools/c-parser/Simpl/ex/VcgExTotal.thy | 14 +- tools/c-parser/Simpl/hoare.ML | 46 +- tools/c-parser/Simpl/hoare_syntax.ML | 26 +- 32 files changed, 1079 insertions(+), 1098 deletions(-) diff --git a/tools/c-parser/Simpl/AlternativeSmallStep.thy b/tools/c-parser/Simpl/AlternativeSmallStep.thy index 013b46295..0b3184055 100644 --- a/tools/c-parser/Simpl/AlternativeSmallStep.thy +++ b/tools/c-parser/Simpl/AlternativeSmallStep.thy @@ -26,13 +26,13 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Alternative Small Step Semantics *} +section \Alternative Small Step Semantics\ theory AlternativeSmallStep imports HoareTotalDef begin -text {* +text \ This is the small-step semantics, which is described and used in my PhD-thesis \cite{Schirmer-PhD}. It decomposes the statement into a list of statements and finally executes the head. So the redex is always the head of the list. The equivalence between termination @@ -42,10 +42,10 @@ the new small-step semantics. However, it is technically more involved since the configurations are more complicated. Thats why I switched to the new small-step semantics in the "main trunk". I keep this alternative version and the important proofs in this theory, so that one can compare both approaches. -*} +\ -subsection {*Small-Step Computation: @{text "\\(cs, css, s) \ (cs', css', s')"}*} +subsection \Small-Step Computation: \\\(cs, css, s) \ (cs', css', s')\\ type_synonym ('s,'p,'f) continuation = "('s,'p,'f) com list \ ('s,'p,'f) com list" @@ -164,7 +164,7 @@ abbreviation "\\cs0 \\<^sup>+ cs1 == (step \)\<^sup>+\<^sup>+ cs0 cs1" -subsubsection {* Structural Properties of Small Step Computations *} +subsubsection \Structural Properties of Small Step Computations\ lemma Fault_app_steps: "\\(cs@xs,css,Fault f) \\<^sup>* (xs,css,Fault f)" proof (induct cs) @@ -202,9 +202,9 @@ next by simp qed -text {* We can only append commands inside a block, if execution does not +text \We can only append commands inside a block, if execution does not enter or exit a block. - *} +\ lemma app_step: assumes step: "\\(cs,css,s) \ (cs',css',t)" shows "css=css' \ \\(cs@xs,css,s) \ (cs'@xs,css',t)" @@ -213,9 +213,9 @@ apply induct apply (simp_all del: fun_upd_apply,(blast intro: step.intros)+) done -text {* We can append whole blocks, without interfering with the actual +text \We can append whole blocks, without interfering with the actual block. Outer blocks do not influence execution of - inner blocks. *} + inner blocks.\ lemma app_css_step: assumes step: "\\(cs,css,s) \ (cs',css',t)" shows "\\(cs,css@xs,s) \ (cs',css'@xs,t)" @@ -224,13 +224,13 @@ apply induct apply (simp_all del: fun_upd_apply,(blast intro: step.intros)+) done -ML {* +ML \ ML_Thms.bind_thm ("trancl_induct3", Split_Rule.split_rule @{context} (Rule_Insts.read_instantiate @{context} [((("a", 0), Position.none), "(ax, ay, az)"), ((("b", 0), Position.none), "(bx, by, bz)")] [] @{thm tranclp_induct})); -*} +\ lemma app_css_steps: assumes step: "\\(cs,css,s) \\<^sup>+ (cs',css',t)" @@ -380,7 +380,7 @@ proof - by auto qed -subsubsection {* Equivalence between Big and Small-Step Semantics *} +subsubsection \Equivalence between Big and Small-Step Semantics\ lemma exec_impl_steps: assumes exec: "\\\c,s\ \ t" @@ -553,13 +553,13 @@ inductive_cases execs_elim_cases [cases set]: "\\\[],css,s\ \ t" "\\\c#cs,css,s\ \ t" -ML {* +ML \ ML_Thms.bind_thm ("converse_rtrancl_induct3", Split_Rule.split_rule @{context} (Rule_Insts.read_instantiate @{context} [((("a", 0), Position.none), "(cs, css, s)"), ((("b", 0), Position.none), "(cs', css', t)")] [] @{thm converse_rtranclp_induct})); -*} +\ lemma execs_Fault_end: assumes execs: "\\\cs,css,s\ \ t" shows "s=Fault f\ t=Fault f" @@ -660,11 +660,9 @@ next from execs_rest Abrupt have "\\\Throw # cs,css,Normal t''\ \ t" by (cases) auto - then obtain v where - "\\\Throw,Normal t''\ \ v" and - rest: "\\\cs,css,v\ \ t" + then obtain v where v: "\\\Throw,Normal t''\ \ v" "\\\cs,css,v\ \ t" by (clarsimp elim!: execs_elim_cases) - moreover from this have "v=Abrupt t''" + moreover from v have "v=Abrupt t''" by (auto elim: exec_Normal_elim_cases) ultimately show ?thesis by (auto intro: execs.Cons) @@ -700,7 +698,7 @@ corollary steps_eq_exec: "\\([c],[],s) \\<^sup>* ( by (blast intro: steps_impl_exec exec_impl_steps) -subsection {* Infinite Computations: @{text "inf \ cs css s"}*} +subsection \Infinite Computations: \inf \ cs css s\\ definition inf :: "[('s,'p,'f) body,('s,'p,'f) com list,('s,'p,'f) continuation list,('s,'f) xstate] @@ -711,7 +709,7 @@ lemma not_infI: "\\f. \f 0 = (cs,css,s); \i. \\ \ \inf \ cs css s" by (auto simp add: inf_def) -subsection {* Equivalence of Termination and Absence of Infinite Computations *} +subsection \Equivalence of Termination and Absence of Infinite Computations\ inductive "terminatess":: "[('s,'p,'f) body,('s,'p,'f) com list, @@ -979,13 +977,13 @@ next qed -ML {* +ML \ ML_Thms.bind_thm ("rtrancl_induct3", Split_Rule.split_rule @{context} (Rule_Insts.read_instantiate @{context} [((("a", 0), Position.none), "(ax, ay, az)"), ((("b", 0), Position.none), "(bx, by, bz)")] [] @{thm rtranclp_induct})); -*} +\ lemma steps_preserves_terminations: assumes steps: "\\(cs,css,s) \\<^sup>* (cs',css',t)" @@ -1232,7 +1230,7 @@ next have not_finished': "\i < Suc k. \ (CS (f i) = cs \ CSS (f i) = css)" by fact with simul have not_finished: "\i (pcs i = [] \ pcss i = [])" - by (auto simp add: CS_def CSS_def S_def split: split_if_asm) + by (auto simp add: CS_def CSS_def S_def split: if_split_asm) show ?case proof (clarify) fix i @@ -1318,7 +1316,7 @@ next moreover from css' cs' pcs_pcss_Suc_i obtain "pcs (Suc i) = p'@ps" and "pcss (Suc i) = []" - by (simp split: split_if_asm) + by (simp split: if_split_asm) ultimately show ?thesis using pcs_i pcss_Nil f_i f_Suc_i by (simp add: CS_def CSS_def S_def p_def) @@ -1343,7 +1341,7 @@ next from css' pcs_pcss_Suc_i obtain "pcs (Suc i) = cs'" "pcss (Suc i) = [(pnorm@ps, pabr@ps)]" apply (cases "pcss (Suc i)") - apply (auto split: split_if_asm) + apply (auto split: if_split_asm) done ultimately show ?thesis using pcs_i pcss_Nil f_i f_Suc_i @@ -1376,7 +1374,7 @@ next moreover from cs'' css'' css' False pcs_pcss_Suc_i obtain "pcs (Suc i) = cs'" "pcss (Suc i) = css'''@pcss i" - apply (auto split: split_if_asm) + apply (auto split: if_split_asm) apply (drule (4) last_butlast_app) by simp ultimately show ?thesis @@ -1389,10 +1387,10 @@ next proof (cases "butlast (pcss i)") case (Cons bpcs bpcss) with cs''_Nil step_i_full css'' - have "\\ ([],[hd css'']@tl css'',t'') \ (cs',css',t')" + have *: "\\ ([],[hd css'']@tl css'',t'') \ (cs',css',t')" by simp moreover - from step_Nil [OF this] + from step_Nil [OF *] have css': "css'=tl css''" by simp ultimately have @@ -1400,7 +1398,7 @@ next by simp from css'' Cons pcss_i_not_Nil have "hd css'' = hd (pcss i)" - by (auto simp add: neq_Nil_conv split: split_if_asm) + by (auto simp add: neq_Nil_conv split: if_split_asm) with cs'' cs''_Nil Nil_change_css_step [where ass="[hd css'']" and css="tl css''" and ass'="[]" and @@ -1413,7 +1411,7 @@ next moreover from css' css'' cs''_Nil Cons pcss_i_not_Nil pcs_pcss_Suc_i obtain "pcs (Suc i) = cs'" "pcss (Suc i) = tl (pcss i)" - apply (clarsimp split: split_if_asm) + apply (clarsimp split: if_split_asm) apply (drule (4) last_butlast_tl) by simp ultimately show ?thesis @@ -1425,7 +1423,7 @@ next obtain pnorm pabr where css'': "css''= [(pnorm@cs,pabr@cs)]@css" and pcss_i: "pcss i = [(pnorm,pabr)]" - by (force simp add: neq_Nil_conv split: split_if_asm) + by (force simp add: neq_Nil_conv split: if_split_asm) with cs''_Nil step_i_full have "\\([],[(pnorm@cs,pabr@cs)]@css,t'') \ (cs',css',t')" by simp @@ -1443,7 +1441,7 @@ next moreover from css'' css' cs' pcss_i pcs_pcss_Suc_i obtain "pcs (Suc i) = ?pcs_Suc_i" "pcss (Suc i) = []" - by (simp split: split_if_asm xstate.splits) + by (simp split: if_split_asm xstate.splits) ultimately show ?thesis using pcss_i cs'' cs''_Nil f_i f_Suc_i @@ -1495,7 +1493,7 @@ proof - have "\\ (pcs 0, pcss 0, S (f 0)) \\<^sup>* (pcs k, pcss k, S (f k))". moreover from f_0 simul [rule_format, of 0] have "(pcs 0, pcss 0, S (f 0)) = ([c],[],s)" - by (auto split: split_if_asm simp add: CS_def CSS_def S_def) + by (auto split: if_split_asm simp add: CS_def CSS_def S_def) ultimately show ?thesis by simp qed @@ -1573,7 +1571,7 @@ next by (auto simp add: CSS_def CS_def cong: if_cong) from c_unfinished [rule_format, of k] f_k pcs_pcss_k have pcs_pcss_empty: "\ (pcs = [] \ pcss = [])" - by (auto simp add: CS_def CSS_def S_def split: split_if_asm) + by (auto simp add: CS_def CSS_def S_def split: if_split_asm) show ?thesis proof (cases "pcss = []") case True @@ -1651,23 +1649,23 @@ next proof (cases "butlast pcss") case (Cons bpcs bpcss) with cs''_Nil step_i_full css'' - have "\\ ([],[hd css'']@tl css'',t'') \ (cs',css',t')" + have *: "\\ ([],[hd css'']@tl css'',t'') \ (cs',css',t')" by simp moreover - from step_Nil [OF this] + from step_Nil [OF *] obtain css': "css'=tl css''" and cs': "cs' = (case t'' of Abrupt s' \ snd (hd css'') | _ \ fst (hd css''))" by (auto split: xstate.splits) from css'' Cons pcss_k_not_Nil have "hd css'' = hd pcss" - by (auto simp add: neq_Nil_conv split: split_if_asm) + by (auto simp add: neq_Nil_conv split: if_split_asm) with css' cs' css'' cs''_Nil Cons pcss_k_not_Nil f_Suc_k eq_i_Suc_k show ?thesis apply (rule_tac x="cs'" in exI) apply (rule_tac x="tl pcss" in exI) apply (clarsimp split: xstate.splits - simp add: CS_def CSS_def neq_Nil_conv split: split_if_asm) + simp add: CS_def CSS_def neq_Nil_conv split: if_split_asm) done next case Nil @@ -1675,7 +1673,7 @@ next obtain pnorm pabr where css'': "css''= [(pnorm@cs,pabr@cs)]@css" and pcss_k: "pcss = [(pnorm,pabr)]" - by (force simp add: neq_Nil_conv split: split_if_asm) + by (force simp add: neq_Nil_conv split: if_split_asm) with cs''_Nil step_i_full have "\\([],[(pnorm@cs,pabr@cs)]@css,t'') \ (cs',css',t')" by simp @@ -1745,7 +1743,7 @@ proof - show ?thesis proof (cases "\i. CS (f i) = cs \ CSS (f i) = css") case True - def k\"(LEAST i. CS (f i) = cs \ CSS (f i) = css)" + define k where "k = (LEAST i. CS (f i) = cs \ CSS (f i) = css)" from True obtain CS_f_k: "CS (f k) = cs" and CSS_f_k: "CSS (f k) = css" apply - @@ -1780,7 +1778,7 @@ proof - by iprover from pcs_pcss [rule_format, of k] CS_f_k CSS_f_k have finished: "pcs k = []" "pcss k = []" - by (auto simp add: CS_def CSS_def S_def split: split_if_asm) + by (auto simp add: CS_def CSS_def S_def split: if_split_asm) from pcs_pcss have simul: "\i\k. (if pcss i = [] then CSS (f i)=css \ CS (f i)=pcs i@cs else CS (f i)=pcs i \ @@ -1827,10 +1825,10 @@ proof - [(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@ css)" by iprover - def "g" \ "\i. (pcs i, pcss i, S (f i))" + define g where "g i = (pcs i, pcss i, S (f i))" for i from pcs_pcss [rule_format, of 0] f_0 have "g 0 = ([c],[],s)" - by (auto split: split_if_asm simp add: CS_def CSS_def S_def g_def) + by (auto split: if_split_asm simp add: CS_def CSS_def S_def g_def) moreover from steps_hd_drop_suffix_infinite [OF f_0 f_step unfinished pcs_pcss] have "\i. \\g i \ g (Suc i)" @@ -1876,7 +1874,7 @@ next f_0: "f 0 = (c1# c2#cs,css,Normal s)" and f_step: "\i. \\f i \ f (Suc i)" by (auto simp add: inf_def) - def g\"\i. case i of 0 \ (Seq c1 c2#cs,css,Normal s) | Suc j \ f j" + define g where "g i = (case i of 0 \ (Seq c1 c2#cs,css,Normal s) | Suc j \ f j)" for i with f_0 have "\\g 0 \ g (Suc 0)" by (auto intro: step.intros) @@ -1915,7 +1913,7 @@ next f_0: "f 0 = (c # While b c #cs,css,Normal s)" and f_step: "\i. \\f i \ f (Suc i)" by (auto simp add: inf_def) - def h\"\i. case i of 0 \ (While b c#cs,css,Normal s) | Suc j \ f j" + define h where "h i = (case i of 0 \ (While b c#cs,css,Normal s) | Suc j \ f j)" for i with b f_0 have "\\h 0 \ h (Suc 0)" by (auto intro: step.intros) @@ -1952,7 +1950,7 @@ next f_0: "f 0 = ([c1],(cs,c2#cs)#css,Normal s)" and f_step: "\i. \\f i \ f (Suc i)" by (auto simp add: inf_def) - def h\"\i. case i of 0 \ (Catch c1 c2#cs,css,Normal s) | Suc j \ f j" + define h where "h i = (case i of 0 \ (Catch c1 c2#cs,css,Normal s) | Suc j \ f j)" for i with f_0 have "\\h 0 \ h (Suc 0)" by (auto intro: step.intros) @@ -2542,7 +2540,7 @@ where {((t,q),(s,p)). \\the (\ p)\Normal s \ (\css. \\([the (\ p)],[],Normal s) \\<^sup>+ ([the (\ q)],css,Normal t))}" -text {* Sequencing computations, or more exactly continuation stacks *} +text \Sequencing computations, or more exactly continuation stacks\ primrec seq:: "(nat \ 'a list) \ nat \ 'a list" where "seq css 0 = []" | @@ -2571,7 +2569,7 @@ proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain, done show False proof - - from inf' -- {* Skolemization of css with axiom of choice *} + from inf' \ \Skolemization of css with axiom of choice\ have "\css. \i. \\(the (\ (p i))) \ Normal (s i) \ \\([the (\ (p i))],[],Normal (s i)) \\<^sup>+ ([the (\ (p (Suc i)))],css i,Normal (s (Suc i)))" @@ -2583,7 +2581,7 @@ proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain, step_css: "\i. \\([the (\ (p i))],[],Normal (s i)) \\<^sup>+ ([the (\ (p (Suc i)))],css i,Normal (s (Suc i)))" by blast - def f == "\i. ([the (\ (p i))], seq css i,Normal (s i)::('a,'c) xstate)" + define f where "f i = ([the (\ (p i))], seq css i,Normal (s i)::('a,'c) xstate)" for i have "f 0 = ([the (\ (p 0))],[],Normal (s 0))" by (simp add: f_def) moreover @@ -2608,7 +2606,7 @@ proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain, qed qed -text {* An alternative proof using Hilbert-choice instead of axiom of choice.*} +text \An alternative proof using Hilbert-choice instead of axiom of choice.\ theorem "wf (termi_call_steps \)" proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain, clarify,simp) @@ -2631,10 +2629,10 @@ proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain, done show "False" proof - - def CSS \ "\i. (SOME css. + define CSS where "CSS i = (SOME css. \\([the (\ (p i))],[], Normal (s i)) \\<^sup>+ - ([the (\ (p (i+1)))],css,Normal (s (i+1))))" - def f == "\i. ([the (\ (p i))], seq CSS i,Normal (s i)::('a,'c) xstate)" + ([the (\ (p (i+1)))],css,Normal (s (i+1))))" for i + define f where "f i = ([the (\ (p i))], seq CSS i,Normal (s i)::('a,'c) xstate)" for i have "f 0 = ([the (\ (p 0))],[],Normal (s 0))" by (simp add: f_def) moreover @@ -2980,7 +2978,7 @@ corollary terminates_iff_not_inf: apply (erule not_inf_impl_terminates) done -subsection {* Completeness of Total Correctness Hoare Logic*} +subsection \Completeness of Total Correctness Hoare Logic\ lemma ConseqMGT: assumes modif: "\Z::'a. \,\ \\<^sub>t\<^bsub>/F\<^esub> (P' Z::'a assn) c (Q' Z),(A' Z)" @@ -3734,10 +3732,10 @@ next qed -text {* To prove a procedure implementation correct it suffices to assume +text \To prove a procedure implementation correct it suffices to assume only the procedure specifications of procedures that actually occur during evaluation of the body. - *} +\ lemma Call_lemma: assumes Call: "\q \ dom \. \Z. \,\ \\<^sub>t\<^bsub>/F\<^esub> @@ -3815,7 +3813,7 @@ lemma image_Un_conv: "f ` (\p\dom \. \Z. {x p Z}) = (\ by (auto iff: not_None_eq) -text {* Another proof of @{text MGT_Call}, maybe a little more readable *} +text \Another proof of \MGT_Call\, maybe a little more readable\ lemma "\p \ dom \. \Z. \,{} \\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \ \\\Call p,Normal s\ \\({Stuck} \ Fault ` (-F)) \ @@ -3827,15 +3825,15 @@ proof - { fix p Z \ assume defined: "p \ dom \" - def Specs == "(\p\dom \. \Z. + define Specs where "Specs = (\p\dom \. \Z. {({s. s=Z \ \\\Call p,Normal s\ \\({Stuck} \ Fault ` (-F)) \ \\Call p\Normal s}, p, {t. \\\Call p,Normal Z\ \ Normal t}, {t. \\\Call p,Normal Z\ \ Abrupt t})})" - def Specs_wf == "(\p \. (\(P,q,Q,A). - (P \ {s. ((s,q),\,p) \ termi_call_steps \}, q, Q, A)) ` Specs)" + define Specs_wf where "Specs_wf p \ = (\(P,q,Q,A). + (P \ {s. ((s,q),\,p) \ termi_call_steps \}, q, Q, A)) ` Specs" for p \ have "\,Specs_wf p \ \\<^sub>t\<^bsub>/F\<^esub>({\} \ {s. s = Z \ \\\the (\ p),Normal s\ \\({Stuck} \ Fault ` (-F)) \ @@ -3883,4 +3881,4 @@ proof - done qed -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/DPC0Expressions.thy b/tools/c-parser/Simpl/DPC0Expressions.thy index 3db322ff8..142713a13 100644 --- a/tools/c-parser/Simpl/DPC0Expressions.thy +++ b/tools/c-parser/Simpl/DPC0Expressions.thy @@ -4,7 +4,7 @@ License: LGPL *) -section {* SHORTENED! Parallel expressions in DPC/Hoare. *} +section \SHORTENED! Parallel expressions in DPC/Hoare.\ theory DPC0Expressions imports Main begin diff --git a/tools/c-parser/Simpl/DPC0Library.thy b/tools/c-parser/Simpl/DPC0Library.thy index 22d2de20a..a6fd0845a 100644 --- a/tools/c-parser/Simpl/DPC0Library.thy +++ b/tools/c-parser/Simpl/DPC0Library.thy @@ -4,20 +4,20 @@ License: LGPL *) -section {* DPC0 standard library *} +section \DPC0 standard library\ theory DPC0Library imports DPC0Expressions Vcg begin -text {* This theory constitutes a standard library for DPC0 programs. At +text \This theory constitutes a standard library for DPC0 programs. At first, it includes (indirectly) the C0 library and (directly) its extensions for DPC0 specific expressions. Secondly, the Vcg of the verification environment is included and its syntax extended by the DPC0 specific statement constructs for contextualization. -*} +\ (* =================================================== *) -section {* Auxiliary functions for the concrete syntax *} +section \Auxiliary functions for the concrete syntax\ (* =================================================== *) @@ -34,7 +34,7 @@ where (* ============================================= *) -section {* Concrete syntax for Contextualization *} +section \Concrete syntax for Contextualization\ (* ============================================= *) syntax @@ -53,7 +53,7 @@ translations "_WhereElse m c s1 s2" => "(_Loc (_locinit c (p_and \c m)) s1);; (_Loc (_locinit c (p_and \c (p_not m))) s2)" -print_translation {* +print_translation \ let fun in_tr' [Const (@{const_syntax list_multsel}, _) $ x $ @@ -87,9 +87,9 @@ print_translation {* [(@{syntax_const "_Assign"}, K in_tr'), (@{syntax_const "_Loc"}, K where_tr')] end -*} +\ -print_ast_translation {* +print_ast_translation \ let fun where_else_tr' [Appl [Constant @{syntax_const "_Where"}, m, c, s1], @@ -98,7 +98,7 @@ print_ast_translation {* if c = c' andalso m = m' then Appl [Constant @{syntax_const "_WhereElse"}, m, c, s1, s2] else raise Match in [(@{syntax_const "_seq"}, K where_else_tr')] end -*} +\ end diff --git a/tools/c-parser/Simpl/HeapList.thy b/tools/c-parser/Simpl/HeapList.thy index df27c8f06..dc41bf81b 100644 --- a/tools/c-parser/Simpl/HeapList.thy +++ b/tools/c-parser/Simpl/HeapList.thy @@ -25,12 +25,12 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Paths and Lists in the Heap *} +section \Paths and Lists in the Heap\ theory HeapList imports Simpl_Heap begin -text {* Adapted from 'HOL/Hoare/Heap.thy'. *} +text \Adapted from 'HOL/Hoare/Heap.thy'.\ subsection "Paths in The Heap" @@ -67,10 +67,10 @@ lemma Path_upd_same [simp]: ((p=Null \ q=Null \ qs = []) \ (p\Null \ q=p \ (\x\set qs. x=p)))" by (induct qs) auto -text {* @{thm[source] Path_upd_same} prevents +text \@{thm[source] Path_upd_same} prevents @{term "p\Null \ Path p (f(p:=p)) q qs = X"} from looping, because of @{thm[source] Path_not_Null_iff} and @{thm[source]fun_upd_apply}. - *} +\ lemma notin_Path_updateI [intro]: "\Path p h q ps ; r \ set ps\ \ Path p (h(r := y)) q ps " @@ -135,10 +135,10 @@ apply simp apply (fast dest: List_upd_same_lemma) done -text {* @{thm[source] List_upd_same} prevents +text \@{thm[source] List_upd_same} prevents @{term "p\Null \ List p (h(p:=p)) as = X"} from looping, because of @{thm[source] List_not_Null} and @{thm[source] fun_upd_apply}. - *} +\ lemma List_update_new [simp]: "\set ps \ set alloc\ \ List p (h(new (set alloc) := x)) ps = List p h ps" @@ -189,9 +189,9 @@ lemma heap_eq_ListI1: by (simp add: heap_eq_List_eq [OF hp_eq]) -text {* The following lemmata are usefull for the simplifier to instantiate +text \The following lemmata are usefull for the simplifier to instantiate bound variables in the assumptions resp. conclusion, using the uniqueness -of the List predicate *} +of the List predicate\ lemma conj_impl_simp: "(P \ Q \ K) = (P \ Q \ K)" by auto @@ -294,4 +294,4 @@ apply (drule (1) the1_equality) apply simp done -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/Hoare.thy b/tools/c-parser/Simpl/Hoare.thy index 0884a52bd..f15838f1a 100644 --- a/tools/c-parser/Simpl/Hoare.thy +++ b/tools/c-parser/Simpl/Hoare.thy @@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Auxiliary Definitions/Lemmas to Facilitate Hoare Logic *} +section \Auxiliary Definitions/Lemmas to Facilitate Hoare Logic\ theory Hoare imports HoarePartial HoareTotal begin @@ -322,9 +322,9 @@ lemma in_mlex_iff: lemma in_inv_image_iff: "(x,y) \ inv_image r f = ((f x, f y) \ r)" by (simp add: inv_image_def) -text {* This is actually the same as @{thm [source] wf_mlex}. However, this basic +text \This is actually the same as @{thm [source] wf_mlex}. However, this basic proof took me so long that I'm not willing to delete it. -*} +\ lemma wf_measure_lex_prod [simp,intro]: assumes wf_r: "wf r" shows "wf (f <*mlex*> r)" @@ -421,4 +421,4 @@ lemma all_imp_eq_triv: "(\x. x = k \ Q) = Q" "(\x. k = x \ Q) = Q" by auto -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/HoarePartial.thy b/tools/c-parser/Simpl/HoarePartial.thy index d401b41da..45e8afe40 100644 --- a/tools/c-parser/Simpl/HoarePartial.thy +++ b/tools/c-parser/Simpl/HoarePartial.thy @@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Derived Hoare Rules for Partial Correctness *} +section \Derived Hoare Rules for Partial Correctness\ theory HoarePartial imports HoarePartialProps begin @@ -367,8 +367,8 @@ proof - done qed -text {* @{term "J"} will be instantiated by tactic with @{term "gs' \ I"} for - those guards that are not stripped.*} +text \@{term "J"} will be instantiated by tactic with @{term "gs' \ I"} for + those guards that are not stripped.\ lemma WhileAnnoG: "\,\\\<^bsub>/F\<^esub> P (guards gs (whileAnno b J V (Seq c (guards gs Skip)))) Q,A @@ -377,7 +377,7 @@ lemma WhileAnnoG: by (simp add: whileAnnoG_def whileAnno_def while_def) -text {* This form stems from @{term "strip_guards F (whileAnnoG gs b I V c)"} *} +text \This form stems from @{term "strip_guards F (whileAnnoG gs b I V c)"}\ lemma WhileNoGuard': assumes P_I: "P \ I" @@ -929,8 +929,8 @@ qed lemma ProcProcParModifyReturn: assumes q: "P \ {s. p s = q} \ P'" - --{* @{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in - @{term P'}, so the vcg can simplify it. *} + \\@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in + @{term P'}, so the vcg can simplify it.\ assumes to_prove: "\,\\\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" assumes ret_nrm_modif: "\s t. t \ (Modif (init s)) \ return' s t = return s t" @@ -953,8 +953,8 @@ qed lemma ProcProcParModifyReturnSameFaults: assumes q: "P \ {s. p s = q} \ P'" - --{* @{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in - @{term P'}, so the vcg can simplify it. *} + \\@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in + @{term P'}, so the vcg can simplify it.\ assumes to_prove: "\,\\\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" assumes ret_nrm_modif: "\s t. t \ (Modif (init s)) \ return' s t = return s t" @@ -978,8 +978,8 @@ qed lemma ProcProcParModifyReturnNoAbr: assumes q: "P \ {s. p s = q} \ P'" - --{* @{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as - first conjunction in @{term P'}, so the vcg can simplify it. *} + \\@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as + first conjunction in @{term P'}, so the vcg can simplify it.\ assumes to_prove: "\,\\\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" assumes ret_nrm_modif: "\s t. t \ (Modif (init s)) \ return' s t = return s t" @@ -998,8 +998,8 @@ qed lemma ProcProcParModifyReturnNoAbrSameFaults: assumes q: "P \ {s. p s = q} \ P'" - --{* @{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as - first conjunction in @{term P'}, so the vcg can simplify it. *} + \\@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as + first conjunction in @{term P'}, so the vcg can simplify it.\ assumes to_prove: "\,\\\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" assumes ret_nrm_modif: "\s t. t \ (Modif (init s)) \ return' s t = return s t" @@ -1106,16 +1106,16 @@ proof - qed -subsection {* Rules for Single-Step Proof \label{sec:hoare-isar} *} +subsection \Rules for Single-Step Proof \label{sec:hoare-isar}\ -text {* +text \ We are now ready to introduce a set of Hoare rules to be used in single-step structured proofs in Isabelle/Isar. \medskip Assertions of Hoare Logic may be manipulated in calculational proofs, with the inclusion expressed in terms of sets or predicates. Reversed order is supported as well. -*} +\ lemma annotateI [trans]: "\\,\\\<^bsub>/F\<^esub>P anno Q,A; c = anno\ \ \,\\\<^bsub>/F\<^esub>P c Q,A" @@ -1209,4 +1209,4 @@ lemma WhileConj [intro?]: (* FIXME: Add rules for guarded while *) -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/HoarePartialDef.thy b/tools/c-parser/Simpl/HoarePartialDef.thy index 4e89bfb88..3b1ae23ae 100644 --- a/tools/c-parser/Simpl/HoarePartialDef.thy +++ b/tools/c-parser/Simpl/HoarePartialDef.thy @@ -26,12 +26,12 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Hoare Logic for Partial Correctness *} +section \Hoare Logic for Partial Correctness\ theory HoarePartialDef imports Semantic begin type_synonym ('s,'p) quadruple = "('s assn \ 'p \ 's assn \ 's assn)" -subsection {* Validity of Hoare Tuples: @{text "\,\\\<^bsub>/F\<^esub> P c Q,A"} *} +subsection \Validity of Hoare Tuples: \\,\\\<^bsub>/F\<^esub> P c Q,A\\ definition valid :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] => bool" @@ -74,7 +74,7 @@ notation (ASCII) cnvalid ("_,_|=_:'/_/ _ _ _,_" [61,60,60,60,1000, 20, 1000,1000] 60) -subsection {*Properties of Validity *} +subsection \Properties of Validity\ lemma valid_iff_nvalid: "\\\<^bsub>/F\<^esub> P c Q,A = (\n. \\n:\<^bsub>/F\<^esub> P c Q,A)" apply (simp only: valid_def nvalid_def exec_iff_execn ) @@ -176,12 +176,11 @@ proof (rule nvalidI) next case False with exec P validn - have "t' \ Normal ` Q \ Abrupt ` A" + have *: "t' \ Normal ` Q \ Abrupt ` A" by (auto simp add: nvalid_def) - moreover - from this t' have "t'=t" + with t' have "t'=t" by auto - ultimately show ?thesis + with * show ?thesis by simp qed qed @@ -209,18 +208,17 @@ proof (rule validI) next case False with exec P valid - have "t' \ Normal ` Q \ Abrupt ` A" + have *: "t' \ Normal ` Q \ Abrupt ` A" by (auto simp add: valid_def) - moreover - from this t' have "t'=t" + with t' have "t'=t" by auto - ultimately show ?thesis + with * show ?thesis by simp qed qed -subsection {* The Hoare Rules: @{text "\,\\\<^bsub>/F\<^esub> P c Q,A"} *} +subsection \The Hoare Rules: \\,\\\<^bsub>/F\<^esub> P c Q,A\\ lemma mono_WeakenContext: "A \ B \ (\(P, c, Q, A'). (\, \, F, P, c, Q, A') \ A) x \ @@ -284,14 +282,14 @@ where | ExFalso: "\\n. \,\\n:\<^bsub>/F\<^esub> P c Q,A; \ \\\<^bsub>/F\<^esub> P c Q,A\ \ \,\\\<^bsub>/F\<^esub> P c Q,A" - -- {* This is a hack rule that enables us to derive completeness for - an arbitrary context @{text "\"}, from completeness for an empty context.*} + \ \This is a hack rule that enables us to derive completeness for + an arbitrary context \\\, from completeness for an empty context.\ -text {* Does not work, because of rule ExFalso, the context @{text "\"} is to blame. +text \Does not work, because of rule ExFalso, the context \\\ is to blame. A weaker version with empty context can be derived from soundness - and completeness later on. *} + and completeness later on.\ lemma hoare_strip_\: assumes deriv: "\,\\\<^bsub>/F\<^esub> P p Q,A" shows "strip (-F) \,\\\<^bsub>/F\<^esub> P p Q,A" @@ -385,7 +383,7 @@ next qed (blast intro: hoarep.intros)+ -subsection {* Some Derived Rules *} +subsection \Some Derived Rules\ lemma Conseq': "\s. s \ P \ (\P' Q' A'. @@ -433,4 +431,4 @@ apply blast apply blast done -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/HoarePartialProps.thy b/tools/c-parser/Simpl/HoarePartialProps.thy index b493e6332..8536f000a 100644 --- a/tools/c-parser/Simpl/HoarePartialProps.thy +++ b/tools/c-parser/Simpl/HoarePartialProps.thy @@ -26,11 +26,11 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Properties of Partial Correctness Hoare Logic *} +section \Properties of Partial Correctness Hoare Logic\ theory HoarePartialProps imports HoarePartialDef begin -subsection {* Soundness *} +subsection \Soundness\ lemma hoare_cnvalid: assumes hoare: "\,\\\<^bsub>/F\<^esub> P c Q,A" @@ -411,7 +411,7 @@ qed theorem hoare_sound: "\,\\\<^bsub>/F\<^esub> P c Q,A \ \,\\\<^bsub>/F\<^esub> P c Q,A" by (iprover intro: cnvalid_to_cvalid hoare_cnvalid) -subsection {* Completeness *} +subsection \Completeness\ lemma MGT_valid: "\\\<^bsub>/F\<^esub>{s. s=Z \ \\\c,Normal s\ \\({Stuck} \ Fault ` (-F))} c @@ -426,8 +426,8 @@ proof (rule validI) by (cases t) (auto simp add: final_notin_def) qed -text {* The consequence rule where the existential @{term Z} is instantiated -to @{term s}. Usefull in proof of @{text "MGT_lemma"}.*} +text \The consequence rule where the existential @{term Z} is instantiated +to @{term s}. Usefull in proof of \MGT_lemma\.\ lemma ConseqMGT: assumes modif: "\Z. \,\ \\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)" assumes impl: "\s. s \ P \ s \ P' s \ (\t. t \ Q' s \ t \ Q) \ @@ -493,10 +493,10 @@ lemma MGT_implies_complete: apply (auto simp add: valid_def intro!: final_notinI) done -text {* Equipped only with the classic consequence rule @{thm "conseqPrePost"} +text \Equipped only with the classic consequence rule @{thm "conseqPrePost"} we can only derive this syntactically more involved version of completeness. But semantically it is equivalent to the "real" one - (see below) *} + (see below)\ lemma MGT_implies_complete': assumes MGT: "\Z. \,{}\\<^bsub>/F\<^esub> {s. s=Z \ \\\c,Normal s\ \\({Stuck} \ Fault ` (-F))} c @@ -512,7 +512,7 @@ lemma MGT_implies_complete': apply (fastforce simp add: valid_def) done -text {* Semantic equivalence of both kind of formulations *} +text \Semantic equivalence of both kind of formulations\ lemma valid_involved_to_valid: assumes valid: "\Z. \\\<^bsub>/F\<^esub> {s. s=Z \ s \ P} c {t. Z \ P \ t \ Q},{t. Z \ P \ t \ A}" @@ -526,10 +526,10 @@ lemma valid_involved_to_valid: apply fastforce done -text {* The sophisticated consequence rule allow us to do this +text \The sophisticated consequence rule allow us to do this semantical transformation on the hoare-level, too. The magic is, that it allow us to - choose the instance of @{term Z} under the assumption of an state @{term "s \ P"} *} + choose the instance of @{term Z} under the assumption of an state @{term "s \ P"}\ lemma assumes deriv: "\Z. \,{}\\<^bsub>/F\<^esub> {s. s=Z \ s \ P} c {t. Z \ P \ t \ Q},{t. Z \ P \ t \ A}" @@ -1068,9 +1068,9 @@ proof (rule hoare_complete) qed -subsection {* And Now: Some Useful Rules *} +subsection \And Now: Some Useful Rules\ -subsubsection {* Consequence *} +subsubsection \Consequence\ lemma LiberalConseq_sound: @@ -1334,7 +1334,7 @@ apply (rule LiberalConseq_noguards_nothrows apply auto done -subsubsection {* Modify Return *} +subsubsection \Modify Return\ lemma ProcModifyReturn_sound: assumes valid_call: "\n. \,\ \n:\<^bsub>/F\<^esub> P call init p return' c Q,A" @@ -1566,7 +1566,7 @@ using modifies_spec apply (blast intro: hoare_cnvalid) done -subsubsection {* DynCall *} +subsubsection \DynCall\ lemma dynProcModifyReturn_sound: assumes valid_call: "\n. \,\ \n:\<^bsub>/F\<^esub> P dynCall init p return' c Q,A" @@ -1825,7 +1825,7 @@ apply assumption done -subsubsection {* Conjunction of Postcondition *} +subsubsection \Conjunction of Postcondition\ lemma PostConjI_sound: assumes valid_Q: "\n. \,\ \n:\<^bsub>/F\<^esub> P c Q,A" @@ -1878,12 +1878,12 @@ proof (rule cnvalidI) show "t \ Normal ` (Q \ R) \ Abrupt ` (A \ X)" proof - from cnvalidD [OF validF [rule_format] ctxt exec P t_noFault] - have "t \ Normal ` Q \ Abrupt ` A". - moreover from this have "t \ Fault ` G" + have *: "t \ Normal ` Q \ Abrupt ` A". + then have "t \ Fault ` G" by auto from cnvalidD [OF validG [rule_format] ctxt' exec P' this] have "t \ Normal ` R \ Abrupt ` X" . - ultimately show ?thesis by auto + with * show ?thesis by auto qed qed @@ -1900,7 +1900,7 @@ using validF apply (blast intro:hoare_cnvalid) using validG apply (blast intro:hoare_cnvalid) done -subsubsection {* Weaken Context *} +subsubsection \Weaken Context\ lemma WeakenContext_sound: @@ -1934,7 +1934,7 @@ using deriv_ctxt apply (blast intro: hoare_cnvalid) done -subsubsection {* Guards and Guarantees *} +subsubsection \Guards and Guarantees\ lemma SplitGuards_sound: assumes valid_c1: "\n. \,\\n:\<^bsub>/F\<^esub> P c\<^sub>1 Q,A" @@ -2323,7 +2323,7 @@ apply (iprover intro: hoare_cnvalid [OF deriv]) done -subsubsection {* Restricting the Procedure Environment *} +subsubsection \Restricting the Procedure Environment\ lemma nvalid_restrict_to_nvalid: assumes valid_c: "\|\<^bsub>M\<^esub>\n:\<^bsub>/F\<^esub> P c Q,A" @@ -2396,4 +2396,4 @@ shows "\,{}\\<^bsub>/F'\<^esub> P c Q,A" apply (insert hoare_sound [OF deriv_c]) by (simp add: cvalid_def) -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/HoareTotal.thy b/tools/c-parser/Simpl/HoareTotal.thy index 42f3406bc..1a0391a9c 100644 --- a/tools/c-parser/Simpl/HoareTotal.thy +++ b/tools/c-parser/Simpl/HoareTotal.thy @@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Derived Hoare Rules for Total Correctness *} +section \Derived Hoare Rules for Total Correctness\ theory HoareTotal imports HoareTotalProps begin @@ -37,8 +37,8 @@ lemma conseq_no_aux: \,\\\<^sub>t\<^bsub>/F\<^esub> P c Q,A" by (rule conseq [where P'="\Z. P'" and Q'="\Z. Q'" and A'="\Z. A'"]) auto -text {* If for example a specification for a "procedure pointer" parameter -is in the precondition we can extract it with this rule *} +text \If for example a specification for a "procedure pointer" parameter +is in the precondition we can extract it with this rule\ lemma conseq_exploit_pre: "\\s \ P. \,\ \\<^sub>t\<^bsub>/F\<^esub> ({s} \ P) c Q,A\ \ @@ -387,8 +387,8 @@ qed lemma "\,\\\<^bsub>/F\<^esub> (P \ b) c Q,A \ \,\\\<^bsub>/F\<^esub> (P \ b) (Seq c (Guard f Q Skip)) Q,A" oops -text {* @{term "J"} will be instantiated by tactic with @{term "gs' \ I"} for - those guards that are not stripped.*} +text \@{term "J"} will be instantiated by tactic with @{term "gs' \ I"} for + those guards that are not stripped.\ lemma WhileAnnoG: "\,\\\<^sub>t\<^bsub>/F\<^esub> P (guards gs (whileAnno b J V (Seq c (guards gs Skip)))) Q,A @@ -396,7 +396,7 @@ lemma WhileAnnoG: \,\\\<^sub>t\<^bsub>/F\<^esub> P (whileAnnoG gs b I V c) Q,A" by (simp add: whileAnnoG_def whileAnno_def while_def) -text {* This form stems from @{term "strip_guards F (whileAnnoG gs b I V c)"} *} +text \This form stems from @{term "strip_guards F (whileAnnoG gs b I V c)"}\ lemma WhileNoGuard': assumes P_I: "P \ I" assumes deriv_body: "\\. \,\\\<^sub>t\<^bsub>/F\<^esub> ({\} \ I \ b) c ({t. (t, \) \ V} \ I),A" @@ -972,8 +972,8 @@ qed lemma ProcProcParModifyReturn: assumes q: "P \ {s. p s = q} \ P'" - --{* @{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in - @{term P'}, so the vcg can simplify it. *} + \\@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in + @{term P'}, so the vcg can simplify it.\ assumes to_prove: "\,\\\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" assumes ret_nrm_modif: "\s t. t \ (Modif (init s)) \ return' s t = return s t" @@ -997,8 +997,8 @@ qed lemma ProcProcParModifyReturnSameFaults: assumes q: "P \ {s. p s = q} \ P'" - --{* @{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in - @{term P'}, so the vcg can simplify it. *} + \\@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in + @{term P'}, so the vcg can simplify it.\ assumes to_prove: "\,\\\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" assumes ret_nrm_modif: "\s t. t \ (Modif (init s)) \ return' s t = return s t" @@ -1021,8 +1021,8 @@ qed lemma ProcProcParModifyReturnNoAbr: assumes q: "P \ {s. p s = q} \ P'" - --{* @{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as - first conjunction in @{term P'}, so the vcg can simplify it. *} + \\@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as + first conjunction in @{term P'}, so the vcg can simplify it.\ assumes to_prove: "\,\\\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" assumes ret_nrm_modif: "\s t. t \ (Modif (init s)) \ return' s t = return s t" @@ -1042,8 +1042,8 @@ qed lemma ProcProcParModifyReturnNoAbrSameFaults: assumes q: "P \ {s. p s = q} \ P'" - --{* @{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as - first conjunction in @{term P'}, so the vcg can simplify it. *} + \\@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as + first conjunction in @{term P'}, so the vcg can simplify it.\ assumes to_prove: "\,\\\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" assumes ret_nrm_modif: "\s t. t \ (Modif (init s)) \ return' s t = return s t" @@ -1149,16 +1149,16 @@ proof - by (rule E) qed -subsubsection {* Rules for Single-Step Proof \label{sec:hoare-isar} *} +subsubsection \Rules for Single-Step Proof \label{sec:hoare-isar}\ -text {* +text \ We are now ready to introduce a set of Hoare rules to be used in single-step structured proofs in Isabelle/Isar. \medskip Assertions of Hoare Logic may be manipulated in calculational proofs, with the inclusion expressed in terms of sets or predicates. Reversed order is supported as well. -*} +\ lemma annotateI [trans]: diff --git a/tools/c-parser/Simpl/HoareTotalDef.thy b/tools/c-parser/Simpl/HoareTotalDef.thy index 4dc50dc5b..c790d3b0d 100644 --- a/tools/c-parser/Simpl/HoareTotalDef.thy +++ b/tools/c-parser/Simpl/HoareTotalDef.thy @@ -26,11 +26,11 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Hoare Logic for Total Correctness *} +section \Hoare Logic for Total Correctness\ theory HoareTotalDef imports HoarePartialDef Termination begin -subsection {* Validity of Hoare Tuples: @{text "\\\<^sub>t\<^bsub>/F\<^esub> P c Q,A"} *} +subsection \Validity of Hoare Tuples: \\\\<^sub>t\<^bsub>/F\<^esub> P c Q,A\\ definition validt :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] \ bool" @@ -52,7 +52,7 @@ notation (ASCII) validt ("_|=t'/_/ _ _ _,_" [61,60,1000, 20, 1000,1000] 60) and cvalidt ("_,_|=t'/_ / _ _ _,_" [61,60,60,1000, 20, 1000,1000] 60) -subsection {* Properties of Validity *} +subsection \Properties of Validity\ lemma validtI: "\\s t. \\\\c,Normal s\ \ t;s \ P;t \ Fault ` F\ \ t \ Normal ` Q \ Abrupt ` A; @@ -87,7 +87,7 @@ lemma validt_augment_Faults: using valid F' by (auto intro: valid_augment_Faults simp add: validt_def) -subsection {* The Hoare Rules: @{text "\,\\\<^sub>t\<^bsub>/F\<^esub> P c Q,A" } *} +subsection \The Hoare Rules: \\,\\\<^sub>t\<^bsub>/F\<^esub> P c Q,A\\ inductive "hoaret"::"[('s,'p,'f) body,('s,'p) quadruple set,'f set, 's assn,('s,'p,'f) com,'s assn,'s assn] @@ -150,13 +150,13 @@ where \,\\\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" | ExFalso: "\\,\\\<^sub>t\<^bsub>/F\<^esub> P c Q,A; \ \\\<^sub>t\<^bsub>/F\<^esub> P c Q,A\ \ \,\\\<^sub>t\<^bsub>/F\<^esub> P c Q,A" - -- {* This is a hack rule that enables us to derive completeness for - an arbitrary context @{text "\"}, from completeness for an empty context.*} + \ \This is a hack rule that enables us to derive completeness for + an arbitrary context \\\, from completeness for an empty context.\ -text {* Does not work, because of rule ExFalso, the context @{text \} is to blame. +text \Does not work, because of rule ExFalso, the context \\\ is to blame. A weaker version with empty context can be derived from soundness - later on. *} + later on.\ lemma hoaret_to_hoarep: assumes hoaret: "\,\\\<^sub>t\<^bsub>/F\<^esub> P p Q,A" shows "\,\\\<^bsub>/F\<^esub> P p Q,A" @@ -302,7 +302,7 @@ next by (fastforce intro: hoaret.ExFalso simp add: cvalidt_def) qed (blast intro: hoaret.intros)+ -subsection {* Some Derived Rules *} +subsection \Some Derived Rules\ lemma Conseq': "\s. s \ P \ diff --git a/tools/c-parser/Simpl/HoareTotalProps.thy b/tools/c-parser/Simpl/HoareTotalProps.thy index 0556a2d6f..8a24db0cf 100644 --- a/tools/c-parser/Simpl/HoareTotalProps.thy +++ b/tools/c-parser/Simpl/HoareTotalProps.thy @@ -26,11 +26,11 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Properties of Total Correctness Hoare Logic *} +section \Properties of Total Correctness Hoare Logic\ theory HoareTotalProps imports SmallStep HoareTotalDef HoarePartialProps begin -subsection {* Soundness *} +subsection \Soundness\ lemma hoaret_sound: assumes hoare: "\,\\\<^sub>t\<^bsub>/F\<^esub> P c Q,A" @@ -621,7 +621,7 @@ proof - by (rule hoare_complete) qed -subsection {* Completeness *} +subsection \Completeness\ lemma MGT_valid: "\\\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \ \\\c,Normal s\ \\({Stuck} \ Fault ` (-F)) \ \\c\Normal s} c @@ -643,8 +643,8 @@ next by blast qed -text {* The consequence rule where the existential @{term Z} is instantiated -to @{term s}. Usefull in proof of @{text "MGT_lemma"}.*} +text \The consequence rule where the existential @{term Z} is instantiated +to @{term s}. Usefull in proof of \MGT_lemma\.\ lemma ConseqMGT: assumes modif: "\Z::'a. \,\ \\<^sub>t\<^bsub>/F\<^esub> (P' Z::'a assn) c (Q' Z),(A' Z)" assumes impl: "\s. s \ P \ s \ P' s \ (\t. t \ Q' s \ t \ Q) \ @@ -2009,10 +2009,10 @@ next qed -text {* To prove a procedure implementation correct it suffices to assume +text \To prove a procedure implementation correct it suffices to assume only the procedure specifications of procedures that actually occur during evaluation of the body. - *} +\ lemma Call_lemma: assumes A: @@ -2093,7 +2093,7 @@ lemma image_Un_conv: "f ` (\p\dom \. \Z. {x p Z}) = (\ by (auto iff: not_None_eq) -text {* Another proof of @{text MGT_Call}, maybe a little more readable *} +text \Another proof of \MGT_Call\, maybe a little more readable\ lemma "\p \ dom \. \Z. \,{} \\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \ \\\Call p,Normal s\ \\({Stuck} \ Fault ` (-F)) \ @@ -2105,15 +2105,15 @@ proof - { fix p Z \ assume defined: "p \ dom \" - def Specs == "(\p\dom \. \Z. + define Specs where "Specs = (\p\dom \. \Z. {({s. s=Z \ \\\Call p,Normal s\ \\({Stuck} \ Fault ` (-F)) \ \\Call p\Normal s}, p, {t. \\\Call p,Normal Z\ \ Normal t}, {t. \\\Call p,Normal Z\ \ Abrupt t})})" - def Specs_wf == "(\p \. (\(P,q,Q,A). - (P \ {s. ((s,q),\,p) \ termi_call_steps \}, q, Q, A)) ` Specs)" + define Specs_wf where "Specs_wf p \ = (\(P,q,Q,A). + (P \ {s. ((s,q),\,p) \ termi_call_steps \}, q, Q, A)) ` Specs" for p \ have "\,Specs_wf p \ \\<^sub>t\<^bsub>/F\<^esub>({\} \ {s. s = Z \ \\\the (\ p),Normal s\ \\({Stuck} \ Fault ` (-F)) \ @@ -2181,9 +2181,9 @@ next by (rule ExFalso) qed -subsection {* And Now: Some Useful Rules *} +subsection \And Now: Some Useful Rules\ -subsubsection {* Modify Return *} +subsubsection \Modify Return\ lemma ProcModifyReturn_sound: assumes valid_call: "\,\ \\<^sub>t\<^bsub>/F\<^esub> P call init p return' c Q,A" @@ -2481,7 +2481,7 @@ apply (blast intro: hoare_sound) done -subsubsection {* DynCall *} +subsubsection \DynCall\ lemma dynProcModifyReturn_sound: @@ -2823,7 +2823,7 @@ apply (rule hoare_sound [OF modif [rule_format]]) apply assumption done -subsubsection {* Conjunction of Postcondition *} +subsubsection \Conjunction of Postcondition\ lemma PostConjI_sound: assumes valid_Q: "\,\ \\<^sub>t\<^bsub>/F\<^esub> P c Q,A" @@ -2881,12 +2881,12 @@ proof (rule cvalidtI) show "t \ Normal ` (Q \ R) \ Abrupt ` (A \ X)" proof - from cvalidt_postD [OF validF [rule_format] ctxt exec P t_noFault] - have "t \ Normal ` Q \ Abrupt ` A". - moreover from this have "t \ Fault ` G" + have t: "t \ Normal ` Q \ Abrupt ` A". + then have "t \ Fault ` G" by auto from cvalidt_postD [OF validG [rule_format] ctxt' exec P' this] have "t \ Normal ` R \ Abrupt ` X" . - ultimately show ?thesis by auto + with t show ?thesis by auto qed next fix s @@ -2912,7 +2912,7 @@ using validG apply (blast intro:hoaret_sound) done -subsubsection {* Guards and Guarantees *} +subsubsection \Guards and Guarantees\ lemma SplitGuards_sound: assumes valid_c1: "\,\\\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,A" @@ -3391,7 +3391,7 @@ apply (rule NormalizeI_sound) apply (iprover intro: hoaret_sound [OF deriv]) done -subsubsection {* Restricting the Procedure Environment *} +subsubsection \Restricting the Procedure Environment\ lemma validt_restrict_to_validt: assumes validt_c: "\|\<^bsub>M\<^esub>\\<^sub>t\<^bsub>/F\<^esub> P c Q,A" @@ -3429,7 +3429,7 @@ shows "\,{}\\<^sub>t\<^bsub>/F\<^esub> P c Q,A" apply (insert hoaret_sound [OF deriv_c]) by (simp add: cvalidt_def) -subsubsection {* Miscellaneous *} +subsubsection \Miscellaneous\ lemma augment_Faults: assumes deriv_c: "\,{}\\<^sub>t\<^bsub>/F\<^esub> P c Q,A" diff --git a/tools/c-parser/Simpl/Language.thy b/tools/c-parser/Simpl/Language.thy index 707f84f5d..48a684fb3 100644 --- a/tools/c-parser/Simpl/Language.thy +++ b/tools/c-parser/Simpl/Language.thy @@ -26,15 +26,15 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* The Simpl Syntax *} +section \The Simpl Syntax\ theory Language imports "~~/src/HOL/Library/Old_Recdef" begin -subsection {* The Core Language *} +subsection \The Core Language\ -text {* We use a shallow embedding of boolean expressions as well as assertions +text \We use a shallow embedding of boolean expressions as well as assertions as sets of states. -*} +\ type_synonym 's bexp = "'s set" type_synonym 's assn = "'s set" @@ -57,7 +57,7 @@ datatype (dead 's, 'p, 'f) com = -subsection {* Derived Language Constructs *} +subsection \Derived Language Constructs\ definition raise:: "('s \ 's) \ ('s,'p,'f) com" where @@ -160,10 +160,10 @@ lemma snd_guaranteeStripPair: "snd (guaranteeStripPair f g) = g" by (simp add: guaranteeStripPair_def) -subsection {* Operations on Simpl-Syntax *} +subsection \Operations on Simpl-Syntax\ -subsubsection {* Normalisation of Sequential Composition: @{text "sequence"}, @{text "flatten"} and @{text "normalize"} *} +subsubsection \Normalisation of Sequential Composition: \sequence\, \flatten\ and \normalize\\ primrec flatten:: "('s,'p,'f) com \ ('s,'p,'f) com list" where @@ -425,8 +425,8 @@ lemma normalize_guards [simp]: "normalize (guards gs c) = guards gs (normalize c)" by (induct gs) auto -text {* Sequencial composition with guards in the body is not preserved by - normalize *} +text \Sequencial composition with guards in the body is not preserved by + normalize\ lemma normalize_while [simp]: "normalize (while gs b c) = guards gs (While b (sequence Seq (flatten (normalize c) @ flatten (guards gs Skip))))" @@ -452,7 +452,7 @@ lemmas normalize_simps = normalize_while normalize_whileAnno normalize_whileAnnoG normalize_specAnno -subsubsection {* Stripping Guards: @{text "strip_guards"} *} +subsubsection \Stripping Guards: \strip_guards\\ primrec strip_guards:: "'f set \ ('s,'p,'f) com \ ('s,'p,'f) com" where @@ -570,7 +570,7 @@ lemmas strip_guards_simps = strip_guards.simps strip_guards_raise strip_guards_while strip_guards_whileAnno strip_guards_whileAnnoG strip_guards_specAnno -subsubsection {* Marking Guards: @{text "mark_guards"} *} +subsubsection \Marking Guards: \mark_guards\\ primrec mark_guards:: "'f \ ('s,'p,'g) com \ ('s,'p,'f) com" where @@ -703,7 +703,7 @@ lemma dest_Guard_guaranteeStrip [simp]: "dest_Guard (guaranteeStrip f g c) = (f, lemmas dest_Guard_simps = dest_Guard.simps dest_Guard_guaranteeStrip -subsubsection {* Merging Guards: @{text merge_guards}*} +subsubsection \Merging Guards: \merge_guards\\ primrec merge_guards:: "('s,'p,'f) com \ ('s,'p,'f) com" where @@ -732,43 +732,43 @@ where "merge_guards (Catch c\<^sub>1 c\<^sub>2) = Catch (merge_guards c\<^sub>1) (merge_guards c\<^sub>2)" lemma merge_guards_res_Skip: "merge_guards c = Skip \ c = Skip" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_Basic: "merge_guards c = Basic f \ c = Basic f" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_Spec: "merge_guards c = Spec r \ c = Spec r" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_Seq: "merge_guards c = Seq c1 c2 \ \c1' c2'. c = Seq c1' c2' \ merge_guards c1' = c1 \ merge_guards c2' = c2" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_Cond: "merge_guards c = Cond b c1 c2 \ \c1' c2'. c = Cond b c1' c2' \ merge_guards c1' = c1 \ merge_guards c2' = c2" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_While: "merge_guards c = While b c' \ \c''. c = While b c'' \ merge_guards c'' = c'" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_Call: "merge_guards c = Call p \ c = Call p" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_DynCom: "merge_guards c = DynCom c' \ \c''. c = DynCom c'' \ (\s. (merge_guards (c'' s))) = c'" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_Throw: "merge_guards c = Throw \ c = Throw" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_Catch: "merge_guards c = Catch c1 c2 \ \c1' c2'. c = Catch c1' c2' \ merge_guards c1' = c1 \ merge_guards c2' = c2" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemma merge_guards_res_Guard: "merge_guards c = Guard f g c' \ \c'' f' g'. c = Guard f' g' c''" - by (cases c) (auto split: com.splits split_if_asm simp add: is_Guard_def Let_def) + by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def) lemmas merge_guards_res_simps = merge_guards_res_Skip merge_guards_res_Basic merge_guards_res_Spec merge_guards_res_Seq merge_guards_res_Cond @@ -836,9 +836,9 @@ lemma merge_guards_specAnno [simp]: specAnno P (\s. merge_guards (c undefined)) Q A" by (simp add: specAnno_def) -text {* @{term "merge_guards"} for guard-lists as in @{const guards}, @{const while} +text \@{term "merge_guards"} for guard-lists as in @{const guards}, @{const while} and @{const whileAnnoG} may have funny effects since the guard-list has to - be merged with the body statement too.*} + be merged with the body statement too.\ lemmas merge_guards_simps = merge_guards.simps merge_guards_raise merge_guards_condCatch merge_guards_bind merge_guards_bseq merge_guards_block @@ -876,7 +876,7 @@ where "nothrows Throw = False" | "nothrows (Catch c\<^sub>1 c\<^sub>2) = (nothrows c\<^sub>1 \ nothrows c\<^sub>2)" -subsubsection {* Intersecting Guards: @{text "c\<^sub>1 \\<^sub>g c\<^sub>2"}*} +subsubsection \Intersecting Guards: \c\<^sub>1 \\<^sub>g c\<^sub>2\\ inductive_set com_rel ::"(('s,'p,'f) com \ ('s,'p,'f) com) set" where @@ -991,28 +991,28 @@ lemma inter_guards_strip_eq: (strip_guards UNIV c = strip_guards UNIV c2)" apply (induct c1 c2 rule: inter_guards.induct) prefer 8 -apply (simp split: split_if_asm) +apply (simp split: if_split_asm) apply hypsubst apply simp apply (rule ext) apply (erule_tac x=s in allE, erule exE) apply (erule_tac x=s in allE) apply fastforce -apply (fastforce split: option.splits split_if_asm)+ +apply (fastforce split: option.splits if_split_asm)+ done lemma inter_guards_sym: "\c. (c1 \\<^sub>g c2) = Some c \ (c2 \\<^sub>g c1) = Some c" apply (induct c1 c2 rule: inter_guards.induct) apply (simp_all) prefer 7 -apply (simp split: split_if_asm add: not_None_eq) +apply (simp split: if_split_asm add: not_None_eq) apply (rule conjI) apply (clarsimp) apply (rule ext) apply (erule_tac x=s in allE)+ apply fastforce apply fastforce -apply (fastforce split: option.splits split_if_asm)+ +apply (fastforce split: option.splits if_split_asm)+ done @@ -1043,18 +1043,18 @@ lemma inter_guards_While: "(While cnd bdy1 \\<^sub>g c2) = Some c = (\bdy2 bdy. c2 =While cnd bdy2 \ (bdy1 \\<^sub>g bdy2) = Some bdy \ c=While cnd bdy)" - by (cases c2) (auto split: option.splits split_if_asm) + by (cases c2) (auto split: option.splits if_split_asm) lemma inter_guards_Call: "(Call p \\<^sub>g c2) = Some c = (c2=Call p \ c=Call p)" - by (cases c2) (auto split: split_if_asm) + by (cases c2) (auto split: if_split_asm) lemma inter_guards_DynCom: "(DynCom f1 \\<^sub>g c2) = Some c = (\f2. c2=DynCom f2 \ (\s. ((f1 s) \\<^sub>g (f2 s)) \ None) \ c=DynCom (\s. the ((f1 s) \\<^sub>g (f2 s))))" - by (cases c2) (auto split: split_if_asm) + by (cases c2) (auto split: if_split_asm) lemma inter_guards_Guard: @@ -1079,7 +1079,7 @@ lemmas inter_guards_simps = inter_guards_Skip inter_guards_Basic inter_guards_Sp inter_guards_DynCom inter_guards_Guard inter_guards_Throw inter_guards_Catch -subsubsection {* Subset on Guards: @{text "c\<^sub>1 \\<^sub>g c\<^sub>2"} *} +subsubsection \Subset on Guards: \c\<^sub>1 \\<^sub>g c\<^sub>2\\ consts subseteq_guards:: "('s,'p,'f) com \ ('s,'p,'f) com \ bool" @@ -1145,7 +1145,7 @@ lemma subseteq_guards_DynCom: lemma subseteq_guards_Guard: "c \\<^sub>g Guard f g c' \ (c \\<^sub>g c') \ (\c''. c=Guard f g c'' \ (c'' \\<^sub>g c'))" - by (cases c) (auto split: split_if_asm) + by (cases c) (auto split: if_split_asm) lemma subseteq_guards_Throw: "c \\<^sub>g Throw \ c = Throw" diff --git a/tools/c-parser/Simpl/ROOT b/tools/c-parser/Simpl/ROOT index 118304456..c4e3736c6 100644 --- a/tools/c-parser/Simpl/ROOT +++ b/tools/c-parser/Simpl/ROOT @@ -1,6 +1,7 @@ chapter AFP session Simpl (AFP) = HOL + + options [timeout = 600] theories Simpl document_files diff --git a/tools/c-parser/Simpl/Semantic.thy b/tools/c-parser/Simpl/Semantic.thy index 9ba2c9017..94de119f6 100644 --- a/tools/c-parser/Simpl/Semantic.thy +++ b/tools/c-parser/Simpl/Semantic.thy @@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Big-Step Semantics for Simpl *} +section \Big-Step Semantics for Simpl\ theory Semantic imports Language begin notation @@ -69,10 +69,10 @@ lemma not_isFault_iff: "(\ isFault t) = (\f. t \ Fault f)" by (auto elim: isFaultE) (* ************************************************************************* *) -subsection {* Big-Step Execution: @{text "\\\c, s\ \ t"} *} +subsection \Big-Step Execution: \\\\c, s\ \ t\\ (* ************************************************************************* *) -text {* The procedure environment *} +text \The procedure environment\ type_synonym ('s,'p,'f) body = "'p \ ('s,'p,'f) com option" inductive @@ -444,7 +444,7 @@ lemma exec_assoc: "\\\Seq c1 (Seq c2 c3),s\ \< (* ************************************************************************* *) -subsection {* Big-Step Execution with Recursion Limit: @{text "\\\c, s\ =n\ t"} *} +subsection \Big-Step Execution with Recursion Limit: \\\\c, s\ =n\ t\\ (* ************************************************************************* *) inductive "execn"::"[('s,'p,'f) body,('s,'p,'f) com,('s,'f) xstate,nat,('s,'f) xstate] @@ -1197,8 +1197,8 @@ by (auto simp add: final_notin_def intro: exec_Seq') (* ************************************************************************* *) -subsection {* Lemmas about @{const "sequence"}, @{const "flatten"} and - @{const "normalize"} *} +subsection \Lemmas about @{const "sequence"}, @{const "flatten"} and + @{const "normalize"}\ (* ************************************************************************ *) lemma execn_sequence_app: "\s s' t. @@ -1547,7 +1547,7 @@ lemma exec_normalize_iff_exec: by (auto intro: exec_to_exec_normalize exec_normalize_to_exec) (* ************************************************************************* *) -subsection {* Lemmas about @{term "c\<^sub>1 \\<^sub>g c\<^sub>2"} *} +subsection \Lemmas about @{term "c\<^sub>1 \\<^sub>g c\<^sub>2"}\ (* ************************************************************************ *) lemma execn_to_execn_subseteq_guards: "\c s t n. \c \\<^sub>g c'; \\\c,s\ =n\ t\ @@ -1953,7 +1953,7 @@ qed (* ************************************************************************* *) -subsection {* Lemmas about @{const "merge_guards"} *} +subsection \Lemmas about @{const "merge_guards"}\ (* ************************************************************************ *) @@ -2106,7 +2106,7 @@ next proof (cases "s \ g") case False with exec_merge have "t=Fault f" - by (auto split: com.splits split_if_asm elim: execn_Normal_elim_cases + by (auto split: com.splits if_split_asm elim: execn_Normal_elim_cases simp add: Let_def is_Guard_def) with False show ?thesis by (auto intro: execn.intros) @@ -2210,7 +2210,7 @@ corollary exec_merge_guards_to_exec: by (rule iffD2 [OF exec_iff_exec_merge_guards]) (* ************************************************************************* *) -subsection {* Lemmas about @{const "mark_guards"} *} +subsection \Lemmas about @{const "mark_guards"}\ (* ************************************************************************ *) lemma execn_to_execn_mark_guards: @@ -2863,7 +2863,7 @@ proof - qed (* ************************************************************************* *) -subsection {* Lemmas about @{const "strip_guards"} *} +subsection \Lemmas about @{const "strip_guards"}\ (* ************************************************************************* *) lemma execn_to_execn_strip_guards: @@ -3767,7 +3767,7 @@ proof - qed (* ************************************************************************* *) -subsection {* Lemmas about @{term "c\<^sub>1 \\<^sub>g c\<^sub>2"} *} +subsection \Lemmas about @{term "c\<^sub>1 \\<^sub>g c\<^sub>2"}\ (* ************************************************************************* *) lemma inter_guards_execn_Normal_noFault: @@ -4377,7 +4377,7 @@ subsection "Restriction of Procedure Environment" (* ************************************************************************* *) lemma restrict_SomeD: "(m|\<^bsub>A\<^esub>) x = Some y \ m x = Some y" - by (auto simp add: restrict_map_def split: split_if_asm) + by (auto simp add: restrict_map_def split: if_split_asm) (* FIXME: To Map *) lemma restrict_dom_same [simp]: "m|\<^bsub>dom m\<^esub> = m" @@ -4408,7 +4408,7 @@ using exec_restrict notStuck by (induct) (auto intro: execn.intros dest: restrict_SomeD execn_Stuck_end) lemma restrict_NoneD: "m x = None \ (m|\<^bsub>A\<^esub>) x = None" - by (auto simp add: restrict_map_def split: split_if_asm) + by (auto simp add: restrict_map_def split: if_split_asm) lemma execn_to_execn_restrict: assumes execn: "\\\c,s\ =n\ t" diff --git a/tools/c-parser/Simpl/Simpl.thy b/tools/c-parser/Simpl/Simpl.thy index bf54f78b8..18c160242 100644 --- a/tools/c-parser/Simpl/Simpl.thy +++ b/tools/c-parser/Simpl/Simpl.thy @@ -6,7 +6,7 @@ (* Title: Simpl.thy Author: Norbert Schirmer, TU Muenchen -Copyright (C) 2008 Norbert Schirmer +Copyright (C) 2008 Norbert Schirmer Some rights reserved, TU Muenchen This library is free software; you can redistribute it and/or modify @@ -27,19 +27,19 @@ USA (*<*) theory Simpl imports - StateSpace - AlternativeSmallStep - SyntaxTest - "ex/VcgEx" - "ex/VcgExSP" - "ex/VcgExTotal" - "ex/Quicksort" - "ex/XVcgEx" - "ex/ProcParEx" - "ex/ProcParExSP" - "ex/ClosureEx" - "ex/ComposeEx" - "UserGuide" + StateSpace + AlternativeSmallStep + SyntaxTest + "ex/VcgEx" + "ex/VcgExSP" + "ex/VcgExTotal" + "ex/Quicksort" + "ex/XVcgEx" + "ex/ProcParEx" + "ex/ProcParExSP" + "ex/ClosureEx" + "ex/ComposeEx" + "UserGuide" begin end -(*>*) \ No newline at end of file +(*>*) diff --git a/tools/c-parser/Simpl/Simpl_Heap.thy b/tools/c-parser/Simpl/Simpl_Heap.thy index 2862d602f..ad9cc2e52 100644 --- a/tools/c-parser/Simpl/Simpl_Heap.thy +++ b/tools/c-parser/Simpl/Simpl_Heap.thy @@ -92,13 +92,13 @@ consts Null :: ref definition new :: "ref set \ ref" where "new A = (SOME a. a \ {Null} \ A)" -text {* +text \ Constant @{const "Null"} can be defined later on. Conceptually - @{const "Null"} and @{const "new"} are @{text "fixes"} of a locale + @{const "Null"} and @{const "new"} are \fixes\ of a locale with @{prop "finite A \ new A \ A \ {Null}"}. But since definitions relative to a locale do not yet work in Isabelle2005 we use this workaround to avoid lots of parameters in definitions. -*} +\ lemma new_notin [simp,intro]: "finite A \ new (A) \ A" diff --git a/tools/c-parser/Simpl/SmallStep.thy b/tools/c-parser/Simpl/SmallStep.thy index aa8057f82..45044763f 100644 --- a/tools/c-parser/Simpl/SmallStep.thy +++ b/tools/c-parser/Simpl/SmallStep.thy @@ -26,14 +26,14 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Small-Step Semantics and Infinite Computations*} +section \Small-Step Semantics and Infinite Computations\ theory SmallStep imports Termination begin -text {* The redex of a statement is the substatement, which is actually altered +text \The redex of a statement is the substatement, which is actually altered by the next step in the small-step semantics. -*} +\ primrec redex:: "('s,'p,'f)com \ ('s,'p,'f)com" where @@ -50,7 +50,7 @@ where "redex (Catch c\<^sub>1 c\<^sub>2) = redex c\<^sub>1" -subsection {*Small-Step Computation: @{text "\\(c, s) \ (c', s')"}*} +subsection \Small-Step Computation: \\\(c, s) \ (c', s')\\ type_synonym ('s,'p,'f) config = "('s,'p,'f)com \ ('s,'f) xstate" inductive "step"::"[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] \ bool" @@ -138,12 +138,12 @@ inductive_cases step_Normal_elim_cases [cases set]: "\\(Catch c1 c2,Normal s) \ u" -text {* The final configuration is either of the form @{text "(Skip,_)"} for normal +text \The final configuration is either of the form \(Skip,_)\ for normal termination, or @{term "(Throw,Normal s)"} in case the program was started in a @{term "Normal"} state and terminated abruptly. The @{const "Abrupt"} state is not used to model abrupt termination, in contrast to the big-step semantics. Only if the program starts in an @{const "Abrupt"} states it ends in the same @{term "Abrupt"} -state.*} +state.\ definition final:: "('s,'p,'f) config \ bool" where "final cfg = (fst cfg=Skip \ (fst cfg=Throw \ (\s. snd cfg=Normal s)))" @@ -168,7 +168,7 @@ abbreviation (* ************************************************************************ *) -subsection {* Structural Properties of Small Step Computations *} +subsection \Structural Properties of Small Step Computations\ (* ************************************************************************ *) lemma redex_not_Seq: "redex c = Seq c1 c2 \ P" @@ -377,7 +377,7 @@ next qed (* ************************************************************************ *) -subsection {* Equivalence between Small-Step and Big-Step Semantics *} +subsection \Equivalence between Small-Step and Big-Step Semantics\ (* ************************************************************************ *) theorem exec_impl_steps: @@ -967,7 +967,7 @@ next qed (* ************************************************************************ *) -subsection {* Infinite Computations: @{text "\\(c, s) \ \(\)"}*} +subsection \Infinite Computations: \\\(c, s) \ \(\)\\ (* ************************************************************************ *) definition inf:: "('s,'p,'f) body \ ('s,'p,'f) config \ bool" @@ -979,7 +979,7 @@ lemma not_infI: "\\f. \f 0 = cfg; \i. \\Equivalence between Termination and the Absence of Infinite Computations\ (* ************************************************************************ *) @@ -1092,12 +1092,12 @@ next by (blast dest: step_preserves_termination) qed -ML {* +ML \ ML_Thms.bind_thm ("tranclp_induct2", Split_Rule.split_rule @{context} (Rule_Insts.read_instantiate @{context} [((("a", 0), Position.none), "(aa,ab)"), ((("b", 0), Position.none), "(ba,bb)")] [] @{thm tranclp_induct})); -*} +\ lemma steps_preserves_termination': assumes steps: "\\(c,s) \\<^sup>+ (c',s')" @@ -1278,7 +1278,7 @@ proof - show ?thesis proof (cases "\i. final (head (f i))") case True - def k\"(LEAST i. final (head (f i)))" + define k where "k = (LEAST i. final (head (f i)))" have less_k: "\i final (head (f i))" apply (intro allI impI) apply (unfold k_def) @@ -1326,7 +1326,7 @@ proof - obtain "\\(Seq Skip c\<^sub>2,s') \ (c\<^sub>2,s')" and f_Suc_k: "f (k + 1) = (c\<^sub>2,s')" by (fastforce elim: step.cases intro: step.intros) - def g\"\i. f (i + (k + 1))" + define g where "g i = f (i + (k + 1))" for i from f_Suc_k have g_0: "g 0 = (c\<^sub>2,s')" by (simp add: g_def) @@ -1347,7 +1347,7 @@ proof - obtain "\\(Seq Throw c\<^sub>2,s') \ (Throw,s')" and f_Suc_k: "f (k + 1) = (Throw,s')" by (fastforce elim: step_elim_cases intro: step.intros) - def g\"\i. f (i + (k + 1))" + define g where "g i = f (i + (k + 1))" for i from f_Suc_k have g_0: "g 0 = (Throw,s')" by (simp add: g_def) @@ -1398,7 +1398,7 @@ proof - show ?thesis proof (cases "\i. final (head (f i))") case True - def k\"(LEAST i. final (head (f i)))" + define k where "k = (LEAST i. final (head (f i)))" have less_k: "\i final (head (f i))" apply (intro allI impI) apply (unfold k_def) @@ -1463,7 +1463,7 @@ proof - obtain "\\(Catch Throw c\<^sub>2,s') \ (c\<^sub>2,s')" and f_Suc_k: "f (k + 1) = (c\<^sub>2,s')" by (fastforce elim: step_elim_cases intro: step.intros) - def g\"\i. f (i + (k + 1))" + define g where "g i = f (i + (k + 1))" for i from f_Suc_k have g_0: "g 0 = (c\<^sub>2,s')" by (simp add: g_def) @@ -2161,12 +2161,12 @@ next finally show ?case . qed -ML {* +ML \ ML_Thms.bind_thm ("trancl_induct2", Split_Rule.split_rule @{context} (Rule_Insts.read_instantiate @{context} [((("a", 0), Position.none), "(aa, ab)"), ((("b", 0), Position.none), "(ba, bb)")] [] @{thm trancl_induct})); -*} +\ lemma steps_redex': assumes steps: "\\ (r, s) \\<^sup>+ (r', s')" @@ -2310,8 +2310,8 @@ proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain, \\Call p \ Normal s \ (\c. \\ (Call p, Normal s) \\<^sup>+ (c, Normal t) \ redex c = Call q)) (f (Suc i)) (f i)" - def s\"\i::nat. fst (f i)" - def p\"\i::nat. snd (f i)::'b" + define s where "s i = fst (f i)" for i :: nat + define p where "p i = (snd (f i)::'b)" for i :: nat from inf have inf': "\i. \\Call (p i) \ Normal (s i) \ (\c. \\ (Call (p i), Normal (s i)) \\<^sup>+ (c, Normal (s (i+1))) \ @@ -2335,7 +2335,7 @@ proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain, steps_c: "\i. \\ (Call (p i), Normal (s i)) \\<^sup>+ (c i, Normal (s (i+1)))" and red_c: "\i. redex (c i) = Call (p (i+1))" by auto - def g\"\i. (seq c (p 0) i,Normal (s i)::('a,'c) xstate)" + define g where "g i = (seq c (p 0) i,Normal (s i)::('a,'c) xstate)" for i from red_c [rule_format, of 0] have "g 0 = (Call (p 0), Normal (s 0))" by (simp add: g_def) @@ -2783,14 +2783,14 @@ corollary terminates_iff_no_infinite_computation: done (* ************************************************************************* *) -subsection {* Generalised Redexes *} +subsection \Generalised Redexes\ (* ************************************************************************* *) -text {* +text \ For an important lemma for the completeness proof of the Hoare-logic for total correctness we need a generalisation of @{const "redex"} that not only yield the redex itself but all the enclosing statements as well. -*} +\ primrec redexes:: "('s,'p,'f)com \ ('s,'p,'f)com set" where @@ -3117,4 +3117,4 @@ using termi by induct (auto intro: terminates.intros) -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/StateSpace.thy b/tools/c-parser/Simpl/StateSpace.thy index c8dabe1f9..e6a664102 100644 --- a/tools/c-parser/Simpl/StateSpace.thy +++ b/tools/c-parser/Simpl/StateSpace.thy @@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* State Space Template *} +section \State Space Template\ theory StateSpace imports Hoare begin @@ -43,4 +43,4 @@ record ('g, 'n, 'val) stateSP = "'g state" + lemma upd_globals_conv: "upd_globals f = (\s. s\globals := f (globals s)\)" by (rule ext) (simp add: upd_globals_def) -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/SyntaxTest.thy b/tools/c-parser/Simpl/SyntaxTest.thy index 7f2efbb0d..5b00c996d 100644 --- a/tools/c-parser/Simpl/SyntaxTest.thy +++ b/tools/c-parser/Simpl/SyntaxTest.thy @@ -94,4 +94,4 @@ end end -(*>*) \ No newline at end of file +(*>*) diff --git a/tools/c-parser/Simpl/Termination.thy b/tools/c-parser/Simpl/Termination.thy index cb0a0963c..a540e59ae 100644 --- a/tools/c-parser/Simpl/Termination.thy +++ b/tools/c-parser/Simpl/Termination.thy @@ -25,11 +25,11 @@ License along with this library; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Terminating Programs *} +section \Terminating Programs\ theory Termination imports Semantic begin -subsection {* Inductive Characterisation: @{text "\\c\s"}*} +subsection \Inductive Characterisation: \\\c\s\\ inductive "terminates"::"('s,'p,'f) body \ ('s,'p,'f) com \ ('s,'f) xstate \ bool" ("_\_ \ _" [60,20,60] 89) @@ -311,8 +311,8 @@ done (* ************************************************************************* *) -subsection {* Lemmas about @{const "sequence"}, @{const "flatten"} and - @{const "normalize"} *} +subsection \Lemmas about @{const "sequence"}, @{const "flatten"} and + @{const "normalize"}\ (* ************************************************************************ *) lemma terminates_sequence_app: @@ -630,7 +630,7 @@ lemma terminates_iff_terminates_normalize: terminates_normalize_to_terminates) (* ************************************************************************* *) -subsection {* Lemmas about @{const "strip_guards"} *} +subsection \Lemmas about @{const "strip_guards"}\ (* ************************************************************************* *) lemma terminates_strip_guards_to_terminates: "\s. \\strip_guards F c\s \ \\c\s" @@ -722,8 +722,8 @@ next proof (induct) case (WhileTrue s b' c') have eqs: "While b' c' = While b (strip_guards F c)" by fact - with `s\b'` have b: "s\b" by simp - from eqs `\\c' \ Normal s` have "\\strip_guards F c \ Normal s" + with \s\b'\ have b: "s\b" by simp + from eqs \\\c' \ Normal s\ have "\\strip_guards F c \ Normal s" by simp hence term_c: "\\c \ Normal s" by (rule hyp_c) @@ -770,7 +770,7 @@ next case Guard thus ?case by (cases s) (auto elim: terminates_Normal_elim_cases intro: terminates.intros - split: split_if_asm) + split: if_split_asm) next case Throw thus ?case by simp next @@ -876,7 +876,7 @@ next qed (auto intro: terminates.intros) (* ************************************************************************* *) -subsection {* Lemmas about @{term "c\<^sub>1 \\<^sub>g c\<^sub>2"} *} +subsection \Lemmas about @{term "c\<^sub>1 \\<^sub>g c\<^sub>2"}\ (* ************************************************************************* *) lemma inter_guards_terminates: @@ -1131,7 +1131,7 @@ proof - qed (* ************************************************************************* *) -subsection {* Lemmas about @{const "mark_guards"} *} +subsection \Lemmas about @{const "mark_guards"}\ (* ************************************************************************ *) lemma terminates_to_terminates_mark_guards: @@ -1383,7 +1383,7 @@ lemma terminates_mark_guards_to_terminates: (* ************************************************************************* *) -subsection {* Lemmas about @{const "merge_guards"} *} +subsection \Lemmas about @{const "merge_guards"}\ (* ************************************************************************ *) lemma terminates_to_terminates_merge_guards: @@ -1428,7 +1428,7 @@ next have "s \ g" by fact thus ?case by (cases "merge_guards c") - (auto intro: terminates.intros split: split_if_asm simp add: Let_def) + (auto intro: terminates.intros split: if_split_asm simp add: Let_def) qed (fastforce intro: terminates.intros dest: exec_merge_guards_to_exec)+ lemma terminates_merge_guards_to_terminates_Normal: @@ -1573,7 +1573,7 @@ theorem terminates_iff_terminates_merge_guards: terminates_merge_guards_to_terminates) (* ************************************************************************* *) -subsection {* Lemmas about @{term "c\<^sub>1 \\<^sub>g c\<^sub>2"} *} +subsection \Lemmas about @{term "c\<^sub>1 \\<^sub>g c\<^sub>2"}\ (* ************************************************************************ *) lemma terminates_fewer_guards_Normal: @@ -1916,12 +1916,11 @@ next next case False with exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1 - have "\\\c1,Normal s \ \ s'" + have *: "\\\c1,Normal s \ \ s'" by (auto simp add: final_notin_def elim!: isFaultE) - moreover - from this noFault_Seq have "\\\c2,s' \ \\Fault ` F" + with noFault_Seq have "\\\c2,s' \ \\Fault ` F" by (auto simp add: final_notin_def intro: exec.intros) - ultimately show ?thesis + with * show ?thesis using Seq.hyps by simp qed } @@ -1951,12 +1950,11 @@ next next case False with exec_strip_guards_to_exec [OF exec_strip_guards_c] noFault_c - have "\\\c,Normal s \ \ s'" + have *: "\\\c,Normal s \ \ s'" by (auto simp add: final_notin_def elim!: isFaultE) - moreover - from this s_in_b noFault_while have "\\\While b c,s' \ \\Fault ` F" + with s_in_b noFault_while have "\\\While b c,s' \ \\Fault ` F" by (auto simp add: final_notin_def intro: exec.intros) - ultimately show ?thesis + with * show ?thesis using WhileTrue.hyps by simp qed } @@ -1990,12 +1988,11 @@ next have "\\strip_guards F c2 \ Normal s'" proof - from exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1 - have "\\\c1,Normal s \ \ Abrupt s'" + have *: "\\\c1,Normal s \ \ Abrupt s'" by (auto simp add: final_notin_def elim!: isFaultE) - moreover - from this noFault_Catch have "\\\c2,Normal s' \ \\Fault ` F" + with noFault_Catch have "\\\c2,Normal s' \ \\Fault ` F" by (auto simp add: final_notin_def intro: exec.intros) - ultimately show ?thesis + with * show ?thesis using Catch.hyps by simp qed } @@ -2004,7 +2001,7 @@ next qed (* ************************************************************************* *) -subsection {* Lemmas about @{const "strip_guards"} *} +subsection \Lemmas about @{const "strip_guards"}\ (* ************************************************************************* *) lemma terminates_noFault_strip: @@ -2048,12 +2045,11 @@ next next case False with exec_strip_to_exec [OF exec_strip_c1] noFault_c1 - have "\\\c1,Normal s \ \ s'" + have *: "\\\c1,Normal s \ \ s'" by (auto simp add: final_notin_def elim!: isFaultE) - moreover - from this noFault_Seq have "\\\c2,s' \ \\Fault ` F" + with noFault_Seq have "\\\c2,s' \ \\Fault ` F" by (auto simp add: final_notin_def intro: exec.intros) - ultimately show ?thesis + with * show ?thesis using Seq.hyps by (simp del: strip_simp) qed } @@ -2083,12 +2079,11 @@ next next case False with exec_strip_to_exec [OF exec_strip_c] noFault_c - have "\\\c,Normal s \ \ s'" + have *: "\\\c,Normal s \ \ s'" by (auto simp add: final_notin_def elim!: isFaultE) - moreover - from this s_in_b noFault_while have "\\\While b c,s' \ \\Fault ` F" + with s_in_b noFault_while have "\\\While b c,s' \ \\Fault ` F" by (auto simp add: final_notin_def intro: exec.intros) - ultimately show ?thesis + with * show ?thesis using WhileTrue.hyps by (simp del: strip_simp) qed } @@ -2134,12 +2129,11 @@ next have "strip F \\c2 \ Normal s'" proof - from exec_strip_to_exec [OF exec_strip_c1] noFault_c1 - have "\\\c1,Normal s \ \ Abrupt s'" + have *: "\\\c1,Normal s \ \ Abrupt s'" by (auto simp add: final_notin_def elim!: isFaultE) - moreover - from this noFault_Catch have "\\\c2,Normal s' \ \\Fault ` F" + with * noFault_Catch have "\\\c2,Normal s' \ \\Fault ` F" by (auto simp add: final_notin_def intro: exec.intros) - ultimately show ?thesis + with * show ?thesis using Catch.hyps by (simp del: strip_simp) qed } @@ -2149,7 +2143,7 @@ qed (* ************************************************************************* *) -subsection {* Miscellaneous *} +subsection \Miscellaneous\ (* ************************************************************************* *) lemma terminates_while_lemma: @@ -2337,4 +2331,4 @@ next qed qed -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/UserGuide.thy b/tools/c-parser/Simpl/UserGuide.thy index 2478ba7cb..c7539c872 100644 --- a/tools/c-parser/Simpl/UserGuide.thy +++ b/tools/c-parser/Simpl/UserGuide.thy @@ -25,7 +25,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* User Guide \label{sec:UserGuide}*} +section \User Guide \label{sec:UserGuide}\ (*<*) theory UserGuide imports HeapList Vcg @@ -40,16 +40,16 @@ syntax -text {* +text \ We introduce the verification environment with a couple of examples that illustrate how to use the different bits and pieces to verify programs. -*} +\ -subsection {* Basics *} +subsection \Basics\ -text {* +text \ First of all we have to decide how to represent the state space. There are currently two implementations. One is based on records the other @@ -69,7 +69,7 @@ In this user guide we prefer statespaces, but give some comments on the usage of records in Section \ref{sec:records}. -*} +\ hoarestate vars = A :: nat @@ -79,13 +79,13 @@ hoarestate vars = R :: nat S :: nat -text (in vars) {* The command \isacommand{hoarestate} is a simple preprocessor +text (in vars) \The command \isacommand{hoarestate} is a simple preprocessor for the command \isacommand{statespaces} which decorates the state -components with the suffix @{text "_'"}, to avoid cluttering the +components with the suffix \_'\, to avoid cluttering the namespace. Also note that underscores are printed as hyphens in this documentation. So what you see as @{term "A_'"} in this document is actually \texttt{A\_'}. Every component name becomes a fixed variable in -the locale @{text vars} and can no longer be used for logical +the locale \vars\ and can no longer be used for logical variables. Lookup of a component @{term "A_'"} in a state @{term "s"} is written as @@ -93,83 +93,83 @@ Lookup of a component @{term "A_'"} in a state @{term "s"} is written as To deal with local and global variables in the context of procedures the program state is organised as a record containing the two componets @{const "locals"} -and @{const "globals"}. The variables defined in hoarestate @{text "vars"} reside +and @{const "globals"}. The variables defined in hoarestate \vars\ reside in the @{const "locals"} part. -*} +\ -text {* +text \ Here is a first example. -*} +\ lemma (in vars) "\\ \\N = 5\ \N :== 2 * \N \\N = 10\" apply vcg - txt {* @{subgoals} *} + txt \@{subgoals}\ apply simp - txt {* @{subgoals} *} + txt \@{subgoals}\ done -text {* We enable the locale of statespace @{text vars} by the +text \We enable the locale of statespace \vars\ by the \texttt{in vars} directive. The verification condition generator is -invoked via the @{text vcg} method and leaves us with the expected -subgoal that can be proved by simplification. *} +invoked via the \vcg\ method and leaves us with the expected +subgoal that can be proved by simplification.\ -text (in vars) {* +text (in vars) \ If we refer to components (variables) of the state-space of the program - we always mark these with @{text "\"} (in assertions and also in the + we always mark these with \\\ (in assertions and also in the program itself). It is the acute-symbol and is present on most keyboards. The assertions of the Hoare tuple are ordinary Isabelle sets. As we usually want to refer to the state space in the assertions, we provide special brackets for them. They can be written - as {\verb+{| |}+} in ASCII or @{text "\ \"} with symbols. Internally, + as {\verb+{| |}+} in ASCII or \\ \\ with symbols. Internally, marking variables has two effects. First of all we refer to the implicit - state and secondary we get rid of the suffix @{text "_'"}. + state and secondary we get rid of the suffix \_'\. So the assertion @{term "{|\N = 5|}"} internally gets expanded to - @{text "{s. locals s \N_' = 5}"} written in ordinary set comprehension notation of - Isabelle. It describes the set of states where the @{text "N_'"} component - is equal to @{text "5"}. + \{s. locals s \N_' = 5}\ written in ordinary set comprehension notation of + Isabelle. It describes the set of states where the \N_'\ component + is equal to \5\. An empty context and an empty postcondition for abrupt termination can be omitted. The lemma above is a shorthand for - @{text "\,{}\ \\N = 5\ \N :== 2 * \N \\N = 10\,{}"}. -*} + \\,{}\ \\N = 5\ \N :== 2 * \N \\N = 10\,{}\. +\ -text {* We can step through verification condition generation by the -method @{text vcg_step}. -*} +text \We can step through verification condition generation by the +method \vcg_step\. +\ lemma (in vars) "\,{}\ \\N = 5\ \N :== 2 * \N \\N = 10\" apply vcg_step - txt {* @{subgoals} *} - txt {* The last step of verification condition generation, + txt \@{subgoals}\ + txt \The last step of verification condition generation, transforms the inclusion of state sets to the corresponding predicate on components of the state space. - *} +\ apply vcg_step - txt {* @{subgoals} *} + txt \@{subgoals}\ by simp -text {* +text \ Although our assertions work semantically on the state space, stepping through verification condition generation ``feels'' like the expected syntactic substitutions of traditional Hoare logic. This is achieved by light simplification on the assertions calculated by the Hoare rules. -*} +\ lemma (in vars) "\\ \\N = 5\ \N :== 2 * \N \\N = 10\" apply (rule HoarePartial.Basic) - txt {* @{subgoals} *} + txt \@{subgoals}\ apply (simp only: mem_Collect_eq) - txt {* @{subgoals} *} + txt \@{subgoals}\ apply (tactic - {* Hoare.BasicSimpTac @{context} Hoare.Function false - [] (K all_tac) 1*}) - txt {* @{subgoals} *} + \Hoare.BasicSimpTac @{context} Hoare.Function false + [] (K all_tac) 1\) + txt \@{subgoals}\ by simp -text {* The next example shows how we deal with the while loop. Note the +text \The next example shows how we deal with the while loop. Note the invariant annotation. -*} +\ lemma (in vars) "\,{}\ \\M = 0 \ \S = 0\ @@ -178,24 +178,24 @@ lemma (in vars) DO \S :== \S + b;; \M :== \M + 1 OD \\S = a * b\" apply vcg - txt {* @{subgoals [display]} *} - txt {* The verification condition generator gives us three proof obligations, + txt \@{subgoals [display]}\ + txt \The verification condition generator gives us three proof obligations, stemming from the path from the precondition to the invariant, from the invariant together with loop condition through the loop body to the invariant, and finally from the invariant together - with the negated loop condition to the postcondition.*} + with the negated loop condition to the postcondition.\ apply auto done -subsection {* Procedures *} +subsection \Procedures\ -subsubsection {* Declaration *} +subsubsection \Declaration\ -text {* +text \ Our first procedure is a simple square procedure. We provide the command \isacommand{procedures}, to declare and define a procedure. -*} +\ procedures Square (N::nat|R::nat) @@ -204,28 +204,28 @@ procedures -text {* A procedure is given by the signature of the procedure +text \A procedure is given by the signature of the procedure followed by the procedure body. The signature consists of the name of the procedure and a list of parameters together with their types. The -parameters in front of the pipe @{text "|"} are value parameters and +parameters in front of the pipe \|\ are value parameters and behind the pipe are the result parameters. Value parameters model call by value semantics. The value of a result parameter at the end of the procedure is passed back to the caller. Local variables follow the -@{text "where"}. If there are no local variables the @{text "where \ -in"} can be omitted. The variable @{term "I"} is actually unused in -the body, but is used in the examples below. *} +\where\. If there are no local variables the \where \ +in\ can be omitted. The variable @{term "I"} is actually unused in +the body, but is used in the examples below.\ -text {* +text \ The procedures command provides convenient syntax for procedure calls (that creates the proper @{term init}, @{term return} and @{term result} functions on the fly) and creates locales and statespaces to reason about the procedure. The purpose of locales is to set up logical contexts to support modular reasoning. Locales can be seen as freeze-dried proof contexts that get alive as you setup a new lemma or theorem (\cite{Ballarin-04-locales}). -The locale the user deals with is named @{text "Square_impl"}. +The locale the user deals with is named \Square_impl\. It defines the procedure name (internally @{term "Square_'proc"}), the procedure body -(named @{text "Square_body"}) and the statespaces for parameters and local and +(named \Square_body\) and the statespaces for parameters and local and global variables. Moreover it contains the assumption @{term "\ Square_'proc = Some Square_body"}, which states @@ -237,30 +237,30 @@ In this locale the procedure context @{term "\"} is fixed. So we always use this letter for the procedure specification. This is crucial, if we prove programs under the assumption of some procedure specifications. -*} +\ (*<*) context Square_impl begin (*>*) -text {* The procedures command generates syntax, so that we can -either write @{text "CALL Square(\I,\R)"} or @{term "\I :== CALL +text \The procedures command generates syntax, so that we can +either write \CALL Square(\I,\R)\ or @{term "\I :== CALL Square(\R)"} for the procedure call. The internal term is the following: -*} +\ (*<*) declare [[hoare_use_call_tr' = false]] (*>*) -text {* \small @{term [display] "CALL Square(\I,\R)"} *} +text \\small @{term [display] "CALL Square(\I,\R)"}\ (*<*) declare [[hoare_use_call_tr' = true]] (*>*) -text {* Note the +text \Note the additional decoration (with the procedure name) of the parameter and - local variable names.*} + local variable names.\ (*<*) end (*>*) -text {* The abstract syntax for the +text \The abstract syntax for the procedure call is @{term "call init p return result"}. The @{term "init"} function copies the values of the actual parameters to the formal parameters, the @{term return} function copies the global @@ -271,50 +271,50 @@ be all kind of expressions, since we only need their value. But result parameters must be proper ``lvalues'': variables (including dereferenced pointers) or array locations, since we have to assign values to them. -*} +\ -subsubsection {* Verification *} +subsubsection \Verification\ -text (in Square_impl) {* +text (in Square_impl) \ A procedure specification is an ordinary Hoare tuple. We use the parameterless -call for the specification; @{text "\R :== PROC Square(\N)"} is syntactic sugar -for @{text "Call Square_'proc"}. This emphasises that the specification +call for the specification; \\R :== PROC Square(\N)\ is syntactic sugar +for \Call Square_'proc\. This emphasises that the specification describes the internal behaviour of the procedure, whereas parameter passing corresponds to the procedure call. -The following precondition fixes the current value @{text "\N"} to the logical +The following precondition fixes the current value \\N\ to the logical variable @{term n}. Universal quantification of @{term "n"} enables us to adapt the specification to an actual parameter. The specification is used in the rule for procedure call when we come upon a call to @{term Square}. Thus @{term "n"} plays the role of the auxiliary variable @{term "Z"}. -*} +\ -text {* To verify the procedure we need to verify the body. We use +text \To verify the procedure we need to verify the body. We use a derived variant of the general recursion rule, tailored for non recursive procedures: @{thm [source] HoarePartial.ProcNoRec1}: \begin{center} @{thm [mode=Rule,mode=ParenStmt] HoarePartial.ProcNoRec1 [no_vars]} \end{center} The naming convention for the rule -is the following: The @{text "1"} expresses that we look at one - procedure, and @{text NoRec} that the procedure is non +is the following: The \1\ expresses that we look at one + procedure, and \NoRec\ that the procedure is non recursive. -*} +\ lemma (in Square_impl) shows "\n. \\\\N = n\ \R :== PROC Square(\N) \\R = n * n\" -txt {* The directive @{text "in"} has the effect that +txt \The directive \in\ has the effect that the context of the locale @{term "Square_impl"} is included to the current lemma, and that the lemma is added as a fact to the locale, after it is proven. The next time locale @{term "Square_impl"} is invoked this lemma is immediately available as fact, which the verification condition generator can use. -*} +\ apply (hoare_rule HoarePartial.ProcNoRec1) txt "@{subgoals[display]}" - txt {* The method @{text "hoare_rule"}, like @{text "rule"} applies a + txt \The method \hoare_rule\, like \rule\ applies a single rule, but additionally does some ``obvious'' steps: It solves the canonical side-conditions of various Hoare-rules and it automatically expands the @@ -324,31 +324,31 @@ apply (hoare_rule HoarePartial.ProcNoRec1) can unfold the definition of the body. The proof is finished by the vcg and simp. - *} +\ txt "@{subgoals[display]}" by vcg simp -text {* If the procedure is non recursive and there is no specification given, the -verification condition generator automatically expands the body.*} +text \If the procedure is non recursive and there is no specification given, the +verification condition generator automatically expands the body.\ lemma (in Square_impl) Square_spec: shows "\n. \\\\N = n\ \R :== PROC Square(\N) \\R = n * n\" by vcg simp -text {* An important naming convention is to name the specification as -@{text "_spec"}. The verification condition generator refers to +text \An important naming convention is to name the specification as +\_spec\. The verification condition generator refers to this name in order to search for a specification in the theorem database. -*} +\ -subsubsection {* Usage *} +subsubsection \Usage\ -text{* Let us see how we can use procedure specifications. *} +text\Let us see how we can use procedure specifications.\ (* FIXME: maybe don't show this at all *) lemma (in Square_impl) shows "\\\\I = 2\ \R :== CALL Square(\I) \\R = 4\" - txt {* Remember that we have already proven @{thm [source] "Square_spec"} in the locale - @{text "Square_impl"}. This is crucial for + txt \Remember that we have already proven @{thm [source] "Square_spec"} in the locale + \Square_impl\. This is crucial for verification condition generation. When reaching a procedure call, it looks for the specification (by its name) and applies the rule @{thm [source,mode=ParenStmt] HoarePartial.ProcSpec} @@ -360,7 +360,7 @@ instantiated with the specification @{thm [display] Square_spec [no_vars]} The specification talks about the formal parameters @{term "N"} and @{term R}. The precondition @{term "\\N = n\"} just fixes the initial - value of @{text N}. + value of \N\. The actual parameters are @{term "I"} and @{term "R"}. We have to adapt the specification to this calling context. @{term "\n. \\ \\I = n\ \R :== CALL Square(\I) \\R = n * n\"}. @@ -371,21 +371,21 @@ instantiated with the specification tells us @{term "\\I = n\"} for the pre-state. So the value of @{term n} is the value of @{term I} in the pre-state. So we arrive at @{term "\\I = 2\ \ \\I * \I = 4\"}. - *} +\ apply vcg_step txt "@{subgoals[display]}" - txt {* + txt \ The second set looks slightly more involved: @{term "\\t. \<^bsup>t\<^esup>R = \I * \I \ \I * \I = 4\"}, this is an artefact from the - procedure call rule. Originally @{text "\I * \I = 4"} was @{text "\<^bsup>t\<^esup>R = 4"}. Where + procedure call rule. Originally \\I * \I = 4\ was \\<^bsup>t\<^esup>R = 4\. Where @{term "t"} denotes the final state of the procedure and the superscript notation allows to select a component from a particular state. - *} +\ apply vcg_step txt "@{subgoals[display]}" by simp -text {* +text \ The adaption of the procedure specification to the actual calling context is done due to the @{term init}, @{term return} and @{term result} functions in the rule @{thm [source] HoarePartial.ProcSpec} (or in the variant @@ -393,16 +393,16 @@ in the rule @{thm [source] HoarePartial.ProcSpec} (or in the variant incorporates the fact that the postcondition for abrupt termination is the empty set). For the readers interested in the internals, here a version without vcg. -*} +\ lemma (in Square_impl) shows "\\\\I = 2\ \R :== CALL Square(\I) \\R = 4\" apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ Square_spec]) txt "@{subgoals[display]}" - txt {* This is the raw verification condition, + txt \This is the raw verification condition, It is interesting to see how the auxiliary variable @{term "Z"} is actually used. It is unified with @{term n} of the specification and fixes the state after parameter passing. - *} +\ apply simp txt "@{subgoals[display]}" prefer 2 @@ -413,11 +413,11 @@ lemma (in Square_impl) -subsubsection {* Recursion *} +subsubsection \Recursion\ -text {* We want to define a procedure for the factorial. We first +text \We want to define a procedure for the factorial. We first define a HOL function that calculates it, to specify the procedure later on. -*} +\ primrec fac:: "nat \ nat" where @@ -429,7 +429,7 @@ lemma fac_simp [simp]: "0 < i \ fac i = i * fac (i - 1)" by (cases i) simp_all (*>*) -text {* Now we define the procedure. *} +text \Now we define the procedure.\ procedures Fac (N::nat | R::nat) "IF \N = 0 THEN \R :== 1 @@ -437,9 +437,9 @@ procedures \R :== \N * \R FI" -text {* +text \ Now let us prove that our implementation of @{term "Fac"} meets its specification. -*} +\ lemma (in Fac_impl) shows "\n. \\ \\N = n\ \R :== PROC Fac(\N) \\R = fac n\" @@ -450,7 +450,7 @@ txt "@{subgoals[display]}" apply simp done -text {* +text \ Since the factorial is implemented recursively, the main ingredient of this proof is, to assume that the specification holds for the recursive call of @{term Fac} and prove the body correct. @@ -462,36 +462,36 @@ the rule @{thm [source] HoarePartial.ProcRec1} \end{center} The verification condition generator infers the specification out of the context @{term "\"} when it encounters a recursive call of the factorial. -*} +\ -subsection {* Global Variables and Heap \label{sec:VcgHeap}*} +subsection \Global Variables and Heap \label{sec:VcgHeap}\ -text {* +text \ Now we define and verify some procedures on heap-lists. We consider list structures consisting of two fields, a content element @{term "cont"} and a reference to the next list element @{term "next"}. We model this by the following state space where every field has its own heap. -*} +\ hoarestate globals_heap = "next" :: "ref \ ref" cont :: "ref \ nat" -text {* It is mandatory to start the state name with `globals'. This is exploited +text \It is mandatory to start the state name with `globals'. This is exploited by the syntax translations to store the components in the @{const globals} part of the state. -*} +\ -text {* Updates to global components inside a procedure are +text \Updates to global components inside a procedure are always propagated to the caller. This is implicitly done by the parameter passing syntax translations. -*} +\ -text {* We first define an append function on lists. It takes two +text \We first define an append function on lists. It takes two references as parameters. It appends the list referred to by the first parameter with the list referred to by the second parameter. The statespace of the global variables has to be imported. -*} +\ procedures (imports globals_heap) append(p :: ref, q::ref | p::ref) @@ -502,39 +502,39 @@ procedures (imports globals_heap) context append_impl begin (*>*) -text {* +text \ The difference of a global and a local variable is that global variables are automatically copied back to the procedure caller. We can study this effect on the translation of @{term "\p :== CALL append(\p,\q)"}: -*} +\ (*<*) declare [[hoare_use_call_tr' = false]] (*>*) -text {* +text \ @{term [display] "\p :== CALL append(\p,\q)"} -*} +\ (*<*) declare [[hoare_use_call_tr' = true]] end (*>*) -text {* Below we give two specifications this time. +text \Below we give two specifications this time. One captures the functional behaviour and focuses on the entities that are potentially modified by the procedure, the second one is a pure frame condition. -*} +\ -text {* +text \ The functional specification below introduces two logical variables besides the state space variable @{term "\"}, namely @{term "Ps"} and @{term "Qs"}. They are universally quantified and range over both the pre-and the postcondition, so that we are able to properly instantiate the specification -during the proofs. The syntax @{text "\\. \\"} is a shorthand to fix the current -state: @{text "{s. \ = s \}"}. Moreover @{text "\<^bsup>\\<^esup>x"} abbreviates -the lookup of variable @{text "x"} in the state -@{text \}. +during the proofs. The syntax \\\. \\\ is a shorthand to fix the current +state: \{s. \ = s \}\. Moreover \\<^bsup>\\<^esup>x\ abbreviates +the lookup of variable \x\ in the state +\\\. The approach to specify procedures on lists basically follows \cite{MehtaN-CADE03}. From the pointer structure @@ -553,7 +553,7 @@ the references in @{term h} up to the reference @{term y}. A list @{term "List p h ps"} is a path starting in @{term p} and ending up in @{term Null}. -*} +\ lemma (in append_impl) append_spec1: @@ -562,32 +562,32 @@ shows "\\ Ps Qs. \p :== PROC append(\p,\q) \List \p \next (Ps@Qs) \ (\x. x\set Ps \ \next x = \<^bsup>\\<^esup>next x)\" apply (hoare_rule HoarePartial.ProcRec1) -txt {* @{subgoals [margin=80,display]} +txt \@{subgoals [margin=80,display]} Note that @{term "hoare_rule"} takes care of multiple auxiliary variables! @{thm [source] HoarePartial.ProcRec1} has only one auxiliary variable, namely @{term Z}. -But the type of @{term Z} can be instantiated arbitrarily. So @{text "hoare_rule"} +But the type of @{term Z} can be instantiated arbitrarily. So \hoare_rule\ instantiates @{term Z} with the tuple @{term "(\,Ps,Qs)"} and derives a proper variant -of the rule. Therefore @{text "hoare_rule"} depends on the proper quantification of +of the rule. Therefore \hoare_rule\ depends on the proper quantification of auxiliary variables! -*} +\ apply vcg -txt {* @{subgoals [display]} -For each branch of the @{text IF} statement we have one conjunct to prove. The -@{text THEN} branch starts with @{text "p = Null \ \"} and the @{text ELSE} branch -with @{text "p \ Null \ \"}. Let us focus on the @{text ELSE} branch, were the +txt \@{subgoals [display]} +For each branch of the \IF\ statement we have one conjunct to prove. The +\THEN\ branch starts with \p = Null \ \\ and the \ELSE\ branch +with \p \ Null \ \\. Let us focus on the \ELSE\ branch, were the recursive call to append occurs. First of all we have to prove that the precondition for the recursive call is fulfilled. That means we have to provide some witnesses for -the lists @{term Psa} and @{term Qsa} which are referenced by @{text "p\next"} (now +the lists @{term Psa} and @{term Qsa} which are referenced by \p\next\ (now written as @{term "next p"}) and @{term q}. Then we have to show that we can derive the overall postcondition from the postcondition of the recursive call. The state components that have changed by the recursive call are the ones with the suffix -@{text a}, like @{text nexta} and @{text pa}. -*} +\a\, like \nexta\ and \pa\. +\ apply fastforce done -text {* If the verification condition generator works on a procedure +text \If the verification condition generator works on a procedure call it checks whether it can find a modifies clause in the context. If one is present the procedure call is simplified before the Hoare rule @{thm [source] HoarePartial.ProcSpec} is @@ -598,28 +598,28 @@ simplification is justified by the rule @{thm [source] HoarePartial.ProcModifyReturn}. So after this simplification all global components that do not appear in the modifies clause are treated -as local variables. *} +as local variables.\ -text {* We study the effect of the modifies clause on the following +text \We study the effect of the modifies clause on the following examples, where we want to prove that @{term "append"} does not change the @{term "cont"} part of the heap. -*} +\ lemma (in append_impl) shows "\\ \\cont=c\ \p :== CALL append(Null,Null) \\cont=c\" proof - note append_spec = append_spec1 show ?thesis apply vcg - txt {* @{subgoals [display]} *} - txt {* Only focus on the very last line: @{term conta} is the heap component + txt \@{subgoals [display]}\ + txt \Only focus on the very last line: @{term conta} is the heap component after the procedure call, and @{term cont} the heap component before the procedure call. Since we have not added the modified clause we do not know that they have to be equal. - *} +\ oops -text {* +text \ We now add the frame condition. The list in the modifies clause names all global state components that may be changed by the procedure. Note that we know from the modifies clause @@ -627,7 +627,7 @@ that the @{term cont} parts are not changed. Also a small side note on the syntax. We use ordinary brackets in the postcondition of the modifies clause, and also the state components do not carry the acute, because we explicitly note the state @{term t} here. -*} +\ lemma (in append_impl) append_modifies: @@ -637,17 +637,17 @@ lemma (in append_impl) append_modifies: apply (vcg spec=modifies) done -text {* We tell the verification condition generator to use only the +text \We tell the verification condition generator to use only the modifies clauses and not to search for functional specifications by -the parameter @{text "spec=modifies"}. It also tries to solve the +the parameter \spec=modifies\. It also tries to solve the verification conditions automatically. Again it is crucial to name the lemma with this naming scheme, since the verfication condition generator searches for these names. -*} +\ -text {* The modifies clause is equal to a state update specification +text \The modifies clause is equal to a state update specification of the following form. -*} +\ lemma (in append_impl) shows "{t. t may_only_modify_globals Z in [next]} = @@ -656,8 +656,8 @@ lemma (in append_impl) shows "{t. t may_only_modify_globals Z in [next]} apply simp done -text {* Now that we have proven the frame-condition, it is available within -the locale @{text "append_impl"} and the @{text "vcg"} exploits it.*} +text \Now that we have proven the frame-condition, it is available within +the locale \append_impl\ and the \vcg\ exploits it.\ lemma (in append_impl) shows "\\ \\cont=c\ \p :== CALL append(Null,Null) \\cont=c\" @@ -665,23 +665,23 @@ proof - note append_spec = append_spec1 show ?thesis apply vcg - txt {* @{subgoals [display]} *} - txt {* With a modifies clause present we know that no change to @{term cont} + txt \@{subgoals [display]}\ + txt \With a modifies clause present we know that no change to @{term cont} has occurred. - *} +\ by simp qed -text {* +text \ Of course we could add the modifies clause to the functional specification as well. But separating both has the advantage that we split up the verification work. We can make use of the modifies clause before we apply the functional specification in a fully automatic fashion. -*} +\ -text {* +text \ To prove that a procedure respects the modifies clause, we only need the modifies clauses of the procedures called in the body. We do not need the functional specifications. So we can always prove the modifies @@ -689,13 +689,13 @@ clause without functional specifications, but we may need the modifies clause to prove the functional specifications. So usually the modifies clause is proved before the proof of the functional specification, so that it can already be used by the verification condition generator. -*} +\ -subsection {* Total Correctness *} +subsection \Total Correctness\ -text {* When proving total correctness the additional proof burden to +text \When proving total correctness the additional proof burden to the user is to come up with a well-founded relation and to prove that certain states get smaller according to this relation. Proving that a relation is well-founded can be quite hard. But fortunately there are @@ -711,7 +711,7 @@ best explained by some equations: @{thm in_lex_iff [no_vars]}\\ @{thm in_inv_image_iff [no_vars]} -Another useful construction is @{text "<*mlex*>"} which is a combination +Another useful construction is \<*mlex*>\ which is a combination of a measure and a lexicographic product: @{thm in_mlex_iff [no_vars]}\\ @@ -720,7 +720,7 @@ The state may either decrease according to the measure function @{term f} or the measure stays the same and the state decreases because of the relation @{term r}. Lets look at a loop: -*} +\ lemma (in vars) "\\\<^sub>t \\M = 0 \ \S = 0\ @@ -730,40 +730,40 @@ lemma (in vars) DO \S :== \S + b;; \M :== \M + 1 OD \\S = a * b\" apply vcg -txt {* @{subgoals [display]} +txt \@{subgoals [display]} The first conjunct of the second subgoal is the proof obligation that the variant decreases in the loop body. -*} +\ by auto -text {* The variant annotation is preceded by @{text VAR}. The capital @{text MEASURE} -is a shorthand for @{text "measure (\s. a - \<^bsup>s\<^esup>M)"}. Analogous there is a capital -@{text "<*MLEX*>"}. -*} +text \The variant annotation is preceded by \VAR\. The capital \MEASURE\ +is a shorthand for \measure (\s. a - \<^bsup>s\<^esup>M)\. Analogous there is a capital +\<*MLEX*>\. +\ lemma (in Fac_impl) Fac_spec': shows "\\. \\\<^sub>t {\} \R :== PROC Fac(\N) \\R = fac \<^bsup>\\<^esup>N\" apply (hoare_rule HoareTotal.ProcRec1 [where r="measure (\(s,p). \<^bsup>s\<^esup>N)"]) -txt {* In case of the factorial the parameter @{term N} decreases in every call. This +txt \In case of the factorial the parameter @{term N} decreases in every call. This is easily expressed by the measure function. Note that the well-founded relation for recursive procedures is formally defined on tuples containing the state space and the procedure name. -*} -txt {* @{subgoals [display]} +\ +txt \@{subgoals [display]} The initial call to the factorial is in state @{term "\"}. Note that in the precondition @{term "{\} \ {\'}"}, @{term "\'"} stems from the lemma we want to prove and @{term "\"} stems from the recursion rule for total correctness. Both are synonym for the initial state. To use the assumption in the Hoare context we have to show that the call to the factorial is invoked on a smaller @{term N} compared -to the initial @{text "\<^bsup>\\<^esup>N"}. -*} +to the initial \\<^bsup>\\<^esup>N\. +\ apply vcg -txt {* @{subgoals [display]} -The tribute to termination is that we have to show @{text "N - 1 < N"} in case of +txt \@{subgoals [display]} +The tribute to termination is that we have to show \N - 1 < N\ in case of the recursive call. -*} +\ by simp lemma (in append_impl) append_spec2: @@ -773,15 +773,15 @@ shows "\\ Ps Qs. \\\<^sub>t \List \p \next (Ps@Qs) \ (\x. x\set Ps \ \next x = \<^bsup>\\<^esup>next x)\" apply (hoare_rule HoareTotal.ProcRec1 [where r="measure (\(s,p). length (list \<^bsup>s\<^esup>p \<^bsup>s\<^esup>next))"]) -txt {* In case of the append function the length of the list referenced by @{term p} +txt \In case of the append function the length of the list referenced by @{term p} decreases in every recursive call. -*} -txt {* @{subgoals [margin=80,display]} *} +\ +txt \@{subgoals [margin=80,display]}\ apply vcg apply (fastforce simp add: List_list) done -text {* +text \ In case of the lists above, we have used a relational list abstraction @{term List} to construct the HOL lists @{term Ps} and @{term Qs} for the pre- and postcondition. To supply a proper measure function we use a functional abstraction @{term list}. @@ -792,14 +792,14 @@ since the lists are already uniquely determined by the relational abstraction: @{thm list_def [no_vars]} \isacommand{lemma} @{thm List_conv_islist_list [no_vars]} -*} +\ -text {* +text \ The next contrived example is taken from \cite{Homeier-95-vcg}, to illustrate a more complex termination criterion for mutually recursive procedures. The procedures do not calculate anything useful. -*} +\ procedures @@ -816,25 +816,25 @@ procedures IF 0 < \M THEN CALL coast(\N,\M- 1) FI" -text {* -In the recursive calls in procedure @{text pedal} the first argument always decreases. -In the body of @{text coast} in the recursive call of @{text coast} the second -argument decreases, but in the call to @{text pedal} no argument decreases. +text \ +In the recursive calls in procedure \pedal\ the first argument always decreases. +In the body of \coast\ in the recursive call of \coast\ the second +argument decreases, but in the call to \pedal\ no argument decreases. Therefore an relation only on the state space is insufficient. We have to take the procedure names into account, too. -We consider the procedure @{text coast} to be ``bigger'' than @{text pedal} +We consider the procedure \coast\ to be ``bigger'' than \pedal\ when we construct a well-founded relation on the product of state space and procedure names. -*} +\ -ML {* ML_Thms.bind_thm ("HoareTotal_ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Total 2)*} +ML \ML_Thms.bind_thm ("HoareTotal_ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Total 2)\ -text {* +text \ We provide the ML function {\tt gen\_proc\_rec} to automatically derive a convenient rule for recursion for a given number of mutually recursive procedures. -*} +\ lemma (in pedal_coast_clique) @@ -844,19 +844,19 @@ apply (hoare_rule HoareTotal_ProcRec2 [where r= "((\(s,p). \<^bsup>s\<^esup>N) <*mlex*> (\(s,p). \<^bsup>s\<^esup>M) <*mlex*> measure (\(s,p). if p = coast_'proc then 1 else 0))"]) - txt {* We can directly express the termination condition described above with - the @{text "<*mlex*>"} construction. Either state component @{text N} decreases, - or it stays the same and @{text M} decreases or this also stays the same, but - then the procedure name has to decrease.*} - txt {* @{subgoals [margin=80,display]} *} + txt \We can directly express the termination condition described above with + the \<*mlex*>\ construction. Either state component \N\ decreases, + or it stays the same and \M\ decreases or this also stays the same, but + then the procedure name has to decrease.\ + txt \@{subgoals [margin=80,display]}\ apply simp_all - txt {* @{subgoals [margin=75,display]} *} + txt \@{subgoals [margin=75,display]}\ by (vcg,simp)+ -text {* We can achieve the same effect without @{text "<*mlex*>"} by using - the ordinary lexicographic product @{text "<*lex*>"}, @{text "inv_image"} and - @{text "measure"} -*} +text \We can achieve the same effect without \<*mlex*>\ by using + the ordinary lexicographic product \<*lex*>\, \inv_image\ and + \measure\ +\ lemma (in pedal_coast_clique) shows "(\\. \\\<^sub>t {\} PROC pedal(\N,\M) UNIV) \ @@ -866,18 +866,18 @@ apply (hoare_rule HoareTotal_ProcRec2 measure (\m. m) <*lex*> measure (\p. if p = coast_'proc then 1 else 0)) (\(s,p). (\<^bsup>s\<^esup>N,\<^bsup>s\<^esup>M,p))"]) - txt {* With the lexicographic product we construct a well-founded relation on + txt \With the lexicographic product we construct a well-founded relation on triples of type @{typ "(nat\nat\string)"}. With @{term inv_image} we project the components out of the state-space and the procedure names to this triple. - *} - txt {* @{subgoals [margin=75,display]} *} +\ + txt \@{subgoals [margin=75,display]}\ apply simp_all by (vcg,simp)+ -text {* By doing some arithmetic we can express the termination condition with a single +text \By doing some arithmetic we can express the termination condition with a single measure function. -*} +\ lemma (in pedal_coast_clique) shows "(\\. \\\<^sub>t {\} PROC pedal(\N,\M) UNIV) \ @@ -885,40 +885,40 @@ shows "(\\. \\\<^sub>t {\} PROC pedal(\< apply(hoare_rule HoareTotal_ProcRec2 [where r= "measure (\(s,p). \<^bsup>s\<^esup>N + \<^bsup>s\<^esup>M + (if p = coast_'proc then 1 else 0))"]) apply simp_all -txt {* @{subgoals [margin=75,display]} *} +txt \@{subgoals [margin=75,display]}\ by (vcg,simp,arith?)+ -subsection {* Guards *} +subsection \Guards\ -text (in vars) {* The purpose of a guard is to guard the {\bf (sub-) expressions} of a +text (in vars) \The purpose of a guard is to guard the {\bf (sub-) expressions} of a statement against runtime faults. Typical runtime faults are array bound violations, dereferencing null pointers or arithmetical overflow. Guards make the potential runtime faults explicit, since the expressions themselves never ``fail'' because they are ordinary HOL expressions. To relieve the user from typing in lots of standard guards for every subexpression, we supply some input syntax for the common language constructs that automatically generate the guards. -For example the guarded assignment @{text "\M :==\<^sub>g (\M + 1) div \N"} gets expanded to +For example the guarded assignment \\M :==\<^sub>g (\M + 1) div \N\ gets expanded to guarded command @{term "\M :==\<^sub>g (\M + 1) div \N"}. Here @{term "in_range"} is uninterpreted by now. -*} +\ lemma (in vars) "\\\True\ \M :==\<^sub>g (\M + 1) div \N \True\" apply vcg -txt {* @{subgoals} *} +txt \@{subgoals}\ oops -text {* -The user can supply on (overloaded) definition of @{text "in_range"} +text \ +The user can supply on (overloaded) definition of \in_range\ to fit to his needs. Currently guards are generated for: \begin{itemize} -\item overflow and underflow of numbers (@{text "in_range"}). For subtraction of - natural numbers @{text "a - b"} the guard @{text "b \ a"} is generated instead - of @{text "in_range"} to guard against underflows. -\item division by @{text 0} +\item overflow and underflow of numbers (\in_range\). For subtraction of + natural numbers \a - b\ the guard \b \ a\ is generated instead + of \in_range\ to guard against underflows. +\item division by \0\ \item dereferencing of @{term Null} pointers \item array bound violations \end{itemize} @@ -926,22 +926,22 @@ Currently guards are generated for: Following (input) variants of guarded statements are available: \begin{itemize} -\item Assignment: @{text "\ :==\<^sub>g \"} -\item If: @{text "IF\<^sub>g \"} -\item While: @{text "WHILE\<^sub>g \"} -\item Call: @{text "CALL\<^sub>g \"} or @{text "\ :== CALL\<^sub>g \"} +\item Assignment: \\ :==\<^sub>g \\ +\item If: \IF\<^sub>g \\ +\item While: \WHILE\<^sub>g \\ +\item Call: \CALL\<^sub>g \\ or \\ :== CALL\<^sub>g \\ \end{itemize} -*} +\ -subsection {* Miscellaneous Techniques *} +subsection \Miscellaneous Techniques\ -subsubsection {* Modifies Clause *} +subsubsection \Modifies Clause\ -text {* We look at some issues regarding the modifies clause with the example +text \We look at some issues regarding the modifies clause with the example of insertion sort for heap lists. -*} +\ primrec sorted:: "('a \ 'a \ bool) \ 'a list \ bool" where @@ -984,7 +984,7 @@ lemma (in insert_impl) insert_spec: done (*>*) -text {* +text \ In the postcondition of the functional specification there is a small but important subtlety. Whenever we talk about the @{term "cont"} part we refer to the one of the pre-state. @@ -992,23 +992,23 @@ The reason is that we have separated out the information that @{term "cont"} is modified by the procedure, to the modifies clause. So whenever we talk about unmodified parts in the postcondition we have to use the pre-state part, or explicitly state an equality in the postcondition. -The reason is simple. If the postcondition would talk about @{text "\cont"} -instead of \mbox{@{text "\<^bsup>\\<^esup>cont"}}, we get a new instance of @{text "cont"} during +The reason is simple. If the postcondition would talk about \\cont\ +instead of \mbox{\\<^bsup>\\<^esup>cont\}, we get a new instance of \cont\ during verification and the postcondition would only state something about this new instance. But as the verification condition generator uses the modifies clause the caller of @{term "insert"} instead still has the -old @{text "cont"} after the call. Thats the sense of the modifies clause. +old \cont\ after the call. Thats the sense of the modifies clause. So the caller and the specification simply talk about two different things, without being able to relate them (unless an explicit equality is added to the specification). -*} +\ -subsubsection {* Annotations *} +subsubsection \Annotations\ -text {* +text \ Annotations (like loop invariants) -are mere syntactic sugar of statements that are used by the @{text "vcg"}. +are mere syntactic sugar of statements that are used by the \vcg\. Logically a statement with an annotation is equal to the statement without it. Hence annotations can be introduced by the user while building a proof: @@ -1020,14 +1020,14 @@ nesting of sequential composition. Then after stripping the annotations the resu is no longer syntactically identical to original one, only equivalent modulo associativity of sequential composition. The following rule also deals with this case: @{thm [source] HoarePartial.annotate_normI}: @{thm [mode=Rule] HoarePartial.annotate_normI [no_vars]} -*} +\ -text_raw {* \paragraph{Loop Annotations} +text_raw \\paragraph{Loop Annotations} \mbox{} \medskip \mbox{} -*} +\ procedures (imports globals_heap) insertSort(p::ref| p::ref) @@ -1051,11 +1051,11 @@ done -text {* Insertion sort is not implemented recursively here, but with a +text \Insertion sort is not implemented recursively here, but with a loop. Note that the while loop is not annotated with an invariant in the procedure definition. The invariant only comes into play during verification. -Therefore we annotate the loop first, before we run the @{text "vcg"}. -*} +Therefore we annotate the loop first, before we run the \vcg\. +\ lemma (in insertSort_impl) insertSort_spec: shows "\\ Ps. @@ -1074,7 +1074,7 @@ apply (hoare_rule anno= DO \q :== \p;; \p :== \p\\next;; \r :== CALL insert(\q,\r) OD;; \p :== \r" in HoarePartial.annotateI) apply vcg -txt {* @{text "\"} *} +txt \\\\\ (*<*) apply fastforce @@ -1091,20 +1091,20 @@ txt {* @{text "\"} *} done (*>*) -text {* The method @{text "hoare_rule"} automatically solves the side-condition +text \The method \hoare_rule\ automatically solves the side-condition that the annotated - program is the same as the original one after stripping the annotations. *} + program is the same as the original one after stripping the annotations.\ -text_raw {* \paragraph{Specification Annotations} +text_raw \\paragraph{Specification Annotations} \mbox{} \medskip \mbox{} -*} +\ -text {* +text \ When verifying a larger block of program text, it might be useful to split up the block and to prove the parts in isolation. This is especially useful to isolate loops. On the level of the Hoare calculus @@ -1125,15 +1125,15 @@ used by the verification condition generator. We express this by defining the whole @{term specAnno} to be equivalent with the body applied to an arbitrary variable. -The Hoare rule for @{text "specAnno"} is mainly an instance of the consequence rule: +The Hoare rule for \specAnno\ is mainly an instance of the consequence rule: @{thm [mode=Rule,mode=ParenStmt] HoarePartial.SpecAnno [no_vars]} The side-condition @{term "\Z. c Z = c undefined"} expresses the intention of body @{term c} explained above: The raw body is independent of the auxiliary variable. This -side-condition is solved automatically by the @{text "vcg"}. The concrete syntax for +side-condition is solved automatically by the \vcg\. The concrete syntax for this specification annotation is shown in the following example: -*} +\ lemma (in vars) "\\ {\} \I :== \M;; @@ -1141,27 +1141,27 @@ lemma (in vars) "\\ {\} \M :== \N;; \N :== \I \\M = \<^bsup>\\<^esup>N \ \N = \<^bsup>\\<^esup>I\ \\M = \<^bsup>\\<^esup>N \ \N = \<^bsup>\\<^esup>M\" -txt {* With the annotation we can name an intermediate state @{term \}. Since the +txt \With the annotation we can name an intermediate state @{term \}. Since the postcondition refers to @{term "\"} we have to link the information about - the equivalence of @{text "\<^bsup>\\<^esup>I"} and @{text "\<^bsup>\\<^esup>M"} in the specification in order + the equivalence of \\<^bsup>\\<^esup>I\ and \\<^bsup>\\<^esup>M\ in the specification in order to be able to derive the postcondition. - *} +\ apply vcg_step apply vcg_step -txt {* @{subgoals [display]} *} -txt {* The first subgoal is the isolated Hoare tuple. The second one is the +txt \@{subgoals [display]}\ +txt \The first subgoal is the isolated Hoare tuple. The second one is the side-condition of the consequence rule that allows us to derive the outermost pre/post condition from our inserted specification. - @{text "\I = \<^bsup>\\<^esup>M"} is the precondition of the specification, + \\I = \<^bsup>\\<^esup>M\ is the precondition of the specification, The second conjunct is a simplified version of - @{text "\t. \<^bsup>t\<^esup>M = \N \ \<^bsup>t\<^esup>N = \I \ \<^bsup>t\<^esup>M = \<^bsup>\\<^esup>N \ \<^bsup>t\<^esup>N = \<^bsup>\\<^esup>M"} expressing that the + \\t. \<^bsup>t\<^esup>M = \N \ \<^bsup>t\<^esup>N = \I \ \<^bsup>t\<^esup>M = \<^bsup>\\<^esup>N \ \<^bsup>t\<^esup>N = \<^bsup>\\<^esup>M\ expressing that the postcondition of the specification implies the outermost postcondition. - *} +\ apply vcg -txt {* @{subgoals [display]} *} +txt \@{subgoals [display]}\ apply simp apply vcg -txt {* @{subgoals [display]} *} +txt \@{subgoals [display]}\ by simp @@ -1173,19 +1173,19 @@ lemma (in vars) \\M = \<^bsup>\\<^esup>N \ \N = \<^bsup>\\<^esup>I\ \\M = \<^bsup>\\<^esup>N \ \N = \<^bsup>\\<^esup>M\" apply vcg -txt {* @{subgoals [display]} *} +txt \@{subgoals [display]}\ by simp_all -text {* Note that @{text "vcg_step"} changes the order of sequential composition, to -allow the user to decompose sequences by repeated calls to @{text "vcg_step"}, whereas -@{text "vcg"} preserves the order. +text \Note that \vcg_step\ changes the order of sequential composition, to +allow the user to decompose sequences by repeated calls to \vcg_step\, whereas +\vcg\ preserves the order. The above example illustrates how we can introduce a new logical state variable @{term "\"}. You can introduce multiple variables by using a tuple: -*} +\ lemma (in vars) @@ -1196,25 +1196,25 @@ lemma (in vars) \\M = n \ \N = i\ \\M = \<^bsup>\\<^esup>N \ \N = \<^bsup>\\<^esup>M\" apply vcg -txt {* @{subgoals [display]} *} +txt \@{subgoals [display]}\ by simp_all -text_raw {* \paragraph{Lemma Annotations} +text_raw \\paragraph{Lemma Annotations} \mbox{} \medskip \mbox{} -*} +\ -text {* +text \ The specification annotations described before split the verification into several Hoare triples which result in several subgoals. If we instead want to proof the Hoare triples independently as -separate lemmas we can use the @{text "LEMMA"} annotation to plug together the +separate lemmas we can use the \LEMMA\ annotation to plug together the lemmas. It inserts the lemma in the same fashion as the specification annotation. -*} +\ lemma (in vars) foo_lemma: "\n m. \\ \\N = n \ \M = m\ \N :== \N + 1;; \M :== \M + 1 \\N = n + 1 \ \M = m + 1\" @@ -1264,24 +1264,24 @@ lemma (in vars) done -subsubsection {* Total Correctness of Nested Loops *} +subsubsection \Total Correctness of Nested Loops\ -text {* +text \ When proving termination of nested loops it is sometimes necessary to express that the loop variable of the outer loop is not modified in the inner loop. To express this one has to fix the value of the outer loop variable before the inner loop and use this value in the invariant of the inner loop. This can be achieved by surrounding the inner while loop -with an @{text "ANNO"} specification as explained previously. However, this +with an \ANNO\ specification as explained previously. However, this leads to repeating the invariant of the inner loop three times: in the invariant itself and -in the the pre- and postcondition of the @{text "ANNO"} specification. Moreover one has -to deal with the additional subgoal introduced by @{text "ANNO"} that expresses how +in the the pre- and postcondition of the \ANNO\ specification. Moreover one has +to deal with the additional subgoal introduced by \ANNO\ that expresses how the pre- and postcondition is connected to the invariant. To avoid this extra specification and verification work, we introduce an variant of the annotated while-loop, where one can -introduce logical variables by @{text "FIX"}. As for the @{text "ANNO"} specification -multiple logical variables can be introduced via a tuple (@{text "FIX (a,b,c)."}). +introduce logical variables by \FIX\. As for the \ANNO\ specification +multiple logical variables can be introduced via a tuple (\FIX (a,b,c).\). The Hoare logic rule for the augmented while-loop is a mixture of the invariant rule for -loops and the consequence rule for @{text "ANNO"}: +loops and the consequence rule for \ANNO\: \begin{center} @{thm [mode=Rule,mode=ParenStmt] HoareTotal.WhileAnnoFix' [no_vars]} @@ -1303,7 +1303,7 @@ loop variable @{term "M"} while the inner loop increments @{term "N"}. To discha proof obligation for the termination of the outer loop, we need to know that the inner loop does not mess around with @{term "M"}. This is expressed by introducing the logical variable @{term "m"} and fixing the value of @{term "M"} to it. -*} +\ lemma (in vars) @@ -1324,7 +1324,7 @@ lemma (in vars) OD \\M=i \ (\M\0 \ \N=j)\" apply vcg -txt {* @{subgoals [display]} +txt \@{subgoals [display]} The first subgoal is from the precondition to the invariant of the outer loop. The fourth subgoal is from the invariant together with the negated loop condition @@ -1337,11 +1337,11 @@ of the inner loop. And at the same time from the invariant of the inner loop to invariant of the outer loop (together with the proof obligation that the measure of the outer loop decreases). The universal quantified variables @{term "Ma"} and @{term "N"} are the ``fresh'' state variables introduced for the final state of the inner loop. -The equality @{term "Ma=M"} is the result of the equality @{text "\M=m"} in the inner +The equality @{term "Ma=M"} is the result of the equality \\M=m\ in the inner invariant. Subgoal three is the preservation of the invariant by the inner loop body (together with the proof obligation that the measure of the inner loop decreases). -*} +\ (*<*) apply (simp) apply (simp,arith) @@ -1349,9 +1349,9 @@ apply (simp,arith) done (*>*) -subsection {* Functional Correctness, Termination and Runtime Faults *} +subsection \Functional Correctness, Termination and Runtime Faults\ -text {* +text \ Total correctness of a program with guards conceptually leads to three verification tasks. \begin{itemize} @@ -1372,7 +1372,7 @@ functional specification parts. So after all there is no reason why we should again prove the absence of runtime faults and termination for the modifies clause. Therefor it suffices to have partial correctness of the modifies clause for a program were all guards are -ignored. This leads to the following pattern: *} +ignored. This leads to the following pattern:\ @@ -1384,67 +1384,67 @@ procedures foo (N::nat|M::nat) foo_modifies: "\\. \\\<^bsub>/UNIV\<^esub> {\} \M :== PROC foo(\N) {t. t may_only_modify_globals \ in []}" -text {* +text \ The verification condition generator can solve those modifies clauses automatically -and can use them to simplify calls to @{text foo} even in the context of total +and can use them to simplify calls to \foo\ even in the context of total correctness. -*} +\ -subsection {* Procedures and Locales \label{sec:Locales}*} +subsection \Procedures and Locales \label{sec:Locales}\ -text {* +text \ Verification of a larger program is organised on the granularity of procedures. We proof the procedures in a bottom up fashion. Of course you can also always use Isabelle's -dummy proof @{text "sorry"} to prototype your formalisation. So you can write the +dummy proof \sorry\ to prototype your formalisation. So you can write the theory in a bottom up fashion but actually prove the lemmas in any other order. Here are some explanations of handling of locales. In the examples below, consider -@{text proc\<^sub>1} and @{text proc\<^sub>2} to be ``leaf'' procedures, which do not call any +\proc\<^sub>1\ and \proc\<^sub>2\ to be ``leaf'' procedures, which do not call any other procedure. -Procedure @{text "proc"} directly calls @{text proc\<^sub>1} and @{text proc\<^sub>2}. +Procedure \proc\ directly calls \proc\<^sub>1\ and \proc\<^sub>2\. -\isacommand{lemma} (\isacommand{in} @{text "proc\<^sub>1_impl"}) @{text "proc\<^sub>1_modifies"}:\\ -\isacommand{shows} @{text "\"} +\isacommand{lemma} (\isacommand{in} \proc\<^sub>1_impl\) \proc\<^sub>1_modifies\:\\ +\isacommand{shows} \\\ -After the proof of @{text "proc\<^sub>1_modifies"}, the \isacommand{in} directive +After the proof of \proc\<^sub>1_modifies\, the \isacommand{in} directive stores the lemma in the -locale @{text "proc\<^sub>1_impl"}. When we later on include @{text "proc\<^sub>1_impl"} or prove -another theorem in locale @{text "proc\<^sub>1_impl"} the lemma @{text "proc\<^sub>1_modifies"} +locale \proc\<^sub>1_impl\. When we later on include \proc\<^sub>1_impl\ or prove +another theorem in locale \proc\<^sub>1_impl\ the lemma \proc\<^sub>1_modifies\ will already be available as fact. -\isacommand{lemma} (\isacommand{in} @{text "proc\<^sub>1_impl"}) @{text "proc\<^sub>1_spec"}:\\ -\isacommand{shows} @{text "\"} +\isacommand{lemma} (\isacommand{in} \proc\<^sub>1_impl\) \proc\<^sub>1_spec\:\\ +\isacommand{shows} \\\ -\isacommand{lemma} (\isacommand{in} @{text "proc\<^sub>2_impl"}) @{text "proc\<^sub>2_modifies"}:\\ -\isacommand{shows} @{text "\"} +\isacommand{lemma} (\isacommand{in} \proc\<^sub>2_impl\) \proc\<^sub>2_modifies\:\\ +\isacommand{shows} \\\ -\isacommand{lemma} (\isacommand{in} @{text "proc\<^sub>2_impl"}) @{text "proc\<^sub>2_spec"}:\\ -\isacommand{shows} @{text "\"} +\isacommand{lemma} (\isacommand{in} \proc\<^sub>2_impl\) \proc\<^sub>2_spec\:\\ +\isacommand{shows} \\\ -\isacommand{lemma} (\isacommand{in} @{text "proc_impl"}) @{text "proc_modifies"}:\\ -\isacommand{shows} @{text "\"} +\isacommand{lemma} (\isacommand{in} \proc_impl\) \proc_modifies\:\\ +\isacommand{shows} \\\ -Note that we do not explicitly include anything about @{text "proc\<^sub>1"} or -@{text "proc\<^sub>2"} here. This is handled automatically. When defining -an @{text impl}-locale it imports all @{text impl}-locales of procedures that are -called in the body. In case of @{text "proc_impl"} this means, that @{text "proc\<^sub>1_impl"} -and @{text "proc\<^sub>2_impl"} are imported. This has the neat effect that all theorems that -are proven in @{text "proc\<^sub>1_impl"} and @{text "proc\<^sub>2_impl"} are also present -in @{text "proc_impl"}. +Note that we do not explicitly include anything about \proc\<^sub>1\ or +\proc\<^sub>2\ here. This is handled automatically. When defining +an \impl\-locale it imports all \impl\-locales of procedures that are +called in the body. In case of \proc_impl\ this means, that \proc\<^sub>1_impl\ +and \proc\<^sub>2_impl\ are imported. This has the neat effect that all theorems that +are proven in \proc\<^sub>1_impl\ and \proc\<^sub>2_impl\ are also present +in \proc_impl\. -\isacommand{lemma} (\isacommand{in} @{text "proc_impl"}) @{text "proc_spec"}:\\ -\isacommand{shows} @{text "\"} +\isacommand{lemma} (\isacommand{in} \proc_impl\) \proc_spec\:\\ +\isacommand{shows} \\\ As we have seen in this example you only have to prove a procedure in its own -@{text "impl"} locale. You do not have to include any other locale. -*} +\impl\ locale. You do not have to include any other locale. +\ -subsection {* Records \label{sec:records}*} +subsection \Records \label{sec:records}\ -text {* +text \ Before @{term "statespaces"} where introduced the state was represented as a @{term "record"}. This is still supported. Compared to the flexibility of statespaces there are some drawbacks in particular with respect to modularity. Even names of local variables and @@ -1453,18 +1453,18 @@ statespaces also allow multiple inheritance. The usage of records is quite simil We repeat the example of an append function for heap lists. First we define the global components. Again the appearance of the prefix `globals' is mandatory. This is the way the syntax layer distinguishes local and global variables. -*} +\ record globals_list = next_' :: "ref \ ref" cont_' :: "ref \ nat" -text {* The local variables also have to be defined as a record before the actual definition -of the procedure. The parent record @{text "state"} defines a generic @{term "globals"} +text \The local variables also have to be defined as a record before the actual definition +of the procedure. The parent record \state\ defines a generic @{term "globals"} field as a place-holder for the record of global components. In contrast to the statespace approach there is no single @{term "locals"} slot. The local components are just added to the record. -*} +\ record 'g list_vars = "'g state" + p_' :: "ref" q_' :: "ref" @@ -1472,20 +1472,20 @@ record 'g list_vars = "'g state" + root_' :: "ref" tmp_' :: "ref" -text {* Since the parameters and local variables are determined by the record, there are +text \Since the parameters and local variables are determined by the record, there are no type annotations or definitions of local variables while defining a procedure. -*} +\ procedures append'(p,q|p) = "IF \p=Null THEN \p :== \q ELSE \p \\next:== CALL append'(\p\\next,\q) FI" -text {* As in the statespace approach, a locale called @{text "append'_impl"} is created. +text \As in the statespace approach, a locale called \append'_impl\ is created. Note that we do not give any explicit information which global or local state-record to use. Since the records are already defined we rely on Isabelle's type inference. Dealing with the locale is analogous to the case with statespaces. -*} +\ lemma (in append'_impl) append'_modifies: shows @@ -1506,34 +1506,34 @@ lemma (in append'_impl) append'_spec: done -text {* +text \ However, in some corner cases the inferred state type in a procedure definition can be too general which raises problems when attempting to proof a suitable specifications in the locale. Consider for example the simple procedure body @{term "\p :== NULL"} for a procedure -@{text "init"}. -*} +\init\. +\ procedures init (|p) = "\p:== Null" -text {* +text \ Here Isabelle can only infer the local variable record. Since no reference to any global variable is -made the type fixed for the global variables (in the locale @{text "init'_impl"}) is a +made the type fixed for the global variables (in the locale \init'_impl\) is a type variable say @{typ "'g"} and not a @{term "globals_list"} record. Any specification mentioning @{term "next"} or @{term "cont"} restricts the state type and cannot be -added to the locale @{text "init_impl"}. Hence we have to restrict the body +added to the locale \init_impl\. Hence we have to restrict the body @{term "\p :== NULL"} in the first place by adding a typing annotation: -*} +\ procedures init' (|p) = "\p:== Null::(('a globals_list_scheme, 'b) list_vars_scheme, char list, 'c) com" -subsubsection {* Extending State Spaces *} -text {* +subsubsection \Extending State Spaces\ +text \ The records in Isabelle are extensible \cite{Nipkow-02-hol,NaraschewskiW-TPHOLs98}. In principle this can be exploited during verification. The state space can be extended while we we add procedures. @@ -1543,14 +1543,14 @@ But there is one major drawback: \end{itemize} You can extend both the main state record as well as the record for the global variables. -*} +\ -subsubsection {* Mapping Variables to Record Fields *} +subsubsection \Mapping Variables to Record Fields\ -text {* +text \ Generally the state space (global and local variables) is flat and all components are accessible from everywhere. Locality or globality of variables is achieved by -the proper @{text "init"} and @{text "return"}/@{text "result"} functions in procedure +the proper \init\ and \return\/\result\ functions in procedure calls. What is the best way to map programming language variables to the state records? One way is to disambiguate all names, by using the procedure names as prefix or the structure names for heap components. This leads to long names and lots of @@ -1559,8 +1559,8 @@ variable @{term i} of procedure @{term A} and variable @{term "i"} of procedure can be mapped to the same record component, without any harm, provided they have the same logical type. Therefor for local variables it is preferable to map them per type. You only have to distinguish a variable with the same name if they have a different type. -Note that all pointers just have logical type @{text "ref"}. So you even do not -have to distinguish between a pointer @{text p} to a integer and a pointer @{text p} to +Note that all pointers just have logical type \ref\. So you even do not +have to distinguish between a pointer \p\ to a integer and a pointer \p\ to a list. For global components (global variables and heap structures) you have to disambiguate the name. But hopefully the field names of structures have different names anyway. @@ -1569,16 +1569,16 @@ the logic. You have to disambiguate global and local names! As the names of the components show up in the specifications and the proof obligations, names are even more important as for programming. Try to find meaningful and short names, to avoid cluttering up your reasoning. -*} +\ (*<*) -text {* +text \ in locales, includes, spec or impl? Names: per type not per procedure\ downgrading total to partial\ -*} +\ (*>*) -text {**} +text \\ (*<*) end (*>*) diff --git a/tools/c-parser/Simpl/Vcg.thy b/tools/c-parser/Simpl/Vcg.thy index 6705832d7..95a6b8046 100644 --- a/tools/c-parser/Simpl/Vcg.thy +++ b/tools/c-parser/Simpl/Vcg.thy @@ -25,7 +25,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Facilitating the Hoare Logic *} +section \Facilitating the Hoare Logic\ theory Vcg imports StateSpace "~~/src/HOL/Statespace/StateSpaceLocale" Generalise keywords "procedures" "hoarestate" :: thy_decl @@ -51,11 +51,11 @@ method_setup vcg_step = "Hoare.vcg_step" method_setup hoare_rule = "Hoare.hoare_rule" "apply single hoare rule and solve certain sideconditions" -text {* Variables of the programming language are represented as components +text \Variables of the programming language are represented as components of a record. To avoid cluttering up the namespace of Isabelle with lots of typical variable names, we append a unusual suffix at the end of each name by parsing -*} +\ definition list_multsel:: "'a list \ nat list \ 'a list" (infixl "!!" 100) where "xs !! ns = map (nth xs) ns" @@ -66,7 +66,7 @@ definition list_multupd:: "'a list \ nat list \ 'a list nonterminal lmupdbinds and lmupdbind syntax - -- {* multiple list update *} + \ \multiple list update\ "_lmupdbind":: "['a, 'a] => lmupdbind" ("(2_ [:=]/ _)") "" :: "lmupdbind => lmupdbinds" ("_") "_lmupdbinds" :: "[lmupdbind, lmupdbinds] => lmupdbinds" ("_,/ _") @@ -77,14 +77,14 @@ translations "xs[is[:=]ys]" == "CONST list_multupd xs is ys" -subsection {* Some Fancy Syntax *} +subsection \Some Fancy Syntax\ (* priority guidline: * If command should be atomic for the guard it must have at least priority 21. *) -text {* reverse application *} +text \reverse application\ definition rapp:: "'a \ ('a \ 'b) \ 'b" (infixr "|>" 60) where "rapp x f = f x" @@ -298,25 +298,25 @@ translations "(_switchcasesCons b bs)" => "CONST Cons b bs" "(_Switch v vs)" => "CONST switch (_quote v) vs" -parse_ast_translation {* +parse_ast_translation \ let fun tr c asts = Ast.mk_appl (Ast.Constant c) (map Ast.strip_positions asts) in [(@{syntax_const "_antiquoteCur0"}, K (tr @{syntax_const "_antiquoteCur"})), (@{syntax_const "_antiquoteOld0"}, K (tr @{syntax_const "_antiquoteOld"}))] end -*} +\ -print_ast_translation {* +print_ast_translation \ let fun tr c asts = Ast.mk_appl (Ast.Constant c) asts in [(@{syntax_const "_antiquoteCur"}, K (tr @{syntax_const "_antiquoteCur0"})), (@{syntax_const "_antiquoteOld"}, K (tr @{syntax_const "_antiquoteOld0"}))] end -*} +\ -print_ast_translation {* +print_ast_translation \ let fun dest_abs (Ast.Appl [Ast.Constant @{syntax_const "_abs"}, x, t]) = (x, t) | dest_abs _ = raise Match; @@ -343,7 +343,7 @@ print_ast_translation {* [(@{const_syntax specAnno}, K spec_tr'), (@{const_syntax whileAnnoFix}, K whileAnnoFix_tr')] end -*} +\ @@ -424,7 +424,7 @@ definition Let':: "['a, 'a => 'b] => 'b" ML_file "hoare_syntax.ML" -parse_translation {* +parse_translation \ let val argsC = @{syntax_const "_modifyargs"}; val globalsN = "globals"; @@ -461,10 +461,10 @@ parse_translation {* [(@{syntax_const "_may_modify"}, may_modify_tr), (@{syntax_const "_may_not_modify"}, may_not_modify_tr)] end; -*} +\ -print_translation {* +print_translation \ let val argsC = @{syntax_const "_modifyargs"}; val chop = Hoare.chopsfx Hoare.deco; @@ -499,7 +499,7 @@ print_translation {* [(@{const_syntax mex}, K may_modify_tr'), (@{const_syntax meq}, K may_not_modify_tr')] end; -*} +\ (* decorate state components with suffix *) @@ -520,13 +520,13 @@ parse_ast_translation {* *) -parse_translation {* +parse_translation \ [(@{syntax_const "_antiquoteCur"}, K (Hoare_Syntax.antiquote_varname_tr @{syntax_const "_antiquoteCur"}))] -*} +\ -parse_translation {* +parse_translation \ [(@{syntax_const "_antiquoteOld"}, Hoare_Syntax.antiquoteOld_tr), (@{syntax_const "_Call"}, Hoare_Syntax.call_tr false false), (@{syntax_const "_FCall"}, Hoare_Syntax.fcall_tr), @@ -540,7 +540,7 @@ parse_translation {* (@{syntax_const "_GuardedDynCall"}, Hoare_Syntax.call_tr true true), (@{syntax_const "_GuardedDynCallAss"}, Hoare_Syntax.call_ass_tr true true), (@{syntax_const "_BasicBlock"}, Hoare_Syntax.basic_assigns_tr)] -*} +\ (* (@{syntax_const "_Call"}, Hoare_Syntax.call_ast_tr), @@ -549,16 +549,16 @@ parse_translation {* (@{syntax_const "_GuardedCallAss"}, Hoare_Syntax.guarded_call_ass_ast_tr) *) -parse_translation {* +parse_translation \ let fun quote_tr ctxt [t] = Hoare_Syntax.quote_tr ctxt @{syntax_const "_antiquoteCur"} t | quote_tr ctxt ts = raise TERM ("quote_tr", ts); in [(@{syntax_const "_quote"}, quote_tr)] end -*} +\ -parse_translation {* +parse_translation \ [(@{syntax_const "_Assign"}, Hoare_Syntax.assign_tr), (@{syntax_const "_raise"}, Hoare_Syntax.raise_tr), (@{syntax_const "_New"}, Hoare_Syntax.new_tr), @@ -570,15 +570,15 @@ parse_translation {* (@{syntax_const "_GuardedWhileFix_inv_var_hook"}, Hoare_Syntax.guarded_WhileFix_tr), (@{syntax_const "_GuardedCond"}, Hoare_Syntax.guarded_Cond_tr), (@{syntax_const "_Basic"}, Hoare_Syntax.basic_tr)] -*} +\ -parse_translation {* +parse_translation \ [(@{syntax_const "_Init"}, Hoare_Syntax.init_tr), (@{syntax_const "_Loc"}, Hoare_Syntax.loc_tr)] -*} +\ -print_translation {* +print_translation \ [(@{const_syntax Basic}, Hoare_Syntax.assign_tr'), (@{const_syntax raise}, Hoare_Syntax.raise_tr'), (@{const_syntax Basic}, Hoare_Syntax.new_tr'), @@ -593,10 +593,10 @@ print_translation {* (@{const_syntax whileAnnoG}, Hoare_Syntax.whileAnnoG_tr'), (@{const_syntax whileAnnoGFix}, Hoare_Syntax.whileAnnoGFix_tr'), (@{const_syntax bind}, Hoare_Syntax.bind_tr')] -*} +\ -print_translation {* +print_translation \ let fun spec_tr' ctxt ((coll as Const _)$ ((splt as Const _) $ (t as (Abs (s,T,p))))::ts) = @@ -614,7 +614,7 @@ print_translation {* end | spec_tr' _ ts = raise Match in [(@{const_syntax Spec}, spec_tr')] end -*} +\ syntax "_Measure":: "('a \ nat) \ ('a \ 'a) set" @@ -629,7 +629,7 @@ translations -print_translation {* +print_translation \ let fun selector (Const (c,T)) = Hoare.is_state_var c | selector _ = false; @@ -650,14 +650,14 @@ print_translation {* [(@{const_syntax measure}, measure_tr'), (@{const_syntax mlex_prod}, mlex_tr')] end -*} +\ -print_translation {* +print_translation \ [(@{const_syntax call}, Hoare_Syntax.call_tr'), (@{const_syntax dynCall}, Hoare_Syntax.dyn_call_tr'), (@{const_syntax fcall}, Hoare_Syntax.fcall_tr'), (@{const_syntax Call}, Hoare_Syntax.proc_tr')] -*} +\ -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/XVcg.thy b/tools/c-parser/Simpl/XVcg.thy index eb39460dd..73612073b 100644 --- a/tools/c-parser/Simpl/XVcg.thy +++ b/tools/c-parser/Simpl/XVcg.thy @@ -32,11 +32,11 @@ imports Vcg begin -text {* We introduce a syntactic variant of the let-expression so that we can +text \We introduce a syntactic variant of the let-expression so that we can safely unfold it during verification condition generation. With the new -theorem attribute @{text "vcg_simp"} we can declare equalities to be used +theorem attribute \vcg_simp\ we can declare equalities to be used by the verification condition generator, while simplifying assertions. -*} +\ syntax "_Let'" :: "[letbinds, basicblock] => basicblock" ("(LET (_)/ IN (_))" 23) @@ -54,4 +54,4 @@ lemma Let'_split_conv [vcg_simp]: (Let' x (\p. (f p) (fst (g p)) (snd (g p))))" by (simp add: split_def) -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/ex/Closure.thy b/tools/c-parser/Simpl/ex/Closure.thy index 3888f86b4..5a4ad5677 100644 --- a/tools/c-parser/Simpl/ex/Closure.thy +++ b/tools/c-parser/Simpl/ex/Closure.thy @@ -303,7 +303,7 @@ lemma app_closure_spec: apply blast done -text {* Implementation of closures as association lists. *} +text \Implementation of closures as association lists.\ definition "gen_upd var es s = foldl (\s (x,i). the (var x) i s) s es" definition "ap es c \ (es@fst c,snd c)" @@ -349,4 +349,4 @@ proof - by (simp add: c ap_def) qed -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/ex/ClosureEx.thy b/tools/c-parser/Simpl/ex/ClosureEx.thy index 056253641..ab0f7c69b 100644 --- a/tools/c-parser/Simpl/ex/ClosureEx.thy +++ b/tools/c-parser/Simpl/ex/ClosureEx.thy @@ -262,4 +262,4 @@ apply (erule allE) apply assumption done -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/ex/Compose.thy b/tools/c-parser/Simpl/ex/Compose.thy index 528f7308d..d35f42961 100644 --- a/tools/c-parser/Simpl/ex/Compose.thy +++ b/tools/c-parser/Simpl/ex/Compose.thy @@ -31,14 +31,14 @@ section "Experiments on State Composition" theory Compose imports "../HoareTotalProps" begin -text {* +text \ We develop some theory to support state-space modular development of programs. These experiments aim at the representation of state-spaces with records. -If we use @{text "statespaces"} instead we get this kind of compositionality for free. -*} +If we use \statespaces\ instead we get this kind of compositionality for free. +\ -subsection {* Changing the State-Space *} +subsection \Changing the State-Space\ (* Lift a command on statespace 'b to work on statespace 'a *) @@ -269,15 +269,15 @@ lemma (in lift_state_space) lift\<^sub>e_def': -text {* +text \ The problem is that @{term "(lift\<^sub>c project inject \ \)"} is quite a strong premise. The problem is that @{term "\"} is a function here. A map would be better. We only have to lift those procedures in the domain of @{term "\"}: -@{text "\ p = Some bdy \ \' p = Some lift\<^sub>c project inject bdy"}. +\\ p = Some bdy \ \' p = Some lift\<^sub>c project inject bdy\. We then can com up with theorems that allow us to extend the domains of @{term \} and preserve validity. -*} +\ lemma (in lift_state_space) @@ -885,17 +885,15 @@ proof (rule validI) Normal ` (Modif (project s)) \ Abrupt ` (ModifAbr (project s))" using valid [rule_format, of "(project s)"] by (auto simp add: valid_def project\<^sub>x_def) - hence "t \ Normal ` lift\<^sub>s (Modif (project s)) \ + hence t: "t \ Normal ` lift\<^sub>s (Modif (project s)) \ Abrupt ` lift\<^sub>s (ModifAbr (project s))" by (cases t) (auto simp add: project\<^sub>x_def lift\<^sub>s_def Compose.lift\<^sub>s_def) - moreover - from this - have "t \ Fault ` UNIV \ {Stuck}" + then have "t \ Fault ` UNIV \ {Stuck}" by (cases t) auto from lift_exec_inject_same [OF exec _ this] have "state t = inject (state (Normal s)) (project (state t))" by simp - ultimately show ?thesis + with t show ?thesis using P by auto qed qed @@ -925,7 +923,7 @@ apply (rule HoarePartialDef.conseq [OF hoare_lift_modifies [OF deriv]]) apply blast done -subsection {* Renaming Procedures *} +subsection \Renaming Procedures\ primrec rename:: "('p \ 'q) \ ('s,'p,'f) com \ ('s,'q,'f) com" where diff --git a/tools/c-parser/Simpl/ex/Quicksort.thy b/tools/c-parser/Simpl/ex/Quicksort.thy index 58568f42c..75f559461 100644 --- a/tools/c-parser/Simpl/ex/Quicksort.thy +++ b/tools/c-parser/Simpl/ex/Quicksort.thy @@ -278,4 +278,4 @@ apply (erule_tac x=x in allE)+ apply (force dest!: perm_set_eq) done -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/ex/VcgEx.thy b/tools/c-parser/Simpl/ex/VcgEx.thy index f0915a435..099e929fc 100644 --- a/tools/c-parser/Simpl/ex/VcgEx.thy +++ b/tools/c-parser/Simpl/ex/VcgEx.thy @@ -26,21 +26,21 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Examples using the Verification Environment *} +section \Examples using the Verification Environment\ theory VcgEx imports "../HeapList" "../Vcg" begin -text {* Some examples, especially the single-step Isar proofs are taken from +text \Some examples, especially the single-step Isar proofs are taken from \texttt{HOL/Isar\_examples/HoareEx.thy}. -*} +\ -subsection {* State Spaces *} +subsection \State Spaces\ -text {* +text \ First of all we provide a store of program variables that occur in the programs considered later. Slightly unexpected things may happen when attempting to work with undeclared variables. -*} +\ record 'g vars = "'g state" + A_' :: nat @@ -55,57 +55,57 @@ record 'g vars = "'g state" + -text {* We decorate the state components in the record with the suffix @{text "_'"}, +text \We decorate the state components in the record with the suffix \_'\, to avoid cluttering the namespace with the simple names that could no longer be used for logical variables otherwise. -*} +\ -text {* We will first consider programs without procedures, later on +text \We will first consider programs without procedures, later on we will regard procedures without global variables and finally we will get the full pictures: mutually recursive procedures with global variables (including heap). -*} +\ -subsection {* Basic Examples *} +subsection \Basic Examples\ -text {* +text \ We look at few trivialities involving assignment and sequential composition, in order to get an idea of how to work with our formulation of Hoare Logic. -*} +\ -text {* +text \ Using the basic rule directly is a bit cumbersome. -*} +\ lemma "\\ {|\N = 5|} \N :== 2 * \N {|\N = 10|}" apply (rule HoarePartial.Basic) apply simp done -text {* +text \ If we refer to components (variables) of the state-space of the program - we always mark these with @{text "\"}. It is the acute-symbol and is present on + we always mark these with \\\. It is the acute-symbol and is present on most keyboards. So all program variables are marked with the acute and all logical variables are not. The assertions of the Hoare tuple are ordinary Isabelle sets. As we usually want to refer to the state space in the assertions, we provide special brackets for them. They can be written - as {\verb+{| |}+} in ASCII or @{text "\ \"} with symbols. Internally + as {\verb+{| |}+} in ASCII or \\ \\ with symbols. Internally marking variables has two effects. First of all we refer to the implicit - state and secondary we get rid of the suffix @{text "_'"}. + state and secondary we get rid of the suffix \_'\. So the assertion @{term "{|\N = 5|}"} internally gets expanded to - @{text "{s. N_' s = 5}"} written in ordinary set comprehension notation of - Isabelle. It describes the set of states where the @{text "N_'"} component - is equal to @{text "5"}. -*} + \{s. N_' s = 5}\ written in ordinary set comprehension notation of + Isabelle. It describes the set of states where the \N_'\ component + is equal to \5\. +\ -text {* +text \ Certainly we want the state modification already done, e.g.\ by - simplification. The @{text vcg} method performs the basic state + simplification. The \vcg\ method performs the basic state update for us; we may apply the Simplifier afterwards to achieve ``obvious'' consequences as well. -*} +\ lemma "\\ \True\ \N :== 10 \\N = 10\" @@ -138,10 +138,10 @@ lemma "\\ \\M = a \ \N = b\ \\M = b \ \N = a\" by vcg -text {* +text \ We can also perform verification conditions generation step by step by using -the @{text vcg_step} method. -*} +the \vcg_step\ method. +\ lemma "\\ \\M = a \ \N = b\ \I :== \M;; \M :== \N;; \N :== \I @@ -152,12 +152,12 @@ lemma "\\ \\M = a \ \N = b\ apply vcg_step done -text {* +text \ It is important to note that statements like the following one can only be proven for each individual program variable. Due to the extra-logical nature of record fields, we cannot formulate a theorem relating record selectors and updates schematically. -*} +\ lemma "\\ \\N = a\ \N :== \N \\N = a\" by vcg @@ -173,11 +173,11 @@ lemma "\\{s. x_' s = a} (Basic (\s. x_'_update (x_' s) oops -text {* +text \ In the following assignments we make use of the consequence rule in order to achieve the intended precondition. Certainly, the - @{text vcg} method is able to handle this case, too. -*} + \vcg\ method is able to handle this case, too. +\ lemma "\\ \\M = \N\ \M :== \M + 1 \\M \ \N\" proof - @@ -191,8 +191,8 @@ qed lemma "\\ \\M = \N\ \M :== \M + 1 \\M \ \N\" proof - have "\m n::nat. m = n \ m + 1 \ n" - -- {* inclusion of assertions expressed in ``pure'' logic, *} - -- {* without mentioning the state space *} + \ \inclusion of assertions expressed in ``pure'' logic,\ + \ \without mentioning the state space\ by simp also have "\\ \\M + 1 \ \N\ \M :== \M + 1 \\M \ \N\" by vcg @@ -204,14 +204,14 @@ lemma "\\ \\M = \N\ \M := apply simp done -subsection {* Multiplication by Addition *} +subsection \Multiplication by Addition\ -text {* +text \ We now do some basic examples of actual \texttt{WHILE} programs. This one is a loop for calculating the product of two natural numbers, by iterated addition. We first give detailed structured proof based on single-step Hoare rules. -*} +\ lemma "\\ \\M = 0 \ \S = 0\ WHILE \M \ a @@ -235,12 +235,12 @@ proof - qed -text {* - The subsequent version of the proof applies the @{text vcg} method +text \ + The subsequent version of the proof applies the \vcg\ method to reduce the Hoare statement to a purely logical problem that can be solved fully automatically. Note that we have to specify the \texttt{WHILE} loop invariant in the original statement. -*} +\ lemma "\\ \\M = 0 \ \S = 0\ WHILE \M \ a @@ -251,7 +251,7 @@ lemma "\\ \\M = 0 \ \S = 0\ apply auto done -text {* Here some examples of ``breaking'' out of a loop *} +text \Here some examples of ``breaking'' out of a loop\ lemma "\\ \\M = 0 \ \S = 0\ TRY @@ -283,10 +283,10 @@ apply auto done -text {* Some more syntactic sugar, the label statement @{text "\ \ \"} as shorthand -for the @{text "TRY-CATCH"} above, and the @{text "RAISE"} for an state-update followed -by a @{text "THROW"}. -*} +text \Some more syntactic sugar, the label statement \\ \ \\ as shorthand +for the \TRY-CATCH\ above, and the \RAISE\ for an state-update followed +by a \THROW\. +\ lemma "\\ \\M = 0 \ \S = 0\ \\Abr = ''Break''\\ WHILE True INV \\S = \M * b\ DO IF \M = a THEN RAISE \Abr :== ''Break'' @@ -326,7 +326,7 @@ apply vcg apply auto done -text {* Blocks *} +text \Blocks\ lemma "\\\\I = i\ LOC \I;; \I :== 2 COL \\I \ i\" apply vcg @@ -338,13 +338,13 @@ lemma "\\ \\N = n\ LOC \N :== 10 by vcg -subsection {* Summing Natural Numbers *} +subsection \Summing Natural Numbers\ -text {* +text \ We verify an imperative program to sum natural numbers up to a given limit. First some functional definition for proper specification of the problem. -*} +\ primrec sum :: "(nat => nat) => nat => nat" @@ -358,13 +358,13 @@ syntax translations "SUMM jj. b) k" -text {* +text \ The following proof is quite explicit in the individual steps taken, - with the @{text vcg} method only applied locally to take care of + with the \vcg\ method only applied locally to take care of assignment and sequential composition. Note that we express intermediate proof obligation in pure logic, without referring to the state space. -*} +\ theorem "\\ \True\ \S :== 0;; \I :== 1;; @@ -401,10 +401,10 @@ proof - finally show ?thesis . qed -text {* - The next version uses the @{text vcg} method, while still explaining +text \ + The next version uses the \vcg\ method, while still explaining the resulting proof obligations in an abstract, structured manner. -*} +\ theorem "\\ \True\ \S :== 0;; \I :== 1;; @@ -431,10 +431,10 @@ proof - qed qed -text {* +text \ Certainly, this proof may be done fully automatically as well, provided that the invariant is given beforehand. -*} +\ theorem "\\ \True\ \S :== 0;; \I :== 1;; @@ -449,7 +449,7 @@ theorem "\\ \True\ apply auto done -subsection {* SWITCH *} +subsection \SWITCH\ lemma "\\ \\N = 5\ SWITCH \B {True} \ \N :== 6 @@ -469,13 +469,13 @@ apply vcg apply simp done -subsection {* (Mutually) Recursive Procedures *} +subsection \(Mutually) Recursive Procedures\ -subsubsection {* Factorial *} +subsubsection \Factorial\ -text {* We want to define a procedure for the factorial. We first +text \We want to define a procedure for the factorial. We first define a HOL functions that calculates it to specify the procedure later on. -*} +\ primrec fac:: "nat \ nat" where @@ -485,7 +485,7 @@ where lemma fac_simp [simp]: "0 < i \ fac i = i * fac (i - 1)" by (cases i) simp_all -text {* Now we define the procedure *} +text \Now we define the procedure\ procedures Fac (N|R) = "IF \N = 0 THEN \R :== 1 @@ -495,23 +495,23 @@ procedures -text {* A procedure is given by the signature of the procedure +text \A procedure is given by the signature of the procedure followed by the procedure body. The signature consists of the name of the procedure and a list of -parameters. The parameters in front of the pipe @{text "|"} are value parameters +parameters. The parameters in front of the pipe \|\ are value parameters and behind the pipe are the result parameters. Value parameters model call by value semantics. The value of a result parameter at the end of the procedure is passed back to the caller. -*} +\ -text {* -Behind the scenes the @{text "procedures"} command provides us convenient syntax +text \ +Behind the scenes the \procedures\ command provides us convenient syntax for procedure calls, defines a constant for the procedure body (named @{term "Fac_body"}) and creates some locales. The purpose of locales is to set up logical contexts to support modular reasoning. -A locale is named @{text Fac_impl} and extends the @{text hoare} locale +A locale is named \Fac_impl\ and extends the \hoare\ locale with a theorem @{term "\ ''Fac'' = Fac_body"} that simply states how the procedure is defined in the procedure context. Check out the locales. The purpose of the locales is to give us easy means to setup the context @@ -520,40 +520,40 @@ In these locales the procedure context @{term "\"} is fixed. So always use this letter in procedure specifications. This is crucial, if we later on prove some tuples under the assumption of some procedure specifications. -*} +\ thm Fac_body.Fac_body_def print_locale Fac_impl -text {* +text \ To see how a call is syntactically translated you can switch off the -printing translation via the configuration option @{text hoare_use_call_tr'} -*} +printing translation via the configuration option \hoare_use_call_tr'\ +\ context Fac_impl begin -text {* +text \ @{term "CALL Fac(\N,\M)"} is internally: -*} +\ declare [[hoare_use_call_tr' = false]] -text {* +text \ @{term "CALL Fac(\N,\M)"} -*} +\ term "CALL Fac(\N,\M)" declare [[hoare_use_call_tr' = true]] end -text {* +text \ Now let us prove that @{term "Fac"} meets its specification. -*} +\ -text {* +text \ Procedure specifications are ordinary Hoare tuples. We use the parameterless -call for the specification; @{text "\R :== PROC Fac(\N)"} is syntactic sugar -for @{text "Call ''Fac''"}. This emphasises that the specification +call for the specification; \\R :== PROC Fac(\N)\ is syntactic sugar +for \Call ''Fac''\. This emphasises that the specification describes the internal behaviour of the procedure, whereas parameter passing corresponds to the procedure call. -*} +\ lemma (in Fac_impl) @@ -564,7 +564,7 @@ lemma (in Fac_impl) done -text {* +text \ Since the factorial was implemented recursively, the main ingredient of this proof is, to assume that the specification holds for the recursive call of @{term Fac} and prove the body correct. @@ -574,13 +574,13 @@ the rule @{thm [source] HoarePartial.ProcRec1} @{thm [display] HoarePartial.ProcRec1 [no_vars]} The verification condition generator will infer the specification out of the context when it encounters a recursive call of the factorial. -*} +\ -text {* We can also step through verification condition generation. When +text \We can also step through verification condition generation. When the verification condition generator encounters a procedure call it tries to -use the rule @{text ProcSpec}. To be successful there must be a specification +use the rule \ProcSpec\. To be successful there must be a specification of the procedure in the context. -*} +\ lemma (in Fac_impl) shows "\n. \\\\N=n\ \R :== PROC Fac(\N) \\R = fac n\" @@ -594,7 +594,7 @@ lemma (in Fac_impl) done -text {* Here some Isar style version of the proof *} +text \Here some Isar style version of the proof\ lemma (in Fac_impl) shows "\n. \\\\N=n\ \R :== PROC Fac(\N) \\R = fac n\" proof (hoare_rule HoarePartial.ProcRec1) @@ -611,10 +611,10 @@ proof (hoare_rule HoarePartial.ProcRec1) done qed -text {* To avoid retyping of potentially large pre and postconditions in +text \To avoid retyping of potentially large pre and postconditions in the previous proof we can use the casual term abbreviations of the Isar language. -*} +\ lemma (in Fac_impl) shows "\n. \\\\N=n\ \R :== PROC Fac(\N) \\R = fac n\" @@ -633,24 +633,24 @@ proof (hoare_rule HoarePartial.ProcRec1) done qed -text {* The previous proof pattern has still some kind of inconvenience. +text \The previous proof pattern has still some kind of inconvenience. The augmented context is always printed in the proof state. That can mess up the state, especially if we have large specifications. This may be annoying if we want to develop single step or structured proofs. In this case it can be a good idea to introduce a new variable for the augmented context. -*} +\ lemma (in Fac_impl) Fac_spec: shows "\n. \\\\N=n\ \R :== PROC Fac(\N) \\R = fac n\" (is "\n. \\(?Pre n) ?Fac (?Post n)") proof (hoare_rule HoarePartial.ProcRec1) - def "\'"=="(\n. {(?Pre n, Fac_'proc, ?Post n,{}::('a, 'b) vars_scheme set)})" + define \' where "\' = (\n. {(?Pre n, Fac_'proc, ?Post n,{}::('a, 'b) vars_scheme set)})" have Fac_spec: "\n. \,\'\(?Pre n) ?Fac (?Post n)" by (unfold \'_def, rule allI, rule hoarep.Asm) auto - txt {* We have to name the fact @{text "Fac_spec"}, so that the vcg can + txt \We have to name the fact \Fac_spec\, so that the vcg can use the specification for the recursive call, since it cannot infer it - from the opaque @{term "\'"}. *} + from the opaque @{term "\'"}.\ show "\\. \,\'\ (?Pre \) IF \N = 0 THEN \R :== 1 ELSE \R :== CALL Fac(\N - 1);; \R :== \N * \R FI (?Post \)" apply vcg @@ -658,7 +658,7 @@ proof (hoare_rule HoarePartial.ProcRec1) done qed -text {* There are different rules available to prove procedure calls, +text \There are different rules available to prove procedure calls, depending on the kind of postcondition and whether or not the procedure is recursive or even mutually recursive. See for example @{thm [source] HoarePartial.ProcRec1}, @@ -668,15 +668,15 @@ They are all derived from the most general rule All of them have some side-condition concerning definedness of the procedure. They can be solved in a uniform fashion. Thats why we have created the method -@{text "hoare_rule"}, which behaves like the method @{text "rule"} but automatically +\hoare_rule\, which behaves like the method \rule\ but automatically tries to solve the side-conditions. -*} +\ -subsubsection {* Odd and Even *} +subsubsection \Odd and Even\ -text {* Odd and even are defined mutually recursive here. In the -@{text "procedures"} command we conjoin both definitions with @{text "and"}. -*} +text \Odd and even are defined mutually recursive here. In the +\procedures\ command we conjoin both definitions with \and\. +\ procedures odd(N | A) = "IF \N=0 THEN \A:==0 @@ -699,14 +699,14 @@ thm even_body.even_body_def print_locale odd_even_clique -text {* To prove the procedure calls to @{term "odd"} respectively +text \To prove the procedure calls to @{term "odd"} respectively @{term "even"} correct we first derive a rule to justify that we can assume both specifications to verify the bodies. This rule can be derived from the general @{thm [source] HoarePartial.ProcRec} rule. An ML function does this work: -*} +\ -ML {* ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2) *} +ML \ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2)\ lemma (in odd_even_clique) @@ -729,10 +729,10 @@ proof - by iprover+ qed -subsection {*Expressions With Side Effects *} +subsection \Expressions With Side Effects\ -text {* \texttt{R := N++ + M++} *} +text \\texttt{R := N++ + M++}\ lemma "\\ \True\ \N \ n. \N :== \N + 1 \ \M \ m. \M :== \M + 1 \ @@ -742,7 +742,7 @@ apply vcg apply simp done -text {*\texttt{R := Fac (N) + Fac (M)} *} +text \\texttt{R := Fac (N) + Fac (M)}\ lemma (in Fac_impl) shows "\\ \True\ CALL Fac(\N) \ n. CALL Fac(\M) \ m. @@ -752,7 +752,7 @@ apply vcg done -text {*\texttt{ R := (Fac(Fac (N)))}*} +text \\texttt{ R := (Fac(Fac (N)))}\ lemma (in Fac_impl) shows "\\ \True\ CALL Fac(\N) \ n. CALL Fac(n) \ m. @@ -762,15 +762,15 @@ apply vcg done -subsection {* Global Variables and Heap *} +subsection \Global Variables and Heap\ -text {* +text \ Now we define and verify some procedures on heap-lists. We consider list structures consisting of two fields, a content element @{term "cont"} and a reference to the next list element @{term "next"}. We model this by the following state space where every field has its own heap. -*} +\ record globals_list = next_' :: "ref \ ref" @@ -783,16 +783,16 @@ record 'g list_vars = "'g state" + root_' :: "ref" tmp_' :: "ref" -text {* Updates to global components inside a procedure will +text \Updates to global components inside a procedure will always be propagated to the caller. This is implicitly done by the parameter passing syntax translations. The record containing the global variables must begin with the prefix "globals". -*} +\ -text {* We first define an append function on lists. It takes two +text \We first define an append function on lists. It takes two references as parameters. It appends the list referred to by the first parameter with the list referred to by the second parameter, and returns the result right into the first parameter. -*} +\ procedures append(p,q|p) = @@ -815,7 +815,7 @@ declare [[hoare_use_call_tr' = false]] term "CALL append(\p,\q,\p\\next)" declare [[hoare_use_call_tr' = true]] end -text {* Below we give two specifications this time. +text \Below we give two specifications this time. One captures the functional behaviour and focuses on the entities that are potentially modified by the procedure, the other one is a pure frame condition. @@ -830,9 +830,9 @@ The functional specification now introduces two logical variables besides the state space variable @{term "\"}, namely @{term "Ps"} and @{term "Qs"}. They are universally quantified and range over both the pre and the postcondition, so that we are able to properly instantiate the specification -during the proofs. The syntax @{text "\\. \\"} is a shorthand to fix the current -state: @{text "{s. \ = s \}"}. -*} +during the proofs. The syntax \\\. \\\ is a shorthand to fix the current +state: \{s. \ = s \}\. +\ lemma (in append_impl) append_spec: shows "\\ Ps Qs. \\ @@ -845,9 +845,9 @@ lemma (in append_impl) append_spec: done -text {* The modifies clause is equal to a proper record update specification +text \The modifies clause is equal to a proper record update specification of the following form. -*} +\ lemma "{t. t may_only_modify_globals Z in [next]} @@ -857,7 +857,7 @@ lemma "{t. t may_only_modify_globals Z in [next]} apply (simp) done -text {* If the verification condition generator works on a procedure call +text \If the verification condition generator works on a procedure call it checks whether it can find a modified clause in the context. If one is present the procedure call is simplified before the Hoare rule @{thm [source] HoarePartial.ProcSpec} is applied. Simplification of the procedure call means, @@ -866,24 +866,24 @@ components that occur in the modifies clause will actually be copied back. This simplification is justified by the rule @{thm [source] HoarePartial.ProcModifyReturn}. So after this simplification all global components that do not appear in the modifies clause will be treated as local variables. -*} +\ -text {* You can study the effect of the modifies clause on the following two +text \You can study the effect of the modifies clause on the following two examples, where we want to prove that @{term "append"} does not change the @{term "cont"} part of the heap. -*} +\ lemma (in append_impl) shows "\\ \\p=Null \ \cont=c\ \p :== CALL append(\p,Null) \\cont=c\" apply vcg oops -text {* To prove the frame condition, +text \To prove the frame condition, we have to tell the verification condition generator to use only the modifies clauses and not to search for functional specifications by -the parameter @{text "spec=modifies"} It will also try to solve the +the parameter \spec=modifies\ It will also try to solve the verification conditions automatically. -*} +\ lemma (in append_impl) append_modifies: shows @@ -899,27 +899,27 @@ lemma (in append_impl) apply simp done -text {* +text \ Of course we could add the modifies clause to the functional specification as well. But separating both has the advantage that we split up the verification work. We can make use of the modifies clause before we apply the functional specification in a fully automatic fashion. -*} +\ -text {* To verify the body of @{term "append"} we do not need the modifies +text \To verify the body of @{term "append"} we do not need the modifies clause, since the specification does not talk about @{term "cont"} at all, and we don't access @{term "cont"} inside the body. This may be different for more complex procedures. -*} +\ -text {* +text \ To prove that a procedure respects the modifies clause, we only need the modifies clauses of the procedures called in the body. We do not need the functional specifications. So we can always prove the modifies clause without functional specifications, but me may need the modifies clause to prove the functional specifications. -*} +\ @@ -928,7 +928,7 @@ clause to prove the functional specifications. -subsubsection {*Insertion Sort*} +subsubsection \Insertion Sort\ primrec sorted:: "('a \ 'a \ bool) \ 'a list \ bool" where @@ -949,7 +949,7 @@ procedures FI" -text {* +text \ In the postcondition of the functional specification there is a small but important subtlety. Whenever we talk about the @{term "cont"} part we refer to the one of the pre-state, even in the conclusion of the implication. @@ -957,16 +957,16 @@ The reason is, that we have separated out, that @{term "cont"} is not modified by the procedure, to the modifies clause. So whenever we talk about unmodified parts in the postcondition we have to use the pre-state part, or explicitly state an equality in the postcondition. -The reason is simple. If the postcondition would talk about @{text "\cont"} -instead of @{text "\<^bsup>\\<^esup>cont"}, we get a new instance of @{text "cont"} during +The reason is simple. If the postcondition would talk about \\cont\ +instead of \\<^bsup>\\<^esup>cont\, we get a new instance of \cont\ during verification and the postcondition would only state something about this new instance. But as the verification condition generator uses the -modifies clause the caller of @{text "insert"} instead still has the -old @{text "cont"} after the call. Thats the very reason for the modifies clause. +modifies clause the caller of \insert\ instead still has the +old \cont\ after the call. Thats the very reason for the modifies clause. So the caller and the specification will simply talk about two different things, without being able to relate them (unless an explicit equality is added to the specification). -*} +\ lemma (in insert_impl) insert_modifies: "\\. \\ {\} \p :== PROC insert(\r,\p){t. t may_only_modify_globals \ in [next]}" @@ -1015,12 +1015,12 @@ apply (vcg spec=modifies) done -text {* Insertion sort is not implemented recursively here but with a while +text \Insertion sort is not implemented recursively here but with a while loop. Note that the while loop is not annotated with an invariant in the procedure definition. The invariant only comes into play during verification. Therefore we will annotate the body during the proof with the rule @{thm [source] HoarePartial.annotateI}. -*} +\ lemma (in insertSort_impl) insertSort_body_spec: @@ -1054,11 +1054,11 @@ lemma (in insertSort_impl) insertSort_body_spec: subsubsection "Memory Allocation and Deallocation" -text {* The basic idea of memory management is to keep a list of allocated +text \The basic idea of memory management is to keep a list of allocated references in the state space. Allocation of a new reference adds a new reference to the list deallocation removes a reference. Moreover we keep a counter "free" for the free memory. -*} +\ record globals_list_alloc = globals_list + alloc_'::"ref list" @@ -1071,7 +1071,7 @@ record 'g list_vars' = "'g list_vars" + definition "sz = (2::nat)" -text {* Restrict locale @{text hoare} to the required type. *} +text \Restrict locale \hoare\ to the required type.\ locale hoare_ex = hoare \ for \ :: "'c \ (('a globals_list_alloc_scheme, 'b) list_vars'_scheme, 'c, 'd) com" @@ -1131,14 +1131,14 @@ apply (simp add: sz_def) apply fastforce done -subsection {* Fault Avoiding Semantics *} +subsection \Fault Avoiding Semantics\ -text {* +text \ If we want to ensure that no runtime errors occur we can insert guards into the code. We will not be able to prove any nontrivial Hoare triple about code with guards, if we cannot show that the guards will never fail. A trivial hoare triple is one with an empty precondition. -*} +\ lemma "\\ \True\ \\p\Null\\ \p\\next :== \p \True\" @@ -1149,9 +1149,9 @@ lemma "\\ {} \\p\Null\\Let us consider this small program that reverts a list. At first without guards. -*} +\ lemma (in hoare_ex) rev_strip: "\\ \List \p \next Ps \ List \q \next Qs \ set Ps \ set Qs = {} \ set Ps \ set \alloc \ set Qs \ set \alloc\ @@ -1168,9 +1168,9 @@ apply (vcg) apply fastforce+ done -text {* If we want to ensure that we do not dereference @{term "Null"} or +text \If we want to ensure that we do not dereference @{term "Null"} or access unallocated memory, we have to add some guards. -*} +\ locale hoare_ex_guard = hoare \ for \ :: "'c \ (('a globals_list_alloc_scheme, 'b) list_vars'_scheme, 'c, bool) com" @@ -1193,9 +1193,9 @@ apply fastforce+ done -text {* We can also just prove that no faults will occur, by giving the +text \We can also just prove that no faults will occur, by giving the trivial postcondition. -*} +\ lemma (in hoare_ex_guard) rev_noFault: "\\ \List \p \next Ps \ List \q \next Qs \ set Ps \ set Qs = {} \ set Ps \ set \alloc \ set Qs \ set \alloc\ @@ -1251,10 +1251,10 @@ proof - qed -text {* We can then combine the prove that no fault will occur with the +text \We can then combine the prove that no fault will occur with the functional proof of the programme without guards to get the full prove by the rule @{thm HoarePartialProps.CombineStrip} -*} +\ lemma @@ -1277,15 +1277,15 @@ apply simp done -text {* In the previous example the effort to split up the prove did not +text \In the previous example the effort to split up the prove did not really pay off. But when we think of programs with a lot of guards and complicated specifications it may be better to first focus on a prove without the messy guards. Maybe it is possible to automate the no fault proofs so that it suffices to focus on the stripped program. -*} +\ -text {* +text \ The purpose of guards is to watch for faults that can occur during evaluation of expressions. In the example before we watched for null pointer dereferencing or memory faults. We can also look for array index bounds or @@ -1293,9 +1293,9 @@ division by zero. As the condition of a while loop is evaluated in each iteration we cannot just add a guard before the while loop. Instead we need a special guard for the condition. Example: @{term "WHILE \\p\Null\\ \p\\next\Null DO SKIP OD"} -*} +\ -subsection {* Circular Lists *} +subsection \Circular Lists\ definition distPath :: "ref \ (ref \ ref) \ ref \ ref list \ bool" where "distPath x next y as = (Path x next y as \ distinct as)" @@ -1333,10 +1333,10 @@ apply (induct Ps) apply (auto simp add:fun_upd_apply) done -text {* +text \ The simple algorithm for acyclic list reversal, with modified annotations, works for cyclic lists as well.: -*} +\ lemma circular_list_rev_II: "\\ @@ -1367,17 +1367,17 @@ apply force apply fastforce done -text{* Although the above algorithm is more succinct, its invariant +text\Although the above algorithm is more succinct, its invariant looks more involved. The reason for the case distinction on @{term q} is due to the fact that during execution, the pointer variables can point to either cyclic or acyclic structures. -*} +\ -text {* +text \ When working on lists, its sometimes better to remove @{thm[source] fun_upd_apply} from the simpset, and instead include @{thm[source] fun_upd_same} and @{thm[source] fun_upd_other} to the simpset -*} +\ (* declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp] @@ -1415,7 +1415,7 @@ apply vcg_step apply auto done -text {* Instead of annotations one can also directly use previously proven lemmas.*} +text \Instead of annotations one can also directly use previously proven lemmas.\ lemma foo_lemma: "\n m. \\ \\N = n \ \M = m\ \N :== \N + 1;; \M :== \M + 1 \\N = n + 1 \ \M = m + 1\" by vcg @@ -1458,7 +1458,7 @@ lemma "\\ \\N = n \ \M = m\ apply simp done -text {* Just some test on marked, guards *} +text \Just some test on marked, guards\ lemma "\\\True\ WHILE \P \N \\, \Q \M\#, \R \N\\ \N < \M INV \\N < 2\ DO \N :== \M @@ -1508,4 +1508,4 @@ lemma "\\\<^bsub>/{True}\<^esub> \True\ WHILE apply vcg oops -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/ex/VcgExSP.thy b/tools/c-parser/Simpl/ex/VcgExSP.thy index 8a9dafb18..618d07125 100644 --- a/tools/c-parser/Simpl/ex/VcgExSP.thy +++ b/tools/c-parser/Simpl/ex/VcgExSP.thy @@ -26,18 +26,18 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Examples using Statespaces *} +section \Examples using Statespaces\ theory VcgExSP imports "../HeapList" "../Vcg" begin -subsection {* State Spaces *} +subsection \State Spaces\ -text {* +text \ First of all we provide a store of program variables that occur in the programs considered later. Slightly unexpected things may happen when attempting to work with undeclared variables. -*} +\ hoarestate state_space = @@ -53,29 +53,29 @@ hoarestate state_space = lemma (in state_space)"\\ \\N = n\ LOC \N :== 10;; \N :== \N + 2 COL \\N = n\" by vcg -text {* Internally we decorate the state components in the statespace with the -suffix @{text "_'"}, +text \Internally we decorate the state components in the statespace with the +suffix \_'\, to avoid cluttering the namespace with the simple names that could no longer be used for logical variables otherwise. -*} +\ -text {* We will first consider programs without procedures, later on +text \We will first consider programs without procedures, later on we will regard procedures without global variables and finally we will get the full pictures: mutually recursive procedures with global variables (including heap). -*} +\ -subsection {* Basic Examples *} +subsection \Basic Examples\ -text {* +text \ We look at few trivialities involving assignment and sequential composition, in order to get an idea of how to work with our formulation of Hoare Logic. -*} +\ -text {* +text \ Using the basic rule directly is a bit cumbersome. -*} +\ lemma (in state_space) "\\ {|\N = 5|} \N :== 2 * \N {|\N = 10|}" apply (rule HoarePartial.Basic) @@ -118,10 +118,10 @@ lemma (in state_space) apply simp done -text {* +text \ We can also perform verification conditions generation step by step by using -the @{text vcg_step} method. -*} +the \vcg_step\ method. +\ lemma (in state_space) shows "\\ \\M = a \ \N = b\ @@ -135,11 +135,11 @@ lemma (in state_space) done -text {* +text \ In the following assignments we make use of the consequence rule in order to achieve the intended precondition. Certainly, the - @{text vcg} method is able to handle this case, too. -*} + \vcg\ method is able to handle this case, too. +\ lemma (in state_space) shows "\\ \\M = \N\ \M :== \M + 1 \\M \ \N\" @@ -155,8 +155,8 @@ lemma (in state_space) shows "\\ \\M = \N\ \M :== \M + 1 \\M \ \N\" proof - have "\m n::nat. m = n \ m + 1 \ n" - -- {* inclusion of assertions expressed in ``pure'' logic, *} - -- {* without mentioning the state space *} + \ \inclusion of assertions expressed in ``pure'' logic,\ + \ \without mentioning the state space\ by simp also have "\\ \\M + 1 \ \N\ \M :== \M + 1 \\M \ \N\" by vcg @@ -169,14 +169,14 @@ lemma (in state_space) apply simp done -subsection {* Multiplication by Addition *} +subsection \Multiplication by Addition\ -text {* +text \ We now do some basic examples of actual \texttt{WHILE} programs. This one is a loop for calculating the product of two natural numbers, by iterated addition. We first give detailed structured proof based on single-step Hoare rules. -*} +\ lemma (in state_space) shows "\\ \\M = 0 \ \S = 0\ @@ -201,12 +201,12 @@ proof - qed -text {* - The subsequent version of the proof applies the @{text vcg} method +text \ + The subsequent version of the proof applies the \vcg\ method to reduce the Hoare statement to a purely logical problem that can be solved fully automatically. Note that we have to specify the \texttt{WHILE} loop invariant in the original statement. -*} +\ lemma (in state_space) shows "\\ \\M = 0 \ \S = 0\ @@ -218,7 +218,7 @@ lemma (in state_space) apply auto done -text {* Here some examples of ``breaking'' out of a loop *} +text \Here some examples of ``breaking'' out of a loop\ lemma (in state_space) shows "\\ \\M = 0 \ \S = 0\ @@ -257,10 +257,10 @@ done -text {* Some more syntactic sugar, the label statement @{text "\ \ \"} as shorthand -for the @{text "TRY-CATCH"} above, and the @{text "RAISE"} for an state-update followed -by a @{text "THROW"}. -*} +text \Some more syntactic sugar, the label statement \\ \ \\ as shorthand +for the \TRY-CATCH\ above, and the \RAISE\ for an state-update followed +by a \THROW\. +\ lemma (in state_space) shows "\\ \\M = 0 \ \S = 0\ \\Abr = ''Break''\\ WHILE True INV \\S = \M * b\ @@ -303,7 +303,7 @@ apply vcg apply auto done -text {* Blocks *} +text \Blocks\ lemma (in state_space) shows "\\\\I = i\ LOC \I;; \I :== 2 COL \\I \ i\" @@ -311,13 +311,13 @@ lemma (in state_space) by simp -subsection {* Summing Natural Numbers *} +subsection \Summing Natural Numbers\ -text {* +text \ We verify an imperative program to sum natural numbers up to a given limit. First some functional definition for proper specification of the problem. -*} +\ primrec sum :: "(nat => nat) => nat => nat" @@ -331,13 +331,13 @@ syntax translations "SUMM jj. b) k" -text {* +text \ The following proof is quite explicit in the individual steps taken, - with the @{text vcg} method only applied locally to take care of + with the \vcg\ method only applied locally to take care of assignment and sequential composition. Note that we express intermediate proof obligation in pure logic, without referring to the state space. -*} +\ theorem (in state_space) shows "\\ \True\ @@ -375,10 +375,10 @@ proof - finally show ?thesis . qed -text {* - The next version uses the @{text vcg} method, while still explaining +text \ + The next version uses the \vcg\ method, while still explaining the resulting proof obligations in an abstract, structured manner. -*} +\ theorem (in state_space) shows "\\ \True\ @@ -406,10 +406,10 @@ proof - qed qed -text {* +text \ Certainly, this proof may be done fully automatically as well, provided that the invariant is given beforehand. -*} +\ theorem (in state_space) shows "\\ \True\ @@ -425,7 +425,7 @@ theorem (in state_space) apply auto done -subsection {* SWITCH *} +subsection \SWITCH\ lemma (in state_space) shows "\\ \\N = 5\ SWITCH \B @@ -447,13 +447,13 @@ apply vcg apply simp done -subsection {* (Mutually) Recursive Procedures *} +subsection \(Mutually) Recursive Procedures\ -subsubsection {* Factorial *} +subsubsection \Factorial\ -text {* We want to define a procedure for the factorial. We first +text \We want to define a procedure for the factorial. We first define a HOL functions that calculates it to specify the procedure later on. -*} +\ primrec fac:: "nat \ nat" where @@ -463,7 +463,7 @@ where lemma fac_simp [simp]: "0 < i \ fac i = i * fac (i - 1)" by (cases i) simp_all -text {* Now we define the procedure *} +text \Now we define the procedure\ procedures @@ -475,27 +475,27 @@ procedures print_locale Fac_impl -text {* +text \ To see how a call is syntactically translated you can switch off the -printing translation via the configuration option @{text hoare_use_call_tr'} -*} +printing translation via the configuration option \hoare_use_call_tr'\ +\ context Fac_impl begin -text {* +text \ @{term "CALL Fac(\N,\R)"} is internally: -*} +\ declare [[hoare_use_call_tr' = false]] -text {* +text \ @{term "CALL Fac(\N,\R)"} -*} +\ term "CALL Fac(\N,\R)" declare [[hoare_use_call_tr' = true]] -text {* +text \ Now let us prove that @{term "Fac"} meets its specification. -*} +\ end @@ -508,7 +508,7 @@ lemma (in Fac_impl) Fac_spec': done -text {* +text \ Since the factorial was implemented recursively, the main ingredient of this proof is, to assume that the specification holds for the recursive call of @{term Fac} and prove the body correct. @@ -518,13 +518,13 @@ the rule @{thm [source] HoarePartial.ProcRec1} @{thm [display] HoarePartial.ProcRec1 [no_vars]} The verification condition generator will infer the specification out of the context when it encounters a recursive call of the factorial. -*} +\ -text {* We can also step through verification condition generation. When +text \We can also step through verification condition generation. When the verification condition generator encounters a procedure call it tries to - use the rule @{text ProcSpec}. To be successful there must be a specification + use the rule \ProcSpec\. To be successful there must be a specification of the procedure in the context. -*} +\ lemma (in Fac_impl) Fac_spec1: shows "\\. \,\\{\} \R :== PROC Fac(\N) \\R = fac \<^bsup>\\<^esup>N\" @@ -538,7 +538,7 @@ lemma (in Fac_impl) Fac_spec1: done -text {* Here some Isar style version of the proof *} +text \Here some Isar style version of the proof\ lemma (in Fac_impl) Fac_spec2: shows "\\. \,\\{\} \R :== PROC Fac(\N) \\R = fac \<^bsup>\\<^esup>N\" @@ -556,10 +556,10 @@ proof (hoare_rule HoarePartial.ProcRec1) done qed -text {* To avoid retyping of potentially large pre and postconditions in +text \To avoid retyping of potentially large pre and postconditions in the previous proof we can use the casual term abbreviations of the Isar language. -*} +\ lemma (in Fac_impl) Fac_spec3: shows "\\. \,\\{\} \R :== PROC Fac(\N) \\R = fac \<^bsup>\\<^esup>N\" @@ -578,24 +578,24 @@ proof (hoare_rule HoarePartial.ProcRec1) done qed -text {* The previous proof pattern has still some kind of inconvenience. +text \The previous proof pattern has still some kind of inconvenience. The augmented context is always printed in the proof state. That can mess up the state, especially if we have large specifications. This may be annoying if we want to develop single step or structured proofs. In this case it can be a good idea to introduce a new variable for the augmented context. -*} +\ lemma (in Fac_impl) Fac_spec4: shows "\\. \,\\{\} \R :== PROC Fac(\N) \\R = fac \<^bsup>\\<^esup>N\" (is "\\. \,\\(?Pre \) ?Fac (?Post \)") proof (hoare_rule HoarePartial.ProcRec1) - def "\'"=="(\\(\\. {(?Pre \, Fac_'proc, ?Post \,{})}))" + define \' where "\' = \ \ (\\. {(?Pre \, Fac_'proc, ?Post \,{})})" have Fac_spec: "\\. \,\'\(?Pre \) ?Fac (?Post \)" by (unfold \'_def, rule allI, rule hoarep.Asm) simp - txt {* We have to name the fact @{text "Fac_spec"}, so that the vcg can + txt \We have to name the fact \Fac_spec\, so that the vcg can use the specification for the recursive call, since it cannot infer it - from the opaque @{term "\'"}. *} + from the opaque @{term "\'"}.\ show "\\. \,\'\ (?Pre \) IF \N = 0 THEN \R :== 1 ELSE \R :== CALL Fac(\N - 1);; \R :== \N * \R FI (?Post \)" apply vcg @@ -603,7 +603,7 @@ proof (hoare_rule HoarePartial.ProcRec1) done qed -text {* There are different rules available to prove procedure calls, +text \There are different rules available to prove procedure calls, depending on the kind of postcondition and whether or not the procedure is recursive or even mutually recursive. See for example @{thm [source] HoareTotal.ProcRec1}, @@ -613,15 +613,15 @@ They are all derived from the most general rule All of them have some side-conditions concerning the parameter passing protocol and its relation to the pre and postcondition. They can be solved in a uniform fashion. Thats why we have created the method -@{text "hoare_rule"}, which behaves like the method @{text "rule"} but automatically +\hoare_rule\, which behaves like the method \rule\ but automatically tries to solve the side-conditions. -*} +\ -subsubsection {* Odd and Even *} +subsubsection \Odd and Even\ -text {* Odd and even are defined mutually recursive here. In the -@{text "procedures"} command we conjoin both definitions with @{text "and"}. -*} +text \Odd and even are defined mutually recursive here. In the +\procedures\ command we conjoin both definitions with \and\. +\ procedures odd(N::nat | A::nat) "IF \N=0 THEN \A:==0 @@ -640,16 +640,16 @@ print_theorems print_locale! odd_even_clique -text {* To prove the procedure calls to @{term "odd"} respectively +text \To prove the procedure calls to @{term "odd"} respectively @{term "even"} correct we first derive a rule to justify that we can assume both specifications to verify the bodies. This rule can be derived from the general @{thm [source] HoareTotal.ProcRec} rule. An ML function will do this work: -*} +\ -ML {* ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2) *} +ML \ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2)\ lemma (in odd_even_clique) @@ -672,7 +672,7 @@ proof - by iprover+ qed -subsection {*Expressions With Side Effects *} +subsection \Expressions With Side Effects\ (* R := N++ + M++*) @@ -712,15 +712,15 @@ proof - qed -subsection {* Global Variables and Heap *} +subsection \Global Variables and Heap\ -text {* +text \ Now we will define and verify some procedures on heap-lists. We consider list structures consisting of two fields, a content element @{term "cont"} and a reference to the next list element @{term "next"}. We model this by the following state space where every field has its own heap. -*} +\ hoarestate globals_list = @@ -730,16 +730,16 @@ hoarestate globals_list = -text {* Updates to global components inside a procedure will +text \Updates to global components inside a procedure will always be propagated to the caller. This is implicitly done by the parameter passing syntax translations. The record containing the global variables must begin with the prefix "globals". -*} +\ -text {* We will first define an append function on lists. It takes two +text \We will first define an append function on lists. It takes two references as parameters. It appends the list referred to by the first parameter with the list referred to by the second parameter, and returns the result right into the first parameter. -*} +\ procedures (imports globals_list) append(p::ref,q::ref|p::ref) @@ -754,7 +754,7 @@ term "CALL append(\p,\q,\p\\next)" end declare [[hoare_use_call_tr' = true]] -text {* Below we give two specifications this time.. +text \Below we give two specifications this time.. The first one captures the functional behaviour and focuses on the entities that are potentially modified by the procedure, the second one is a pure frame condition. @@ -769,9 +769,9 @@ The functional specification now introduces two logical variables besides the state space variable @{term "\"}, namely @{term "Ps"} and @{term "Qs"}. They are universally quantified and range over both the pre and the postcondition, so that we are able to properly instantiate the specification -during the proofs. The syntax @{text "\\. \\"} is a shorthand to fix the current -state: @{text "{s. \ = s \}"}. -*} +during the proofs. The syntax \\\. \\\ is a shorthand to fix the current +state: \{s. \ = s \}\. +\ lemma (in append_impl) append_spec: shows "\\ Ps Qs. \\ @@ -784,9 +784,9 @@ lemma (in append_impl) append_spec: done -text {* The modifies clause is equal to a proper record update specification +text \The modifies clause is equal to a proper record update specification of the following form. -*} +\ lemma (in append_impl) shows "{t. t may_only_modify_globals Z in [next]} = @@ -795,7 +795,7 @@ lemma (in append_impl) shows "{t. t may_only_modify_globals Z in [next]} apply simp done -text {* If the verification condition generator works on a procedure call +text \If the verification condition generator works on a procedure call it checks whether it can find a modifies clause in the context. If one is present the procedure call is simplified before the Hoare rule @{thm [source] HoareTotal.ProcSpec} is applied. Simplification of the procedure call means, @@ -804,23 +804,23 @@ components that occur in the modifies clause will actually be copied back. This simplification is justified by the rule @{thm [source] HoareTotal.ProcModifyReturn}. So after this simplification all global components that do not appear in the modifies clause will be treated as local variables. -*} +\ -text {* You can study the effect of the modifies clause on the following two +text \You can study the effect of the modifies clause on the following two examples, where we want to prove that @{term "append"} does not change the @{term "cont"} part of the heap. -*} +\ lemma (in append_impl) shows "\\ \\p=Null \ \cont=c\ \p :== CALL append(\p,Null) \\cont=c\" apply vcg oops -text {* To prove the frame condition, +text \To prove the frame condition, we have to tell the verification condition generator to use only the modifies clauses and not to search for functional specifications by -the parameter @{text "spec=modifies"} It will also try to solve the +the parameter \spec=modifies\ It will also try to solve the verification conditions automatically. -*} +\ lemma (in append_impl) append_modifies: shows @@ -835,32 +835,32 @@ lemma (in append_impl) apply simp done -text {* +text \ Of course we could add the modifies clause to the functional specification as well. But separating both has the advantage that we split up the verification work. We can make use of the modifies clause before we apply the functional specification in a fully automatic fashion. -*} +\ -text {* To verify the body of @{term "append"} we do not need the modifies +text \To verify the body of @{term "append"} we do not need the modifies clause, since the specification does not talk about @{term "cont"} at all, and we don't access @{term "cont"} inside the body. This may be different for more complex procedures. -*} +\ -text {* +text \ To prove that a procedure respects the modifies clause, we only need the modifies clauses of the procedures called in the body. We do not need the functional specifications. So we can always prove the modifies clause without functional specifications, but me may need the modifies clause to prove the functional specifications. -*} +\ -subsubsection {*Insertion Sort*} +subsubsection \Insertion Sort\ primrec sorted:: "('a \ 'a \ bool) \ 'a list \ bool" where @@ -881,7 +881,7 @@ procedures (imports globals_list) FI" -text {* +text \ In the postcondition of the functional specification there is a small but important subtlety. Whenever we talk about the @{term "cont"} part we refer to the one of the pre-state, even in the conclusion of the implication. @@ -889,16 +889,16 @@ The reason is, that we have separated out, that @{term "cont"} is not modified by the procedure, to the modifies clause. So whenever we talk about unmodified parts in the postcondition we have to use the pre-state part, or explicitely state an equality in the postcondition. -The reason is simple. If the postcondition would talk about @{text "\cont"} -instead of @{text "\<^bsup>\\<^esup>cont"}, we will get a new instance of @{text "cont"} during +The reason is simple. If the postcondition would talk about \\cont\ +instead of \\<^bsup>\\<^esup>cont\, we will get a new instance of \cont\ during verification and the postcondition would only state something about this new instance. But as the verification condition generator will use the -modifies clause the caller of @{text "insert"} instead will still have the -old @{text "cont"} after the call. Thats the sense of the modifies clause. +modifies clause the caller of \insert\ instead will still have the +old \cont\ after the call. Thats the sense of the modifies clause. So the caller and the specification will simply talk about two different things, without being able to relate them (unless an explicit equality is added to the specification). -*} +\ lemma (in insert_impl) insert_modifies: "\\. \\ {\} \p :== PROC insert(\r,\p){t. t may_only_modify_globals \ in [next]}" @@ -949,12 +949,12 @@ apply (vcg spec=modifies) done -text {* Insertion sort is not implemented recursively here but with a while +text \Insertion sort is not implemented recursively here but with a while loop. Note that the while loop is not annotated with an invariant in the procedure definition. The invariant only comes into play during verification. Therefore we will annotate the body during the proof with the rule @{thm [source] HoareTotal.annotateI}. -*} +\ lemma (in insertSort_impl) insertSort_body_spec: @@ -988,11 +988,11 @@ lemma (in insertSort_impl) insertSort_body_spec: subsubsection "Memory Allocation and Deallocation" -text {* The basic idea of memory management is to keep a list of allocated +text \The basic idea of memory management is to keep a list of allocated references in the state space. Allocation of a new reference adds a new reference to the list deallocation removes a reference. Moreover we keep a counter "free" for the free memory. -*} +\ (* record globals_list_alloc = globals_list + @@ -1077,14 +1077,14 @@ apply (simp add: sz_def) apply fastforce done -subsection {* Fault Avoiding Semantics *} +subsection \Fault Avoiding Semantics\ -text {* +text \ If we want to ensure that no runtime errors occur we can insert guards into the code. We will not be able to prove any nontrivial Hoare triple about code with guards, if we cannot show that the guards will never fail. A trivial Hoare triple is one with an empty precondtion. -*} +\ lemma (in list_alloc) "\,\\ \True\ \\p\Null\\ \p\\next :== \p \True\" @@ -1095,9 +1095,9 @@ lemma (in list_alloc) "\,\\ {} \\p\Let us consider this small program that reverts a list. At first without guards. -*} +\ lemma (in list_alloc) shows "\,\\ \List \p \next Ps \ List \q \next Qs \ set Ps \ set Qs = {} \ @@ -1115,9 +1115,9 @@ apply (vcg) apply fastforce+ done -text {* If we want to ensure that we do not dereference @{term "Null"} or +text \If we want to ensure that we do not dereference @{term "Null"} or access unallocated memory, we have to add some guards. -*} +\ lemma (in list_alloc) shows "\,\\ \List \p \next Ps \ List \q \next Qs \ set Ps \ set Qs = {} \ @@ -1136,9 +1136,9 @@ apply fastforce+ done -text {* We can also just prove that no faults will occur, by giving the +text \We can also just prove that no faults will occur, by giving the trivial postcondition. -*} +\ lemma (in list_alloc) rev_noFault: shows "\,\\ \List \p \next Ps \ List \q \next Qs \ set Ps \ set Qs = {} \ @@ -1197,10 +1197,10 @@ proof - qed -text {* We can then combine the prove that no fault will occur with the +text \We can then combine the prove that no fault will occur with the functional prove of the programm without guards to get the full proove by the rule @{thm HoarePartialProps.CombineStrip} -*} +\ lemma (in list_alloc) @@ -1223,16 +1223,16 @@ apply simp done -text {* In the previous example the effort to split up the prove did not +text \In the previous example the effort to split up the prove did not really pay off. But when we think of programs with a lot of guards and complicated specifications it may be better to first focus on a prove without the messy guards. Maybe it is possible to automate the no fault proofs so that it suffices to focus on the stripped program. -*} +\ context list_alloc begin -text {* +text \ The purpose of guards is to watch for faults that can occur during evaluation of expressions. In the example before we watched for null pointer dereferencing or memory faults. We can also look for array index bounds or @@ -1240,10 +1240,10 @@ division by zero. As the condition of a while loop is evaluated in each iteration we cannot just add a guard before the while loop. Instead we need a special guard for the condition. Example: @{term "WHILE \\p\Null\\ \p\\next\Null DO SKIP OD"} -*} +\ end -subsection {* Cicular Lists *} +subsection \Cicular Lists\ definition distPath :: "ref \ (ref \ ref) \ ref \ ref list \ bool" where "distPath x next y as = (Path x next y as \ distinct as)" @@ -1282,10 +1282,10 @@ apply (induct Ps) apply (auto simp add:fun_upd_apply) done -text {* +text \ The simple algorithm for acyclic list reversal, with modified annotations, works for cyclic lists as well.: -*} +\ lemma (in list_alloc) circular_list_rev_II: "\,\\ @@ -1316,17 +1316,17 @@ apply force apply fastforce done -text{* Although the above algorithm is more succinct, its invariant +text\Although the above algorithm is more succinct, its invariant looks more involved. The reason for the case distinction on @{term q} is due to the fact that during execution, the pointer variables can point to either cyclic or acyclic structures. -*} +\ -text {* +text \ When working on lists, its sometimes better to remove @{thm[source] fun_upd_apply} from the simpset, and instead include @{thm[source] fun_upd_same} and @{thm[source] fun_upd_other} to the simpset -*} +\ (* declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp] @@ -1368,7 +1368,7 @@ apply vcg_step apply auto done -text {* Just some test on marked, guards *} +text \Just some test on marked, guards\ lemma (in state_space) "\\\True\ WHILE \P \N \\, \Q \M\#, \R \N\\ \N < \M INV \\N < 2\ DO \N :== \M @@ -1385,4 +1385,4 @@ lemma (in state_space) "\\\<^bsub>/{True}\<^esub> \Tru apply vcg oops -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/ex/VcgExTotal.thy b/tools/c-parser/Simpl/ex/VcgExTotal.thy index b8ed84a0e..e0a388cdd 100644 --- a/tools/c-parser/Simpl/ex/VcgExTotal.thy +++ b/tools/c-parser/Simpl/ex/VcgExTotal.thy @@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -section {* Examples for Total Correctness *} +section \Examples for Total Correctness\ theory VcgExTotal imports "../HeapList" "../Vcg" begin @@ -60,10 +60,10 @@ apply vcg apply auto done -text {* Total correctness of a nested loop. In the inner loop we have to +text \Total correctness of a nested loop. In the inner loop we have to express that the loop variable of the outer loop is not changed. We use -@{text "FIX"} to introduce a new logical variable -*} +\FIX\ to introduce a new logical variable +\ lemma "\\\<^sub>t \\M=0 \ \N=0\ WHILE (\M < i) @@ -214,7 +214,7 @@ procedures Rev(p|p) = Rev_modifies: "\\. \\\<^bsub>/UNIV\<^esub> {\} \p :== PROC Rev(\p) {t. t may_only_modify_globals \ in [next]}" -text {* We only need partial correctness of modifies clause!*} +text \We only need partial correctness of modifies clause!\ @@ -307,7 +307,7 @@ and IF 0 < \M THEN CALL coast(\N,\M- 1) FI" -ML {* ML_Thms.bind_thm ("HoareTotal_ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Total 2)*} +ML \ML_Thms.bind_thm ("HoareTotal_ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Total 2)\ lemma (in pedal_coast_clique) @@ -383,4 +383,4 @@ lemma (in pedal_coast_clique) done -end \ No newline at end of file +end diff --git a/tools/c-parser/Simpl/hoare.ML b/tools/c-parser/Simpl/hoare.ML index 70d9c12cb..06ecece08 100644 --- a/tools/c-parser/Simpl/hoare.ML +++ b/tools/c-parser/Simpl/hoare.ML @@ -135,20 +135,25 @@ fun dest_Un (Const (@{const_name Lattices.sup}, _) $ t1 $ t2) = dest_Un t1 @ des fun mk_UN' dT rT t = let val dTs = HOLogic.mk_setT dT; + val rTs = HOLogic.mk_setT rT; in - Const (@{const_name Complete_Lattices.SUPREMUM}, - dTs --> (dT --> rT) --> rT) $ - Const (@{const_name Orderings.top}, dTs) $ t + Const (@{const_name Complete_Lattices.Sup}, rTs --> rT) $ + (Const (@{const_name image}, (dT --> rT) --> dTs --> rTs) $ t $ + Const (@{const_name Orderings.top}, dTs)) end; fun mk_UN ((x, T), P) = mk_UN' T (fastype_of P) (absfree (x, T) P); -fun dest_UN (Const (@{const_name Complete_Lattices.SUPREMUM}, _) $ Const (@{const_name Orderings.top}, _) $ Abs (x, T, t)) = +fun dest_UN (Const (@{const_name Complete_Lattices.Sup}, _) $ + (Const (@{const_name Set.image}, _) $ Abs (x, T, t) $ + Const (@{const_name Orderings.top}, _))) = let val (vars, body) = dest_UN t in ((x, T) :: vars, body) end | dest_UN t = ([], t); -fun tap_UN (Const (@{const_name Complete_Lattices.SUPREMUM}, _) $ Const (@{const_name Orderings.top}, _) $ t) = SOME t +fun tap_UN (Const (@{const_name Complete_Lattices.Sup}, _) $ + (Const (@{const_name Set.image}, _) $ t $ + Const (@{const_name Orderings.top}, _))) = SOME t | tap_UN _ = NONE; @@ -534,7 +539,7 @@ fun dest_Guard (Const (@{const_name Language.com.Guard},_)$f$g$c) = (f,g,c,false fun add_declaration name decl thy = thy - |> Named_Target.init name + |> Named_Target.init NONE name |> Local_Theory.declaration {syntax = false, pervasive = false} decl |> Local_Theory.exit |> Proof_Context.theory_of; @@ -569,7 +574,7 @@ structure Hoare_Data = Generic_Data type T = hoare_data; val empty = make_hoare_data - (Symtab.empty: proc_info Symtab.table) (* smlnj needs typing *) + (Symtab.empty: proc_info Symtab.table) ([]:string list list) (Function) (stamp (),(K (K NONE)): Proof.context -> term -> term option) @@ -883,7 +888,7 @@ fun apply_in_context thy lexp f t = fun add_abbrev loc mode name spec thy = thy - |> Named_Target.init loc + |> Named_Target.init NONE loc |> (fn lthy => let val t = Syntax.read_term (Local_Theory.target_of lthy) spec; in Local_Theory.abbrev mode ((Binding.name name, NoSyn), t) lthy end) |> #2 @@ -1055,7 +1060,7 @@ fun procedures_definition locname procs thy = fun add_decl_and_def lname ctxt = ctxt |> Proof_Context.theory_of - |> Named_Target.init lname + |> Named_Target.init NONE lname |> Local_Theory.declaration {syntax = false, pervasive = false} parameter_info_decl |> (fn lthy => if has_body name then snd (Local_Theory.define (def lthy) lthy) @@ -1187,7 +1192,7 @@ fun procedures_definition locname procs thy = (* outer syntax *) -val var_declP = Parse.name -- (@{keyword "::"} |-- Parse.!!! Parse.typ_group); +val var_declP = Parse.name -- (@{keyword "::"} |-- Parse.!!! Parse.embedded); val var_declP' = Parse.name >> (fn n => (n,"")); val localsP = Scan.repeat var_declP; @@ -1211,10 +1216,10 @@ val proc_decl = proc_decl_statespace >> pair Function || proc_decl_record >> pai val loc_decl = Scan.optional (@{keyword "where"} |-- localsP --| @{keyword "in"}) [] -val proc_body = Parse.term_group (*>> BodyTerm*) +val proc_body = Parse.embedded (*>> BodyTerm*) -fun proc_specs x = (Parse.!!! (Scan.repeat (Parse_Spec.thm_name ":" -- Parse.prop_group)) +fun proc_specs x = (Parse.!!! (Scan.repeat (Parse_Spec.thm_name ":" -- Parse.embedded)) >> map (fn ((thm_name, _), prop) => (Binding.name_of thm_name, prop))) x val par_loc = @@ -1581,10 +1586,9 @@ fun assertion_simp_tac ctxt state_kind thms i = (* simplify equality test on strings (and datatype-constructors) and propagate result*) fun string_eq_simp_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt - addsimps (@{thms list.inject} @ @{thms char.inject} - @ @{thms list.distinct} @ @{thms simp_thms})); - - + addsimps @{thms list.inject list.distinct Char_eq_Char_iff + cut_eq_simps simp_thms}); + fun assertion_string_eq_simp_tac ctxt state_kind thms i = assertion_simp_tac ctxt state_kind thms i THEN_MAYBE string_eq_simp_tac ctxt i; @@ -2957,8 +2961,8 @@ val ss = simpset_of (put_simpset (simpset_of @{theory_context Fun}) @{context} addsimps (@{thm StateFun.lookup_def} :: @{thm StateFun.id_id_cancel} - :: @{thms list.inject} @ @{thms char.inject} - @ @{thms list.distinct} @ @{thms simp_thms}) + :: @{thms list.inject list.distinct Char_eq_Char_iff + cut_eq_simps simp_thms}) addsimprocs [Record.simproc, StateFun.lazy_conj_simproc] |> fold Simplifier.add_cong @{thms block_conj_cong}); @@ -3098,11 +3102,11 @@ local val state_fun_update_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps ([@{thm StateFun.update_def}, @{thm id_def}, @{thm fun_upd_apply}, @{thm if_True}, @{thm if_False}] - @ @{thms list.inject} @ @{thms char.inject} - @ @{thms list.distinct} @ @{thms simp_thms} @ K_fun_convs) + @ @{thms list.inject list.distinct Char_eq_Char_iff + cut_eq_simps simp_thms} @ K_fun_convs) addsimprocs [DistinctTreeProver.distinct_simproc ["distinct_fields", "distinct_fields_globals"]] |> Simplifier.add_cong @{thm imp_cong} (* K_fun_congs FIXME: Stefan fragen*) - |> Splitter.add_split @{thm split_if}); + |> Splitter.add_split @{thm if_split}); in diff --git a/tools/c-parser/Simpl/hoare_syntax.ML b/tools/c-parser/Simpl/hoare_syntax.ML index d148afe73..d2f29a66b 100644 --- a/tools/c-parser/Simpl/hoare_syntax.ML +++ b/tools/c-parser/Simpl/hoare_syntax.ML @@ -115,18 +115,6 @@ fun mk_list [] = Syntax.const @{const_syntax Nil} fun unsuffix' sfx a = unsuffix sfx a handle Fail _ => raise Match; fun unsuffixI sfx a = unsuffix sfx a handle Fail _ => a; -fun mk_nib n = "Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10)); - -fun mk_char c = - if Char.isAscii c andalso Char.isPrint c then - Syntax.const @{const_syntax Char} $ - Syntax.const (mk_nib (Char.ord c div 16)) $ - Syntax.const (mk_nib (Char.ord c mod 16)) - else raise TERM ("call_tr: printable procedure name expected: " ^ str c, []); - -fun mk_string [] = Syntax.const @{const_syntax Nil} - | mk_string (c::cs) = Syntax.const @{const_syntax Cons} $ mk_char c $ mk_string cs; - fun is_prefix_or_suffix s t = can (unprefix s) t orelse can (unsuffix s) t; @@ -328,7 +316,7 @@ fun antiquote_applied_only_to P = else test i t andalso test i u | u => test i t andalso test i u) | test i (Abs (x, T, t)) = test (i + 1) t - | test i a = true; + | test i _ = true; in test 0 end; @@ -341,12 +329,12 @@ fun antiquote_mult_tr' ctxt is_selector current old = else if is_selector t (* other quantified states *) then Syntax.const old $ Bound j $ tr' i (Hoare.undeco ctxt t) else tr' i t $ tr' i u - | pre as ((Const (m,_) $ (s as Free _))) (* pre state *) => + | pre as ((Const (m,_) $ Free _)) (* pre state *) => if (m = @{syntax_const "_bound"} orelse m = @{syntax_const "_free"}) andalso is_selector t then Syntax.const old $ pre $ tr' i (Hoare.undeco ctxt t) else tr' i t $ pre - | pre as ((Const (m,_) $ (s as Var _))) (* pre state *) => + | pre as ((Const (m,_) $ Var _)) (* pre state *) => if m = @{syntax_const "_var"} andalso is_selector t then Syntax.const old $ pre $ tr' i (Hoare.undeco ctxt t) else tr' i t $ pre @@ -463,9 +451,9 @@ fun update_tr ctxt ps off_var off_val e | update_tr _ _ _ _ e t = raise TERM ("update_tr", [t]) -fun app_assign_tr f ctxt (ts as [v, e]) = +fun app_assign_tr f ctxt [v, e] = let - fun offset v = 0; + fun offset _ = 0; in f $ Abs ("s", dummyT, update_tr ctxt [] offset offset (antiquoteCur_tr ctxt e) v (Bound 0)) end | app_assign_tr _ _ ts = raise TERM ("assign_tr", ts); @@ -735,7 +723,7 @@ fun guard ctxt Ts (add as (Const (@{const_name Groups.plus},_) $ l $ r)) = guard ctxt Ts l & mk_imp (HOLogic.Not $ l,guard ctxt Ts r) | guard ctxt Ts (dv as (Const (@{const_name Rings.divide},_) $ l $ r)) = guard ctxt Ts l & guard ctxt Ts r & SOME (not_zero r) & SOME (in_range dv) (* FIXME: Make more concrete guard...*) - | guard ctxt Ts (Const (@{const_name Divides.div_class.mod},_) $ l $ r) = + | guard ctxt Ts (Const (@{const_name Rings.modulo},_) $ l $ r) = guard ctxt Ts l & guard ctxt Ts r & SOME (not_zero r) | guard ctxt Ts (un as (Const (@{const_name Groups.uminus},_) $ n)) = guard ctxt Ts n & SOME (in_range un) @@ -960,7 +948,7 @@ fun mk_call_tr ctxt grd Call formals pn pt actuals has_args cont = (* FIXME: What is prfx for, maybe unused *) fun dest_procname ctxt prfx false (Const (p, _)) = - (prfx ^ suffix Hoare.proc_deco p, mk_string (String.explode p)) + (prfx ^ suffix Hoare.proc_deco p, HOLogic.mk_string p) | dest_procname ctxt prfx false (t as Free (p, T)) = (prfx ^ suffix Hoare.proc_deco p, Free (suffix Hoare.proc_deco p, T)) | dest_procname ctxt prfx false (Const (@{syntax_const "_free"},_) $ Free (p,T)) =