author | desharna |
Thu, 09 Jul 2020 11:39:16 +0200 | |
changeset 72004 | 913162a47d9f |
parent 39502 | cffceed8e7fa |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* A STORE FOR UNIT THEOREMS *) |
|
72004 | 3 |
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
structure Units :> Units = |
|
7 |
struct |
|
8 |
||
9 |
open Useful; |
|
10 |
||
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
(* A type of unit store. *) |
|
13 |
(* ------------------------------------------------------------------------- *) |
|
14 |
||
15 |
type unitThm = Literal.literal * Thm.thm; |
|
16 |
||
17 |
datatype units = Units of unitThm LiteralNet.literalNet; |
|
18 |
||
19 |
(* ------------------------------------------------------------------------- *) |
|
20 |
(* Basic operations. *) |
|
21 |
(* ------------------------------------------------------------------------- *) |
|
22 |
||
23 |
val empty = Units (LiteralNet.new {fifo = false}); |
|
24 |
||
25 |
fun size (Units net) = LiteralNet.size net; |
|
26 |
||
27 |
fun toString units = "U{" ^ Int.toString (size units) ^ "}"; |
|
28 |
||
29 |
val pp = Print.ppMap toString Print.ppString; |
|
30 |
||
31 |
(* ------------------------------------------------------------------------- *) |
|
32 |
(* Add units into the store. *) |
|
33 |
(* ------------------------------------------------------------------------- *) |
|
34 |
||
35 |
fun add (units as Units net) (uTh as (lit,th)) = |
|
36 |
let |
|
37 |
val net = LiteralNet.insert net (lit,uTh) |
|
38 |
in |
|
39 |
case total Literal.sym lit of |
|
40 |
NONE => Units net |
|
41 |
| SOME (lit' as (pol,_)) => |
|
42 |
let |
|
43 |
val th' = (if pol then Rule.symEq else Rule.symNeq) lit th |
|
44 |
val net = LiteralNet.insert net (lit',(lit',th')) |
|
45 |
in |
|
46 |
Units net |
|
47 |
end |
|
48 |
end; |
|
49 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
50 |
val addList = List.foldl (fn (th,u) => add u th); |
39348 | 51 |
|
52 |
(* ------------------------------------------------------------------------- *) |
|
53 |
(* Matching. *) |
|
54 |
(* ------------------------------------------------------------------------- *) |
|
55 |
||
56 |
fun match (Units net) lit = |
|
57 |
let |
|
58 |
fun check (uTh as (lit',_)) = |
|
59 |
case total (Literal.match Subst.empty lit') lit of |
|
60 |
NONE => NONE |
|
61 |
| SOME sub => SOME (uTh,sub) |
|
62 |
in |
|
63 |
first check (LiteralNet.match net lit) |
|
64 |
end; |
|
65 |
||
66 |
(* ------------------------------------------------------------------------- *) |
|
67 |
(* Reducing by repeated matching and resolution. *) |
|
68 |
(* ------------------------------------------------------------------------- *) |
|
69 |
||
70 |
fun reduce units = |
|
71 |
let |
|
72 |
fun red1 (lit,news_th) = |
|
73 |
case total Literal.destIrrefl lit of |
|
74 |
SOME tm => |
|
75 |
let |
|
76 |
val (news,th) = news_th |
|
77 |
val th = Thm.resolve lit th (Thm.refl tm) |
|
78 |
in |
|
79 |
(news,th) |
|
80 |
end |
|
81 |
| NONE => |
|
82 |
let |
|
83 |
val lit' = Literal.negate lit |
|
84 |
in |
|
85 |
case match units lit' of |
|
86 |
NONE => news_th |
|
87 |
| SOME ((_,rth),sub) => |
|
88 |
let |
|
89 |
val (news,th) = news_th |
|
90 |
val rth = Thm.subst sub rth |
|
91 |
val th = Thm.resolve lit th rth |
|
92 |
val new = LiteralSet.delete (Thm.clause rth) lit' |
|
93 |
val news = LiteralSet.union new news |
|
94 |
in |
|
95 |
(news,th) |
|
96 |
end |
|
97 |
end |
|
98 |
||
99 |
fun red (news,th) = |
|
100 |
if LiteralSet.null news then th |
|
101 |
else red (LiteralSet.foldl red1 (LiteralSet.empty,th) news) |
|
102 |
in |
|
103 |
fn th => Rule.removeSym (red (Thm.clause th, th)) |
|
104 |
end; |
|
105 |
||
106 |
end |