Wie werden sowohl Schlüssel als auch Werte eines Mappings abgebildet?

Question

Ich brauche eine Funktion zu definieren, die Schlüssel und Werte eines endlichen Karte in einen Satz von Schlüsselwertpaaren abbildet:

theory Test 
    imports Main "~~/src/HOL/Library/Finite_Map" 
begin 

definition denorm :: "('a, 'b) fmap ⇒ ('a × 'b) fset" where 
    "denorm m ≡ " 

end 

Das Problem ist, dass ich diese Funktion durch Rekursion nicht definieren kann, weil fmap ISN ist kein induktiver Datentyp und hat keine Konstruktoren.

Ich denke, dass fmap wird als eine Liste von Paaren intern dargestellt. Ist es möglich, fmap in die Liste zu konvertieren? Ich brauche eine Inverse von Funktion.

Answer 1

Eine Möglichkeit ist Bild zusammensetzt, Domäne und lookup: Der Ausdruck

λ m. (λ k. (k, the (fmlookup m k))) |`| fmdom m 

den gewünschten Typ

('a, 'b) fmap ⇒ ('a × 'b) fset 

und sollte den gewünschten Satz für eine Karte m berechnen.

Answer 2

Diese Funktion ist schon da:

fset_of_fmap :: "('a, 'b) fmap ⇒ ('a × 'b) fset"