src/HOL/Tools/Datatype/datatype_rep_proofs.ML
changeset 32765 3032c0308019
parent 32727 9072201cd69d
child 32874 5281cebb1a37
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
    76 
    76 
    77     val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
    77     val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
    78     val leafTs' = get_nonrec_types descr' sorts;
    78     val leafTs' = get_nonrec_types descr' sorts;
    79     val branchTs = get_branching_types descr' sorts;
    79     val branchTs = get_branching_types descr' sorts;
    80     val branchT = if null branchTs then HOLogic.unitT
    80     val branchT = if null branchTs then HOLogic.unitT
    81       else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
    81       else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
    82     val arities = get_arities descr' \ 0;
    82     val arities = get_arities descr' \ 0;
    83     val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
    83     val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
    84     val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
    84     val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
    85     val recTs = get_rec_types descr' sorts;
    85     val recTs = get_rec_types descr' sorts;
    86     val newTs = Library.take (length (hd descr), recTs);
    86     val newTs = Library.take (length (hd descr), recTs);
    87     val oldTs = Library.drop (length (hd descr), recTs);
    87     val oldTs = Library.drop (length (hd descr), recTs);
    88     val sumT = if null leafTs then HOLogic.unitT
    88     val sumT = if null leafTs then HOLogic.unitT
    89       else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
    89       else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
    90     val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
    90     val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
    91     val UnivT = HOLogic.mk_setT Univ_elT;
    91     val UnivT = HOLogic.mk_setT Univ_elT;
    92     val UnivT' = Univ_elT --> HOLogic.boolT;
    92     val UnivT' = Univ_elT --> HOLogic.boolT;
    93     val Collect = Const ("Collect", UnivT' --> UnivT);
    93     val Collect = Const ("Collect", UnivT' --> UnivT);
    94 
    94 
   114       in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
   114       in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
   115       end;
   115       end;
   116 
   116 
   117     (* make injections for constructors *)
   117     (* make injections for constructors *)
   118 
   118 
   119     fun mk_univ_inj ts = BalancedTree.access
   119     fun mk_univ_inj ts = Balanced_Tree.access
   120       {left = fn t => In0 $ t,
   120       {left = fn t => In0 $ t,
   121         right = fn t => In1 $ t,
   121         right = fn t => In1 $ t,
   122         init =
   122         init =
   123           if ts = [] then Const (@{const_name undefined}, Univ_elT)
   123           if ts = [] then Const (@{const_name undefined}, Univ_elT)
   124           else foldr1 (HOLogic.mk_binop Scons_name) ts};
   124           else foldr1 (HOLogic.mk_binop Scons_name) ts};