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