Stream: Beginner Questions

Topic: How to work with function defs that have lets in proofs

waynee95 (Nov 30 2022 at 16:57):

I am not sure how to deal with function definitions that contain lets inside proofs.

Unfolding the function definition yields

  have "lapprox_tm0 η0 η1 d φ x ⊥ (Suc n) = (let (val, η1', d') = lapprox_tm0 η0 η1 d φ x ⊥ n in
                                          eval_tm0 (η0(x := val)) η1' d' φ)"
    by simp

Eventually I would like to connect lapprox_tm0 to eval_tm0 but the following obviously does not work since the variables are not in scope

  have "lapprox_tm0 η0' η1' d φ x ⊥ (Suc n) = (let (val, η1'', d') = lapprox_tm0 η0' η1' d φ x ⊥ n in
                                          eval_tm0 (η0'(x := val)) η1'' d' φ)"
    by simp
  then have "lapprox_tm0 η0' η1' d φ x ⊥ (Suc n) = eval_tm0 (η0'(x := val)) η1'' d' φ" (* error *)

so simp fails on the last step.

On paper I would imagine to do the following

  fix val η1'' d'
  assume "lapprox_tm0 η0 η1 d φ x ⊥ n = (val, η1'', d')"
  then have 1: "lapprox_tm0 η0 η1 d φ x ⊥ (Suc n) = eval_tm0 (η0(x := val)) η1'' d' φ"
    by simp

where now simp would work. But I cannot do this inside the proof in Isabelle since I got that assume there which causes the proof state to error obviously.

Jonathan Julian Huerta y Munive (Dec 01 2022 at 09:47):

I do not know the details of your proof. You might want to provide a minimal working example of your problem, but to cover the basics, have you passed the definition of Let Let_def to the simplifier? i.e. apply (simp add: Let_def)?

Last updated: Dec 21 2024 at 16:20 UTC