datatype thmref: added Fact;
authorwenzelm
Fri Oct 28 22:27:59 2005 +0200 (2005-10-28)
changeset 18031b17e25a7d820
parent 18030 5dadabde8fe4
child 18032 3295e9982a5b
datatype thmref: added Fact;
renamed Goal constant to prop;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Fri Oct 28 22:27:58 2005 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Fri Oct 28 22:27:59 2005 +0200
     1.3 @@ -8,7 +8,10 @@
     1.4  signature BASIC_PURE_THY =
     1.5  sig
     1.6    datatype interval = FromTo of int * int | From of int | Single of int
     1.7 -  datatype thmref = Name of string | NameSelection of string * interval list
     1.8 +  datatype thmref =
     1.9 +    Name of string |
    1.10 +    NameSelection of string * interval list |
    1.11 +    Fact of string
    1.12    val print_theorems: theory -> unit
    1.13    val print_theory: theory -> unit
    1.14    val get_thm: theory -> thmref -> thm
    1.15 @@ -19,7 +22,7 @@
    1.16    structure ProtoPure:
    1.17      sig
    1.18        val thy: theory
    1.19 -      val Goal_def: thm
    1.20 +      val prop_def: thm
    1.21      end
    1.22  end;
    1.23  
    1.24 @@ -168,22 +171,27 @@
    1.25  
    1.26  datatype thmref =
    1.27    Name of string |
    1.28 -  NameSelection of string * interval list;
    1.29 +  NameSelection of string * interval list |
    1.30 +  Fact of string;
    1.31  
    1.32  fun name_of_thmref (Name name) = name
    1.33 -  | name_of_thmref (NameSelection (name, _)) = name;
    1.34 +  | name_of_thmref (NameSelection (name, _)) = name
    1.35 +  | name_of_thmref (Fact _) = raise ERROR_MESSAGE "Illegal literal fact";
    1.36  
    1.37  fun map_name_of_thmref f (Name name) = Name (f name)
    1.38 -  | map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is);
    1.39 +  | map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is)
    1.40 +  | map_name_of_thmref _ thmref = thmref;
    1.41  
    1.42  fun string_of_thmref (Name name) = name
    1.43    | string_of_thmref (NameSelection (name, is)) =
    1.44 -      name ^ enclose "(" ")" (commas (map string_of_interval is));
    1.45 +      name ^ enclose "(" ")" (commas (map string_of_interval is))
    1.46 +  | string_of_thmref (Fact _) = raise ERROR_MESSAGE "Illegal literal fact";
    1.47  
    1.48  
    1.49  (* select_thm *)
    1.50  
    1.51  fun select_thm (Name _) thms = thms
    1.52 +  | select_thm (Fact _) thms = thms
    1.53    | select_thm (NameSelection (name, is)) thms =
    1.54        let
    1.55          val n = length thms;
    1.56 @@ -219,7 +227,7 @@
    1.57  fun get_thms_closure thy =
    1.58    let val closures = map lookup_thms (thy :: Theory.ancestors_of thy) in
    1.59      fn thmref =>
    1.60 -      let val name = name_of_thmref thmref
    1.61 +      let val name = name_of_thmref thmref;
    1.62        in select_thm thmref (the_thms name (get_first (fn f => f name) closures)) end
    1.63    end;
    1.64  
    1.65 @@ -317,7 +325,7 @@
    1.66          val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy';
    1.67          val space' = Sign.declare_name thy' name space;
    1.68          val theorems' = Symtab.update (name, thms') theorems;
    1.69 -        val index' = FactIndex.add (K false) (name, thms') index;
    1.70 +        val index' = FactIndex.add_global (name, thms') index;
    1.71        in
    1.72          (case Symtab.lookup theorems name of
    1.73            NONE => ()
    1.74 @@ -507,7 +515,7 @@
    1.75     [("==", "'a => 'a => prop", InfixrName ("==", 2)),
    1.76      ("==>", "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    1.77      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
    1.78 -    ("Goal", "prop => prop", NoSyn),
    1.79 +    ("prop", "prop => prop", NoSyn),
    1.80      ("TYPE", "'a itself", NoSyn),
    1.81      (Term.dummy_patternN, "'a", Delimfix "'_")]
    1.82    |> Theory.add_finals_i false
    1.83 @@ -522,7 +530,7 @@
    1.84    |> Theory.add_trfunsT Syntax.pure_trfunsT
    1.85    |> Sign.local_path
    1.86    |> (#1 oo (add_defs_i false o map Thm.no_attributes))
    1.87 -   [("Goal_def", Logic.mk_equals (Logic.mk_goal A, A))]
    1.88 +   [("prop_def", Logic.mk_equals (Logic.protect A, A))]
    1.89    |> (#1 o add_thmss [(("nothing", []), [])])
    1.90    |> Theory.add_axioms_i Proofterm.equality_axms
    1.91    |> Theory.end_theory;
    1.92 @@ -530,7 +538,7 @@
    1.93  structure ProtoPure =
    1.94  struct
    1.95    val thy = proto_pure;
    1.96 -  val Goal_def = get_axiom thy "Goal_def";
    1.97 +  val prop_def = get_axiom thy "prop_def";
    1.98  end;
    1.99  
   1.100  end;