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
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 *}
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