equal
deleted
inserted
replaced
136 \ ==> f (fold f e A) (fold f e B) = \ |
136 \ ==> f (fold f e A) (fold f e B) = \ |
137 \ f (fold f e (A Un B)) (fold f e (A Int B))"; |
137 \ f (fold f e (A Un B)) (fold f e (A Int B))"; |
138 by (etac finite_induct 1); |
138 by (etac finite_induct 1); |
139 by (Simp_tac 1); |
139 by (Simp_tac 1); |
140 by (asm_simp_tac |
140 by (asm_simp_tac |
141 (simpset() addsimps (f_ac @ [insert_absorb, Int_insert_left])) 1); |
141 (simpset() addsimps f_ac @ [insert_absorb, Int_insert_left]) 1); |
142 by (rtac impI 1); |
142 by (rtac impI 1); |
143 by (stac f_commute 1 THEN rtac refl 1); |
143 by (stac f_commute 1 THEN rtac refl 1); |
144 qed "fold_Un_Int"; |
144 qed "fold_Un_Int"; |
145 |
145 |
146 Goal "[| finite A; finite B; A Int B = {} |] \ |
146 Goal "[| finite A; finite B; A Int B = {} |] \ |