add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
authorwenzelm
Sun Nov 15 21:58:40 2009 +0100 (2009-11-15)
changeset 337046aeb8454efc1
parent 33703 50b6c07c0dd4
child 33706 7017aee615d6
child 33708 b45d3b8cc74e
add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
explicit extraction_expand vs. extraction_expand_def attribute;
src/HOL/Extraction.thy
src/HOL/Lambda/NormalForm.thy
src/Pure/Proof/extraction.ML
     1.1 --- a/src/HOL/Extraction.thy	Sun Nov 15 20:57:42 2009 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Sun Nov 15 21:58:40 2009 +0100
     1.3 @@ -43,10 +43,12 @@
     1.4    allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
     1.5    notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
     1.6    induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
     1.7 -  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
     1.8    induct_atomize induct_rulify induct_rulify_fallback
     1.9    True_implies_equals TrueE
    1.10  
    1.11 +lemmas [extraction_expand_def] =
    1.12 +  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.13 +
    1.14  datatype sumbool = Left | Right
    1.15  
    1.16  subsection {* Type of extracted program *}
     2.1 --- a/src/HOL/Lambda/NormalForm.thy	Sun Nov 15 20:57:42 2009 +0100
     2.2 +++ b/src/HOL/Lambda/NormalForm.thy	Sun Nov 15 21:58:40 2009 +0100
     2.3 @@ -14,7 +14,7 @@
     2.4    listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
     2.5    "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
     2.6  
     2.7 -declare listall_def [extraction_expand]
     2.8 +declare listall_def [extraction_expand_def]
     2.9  
    2.10  theorem listall_nil: "listall P []"
    2.11    by (simp add: listall_def)
     3.1 --- a/src/Pure/Proof/extraction.ML	Sun Nov 15 20:57:42 2009 +0100
     3.2 +++ b/src/Pure/Proof/extraction.ML	Sun Nov 15 21:58:40 2009 +0100
     3.3 @@ -15,7 +15,7 @@
     3.4      -> theory -> theory
     3.5    val add_realizers : (thm * (string list * string * string)) list
     3.6      -> theory -> theory
     3.7 -  val add_expand_thms : thm list -> theory -> theory
     3.8 +  val add_expand_thm : bool -> thm -> theory -> theory
     3.9    val add_types : (xstring * ((term -> term option) list *
    3.10      (term -> typ -> term -> typ -> term) option)) list -> theory -> theory
    3.11    val extract : (thm * string list) list -> theory -> theory
    3.12 @@ -342,21 +342,16 @@
    3.13  
    3.14  (** expanding theorems / definitions **)
    3.15  
    3.16 -fun add_expand_thm thm thy =
    3.17 +fun add_expand_thm is_def thm thy =
    3.18    let
    3.19      val {realizes_eqns, typeof_eqns, types, realizers,
    3.20        defs, expand, prep} = ExtractionData.get thy;
    3.21  
    3.22      val name = Thm.get_name thm;
    3.23 -    val _ = name <> "" orelse error "add_expand_thms: unnamed theorem";
    3.24 -
    3.25 -    val is_def =
    3.26 -      (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
    3.27 -         (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
    3.28 -           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.axiom thy) name)
    3.29 -       | _ => false) handle TERM _ => false;
    3.30 +    val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
    3.31    in
    3.32 -    (ExtractionData.put (if is_def then
    3.33 +    thy |> ExtractionData.put
    3.34 +      (if is_def then
    3.35          {realizes_eqns = realizes_eqns,
    3.36           typeof_eqns = add_rule ([],
    3.37             Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
    3.38 @@ -366,12 +361,11 @@
    3.39        else
    3.40          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
    3.41           realizers = realizers, defs = defs,
    3.42 -         expand = insert (op =) (name, prop_of thm) expand, prep = prep}) thy)
    3.43 +         expand = insert (op =) (name, prop_of thm) expand, prep = prep})
    3.44    end;
    3.45  
    3.46 -val add_expand_thms = fold add_expand_thm;
    3.47 -
    3.48 -val extraction_expand = Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I);
    3.49 +fun extraction_expand is_def =
    3.50 +  Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm is_def th) I);
    3.51  
    3.52  
    3.53  (** types with computational content **)
    3.54 @@ -431,8 +425,10 @@
    3.55        "(realizes (r) (!!x. PROP P (x))) ==  \
    3.56      \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
    3.57  
    3.58 -   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed extraction_expand)
    3.59 -     "specify theorems / definitions to be expanded during extraction"));
    3.60 +   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
    3.61 +     "specify theorems to be expanded during extraction" #>
    3.62 +   Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
    3.63 +     "specify definitions to be expanded during extraction"));
    3.64  
    3.65  
    3.66  (**** extract program ****)