author | wenzelm |
Thu, 02 Oct 2008 19:59:00 +0200 | |
changeset 28464 | dcc030b52583 |
parent 26834 | 87a5b9ec3863 |
child 30190 | 479806475f3c |
permissions | -rw-r--r-- |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
1 |
(* |
15098 | 2 |
Title: Transitivity reasoner for transitive closures of relations |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
3 |
Id: $Id$ |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
4 |
Author: Oliver Kutter |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
5 |
Copyright: TU Muenchen |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
6 |
*) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
7 |
|
15098 | 8 |
(* |
9 |
||
10 |
The packages provides tactics trancl_tac and rtrancl_tac that prove |
|
11 |
goals of the form |
|
12 |
||
13 |
(x,y) : r^+ and (x,y) : r^* (rtrancl_tac only) |
|
14 |
||
15 |
from premises of the form |
|
16 |
||
17 |
(x,y) : r, (x,y) : r^+ and (x,y) : r^* (rtrancl_tac only) |
|
18 |
||
19 |
by reflexivity and transitivity. The relation r is determined by inspecting |
|
20 |
the conclusion. |
|
21 |
||
22 |
The package is implemented as an ML functor and thus not limited to |
|
23 |
particular constructs for transitive and reflexive-transitive |
|
24 |
closures, neither need relations be represented as sets of pairs. In |
|
25 |
order to instantiate the package for transitive closure only, supply |
|
26 |
dummy theorems to the additional rules for reflexive-transitive |
|
27 |
closures, and don't use rtrancl_tac! |
|
28 |
||
29 |
*) |
|
30 |
||
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
31 |
signature TRANCL_ARITH = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
32 |
sig |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
33 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
34 |
(* theorems for transitive closure *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
35 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
36 |
val r_into_trancl : thm |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
37 |
(* (a,b) : r ==> (a,b) : r^+ *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
38 |
val trancl_trans : thm |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
39 |
(* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
40 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
41 |
(* additional theorems for reflexive-transitive closure *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
42 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
43 |
val rtrancl_refl : thm |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
44 |
(* (a,a): r^* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
45 |
val r_into_rtrancl : thm |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
46 |
(* (a,b) : r ==> (a,b) : r^* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
47 |
val trancl_into_rtrancl : thm |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
48 |
(* (a,b) : r^+ ==> (a,b) : r^* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
49 |
val rtrancl_trancl_trancl : thm |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
50 |
(* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
51 |
val trancl_rtrancl_trancl : thm |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
52 |
(* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
53 |
val rtrancl_trans : thm |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
54 |
(* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
55 |
|
15098 | 56 |
(* decomp: decompose a premise or conclusion |
57 |
||
58 |
Returns one of the following: |
|
59 |
||
15531 | 60 |
NONE if not an instance of a relation, |
61 |
SOME (x, y, r, s) if instance of a relation, where |
|
15098 | 62 |
x: left hand side argument, y: right hand side argument, |
63 |
r: the relation, |
|
64 |
s: the kind of closure, one of |
|
65 |
"r": the relation itself, |
|
66 |
"r^+": transitive closure of the relation, |
|
67 |
"r^*": reflexive-transitive closure of the relation |
|
68 |
*) |
|
69 |
||
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
70 |
val decomp: term -> (term * term * term * string) option |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
71 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
72 |
end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
73 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
74 |
signature TRANCL_TAC = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
75 |
sig |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
76 |
val trancl_tac: int -> tactic; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
77 |
val rtrancl_tac: int -> tactic; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
78 |
end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
79 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
80 |
functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
81 |
struct |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
82 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
83 |
|
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
84 |
datatype proof |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
85 |
= Asm of int |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
86 |
| Thm of proof list * thm; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
87 |
|
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
88 |
exception Cannot; (* internal exception: raised if no proof can be found *) |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
89 |
|
26834
87a5b9ec3863
Terms returned by decomp are now eta-contracted.
berghofe
parents:
22257
diff
changeset
|
90 |
fun decomp t = Option.map (fn (x, y, rel, r) => |
87a5b9ec3863
Terms returned by decomp are now eta-contracted.
berghofe
parents:
22257
diff
changeset
|
91 |
(Envir.beta_eta_contract x, Envir.beta_eta_contract y, |
87a5b9ec3863
Terms returned by decomp are now eta-contracted.
berghofe
parents:
22257
diff
changeset
|
92 |
Envir.beta_eta_contract rel, r)) (Cls.decomp t); |
87a5b9ec3863
Terms returned by decomp are now eta-contracted.
berghofe
parents:
22257
diff
changeset
|
93 |
|
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
94 |
fun prove thy r asms = |
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
95 |
let |
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
96 |
fun inst thm = |
26834
87a5b9ec3863
Terms returned by decomp are now eta-contracted.
berghofe
parents:
22257
diff
changeset
|
97 |
let val SOME (_, _, r', _) = decomp (concl_of thm) |
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
98 |
in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end; |
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
99 |
fun pr (Asm i) = List.nth (asms, i) |
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
100 |
| pr (Thm (prfs, thm)) = map pr prfs MRS inst thm |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
101 |
in pr end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
102 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
103 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
104 |
(* Internal datatype for inequalities *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
105 |
datatype rel |
15098 | 106 |
= Trans of term * term * proof (* R^+ *) |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
107 |
| RTrans of term * term * proof; (* R^* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
108 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
109 |
(* Misc functions for datatype rel *) |
15098 | 110 |
fun lower (Trans (x, _, _)) = x |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
111 |
| lower (RTrans (x,_,_)) = x; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
112 |
|
15098 | 113 |
fun upper (Trans (_, y, _)) = y |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
114 |
| upper (RTrans (_,y,_)) = y; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
115 |
|
15098 | 116 |
fun getprf (Trans (_, _, p)) = p |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
117 |
| getprf (RTrans (_,_, p)) = p; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
118 |
|
15098 | 119 |
(* ************************************************************************ *) |
120 |
(* *) |
|
121 |
(* mkasm_trancl Rel (t,n): term -> (term , int) -> rel list *) |
|
122 |
(* *) |
|
123 |
(* Analyse assumption t with index n with respect to relation Rel: *) |
|
124 |
(* If t is of the form "(x, y) : Rel" (or Rel^+), translate to *) |
|
125 |
(* an object (singleton list) of internal datatype rel. *) |
|
126 |
(* Otherwise return empty list. *) |
|
127 |
(* *) |
|
128 |
(* ************************************************************************ *) |
|
129 |
||
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
130 |
fun mkasm_trancl Rel (t, n) = |
26834
87a5b9ec3863
Terms returned by decomp are now eta-contracted.
berghofe
parents:
22257
diff
changeset
|
131 |
case decomp t of |
15531 | 132 |
SOME (x, y, rel,r) => if rel aconv Rel then |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
133 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
134 |
(case r of |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
135 |
"r" => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
136 |
| "r+" => [Trans (x,y, Asm n)] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
137 |
| "r*" => [] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
138 |
| _ => error ("trancl_tac: unknown relation symbol")) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
139 |
else [] |
15531 | 140 |
| NONE => []; |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
141 |
|
15098 | 142 |
(* ************************************************************************ *) |
143 |
(* *) |
|
144 |
(* mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list *) |
|
145 |
(* *) |
|
146 |
(* Analyse assumption t with index n with respect to relation Rel: *) |
|
147 |
(* If t is of the form "(x, y) : Rel" (or Rel^+ or Rel^* ), translate to *) |
|
148 |
(* an object (singleton list) of internal datatype rel. *) |
|
149 |
(* Otherwise return empty list. *) |
|
150 |
(* *) |
|
151 |
(* ************************************************************************ *) |
|
152 |
||
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
153 |
fun mkasm_rtrancl Rel (t, n) = |
26834
87a5b9ec3863
Terms returned by decomp are now eta-contracted.
berghofe
parents:
22257
diff
changeset
|
154 |
case decomp t of |
15531 | 155 |
SOME (x, y, rel, r) => if rel aconv Rel then |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
156 |
(case r of |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
157 |
"r" => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
158 |
| "r+" => [ Trans (x,y, Asm n)] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
159 |
| "r*" => [ RTrans(x,y, Asm n)] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
160 |
| _ => error ("rtrancl_tac: unknown relation symbol" )) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
161 |
else [] |
15531 | 162 |
| NONE => []; |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
163 |
|
15098 | 164 |
(* ************************************************************************ *) |
165 |
(* *) |
|
166 |
(* mkconcl_trancl t: term -> (term, rel, proof) *) |
|
167 |
(* mkconcl_rtrancl t: term -> (term, rel, proof) *) |
|
168 |
(* *) |
|
169 |
(* Analyse conclusion t: *) |
|
170 |
(* - must be of form "(x, y) : r^+ (or r^* for rtrancl) *) |
|
171 |
(* - returns r *) |
|
172 |
(* - conclusion in internal form *) |
|
173 |
(* - proof object *) |
|
174 |
(* *) |
|
175 |
(* ************************************************************************ *) |
|
176 |
||
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
177 |
fun mkconcl_trancl t = |
26834
87a5b9ec3863
Terms returned by decomp are now eta-contracted.
berghofe
parents:
22257
diff
changeset
|
178 |
case decomp t of |
15531 | 179 |
SOME (x, y, rel, r) => (case r of |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
180 |
"r+" => (rel, Trans (x,y, Asm ~1), Asm 0) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
181 |
| _ => raise Cannot) |
15531 | 182 |
| NONE => raise Cannot; |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
183 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
184 |
fun mkconcl_rtrancl t = |
26834
87a5b9ec3863
Terms returned by decomp are now eta-contracted.
berghofe
parents:
22257
diff
changeset
|
185 |
case decomp t of |
15531 | 186 |
SOME (x, y, rel,r ) => (case r of |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
187 |
"r+" => (rel, Trans (x,y, Asm ~1), Asm 0) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
188 |
| "r*" => (rel, RTrans (x,y, Asm ~1), Asm 0) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
189 |
| _ => raise Cannot) |
15531 | 190 |
| NONE => raise Cannot; |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
191 |
|
15098 | 192 |
(* ************************************************************************ *) |
193 |
(* *) |
|
194 |
(* makeStep (r1, r2): rel * rel -> rel *) |
|
195 |
(* *) |
|
196 |
(* Apply transitivity to r1 and r2, obtaining a new element of r^+ or r^*, *) |
|
197 |
(* according the following rules: *) |
|
198 |
(* *) |
|
199 |
(* ( (a, b) : r^+ , (b,c) : r^+ ) --> (a,c) : r^+ *) |
|
200 |
(* ( (a, b) : r^* , (b,c) : r^+ ) --> (a,c) : r^+ *) |
|
201 |
(* ( (a, b) : r^+ , (b,c) : r^* ) --> (a,c) : r^+ *) |
|
202 |
(* ( (a, b) : r^* , (b,c) : r^* ) --> (a,c) : r^* *) |
|
203 |
(* *) |
|
204 |
(* ************************************************************************ *) |
|
205 |
||
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
206 |
fun makeStep (Trans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_trans)) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
207 |
(* refl. + trans. cls. rules *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
208 |
| makeStep (RTrans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl)) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
209 |
| makeStep (Trans (a,_,p), RTrans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl)) |
15098 | 210 |
| makeStep (RTrans (a,_,p), RTrans(_,c,q)) = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans)); |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
211 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
212 |
(* ******************************************************************* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
213 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
214 |
(* transPath (Clslist, Cls): (rel list * rel) -> rel *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
215 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
216 |
(* If a path represented by a list of elements of type rel is found, *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
217 |
(* this needs to be contracted to a single element of type rel. *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
218 |
(* Prior to each transitivity step it is checked whether the step is *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
219 |
(* valid. *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
220 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
221 |
(* ******************************************************************* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
222 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
223 |
fun transPath ([],acc) = acc |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
224 |
| transPath (x::xs,acc) = transPath (xs, makeStep(acc,x)) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
225 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
226 |
(* ********************************************************************* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
227 |
(* Graph functions *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
228 |
(* ********************************************************************* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
229 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
230 |
(* *********************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
231 |
(* Functions for constructing graphs *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
232 |
(* *********************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
233 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
234 |
fun addEdge (v,d,[]) = [(v,d)] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
235 |
| addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
236 |
else (u,dl):: (addEdge(v,d,el)); |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
237 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
238 |
(* ********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
239 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
240 |
(* mkGraph constructs from a list of objects of type rel a graph g *) |
15098 | 241 |
(* and a list of all edges with label r+. *) |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
242 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
243 |
(* ********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
244 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
245 |
fun mkGraph [] = ([],[]) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
246 |
| mkGraph ys = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
247 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
248 |
fun buildGraph ([],g,zs) = (g,zs) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
249 |
| buildGraph (x::xs, g, zs) = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
250 |
case x of (Trans (_,_,_)) => |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
251 |
buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
252 |
| _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
253 |
in buildGraph (ys, [], []) end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
254 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
255 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
256 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
257 |
(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
258 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
259 |
(* List of successors of u in graph g *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
260 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
261 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
262 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
263 |
fun adjacent eq_comp ((v,adj)::el) u = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
264 |
if eq_comp (u, v) then adj else adjacent eq_comp el u |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
265 |
| adjacent _ [] _ = [] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
266 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
267 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
268 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
269 |
(* dfs eq_comp g u v: *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
270 |
(* ('a * 'a -> bool) -> ('a *( 'a * rel) list) list -> *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
271 |
(* 'a -> 'a -> (bool * ('a * rel) list) *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
272 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
273 |
(* Depth first search of v from u. *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
274 |
(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
275 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
276 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
277 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
278 |
fun dfs eq_comp g u v = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
279 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
280 |
val pred = ref nil; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
281 |
val visited = ref nil; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
282 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
283 |
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
284 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
285 |
fun dfs_visit u' = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
286 |
let val _ = visited := u' :: (!visited) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
287 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
288 |
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
289 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
290 |
in if been_visited v then () |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
291 |
else (app (fn (v',l) => if been_visited v' then () else ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
292 |
update (v',l); |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
293 |
dfs_visit v'; ()) )) (adjacent eq_comp g u') |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
294 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
295 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
296 |
dfs_visit u; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
297 |
if (been_visited v) then (true, (!pred)) else (false , []) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
298 |
end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
299 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
300 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
301 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
302 |
(* transpose g: *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
303 |
(* (''a * ''a list) list -> (''a * ''a list) list *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
304 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
305 |
(* Computes transposed graph g' from g *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
306 |
(* by reversing all edges u -> v to v -> u *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
307 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
308 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
309 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
310 |
fun transpose eq_comp g = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
311 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
312 |
(* Compute list of reversed edges for each adjacency list *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
313 |
fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
314 |
| flip (_,nil) = nil |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
315 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
316 |
(* Compute adjacency list for node u from the list of edges |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
317 |
and return a likewise reduced list of edges. The list of edges |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
318 |
is searches for edges starting from u, and these edges are removed. *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
319 |
fun gather (u,(v,w)::el) = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
320 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
321 |
val (adj,edges) = gather (u,el) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
322 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
323 |
if eq_comp (u, v) then (w::adj,edges) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
324 |
else (adj,(v,w)::edges) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
325 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
326 |
| gather (_,nil) = (nil,nil) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
327 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
328 |
(* For every node in the input graph, call gather to find all reachable |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
329 |
nodes in the list of edges *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
330 |
fun assemble ((u,_)::el) edges = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
331 |
let val (adj,edges) = gather (u,edges) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
332 |
in (u,adj) :: assemble el edges |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
333 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
334 |
| assemble nil _ = nil |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
335 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
336 |
(* Compute, for each adjacency list, the list with reversed edges, |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
337 |
and concatenate these lists. *) |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
338 |
val flipped = foldr (op @) nil (map flip g) |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
339 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
340 |
in assemble g flipped end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
341 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
342 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
343 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
344 |
(* dfs_reachable eq_comp g u: *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
345 |
(* (int * int list) list -> int -> int list *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
346 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
347 |
(* Computes list of all nodes reachable from u in g. *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
348 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
349 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
350 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
351 |
fun dfs_reachable eq_comp g u = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
352 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
353 |
(* List of vertices which have been visited. *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
354 |
val visited = ref nil; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
355 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
356 |
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
357 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
358 |
fun dfs_visit g u = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
359 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
360 |
val _ = visited := u :: !visited |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
361 |
val descendents = |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
362 |
foldr (fn ((v,l),ds) => if been_visited v then ds |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
363 |
else v :: dfs_visit g v @ ds) |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
364 |
nil (adjacent eq_comp g u) |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
365 |
in descendents end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
366 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
367 |
in u :: dfs_visit g u end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
368 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
369 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
370 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
371 |
(* dfs_term_reachable g u: *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
372 |
(* (term * term list) list -> term -> term list *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
373 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
374 |
(* Computes list of all nodes reachable from u in g. *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
375 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
376 |
(* *********************************************************************** *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
377 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
378 |
fun dfs_term_reachable g u = dfs_reachable (op aconv) g u; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
379 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
380 |
(* ************************************************************************ *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
381 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
382 |
(* findPath x y g: Term.term -> Term.term -> *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
383 |
(* (Term.term * (Term.term * rel list) list) -> *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
384 |
(* (bool, rel list) *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
385 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
386 |
(* Searches a path from vertex x to vertex y in Graph g, returns true and *) |
15098 | 387 |
(* the list of edges if path is found, otherwise false and nil. *) |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
388 |
(* *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
389 |
(* ************************************************************************ *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
390 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
391 |
fun findPath x y g = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
392 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
393 |
val (found, tmp) = dfs (op aconv) g x y ; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
394 |
val pred = map snd tmp; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
395 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
396 |
fun path x y = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
397 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
398 |
(* find predecessor u of node v and the edge u -> v *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
399 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
400 |
fun lookup v [] = raise Cannot |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
401 |
| lookup v (e::es) = if (upper e) aconv v then e else lookup v es; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
402 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
403 |
(* traverse path backwards and return list of visited edges *) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
404 |
fun rev_path v = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
405 |
let val l = lookup v pred |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
406 |
val u = lower l; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
407 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
408 |
if u aconv x then [l] else (rev_path u) @ [l] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
409 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
410 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
411 |
in rev_path y end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
412 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
413 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
414 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
415 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
416 |
if found then ( (found, (path x y) )) else (found,[]) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
417 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
418 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
419 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
420 |
end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
421 |
|
15098 | 422 |
(* ************************************************************************ *) |
423 |
(* *) |
|
424 |
(* findRtranclProof g tranclEdges subgoal: *) |
|
425 |
(* (Term.term * (Term.term * rel list) list) -> rel -> proof list *) |
|
426 |
(* *) |
|
427 |
(* Searches in graph g a proof for subgoal. *) |
|
428 |
(* *) |
|
429 |
(* ************************************************************************ *) |
|
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
430 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
431 |
fun findRtranclProof g tranclEdges subgoal = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
432 |
case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
433 |
let val (found, path) = findPath (lower subgoal) (upper subgoal) g |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
434 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
435 |
if found then ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
436 |
let val path' = (transPath (tl path, hd path)) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
437 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
438 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
439 |
case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
440 |
| _ => [getprf path'] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
441 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
442 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
443 |
) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
444 |
else raise Cannot |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
445 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
446 |
) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
447 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
448 |
| (Trans (x,y,_)) => ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
449 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
450 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
451 |
val Vx = dfs_term_reachable g x; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
452 |
val g' = transpose (op aconv) g; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
453 |
val Vy = dfs_term_reachable g' y; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
454 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
455 |
fun processTranclEdges [] = raise Cannot |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
456 |
| processTranclEdges (e::es) = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
457 |
if (upper e) mem Vx andalso (lower e) mem Vx |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
458 |
andalso (upper e) mem Vy andalso (lower e) mem Vy |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
459 |
then ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
460 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
461 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
462 |
if (lower e) aconv x then ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
463 |
if (upper e) aconv y then ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
464 |
[(getprf e)] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
465 |
) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
466 |
else ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
467 |
let |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
468 |
val (found,path) = findPath (upper e) y g |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
469 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
470 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
471 |
if found then ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
472 |
[getprf (transPath (path, e))] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
473 |
) else processTranclEdges es |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
474 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
475 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
476 |
) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
477 |
) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
478 |
else if (upper e) aconv y then ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
479 |
let val (xufound,xupath) = findPath x (lower e) g |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
480 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
481 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
482 |
if xufound then ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
483 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
484 |
let val xuRTranclEdge = transPath (tl xupath, hd xupath) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
485 |
val xyTranclEdge = makeStep(xuRTranclEdge,e) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
486 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
487 |
in [getprf xyTranclEdge] end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
488 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
489 |
) else processTranclEdges es |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
490 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
491 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
492 |
) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
493 |
else ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
494 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
495 |
let val (xufound,xupath) = findPath x (lower e) g |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
496 |
val (vyfound,vypath) = findPath (upper e) y g |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
497 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
498 |
if xufound then ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
499 |
if vyfound then ( |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
500 |
let val xuRTranclEdge = transPath (tl xupath, hd xupath) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
501 |
val vyRTranclEdge = transPath (tl vypath, hd vypath) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
502 |
val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
503 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
504 |
in [getprf xyTranclEdge] end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
505 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
506 |
) else processTranclEdges es |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
507 |
) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
508 |
else processTranclEdges es |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
509 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
510 |
) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
511 |
) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
512 |
else processTranclEdges es; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
513 |
in processTranclEdges tranclEdges end ) |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
514 |
| _ => raise Cannot |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
515 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
516 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
517 |
fun solveTrancl (asms, concl) = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
518 |
let val (g,_) = mkGraph asms |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
519 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
520 |
let val (_, subgoal, _) = mkconcl_trancl concl |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
521 |
val (found, path) = findPath (lower subgoal) (upper subgoal) g |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
522 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
523 |
if found then [getprf (transPath (tl path, hd path))] |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
524 |
else raise Cannot |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
525 |
end |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
526 |
end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
527 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
528 |
fun solveRtrancl (asms, concl) = |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
529 |
let val (g,tranclEdges) = mkGraph asms |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
530 |
val (_, subgoal, _) = mkconcl_rtrancl concl |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
531 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
532 |
findRtranclProof g tranclEdges subgoal |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
533 |
end; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
534 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
535 |
|
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
536 |
val trancl_tac = SUBGOAL (fn (A, n) => fn st => |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
537 |
let |
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
538 |
val thy = theory_of_thm st; |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
539 |
val Hs = Logic.strip_assums_hyp A; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
540 |
val C = Logic.strip_assums_concl A; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
541 |
val (rel,subgoals, prf) = mkconcl_trancl C; |
15570 | 542 |
val prems = List.concat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1))) |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
543 |
val prfs = solveTrancl (prems, C); |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
544 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
545 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
546 |
METAHYPS (fn asms => |
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
547 |
let val thms = map (prove thy rel asms) prfs |
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
548 |
in rtac (prove thy rel thms prf) 1 end) n st |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
549 |
end |
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
550 |
handle Cannot => no_tac st); |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
551 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
552 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
553 |
|
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
554 |
val rtrancl_tac = SUBGOAL (fn (A, n) => fn st => |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
555 |
let |
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
556 |
val thy = theory_of_thm st; |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
557 |
val Hs = Logic.strip_assums_hyp A; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
558 |
val C = Logic.strip_assums_concl A; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
559 |
val (rel,subgoals, prf) = mkconcl_rtrancl C; |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
560 |
|
15570 | 561 |
val prems = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1))) |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
562 |
val prfs = solveRtrancl (prems, C); |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
563 |
in |
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
564 |
METAHYPS (fn asms => |
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
565 |
let val thms = map (prove thy rel asms) prfs |
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
566 |
in rtac (prove thy rel thms prf) 1 end) n st |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
567 |
end |
22257
159bfab776e2
"prove" function now instantiates relation variable in order
berghofe
parents:
15574
diff
changeset
|
568 |
handle Cannot => no_tac st); |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
569 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff
changeset
|
570 |
end; |