# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272882267 -7200
# Node ID 8ffede2c8ce90a3e0854c73d3c2643f7c9c0cd1f
# Parent  f761f83e541a65ea206e909fe3a20eff8ab335d2
Introduce eq_iff_simp to match the one from Parser.

diff -r f761f83e541a -r 8ffede2c8ce9 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon May 03 11:43:27 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 03 12:24:27 2010 +0200
@@ -397,24 +397,25 @@
   
   (* 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;
+
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1
+    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
   (* provind alpha equivalence *)
   val _ = warning "Proving equivalence";
   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff_simp lthy6;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
     else build_equivps alpha_ts reflps alpha_induct
-      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
+      inject alpha_eq_iff_simp distincts alpha_cases alpha_eqvt lthy6;
   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
@@ -442,12 +443,12 @@
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
-(*  val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;*)
+(*  val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;*)
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
         (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11
   fun const_rsp_tac _ =
-    let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
-      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+    let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a
+      in constr_rsp_tac alpha_eq_iff_simp (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) (fv @ fvbn)
@@ -509,6 +510,7 @@
   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
   val (names, supp_eq_t) = supp_eq fv_alpha_all;
   val _ = warning "Support Equations";
+  val q_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) q_eq_iff;
   (*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 (fn _ => Skip_Proof.cheat_tac thy)) handle _ => [];
   val lthy23 = note_suffix "supp" q_supp lthy22;