equal
deleted
inserted
replaced
87 ultimately show ?case by blast |
87 ultimately show ?case by blast |
88 next |
88 next |
89 case Seq thus ?case by blast |
89 case Seq thus ?case by blast |
90 next |
90 next |
91 case (IfTrue b s c1 s' c2) |
91 case (IfTrue b s c1 s' c2) |
92 have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems by auto |
92 have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto |
93 obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
93 obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
94 using IfTrue(3)[OF anti_mono[OF `sec b \<turnstile> c1`] IfTrue.prems(2)] by blast |
94 using IfTrue.IH[OF anti_mono[OF `sec b \<turnstile> c1`] `s = t (\<le> l)`] by blast |
95 show ?case |
95 show ?case |
96 proof cases |
96 proof cases |
97 assume "sec b \<le> l" |
97 assume "sec b \<le> l" |
98 hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto |
98 hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto |
99 hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le) |
99 hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le) |
114 ultimately |
114 ultimately |
115 show ?case using `s = t (\<le> l)` by auto |
115 show ?case using `s = t (\<le> l)` by auto |
116 qed |
116 qed |
117 next |
117 next |
118 case (IfFalse b s c2 s' c1) |
118 case (IfFalse b s c2 s' c1) |
119 have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems by auto |
119 have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto |
120 obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
120 obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
121 using IfFalse(3)[OF anti_mono[OF `sec b \<turnstile> c2`] IfFalse.prems(2)] by blast |
121 using IfFalse.IH[OF anti_mono[OF `sec b \<turnstile> c2`] `s = t (\<le> l)`] by blast |
122 show ?case |
122 show ?case |
123 proof cases |
123 proof cases |
124 assume "sec b \<le> l" |
124 assume "sec b \<le> l" |
125 hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto |
125 hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto |
126 hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le) |
126 hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le) |
149 with WhileFalse.prems(2) show ?case by auto |
149 with WhileFalse.prems(2) show ?case by auto |
150 next |
150 next |
151 case (WhileTrue b s c s'' s') |
151 case (WhileTrue b s c s'' s') |
152 let ?w = "WHILE b DO c" |
152 let ?w = "WHILE b DO c" |
153 from `0 \<turnstile> ?w` have [simp]: "sec b = 0" by auto |
153 from `0 \<turnstile> ?w` have [simp]: "sec b = 0" by auto |
154 have "0 \<turnstile> c" using WhileTrue.prems(1) by auto |
154 have "0 \<turnstile> c" using `0 \<turnstile> WHILE b DO c` by auto |
155 from WhileTrue.IH(1)[OF this WhileTrue.prems(2)] |
155 from WhileTrue.IH(1)[OF this `s = t (\<le> l)`] |
156 obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast |
156 obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast |
157 from WhileTrue.IH(2)[OF `0 \<turnstile> ?w` this(2)] |
157 from WhileTrue.IH(2)[OF `0 \<turnstile> ?w` this(2)] |
158 obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast |
158 obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast |
159 from `bval b s` have "bval b t" |
159 from `bval b s` have "bval b t" |
160 using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto |
160 using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto |