Actually, I was able to make some functions executable, e.g. running

```
value "Dang (fst r1)"
```

prints the correct behavior

```
"⌈indeg ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 1 ⌈∧⌉ ⌈outdeg ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 0 ⌈∧⌉ form.T"
:: "form"
```

but when trying to use the `Dang`

fun in a theorem (equality in this case) like

```
lemma "(Dang (fst r1)) = (⌈indeg ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 1 ⌈∧⌉ ⌈outdeg ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 0 ⌈∧⌉ form.T)"
apply (simp add: r1_def)
```

The remaining goal looks like

```
goal (1 subgoal):
1. (eval g undefined
(foldr
(λk a. ⌈indeg ↝⇩V k⌉ ⌈=⌉
▹⇩I foldr
(λka b.
if edge_trg
(the (if ka = Suc 0 then Some ⦇edge_src = Suc 0, edge_trg = 2, edge_mark = RuleMarkEdge_None, edge_label = [Var 3]⦈
else [2 ↦ ⦇edge_src = Suc 0, edge_trg = 3, edge_mark = RuleMarkEdge_None, edge_label = [Var 4]⦈] ka)) =
k
then Suc b else b)
(Mapping.ordered_keys
(AList_Mapping.Mapping
[(Suc 0, ⦇edge_src = Suc 0, edge_trg = 2, edge_mark = RuleMarkEdge_None, edge_label = [Var 3]⦈),
(2, ⦇edge_src = Suc 0, edge_trg = 3, edge_mark = RuleMarkEdge_None, edge_label = [Var 4]⦈)]))
0 ⌈∧⌉
⌈outdeg ↝⇩V k⌉ ⌈=⌉
....
```

I guess, some simplification rules are missing (e.g. Mapping.ordered_keys, or AList_Mapping.Mapping). For me, the expected behavior would be that `simp`

would equally evaluate. What peace am I missing?

From https://isabelle.in.tum.de/dist/Isabelle2021/doc/codegen.pdf:

`apply code_simp`

?

yea ... actually this was what I was looking for, thanks again :-)

Last updated: Jun 20 2024 at 08:21 UTC