マッピングのキーと値の両方をマッピングする方法は？

Question

私は、キーと値のペアのセットに有限のマップのキーと値をマップする関数を定義する必要があります。

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

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

end 

問題は、私はfmap ISNので、再帰することで、この関数を定義することができないということです誘導データ型ではなく、コンストラクタもありません。

fmapは内部的にペアのリストとして表されると思います。 fmapをリストに変換できますか？私はfmap_of_listの逆関数が必要です。

Answer 1

1つの可能な方法は、画像、ドメイン、およびルックアップを構成することである：式

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

は、所望のタイプ

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

を有しており、マップmための所望のセットを計算しなければなりません。

Answer 2

この機能は、すでにそこにある：

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