CODEWITHSUNDEEP
isabelle
Denis
Denis

Reputation: 1271

How to defined a constructive predicate for a map?

Here are two simple predicates:

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]"

The problem is that value returns errors such as:

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

How to define these predicates to be able to evaluate them using value or values?

Maybe ~~/src/HOL/Library/Finite_Map and ~~/src/HOL/Library/Mapping can help, but I get similar errors using them.

~~/src/HOL/Library/FinFun seems ideal for my task, but I get the same error:

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

value "ff_is_empty (K$ None)"

Upvotes: 2

Views: 121

Answers (1)

Denis
Denis

Reputation: 1271

I've got it! ~~/src/HOL/Library/FinFun is great. Details can be found in this presentation. Also look at "Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL" by Andreas Lochbihler.

For each predicate one must define a lemma replacing ∀ by finfun_All. This lemma is used for code generation:

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)"

Upvotes: 2

Related Questions