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

thm ty_tys.distinct

thm ty_tys.induct

thm ty_tys.inducts

thm ty_tys.exhaust 

thm 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

section {* defined as two separate nominal datatypes *}

nominal_datatype ty2 =

  Var2 "name"

| Fun2 "ty2" "ty2"

nominal_datatype tys2 =

  All2 xs::"name fset" ty::"ty2" binds (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

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