Theory Terms

theory Terms
  imports "Nominal-Utils" Vars  "AList-Utils-Nominal"
begin

subsubsection {* Expressions *}

text {*
This is the main data type of the development; our minimal lambda calculus with recursive let-bindings.
It is created using the nominal\_datatype command, which creates alpha-equivalence classes.

The package does not support nested recursion, so the bindings of the let cannot simply be of type
@{text "(var, exp) list"}. Instead, the definition of lists have to be inlined here, as the custom type
@{text "assn"}. Later we create conversion functions between these two types, define a properly typed @{text let} 
and redo the various lemmas in terms of that, so that afterwards, the type @{text "assn"} is no longer
referenced.
*}

nominal_datatype exp =
  Var var
| App exp var
| LetA as::assn body::exp binds "bn as" in body as
| Lam x::var body::exp binds x in body  ("Lam [_]. _" [100, 100] 100)
| Bool bool
| IfThenElse exp exp exp  ("((_)/ ? (_)/ : (_))" [0, 0, 10] 10)
and assn =
  ANil | ACons var exp assn
binder
  bn :: "assn ⇒ atom list"
where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"

notation (latex output) Terms.Var ("_")
notation (latex output) Terms.App ("_ _")
notation (latex output) Terms.Lam ("λ_. _"  [100, 100] 100)

type_synonym heap = "(var × exp) list"

lemma exp_assn_size_eqvt[eqvt]: "p ∙ (size :: exp ⇒ nat) = size"
  by (metis exp_assn.size_eqvt(1) fun_eqvtI permute_pure)

subsubsection {* Rewriting in terms of heaps *}

text {*
We now work towards using @{type heap} instead of @{type assn}. All this
could be skipped if Nominal supported nested recursion.
*}

text {*
Conversion from @{typ assn} to @{typ heap}.
*}

nominal_function asToHeap :: "assn ⇒ heap" 
 where ANilToHeap: "asToHeap ANil = []"
 | AConsToHeap: "asToHeap (ACons v e as) = (v, e) # asToHeap as"
unfolding eqvt_def asToHeap_graph_aux_def
apply rule
apply simp
apply rule
apply(case_tac x rule: exp_assn.exhaust(2))
apply auto
done
nominal_termination(eqvt) by lexicographic_order

lemma asToHeap_eqvt: "eqvt asToHeap"
  unfolding eqvt_def
  by (auto simp add: permute_fun_def asToHeap.eqvt)

text {* The other direction. *}

fun heapToAssn :: "heap ⇒ assn"
  where "heapToAssn [] = ANil" 
  | "heapToAssn ((v,e)#Γ) = ACons v e (heapToAssn Γ)"

declare heapToAssn.simps[simp del]

lemma heapToAssn_eqvt[simp,eqvt]: "p ∙ heapToAssn Γ =  heapToAssn (p ∙ Γ)"
  by (induct Γ rule: heapToAssn.induct)
     (auto simp add: heapToAssn.simps)

lemma bn_heapToAssn: "bn (heapToAssn Γ) = map (λx. atom (fst x)) Γ"
  by (induct rule: heapToAssn.induct)
     (auto simp add: heapToAssn.simps exp_assn.bn_defs)

lemma set_bn_to_atom_domA:
  "set (bn as) = atom ` domA (asToHeap as)"
   by (induct as rule: asToHeap.induct)
      (auto simp add: exp_assn.bn_defs)

text {*
They are inverse to each other.
*}

lemma heapToAssn_asToHeap[simp]:
  "heapToAssn (asToHeap as) = as"
  by (induct  rule: exp_assn.inducts(2)[of "λ _ . True"])
     (auto simp add: heapToAssn.simps)

lemma asToHeap_heapToAssn[simp]:
  "asToHeap (heapToAssn as) = as"
  by (induct rule: heapToAssn.induct)
     (auto simp add: heapToAssn.simps)

lemma heapToAssn_inject[simp]:
  "heapToAssn x = heapToAssn y ⟷ x = y"
  by (metis asToHeap_heapToAssn)

text {*
They are transparent to various notions from the Nominal package.
*}

lemma supp_heapToAssn: "supp (heapToAssn Γ) = supp Γ"
  by (induct rule: heapToAssn.induct)
     (simp_all add: heapToAssn.simps  exp_assn.supp supp_Nil supp_Cons supp_Pair sup_assoc)

