src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 50170 8155e280f239
parent 49693 393d7242adaf
child 51380 cac8c9a636b6
equal deleted inserted replaced
50161:4fc4237488ab 50170:8155e280f239
    44 val mp_conj = @{thm mp_conj};
    44 val mp_conj = @{thm mp_conj};
    45 
    45 
    46 val simp_attrs = @{attributes [simp]};
    46 val simp_attrs = @{attributes [simp]};
    47 val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
    47 val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
    48 
    48 
    49 fun split_list4 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs);
    49 fun split_list4 [] = ([], [], [], [])
       
    50   | split_list4 ((x1, x2, x3, x4) :: xs) =
       
    51     let val (xs1, xs2, xs3, xs4) = split_list4 xs;
       
    52     in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
    50 
    53 
    51 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
    54 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
    52 
    55 
    53 fun typ_subst inst (T as Type (s, Ts)) =
    56 fun typ_subst inst (T as Type (s, Ts)) =
    54     (case AList.lookup (op =) inst T of
    57     (case AList.lookup (op =) inst T of
   461 
   464 
   462         val ctrs = map (mk_ctr As) ctrs0;
   465         val ctrs = map (mk_ctr As) ctrs0;
   463 
   466 
   464         fun wrap lthy =
   467         fun wrap lthy =
   465           let
   468           let
   466             fun exhaust_tac {context = ctxt, ...} =
   469             fun exhaust_tac {context = ctxt, prems = _} =
   467               let
   470               let
   468                 val ctor_iff_dtor_thm =
   471                 val ctor_iff_dtor_thm =
   469                   let
   472                   let
   470                     val goal =
   473                     val goal =
   471                       fold_rev Logic.all [w, u]
   474                       fold_rev Logic.all [w, u]