equal
deleted
inserted
replaced
717 (\<exists>v. (\<exists>t. (Z', t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s') \<and> |
717 (\<exists>v. (\<exists>t. (Z', t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s') \<and> |
718 (fst s' = None \<longrightarrow> \<not> the_Bool v)) \<and> Y' = \<diamondsuit>" |
718 (fst s' = None \<longrightarrow> \<not> the_Bool v)) \<and> Y' = \<diamondsuit>" |
719 show "Y' = \<diamondsuit> \<and> G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'" |
719 show "Y' = \<diamondsuit> \<and> G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'" |
720 proof - |
720 proof - |
721 from asm obtain v t where |
721 from asm obtain v t where |
722 \<comment> \<open>@{term "Z'"} gets instantiated with @{term "Norm s"}\<close> |
722 \<comment> \<open>\<^term>\<open>Z'\<close> gets instantiated with \<^term>\<open>Norm s\<close>\<close> |
723 unroll: "(Norm s, t) \<in> (unroll G l e c)\<^sup>*" and |
723 unroll: "(Norm s, t) \<in> (unroll G l e c)\<^sup>*" and |
724 eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" and |
724 eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" and |
725 normal_termination: "normal s' \<longrightarrow> \<not> the_Bool v" and |
725 normal_termination: "normal s' \<longrightarrow> \<not> the_Bool v" and |
726 Y': "Y' = \<diamondsuit>" |
726 Y': "Y' = \<diamondsuit>" |
727 by auto |
727 by auto |
1367 shows "\<forall>A. A \<subseteq> uA \<longrightarrow> n \<le> card uA \<longrightarrow> card A = card uA - n |
1367 shows "\<forall>A. A \<subseteq> uA \<longrightarrow> n \<le> card uA \<longrightarrow> card A = card uA - n |
1368 \<longrightarrow> (\<forall>t. P A {mgf t})" |
1368 \<longrightarrow> (\<forall>t. P A {mgf t})" |
1369 using finU uA |
1369 using finU uA |
1370 apply - |
1370 apply - |
1371 apply (induct_tac "n") |
1371 apply (induct_tac "n") |
1372 apply (tactic "ALLGOALS (clarsimp_tac @{context})") |
1372 apply (tactic "ALLGOALS (clarsimp_tac \<^context>)") |
1373 apply (tactic \<open>dresolve_tac @{context} [Thm.permute_prems 0 1 @{thm card_seteq}] 1\<close>) |
1373 apply (tactic \<open>dresolve_tac \<^context> [Thm.permute_prems 0 1 @{thm card_seteq}] 1\<close>) |
1374 apply simp |
1374 apply simp |
1375 apply (erule finite_imageI) |
1375 apply (erule finite_imageI) |
1376 apply (simp add: MGF_asm ax_derivs_asm) |
1376 apply (simp add: MGF_asm ax_derivs_asm) |
1377 apply (rule MGF_asm) |
1377 apply (rule MGF_asm) |
1378 apply (rule ballI) |
1378 apply (rule ballI) |