Comment mapper les deux clés et les valeurs d'un mappage?

Question

J'ai besoin de définir une fonction qui clés et des valeurs d'une carte finie en un ensemble de paires clé-valeur:

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

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

end 

Le problème est que je ne peux pas définir cette fonction par récursion, parce que fmap ISN 't un type de données inductif et il n'a aucun constructeur.

Je suppose que fmap est représenté sous la forme d'une liste de paires en interne. Est-il possible de convertir fmap à la liste? J'ai besoin d'une fonction inverse de fmap_of_list.

Answer 1

Une façon possible consiste à composer l'image, le domaine et recherche: l'expression

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

a le type désiré

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

et doit calculer la consigne souhaitée pour une carte m.

Answer 2

Cette fonction est déjà là:

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