equal
deleted
inserted
replaced
854 (* Note: `n <= foldl op+ n ns' looks simpler, but is more difficult to use |
854 (* Note: `n <= foldl op+ n ns' looks simpler, but is more difficult to use |
855 because it requires an additional transitivity step |
855 because it requires an additional transitivity step |
856 *) |
856 *) |
857 Goal "!n::nat. m <= n --> m <= foldl op+ n ns"; |
857 Goal "!n::nat. m <= n --> m <= foldl op+ n ns"; |
858 by (induct_tac "ns" 1); |
858 by (induct_tac "ns" 1); |
859 by (Simp_tac 1); |
859 by Auto_tac; |
860 by (Asm_full_simp_tac 1); |
|
861 qed_spec_mp "start_le_sum"; |
860 qed_spec_mp "start_le_sum"; |
862 |
861 |
863 Goal "n : set ns ==> n <= foldl op+ 0 ns"; |
862 Goal "n : set ns ==> n <= foldl op+ 0 ns"; |
864 by (force_tac (claset() addIs [start_le_sum], |
863 by (force_tac (claset() addIs [start_le_sum], |
865 simpset() addsimps [in_set_conv_decomp]) 1); |
864 simpset() addsimps [in_set_conv_decomp]) 1); |