theory TypeSchemes

imports "../Nominal2"

begin

section {*** Type Schemes ***}

thm Set.set_mp Set.subsetD

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

lemma test:

  assumes a: "f x = Inl y"

  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"

using a 

apply(frule_tac p="p" in permute_boolI)

apply(simp (no_asm_use) only: eqvts)

apply(subst (asm) permute_fun_app_eq)

back

apply(simp)

done

lemma test2:

  assumes a: "f x = Inl y"

  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"

using a 

apply(frule_tac p="p" in permute_boolI)

apply(simp (no_asm_use) only: eqvts)

apply(subst (asm) permute_fun_app_eq)

back

apply(simp)

done

lemma helper:

  assumes "A - C = A - D"

  and "B - C = B - D"

  and "E \<subseteq> A \<union> B"

  shows "E - C = E - D"

using assms

by blast

definition "MYUNDEFINED \<equiv> undefined"

--"The following is accepted by 'function' but not by 'nominal_primrec'"

function (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")

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

thm subst_substs_graph_def

thm subst_substs_sumC_def

oops

lemma Abs_res_fcb:

  fixes xs ys :: "('a :: at_base) set"

    and S T :: "'b :: fs"

  assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)"

    and f1: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T"

    and f2: "\<And>x. supp T - atom ` xs = supp S - atom ` ys \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T"

    and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S

               \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S \<Longrightarrow> p \<bullet> (f xs T) = f ys S"

  shows "f xs T = f ys S"

  using e apply -

  apply (subst (asm) Abs_eq_res_set)

  apply (subst (asm) Abs_eq_iff2)

  apply (simp add: alphas)

  apply (elim exE conjE)

  apply(rule trans)

  apply (rule_tac p="p" in supp_perm_eq[symmetric])

  apply(rule fresh_star_supp_conv)

  apply(drule fresh_star_perm_set_conv)

  apply (rule finite_Diff)

  apply (rule finite_supp)

  apply (subgoal_tac "(atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S) \<sharp>* f xs T")

  apply (metis Un_absorb2 fresh_star_Un)

  apply (subst fresh_star_Un)

  apply (rule conjI)

  apply (simp add: fresh_star_def f1)

  apply (subgoal_tac "supp T - atom ` xs = supp S - atom ` ys")

  apply (simp add: fresh_star_def f2)

  apply blast

  apply (simp add: eqv)

  done

nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys")

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

thm subst_substs_graph_def

thm subst_substs_sumC_def

oops

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

thm subst_substs_graph_def

thm subst_substs_sumC_def

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)

--"Eqvt One way"

apply(erule subst_substs_graph.induct)

apply(perm_simp)

apply(rule subst_substs_graph.intros)

apply(erule subst_substs_graph.cases)

apply(simp (no_asm_use) only: eqvts)

apply(subst test)

back

apply(assumption)

apply(rotate_tac 1)

apply(erule subst_substs_graph.cases)

apply(subst test)

back

apply(assumption)

apply(perm_simp)

apply(rule subst_substs_graph.intros)

apply(assumption)

apply(assumption)

apply(subst test)

back

apply(assumption)

apply(perm_simp)

apply(rule subst_substs_graph.intros)

apply(assumption)

apply(assumption)

apply(simp)

--"A"

apply(simp (no_asm_use) only: eqvts)

apply(subst test)

back

apply(assumption)

apply(rotate_tac 1)

apply(erule subst_substs_graph.cases)

apply(subst test)

back

apply(assumption)

apply(perm_simp)

apply(rule subst_substs_graph.intros)

apply(assumption)

apply(assumption)

apply(subst test)

back

apply(assumption)

apply(perm_simp)

apply(rule subst_substs_graph.intros)

apply(assumption)

apply(assumption)

apply(simp)

--"A"

apply(simp)

apply(erule subst_substs_graph.cases)

apply(simp (no_asm_use) only: eqvts)

apply(subst test)

back

back

apply(assumption)

apply(rule subst_substs_graph.intros)

apply (simp add: eqvts)

apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")

apply (simp add: image_eqvt eqvts_raw eqvts)

apply (simp add: fresh_star_permute_iff)

apply(perm_simp)

apply(assumption)

apply(simp (no_asm_use) only: eqvts)

apply(subst test)

back

back

apply(assumption)

apply(rule subst_substs_graph.intros)

apply (simp add: eqvts)

apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")

apply (simp add: image_eqvt eqvts_raw eqvts)

apply (simp add: fresh_star_permute_iff)

apply(perm_simp)

apply(assumption)

apply(simp)

--"Eqvt done"

apply(rule TrueI)

apply (case_tac x)

apply simp apply clarify 

apply (rule_tac y="b" in ty_tys.exhaust(1))

apply (auto)[1]

