adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Isabelle2016-1: update Simpl

This commit is contained in:
Matthew Brecknell 2016-10-25 11:23:16 +11:00
parent 1a590fbbb2
commit f8b1c7d5ae
32 changed files with 1079 additions and 1098 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

120
tools/c-parser/Simpl/AlternativeSmallStep.thy
View File

@ -26,13 +26,13 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Alternative Small Step Semantics *}
section \<open>Alternative Small Step Semantics\<close>
theory AlternativeSmallStep imports HoareTotalDef
begin
text {*
text \<open>
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.
*}
\<close>
subsection {*Small-Step Computation: @{text "\<Gamma>\<turnstile>(cs, css, s) \<rightarrow> (cs', css', s')"}*}
subsection \<open>Small-Step Computation: \<open>\<Gamma>\<turnstile>(cs, css, s) \<rightarrow> (cs', css', s')\<close>\<close>
type_synonym ('s,'p,'f) continuation = "('s,'p,'f) com list \<times> ('s,'p,'f) com list"
@ -164,7 +164,7 @@ abbreviation
"\<Gamma>\<turnstile>cs0 \<rightarrow>\<^sup>+ cs1 == (step \<Gamma>)\<^sup>+\<^sup>+ cs0 cs1"
subsubsection {* Structural Properties of Small Step Computations *}
subsubsection \<open>Structural Properties of Small Step Computations\<close>
lemma Fault_app_steps: "\<Gamma>\<turnstile>(cs@xs,css,Fault f) \<rightarrow>\<^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 \<open>We can only append commands inside a block, if execution does not
enter or exit a block.
*}
\<close>
lemma app_step:
assumes step: "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow> (cs',css',t)"
shows "css=css' \<Longrightarrow> \<Gamma>\<turnstile>(cs@xs,css,s) \<rightarrow> (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 \<open>We can append whole blocks, without interfering with the actual
block. Outer blocks do not influence execution of
inner blocks. *}
inner blocks.\<close>
lemma app_css_step:
assumes step: "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow> (cs',css',t)"
shows "\<Gamma>\<turnstile>(cs,css@xs,s) \<rightarrow> (cs',css'@xs,t)"
@ -224,13 +224,13 @@ apply induct
apply (simp_all del: fun_upd_apply,(blast intro: step.intros)+)
done
ML {*
ML \<open>
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}));
*}
\<close>
lemma app_css_steps:
assumes step: "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow>\<^sup>+ (cs',css',t)"
@ -380,7 +380,7 @@ proof -
by auto
qed
subsubsection {* Equivalence between Big and Small-Step Semantics *}
subsubsection \<open>Equivalence between Big and Small-Step Semantics\<close>
lemma exec_impl_steps:
assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t"
@ -553,13 +553,13 @@ inductive_cases execs_elim_cases [cases set]:
"\<Gamma>\<turnstile>\<langle>[],css,s\<rangle> \<Rightarrow> t"
"\<Gamma>\<turnstile>\<langle>c#cs,css,s\<rangle> \<Rightarrow> t"
ML {*
ML \<open>
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}));
*}
\<close>
lemma execs_Fault_end:
assumes execs: "\<Gamma>\<turnstile>\<langle>cs,css,s\<rangle> \<Rightarrow> t" shows "s=Fault f\<Longrightarrow> t=Fault f"
@ -660,11 +660,9 @@ next
from execs_rest Abrupt have
"\<Gamma>\<turnstile>\<langle>Throw # cs,css,Normal t''\<rangle> \<Rightarrow> t"
by (cases) auto
then obtain v where
"\<Gamma>\<turnstile>\<langle>Throw,Normal t''\<rangle> \<Rightarrow> v" and
rest: "\<Gamma>\<turnstile>\<langle>cs,css,v\<rangle> \<Rightarrow> t"
then obtain v where v: "\<Gamma>\<turnstile>\<langle>Throw,Normal t''\<rangle> \<Rightarrow> v" "\<Gamma>\<turnstile>\<langle>cs,css,v\<rangle> \<Rightarrow> 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: "\<Gamma>\<turnstile>([c],[],s) \<rightarrow>\<^sup>* (
by (blast intro: steps_impl_exec exec_impl_steps)
subsection {* Infinite Computations: @{text "inf \<Gamma> cs css s"}*}
subsection \<open>Infinite Computations: \<open>inf \<Gamma> cs css s\<close>\<close>
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: "\<lbrakk>\<And>f. \<lbrakk>f 0 = (cs,css,s); \<And>i. \<Gamma>\
\<Longrightarrow> \<not>inf \<Gamma> cs css s"
by (auto simp add: inf_def)
subsection {* Equivalence of Termination and Absence of Infinite Computations *}
subsection \<open>Equivalence of Termination and Absence of Infinite Computations\<close>
inductive "terminatess":: "[('s,'p,'f) body,('s,'p,'f) com list,
@ -979,13 +977,13 @@ next
qed
ML {*
ML \<open>
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}));
*}
\<close>
lemma steps_preserves_terminations:
assumes steps: "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow>\<^sup>* (cs',css',t)"
@ -1232,7 +1230,7 @@ next
have not_finished': "\<forall>i < Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)" by fact
with simul
have not_finished: "\<forall>i<Suc k. \<not> (pcs i = [] \<and> 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 "\<Gamma>\<turnstile> ([],[hd css'']@tl css'',t'') \<rightarrow> (cs',css',t')"
have *: "\<Gamma>\<turnstile> ([],[hd css'']@tl css'',t'') \<rightarrow> (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 "\<Gamma>\<turnstile>([],[(pnorm@cs,pabr@cs)]@css,t'') \<rightarrow> (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 "\<Gamma>\<turnstile> (pcs 0, pcss 0, S (f 0)) \<rightarrow>\<^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: "\<not> (pcs = [] \<and> 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 "\<Gamma>\<turnstile> ([],[hd css'']@tl css'',t'') \<rightarrow> (cs',css',t')"
have *: "\<Gamma>\<turnstile> ([],[hd css'']@tl css'',t'') \<rightarrow> (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' \<Rightarrow> snd (hd css'')
| _ \<Rightarrow> 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 "\<Gamma>\<turnstile>([],[(pnorm@cs,pabr@cs)]@css,t'') \<rightarrow> (cs',css',t')"
by simp
@ -1745,7 +1743,7 @@ proof -
show ?thesis
proof (cases "\<exists>i. CS (f i) = cs \<and> CSS (f i) = css")
case True
def k\<equiv>"(LEAST i. CS (f i) = cs \<and> CSS (f i) = css)"
define k where "k = (LEAST i. CS (f i) = cs \<and> 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: "\<forall>i\<le>k. (if pcss i = [] then CSS (f i)=css \<and> CS (f i)=pcs i@cs
else CS (f i)=pcs i \<and>
@ -1827,10 +1825,10 @@ proof -
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css)"
by iprover
def "g" \<equiv> "\<lambda>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 "\<forall>i. \<Gamma>\<turnstile>g i \<rightarrow> g (Suc i)"
@ -1876,7 +1874,7 @@ next
f_0: "f 0 = (c1# c2#cs,css,Normal s)" and
f_step: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
by (auto simp add: inf_def)
def g\<equiv>"\<lambda>i. case i of 0 \<Rightarrow> (Seq c1 c2#cs,css,Normal s) | Suc j \<Rightarrow> f j"
define g where "g i = (case i of 0 \<Rightarrow> (Seq c1 c2#cs,css,Normal s) | Suc j \<Rightarrow> f j)" for i
with f_0 have
"\<Gamma>\<turnstile>g 0 \<rightarrow> 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: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
by (auto simp add: inf_def)
def h\<equiv>"\<lambda>i. case i of 0 \<Rightarrow> (While b c#cs,css,Normal s) | Suc j \<Rightarrow> f j"
define h where "h i = (case i of 0 \<Rightarrow> (While b c#cs,css,Normal s) | Suc j \<Rightarrow> f j)" for i
with b f_0 have
"\<Gamma>\<turnstile>h 0 \<rightarrow> 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: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
by (auto simp add: inf_def)
def h\<equiv>"\<lambda>i. case i of 0 \<Rightarrow> (Catch c1 c2#cs,css,Normal s) | Suc j \<Rightarrow> f j"
define h where "h i = (case i of 0 \<Rightarrow> (Catch c1 c2#cs,css,Normal s) | Suc j \<Rightarrow> f j)" for i
with f_0 have
"\<Gamma>\<turnstile>h 0 \<rightarrow> h (Suc 0)"
by (auto intro: step.intros)
@ -2542,7 +2540,7 @@ where
{((t,q),(s,p)). \<Gamma>\<turnstile>the (\<Gamma> p)\<down>Normal s \<and>
(\<exists>css. \<Gamma>\<turnstile>([the (\<Gamma> p)],[],Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)],css,Normal t))}"
text {* Sequencing computations, or more exactly continuation stacks *}
text \<open>Sequencing computations, or more exactly continuation stacks\<close>
primrec seq:: "(nat \<Rightarrow> 'a list) \<Rightarrow> nat \<Rightarrow> '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' \<comment> \<open>Skolemization of css with axiom of choice\<close>
have "\<exists>css. \<forall>i. \<Gamma>\<turnstile>(the (\<Gamma> (p i))) \<down> Normal (s i) \<and>
\<Gamma>\<turnstile>([the (\<Gamma> (p i))],[],Normal (s i)) \<rightarrow>\<^sup>+
([the (\<Gamma> (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: "\<forall>i. \<Gamma>\<turnstile>([the (\<Gamma> (p i))],[],Normal (s i)) \<rightarrow>\<^sup>+
([the (\<Gamma> (p (Suc i)))],css i,Normal (s (Suc i)))"
by blast
def f == "\<lambda>i. ([the (\<Gamma> (p i))], seq css i,Normal (s i)::('a,'c) xstate)"
define f where "f i = ([the (\<Gamma> (p i))], seq css i,Normal (s i)::('a,'c) xstate)" for i
have "f 0 = ([the (\<Gamma> (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 \<open>An alternative proof using Hilbert-choice instead of axiom of choice.\<close>
theorem "wf (termi_call_steps \<Gamma>)"
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 \<equiv> "\<lambda>i. (SOME css.
define CSS where "CSS i = (SOME css.
\<Gamma>\<turnstile>([the (\<Gamma> (p i))],[], Normal (s i)) \<rightarrow>\<^sup>+
([the (\<Gamma> (p (i+1)))],css,Normal (s (i+1))))"
def f == "\<lambda>i. ([the (\<Gamma> (p i))], seq CSS i,Normal (s i)::('a,'c) xstate)"
([the (\<Gamma> (p (i+1)))],css,Normal (s (i+1))))" for i
define f where "f i = ([the (\<Gamma> (p i))], seq CSS i,Normal (s i)::('a,'c) xstate)" for i
have "f 0 = ([the (\<Gamma> (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 \<open>Completeness of Total Correctness Hoare Logic\<close>
lemma ConseqMGT:
assumes modif: "\<forall>Z::'a. \<Gamma>,\<Theta> \<turnstile>\<^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 \<open>To prove a procedure implementation correct it suffices to assume
only the procedure specifications of procedures that actually
occur during evaluation of the body.
*}
\<close>
lemma Call_lemma:
assumes
Call: "\<forall>q \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
@ -3815,7 +3813,7 @@ lemma image_Un_conv: "f ` (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {x p Z}) = (\
by (auto iff: not_None_eq)
text {* Another proof of @{text MGT_Call}, maybe a little more readable *}
text \<open>Another proof of \<open>MGT_Call\<close>, maybe a little more readable\<close>
lemma
"\<forall>p \<in> dom \<Gamma>. \<forall>Z.
\<Gamma>,{} \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
@ -3827,15 +3825,15 @@ proof -
{
fix p Z \<sigma>
assume defined: "p \<in> dom \<Gamma>"
def Specs == "(\<Union>p\<in>dom \<Gamma>. \<Union>Z.
define Specs where "Specs = (\<Union>p\<in>dom \<Gamma>. \<Union>Z.
{({s. s=Z \<and>
\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
\<Gamma>\<turnstile>Call p\<down>Normal s},
p,
{t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
{t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})})"
def Specs_wf == "(\<lambda>p \<sigma>. (\<lambda>(P,q,Q,A).
(P \<inter> {s. ((s,q),\<sigma>,p) \<in> termi_call_steps \<Gamma>}, q, Q, A)) ` Specs)"
define Specs_wf where "Specs_wf p \<sigma> = (\<lambda>(P,q,Q,A).
(P \<inter> {s. ((s,q),\<sigma>,p) \<in> termi_call_steps \<Gamma>}, q, Q, A)) ` Specs" for p \<sigma>
have "\<Gamma>,Specs_wf p \<sigma>
\<turnstile>\<^sub>t\<^bsub>/F\<^esub>({\<sigma>} \<inter>
{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
@ -3883,4 +3881,4 @@ proof -
done
qed
end
end

2
tools/c-parser/Simpl/DPC0Expressions.thy
View File

@ -4,7 +4,7 @@
License: LGPL
*)
section {* SHORTENED! Parallel expressions in DPC/Hoare. *}
section \<open>SHORTENED! Parallel expressions in DPC/Hoare.\<close>
theory DPC0Expressions imports Main begin

18
tools/c-parser/Simpl/DPC0Library.thy
View File

@ -4,20 +4,20 @@
License: LGPL
*)
section {* DPC0 standard library *}
section \<open>DPC0 standard library\<close>
theory DPC0Library imports DPC0Expressions Vcg begin
text {* This theory constitutes a standard library for DPC0 programs. At
text \<open>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.
*}
\<close>
(* =================================================== *)
section {* Auxiliary functions for the concrete syntax *}
section \<open>Auxiliary functions for the concrete syntax\<close>
(* =================================================== *)
@ -34,7 +34,7 @@ where
(* ============================================= *)
section {* Concrete syntax for Contextualization *}
section \<open>Concrete syntax for Contextualization\<close>
(* ============================================= *)
syntax
@ -53,7 +53,7 @@ translations
"_WhereElse m c s1 s2" => "(_Loc (_locinit c (p_and \<acute>c m)) s1);;
(_Loc (_locinit c (p_and \<acute>c (p_not m))) s2)"
print_translation {*
print_translation \<open>
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
*}
\<close>
print_ast_translation {*
print_ast_translation \<open>
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
*}
\<close>
end

18
tools/c-parser/Simpl/HeapList.thy
View File

@ -25,12 +25,12 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Paths and Lists in the Heap *}
section \<open>Paths and Lists in the Heap\<close>
theory HeapList
imports Simpl_Heap
begin
text {* Adapted from 'HOL/Hoare/Heap.thy'. *}
text \<open>Adapted from 'HOL/Hoare/Heap.thy'.\<close>
subsection "Paths in The Heap"
@ -67,10 +67,10 @@ lemma Path_upd_same [simp]:
((p=Null \<and> q=Null \<and> qs = []) \<or> (p\<noteq>Null \<and> q=p \<and> (\<forall>x\<in>set qs. x=p)))"
by (induct qs) auto
text {* @{thm[source] Path_upd_same} prevents
text \<open>@{thm[source] Path_upd_same} prevents
@{term "p\<noteq>Null \<Longrightarrow> Path p (f(p:=p)) q qs = X"} from looping, because of
@{thm[source] Path_not_Null_iff} and @{thm[source]fun_upd_apply}.
*}
\<close>
lemma notin_Path_updateI [intro]:
"\<lbrakk>Path p h q ps ; r \<notin> set ps\<rbrakk> \<Longrightarrow> 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 \<open>@{thm[source] List_upd_same} prevents
@{term "p\<noteq>Null \<Longrightarrow> List p (h(p:=p)) as = X"} from looping, because of
@{thm[source] List_not_Null} and @{thm[source] fun_upd_apply}.
*}
\<close>
lemma List_update_new [simp]: "\<lbrakk>set ps \<subseteq> set alloc\<rbrakk>
\<Longrightarrow> 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 \<open>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\<close>
lemma conj_impl_simp: "(P \<and> Q \<longrightarrow> K) = (P \<longrightarrow> Q \<longrightarrow> K)"
by auto
@ -294,4 +294,4 @@ apply (drule (1) the1_equality)
apply simp
done
end
end

8
tools/c-parser/Simpl/Hoare.thy
View File

@ -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 \<open>Auxiliary Definitions/Lemmas to Facilitate Hoare Logic\<close>
theory Hoare imports HoarePartial HoareTotal begin
@ -322,9 +322,9 @@ lemma in_mlex_iff:
lemma in_inv_image_iff: "(x,y) \<in> inv_image r f = ((f x, f y) \<in> r)"
by (simp add: inv_image_def)
text {* This is actually the same as @{thm [source] wf_mlex}. However, this basic
text \<open>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.
*}
\<close>
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: "(\<forall>x. x = k \<longrightarrow> Q) = Q"
"(\<forall>x. k = x \<longrightarrow> Q) = Q"
by auto
end
end

32
tools/c-parser/Simpl/HoarePartial.thy
View File

@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Derived Hoare Rules for Partial Correctness *}
section \<open>Derived Hoare Rules for Partial Correctness\<close>
theory HoarePartial imports HoarePartialProps begin
@ -367,8 +367,8 @@ proof -
done
qed
text {* @{term "J"} will be instantiated by tactic with @{term "gs' \<inter> I"} for
those guards that are not stripped.*}
text \<open>@{term "J"} will be instantiated by tactic with @{term "gs' \<inter> I"} for
those guards that are not stripped.\<close>
lemma WhileAnnoG:
"\<Gamma>,\<Theta>\<turnstile>\<^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 \<open>This form stems from @{term "strip_guards F (whileAnnoG gs b I V c)"}\<close>
lemma WhileNoGuard':
assumes P_I: "P \<subseteq> I"
@ -929,8 +929,8 @@ qed
lemma ProcProcParModifyReturn:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
--{* @{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it. *}
\<comment>\<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
@ -953,8 +953,8 @@ qed
lemma ProcProcParModifyReturnSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
--{* @{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it. *}
\<comment>\<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
@ -978,8 +978,8 @@ qed
lemma ProcProcParModifyReturnNoAbr:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
--{* @{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it. *}
\<comment>\<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
@ -998,8 +998,8 @@ qed
lemma ProcProcParModifyReturnNoAbrSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
--{* @{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it. *}
\<comment>\<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
@ -1106,16 +1106,16 @@ proof -
qed
subsection {* Rules for Single-Step Proof \label{sec:hoare-isar} *}
subsection \<open>Rules for Single-Step Proof \label{sec:hoare-isar}\<close>
text {*
text \<open>
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.
*}
\<close>
lemma annotateI [trans]:
"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>P anno Q,A; c = anno\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>P c Q,A"
@ -1209,4 +1209,4 @@ lemma WhileConj [intro?]:
(* FIXME: Add rules for guarded while *)
end
end

34
tools/c-parser/Simpl/HoarePartialDef.thy
View File

@ -26,12 +26,12 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Hoare Logic for Partial Correctness *}
section \<open>Hoare Logic for Partial Correctness\<close>
theory HoarePartialDef imports Semantic begin
type_synonym ('s,'p) quadruple = "('s assn \<times> 'p \<times> 's assn \<times> 's assn)"
subsection {* Validity of Hoare Tuples: @{text "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A"} *}
subsection \<open>Validity of Hoare Tuples: \<open>\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A\<close>\<close>
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 \<open>Properties of Validity\<close>
lemma valid_iff_nvalid: "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A = (\<forall>n. \<Gamma>\<Turnstile>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' \<in> Normal ` Q \<union> Abrupt ` A"
have *: "t' \<in> Normal ` Q \<union> 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' \<in> Normal ` Q \<union> Abrupt ` A"
have *: "t' \<in> Normal ` Q \<union> 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 "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"} *}
subsection \<open>The Hoare Rules: \<open>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A\<close>\<close>
lemma mono_WeakenContext: "A \<subseteq> B \<Longrightarrow>
(\<lambda>(P, c, Q, A'). (\<Gamma>, \<Theta>, F, P, c, Q, A') \<in> A) x \<longrightarrow>
@ -284,14 +282,14 @@ where
| ExFalso: "\<lbrakk>\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A; \<not> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
-- {* This is a hack rule that enables us to derive completeness for
an arbitrary context @{text "\<Theta>"}, from completeness for an empty context.*}
\<comment> \<open>This is a hack rule that enables us to derive completeness for
an arbitrary context \<open>\<Theta>\<close>, from completeness for an empty context.\<close>
text {* Does not work, because of rule ExFalso, the context @{text "\<Theta>"} is to blame.
text \<open>Does not work, because of rule ExFalso, the context \<open>\<Theta>\<close> is to blame.
A weaker version with empty context can be derived from soundness
and completeness later on. *}
and completeness later on.\<close>
lemma hoare_strip_\<Gamma>:
assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P p Q,A"
shows "strip (-F) \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P p Q,A"
@ -385,7 +383,7 @@ next
qed (blast intro: hoarep.intros)+
subsection {* Some Derived Rules *}
subsection \<open>Some Derived Rules\<close>
lemma Conseq': "\<forall>s. s \<in> P \<longrightarrow>
(\<exists>P' Q' A'.
@ -433,4 +431,4 @@ apply blast
apply blast
done
end
end

44
tools/c-parser/Simpl/HoarePartialProps.thy
View File

@ -26,11 +26,11 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Properties of Partial Correctness Hoare Logic *}
section \<open>Properties of Partial Correctness Hoare Logic\<close>
theory HoarePartialProps imports HoarePartialDef begin
subsection {* Soundness *}
subsection \<open>Soundness\<close>
lemma hoare_cnvalid:
assumes hoare: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
@ -411,7 +411,7 @@ qed
theorem hoare_sound: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
by (iprover intro: cnvalid_to_cvalid hoare_cnvalid)
subsection {* Completeness *}
subsection \<open>Completeness\<close>
lemma MGT_valid:
"\<Gamma>\<Turnstile>\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> 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 \<open>The consequence rule where the existential @{term Z} is instantiated
to @{term s}. Usefull in proof of \<open>MGT_lemma\<close>.\<close>
lemma ConseqMGT:
assumes modif: "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)"
assumes impl: "\<And>s. s \<in> P \<Longrightarrow> s \<in> P' s \<and> (\<forall>t. t \<in> Q' s \<longrightarrow> t \<in> Q) \<and>
@ -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 \<open>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)\<close>
lemma MGT_implies_complete':
assumes MGT: "\<forall>Z. \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub>
{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> 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 \<open>Semantic equivalence of both kind of formulations\<close>
lemma valid_involved_to_valid:
assumes valid:
"\<forall>Z. \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}"
@ -526,10 +526,10 @@ lemma valid_involved_to_valid:
apply fastforce
done
text {* The sophisticated consequence rule allow us to do this
text \<open>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 \<in> P"} *}
choose the instance of @{term Z} under the assumption of an state @{term "s \<in> P"}\<close>
lemma
assumes deriv:
"\<forall>Z. \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}"
@ -1068,9 +1068,9 @@ proof (rule hoare_complete)
qed
subsection {* And Now: Some Useful Rules *}
subsection \<open>And Now: Some Useful Rules\<close>
subsubsection {* Consequence *}
subsubsection \<open>Consequence\<close>
lemma LiberalConseq_sound:
@ -1334,7 +1334,7 @@ apply (rule LiberalConseq_noguards_nothrows
apply auto
done
subsubsection {* Modify Return *}
subsubsection \<open>Modify Return\<close>
lemma ProcModifyReturn_sound:
assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>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 \<open>DynCall\<close>
lemma dynProcModifyReturn_sound:
assumes valid_call: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
@ -1825,7 +1825,7 @@ apply assumption
done
subsubsection {* Conjunction of Postcondition *}
subsubsection \<open>Conjunction of Postcondition\<close>
lemma PostConjI_sound:
assumes valid_Q: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
@ -1878,12 +1878,12 @@ proof (rule cnvalidI)
show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> X)"
proof -
from cnvalidD [OF validF [rule_format] ctxt exec P t_noFault]
have "t \<in> Normal ` Q \<union> Abrupt ` A".
moreover from this have "t \<notin> Fault ` G"
have *: "t \<in> Normal ` Q \<union> Abrupt ` A".
then have "t \<notin> Fault ` G"
by auto
from cnvalidD [OF validG [rule_format] ctxt' exec P' this]
have "t \<in> Normal ` R \<union> 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 \<open>Weaken Context\<close>
lemma WeakenContext_sound:
@ -1934,7 +1934,7 @@ using deriv_ctxt
apply (blast intro: hoare_cnvalid)
done
subsubsection {* Guards and Guarantees *}
subsubsection \<open>Guards and Guarantees\<close>
lemma SplitGuards_sound:
assumes valid_c1: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>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 \<open>Restricting the Procedure Environment\<close>
lemma nvalid_restrict_to_nvalid:
assumes valid_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
@ -2396,4 +2396,4 @@ shows "\<Gamma>,{}\<turnstile>\<^bsub>/F'\<^esub> P c Q,A"
apply (insert hoare_sound [OF deriv_c])
by (simp add: cvalid_def)
end
end

34
tools/c-parser/Simpl/HoareTotal.thy
View File

@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Derived Hoare Rules for Total Correctness *}
section \<open>Derived Hoare Rules for Total Correctness\<close>
theory HoareTotal imports HoareTotalProps begin
@ -37,8 +37,8 @@ lemma conseq_no_aux:
\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
by (rule conseq [where P'="\<lambda>Z. P'" and Q'="\<lambda>Z. Q'" and A'="\<lambda>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 \<open>If for example a specification for a "procedure pointer" parameter
is in the precondition we can extract it with this rule\<close>
lemma conseq_exploit_pre:
"\<lbrakk>\<forall>s \<in> P. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s} \<inter> P) c Q,A\<rbrakk>
\<Longrightarrow>
@ -387,8 +387,8 @@ qed
lemma "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> b) c Q,A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> b) (Seq c (Guard f Q Skip)) Q,A"
oops
text {* @{term "J"} will be instantiated by tactic with @{term "gs' \<inter> I"} for
those guards that are not stripped.*}
text \<open>@{term "J"} will be instantiated by tactic with @{term "gs' \<inter> I"} for
those guards that are not stripped.\<close>
lemma WhileAnnoG:
"\<Gamma>,\<Theta>\<turnstile>\<^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:
\<Gamma>,\<Theta>\<turnstile>\<^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 \<open>This form stems from @{term "strip_guards F (whileAnnoG gs b I V c)"}\<close>
lemma WhileNoGuard':
assumes P_I: "P \<subseteq> I"
assumes deriv_body: "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) c ({t. (t, \<sigma>) \<in> V} \<inter> I),A"
@ -972,8 +972,8 @@ qed
lemma ProcProcParModifyReturn:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
--{* @{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it. *}
\<comment>\<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
@ -997,8 +997,8 @@ qed
lemma ProcProcParModifyReturnSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
--{* @{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it. *}
\<comment>\<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
@ -1021,8 +1021,8 @@ qed
lemma ProcProcParModifyReturnNoAbr:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
--{* @{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it. *}
\<comment>\<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
@ -1042,8 +1042,8 @@ qed
lemma ProcProcParModifyReturnNoAbrSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
--{* @{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it. *}
\<comment>\<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> 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 \<open>Rules for Single-Step Proof \label{sec:hoare-isar}\<close>
text {*
text \<open>
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.
*}
\<close>
lemma annotateI [trans]:

18
tools/c-parser/Simpl/HoareTotalDef.thy
View File

@ -26,11 +26,11 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Hoare Logic for Total Correctness *}
section \<open>Hoare Logic for Total Correctness\<close>
theory HoareTotalDef imports HoarePartialDef Termination begin
subsection {* Validity of Hoare Tuples: @{text "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"} *}
subsection \<open>Validity of Hoare Tuples: \<open>\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A\<close>\<close>
definition
validt :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] \<Rightarrow> 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 \<open>Properties of Validity\<close>
lemma validtI:
"\<lbrakk>\<And>s t. \<lbrakk>\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t;s \<in> P;t \<notin> Fault ` F\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q \<union> 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 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" } *}
subsection \<open>The Hoare Rules: \<open>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A\<close>\<close>
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
\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
| ExFalso: "\<lbrakk>\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A; \<not> \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^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 "\<Theta>"}, from completeness for an empty context.*}
\<comment> \<open>This is a hack rule that enables us to derive completeness for
an arbitrary context \<open>\<Theta>\<close>, from completeness for an empty context.\<close>
text {* Does not work, because of rule ExFalso, the context @{text \<Theta>} is to blame.
text \<open>Does not work, because of rule ExFalso, the context \<open>\<Theta>\<close> is to blame.
A weaker version with empty context can be derived from soundness
later on. *}
later on.\<close>
lemma hoaret_to_hoarep:
assumes hoaret: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P p Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^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 \<open>Some Derived Rules\<close>
lemma Conseq': "\<forall>s. s \<in> P \<longrightarrow>

42
tools/c-parser/Simpl/HoareTotalProps.thy
View File

@ -26,11 +26,11 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Properties of Total Correctness Hoare Logic *}
section \<open>Properties of Total Correctness Hoare Logic\<close>
theory HoareTotalProps imports SmallStep HoareTotalDef HoarePartialProps begin
subsection {* Soundness *}
subsection \<open>Soundness\<close>
lemma hoaret_sound:
assumes hoare: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
@ -621,7 +621,7 @@ proof -
by (rule hoare_complete)
qed
subsection {* Completeness *}
subsection \<open>Completeness\<close>
lemma MGT_valid:
"\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>c\<down>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 \<open>The consequence rule where the existential @{term Z} is instantiated
to @{term s}. Usefull in proof of \<open>MGT_lemma\<close>.\<close>
lemma ConseqMGT:
assumes modif: "\<forall>Z::'a. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z::'a assn) c (Q' Z),(A' Z)"
assumes impl: "\<And>s. s \<in> P \<Longrightarrow> s \<in> P' s \<and> (\<forall>t. t \<in> Q' s \<longrightarrow> t \<in> Q) \<and>
@ -2009,10 +2009,10 @@ next
qed
text {* To prove a procedure implementation correct it suffices to assume
text \<open>To prove a procedure implementation correct it suffices to assume
only the procedure specifications of procedures that actually
occur during evaluation of the body.
*}
\<close>
lemma Call_lemma:
assumes A:
@ -2093,7 +2093,7 @@ lemma image_Un_conv: "f ` (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {x p Z}) = (\
by (auto iff: not_None_eq)
text {* Another proof of @{text MGT_Call}, maybe a little more readable *}
text \<open>Another proof of \<open>MGT_Call\<close>, maybe a little more readable\<close>
lemma
"\<forall>p \<in> dom \<Gamma>. \<forall>Z.
\<Gamma>,{} \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
@ -2105,15 +2105,15 @@ proof -
{
fix p Z \<sigma>
assume defined: "p \<in> dom \<Gamma>"
def Specs == "(\<Union>p\<in>dom \<Gamma>. \<Union>Z.
define Specs where "Specs = (\<Union>p\<in>dom \<Gamma>. \<Union>Z.
{({s. s=Z \<and>
\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
\<Gamma>\<turnstile>Call p\<down>Normal s},
p,
{t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
{t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})})"
def Specs_wf == "(\<lambda>p \<sigma>. (\<lambda>(P,q,Q,A).
(P \<inter> {s. ((s,q),\<sigma>,p) \<in> termi_call_steps \<Gamma>}, q, Q, A)) ` Specs)"
define Specs_wf where "Specs_wf p \<sigma> = (\<lambda>(P,q,Q,A).
(P \<inter> {s. ((s,q),\<sigma>,p) \<in> termi_call_steps \<Gamma>}, q, Q, A)) ` Specs" for p \<sigma>
have "\<Gamma>,Specs_wf p \<sigma>
\<turnstile>\<^sub>t\<^bsub>/F\<^esub>({\<sigma>} \<inter>
{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
@ -2181,9 +2181,9 @@ next
by (rule ExFalso)
qed
subsection {* And Now: Some Useful Rules *}
subsection \<open>And Now: Some Useful Rules\<close>
subsubsection {* Modify Return *}
subsubsection \<open>Modify Return\<close>
lemma ProcModifyReturn_sound:
assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^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 \<open>DynCall\<close>
lemma dynProcModifyReturn_sound:
@ -2823,7 +2823,7 @@ apply (rule hoare_sound [OF modif [rule_format]])
apply assumption
done
subsubsection {* Conjunction of Postcondition *}
subsubsection \<open>Conjunction of Postcondition\<close>
lemma PostConjI_sound:
assumes valid_Q: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
@ -2881,12 +2881,12 @@ proof (rule cvalidtI)
show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> X)"
proof -
from cvalidt_postD [OF validF [rule_format] ctxt exec P t_noFault]
have "t \<in> Normal ` Q \<union> Abrupt ` A".
moreover from this have "t \<notin> Fault ` G"
have t: "t \<in> Normal ` Q \<union> Abrupt ` A".
then have "t \<notin> Fault ` G"
by auto
from cvalidt_postD [OF validG [rule_format] ctxt' exec P' this]
have "t \<in> Normal ` R \<union> 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 \<open>Guards and Guarantees\<close>
lemma SplitGuards_sound:
assumes valid_c1: "\<Gamma>,\<Theta>\<Turnstile>\<^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 \<open>Restricting the Procedure Environment\<close>
lemma validt_restrict_to_validt:
assumes validt_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
@ -3429,7 +3429,7 @@ shows "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
apply (insert hoaret_sound [OF deriv_c])
by (simp add: cvalidt_def)
subsubsection {* Miscellaneous *}
subsubsection \<open>Miscellaneous\<close>
lemma augment_Faults:
assumes deriv_c: "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"

70
tools/c-parser/Simpl/Language.thy
View File

@ -26,15 +26,15 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* The Simpl Syntax *}
section \<open>The Simpl Syntax\<close>
theory Language imports "~~/src/HOL/Library/Old_Recdef" begin
subsection {* The Core Language *}
subsection \<open>The Core Language\<close>
text {* We use a shallow embedding of boolean expressions as well as assertions
text \<open>We use a shallow embedding of boolean expressions as well as assertions
as sets of states.
*}
\<close>
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 \<open>Derived Language Constructs\<close>
definition
raise:: "('s \<Rightarrow> 's) \<Rightarrow> ('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 \<open>Operations on Simpl-Syntax\<close>
subsubsection {* Normalisation of Sequential Composition: @{text "sequence"}, @{text "flatten"} and @{text "normalize"} *}
subsubsection \<open>Normalisation of Sequential Composition: \<open>sequence\<close>, \<open>flatten\<close> and \<open>normalize\<close>\<close>
primrec flatten:: "('s,'p,'f) com \<Rightarrow> ('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 \<open>Sequencial composition with guards in the body is not preserved by
normalize\<close>
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 \<open>Stripping Guards: \<open>strip_guards\<close>\<close>
primrec strip_guards:: "'f set \<Rightarrow> ('s,'p,'f) com \<Rightarrow> ('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 \<open>Marking Guards: \<open>mark_guards\<close>\<close>
primrec mark_guards:: "'f \<Rightarrow> ('s,'p,'g) com \<Rightarrow> ('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 \<open>Merging Guards: \<open>merge_guards\<close>\<close>
primrec merge_guards:: "('s,'p,'f) com \<Rightarrow> ('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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow>
\<exists>c1' c2'. c = Seq c1' c2' \<and> merge_guards c1' = c1 \<and> 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 \<Longrightarrow>
\<exists>c1' c2'. c = Cond b c1' c2' \<and> merge_guards c1' = c1 \<and> 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' \<Longrightarrow>
\<exists>c''. c = While b c'' \<and> 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 \<Longrightarrow> 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' \<Longrightarrow>
\<exists>c''. c = DynCom c'' \<and> (\<lambda>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 \<Longrightarrow> 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 \<Longrightarrow>
\<exists>c1' c2'. c = Catch c1' c2' \<and> merge_guards c1' = c1 \<and> 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' \<Longrightarrow> \<exists>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 (\<lambda>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 \<open>@{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.\<close>
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 \<and> nothrows c\<^sub>2)"
subsubsection {* Intersecting Guards: @{text "c\<^sub>1 \<inter>\<^sub>g c\<^sub>2"}*}
subsubsection \<open>Intersecting Guards: \<open>c\<^sub>1 \<inter>\<^sub>g c\<^sub>2\<close>\<close>
inductive_set com_rel ::"(('s,'p,'f) com \<times> ('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: "\<And>c. (c1 \<inter>\<^sub>g c2) = Some c \<Longrightarrow> (c2 \<inter>\<^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 \<inter>\<^sub>g c2) = Some c =
(\<exists>bdy2 bdy. c2 =While cnd bdy2 \<and> (bdy1 \<inter>\<^sub>g bdy2) = Some bdy \<and>
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 \<inter>\<^sub>g c2) = Some c =
(c2=Call p \<and> 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 \<inter>\<^sub>g c2) = Some c =
(\<exists>f2. c2=DynCom f2 \<and> (\<forall>s. ((f1 s) \<inter>\<^sub>g (f2 s)) \<noteq> None) \<and>
c=DynCom (\<lambda>s. the ((f1 s) \<inter>\<^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 \<subseteq>\<^sub>g c\<^sub>2"} *}
subsubsection \<open>Subset on Guards: \<open>c\<^sub>1 \<subseteq>\<^sub>g c\<^sub>2\<close>\<close>
consts subseteq_guards:: "('s,'p,'f) com \<times> ('s,'p,'f) com \<Rightarrow> bool"
@ -1145,7 +1145,7 @@ lemma subseteq_guards_DynCom:
lemma subseteq_guards_Guard:
"c \<subseteq>\<^sub>g Guard f g c' \<Longrightarrow>
(c \<subseteq>\<^sub>g c') \<or> (\<exists>c''. c=Guard f g c'' \<and> (c'' \<subseteq>\<^sub>g c'))"
by (cases c) (auto split: split_if_asm)
by (cases c) (auto split: if_split_asm)
lemma subseteq_guards_Throw:
"c \<subseteq>\<^sub>g Throw \<Longrightarrow> c = Throw"

1
tools/c-parser/Simpl/ROOT
View File

@ -1,6 +1,7 @@
chapter AFP
session Simpl (AFP) = HOL +
options [timeout = 600]
theories
Simpl
document_files

28
tools/c-parser/Simpl/Semantic.thy
View File

@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Big-Step Semantics for Simpl *}
section \<open>Big-Step Semantics for Simpl\<close>
theory Semantic imports Language begin
notation
@ -69,10 +69,10 @@ lemma not_isFault_iff: "(\<not> isFault t) = (\<forall>f. t \<noteq> Fault f)"
by (auto elim: isFaultE)
(* ************************************************************************* *)
subsection {* Big-Step Execution: @{text "\<Gamma>\<turnstile>\<langle>c, s\<rangle> \<Rightarrow> t"} *}
subsection \<open>Big-Step Execution: \<open>\<Gamma>\<turnstile>\<langle>c, s\<rangle> \<Rightarrow> t\<close>\<close>
(* ************************************************************************* *)
text {* The procedure environment *}
text \<open>The procedure environment\<close>
type_synonym ('s,'p,'f) body = "'p \<Rightarrow> ('s,'p,'f) com option"
inductive
@ -444,7 +444,7 @@ lemma exec_assoc: "\<Gamma>\<turnstile>\<langle>Seq c1 (Seq c2 c3),s\<rangle> \<
(* ************************************************************************* *)
subsection {* Big-Step Execution with Recursion Limit: @{text "\<Gamma>\<turnstile>\<langle>c, s\<rangle> =n\<Rightarrow> t"} *}
subsection \<open>Big-Step Execution with Recursion Limit: \<open>\<Gamma>\<turnstile>\<langle>c, s\<rangle> =n\<Rightarrow> t\<close>\<close>
(* ************************************************************************* *)
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 \<open>Lemmas about @{const "sequence"}, @{const "flatten"} and
@{const "normalize"}\<close>
(* ************************************************************************ *)
lemma execn_sequence_app: "\<And>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 \<subseteq>\<^sub>g c\<^sub>2"} *}
subsection \<open>Lemmas about @{term "c\<^sub>1 \<subseteq>\<^sub>g c\<^sub>2"}\<close>
(* ************************************************************************ *)
lemma execn_to_execn_subseteq_guards: "\<And>c s t n. \<lbrakk>c \<subseteq>\<^sub>g c'; \<Gamma>\<turnstile>\<langle>c,s\<rangle> =n\<Rightarrow> t\<rbrakk>
@ -1953,7 +1953,7 @@ qed
(* ************************************************************************* *)
subsection {* Lemmas about @{const "merge_guards"} *}
subsection \<open>Lemmas about @{const "merge_guards"}\<close>
(* ************************************************************************ *)
@ -2106,7 +2106,7 @@ next
proof (cases "s \<in> 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 \<open>Lemmas about @{const "mark_guards"}\<close>
(* ************************************************************************ *)
lemma execn_to_execn_mark_guards:
@ -2863,7 +2863,7 @@ proof -
qed
(* ************************************************************************* *)
subsection {* Lemmas about @{const "strip_guards"} *}
subsection \<open>Lemmas about @{const "strip_guards"}\<close>
(* ************************************************************************* *)
lemma execn_to_execn_strip_guards:
@ -3767,7 +3767,7 @@ proof -
qed
(* ************************************************************************* *)
subsection {* Lemmas about @{term "c\<^sub>1 \<inter>\<^sub>g c\<^sub>2"} *}
subsection \<open>Lemmas about @{term "c\<^sub>1 \<inter>\<^sub>g c\<^sub>2"}\<close>
(* ************************************************************************* *)
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 \<Longrightarrow> 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 \<Longrightarrow> (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: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> =n\<Rightarrow> t"

30
tools/c-parser/Simpl/Simpl.thy
View File

@ -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
(*>*)
(*>*)

6
tools/c-parser/Simpl/Simpl_Heap.thy
View File

@ -92,13 +92,13 @@ consts Null :: ref
definition new :: "ref set \<Rightarrow> ref" where
"new A = (SOME a. a \<notin> {Null} \<union> A)"
text {*
text \<open>
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 \<open>fixes\<close> of a locale
with @{prop "finite A \<Longrightarrow> new A \<notin> A \<union> {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.
*}
\<close>
lemma new_notin [simp,intro]:
"finite A \<Longrightarrow> new (A) \<notin> A"

52
tools/c-parser/Simpl/SmallStep.thy
View File

@ -26,14 +26,14 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Small-Step Semantics and Infinite Computations*}
section \<open>Small-Step Semantics and Infinite Computations\<close>
theory SmallStep imports Termination
begin
text {* The redex of a statement is the substatement, which is actually altered
text \<open>The redex of a statement is the substatement, which is actually altered
by the next step in the small-step semantics.
*}
\<close>
primrec redex:: "('s,'p,'f)com \<Rightarrow> ('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 "\<Gamma>\<turnstile>(c, s) \<rightarrow> (c', s')"}*}
subsection \<open>Small-Step Computation: \<open>\<Gamma>\<turnstile>(c, s) \<rightarrow> (c', s')\<close>\<close>
type_synonym ('s,'p,'f) config = "('s,'p,'f)com \<times> ('s,'f) xstate"
inductive "step"::"[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] \<Rightarrow> bool"
@ -138,12 +138,12 @@ inductive_cases step_Normal_elim_cases [cases set]:
"\<Gamma>\<turnstile>(Catch c1 c2,Normal s) \<rightarrow> u"
text {* The final configuration is either of the form @{text "(Skip,_)"} for normal
text \<open>The final configuration is either of the form \<open>(Skip,_)\<close> 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.\<close>
definition final:: "('s,'p,'f) config \<Rightarrow> bool" where
"final cfg = (fst cfg=Skip \<or> (fst cfg=Throw \<and> (\<exists>s. snd cfg=Normal s)))"
@ -168,7 +168,7 @@ abbreviation
(* ************************************************************************ *)
subsection {* Structural Properties of Small Step Computations *}
subsection \<open>Structural Properties of Small Step Computations\<close>
(* ************************************************************************ *)
lemma redex_not_Seq: "redex c = Seq c1 c2 \<Longrightarrow> P"
@ -377,7 +377,7 @@ next
qed
(* ************************************************************************ *)
subsection {* Equivalence between Small-Step and Big-Step Semantics *}
subsection \<open>Equivalence between Small-Step and Big-Step Semantics\<close>
(* ************************************************************************ *)
theorem exec_impl_steps:
@ -967,7 +967,7 @@ next
qed
(* ************************************************************************ *)
subsection {* Infinite Computations: @{text "\<Gamma>\<turnstile>(c, s) \<rightarrow> \<dots>(\<infinity>)"}*}
subsection \<open>Infinite Computations: \<open>\<Gamma>\<turnstile>(c, s) \<rightarrow> \<dots>(\<infinity>)\<close>\<close>
(* ************************************************************************ *)
definition inf:: "('s,'p,'f) body \<Rightarrow> ('s,'p,'f) config \<Rightarrow> bool"
@ -979,7 +979,7 @@ lemma not_infI: "\<lbrakk>\<And>f. \<lbrakk>f 0 = cfg; \<And>i. \<Gamma>\<turnst
by (auto simp add: inf_def)
(* ************************************************************************ *)
subsection {* Equivalence between Termination and the Absence of Infinite Computations*}
subsection \<open>Equivalence between Termination and the Absence of Infinite Computations\<close>
(* ************************************************************************ *)
@ -1092,12 +1092,12 @@ next
by (blast dest: step_preserves_termination)
qed
ML {*
ML \<open>
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}));
*}
\<close>
lemma steps_preserves_termination':
assumes steps: "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>+ (c',s')"
@ -1278,7 +1278,7 @@ proof -
show ?thesis
proof (cases "\<exists>i. final (head (f i))")
case True
def k\<equiv>"(LEAST i. final (head (f i)))"
define k where "k = (LEAST i. final (head (f i)))"
have less_k: "\<forall>i<k. \<not> final (head (f i))"
apply (intro allI impI)
apply (unfold k_def)
@ -1326,7 +1326,7 @@ proof -
obtain "\<Gamma>\<turnstile>(Seq Skip c\<^sub>2,s') \<rightarrow> (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\<equiv>"\<lambda>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 "\<Gamma>\<turnstile>(Seq Throw c\<^sub>2,s') \<rightarrow> (Throw,s')" and
f_Suc_k: "f (k + 1) = (Throw,s')"
by (fastforce elim: step_elim_cases intro: step.intros)
def g\<equiv>"\<lambda>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 "\<exists>i. final (head (f i))")
case True
def k\<equiv>"(LEAST i. final (head (f i)))"
define k where "k = (LEAST i. final (head (f i)))"
have less_k: "\<forall>i<k. \<not> final (head (f i))"
apply (intro allI impI)
apply (unfold k_def)
@ -1463,7 +1463,7 @@ proof -
obtain "\<Gamma>\<turnstile>(Catch Throw c\<^sub>2,s') \<rightarrow> (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\<equiv>"\<lambda>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 \<open>
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}));
*}
\<close>
lemma steps_redex':
assumes steps: "\<Gamma>\<turnstile> (r, s) \<rightarrow>\<^sup>+ (r', s')"
@ -2310,8 +2310,8 @@ proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain,
\<Gamma>\<turnstile>Call p \<down> Normal s \<and>
(\<exists>c. \<Gamma>\<turnstile> (Call p, Normal s) \<rightarrow>\<^sup>+ (c, Normal t) \<and> redex c = Call q))
(f (Suc i)) (f i)"
def s\<equiv>"\<lambda>i::nat. fst (f i)"
def p\<equiv>"\<lambda>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': "\<forall>i. \<Gamma>\<turnstile>Call (p i) \<down> Normal (s i) \<and>
(\<exists>c. \<Gamma>\<turnstile> (Call (p i), Normal (s i)) \<rightarrow>\<^sup>+ (c, Normal (s (i+1))) \<and>
@ -2335,7 +2335,7 @@ proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain,
steps_c: "\<forall>i. \<Gamma>\<turnstile> (Call (p i), Normal (s i)) \<rightarrow>\<^sup>+ (c i, Normal (s (i+1)))" and
red_c: "\<forall>i. redex (c i) = Call (p (i+1))"
by auto
def g\<equiv>"\<lambda>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 \<open>Generalised Redexes\<close>
(* ************************************************************************* *)
text {*
text \<open>
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.
*}
\<close>
primrec redexes:: "('s,'p,'f)com \<Rightarrow> ('s,'p,'f)com set"
where
@ -3117,4 +3117,4 @@ using termi
by induct (auto intro: terminates.intros)
end
end

4
tools/c-parser/Simpl/StateSpace.thy
View File

@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* State Space Template *}
section \<open>State Space Template\<close>
theory StateSpace imports Hoare
begin
@ -43,4 +43,4 @@ record ('g, 'n, 'val) stateSP = "'g state" +
lemma upd_globals_conv: "upd_globals f = (\<lambda>s. s\<lparr>globals := f (globals s)\<rparr>)"
by (rule ext) (simp add: upd_globals_def)
end
end

2
tools/c-parser/Simpl/SyntaxTest.thy
View File

@ -94,4 +94,4 @@ end
end
(*>*)
(*>*)

74
tools/c-parser/Simpl/Termination.thy
View File

@ -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 \<open>Terminating Programs\<close>
theory Termination imports Semantic begin
subsection {* Inductive Characterisation: @{text "\<Gamma>\<turnstile>c\<down>s"}*}
subsection \<open>Inductive Characterisation: \<open>\<Gamma>\<turnstile>c\<down>s\<close>\<close>
inductive "terminates"::"('s,'p,'f) body \<Rightarrow> ('s,'p,'f) com \<Rightarrow> ('s,'f) xstate \<Rightarrow> bool"
("_\<turnstile>_ \<down> _" [60,20,60] 89)
@ -311,8 +311,8 @@ done
(* ************************************************************************* *)
subsection {* Lemmas about @{const "sequence"}, @{const "flatten"} and
@{const "normalize"} *}
subsection \<open>Lemmas about @{const "sequence"}, @{const "flatten"} and
@{const "normalize"}\<close>
(* ************************************************************************ *)
lemma terminates_sequence_app:
@ -630,7 +630,7 @@ lemma terminates_iff_terminates_normalize:
terminates_normalize_to_terminates)
(* ************************************************************************* *)
subsection {* Lemmas about @{const "strip_guards"} *}
subsection \<open>Lemmas about @{const "strip_guards"}\<close>
(* ************************************************************************* *)
lemma terminates_strip_guards_to_terminates: "\<And>s. \<Gamma>\<turnstile>strip_guards F c\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>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\<in>b'` have b: "s\<in>b" by simp
from eqs `\<Gamma>\<turnstile>c' \<down> Normal s` have "\<Gamma>\<turnstile>strip_guards F c \<down> Normal s"
with \<open>s\<in>b'\<close> have b: "s\<in>b" by simp
from eqs \<open>\<Gamma>\<turnstile>c' \<down> Normal s\<close> have "\<Gamma>\<turnstile>strip_guards F c \<down> Normal s"
by simp
hence term_c: "\<Gamma>\<turnstile>c \<down> 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 \<inter>\<^sub>g c\<^sub>2"} *}
subsection \<open>Lemmas about @{term "c\<^sub>1 \<inter>\<^sub>g c\<^sub>2"}\<close>
(* ************************************************************************* *)
lemma inter_guards_terminates:
@ -1131,7 +1131,7 @@ proof -
qed
(* ************************************************************************* *)
subsection {* Lemmas about @{const "mark_guards"} *}
subsection \<open>Lemmas about @{const "mark_guards"}\<close>
(* ************************************************************************ *)
lemma terminates_to_terminates_mark_guards:
@ -1383,7 +1383,7 @@ lemma terminates_mark_guards_to_terminates:
(* ************************************************************************* *)
subsection {* Lemmas about @{const "merge_guards"} *}
subsection \<open>Lemmas about @{const "merge_guards"}\<close>
(* ************************************************************************ *)
lemma terminates_to_terminates_merge_guards:
@ -1428,7 +1428,7 @@ next
have "s \<notin> 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 \<subseteq>\<^sub>g c\<^sub>2"} *}
subsection \<open>Lemmas about @{term "c\<^sub>1 \<subseteq>\<^sub>g c\<^sub>2"}\<close>
(* ************************************************************************ *)
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 "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this noFault_Seq have "\<Gamma>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
with noFault_Seq have "\<Gamma>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>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 "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'"
have *: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this s_in_b noFault_while have "\<Gamma>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
with s_in_b noFault_while have "\<Gamma>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>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 "\<Gamma>\<turnstile>strip_guards F c2 \<down> Normal s'"
proof -
from exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1
have "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this noFault_Catch have "\<Gamma>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
with noFault_Catch have "\<Gamma>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>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 \<open>Lemmas about @{const "strip_guards"}\<close>
(* ************************************************************************* *)
lemma terminates_noFault_strip:
@ -2048,12 +2045,11 @@ next
next
case False
with exec_strip_to_exec [OF exec_strip_c1] noFault_c1
have "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this noFault_Seq have "\<Gamma>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
with noFault_Seq have "\<Gamma>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>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 "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'"
have *: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this s_in_b noFault_while have "\<Gamma>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
with s_in_b noFault_while have "\<Gamma>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>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 \<Gamma>\<turnstile>c2 \<down> Normal s'"
proof -
from exec_strip_to_exec [OF exec_strip_c1] noFault_c1
have "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this noFault_Catch have "\<Gamma>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
with * noFault_Catch have "\<Gamma>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>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 \<open>Miscellaneous\<close>
(* ************************************************************************* *)
lemma terminates_while_lemma:
@ -2337,4 +2331,4 @@ next
qed
qed
end
end

