equal
deleted
inserted
replaced
88 "\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> |
88 "\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> |
89 card (nyinitcls G (x,init_class_obj G C s)) \<le> n" |
89 card (nyinitcls G (x,init_class_obj G C s)) \<le> n" |
90 apply (subgoal_tac |
90 apply (subgoal_tac |
91 "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))") |
91 "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))") |
92 apply clarsimp |
92 apply clarsimp |
93 apply (erule thin_rl) |
93 apply (erule_tac V="nyinitcls G (x, s) = ?rhs" in thin_rl) |
94 apply (rule card_Suc_lemma [OF _ _ finite_nyinitcls]) |
94 apply (rule card_Suc_lemma [OF _ _ finite_nyinitcls]) |
95 apply (auto dest!: not_initedD elim!: |
95 apply (auto dest!: not_initedD elim!: |
96 simp add: nyinitcls_def inited_def split add: split_if_asm) |
96 simp add: nyinitcls_def inited_def split add: split_if_asm) |
97 done |
97 done |
98 |
98 |
384 apply (unfold MGF_def) |
384 apply (unfold MGF_def) |
385 apply (auto del: conjI elim!: conseq12) |
385 apply (auto del: conjI elim!: conseq12) |
386 apply (case_tac "\<exists>w s. G\<turnstile>Norm sa \<midarrow>t\<succ>\<rightarrow> (w,s) ") |
386 apply (case_tac "\<exists>w s. G\<turnstile>Norm sa \<midarrow>t\<succ>\<rightarrow> (w,s) ") |
387 apply (fast dest: unique_eval) |
387 apply (fast dest: unique_eval) |
388 apply clarsimp |
388 apply clarsimp |
389 apply (erule thin_rl) |
|
390 apply (erule thin_rl) |
|
391 apply (drule split_paired_All [THEN subst]) |
389 apply (drule split_paired_All [THEN subst]) |
392 apply (clarsimp elim!: state_not_single) |
390 apply (clarsimp elim!: state_not_single) |
393 done |
391 done |
394 |
392 |
395 |
393 |
676 apply (rule ballI) |
674 apply (rule ballI) |
677 apply (case_tac "mgf_call pn : A") |
675 apply (case_tac "mgf_call pn : A") |
678 apply (fast intro: ax_derivs_asm) |
676 apply (fast intro: ax_derivs_asm) |
679 apply (rule MGF_nested_Methd) |
677 apply (rule MGF_nested_Methd) |
680 apply (rule ballI) |
678 apply (rule ballI) |
681 apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] impE, |
679 apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec) |
682 erule_tac [4] spec) |
|
683 apply fast |
680 apply fast |
684 apply (erule Suc_leD) |
|
685 apply (drule finite_subset) |
681 apply (drule finite_subset) |
686 apply (erule finite_imageI) |
682 apply (erule finite_imageI) |
687 apply auto |
683 apply auto |
688 apply arith |
684 apply arith |
689 done |
685 done |