src/HOL/Nominal/Examples/W.thy

Mirabelle: actions are responsible for handling exceptions,
Mirabelle core logs only structural information,
measuring running times for sledgehammer and subsequent metis invocation,
Mirabelle produces reports for every theory (only for sledgehammer at the moment)

theory W
imports Nominal
begin

text {* Example for strong induction rules avoiding sets of atoms. *}

atom_decl tvar var 

abbreviation
  "difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60) 
where
  "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"

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

lemma difference_fresh:
  fixes X::"tvar"
  and   Xs Ys::"tvar list"
  assumes a: "X\<in>set Ys"
  shows "X\<sharp>(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 \<subseteq> set ys"
  shows "xs - ys = []"
using asm
by (induct xs) (auto)

nominal_datatype ty = 
    TVar "tvar"
  | Fun "ty" "ty" ("_\<rightarrow>_" [100,100] 100)

nominal_datatype tyS = 
    Ty  "ty"
  | ALL "\<guillemotleft>tvar\<guillemotright>tyS" ("\<forall>[_]._" [100,100] 100)

nominal_datatype trm = 
    Var "var"
  | App "trm" "trm" 
  | Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
  | Let "\<guillemotleft>var\<guillemotright>trm" "trm" 

abbreviation
  LetBe :: "var \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" ("Let _ be _ in _" [100,100,100] 100)
where
 "Let x be t1 in t2 \<equiv> trm.Let x t2 t1"

types 
  Ctxt  = "(var\<times>tyS) list" 

text {* free type variables *}

consts ftv :: "'a \<Rightarrow> 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 \<Rightarrow> tvar list"
where
[simp]: "ftv_tvar X \<equiv> [(X::tvar)]"

definition
  ftv_var :: "var \<Rightarrow> tvar list"
where
[simp]: "ftv_var x \<equiv> []"

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

nominal_primrec 
  ftv_ty :: "ty \<Rightarrow> tvar list"
where
  "ftv_ty (TVar X) = [X]"
| "ftv_ty (T1 \<rightarrow>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\<bullet>(ftv T) = ftv (pi\<bullet>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 \<Rightarrow> tvar list"
where
  "ftv_tyS (Ty T)    = ((ftv (T::ty))::tvar list)"
| "ftv_tyS (\<forall>[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\<bullet>(ftv S) = ftv (pi\<bullet>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\<bullet>(ftv \<Gamma>) = ftv (pi\<bullet>\<Gamma>)"
by (induct \<Gamma>) (auto simp add: eqvts)

text {* Valid *}
inductive
  valid :: "Ctxt \<Rightarrow> bool"
where
  V_Nil[intro]:  "valid []"
| V_Cons[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,S)#\<Gamma>)"

equivariance valid

text {* General *}
consts
  gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS"

primrec 
  "gen T [] = Ty T"
  "gen T (X#Xs) = \<forall>[X].(gen T Xs)"

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



abbreviation 
  close :: "Ctxt \<Rightarrow> ty \<Rightarrow> tyS"
where 
  "close \<Gamma> T \<equiv> gen T ((ftv T) - (ftv \<Gamma>))"

lemma close_eqvt[eqvt]:
  fixes pi::"tvar prm"
  shows "pi\<bullet>(close \<Gamma> T) = close (pi\<bullet>\<Gamma>) (pi\<bullet>T)"
by (simp_all only: eqvts)
  
text {* Substitution *}

types Subst = "(tvar\<times>ty) list"

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

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

fun
  lookup :: "Subst \<Rightarrow> tvar \<Rightarrow> ty"   
where
  "lookup [] X        = TVar X"
| "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"

lemma lookup_eqvt[eqvt]:
  fixes pi::"tvar prm"
  shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
by (induct \<theta>) (auto simp add: eqvts)

lemma lookup_fresh:
  fixes X::"tvar"
  assumes a: "X\<sharp>\<theta>"
  shows "lookup \<theta> 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
  "\<theta><TVar X>   = lookup \<theta> X"
| "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
by (rule TrueI)+

end

lemma psubst_ty_eqvt[eqvt]:
  fixes pi::"tvar prm"
  and   \<theta>::"Subst"
  and   T::"ty"
  shows "pi\<bullet>(\<theta><T>) = (pi\<bullet>\<theta>)<(pi\<bullet>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 \<Rightarrow> tyS \<Rightarrow> tyS"
where 
  "\<theta><(Ty T)> = Ty (\<theta><T>)"
| "X\<sharp>\<theta> \<Longrightarrow> \<theta><(\<forall>[X].S)> = \<forall>[X].(\<theta><S>)"
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 \<Rightarrow> Ctxt \<Rightarrow> Ctxt"
where
  "psubst_Ctxt \<theta> [] = []"
| "psubst_Ctxt \<theta> ((x,S)#\<Gamma>) = (x,\<theta><S>)#(psubst_Ctxt \<theta> \<Gamma>)"

end

lemma fresh_lookup:
  fixes X::"tvar"
  and   \<theta>::"Subst"
  and   Y::"tvar"
  assumes asms: "X\<sharp>Y" "X\<sharp>\<theta>"
  shows "X\<sharp>(lookup \<theta> 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\<sharp>\<theta>" "X\<sharp>T"
  shows "X\<sharp>\<theta><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   \<theta>::"Subst"
  and   S::"tyS"
  assumes asms: "X\<sharp>\<theta>" "X\<sharp>S"
  shows "X\<sharp>\<theta><S>"
  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\<sharp>\<theta>" "X\<sharp>\<Gamma>"
  shows "X\<sharp>\<theta><\<Gamma>>"
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\<sharp>S"
  shows "X\<sharp>T[X::=S]"
  using asms
by (nominal_induct T rule: ty.strong_induct)
   (auto simp add: fresh_atm)

text {* instance of a type scheme *}
inductive
  inst :: "ty \<Rightarrow> tyS \<Rightarrow> bool"("_ \<prec> _" [50,51] 50)  
where
  I_Ty[intro]:  "T \<prec> (Ty T)" 
| I_All[intro]: "\<lbrakk>X\<sharp>T'; T \<prec> S\<rbrakk> \<Longrightarrow> T[X::=T'] \<prec> \<forall>[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\<sharp>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\<sharp>\<theta>" 
  shows "\<theta><T[X::=T']> = (\<theta><T>)[X::=\<theta><T'>]"
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 \<prec> S"
  shows "\<theta><T> \<prec> \<theta><S>"
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{* typing judgements *}
inductive
  typing :: "Ctxt \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
where
  T_VAR[intro]: "\<lbrakk>valid \<Gamma>; (x,S)\<in>set \<Gamma>; T \<prec> S\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
| T_APP[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t\<^isub>1 t\<^isub>2 : T\<^isub>2" 
| T_LAM[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,Ty T\<^isub>1)#\<Gamma>) \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"
| T_LET[intro]: "\<lbrakk>x\<sharp>\<Gamma>; \<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1; ((x,close \<Gamma> T\<^isub>1)#\<Gamma>) \<turnstile> t\<^isub>2 : T\<^isub>2; set (ftv T\<^isub>1 - ftv \<Gamma>) \<sharp>* T\<^isub>2\<rbrakk> 
                 \<Longrightarrow> \<Gamma> \<turnstile> Let x be t\<^isub>1 in t\<^isub>2 : T\<^isub>2"

equivariance typing[tvar]

lemma fresh_tvar_trm: 
  fixes X::"tvar"
  and   t::"trm"
  shows "X\<sharp>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 \<Gamma> = set (ftv \<Gamma>)"
apply (induct \<Gamma>)
apply (simp_all add: supp_list_nil supp_list_cons)
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\<^isub>1 - ftv \<Gamma>)"
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:
  "\<forall>(x,y)\<in>set (pi::tvar prm). x \<sharp> z \<and> y \<sharp> z \<Longrightarrow> pi \<bullet> (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 \<in> S"
  and     "S \<sharp>* z"
  shows  "x \<sharp> z"
