theory W
imports "HOL-Nominal.Nominal"
begin
text \<open>Example for strong induction rules avoiding sets of atoms.\<close>
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 \<open>free type variables\<close>
consts ftv :: "'a \ tvar list"
overloading
ftv_prod \<equiv> "ftv :: ('a \<times> 'b) \<Rightarrow> tvar list"
ftv_tvar \<equiv> "ftv :: tvar \<Rightarrow> tvar list"
ftv_var \<equiv> "ftv :: var \<Rightarrow> tvar list"
ftv_list \<equiv> "ftv :: 'a list \<Rightarrow> tvar list"
ftv_ty \<equiv> "ftv :: ty \<Rightarrow> 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)
(perm_simp add: append_eqvt)+
overloading
ftv_tyS \<equiv> "ftv :: tyS \<Rightarrow> 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(finite_guess add: ftv_ty_eqvt fs_tvar1)+
apply(rule TrueI)+
apply(rule difference_fresh)
apply(simp)
apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+
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 add: eqvts)
apply(simp only: ftv_tyS.simps)
apply(simp only: eqvts)
apply(simp add: eqvts)
done
lemma ftv_Ctxt_eqvt[eqvt]:
fixes pi::"tvar prm"
and \<Gamma>::"Ctxt"
shows "pi\(ftv \) = ftv (pi\\)"
by (induct \<Gamma>) (auto simp add: eqvts)
text \<open>Valid\<close>
inductive
valid :: "Ctxt \ bool"
where
V_Nil[intro]: "valid []"
| V_Cons[intro]: "\valid \;x\\\\ valid ((x,S)#\)"
equivariance valid
text \<open>General\<close>
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 \<open>Substitution\<close>
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)])"
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 \<theta>) (auto simp add: eqvts)
lemma lookup_fresh:
fixes X::"tvar"
assumes a: "X\\"
shows "lookup \ X = TVar X"
using a
by (induct \<theta>)
(auto simp add: fresh_list_cons fresh_prod fresh_atm)
overloading
psubst_ty \<equiv> "psubst :: Subst \<Rightarrow> ty \<Rightarrow> ty"
begin
nominal_primrec
psubst_ty
where
"\ = lookup \ X"
| "\1 \ T\<^sub>2> = (\1>) \ (\2>)"
by (rule TrueI)+
end
lemma psubst_ty_eqvt[eqvt]:
fixes pi::"tvar prm"
and \<theta>::"Subst"
and T::"ty"
shows "pi\(\) = (pi\\)<(pi\T)>"
by (induct T rule: ty.induct) (simp_all add: eqvts)
overloading
psubst_tyS \<equiv> "psubst :: Subst \<Rightarrow> tyS \<Rightarrow> tyS"
begin
nominal_primrec
psubst_tyS :: "Subst \ tyS \ tyS"
where
"\<(Ty T)> = Ty (\)"
| "X\\ \ \<(\[X].S)> = \[X].(\)"
apply(finite_guess add: psubst_ty_eqvt fs_tvar1)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(fresh_guess add: psubst_ty_eqvt fs_tvar1)+
done
end
overloading
psubst_Ctxt \<equiv> "psubst :: Subst \<Rightarrow> Ctxt \<Rightarrow> Ctxt"
begin
fun
psubst_Ctxt :: "Subst \ Ctxt \ Ctxt"
where
"psubst_Ctxt \ [] = []"
| "psubst_Ctxt \ ((x,S)#\) = (x,\)#(psubst_Ctxt \ \)"
end
lemma fresh_lookup:
fixes X::"tvar"
and \<theta>::"Subst"
and Y::"tvar"
assumes asms: "X\Y" "X\\"
shows "X\(lookup \ Y)"
using asms
by (induct \<theta>)
(auto simp add: fresh_list_cons fresh_prod fresh_atm)
lemma fresh_psubst_ty:
fixes X::"tvar"
and \<theta>::"Subst"
and T::"ty"
assumes asms: "X\\" "X\T"
shows "X\\"
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 \<theta>::"Subst"
and S::"tyS"
assumes asms: "X\\" "X\S"
shows "X\\"
using asms
by (nominal_induct S avoiding: \<theta> X rule: tyS.strong_induct)
(auto simp add: fresh_psubst_ty abs_fresh)
lemma fresh_psubst_Ctxt:
fixes X::"tvar"
and \<theta>::"Subst"
and \<Gamma>::"Ctxt"
assumes asms: "X\\" "X\\"
shows "X\\<\>"
using asms
by (induct \<Gamma>)
(auto simp add: fresh_psubst_tyS fresh_list_cons)
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)
(auto simp add: fresh_atm)
text \<open>instance of a type scheme\<close>
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
by (simp_all add: abs_fresh subst_freshfact2_ty)
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)
(auto simp add: fresh_atm)
lemma psubst_ty_lemma:
fixes \<theta>::"Subst"
and X::"tvar"
and T'::"ty"
and T::"ty"
assumes a: "X\\"
shows "\ = (\)[X::=\]"
using a
apply(nominal_induct T avoiding: \<theta> X T' rule: ty.strong_induct)
apply(auto simp add: ty.inject lookup_fresh)
apply(rule sym)
apply(rule subst_forget_ty)
apply(rule fresh_lookup)
apply(simp_all add: fresh_atm)
done
lemma general_preserved:
fixes \<theta>::"Subst"
assumes a: "T \ S"
shows "\ \ \"
using a
apply(nominal_induct T S avoiding: \<theta> rule: inst.strong_induct)
apply(auto)[1]
apply(simp add: psubst_ty_lemma)
apply(rule_tac I_All)
apply(simp add: fresh_psubst_ty)
apply(simp)
done
text\<open>typing judgements\<close>
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\<^sub>1 : T\<^sub>1\T\<^sub>2; \ \ t\<^sub>2 : T\<^sub>1\\ \ \ App t\<^sub>1 t\<^sub>2 : T\<^sub>2"
| T_LAM[intro]: "\x\\;((x,Ty T\<^sub>1)#\) \ t : T\<^sub>2\ \ \ \ Lam [x].t : T\<^sub>1\T\<^sub>2"
| T_LET[intro]: "\x\\; \ \ t\<^sub>1 : T\<^sub>1; ((x,close \ T\<^sub>1)#\) \ t\<^sub>2 : T\<^sub>2; set (ftv T\<^sub>1 - ftv \) \* T\<^sub>2\
\<Longrightarrow> \<Gamma> \<turnstile> Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>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)
(simp_all add: fresh_atm abs_fresh)
lemma ftv_ty:
fixes T::"ty"
shows "supp T = set (ftv T)"
by (nominal_induct T rule: ty.strong_induct)
(simp_all add: ty.supp supp_atm)
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 \<Gamma>::"Ctxt"
shows "supp \ = set (ftv \)"
apply (induct \<Gamma>)
apply (simp_all add: supp_list_nil supp_list_cons)
apply (rename_tac a \<Gamma>')
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)
(simp_all add: supp_list_nil supp_list_cons supp_atm)
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)
(simp_all add: supp_list_nil supp_list_cons supp_atm)
nominal_inductive2 typing
avoids T_LET: "set (ftv T\<^sub>1 - ftv \)"
apply (simp add: fresh_star_def fresh_def ftv_Ctxt)
apply (simp add: fresh_star_def fresh_tvar_trm)
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 (simp add: split_paired_all pt_tvar2)
apply (frule_tac x="(a, b)" in bspec)
apply simp
apply (simp add: perm_fresh_fresh)
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")
apply(simp add: abs_fresh)
apply(simp add: abs_fresh)
done
lemma close_fresh:
fixes \<Gamma>::"Ctxt"
shows "\(X::tvar)\set ((ftv T) - (ftv \)). X\(close \ T)"
by (simp add: fresh_gen_set)
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\<^sub>1 : T\<^sub>1"
and t2: "((x,close \ T\<^sub>1)#\) \ t\<^sub>2 : T\<^sub>2"
shows "\ \ Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>2"
proof -
have fin: "finite (set (ftv T\<^sub>1 - ftv \))" by simp
obtain pi where pi1: "(pi \ set (ftv T\<^sub>1 - ftv \)) \* (T\<^sub>2, \)"
and pi2: "set pi \ set (ftv T\<^sub>1 - ftv \) \ (pi \ set (ftv T\<^sub>1 - ftv \))"
by (rule at_set_avoiding [OF at_tvar_inst fin fs_tvar1, of "(T\<^sub>2, \)"])
from pi1 have pi1': "(pi \ set (ftv T\<^sub>1 - ftv \)) \* \"
by (simp add: fresh_star_prod)
have Gamma_fresh: "\(x,y)\set pi. x \ \ \ y \ \"
apply (rule ballI)
apply (simp add: split_paired_all)
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\<^sub>1 \ y \ close \ T\<^sub>1"
apply (rule ballI)
apply (simp add: split_paired_all)
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\<^sub>1 : pi \ T\<^sub>1"
by (simp add: perm_fresh_fresh_aux eqvts fresh_tvar_trm)
moreover from t2 close_fresh'
have "(x,(pi \ close \ T\<^sub>1))#\ \ t\<^sub>2 : T\<^sub>2"
by (simp add: perm_fresh_fresh_aux)
with Gamma_fresh have "(x,close \ (pi \ T\<^sub>1))#\ \ t\<^sub>2 : T\<^sub>2"
by (simp add: close_eqvt perm_fresh_fresh_aux)
moreover from pi1 Gamma_fresh
have "set (ftv (pi \ T\<^sub>1) - ftv \) \* T\<^sub>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 \<theta>::"Subst"
and X Y ::"tvar"
assumes a1: "X \ set (ftv T)"
and a2: "Y \ set (ftv (lookup \ X))"
shows "Y \ set (ftv (\))"
using a1 a2
by (nominal_induct T rule: ty.strong_induct) (auto)
lemma ftv_tyS_subst:
fixes S::"tyS"
and \<theta>::"Subst"
and X Y::"tvar"
assumes a1: "X \ set (ftv S)"
and a2: "Y \ set (ftv (lookup \ X))"
shows "Y \ set (ftv (\))"
using a1 a2
by (nominal_induct S avoiding: \<theta> Y rule: tyS.strong_induct)
(auto simp add: ftv_ty_subst fresh_atm)
lemma ftv_Ctxt_subst:
fixes \<Gamma>::"Ctxt"
and \<theta>::"Subst"
assumes a1: "X \ set (ftv \)"
and a2: "Y \ set (ftv (lookup \ X))"
shows "Y \ set (ftv (\<\>))"
using a1 a2
by (induct \<Gamma>)
(auto simp add: ftv_tyS_subst)
lemma gen_preserved1:
assumes asm: "Xs \* \"
shows "\ = gen (\) Xs"
using asm
by (induct Xs)
(auto simp add: fresh_star_def)
lemma gen_preserved2:
fixes T::"ty"
and \<Gamma>::"Ctxt"
assumes asm: "((ftv T) - (ftv \)) \* \"
shows "((ftv (\)) - (ftv (\<\>))) = ((ftv T) - (ftv \))"
using asm
apply(nominal_induct T rule: ty.strong_induct)
apply(auto simp add: fresh_star_def)
apply(simp add: lookup_fresh)
apply(simp add: ftv_Ctxt[symmetric])
apply(fold fresh_def)
apply(rule fresh_psubst_Ctxt)
apply(assumption)
apply(assumption)
apply(rule difference_supset)
apply(auto)
apply(simp add: ftv_Ctxt_subst)
done
lemma close_preserved:
fixes \<Gamma>::"Ctxt"
assumes asm: "((ftv T) - (ftv \)) \* \"
shows "\ T> = close (\<\>) (\)"
using asm
by (simp add: gen_preserved1 gen_preserved2)
lemma var_fresh_for_ty:
fixes x::"var"
and T::"ty"
shows "x\T"
by (nominal_induct T rule: ty.strong_induct)
(simp_all add: fresh_atm)
lemma var_fresh_for_tyS:
fixes x::"var"
and S::"tyS"
shows "x\S"
by (nominal_induct S rule: tyS.strong_induct)
(simp_all add: abs_fresh var_fresh_for_ty)
lemma psubst_fresh_Ctxt:
fixes x::"var"
and \<Gamma>::"Ctxt"
and \<theta>::"Subst"
shows "x\\<\> = x\\"
by (induct \<Gamma>)
(auto simp add: fresh_list_cons fresh_list_nil fresh_prod var_fresh_for_tyS)
lemma psubst_valid:
fixes \<theta>::Subst
and \<Gamma>::Ctxt
assumes a: "valid \"
shows "valid (\<\>)"
using a
by (induct)
(auto simp add: psubst_fresh_Ctxt)
lemma psubst_in:
fixes \<Gamma>::"Ctxt"
and \<theta>::"Subst"
and pi::"tvar prm"
and S::"tyS"
assumes a: "(x,S)\set \"
shows "(x,\)\set (\<\>)"
using a
by (induct \<Gamma>)
(auto simp add: calc_atm)
lemma typing_preserved:
fixes \<theta>::"Subst"
and pi::"tvar prm"
assumes a: "\ \ t : T"
shows "(\<\>) \ t : (\)"
using a
proof (nominal_induct \<Gamma> t T avoiding: \<theta> rule: typing.strong_induct)
case (T_VAR \<Gamma> 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,\)\set (\<\>)" using a2 by (simp add: psubst_in)
moreover
have "\ \ \" using a3 by (simp add: general_preserved)
ultimately show "(\<\>) \ Var x : (\)" by (simp add: typing.T_VAR)
next
case (T_APP \<Gamma> t1 T1 T2 t2)
have "\<\> \ t1 : \ T2>" by fact
then have "\<\> \ t1 : (\) \ (\)" by simp
moreover
have "\<\> \ t2 : \" by fact
ultimately show "\<\> \ App t1 t2 : \" by (simp add: typing.T_APP)
next
case (T_LAM x \<Gamma> T1 t T2)
fix pi::"tvar prm" and \<theta>::"Subst"
have "x\\" by fact
then have "x\\<\>" by (simp add: psubst_fresh_Ctxt)
moreover
have "\<((x, Ty T1)#\)> \ t : \" by fact
then have "((x, Ty (\))#(\<\>)) \ t : \" by (simp add: calc_atm)
ultimately show "\<\> \ Lam [x].t : \ T2>" by (simp add: typing.T_LAM)
next
case (T_LET x \<Gamma> 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 : \" by fact
have a3: "\<((x, close \ T1)#\)> \ t2 : \" by fact
from a2 a3 show "\<\> \ Let x be t1 in t2 : \"
apply -
apply(rule better_T_LET)
apply(rule a1)
apply(rule a2)
apply(simp add: close_preserved vc)
done
qed
end
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
