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