equal
deleted
inserted
replaced
863 case empty then show ?case by simp |
863 case empty then show ?case by simp |
864 next |
864 next |
865 case (insert x F) then show ?case apply - |
865 case (insert x F) then show ?case apply - |
866 apply (simp add: subset_insert_iff, clarify) |
866 apply (simp add: subset_insert_iff, clarify) |
867 apply (subgoal_tac "finite C") |
867 apply (subgoal_tac "finite C") |
868 prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) |
868 prefer 2 apply (blast dest: finite_subset [rotated]) |
869 apply (subgoal_tac "C = insert x (C - {x})") |
869 apply (subgoal_tac "C = insert x (C - {x})") |
870 prefer 2 apply blast |
870 prefer 2 apply blast |
871 apply (erule ssubst) |
871 apply (erule ssubst) |
872 apply (simp add: Ball_def del: insert_Diff_single) |
872 apply (simp add: Ball_def del: insert_Diff_single) |
873 done |
873 done |
1515 proof - |
1515 proof - |
1516 from assms have "ALL C. C <= A --> (ALL x:C. g x = h x) --> F g C = F h C" |
1516 from assms have "ALL C. C <= A --> (ALL x:C. g x = h x) --> F g C = F h C" |
1517 apply - apply (erule finite_induct) apply simp |
1517 apply - apply (erule finite_induct) apply simp |
1518 apply (simp add: subset_insert_iff, clarify) |
1518 apply (simp add: subset_insert_iff, clarify) |
1519 apply (subgoal_tac "finite C") |
1519 apply (subgoal_tac "finite C") |
1520 prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) |
1520 prefer 2 apply (blast dest: finite_subset [rotated]) |
1521 apply (subgoal_tac "C = insert x (C - {x})") |
1521 apply (subgoal_tac "C = insert x (C - {x})") |
1522 prefer 2 apply blast |
1522 prefer 2 apply blast |
1523 apply (erule ssubst) |
1523 apply (erule ssubst) |
1524 apply (drule spec) |
1524 apply (drule spec) |
1525 apply (erule (1) notE impE) |
1525 apply (erule (1) notE impE) |