theory TypeSchemes

imports "../Nominal2"

begin

section {*** Type Schemes ***}

atom_decl name 

(* defined as a single nominal datatype *)

nominal_datatype ty =

  Var "name"

| Fun "ty" "ty"

and tys =

  All xs::"name fset" ty::"ty" bind (res) xs in ty

thm ty_tys.distinct

thm ty_tys.induct

thm ty_tys.exhaust

thm ty_tys.fv_defs

thm ty_tys.bn_defs

thm ty_tys.perm_simps

thm ty_tys.eq_iff

thm ty_tys.fv_bn_eqvt

thm ty_tys.size_eqvt

thm ty_tys.supports

thm ty_tys.supp

thm ty_tys.fresh

(* defined as two separate nominal datatypes *)

nominal_datatype ty2 =

  Var2 "name"

| Fun2 "ty2" "ty2"

nominal_datatype tys2 =

  All2 xs::"name fset" ty::"ty2" bind (res) xs in ty

thm tys2.distinct

thm tys2.induct

thm tys2.exhaust

thm tys2.fv_defs

thm tys2.bn_defs

thm tys2.perm_simps

thm tys2.eq_iff

thm tys2.fv_bn_eqvt

thm tys2.size_eqvt

thm tys2.supports

thm tys2.supp

thm tys2.fresh

lemma strong_exhaust:

  fixes c::"'a::fs"

  assumes "\<And>names ty. \<lbrakk>fset (map_fset atom names) \<sharp>* c; y = All2 names ty\<rbrakk> \<Longrightarrow> P"

  shows "P"

apply(rule_tac y="y" in tys2.exhaust)

apply(rename_tac names ty2)

apply(subgoal_tac "\<exists>q. (q \<bullet> (fset (map_fset atom names))) \<sharp>* c \<and> supp (All2 names ty2) \<sharp>* q")

apply(erule exE)

apply(perm_simp)

apply(erule conjE)

apply(rule assms(1))

apply(assumption)

apply(clarify)

apply(drule supp_perm_eq[symmetric])

apply(simp)

apply(rule at_set_avoiding2)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp)

apply(simp add: fresh_star_def)

apply(simp add: tys2.fresh)

done

lemma strong_induct:

  fixes c::"'a::fs"

  assumes "\<And>names ty2 c. fset (map_fset atom names) \<sharp>* c \<Longrightarrow> P c (All2 names ty2)"

  shows "P c tys"

using assms

apply(induction_schema)

apply(rule_tac y="tys" in strong_exhaust)

apply(blast)

apply(relation "measure (\<lambda>(x,y). size y)")

apply(simp_all add: tys2.size)

done

text {* Some Tests *}

lemma

  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"

  apply(simp add: ty_tys.eq_iff)

  apply(simp add: Abs_eq_iff)

  apply(rule_tac x="0::perm" in exI)

  apply(simp add: alphas)

  apply(simp add: fresh_star_def fresh_zero_perm supp_at_base)

  apply(simp add: ty_tys.supp supp_at_base)

  done

lemma

  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"

  apply(simp add: ty_tys.eq_iff Abs_eq_iff)

  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)

  apply(simp add: alphas fresh_star_def supp_at_base ty_tys.supp)

  done

lemma

  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"

  apply(simp add: ty_tys.eq_iff Abs_eq_iff)

  apply(rule_tac x="0::perm" in exI)

  apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)

done

lemma

  assumes a: "a \<noteq> b"

  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"

  using a

  apply(simp add: ty_tys.eq_iff Abs_eq_iff)

  apply(clarify)

  apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)

  apply auto

  done

text {* Some lemmas about fsets *}

lemma atom_map_fset_cong:

  shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"

  apply(rule inj_map_fset_cong)

  apply(simp add: inj_on_def)

  done

lemma supp_map_fset_atom:

  shows "supp (map_fset atom S) = supp S"

  unfolding supp_def

  apply(perm_simp)

  apply(simp add: atom_map_fset_cong)

  done

lemma supp_at_fset:

  fixes S::"('a::at_base) fset"

  shows "supp S = fset (map_fset atom S)"

  apply (induct S)

  apply (simp add: supp_empty_fset)

  apply (simp add: supp_insert_fset)

  apply (simp add: supp_at_base)

  done

lemma fresh_star_atom:

  fixes a::"'a::at_base"

  shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S"

  apply (induct S)

  apply (simp add: fresh_set_empty)

  apply simp

  apply (unfold fresh_def)

  apply (simp add: supp_of_finite_insert)

  apply (rule conjI)

  apply (unfold fresh_star_def)

  apply simp

  apply (unfold fresh_def)

  apply (simp add: supp_at_base supp_atom)

  apply clarify

  apply auto

  done

(*

fun

  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"

where

  "lookup [] n = Var n"

| "lookup ((p, s) # t) n = (if p = n then s else lookup t n)"

locale subst_loc =

fixes

    subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"

and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"

assumes

    s1: "subst \<theta> (Var n) = lookup \<theta> n"

and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)"

and s3: "fset (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"

begin

lemma subst_ty:

  assumes x: "atom x \<sharp> t"

  shows "subst [(x, S)] t = t"

  using x

  apply (induct t rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])

  by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base)

lemma subst_tyS:

  shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T"

  apply (rule strong_induct[of

    "\<lambda>a t. True" "\<lambda>(x, S) T. (atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T)" _ "t" "(x, S)", simplified])

  apply clarify

  apply (subst s3)

  apply (simp add: fresh_star_def fresh_Cons fresh_Nil)

  apply (subst subst_ty)

  apply (simp_all add: fresh_star_prod_elim)

  apply (drule fresh_star_atom)

  apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])

  apply (subgoal_tac "atom a \<notin> fset (fmap atom fset)")

  apply blast

  apply (metis supp_finite_atom_set finite_fset)

  done

lemma subst_lemma_pre:

  "z \<sharp> (N,L) \<longrightarrow> z \<sharp> (subst [(y, L)] N)"

  apply (induct N rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])

  apply (simp add: s1)

  apply (auto simp add: fresh_Pair)

  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])[3]

  apply (simp add: s2)

  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])

  done

lemma substs_lemma_pre:

  "atom z \<sharp> (N,L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N)"

  apply (rule strong_induct[of

    "\<lambda>a t. True" "\<lambda>(z, y, L) N. (atom z \<sharp> (N, L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N))" _ _ "(z, y, L)", simplified])

  apply clarify

  apply (subst s3)

  apply (simp add: fresh_star_def fresh_Cons fresh_Nil fresh_Pair)

  apply (simp_all add: fresh_star_prod_elim fresh_Pair)

  apply clarify

  apply (drule fresh_star_atom)

  apply (drule fresh_star_atom)

  apply (simp add: fresh_def)

  apply (simp only: ty_tys.fv[simplified ty_tys.supp])

  apply (subgoal_tac "atom a \<notin> supp (subst [(aa, b)] t)")

  apply blast

  apply (subgoal_tac "atom a \<notin> supp t")

  apply (fold fresh_def)[1]

  apply (rule mp[OF subst_lemma_pre])

  apply (simp add: fresh_Pair)

  apply (subgoal_tac "atom a \<notin> (fset (fmap atom fset))")

  apply blast

  apply (metis supp_finite_atom_set finite_fset)

  done

lemma subst_lemma:

  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>

    subst [(y, L)] (subst [(x, N)] M) =

    subst [(x, (subst [(y, L)] N))] (subst [(y, L)] M)"

  apply (induct M rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])

  apply (simp_all add: s1 s2)

  apply clarify

  apply (subst (2) subst_ty)

  apply simp_all

  done

lemma substs_lemma:

  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>

    substs [(y, L)] (substs [(x, N)] M) =

    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)"

  apply (rule strong_induct[of

    "\<lambda>a t. True" "\<lambda>(x, y, N, L) M. x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>

    substs [(y, L)] (substs [(x, N)] M) =

    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)" _ _ "(x, y, N, L)", simplified])

  apply clarify

  apply (simp_all add: fresh_star_prod_elim fresh_Pair)

  apply (subst s3)

  apply (unfold fresh_star_def)[1]

  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)

  apply (subst s3)

  apply (unfold fresh_star_def)[1]

  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)

  apply (subst s3)

  apply (unfold fresh_star_def)[1]

  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)

  apply (subst s3)

  apply (unfold fresh_star_def)[1]

  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)

  apply (rule ballI)

  apply (rule mp[OF subst_lemma_pre])

  apply (simp add: fresh_Pair)

  apply (subst subst_lemma)

  apply simp_all

  done

end

*)

end