src/Pure/Proof/extraction.ML
changeset 33704 6aeb8454efc1
parent 33522 737589bb9bb8
child 33832 cff42395c246
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun Nov 15 20:57:42 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Nov 15 21:58:40 2009 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4      -> theory -> theory
     1.5    val add_realizers : (thm * (string list * string * string)) list
     1.6      -> theory -> theory
     1.7 -  val add_expand_thms : thm list -> theory -> theory
     1.8 +  val add_expand_thm : bool -> thm -> theory -> theory
     1.9    val add_types : (xstring * ((term -> term option) list *
    1.10      (term -> typ -> term -> typ -> term) option)) list -> theory -> theory
    1.11    val extract : (thm * string list) list -> theory -> theory
    1.12 @@ -342,21 +342,16 @@
    1.13  
    1.14  (** expanding theorems / definitions **)
    1.15  
    1.16 -fun add_expand_thm thm thy =
    1.17 +fun add_expand_thm is_def thm thy =
    1.18    let
    1.19      val {realizes_eqns, typeof_eqns, types, realizers,
    1.20        defs, expand, prep} = ExtractionData.get thy;
    1.21  
    1.22      val name = Thm.get_name thm;
    1.23 -    val _ = name <> "" orelse error "add_expand_thms: unnamed theorem";
    1.24 -
    1.25 -    val is_def =
    1.26 -      (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
    1.27 -         (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
    1.28 -           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.axiom thy) name)
    1.29 -       | _ => false) handle TERM _ => false;
    1.30 +    val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
    1.31    in
    1.32 -    (ExtractionData.put (if is_def then
    1.33 +    thy |> ExtractionData.put
    1.34 +      (if is_def then
    1.35          {realizes_eqns = realizes_eqns,
    1.36           typeof_eqns = add_rule ([],
    1.37             Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
    1.38 @@ -366,12 +361,11 @@
    1.39        else
    1.40          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
    1.41           realizers = realizers, defs = defs,
    1.42 -         expand = insert (op =) (name, prop_of thm) expand, prep = prep}) thy)
    1.43 +         expand = insert (op =) (name, prop_of thm) expand, prep = prep})
    1.44    end;
    1.45  
    1.46 -val add_expand_thms = fold add_expand_thm;
    1.47 -
    1.48 -val extraction_expand = Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I);
    1.49 +fun extraction_expand is_def =
    1.50 +  Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm is_def th) I);
    1.51  
    1.52  
    1.53  (** types with computational content **)
    1.54 @@ -431,8 +425,10 @@
    1.55        "(realizes (r) (!!x. PROP P (x))) ==  \
    1.56      \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
    1.57  
    1.58 -   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed extraction_expand)
    1.59 -     "specify theorems / definitions to be expanded during extraction"));
    1.60 +   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
    1.61 +     "specify theorems to be expanded during extraction" #>
    1.62 +   Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
    1.63 +     "specify definitions to be expanded during extraction"));
    1.64  
    1.65  
    1.66  (**** extract program ****)