lemma supp_asToHeap: "supp (asToHeap as) = supp as"
   by (induct as rule: asToHeap.induct)
      (simp_all add:  exp_assn.supp supp_Nil supp_Cons supp_Pair sup_assoc)

lemma fv_asToHeap: "fv (asToHeap Γ) = fv Γ"
  unfolding fv_def by (auto simp add: supp_asToHeap)

lemma fv_heapToAssn: "fv (heapToAssn Γ) = fv Γ"
  unfolding fv_def by (auto simp add: supp_heapToAssn)

lemma [simp]: "size (heapToAssn Γ) = size_list (λ (v,e) . size e) Γ"
  by (induct rule: heapToAssn.induct)
     (simp_all add: heapToAssn.simps)

lemma Lam_eq_same_var[simp]: "Lam [y]. e = Lam [y]. e' ⟷  e = e'"
  by auto (metis fresh_PairD(2) obtain_fresh)

text {* Now we define the Let constructor in the form that we actually want. *}

hide_const HOL.Let
definition Let :: "heap ⇒ exp ⇒ exp"
  where "Let Γ e = LetA (heapToAssn Γ) e"

notation (latex output) Let ("\textrm{\textsf{let}} _ \textrm{\textsf{in}} _")

abbreviation
  LetBe :: "var⇒exp⇒exp⇒exp" ("let _ be _ in _ " [100,100,100] 100)
where
  "let x be t1 in t2 ≡ Let [(x,t1)] t2"

text {*
We rewrite all (relevant) lemmas about @{term LetA} in terms of @{term Let}.
*}

