# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1275398461 -7200
# Node ID 86c977b4a9bbcb62249e264598700824d6f45b15
# Parent  93ab397f5980dd04878c3134cb64566f4629d9d3
equivariance done

diff -r 93ab397f5980 -r 86c977b4a9bb Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Tue Jun 01 15:01:05 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Tue Jun 01 15:21:01 2010 +0200
@@ -10,7 +10,7 @@
   val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
   val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
   
-  val equivariance: term list -> thm -> thm list -> Proof.context -> thm list * local_theory
+  val equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory
   val equivariance_cmd: string -> Proof.context -> local_theory
 end
 
@@ -147,7 +147,7 @@
   (thm', ctxt')
 end
 
-fun equivariance pred_trms raw_induct intrs ctxt = 
+fun equivariance note_flag pred_trms raw_induct intrs ctxt = 
 let
   val is_already_eqvt = 
     filter (is_eqvt ctxt) pred_trms
@@ -172,7 +172,9 @@
     |> singleton (ProofContext.export ctxt' ctxt))
   val thms' = map (fn th => zero_var_indexes (th RS mp)) thms
 in
-  ctxt |> fold_map note_named_thm (pred_names ~~ thms')   
+  if note_flag
+  then ctxt |> fold_map note_named_thm (pred_names ~~ thms')  
+  else (thms', ctxt) 
 end
 
 fun equivariance_cmd pred_name ctxt =
@@ -181,7 +183,7 @@
   val (_, {preds, raw_induct, intrs, ...}) =
     Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
 in
-  equivariance preds raw_induct intrs ctxt |> snd
+  equivariance true preds raw_induct intrs ctxt |> snd
 end
 
 local structure P = Parse and K = Keyword in
diff -r 93ab397f5980 -r 86c977b4a9bb Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Jun 01 15:01:05 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jun 01 15:21:01 2010 +0200
@@ -7,7 +7,7 @@
 ML {*  Function.add_function *}
 
 ML {* print_depth 50 *}
-declare [[STEPS = 8]]
+declare [[STEPS = 9]]
 
 
 nominal_datatype trm =
diff -r 93ab397f5980 -r 86c977b4a9bb Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Jun 01 15:01:05 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Jun 01 15:21:01 2010 +0200
@@ -403,11 +403,19 @@
  
   val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp
 
-  val (alpha_eqvt, lthy6a) =
+  
+
+  val (alpha_eqvt, _) =
     if get_STEPS lthy > 8
-    then Nominal_Eqvt.equivariance alpha_trms alpha_induct alpha_intros lthy_tmp'
+    then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp'
     else raise TEST lthy4
 
+  (*
+  val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt))
+  val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt))
+  val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt))
+  *)
+
   val _ = 
     if get_STEPS lthy > 9
     then true else raise TEST lthy4
@@ -417,15 +425,15 @@
 
   val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
 
-  val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy6a;
+  val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4;
   val alpha_equivp =
-    if !cheat_equivp then map (equivp_hack lthy6a) alpha_trms
+    if !cheat_equivp then map (equivp_hack lthy4) alpha_trms
     else build_equivps alpha_trms reflps alpha_induct
-      inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy6a;
+      inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4;
   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
-  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy6a;
+  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy4;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>