author | ballarin |
Mon, 08 Mar 2004 12:17:43 +0100 | |
changeset 14445 | 4392cb82018b |
parent 14398 | c5c47703f763 |
child 15098 | 0726e7b15618 |
permissions | -rw-r--r-- |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1 |
(* |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
2 |
Title: Transitivity reasoner for partial and linear orders |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
3 |
Id: $Id$ |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
4 |
Author: Oliver Kutter |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
5 |
Copyright: TU Muenchen |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
6 |
*) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
7 |
|
14445 | 8 |
(* TODO: reduce number of input thms *) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
9 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
10 |
(* |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
11 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
12 |
The packages provides tactics partial_tac and linear_tac that use all |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
13 |
premises of the form |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
14 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
15 |
t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
16 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
17 |
to |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
18 |
1. either derive a contradiction, |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
19 |
in which case the conclusion can be any term, |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
20 |
2. or prove the conclusion, which must be of the same form as the |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
21 |
premises (excluding ~(t < u) and ~(t <= u) for partial orders) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
22 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
23 |
The package is implemented as an ML functor and thus not limited to the |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
24 |
relation <= and friends. It can be instantiated to any partial and/or |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
25 |
linear order --- for example, the divisibility relation "dvd". In |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
26 |
order to instantiate the package for a partial order only, supply |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
27 |
dummy theorems to the rules for linear orders, and don't use |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
28 |
linear_tac! |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
29 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
30 |
*) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
31 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
32 |
signature LESS_ARITH = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
33 |
sig |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
34 |
(* Theorems for partial orders *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
35 |
val less_reflE: thm (* x < x ==> P *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
36 |
val le_refl: thm (* x <= x *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
37 |
val less_imp_le: thm (* x < y ==> x <= y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
38 |
val eqI: thm (* [| x <= y; y <= x |] ==> x = y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
39 |
val eqD1: thm (* x = y ==> x <= y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
40 |
val eqD2: thm (* x = y ==> y <= x *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
41 |
val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
42 |
val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
43 |
val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
44 |
val le_trans: thm (* [| x < y; y < z |] ==> x < z *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
45 |
val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
46 |
val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
47 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
48 |
(* Additional theorems for linear orders *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
49 |
val not_lessD: thm (* ~(x < y) ==> y <= x *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
50 |
val not_leD: thm (* ~(x <= y) ==> y < x *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
51 |
val not_lessI: thm (* y <= x ==> ~(x < y) *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
52 |
val not_leI: thm (* y < x ==> ~(x <= y) *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
53 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
54 |
(* Additional theorems for subgoals of form x ~= y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
55 |
val less_imp_neq : thm (* x < y ==> x ~= y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
56 |
val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
57 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
58 |
(* Analysis of premises and conclusion *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
59 |
(* decomp_x (`x Rel y') should yield (x, Rel, y) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
60 |
where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
61 |
other relation symbols cause an error message *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
62 |
val decomp_part: Sign.sg -> term -> (term * string * term) option |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
63 |
val decomp_lin: Sign.sg -> term -> (term * string * term) option |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
64 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
65 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
66 |
signature TRANS_TAC = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
67 |
sig |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
68 |
val partial_tac: int -> tactic |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
69 |
val linear_tac: int -> tactic |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
70 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
71 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
72 |
functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
73 |
struct |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
74 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
75 |
(* Extract subgoal with signature *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
76 |
fun SUBGOAL goalfun i st = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
77 |
goalfun (List.nth(prems_of st, i-1), i, sign_of_thm st) st |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
78 |
handle Subscript => Seq.empty; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
79 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
80 |
(* Internal datatype for the proof *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
81 |
datatype proof |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
82 |
= Asm of int |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
83 |
| Thm of proof list * thm; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
84 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
85 |
exception Cannot; |
14445 | 86 |
(* Internal exception, raised if conclusion cannot be derived from |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
87 |
assumptions. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
88 |
exception Contr of proof; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
89 |
(* Internal exception, raised if contradiction ( x < x ) was derived *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
90 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
91 |
fun prove asms = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
92 |
let fun pr (Asm i) = nth_elem (i, asms) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
93 |
| pr (Thm (prfs, thm)) = (map pr prfs) MRS thm |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
94 |
in pr end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
95 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
96 |
(* Internal datatype for inequalities *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
97 |
datatype less |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
98 |
= Less of term * term * proof |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
99 |
| Le of term * term * proof |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
100 |
| NotEq of term * term * proof; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
101 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
102 |
(* Misc functions for datatype less *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
103 |
fun lower (Less (x, _, _)) = x |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
104 |
| lower (Le (x, _, _)) = x |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
105 |
| lower (NotEq (x,_,_)) = x; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
106 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
107 |
fun upper (Less (_, y, _)) = y |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
108 |
| upper (Le (_, y, _)) = y |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
109 |
| upper (NotEq (_,y,_)) = y; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
110 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
111 |
fun getprf (Less (_, _, p)) = p |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
112 |
| getprf (Le (_, _, p)) = p |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
113 |
| getprf (NotEq (_,_, p)) = p; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
114 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
115 |
(* ************************************************************************ *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
116 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
117 |
(* mkasm_partial sign (t, n) : Sign.sg -> (Term.term * int) -> less *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
118 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
119 |
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
120 |
(* translated to an element of type less. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
121 |
(* Partial orders only. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
122 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
123 |
(* ************************************************************************ *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
124 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
125 |
fun mkasm_partial sign (t, n) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
126 |
case Less.decomp_part sign t of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
127 |
Some (x, rel, y) => (case rel of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
128 |
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
129 |
else [Less (x, y, Asm n)] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
130 |
| "~<" => [] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
131 |
| "<=" => [Le (x, y, Asm n)] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
132 |
| "~<=" => [] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
133 |
| "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
134 |
Le (y, x, Thm ([Asm n], Less.eqD2))] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
135 |
| "~=" => if (x aconv y) then |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
136 |
raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
137 |
else [ NotEq (x, y, Asm n), |
14445 | 138 |
NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
139 |
| _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
140 |
"''returned by decomp_part.")) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
141 |
| None => []; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
142 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
143 |
(* ************************************************************************ *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
144 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
145 |
(* mkasm_linear sign (t, n) : Sign.sg -> (Term.term * int) -> less *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
146 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
147 |
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
148 |
(* translated to an element of type less. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
149 |
(* Linear orders only. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
150 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
151 |
(* ************************************************************************ *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
152 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
153 |
fun mkasm_linear sign (t, n) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
154 |
case Less.decomp_lin sign t of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
155 |
Some (x, rel, y) => (case rel of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
156 |
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
157 |
else [Less (x, y, Asm n)] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
158 |
| "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
159 |
| "<=" => [Le (x, y, Asm n)] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
160 |
| "~<=" => if (x aconv y) then |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
161 |
raise (Contr (Thm ([Thm ([Asm n], Less.not_leD)], Less.less_reflE))) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
162 |
else [Less (y, x, Thm ([Asm n], Less.not_leD))] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
163 |
| "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
164 |
Le (y, x, Thm ([Asm n], Less.eqD2))] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
165 |
| "~=" => if (x aconv y) then |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
166 |
raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
167 |
else [ NotEq (x, y, Asm n), |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
168 |
NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
169 |
| _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^ |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
170 |
"''returned by decomp_lin.")) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
171 |
| None => []; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
172 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
173 |
(* ************************************************************************ *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
174 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
175 |
(* mkconcl_partial sign t : Sign.sg -> Term.term -> less *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
176 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
177 |
(* Translates conclusion t to an element of type less. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
178 |
(* Partial orders only. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
179 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
180 |
(* ************************************************************************ *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
181 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
182 |
fun mkconcl_partial sign t = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
183 |
case Less.decomp_part sign t of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
184 |
Some (x, rel, y) => (case rel of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
185 |
"<" => ([Less (x, y, Asm ~1)], Asm 0) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
186 |
| "<=" => ([Le (x, y, Asm ~1)], Asm 0) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
187 |
| "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
188 |
Thm ([Asm 0, Asm 1], Less.eqI)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
189 |
| "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
190 |
| _ => raise Cannot) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
191 |
| None => raise Cannot; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
192 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
193 |
(* ************************************************************************ *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
194 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
195 |
(* mkconcl_linear sign t : Sign.sg -> Term.term -> less *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
196 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
197 |
(* Translates conclusion t to an element of type less. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
198 |
(* Linear orders only. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
199 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
200 |
(* ************************************************************************ *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
201 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
202 |
fun mkconcl_linear sign t = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
203 |
case Less.decomp_lin sign t of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
204 |
Some (x, rel, y) => (case rel of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
205 |
"<" => ([Less (x, y, Asm ~1)], Asm 0) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
206 |
| "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
207 |
| "<=" => ([Le (x, y, Asm ~1)], Asm 0) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
208 |
| "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
209 |
| "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
210 |
Thm ([Asm 0, Asm 1], Less.eqI)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
211 |
| "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
212 |
| _ => raise Cannot) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
213 |
| None => raise Cannot; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
214 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
215 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
216 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
217 |
(* mergeLess (less1,less2): less * less -> less *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
218 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
219 |
(* Merge to elements of type less according to the following rules *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
220 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
221 |
(* x < y && y < z ==> x < z *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
222 |
(* x < y && y <= z ==> x < z *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
223 |
(* x <= y && y < z ==> x < z *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
224 |
(* x <= y && y <= z ==> x <= z *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
225 |
(* x <= y && x ~= y ==> x < y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
226 |
(* x ~= y && x <= y ==> x < y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
227 |
(* x < y && x ~= y ==> x < y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
228 |
(* x ~= y && x < y ==> x < y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
229 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
230 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
231 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
232 |
fun mergeLess (Less (x, _, p) , Less (_ , z, q)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
233 |
Less (x, z, Thm ([p,q] , Less.less_trans)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
234 |
| mergeLess (Less (x, _, p) , Le (_ , z, q)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
235 |
Less (x, z, Thm ([p,q] , Less.less_le_trans)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
236 |
| mergeLess (Le (x, _, p) , Less (_ , z, q)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
237 |
Less (x, z, Thm ([p,q] , Less.le_less_trans)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
238 |
| mergeLess (Le (x, z, p) , NotEq (x', z', q)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
239 |
if (x aconv x' andalso z aconv z' ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
240 |
then Less (x, z, Thm ([p,q] , Less.le_neq_trans)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
241 |
else error "linear/partial_tac: internal error le_neq_trans" |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
242 |
| mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
243 |
if (x aconv x' andalso z aconv z') |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
244 |
then Less (x, z, Thm ([p,q] , Less.neq_le_trans)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
245 |
else error "linear/partial_tac: internal error neq_le_trans" |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
246 |
| mergeLess (NotEq (x, z, p) , Less (x' , z', q)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
247 |
if (x aconv x' andalso z aconv z') |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
248 |
then Less ((x' , z', q)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
249 |
else error "linear/partial_tac: internal error neq_less_trans" |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
250 |
| mergeLess (Less (x, z, p) , NotEq (x', z', q)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
251 |
if (x aconv x' andalso z aconv z') |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
252 |
then Less (x, z, p) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
253 |
else error "linear/partial_tac: internal error less_neq_trans" |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
254 |
| mergeLess (Le (x, _, p) , Le (_ , z, q)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
255 |
Le (x, z, Thm ([p,q] , Less.le_trans)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
256 |
| mergeLess (_, _) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
257 |
error "linear/partial_tac: internal error: undefined case"; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
258 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
259 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
260 |
(* ******************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
261 |
(* tr checks for valid transitivity step *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
262 |
(* ******************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
263 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
264 |
infix tr; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
265 |
fun (Less (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
266 |
| (Le (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
267 |
| (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
268 |
| (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
269 |
| _ tr _ = false; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
270 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
271 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
272 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
273 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
274 |
(* transPath (Lesslist, Less): (less list * less) -> less *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
275 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
276 |
(* If a path represented by a list of elements of type less is found, *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
277 |
(* this needs to be contracted to a single element of type less. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
278 |
(* Prior to each transitivity step it is checked whether the step is *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
279 |
(* valid. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
280 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
281 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
282 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
283 |
fun transPath ([],lesss) = lesss |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
284 |
| transPath (x::xs,lesss) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
285 |
if lesss tr x then transPath (xs, mergeLess(lesss,x)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
286 |
else error "linear/partial_tac: internal error transpath"; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
287 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
288 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
289 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
290 |
(* less1 subsumes less2 : less -> less -> bool *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
291 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
292 |
(* subsumes checks whether less1 implies less2 *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
293 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
294 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
295 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
296 |
infix subsumes; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
297 |
fun (Less (x, y, _)) subsumes (Le (x', y', _)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
298 |
(x aconv x' andalso y aconv y') |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
299 |
| (Less (x, y, _)) subsumes (Less (x', y', _)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
300 |
(x aconv x' andalso y aconv y') |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
301 |
| (Le (x, y, _)) subsumes (Le (x', y', _)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
302 |
(x aconv x' andalso y aconv y') |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
303 |
| (Less (x, y, _)) subsumes (NotEq (x', y', _)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
304 |
(x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
305 |
| (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
306 |
(x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
307 |
| (Le _) subsumes (Less _) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
308 |
error "linear/partial_tac: internal error: Le cannot subsume Less" |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
309 |
| _ subsumes _ = false; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
310 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
311 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
312 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
313 |
(* triv_solv less1 : less -> proof Library.option *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
314 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
315 |
(* Solves trivial goal x <= x. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
316 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
317 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
318 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
319 |
fun triv_solv (Le (x, x', _)) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
320 |
if x aconv x' then Some (Thm ([], Less.le_refl)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
321 |
else None |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
322 |
| triv_solv _ = None; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
323 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
324 |
(* ********************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
325 |
(* Graph functions *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
326 |
(* ********************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
327 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
328 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
329 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
330 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
331 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
332 |
(* General: *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
333 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
334 |
(* Inequalities are represented by various types of graphs. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
335 |
(* *) |
14445 | 336 |
(* 1. (Term.term * (Term.term * less) list) list *) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
337 |
(* - Graph of this type is generated from the assumptions, *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
338 |
(* it does contain information on which edge stems from which *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
339 |
(* assumption. *) |
14445 | 340 |
(* - Used to compute strongly connected components *) |
341 |
(* - Used to compute component subgraphs *) |
|
342 |
(* - Used for component subgraphs to reconstruct paths in components*) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
343 |
(* *) |
14445 | 344 |
(* 2. (int * (int * less) list ) list *) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
345 |
(* - Graph of this type is generated from the strong components of *) |
14445 | 346 |
(* graph of type 1. It consists of the strong components of *) |
347 |
(* graph 1, where nodes are indices of the components. *) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
348 |
(* Only edges between components are part of this graph. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
349 |
(* - Used to reconstruct paths between several components. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
350 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
351 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
352 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
353 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
354 |
(* *********************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
355 |
(* Functions for constructing graphs *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
356 |
(* *********************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
357 |
|
14445 | 358 |
fun addEdge (v,d,[]) = [(v,d)] |
359 |
| addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) |
|
360 |
else (u,dl):: (addEdge(v,d,el)); |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
361 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
362 |
(* ********************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
363 |
(* *) |
14445 | 364 |
(* mkGraphs constructs from a list of objects of type less a graph g, *) |
365 |
(* by taking all edges that are candidate for a <=, and a list neqE, by *) |
|
366 |
(* taking all edges that are candiate for a ~= *) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
367 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
368 |
(* ********************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
369 |
|
14445 | 370 |
fun mkGraphs [] = ([],[],[]) |
371 |
| mkGraphs lessList = |
|
372 |
let |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
373 |
|
14445 | 374 |
fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE) |
375 |
| buildGraphs (l::ls, leqG,neqG, neqE) = case l of |
|
376 |
(Less (x,y,p)) => |
|
377 |
buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) , |
|
378 |
addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
379 |
| (Le (x,y,p)) => |
14445 | 380 |
buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) |
381 |
| (NotEq (x,y,p)) => |
|
382 |
buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ; |
|
383 |
||
384 |
in buildGraphs (lessList, [], [], []) end; |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
385 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
386 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
387 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
388 |
(* *) |
14445 | 389 |
(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
390 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
391 |
(* List of successors of u in graph g *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
392 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
393 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
394 |
|
14445 | 395 |
fun adjacent eq_comp ((v,adj)::el) u = |
396 |
if eq_comp (u, v) then adj else adjacent eq_comp el u |
|
397 |
| adjacent _ [] _ = [] |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
398 |
|
14445 | 399 |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
400 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
401 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
402 |
(* transpose g: *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
403 |
(* (''a * ''a list) list -> (''a * ''a list) list *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
404 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
405 |
(* Computes transposed graph g' from g *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
406 |
(* by reversing all edges u -> v to v -> u *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
407 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
408 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
409 |
|
14445 | 410 |
fun transpose eq_comp g = |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
411 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
412 |
(* Compute list of reversed edges for each adjacency list *) |
14445 | 413 |
fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
414 |
| flip (_,nil) = nil |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
415 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
416 |
(* Compute adjacency list for node u from the list of edges |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
417 |
and return a likewise reduced list of edges. The list of edges |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
418 |
is searches for edges starting from u, and these edges are removed. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
419 |
fun gather (u,(v,w)::el) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
420 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
421 |
val (adj,edges) = gather (u,el) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
422 |
in |
14445 | 423 |
if eq_comp (u, v) then (w::adj,edges) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
424 |
else (adj,(v,w)::edges) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
425 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
426 |
| gather (_,nil) = (nil,nil) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
427 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
428 |
(* For every node in the input graph, call gather to find all reachable |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
429 |
nodes in the list of edges *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
430 |
fun assemble ((u,_)::el) edges = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
431 |
let val (adj,edges) = gather (u,edges) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
432 |
in (u,adj) :: assemble el edges |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
433 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
434 |
| assemble nil _ = nil |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
435 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
436 |
(* Compute, for each adjacency list, the list with reversed edges, |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
437 |
and concatenate these lists. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
438 |
val flipped = foldr (op @) ((map flip g),nil) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
439 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
440 |
in assemble g flipped end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
441 |
|
14445 | 442 |
(* *********************************************************************** *) |
443 |
(* *) |
|
444 |
(* scc_term : (term * term list) list -> term list list *) |
|
445 |
(* *) |
|
446 |
(* The following is based on the algorithm for finding strongly connected *) |
|
447 |
(* components described in Introduction to Algorithms, by Cormon, Leiserson*) |
|
448 |
(* and Rivest, section 23.5. The input G is an adjacency list description *) |
|
449 |
(* of a directed graph. The output is a list of the strongly connected *) |
|
450 |
(* components (each a list of vertices). *) |
|
451 |
(* *) |
|
452 |
(* *) |
|
453 |
(* *********************************************************************** *) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
454 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
455 |
fun scc_term G = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
456 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
457 |
(* Ordered list of the vertices that DFS has finished with; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
458 |
most recently finished goes at the head. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
459 |
val finish : term list ref = ref nil |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
460 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
461 |
(* List of vertices which have been visited. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
462 |
val visited : term list ref = ref nil |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
463 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
464 |
fun been_visited v = exists (fn w => w aconv v) (!visited) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
465 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
466 |
(* Given the adjacency list rep of a graph (a list of pairs), |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
467 |
return just the first element of each pair, yielding the |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
468 |
vertex list. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
469 |
val members = map (fn (v,_) => v) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
470 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
471 |
(* Returns the nodes in the DFS tree rooted at u in g *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
472 |
fun dfs_visit g u : term list = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
473 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
474 |
val _ = visited := u :: !visited |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
475 |
val descendents = |
14445 | 476 |
foldr (fn ((v,l),ds) => if been_visited v then ds |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
477 |
else v :: dfs_visit g v @ ds) |
14445 | 478 |
((adjacent (op aconv) g u) ,nil) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
479 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
480 |
finish := u :: !finish; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
481 |
descendents |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
482 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
483 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
484 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
485 |
(* DFS on the graph; apply dfs_visit to each vertex in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
486 |
the graph, checking first to make sure the vertex is |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
487 |
as yet unvisited. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
488 |
app (fn u => if been_visited u then () |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
489 |
else (dfs_visit G u; ())) (members G); |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
490 |
visited := nil; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
491 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
492 |
(* We don't reset finish because its value is used by |
14445 | 493 |
foldl below, and it will never be used again (even |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
494 |
though dfs_visit will continue to modify it). *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
495 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
496 |
(* DFS on the transpose. The vertices returned by |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
497 |
dfs_visit along with u form a connected component. We |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
498 |
collect all the connected components together in a |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
499 |
list, which is what is returned. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
500 |
foldl (fn (comps,u) => |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
501 |
if been_visited u then comps |
14445 | 502 |
else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps)) (nil,(!finish)) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
503 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
504 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
505 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
506 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
507 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
508 |
(* dfs_int_reachable g u: *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
509 |
(* (int * int list) list -> int -> int list *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
510 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
511 |
(* Computes list of all nodes reachable from u in g. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
512 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
513 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
514 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
515 |
fun dfs_int_reachable g u = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
516 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
517 |
(* List of vertices which have been visited. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
518 |
val visited : int list ref = ref nil |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
519 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
520 |
fun been_visited v = exists (fn w => w = v) (!visited) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
521 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
522 |
fun dfs_visit g u : int list = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
523 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
524 |
val _ = visited := u :: !visited |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
525 |
val descendents = |
14445 | 526 |
foldr (fn ((v,l),ds) => if been_visited v then ds |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
527 |
else v :: dfs_visit g v @ ds) |
14445 | 528 |
( ((adjacent (op =) g u)) ,nil) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
529 |
in descendents end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
530 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
531 |
in u :: dfs_visit g u end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
532 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
533 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
534 |
fun indexComps components = |
14445 | 535 |
ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components); |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
536 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
537 |
fun indexNodes IndexComp = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
538 |
flat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp); |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
539 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
540 |
fun getIndex v [] = ~1 |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
541 |
| getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
542 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
543 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
544 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
545 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
546 |
(* *) |
14445 | 547 |
(* dfs eq_comp g u v: *) |
548 |
(* ('a * 'a -> bool) -> ('a *( 'a * less) list) list -> *) |
|
549 |
(* 'a -> 'a -> (bool * ('a * less) list) *) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
550 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
551 |
(* Depth first search of v from u. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
552 |
(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
553 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
554 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
555 |
|
14445 | 556 |
fun dfs eq_comp g u v = |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
557 |
let |
14445 | 558 |
val pred = ref nil; |
559 |
val visited = ref nil; |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
560 |
|
14445 | 561 |
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
562 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
563 |
fun dfs_visit u' = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
564 |
let val _ = visited := u' :: (!visited) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
565 |
|
14445 | 566 |
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
567 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
568 |
in if been_visited v then () |
14445 | 569 |
else (app (fn (v',l) => if been_visited v' then () else ( |
570 |
update (v',l); |
|
571 |
dfs_visit v'; ()) )) (adjacent eq_comp g u') |
|
572 |
end |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
573 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
574 |
dfs_visit u; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
575 |
if (been_visited v) then (true, (!pred)) else (false , []) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
576 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
577 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
578 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
579 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
580 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
581 |
(* completeTermPath u v g: *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
582 |
(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
583 |
(* -> less list *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
584 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
585 |
(* Complete the path from u to v in graph g. Path search is performed *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
586 |
(* with dfs_term g u v. This yields for each node v' its predecessor u' *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
587 |
(* and the edge u' -> v'. Allows traversing graph backwards from v and *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
588 |
(* finding the path u -> v. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
589 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
590 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
591 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
592 |
|
14445 | 593 |
fun completeTermPath u v g = |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
594 |
let |
14445 | 595 |
val (found, tmp) = dfs (op aconv) g u v ; |
596 |
val pred = map snd tmp; |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
597 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
598 |
fun path x y = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
599 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
600 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
601 |
(* find predecessor u of node v and the edge u -> v *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
602 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
603 |
fun lookup v [] = raise Cannot |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
604 |
| lookup v (e::es) = if (upper e) aconv v then e else lookup v es; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
605 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
606 |
(* traverse path backwards and return list of visited edges *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
607 |
fun rev_path v = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
608 |
let val l = lookup v pred |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
609 |
val u = lower l; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
610 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
611 |
if u aconv x then [l] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
612 |
else (rev_path u) @ [l] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
613 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
614 |
in rev_path y end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
615 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
616 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
617 |
if found then (if u aconv v then [(Le (u, v, (Thm ([], Less.le_refl))))] |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
618 |
else path u v ) else raise Cannot |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
619 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
620 |
|
14445 | 621 |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
622 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
623 |
(* *) |
14445 | 624 |
(* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal: *) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
625 |
(* *) |
14445 | 626 |
(* (int * (int * less) list) list * less list * (Term.term * int) list *) |
627 |
(* * ((term * (term * less) list) list) list -> Less -> proof *) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
628 |
(* *) |
14445 | 629 |
(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a *) |
630 |
(* proof for subgoal. Raises exception Cannot if this is not possible. *) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
631 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
632 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
633 |
|
14445 | 634 |
fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal = |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
635 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
636 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
637 |
(* complete path x y from component graph *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
638 |
fun completeComponentPath x y predlist = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
639 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
640 |
val xi = getIndex x ntc |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
641 |
val yi = getIndex y ntc |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
642 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
643 |
fun lookup k [] = raise Cannot |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
644 |
| lookup k ((h,l)::us) = if k = h then l else lookup k us; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
645 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
646 |
fun rev_completeComponentPath y' = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
647 |
let val edge = lookup (getIndex y' ntc) predlist |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
648 |
val u = lower edge |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
649 |
val v = upper edge |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
650 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
651 |
if (getIndex u ntc) = xi then |
14445 | 652 |
(completeTermPath x u (nth_elem(xi, sccSubgraphs)) )@[edge] |
653 |
@(completeTermPath v y' (nth_elem((getIndex y' ntc),sccSubgraphs)) ) |
|
654 |
else (rev_completeComponentPath u)@[edge] |
|
655 |
@(completeTermPath v y' (nth_elem((getIndex y' ntc),sccSubgraphs)) ) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
656 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
657 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
658 |
if x aconv y then |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
659 |
[(Le (x, y, (Thm ([], Less.le_refl))))] |
14445 | 660 |
else ( if xi = yi then completeTermPath x y (nth_elem(xi, sccSubgraphs)) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
661 |
else rev_completeComponentPath y ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
662 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
663 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
664 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
665 |
(* findLess e x y xi yi xreachable yreachable *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
666 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
667 |
(* Find a path from x through e to y, of weight < *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
668 |
(* ******************************************************************* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
669 |
|
14445 | 670 |
fun findLess e x y xi yi xreachable yreachable = |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
671 |
let val u = lower e |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
672 |
val v = upper e |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
673 |
val ui = getIndex u ntc |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
674 |
val vi = getIndex v ntc |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
675 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
676 |
in |
14445 | 677 |
if ui mem xreachable andalso vi mem xreachable andalso |
678 |
ui mem yreachable andalso vi mem yreachable then ( |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
679 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
680 |
(case e of (Less (_, _, _)) => |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
681 |
let |
14445 | 682 |
val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
683 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
684 |
if xufound then ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
685 |
let |
14445 | 686 |
val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
687 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
688 |
if vyfound then ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
689 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
690 |
val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
691 |
val xyLesss = transPath (tl xypath, hd xypath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
692 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
693 |
if xyLesss subsumes subgoal then Some (getprf xyLesss) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
694 |
else None |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
695 |
end) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
696 |
else None |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
697 |
end) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
698 |
else None |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
699 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
700 |
| _ => |
14445 | 701 |
let val (uvfound, uvpred) = dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
702 |
in |
14445 | 703 |
if uvfound then ( |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
704 |
let |
14445 | 705 |
val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
706 |
in |
14445 | 707 |
if xufound then ( |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
708 |
let |
14445 | 709 |
val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
710 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
711 |
if vyfound then ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
712 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
713 |
val uvpath = completeComponentPath u v uvpred |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
714 |
val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
715 |
val xypath = (completeComponentPath x u xupred)@[uvLesss]@(completeComponentPath v y vypred) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
716 |
val xyLesss = transPath (tl xypath, hd xypath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
717 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
718 |
if xyLesss subsumes subgoal then Some (getprf xyLesss) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
719 |
else None |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
720 |
end ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
721 |
else None |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
722 |
end) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
723 |
else None |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
724 |
end ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
725 |
else None |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
726 |
end ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
727 |
) else None |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
728 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
729 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
730 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
731 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
732 |
(* looking for x <= y: any path from x to y is sufficient *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
733 |
case subgoal of (Le (x, y, _)) => ( |
14445 | 734 |
if sccGraph = [] then raise Cannot else ( |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
735 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
736 |
val xi = getIndex x ntc |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
737 |
val yi = getIndex y ntc |
14445 | 738 |
(* searches in sccGraph a path from xi to yi *) |
739 |
val (found, pred) = dfs (op =) sccGraph xi yi |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
740 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
741 |
if found then ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
742 |
let val xypath = completeComponentPath x y pred |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
743 |
val xyLesss = transPath (tl xypath, hd xypath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
744 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
745 |
(case xyLesss of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
746 |
(Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], Less.less_imp_le)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
747 |
else raise Cannot |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
748 |
| _ => if xyLesss subsumes subgoal then (getprf xyLesss) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
749 |
else raise Cannot) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
750 |
end ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
751 |
else raise Cannot |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
752 |
end |
14445 | 753 |
) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
754 |
) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
755 |
(* looking for x < y: particular path required, which is not necessarily |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
756 |
found by normal dfs *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
757 |
| (Less (x, y, _)) => ( |
14445 | 758 |
if sccGraph = [] then raise Cannot else ( |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
759 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
760 |
val xi = getIndex x ntc |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
761 |
val yi = getIndex y ntc |
14445 | 762 |
val sccGraph_transpose = transpose (op =) sccGraph |
763 |
(* all components that can be reached from component xi *) |
|
764 |
val xreachable = dfs_int_reachable sccGraph xi |
|
765 |
(* all comonents reachable from y in the transposed graph sccGraph' *) |
|
766 |
val yreachable = dfs_int_reachable sccGraph_transpose yi |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
767 |
(* for all edges u ~= v or u < v check if they are part of path x < y *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
768 |
fun processNeqEdges [] = raise Cannot |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
769 |
| processNeqEdges (e::es) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
770 |
case (findLess e x y xi yi xreachable yreachable) of (Some prf) => prf |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
771 |
| _ => processNeqEdges es |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
772 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
773 |
in |
14445 | 774 |
processNeqEdges neqE |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
775 |
end |
14445 | 776 |
) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
777 |
) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
778 |
| (NotEq (x, y, _)) => ( |
14445 | 779 |
(* if there aren't any edges that are candidate for a ~= raise Cannot *) |
780 |
if neqE = [] then raise Cannot |
|
781 |
(* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *) |
|
782 |
else if sccSubgraphs = [] then ( |
|
783 |
(case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of |
|
784 |
( Some (NotEq (x, y, p)), NotEq (x', y', _)) => |
|
785 |
if (x aconv x' andalso y aconv y') then p |
|
786 |
else Thm ([p], thm "not_sym") |
|
787 |
| ( Some (Less (x, y, p)), NotEq (x', y', _)) => |
|
788 |
if x aconv x' andalso y aconv y' then (Thm ([p], Less.less_imp_neq)) |
|
789 |
else (Thm ([(Thm ([p], Less.less_imp_neq))], thm "not_sym")) |
|
790 |
| _ => raise Cannot) |
|
791 |
) else ( |
|
792 |
||
793 |
let val xi = getIndex x ntc |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
794 |
val yi = getIndex y ntc |
14445 | 795 |
val sccGraph_transpose = transpose (op =) sccGraph |
796 |
val xreachable = dfs_int_reachable sccGraph xi |
|
797 |
val yreachable = dfs_int_reachable sccGraph_transpose yi |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
798 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
799 |
fun processNeqEdges [] = raise Cannot |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
800 |
| processNeqEdges (e::es) = ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
801 |
let val u = lower e |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
802 |
val v = upper e |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
803 |
val ui = getIndex u ntc |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
804 |
val vi = getIndex v ntc |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
805 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
806 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
807 |
(* if x ~= y follows from edge e *) |
14445 | 808 |
if e subsumes subgoal then ( |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
809 |
case e of (Less (u, v, q)) => ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
810 |
if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
811 |
else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym")) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
812 |
) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
813 |
| (NotEq (u,v, q)) => ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
814 |
if u aconv x andalso v aconv y then q |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
815 |
else (Thm ([q], thm "not_sym")) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
816 |
) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
817 |
) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
818 |
(* if SCC_x is linked to SCC_y via edge e *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
819 |
else if ui = xi andalso vi = yi then ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
820 |
case e of (Less (_, _,_)) => ( |
14445 | 821 |
let val xypath = (completeTermPath x u (nth_elem(ui, sccSubgraphs)) ) @ [e] @ (completeTermPath v y (nth_elem(vi, sccSubgraphs)) ) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
822 |
val xyLesss = transPath (tl xypath, hd xypath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
823 |
in (Thm ([getprf xyLesss], Less.less_imp_neq)) end) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
824 |
| _ => ( |
14445 | 825 |
let |
826 |
val xupath = completeTermPath x u (nth_elem(ui, sccSubgraphs)) |
|
827 |
val uxpath = completeTermPath u x (nth_elem(ui, sccSubgraphs)) |
|
828 |
val vypath = completeTermPath v y (nth_elem(vi, sccSubgraphs)) |
|
829 |
val yvpath = completeTermPath y v (nth_elem(vi, sccSubgraphs)) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
830 |
val xuLesss = transPath (tl xupath, hd xupath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
831 |
val uxLesss = transPath (tl uxpath, hd uxpath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
832 |
val vyLesss = transPath (tl vypath, hd vypath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
833 |
val yvLesss = transPath (tl yvpath, hd yvpath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
834 |
val x_eq_u = (Thm ([(getprf xuLesss),(getprf uxLesss)], Less.eqI)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
835 |
val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], Less.eqI)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
836 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
837 |
(Thm ([x_eq_u , (getprf e), v_eq_y ], Less.eq_neq_eq_imp_neq)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
838 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
839 |
) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
840 |
) else if ui = yi andalso vi = xi then ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
841 |
case e of (Less (_, _,_)) => ( |
14445 | 842 |
let val xypath = (completeTermPath y u (nth_elem(ui, sccSubgraphs)) ) @ [e] @ (completeTermPath v x (nth_elem(vi, sccSubgraphs)) ) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
843 |
val xyLesss = transPath (tl xypath, hd xypath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
844 |
in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
845 |
| _ => ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
846 |
|
14445 | 847 |
let val yupath = completeTermPath y u (nth_elem(ui, sccSubgraphs)) |
848 |
val uypath = completeTermPath u y (nth_elem(ui, sccSubgraphs)) |
|
849 |
val vxpath = completeTermPath v x (nth_elem(vi, sccSubgraphs)) |
|
850 |
val xvpath = completeTermPath x v (nth_elem(vi, sccSubgraphs)) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
851 |
val yuLesss = transPath (tl yupath, hd yupath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
852 |
val uyLesss = transPath (tl uypath, hd uypath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
853 |
val vxLesss = transPath (tl vxpath, hd vxpath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
854 |
val xvLesss = transPath (tl xvpath, hd xvpath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
855 |
val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], Less.eqI)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
856 |
val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
857 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
858 |
(Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], thm "not_sym")) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
859 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
860 |
) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
861 |
) else ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
862 |
(* there exists a path x < y or y < x such that |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
863 |
x ~= y may be concluded *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
864 |
case (findLess e x y xi yi xreachable yreachable) of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
865 |
(Some prf) => (Thm ([prf], Less.less_imp_neq)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
866 |
| None => ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
867 |
let |
14445 | 868 |
val yr = dfs_int_reachable sccGraph yi |
869 |
val xr = dfs_int_reachable sccGraph_transpose xi |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
870 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
871 |
case (findLess e y x yi xi yr xr) of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
872 |
(Some prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
873 |
| _ => processNeqEdges es |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
874 |
end) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
875 |
) end) |
14445 | 876 |
in processNeqEdges neqE end) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
877 |
) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
878 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
879 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
880 |
|
14445 | 881 |
(* ******************************************************************* *) |
882 |
(* *) |
|
883 |
(* mk_sccGraphs components leqG neqG ntc : *) |
|
884 |
(* Term.term list list -> *) |
|
885 |
(* (Term.term * (Term.term * less) list) list -> *) |
|
886 |
(* (Term.term * (Term.term * less) list) list -> *) |
|
887 |
(* (Term.term * int) list -> *) |
|
888 |
(* (int * (int * less) list) list * *) |
|
889 |
(* ((Term.term * (Term.term * less) list) list) list *) |
|
890 |
(* *) |
|
891 |
(* *) |
|
892 |
(* Computes, from graph leqG, list of all its components and the list *) |
|
893 |
(* ntc (nodes, index of component) a graph whose nodes are the *) |
|
894 |
(* indices of the components of g. Egdes of the new graph are *) |
|
895 |
(* only the edges of g linking two components. Also computes for each *) |
|
896 |
(* component the subgraph of leqG that forms this component. *) |
|
897 |
(* *) |
|
898 |
(* For each component SCC_i is checked if there exists a edge in neqG *) |
|
899 |
(* that leads to a contradiction. *) |
|
900 |
(* *) |
|
901 |
(* We have a contradiction for edge u ~= v and u < v if: *) |
|
902 |
(* - u and v are in the same component, *) |
|
903 |
(* that is, a path u <= v and a path v <= u exist, hence u = v. *) |
|
904 |
(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *) |
|
905 |
(* *) |
|
906 |
(* ******************************************************************* *) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
907 |
|
14445 | 908 |
fun mk_sccGraphs _ [] _ _ = ([],[]) |
909 |
| mk_sccGraphs components leqG neqG ntc = |
|
910 |
let |
|
911 |
(* Liste (Index der Komponente, Komponente *) |
|
912 |
val IndexComp = indexComps components; |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
913 |
|
14445 | 914 |
|
915 |
fun handleContr edge g = |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
916 |
(case edge of |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
917 |
(Less (x, y, _)) => ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
918 |
let |
14445 | 919 |
val xxpath = edge :: (completeTermPath y x g ) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
920 |
val xxLesss = transPath (tl xxpath, hd xxpath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
921 |
val q = getprf xxLesss |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
922 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
923 |
raise (Contr (Thm ([q], Less.less_reflE ))) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
924 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
925 |
) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
926 |
| (NotEq (x, y, _)) => ( |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
927 |
let |
14445 | 928 |
val xypath = (completeTermPath x y g ) |
929 |
val yxpath = (completeTermPath y x g ) |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
930 |
val xyLesss = transPath (tl xypath, hd xypath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
931 |
val yxLesss = transPath (tl yxpath, hd yxpath) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
932 |
val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
933 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
934 |
raise (Contr (Thm ([q], Less.less_reflE ))) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
935 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
936 |
) |
14445 | 937 |
| _ => error "trans_tac/handleContr: invalid Contradiction"); |
938 |
||
939 |
||
940 |
(* k is index of the actual component *) |
|
941 |
||
942 |
fun processComponent (k, comp) = |
|
943 |
let |
|
944 |
(* all edges with weight <= of the actual component *) |
|
945 |
val leqEdges = flat (map (adjacent (op aconv) leqG) comp); |
|
946 |
(* all edges with weight ~= of the actual component *) |
|
947 |
val neqEdges = map snd (flat (map (adjacent (op aconv) neqG) comp)); |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
948 |
|
14445 | 949 |
(* find an edge leading to a contradiction *) |
950 |
fun findContr [] = None |
|
951 |
| findContr (e::es) = |
|
952 |
let val ui = (getIndex (lower e) ntc) |
|
953 |
val vi = (getIndex (upper e) ntc) |
|
954 |
in |
|
955 |
if ui = vi then Some e |
|
956 |
else findContr es |
|
957 |
end; |
|
958 |
||
959 |
(* sort edges into component internal edges and |
|
960 |
edges pointing away from the component *) |
|
961 |
fun sortEdges [] (intern,extern) = (intern,extern) |
|
962 |
| sortEdges ((v,l)::es) (intern, extern) = |
|
963 |
let val k' = getIndex v ntc in |
|
964 |
if k' = k then |
|
965 |
sortEdges es (l::intern, extern) |
|
966 |
else sortEdges es (intern, (k',l)::extern) end; |
|
967 |
||
968 |
(* Insert edge into sorted list of edges, where edge is |
|
969 |
only added if |
|
970 |
- it is found for the first time |
|
971 |
- it is a <= edge and no parallel < edge was found earlier |
|
972 |
- it is a < edge |
|
973 |
*) |
|
974 |
fun insert (h,l) [] = [(h,l)] |
|
975 |
| insert (h,l) ((k',l')::es) = if h = k' then ( |
|
976 |
case l of (Less (_, _, _)) => (h,l)::es |
|
977 |
| _ => (case l' of (Less (_, _, _)) => (h,l')::es |
|
978 |
| _ => (k',l)::es) ) |
|
979 |
else (k',l'):: insert (h,l) es; |
|
980 |
||
981 |
(* Reorganise list of edges such that |
|
982 |
- duplicate edges are removed |
|
983 |
- if a < edge and a <= edge exist at the same time, |
|
984 |
remove <= edge *) |
|
985 |
fun reOrganizeEdges [] sorted = sorted: (int * less) list |
|
986 |
| reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted); |
|
987 |
||
988 |
(* construct the subgraph forming the strongly connected component |
|
989 |
from the edge list *) |
|
990 |
fun sccSubGraph [] g = g |
|
991 |
| sccSubGraph (l::ls) g = |
|
992 |
sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g)) |
|
993 |
||
994 |
val (intern, extern) = sortEdges leqEdges ([], []); |
|
995 |
val subGraph = sccSubGraph intern []; |
|
996 |
||
997 |
in |
|
998 |
case findContr neqEdges of Some e => handleContr e subGraph |
|
999 |
| _ => ((k, (reOrganizeEdges (extern) [])), subGraph) |
|
1000 |
end; |
|
1001 |
||
1002 |
val tmp = map processComponent IndexComp |
|
1003 |
in |
|
1004 |
( (map fst tmp), (map snd tmp)) |
|
1005 |
end; |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1006 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1007 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1008 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1009 |
(* solvePartialOrder sign (asms,concl) : *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1010 |
(* Sign.sg -> less list * Term.term -> proof list *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1011 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1012 |
(* Find proof if possible for partial orders. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1013 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1014 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1015 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1016 |
fun solvePartialOrder sign (asms, concl) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1017 |
let |
14445 | 1018 |
val (leqG, neqG, neqE) = mkGraphs asms |
1019 |
val components = scc_term leqG |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1020 |
val ntc = indexNodes (indexComps components) |
14445 | 1021 |
val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1022 |
in |
14445 | 1023 |
let |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1024 |
val (subgoals, prf) = mkconcl_partial sign concl |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1025 |
fun solve facts less = |
14445 | 1026 |
(case triv_solv less of None => findProof (sccGraph, neqE, ntc, sccSubgraphs ) less |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1027 |
| Some prf => prf ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1028 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1029 |
map (solve asms) subgoals |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1030 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1031 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1032 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1033 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1034 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1035 |
(* solveTotalOrder sign (asms,concl) : *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1036 |
(* Sign.sg -> less list * Term.term -> proof list *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1037 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1038 |
(* Find proof if possible for linear orders. *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1039 |
(* *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1040 |
(* *********************************************************************** *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1041 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1042 |
fun solveTotalOrder sign (asms, concl) = |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1043 |
let |
14445 | 1044 |
val (leqG, neqG, neqE) = mkGraphs asms |
1045 |
val components = scc_term leqG |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1046 |
val ntc = indexNodes (indexComps components) |
14445 | 1047 |
val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1048 |
in |
14445 | 1049 |
let |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1050 |
val (subgoals, prf) = mkconcl_linear sign concl |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1051 |
fun solve facts less = |
14445 | 1052 |
(case triv_solv less of None => findProof (sccGraph, neqE, ntc, sccSubgraphs) less |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1053 |
| Some prf => prf ) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1054 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1055 |
map (solve asms) subgoals |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1056 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1057 |
end; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1058 |
|
14445 | 1059 |
(* partial_tac - solves partial orders *) |
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1060 |
val partial_tac = SUBGOAL (fn (A, n, sign) => |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1061 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1062 |
val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1063 |
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1064 |
val C = subst_bounds (rfrees, Logic.strip_assums_concl A) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1065 |
val lesss = flat (ListPair.map (mkasm_partial sign) (Hs, 0 upto (length Hs - 1))) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1066 |
val prfs = solvePartialOrder sign (lesss, C); |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1067 |
val (subgoals, prf) = mkconcl_partial sign C; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1068 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1069 |
METAHYPS (fn asms => |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1070 |
let val thms = map (prove asms) prfs |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1071 |
in rtac (prove thms prf) 1 end) n |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1072 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1073 |
handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1074 |
| Cannot => no_tac |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1075 |
); |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1076 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1077 |
(* linear_tac - solves linear/total orders *) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1078 |
val linear_tac = SUBGOAL (fn (A, n, sign) => |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1079 |
let |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1080 |
val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1081 |
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1082 |
val C = subst_bounds (rfrees, Logic.strip_assums_concl A) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1083 |
val lesss = flat (ListPair.map (mkasm_linear sign) (Hs, 0 upto (length Hs - 1))) |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1084 |
val prfs = solveTotalOrder sign (lesss, C); |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1085 |
val (subgoals, prf) = mkconcl_linear sign C; |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1086 |
in |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1087 |
METAHYPS (fn asms => |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1088 |
let val thms = map (prove asms) prfs |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1089 |
in rtac (prove thms prf) 1 end) n |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1090 |
end |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1091 |
handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1092 |
| Cannot => no_tac); |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1093 |
|
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
diff
changeset
|
1094 |
end; |