350 Goal "[| I:Fin(X);F:program |] \ |
350 Goal "[| I:Fin(X);F:program |] \ |
351 \ ==> (ALL i:I. F : (A(i)) LeadsTo (A'(i) Un C)) --> \ |
351 \ ==> (ALL i:I. F : (A(i)) LeadsTo (A'(i) Un C)) --> \ |
352 \ (ALL i:I. F : (A'(i)) Co (A'(i) Un C)) --> \ |
352 \ (ALL i:I. F : (A'(i)) Co (A'(i) Un C)) --> \ |
353 \ F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)"; |
353 \ F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)"; |
354 by (etac Fin_induct 1); |
354 by (etac Fin_induct 1); |
355 by (auto_tac (claset(), simpset() addsimps [Inter_0])); |
355 by (auto_tac (claset(), simpset() delsimps INT_simps |
356 by (case_tac "y=0" 1); |
356 addsimps [Inter_0])); |
357 by Auto_tac; |
|
358 by (etac not_emptyE 1); |
|
359 by (subgoal_tac "Inter(cons(A(x), RepFun(y, A)))= A(x) Int Inter(RepFun(y,A)) &\ |
|
360 \ Inter(cons(A'(x), RepFun(y, A')))= A'(x) Int Inter(RepFun(y,A'))" 1); |
|
361 by (Blast_tac 2); |
|
362 by (Asm_simp_tac 1); |
|
363 by (rtac Completion 1); |
357 by (rtac Completion 1); |
364 by (subgoal_tac "Inter(RepFun(y, A')) Un C = (INT x:RepFun(y, A'). x Un C)" 4); |
358 by (asm_simp_tac (simpset() delsimps INT_simps addsimps INT_extend_simps) 4); |
365 by (asm_simp_tac (simpset() delsimps INT_simps) 4); |
|
366 by (rtac Constrains_INT 4); |
359 by (rtac Constrains_INT 4); |
367 by (REPEAT(Blast_tac 1)); |
360 by (REPEAT(Blast_tac 1)); |
368 val lemma = result(); |
361 val lemma = result(); |
369 |
362 |
370 val prems = Goal |
363 val prems = Goal |