# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268824715 -3600
# Node ID 21cbb5b0e321ba63e2416f0efc24aa94136bcf86
# Parent  4ac3485899e182247e346fc211470e539af41bac
cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.

diff -r 4ac3485899e1 -r 21cbb5b0e321 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 17 11:40:58 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 12:18:35 2010 +0100
@@ -389,16 +389,12 @@
                 val rhs_binds = fv_binds args2 rbinds;
                 val rhs_arg = foldr1 HOLogic.mk_prod bound_args2;
                 val rhs = mk_pair (rhs_binds, rhs_arg);
-                val _ = tracing (PolyML.makestring bound_in_ty_nos);
                 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos);
-                val _ = tracing (PolyML.makestring fvs);
                 val fv = mk_compound_fv fvs;
                 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos);
-                val _ = tracing (PolyML.makestring alphas);
                 val alpha = mk_compound_alpha alphas;
                 val pi = foldr1 add_perm (distinct (op =) rpis);
                 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
-                val _ = tracing (PolyML.makestring alpha_gen_pre);
                 val alpha_gen = Syntax.check_term lthy alpha_gen_pre
               in
                 alpha_gen
@@ -449,7 +445,6 @@
   val fv_names_all = fv_names_fst @ fv_bn_names;
   val add_binds = map (fn x => (Attrib.empty_binding, x))
 (* Function_Fun.add_fun Function_Common.default_config ... true *)
-(*  val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*)
   val (fvs, lthy') = (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
   val (fvs2, lthy'') =
diff -r 4ac3485899e1 -r 21cbb5b0e321 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Mar 17 11:40:58 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 17 12:18:35 2010 +0100
@@ -243,7 +243,7 @@
 
   val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs)
 
-  val _ = tracing (cat_lines (map PolyML.makestring raw_bns)) 
+(*val _ = tracing (cat_lines (map PolyML.makestring raw_bns))*)
 in
   lthy 
   |> add_datatype_wrapper raw_dt_names raw_dts 
@@ -289,6 +289,7 @@
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
+  val _ = tracing "Raw declarations";
   val thy = ProofContext.theory_of lthy
   val thy_name = Context.theory_name thy
   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
@@ -311,6 +312,7 @@
   val rel_distinct = map #distinct rel_dtinfos;
   val induct = #induct dtinfo;
   val inducts = #inducts dtinfo;
+  val _ = tracing "Defining permutations, fv and alpha";
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
   val raw_binds_flat = map (map flat) raw_binds;
@@ -336,29 +338,25 @@
   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
+  val _ = tracing "Proving equivariance";
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
-  val _ = tracing "3";
   val fv_eqvt_tac =
     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
     else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
-  val _ = tracing "4";
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5;
-  val _ = tracing "4a";
   val (fv_bn_eqvts, lthy6a) = 
     if fv_ts_loc_bn = [] then ([], lthy6) else
     fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) 
       (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
-  val _ = tracing "4b";
   val lthy6 = lthy6a;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
-  val _ = tracing "5";
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1
   val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6;
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
-  val _ = map tracing (map PolyML.makestring alpha_eqvt)
+  val _ = tracing "Proving equivalence";
   val alpha_equivp_loc = 
     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn
     else build_equivps alpha_ts_loc induct alpha_induct_loc
@@ -382,6 +380,7 @@
   val consts = map (Morphism.term morphism_8_7) consts_loc;
   (* Could be done nicer *)
   val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
+  val _ = tracing "Proving respects";
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
       (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
@@ -400,12 +399,14 @@
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
+  val _ = tracing "Lifting permutations";
   val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
   val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
   val q_name = space_implode "_" qty_names;
+  val _ = tracing "Lifting induction";
   val q_induct = lift_thm lthy13 induct;
   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
   val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
@@ -416,6 +417,7 @@
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
   val q_bn = map (lift_thm lthy16) raw_bn_eqs;
   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
+  val _ = tracing "Lifting pseudo-injectivity";
   val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj
   val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1
   val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2;
@@ -429,8 +431,8 @@
   val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
+  val _ = tracing "Finite Support";
   val supports = map (prove_supports lthy20 q_perm) consts
-  val _ = map tracing (map PolyML.makestring supports);
   val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys) handle _ => []
   val thy3 = Local_Theory.exit_global lthy20;
   val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
diff -r 4ac3485899e1 -r 21cbb5b0e321 Nominal/Test.thy
--- a/Nominal/Test.thy	Wed Mar 17 11:40:58 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 12:18:35 2010 +0100
@@ -107,7 +107,6 @@
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 
-ML {* val _ = cheat_alpha_eqvt := true *}
 ML {* val _ = recursive := true *}
 
 nominal_datatype lam' =