# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274880894 -7200
# Node ID 9fb315392493f8d1d6905ebe6ecb0d323c3f0068
# Parent  09bbed4f21d68550156c3177a8ee3f7f70f94ab8
added FSet to the correct paper

diff -r 09bbed4f21d6 -r 9fb315392493 Nominal/Equivp.thy
--- a/Nominal/Equivp.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/Equivp.thy	Wed May 26 15:34:54 2010 +0200
@@ -340,28 +340,6 @@
 
 
 
-ML {*
-fun build_eqvt_gl pi frees fnctn ctxt =
-let
-  val typ = domain_type (fastype_of fnctn);
-  val arg = the (AList.lookup (op=) frees typ);
-in
-  ([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt)
-end
-*}
 
-ML {*
-fun prove_eqvt tys ind simps funs ctxt =
-let
-  val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
-  val pi = Free (pi, @{typ perm});
-  val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'))
-  val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
-  val ths = Variable.export ctxt' ctxt ths_loc
-  val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
-in
-  (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
-end
-*}
 
 end
diff -r 09bbed4f21d6 -r 9fb315392493 Nominal/Ex/Ex2.thy
--- a/Nominal/Ex/Ex2.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/Ex/Ex2.thy	Wed May 26 15:34:54 2010 +0200
@@ -3,6 +3,7 @@
 begin
 
 text {* example 2 *}
+declare [[STEPS = 8]]
 
 atom_decl name
 
@@ -21,6 +22,13 @@
   "f PN = {}"
 | "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
+
+thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars]
+thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
+
+
+
+
 thm trm_pat.bn
 thm trm_pat.perm
 thm trm_pat.induct
diff -r 09bbed4f21d6 -r 9fb315392493 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/NewParser.thy	Wed May 26 15:34:54 2010 +0200
@@ -287,12 +287,6 @@
 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 ML {* val cheat_supp_eq = Unsynchronized.ref false *}
 
-ML {*
-fun remove_loop t =
-  let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end
-  handle TERM _ => @{thm eqTrueI} OF [t]
-*}
-
 
 ML {*
 (* for testing porposes - to exit the procedure early *)
@@ -305,7 +299,69 @@
 
 setup STEPS_setup
 
-ML {* dtyp_no_of_typ *}
+ML {*
+fun mk_conjl props =
+  fold (fn a => fn b =>
+    if a = @{term True} then b else
+    if b = @{term True} then a else
+    HOLogic.mk_conj (a, b)) (rev props) @{term True};
+*}
+
+ML {*
+val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
+
+(* Given function for buildng a goal for an input, prepares a
+   one common goals for all the inputs and proves it by induction
+   together *)
+ML {*
+fun prove_by_induct tys build_goal ind utac inputs ctxt =
+let
+  val names = Datatype_Prop.make_tnames tys;
+  val (names', ctxt') = Variable.variant_fixes names ctxt;
+  val frees = map Free (names' ~~ tys);
+  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';
+  val gls = flat gls_lists;
+  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
+  val trm_gl_lists = map trm_gls_map frees;
+  val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
+  val trm_gls = map mk_conjl trm_gl_lists;
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
+  fun tac {context,...} = (
+    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
+    THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1
+  val th_loc = Goal.prove ctxt'' [] [] gl tac
+  val ths_loc = HOLogic.conj_elims th_loc
+  val ths = Variable.export ctxt'' ctxt ths_loc
+in
+  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
+end
+*}
+
+ML {*
+fun build_eqvt_gl pi frees fnctn ctxt =
+let
+  val typ = domain_type (fastype_of fnctn);
+  val arg = the (AList.lookup (op=) frees typ);
+in
+  ([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt)
+end
+*}
+
+ML {*
+fun prove_eqvt tys ind simps funs ctxt =
+let
+  val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt;
+  val p = Free (p, @{typ perm})
+  val simp_set = @{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'
+  val tac = asm_full_simp_tac (HOL_ss addsimps simp_set)
+  val ths_loc = prove_by_induct tys (build_eqvt_gl p) ind tac funs ctxt'
+  val ths = Variable.export ctxt' ctxt ths_loc
+  val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
+in
+  (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
+end
+*}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
@@ -325,7 +381,7 @@
   val inject_thms = flat (map #inject dtinfos);
   val distinct_thms = flat (map #distinct dtinfos);
   val rel_dtinfos = List.take (dtinfos, (length dts)); 
-  val rel_distinct = map #distinct rel_dtinfos;  (* thm list list *)
+  val raw_constrs_distinct = (map #distinct rel_dtinfos); 
   val induct_thm = #induct dtinfo;
   val exhaust_thms = map #exhaust dtinfos;
 
@@ -354,24 +410,21 @@
     else raise TEST lthy3
 
   (* definition of raw alphas *)
-  val (alpha_ts, alpha_bn_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) =
+  val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
     if get_STEPS lthy > 4 
     then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a
     else raise TEST lthy3a
   
-  (* HERE *)
+  (* definition of alpha-distinct lemmas *)
+  val (alpha_distincts, alpha_bn_distincts) = 
+    mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info
+
   (* definition of raw_alpha_eq_iff  lemmas *)
-  val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) (rel_distinct ~~ alpha_ts));
-  val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
-    ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_bn_ts))
- 
   val alpha_eq_iff = 
     if get_STEPS lthy > 5
-    then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
+    then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
     else raise TEST lthy4
 
-  val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
-  
   (* proving equivariance lemmas for bns, fvs and alpha *)
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = 
@@ -386,22 +439,22 @@
 
   val (alpha_eqvt, lthy6a) =
     if get_STEPS lthy > 8
-    then Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6
+    then Nominal_Eqvt.equivariance alpha_trms alpha_induct alpha_intros lthy6
     else raise TEST lthy6
 
 
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
-  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts, alpha_bn_ts) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
+  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos;
+  val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy6a;
   val alpha_equivp =
-    if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts
-    else build_equivps alpha_ts reflps alpha_induct
-      inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a;
+    if !cheat_equivp then map (equivp_hack lthy6a) alpha_trms
+    else build_equivps alpha_trms reflps alpha_induct
+      inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy6a;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts alpha_equivp lthy6a;
+  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy6a;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>
@@ -410,7 +463,7 @@
           Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = warning "Proving respects";
-  val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
+  val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;
@@ -418,7 +471,7 @@
 
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
     else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1;
-  val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
+  val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9;
   val (fv_rsp_pre, lthy10) = fold_map
     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
     (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9;
@@ -427,12 +480,12 @@
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
     else
-      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_bn_ts lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
+      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
-    alpha_bn_rsp_tac) alpha_bn_ts lthy11
+    alpha_bn_rsp_tac) alpha_bn_trms lthy11
   fun const_rsp_tac _ =
-    let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_bn_ts lthy11a
-      in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+    let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a
+      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
     val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
@@ -440,9 +493,9 @@
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
-  val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_ts
-  val (qalpha_bn_ts, qalphabn_defs, lthy12c) = 
-    quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_ts) lthy12b;
+  val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms
+  val (qalpha_bn_trms, qalphabn_defs, lthy12c) = 
+    quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_trms) lthy12b;
   val _ = warning "Lifting permutations";
   val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
@@ -470,14 +523,14 @@
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = warning "Lifting eq-iff";
   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
-  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff_simp
+  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff
   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0
   val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded1;
   val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
-  val q_dis = map (lift_thm qtys lthy18) rel_dists;
+  val q_dis = map (lift_thm qtys lthy18) alpha_distincts;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
   val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt);
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
@@ -490,7 +543,7 @@
   val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
   fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
   val lthy22 = Class.prove_instantiation_instance tac lthy21
-  val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts, qalpha_bn_ts) bn_nos;
+  val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos;
   val (names, supp_eq_t) = supp_eq fv_alpha_all;
   val _ = warning "Support Equations";
   fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else
diff -r 09bbed4f21d6 -r 9fb315392493 Nominal/Perm.thy
--- a/Nominal/Perm.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/Perm.thy	Wed May 26 15:34:54 2010 +0200
@@ -48,33 +48,5 @@
 end
 *}
 
