theory ResourcedDenotational imports "Abstract-Denotational-Props" "CValue-Nominal" "C-restr" begin type_synonym CEnv = "var ⇒ (C → CValue)" interpretation semantic_domain "Λ f . Λ r. CFn⋅(Λ v. (f⋅(v))|⇘r⇙)" "Λ x y. (Λ r. (x⋅r ↓CFn y|⇘r⇙)⋅r)" "Λ b r. CB⋅b" "Λ scrut v1 v2 r. CB_project⋅(scrut⋅r)⋅(v1⋅r)⋅(v2⋅r)" "C_case". abbreviation ESem_syn'' ("𝒩⟦ _ ⟧⇘_⇙" [60,60] 60) where "𝒩⟦ e ⟧⇘ρ⇙ ≡ ESem e ⋅ ρ" abbreviation EvalHeapSem_syn'' ("❙𝒩⟦ _ ❙⟧⇘_⇙" [0,0] 110) where "❙𝒩⟦Γ❙⟧⇘ρ⇙ ≡ evalHeap Γ (λ e. 𝒩⟦e⟧⇘ρ⇙)" abbreviation HSem_syn' ("𝒩⦃_⦄_" [60,60] 60) where "𝒩⦃Γ⦄ρ ≡ HSem Γ ⋅ ρ" abbreviation HSem_bot ("𝒩⦃_⦄" [60] 60) where "𝒩⦃Γ⦄ ≡ 𝒩⦃Γ⦄⊥" text {* Here we re-state the simplification rules, cleaned up by beta-reducing the locale parameters. *} lemma CESem_simps: "𝒩⟦ Lam [x]. e ⟧⇘ρ⇙ = (Λ (C⋅r). CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙)|⇘r⇙))" "𝒩⟦ App e x ⟧⇘ρ⇙ = (Λ (C⋅r). ((𝒩⟦ e ⟧⇘ρ⇙)⋅r ↓CFn ρ x|⇘r⇙)⋅r)" "𝒩⟦ Var x ⟧⇘ρ⇙ = (Λ (C⋅r). (ρ x) ⋅ r)" "𝒩⟦ Bool b ⟧⇘ρ⇙ = (Λ (C⋅r). CB⋅(Discr b))" "𝒩⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘ρ⇙ = (Λ (C⋅r). CB_project⋅((𝒩⟦ scrut ⟧⇘ρ⇙)⋅r)⋅((𝒩⟦ e⇩1 ⟧⇘ρ⇙)⋅r)⋅((𝒩⟦ e⇩2 ⟧⇘ρ⇙)⋅r))" "𝒩⟦ Let as body ⟧⇘ρ⇙ = (Λ (C ⋅ r). (𝒩⟦body⟧⇘𝒩⦃as⦄ρ⇙) ⋅ r)" by (auto simp add: eta_cfun) lemma CESem_bot[simp]:"(𝒩⟦ e ⟧⇘σ⇙)⋅⊥ = ⊥" by (nominal_induct e arbitrary: σ rule: exp_strong_induct) auto lemma CHSem_bot[simp]:"((𝒩⦃ Γ ⦄) x)⋅⊥ = ⊥" by (cases "x ∈ domA Γ") (auto simp add: lookup_HSem_heap lookup_HSem_other) text {* Sometimes we do not care much about the resource usage and just want a simpler formula. *} lemma CESem_simps_no_tick: "(𝒩⟦ Lam [x]. e ⟧⇘ρ⇙)⋅r ⊑ CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙)|⇘r⇙)" "(𝒩⟦ App e x ⟧⇘ρ⇙)⋅r ⊑ ((𝒩⟦ e ⟧⇘ρ⇙)⋅r ↓CFn ρ x|⇘r⇙)⋅r" "𝒩⟦ Var x ⟧⇘ρ⇙ ⊑ ρ x" "(𝒩⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘ρ⇙)⋅r ⊑ CB_project⋅((𝒩⟦ scrut ⟧⇘ρ⇙)⋅r)⋅((𝒩⟦ e⇩1 ⟧⇘ρ⇙)⋅r)⋅((𝒩⟦ e⇩2 ⟧⇘ρ⇙)⋅r)" "𝒩⟦ Let as body ⟧⇘ρ⇙ ⊑ 𝒩⟦body⟧⇘𝒩⦃as⦄ρ⇙" apply - apply (rule below_trans[OF monofun_cfun_arg[OF below_C]], simp) apply (rule below_trans[OF monofun_cfun_arg[OF below_C]], simp) apply (rule cfun_belowI, rule below_trans[OF monofun_cfun_arg[OF below_C]], simp) apply (rule below_trans[OF monofun_cfun_arg[OF below_C]], simp) apply (rule cfun_belowI, rule below_trans[OF monofun_cfun_arg[OF below_C]], simp) done lemma CELam_no_restr: "(𝒩⟦ Lam [x]. e ⟧⇘ρ⇙)⋅r ⊑ CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙))" proof- have "(𝒩⟦ Lam [x]. e ⟧⇘ρ⇙)⋅r ⊑ CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙)|⇘r⇙)" by (rule CESem_simps_no_tick) also have "… ⊑ CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙))" by (intro cont2cont monofun_LAM below_trans[OF C_restr_below] monofun_cfun_arg below_refl fun_upd_mono) finally show ?thesis by this (intro cont2cont) qed lemma CEApp_no_restr: "(𝒩⟦ App e x ⟧⇘ρ⇙)⋅r ⊑ ((𝒩⟦ e ⟧⇘ρ⇙)⋅r ↓CFn ρ x)⋅r" proof- have "(𝒩⟦ App e x ⟧⇘ρ⇙)⋅r ⊑ ((𝒩⟦ e ⟧⇘ρ⇙)⋅r ↓CFn ρ x|⇘r⇙)⋅r" by (rule CESem_simps_no_tick) also have "ρ x|⇘r⇙ ⊑ ρ x" by (rule C_restr_below) finally show ?thesis by this (intro cont2cont) qed end