equal
deleted
inserted
replaced
32 case False with prems show ?thesis by (simp add: setsum_def) |
32 case False with prems show ?thesis by (simp add: setsum_def) |
33 qed |
33 qed |
34 qed |
34 qed |
35 *) |
35 *) |
36 |
36 |
37 (* Instruct simplifier to simplify assumptions introduced by congs. |
37 (* With this variant of setsum_cong, assumptions |
38 This makes setsum_cong more convenient to use, because assumptions |
|
39 like i:{m..n} get simplified (to m <= i & i <= n). *) |
38 like i:{m..n} get simplified (to m <= i & i <= n). *) |
40 |
39 |
41 declare setsum_cong [cong] |
40 declare strong_setsum_cong [cong] |
42 |
|
43 ML_setup {* |
|
44 simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; |
|
45 *} |
|
46 |
41 |
47 section {* Definition of type up *} |
42 section {* Definition of type up *} |
48 |
43 |
49 constdefs |
44 constdefs |
50 bound :: "[nat, nat => 'a::zero] => bool" |
45 bound :: "[nat, nat => 'a::zero] => bool" |