-ML {*
-fun neq_to_rel r neq =
-let
-  val neq = HOLogic.dest_Trueprop (prop_of neq)
-  val eq = HOLogic.dest_not neq
-  val (lhs, rhs) = HOLogic.dest_eq eq
-  val rel = r $ lhs $ rhs
-  val nrel = HOLogic.mk_not rel
-in
-  HOLogic.mk_Trueprop nrel
-end
-*}
-
-ML {*
-fun neq_to_rel_tac cases distinct =
-  rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)
-*}
-
-ML {*
-fun distinct_rel ctxt cases (dists, rel) =
-let
-  val ((_, thms), ctxt') = Variable.import false dists ctxt
-  val terms = map (neq_to_rel rel) thms
-  val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms
-in
-  Variable.export ctxt' ctxt nrels
-end
-*}
 
 end
diff -r 09bbed4f21d6 -r 9fb315392493 Nominal/Tacs.thy
--- a/Nominal/Tacs.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/Tacs.thy	Wed May 26 15:34:54 2010 +0200
@@ -17,44 +17,7 @@
 end
 *}
 
-ML {*
-fun mk_conjl props =
-  fold (fn a => fn b =>
-    if a = @{term True} then b else
-    if b = @{term True} then a else
-    HOLogic.mk_conj (a, b)) (rev props) @{term True};
-*}
 
