equal
deleted
inserted
replaced
52 |
52 |
53 lemma valuesum_choice: |
53 lemma valuesum_choice: |
54 "finite (Mapping.keys M) \<Longrightarrow> x \<in> Mapping.keys M \<Longrightarrow> y \<in> Mapping.keys M \<Longrightarrow> |
54 "finite (Mapping.keys M) \<Longrightarrow> x \<in> Mapping.keys M \<Longrightarrow> y \<in> Mapping.keys M \<Longrightarrow> |
55 the (Mapping.lookup M x) + valuesum (Mapping.delete x M) = |
55 the (Mapping.lookup M x) + valuesum (Mapping.delete x M) = |
56 the (Mapping.lookup M y) + valuesum (Mapping.delete y M)" |
56 the (Mapping.lookup M y) + valuesum (Mapping.delete y M)" |
57 unfolding valuesum_def by transfer (simp add: setsum_diff) |
57 unfolding valuesum_def by transfer (simp add: sum_diff) |
58 |
58 |
59 text \<open> |
59 text \<open> |
60 Given \<open>valuesum_rec\<close> as initial description, we stepwise refine it to something executable; |
60 Given \<open>valuesum_rec\<close> as initial description, we stepwise refine it to something executable; |
61 first, we formally insert the constructor @{term Mapping} and split the one equation into two, |
61 first, we formally insert the constructor @{term Mapping} and split the one equation into two, |
62 where the second one provides the necessary context: |
62 where the second one provides the necessary context: |