src/HOL/ex/Execute_Choice.thy
changeset 61343 5b5656a63bd6
parent 58889 5b7a9633cfa8
child 61933 cf58b5b794b2
--- a/src/HOL/ex/Execute_Choice.thy	Tue Oct 06 17:46:07 2015 +0200
+++ b/src/HOL/ex/Execute_Choice.thy	Tue Oct 06 17:47:28 2015 +0200
@@ -1,22 +1,22 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-section {* A simple cookbook example how to eliminate choice in programs. *}
+section \<open>A simple cookbook example how to eliminate choice in programs.\<close>
 
 theory Execute_Choice
 imports Main "~~/src/HOL/Library/AList_Mapping"
 begin
 
-text {*
+text \<open>
   A trivial example:
-*}
+\<close>
 
 definition valuesum :: "('a, 'b :: ab_group_add) mapping \<Rightarrow> 'b" where
   "valuesum m = (\<Sum>k \<in> Mapping.keys m. the (Mapping.lookup m k))"
 
-text {*
+text \<open>
   Not that instead of defining @{term valuesum} with choice, we define it
   directly and derive a description involving choice afterwards:
-*}
+\<close>
 
 lemma valuesum_rec:
   assumes fin: "finite (dom (Mapping.lookup m))"
@@ -44,11 +44,11 @@
   then show ?thesis unfolding is_empty_def valuesum_def by transfer simp
 qed
 
-text {*
+text \<open>
   In the context of the else-branch we can show that the exact choice is
   irrelvant; in practice, finding this point where choice becomes irrelevant is the
   most difficult thing!
-*}
+\<close>
 
 lemma valuesum_choice:
   "finite (Mapping.keys M) \<Longrightarrow> x \<in> Mapping.keys M \<Longrightarrow> y \<in> Mapping.keys M \<Longrightarrow>
@@ -56,11 +56,11 @@
     the (Mapping.lookup M y) + valuesum (Mapping.delete y M)"
   unfolding valuesum_def  by transfer (simp add: setsum_diff)
 
-text {*
+text \<open>
   Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable;
   first, we formally insert the constructor @{term Mapping} and split the one equation into two,
   where the second one provides the necessary context:
-*}
+\<close>
 
 lemma valuesum_rec_Mapping:
   shows [code]: "valuesum (Mapping []) = 0"
@@ -68,12 +68,12 @@
     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 null_def)
 
-text {*
+text \<open>
   As a side effect the precondition disappears (but note this has nothing to do with choice!).
   The first equation deals with the uncritical empty case and can already be used for code generation.
 
   Using @{text valuesum_choice}, we are able to prove an executable version of @{term valuesum}:
-*}
+\<close>
 
 lemma valuesum_rec_exec [code]:
   "valuesum (Mapping (x # xs)) = (let l = fst (hd (x # xs)) in
@@ -93,9 +93,9 @@
   then show ?thesis by (simp add: valuesum_rec_Mapping)
 qed
   
-text {*
+text \<open>
   See how it works:
-*}
+\<close>
 
 value "valuesum (Mapping [(''abc'', (42::int)), (''def'', 1705)])"