-ML {*
-val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
-*}
-
-(* Given function for buildng a goal for an input, prepares a
-   one common goals for all the inputs and proves it by induction
-   together *)
-ML {*
-fun prove_by_induct tys build_goal ind utac inputs ctxt =
-let
-  val names = Datatype_Prop.make_tnames tys;
-  val (names', ctxt') = Variable.variant_fixes names ctxt;
-  val frees = map Free (names' ~~ tys);
-  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';
-  val gls = flat gls_lists;
-  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
-  val trm_gl_lists = map trm_gls_map frees;
-  val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
-  val trm_gls = map mk_conjl trm_gl_lists;
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
-  fun tac {context,...} = (
-    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
-    THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1
-  val th_loc = Goal.prove ctxt'' [] [] gl tac
-  val ths_loc = HOLogic.conj_elims th_loc
-  val ths = Variable.export ctxt'' ctxt ths_loc
-in
-  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
 
 ML {*
 fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =
@@ -83,41 +46,6 @@
   filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
 end
 *}
-(* Code for transforming an inductive relation to a function *)
-ML {*
-fun rel_inj_tac dist_inj intrs elims =
-  SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
-  (rtac @{thm iffI} THEN' RANGE [
-     (eresolve_tac elims THEN_ALL_NEW
-       asm_full_simp_tac (HOL_ss addsimps dist_inj)
-     ),
-     asm_full_simp_tac (HOL_ss addsimps intrs)])
-*}
-
-ML {*
-fun build_rel_inj_gl thm =
-  let
-    val prop = prop_of thm;
-    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
-    val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
-    fun list_conj l = foldr1 HOLogic.mk_conj l;
-  in
-    if hyps = [] then concl
-    else HOLogic.mk_eq (concl, list_conj hyps)
-  end;
-*}
-
-ML {*
-fun build_rel_inj intrs dist_inj elims ctxt =
-let
-  val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
-  val gls = map (HOLogic.mk_Trueprop o build_rel_inj_gl) thms_imp;
-  fun tac _ = rel_inj_tac dist_inj intrs elims 1;
-  val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
-in
-  Variable.export ctxt' ctxt thms
-end
-*}
 
 ML {*
 fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm
diff -r 09bbed4f21d6 -r 9fb315392493 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Wed May 26 15:34:54 2010 +0200
@@ -10,11 +10,18 @@
   val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
     bclause list list list -> term list -> Proof.context -> 
     term list * term list * thm list * thm list * thm * local_theory
+
+  val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> 
+    term list -> term list -> bn_info -> thm list * thm list
+
+  val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
 struct
 
+(** definition of the inductive rules for alpha and alpha_bn **)
+
 (* construct the compound terms for prod_fv and prod_alpha *)
 fun mk_prod_fv (t1, t2) =
 let
@@ -216,7 +223,7 @@
   
   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 = true, fork_mono = false}
+      coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
      all_alpha_names [] all_alpha_intros [] lthy
 
   val all_alpha_trms_loc = #preds alphas;
@@ -235,5 +242,86 @@
   (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
 end
 
+
+(** produces the distinctness theorems **)
+
+(* transforms the distinctness theorems of the constructors 
+   to "not-alphas" of the constructors *)
+fun mk_alpha_distinct_goal alpha neq =
+let
+  val (lhs, rhs) = 
+    neq
+    |> HOLogic.dest_Trueprop
+    |> HOLogic.dest_not
+    |> HOLogic.dest_eq
+in
+  alpha $ lhs $ rhs
+  |> HOLogic.mk_not
+  |> HOLogic.mk_Trueprop
+end
+
+fun distinct_tac cases distinct_thms =
+  rtac notI THEN' eresolve_tac cases 
+  THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
+
+fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) =
+let
+  val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt
+  val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms
+  val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals
+in
+  Variable.export ctxt' ctxt nrels
+end
+
+fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos =
+let
+  val alpha_distincts = 
+    map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms)
+  val distinc_thms = map 
+  val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos
+  val alpha_bn_distincts =  
+    map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_trms)
+in
+  (flat alpha_distincts, flat alpha_bn_distincts)
+end
+
+
+(** produces the alpha_eq_iff simplification rules **)
+
+(* in case a theorem is of the form (C.. = C..), it will be
+   rewritten to ((C.. = C..) = True) *)
+fun mk_simp_rule thm =
+  case (prop_of thm) of
+    @{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm]
+  | _ => thm
+
+fun alpha_eq_iff_tac dist_inj intros elims =
+  SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE'
+  (rtac @{thm iffI} THEN' 
+    RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj),
+           asm_full_simp_tac (HOL_ss addsimps intros)])
+
+fun mk_alpha_eq_iff_goal thm =
+  let
+    val prop = prop_of thm;
+    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
+    val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
+    fun list_conj l = foldr1 HOLogic.mk_conj l;
+  in
+    if hyps = [] then HOLogic.mk_Trueprop concl
+    else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
+  end;
+
+fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =
+let
+  val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
+  val goals = map mk_alpha_eq_iff_goal thms_imp;
+  val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1;
+  val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
+in
+  Variable.export ctxt' ctxt thms
+  |> map mk_simp_rule
+end
+
 end (* structure *)
 