lemma size_Let[simp]: "size (Let Γ e) = size_list (λp. size (snd p)) Γ + size e + Suc 0"
  unfolding Let_def by (auto simp add: split_beta')

lemma Let_distinct[simp]:
  "Var v ≠ Let Γ e"
  "Let Γ e ≠ Var v"
  "App e v ≠ Let Γ e'"
  "Lam [v]. e' ≠ Let Γ e"
  "Let Γ e ≠ Lam [v]. e'"
  "Let Γ e' ≠ App e v"
  "Bool b ≠ Let Γ e"
  "Let Γ e ≠ Bool b"
  "(scrut ? e1 : e2) ≠ Let Γ e"
  "Let Γ e ≠ (scrut ? e1 : e2)"
  unfolding Let_def by simp_all

lemma Let_perm_simps[simp,eqvt]:
  "p ∙ Let Γ e = Let (p ∙ Γ) (p ∙ e)"
  unfolding Let_def by simp

lemma Let_supp:
  "supp (Let Γ e) = (supp e ∪ supp Γ) - atom ` (domA Γ)"
  unfolding Let_def by (simp add: exp_assn.supp supp_heapToAssn bn_heapToAssn domA_def image_image)

lemma Let_fresh[simp]:
  "a ♯ Let Γ e = (a ♯ e ∧ a ♯ Γ ∨ a ∈ atom ` domA Γ)"
  unfolding fresh_def by (auto simp add: Let_supp)

lemma Abs_eq_cong:
  assumes "⋀ p. (p ∙ x = x') ⟷ (p ∙ y = y')"
  assumes "supp y = supp x"
  assumes "supp y' = supp x'"
  shows "([a]lst. x = [a']lst. x') ⟷ ([a]lst. y = [a']lst. y')"
  by (simp add: Abs_eq_iff alpha_lst assms)

lemma Let_eq_iff[simp]:
  "(Let Γ e = Let Γ' e') = ([map (λx. atom (fst x)) Γ ]lst. (e, Γ) = [map (λx. atom (fst x)) Γ']lst. (e',Γ'))"
  unfolding Let_def 
  apply (simp add: bn_heapToAssn)
  apply (rule Abs_eq_cong)
  apply (simp_all add: supp_Pair supp_heapToAssn)
  done

lemma exp_strong_exhaust:
  fixes c :: "'a :: fs"
  assumes "⋀var. y = Var var ⟹ P"
  assumes "⋀exp var. y = App exp var ⟹ P"
  assumes "⋀Γ exp. atom ` domA Γ ♯* c ⟹ y = Let Γ exp ⟹ P"
  assumes "⋀var exp. {atom var} ♯* c ⟹ y = Lam [var]. exp ⟹ P"
  assumes "⋀ b. (y = Bool b) ⟹ P"
  assumes "⋀ scrut e1 e2. y = (scrut ? e1 : e2) ⟹ P"
  shows P
  apply (rule  exp_assn.strong_exhaust(1)[where y = y and c = c])
  apply (metis assms(1))
  apply (metis assms(2))
  apply (metis assms(3) set_bn_to_atom_domA Let_def heapToAssn_asToHeap)
  apply (metis assms(4))
  apply (metis assms(5))
  apply (metis assms(6))
  done

text {*
And finally the induction rules with @{term Let}.
*}

lemma exp_heap_induct[case_names Var App Let Lam Bool IfThenElse Nil Cons]:
  assumes "⋀b var. P1 (Var var)"
  assumes "⋀exp var. P1 exp ⟹ P1 (App exp var)"
  assumes "⋀Γ exp. P2 Γ ⟹ P1 exp ⟹ P1 (Let Γ exp)"
  assumes "⋀var exp. P1 exp ⟹ P1 (Lam [var]. exp)"
  assumes "⋀ b. P1 (Bool b)"
  assumes "⋀ scrut e1 e2. P1 scrut ⟹ P1 e1 ⟹ P1 e2 ⟹ P1 (scrut ? e1 : e2)"
  assumes "P2 []"
  assumes "⋀var exp Γ. P1 exp ⟹ P2 Γ ⟹ P2 ((var, exp)#Γ)"
  shows "P1 e" and "P2 Γ"
proof-
  have "P1 e" and "P2 (asToHeap (heapToAssn Γ))"
    apply (induct rule: exp_assn.inducts[of P1 "λ assn. P2 (asToHeap assn)"])
    apply (metis assms(1))
    apply (metis assms(2))
    apply (metis assms(3) Let_def heapToAssn_asToHeap )
    apply (metis assms(4))
    apply (metis assms(5))
    apply (metis assms(6))
    apply (metis assms(7) asToHeap.simps(1))
    apply (metis assms(8) asToHeap.simps(2))
    done
  thus "P1 e" and "P2 Γ" unfolding asToHeap_heapToAssn.
qed

lemma exp_heap_strong_induct[case_names Var App Let Lam Bool IfThenElse Nil Cons]:
  assumes "⋀var c. P1 c (Var var)"
  assumes "⋀exp var c. (⋀c. P1 c exp) ⟹ P1 c (App exp var)"
  assumes "⋀Γ exp c. atom ` domA Γ ♯* c ⟹ (⋀c. P2 c Γ) ⟹ (⋀c. P1 c exp) ⟹ P1 c (Let Γ exp)"
  assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P1 c exp) ⟹ P1 c (Lam [var]. exp)"
  assumes "⋀ b c. P1 c (Bool b)"
  assumes "⋀ scrut e1 e2 c. (⋀ c. P1 c scrut) ⟹ (⋀ c. P1 c e1) ⟹ (⋀ c. P1 c e2) ⟹ P1 c (scrut ? e1 : e2)"
  assumes "⋀c. P2 c []"
  assumes "⋀var exp Γ c. (⋀c. P1 c exp) ⟹ (⋀c. P2 c Γ) ⟹ P2 c ((var,exp)#Γ)"
  fixes c :: "'a :: fs"
  shows "P1 c e" and "P2 c Γ"
proof-
  have "P1 c e" and "P2 c (asToHeap (heapToAssn Γ))"
    apply (induct rule: exp_assn.strong_induct[of P1 "λ c assn. P2 c (asToHeap assn)"])
    apply (metis assms(1))
    apply (metis assms(2))
    apply (metis assms(3) set_bn_to_atom_domA Let_def heapToAssn_asToHeap )
    apply (metis assms(4))
    apply (metis assms(5))
    apply (metis assms(6))
    apply (metis assms(7) asToHeap.simps(1))
    apply (metis assms(8) asToHeap.simps(2))
    done
  thus "P1 c e" and "P2 c Γ" unfolding asToHeap_heapToAssn.
qed

subsubsection {* Nice induction rules *}

text {*
These rules can be used instead of the original induction rules, which require a separate
goal for @{typ assn}.
*}

