# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1334928515 -7200
# Node ID aa1ba91ed1ffea2e21e67218e587cd90ef51923b
# Parent  8bda1d947df3c65d448c11ae54dbf755938ed3d2
Pass proper rsp theorems for constructors and for size

diff -r 8bda1d947df3 -r aa1ba91ed1ff Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu Apr 12 01:39:54 2012 +0100
+++ b/Nominal/Nominal2.thy	Fri Apr 20 15:28:35 2012 +0200
@@ -321,7 +321,7 @@
       |> map mk_funs_rsp
 
   val raw_constrs_rsp = 
-    raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux) 
+    raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux) 
     
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
@@ -333,9 +333,12 @@
   (* noting the quot_respects lemmas *)
   val (_, lthy6) = 
     Local_Theory.note ((Binding.empty, [rsp_attr]),
-      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ 
+      raw_funs_rsp @ alpha_permute_rsp @ 
       alpha_bn_rsp @ raw_perm_bn_rsp) lthy5
 
+  val _ = tracing (PolyML.makestring (raw_size_rsp, raw_funs_rsp, alpha_permute_rsp,
+      alpha_bn_rsp, raw_perm_bn_rsp))
+
   val _ = trace_msg (K "Defining the quotient types...")
   val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts
      
@@ -348,12 +351,12 @@
 
   val qtys = map #qtyp qty_infos
   val qty_full_names = map (fst o dest_Type) qtys
-  val qty_names = map Long_Name.base_name qty_full_names             
+  val qty_names = map Long_Name.base_name qty_full_names
 
   val _ = trace_msg (K "Defining the quotient constants...")
   val qconstrs_descrs =
-    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) 
-      (get_cnstrs dts) raw_all_cns
+    (map2 o map2) (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th))
+      (get_cnstrs dts) (map (op ~~) (raw_all_cns ~~ raw_constrs_rsp))
 
   val qbns_descr =
     map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns
@@ -378,7 +381,8 @@
       qty_names raw_perm_funs
 
   val qsize_descr =
-    map2 (fn n => fn t => ("size_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_size_trms
+    map2 (fn n => fn (t, th) => ("size_" ^ n, t, NoSyn, th)) qty_names
+      (raw_size_trms ~~ (take (length raw_size_trms) raw_size_rsp))
 
   val qperm_bn_descr = 
     map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
diff -r 8bda1d947df3 -r aa1ba91ed1ff Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Thu Apr 12 01:39:54 2012 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Fri Apr 20 15:28:35 2012 +0200
@@ -29,7 +29,7 @@
   val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> 
     thm list -> thm list
   val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list
-  val raw_constrs_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
+  val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list
   val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list
   val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
   
@@ -749,9 +749,10 @@
       |> Syntax.check_term ctxt
       |> HOLogic.mk_Trueprop
   in
+    map (fn constrs =>
     Goal.prove_multi ctxt [] [] (map prep_goal constrs)
       (K (HEADGOAL 
-        (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))
+        (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))) constrs
   end
 
 
diff -r 8bda1d947df3 -r aa1ba91ed1ff Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Thu Apr 12 01:39:54 2012 +0100
+++ b/Nominal/nominal_dt_quot.ML	Fri Apr 20 15:28:35 2012 +0200
@@ -105,7 +105,7 @@
       |> Local_Theory.exit_global
       |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) 
   
-    val (qs, lthy2) = define_qconsts qtys perm_specs lthy1
+    val (_, lthy2) = define_qconsts qtys perm_specs lthy1
 
     val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2