author  haftmann 
Thu, 18 Nov 2010 17:01:15 +0100  
changeset 40602  91e583511113 
parent 37744  3daaf23b9ab4 
child 42361  23f352990944 
permissions  rwrr 
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, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

5 
*) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

6 

14445  7 
(* TODO: reduce number of input thms *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

8 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

9 
(* 
c5c47703f763
Efficient, graphbased 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, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

12 
premises of the form 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

13 

c5c47703f763
Efficient, graphbased 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, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

15 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

16 
to 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

17 
1. either derive a contradiction, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

18 
in which case the conclusion can be any term, 
c5c47703f763
Efficient, graphbased 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, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

20 
premises (excluding ~(t < u) and ~(t <= u) for partial orders) 
c5c47703f763
Efficient, graphbased 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, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

27 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

28 
*) 
c5c47703f763
Efficient, graphbased 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, graphbased 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, graphbased 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, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

44 
end; 
c5c47703f763
Efficient, graphbased 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, graphbased 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, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

265 
(* Internal datatype for the proof *) 
c5c47703f763
Efficient, graphbased 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, graphbased 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, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

272 
assumptions. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

273 
exception Contr of proof; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

274 
(* Internal exception, raised if contradiction ( x < x ) was derived *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

275 

32215  276 
fun prove asms = 
15570  277 
let fun pr (Asm i) = List.nth (asms, i) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

278 
 pr (Thm (prfs, thm)) = (map pr prfs) MRS thm 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

279 
in pr end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

280 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

281 
(* Internal datatype for inequalities *) 
32215  282 
datatype less 
283 
= Less of term * term * proof 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

284 
 Le of term * term * proof 
32215  285 
 NotEq of term * term * proof; 
286 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

287 
(* Misc functions for datatype less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

288 
fun lower (Less (x, _, _)) = x 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

289 
 lower (Le (x, _, _)) = x 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

290 
 lower (NotEq (x,_,_)) = x; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

291 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

292 
fun upper (Less (_, y, _)) = y 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

293 
 upper (Le (_, y, _)) = y 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

294 
 upper (NotEq (_,y,_)) = y; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

295 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

296 
fun getprf (Less (_, _, p)) = p 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

297 
 getprf (Le (_, _, p)) = p 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

298 
 getprf (NotEq (_,_, p)) = p; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

299 

24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

300 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

301 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

302 
(* *) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

303 
(* mkasm_partial *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

304 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

305 
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

306 
(* translated to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

307 
(* Partial orders only. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

308 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

309 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

310 

33206  311 
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

312 
case decomp sign t of 
15531  313 
SOME (x, rel, y) => (case rel of 
32215  314 
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

315 
else [Less (x, y, Asm n)] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

316 
 "~<" => [] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

317 
 "<=" => [Le (x, y, Asm n)] 
32215  318 
 "~<=" => [] 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

319 
 "=" => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)), 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

320 
Le (y, x, Thm ([Asm n], #eqD2 less_thms))] 
32215  321 
 "~=" => if (x aconv y) then 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

322 
raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

323 
else [ NotEq (x, y, Asm n), 
32215  324 
NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

325 
 _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

326 
"''returned by decomp.")) 
15531  327 
 NONE => []; 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

328 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

329 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

330 
(* *) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

331 
(* mkasm_linear *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

332 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

333 
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

334 
(* translated to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

335 
(* Linear orders only. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

336 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

337 
(* ************************************************************************ *) 
32215  338 

33206  339 
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

340 
case decomp sign t of 
15531  341 
SOME (x, rel, y) => (case rel of 
32215  342 
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

343 
else [Less (x, y, Asm n)] 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

344 
 "~<" => [Le (y, x, Thm ([Asm n], #not_lessD less_thms))] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

345 
 "<=" => [Le (x, y, Asm n)] 
32215  346 
 "~<=" => if (x aconv y) then 
347 
raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms))) 

348 
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

349 
 "=" => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)), 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

350 
Le (y, x, Thm ([Asm n], #eqD2 less_thms))] 
32215  351 
 "~=" => if (x aconv y) then 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

352 
raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

353 
else [ NotEq (x, y, Asm n), 
32215  354 
NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

355 
 _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^ 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

356 
"''returned by decomp.")) 
15531  357 
 NONE => []; 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

358 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

359 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

360 
(* *) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

361 
(* mkconcl_partial *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

362 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

363 
(* Translates conclusion t to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

364 
(* Partial orders only. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

365 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

366 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

367 

24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

368 
fun mkconcl_partial decomp (less_thms : less_arith) sign t = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

369 
case decomp sign t of 
15531  370 
SOME (x, rel, y) => (case rel of 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

371 
"<" => ([Less (x, y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

372 
 "<=" => ([Le (x, y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

373 
 "=" => ([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

374 
Thm ([Asm 0, Asm 1], #eqI less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

375 
 "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

376 
 _ => raise Cannot) 
15531  377 
 NONE => raise Cannot; 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

378 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

379 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

380 
(* *) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

381 
(* mkconcl_linear *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

382 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

383 
(* Translates conclusion t to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

384 
(* Linear orders only. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

385 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

386 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

387 

24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

388 
fun mkconcl_linear decomp (less_thms : less_arith) sign t = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

389 
case decomp sign t of 
15531  390 
SOME (x, rel, y) => (case rel of 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

391 
"<" => ([Less (x, y, Asm ~1)], Asm 0) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

392 
 "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], #not_lessI less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

393 
 "<=" => ([Le (x, y, Asm ~1)], Asm 0) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

394 
 "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], #not_leI less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

395 
 "=" => ([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

396 
Thm ([Asm 0, Asm 1], #eqI less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

397 
 "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

398 
 _ => raise Cannot) 
15531  399 
 NONE => raise Cannot; 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

400 

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 
(*** The common part for partial and linear orders ***) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

403 

9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

404 
(* Analysis of premises and conclusion: *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

405 
(* decomp (`x Rel y') should yield (x, Rel, y) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

406 
where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

407 
other relation symbols cause an error message *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

408 

32215  409 
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

410 

9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

411 
let 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

412 

26834
87a5b9ec3863
Terms returned by decomp are now etacontracted.
berghofe
parents:
24704
diff
changeset

413 
fun decomp sign t = Option.map (fn (x, rel, y) => 
87a5b9ec3863
Terms returned by decomp are now etacontracted.
berghofe
parents:
24704
diff
changeset

414 
(Envir.beta_eta_contract x, rel, Envir.beta_eta_contract y)) (decomp' sign t); 
87a5b9ec3863
Terms returned by decomp are now etacontracted.
berghofe
parents:
24704
diff
changeset

415 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

416 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

417 
(* *) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

418 
(* mergeLess *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

419 
(* *) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

420 
(* Merge two elements of type less according to the following rules *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

421 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

422 
(* x < y && y < z ==> x < z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

423 
(* x < y && y <= z ==> x < z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

424 
(* x <= y && y < z ==> x < z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

425 
(* x <= y && y <= z ==> x <= z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

426 
(* x <= y && x ~= y ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

427 
(* x ~= y && x <= y ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

428 
(* x < y && x ~= y ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

429 
(* x ~= y && x < y ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

430 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

431 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

432 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

433 
fun mergeLess (Less (x, _, p) , Less (_ , z, q)) = 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

434 
Less (x, z, Thm ([p,q] , #less_trans less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

435 
 mergeLess (Less (x, _, p) , Le (_ , z, q)) = 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

436 
Less (x, z, Thm ([p,q] , #less_le_trans less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

437 
 mergeLess (Le (x, _, p) , Less (_ , z, q)) = 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

438 
Less (x, z, Thm ([p,q] , #le_less_trans less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

439 
 mergeLess (Le (x, z, p) , NotEq (x', z', q)) = 
32215  440 
if (x aconv x' andalso z aconv z' ) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

441 
then Less (x, z, Thm ([p,q] , #le_neq_trans less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

442 
else error "linear/partial_tac: internal error le_neq_trans" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

443 
 mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = 
32215  444 
if (x aconv x' andalso z aconv z') 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

445 
then Less (x, z, Thm ([p,q] , #neq_le_trans less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

446 
else error "linear/partial_tac: internal error neq_le_trans" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

447 
 mergeLess (NotEq (x, z, p) , Less (x' , z', q)) = 
32215  448 
if (x aconv x' andalso z aconv z') 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

449 
then Less ((x' , z', q)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

450 
else error "linear/partial_tac: internal error neq_less_trans" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

451 
 mergeLess (Less (x, z, p) , NotEq (x', z', q)) = 
32215  452 
if (x aconv x' andalso z aconv z') 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

453 
then Less (x, z, p) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

454 
else error "linear/partial_tac: internal error less_neq_trans" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

455 
 mergeLess (Le (x, _, p) , Le (_ , z, q)) = 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

456 
Le (x, z, Thm ([p,q] , #le_trans less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

457 
 mergeLess (_, _) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

458 
error "linear/partial_tac: internal error: undefined case"; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

459 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

460 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

461 
(* ******************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

462 
(* tr checks for valid transitivity step *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

463 
(* ******************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

464 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

465 
infix tr; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

466 
fun (Less (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

467 
 (Le (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

468 
 (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

469 
 (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

470 
 _ tr _ = false; 
32215  471 

472 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

473 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

474 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

475 
(* transPath (Lesslist, Less): (less list * less) > less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

476 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

477 
(* If a path represented by a list of elements of type less is found, *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

478 
(* this needs to be contracted to a single element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

479 
(* Prior to each transitivity step it is checked whether the step is *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

480 
(* valid. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

481 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

482 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

483 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

484 
fun transPath ([],lesss) = lesss 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

485 
 transPath (x::xs,lesss) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

486 
if lesss tr x then transPath (xs, mergeLess(lesss,x)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

487 
else error "linear/partial_tac: internal error transpath"; 
32215  488 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

489 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

490 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

491 
(* less1 subsumes less2 : less > less > bool *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

492 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

493 
(* subsumes checks whether less1 implies less2 *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

494 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

495 
(* ******************************************************************* *) 
32215  496 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

497 
infix subsumes; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

498 
fun (Less (x, y, _)) subsumes (Le (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

499 
(x aconv x' andalso y aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

500 
 (Less (x, y, _)) subsumes (Less (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

501 
(x aconv x' andalso y aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

502 
 (Le (x, y, _)) subsumes (Le (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

503 
(x aconv x' andalso y aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

504 
 (Less (x, y, _)) subsumes (NotEq (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

505 
(x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

506 
 (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

507 
(x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

508 
 (Le _) subsumes (Less _) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

509 
error "linear/partial_tac: internal error: Le cannot subsume Less" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

510 
 _ subsumes _ = false; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

511 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

512 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

513 
(* *) 
15531  514 
(* triv_solv less1 : less > proof option *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

515 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

516 
(* Solves trivial goal x <= x. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

517 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

518 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

519 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

520 
fun triv_solv (Le (x, x', _)) = 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

521 
if x aconv x' then SOME (Thm ([], #le_refl less_thms)) 
15531  522 
else NONE 
523 
 triv_solv _ = NONE; 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

524 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

525 
(* ********************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

526 
(* Graph functions *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

527 
(* ********************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

528 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

529 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

530 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

531 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

532 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

533 
(* General: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

534 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

535 
(* Inequalities are represented by various types of graphs. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

536 
(* *) 
14445  537 
(* 1. (Term.term * (Term.term * less) list) list *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

538 
(*  Graph of this type is generated from the assumptions, *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

539 
(* it does contain information on which edge stems from which *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

540 
(* assumption. *) 
14445  541 
(*  Used to compute strongly connected components *) 
542 
(*  Used to compute component subgraphs *) 

543 
(*  Used for component subgraphs to reconstruct paths in components*) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

544 
(* *) 
14445  545 
(* 2. (int * (int * less) list ) list *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

546 
(*  Graph of this type is generated from the strong components of *) 
14445  547 
(* graph of type 1. It consists of the strong components of *) 
548 
(* graph 1, where nodes are indices of the components. *) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

549 
(* Only edges between components are part of this graph. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

550 
(*  Used to reconstruct paths between several components. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

551 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

552 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

553 

32215  554 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

555 
(* *********************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

556 
(* Functions for constructing graphs *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

557 
(* *********************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

558 

14445  559 
fun addEdge (v,d,[]) = [(v,d)] 
560 
 addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) 

561 
else (u,dl):: (addEdge(v,d,el)); 

32215  562 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

563 
(* ********************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

564 
(* *) 
32215  565 
(* mkGraphs constructs from a list of objects of type less a graph g, *) 
14445  566 
(* by taking all edges that are candidate for a <=, and a list neqE, by *) 
567 
(* taking all edges that are candiate for a ~= *) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

568 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

569 
(* ********************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

570 

14445  571 
fun mkGraphs [] = ([],[],[]) 
32215  572 
 mkGraphs lessList = 
14445  573 
let 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

574 

14445  575 
fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE) 
32215  576 
 buildGraphs (l::ls, leqG,neqG, neqE) = case l of 
577 
(Less (x,y,p)) => 

578 
buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) , 

579 
addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

580 
 (Le (x,y,p)) => 
32215  581 
buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) 
582 
 (NotEq (x,y,p)) => 

14445  583 
buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ; 
584 

585 
in buildGraphs (lessList, [], [], []) end; 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

586 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

587 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

588 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

589 
(* *) 
14445  590 
(* adjacent g u : (''a * 'b list ) list > ''a > 'b list *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

591 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

592 
(* List of successors of u in graph g *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

593 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

594 
(* *********************************************************************** *) 
32215  595 

596 
fun adjacent eq_comp ((v,adj)::el) u = 

14445  597 
if eq_comp (u, v) then adj else adjacent eq_comp el u 
32215  598 
 adjacent _ [] _ = [] 
599 

600 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

601 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

602 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

603 
(* transpose g: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

604 
(* (''a * ''a list) list > (''a * ''a list) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

605 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

606 
(* Computes transposed graph g' from g *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

607 
(* by reversing all edges u > v to v > u *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

608 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

609 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

610 

14445  611 
fun transpose eq_comp g = 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

612 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

613 
(* Compute list of reversed edges for each adjacency list *) 
14445  614 
fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el) 
32768  615 
 flip (_,[]) = [] 
32215  616 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

617 
(* Compute adjacency list for node u from the list of edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

618 
and return a likewise reduced list of edges. The list of edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

619 
is searches for edges starting from u, and these edges are removed. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

620 
fun gather (u,(v,w)::el) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

621 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

622 
val (adj,edges) = gather (u,el) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

623 
in 
14445  624 
if eq_comp (u, v) then (w::adj,edges) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

625 
else (adj,(v,w)::edges) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

626 
end 
32768  627 
 gather (_,[]) = ([],[]) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

628 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

629 
(* For every node in the input graph, call gather to find all reachable 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

630 
nodes in the list of edges *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

631 
fun assemble ((u,_)::el) edges = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

632 
let val (adj,edges) = gather (u,edges) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

633 
in (u,adj) :: assemble el edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

634 
end 
32768  635 
 assemble [] _ = [] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

636 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

637 
(* Compute, for each adjacency list, the list with reversed edges, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

638 
and concatenate these lists. *) 
32768  639 
val flipped = maps flip g 
32215  640 

641 
in assemble g flipped end 

642 

14445  643 
(* *********************************************************************** *) 
32215  644 
(* *) 
14445  645 
(* scc_term : (term * term list) list > term list list *) 
646 
(* *) 

647 
(* The following is based on the algorithm for finding strongly connected *) 

648 
(* components described in Introduction to Algorithms, by Cormon, Leiserson*) 

649 
(* and Rivest, section 23.5. The input G is an adjacency list description *) 

650 
(* of a directed graph. The output is a list of the strongly connected *) 

32215  651 
(* components (each a list of vertices). *) 
652 
(* *) 

14445  653 
(* *) 
654 
(* *********************************************************************** *) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

655 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

656 
fun scc_term G = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

657 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

658 
(* Ordered list of the vertices that DFS has finished with; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

659 
most recently finished goes at the head. *) 
32740  660 
val finish : term list Unsynchronized.ref = Unsynchronized.ref [] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

661 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

662 
(* List of vertices which have been visited. *) 
32740  663 
val visited : term list Unsynchronized.ref = Unsynchronized.ref [] 
32215  664 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

665 
fun been_visited v = exists (fn w => w aconv v) (!visited) 
32215  666 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

667 
(* Given the adjacency list rep of a graph (a list of pairs), 
32215  668 
return just the first element of each pair, yielding the 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

669 
vertex list. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

670 
val members = map (fn (v,_) => v) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

671 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

672 
(* Returns the nodes in the DFS tree rooted at u in g *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

673 
fun dfs_visit g u : term list = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

674 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

675 
val _ = visited := u :: !visited 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

676 
val descendents = 
30190  677 
List.foldr (fn ((v,l),ds) => if been_visited v then ds 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

678 
else v :: dfs_visit g v @ ds) 
32768  679 
[] (adjacent (op aconv) g u) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

680 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

681 
finish := u :: !finish; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

682 
descendents 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

683 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

684 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

685 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

686 
(* DFS on the graph; apply dfs_visit to each vertex in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

687 
the graph, checking first to make sure the vertex is 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

688 
as yet unvisited. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

689 
app (fn u => if been_visited u then () 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

690 
else (dfs_visit G u; ())) (members G); 
32768  691 
visited := []; 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

692 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

693 
(* We don't reset finish because its value is used by 
14445  694 
foldl below, and it will never be used again (even 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

695 
though dfs_visit will continue to modify it). *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

696 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

697 
(* DFS on the transpose. The vertices returned by 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

698 
dfs_visit along with u form a connected component. We 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

699 
collect all the connected components together in a 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

700 
list, which is what is returned. *) 
33245  701 
fold (fn u => fn comps => 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

702 
if been_visited u then comps 
33245  703 
else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!finish) [] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

704 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

705 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

706 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

707 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

708 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

709 
(* dfs_int_reachable g u: *) 
32215  710 
(* (int * int list) list > int > int list *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

711 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

712 
(* Computes list of all nodes reachable from u in g. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

713 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

714 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

715 

32215  716 
fun dfs_int_reachable g u = 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

717 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

718 
(* List of vertices which have been visited. *) 
32740  719 
val visited : int list Unsynchronized.ref = Unsynchronized.ref [] 
32215  720 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

721 
fun been_visited v = exists (fn w => w = v) (!visited) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

722 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

723 
fun dfs_visit g u : int list = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

724 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

725 
val _ = visited := u :: !visited 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

726 
val descendents = 
30190  727 
List.foldr (fn ((v,l),ds) => if been_visited v then ds 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

728 
else v :: dfs_visit g v @ ds) 
32768  729 
[] (adjacent (op =) g u) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

730 
in descendents end 
32215  731 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

732 
in u :: dfs_visit g u end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

733 

32215  734 

735 
fun indexNodes IndexComp = 

32952  736 
maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp; 
32215  737 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

738 
fun getIndex v [] = ~1 
32215  739 
 getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; 
740 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

741 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

742 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

743 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

744 
(* *) 
14445  745 
(* dfs eq_comp g u v: *) 
746 
(* ('a * 'a > bool) > ('a *( 'a * less) list) list > *) 

32215  747 
(* 'a > 'a > (bool * ('a * less) list) *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

748 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

749 
(* Depth first search of v from u. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

750 
(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

751 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

752 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

753 

32215  754 
fun dfs eq_comp g u v = 
755 
let 

32740  756 
val pred = Unsynchronized.ref []; 
757 
val visited = Unsynchronized.ref []; 

32215  758 

14445  759 
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) 
32215  760 

761 
fun dfs_visit u' = 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

762 
let val _ = visited := u' :: (!visited) 
32215  763 

14445  764 
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; 
32215  765 

766 
in if been_visited v then () 

14445  767 
else (app (fn (v',l) => if been_visited v' then () else ( 
32215  768 
update (v',l); 
14445  769 
dfs_visit v'; ()) )) (adjacent eq_comp g u') 
770 
end 

32215  771 
in 
772 
dfs_visit u; 

773 
if (been_visited v) then (true, (!pred)) else (false , []) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

774 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

775 

32215  776 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

777 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

778 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

779 
(* completeTermPath u v g: *) 
32215  780 
(* Term.term > Term.term > (Term.term * (Term.term * less) list) list *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

781 
(* > less list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

782 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

783 
(* Complete the path from u to v in graph g. Path search is performed *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

784 
(* with dfs_term g u v. This yields for each node v' its predecessor u' *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

785 
(* and the edge u' > v'. Allows traversing graph backwards from v and *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

786 
(* finding the path u > v. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

787 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

788 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

789 

32215  790 

791 
fun completeTermPath u v g = 

792 
let 

14445  793 
val (found, tmp) = dfs (op aconv) g u v ; 
794 
val pred = map snd tmp; 

32215  795 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

796 
fun path x y = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

797 
let 
32215  798 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

799 
(* find predecessor u of node v and the edge u > v *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

800 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

801 
fun lookup v [] = raise Cannot 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

802 
 lookup v (e::es) = if (upper e) aconv v then e else lookup v es; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

803 

32215  804 
(* traverse path backwards and return list of visited edges *) 
805 
fun rev_path v = 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

806 
let val l = lookup v pred 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

807 
val u = lower l; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

808 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

809 
if u aconv x then [l] 
32215  810 
else (rev_path u) @ [l] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

811 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

812 
in rev_path y end; 
32215  813 

814 
in 

24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

815 
if found then (if u aconv v then [(Le (u, v, (Thm ([], #le_refl less_thms))))] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

816 
else path u v ) else raise Cannot 
32215  817 
end; 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

818 

32215  819 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

820 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

821 
(* *) 
14445  822 
(* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal: *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

823 
(* *) 
14445  824 
(* (int * (int * less) list) list * less list * (Term.term * int) list *) 
825 
(* * ((term * (term * less) list) list) list > Less > proof *) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

826 
(* *) 
14445  827 
(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a *) 
828 
(* proof for subgoal. Raises exception Cannot if this is not possible. *) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

829 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

830 
(* *********************************************************************** *) 
32215  831 

14445  832 
fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal = 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

833 
let 
32215  834 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

835 
(* complete path x y from component graph *) 
32215  836 
fun completeComponentPath x y predlist = 
837 
let 

838 
val xi = getIndex x ntc 

839 
val yi = getIndex y ntc 

840 

841 
fun lookup k [] = raise Cannot 

842 
 lookup k ((h: int,l)::us) = if k = h then l else lookup k us; 

843 

844 
fun rev_completeComponentPath y' = 

845 
let val edge = lookup (getIndex y' ntc) predlist 

846 
val u = lower edge 

847 
val v = upper edge 

848 
in 

849 
if (getIndex u ntc) = xi then 

850 
(completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge] 

851 
@(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) 

852 
else (rev_completeComponentPath u)@[edge] 

853 
@(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

854 
end 
32215  855 
in 
856 
if x aconv y then 

24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

857 
[(Le (x, y, (Thm ([], #le_refl less_thms))))] 
15570  858 
else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi)) 
32215  859 
else rev_completeComponentPath y ) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

860 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

861 

32215  862 
(* ******************************************************************* *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

863 
(* findLess e x y xi yi xreachable yreachable *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

864 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

865 
(* Find a path from x through e to y, of weight < *) 
32215  866 
(* ******************************************************************* *) 
867 

868 
fun findLess e x y xi yi xreachable yreachable = 

869 
let val u = lower e 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

870 
val v = upper e 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

871 
val ui = getIndex u ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

872 
val vi = getIndex v ntc 
32215  873 

874 
in 

36692
54b64d4ad524
farewell to oldstyle 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

875 
if member (op =) xreachable ui andalso member (op =) xreachable vi andalso 
54b64d4ad524
farewell to oldstyle 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

876 
member (op =) yreachable ui andalso member (op =) yreachable vi then ( 
32215  877 

878 
(case e of (Less (_, _, _)) => 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

879 
let 
14445  880 
val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) 
32215  881 
in 
882 
if xufound then ( 

883 
let 

884 
val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi 

885 
in 

886 
if vyfound then ( 

887 
let 

888 
val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred) 

889 
val xyLesss = transPath (tl xypath, hd xypath) 

890 
in 

891 
if xyLesss subsumes subgoal then SOME (getprf xyLesss) 

15531  892 
else NONE 
32215  893 
end) 
894 
else NONE 

895 
end) 

896 
else NONE 

897 
end 

898 
 _ => 

899 
let val (uvfound, uvpred) = dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) 

900 
in 

901 
if uvfound then ( 

902 
let 

903 
val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) 

904 
in 

905 
if xufound then ( 

906 
let 

907 
val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi 

908 
in 

909 
if vyfound then ( 

910 
let 

911 
val uvpath = completeComponentPath u v uvpred 

912 
val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e) 

913 
val xypath = (completeComponentPath x u xupred)@[uvLesss]@(completeComponentPath v y vypred) 

914 
val xyLesss = transPath (tl xypath, hd xypath) 

915 
in 

916 
if xyLesss subsumes subgoal then SOME (getprf xyLesss) 

15531  917 
else NONE 
32215  918 
end ) 
919 
else NONE 

920 
end) 

921 
else NONE 

922 
end ) 

923 
else NONE 

924 
end ) 

15531  925 
) else NONE 
32215  926 
end; 
927 

928 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

929 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

930 
(* looking for x <= y: any path from x to y is sufficient *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

931 
case subgoal of (Le (x, y, _)) => ( 
32215  932 
if null sccGraph then raise Cannot else ( 
933 
let 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

934 
val xi = getIndex x ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

935 
val yi = getIndex y ntc 
14445  936 
(* searches in sccGraph a path from xi to yi *) 
937 
val (found, pred) = dfs (op =) sccGraph xi yi 

32215  938 
in 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

939 
if found then ( 
32215  940 
let val xypath = completeComponentPath x y pred 
941 
val xyLesss = transPath (tl xypath, hd xypath) 

942 
in 

943 
(case xyLesss of 

944 
(Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms)) 

945 
else raise Cannot 

946 
 _ => if xyLesss subsumes subgoal then (getprf xyLesss) 

947 
else raise Cannot) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

948 
end ) 
32215  949 
else raise Cannot 
950 
end 

14445  951 
) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

952 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

953 
(* looking for x < y: particular path required, which is not necessarily 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

954 
found by normal dfs *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

955 
 (Less (x, y, _)) => ( 
19617  956 
if null sccGraph then raise Cannot else ( 
32215  957 
let 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

958 
val xi = getIndex x ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

959 
val yi = getIndex y ntc 
14445  960 
val sccGraph_transpose = transpose (op =) sccGraph 
961 
(* all components that can be reached from component xi *) 

962 
val xreachable = dfs_int_reachable sccGraph xi 

963 
(* all comonents reachable from y in the transposed graph sccGraph' *) 

964 
val yreachable = dfs_int_reachable sccGraph_transpose yi 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

965 
(* for all edges u ~= v or u < v check if they are part of path x < y *) 
32215  966 
fun processNeqEdges [] = raise Cannot 
967 
 processNeqEdges (e::es) = 

968 
case (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

969 
 _ => processNeqEdges es 
32215  970 

971 
in 

972 
processNeqEdges neqE 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

973 
end 
14445  974 
) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

975 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

976 
 (NotEq (x, y, _)) => ( 
14445  977 
(* if there aren't any edges that are candidate for a ~= raise Cannot *) 
19617  978 
if null neqE then raise Cannot 
14445  979 
(* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *) 
19617  980 
else if null sccSubgraphs then ( 
14445  981 
(case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of 
15531  982 
( SOME (NotEq (x, y, p)), NotEq (x', y', _)) => 
32215  983 
if (x aconv x' andalso y aconv y') then p 
984 
else Thm ([p], #not_sym less_thms) 

985 
 ( SOME (Less (x, y, p)), NotEq (x', y', _)) => 

24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

986 
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

987 
else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms)) 
32215  988 
 _ => raise Cannot) 
14445  989 
) else ( 
32215  990 

991 
let val xi = getIndex x ntc 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

992 
val yi = getIndex y ntc 
32215  993 
val sccGraph_transpose = transpose (op =) sccGraph 
14445  994 
val xreachable = dfs_int_reachable sccGraph xi 
32215  995 
val yreachable = dfs_int_reachable sccGraph_transpose yi 
996 

997 
fun processNeqEdges [] = raise Cannot 

998 
 processNeqEdges (e::es) = ( 

999 
let val u = lower e 

1000 
val v = upper e 

1001 
val ui = getIndex u ntc 

1002 
val vi = getIndex v ntc 

1003 

1004 
in 

1005 
(* if x ~= y follows from edge e *) 

1006 
if e subsumes subgoal then ( 

1007 
case e of (Less (u, v, q)) => ( 

1008 
if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms)) 

1009 
else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms)) 

1010 
) 

1011 
 (NotEq (u,v, q)) => ( 

1012 
if u aconv x andalso v aconv y then q 

1013 
else (Thm ([q], #not_sym less_thms)) 

1014 
) 

1015 
) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1016 
(* if SCC_x is linked to SCC_y via edge e *) 
32215  1017 
else if ui = xi andalso vi = yi then ( 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1018 
case e of (Less (_, _,_)) => ( 
32215  1019 
let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) ) 
1020 
val xyLesss = transPath (tl xypath, hd xypath) 

1021 
in (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end) 

1022 
 _ => ( 

1023 
let 

1024 
val xupath = completeTermPath x u (List.nth(sccSubgraphs, ui)) 

1025 
val uxpath = completeTermPath u x (List.nth(sccSubgraphs, ui)) 

1026 
val vypath = completeTermPath v y (List.nth(sccSubgraphs, vi)) 

1027 
val yvpath = completeTermPath y v (List.nth(sccSubgraphs, vi)) 

1028 
val xuLesss = transPath (tl xupath, hd xupath) 

1029 
val uxLesss = transPath (tl uxpath, hd uxpath) 

1030 
val vyLesss = transPath (tl vypath, hd vypath) 

1031 
val yvLesss = transPath (tl yvpath, hd yvpath) 

1032 
val x_eq_u = (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms)) 

1033 
val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms)) 

1034 
in 

1035 
(Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms)) 

1036 
end 

1037 
) 

1038 
) else if ui = yi andalso vi = xi then ( 

1039 
case e of (Less (_, _,_)) => ( 

1040 
let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) ) 

1041 
val xyLesss = transPath (tl xypath, hd xypath) 

1042 
in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end ) 

1043 
 _ => ( 

1044 

1045 
let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui)) 

1046 
val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui)) 

1047 
val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi)) 

1048 
val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi)) 

1049 
val yuLesss = transPath (tl yupath, hd yupath) 

1050 
val uyLesss = transPath (tl uypath, hd uypath) 

1051 
val vxLesss = transPath (tl vxpath, hd vxpath) 

1052 
val xvLesss = transPath (tl xvpath, hd xvpath) 

1053 
val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms)) 

1054 
val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms)) 

1055 
in 

1056 
(Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms)) 

1057 
end 

1058 
) 

1059 
) else ( 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1060 
(* there exists a path x < y or y < x such that 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1061 
x ~= y may be concluded *) 
32215  1062 
case (findLess e x y xi yi xreachable yreachable) of 
1063 
(SOME prf) => (Thm ([prf], #less_imp_neq less_thms)) 

15531  1064 
 NONE => ( 
32215  1065 
let 
1066 
val yr = dfs_int_reachable sccGraph yi 

1067 
val xr = dfs_int_reachable sccGraph_transpose xi 

1068 
in 

1069 
case (findLess e y x yi xi yr xr) of 

1070 
(SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms)) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1071 
 _ => processNeqEdges es 
32215  1072 
end) 
1073 
) end) 

14445  1074 
in processNeqEdges neqE end) 
32215  1075 
) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1076 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1077 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1078 

14445  1079 
(* ******************************************************************* *) 
1080 
(* *) 

1081 
(* mk_sccGraphs components leqG neqG ntc : *) 

1082 
(* Term.term list list > *) 

1083 
(* (Term.term * (Term.term * less) list) list > *) 

1084 
(* (Term.term * (Term.term * less) list) list > *) 

1085 
(* (Term.term * int) list > *) 

1086 
(* (int * (int * less) list) list * *) 

1087 
(* ((Term.term * (Term.term * less) list) list) list *) 

1088 
(* *) 

1089 
(* *) 

1090 
(* Computes, from graph leqG, list of all its components and the list *) 

1091 
(* ntc (nodes, index of component) a graph whose nodes are the *) 

1092 
(* indices of the components of g. Egdes of the new graph are *) 

1093 
(* only the edges of g linking two components. Also computes for each *) 

1094 
(* component the subgraph of leqG that forms this component. *) 

1095 
(* *) 

1096 
(* For each component SCC_i is checked if there exists a edge in neqG *) 

1097 
(* that leads to a contradiction. *) 

1098 
(* *) 

1099 
(* We have a contradiction for edge u ~= v and u < v if: *) 

1100 
(*  u and v are in the same component, *) 

1101 
(* that is, a path u <= v and a path v <= u exist, hence u = v. *) 

1102 
(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *) 

1103 
(* *) 

1104 
(* ******************************************************************* *) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1105 

14445  1106 
fun mk_sccGraphs _ [] _ _ = ([],[]) 
32215  1107 
 mk_sccGraphs components leqG neqG ntc = 
14445  1108 
let 
1109 
(* Liste (Index der Komponente, Komponente *) 

33063  1110 
val IndexComp = map_index I components; 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1111 

32215  1112 

1113 
fun handleContr edge g = 

1114 
(case edge of 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1115 
(Less (x, y, _)) => ( 
32215  1116 
let 
1117 
val xxpath = edge :: (completeTermPath y x g ) 

1118 
val xxLesss = transPath (tl xxpath, hd xxpath) 

1119 
val q = getprf xxLesss 

1120 
in 

1121 
raise (Contr (Thm ([q], #less_reflE less_thms ))) 

1122 
end 

1123 
) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1124 
 (NotEq (x, y, _)) => ( 
32215  1125 
let 
1126 
val xypath = (completeTermPath x y g ) 

1127 
val yxpath = (completeTermPath y x g ) 

1128 
val xyLesss = transPath (tl xypath, hd xypath) 

1129 
val yxLesss = transPath (tl yxpath, hd yxpath) 

1130 
val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) 

1131 
in 

1132 
raise (Contr (Thm ([q], #less_reflE less_thms ))) 

1133 
end 

1134 
) 

1135 
 _ => error "trans_tac/handleContr: invalid Contradiction"); 

1136 

1137 

1138 
(* k is index of the actual component *) 

1139 

1140 
fun processComponent (k, comp) = 

1141 
let 

1142 
(* all edges with weight <= of the actual component *) 

32952  1143 
val leqEdges = maps (adjacent (op aconv) leqG) comp; 
32215  1144 
(* all edges with weight ~= of the actual component *) 
32952  1145 
val neqEdges = map snd (maps (adjacent (op aconv) neqG) comp); 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1146 

32215  1147 
(* find an edge leading to a contradiction *) 
15531  1148 
fun findContr [] = NONE 
32215  1149 
 findContr (e::es) = 
1150 
let val ui = (getIndex (lower e) ntc) 

1151 
val vi = (getIndex (upper e) ntc) 

1152 
in 

1153 
if ui = vi then SOME e 

1154 
else findContr es 

1155 
end; 

1156 

1157 
(* sort edges into component internal edges and 

1158 
edges pointing away from the component *) 

1159 
fun sortEdges [] (intern,extern) = (intern,extern) 

1160 
 sortEdges ((v,l)::es) (intern, extern) = 

1161 
let val k' = getIndex v ntc in 

1162 
if k' = k then 

1163 
sortEdges es (l::intern, extern) 

1164 
else sortEdges es (intern, (k',l)::extern) end; 

1165 

1166 
(* Insert edge into sorted list of edges, where edge is 

14445  1167 
only added if 
1168 
 it is found for the first time 

1169 
 it is a <= edge and no parallel < edge was found earlier 

1170 
 it is a < edge 

1171 
*) 

32215  1172 
fun insert (h: int,l) [] = [(h,l)] 
1173 
 insert (h,l) ((k',l')::es) = if h = k' then ( 

1174 
case l of (Less (_, _, _)) => (h,l)::es 

1175 
 _ => (case l' of (Less (_, _, _)) => (h,l')::es 

1176 
 _ => (k',l)::es) ) 

1177 
else (k',l'):: insert (h,l) es; 

1178 

1179 
(* Reorganise list of edges such that 

14445  1180 
 duplicate edges are removed 
1181 
 if a < edge and a <= edge exist at the same time, 

1182 
remove <= edge *) 

32215  1183 
fun reOrganizeEdges [] sorted = sorted: (int * less) list 
1184 
 reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted); 

1185 

14445  1186 
(* construct the subgraph forming the strongly connected component 
32215  1187 
from the edge list *) 
1188 
fun sccSubGraph [] g = g 

1189 
 sccSubGraph (l::ls) g = 

1190 
sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g)) 

1191 

1192 
val (intern, extern) = sortEdges leqEdges ([], []); 

14445  1193 
val subGraph = sccSubGraph intern []; 
32215  1194 

1195 
in 

15531  1196 
case findContr neqEdges of SOME e => handleContr e subGraph 
32215  1197 
 _ => ((k, (reOrganizeEdges (extern) [])), subGraph) 
1198 
end; 

1199 

1200 
val tmp = map processComponent IndexComp 

1201 
in 

1202 
( (map fst tmp), (map snd tmp)) 

1203 
end; 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1204 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1205 

24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1206 
(** Find proof if possible. **) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1207 

24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1208 
fun gen_solve mkconcl sign (asms, concl) = 
32215  1209 
let 
14445  1210 
val (leqG, neqG, neqE) = mkGraphs asms 
32215  1211 
val components = scc_term leqG 
33063  1212 
val ntc = indexNodes (map_index I components) 
14445  1213 
val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1214 
in 
32215  1215 
let 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1216 
val (subgoals, prf) = mkconcl decomp less_thms sign concl 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1217 
fun solve facts less = 
15531  1218 
(case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less 
1219 
 SOME prf => prf ) 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1220 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1221 
map (solve asms) subgoals 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1222 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1223 
end; 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1224 

9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1225 
in 
32215  1226 
SUBGOAL (fn (A, n) => fn st => 
1227 
let 

1228 
val thy = ProofContext.theory_of ctxt; 

1229 
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); 

1230 
val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) 

1231 
val C = subst_bounds (rfrees, Logic.strip_assums_concl A) 

33206  1232 
val lesss = flat (map_index (mkasm decomp less_thms thy) Hs) 
32215  1233 
val prfs = gen_solve mkconcl thy (lesss, C); 
1234 
val (subgoals, prf) = mkconcl decomp less_thms thy C; 

1235 
in 

32283  1236 
Subgoal.FOCUS (fn {prems = asms, ...} => 
32215  1237 
let val thms = map (prove (prems @ asms)) prfs 
1238 
in rtac (prove thms prf) 1 end) ctxt n st 

1239 
end 

1240 
handle Contr p => 

32283  1241 
(Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st 
32215  1242 
handle Subscript => Seq.empty) 
1243 
 Cannot => Seq.empty 

1244 
 Subscript => Seq.empty) 

24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1245 
end; 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1246 

14445  1247 
(* partial_tac  solves partial orders *) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1248 
val partial_tac = gen_order_tac mkasm_partial mkconcl_partial; 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1249 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1250 
(* linear_tac  solves linear/total orders *) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1251 
val linear_tac = gen_order_tac mkasm_linear mkconcl_linear; 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1252 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1253 
end; 