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 (set+) xs in ty

thm ty_tys.distinct

thm ty_tys.induct

thm ty_tys.inducts

thm ty_tys.exhaust ty_tys.strong_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

fun

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

where

  "lookup [] Y = Var Y"

| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"

lemma lookup_eqvt[eqvt]:

  shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"

apply(induct Ts T rule: lookup.induct)

apply(simp_all)

done

nominal_primrec

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

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

where

  "subst \<theta> (Var X) = lookup \<theta> X"

| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"

| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"

term subst_substs_sumC

term Inl

thm subst_substs_graph.induct

thm subst_substs_graph.intros

thm Projl.simps

apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")

apply(simp add: eqvt_def)

apply(rule allI)

apply(simp add: permute_fun_def permute_bool_def)

apply(rule ext)

apply(rule ext)

apply(rule iffI)

apply(drule_tac x="p" in meta_spec)

apply(drule_tac x="- p \<bullet> x" in meta_spec)

apply(drule_tac x="- p \<bullet> xa" in meta_spec)

apply(simp)

apply(drule_tac x="-p" in meta_spec)

apply(drule_tac x="x" in meta_spec)

apply(drule_tac x="xa" in meta_spec)

apply(simp)

thm subst_substs_graph.induct

thm subst_substs_graph.intros

thm Projl.simps

apply(erule subst_substs_graph.induct)

apply(perm_simp)

apply(rule subst_substs_graph.intros)

apply(simp only: eqvts)

thm Projl.simps

term Inl

term Inr

apply(perm_simp)

thm subst_substs_graph.intros

thm Projl.simps

oops

section {* defined as two separate nominal datatypes *}

nominal_datatype ty2 =

  Var2 "name"

| Fun2 "ty2" "ty2"

nominal_datatype tys2 =

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

thm tys2.distinct

thm tys2.induct tys2.strong_induct

thm tys2.exhaust tys2.strong_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

fun

  lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"

where

  "lookup2 [] Y = Var2 Y"

| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"

lemma lookup2_eqvt[eqvt]:

  shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"

apply(induct Ts T rule: lookup2.induct)

apply(simp_all)

done

nominal_primrec

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

where

  "subst \<theta> (Var2 X) = lookup2 \<theta> X"

| "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"

defer

apply(case_tac x)

apply(simp)

apply(rule_tac y="b" in ty2.exhaust)

apply(blast)

apply(blast)

apply(simp_all add: ty2.distinct)

apply(simp add: ty2.eq_iff)

apply(simp add: ty2.eq_iff)

apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)")

apply(simp add: eqvt_def)

apply(rule allI)

apply(simp add: permute_fun_def permute_bool_def)

apply(rule ext)

apply(rule ext)

apply(rule iffI)

apply(drule_tac x="p" in meta_spec)

apply(drule_tac x="- p \<bullet> x" in meta_spec)

apply(drule_tac x="- p \<bullet> xa" in meta_spec)

apply(simp)

apply(drule_tac x="-p" in meta_spec)

apply(drule_tac x="x" in meta_spec)

apply(drule_tac x="xa" in meta_spec)

apply(simp)

apply(erule subst_graph.induct)

apply(perm_simp)

apply(rule subst_graph.intros)

apply(perm_simp)

apply(rule subst_graph.intros)

apply(assumption)

apply(assumption)

done

termination

  apply(relation "measure (size o snd)")

  apply(simp_all add: ty2.size)

  done

lemma subst_eqvt[eqvt]:

  shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)"

apply(induct \<theta> T rule: subst.induct)

apply(simp_all add: lookup2_eqvt)

done

lemma j:

  assumes "a \<sharp> Ts" " a \<sharp> X"

  shows "a \<sharp> lookup2 Ts X"

using assms

apply(induct Ts X rule: lookup2.induct)

apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair)

done

lemma i:

  assumes "a \<sharp> t" " a \<sharp> \<theta>"

  shows "a \<sharp> subst \<theta> t"

using assms

apply(induct \<theta> t rule: subst.induct)

apply(auto simp add: ty2.fresh j)

done 

lemma k:

  assumes "as \<sharp>* t" " as \<sharp>* \<theta>"

  shows "as \<sharp>* subst \<theta> t"

using assms

by (simp add: fresh_star_def i)

lemma h:

  assumes "as \<subseteq> bs \<union> cs"

  and " cs \<sharp>* x"

  shows "(as - bs) \<sharp>* x"

using assms

by (auto simp add: fresh_star_def)

nominal_primrec

  substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"

where

  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"

oops

text {* Some Tests about Alpha-Equality *}

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 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

  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

end