lemma exp_induct[case_names Var App Let Lam Bool IfThenElse]:
  assumes "⋀var. P (Var var)"
  assumes "⋀exp var. P exp ⟹ P (App exp var)"
  assumes "⋀Γ exp. (⋀ x. x ∈ domA Γ ⟹  P (the (map_of Γ x))) ⟹ P exp ⟹ P (Let Γ exp)"
  assumes "⋀var exp.  P exp ⟹ P (Lam [var]. exp)"
  assumes "⋀ b. P (Bool b)"
  assumes "⋀ scrut e1 e2. P scrut ⟹ P e1 ⟹ P e2 ⟹ P (scrut ? e1 : e2)"
  shows "P exp"
  apply (rule exp_heap_induct[of P "λ Γ. (∀x ∈ domA Γ. P (the (map_of Γ x)))"])
  apply (metis assms(1))
  apply (metis assms(2))
  apply (metis assms(3))
  apply (metis assms(4))
  apply (metis assms(5))
  apply (metis assms(6))
  apply auto
  done

lemma  exp_strong_induct_set[case_names Var App Let Lam Bool IfThenElse]:
  assumes "⋀var c. P c (Var var)"
  assumes "⋀exp var c. (⋀c. P c exp) ⟹ P c (App exp var)"
  assumes "⋀Γ exp c.
    atom ` domA Γ ♯* c ⟹ (⋀c x e. (x,e) ∈ set Γ ⟹  P c e) ⟹ (⋀c. P c exp) ⟹ P c (Let Γ exp)"
  assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P c exp) ⟹ P c (Lam [var]. exp)"
  assumes "⋀b c. P c (Bool b)"
  assumes "⋀scrut e1 e2 c. (⋀ c. P c scrut) ⟹ (⋀ c. P c e1) ⟹ (⋀ c. P c e2) ⟹ P c (scrut ? e1 : e2)"
  shows "P (c::'a::fs) exp"
  apply (rule exp_heap_strong_induct(1)[of P "λ c Γ. (∀(x,e) ∈ set Γ. P c e)"])
  apply (metis assms(1))
  apply (metis assms(2))
  apply (metis assms(3) split_conv)
  apply (metis assms(4))
  apply (metis assms(5))
  apply (metis assms(6))
  apply auto
  done


lemma  exp_strong_induct[case_names Var App Let Lam Bool IfThenElse]:
  assumes "⋀var c. P c (Var var)"
  assumes "⋀exp var c. (⋀c. P c exp) ⟹ P c (App exp var)"
  assumes "⋀Γ exp c.
    atom ` domA Γ ♯* c ⟹ (⋀c x. x ∈ domA Γ ⟹  P c (the (map_of Γ x))) ⟹ (⋀c. P c exp) ⟹ P c (Let Γ exp)"
  assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P c exp) ⟹ P c (Lam [var]. exp)"
  assumes "⋀b c. P c (Bool b)"
  assumes "⋀ scrut e1 e2 c. (⋀ c. P c scrut) ⟹ (⋀ c. P c e1) ⟹ (⋀ c. P c e2) ⟹ P c (scrut ? e1 : e2)"
  shows "P (c::'a::fs) exp"
  apply (rule exp_heap_strong_induct(1)[of P "λ c Γ. (∀x ∈ domA Γ. P c (the (map_of Γ x)))"])
  apply (metis assms(1))
  apply (metis assms(2))
  apply (metis assms(3))
  apply (metis assms(4))
  apply (metis assms(5))
  apply (metis assms(6))
  apply auto
  done

subsubsection {* Testing alpha equivalence *}
              
lemma alpha_test:
  shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
  by (simp add: Abs1_eq_iff fresh_at_base pure_fresh)

lemma alpha_test2:
  shows "let x be (Var x) in (Var x) = let y be (Var y) in (Var y)"
  by (simp add: fresh_Cons fresh_Nil Abs1_eq_iff fresh_Pair add: fresh_at_base pure_fresh)

lemma alpha_test3:
  shows "
    Let [(x, Var y), (y, Var x)] (Var x)
    =
    Let [(y, Var x), (x, Var y)] (Var y)" (is "Let ?la ?lb = _")
  by (simp add: bn_heapToAssn Abs1_eq_iff fresh_Pair fresh_at_base
                Abs_swap2[of "atom x" "(?lb, [(x, Var y), (y, Var x)])" "[atom x, atom y]" "atom y"])

subsubsection {* Free variables *}

