# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269424190 -3600
# Node ID b63e85d367153a97d740a590069c18735ba49817
# Parent  006d81399f6a18bbac6eb604c689654f0d704657
Export all the cheats needed for Core Haskell.

diff -r 006d81399f6a -r b63e85d36715 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Mar 24 09:59:47 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 24 10:49:50 2010 +0100
@@ -286,13 +286,13 @@
 end
 *}
 
-(* This one is not needed for the proper examples *)
 ML {* val cheat_equivp = Unsynchronized.ref false *}
-
-(* These 4 are not needed any more *)
-ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
+ML {* val cheat_bn_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
+ML {* val cheat_bn_rsp = Unsynchronized.ref false *}
+ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
+ML {* val cheat_const_rsp = Unsynchronized.ref false *}
 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
 ML {* fun map_option _ NONE = NONE
@@ -345,6 +345,11 @@
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
   val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
+  fun build_bv_eqvt simps inducts (t, n) ctxt =
+    build_eqvts Binding.empty [t]
+      (if !cheat_bn_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
+       else build_eqvts_tac (nth inducts n) simps ctxt
+      ) ctxt
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val fv_eqvt_tac =
     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
@@ -384,8 +389,9 @@
   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 lthy8 1)) bns lthy8;
+    fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ =>
+       if !cheat_bn_rsp then (Skip_Proof.cheat_tac thy) else
+       fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
     else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
@@ -396,13 +402,19 @@
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
-  val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11;
-  fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1
+  fun const_rsp_tac _ =
+    if !cheat_const_rsp then Skip_Proof.cheat_tac thy
+    else let val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11
+      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
   val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11
-  val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos))
   val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a
+    (fn _ =>
+      if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
+      else
+        let val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts
+        (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) in
+        asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end)) alpha_ts_bn lthy11a
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
diff -r 006d81399f6a -r b63e85d36715 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Wed Mar 24 09:59:47 2010 +0100
+++ b/Nominal/Rsp.thy	Wed Mar 24 10:49:50 2010 +0100
@@ -212,11 +212,6 @@
 *}
 
 ML {*
-fun build_bv_eqvt simps inducts (t, n) ctxt =
-  build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt
-*}
-
-ML {*
 fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =
 let
   val (fvs_alphas, ls) = split_list fv_alphas_lst;