src/HOL/Tools/inductive_realizer.ML
changeset 31781 861e675f01e6
parent 31723 f5cafe803b55
child 31783 cfbe9609ceb1
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 12:09:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 14:50:34 2009 +0200
     1.3 @@ -305,16 +305,17 @@
     1.4  
     1.5      (** datatype representing computational content of inductive set **)
     1.6  
     1.7 -    val ((dummies, dt_info), thy2) =
     1.8 +    val ((dummies, (dt_names_rules)), thy2) =
     1.9        thy1
    1.10        |> add_dummies (Datatype.add_datatype
    1.11             { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
    1.12             (map (pair false) dts) []
    1.13        ||> Extraction.add_typeof_eqns_i ty_eqs
    1.14        ||> Extraction.add_realizes_eqns_i rlz_eqs;
    1.15 -    fun get f = (these oo Option.map) f;
    1.16 +    val rec_thms = these (Option.map (#rec_thms o snd) dt_names_rules);
    1.17 +    val case_thms = these (Option.map (#case_thms o snd) dt_names_rules);
    1.18      val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
    1.19 -      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
    1.20 +      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
    1.21      val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
    1.22        if member (op =) rsets s then
    1.23          let
    1.24 @@ -324,7 +325,7 @@
    1.25            HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
    1.26          end
    1.27        else (replicate (length rs) Extraction.nullt, (recs, dummies)))
    1.28 -        rss (get #rec_thms dt_info, dummies);
    1.29 +        rss (rec_thms, dummies);
    1.30      val rintrs = map (fn (intr, c) => Envir.eta_contract
    1.31        (Extraction.realizes_of thy2 vs
    1.32          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
    1.33 @@ -386,8 +387,7 @@
    1.34            end) (rlzs ~~ rnames);
    1.35          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
    1.36            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
    1.37 -        val rews = map mk_meta_eq
    1.38 -          (fst_conv :: snd_conv :: get #rec_thms dt_info);
    1.39 +        val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
    1.40          val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
    1.41            [rtac (#raw_induct ind_info) 1,
    1.42             rewrite_goals_tac rews,
    1.43 @@ -417,7 +417,7 @@
    1.44      (** realizer for elimination rules **)
    1.45  
    1.46      val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
    1.47 -      HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
    1.48 +      HOLogic.dest_Trueprop o prop_of o hd) case_thms;
    1.49  
    1.50      fun add_elim_realizer Ps
    1.51        (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
    1.52 @@ -476,7 +476,7 @@
    1.53      val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
    1.54        add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
    1.55          (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
    1.56 -           elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
    1.57 +           elimps ~~ case_thms ~~ case_names ~~ dummies)
    1.58  
    1.59    in Sign.restore_naming thy thy6 end;
    1.60