lemma fv_supp_exp: "supp e = atom ` (fv (e::exp) :: var set)" and fv_supp_as: "supp as = atom ` (fv (as::assn) :: var set)"
  by (induction e and as rule:exp_assn.inducts)
     (auto simp add: fv_def exp_assn.supp supp_at_base pure_supp)

lemma fv_supp_heap: "supp (Γ::heap) = atom ` (fv Γ :: var set)"
  by (metis fv_def fv_supp_as supp_heapToAssn)

lemma fv_Lam[simp]: "fv (Lam [x]. e) = fv e - {x}"
  unfolding fv_def by (auto simp add: exp_assn.supp)
lemma fv_Var[simp]: "fv (Var x) = {x}"
  unfolding fv_def by (auto simp add: exp_assn.supp supp_at_base pure_supp)
lemma fv_App[simp]: "fv (App e x) = insert x (fv e)"
  unfolding fv_def by (auto simp add: exp_assn.supp supp_at_base)
lemma fv_Let[simp]: "fv (Let Γ e) = (fv Γ ∪ fv e) - domA Γ"
  unfolding fv_def by (auto simp add: Let_supp exp_assn.supp supp_at_base set_bn_to_atom_domA)
lemma fv_Bool[simp]: "fv (Bool b) = {}"
  unfolding fv_def by (auto simp add: exp_assn.supp pure_supp)
lemma fv_IfThenElse[simp]: "fv (scrut ? e1 : e2)  = fv scrut ∪ fv e1 ∪ fv e2"
  unfolding fv_def by (auto simp add: exp_assn.supp)


lemma fv_delete_heap:
  assumes "map_of Γ x = Some e"
  shows "fv (delete x Γ, e) ∪ {x} ⊆ (fv (Γ, Var x) :: var set)"
proof-
  have "fv (delete x Γ) ⊆ fv Γ" by (metis fv_delete_subset)
  moreover
  have "(x,e) ∈ set Γ" by (metis assms map_of_SomeD)
  hence "fv e ⊆ fv Γ" by (metis assms domA_from_set map_of_fv_subset option.sel)
  moreover
  have "x ∈ fv (Var x)" by simp
  ultimately show ?thesis by auto
qed

subsubsection {* Lemmas helping with nominal definitions *}

lemma eqvt_lam_case:
  assumes "Lam [x]. e = Lam [x']. e'"
  assumes "⋀ π . supp (-π) ♯* (fv (Lam [x]. e) :: var set) ⟹
                 supp π ♯* (Lam [x]. e) ⟹
        F (π ∙ e) (π ∙ x) (Lam [x]. e) = F e x (Lam [x]. e)"
  shows "F e x (Lam [x]. e) = F e' x' (Lam [x']. e')"
proof-

  from assms(1)
  have "[[atom x]]lst. (e, x) = [[atom x']]lst. (e', x')" by auto
  then obtain p
    where "(supp (e, x) - {atom x}) ♯* p"
    and [simp]: "p ∙ x = x'"
    and [simp]: "p ∙ e = e'"
    unfolding  Abs_eq_iff(3) alpha_lst.simps by auto

  from `_ ♯* p`
  have *: "supp (-p) ♯* (fv (Lam [x]. e) :: var set)"
    by (auto simp add: fresh_star_def fresh_def supp_finite_set_at_base supp_Pair fv_supp_exp fv_supp_heap supp_minus_perm)

  from `_ ♯* p`
  have **: "supp p ♯* Lam [x]. e"
    by (auto simp add: fresh_star_def fresh_def supp_Pair fv_supp_exp)

  have "F e x (Lam [x]. e) =  F (p ∙ e) (p ∙ x) (Lam [x]. e)" by (rule assms(2)[OF * **, symmetric])
  also have "… = F e' x' (Lam [x']. e')" by (simp add: assms(1))
  finally show ?thesis.
qed

