author | wenzelm |
Sat, 15 Mar 2008 22:07:31 +0100 | |
changeset 26290 | e025bf1cc0f1 |
parent 26281 | 328fd1c551ef |
child 26307 | 27d3de85c266 |
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 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
5 |
Environment of named facts (admits overriding). Optional indexing by |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
6 |
proposition. |
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 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
9 |
signature FACTS = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
10 |
sig |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
11 |
type T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
12 |
val space_of: T -> NameSpace.T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
13 |
val lookup: T -> string -> thm list option |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
14 |
val dest: T -> (string * thm list) list |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
15 |
val extern: T -> (xstring * thm list) list |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
16 |
val props: T -> thm list |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
17 |
val could_unify: T -> term -> thm list |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
18 |
val empty: T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
19 |
val merge: T * T -> T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
20 |
val add: bool -> NameSpace.naming -> string * thm list -> T -> T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
21 |
val del: string -> T -> T |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
22 |
end; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
23 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
24 |
structure Facts: FACTS = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
25 |
struct |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
26 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
27 |
(* datatype *) |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
28 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
29 |
datatype T = Facts of |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
30 |
{facts: thm list NameSpace.table, |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
31 |
props: thm Net.net}; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
32 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
33 |
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
|
34 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
35 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
36 |
(* named facts *) |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
37 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
38 |
fun facts_of (Facts {facts, ...}) = facts; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
39 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
40 |
val space_of = #1 o facts_of; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
41 |
val lookup = Symtab.lookup o #2 o facts_of; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
42 |
val dest = NameSpace.dest_table o facts_of; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
43 |
val extern = NameSpace.extern_table o facts_of; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
44 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
45 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
46 |
(* indexed props *) |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
47 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
48 |
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
|
49 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
50 |
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
|
51 |
fun could_unify (Facts {props, ...}) = Net.unify_term props; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
52 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
53 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
54 |
(* build facts *) |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
55 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
56 |
val empty = make_facts NameSpace.empty_table Net.empty; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
57 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
58 |
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
|
59 |
let |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
60 |
val facts' = NameSpace.merge_tables (K true) (facts1, facts2); |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
61 |
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
|
62 |
in make_facts facts' props' end; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
63 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
64 |
fun add do_props naming (name, ths) (Facts {facts, props}) = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
65 |
let |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
66 |
val facts' = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
67 |
if name = "" then facts |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
68 |
else |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
69 |
let |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
70 |
val (space, tab) = facts; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
71 |
val space' = NameSpace.declare naming name space; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
72 |
val tab' = Symtab.update (name, ths) tab; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
73 |
in (space', tab') end; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
74 |
val props' = |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
75 |
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
|
76 |
else props; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
77 |
in make_facts facts' props' end; |
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
78 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
79 |
fun del name (Facts {facts = (space, tab), props}) = |
26290 | 80 |
let |
81 |
val space' = NameSpace.hide true name space handle ERROR _ => space; |
|
82 |
val tab' = Symtab.delete_safe name tab; |
|
83 |
in make_facts (space', tab') props end; |
|
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
84 |
|
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset
|
85 |
end; |