diff -r 09bbed4f21d6 -r 9fb315392493 Slides/Slides1.thy
--- a/Slides/Slides1.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Slides/Slides1.thy	Wed May 26 15:34:54 2010 +0200
@@ -23,7 +23,7 @@
   \large General Bindings\\[15mm]
   \end{tabular}}
   \begin{center}
-  joint work with {\bf Cezary} and Brian Huffman\\[0mm] 
+  joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] 
   \end{center}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -33,10 +33,28 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1>
+  \begin{frame}<1-2>
   \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
   \mbox{}\\[-3mm]
 
+  \begin{itemize}
+  \item sorted atoms and sort-respecting permutations\medskip
+
+  \onslide<2->{
+  \item[] in old Nominal: atoms have dif\!ferent type
+
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{7mm}}c}
+  $[] \act c \dn c$ &
+  @{text "(a b)::\<pi> \<bullet> c \<equiv>"} 
+  $\begin{cases}
+  \mbox{@{text "b"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = a"}}\\
+  \mbox{@{text "a"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = b"}}\\
+  \mbox{@{text "\<pi> \<bullet> c"}} & \text{otherwise}
+  \end{cases}$
+  \end{tabular}
+  \end{center}}
+  \end{itemize}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -45,6 +63,30 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
+  \begin{frame}<1>
+  \frametitle{\begin{tabular}{c}Problems\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item $\_ \act \_ :: \alpha perm \Rightarrow \beta \Rightarrow \beta$
+
+  \item $supp \_ :: \beta \Rightarrow \alpha set$
+
+  \begin{center}
+  $finite (supp x)_{\alpha_1} \ldots finite (supp x)_{\alpha_n}$
+  \end{center}
+  
+  \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
   \begin{frame}<1>[c]
   \frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}
   \mbox{}\\[-3mm]
diff -r 09bbed4f21d6 -r 9fb315392493 Slides/document/root.tex
--- a/Slides/document/root.tex	Tue May 25 00:24:41 2010 +0100
+++ b/Slides/document/root.tex	Wed May 26 15:34:54 2010 +0200
@@ -24,15 +24,26 @@
 \usepackage{graphicx} 
 \usepackage{xcolor} 
 
+% general math stuff
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}}
+\renewcommand{\emptyset}{\varnothing}% nice round empty set
+\renewcommand{\Gamma}{\varGamma} 
+\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
+\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
+\newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}}
+\newcommand{\fresh}{\mathrel{\#}}
+\newcommand{\act}{{\raisebox{-0.5mm}{\Large$\boldsymbol{\cdot}$}}}% swapping action
+\newcommand{\swap}[2]{(#1\,#2)}% swapping operation
 
 
 
 % Isabelle configuration
 %%\urlstyle{rm}
-\isabellestyle{rm}
-\renewcommand{\isastyle}{\rm}%
-\renewcommand{\isastyleminor}{\rm}%
-\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
+\isabellestyle{it}
+\renewcommand{\isastyle}{\it}%
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastylescript}{\footnotesize\it\slshape}%
 \renewcommand{\isatagproof}{}
 \renewcommand{\endisatagproof}{}
 \renewcommand{\isamarkupcmt}[1]{#1}
@@ -48,21 +59,11 @@
 \renewcommand{\isasymsharp}{\isamath{\#}}
 \renewcommand{\isasymdots}{\isamath{...}}
 \renewcommand{\isasymbullet}{\act}
+\renewcommand{\isasymequiv}{$\dn$}
 
 % mathpatir
 \mprset{sep=1em}
 
-% general math stuff
-\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
-\newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}}
-\renewcommand{\emptyset}{\varnothing}% nice round empty set
-\renewcommand{\Gamma}{\varGamma} 
-\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
-\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
-\newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}}
-\newcommand{\fresh}{\mathrel{\#}}
-\newcommand{\act}{{\raisebox{-0.5mm}{\Large$\boldsymbol{\cdot}$}}}% swapping action
-\newcommand{\swap}[2]{(#1\,#2)}% swapping operation
 
 % beamer stuff 
 \renewcommand{\slidecaption}{Salvador, 26.~August 2008}