# HG changeset patch # User bulwahn # Date 1253715612 -7200 # Node ID 2faf1148c062efe1315ce4c976f058538f252522 # Parent f4d179d91af25016ffefa525f9023646dcbf663c handling of definitions diff -r f4d179d91af2 -r 2faf1148c062 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/IsaMakefile Wed Sep 23 16:20:12 2009 +0200 @@ -6,7 +6,7 @@ default: HOL generate: HOL-Generate-HOL HOL-Generate-HOLLight -images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4 +images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4 HOL-MicroJava #Note: keep targets sorted (except for HOL-Library and HOL-ex) test: \ diff -r f4d179d91af2 -r 2faf1148c062 src/HOL/ex/RPred.thy --- a/src/HOL/ex/RPred.thy Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/ex/RPred.thy Wed Sep 23 16:20:12 2009 +0200 @@ -14,13 +14,15 @@ definition return :: "'a => 'a rpred" where "return x = Pair (Predicate.single x)" -definition bind :: "'a rpred \ ('a \ 'b rpred) \ 'b rpred" (infixl "\=" 60) +definition bind :: "'a rpred \ ('a \ 'b rpred) \ 'b rpred" +(* (infixl "\=" 60) *) where "bind RP f = (\s. let (P, s') = RP s; (s1, s2) = Random.split_seed s' in (Predicate.bind P (%a. fst (f a s1)), s2))" -definition supp :: "'a rpred \ 'a rpred \ 'a rpred" (infixl "\" 80) +definition supp :: "'a rpred \ 'a rpred \ 'a rpred" +(* (infixl "\" 80) *) where "supp RP1 RP2 = (\s. let (P1, s') = RP1 s; (P2, s'') = RP2 s' in (upper_semilattice_class.sup P1 P2, s''))" @@ -43,6 +45,8 @@ where "lift_random g = scomp g (Pair o (Predicate.single o fst))" definition map_rpred :: "('a \ 'b) \ ('a rpred \ 'b rpred)" -where "map_rpred f P = P \= (return o f)" +where "map_rpred f P = bind P (return o f)" + +hide (open) const return bind supp end \ No newline at end of file diff -r f4d179d91af2 -r 2faf1148c062 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Sep 23 16:20:12 2009 +0200 +++ b/src/Pure/Isar/code.ML Wed Sep 23 16:20:12 2009 +0200 @@ -781,12 +781,48 @@ end; (** datastructure to log definitions for preprocessing of the predicate compiler **) -(* -structure Predicate_Compile_Preproc_Const_Defs = Named_Thms +(* obviously a clone of Named_Thms *) + +signature PREDICATE_COMPILE_PREPROC_CONST_DEFS = +sig + val get: Proof.context -> thm list + val add_thm: thm -> Context.generic -> Context.generic + val del_thm: thm -> Context.generic -> Context.generic + + val add_attribute : attribute + val del_attribute : attribute + + val add_attrib : Attrib.src + + val setup: theory -> theory +end; + +structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS = +struct + +structure Data = GenericDataFun ( - val name = "predicate_compile_preproc_const_def" - val description = - "definitions of constants as needed by the preprocessing for the predicate compiler" -) -*) + type T = thm list; + val empty = []; + val extend = I; + fun merge _ = Thm.merge_thms; +); + +val get = Data.get o Context.Proof; + +val add_thm = Data.map o Thm.add_thm; +val del_thm = Data.map o Thm.del_thm; + +val add_attribute = Thm.declaration_attribute add_thm; +val del_attribute = Thm.declaration_attribute del_thm; + +val add_attrib = Attrib.internal (K add_attribute) + +val setup = + Attrib.setup (Binding.name "pred_compile_preproc") (Attrib.add_del add_attribute del_attribute) + ("declaration of definition for preprocessing of the predicate compiler") #> + PureThy.add_thms_dynamic (Binding.name "pred_compile_preproc", Data.get); + +end; + structure Code : CODE = struct open Code; end; diff -r f4d179d91af2 -r 2faf1148c062 src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Wed Sep 23 16:20:12 2009 +0200 +++ b/src/Pure/Isar/constdefs.ML Wed Sep 23 16:20:12 2009 +0200 @@ -52,7 +52,7 @@ thy |> Sign.add_consts_i [(b, T, mx)] |> PureThy.add_defs false [((name, def), atts)] - |-> (fn [thm] => Code.add_default_eqn thm); + |-> (fn [thm] => Code.add_default_eqn thm #> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm)); in ((c, T), thy') end; fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy = diff -r f4d179d91af2 -r 2faf1148c062 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Wed Sep 23 16:20:12 2009 +0200 +++ b/src/Pure/Isar/specification.ML Wed Sep 23 16:20:12 2009 +0200 @@ -209,7 +209,7 @@ (var, ((Binding.suffix_name "_raw" name, []), rhs)); val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK - ((name, Predicate_Compile_Preproc_Const_Defs.add :: Code.add_default_eqn_attrib :: atts), + ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib :: Code.add_default_eqn_attrib :: atts), [prove lthy2 th]); val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;