author | wenzelm |
Sat, 28 Jun 2008 22:52:03 +0200 | |
changeset 27388 | 226835ea8d2b |
parent 22578 | b0eb5652f210 |
child 29276 | 94b1ffec9201 |
permissions | -rw-r--r-- |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
1 |
(* |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
2 |
Title: Reasoner for simple transitivity and quasi orders. |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
3 |
Id: $Id$ |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
4 |
Author: Oliver Kutter |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
5 |
Copyright: TU Muenchen |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
6 |
*) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
7 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
8 |
(* |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
9 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
10 |
The package provides tactics trans_tac and quasi_tac that use |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
11 |
premises of the form |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
12 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
13 |
t = u, t ~= u, t < u and t <= u |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
14 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
15 |
to |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
16 |
- either derive a contradiction, in which case the conclusion can be |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
17 |
any term, |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
18 |
- or prove the concluson, which must be of the form t ~= u, t < u or |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
19 |
t <= u. |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
20 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
21 |
Details: |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
22 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
23 |
1. trans_tac: |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
24 |
Only premises of form t <= u are used and the conclusion must be of |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
25 |
the same form. The conclusion is proved, if possible, by a chain of |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
26 |
transitivity from the assumptions. |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
27 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
28 |
2. quasi_tac: |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
29 |
<= is assumed to be a quasi order and < its strict relative, defined |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
30 |
as t < u == t <= u & t ~= u. Again, the conclusion is proved from |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
31 |
the assumptions. |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
32 |
Note that the presence of a strict relation is not necessary for |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
33 |
quasi_tac. Configure decomp_quasi to ignore < and ~=. A list of |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
34 |
required theorems for both situations is given below. |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
35 |
*) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
36 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
37 |
signature LESS_ARITH = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
38 |
sig |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
39 |
(* Transitivity of <= |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
40 |
Note that transitivities for < hold for partial orders only. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
41 |
val le_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
42 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
43 |
(* Additional theorem for quasi orders *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
44 |
val le_refl: thm (* x <= x *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
45 |
val eqD1: thm (* x = y ==> x <= y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
46 |
val eqD2: thm (* x = y ==> y <= x *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
47 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
48 |
(* Additional theorems for premises of the form x < y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
49 |
val less_reflE: thm (* x < x ==> P *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
50 |
val less_imp_le : thm (* x < y ==> x <= y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
51 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
52 |
(* Additional theorems for premises of the form x ~= y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
53 |
val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
54 |
val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
55 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
56 |
(* Additional theorem for goals of form x ~= y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
57 |
val less_imp_neq : thm (* x < y ==> x ~= y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
58 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
59 |
(* Analysis of premises and conclusion *) |
15531 | 60 |
(* decomp_x (`x Rel y') should yield SOME (x, Rel, y) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
61 |
where Rel is one of "<", "<=", "=" and "~=", |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
62 |
other relation symbols cause an error message *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
63 |
(* decomp_trans is used by trans_tac, it may only return Rel = "<=" *) |
19250 | 64 |
val decomp_trans: theory -> term -> (term * string * term) option |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
65 |
(* decomp_quasi is used by quasi_tac *) |
19250 | 66 |
val decomp_quasi: theory -> term -> (term * string * term) option |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
67 |
end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
68 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
69 |
signature QUASI_TAC = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
70 |
sig |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
71 |
val trans_tac: int -> tactic |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
72 |
val quasi_tac: int -> tactic |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
73 |
end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
74 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
75 |
functor Quasi_Tac_Fun (Less: LESS_ARITH): QUASI_TAC = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
76 |
struct |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
77 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
78 |
(* Extract subgoal with signature *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
79 |
fun SUBGOAL goalfun i st = |
22578 | 80 |
goalfun (List.nth(prems_of st, i-1), i, Thm.theory_of_thm st) st |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
81 |
handle Subscript => Seq.empty; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
82 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
83 |
(* Internal datatype for the proof *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
84 |
datatype proof |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
85 |
= Asm of int |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
86 |
| Thm of proof list * thm; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
87 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
88 |
exception Cannot; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
89 |
(* Internal exception, raised if conclusion cannot be derived from |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
90 |
assumptions. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
91 |
exception Contr of proof; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
92 |
(* Internal exception, raised if contradiction ( x < x ) was derived *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
93 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
94 |
fun prove asms = |
15570 | 95 |
let fun pr (Asm i) = List.nth (asms, i) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
96 |
| pr (Thm (prfs, thm)) = (map pr prfs) MRS thm |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
97 |
in pr end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
98 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
99 |
(* Internal datatype for inequalities *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
100 |
datatype less |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
101 |
= Less of term * term * proof |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
102 |
| Le of term * term * proof |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
103 |
| NotEq of term * term * proof; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
104 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
105 |
(* Misc functions for datatype less *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
106 |
fun lower (Less (x, _, _)) = x |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
107 |
| lower (Le (x, _, _)) = x |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
108 |
| lower (NotEq (x,_,_)) = x; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
109 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
110 |
fun upper (Less (_, y, _)) = y |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
111 |
| upper (Le (_, y, _)) = y |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
112 |
| upper (NotEq (_,y,_)) = y; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
113 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
114 |
fun getprf (Less (_, _, p)) = p |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
115 |
| getprf (Le (_, _, p)) = p |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
116 |
| getprf (NotEq (_,_, p)) = p; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
117 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
118 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
119 |
(* *) |
19250 | 120 |
(* mkasm_trans sign (t, n) : theory -> (Term.term * int) -> less *) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
121 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
122 |
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
123 |
(* translated to an element of type less. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
124 |
(* Only assumptions of form x <= y are used, all others are ignored *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
125 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
126 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
127 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
128 |
fun mkasm_trans sign (t, n) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
129 |
case Less.decomp_trans sign t of |
15531 | 130 |
SOME (x, rel, y) => |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
131 |
(case rel of |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
132 |
"<=" => [Le (x, y, Asm n)] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
133 |
| _ => error ("trans_tac: unknown relation symbol ``" ^ rel ^ |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
134 |
"''returned by decomp_trans.")) |
15531 | 135 |
| NONE => []; |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
136 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
137 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
138 |
(* *) |
19250 | 139 |
(* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less *) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
140 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
141 |
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
142 |
(* translated to an element of type less. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
143 |
(* Quasi orders only. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
144 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
145 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
146 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
147 |
fun mkasm_quasi sign (t, n) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
148 |
case Less.decomp_quasi sign t of |
15531 | 149 |
SOME (x, rel, y) => (case rel of |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
150 |
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
151 |
else [Less (x, y, Asm n)] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
152 |
| "<=" => [Le (x, y, Asm n)] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
153 |
| "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
154 |
Le (y, x, Thm ([Asm n], Less.eqD2))] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
155 |
| "~=" => if (x aconv y) then |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
156 |
raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
157 |
else [ NotEq (x, y, Asm n), |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
158 |
NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
159 |
| _ => error ("quasi_tac: unknown relation symbol ``" ^ rel ^ |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
160 |
"''returned by decomp_quasi.")) |
15531 | 161 |
| NONE => []; |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
162 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
163 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
164 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
165 |
(* *) |
19250 | 166 |
(* mkconcl_trans sign t : theory -> Term.term -> less *) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
167 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
168 |
(* Translates conclusion t to an element of type less. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
169 |
(* Only for Conclusions of form x <= y or x < y. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
170 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
171 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
172 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
173 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
174 |
fun mkconcl_trans sign t = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
175 |
case Less.decomp_trans sign t of |
15531 | 176 |
SOME (x, rel, y) => (case rel of |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
177 |
"<=" => (Le (x, y, Asm ~1), Asm 0) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
178 |
| _ => raise Cannot) |
15531 | 179 |
| NONE => raise Cannot; |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
180 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
181 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
182 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
183 |
(* *) |
19250 | 184 |
(* mkconcl_quasi sign t : theory -> Term.term -> less *) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
185 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
186 |
(* Translates conclusion t to an element of type less. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
187 |
(* Quasi orders only. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
188 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
189 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
190 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
191 |
fun mkconcl_quasi sign t = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
192 |
case Less.decomp_quasi sign t of |
15531 | 193 |
SOME (x, rel, y) => (case rel of |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
194 |
"<" => ([Less (x, y, Asm ~1)], Asm 0) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
195 |
| "<=" => ([Le (x, y, Asm ~1)], Asm 0) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
196 |
| "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
197 |
| _ => raise Cannot) |
15531 | 198 |
| NONE => raise Cannot; |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
199 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
200 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
201 |
(* ******************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
202 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
203 |
(* mergeLess (less1,less2): less * less -> less *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
204 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
205 |
(* Merge to elements of type less according to the following rules *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
206 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
207 |
(* x <= y && y <= z ==> x <= z *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
208 |
(* x <= y && x ~= y ==> x < y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
209 |
(* x ~= y && x <= y ==> x < y *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
210 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
211 |
(* ******************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
212 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
213 |
fun mergeLess (Le (x, _, p) , Le (_ , z, q)) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
214 |
Le (x, z, Thm ([p,q] , Less.le_trans)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
215 |
| mergeLess (Le (x, z, p) , NotEq (x', z', q)) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
216 |
if (x aconv x' andalso z aconv z' ) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
217 |
then Less (x, z, Thm ([p,q] , Less.le_neq_trans)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
218 |
else error "quasi_tac: internal error le_neq_trans" |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
219 |
| mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
220 |
if (x aconv x' andalso z aconv z') |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
221 |
then Less (x, z, Thm ([p,q] , Less.neq_le_trans)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
222 |
else error "quasi_tac: internal error neq_le_trans" |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
223 |
| mergeLess (_, _) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
224 |
error "quasi_tac: internal error: undefined case"; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
225 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
226 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
227 |
(* ******************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
228 |
(* tr checks for valid transitivity step *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
229 |
(* ******************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
230 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
231 |
infix tr; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
232 |
fun (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
233 |
| _ tr _ = false; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
234 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
235 |
(* ******************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
236 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
237 |
(* transPath (Lesslist, Less): (less list * less) -> less *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
238 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
239 |
(* If a path represented by a list of elements of type less is found, *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
240 |
(* this needs to be contracted to a single element of type less. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
241 |
(* Prior to each transitivity step it is checked whether the step is *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
242 |
(* valid. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
243 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
244 |
(* ******************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
245 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
246 |
fun transPath ([],lesss) = lesss |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
247 |
| transPath (x::xs,lesss) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
248 |
if lesss tr x then transPath (xs, mergeLess(lesss,x)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
249 |
else error "trans/quasi_tac: internal error transpath"; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
250 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
251 |
(* ******************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
252 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
253 |
(* less1 subsumes less2 : less -> less -> bool *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
254 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
255 |
(* subsumes checks whether less1 implies less2 *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
256 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
257 |
(* ******************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
258 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
259 |
infix subsumes; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
260 |
fun (Le (x, y, _)) subsumes (Le (x', y', _)) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
261 |
(x aconv x' andalso y aconv y') |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
262 |
| (Le _) subsumes (Less _) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
263 |
error "trans/quasi_tac: internal error: Le cannot subsume Less" |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
264 |
| (NotEq(x,y,_)) subsumes (NotEq(x',y',_)) = x aconv x' andalso y aconv y' orelse x aconv y' andalso y aconv x' |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
265 |
| _ subsumes _ = false; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
266 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
267 |
(* ******************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
268 |
(* *) |
15531 | 269 |
(* triv_solv less1 : less -> proof option *) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
270 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
271 |
(* Solves trivial goal x <= x. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
272 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
273 |
(* ******************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
274 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
275 |
fun triv_solv (Le (x, x', _)) = |
15531 | 276 |
if x aconv x' then SOME (Thm ([], Less.le_refl)) |
277 |
else NONE |
|
278 |
| triv_solv _ = NONE; |
|
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
279 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
280 |
(* ********************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
281 |
(* Graph functions *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
282 |
(* ********************************************************************* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
283 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
284 |
(* *********************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
285 |
(* Functions for constructing graphs *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
286 |
(* *********************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
287 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
288 |
fun addEdge (v,d,[]) = [(v,d)] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
289 |
| addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
290 |
else (u,dl):: (addEdge(v,d,el)); |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
291 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
292 |
(* ********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
293 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
294 |
(* mkQuasiGraph constructs from a list of objects of type less a graph g, *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
295 |
(* by taking all edges that are candidate for a <=, and a list neqE, by *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
296 |
(* taking all edges that are candiate for a ~= *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
297 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
298 |
(* ********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
299 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
300 |
fun mkQuasiGraph [] = ([],[]) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
301 |
| mkQuasiGraph lessList = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
302 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
303 |
fun buildGraphs ([],leG, neqE) = (leG, neqE) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
304 |
| buildGraphs (l::ls, leG, neqE) = case l of |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
305 |
(Less (x,y,p)) => |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
306 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
307 |
val leEdge = Le (x,y, Thm ([p], Less.less_imp_le)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
308 |
val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)), |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
309 |
NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
310 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
311 |
buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
312 |
end |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
313 |
| (Le (x,y,p)) => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
314 |
| _ => buildGraphs (ls, leG, l::neqE) ; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
315 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
316 |
in buildGraphs (lessList, [], []) end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
317 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
318 |
(* ********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
319 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
320 |
(* mkGraph constructs from a list of objects of type less a graph g *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
321 |
(* Used for plain transitivity chain reasoning. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
322 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
323 |
(* ********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
324 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
325 |
fun mkGraph [] = [] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
326 |
| mkGraph lessList = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
327 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
328 |
fun buildGraph ([],g) = g |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
329 |
| buildGraph (l::ls, g) = buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
330 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
331 |
in buildGraph (lessList, []) end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
332 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
333 |
(* *********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
334 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
335 |
(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
336 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
337 |
(* List of successors of u in graph g *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
338 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
339 |
(* *********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
340 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
341 |
fun adjacent eq_comp ((v,adj)::el) u = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
342 |
if eq_comp (u, v) then adj else adjacent eq_comp el u |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
343 |
| adjacent _ [] _ = [] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
344 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
345 |
(* *********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
346 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
347 |
(* dfs eq_comp g u v: *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
348 |
(* ('a * 'a -> bool) -> ('a *( 'a * less) list) list -> *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
349 |
(* 'a -> 'a -> (bool * ('a * less) list) *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
350 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
351 |
(* Depth first search of v from u. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
352 |
(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
353 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
354 |
(* *********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
355 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
356 |
fun dfs eq_comp g u v = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
357 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
358 |
val pred = ref nil; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
359 |
val visited = ref nil; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
360 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
361 |
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
362 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
363 |
fun dfs_visit u' = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
364 |
let val _ = visited := u' :: (!visited) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
365 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
366 |
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
367 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
368 |
in if been_visited v then () |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
369 |
else (app (fn (v',l) => if been_visited v' then () else ( |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
370 |
update (v',l); |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
371 |
dfs_visit v'; ()) )) (adjacent eq_comp g u') |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
372 |
end |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
373 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
374 |
dfs_visit u; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
375 |
if (been_visited v) then (true, (!pred)) else (false , []) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
376 |
end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
377 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
378 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
379 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
380 |
(* Begin: Quasi Order relevant functions *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
381 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
382 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
383 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
384 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
385 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
386 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
387 |
(* findPath x y g: Term.term -> Term.term -> *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
388 |
(* (Term.term * (Term.term * less list) list) -> *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
389 |
(* (bool, less list) *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
390 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
391 |
(* Searches a path from vertex x to vertex y in Graph g, returns true and *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
392 |
(* the list of edges forming the path, if a path is found, otherwise false *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
393 |
(* and nil. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
394 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
395 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
396 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
397 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
398 |
fun findPath x y g = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
399 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
400 |
val (found, tmp) = dfs (op aconv) g x y ; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
401 |
val pred = map snd tmp; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
402 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
403 |
fun path x y = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
404 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
405 |
(* find predecessor u of node v and the edge u -> v *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
406 |
fun lookup v [] = raise Cannot |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
407 |
| lookup v (e::es) = if (upper e) aconv v then e else lookup v es; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
408 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
409 |
(* traverse path backwards and return list of visited edges *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
410 |
fun rev_path v = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
411 |
let val l = lookup v pred |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
412 |
val u = lower l; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
413 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
414 |
if u aconv x then [l] else (rev_path u) @ [l] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
415 |
end |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
416 |
in rev_path y end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
417 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
418 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
419 |
if found then ( |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
420 |
if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))]) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
421 |
else (found, (path x y) )) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
422 |
else (found,[]) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
423 |
end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
424 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
425 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
426 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
427 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
428 |
(* findQuasiProof (leqG, neqE) subgoal: *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
429 |
(* (Term.term * (Term.term * less list) list) * less list -> less -> proof *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
430 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
431 |
(* Constructs a proof for subgoal by searching a special path in leqG and *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
432 |
(* neqE. Raises Cannot if construction of the proof fails. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
433 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
434 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
435 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
436 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
437 |
(* As the conlusion can be either of form x <= y, x < y or x ~= y we have *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
438 |
(* three cases to deal with. Finding a transitivity path from x to y with label *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
439 |
(* 1. <= *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
440 |
(* This is simply done by searching any path from x to y in the graph leG. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
441 |
(* The graph leG contains only edges with label <=. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
442 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
443 |
(* 2. < *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
444 |
(* A path from x to y with label < can be found by searching a path with *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
445 |
(* label <= from x to y in the graph leG and merging the path x <= y with *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
446 |
(* a parallel edge x ~= y resp. y ~= x to x < y. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
447 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
448 |
(* 3. ~= *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
449 |
(* If the conclusion is of form x ~= y, we can find a proof either directly, *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
450 |
(* if x ~= y or y ~= x are among the assumptions, or by constructing x ~= y if *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
451 |
(* x < y or y < x follows from the assumptions. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
452 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
453 |
fun findQuasiProof (leG, neqE) subgoal = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
454 |
case subgoal of (Le (x,y, _)) => ( |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
455 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
456 |
val (xyLefound,xyLePath) = findPath x y leG |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
457 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
458 |
if xyLefound then ( |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
459 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
460 |
val Le_x_y = (transPath (tl xyLePath, hd xyLePath)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
461 |
in getprf Le_x_y end ) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
462 |
else raise Cannot |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
463 |
end ) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
464 |
| (Less (x,y,_)) => ( |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
465 |
let |
15531 | 466 |
fun findParallelNeq [] = NONE |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
467 |
| findParallelNeq (e::es) = |
15531 | 468 |
if (x aconv (lower e) andalso y aconv (upper e)) then SOME e |
469 |
else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym")))) |
|
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
470 |
else findParallelNeq es ; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
471 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
472 |
(* test if there is a edge x ~= y respectivly y ~= x and *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
473 |
(* if it possible to find a path x <= y in leG, thus we can conclude x < y *) |
15531 | 474 |
(case findParallelNeq neqE of (SOME e) => |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
475 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
476 |
val (xyLeFound,xyLePath) = findPath x y leG |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
477 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
478 |
if xyLeFound then ( |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
479 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
480 |
val Le_x_y = (transPath (tl xyLePath, hd xyLePath)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
481 |
val Less_x_y = mergeLess (e, Le_x_y) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
482 |
in getprf Less_x_y end |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
483 |
) else raise Cannot |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
484 |
end |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
485 |
| _ => raise Cannot) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
486 |
end ) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
487 |
| (NotEq (x,y,_)) => |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
488 |
(* First check if a single premiss is sufficient *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
489 |
(case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of |
15531 | 490 |
(SOME (NotEq (x, y, p)), NotEq (x', y', _)) => |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
491 |
if (x aconv x' andalso y aconv y') then p |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
492 |
else Thm ([p], thm "not_sym") |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
493 |
| _ => raise Cannot |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
494 |
) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
495 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
496 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
497 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
498 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
499 |
(* End: Quasi Order relevant functions *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
500 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
501 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
502 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
503 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
504 |
(* *********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
505 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
506 |
(* solveLeTrans sign (asms,concl) : *) |
19250 | 507 |
(* theory -> less list * Term.term -> proof list *) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
508 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
509 |
(* Solves *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
510 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
511 |
(* *********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
512 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
513 |
fun solveLeTrans sign (asms, concl) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
514 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
515 |
val g = mkGraph asms |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
516 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
517 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
518 |
val (subgoal, prf) = mkconcl_trans sign concl |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
519 |
val (found, path) = findPath (lower subgoal) (upper subgoal) g |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
520 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
521 |
if found then [getprf (transPath (tl path, hd path))] |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
522 |
else raise Cannot |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
523 |
end |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
524 |
end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
525 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
526 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
527 |
(* *********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
528 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
529 |
(* solveQuasiOrder sign (asms,concl) : *) |
19250 | 530 |
(* theory -> less list * Term.term -> proof list *) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
531 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
532 |
(* Find proof if possible for quasi order. *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
533 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
534 |
(* *********************************************************************** *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
535 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
536 |
fun solveQuasiOrder sign (asms, concl) = |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
537 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
538 |
val (leG, neqE) = mkQuasiGraph asms |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
539 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
540 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
541 |
val (subgoals, prf) = mkconcl_quasi sign concl |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
542 |
fun solve facts less = |
15531 | 543 |
(case triv_solv less of NONE => findQuasiProof (leG, neqE) less |
544 |
| SOME prf => prf ) |
|
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
545 |
in map (solve asms) subgoals end |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
546 |
end; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
547 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
548 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
549 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
550 |
(* Tactics *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
551 |
(* *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
552 |
(* - trans_tac *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
553 |
(* - quasi_tac, solves quasi orders *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
554 |
(* ************************************************************************ *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
555 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
556 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
557 |
(* trans_tac - solves transitivity chains over <= *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
558 |
val trans_tac = SUBGOAL (fn (A, n, sign) => |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
559 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
560 |
val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
561 |
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
562 |
val C = subst_bounds (rfrees, Logic.strip_assums_concl A) |
15570 | 563 |
val lesss = List.concat (ListPair.map (mkasm_trans sign) (Hs, 0 upto (length Hs - 1))) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
564 |
val prfs = solveLeTrans sign (lesss, C); |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
565 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
566 |
val (subgoal, prf) = mkconcl_trans sign C; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
567 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
568 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
569 |
METAHYPS (fn asms => |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
570 |
let val thms = map (prove asms) prfs |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
571 |
in rtac (prove thms prf) 1 end) n |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
572 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
573 |
end |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
574 |
handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
575 |
| Cannot => no_tac |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
576 |
); |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
577 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
578 |
(* quasi_tac - solves quasi orders *) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
579 |
val quasi_tac = SUBGOAL (fn (A, n, sign) => |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
580 |
let |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
581 |
val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
582 |
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
583 |
val C = subst_bounds (rfrees, Logic.strip_assums_concl A) |
15570 | 584 |
val lesss = List.concat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1))) |
15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
585 |
val prfs = solveQuasiOrder sign (lesss, C); |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
586 |
val (subgoals, prf) = mkconcl_quasi sign C; |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
587 |
in |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
588 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
589 |
METAHYPS (fn asms => |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
590 |
let val thms = map (prove asms) prfs |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
591 |
in rtac (prove thms prf) 1 end) n |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
592 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
593 |
end |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
594 |
handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
595 |
| Cannot => no_tac |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
596 |
); |
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
597 |
|
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff
changeset
|
598 |
end; |