equal
deleted
inserted
replaced
9 Skip: |
9 Skip: |
10 "l \<turnstile> SKIP" | |
10 "l \<turnstile> SKIP" | |
11 Assign: |
11 Assign: |
12 "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" | |
12 "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" | |
13 Seq: |
13 Seq: |
14 "\<lbrakk> l \<turnstile> c\<^isub>1; l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" | |
14 "\<lbrakk> l \<turnstile> c\<^isub>1; l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;;c\<^isub>2" | |
15 If: |
15 If: |
16 "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1; max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" | |
16 "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1; max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" | |
17 While: |
17 While: |
18 "max (sec b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c" |
18 "max (sec b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c" |
19 |
19 |
22 value "0 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP" |
22 value "0 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP" |
23 value "1 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x'' ::= N 0 ELSE SKIP" |
23 value "1 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x'' ::= N 0 ELSE SKIP" |
24 value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP" |
24 value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP" |
25 |
25 |
26 inductive_cases [elim!]: |
26 inductive_cases [elim!]: |
27 "l \<turnstile> x ::= a" "l \<turnstile> c\<^isub>1;c\<^isub>2" "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" "l \<turnstile> WHILE b DO c" |
27 "l \<turnstile> x ::= a" "l \<turnstile> c\<^isub>1;;c\<^isub>2" "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" "l \<turnstile> WHILE b DO c" |
28 |
28 |
29 |
29 |
30 text{* An important property: anti-monotonicity. *} |
30 text{* An important property: anti-monotonicity. *} |
31 |
31 |
32 lemma anti_mono: "\<lbrakk> l \<turnstile> c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c" |
32 lemma anti_mono: "\<lbrakk> l \<turnstile> c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c" |
185 Skip': |
185 Skip': |
186 "l \<turnstile>' SKIP" | |
186 "l \<turnstile>' SKIP" | |
187 Assign': |
187 Assign': |
188 "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" | |
188 "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" | |
189 Seq': |
189 Seq': |
190 "\<lbrakk> l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" | |
190 "\<lbrakk> l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;;c\<^isub>2" | |
191 If': |
191 If': |
192 "\<lbrakk> sec b \<le> l; l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" | |
192 "\<lbrakk> sec b \<le> l; l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" | |
193 While': |
193 While': |
194 "\<lbrakk> sec b \<le> l; l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" | |
194 "\<lbrakk> sec b \<le> l; l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" | |
195 anti_mono': |
195 anti_mono': |
219 Skip2: |
219 Skip2: |
220 "\<turnstile> SKIP : l" | |
220 "\<turnstile> SKIP : l" | |
221 Assign2: |
221 Assign2: |
222 "sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" | |
222 "sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" | |
223 Seq2: |
223 Seq2: |
224 "\<lbrakk> \<turnstile> c\<^isub>1 : l\<^isub>1; \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^isub>1;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " | |
224 "\<lbrakk> \<turnstile> c\<^isub>1 : l\<^isub>1; \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^isub>1;;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " | |
225 If2: |
225 If2: |
226 "\<lbrakk> sec b \<le> min l\<^isub>1 l\<^isub>2; \<turnstile> c\<^isub>1 : l\<^isub>1; \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> |
226 "\<lbrakk> sec b \<le> min l\<^isub>1 l\<^isub>2; \<turnstile> c\<^isub>1 : l\<^isub>1; \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> |
227 \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" | |
227 \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" | |
228 While2: |
228 While2: |
229 "\<lbrakk> sec b \<le> l; \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l" |
229 "\<lbrakk> sec b \<le> l; \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l" |