# Theory DenotEqualitiesFSet

```subsection "Denotational equalities regarding reduction"

theory DenotEqualitiesFSet
imports DenotCongruenceFSet
begin

theorem eval_prim[simp]: assumes e1:"E e1 = E (ENat n1)" and e2:"E e2 = E (ENat n2)"
shows "E(EPrim f e1 e2)=E(ENat (f n1 n2))"
using e1 e2 by auto

theorem eval_ifz[simp]: assumes e1: "E e1  = E(ENat 0)" shows "E(EIf e1 e2 e3) = E(e3)"
using e1 by auto

theorem eval_ifnz[simp]: assumes e1: "E(e1) = E(ENat n)" and nz: "n ≠ 0"
shows "E(EIf e1 e2 e3) = E(e2)"
using e1 nz by auto

theorem eval_app_lam: assumes vv: "is_val v"
shows "E(EApp (ELam x e) v) = E (subst x v e)"
apply (rule ext) apply (rule equalityI) apply (rule subsetI)
apply (subgoal_tac "EApp (ELam x e) v ⟶ subst x v e") prefer 2 apply (rule beta)
using vv apply assumption apply (rule subject_reduction) apply assumption apply assumption
apply (rule subsetI)
apply (subgoal_tac "EApp (ELam x e) v ⟶ subst x v e") prefer 2 apply (rule beta)
using vv apply assumption apply (rule reverse_step_pres_denot) apply assumption
apply assumption
done

end
```