theory Launchbury imports Terms Substitution begin subsubsection {* The natural semantics *} text {* This is the semantics as in \cite{launchbury}, with two differences: \begin{itemize} \item Explicit freshness requirements for bound variables in the application and the Let rule. \item An additional parameter that stores variables that have to be avoided, but do not occur in the judgement otherwise, follwing \cite{sestoft}. \end{itemize} *} inductive reds :: "heap ⇒ exp ⇒ var list ⇒ heap ⇒ exp ⇒ bool" ("_ : _ ⇓⇘_⇙ _ : _" [50,50,50,50] 50) where Lambda: "Γ : (Lam [x]. e) ⇓⇘L⇙ Γ : (Lam [x]. e)" | Application: "⟦ atom y ♯ (Γ,e,x,L,Δ,Θ,z) ; Γ : e ⇓⇘L⇙ Δ : (Lam [y]. e'); Δ : e'[y ::= x] ⇓⇘L⇙ Θ : z ⟧ ⟹ Γ : App e x ⇓⇘L⇙ Θ : z" | Variable: "⟦ map_of Γ x = Some e; delete x Γ : e ⇓⇘x#L⇙ Δ : z ⟧ ⟹ Γ : Var x ⇓⇘L⇙ (x, z) # Δ : z" | Let: "⟦ atom ` domA Δ ♯* (Γ, L); Δ @ Γ : body ⇓⇘L⇙ Θ : z ⟧ ⟹ Γ : Let Δ body ⇓⇘L⇙ Θ : z" | Bool: "Γ : Bool b ⇓⇘L⇙ Γ : Bool b" | IfThenElse: "⟦ Γ : scrut ⇓⇘L⇙ Δ : (Bool b); Δ : (if b then e⇩1 else e⇩2) ⇓⇘L⇙ Θ : z ⟧ ⟹ Γ : (scrut ? e⇩1 : e⇩2) ⇓⇘L⇙ Θ : z" equivariance reds nominal_inductive reds avoids Application: "y" by (auto simp add: fresh_star_def fresh_Pair) subsubsection {* Example evaluations *} lemma eval_test: "[] : (Let [(x, Lam [y]. Var y)] (Var x)) ⇓⇘[]⇙ [(x, Lam [y]. Var y)] : (Lam [y]. Var y)" apply(auto intro!: Lambda Application Variable Let simp add: fresh_Pair fresh_Cons fresh_Nil fresh_star_def) done lemma eval_test2: "y ≠ x ⟹ n ≠ y ⟹ n ≠ x ⟹[] : (Let [(x, Lam [y]. Var y)] (App (Var x) x)) ⇓⇘[]⇙ [(x, Lam [y]. Var y)] : (Lam [y]. Var y)" by (auto intro!: Lambda Application Variable Let simp add: fresh_Pair fresh_at_base fresh_Cons fresh_Nil fresh_star_def pure_fresh) subsubsection {* Better introduction rules *} text {* This variant do not require freshness. *} lemma reds_ApplicationI: assumes "Γ : e ⇓⇘L⇙ Δ : Lam [y]. e'" assumes "Δ : e'[y::=x] ⇓⇘L⇙ Θ : z" shows "Γ : App e x ⇓⇘L⇙ Θ : z" proof- obtain y' :: var where "atom y' ♯ (Γ, e, x, L, Δ, Θ, z, e')" by (rule obtain_fresh) have a: "Lam [y']. ((y' ↔ y) ∙ e') = Lam [y]. e'" using `atom y' ♯ _` by (auto simp add: Abs1_eq_iff fresh_Pair fresh_at_base) have b: "((y' ↔ y) ∙ e')[y'::=x] = e'[y::=x]" proof(cases "x = y") case True have "atom y' ♯ e'" using `atom y' ♯ _` by simp thus ?thesis by (simp add: True subst_swap_same subst_subst_back) next case False hence "atom y ♯ x" by simp have [simp]: "(y' ↔ y) ∙ x = x" using `atom y ♯ _` `atom y' ♯ _` by (simp add: flip_fresh_fresh fresh_Pair fresh_at_base) have "((y' ↔ y) ∙ e')[y'::=x] = (y' ↔ y) ∙ (e'[y::=x])" by simp also have "… = e'[y::=x]" using `atom y ♯ _` `atom y' ♯ _` by (simp add: flip_fresh_fresh fresh_Pair fresh_at_base subst_pres_fresh) finally show ?thesis. qed have "atom y' ♯ (Γ, e, x, L, Δ, Θ, z)" using `atom y' ♯ _` by (simp add: fresh_Pair) from this assms[folded a b] show ?thesis .. qed lemma reds_SmartLet: "⟦ atom ` domA Δ ♯* (Γ, L); Δ @ Γ : body ⇓⇘L⇙ Θ : z ⟧ ⟹ Γ : SmartLet Δ body ⇓⇘L⇙ Θ : z" unfolding SmartLet_def by (auto intro: reds.Let) text {* A single rule for values *} lemma reds_isValI: "isVal z ⟹ Γ : z ⇓⇘L⇙ Γ : z" by (cases z rule:isVal.cases) (auto intro: reds.intros) subsubsection {* Properties of the semantics *} text {* Heap entries are never removed. *} lemma reds_doesnt_forget: "Γ : e ⇓⇘L⇙ Δ : z ⟹ domA Γ ⊆ domA Δ" by(induct rule: reds.induct) auto text {* Live variables are not added to the heap. *} lemma reds_avoids_live': assumes "Γ : e ⇓⇘L⇙ Δ : z" shows "(domA Δ - domA Γ) ∩ set L = {}" using assms by(induct rule:reds.induct) (auto dest: map_of_domAD fresh_distinct_list simp add: fresh_star_Pair) lemma reds_avoids_live: "⟦ Γ : e ⇓⇘L⇙ Δ : z; x ∈ set L; x ∉ domA Γ ⟧ ⟹ x ∉ domA Δ" using reds_avoids_live' by blast text {* Fresh variables either stay fresh or are added to the heap. *} lemma reds_fresh:" ⟦ Γ : e ⇓⇘L⇙ Δ : z; atom (x::var) ♯ (Γ, e) ⟧ ⟹ atom x ♯ (Δ, z) ∨ x ∈ (domA Δ - set L)" proof(induct rule: reds.induct) case (Lambda Γ x e) thus ?case by auto next case (Application y Γ e x' L Δ Θ z e') hence "atom x ♯ (Δ, Lam [y]. e') ∨ x ∈ domA Δ - set (x' # L)" by (auto simp add: fresh_Pair) thus ?case proof assume "atom x ♯ (Δ, Lam [y]. e')" hence "atom x ♯ e'[y ::= x']" using Application.prems by (auto intro: subst_pres_fresh simp add: fresh_Pair) thus ?thesis using Application.hyps(5) `atom x ♯ (Δ, Lam [y]. e')` by auto next assume "x ∈ domA Δ - set (x' # L)" thus ?thesis using reds_doesnt_forget[OF Application.hyps(4)] by auto qed next case(Variable Γ v e L Δ z) have "atom x ♯ Γ" and "atom x ♯ v" using Variable.prems(1) by (auto simp add: fresh_Pair) from fresh_delete[OF this(1)] have "atom x ♯ delete v Γ". moreover have "v ∈ domA Γ" using Variable.hyps(1) by (metis domA_from_set map_of_SomeD) from fresh_map_of[OF this `atom x ♯ Γ`] have "atom x ♯ the (map_of Γ v)". hence "atom x ♯ e" using `map_of Γ v = Some e` by simp ultimately have "atom x ♯ (Δ, z) ∨ x ∈ domA Δ - set (v # L)" using Variable.hyps(3) by (auto simp add: fresh_Pair) thus ?case using `atom x ♯ v` by (auto simp add: fresh_Pair fresh_Cons fresh_at_base) next case (Bool Γ b L) thus ?case by auto next case (IfThenElse Γ scrut L Δ b e⇩1 e⇩2 Θ z) from `atom x ♯ (Γ, scrut ? e⇩1 : e⇩2)` have "atom x ♯ (Γ, scrut)" and "atom x ♯ (e⇩1, e⇩2)" by (auto simp add: fresh_Pair) from IfThenElse.hyps(2)[OF this(1)] show ?case proof assume "atom x ♯ (Δ, Bool b)" with `atom x ♯ (e⇩1, e⇩2)` have "atom x ♯ (Δ, if b then e⇩1 else e⇩2)" by auto from IfThenElse.hyps(4)[OF this] show ?thesis. next assume "x ∈ domA Δ - set L" with reds_doesnt_forget[OF `Δ : (if b then e⇩1 else e⇩2) ⇓⇘L⇙ Θ : z`] show ?thesis by auto qed next case (Let Δ Γ L body Θ z) show ?case proof (cases "x ∈ domA Δ") case False hence "atom x ♯ Δ" using Let.prems by(auto simp add: fresh_Pair) show ?thesis apply(rule Let.hyps(3)) using Let.prems `atom x ♯ Δ` False by (auto simp add: fresh_Pair fresh_append) next case True hence "x ∉ set L" using Let(1) by (metis fresh_PairD(2) fresh_star_def image_eqI set_not_fresh) with True show ?thesis using reds_doesnt_forget[OF Let.hyps(2)] by auto qed qed lemma reds_fresh_fv: "⟦ Γ : e ⇓⇘L⇙ Δ : z; x ∈ fv (Δ, z) ∧ (x ∉ domA Δ ∨ x ∈ set L) ⟧ ⟹ x ∈ fv (Γ, e)" using reds_fresh unfolding fv_def fresh_def by blast lemma new_free_vars_on_heap: assumes "Γ : e ⇓⇘L⇙ Δ : z" shows "fv (Δ, z) - domA Δ ⊆ fv (Γ, e) - domA Γ" using reds_fresh_fv[OF assms(1)] reds_doesnt_forget[OF assms(1)] by auto lemma reds_pres_closed: assumes "Γ : e ⇓⇘L⇙ Δ : z" and "fv (Γ, e) ⊆ set L ∪ domA Γ" shows "fv (Δ, z) ⊆ set L ∪ domA Δ" using new_free_vars_on_heap[OF assms(1)] assms(2) by auto text {* Reducing the set of variables to avoid is always possible. *} lemma reds_smaller_L: "⟦ Γ : e ⇓⇘L⇙ Δ : z; set L' ⊆ set L ⟧ ⟹ Γ : e ⇓⇘L'⇙ Δ : z" proof(nominal_induct avoiding : L' rule: reds.strong_induct) case (Lambda Γ x e L L') show ?case by (rule reds.Lambda) next case (Application y Γ e xa L Δ Θ z e' L') from Application.hyps(10)[OF Application.prems] Application.hyps(12)[OF Application.prems] show ?case by (rule reds_ApplicationI) next case (Variable Γ xa e L Δ z L') have "set (xa # L') ⊆ set (xa # L)" using Variable.prems by auto thus ?case by (rule reds.Variable[OF Variable(1) Variable.hyps(3)]) next case (Bool b) show ?case.. next case (IfThenElse Γ scrut L Δ b e⇩1 e⇩2 Θ z L') thus ?case by (metis reds.IfThenElse) next case (Let Δ Γ L body Θ z L') have "atom ` domA Δ ♯* (Γ, L')" using Let(1-3) Let.prems by (auto simp add: fresh_star_Pair fresh_star_set_subset) thus ?case by (rule reds.Let[OF _ Let.hyps(4)[OF Let.prems]]) qed text {* Things are evaluated to a lambda expression, and the variable can be freely chose. *} lemma result_evaluated: "Γ : e ⇓⇘L⇙ Δ : z ⟹ isVal z" by (induct Γ e L Δ z rule:reds.induct) (auto dest: reds_doesnt_forget) lemma result_evaluated_fresh: assumes "Γ : e ⇓⇘L⇙ Δ : z" obtains y e' where "z = (Lam [y]. e')" and "atom y ♯ (c::'a::fs)" | b where "z = Bool b" proof- from assms have "isVal z" by (rule result_evaluated) hence "(∃ y e'. z = Lam [y]. e' ∧ atom y ♯ c) ∨ (∃ b. z = Bool b)" by (nominal_induct z avoiding: c rule:exp_strong_induct) auto thus thesis using that by blast qed end