title: How to map both keys and values of a mapping?
body: <p>I need to define a function which maps keys and values of a finite map into a set of key-value pairs:</p>
  
  <pre><code>theory Test
    imports Main "~~/src/HOL/Library/Finite_Map"
  begin
  
  definition denorm :: "('a, 'b) fmap ⇒ ('a × 'b) fset" where
    "denorm m ≡ "
  
  end
  </code></pre>
  
  <p>The problem is that I can't define this function by recursion, because <code>fmap</code> isn't an inductive data type and it doesn't have any constructors.</p>
  
  <p>I guess that <code>fmap</code> is represented as a list of pairs internally. Is it possible to convert <code>fmap</code> to the list? I need an inverse of <code>fmap_of_list</code> function.</p>