7 |
7 |
8 theory AxSound imports AxSem begin |
8 theory AxSound imports AxSem begin |
9 |
9 |
10 section "validity" |
10 section "validity" |
11 |
11 |
12 consts |
12 definition |
13 |
13 triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57) |
14 triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" |
14 where |
15 ( "_\<Turnstile>_\<Colon>_"[61,0, 58] 57) |
15 "G\<Turnstile>n\<Colon>t = |
16 ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" |
16 (case t of {P} t\<succ> {Q} \<Rightarrow> |
17 ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57) |
17 \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) |
18 |
18 \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> |
19 defs triple_valid2_def: "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow> |
19 \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow> |
20 \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) |
20 (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L)))))" |
21 \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> |
|
22 \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow> |
|
23 (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L))))" |
|
24 |
21 |
25 text {* This definition differs from the ordinary @{text triple_valid_def} |
22 text {* This definition differs from the ordinary @{text triple_valid_def} |
26 manly in the conclusion: We also ensures conformance of the result state. So |
23 manly in the conclusion: We also ensures conformance of the result state. So |
27 we don't have to apply the type soundness lemma all the time during |
24 we don't have to apply the type soundness lemma all the time during |
28 induction. This definition is only introduced for the soundness |
25 induction. This definition is only introduced for the soundness |
29 proof of the axiomatic semantics, in the end we will conclude to |
26 proof of the axiomatic semantics, in the end we will conclude to |
30 the ordinary definition. |
27 the ordinary definition. |
31 *} |
28 *} |
32 |
29 |
33 defs ax_valids2_def: "G,A|\<Turnstile>\<Colon>ts \<equiv> \<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t)" |
30 definition |
|
31 ax_valids2 :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57) |
|
32 where "G,A|\<Turnstile>\<Colon>ts = (\<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t))" |
34 |
33 |
35 lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} = |
34 lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} = |
36 (\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow> |
35 (\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow> |
37 (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> |
36 (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> |
38 \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow> |
37 \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow> |