src/HOL/Tools/inductive_realizer.ML
changeset 16123 1381e90c2694
parent 15706 bc264e730103
child 16861 7446b4be013b
equal deleted inserted replaced
16122:864fda4a4056 16123:1381e90c2694
   285     val (_, params) = strip_comb S;
   285     val (_, params) = strip_comb S;
   286     val params' = map dest_Var params;
   286     val params' = map dest_Var params;
   287     val rss = Library.foldl add_rule ([], intrs);
   287     val rss = Library.foldl add_rule ([], intrs);
   288     val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
   288     val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
   289     val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
   289     val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
   290     val {path, ...} = Sign.rep_sg (sign_of thy);
   290 
   291     val thy1 = thy |>
   291     val thy1 = thy |>
   292       Theory.root_path |>
   292       Theory.root_path |>
   293       Theory.add_path (NameSpace.pack prfx);
   293       Theory.add_path (NameSpace.pack prfx);
   294     val (ty_eqs, rlz_eqs) = split_list
   294     val (ty_eqs, rlz_eqs) = split_list
   295       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
   295       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
   438     val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
   438     val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
   439       add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
   439       add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
   440         (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
   440         (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
   441            elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
   441            elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
   442 
   442 
   443   in Theory.add_path (NameSpace.pack (getOpt (path, []))) thy6 end;
   443   in Theory.restore_naming thy thy6 end;
   444 
   444 
   445 fun add_ind_realizers name rsets thy =
   445 fun add_ind_realizers name rsets thy =
   446   let
   446   let
   447     val (_, {intrs, induct, raw_induct, elims, ...}) =
   447     val (_, {intrs, induct, raw_induct, elims, ...}) =
   448       (case InductivePackage.get_inductive thy name of
   448       (case InductivePackage.get_inductive thy name of