--- a/Nominal/Rsp.thy	Wed Mar 17 11:53:56 2010 +0100
+++ b/Nominal/Rsp.thy	Wed Mar 17 11:54:22 2010 +0100
@@ -186,7 +186,7 @@
   (split_conjs THEN_ALL_NEW TRY o resolve_tac
     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
   THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt))
+  asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt))
 *}
 
 ML {*

--- a/Nominal/Term5.thy	Wed Mar 17 11:53:56 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 17 11:54:22 2010 +0100
@@ -50,7 +50,7 @@
 (*lemma alpha5_eqvt:
   "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and>
   (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and>
-  (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"
+  (alpha_rbv5 b c \<longrightarrow> alpha_rbv5 (p \<bullet> b) (p \<bullet> c))"
 apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *})
 done*)
 
@@ -75,10 +75,21 @@
 apply (simp_all add: alpha5_inj)
 apply (erule exE)
 apply (rule_tac x="- pi" in exI)
+apply (simp add: alpha_gen)
+  apply(simp add: fresh_star_def fresh_minus_perm)
 apply clarify
 apply (rule conjI)
-apply (erule_tac [!] alpha_gen_compose_sym)
-apply (simp_all add: alpha5_eqvt)
+apply (rotate_tac 3)
+apply (frule_tac p="- pi" in alpha5_eqvt(2))
+apply simp
+apply (rule conjI)
+apply (rotate_tac 5)
+apply (frule_tac p="- pi" in alpha5_eqvt(1))
+apply simp
+apply (rotate_tac 6)
+apply simp
+apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])
+apply (simp)
 done
 
 lemma alpha5_transp:
@@ -94,19 +105,29 @@
 apply (simp_all add: alpha5_inj)
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
-apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
-apply clarify
-apply (rule conjI)
-apply (erule alpha_gen_compose_trans)
-apply (assumption)
-apply (simp add: alpha5_eqvt)
-apply (erule alpha_gen_compose_trans)
-apply (assumption)
-apply (simp add: alpha5_eqvt)
+defer
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
+apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
+apply (simp add: alpha_gen)
+apply clarify
+apply(simp add: fresh_star_plus)
+apply (rule conjI)
+apply (erule_tac x="- pi \<bullet> rltsaa" in allE)
+apply (rotate_tac 5)
+apply (drule_tac p="- pi" in alpha5_eqvt(2))
+apply simp
+apply (drule_tac p="pi" in alpha5_eqvt(2))
+apply simp
+apply (erule_tac x="- pi \<bullet> rtrm5aa" in allE)
+apply (rotate_tac 7)
+apply (drule_tac p="- pi" in alpha5_eqvt(1))
+apply simp
+apply (rotate_tac 3)
+apply (drule_tac p="pi" in alpha5_eqvt(1))
+apply simp
 done
 
 lemma alpha5_equivp:
@@ -146,7 +167,7 @@
   apply(simp_all add: eqvts)
   apply(simp add: alpha_gen)
   apply(clarify)
-  apply(simp)
+  apply blast
 done
 
 lemma bv_list_rsp:
@@ -234,20 +255,25 @@
 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
 lemmas bv5[simp] = rbv5.simps[quot_lifted]
 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
-lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen]
 lemmas alpha5_DIS = alpha_dis[quot_lifted]
 
+(* why is this not in Isabelle? *)
+lemma set_sub: "{a, b} - {b} = {a} - {b}"
+by auto
+
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
-apply (simp only: alpha5_INJ)
-apply (simp only: bv5)
+apply (simp only: alpha5_INJ bv5)
 apply simp
 apply (rule allI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts)
 apply (rule impI)
 apply (rule impI)
-sorry (* The assumption is false, so it is true *)
+apply (rule impI)
+apply (simp add: set_sub)
+done
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
@@ -256,6 +282,7 @@
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
+apply (simp add: eqvts)
 done
 
 lemma lets_ok3:

--- a/Nominal/Term5a.thy	Wed Mar 17 11:53:56 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-theory Term5
-imports "Parser"
-begin
-
-atom_decl name
-
-ML {* restricted_nominal := 2 *}
-
-nominal_datatype trm5 =
-  Vr5 "name"
-| Ap5 "trm5" "trm5"
-| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
-and lts =
-  Lnil
-| Lcons "name" "trm5" "lts"
-binder
-  bv5
-where
-  "bv5 Lnil = {}"
-| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
-
-lemma lets_ok:
-  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-apply (simp add: trm5_lts_inject)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp_all add: alpha_gen)
-apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn)
-done
-
-lemma lets_nok:
-  "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))"
-apply (simp only: trm5_lts_inject not_ex)
-apply (rule allI)
-apply (simp add: alpha_gen)
-apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject)
-done
-
-end

--- a/Nominal/Term5n.thy	Wed Mar 17 11:53:56 2010 +0100
+++ b/Nominal/Term5n.thy	Wed Mar 17 11:54:22 2010 +0100
@@ -53,10 +53,34 @@
 build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac  @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *}
 print_theorems
 
+lemma alpha5_reflp:
+"y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 x x)"
+apply (rule rtrm5_rlts.induct)
+apply (simp_all add: alpha5_inj)
+apply (rule_tac x="0::perm" in exI)
+apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
+done
+
+lemma alpha5_symp:
+"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
+(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
+(alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
+sorry
+
+lemma alpha5_transp:
+"(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>
+(x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>
+(alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))"
+sorry
+
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"
   "equivp alpha_rlts"
-  sorry
+  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+  apply (simp_all only: alpha5_reflp)
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
 
 quotient_type
   trm5 = rtrm5 / alpha_rtrm5
@@ -96,14 +120,34 @@
   apply simp
   done
 
-lemma alpha_rbv5_rsp: "xa \<approx>l y \<Longrightarrow> xb \<approx>l ya \<Longrightarrow> alpha_rbv5 xa xb = alpha_rbv5 y ya"
+local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
+print_theorems
+
+lemma alpha_rbv_rsp_pre:
+  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z"
   apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (simp_all)
-  defer defer (* should follow from distinctness *)
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply (case_tac [!] z)
+  apply (simp_all add: alpha_dis alpha5_inj)
   apply clarify
-  apply (simp add: alpha5_inj)
-  sorry (* should be true? *)
+  apply auto
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
+
+lemma alpha_rbv_rsp_pre2:
+  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y"
+  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply (case_tac [!] z)
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply auto
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
 
 lemma [quot_respect]:
   "(alpha_rlts ===> op =) fv_rlts fv_rlts"
@@ -117,12 +161,8 @@
   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
   "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"
-  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv5_rsp)
+  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv_rsp_pre alpha_rbv_rsp_pre2 alpha5_reflp)
   apply (clarify)
-  apply (rule conjI)
-  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (simp_all add: alpha5_inj)
-  apply clarify
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
 done
 
@@ -168,7 +208,7 @@
 apply (simp add: alpha5_INJ)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
+apply (simp add: permute_trm5_lts fresh_star_def eqvts)
 done
 
 lemma lets_ok3:
@@ -185,6 +225,7 @@
 apply (simp add: alpha5_INJ alpha_gen)
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts)
+apply blast
 done
 
 lemma distinct_helper:

--- a/Nominal/TySch.thy	Wed Mar 17 11:53:56 2010 +0100
+++ b/Nominal/TySch.thy	Wed Mar 17 11:54:22 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