# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282040273 -28800
# Node ID 83990a42a0686c8a95903621c8dabf06246edc25
# Parent  f1980f89c405c037266789111f3272e66137bb07
more tuning of the code

diff -r f1980f89c405 -r 83990a42a068 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Aug 17 18:00:55 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 18:17:53 2010 +0800
@@ -21,7 +21,9 @@
 where
   "bn (As x y t) = {atom x}"
 
-(* can lift *)
+ML {* Function.prove_termination *}
+
+text {* can lift *}
 
 thm distinct
 thm trm_raw_assg_raw.inducts
diff -r f1980f89c405 -r 83990a42a068 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Aug 17 18:00:55 2010 +0800
+++ b/Nominal/NewParser.thy	Tue Aug 17 18:17:53 2010 +0800
@@ -283,12 +283,6 @@
 *}
 
 
-
-ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
-ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
-ML {* val cheat_supp_eq = Unsynchronized.ref false *}
-
-
 ML {*
 (* for testing porposes - to exit the procedure early *)
 exception TEST of Proof.context
@@ -331,7 +325,7 @@
     |> `(fn thms => (length thms) div 2)
     |> uncurry drop
   
-  (* definitions of raw permutations *)
+  (* definitions of raw permutations by primitive recursion *)
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
     if get_STEPS lthy0 > 1 
@@ -567,8 +561,7 @@
        resolve_tac bns_rsp_pre' 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 raw_fv_defs lthy8 1;
+  fun fv_rsp_tac _ = fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1;
 
   val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
 
@@ -579,9 +572,7 @@
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs
     (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_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms raw_exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
+  fun alpha_bn_rsp_tac _ = let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms raw_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_trms lthy11
   fun const_rsp_tac _ =
@@ -656,8 +647,7 @@
   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
-    supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
+  fun supp_eq_tac' _ =  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;
diff -r f1980f89c405 -r 83990a42a068 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Tue Aug 17 18:00:55 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Aug 17 18:17:53 2010 +0800
@@ -240,12 +240,12 @@
 
   val morphism = ProofContext.export_morphism lthy'' lthy
   val fs_exp = map (Morphism.term morphism) fs
-
+  val simps_exp = map (Morphism.thm morphism) (the simps)
+  val inducts_exp = map (Morphism.thm morphism) (the inducts)
   val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
-  val simps_exp = map (Morphism.thm morphism) (the simps)
-  val fv_bns_inducts_exp = map (Morphism.thm morphism) (the inducts)
+  
 in
-  (fv_frees_exp, fv_bns_exp, simps_exp, fv_bns_inducts_exp, lthy'')
+  (fv_frees_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'')
 end