Stream: Beginner Questions

Topic: evaluation value\theorem


view this post on Zulip Robert Soeldner (Jul 21 2021 at 17:48):

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?

view this post on Zulip Mathias Fleury (Jul 21 2021 at 19:05):

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

apply code_simp?

view this post on Zulip Robert Soeldner (Jul 21 2021 at 19:07):

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


Last updated: Sep 25 2021 at 08:21 UTC