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

subsubsection ‹Expressions›

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

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

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 ‹
  now work towards using @{type heap} instead of @{type assn}. All this
  be skipped if Nominal supported nested recursion.
 ›

text ‹
  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 ‹
  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 ‹
  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 ‹
  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 ‹
  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 ‹
  rules can be used instead of the original induction rules, which require a separate
  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: "\<And> \<pi> e'. \<pi> \<bullet> F e x e' = F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (\<pi> \<bullet> e')"
  assumes F_supp: "atom x \<sharp> 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)) \<subseteq> supp e \<union> supp x \<union> supp (Lam [x]. e)" by (rule supp_fun_app_eqvt3)    
  with F_supp[unfolded fresh_def]
  have *: "supp (F e x (Lam [x]. e)) \<subseteq> supp (Lam [x]. e)" by (auto simp add: exp_assn.supp supp_at_base)

  fix \<pi> :: perm
  assume "supp \<pi> \<sharp>* Lam [x]. e" with *
  have "supp \<pi> \<sharp>* F e x (Lam [x]. e)" by (auto simp add: fresh_star_def fresh_def)
  hence "F e x (Lam [x]. e) = \<pi> \<bullet> (F e x (Lam [x]. e))" by (metis perm_supp_eq)
  also have "\<dots> =  F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (\<pi> \<bullet> (Lam [x]. e))" by (simp add: F_eqvt)
  also have "\<pi> \<bullet> (Lam [x]. e) = (Lam [x]. e)" using `supp \<pi> \<sharp>* Lam [x]. e` by (metis perm_supp_eq)
  finally show "F (\<pi> \<bullet> e) (\<pi> \<bullet> 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 ‹
  program transformations might change the bound variables, possibly making it an empty list.
  smart constructor avoids the empty let in the resulting expression. Semantically, it should
  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 \<Rightarrow> var set" where
  "thunks [] = {}"
  | "thunks ((x,e)#\<Gamma>) = (if isLam e then {} else {x}) \<union> thunks \<Gamma>"
*)

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