# HG changeset patch
# User wenzelm
# Date 1258318720 -3600
# Node ID 6aeb8454efc15bf155027a4c4423cb71c2a3771d
# Parent  50b6c07c0dd40e92af73891f5f054beba2664bc9
add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
explicit extraction_expand vs. extraction_expand_def attribute;

diff -r 50b6c07c0dd4 -r 6aeb8454efc1 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Sun Nov 15 20:57:42 2009 +0100
+++ b/src/HOL/Extraction.thy	Sun Nov 15 21:58:40 2009 +0100
@@ -43,10 +43,12 @@
   allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
   notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
   induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
-  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   induct_atomize induct_rulify induct_rulify_fallback
   True_implies_equals TrueE
 
+lemmas [extraction_expand_def] =
+  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
+
 datatype sumbool = Left | Right
 
 subsection {* Type of extracted program *}
diff -r 50b6c07c0dd4 -r 6aeb8454efc1 src/HOL/Lambda/NormalForm.thy
--- a/src/HOL/Lambda/NormalForm.thy	Sun Nov 15 20:57:42 2009 +0100
+++ b/src/HOL/Lambda/NormalForm.thy	Sun Nov 15 21:58:40 2009 +0100
@@ -14,7 +14,7 @@
   listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
 
-declare listall_def [extraction_expand]
+declare listall_def [extraction_expand_def]
 
 theorem listall_nil: "listall P []"
   by (simp add: listall_def)
diff -r 50b6c07c0dd4 -r 6aeb8454efc1 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Nov 15 20:57:42 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Nov 15 21:58:40 2009 +0100
@@ -15,7 +15,7 @@
     -> theory -> theory
   val add_realizers : (thm * (string list * string * string)) list
     -> theory -> theory
-  val add_expand_thms : thm list -> theory -> theory
+  val add_expand_thm : bool -> thm -> theory -> theory
   val add_types : (xstring * ((term -> term option) list *
     (term -> typ -> term -> typ -> term) option)) list -> theory -> theory
   val extract : (thm * string list) list -> theory -> theory
@@ -342,21 +342,16 @@
 
 (** expanding theorems / definitions **)
 
-fun add_expand_thm thm thy =
+fun add_expand_thm is_def thm thy =
   let
     val {realizes_eqns, typeof_eqns, types, realizers,
       defs, expand, prep} = ExtractionData.get thy;
 
     val name = Thm.get_name thm;
-    val _ = name <> "" orelse error "add_expand_thms: unnamed theorem";
-
-    val is_def =
-      (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
-         (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
-           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.axiom thy) name)
-       | _ => false) handle TERM _ => false;
+    val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
   in
-    (ExtractionData.put (if is_def then
+    thy |> ExtractionData.put
+      (if is_def then
         {realizes_eqns = realizes_eqns,
          typeof_eqns = add_rule ([],
            Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
@@ -366,12 +361,11 @@
       else
         {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
          realizers = realizers, defs = defs,
-         expand = insert (op =) (name, prop_of thm) expand, prep = prep}) thy)
+         expand = insert (op =) (name, prop_of thm) expand, prep = prep})
   end;
 
-val add_expand_thms = fold add_expand_thm;
-
-val extraction_expand = Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I);
+fun extraction_expand is_def =
+  Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm is_def th) I);
 
 
 (** types with computational content **)
@@ -431,8 +425,10 @@
       "(realizes (r) (!!x. PROP P (x))) ==  \
     \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
 
-   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed extraction_expand)
-     "specify theorems / definitions to be expanded during extraction"));
+   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
+     "specify theorems to be expanded during extraction" #>
+   Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
+     "specify definitions to be expanded during extraction"));
 
 
 (**** extract program ****)