116 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or

   117    appends of elements; in case of recursive calls it retruns also the applied

   118    bn function *)

   119 ML {*

   120 fun strip_bn_fun lthy args t =

   121 let 

   122   fun aux t =

   123     case t of

   124       Const (@{const_name sup}, _) $ l $ r => aux l @ aux r

   125     | Const (@{const_name append}, _) $ l $ r => aux l @ aux r

   126     | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>

   127         (find_index (equal x) args, NONE) :: aux y

   128     | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>

   129         (find_index (equal x) args, NONE) :: aux y

   130     | Const (@{const_name bot}, _) => []

   131     | Const (@{const_name Nil}, _) => []

   132     | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)]

   133     | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t))

   134 in

   135   aux t

   136 end  

   137 *}

   138 

   139 ML {*

   140 (** definition of the raw binding functions **)

   141 

   142 fun prep_bn_info lthy dt_names dts bn_funs eqs = 

   143 let

   144   fun process_eq eq = 

   145   let

   146     val (lhs, rhs) = eq

   147       |> HOLogic.dest_Trueprop

   148       |> HOLogic.dest_eq

   149     val (bn_fun, [cnstr]) = strip_comb lhs

   150     val (_, ty) = dest_Const bn_fun

   151     val (ty_name, _) = dest_Type (domain_type ty)

   152     val dt_index = find_index (fn x => x = ty_name) dt_names

   153     val (cnstr_head, cnstr_args) = strip_comb cnstr    

   154     val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head))

   155     val rhs_elements = strip_bn_fun lthy cnstr_args rhs

   156   in

   157     ((bn_fun, dt_index), (cnstr_name, rhs_elements))

   158   end

   159 

   160   (* order according to constructor names *)

   161   fun cntrs_order ((bn, dt_index), data) = 

   162   let

   163     val dt = nth dts dt_index                      

   164     val cts = (fn (_, _, _, x) => x) dt     

   165     val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts  

   166   in

   167     (bn, (bn, dt_index, order (op=) ct_names data))

   168   end

   169  

   170 in

   171   eqs

   172   |> map process_eq 

   173   |> AList.group (op=)      (* eqs grouped according to bn_functions *)

   174   |> map cntrs_order        (* inner data ordered according to constructors *)

   175   |> order (op=) bn_funs    (* ordered according to bn_functions *)

   176 end

   177 *}

   178 

   179 ML {*

   180 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =

   181   if null raw_bn_funs 

   182   then ([], [], [], [], lthy)

   183   else 

   184     let

   185       val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs

   186         Function_Common.default_config (pat_completeness_simp constr_thms) lthy

   187 

   188       val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1)

   189       val {fs, simps, inducts, ...} = info

   190 

   191       val raw_bn_induct = (the inducts)

   192       val raw_bn_eqs = the simps

   193 

   194       val raw_bn_info = 

   195         prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs)

   196     in

   197       (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)

   198     end

   199 

   200 *}