# Theory W

```theory W
imports "HOL-Nominal.Nominal"
begin

text ‹Example for strong induction rules avoiding sets of atoms.›

atom_decl tvar var

abbreviation
"difference_list" :: "'a list ⇒ 'a list ⇒ 'a list" ("_ - _" [60,60] 60)
where
"xs - ys ≡ [x ← xs. x∉set ys]"

lemma difference_eqvt_tvar[eqvt]:
fixes pi::"tvar prm"
and   Xs Ys::"tvar list"
shows "pi∙(Xs - Ys) = (pi∙Xs) - (pi∙Ys)"
by (induct Xs) (simp_all add: eqvts)

lemma difference_fresh:
fixes X::"tvar"
and   Xs Ys::"tvar list"
assumes a: "X∈set Ys"
shows "X♯(Xs - Ys)"
using a
by (induct Xs) (auto simp add: fresh_list_nil fresh_list_cons fresh_atm)

lemma difference_supset:
fixes xs::"'a list"
and   ys::"'a list"
and   zs::"'a list"
assumes asm: "set xs ⊆ set ys"
shows "xs - ys = []"
using asm
by (induct xs) (auto)

nominal_datatype ty =
TVar "tvar"
| Fun "ty" "ty" ("_→_" [100,100] 100)

nominal_datatype tyS =
Ty  "ty"
| ALL "«tvar»tyS" ("∀[_]._" [100,100] 100)

nominal_datatype trm =
Var "var"
| App "trm" "trm"
| Lam "«var»trm" ("Lam [_]._" [100,100] 100)
| Let "«var»trm" "trm"

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

type_synonym
Ctxt  = "(var×tyS) list"

text ‹free type variables›

consts ftv :: "'a ⇒ tvar list"

ftv_prod ≡ "ftv :: ('a × 'b) ⇒ tvar list"
ftv_tvar ≡ "ftv :: tvar ⇒ tvar list"
ftv_var  ≡ "ftv :: var ⇒ tvar list"
ftv_list ≡ "ftv :: 'a list ⇒ tvar list"
ftv_ty   ≡ "ftv :: ty ⇒ tvar list"
begin

primrec
ftv_prod
where
"ftv_prod (x, y) = (ftv x) @ (ftv y)"

definition
ftv_tvar :: "tvar ⇒ tvar list"
where
[simp]: "ftv_tvar X ≡ [(X::tvar)]"

definition
ftv_var :: "var ⇒ tvar list"
where
[simp]: "ftv_var x ≡ []"

primrec
ftv_list
where
"ftv_list [] = []"
| "ftv_list (x#xs) = (ftv x)@(ftv_list xs)"

nominal_primrec
ftv_ty :: "ty ⇒ tvar list"
where
"ftv_ty (TVar X) = [X]"
| "ftv_ty (T1 →T2) = (ftv_ty T1) @ (ftv_ty T2)"
by (rule TrueI)+

end

lemma ftv_ty_eqvt[eqvt]:
fixes pi::"tvar prm"
and   T::"ty"
shows "pi∙(ftv T) = ftv (pi∙T)"
by (nominal_induct T rule: ty.strong_induct)

ftv_tyS  ≡ "ftv :: tyS ⇒ tvar list"
begin

nominal_primrec
ftv_tyS :: "tyS ⇒ tvar list"
where
"ftv_tyS (Ty T)    = ((ftv (T::ty))::tvar list)"
| "ftv_tyS (∀[X].S) = (ftv_tyS S) - [X]"
apply(rule TrueI)+
apply(rule difference_fresh)
apply(simp)
done

end

lemma ftv_tyS_eqvt[eqvt]:
fixes pi::"tvar prm"
and   S::"tyS"
shows "pi∙(ftv S) = ftv (pi∙S)"
apply(nominal_induct S rule: tyS.strong_induct)
apply(simp only: ftv_tyS.simps)
apply(simp only: eqvts)
done

lemma ftv_Ctxt_eqvt[eqvt]:
fixes pi::"tvar prm"
and   Γ::"Ctxt"
shows "pi∙(ftv Γ) = ftv (pi∙Γ)"
by (induct Γ) (auto simp add: eqvts)

text ‹Valid›
inductive
valid :: "Ctxt ⇒ bool"
where
V_Nil[intro]:  "valid []"
| V_Cons[intro]: "⟦valid Γ;x♯Γ⟧⟹ valid ((x,S)#Γ)"

equivariance valid

text ‹General›
primrec gen :: "ty ⇒ tvar list ⇒ tyS" where
"gen T [] = Ty T"
| "gen T (X#Xs) = ∀[X].(gen T Xs)"

lemma gen_eqvt[eqvt]:
fixes pi::"tvar prm"
shows "pi∙(gen T Xs) = gen (pi∙T) (pi∙Xs)"
by (induct Xs) (simp_all add: eqvts)

abbreviation
close :: "Ctxt ⇒ ty ⇒ tyS"
where
"close Γ T ≡ gen T ((ftv T) - (ftv Γ))"

lemma close_eqvt[eqvt]:
fixes pi::"tvar prm"
shows "pi∙(close Γ T) = close (pi∙Γ) (pi∙T)"
by (simp_all only: eqvts)

text ‹Substitution›

type_synonym Subst = "(tvar×ty) list"

consts
psubst :: "Subst ⇒ 'a ⇒ 'a"       ("_<_>" [100,60] 120)

abbreviation
subst :: "'a ⇒ tvar ⇒ ty ⇒ 'a"  ("_[_::=_]" [100,100,100] 100)
where
"smth[X::=T] ≡ ([(X,T)])<smth>"

fun
lookup :: "Subst ⇒ tvar ⇒ ty"
where
"lookup [] X        = TVar X"
| "lookup ((Y,T)#θ) X = (if X=Y then T else lookup θ X)"

lemma lookup_eqvt[eqvt]:
fixes pi::"tvar prm"
shows "pi∙(lookup θ X) = lookup (pi∙θ) (pi∙X)"
by (induct θ) (auto simp add: eqvts)

lemma lookup_fresh:
fixes X::"tvar"
assumes a: "X♯θ"
shows "lookup θ X = TVar X"
using a
by (induct θ)
(auto simp add: fresh_list_cons fresh_prod fresh_atm)

psubst_ty ≡ "psubst :: Subst ⇒ ty ⇒ ty"
begin

nominal_primrec
psubst_ty
where
"θ<TVar X>   = lookup θ X"
| "θ<T⇩1 → T⇩2> = (θ<T⇩1>) → (θ<T⇩2>)"
by (rule TrueI)+

end

lemma psubst_ty_eqvt[eqvt]:
fixes pi::"tvar prm"
and   θ::"Subst"
and   T::"ty"
shows "pi∙(θ<T>) = (pi∙θ)<(pi∙T)>"
by (induct T rule: ty.induct) (simp_all add: eqvts)

psubst_tyS ≡ "psubst :: Subst ⇒ tyS ⇒ tyS"
begin

nominal_primrec
psubst_tyS :: "Subst ⇒ tyS ⇒ tyS"
where
"θ<(Ty T)> = Ty (θ<T>)"
| "X♯θ ⟹ θ<(∀[X].S)> = ∀[X].(θ<S>)"
apply(rule TrueI)+
done

end

psubst_Ctxt ≡ "psubst :: Subst ⇒ Ctxt ⇒ Ctxt"
begin

fun
psubst_Ctxt :: "Subst ⇒ Ctxt ⇒ Ctxt"
where
"psubst_Ctxt θ [] = []"
| "psubst_Ctxt θ ((x,S)#Γ) = (x,θ<S>)#(psubst_Ctxt θ Γ)"

end

lemma fresh_lookup:
fixes X::"tvar"
and   θ::"Subst"
and   Y::"tvar"
assumes asms: "X♯Y" "X♯θ"
shows "X♯(lookup θ Y)"
using asms
by (induct θ)
(auto simp add: fresh_list_cons fresh_prod fresh_atm)

lemma fresh_psubst_ty:
fixes X::"tvar"
and   θ::"Subst"
and   T::"ty"
assumes asms: "X♯θ" "X♯T"
shows "X♯θ<T>"
using asms
by (nominal_induct T rule: ty.strong_induct)
(auto simp add: fresh_list_append fresh_list_cons fresh_prod fresh_lookup)

lemma fresh_psubst_tyS:
fixes X::"tvar"
and   θ::"Subst"
and   S::"tyS"
assumes asms: "X♯θ" "X♯S"
shows "X♯θ<S>"
using asms
by (nominal_induct S avoiding: θ  X rule: tyS.strong_induct)

lemma fresh_psubst_Ctxt:
fixes X::"tvar"
and   θ::"Subst"
and   Γ::"Ctxt"
assumes asms: "X♯θ" "X♯Γ"
shows "X♯θ<Γ>"
using asms
by (induct Γ)

lemma subst_freshfact2_ty:
fixes   X::"tvar"
and     Y::"tvar"
and     T::"ty"
assumes asms: "X♯S"
shows "X♯T[X::=S]"
using asms
by (nominal_induct T rule: ty.strong_induct)

text ‹instance of a type scheme›
inductive
inst :: "ty ⇒ tyS ⇒ bool"("_ ≺ _" [50,51] 50)
where
I_Ty[intro]:  "T ≺ (Ty T)"
| I_All[intro]: "⟦X♯T'; T ≺ S⟧ ⟹ T[X::=T'] ≺ ∀[X].S"

equivariance inst[tvar]

nominal_inductive inst

lemma subst_forget_ty:
fixes T::"ty"
and   X::"tvar"
assumes a: "X♯T"
shows "T[X::=S] = T"
using a
by  (nominal_induct T rule: ty.strong_induct)

lemma psubst_ty_lemma:
fixes θ::"Subst"
and   X::"tvar"
and   T'::"ty"
and   T::"ty"
assumes a: "X♯θ"
shows "θ<T[X::=T']> = (θ<T>)[X::=θ<T'>]"
using a
apply(nominal_induct T avoiding: θ X T' rule: ty.strong_induct)
apply(rule sym)
apply(rule subst_forget_ty)
apply(rule fresh_lookup)
done

lemma general_preserved:
fixes θ::"Subst"
assumes a: "T ≺ S"
shows "θ<T> ≺ θ<S>"
using a
apply(nominal_induct T S avoiding: θ rule: inst.strong_induct)
apply(auto)[1]
apply(rule_tac I_All)
apply(simp)
done

text‹typing judgements›
inductive
typing :: "Ctxt ⇒ trm ⇒ ty ⇒ bool" (" _ ⊢ _ : _ " [60,60,60] 60)
where
T_VAR[intro]: "⟦valid Γ; (x,S)∈set Γ; T ≺ S⟧⟹ Γ ⊢ Var x : T"
| T_APP[intro]: "⟦Γ ⊢ t⇩1 : T⇩1→T⇩2; Γ ⊢ t⇩2 : T⇩1⟧⟹ Γ ⊢ App t⇩1 t⇩2 : T⇩2"
| T_LAM[intro]: "⟦x♯Γ;((x,Ty T⇩1)#Γ) ⊢ t : T⇩2⟧ ⟹ Γ ⊢ Lam [x].t : T⇩1→T⇩2"
| T_LET[intro]: "⟦x♯Γ; Γ ⊢ t⇩1 : T⇩1; ((x,close Γ T⇩1)#Γ) ⊢ t⇩2 : T⇩2; set (ftv T⇩1 - ftv Γ) ♯* T⇩2⟧
⟹ Γ ⊢ Let x be t⇩1 in t⇩2 : T⇩2"

equivariance typing[tvar]

lemma fresh_tvar_trm:
fixes X::"tvar"
and   t::"trm"
shows "X♯t"
by (nominal_induct t rule: trm.strong_induct)

lemma ftv_ty:
fixes T::"ty"
shows "supp T = set (ftv T)"
by (nominal_induct T rule: ty.strong_induct)

lemma ftv_tyS:
fixes S::"tyS"
shows "supp S = set (ftv S)"
by (nominal_induct S rule: tyS.strong_induct)
(auto simp add: tyS.supp abs_supp ftv_ty)

lemma ftv_Ctxt:
fixes Γ::"Ctxt"
shows "supp Γ = set (ftv Γ)"
apply (induct Γ)
apply (rename_tac a Γ')
apply (case_tac a)
apply (simp add: supp_prod supp_atm ftv_tyS)
done

lemma ftv_tvars:
fixes Tvs::"tvar list"
shows "supp Tvs = set Tvs"
by (induct Tvs)

lemma difference_supp:
fixes xs ys::"tvar list"
shows "((supp (xs - ys))::tvar set) = supp xs - supp ys"
by (induct xs)
(auto simp add: supp_list_nil supp_list_cons ftv_tvars)

lemma set_supp_eq:
fixes xs::"tvar list"
shows "set xs = supp xs"
by (induct xs)

nominal_inductive2 typing
avoids T_LET: "set (ftv T⇩1 - ftv Γ)"
apply (simp add: fresh_star_def fresh_def ftv_Ctxt)
apply assumption
apply simp
done

lemma perm_fresh_fresh_aux:
"∀(x,y)∈set (pi::tvar prm). x ♯ z ∧ y ♯ z ⟹ pi ∙ (z::'a::pt_tvar) = z"
apply (induct pi rule: rev_induct)
apply simp
apply (frule_tac x="(a, b)" in bspec)
apply simp
done

lemma freshs_mem:
fixes S::"tvar set"
assumes "x ∈ S"
and     "S ♯* z"
shows  "x ♯ z"
using assms by (simp add: fresh_star_def)

lemma fresh_gen_set:
fixes X::"tvar"
and   Xs::"tvar list"
assumes asm: "X∈set Xs"
shows "X♯gen T Xs"
using asm
apply(induct Xs)
apply(simp)
apply(rename_tac a Xs')
apply(case_tac "X=a")
done

lemma close_fresh:
fixes Γ::"Ctxt"
shows "∀(X::tvar)∈set ((ftv T) - (ftv Γ)). X♯(close Γ T)"

lemma gen_supp:
shows "(supp (gen T Xs)::tvar set) = supp T - supp Xs"
by (induct Xs)
(auto simp add: supp_list_nil supp_list_cons tyS.supp abs_supp supp_atm)

lemma minus_Int_eq:
shows "T - (T - U) = T ∩ U"
by blast

lemma close_supp:
shows "supp (close Γ T) = set (ftv T) ∩ set (ftv Γ)"
apply (simp add: gen_supp difference_supp ftv_ty ftv_Ctxt)
apply (simp only: set_supp_eq minus_Int_eq)
done

lemma better_T_LET:
assumes x: "x♯Γ"
and t1: "Γ ⊢ t⇩1 : T⇩1"
and t2: "((x,close Γ T⇩1)#Γ) ⊢ t⇩2 : T⇩2"
shows "Γ ⊢ Let x be t⇩1 in t⇩2 : T⇩2"
proof -
have fin: "finite (set (ftv T⇩1 - ftv Γ))" by simp
obtain pi where pi1: "(pi ∙ set (ftv T⇩1 - ftv Γ)) ♯* (T⇩2, Γ)"
and pi2: "set pi ⊆ set (ftv T⇩1 - ftv Γ) × (pi ∙ set (ftv T⇩1 - ftv Γ))"
by (rule at_set_avoiding [OF at_tvar_inst fin fs_tvar1, of "(T⇩2, Γ)"])
from pi1 have pi1': "(pi ∙ set (ftv T⇩1 - ftv Γ)) ♯* Γ"
have Gamma_fresh: "∀(x,y)∈set pi. x ♯ Γ ∧ y ♯ Γ"
apply (rule ballI)
apply (drule subsetD [OF pi2])
apply (erule SigmaE)
apply (drule freshs_mem [OF _ pi1'])
apply (simp add: ftv_Ctxt [symmetric] fresh_def)
done
have close_fresh': "∀(x, y)∈set pi. x ♯ close Γ T⇩1 ∧ y ♯ close Γ T⇩1"
apply (rule ballI)
apply (drule subsetD [OF pi2])
apply (erule SigmaE)
apply (drule bspec [OF close_fresh])
apply (drule freshs_mem [OF _ pi1'])
apply (simp add: fresh_def close_supp ftv_Ctxt)
done
note x
moreover from Gamma_fresh perm_boolI [OF t1, of pi]
have "Γ ⊢ t⇩1 : pi ∙ T⇩1"
by (simp add: perm_fresh_fresh_aux eqvts fresh_tvar_trm)
moreover from t2 close_fresh'
have "(x,(pi ∙ close Γ T⇩1))#Γ ⊢ t⇩2 : T⇩2"
with Gamma_fresh have "(x,close Γ (pi ∙ T⇩1))#Γ ⊢ t⇩2 : T⇩2"
moreover from pi1 Gamma_fresh
have "set (ftv (pi ∙ T⇩1) - ftv Γ) ♯* T⇩2"
by (simp only: eqvts fresh_star_prod perm_fresh_fresh_aux)
ultimately show ?thesis by (rule T_LET)
qed

lemma ftv_ty_subst:
fixes T::"ty"
and   θ::"Subst"
and   X Y ::"tvar"
assumes a1: "X ∈ set (ftv T)"
and     a2: "Y ∈ set (ftv (lookup θ X))"
shows "Y ∈ set (ftv (θ<T>))"
using a1 a2
by (nominal_induct T rule: ty.strong_induct) (auto)

lemma ftv_tyS_subst:
fixes S::"tyS"
and   θ::"Subst"
and   X Y::"tvar"
assumes a1: "X ∈ set (ftv S)"
and     a2: "Y ∈ set (ftv (lookup θ X))"
shows "Y ∈ set (ftv (θ<S>))"
using a1 a2
by (nominal_induct S avoiding: θ Y rule: tyS.strong_induct)

lemma ftv_Ctxt_subst:
fixes Γ::"Ctxt"
and   θ::"Subst"
assumes a1: "X ∈ set (ftv Γ)"
and     a2: "Y ∈ set (ftv (lookup θ X))"
shows "Y ∈ set (ftv (θ<Γ>))"
using a1 a2
by (induct Γ)

lemma gen_preserved1:
assumes asm: "Xs ♯* θ"
shows "θ<gen T Xs> = gen (θ<T>) Xs"
using asm
by (induct Xs)

lemma gen_preserved2:
fixes T::"ty"
and   Γ::"Ctxt"
assumes asm: "((ftv T) - (ftv Γ)) ♯* θ"
shows "((ftv (θ<T>)) - (ftv (θ<Γ>))) = ((ftv T) - (ftv Γ))"
using asm
apply(nominal_induct T rule: ty.strong_induct)
apply(fold fresh_def)
apply(rule fresh_psubst_Ctxt)
apply(assumption)
apply(assumption)
apply(rule difference_supset)
apply(auto)
done

lemma close_preserved:
fixes Γ::"Ctxt"
assumes asm: "((ftv T) - (ftv Γ)) ♯* θ"
shows "θ<close Γ T> = close (θ<Γ>) (θ<T>)"
using asm

lemma var_fresh_for_ty:
fixes x::"var"
and   T::"ty"
shows "x♯T"
by (nominal_induct T rule: ty.strong_induct)

lemma var_fresh_for_tyS:
fixes x::"var"
and   S::"tyS"
shows "x♯S"
by (nominal_induct S rule: tyS.strong_induct)

lemma psubst_fresh_Ctxt:
fixes x::"var"
and   Γ::"Ctxt"
and   θ::"Subst"
shows "x♯θ<Γ> = x♯Γ"
by (induct Γ)
(auto simp add: fresh_list_cons fresh_list_nil fresh_prod var_fresh_for_tyS)

lemma psubst_valid:
fixes θ::Subst
and   Γ::Ctxt
assumes a: "valid Γ"
shows "valid (θ<Γ>)"
using a
by (induct)

lemma psubst_in:
fixes Γ::"Ctxt"
and   θ::"Subst"
and   pi::"tvar prm"
and   S::"tyS"
assumes a: "(x,S)∈set Γ"
shows "(x,θ<S>)∈set (θ<Γ>)"
using a
by (induct Γ)

lemma typing_preserved:
fixes θ::"Subst"
and   pi::"tvar prm"
assumes a: "Γ ⊢ t : T"
shows "(θ<Γ>) ⊢ t : (θ<T>)"
using a
proof (nominal_induct Γ t T avoiding: θ rule: typing.strong_induct)
case (T_VAR Γ x S T)
have a1: "valid Γ" by fact
have a2: "(x, S) ∈ set Γ" by fact
have a3: "T ≺ S" by fact
have  "valid (θ<Γ>)" using a1 by (simp add: psubst_valid)
moreover
have  "(x,θ<S>)∈set (θ<Γ>)" using a2 by (simp add: psubst_in)
moreover
have "θ<T> ≺ θ<S>" using a3 by (simp add: general_preserved)
ultimately show "(θ<Γ>) ⊢ Var x : (θ<T>)" by (simp add: typing.T_VAR)
next
case (T_APP Γ t1 T1 T2 t2)
have "θ<Γ> ⊢ t1 : θ<T1 → T2>" by fact
then have "θ<Γ> ⊢ t1 : (θ<T1>) → (θ<T2>)" by simp
moreover
have "θ<Γ> ⊢ t2 : θ<T1>" by fact
ultimately show "θ<Γ> ⊢ App t1 t2 : θ<T2>" by (simp add: typing.T_APP)
next
case (T_LAM x Γ T1 t T2)
fix pi::"tvar prm" and θ::"Subst"
have "x♯Γ" by fact
then have "x♯θ<Γ>" by (simp add: psubst_fresh_Ctxt)
moreover
have "θ<((x, Ty T1)#Γ)> ⊢ t : θ<T2>" by fact
then have "((x, Ty (θ<T1>))#(θ<Γ>)) ⊢ t : θ<T2>" by (simp add: calc_atm)
ultimately show "θ<Γ> ⊢ Lam [x].t : θ<T1 → T2>" by (simp add: typing.T_LAM)
next
case (T_LET x Γ t1 T1 t2 T2)
have vc: "((ftv T1) - (ftv Γ)) ♯* θ" by fact
have "x♯Γ" by fact
then have a1: "x♯θ<Γ>" by (simp add: calc_atm psubst_fresh_Ctxt)
have a2: "θ<Γ> ⊢ t1 : θ<T1>" by fact
have a3: "θ<((x, close Γ T1)#Γ)> ⊢ t2 : θ<T2>" by fact
from a2 a3 show "θ<Γ> ⊢ Let x be t1 in t2 : θ<T2>"
apply -
apply(rule better_T_LET)
apply(rule a1)
apply(rule a2)