diff -r 082d9fd28f89 -r ebf253d80670 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Thu Jul 29 10:16:33 2010 +0100
+++ b/Nominal/NewParser.thy	Fri Jul 30 00:40:32 2010 +0100
@@ -305,24 +305,31 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
-  val all_raw_tys = map (fn (_, (n, _, _)) => n) descr
+  val all_raw_tys = all_dtyps descr sorts
+  val all_raw_ty_names = map (fn (_, (n, _, _)) => n) descr
   val all_raw_constrs = 
     flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts))
 
-  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_tys  
+  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names  
   val inject_thms = flat (map #inject dtinfos);
   val distinct_thms = flat (map #distinct dtinfos);
   val constr_thms = inject_thms @ distinct_thms
   val rel_dtinfos = List.take (dtinfos, (length dts)); 
   val raw_constrs_distinct = (map #distinct rel_dtinfos); 
-  val induct_thm = #induct dtinfo;
+  val raw_induct_thm = #induct dtinfo;
+  val raw_induct_thms = #inducts dtinfo;
   val exhaust_thms = map #exhaust dtinfos;
+  val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys
+  val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
+    |> `(fn thms => (length thms) div 2)
+    |> (uncurry drop)
+  
 
   (* definitions of raw permutations *)
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
     if get_STEPS lthy0 > 1 
-    then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0
+    then Local_Theory.theory_result (define_raw_perms descr sorts raw_induct_thm (length dts)) lthy0
     else raise TEST lthy0
  
   (* noting the raw permutations as eqvt theorems *)
@@ -338,7 +345,7 @@
 
   val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
-    then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
+    then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
     else raise TEST lthy3
 
   val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = 
@@ -367,7 +374,7 @@
     then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
     else raise TEST lthy4
 
-  (* proving equivariance lemmas for bns, fvs and alpha *)
+  (* proving equivariance lemmas for bns, fvs, size and alpha *)
   val _ = warning "Proving equivariance";
   val bn_eqvt = 
     if get_STEPS lthy > 6
@@ -381,13 +388,19 @@
   val fv_eqvt = 
     if get_STEPS lthy > 7
     then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) 
-       (Local_Theory.restore lthy_tmp)
+      (Local_Theory.restore lthy_tmp)
+    else raise TEST lthy4
+
+  val size_eqvt = 
+    if get_STEPS lthy > 8
+    then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) 
+      (Local_Theory.restore lthy_tmp)
     else raise TEST lthy4
  
   val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
 
   val (alpha_eqvt, lthy6) =
-    if get_STEPS lthy > 8
+    if get_STEPS lthy > 9
     then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
     else raise TEST lthy4
 
@@ -395,23 +408,23 @@
   val _ = warning "Proving equivalence"
 
   val alpha_refl_thms = 
-    if get_STEPS lthy > 9
-    then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy6 
+    if get_STEPS lthy > 10
+    then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6 
     else raise TEST lthy6
 
   val alpha_sym_thms = 
-    if get_STEPS lthy > 10
+    if get_STEPS lthy > 11
     then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6 
     else raise TEST lthy6
 
   val alpha_trans_thms = 
-    if get_STEPS lthy > 11
+    if get_STEPS lthy > 12
     then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) 
            alpha_intros alpha_induct alpha_cases lthy6
     else raise TEST lthy6
 
   val alpha_equivp_thms = 
-    if get_STEPS lthy > 12
+    if get_STEPS lthy > 13
     then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6
     else raise TEST lthy6
 
@@ -419,16 +432,14 @@
   val _ = warning "Proving alpha implies bn"
 
   val alpha_bn_imp_thms = 
-    if get_STEPS lthy > 13
+    if get_STEPS lthy > 14
     then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 
     else raise TEST lthy6
   
   (* auxiliary lemmas for respectfulness proofs *)
-  (* HERE *)
-  
-  val test = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs raw_bns raw_fv_bns
-    alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
-  val _ = tracing ("goals\n" ^ cat_lines (map (Syntax.string_of_term lthy6 o prop_of) test))
+  val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
+    raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
+
 
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
@@ -438,7 +449,7 @@
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *)
   
   val (qty_infos, lthy7) = 
-    if get_STEPS lthy > 14
+    if get_STEPS lthy > 15
     then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
     else raise TEST lthy6
 
@@ -463,7 +474,7 @@
     map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
 
   val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = 
-    if get_STEPS lthy > 15
+    if get_STEPS lthy > 16
     then 
       lthy7
       |> qconst_defs qtys qconstrs_descr 
@@ -479,7 +490,7 @@
   val qfv_bns = map #qconst qfv_bns_info
   val qalpha_bns = map #qconst qalpha_bns_info
 
-  (* HERE *)
+  (* temporary theorem bindings *)
 
   val (_, lthy8') = lthy8
      |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) 
@@ -489,9 +500,11 @@
      ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
+     ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
+     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), size_eqvt)
   
   val _ = 
-    if get_STEPS lthy > 16
+    if get_STEPS lthy > 17
     then true else raise TEST lthy8'
   
   (* old stuff *)
@@ -558,7 +571,7 @@
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = warning "Lifting induction";
   val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs;
-  val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm);
+  val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 raw_induct_thm);
   fun note_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
   fun note_simp_suffix s th ctxt =