equal
deleted
inserted
replaced
1 (* Title: HOL/Bali/AxSound.thy |
1 (* Title: HOL/Bali/AxSound.thy |
2 Author: David von Oheimb and Norbert Schirmer |
2 Author: David von Oheimb and Norbert Schirmer |
3 *) |
3 *) |
4 header {* Soundness proof for Axiomatic semantics of Java expressions and |
4 subsection {* Soundness proof for Axiomatic semantics of Java expressions and |
5 statements |
5 statements |
6 *} |
6 *} |
7 |
7 |
8 theory AxSound imports AxSem begin |
8 theory AxSound imports AxSem begin |
9 |
9 |
10 section "validity" |
10 subsubsection "validity" |
11 |
11 |
12 definition |
12 definition |
13 triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57) |
13 triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57) |
14 where |
14 where |
15 "G\<Turnstile>n\<Colon>t = |
15 "G\<Turnstile>n\<Colon>t = |
98 |
98 |
99 lemma "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)" |
99 lemma "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)" |
100 oops |
100 oops |
101 |
101 |
102 |
102 |
103 section "soundness" |
103 subsubsection "soundness" |
104 |
104 |
105 lemma Methd_sound: |
105 lemma Methd_sound: |
106 assumes recursive: "G,A\<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}" |
106 assumes recursive: "G,A\<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}" |
107 shows "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}" |
107 shows "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}" |
108 proof - |
108 proof - |