--- a/src/HOL/IMP/Sec_Typing.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Sec_Typing.thy Fri May 17 08:19:52 2013 +0200
@@ -11,7 +11,7 @@
Assign:
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
Seq:
- "\<lbrakk> l \<turnstile> c\<^isub>1; l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
+ "\<lbrakk> l \<turnstile> c\<^isub>1; l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;;c\<^isub>2" |
If:
"\<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" |
While:
@@ -24,7 +24,7 @@
value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
inductive_cases [elim!]:
- "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"
+ "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"
text{* An important property: anti-monotonicity. *}
@@ -187,7 +187,7 @@
Assign':
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
Seq':
- "\<lbrakk> l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
+ "\<lbrakk> l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;;c\<^isub>2" |
If':
"\<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" |
While':
@@ -221,7 +221,7 @@
Assign2:
"sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
Seq2:
- "\<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 " |
+ "\<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 " |
If2:
"\<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>
\<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |