# HG changeset patch
# User krauss
# Date 1371483054 -7200
# Node ID 23acfc1f3fc4bad9fad6614a86542627a9f03442
# Parent  80c00a851de590d6314b47d803127bfa385d23ae# Parent  741d10d7f2c15e4a3fb0e8ce9db5137f0a860c03
merged

diff -r 80c00a851de5 -r 23acfc1f3fc4 src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Sun Jun 16 22:56:44 2013 +0200
+++ b/src/HOL/IMP/Sec_Typing.thy	Mon Jun 17 17:30:54 2013 +0200
@@ -88,7 +88,7 @@
   case Seq thus ?case by blast
 next
   case (IfTrue b s c1 s' c2)
-  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems(2) by auto
+  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
   show ?case
   proof cases
     assume "sec b \<le> l"
@@ -100,16 +100,16 @@
     assume "\<not> sec b \<le> l"
     have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
       by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
-    from confinement[OF IfTrue.hyps(2) `sec b \<turnstile> c1`] `\<not> sec b \<le> l`
+    from confinement[OF `(c1, s) \<Rightarrow> s'` `sec b \<turnstile> c1`] `\<not> sec b \<le> l`
     have "s = s' (\<le> l)" by auto
     moreover
-    from confinement[OF IfTrue.prems(1) 1] `\<not> sec b \<le> l`
+    from confinement[OF `(IF b THEN c1 ELSE c2, t) \<Rightarrow> t'` 1] `\<not> sec b \<le> l`
     have "t = t' (\<le> l)" by auto
     ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
   qed
 next
   case (IfFalse b s c2 s' c1)
-  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems(2) by auto
+  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
   show ?case
   proof cases
     assume "sec b \<le> l"
@@ -124,7 +124,7 @@
     from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l`
     have "s = s' (\<le> l)" by auto
     moreover
-    from confinement[OF IfFalse.prems(1) 1] `\<not> sec b \<le> l`
+    from confinement[OF `(IF b THEN c1 ELSE c2, t) \<Rightarrow> t'` 1] `\<not> sec b \<le> l`
     have "t = t' (\<le> l)" by auto
     ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
   qed
@@ -141,14 +141,14 @@
     assume "\<not> sec b \<le> l"
     have 1: "sec b \<turnstile> WHILE b DO c"
       by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
-    from confinement[OF WhileFalse.prems(1) 1] `\<not> sec b \<le> l`
+    from confinement[OF `(WHILE b DO c, t) \<Rightarrow> t'` 1] `\<not> sec b \<le> l`
     have "t = t' (\<le> l)" by auto
     thus "s = t' (\<le> l)" using `s = t (\<le> l)` by auto
   qed
 next
   case (WhileTrue b s1 c s2 s3 t1 t3)
   let ?w = "WHILE b DO c"
-  have "sec b \<turnstile> c" using WhileTrue.prems(2) by auto
+  have "sec b \<turnstile> c" using `0 \<turnstile> WHILE b DO c` by auto
   show ?case
   proof cases
     assume "sec b \<le> l"
@@ -167,7 +167,7 @@
     from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec b \<le> l`
     have "s1 = s3 (\<le> l)" by auto
     moreover
-    from confinement[OF WhileTrue.prems(1) 1] `\<not> sec b \<le> l`
+    from confinement[OF `(WHILE b DO c, t1) \<Rightarrow> t3` 1] `\<not> sec b \<le> l`
     have "t1 = t3 (\<le> l)" by auto
     ultimately show "s3 = t3 (\<le> l)" using `s1 = t1 (\<le> l)` by auto
   qed
diff -r 80c00a851de5 -r 23acfc1f3fc4 src/HOL/IMP/Sec_TypingT.thy
--- a/src/HOL/IMP/Sec_TypingT.thy	Sun Jun 16 22:56:44 2013 +0200
+++ b/src/HOL/IMP/Sec_TypingT.thy	Mon Jun 17 17:30:54 2013 +0200
@@ -89,9 +89,9 @@
   case Seq thus ?case by blast
 next
   case (IfTrue b s c1 s' c2)
-  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems by auto
+  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
   obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
-    using IfTrue(3)[OF anti_mono[OF `sec b \<turnstile> c1`] IfTrue.prems(2)] by blast
+    using IfTrue.IH[OF anti_mono[OF `sec b \<turnstile> c1`] `s = t (\<le> l)`] by blast
   show ?case
   proof cases
     assume "sec b \<le> l"
@@ -116,9 +116,9 @@
   qed
 next
   case (IfFalse b s c2 s' c1)
-  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems by auto
+  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
   obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
-    using IfFalse(3)[OF anti_mono[OF `sec b \<turnstile> c2`] IfFalse.prems(2)] by blast
+    using IfFalse.IH[OF anti_mono[OF `sec b \<turnstile> c2`] `s = t (\<le> l)`] by blast
   show ?case
   proof cases
     assume "sec b \<le> l"
@@ -151,8 +151,8 @@
   case (WhileTrue b s c s'' s')
   let ?w = "WHILE b DO c"
   from `0 \<turnstile> ?w` have [simp]: "sec b = 0" by auto
-  have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
-  from WhileTrue.IH(1)[OF this WhileTrue.prems(2)]
+  have "0 \<turnstile> c" using `0 \<turnstile> WHILE b DO c` by auto
+  from WhileTrue.IH(1)[OF this `s = t (\<le> l)`]
   obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
   from WhileTrue.IH(2)[OF `0 \<turnstile> ?w` this(2)]
   obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast