--- a/Nominal/Ex/Foo1.thy	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Mon Dec 06 16:35:42 2010 +0000
@@ -55,43 +55,6 @@
 thm foo.fresh
 thm foo.bn_finite
 
-lemma uu1:
-  shows "alpha_bn1 as (permute_bn1 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(auto)
-done
-
-lemma uu2:
-  shows "alpha_bn2 as (permute_bn2 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(auto)
-done
-
-lemma uu3:
-  shows "alpha_bn3 as (permute_bn3 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(auto)
-done
-
-lemma uu4:
-  shows "alpha_bn4 as (permute_bn4 p as)"
-apply(induct as rule: foo.inducts(3))
-apply(auto)[8]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-done
-
 
 lemma tt1:
   shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)"
@@ -129,30 +92,6 @@
 apply(simp add: atom_eqvt insert_eqvt)
 done
 
-
-lemma Let1_rename:
-  assumes "supp ([bn1 assn]lst. trm) \<sharp>* p"
-  shows "Let1 assn trm = Let1 (permute_bn1 p assn) (p \<bullet> trm)"
-using assms
-apply -
-apply(drule supp_perm_eq[symmetric])
-apply(simp only: permute_Abs)
-apply(simp only: tt1)
-apply(simp only: foo.eq_iff)
-apply(rule conjI)
-apply(rule refl)
-apply(rule uu1)
-done
-
-lemma Let1_rename_a:
-  fixes c::"'a::fs"
-  assumes "y =  Let1 assn trm"
-  shows "\<exists>p. (p \<bullet> (set (bn1 assn))) \<sharp>* c \<and> y = Let1 (permute_bn1 p assn) (p \<bullet> trm)"
-using assms
-apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric])
-apply(simp del: permute_Abs)
-sorry
-
 lemma strong_exhaust1:
   fixes c::"'a::fs"
   assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
@@ -163,60 +102,7 @@
   and     "\<exists>(c::'a::fs) assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P"
   and     "\<exists>(c::'a::fs) assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P"
   shows "P"
-apply(rule_tac y="y" in foo.exhaust(1))
-apply(rule assms(1))
-apply(rule exI)
-apply(assumption)
-apply(rule assms(2))
-apply(rule exI)+
-apply(assumption)
-apply(rule assms(3))
-apply(subgoal_tac "\<exists>p::perm. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
-apply(erule exE)
-apply(perm_simp)
-apply(rule_tac exI)+
-apply(rule conjI)
-apply(simp add: fresh_star_prod)
-apply(erule conjE)+
-apply(assumption)
-apply(simp)
-apply(simp add: foo.eq_iff)
-(* HERE *)
-defer
-defer
-apply(rule assms(4))
-apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn1 assg))) \<sharp>* (c, assg, trm)")
-apply(erule exE)
-apply(perm_simp add: tt1)
-apply(simp only: fresh_star_prod)
-apply(erule conjE)+
-apply(rule_tac exI)+
-apply(rule conjI)
-apply(assumption)
-apply(simp add: foo.eq_iff)
-apply(rule conjI)
-apply(simp only: tt1[symmetric])
-defer
-apply(rule uu1)
-defer
-apply(rule assms(5))
-apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn2 assg))) \<sharp>* (c, assg, trm)")
-apply(erule exE)
-apply(perm_simp add: tt2)
-apply(simp only: fresh_star_prod)
-apply(erule conjE)+
-apply(rule_tac exI)+
-apply(rule conjI)
-apply(assumption)
-apply(simp add: foo.eq_iff)
-apply(rule conjI)
-apply(simp only: tt2[symmetric])
-defer
-apply(rule uu2)
-defer
-apply(rule refl)
-apply(subst (asm) fresh_star_supp_conv)
-apply(simp)
+oops
 
 
 lemma strong_exhaust2:
@@ -229,89 +115,7 @@
   and     "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
   and     "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P"
   shows "P"
-apply(rule strong_exhaust1[where y="y"])
-apply(erule exE)+
-apply(rule assms(1))
-apply(assumption)
-apply(erule exE)+
-apply(rule assms(2))
-apply(assumption)
-apply(erule exE | erule conjE)?
-apply(rule assms(3))
-apply(drule_tac x="c" in spec)
-apply(erule exE | erule conjE)+
-apply(assumption)+
-apply(drule_tac x="c" in spec)
-apply(erule exE | erule conjE)+
-apply(assumption)+
-apply(erule exE | erule conjE)+
-apply(rule assms(4))
-apply(assumption)+
-apply(erule exE | erule conjE)+
-apply(rule assms(5))
-apply(assumption)+
-apply(erule exE | erule conjE)+
-apply(rule assms(6))
-apply(assumption)+
-apply(erule exE | erule conjE)+
-apply(rule assms(7))
-apply(assumption)+
-done
-
-
-
-
-
-
-
-
-
-
-
-
-apply(rule_tac y="y" in foo.exhaust(1))
-apply(rule assms(1))
-apply(rule exI)
-apply(assumption)
-apply(rule assms(2))
-apply(rule exI)+
-apply(assumption)
-apply(rule assms(3))
-apply(rule_tac p="p" in permute_boolE)
-apply(perm_simp)
-apply(simp)
-apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(3))
-apply(perm_simp)
-apply(assumption)
-apply(simp)
-apply(drule supp_perm_eq[symmetric])
-apply(perm_simp)
-apply(simp)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: foo.fresh fresh_star_def)
-apply(drule Let1_rename_a)
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(4))
-apply(simp only: set_eqvt tt1)
-apply(assumption)
-(*
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-*)
-thm assms(5)
-apply(rule assms(5))
-prefer 2
-apply(clarify)
-unfolding foo.eq_iff
-apply
+oops
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
@@ -323,95 +127,7 @@
   and     "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
   and     "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P"
   shows "P"
