src/HOL/ex/Execute_Choice.thy

     let l = (SOME l. l \<in> Mapping.keys m) in the (Mapping.lookup m l) + valuesum (Mapping.delete l m))"
 proof (cases "Mapping.is_empty m")
   case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
 next
   case False
-  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def keys_def)
+  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" unfolding is_empty_def by transfer auto
   then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
      the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
        (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
   proof (rule someI2_ex)
     fix l

     then show "(let l = l
         in the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
         (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
       by simp
    qed
-  then show ?thesis by (simp add: keys_def valuesum_def is_empty_def)
+  then show ?thesis unfolding is_empty_def valuesum_def by transfer simp
 qed
 
 text {*
   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

 
 lemma valuesum_choice:
   "finite (Mapping.keys M) \<Longrightarrow> x \<in> Mapping.keys M \<Longrightarrow> y \<in> Mapping.keys M \<Longrightarrow>
     the (Mapping.lookup M x) + valuesum (Mapping.delete x M) =
     the (Mapping.lookup M y) + valuesum (Mapping.delete y M)"
-  by (simp add: valuesum_def keys_def setsum_diff)
+  unfolding valuesum_def  by transfer (simp add: setsum_diff)
 
 text {*
   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: