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. xset ys]"

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

lemma difference_fresh:
  fixes X::"tvar"
  and   Xs Ys::"tvar list"
  assumes a: "Xset 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"

overloading 
  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 (piT)"
by (nominal_induct T rule: ty.strong_induct)
   (perm_simp add: append_eqvt)+

overloading 
  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(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 (piS)"
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   Γ::"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 (piT) (piXs)"
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Γ) (piT)"
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θ) (piX)"
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)

overloading 
  psubst_ty  "psubst :: Subst  ty  ty"
begin

nominal_primrec 
  psubst_ty
where
  "θ<TVar X>   = lookup θ X"
| "θ<T1  T2> = (θ<T1>)  (θ<T2>)"
by (rule TrueI)+

end

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

overloading 
  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(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  "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: "XY" "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θ" "XT"
  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θ" "XS"
  shows "Xθ<S>"
  using asms
  by (nominal_induct S avoiding: θ  X rule: tyS.strong_induct)
     (auto simp add: fresh_psubst_ty abs_fresh)

lemma fresh_psubst_Ctxt:
  fixes X::"tvar"
  and   θ::"Subst"
  and   Γ::"Ctxt"
  assumes asms: "Xθ" "XΓ"
  shows "Xθ<Γ>"
using asms
by (induct Γ)
   (auto simp add: fresh_psubst_tyS fresh_list_cons)

lemma subst_freshfact2_ty: 
  fixes   X::"tvar"
  and     Y::"tvar"
  and     T::"ty"
  assumes asms: "XS"
  shows "XT[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  tyS  bool"("_  _" [50,51] 50)  
where
  I_Ty[intro]:  "T  (Ty T)" 
| I_All[intro]: "XT'; 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: "XT"
  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 θ::"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(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 θ::"Subst"
  assumes a: "T  S"
  shows "θ<T>  θ<S>"
using a
apply(nominal_induct T S avoiding: θ 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  trm  ty  bool" (" _  _ : _ " [60,60,60] 60) 
where
  T_VAR[intro]: "valid Γ; (x,S)set Γ; T  S Γ  Var x : T"
| T_APP[intro]: "Γ  t1 : T1T2; Γ  t2 : T1 Γ  App t1 t2 : T2" 
| T_LAM[intro]: "xΓ;((x,Ty T1)#Γ)  t : T2  Γ  Lam [x].t : T1T2"
| T_LET[intro]: "xΓ; Γ  t1 : T1; ((x,close Γ T1)#Γ)  t2 : T2; set (ftv T1 - ftv Γ) ♯* T2 
                  Γ  Let x be t1 in t2 : T2"

equivariance typing[tvar]

lemma fresh_tvar_trm: 
  fixes X::"tvar"
  and   t::"trm"
  shows "Xt"
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 Γ::"Ctxt"
  shows "supp Γ = set (ftv Γ)"
apply (induct Γ)
apply (simp_all add: supp_list_nil supp_list_cons)
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) 
   (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 T1 - 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: "Xset Xs" 
  shows "Xgen 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 Γ::"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: "Γ  t1 : T1"
  and t2: "((x,close Γ T1)#Γ)  t2 : T2"
  shows "Γ  Let x be t1 in t2 : T2"
proof -
  have fin: "finite (set (ftv T1 - ftv Γ))" by simp
  obtain pi where pi1: "(pi  set (ftv T1 - ftv Γ)) ♯* (T2, Γ)"
    and pi2: "set pi  set (ftv T1 - ftv Γ) × (pi  set (ftv T1 - ftv Γ))"
    by (rule at_set_avoiding [OF at_tvar_inst fin fs_tvar1, of "(T2, Γ)"])
  from pi1 have pi1': "(pi  set (ftv T1 - 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 Γ T1  y  close Γ T1"
    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 "Γ  t1 : pi  T1"
    by (simp add: perm_fresh_fresh_aux eqvts fresh_tvar_trm)
  moreover from t2 close_fresh'
  have "(x,(pi  close Γ T1))#Γ  t2 : T2"
    by (simp add: perm_fresh_fresh_aux)
  with Gamma_fresh have "(x,close Γ (pi  T1))#Γ  t2 : T2"
    by (simp add: close_eqvt perm_fresh_fresh_aux)
  moreover from pi1 Gamma_fresh
  have "set (ftv (pi  T1) - ftv Γ) ♯* T2"
    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) 
   (auto simp add: ftv_ty_subst fresh_atm)

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 Γ)
   (auto simp add: ftv_tyS_subst)

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

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(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 Γ::"Ctxt"
  assumes asm: "((ftv T) - (ftv Γ)) ♯* θ"
  shows "θ<close Γ T> = close (θ<Γ>) (θ<T>)"
using asm
by (simp add: gen_preserved1 gen_preserved2)

lemma var_fresh_for_ty:
  fixes x::"var"
  and   T::"ty"
  shows "xT"
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 "xS"
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   Γ::"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) 
   (auto simp add: psubst_fresh_Ctxt)

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 Γ)
   (auto simp add: calc_atm)


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)
    apply(simp add: close_preserved vc)
    done
qed



end