Email Gateway (Aug 22 2022 at 15:47): Email Gateway (Aug 22 2022 at 15:47):From: "Siek, Jeremy" <jsiek@indiana.edu>
I’m seeing a case turn into a call to the datatype’s case function in the LaTeX output
(see case-val below), but I’d prefer it to stay as a case.
In particular, I have the following equation in a fun definition.
"E (EIf e1 e2 e3) ρ = (v1 ← E e1 ρ;
case v1 of
(VNat n) ⇒ if n ≠ 0 then E e2 ρ else E e3 ρ
| (VFun t) ⇒ zero)”
But it’s producing the following in the LaTeX (PDF):
E (if e1 then e2 else e3) ρ = set-bind (E e1 ρ) (case-val (λn. if n 0 then E e2 ρ else E e3 ρ) (λt. zero))
I’m wondering if the set-bind is somehow triggering this behavior… It’s the bind for a
non-determinism monad that I define as follows.
definition set_bind :: "'a M ⇒ ('a ⇒ 'b M) ⇒ 'b M" where
"set_bind m f ≡ { v. ∃ v'. v' ∈ m ∧ v ∈ f v' }"
declare set_bind_def[simp]
syntax "_set_bind" :: "[pttrns,'a M,'b] ⇒ 'c" ("(_ ← _;//_)" 0)
translations "P ← E; F" ⇌ "CONST set_bind E (λP. F)”
Any help is appreciated!
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 15:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Jeremy,
An eta-contraction is happening here, because the bound variable v1 is the last argument
to the case operator, so Isabelle sees "%v1. case_val ... ... v1" here. Have you tried to
disable locally eta-contraction, e.g., by declare [[eta_contract = false]]?
Alternatively, you can install a print_translation to avoid the eta-contraction for set_bind:
print_translation {*
Syntax_Trans.preserve_binder_abs2_tr'
@{const_syntax set_bind} @{syntax_const "_set_bind"}
*}
Disclaimer: I've just adapted this from the setup for Ball/Bex, but I haven't tried
whether this works for your specific bind operation.
Hope this helps,
Andreas
Last updated: Apr 25 2024 at 04:18 UTC