apply (auto)[1]

apply simp apply clarify 

apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))

apply (auto)[1]

apply (auto)[5]

--"LAST GOAL"

apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])

apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")

apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")

prefer 2

apply (simp add: eqvt_at_def subst_def)

apply rule

apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)")

apply (subst test2)

apply (drule_tac x="(\<theta>', T)" in meta_spec)

apply assumption

apply simp

--"We require that for Inl it returns Inl. It doesn't work for undefined, but it does work for the following"

 apply (subgoal_tac "\<And>y. \<exists>z. (\<lambda>x. THE_default (sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined) x) (subst_substs_graph x)) (Inl y) = (Inl z)")

prefer 2

apply (simp add: THE_default_def)

apply (case_tac "Ex1 (subst_substs_graph (Inl y))")

prefer 2

apply simp

apply (simp add: the1_equality)

apply auto[1]

apply (erule_tac x="x" in allE)

apply simp

apply(cases rule: subst_substs_graph.cases)

apply assumption

apply (rule_tac x="lookup \<theta> X" in exI)

apply clarify

apply (rule the1_equality)

apply metis apply assumption

apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))

                  (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)

apply clarify

apply (rule the1_equality)

apply metis apply assumption

apply clarify

--"This is exactly the assumption for the properly defined function"

defer

apply clarify

  apply (frule supp_eqvt_at)

  apply (simp add: finite_supp)

  apply (erule Abs_res_fcb)

  apply (simp add: Abs_fresh_iff)

  apply (simp add: Abs_fresh_iff)

  apply auto[1]

  apply (simp add: fresh_def fresh_star_def)

  apply (erule contra_subsetD)

  apply (simp add: supp_Pair)

  apply blast

  apply clarify

  apply (simp)

  apply (simp add: eqvt_at_def)

  apply (subst Abs_eq_iff)

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

  apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")

  apply (simp add: alphas fresh_star_zero)

  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")

  apply blast

  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")

  apply (simp add: supp_Pair eqvts eqvts_raw)

  apply auto[1]

  apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")

  apply (simp add: fresh_star_def fresh_def)

  apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])

  apply (simp add: eqvts eqvts_raw)

  apply (simp add: fresh_star_def fresh_def)

  apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric])

  apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")

  apply (erule subsetD)

  apply (simp add: supp_eqvt)

  apply (metis le_eqvt permute_boolI)

  apply (rule perm_supp_eq)

  apply (simp add: fresh_def fresh_star_def)

  apply blast

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

  by (induct Ts T rule: lookup2.induct) simp_all

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

  unfolding eqvt_def subst_graph_def

  apply (rule, perm_simp, rule)

  apply(rule TrueI)

  apply(case_tac x)

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

  apply(blast)

  apply(blast)

  apply(simp_all add: ty2.distinct)

  done

termination

  by (relation "measure (size o snd)") (simp_all add: ty2.size)

lemma subst_eqvt[eqvt]:

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

  by (induct \<theta> T rule: subst.induct) (simp_all add: lookup2_eqvt)

lemma supp_fun_app2_eqvt:

  assumes e: "eqvt f"

  shows "supp (f a b) \<subseteq> supp a \<union> supp b"

  using supp_fun_app_eqvt[OF e] supp_fun_app

  by blast

lemma supp_subst:

  "supp (subst \<theta> t) \<subseteq> supp \<theta> \<union> supp t"

  apply (rule supp_fun_app2_eqvt)

  unfolding eqvt_def by (simp add: eqvts_raw)

lemma fresh_star_inter1:

  "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"

  unfolding fresh_star_def by blast

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

  unfolding eqvt_def substs_graph_def

  apply (rule, perm_simp, rule)

  apply auto[2]

  apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)

  apply auto

  apply (erule Abs_res_fcb)

  apply (simp add: Abs_fresh_iff)

  apply (simp add: Abs_fresh_iff)

  apply auto[1]

  apply (simp add: fresh_def fresh_star_def)

  apply (rule contra_subsetD[OF  supp_subst])

  apply simp

  apply blast

  apply clarify

  apply (simp add: subst_eqvt)

  apply (subst Abs_eq_iff)

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

  apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")

  apply (simp add: alphas fresh_star_zero)

  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")

  apply blast

  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")

  apply (simp add: supp_Pair eqvts eqvts_raw)

  apply auto[1]

  apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")

  apply (simp add: fresh_star_def fresh_def)

  apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])

  apply (simp add: eqvts eqvts_raw)

  apply (simp add: fresh_star_def fresh_def)

  apply (drule subsetD[OF supp_subst])

  apply (simp add: supp_Pair)

  apply (rule perm_supp_eq)

  apply (simp add: fresh_def fresh_star_def)

  apply blast

  done

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