author | wenzelm |
Wed, 19 Mar 2008 22:27:57 +0100 | |
changeset 26336 | a0e2b706ce73 |
parent 26307 | 27d3de85c266 |
child 26361 | 7946f459c6c8 |
permissions | -rw-r--r-- |
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/facts.ML |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
4 |
|
26307 | 5 |
Environment of named facts, optionally indexed by proposition. |
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
6 |
*) |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
7 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
8 |
signature FACTS = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
9 |
sig |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
10 |
val the_single: string -> thm list -> thm |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
11 |
datatype interval = FromTo of int * int | From of int | Single of int |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
12 |
datatype ref = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
13 |
Named of string * interval list option | |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
14 |
Fact of string |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
15 |
val string_of_ref: ref -> string |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
16 |
val name_of_ref: ref -> string |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
17 |
val map_name_of_ref: (string -> string) -> ref -> ref |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
18 |
val select: ref -> thm list -> thm list |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
19 |
val selections: string * thm list -> (ref * thm) list |
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
20 |
type T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
21 |
val space_of: T -> NameSpace.T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
22 |
val lookup: T -> string -> thm list option |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
23 |
val dest: T -> (string * thm list) list |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
24 |
val extern: T -> (xstring * thm list) list |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
25 |
val props: T -> thm list |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
26 |
val could_unify: T -> term -> thm list |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
27 |
val empty: T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
28 |
val merge: T * T -> T |
26307 | 29 |
val add_global: NameSpace.naming -> string * thm list -> T -> T |
30 |
val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T |
|
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
31 |
val del: string -> T -> T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
32 |
end; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
33 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
34 |
structure Facts: FACTS = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
35 |
struct |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
36 |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
37 |
(** fact references **) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
38 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
39 |
fun the_single _ [th] : thm = th |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
40 |
| the_single name _ = error ("Single theorem expected " ^ quote name); |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
41 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
42 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
43 |
(* datatype interval *) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
44 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
45 |
datatype interval = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
46 |
FromTo of int * int | |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
47 |
From of int | |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
48 |
Single of int; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
49 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
50 |
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
51 |
| string_of_interval (From i) = string_of_int i ^ "-" |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
52 |
| string_of_interval (Single i) = string_of_int i; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
53 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
54 |
fun interval n iv = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
55 |
let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
56 |
(case iv of |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
57 |
FromTo (i, j) => if i <= j then i upto j else err () |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
58 |
| From i => if i <= n then i upto n else err () |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
59 |
| Single i => [i]) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
60 |
end; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
61 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
62 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
63 |
(* datatype ref *) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
64 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
65 |
datatype ref = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
66 |
Named of string * interval list option | |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
67 |
Fact of string; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
68 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
69 |
fun name_of_ref (Named (name, _)) = name |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
70 |
| name_of_ref (Fact _) = error "Illegal literal fact"; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
71 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
72 |
fun map_name_of_ref f (Named (name, is)) = Named (f name, is) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
73 |
| map_name_of_ref _ r = r; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
74 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
75 |
fun string_of_ref (Named (name, NONE)) = name |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
76 |
| string_of_ref (Named (name, SOME is)) = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
77 |
name ^ enclose "(" ")" (commas (map string_of_interval is)) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
78 |
| string_of_ref (Fact _) = error "Illegal literal fact"; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
79 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
80 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
81 |
(* select *) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
82 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
83 |
fun select (Fact _) ths = ths |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
84 |
| select (Named (_, NONE)) ths = ths |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
85 |
| select (Named (name, SOME ivs)) ths = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
86 |
let |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
87 |
val n = length ths; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
88 |
fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")"); |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
89 |
fun sel i = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
90 |
if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
91 |
else nth ths (i - 1); |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
92 |
val is = maps (interval n) ivs handle Fail msg => err msg; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
93 |
in map sel is end; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
94 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
95 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
96 |
(* selections *) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
97 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
98 |
fun selections (name, [th]) = [(Named (name, NONE), th)] |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
99 |
| selections (name, ths) = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
100 |
map2 (fn i => fn th => (Named (name, SOME [Single i]), th)) (1 upto length ths) ths; |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
101 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
102 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
103 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
104 |
(** fact environment **) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
105 |
|
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset
|
106 |
(* datatype T *) |
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
107 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
108 |
datatype T = Facts of |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
109 |
{facts: thm list NameSpace.table, |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
110 |
props: thm Net.net}; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
111 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
112 |
fun make_facts facts props = Facts {facts = facts, props = props}; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
113 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
114 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
115 |
(* named facts *) |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
116 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
117 |
fun facts_of (Facts {facts, ...}) = facts; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
118 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
119 |
val space_of = #1 o facts_of; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
120 |
val lookup = Symtab.lookup o #2 o facts_of; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
121 |
val dest = NameSpace.dest_table o facts_of; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
122 |
val extern = NameSpace.extern_table o facts_of; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
123 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
124 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
125 |
(* indexed props *) |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
126 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
127 |
val prop_ord = Term.term_ord o pairself Thm.full_prop_of; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
128 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
129 |
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props); |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
130 |
fun could_unify (Facts {props, ...}) = Net.unify_term props; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
131 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
132 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
133 |
(* build facts *) |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
134 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
135 |
val empty = make_facts NameSpace.empty_table Net.empty; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
136 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
137 |
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
138 |
let |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
139 |
val facts' = NameSpace.merge_tables (K true) (facts1, facts2); |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
140 |
val props' = Net.merge (is_equal o prop_ord) (props1, props2); |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
141 |
in make_facts facts' props' end; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
142 |
|
26307 | 143 |
fun add permissive do_props naming (name, ths) (Facts {facts, props}) = |
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
144 |
let |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
145 |
val facts' = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
146 |
if name = "" then facts |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
147 |
else |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
148 |
let |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
149 |
val (space, tab) = facts; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
150 |
val space' = NameSpace.declare naming name space; |
26307 | 151 |
val tab' = (if permissive then Symtab.update else Symtab.update_new) (name, ths) tab |
152 |
handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^ |
|
153 |
Position.str_of (Position.thread_data ())); tab); |
|
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
154 |
in (space', tab') end; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
155 |
val props' = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
156 |
if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
157 |
else props; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
158 |
in make_facts facts' props' end; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
159 |
|
26307 | 160 |
val add_global = add false false; |
161 |
val add_local = add true; |
|
162 |
||
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
163 |
fun del name (Facts {facts = (space, tab), props}) = |
26290 | 164 |
let |
165 |
val space' = NameSpace.hide true name space handle ERROR _ => space; |
|
166 |
val tab' = Symtab.delete_safe name tab; |
|
167 |
in make_facts (space', tab') props end; |
|
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
168 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
169 |
end; |