--- a/Nominal/NewParser.thy	Sat Aug 28 18:15:23 2010 +0800
+++ b/Nominal/NewParser.thy	Sun Aug 29 00:09:45 2010 +0800
@@ -9,6 +9,7 @@
      ("nominal_dt_rawfuns.ML")
      ("nominal_dt_alpha.ML")
      ("nominal_dt_quot.ML")
+     ("nominal_dt_supp.ML")
 begin
 
 use "nominal_dt_rawperm.ML"
@@ -23,13 +24,16 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
+use "nominal_dt_supp.ML"
+ML {* open Nominal_Dt_Supp *}
 
 section{* Interface for nominal_datatype *}
 
 ML {*
 (* attributes *)
-val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add)
+val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
+val simp_attr = Attrib.internal (K Simplifier.simp_add)
 
 *}
 
@@ -300,7 +304,7 @@
     else raise TEST lthy0
  
   (* noting the raw permutations as eqvt theorems *)
-  val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a
+  val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
 
   (* definition of raw fv_functions *)
   val _ = warning "Definition of raw fv-functions";
@@ -345,7 +349,7 @@
     else raise TEST lthy4
 
   (* noting the raw_bn_eqvt lemmas in a temprorary theory *)
-  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_bn_eqvt) lthy4)
+  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4)
 
   val raw_fv_eqvt = 
     if get_STEPS lthy > 7
@@ -361,7 +365,7 @@
       |> map (fn thm => thm RS @{thm sym})
     else raise TEST lthy4
  
-  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_fv_eqvt) lthy_tmp)
+  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
 
   val (alpha_eqvt, lthy6) =
     if get_STEPS lthy > 9
@@ -440,7 +444,7 @@
   (* noting the quot_respects lemmas *)
   val (_, lthy6a) = 
     if get_STEPS lthy > 21
-    then Local_Theory.note ((Binding.empty, [rsp_attrib]),
+    then Local_Theory.note ((Binding.empty, [rsp_attr]),
       raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6
     else raise TEST lthy6
 
@@ -503,7 +507,7 @@
     then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
     else raise TEST lthy9
 
-  val qconstrs = map #qconst qconstrs_info
+  val qtrms = map #qconst qconstrs_info
   val qbns = map #qconst qbns_info
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
@@ -536,6 +540,14 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
     else raise TEST lthyA
 
+  (* Supports lemmas *) 
+
+  val qsupports_thms =
+    if get_STEPS lthy > 28
+    then prove_supports lthyB qperm_simps qtrms
+    else raise TEST lthyB
+
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -548,11 +560,12 @@
      ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
-     ||>> Local_Theory.note ((thms_suffix "perm_simps", []), qperm_simps) 
+     ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
+     ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      
 in
   (0, lthy9')