-apply(rule_tac y="y" in foo.exhaust(1))
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)
-apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(3))
-apply(perm_simp)
-apply(assumption)
-apply(simp)
-apply(drule supp_perm_eq[symmetric])
-apply(perm_simp)
-apply(simp)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: foo.fresh fresh_star_def)
-apply(drule Let1_rename_a)
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(4))
-apply(simp only: set_eqvt tt1)
-apply(assumption)
-(*
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-*)
-thm assms(5)
-apply(rule assms(5))
-prefer 2
-apply(clarify)
-unfolding foo.eq_iff
-apply(rule conjI)
-prefer 2
-apply(rule uu2)
-apply(simp only: tt2[symmetric])
-prefer 2
-apply(simp only: tt2[symmetric])
-
-apply(simp_all only:)[2]
-apply(simp add: set_eqvt)
-apply(simp add: tt2)
-apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(simp add: tt2 uu2)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: Abs_fresh_star)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn3 assg))) \<sharp>* c \<and> supp ([bn3 assg]lst.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(6))
-apply(simp add: set_eqvt)
-apply(simp add: tt3)
-apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(simp add: tt3 uu3)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: Abs_fresh_star)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (bn4 assg')) \<sharp>* c \<and> supp ([bn4 assg']set.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(7))
-apply(simp add: tt4)
-apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(simp add: tt4 uu4)
-apply(rule at_set_avoiding2)
-apply(simp add: foo.bn_finite)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: Abs_fresh_star)
-done
-
-thm strong_exhaust1 foo.exhaust(1)
-
-
+oops 
 
 lemma strong_exhaust2:
   assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" 
@@ -448,6 +164,8 @@
   and     a9: "\<And>c. P3 c (BNil)"
   and     a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)"
   shows "P1 c t" "P2 c as" "P3 c as'"
+oops
+(*
 using assms
 apply(induction_schema)
 apply(rule_tac y="t" and c="c" in strong_exhaust1)
@@ -459,6 +177,7 @@
 apply(relation "measure (sum_case (size o snd) (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z))))")
 apply(simp_all add: foo.size)
 done
+*)
 
 end
 

--- a/Nominal/Ex/Foo2.thy	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Mon Dec 06 16:35:42 2010 +0000
@@ -43,17 +43,6 @@
 thm foo.supp
 thm foo.fresh
 
-lemma uu1:
-  shows "alpha_bn as (permute_bn p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[5]
-apply(simp only: foo.perm_bn_simps)
-apply(simp only: foo.eq_iff)
-apply(simp only: foo.perm_bn_simps)
-apply(simp only: foo.eq_iff refl)
-apply(simp)
-done
-
 lemma tt1:
   shows "(p \<bullet> bn as) = bn (permute_bn p as)"
 apply(induct as rule: foo.inducts(2))
@@ -286,10 +275,10 @@
 apply(rule conjI)
 apply(assumption)
 apply(rule conjI)
-apply(rule uu1)
+apply(rule foo.perm_bn_alpha)
 apply(rule conjI)
 apply(assumption)
-apply(rule uu1)
+apply(rule foo.perm_bn_alpha)
 apply(rule at_set_avoiding1)
 apply(simp)
 apply(simp add: finite_supp)
@@ -348,7 +337,6 @@
 apply(erule exE)+
 apply(rule assms(2))
 apply(assumption)
-apply(erule exE)+
 apply(rule assms(3))
 apply(auto)[2]
 apply(erule exE)+

--- a/Nominal/Ex/Multi_Recs2.thy	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Mon Dec 06 16:35:42 2010 +0000
@@ -69,34 +69,6 @@
 thm fun_recs.fsupp
 thm fun_recs.supp
 
-term alpha_b_fnclause
-term alpha_b_fnclauses
-term alpha_b_lrb
-term alpha_b_lrbs
-term alpha_b_pat
-
-term alpha_b_fnclause_raw
-term alpha_b_fnclauses_raw
-term alpha_b_lrb_raw
-term alpha_b_lrbs_raw
-term alpha_b_pat_raw
-
-lemma uu1:
-  fixes as0::exp  and as1::fnclause
-  shows "(\<lambda>x::exp. True) (as0::exp)"
-  and   "alpha_b_fnclause as1 (permute_b_fnclause p as1)"
-  and   "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)"
-  and   "alpha_b_lrb as3 (permute_b_lrb p as3)"
-  and   "alpha_b_lrbs as4 (permute_b_lrbs p as4)"
-  and   "alpha_b_pat as5 (permute_b_pat p as5)"
-apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts)
-apply(simp_all)
-apply(simp only: fun_recs.perm_bn_simps)
-apply(simp only: fun_recs.eq_iff)
-apply(simp)
-oops
-
-
 thm fun_recs.distinct
 thm fun_recs.induct
 thm fun_recs.inducts

--- a/Nominal/Nominal2.thy	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/Nominal2.thy	Mon Dec 06 16:35:42 2010 +0000
@@ -265,8 +265,6 @@
     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
-  val _ = tracing ("raw_bn_funs\n" ^ cat_lines (map (@{make_string} o #1) raw_bn_funs))
- 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
 
@@ -309,12 +307,6 @@
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
     else raise TEST lthy3
 
-  (*
-  val _ = tracing ("RAW_BNS\n" ^ cat_lines (map (Syntax.string_of_term lthy3) raw_bns))
-  val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map (Syntax.string_of_term lthy3 o #1) raw_bn_info))
-  val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map @{make_string} raw_bn_info))
-  *)
-
   (* defining the permute_bn functions *)
   val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = 
     if get_STEPS lthy3a > 2
@@ -493,14 +485,6 @@
   val qalpha_bns_descr = 
     map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
 
-  (*
-  val _ = tracing ("raw_bn_info\n" ^ cat_lines (map (Syntax.string_of_term lthy7 o #1) raw_bn_info))
-  val _ = tracing ("bn_funs\n" ^ cat_lines (map (@{make_string} o #1) bn_funs))
-  val _ = tracing ("raw_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_bns))
-  val _ = tracing ("raw_fv_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_fv_bns))
-  val _ = tracing ("alpha_bn_trms\n" ^ cat_lines (map (Syntax.string_of_term lthy7) alpha_bn_trms))
-  *)
-
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
 
@@ -559,7 +543,7 @@
       ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
     else raise TEST lthy9a
 
-  val (((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), lthyB) = 
+  val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = 
     if get_STEPS lthy > 28
     then
       lthyA 
@@ -568,6 +552,7 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
       ||>> lift_thms qtys [] raw_size_thms
       ||>> lift_thms qtys [] raw_perm_bn_simps
+      ||>> lift_thms qtys [] alpha_refl_thms
     else raise TEST lthyA
 
   val qinducts = Project_Rule.projections lthyA qinduct
@@ -626,11 +611,11 @@
     else []
 
   (* proving that perm_bns preserve alpha *)
-  val qperm_bn_alpha_thms = @{thms TrueI}
-  (*  if get_STEPS lthy > 33
-    then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' lthyC
-    else []*)
-
+  val qperm_bn_alpha_thms = 
+    if get_STEPS lthy > 33
+    then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' 
+      qalpha_refl_thms lthyC
+    else []
 
   (* noting the theorems *)  
 

--- a/Nominal/nominal_dt_alpha.ML	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Mon Dec 06 16:35:42 2010 +0000
@@ -247,8 +247,6 @@
       (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
     val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
 
-    val _ = tracing ("alpha in def\n" ^ cat_lines (map (@{make_string} o fst o #1) all_alpha_names))
-
     val (alphas, lthy') = Inductive.add_inductive_i
        {quiet_mode = true, verbose = false, alt_name = Binding.empty,
         coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}

--- a/Nominal/nominal_dt_supp.ML	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML	Mon Dec 06 16:35:42 2010 +0000
@@ -18,7 +18,7 @@
 
   val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
   val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
-    Proof.context -> thm list
+    thm list -> Proof.context -> thm list
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -204,7 +204,7 @@
     induct_prove qtys props qinduct (K ss_tac) ctxt
   end
 
-fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs ctxt =
+fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt =
   let 
     val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
     val p = Free (p, @{typ perm})
@@ -218,12 +218,11 @@
 
     val props = map2 mk_goal qperm_bns alpha_bns
     val ss_tac = (K (print_tac "test")) THEN' 
-      asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs))
+      asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls))
   in
-    @{thms TrueI}
-    (*induct_prove qtys props qinduct (K ss_tac) ctxt'
+    induct_prove qtys props qinduct (K ss_tac) ctxt'
     |> ProofContext.export ctxt' ctxt
-    |> map (simplify (HOL_basic_ss addsimps @{thms id_def}))*)
+    |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
   end