# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272889837 -7200
# Node ID 070ba8972e97ca2b93b58d5a43dc59a8c08a73c0
# Parent  d974059827adf8cc2a079f9da086101b5a84ad01
Register only non-looping rules in eq_iff

diff -r d974059827ad -r 070ba8972e97 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon May 03 14:03:30 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 03 14:30:37 2010 +0200
@@ -278,6 +278,12 @@
 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]
+*}
+
 text {* 
   nominal_datatype2 does the following things in order:
 
@@ -399,7 +405,8 @@
   
   (* definition of raw_alpha_eq_iff  lemmas *)
   val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
-  val alpha_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) alpha_eq_iff;
+  val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
+  val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);
 
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
@@ -490,15 +497,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 alphas3}) alpha_eq_iff
+  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp
   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
   val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
   val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
   val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
-  val q_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) q_eq_iff;
-  val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff_simp) lthy17;
+  val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   val q_dis = map (lift_thm qtys lthy18) rel_dists;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
   val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt);
@@ -516,7 +522,7 @@
   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
-    supp_eq_tac q_induct q_fv q_perm q_eq_iff_simp lthy22 1;
+    supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
   val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>
     let val _ = warning ("Support eqs failed") in [] end;
   val lthy23 = note_suffix "supp" q_supp lthy22;