using prems  by (simp add: fresh_star_def)

lemma fresh_gen_set:
  fixes X::"tvar"
  and   Xs::"tvar list"
  assumes asm: "X\<in>set Xs" 
  shows "X\<sharp>gen T Xs"
using asm
apply(induct Xs)
apply(simp)
apply(case_tac "X=a")
apply(simp add: abs_fresh)
apply(simp add: abs_fresh)
done

lemma close_fresh:
  fixes \<Gamma>::"Ctxt"
  shows "\<forall>(X::tvar)\<in>set ((ftv T) - (ftv \<Gamma>)). X\<sharp>(close \<Gamma> 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 \<inter> U"
  by blast

lemma close_supp: 
  shows "supp (close \<Gamma> T) = set (ftv T) \<inter> set (ftv \<Gamma>)"
  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\<sharp>\<Gamma>"
  and t1: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1"
  and t2: "((x,close \<Gamma> T\<^isub>1)#\<Gamma>) \<turnstile> t\<^isub>2 : T\<^isub>2"
  shows "\<Gamma> \<turnstile> Let x be t\<^isub>1 in t\<^isub>2 : T\<^isub>2"
proof -
  have fin: "finite (set (ftv T\<^isub>1 - ftv \<Gamma>))" by simp
  obtain pi where pi1: "(pi \<bullet> set (ftv T\<^isub>1 - ftv \<Gamma>)) \<sharp>* (T\<^isub>2, \<Gamma>)"
    and pi2: "set pi \<subseteq> set (ftv T\<^isub>1 - ftv \<Gamma>) \<times> (pi \<bullet> set (ftv T\<^isub>1 - ftv \<Gamma>))"
    by (rule at_set_avoiding [OF at_tvar_inst fin fs_tvar1, of "(T\<^isub>2, \<Gamma>)"])
  from pi1 have pi1': "(pi \<bullet> set (ftv T\<^isub>1 - ftv \<Gamma>)) \<sharp>* \<Gamma>"
    by (simp add: fresh_star_prod)
  have Gamma_fresh: "\<forall>(x,y)\<in>set pi. x \<sharp> \<Gamma> \<and> y \<sharp> \<Gamma>"
    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': "\<forall>(x, y)\<in>set pi. x \<sharp> close \<Gamma> T\<^isub>1 \<and> y \<sharp> close \<Gamma> T\<^isub>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 "\<Gamma> \<turnstile> t\<^isub>1 : pi \<bullet> T\<^isub>1"
    by (simp add: perm_fresh_fresh_aux eqvts fresh_tvar_trm)
  moreover from t2 close_fresh'
  have "(x,(pi \<bullet> close \<Gamma> T\<^isub>1))#\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
    by (simp add: perm_fresh_fresh_aux)
  with Gamma_fresh have "(x,close \<Gamma> (pi \<bullet> T\<^isub>1))#\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
    by (simp add: close_eqvt perm_fresh_fresh_aux)
  moreover from pi1 Gamma_fresh
  have "set (ftv (pi \<bullet> T\<^isub>1) - ftv \<Gamma>) \<sharp>* T\<^isub>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 \<in> set (ftv T)"
  and     a2: "Y \<in> set (ftv (lookup \<theta> X))"
  shows "Y \<in> set (ftv (\<theta><T>))"
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 \<in> set (ftv S)"
  and     a2: "Y \<in> set (ftv (lookup \<theta> X))"
  shows "Y \<in> set (ftv (\<theta><S>))"
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 \<in> set (ftv \<Gamma>)"
  and     a2: "Y \<in> set (ftv (lookup \<theta> X))"
  shows "Y \<in> set (ftv (\<theta><\<Gamma>>))"
using a1 a2
by (induct \<Gamma>)
   (auto simp add: ftv_tyS_subst)

