handling of definitions
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 326622faf1148c062
parent 32661 f4d179d91af2
child 32663 c2f63118b251
handling of definitions
src/HOL/IsaMakefile
src/HOL/ex/RPred.thy
src/Pure/Isar/code.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  default: HOL
     1.6  generate: HOL-Generate-HOL HOL-Generate-HOLLight
     1.7 -images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
     1.8 +images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4 HOL-MicroJava
     1.9  
    1.10  #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    1.11  test: \
     2.1 --- a/src/HOL/ex/RPred.thy	Wed Sep 23 16:20:12 2009 +0200
     2.2 +++ b/src/HOL/ex/RPred.thy	Wed Sep 23 16:20:12 2009 +0200
     2.3 @@ -14,13 +14,15 @@
     2.4  definition return :: "'a => 'a rpred"
     2.5    where "return x = Pair (Predicate.single x)"
     2.6  
     2.7 -definition bind :: "'a rpred \<Rightarrow> ('a \<Rightarrow> 'b rpred) \<Rightarrow> 'b rpred" (infixl "\<guillemotright>=" 60)
     2.8 +definition bind :: "'a rpred \<Rightarrow> ('a \<Rightarrow> 'b rpred) \<Rightarrow> 'b rpred"
     2.9 +(* (infixl "\<guillemotright>=" 60) *)
    2.10    where "bind RP f =
    2.11    (\<lambda>s. let (P, s') = RP s;
    2.12          (s1, s2) = Random.split_seed s'
    2.13      in (Predicate.bind P (%a. fst (f a s1)), s2))"
    2.14  
    2.15 -definition supp :: "'a rpred \<Rightarrow> 'a rpred \<Rightarrow> 'a rpred" (infixl "\<squnion>" 80)
    2.16 +definition supp :: "'a rpred \<Rightarrow> 'a rpred \<Rightarrow> 'a rpred"
    2.17 +(* (infixl "\<squnion>" 80) *)
    2.18  where
    2.19    "supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s'
    2.20    in (upper_semilattice_class.sup P1 P2, s''))"
    2.21 @@ -43,6 +45,8 @@
    2.22    where "lift_random g = scomp g (Pair o (Predicate.single o fst))"
    2.23  
    2.24  definition map_rpred :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
    2.25 -where "map_rpred f P = P \<guillemotright>= (return o f)"
    2.26 +where "map_rpred f P = bind P (return o f)"
    2.27 +
    2.28 +hide (open) const return bind supp 
    2.29    
    2.30  end
    2.31 \ No newline at end of file
     3.1 --- a/src/Pure/Isar/code.ML	Wed Sep 23 16:20:12 2009 +0200
     3.2 +++ b/src/Pure/Isar/code.ML	Wed Sep 23 16:20:12 2009 +0200
     3.3 @@ -781,12 +781,48 @@
     3.4  end;
     3.5  
     3.6  (** datastructure to log definitions for preprocessing of the predicate compiler **)
     3.7 -(*
     3.8 -structure Predicate_Compile_Preproc_Const_Defs = Named_Thms
     3.9 +(* obviously a clone of Named_Thms *)
    3.10 +
    3.11 +signature PREDICATE_COMPILE_PREPROC_CONST_DEFS =
    3.12 +sig
    3.13 +  val get: Proof.context -> thm list
    3.14 +  val add_thm: thm -> Context.generic -> Context.generic
    3.15 +  val del_thm: thm -> Context.generic -> Context.generic
    3.16 +  
    3.17 +  val add_attribute : attribute
    3.18 +  val del_attribute : attribute
    3.19 +  
    3.20 +  val add_attrib : Attrib.src
    3.21 +  
    3.22 +  val setup: theory -> theory
    3.23 +end;
    3.24 +
    3.25 +structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS =
    3.26 +struct
    3.27 +
    3.28 +structure Data = GenericDataFun
    3.29  (
    3.30 -  val name = "predicate_compile_preproc_const_def"
    3.31 -  val description =
    3.32 -    "definitions of constants as needed by the preprocessing for the predicate compiler"
    3.33 -)
    3.34 -*)
    3.35 +  type T = thm list;
    3.36 +  val empty = [];
    3.37 +  val extend = I;
    3.38 +  fun merge _ = Thm.merge_thms;
    3.39 +);
    3.40 +
    3.41 +val get = Data.get o Context.Proof;
    3.42 +
    3.43 +val add_thm = Data.map o Thm.add_thm;
    3.44 +val del_thm = Data.map o Thm.del_thm;
    3.45 +
    3.46 +val add_attribute = Thm.declaration_attribute add_thm;
    3.47 +val del_attribute = Thm.declaration_attribute del_thm;
    3.48 +
    3.49 +val add_attrib = Attrib.internal (K add_attribute)
    3.50 +
    3.51 +val setup =
    3.52 +  Attrib.setup (Binding.name "pred_compile_preproc") (Attrib.add_del add_attribute del_attribute)
    3.53 +    ("declaration of definition for preprocessing of the predicate compiler") #>
    3.54 +  PureThy.add_thms_dynamic (Binding.name "pred_compile_preproc", Data.get);
    3.55 +
    3.56 +end;
    3.57 +
    3.58  structure Code : CODE = struct open Code; end;
     4.1 --- a/src/Pure/Isar/constdefs.ML	Wed Sep 23 16:20:12 2009 +0200
     4.2 +++ b/src/Pure/Isar/constdefs.ML	Wed Sep 23 16:20:12 2009 +0200
     4.3 @@ -52,7 +52,7 @@
     4.4        thy
     4.5        |> Sign.add_consts_i [(b, T, mx)]
     4.6        |> PureThy.add_defs false [((name, def), atts)]
     4.7 -      |-> (fn [thm] => Code.add_default_eqn thm);
     4.8 +      |-> (fn [thm] => Code.add_default_eqn thm #> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
     4.9    in ((c, T), thy') end;
    4.10  
    4.11  fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
     5.1 --- a/src/Pure/Isar/specification.ML	Wed Sep 23 16:20:12 2009 +0200
     5.2 +++ b/src/Pure/Isar/specification.ML	Wed Sep 23 16:20:12 2009 +0200
     5.3 @@ -209,7 +209,7 @@
     5.4          (var, ((Binding.suffix_name "_raw" name, []), rhs));
     5.5      val ((def_name, [th']), lthy3) = lthy2
     5.6        |> LocalTheory.note Thm.definitionK
     5.7 -        ((name, Predicate_Compile_Preproc_Const_Defs.add :: Code.add_default_eqn_attrib :: atts),
     5.8 +        ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib :: Code.add_default_eqn_attrib :: atts),
     5.9            [prove lthy2 th]);
    5.10  
    5.11      val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;