704
tools/c-parser/Simpl/UserGuide.thy
View File

File diff suppressed because it is too large Load Diff

70
tools/c-parser/Simpl/Vcg.thy
View File

@ -25,7 +25,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Facilitating the Hoare Logic *}
section \<open>Facilitating the Hoare Logic\<close>
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 \<open>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
*}
\<close>
definition list_multsel:: "'a list \<Rightarrow> nat list \<Rightarrow> 'a list" (infixl "!!" 100)
where "xs !! ns = map (nth xs) ns"
@ -66,7 +66,7 @@ definition list_multupd:: "'a list \<Rightarrow> nat list \<Rightarrow> 'a list
nonterminal lmupdbinds and lmupdbind
syntax
-- {* multiple list update *}
\<comment> \<open>multiple list update\<close>
"_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 \<open>Some Fancy Syntax\<close>
(* priority guidline:
* If command should be atomic for the guard it must have at least priority 21.
*)
text {* reverse application *}
text \<open>reverse application\<close>
definition rapp:: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> '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 \<open>
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
*}
\<close>
print_ast_translation {*
print_ast_translation \<open>
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
*}
\<close>
print_ast_translation {*
print_ast_translation \<open>
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
*}
\<close>
@ -424,7 +424,7 @@ definition Let':: "['a, 'a => 'b] => 'b"
ML_file "hoare_syntax.ML"
parse_translation {*
parse_translation \<open>
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;
*}
\<close>
print_translation {*
print_translation \<open>
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;
*}
\<close>
(* decorate state components with suffix *)
@ -520,13 +520,13 @@ parse_ast_translation {*
*)
parse_translation {*
parse_translation \<open>
[(@{syntax_const "_antiquoteCur"},
K (Hoare_Syntax.antiquote_varname_tr @{syntax_const "_antiquoteCur"}))]
*}
\<close>
parse_translation {*
parse_translation \<open>
[(@{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)]
*}
\<close>
(*
(@{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 \<open>
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
*}
\<close>
parse_translation {*
parse_translation \<open>
[(@{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)]
*}
\<close>
parse_translation {*
parse_translation \<open>
[(@{syntax_const "_Init"}, Hoare_Syntax.init_tr),
(@{syntax_const "_Loc"}, Hoare_Syntax.loc_tr)]
*}
\<close>
print_translation {*
print_translation \<open>
[(@{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')]
*}
\<close>
print_translation {*
print_translation \<open>
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
*}
\<close>
syntax
"_Measure":: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set"
@ -629,7 +629,7 @@ translations
print_translation {*
print_translation \<open>
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
*}
\<close>
print_translation {*
print_translation \<open>
[(@{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')]
*}
\<close>
end
end

8
tools/c-parser/Simpl/XVcg.thy
View File

@ -32,11 +32,11 @@ imports Vcg
begin
text {* We introduce a syntactic variant of the let-expression so that we can
text \<open>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 \<open>vcg_simp\<close> we can declare equalities to be used
by the verification condition generator, while simplifying assertions.
*}
\<close>
syntax
"_Let'" :: "[letbinds, basicblock] => basicblock" ("(LET (_)/ IN (_))" 23)
@ -54,4 +54,4 @@ lemma Let'_split_conv [vcg_simp]:
(Let' x (\<lambda>p. (f p) (fst (g p)) (snd (g p))))"
by (simp add: split_def)
end
end

4
tools/c-parser/Simpl/ex/Closure.thy
View File

@ -303,7 +303,7 @@ lemma app_closure_spec:
apply blast
done
text {* Implementation of closures as association lists. *}
text \<open>Implementation of closures as association lists.\<close>
definition "gen_upd var es s = foldl (\<lambda>s (x,i). the (var x) i s) s es"
definition "ap es c \<equiv> (es@fst c,snd c)"
@ -349,4 +349,4 @@ proof -
by (simp add: c ap_def)
qed
end
end

2
tools/c-parser/Simpl/ex/ClosureEx.thy
View File

@ -262,4 +262,4 @@ apply (erule allE)
apply assumption
done
end
end

24
tools/c-parser/Simpl/ex/Compose.thy
View File

@ -31,14 +31,14 @@ section "Experiments on State Composition"
theory Compose imports "../HoareTotalProps" begin
text {*
text \<open>
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 \<open>statespaces\<close> instead we get this kind of compositionality for free.
\<close>
subsection {* Changing the State-Space *}
subsection \<open>Changing the State-Space\<close>
(* 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 \<open>
The problem is that @{term "(lift\<^sub>c project inject \<circ> \<Gamma>)"} is quite
a strong premise. The problem is that @{term "\<Gamma>"} is a function here.
A map would be better. We only have to lift those procedures in the domain
of @{term "\<Gamma>"}:
@{text "\<Gamma> p = Some bdy \<longrightarrow> \<Gamma>' p = Some lift\<^sub>c project inject bdy"}.
\<open>\<Gamma> p = Some bdy \<longrightarrow> \<Gamma>' p = Some lift\<^sub>c project inject bdy\<close>.
We then can com up with theorems that allow us to extend the domains
of @{term \<Gamma>} and preserve validity.
*}
\<close>
lemma (in lift_state_space)
@ -885,17 +885,15 @@ proof (rule validI)
Normal ` (Modif (project s)) \<union> Abrupt ` (ModifAbr (project s))"
using valid [rule_format, of "(project s)"]
by (auto simp add: valid_def project\<^sub>x_def)
hence "t \<in> Normal ` lift\<^sub>s (Modif (project s)) \<union>
hence t: "t \<in> Normal ` lift\<^sub>s (Modif (project s)) \<union>
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 \<notin> Fault ` UNIV \<union> {Stuck}"
then have "t \<notin> Fault ` UNIV \<union> {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 \<open>Renaming Procedures\<close>
primrec rename:: "('p \<Rightarrow> 'q) \<Rightarrow> ('s,'p,'f) com \<Rightarrow> ('s,'q,'f) com"
where

2
tools/c-parser/Simpl/ex/Quicksort.thy
View File

@ -278,4 +278,4 @@ apply (erule_tac x=x in allE)+
apply (force dest!: perm_set_eq)
done
end
end

350
tools/c-parser/Simpl/ex/VcgEx.thy
View File

@ -26,21 +26,21 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Examples using the Verification Environment *}
section \<open>Examples using the Verification Environment\<close>
theory VcgEx imports "../HeapList" "../Vcg" begin
text {* Some examples, especially the single-step Isar proofs are taken from
text \<open>Some examples, especially the single-step Isar proofs are taken from
\texttt{HOL/Isar\_examples/HoareEx.thy}.
*}
\<close>
subsection {* State Spaces *}
subsection \<open>State Spaces\<close>
text {*
text \<open>
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.
*}
\<close>
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 \<open>We decorate the state components in the record with the suffix \<open>_'\<close>,
to avoid cluttering the namespace with the simple names that could no longer
be used for logical variables otherwise.
*}
\<close>
text {* We will first consider programs without procedures, later on
text \<open>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).
*}
\<close>
subsection {* Basic Examples *}
subsection \<open>Basic Examples\<close>
text {*
text \<open>
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.
*}
\<close>
text {*
text \<open>
Using the basic rule directly is a bit cumbersome.
*}
\<close>
lemma "\<Gamma>\<turnstile> {|\<acute>N = 5|} \<acute>N :== 2 * \<acute>N {|\<acute>N = 10|}"
apply (rule HoarePartial.Basic) apply simp
done
text {*
text \<open>
If we refer to components (variables) of the state-space of the program
we always mark these with @{text "\<acute>"}. It is the acute-symbol and is present on
we always mark these with \<open>\<acute>\<close>. 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 "\<lbrace> \<rbrace>"} with symbols. Internally
as {\verb+{| |}+} in ASCII or \<open>\<lbrace> \<rbrace>\<close> 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 \<open>_'\<close>.
So the assertion @{term "{|\<acute>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"}.
*}
\<open>{s. N_' s = 5}\<close> written in ordinary set comprehension notation of
Isabelle. It describes the set of states where the \<open>N_'\<close> component
is equal to \<open>5\<close>.
\<close>
text {*
text \<open>
Certainly we want the state modification already done, e.g.\ by
simplification. The @{text vcg} method performs the basic state
simplification. The \<open>vcg\<close> method performs the basic state
update for us; we may apply the Simplifier afterwards to achieve
``obvious'' consequences as well.
*}
\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>N :== 10 \<lbrace>\<acute>N = 10\<rbrace>"
@ -138,10 +138,10 @@ lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
\<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
by vcg
text {*
text \<open>
We can also perform verification conditions generation step by step by using
the @{text vcg_step} method.
*}
the \<open>vcg_step\<close> method.
\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
\<acute>I :== \<acute>M;; \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I
@ -152,12 +152,12 @@ lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
apply vcg_step
done
text {*
text \<open>
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.
*}
\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N :== \<acute>N \<lbrace>\<acute>N = a\<rbrace>"
by vcg
@ -173,11 +173,11 @@ lemma "\<Gamma>\<turnstile>{s. x_' s = a} (Basic (\<lambda>s. x_'_update (x_' s)
oops
text {*
text \<open>
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.
*}
\<open>vcg\<close> method is able to handle this case, too.
\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
@ -191,8 +191,8 @@ qed
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
-- {* inclusion of assertions expressed in ``pure'' logic, *}
-- {* without mentioning the state space *}
\<comment> \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
\<comment> \<open>without mentioning the state space\<close>
by simp
also have "\<Gamma>\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
by vcg
@ -204,14 +204,14 @@ lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :=
apply simp
done
subsection {* Multiplication by Addition *}
subsection \<open>Multiplication by Addition\<close>
text {*
text \<open>
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.
*}
\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
WHILE \<acute>M \<noteq> a
@ -235,12 +235,12 @@ proof -
qed
text {*
The subsequent version of the proof applies the @{text vcg} method
text \<open>
The subsequent version of the proof applies the \<open>vcg\<close> 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.
*}
\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
WHILE \<acute>M \<noteq> a
@ -251,7 +251,7 @@ lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
apply auto
done
text {* Here some examples of ``breaking'' out of a loop *}
text \<open>Here some examples of ``breaking'' out of a loop\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
TRY
@ -283,10 +283,10 @@ apply auto
done
text {* Some more syntactic sugar, the label statement @{text "\<dots> \<bullet> \<dots>"} as shorthand
for the @{text "TRY-CATCH"} above, and the @{text "RAISE"} for an state-update followed
by a @{text "THROW"}.
*}
text \<open>Some more syntactic sugar, the label statement \<open>\<dots> \<bullet> \<dots>\<close> as shorthand
for the \<open>TRY-CATCH\<close> above, and the \<open>RAISE\<close> for an state-update followed
by a \<open>THROW\<close>.
\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
\<lbrace>\<acute>Abr = ''Break''\<rbrace>\<bullet> WHILE True INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break''
@ -326,7 +326,7 @@ apply vcg
apply auto
done
text {* Blocks *}
text \<open>Blocks\<close>
lemma "\<Gamma>\<turnstile>\<lbrace>\<acute>I = i\<rbrace> LOC \<acute>I;; \<acute>I :== 2 COL \<lbrace>\<acute>I \<le> i\<rbrace>"
apply vcg
@ -338,13 +338,13 @@ lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = n\<rbrace> LOC \<acute>N :== 10
by vcg
subsection {* Summing Natural Numbers *}
subsection \<open>Summing Natural Numbers\<close>
text {*
text \<open>
We verify an imperative program to sum natural numbers up to a given
limit. First some functional definition for proper specification of
the problem.
*}
\<close>
primrec
sum :: "(nat => nat) => nat => nat"
@ -358,13 +358,13 @@ syntax
translations
"SUMM j<k. b" == "CONST sum (\<lambda>j. b) k"
text {*
text \<open>
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 \<open>vcg\<close> 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.
*}
\<close>
theorem "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
\<acute>S :== 0;; \<acute>I :== 1;;
@ -401,10 +401,10 @@ proof -
finally show ?thesis .
qed
text {*
The next version uses the @{text vcg} method, while still explaining
text \<open>
The next version uses the \<open>vcg\<close> method, while still explaining
the resulting proof obligations in an abstract, structured manner.
*}
\<close>
theorem "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
\<acute>S :== 0;; \<acute>I :== 1;;
@ -431,10 +431,10 @@ proof -
qed
qed
text {*
text \<open>
Certainly, this proof may be done fully automatically as well, provided
that the invariant is given beforehand.
*}
\<close>
theorem "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
\<acute>S :== 0;; \<acute>I :== 1;;
@ -449,7 +449,7 @@ theorem "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
apply auto
done
subsection {* SWITCH *}
subsection \<open>SWITCH\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> SWITCH \<acute>B
{True} \<Rightarrow> \<acute>N :== 6
@ -469,13 +469,13 @@ apply vcg
apply simp
done
subsection {* (Mutually) Recursive Procedures *}
subsection \<open>(Mutually) Recursive Procedures\<close>
subsubsection {* Factorial *}
subsubsection \<open>Factorial\<close>
text {* We want to define a procedure for the factorial. We first
text \<open>We want to define a procedure for the factorial. We first
define a HOL functions that calculates it to specify the procedure later on.
*}
\<close>
primrec fac:: "nat \<Rightarrow> nat"
where
@ -485,7 +485,7 @@ where
lemma fac_simp [simp]: "0 < i \<Longrightarrow> fac i = i * fac (i - 1)"
by (cases i) simp_all
text {* Now we define the procedure *}
text \<open>Now we define the procedure\<close>
procedures
Fac (N|R) = "IF \<acute>N = 0 THEN \<acute>R :== 1
@ -495,23 +495,23 @@ procedures
text {* A procedure is given by the signature of the procedure
text \<open>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 \<open>|\<close> 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.
*}
\<close>
text {*
Behind the scenes the @{text "procedures"} command provides us convenient syntax
text \<open>
Behind the scenes the \<open>procedures\<close> 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 \<open>Fac_impl\<close> and extends the \<open>hoare\<close> locale
with a theorem @{term "\<Gamma> ''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 "\<Gamma>"} 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.
*}
\<close>
thm Fac_body.Fac_body_def
print_locale Fac_impl
text {*
text \<open>
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 \<open>hoare_use_call_tr'\<close>
\<close>
context Fac_impl
begin
text {*
text \<open>
@{term "CALL Fac(\<acute>N,\<acute>M)"} is internally:
*}
\<close>
declare [[hoare_use_call_tr' = false]]
text {*
text \<open>
@{term "CALL Fac(\<acute>N,\<acute>M)"}
*}
\<close>
term "CALL Fac(\<acute>N,\<acute>M)"
declare [[hoare_use_call_tr' = true]]
end
text {*
text \<open>
Now let us prove that @{term "Fac"} meets its specification.
*}
\<close>
text {*
text \<open>
Procedure specifications are ordinary Hoare tuples. We use the parameterless
call for the specification; @{text "\<acute>R :== PROC Fac(\<acute>N)"} is syntactic sugar
for @{text "Call ''Fac''"}. This emphasises that the specification
call for the specification; \<open>\<acute>R :== PROC Fac(\<acute>N)\<close> is syntactic sugar
for \<open>Call ''Fac''\<close>. This emphasises that the specification
describes the internal behaviour of the procedure, whereas parameter passing
corresponds to the procedure call.
*}
\<close>
lemma (in Fac_impl)
@ -564,7 +564,7 @@ lemma (in Fac_impl)
done
text {*
text \<open>
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.
*}
\<close>
text {* We can also step through verification condition generation. When
text \<open>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 \<open>ProcSpec\<close>. To be successful there must be a specification
of the procedure in the context.
*}
\<close>
lemma (in Fac_impl)
shows "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
@ -594,7 +594,7 @@ lemma (in Fac_impl)
done
text {* Here some Isar style version of the proof *}
text \<open>Here some Isar style version of the proof\<close>
lemma (in Fac_impl)
shows "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
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 \<open>To avoid retyping of potentially large pre and postconditions in
the previous proof we can use the casual term abbreviations of the Isar
language.
*}
\<close>
lemma (in Fac_impl)
shows "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
@ -633,24 +633,24 @@ proof (hoare_rule HoarePartial.ProcRec1)
done
qed
text {* The previous proof pattern has still some kind of inconvenience.
text \<open>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.
*}
\<close>
lemma (in Fac_impl) Fac_spec:
shows "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
(is "\<forall>n. \<Gamma>\<turnstile>(?Pre n) ?Fac (?Post n)")
proof (hoare_rule HoarePartial.ProcRec1)
def "\<Theta>'"=="(\<Union>n. {(?Pre n, Fac_'proc, ?Post n,{}::('a, 'b) vars_scheme set)})"
define \<Theta>' where "\<Theta>' = (\<Union>n. {(?Pre n, Fac_'proc, ?Post n,{}::('a, 'b) vars_scheme set)})"
have Fac_spec: "\<forall>n. \<Gamma>,\<Theta>'\<turnstile>(?Pre n) ?Fac (?Post n)"
by (unfold \<Theta>'_def, rule allI, rule hoarep.Asm) auto
txt {* We have to name the fact @{text "Fac_spec"}, so that the vcg can
txt \<open>We have to name the fact \<open>Fac_spec\<close>, so that the vcg can
use the specification for the recursive call, since it cannot infer it
from the opaque @{term "\<Theta>'"}. *}
from the opaque @{term "\<Theta>'"}.\<close>
show "\<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile> (?Pre \<sigma>) IF \<acute>N = 0 THEN \<acute>R :== 1
ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI (?Post \<sigma>)"
apply vcg
@ -658,7 +658,7 @@ proof (hoare_rule HoarePartial.ProcRec1)
done
qed
text {* There are different rules available to prove procedure calls,
text \<open>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
\<open>hoare_rule\<close>, which behaves like the method \<open>rule\<close> but automatically
tries to solve the side-conditions.
*}
\<close>
subsubsection {* Odd and Even *}
subsubsection \<open>Odd and Even\<close>
text {* Odd and even are defined mutually recursive here. In the
@{text "procedures"} command we conjoin both definitions with @{text "and"}.
*}
text \<open>Odd and even are defined mutually recursive here. In the
\<open>procedures\<close> command we conjoin both definitions with \<open>and\<close>.
\<close>
procedures
odd(N | A) = "IF \<acute>N=0 THEN \<acute>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 \<open>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:
*}
\<close>
ML {* ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2) *}
ML \<open>ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2)\<close>
lemma (in odd_even_clique)
@ -729,10 +729,10 @@ proof -
by iprover+
qed
subsection {*Expressions With Side Effects *}
subsection \<open>Expressions With Side Effects\<close>
text {* \texttt{R := N++ + M++} *}
text \<open>\texttt{R := N++ + M++}\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
\<acute>N \<ggreater> n. \<acute>N :== \<acute>N + 1 \<ggreater>
\<acute>M \<ggreater> m. \<acute>M :== \<acute>M + 1 \<ggreater>
@ -742,7 +742,7 @@ apply vcg
apply simp
done
text {*\texttt{R := Fac (N) + Fac (M)} *}
text \<open>\texttt{R := Fac (N) + Fac (M)}\<close>
lemma (in Fac_impl) shows
"\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(\<acute>M) \<ggreater> m.
@ -752,7 +752,7 @@ apply vcg
done
text {*\texttt{ R := (Fac(Fac (N)))}*}
text \<open>\texttt{ R := (Fac(Fac (N)))}\<close>
lemma (in Fac_impl) shows
"\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(n) \<ggreater> m.
@ -762,15 +762,15 @@ apply vcg
done
subsection {* Global Variables and Heap *}
subsection \<open>Global Variables and Heap\<close>
text {*
text \<open>
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.
*}
\<close>
record globals_list =
next_' :: "ref \<Rightarrow> 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 \<open>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".
*}
\<close>
text {* We first define an append function on lists. It takes two
text \<open>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.
*}
\<close>
procedures
append(p,q|p) =
@ -815,7 +815,7 @@ declare [[hoare_use_call_tr' = false]]
term "CALL append(\<acute>p,\<acute>q,\<acute>p\<rightarrow>\<acute>next)"
declare [[hoare_use_call_tr' = true]]
end
text {* Below we give two specifications this time.
text \<open>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 "\<sigma>"}, 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 "\<lbrace>\<sigma>. \<dots>\<rbrace>"} is a shorthand to fix the current
state: @{text "{s. \<sigma> = s \<dots>}"}.
*}
during the proofs. The syntax \<open>\<lbrace>\<sigma>. \<dots>\<rbrace>\<close> is a shorthand to fix the current
state: \<open>{s. \<sigma> = s \<dots>}\<close>.
\<close>
lemma (in append_impl) append_spec:
shows "\<forall>\<sigma> Ps Qs. \<Gamma>\<turnstile>
@ -845,9 +845,9 @@ lemma (in append_impl) append_spec:
done
text {* The modifies clause is equal to a proper record update specification
text \<open>The modifies clause is equal to a proper record update specification
of the following form.
*}
\<close>
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 \<open>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.
*}
\<close>
text {* You can study the effect of the modifies clause on the following two
text \<open>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.
*}
\<close>
lemma (in append_impl)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>p=Null \<and> \<acute>cont=c\<rbrace> \<acute>p :== CALL append(\<acute>p,Null) \<lbrace>\<acute>cont=c\<rbrace>"
apply vcg
oops
text {* To prove the frame condition,
text \<open>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 \<open>spec=modifies\<close> It will also try to solve the
verification conditions automatically.
*}
\<close>
lemma (in append_impl) append_modifies:
shows
@ -899,27 +899,27 @@ lemma (in append_impl)
apply simp
done
text {*
text \<open>
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.
*}
\<close>
text {* To verify the body of @{term "append"} we do not need the modifies
text \<open>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.
*}
\<close>
text {*
text \<open>
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.
*}
\<close>
@ -928,7 +928,7 @@ clause to prove the functional specifications.
subsubsection {*Insertion Sort*}
subsubsection \<open>Insertion Sort\<close>
primrec sorted:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
where
@ -949,7 +949,7 @@ procedures
FI"
text {*
text \<open>
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 "\<acute>cont"}
instead of @{text "\<^bsup>\<sigma>\<^esup>cont"}, we get a new instance of @{text "cont"} during
The reason is simple. If the postcondition would talk about \<open>\<acute>cont\<close>
instead of \<open>\<^bsup>\<sigma>\<^esup>cont\<close>, we get a new instance of \<open>cont\<close> 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 \<open>insert\<close> instead still has the
old \<open>cont\<close> 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).
*}
\<close>
lemma (in insert_impl) insert_modifies:
"\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC insert(\<acute>r,\<acute>p){t. t may_only_modify_globals \<sigma> in [next]}"
@ -1015,12 +1015,12 @@ apply (vcg spec=modifies)
done
text {* Insertion sort is not implemented recursively here but with a while
text \<open>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}.
*}
\<close>
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 \<open>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.
*}
\<close>
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 \<open>Restrict locale \<open>hoare\<close> to the required type.\<close>
locale hoare_ex =
hoare \<Gamma> for \<Gamma> :: "'c \<rightharpoonup> (('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 \<open>Fault Avoiding Semantics\<close>
text {*
text \<open>
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.
*}
\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<lbrace>\<acute>p\<noteq>Null\<rbrace>\<longmapsto> \<acute>p\<rightarrow>\<acute>next :== \<acute>p \<lbrace>True\<rbrace>"
@ -1149,9 +1149,9 @@ lemma "\<Gamma>\<turnstile> {} \<lbrace>\<acute>p\<noteq>Null\<rbrace>\<longmap
apply vcg
done
text {* Let us consider this small program that reverts a list. At
text \<open>Let us consider this small program that reverts a list. At
first without guards.
*}
\<close>
lemma (in hoare_ex) rev_strip:
"\<Gamma>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
@ -1168,9 +1168,9 @@ apply (vcg)
apply fastforce+
done
text {* If we want to ensure that we do not dereference @{term "Null"} or
text \<open>If we want to ensure that we do not dereference @{term "Null"} or
access unallocated memory, we have to add some guards.
*}
\<close>
locale hoare_ex_guard =
hoare \<Gamma> for \<Gamma> :: "'c \<rightharpoonup> (('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 \<open>We can also just prove that no faults will occur, by giving the
trivial postcondition.
*}
\<close>
lemma (in hoare_ex_guard) rev_noFault:
"\<Gamma>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
@ -1251,10 +1251,10 @@ proof -
qed
text {* We can then combine the prove that no fault will occur with the
text \<open>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}
*}
\<close>
lemma
@ -1277,15 +1277,15 @@ apply simp
done
text {* In the previous example the effort to split up the prove did not
text \<open>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.
*}
\<close>
text {*
text \<open>
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 \<lbrace>\<acute>p\<noteq>Null\<rbrace>\<longmapsto> \<acute>p\<rightarrow>\<acute>next\<noteq>Null DO SKIP OD"}
*}
\<close>
subsection {* Circular Lists *}
subsection \<open>Circular Lists\<close>
definition
distPath :: "ref \<Rightarrow> (ref \<Rightarrow> ref) \<Rightarrow> ref \<Rightarrow> ref list \<Rightarrow> bool" where
"distPath x next y as = (Path x next y as \<and> distinct as)"
@ -1333,10 +1333,10 @@ apply (induct Ps)
apply (auto simp add:fun_upd_apply)
done
text {*
text \<open>
The simple algorithm for acyclic list reversal, with modified
annotations, works for cyclic lists as well.:
*}
\<close>
lemma circular_list_rev_II:
"\<Gamma>\<turnstile>
@ -1367,17 +1367,17 @@ apply force
apply fastforce
done
text{* Although the above algorithm is more succinct, its invariant
text\<open>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.
*}
\<close>
text {*
text \<open>
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
*}
\<close>
(*
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 \<open>Instead of annotations one can also directly use previously proven lemmas.\<close>
lemma foo_lemma: "\<forall>n m. \<Gamma>\<turnstile> \<lbrace>\<acute>N = n \<and> \<acute>M = m\<rbrace> \<acute>N :== \<acute>N + 1;; \<acute>M :== \<acute>M + 1
\<lbrace>\<acute>N = n + 1 \<and> \<acute>M = m + 1\<rbrace>"
by vcg
@ -1458,7 +1458,7 @@ lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = n \<and> \<acute>M = m\<rbrace>
apply simp
done
text {* Just some test on marked, guards *}
text \<open>Just some test on marked, guards\<close>
lemma "\<Gamma>\<turnstile>\<lbrace>True\<rbrace> WHILE \<lbrace>P \<acute>N \<rbrace>\<surd>, \<lbrace>Q \<acute>M\<rbrace>#, \<lbrace>R \<acute>N\<rbrace>\<longmapsto> \<acute>N < \<acute>M
INV \<lbrace>\<acute>N < 2\<rbrace> DO
\<acute>N :== \<acute>M
@ -1508,4 +1508,4 @@ lemma "\<Gamma>\<turnstile>\<^bsub>/{True}\<^esub> \<lbrace>True\<rbrace> WHILE
apply vcg
oops
end
end

290
tools/c-parser/Simpl/ex/VcgExSP.thy
View File

@ -26,18 +26,18 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Examples using Statespaces *}
section \<open>Examples using Statespaces\<close>
theory VcgExSP imports "../HeapList" "../Vcg" begin
subsection {* State Spaces *}
subsection \<open>State Spaces\<close>
text {*
text \<open>
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.
*}
\<close>
hoarestate state_space =
@ -53,29 +53,29 @@ hoarestate state_space =
lemma (in state_space)"\<Gamma>\<turnstile> \<lbrace>\<acute>N = n\<rbrace> LOC \<acute>N :== 10;; \<acute>N :== \<acute>N + 2 COL \<lbrace>\<acute>N = n\<rbrace>"
by vcg
text {* Internally we decorate the state components in the statespace with the
suffix @{text "_'"},
text \<open>Internally we decorate the state components in the statespace with the
suffix \<open>_'\<close>,
to avoid cluttering the namespace with the simple names that could no longer
be used for logical variables otherwise.
*}
\<close>
text {* We will first consider programs without procedures, later on
text \<open>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).
*}
\<close>
subsection {* Basic Examples *}
subsection \<open>Basic Examples\<close>
text {*
text \<open>
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.
*}
\<close>
text {*
text \<open>
Using the basic rule directly is a bit cumbersome.
*}
\<close>
lemma (in state_space) "\<Gamma>\<turnstile> {|\<acute>N = 5|} \<acute>N :== 2 * \<acute>N {|\<acute>N = 10|}"
apply (rule HoarePartial.Basic)
@ -118,10 +118,10 @@ lemma (in state_space)
apply simp
done
text {*
text \<open>
We can also perform verification conditions generation step by step by using
the @{text vcg_step} method.
*}
the \<open>vcg_step\<close> method.
\<close>
lemma (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
@ -135,11 +135,11 @@ lemma (in state_space)
done
text {*
text \<open>
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.
*}
\<open>vcg\<close> method is able to handle this case, too.
\<close>
lemma (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
@ -155,8 +155,8 @@ lemma (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
-- {* inclusion of assertions expressed in ``pure'' logic, *}
-- {* without mentioning the state space *}
\<comment> \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
\<comment> \<open>without mentioning the state space\<close>
by simp
also have "\<Gamma>\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
by vcg
@ -169,14 +169,14 @@ lemma (in state_space)
apply simp
done
subsection {* Multiplication by Addition *}
subsection \<open>Multiplication by Addition\<close>
text {*
text \<open>
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.
*}
\<close>
lemma (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@ -201,12 +201,12 @@ proof -
qed
text {*
The subsequent version of the proof applies the @{text vcg} method
text \<open>
The subsequent version of the proof applies the \<open>vcg\<close> 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.
*}
\<close>
lemma (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@ -218,7 +218,7 @@ lemma (in state_space)
apply auto
done
text {* Here some examples of ``breaking'' out of a loop *}
text \<open>Here some examples of ``breaking'' out of a loop\<close>
lemma (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@ -257,10 +257,10 @@ done
text {* Some more syntactic sugar, the label statement @{text "\<dots> \<bullet> \<dots>"} as shorthand
for the @{text "TRY-CATCH"} above, and the @{text "RAISE"} for an state-update followed
by a @{text "THROW"}.
*}
text \<open>Some more syntactic sugar, the label statement \<open>\<dots> \<bullet> \<dots>\<close> as shorthand
for the \<open>TRY-CATCH\<close> above, and the \<open>RAISE\<close> for an state-update followed
by a \<open>THROW\<close>.
\<close>
lemma (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
\<lbrace>\<acute>Abr = ''Break''\<rbrace>\<bullet> WHILE True INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
@ -303,7 +303,7 @@ apply vcg
apply auto
done
text {* Blocks *}
text \<open>Blocks\<close>
lemma (in state_space)
shows "\<Gamma>\<turnstile>\<lbrace>\<acute>I = i\<rbrace> LOC \<acute>I;; \<acute>I :== 2 COL \<lbrace>\<acute>I \<le> i\<rbrace>"
@ -311,13 +311,13 @@ lemma (in state_space)
by simp
subsection {* Summing Natural Numbers *}
subsection \<open>Summing Natural Numbers\<close>
text {*
text \<open>
We verify an imperative program to sum natural numbers up to a given
limit. First some functional definition for proper specification of
the problem.
*}
\<close>
primrec
sum :: "(nat => nat) => nat => nat"
@ -331,13 +331,13 @@ syntax
translations
"SUMM j<k. b" == "CONST sum (\<lambda>j. b) k"
text {*
text \<open>
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 \<open>vcg\<close> 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.
*}
\<close>
theorem (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
@ -375,10 +375,10 @@ proof -
finally show ?thesis .
qed
text {*
The next version uses the @{text vcg} method, while still explaining
text \<open>
The next version uses the \<open>vcg\<close> method, while still explaining
the resulting proof obligations in an abstract, structured manner.
*}
\<close>
theorem (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
@ -406,10 +406,10 @@ proof -
qed
qed
text {*
text \<open>
Certainly, this proof may be done fully automatically as well, provided
that the invariant is given beforehand.
*}
\<close>
theorem (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
@ -425,7 +425,7 @@ theorem (in state_space)
apply auto
done
subsection {* SWITCH *}
subsection \<open>SWITCH\<close>
lemma (in state_space)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> SWITCH \<acute>B
@ -447,13 +447,13 @@ apply vcg
apply simp
done
subsection {* (Mutually) Recursive Procedures *}
subsection \<open>(Mutually) Recursive Procedures\<close>
subsubsection {* Factorial *}
subsubsection \<open>Factorial\<close>
text {* We want to define a procedure for the factorial. We first
text \<open>We want to define a procedure for the factorial. We first
define a HOL functions that calculates it to specify the procedure later on.
*}
\<close>
primrec fac:: "nat \<Rightarrow> nat"
where
@ -463,7 +463,7 @@ where
lemma fac_simp [simp]: "0 < i \<Longrightarrow> fac i = i * fac (i - 1)"
by (cases i) simp_all
text {* Now we define the procedure *}
text \<open>Now we define the procedure\<close>
procedures
@ -475,27 +475,27 @@ procedures
print_locale Fac_impl
text {*
text \<open>
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 \<open>hoare_use_call_tr'\<close>
\<close>
context Fac_impl
begin
text {*
text \<open>
@{term "CALL Fac(\<acute>N,\<acute>R)"} is internally:
*}
\<close>
declare [[hoare_use_call_tr' = false]]
text {*
text \<open>
@{term "CALL Fac(\<acute>N,\<acute>R)"}
*}
\<close>
term "CALL Fac(\<acute>N,\<acute>R)"
declare [[hoare_use_call_tr' = true]]
text {*
text \<open>
Now let us prove that @{term "Fac"} meets its specification.
*}
\<close>
end
@ -508,7 +508,7 @@ lemma (in Fac_impl) Fac_spec':
done
text {*
text \<open>
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.
*}
\<close>
text {* We can also step through verification condition generation. When
text \<open>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 \<open>ProcSpec\<close>. To be successful there must be a specification
of the procedure in the context.
*}
\<close>
lemma (in Fac_impl) Fac_spec1:
shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>{\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
@ -538,7 +538,7 @@ lemma (in Fac_impl) Fac_spec1:
done
text {* Here some Isar style version of the proof *}
text \<open>Here some Isar style version of the proof\<close>
lemma (in Fac_impl) Fac_spec2:
shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>{\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
@ -556,10 +556,10 @@ proof (hoare_rule HoarePartial.ProcRec1)
done
qed
text {* To avoid retyping of potentially large pre and postconditions in
text \<open>To avoid retyping of potentially large pre and postconditions in
the previous proof we can use the casual term abbreviations of the Isar
language.
*}
\<close>
lemma (in Fac_impl) Fac_spec3:
shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>{\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
@ -578,24 +578,24 @@ proof (hoare_rule HoarePartial.ProcRec1)
done
qed
text {* The previous proof pattern has still some kind of inconvenience.
text \<open>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.
*}
\<close>
lemma (in Fac_impl) Fac_spec4:
shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>{\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
(is "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>(?Pre \<sigma>) ?Fac (?Post \<sigma>)")
proof (hoare_rule HoarePartial.ProcRec1)
def "\<Theta>'"=="(\<Theta>\<union>(\<Union>\<sigma>. {(?Pre \<sigma>, Fac_'proc, ?Post \<sigma>,{})}))"
define \<Theta>' where "\<Theta>' = \<Theta> \<union> (\<Union>\<sigma>. {(?Pre \<sigma>, Fac_'proc, ?Post \<sigma>,{})})"
have Fac_spec: "\<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile>(?Pre \<sigma>) ?Fac (?Post \<sigma>)"
by (unfold \<Theta>'_def, rule allI, rule hoarep.Asm) simp
txt {* We have to name the fact @{text "Fac_spec"}, so that the vcg can
txt \<open>We have to name the fact \<open>Fac_spec\<close>, so that the vcg can
use the specification for the recursive call, since it cannot infer it
from the opaque @{term "\<Theta>'"}. *}
from the opaque @{term "\<Theta>'"}.\<close>
show "\<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile> (?Pre \<sigma>) IF \<acute>N = 0 THEN \<acute>R :== 1
ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI (?Post \<sigma>)"
apply vcg
@ -603,7 +603,7 @@ proof (hoare_rule HoarePartial.ProcRec1)
done
qed
text {* There are different rules available to prove procedure calls,
text \<open>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
\<open>hoare_rule\<close>, which behaves like the method \<open>rule\<close> but automatically
tries to solve the side-conditions.
*}
\<close>
subsubsection {* Odd and Even *}
subsubsection \<open>Odd and Even\<close>
text {* Odd and even are defined mutually recursive here. In the
@{text "procedures"} command we conjoin both definitions with @{text "and"}.
*}
text \<open>Odd and even are defined mutually recursive here. In the
\<open>procedures\<close> command we conjoin both definitions with \<open>and\<close>.
\<close>
procedures
odd(N::nat | A::nat) "IF \<acute>N=0 THEN \<acute>A:==0
@ -640,16 +640,16 @@ print_theorems
print_locale! odd_even_clique
text {* To prove the procedure calls to @{term "odd"} respectively
text \<open>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:
*}
\<close>
ML {* ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2) *}
ML \<open>ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2)\<close>
lemma (in odd_even_clique)
@ -672,7 +672,7 @@ proof -
by iprover+
qed
subsection {*Expressions With Side Effects *}
subsection \<open>Expressions With Side Effects\<close>
(* R := N++ + M++*)
@ -712,15 +712,15 @@ proof -
qed
subsection {* Global Variables and Heap *}
subsection \<open>Global Variables and Heap\<close>
text {*
text \<open>
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.
*}
\<close>
hoarestate globals_list =
@ -730,16 +730,16 @@ hoarestate globals_list =
text {* Updates to global components inside a procedure will
text \<open>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".
*}
\<close>
text {* We will first define an append function on lists. It takes two
text \<open>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.
*}
\<close>
procedures (imports globals_list)
append(p::ref,q::ref|p::ref)
@ -754,7 +754,7 @@ term "CALL append(\<acute>p,\<acute>q,\<acute>p\<rightarrow>\<acute>next)"
end
declare [[hoare_use_call_tr' = true]]
text {* Below we give two specifications this time..
text \<open>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 "\<sigma>"}, 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 "\<lbrace>\<sigma>. \<dots>\<rbrace>"} is a shorthand to fix the current
state: @{text "{s. \<sigma> = s \<dots>}"}.
*}
during the proofs. The syntax \<open>\<lbrace>\<sigma>. \<dots>\<rbrace>\<close> is a shorthand to fix the current
state: \<open>{s. \<sigma> = s \<dots>}\<close>.
\<close>
lemma (in append_impl) append_spec:
shows "\<forall>\<sigma> Ps Qs. \<Gamma>\<turnstile>
@ -784,9 +784,9 @@ lemma (in append_impl) append_spec:
done
text {* The modifies clause is equal to a proper record update specification
text \<open>The modifies clause is equal to a proper record update specification
of the following form.
*}
\<close>
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 \<open>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.
*}
\<close>
text {* You can study the effect of the modifies clause on the following two
text \<open>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.
*}
\<close>
lemma (in append_impl)
shows "\<Gamma>\<turnstile> \<lbrace>\<acute>p=Null \<and> \<acute>cont=c\<rbrace> \<acute>p :== CALL append(\<acute>p,Null) \<lbrace>\<acute>cont=c\<rbrace>"
apply vcg
oops
text {* To prove the frame condition,
text \<open>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 \<open>spec=modifies\<close> It will also try to solve the
verification conditions automatically.
*}
\<close>
lemma (in append_impl) append_modifies:
shows
@ -835,32 +835,32 @@ lemma (in append_impl)
apply simp
done
text {*
text \<open>
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.
*}
\<close>
text {* To verify the body of @{term "append"} we do not need the modifies
text \<open>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.
*}
\<close>
text {*
text \<open>
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.
*}
\<close>
subsubsection {*Insertion Sort*}
subsubsection \<open>Insertion Sort\<close>
primrec sorted:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
where
@ -881,7 +881,7 @@ procedures (imports globals_list)
FI"
text {*
text \<open>
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 "\<acute>cont"}
instead of @{text "\<^bsup>\<sigma>\<^esup>cont"}, we will get a new instance of @{text "cont"} during
The reason is simple. If the postcondition would talk about \<open>\<acute>cont\<close>
instead of \<open>\<^bsup>\<sigma>\<^esup>cont\<close>, we will get a new instance of \<open>cont\<close> 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 \<open>insert\<close> instead will still have the
old \<open>cont\<close> 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).
*}
\<close>
lemma (in insert_impl) insert_modifies:
"\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC insert(\<acute>r,\<acute>p){t. t may_only_modify_globals \<sigma> in [next]}"
@ -949,12 +949,12 @@ apply (vcg spec=modifies)
done
text {* Insertion sort is not implemented recursively here but with a while
text \<open>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}.
*}
\<close>
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 \<open>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.
*}
\<close>
(*
record globals_list_alloc = globals_list +
@ -1077,14 +1077,14 @@ apply (simp add: sz_def)
apply fastforce
done
subsection {* Fault Avoiding Semantics *}
subsection \<open>Fault Avoiding Semantics\<close>
text {*
text \<open>
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.
*}
\<close>
lemma (in list_alloc) "\<Gamma>,\<Theta>\<turnstile> \<lbrace>True\<rbrace> \<lbrace>\<acute>p\<noteq>Null\<rbrace>\<longmapsto> \<acute>p\<rightarrow>\<acute>next :== \<acute>p \<lbrace>True\<rbrace>"
@ -1095,9 +1095,9 @@ lemma (in list_alloc) "\<Gamma>,\<Theta>\<turnstile> {} \<lbrace>\<acute>p\<not
apply vcg
done
text {* Let us consider this small program that reverts a list. At
text \<open>Let us consider this small program that reverts a list. At
first without guards.
*}
\<close>
lemma (in list_alloc)
shows
"\<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
@ -1115,9 +1115,9 @@ apply (vcg)
apply fastforce+
done
text {* If we want to ensure that we do not dereference @{term "Null"} or
text \<open>If we want to ensure that we do not dereference @{term "Null"} or
access unallocated memory, we have to add some guards.
*}
\<close>
lemma (in list_alloc)
shows
"\<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
@ -1136,9 +1136,9 @@ apply fastforce+
done
text {* We can also just prove that no faults will occur, by giving the
text \<open>We can also just prove that no faults will occur, by giving the
trivial postcondition.
*}
\<close>
lemma (in list_alloc) rev_noFault:
shows
"\<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
@ -1197,10 +1197,10 @@ proof -
qed
text {* We can then combine the prove that no fault will occur with the
text \<open>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}
*}
\<close>
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 \<open>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.
*}
\<close>
context list_alloc
begin
text {*
text \<open>
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 \<lbrace>\<acute>p\<noteq>Null\<rbrace>\<longmapsto> \<acute>p\<rightarrow>\<acute>next\<noteq>Null DO SKIP OD"}
*}
\<close>
end
subsection {* Cicular Lists *}
subsection \<open>Cicular Lists\<close>
definition
distPath :: "ref \<Rightarrow> (ref \<Rightarrow> ref) \<Rightarrow> ref \<Rightarrow> ref list \<Rightarrow> bool" where
"distPath x next y as = (Path x next y as \<and> distinct as)"
@ -1282,10 +1282,10 @@ apply (induct Ps)
apply (auto simp add:fun_upd_apply)
done
text {*
text \<open>
The simple algorithm for acyclic list reversal, with modified
annotations, works for cyclic lists as well.:
*}
\<close>
lemma (in list_alloc) circular_list_rev_II:
"\<Gamma>,\<Theta>\<turnstile>
@ -1316,17 +1316,17 @@ apply force
apply fastforce
done
text{* Although the above algorithm is more succinct, its invariant
text\<open>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.
*}
\<close>
text {*
text \<open>
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
*}
\<close>
(*
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 \<open>Just some test on marked, guards\<close>
lemma (in state_space) "\<Gamma>\<turnstile>\<lbrace>True\<rbrace> WHILE \<lbrace>P \<acute>N \<rbrace>\<surd>, \<lbrace>Q \<acute>M\<rbrace>#, \<lbrace>R \<acute>N\<rbrace>\<longmapsto> \<acute>N < \<acute>M
INV \<lbrace>\<acute>N < 2\<rbrace> DO
\<acute>N :== \<acute>M
@ -1385,4 +1385,4 @@ lemma (in state_space) "\<Gamma>\<turnstile>\<^bsub>/{True}\<^esub> \<lbrace>Tru
apply vcg
oops
end
end

14
tools/c-parser/Simpl/ex/VcgExTotal.thy
View File

@ -26,7 +26,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section {* Examples for Total Correctness *}
section \<open>Examples for Total Correctness\<close>
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 \<open>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
*}
\<open>FIX\<close> to introduce a new logical variable
\<close>
lemma "\<Gamma>\<turnstile>\<^sub>t \<lbrace>\<acute>M=0 \<and> \<acute>N=0\<rbrace>
WHILE (\<acute>M < i)
@ -214,7 +214,7 @@ procedures Rev(p|p) =
Rev_modifies:
"\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} \<acute>p :== PROC Rev(\<acute>p) {t. t may_only_modify_globals \<sigma> in [next]}"
text {* We only need partial correctness of modifies clause!*}
text \<open>We only need partial correctness of modifies clause!\<close>
@ -307,7 +307,7 @@ and
IF 0 < \<acute>M THEN CALL coast(\<acute>N,\<acute>M- 1) FI"
ML {* ML_Thms.bind_thm ("HoareTotal_ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Total 2)*}
ML \<open>ML_Thms.bind_thm ("HoareTotal_ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Total 2)\<close>
lemma (in pedal_coast_clique)
@ -383,4 +383,4 @@ lemma (in pedal_coast_clique)
done
end
end

46
tools/c-parser/Simpl/hoare.ML
View File

@ -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

26
tools/c-parser/Simpl/hoare_syntax.ML
View File

@ -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)) =