equal
deleted
inserted
replaced
16 |
16 |
17 (*a simplification step*) |
17 (*a simplification step*) |
18 Goal "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)"; |
18 Goal "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)"; |
19 by (induct_tac "n" 1); |
19 by (induct_tac "n" 1); |
20 by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc]))); |
20 by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc]))); |
21 by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1); |
21 by Auto_tac; |
22 qed "Collect_le_Int_equals"; |
22 qed "Collect_le_Int_equals"; |
23 |
|
24 |
23 |
25 (*Dual of the required property. Converse inclusion fails.*) |
24 (*Dual of the required property. Converse inclusion fails.*) |
26 Goal "(UN i: lessThan n. A i) Int (- A n) <= \ |
25 Goal "(UN i: lessThan n. A i) Int (- A n) <= \ |
27 \ (UN i: lessThan n. (A i) Int (- A (Suc i)))"; |
26 \ (UN i: lessThan n. (A i) Int (- A (Suc i)))"; |
28 by (induct_tac "n" 1); |
27 by (induct_tac "n" 1); |