--- a/Nominal/TySch.thy	Wed Mar 17 11:20:24 2010 +0100
+++ b/Nominal/TySch.thy	Wed Mar 17 11:40:58 2010 +0100
@@ -1,99 +1,123 @@
 theory TySch
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+imports "Parser" "../Attic/Prove"
 begin
 
 atom_decl name
 
-text {* type schemes *}
-datatype ty =
-  Var "name"
-| Fun "ty" "ty"
+ML {* val _ = cheat_fv_rsp := false *}
+ML {* val _ = cheat_const_rsp := false *}
+ML {* val _ = cheat_equivp := false *}
+ML {* val _ = cheat_fv_eqvt := false *}
+ML {* val _ = cheat_alpha_eqvt := false *}
+ML {* val _ = recursive := false  *}
 
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.ty") 1 *}
-print_theorems
-
-datatype tyS =
-  All "name set" "ty"
+nominal_datatype t =
+  Var "name"
+| Fun "t" "t"
+and tyS =
+  All xs::"name set" ty::"t" bind xs in ty
 
-lemma support_image: "supp (atom ` (s :: (('a :: at) set))) = supp s"
-apply (simp add: supp_def)
-apply (simp add: eqvts eqvts_raw)
-(* apply (metis COMBC_def Collect_def Collect_mem_eq atom_name_def_raw finite finite_imageI obtain_at_base rangeI)*)
-sorry
+thm t_tyS_fv
+thm t_tyS_inject
+thm t_tyS_bn
+thm t_tyS_perm
+thm t_tyS_induct
+thm t_tyS_distinct
 
-lemma atom_image_swap_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at) set); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
-apply (simp add: fresh_def)
-apply (simp add: support_image)
-apply (fold fresh_def)
-apply (simp add: swap_fresh_fresh)
-done
-
-lemma "\<lbrakk>a \<sharp> atom ` fun; a \<sharp> t; b \<sharp> atom ` fun; b \<sharp> t\<rbrakk> \<Longrightarrow> All ((a \<rightleftharpoons> b) \<bullet> fun) t = All fun t"
-apply (simp add: atom_image_swap_fresh)
+lemma supports:
+  "(supp (atom i)) supports (Var i)"
+  "(supp A \<union> supp M) supports (Fun A M)"
+apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh t_tyS_perm)
+apply clarify
+apply(simp_all add: fresh_atom)
 done
 
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *}
-print_theorems
+lemma fs:
+  "finite (supp (x\<Colon>t)) \<and> finite (supp (z\<Colon>tyS))"
+apply(induct rule: t_tyS_induct)
+apply(rule supports_finite)
+apply(rule supports)
+apply(simp add: supp_atom)
+apply(rule supports_finite)
+apply(rule supports)
+apply(simp add: supp_atom)
+sorry
 
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty")
- [[[[]], [[], []]]] *}
-print_theorems
+instance t and tyS :: fs
+apply default
+apply (simp_all add: fs)
+sorry
+
+(* Should be moved to a proper place *)
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
 
-(*
-Doesnot work yet since we do not refer to fv_ty
-local_setup {* define_raw_fv (Datatype.the_info @{theory} "TySch.tyS") [[[[], []]]] *}
-print_theorems
-*)
-
-primrec
-  fv_tyS
-where
-  "fv_tyS (All xs T) = (fv_ty T - atom ` xs)"
-
-inductive
-  alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
-where
-  a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2))
-        \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
+lemma supp_fv_t_tyS:
+  shows "supp T = fv_t T" 
+  and   "supp S = fv_tyS S"
+apply(induct T and S rule: t_tyS_inducts)
+apply(simp_all add: t_tyS_fv)
+(* VarTS case *)
+apply(simp only: supp_def)
+apply(simp only: t_tyS_perm)
+apply(simp only: t_tyS_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+(* FunTS case *)
+apply(simp only: supp_def)
+apply(simp only: t_tyS_perm)
+apply(simp only: t_tyS_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+(* All case *)
+apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: t_tyS_perm)
+apply(simp only: permute_ABS)
+apply(simp only: t_tyS_inject)
+apply(simp only: Abs_eq_iff)
+apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(simp only: supp_Abs)
+done
 
 lemma
-  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
-  apply(rule a1)
+  shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
+  apply(simp add: t_tyS_inject)
+  apply(rule_tac x="0::perm" in exI)
   apply(simp add: alpha_gen)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: fresh_star_def)
+  apply(auto)
+  apply(simp add: fresh_star_def fresh_zero_perm)
   done
 
 lemma
-  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
-  apply(rule a1)
-  apply(simp add: alpha_gen)
+  shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))"
+  apply(simp add: t_tyS_inject)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: fresh_star_def)
+  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts)
+  apply auto
   done
 
 lemma
-  shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
-  apply(rule a1)
-  apply(simp add: alpha_gen)
+  shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))"
+  apply(simp add: t_tyS_inject)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: fresh_star_def)
-  done
+  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject)
+oops
 
 lemma
   assumes a: "a \<noteq> b"
-  shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
+  shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))"
   using a
+  apply(simp add: t_tyS_inject)
   apply(clarify)
-  apply(erule alpha_tyS.cases)
-  apply(simp add: alpha_gen)
-  apply(erule conjE)+
-  apply(erule exE)
-  apply(erule conjE)+
-  apply(clarify)
-  apply(simp)
-  apply(simp add: fresh_star_def)
-  apply(auto)
+  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject)
+  apply auto
   done