equal
deleted
inserted
replaced
365 !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})" |
365 !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})" |
366 apply (induct_tac n) |
366 apply (induct_tac n) |
367 apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) |
367 apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) |
368 apply (subgoal_tac "G = mgt_call ` U") |
368 apply (subgoal_tac "G = mgt_call ` U") |
369 prefer 2 |
369 prefer 2 |
370 apply (simp add: card_seteq finite_imageI) |
370 apply (simp add: card_seteq) |
371 apply simp |
371 apply simp |
372 apply (erule prems(3-)) (*MGF_lemma1*) |
372 apply (erule prems(3-)) (*MGF_lemma1*) |
373 apply (rule ballI) |
373 apply (rule ballI) |
374 apply (rule prems) (*hoare_derivs.asm*) |
374 apply (rule prems) (*hoare_derivs.asm*) |
375 apply fast |
375 apply fast |