summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/Execute_Choice.thy

changeset 36109 | 1028cf8c0d1b |

parent 35164 | 8e3b8b5f1e96 |

child 37055 | 8f9f3d61ca8c |

--- a/src/HOL/ex/Execute_Choice.thy Fri Apr 09 13:35:54 2010 +0200 +++ b/src/HOL/ex/Execute_Choice.thy Sun Apr 11 16:51:05 2010 +0200 @@ -58,15 +58,15 @@ text {* Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable; - first, we formally insert the constructor @{term AList} and split the one equation into two, + first, we formally insert the constructor @{term Mapping} and split the one equation into two, where the second one provides the necessary context: *} -lemma valuesum_rec_AList: - shows [code]: "valuesum (AList []) = 0" - and "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in - the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))" - by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList) +lemma valuesum_rec_Mapping: + shows [code]: "valuesum (Mapping []) = 0" + and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in + the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))" + by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping) text {* As a side effect the precondition disappears (but note this has nothing to do with choice!). @@ -76,27 +76,27 @@ *} lemma valuesum_rec_exec [code]: - "valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in - the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))" + "valuesum (Mapping (x # xs)) = (let l = fst (hd (x # xs)) in + the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))" proof - - let ?M = "AList (x # xs)" + let ?M = "Mapping (x # xs)" let ?l1 = "(SOME l. l \<in> Mapping.keys ?M)" let ?l2 = "fst (hd (x # xs))" - have "finite (Mapping.keys ?M)" by (simp add: keys_AList) + have "finite (Mapping.keys ?M)" by (simp add: keys_Mapping) moreover have "?l1 \<in> Mapping.keys ?M" - by (rule someI) (auto simp add: keys_AList) + by (rule someI) (auto simp add: keys_Mapping) moreover have "?l2 \<in> Mapping.keys ?M" - by (simp add: keys_AList) + by (simp add: keys_Mapping) ultimately have "the (Mapping.lookup ?M ?l1) + valuesum (Mapping.delete ?l1 ?M) = the (Mapping.lookup ?M ?l2) + valuesum (Mapping.delete ?l2 ?M)" by (rule valuesum_choice) - then show ?thesis by (simp add: valuesum_rec_AList) + then show ?thesis by (simp add: valuesum_rec_Mapping) qed text {* See how it works: *} -value "valuesum (AList [(''abc'', (42::int)), (''def'', 1705)])" +value "valuesum (Mapping [(''abc'', (42::int)), (''def'', 1705)])" end