src/HOL/Tools/inductive_realizer.ML
changeset 22606 962f824c2df9
parent 22596 d0d2af4db18f
child 22790 e1cff9268177
equal deleted inserted replaced
22605:41b092e7d89a 22606:962f824c2df9
    14 
    14 
    15 structure InductiveRealizer : INDUCTIVE_REALIZER =
    15 structure InductiveRealizer : INDUCTIVE_REALIZER =
    16 struct
    16 struct
    17 
    17 
    18 (* FIXME: LocalTheory.note should return theorems with proper names! *)
    18 (* FIXME: LocalTheory.note should return theorems with proper names! *)
    19 fun name_of_thm thm = (case Proofterm.strip_combt (fst (Proofterm.strip_combP
    19 fun name_of_thm thm =
    20     (Proofterm.rewrite_proof (theory_of_thm thm) ([], []) (proof_of thm)))) of
    20   (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of
    21     (PThm (name, _, _, _), _) => name
    21      [(name, _)] => name
    22   | _ => error "name_of_thm: bad proof");
    22    | _ => error ("name_of_thm: bad proof of theorem\n" ^ string_of_thm thm));
    23 
    23 
    24 (* infer order of variables in intro rules from order of quantifiers in elim rule *)
    24 (* infer order of variables in intro rules from order of quantifiers in elim rule *)
    25 fun infer_intro_vars elim arity intros =
    25 fun infer_intro_vars elim arity intros =
    26   let
    26   let
    27     val thy = theory_of_thm elim;
    27     val thy = theory_of_thm elim;
   395         (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
   395         (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
   396 
   396 
   397     (** realizability predicate **)
   397     (** realizability predicate **)
   398 
   398 
   399     val (ind_info, thy3') = thy2 |>
   399     val (ind_info, thy3') = thy2 |>
   400       TheoryTarget.init NONE |>
   400       InductivePackage.add_inductive_global false "" false false false
   401       InductivePackage.add_inductive_i false "" false false false
       
   402         rlzpreds rlzparams (map (fn (rintr, intr) =>
   401         rlzpreds rlzparams (map (fn (rintr, intr) =>
   403           ((Sign.base_name (name_of_thm intr), []),
   402           ((Sign.base_name (name_of_thm intr), []),
   404            subst_atomic rlzpreds' (Logic.unvarify rintr)))
   403            subst_atomic rlzpreds' (Logic.unvarify rintr)))
   405              (rintrs ~~ maps snd rss)) [] ||>
   404              (rintrs ~~ maps snd rss)) [] ||>
   406       ProofContext.theory_of o LocalTheory.exit ||>
       
   407       Theory.absolute_path;
   405       Theory.absolute_path;
   408     val thy3 = PureThy.hide_thms false
   406     val thy3 = PureThy.hide_thms false
   409       (map name_of_thm (#intrs ind_info)) thy3';
   407       (map name_of_thm (#intrs ind_info)) thy3';
   410 
   408 
   411     (** realizer for induction rule **)
   409     (** realizer for induction rule **)