theory TypeSchemes
imports "../Nominal2"
begin

section {*** Type Schemes ***}

nominal_datatype 
  A = Aa bool | Ab B
and 
  B = Ba bool | Bb A

lemma
  "(p \<bullet> (Sum_Type.Projl (f (Inl x)))) = Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> x)))"
apply(perm_simp)
apply(subst permute_fun_def)
sorry


nominal_primrec
    even :: "nat \<Rightarrow> A"
and odd  :: "nat \<Rightarrow> B"
where
  "even 0 = Aa True"
| "even (Suc n) = Ab (odd n)"
| "odd 0 = Ba False"
| "odd (Suc n) = Bb (even n)"
thm even_odd_graph.intros even_odd_sumC_def
thm sum.cases Product_Type.split
thm even_odd_graph_def 
term Inr
term Sum_Type.Projr
term even_odd_sumC
thm even_odd_sumC_def
unfolding even_odd_sumC_def
sorry

ML {* the *}

thm even.psimps odd.psimps



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
  "(p \<bullet> (Sum_Type.Projl x)) = Sum_Type.Projl (p \<bullet> x)"
apply(case_tac x)
apply(simp)
apply(simp)


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
thm subst_substs_sumC_def
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)
thm subst_substs_graph.cases
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)
defer
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)
defer
apply(perm_simp)
apply(assumption)
apply(simp)
apply(simp_all add: ty_tys.distinct)
defer
apply(simp add: ty_tys.eq_iff)
apply(simp add: ty_tys.eq_iff)
apply(erule conjE)+
apply(simp add: ty_tys.eq_iff)
apply(subst (asm) Abs_eq_iff2)
apply(erule exE)
apply(simp add: alphas)
apply(clarify)
thm subst_def


apply(assumption)
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)


apply(rotate_tac 1)
apply(erule subst_substs_graph.cases)
apply(subst test)
back
apply(assumption)


apply(auto)[4]
thm  subst_substs_graph.cases
thm subst_substs_graph.intros
thm subst_substs_graph.intros(2)[THEN permute_boolI]
term subst_substs_graph
apply(simp only: eqvts)
thm Projl.simps
term Inl
term Inr
apply(perm_simp)
thm subst_substs_graph.intros
apply(simp add: permute_fun_def)
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