lemma gen_preserved1:
  assumes asm: "Xs \<sharp>* \<theta>"
  shows "\<theta><gen T Xs> = gen (\<theta><T>) 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 \<Gamma>)) \<sharp>* \<theta>"
  shows "((ftv (\<theta><T>)) - (ftv (\<theta><\<Gamma>>))) = ((ftv T) - (ftv \<Gamma>))"
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 \<Gamma>)) \<sharp>* \<theta>"
  shows "\<theta><close \<Gamma> T> = close (\<theta><\<Gamma>>) (\<theta><T>)"
using asm
by (simp add: gen_preserved1 gen_preserved2)

lemma var_fresh_for_ty:
  fixes x::"var"
  and   T::"ty"
  shows "x\<sharp>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\<sharp>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\<sharp>\<theta><\<Gamma>> = x\<sharp>\<Gamma>"
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 \<Gamma>"
  shows "valid (\<theta><\<Gamma>>)"
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)\<in>set \<Gamma>"
  shows "(x,\<theta><S>)\<in>set (\<theta><\<Gamma>>)"
using a
by (induct \<Gamma>)
   (auto simp add: calc_atm)


lemma typing_preserved:
  fixes \<theta>::"Subst"
  and   pi::"tvar prm"
  assumes a: "\<Gamma> \<turnstile> t : T"
  shows "(\<theta><\<Gamma>>) \<turnstile> t : (\<theta><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 \<Gamma>" by fact
  have a2: "(x, S) \<in> set \<Gamma>" by fact
  have a3: "T \<prec> S" by fact
  have  "valid (\<theta><\<Gamma>>)" using a1 by (simp add: psubst_valid)
  moreover
  have  "(x,\<theta><S>)\<in>set (\<theta><\<Gamma>>)" using a2 by (simp add: psubst_in)
  moreover
  have "\<theta><T> \<prec> \<theta><S>" using a3 by (simp add: general_preserved)
  ultimately show "(\<theta><\<Gamma>>) \<turnstile> Var x : (\<theta><T>)" by (simp add: typing.T_VAR)
next
  case (T_APP \<Gamma> t1 T1 T2 t2)
  have "\<theta><\<Gamma>> \<turnstile> t1 : \<theta><T1 \<rightarrow> T2>" by fact
  then have "\<theta><\<Gamma>> \<turnstile> t1 : (\<theta><T1>) \<rightarrow> (\<theta><T2>)" by simp
  moreover
  have "\<theta><\<Gamma>> \<turnstile> t2 : \<theta><T1>" by fact
  ultimately show "\<theta><\<Gamma>> \<turnstile> App t1 t2 : \<theta><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\<sharp>\<Gamma>" by fact
  then have "x\<sharp>\<theta><\<Gamma>>" by (simp add: psubst_fresh_Ctxt)
  moreover
  have "\<theta><((x, Ty T1)#\<Gamma>)> \<turnstile> t : \<theta><T2>" by fact
  then have "((x, Ty (\<theta><T1>))#(\<theta><\<Gamma>>)) \<turnstile> t : \<theta><T2>" by (simp add: calc_atm)
  ultimately show "\<theta><\<Gamma>> \<turnstile> Lam [x].t : \<theta><T1 \<rightarrow> T2>" by (simp add: typing.T_LAM)
next
  case (T_LET x \<Gamma> t1 T1 t2 T2)
  have vc: "((ftv T1) - (ftv \<Gamma>)) \<sharp>* \<theta>" by fact
  have "x\<sharp>\<Gamma>" by fact
   then have a1: "x\<sharp>\<theta><\<Gamma>>" by (simp add: calc_atm psubst_fresh_Ctxt)
  have a2: "\<theta><\<Gamma>> \<turnstile> t1 : \<theta><T1>" by fact 
  have a3: "\<theta><((x, close \<Gamma> T1)#\<Gamma>)> \<turnstile> t2 : \<theta><T2>" by fact
  from a2 a3 show "\<theta><\<Gamma>> \<turnstile> Let x be t1 in t2 : \<theta><T2>"
    apply -
    apply(rule better_T_LET)
    apply(rule a1)
    apply(rule a2)
    apply(simp add: close_preserved vc)
    done
qed



end