(* Nice idea, but doesn't work well with extra arguments to the function

lemma eqvt_lam_case_eqvt:
  assumes "Lam [x]. e = Lam [x']. e'"
  assumes F_eqvt: "⋀ π e'. π ∙ F e x e' = F (π ∙ e) (π ∙ x) (π ∙ e')"
  assumes F_supp: "atom x ♯ F e x (Lam [x]. e)"
  shows "F e x (Lam [x]. e) = F e' x' (Lam [x']. e')"
using assms(1)
proof(rule eqvt_lam_case)
  have "eqvt F" unfolding eqvt_def by (rule, perm_simp, rule) so rry
  hence "supp (F e x (Lam [x]. e)) ⊆ supp e ∪ supp x ∪ supp (Lam [x]. e)" by (rule supp_fun_app_eqvt3)    
  with F_supp[unfolded fresh_def]
  have *: "supp (F e x (Lam [x]. e)) ⊆ supp (Lam [x]. e)" by (auto simp add: exp_assn.supp supp_at_base)

  fix π :: perm
  assume "supp π ♯* Lam [x]. e" with *
  have "supp π ♯* F e x (Lam [x]. e)" by (auto simp add: fresh_star_def fresh_def)
  hence "F e x (Lam [x]. e) = π ∙ (F e x (Lam [x]. e))" by (metis perm_supp_eq)
  also have "… =  F (π ∙ e) (π ∙ x) (π ∙ (Lam [x]. e))" by (simp add: F_eqvt)
  also have "π ∙ (Lam [x]. e) = (Lam [x]. e)" using `supp π ♯* Lam [x]. e` by (metis perm_supp_eq)
  finally show "F (π ∙ e) (π ∙ x) (Lam [x]. e) = F e x (Lam [x]. e)"..
qed
*)

lemma eqvt_let_case:
  assumes "Let as body = Let as' body'"
  assumes "⋀ π .
    supp (-π) ♯* (fv (Let as body) :: var set) ⟹
    supp π ♯* Let as body ⟹
    F (π ∙ as) (π ∙ body) (Let as body) = F as body (Let as body)"
  shows "F as body (Let as body) = F as' body' (Let as' body')"
proof-
  from assms(1)
  have "[map (λ p. atom (fst p)) as]lst. (body, as) = [map (λ p. atom (fst p)) as']lst. (body', as')" by auto
  then obtain p
    where "(supp (body, as) - atom ` domA as) ♯* p"
    and [simp]: "p ∙ body = body'"
    and [simp]: "p ∙ as = as'"
    unfolding  Abs_eq_iff(3) alpha_lst.simps by (auto simp add: domA_def image_image)

  from `_ ♯* p`
  have *: "supp (-p) ♯* (fv (Terms.Let as body) :: var set)"
    by (auto simp add: fresh_star_def fresh_def supp_finite_set_at_base supp_Pair fv_supp_exp fv_supp_heap supp_minus_perm)

  from `_ ♯* p`
  have **: "supp p ♯* Terms.Let as body"
    by (auto simp add: fresh_star_def fresh_def supp_Pair fv_supp_exp fv_supp_heap )

  have "F as body (Let as body) =  F (p ∙ as) (p ∙ body) (Let as body)" by (rule assms(2)[OF * **, symmetric])
  also have "… = F as' body' (Let as' body')" by (simp add: assms(1))
  finally show ?thesis.
qed

subsubsection {* A smart constructor for lets *}

text {*
Certian program transformations might change the bound variables, possibly making it an empty list.
This smart constructor avoids the empty let in the resulting expression. Semantically, it should
not make a difference. 
*}

definition SmartLet :: "heap => exp => exp"
  where "SmartLet Γ e = (if Γ = [] then e else Let Γ e)"

lemma SmartLet_eqvt[eqvt]: "π ∙ (SmartLet Γ e) = SmartLet (π ∙ Γ) (π ∙ e)"
  unfolding SmartLet_def by perm_simp rule

lemma SmartLet_supp:
  "supp (SmartLet Γ e) = (supp e ∪ supp Γ) - atom ` (domA Γ)"
  unfolding SmartLet_def using Let_supp by (auto simp add: supp_Nil)

lemma fv_SmartLet[simp]: "fv (SmartLet Γ e) = (fv Γ ∪ fv e) - domA Γ"
  unfolding SmartLet_def by auto

subsubsection {* A predicate for value expressions *}

nominal_function isLam :: "exp ⇒ bool" where
  "isLam (Var x) = False" |
  "isLam (Lam [x]. e) = True" |
  "isLam (App e x) = False" |
  "isLam (Let as e) = False" |
  "isLam (Bool b) = False" |
  "isLam (scrut ? e1 : e2) = False"
  unfolding isLam_graph_aux_def eqvt_def
  apply simp
  apply simp
  apply (metis exp_strong_exhaust)
  apply auto
  done
