waynee95 (Dec 11 2022 at 00:29): waynee95 (Dec 11 2022 at 00:29):I found out how I can approach this and solve me being stuck.
...
then have 0: "eval_tm0 η0 η1 d (App x1 x2) = (let (val, η1', d') = (eval_tm0 η0 η1 d x2) in
(eval_tm1 η0 η1' d' x1 val))"
by simp
...
then have 2: "eval_tm0 η0 η1 d x2 = (val', η1'', d'')
⟹ eval_tm1 η0 η1'' d'' x1 val' = (val, η1', d')
⟹ (∀x. set (d x) ⊆ set (d' x)) ∧ (∀x f. η1 x f ≤ η1' x f)" for val' η1'' d''
by (meson App.IH(1) dual_order.trans)
So if a function relies on the result of another function via a let in its body, I use these conditionals to give names to intermediate values.
Notification Bot (Dec 11 2022 at 00:29):waynee95 has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC