
diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Nominal2.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -146,13 +146,9 @@
 ML {*
 (** definition of the raw binding functions **)
 
-(* TODO: needs cleaning *)
-fun find [] _ = error ("cannot find element")
-  | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
-
-fun prep_bn_info lthy dt_names dts eqs = 
+fun prep_bn_info lthy dt_names dts bn_funs eqs = 
 let
-  fun aux eq = 
+  fun process_eq eq = 
   let
     val (lhs, rhs) = eq
       |> HOLogic.dest_Trueprop
@@ -162,32 +158,32 @@
     val (ty_name, _) = dest_Type (domain_type ty)
     val dt_index = find_index (fn x => x = ty_name) dt_names
     val (cnstr_head, cnstr_args) = strip_comb cnstr    
+    val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head))
     val rhs_elements = strip_bn_fun lthy cnstr_args rhs
   in
-    (dt_index, (bn_fun, (cnstr_head, rhs_elements)))
+    ((bn_fun, dt_index), (cnstr_name, rhs_elements))
   end
 
-  fun order dts i ts = 
+  (* order according to constructor names *)
+  fun cntrs_order ((bn, dt_index), data) = 
   let
-    val dt = nth dts i
-    val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt)
-    val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts
+    val dt = nth dts dt_index                      
+    val cts = (fn (_, _, _, x) => x) dt     
+    val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts  
   in
-    map (find ts') cts
+    (bn, (bn, dt_index, order (op=) ct_names data))
   end
+ 
+in
+  eqs
+  |> map process_eq 
+  |> AList.group (op=)      (* eqs grouped according to bn_functions *)
+  |> map cntrs_order        (* inner data ordered according to constructors *)
+  |> order (op=) bn_funs    (* ordered according to bn_functions *)
+end
+*}
 
-  val unordered = AList.group (op=) (map aux eqs)
-  val unordered' = map (fn (x, y) =>  (x, AList.group (op=) y)) unordered
-  val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' 
-  val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
-
-  (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*)
-  (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*)
-  (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*)
-in
-  ordered'
-end
-
+ML {*
 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
   if null raw_bn_funs 
   then ([], [], [], [], lthy)
@@ -203,7 +199,7 @@
       val raw_bn_eqs = the simps
 
       val raw_bn_info = 
-        prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
+        prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs)
     in
       (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
     end
@@ -269,6 +265,8 @@
     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
+  val _ = tracing ("raw_bn_funs\n" ^ cat_lines (map (@{make_string} o #1) raw_bn_funs))
+ 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
 
@@ -311,6 +309,12 @@
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
     else raise TEST lthy3
 
+  (*
+  val _ = tracing ("RAW_BNS\n" ^ cat_lines (map (Syntax.string_of_term lthy3) raw_bns))
+  val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map (Syntax.string_of_term lthy3 o #1) raw_bn_info))
+  val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map @{make_string} raw_bn_info))
+  *)
+
   (* defining the permute_bn functions *)
   val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = 
     if get_STEPS lthy3a > 2
@@ -489,6 +493,14 @@
   val qalpha_bns_descr = 
     map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
 
+  (*
+  val _ = tracing ("raw_bn_info\n" ^ cat_lines (map (Syntax.string_of_term lthy7 o #1) raw_bn_info))
+  val _ = tracing ("bn_funs\n" ^ cat_lines (map (@{make_string} o #1) bn_funs))
+  val _ = tracing ("raw_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_bns))
+  val _ = tracing ("raw_fv_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_fv_bns))
+  val _ = tracing ("alpha_bn_trms\n" ^ cat_lines (map (Syntax.string_of_term lthy7) alpha_bn_trms))
+  *)
+
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
 
@@ -499,7 +511,7 @@
     map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns
      
 
-  val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qpermute_bns), lthy8) = 
+  val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8)= 
     if get_STEPS lthy > 24
     then 
       lthy7
@@ -527,6 +539,7 @@
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
   val qalpha_bns = map #qconst qalpha_bns_info
+  val qperm_bns = map #qconst qperm_bns_info
 
   (* lifting of the theorems *)
   val _ = warning "Lifting of Theorems"
@@ -586,12 +599,6 @@
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
 
-  (* proving that the qbn result is finite *)
-  val qbn_finite_thms =
-    if get_STEPS lthy > 33
-    then prove_bns_finite qtys qbns qinduct qbn_defs lthyC
-    else []
-
   (* postprocessing of eq and fv theorems *)
 
   val qeq_iffs' = qeq_iffs
@@ -612,6 +619,18 @@
     |> map (fn thm => thm RS transform_thm) 
     |> map (simplify (HOL_basic_ss addsimps transform_thms))
 
+  (* proving that the qbn result is finite *)
+  val qbn_finite_thms =
+    if get_STEPS lthy > 33
+    then prove_bns_finite qtys qbns qinduct qbn_defs lthyC
+    else []
+
+  (* proving that perm_bns preserve alpha *)
+  val qperm_bn_alpha_thms = @{thms TrueI}
+  (*  if get_STEPS lthy > 33
+    then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' lthyC
+    else []*)
+
 
   (* noting the theorems *)  
 
@@ -639,6 +658,7 @@
      ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
      ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
+     ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)