nominal_termination (eqvt) by lexicographic_order

lemma isLam_Lam: "isLam (Lam [x]. e)" by simp

lemma isLam_obtain_fresh:
  assumes "isLam z"
  obtains y e'
  where "z = (Lam [y]. e')" and "atom y ♯ (c::'a::fs)"
using assms by (nominal_induct z avoiding: c rule:exp_strong_induct) auto

nominal_function isVal :: "exp ⇒ bool" where
  "isVal (Var x) = False" |
  "isVal (Lam [x]. e) = True" |
  "isVal (App e x) = False" |
  "isVal (Let as e) = False" |
  "isVal (Bool b) = True" |
  "isVal (scrut ? e1 : e2) = False"
  unfolding isVal_graph_aux_def eqvt_def
  apply simp
  apply simp
  apply (metis exp_strong_exhaust)
  apply auto
  done
nominal_termination (eqvt) by lexicographic_order

lemma isVal_Lam: "isVal (Lam [x]. e)" by simp
lemma isVal_Bool: "isVal (Bool b)" by simp


subsubsection {* The notion of thunks *}
(*
fun thunks :: "heap ⇒ var set" where
  "thunks [] = {}"
  | "thunks ((x,e)#Γ) = (if isLam e then {} else {x}) ∪ thunks Γ"
*)

definition thunks :: "heap ⇒ var set" where
  "thunks Γ = {x . case map_of Γ x of Some e ⇒ ¬ isVal e | None ⇒ False}"

lemma thunks_Nil[simp]: "thunks [] = {}" by (auto simp add: thunks_def)

lemma thunks_domA: "thunks Γ ⊆ domA Γ"
  by (induction Γ ) (auto simp add: thunks_def)

lemma thunks_Cons: "thunks ((x,e)#Γ) = (if isVal e then thunks Γ - {x} else insert x (thunks Γ))"
  by (auto simp add: thunks_def )

lemma thunks_append[simp]: "thunks (Δ@Γ) = thunks Δ ∪ (thunks Γ - domA Δ)"
  by (induction Δ) (auto simp add: thunks_def )

lemma thunks_delete[simp]: "thunks (delete x Γ) = thunks Γ - {x}"
  by (induction Γ) (auto simp add: thunks_def )

lemma thunksI[intro]: "map_of Γ x = Some e ⟹ ¬ isVal e ⟹ x ∈ thunks Γ"
  by (induction Γ) (auto simp add: thunks_def )

lemma thunksE[intro]: "x ∈ thunks Γ ⟹ map_of Γ x = Some e ⟹ ¬ isVal e"
  by (induction Γ) (auto simp add: thunks_def )

lemma thunks_cong: "map_of Γ = map_of Δ ⟹ thunks Γ = thunks Δ"
  by (simp add: thunks_def)

lemma thunks_eqvt[eqvt]:
  "π ∙ thunks Γ = thunks (π ∙ Γ)"
    unfolding thunks_def
    by perm_simp rule

subsubsection {* Non-recursive Let bindings *}

definition nonrec :: "heap ⇒ bool" where
  "nonrec Γ = (∃ x e. Γ = [(x,e)] ∧ x ∉ fv e)"


lemma nonrecE:
  assumes "nonrec Γ"
  obtains x e where "Γ = [(x,e)]" and "x ∉ fv e"
  using assms
  unfolding nonrec_def
  by blast

lemma nonrec_eqvt[eqvt]:
  "nonrec Γ ⟹ nonrec (π ∙ Γ)"
  apply (erule nonrecE)
  apply (auto simp add: nonrec_def fv_def fresh_def )
  apply (metis fresh_at_base_permute_iff fresh_def)
  done

lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam Bool IfThenElse]:
  assumes "⋀var. P (Var var)"
  assumes "⋀exp var. P exp ⟹ P (App exp var)"
  assumes "⋀Γ exp. ¬ nonrec Γ ⟹ (⋀ x. x ∈ domA Γ ⟹  P (the (map_of Γ x))) ⟹ P exp ⟹ P (Let Γ exp)"
  assumes "⋀x e exp. x ∉ fv e ⟹ P e ⟹ P exp ⟹ P (let x be e in exp)"
  assumes "⋀var exp.  P exp ⟹ P (Lam [var]. exp)"
  assumes "⋀b. P (Bool b)"
  assumes "⋀ scrut e1 e2. P scrut ⟹ P e1 ⟹ P e2 ⟹ P (scrut ? e1 : e2)"
  shows "P exp"
  apply (rule exp_induct[of P])
  apply (metis assms(1))
  apply (metis assms(2))
  apply (case_tac "nonrec Γ")
  apply (erule nonrecE)
  apply simp
  apply (metis assms(4))
  apply (metis assms(3))
  apply (metis assms(5))
  apply (metis assms(6))
  apply (metis assms(7))
  done

lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam Bool IfThenElse]:
  assumes "⋀var c. P c (Var var)"
  assumes "⋀exp var c. (⋀c. P c exp) ⟹ P c (App exp var)"
  assumes "⋀Γ exp c.
    atom ` domA Γ ♯* c ⟹ ¬ nonrec Γ ⟹ (⋀c x. x ∈ domA Γ ⟹  P c (the (map_of Γ x))) ⟹ (⋀c. P c exp) ⟹ P c (Let Γ exp)"
  assumes "⋀x e exp c. {atom x} ♯* c ⟹ x ∉ fv e ⟹ (⋀ c. P c e) ⟹ (⋀ c. P c exp) ⟹ P c (let x be e in exp)"
  assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P c exp) ⟹ P c (Lam [var]. exp)"
  assumes "⋀b c. P c (Bool b)"
  assumes "⋀ scrut e1 e2 c. (⋀ c. P c scrut) ⟹ (⋀ c. P c e1) ⟹ (⋀ c. P c e2) ⟹ P c (scrut ? e1 : e2)"
  shows "P (c::'a::fs) exp"
  apply (rule exp_strong_induct[of P])
  apply (metis assms(1))
  apply (metis assms(2))
  apply (case_tac "nonrec Γ")
  apply (erule nonrecE)
  apply simp
  apply (metis assms(4))
  apply (metis assms(3))
  apply (metis assms(5))
  apply (metis assms(6))
  apply (metis assms(7))
  done

lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam Bool IfThenElse]:
  assumes "⋀var c. P c (Var var)"
  assumes "⋀exp var c. (⋀c. P c exp) ⟹ P c (App exp var)"
  assumes "⋀Γ exp c.
    atom ` domA Γ ♯* c ⟹ ¬ nonrec Γ ⟹ (⋀c x e. (x,e) ∈ set Γ ⟹  P c e) ⟹ (⋀c. P c exp) ⟹ P c (Let Γ exp)"
  assumes "⋀x e exp c. {atom x} ♯* c ⟹ x ∉ fv e ⟹ (⋀ c. P c e) ⟹ (⋀ c. P c exp) ⟹ P c (let x be e in exp)"
  assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P c exp) ⟹ P c (Lam [var]. exp)"
  assumes "⋀b c. P c (Bool b)"
  assumes "⋀ scrut e1 e2 c. (⋀ c. P c scrut) ⟹ (⋀ c. P c e1) ⟹ (⋀ c. P c e2) ⟹ P c (scrut ? e1 : e2)"
  shows "P (c::'a::fs) exp"
  apply (rule exp_strong_induct_set(1)[of P])
  apply (metis assms(1))
  apply (metis assms(2))
  apply (case_tac "nonrec Γ")
  apply (erule nonrecE)
  apply simp
  apply (metis assms(4))
  apply (metis assms(3))
  apply (metis assms(5))
  apply (metis assms(6))
  apply (metis assms(7))
  done



subsubsection {* Renaming a lambda-bound variable *}

lemma change_Lam_Variable:
  assumes "y' ≠ y ⟹ atom y' ♯ (e,  y)"
  shows   "Lam [y]. e =  Lam [y']. ((y ↔ y') ∙ e)"
proof(cases "y' = y")
  case True thus ?thesis by simp
next
  case False
  from assms[OF this]
  have "(y ↔ y') ∙ (Lam [y]. e) = Lam [y]. e"
    by -(rule flip_fresh_fresh, (simp add: fresh_Pair)+)
  moreover
  have "(y ↔ y') ∙ (Lam [y]. e) = Lam [y']. ((y ↔ y') ∙ e)"
    by simp
  ultimately
  show "Lam [y]. e =  Lam [y']. ((y ↔ y') ∙ e)" by (simp add: fresh_Pair)
qed


end