Comment définir un prédicat constructif pour une carte?

Question

Voici deux prédicats simples:

definition map_is_empty :: "(string ⇒ nat option) ⇒ bool" where 
    "map_is_empty env ≡ ∀x. env x = None" 

value "map_is_empty Map.empty" 
value "map_is_empty [''x''↦1]" 

definition map_is_less_5 :: "(string ⇒ nat option) ⇒ bool" where 
    "map_is_less_5 env ≡ ∀x. ∃y. env x = Some y ∧ y < 5" 

value "map_is_less_5 [''x''↦1,''y''↦2]" 
value "map_is_less_5 [''x''↦1,''y''↦2,''z''↦7]" 

Le problème est que value renvoie des erreurs telles que:

Wellsortedness error 
(in code equation map_is_empty ?env ≡ ∀x. Option.is_none (?env x), 
with dependency "Pure.dummy_pattern" -> "map_is_empty"): 
Type char list not of sort enum 
No type arity list :: enum 

Comment définir ces prédicats pour pouvoir les évaluer en utilisant value ou values?

Peut-être ~~/src/HOL/Library/Finite_Map et ~~/src/HOL/Library/Mapping peuvent aider, mais je reçois des erreurs similaires en les utilisant.

~~/src/HOL/Library/FinFun semble idéal pour ma tâche, mais je reçois la même erreur:

definition ff_is_empty :: "(string ⇒f nat option) ⇒ bool" where 
    "ff_is_empty env ≡ ∀x. env $ x = None" 

value "ff_is_empty (K$ None)" 

Answer 1

Je l'ai! ~~/src/HOL/Library/FinFun est génial. Les détails peuvent être trouvés dans this presentation. Voir aussi "Formaliser FinFuns - Générer du code pour Fonctions comme données d'Isabelle/HOL" par Andreas Lochbihler. Pour chaque prédicat, il faut définir un lemme remplaçant ∀ par finfun_All. Ce lemme est utilisé pour la génération de code:

definition ff_is_empty :: "(string ⇒f nat option) ⇒ bool" where 
    "ff_is_empty env ⟷ (∀x. env $ x = None)" 

lemma ff_is_empty_code [code]: 
    "ff_is_empty env ⟷ finfun_All ((λx. x = None) ∘$ env)" 
    by (auto simp add: ff_is_empty_def finfun_All_All) 

value "ff_is_empty (K$ None)" 
value "ff_is_empty (K$ None)(''x'' $:= Some 1)" 

fun option_less :: "nat option ⇒ nat ⇒ bool" where 
    "option_less (Some a) b = (a < b)" 
| "option_less _ _ = True" 

definition ff_is_less_5 :: "(string ⇒f nat option) ⇒ bool" where 
    "ff_is_less_5 env ⟷ (∀x. option_less (env $ x) 5)" 

lemma ff_is_less_5_code [code]: 
    "ff_is_less_5 env ⟷ finfun_All ((λx. option_less x 5) ∘$ env)" 
    by (auto simp add: ff_is_less_5_def finfun_All_All) 

value "ff_is_less_5 (K$ None)(''x'' $:= Some 1)" 
value "ff_is_less_5 (K$ None)(''x'' $:= Some 1)(''y'' $:= Some 2)(''z'' $:= Some 7)"