author  ballarin 
Tue, 18 Sep 2007 18:51:07 +0200  
changeset 24639  9b73bc9b05a1 
parent 23577  c5b93c69afd3 
child 24704  9a95634ab135 
permissions  rwrr 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

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

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

7 

14445  8 
(* TODO: reduce number of input thms *) 
14398
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 
(* 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

11 

15103
79846e8792eb
New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
15098
diff
changeset

12 
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

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

14 

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

15 
t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

16 

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

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

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

19 
in which case the conclusion can be any term, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

20 
2. or prove the conclusion, which must be of the same form as the 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

21 
premises (excluding ~(t < u) and ~(t <= u) for partial orders) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

22 

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

23 
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

24 
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

25 
divisibility relation "dvd". In order to instantiate the package for 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

26 
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

27 
orders, and don't use linear_tac! 
14398
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 
*) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

30 

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

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

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

33 
(* Theorems required by the reasoner *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

35 
val empty : thm > less_arith 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

36 
val update : string > thm > less_arith > less_arith 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

37 

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

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

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

40 
(theory > term > (term * string * term) option) > less_arith > int > tactic 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

42 
(theory > term > (term * string * term) option) > less_arith > int > tactic 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

44 

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

45 
structure Order_Tac: ORDER_TAC = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

47 

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

48 
(* Record to handle input theorems in a convenient way. *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

49 

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

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

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

52 
(* Theorems for partial orders *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

53 
less_reflE: thm, (* x < x ==> P *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

54 
le_refl: thm, (* x <= x *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

55 
less_imp_le: thm, (* x < y ==> x <= y *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

56 
eqI: thm, (* [ x <= y; y <= x ] ==> x = y *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

57 
eqD1: thm, (* x = y ==> x <= y *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

58 
eqD2: thm, (* x = y ==> y <= x *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

59 
less_trans: thm, (* [ x < y; y < z ] ==> x < z *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

60 
less_le_trans: thm, (* [ x < y; y <= z ] ==> x < z *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

61 
le_less_trans: thm, (* [ x <= y; y < z ] ==> x < z *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

62 
le_trans: thm, (* [ x <= y; y <= z ] ==> x <= z *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

63 
le_neq_trans : thm, (* [ x <= y ; x ~= y ] ==> x < y *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

64 
neq_le_trans : thm, (* [ x ~= y ; x <= y ] ==> x < y *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

65 
not_sym : thm, (* x ~= y ==> y ~= x *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

66 

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

67 
(* Additional theorems for linear orders *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

68 
not_lessD: thm, (* ~(x < y) ==> y <= x *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

69 
not_leD: thm, (* ~(x <= y) ==> y < x *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

70 
not_lessI: thm, (* y <= x ==> ~(x < y) *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

71 
not_leI: thm, (* y < x ==> ~(x <= y) *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

72 

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

73 
(* Additional theorems for subgoals of form x ~= y *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

74 
less_imp_neq : thm, (* x < y ==> x ~= y *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

75 
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

76 
} 
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 
fun empty dummy_thm = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

79 
{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

80 
eqD1= dummy_thm, eqD2= dummy_thm, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

81 
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

82 
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

83 
not_sym = dummy_thm, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

84 
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

85 
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

86 

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

87 
fun change thms f = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

89 
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

90 
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

91 
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

92 
eq_neq_eq_imp_neq} = thms; 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

93 
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

94 
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

95 
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

96 
eq_neq_eq_imp_neq') = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

97 
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

98 
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

99 
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

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

101 
in {less_reflE = less_reflE', le_refl= le_refl', 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

102 
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

103 
less_trans = less_trans', less_le_trans = less_le_trans', 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

104 
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

105 
neq_le_trans = neq_le_trans', not_sym = not_sym', 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

106 
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

107 
not_leI = not_leI', 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

108 
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

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

110 

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

111 
fun update "less_reflE" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

112 
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

113 
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

114 
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

115 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

116 
(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

117 
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

118 
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

119 
 update "le_refl" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

120 
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

121 
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

122 
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

123 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

124 
(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

125 
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

126 
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

127 
 update "less_imp_le" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

128 
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

129 
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

130 
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

131 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

132 
(less_reflE, le_refl, thm, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

133 
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

134 
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

135 
 update "eqI" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

136 
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

137 
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

138 
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

139 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

140 
(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

141 
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

142 
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

143 
 update "eqD1" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

144 
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

145 
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

146 
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

147 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

148 
(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

149 
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

150 
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

151 
 update "eqD2" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

152 
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

153 
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

154 
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

155 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

156 
(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

157 
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

158 
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

159 
 update "less_trans" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

160 
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

161 
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

162 
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

163 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

164 
(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

165 
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

166 
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

167 
 update "less_le_trans" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

168 
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

169 
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

170 
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

171 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

172 
(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

173 
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

174 
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

175 
 update "le_less_trans" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

176 
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

177 
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

178 
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

179 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

180 
(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

181 
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

182 
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

183 
 update "le_trans" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

184 
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

185 
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

186 
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

187 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

188 
(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

189 
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

190 
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

191 
 update "le_neq_trans" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

192 
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

193 
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

194 
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

195 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

196 
(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

197 
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

198 
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

199 
 update "neq_le_trans" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

200 
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

201 
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

202 
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

203 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

204 
(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

205 
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

206 
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

207 
 update "not_sym" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

208 
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

209 
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

210 
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

211 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

212 
(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

213 
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

214 
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

215 
 update "not_lessD" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

216 
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

217 
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

218 
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

219 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

220 
(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

221 
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

222 
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

223 
 update "not_leD" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

224 
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

225 
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

226 
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

227 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

228 
(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

229 
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

230 
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

231 
 update "not_lessI" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

232 
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

233 
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

234 
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

235 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

236 
(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

237 
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

238 
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

239 
 update "not_leI" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

240 
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

241 
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

242 
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

243 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

244 
(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

245 
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

246 
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

247 
 update "less_imp_neq" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

248 
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

249 
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

250 
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

251 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

252 
(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

253 
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

254 
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

255 
 update "eq_neq_eq_imp_neq" thm thms = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

256 
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

257 
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

258 
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

259 
eq_neq_eq_imp_neq) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

260 
(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

261 
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

262 
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

263 

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

264 

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

265 
(* Extract subgoal with signature *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

266 
fun SUBGOAL goalfun i st = 
22578  267 
goalfun (List.nth(prems_of st, i1), i, Thm.theory_of_thm st) st 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

268 
handle Subscript => Seq.empty; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

269 

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

270 
(* Internal datatype for the proof *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

272 
= Asm of int 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

273 
 Thm of proof list * thm; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

274 

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

275 
exception Cannot; 
14445  276 
(* Internal exception, raised if conclusion cannot be derived from 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

279 
(* Internal exception, raised if contradiction ( x < x ) was derived *) 
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 
fun prove asms = 
15570  282 
let fun pr (Asm i) = List.nth (asms, i) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

285 

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

286 
(* Internal datatype for inequalities *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

288 
= Less of term * term * proof 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

289 
 Le of term * term * proof 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

290 
 NotEq of term * term * proof; 
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 
(* Misc functions for datatype less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

296 

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

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

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

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

300 

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

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

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

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

304 

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

305 

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

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

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

308 
(* mkasm_partial *) 
14398
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 
(* 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

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

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

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

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

315 

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

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

317 
case decomp sign t of 
15531  318 
SOME (x, rel, y) => (case rel of 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

319 
"<" => 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

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

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

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

323 
 "~<=" => [] 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

325 
Le (y, x, Thm ([Asm n], #eqD2 less_thms))] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

326 
 "~=" => if (x aconv y) then 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

327 
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

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

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

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

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

333 

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

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

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

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

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

338 
(* 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

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

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

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

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

343 

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

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

345 
case decomp sign t of 
15531  346 
SOME (x, rel, y) => (case rel of 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

347 
"<" => 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

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

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

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

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 ([Asm n], #not_leD less_thms)], #less_reflE less_thms))) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

355 
Le (y, x, Thm ([Asm n], #eqD2 less_thms))] 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

356 
 "~=" => if (x aconv y) then 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

357 
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

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

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

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

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

363 

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

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

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

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

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

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

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

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

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

372 

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

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

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

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

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

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

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

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

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

383 

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

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

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

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

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

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

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

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

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

392 

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

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

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

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

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

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

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

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

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

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

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

405 

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

406 

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

407 
(*** The common part for partial and linear orders ***) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

408 

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

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

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

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

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

413 

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

414 
fun gen_order_tac mkasm mkconcl decomp (less_thms : less_arith) = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

415 

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

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

417 

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

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

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

422 
(* 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

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

427 
(* x <= y && y <= z ==> x <= z *) 
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 
(* x < y && x ~= y ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

431 
(* x ~= y && x < y ==> x < y *) 
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 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

434 

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

435 
fun mergeLess (Less (x, _, p) , Less (_ , 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_trans less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

438 
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

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

440 
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

441 
 mergeLess (Le (x, z, p) , NotEq (x', z', q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

442 
if (x aconv x' andalso z aconv z' ) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

443 
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

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

445 
 mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

446 
if (x aconv x' andalso z aconv z') 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

447 
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

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

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

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

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

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

453 
 mergeLess (Less (x, z, p) , NotEq (x', z', q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

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

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

460 
error "linear/partial_tac: internal error: undefined case"; 
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 

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 
(* tr checks for valid transitivity step *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

466 

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

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

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

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

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

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

472 
 _ tr _ = false; 
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 
(* ******************************************************************* *) 
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 
(* transPath (Lesslist, Less): (less list * less) > less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

479 
(* 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

480 
(* 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

481 
(* 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

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

485 

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

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

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

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

489 
else error "linear/partial_tac: internal error transpath"; 
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 
(* ******************************************************************* *) 
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 
(* less1 subsumes less2 : less > less > bool *) 
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 
(* subsumes checks whether less1 implies less2 *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

498 

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

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

500 
fun (Less (x, y, _)) subsumes (Le (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 
 (Less (x, y, _)) subsumes (Less (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 
 (Le (x, y, _)) subsumes (Le (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

506 
 (Less (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 
 (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

509 
(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

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

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

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

513 

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

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

515 
(* *) 
15531  516 
(* triv_solv less1 : less > proof option *) 
14398
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 
(* Solves trivial goal x <= x. *) 
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 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

521 

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

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

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

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

526 

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

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

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

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

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

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

542 
(* assumption. *) 
14445  543 
(*  Used to compute strongly connected components *) 
544 
(*  Used to compute component subgraphs *) 

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

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

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

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

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

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

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

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

554 
(* ******************************************************************* *) 
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 

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

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

560 

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

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

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

564 

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

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

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

569 
(* taking all edges that are candiate for a ~= *) 

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

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

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

572 

14445  573 
fun mkGraphs [] = ([],[],[]) 
574 
 mkGraphs lessList = 

575 
let 

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

576 

14445  577 
fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE) 
578 
 buildGraphs (l::ls, leqG,neqG, neqE) = case l of 

579 
(Less (x,y,p)) => 

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

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

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

582 
 (Le (x,y,p)) => 
14445  583 
buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) 
584 
 (NotEq (x,y,p)) => 

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

586 

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

14398
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 

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

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

591 
(* *) 
14445  592 
(* adjacent g u : (''a * 'b list ) list > ''a > 'b list *) 
14398
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 
(* List of successors of u in graph g *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

597 

14445  598 
fun adjacent eq_comp ((v,adj)::el) u = 
599 
if eq_comp (u, v) then adj else adjacent eq_comp el u 

600 
 adjacent _ [] _ = [] 

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

601 

14445  602 

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

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

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

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

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

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

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

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

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

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

612 

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

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

615 
(* Compute list of reversed edges for each adjacency list *) 
14445  616 
fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

618 

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

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

620 
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

621 
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

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

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

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

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

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

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

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

630 

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

631 
(* 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

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

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

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

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

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

637 
 assemble nil _ = nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

638 

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

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

640 
and concatenate these lists. *) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

641 
val flipped = foldr (op @) nil (map flip g) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

642 

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

643 
in assemble g flipped end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

644 

14445  645 
(* *********************************************************************** *) 
646 
(* *) 

647 
(* scc_term : (term * term list) list > term list list *) 

648 
(* *) 

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

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

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

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

653 
(* components (each a list of vertices). *) 

654 
(* *) 

655 
(* *) 

656 
(* *********************************************************************** *) 

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

657 

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

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

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

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

661 
most recently finished goes at the head. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

662 
val finish : term list ref = ref nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

663 

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

664 
(* List of vertices which have been visited. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

665 
val visited : term list ref = ref nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

666 

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

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

668 

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

669 
(* Given the adjacency list rep of a graph (a list of pairs), 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

670 
return just the first element of each pair, yielding the 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

673 

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

674 
(* 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

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

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

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

678 
val descendents = 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

679 
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

680 
else v :: dfs_visit g v @ ds) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

681 
nil (adjacent (op aconv) g u) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

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

687 

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

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

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

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

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

692 
else (dfs_visit G u; ())) (members G); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

693 
visited := nil; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

694 

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

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

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

698 

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

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

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

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

702 
list, which is what is returned. *) 
15570  703 
Library.foldl (fn (comps,u) => 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

704 
if been_visited u then comps 
14445  705 
else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps)) (nil,(!finish)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

712 
(* (int * int list) list > int > int list *) 
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 
(* Computes list of all nodes reachable from u in g. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

717 

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

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

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

720 
(* List of vertices which have been visited. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

721 
val visited : int list ref = ref nil 
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 been_visited v = exists (fn w => w = v) (!visited) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

724 

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

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

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

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

728 
val descendents = 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

729 
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

730 
else v :: dfs_visit g v @ ds) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

731 
nil (adjacent (op =) g u) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

733 

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

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

735 

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

736 

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

737 
fun indexComps components = 
14445  738 
ListPair.map (fn (a,b) => (a,b)) (0 upto (length components 1), components); 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

739 

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

740 
fun indexNodes IndexComp = 
15570  741 
List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp); 
14398
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 
fun getIndex v [] = ~1 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

744 
 getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

745 

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

746 

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

747 

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 
(* *) 
14445  750 
(* dfs eq_comp g u v: *) 
751 
(* ('a * 'a > bool) > ('a *( 'a * less) list) list > *) 

752 
(* 'a > 'a > (bool * ('a * less) list) *) 

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

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

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

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

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

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

758 

14445  759 
fun dfs eq_comp g u v = 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

760 
let 
14445  761 
val pred = ref nil; 
762 
val visited = ref nil; 

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

763 

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

765 

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

766 
fun dfs_visit u' = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

767 
let val _ = visited := u' :: (!visited) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

768 

14445  769 
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

770 

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

771 
in if been_visited v then () 
14445  772 
else (app (fn (v',l) => if been_visited v' then () else ( 
773 
update (v',l); 

774 
dfs_visit v'; ()) )) (adjacent eq_comp g u') 

775 
end 

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

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

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

778 
if (been_visited v) then (true, (!pred)) else (false , []) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

780 

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

781 

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

784 
(* completeTermPath u v g: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

786 
(* > less list *) 
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 
(* 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

789 
(* 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

790 
(* 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

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

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

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

794 

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

795 

14445  796 
fun completeTermPath u v g = 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

797 
let 
14445  798 
val (found, tmp) = dfs (op aconv) g u v ; 
799 
val pred = map snd tmp; 

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

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

803 

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

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

805 

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

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

807 
 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

808 

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

809 
(* traverse path backwards and return list of visited edges *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

810 
fun rev_path v = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

814 
if u aconv x then [l] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

815 
else (rev_path u) @ [l] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

817 
in rev_path y end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

818 

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

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

820 
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

821 
else path u v ) else raise Cannot 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

823 

14445  824 

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

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

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

828 
(* *) 
14445  829 
(* (int * (int * less) list) list * less list * (Term.term * int) list *) 
830 
(* * ((term * (term * less) list) list) list > Less > proof *) 

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

831 
(* *) 
14445  832 
(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a *) 
833 
(* 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

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

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

836 

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

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

839 

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

840 
(* complete path x y from component graph *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

844 
val yi = getIndex y ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

845 

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

846 
fun lookup k [] = raise Cannot 
23577  847 
 lookup k ((h: int,l)::us) = if k = h then l else lookup k us; 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

848 

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

849 
fun rev_completeComponentPath y' = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

850 
let val edge = lookup (getIndex y' ntc) predlist 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

854 
if (getIndex u ntc) = xi then 
15570  855 
(completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge] 
856 
@(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) 

14445  857 
else (rev_completeComponentPath u)@[edge] 
15570  858 
@(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

861 
if x aconv y then 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

864 
else rev_completeComponentPath y ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

866 

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

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

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

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

870 
(* Find a path from x through e to y, of weight < *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

872 

14445  873 
fun findLess e x y xi yi xreachable yreachable = 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

874 
let val u = lower e 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

877 
val vi = getIndex v ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

878 

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

879 
in 
14445  880 
if ui mem xreachable andalso vi mem xreachable andalso 
881 
ui mem yreachable andalso vi mem yreachable then ( 

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

882 

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

883 
(case e of (Less (_, _, _)) => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

884 
let 
14445  885 
val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

887 
if xufound then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

888 
let 
14445  889 
val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

891 
if vyfound then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

893 
val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

894 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

895 
in 
15531  896 
if xyLesss subsumes subgoal then SOME (getprf xyLesss) 
897 
else NONE 

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

898 
end) 
15531  899 
else NONE 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

900 
end) 
15531  901 
else NONE 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

903 
 _ => 
14445  904 
let val (uvfound, uvpred) = dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

905 
in 
14445  906 
if uvfound then ( 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

907 
let 
14445  908 
val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

909 
in 
14445  910 
if xufound then ( 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

911 
let 
14445  912 
val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

914 
if vyfound then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

916 
val uvpath = completeComponentPath u v uvpred 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

917 
val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

918 
val xypath = (completeComponentPath x u xupred)@[uvLesss]@(completeComponentPath v y vypred) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

919 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

920 
in 
15531  921 
if xyLesss subsumes subgoal then SOME (getprf xyLesss) 
922 
else NONE 

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

923 
end ) 
15531  924 
else NONE 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

925 
end) 
15531  926 
else NONE 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

927 
end ) 
15531  928 
else NONE 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

929 
end ) 
15531  930 
) else NONE 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

932 

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

933 

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

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

935 
(* 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

936 
case subgoal of (Le (x, y, _)) => ( 
19617  937 
if null sccGraph then raise Cannot else ( 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

940 
val yi = getIndex y ntc 
14445  941 
(* searches in sccGraph a path from xi to yi *) 
942 
val (found, pred) = dfs (op =) sccGraph xi yi 

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

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

944 
if found then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

945 
let val xypath = completeComponentPath x y pred 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

946 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

948 
(case xyLesss of 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

949 
(Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

951 
 _ => if xyLesss subsumes subgoal then (getprf xyLesss) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

964 
val yi = getIndex y ntc 
14445  965 
val sccGraph_transpose = transpose (op =) sccGraph 
966 
(* all components that can be reached from component xi *) 

967 
val xreachable = dfs_int_reachable sccGraph xi 

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

969 
val yreachable = dfs_int_reachable sccGraph_transpose yi 

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

970 
(* for all edges u ~= v or u < v check if they are part of path x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

972 
 processNeqEdges (e::es) = 
15531  973 
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

974 
 _ => processNeqEdges es 
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 
in 
14445  977 
processNeqEdges neqE 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

981 
 (NotEq (x, y, _)) => ( 
14445  982 
(* if there aren't any edges that are candidate for a ~= raise Cannot *) 
19617  983 
if null neqE then raise Cannot 
14445  984 
(* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *) 
19617  985 
else if null sccSubgraphs then ( 
14445  986 
(case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of 
15531  987 
( SOME (NotEq (x, y, p)), NotEq (x', y', _)) => 
14445  988 
if (x aconv x' andalso y aconv y') then p 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

989 
else Thm ([p], #not_sym less_thms) 
15531  990 
 ( SOME (Less (x, y, p)), NotEq (x', y', _)) => 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

991 
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

992 
else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms)) 
14445  993 
 _ => raise Cannot) 
994 
) else ( 

995 

996 
let val xi = getIndex x ntc 

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

997 
val yi = getIndex y ntc 
14445  998 
val sccGraph_transpose = transpose (op =) sccGraph 
999 
val xreachable = dfs_int_reachable sccGraph xi 

1000 
val yreachable = dfs_int_reachable sccGraph_transpose yi 

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

1001 

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

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

1003 
 processNeqEdges (e::es) = ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1004 
let val u = lower e 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

1007 
val vi = getIndex v ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1008 

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

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

1010 
(* if x ~= y follows from edge e *) 
14445  1011 
if e subsumes subgoal then ( 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1012 
case e of (Less (u, v, q)) => ( 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1013 
if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1014 
else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

1016 
 (NotEq (u,v, q)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1017 
if u aconv x andalso v aconv y then q 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1018 
else (Thm ([q], #not_sym less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

1021 
(* if SCC_x is linked to SCC_y via edge e *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1022 
else if ui = xi andalso vi = yi then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1023 
case e of (Less (_, _,_)) => ( 
15570  1024 
let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) ) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1025 
val xyLesss = transPath (tl xypath, hd xypath) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1026 
in (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1027 
 _ => ( 
14445  1028 
let 
15570  1029 
val xupath = completeTermPath x u (List.nth(sccSubgraphs, ui)) 
1030 
val uxpath = completeTermPath u x (List.nth(sccSubgraphs, ui)) 

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

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

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

1033 
val xuLesss = transPath (tl xupath, hd xupath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1034 
val uxLesss = transPath (tl uxpath, hd uxpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1035 
val vyLesss = transPath (tl vypath, hd vypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1036 
val yvLesss = transPath (tl yvpath, hd yvpath) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1037 
val x_eq_u = (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1038 
val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

1040 
(Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

1043 
) else if ui = yi andalso vi = xi then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1044 
case e of (Less (_, _,_)) => ( 
15570  1045 
let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) ) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1046 
val xyLesss = transPath (tl xypath, hd xypath) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1047 
in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end ) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1048 
 _ => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1049 

15570  1050 
let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui)) 
1051 
val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui)) 

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

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

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

1054 
val yuLesss = transPath (tl yupath, hd yupath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1055 
val uyLesss = transPath (tl uypath, hd uypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1056 
val vxLesss = transPath (tl vxpath, hd vxpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1057 
val xvLesss = transPath (tl xvpath, hd xvpath) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1058 
val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1059 
val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

1061 
(Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

1066 
x ~= y may be concluded *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1067 
case (findLess e x y xi yi xreachable yreachable) of 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1068 
(SOME prf) => (Thm ([prf], #less_imp_neq less_thms)) 
15531  1069 
 NONE => ( 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1070 
let 
14445  1071 
val yr = dfs_int_reachable sccGraph yi 
1072 
val xr = dfs_int_reachable sccGraph_transpose xi 

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

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

1074 
case (findLess e y x yi xi yr xr) of 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1075 
(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

1076 
 _ => processNeqEdges es 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

1082 

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

1083 

14445  1084 
(* ******************************************************************* *) 
1085 
(* *) 

1086 
(* mk_sccGraphs components leqG neqG ntc : *) 

1087 
(* Term.term list list > *) 

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

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

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

1091 
(* (int * (int * less) list) list * *) 

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

1093 
(* *) 

1094 
(* *) 

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

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

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

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

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

1100 
(* *) 

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

1102 
(* that leads to a contradiction. *) 

1103 
(* *) 

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

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

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

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

1108 
(* *) 

1109 
(* ******************************************************************* *) 

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

1110 

14445  1111 
fun mk_sccGraphs _ [] _ _ = ([],[]) 
1112 
 mk_sccGraphs components leqG neqG ntc = 

1113 
let 

1114 
(* Liste (Index der Komponente, Komponente *) 

1115 
val IndexComp = indexComps components; 

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

1116 

14445  1117 

1118 
fun handleContr edge g = 

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

1119 
(case edge of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

1121 
let 
14445  1122 
val xxpath = edge :: (completeTermPath y x g ) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1123 
val xxLesss = transPath (tl xxpath, hd xxpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1124 
val q = getprf xxLesss 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

1126 
raise (Contr (Thm ([q], #less_reflE less_thms ))) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

1130 
let 
14445  1131 
val xypath = (completeTermPath x y g ) 
1132 
val yxpath = (completeTermPath y x g ) 

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

1133 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1134 
val yxLesss = transPath (tl yxpath, hd yxpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1135 
val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

1137 
raise (Contr (Thm ([q], #less_reflE less_thms ))) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

1139 
) 
14445  1140 
 _ => error "trans_tac/handleContr: invalid Contradiction"); 
1141 

1142 

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

1144 

1145 
fun processComponent (k, comp) = 

1146 
let 

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

15570  1148 
val leqEdges = List.concat (map (adjacent (op aconv) leqG) comp); 
14445  1149 
(* all edges with weight ~= of the actual component *) 
15570  1150 
val neqEdges = map snd (List.concat (map (adjacent (op aconv) neqG) comp)); 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1151 

14445  1152 
(* find an edge leading to a contradiction *) 
15531  1153 
fun findContr [] = NONE 
14445  1154 
 findContr (e::es) = 
1155 
let val ui = (getIndex (lower e) ntc) 

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

1157 
in 

15531  1158 
if ui = vi then SOME e 
14445  1159 
else findContr es 
1160 
end; 

1161 

1162 
(* sort edges into component internal edges and 

1163 
edges pointing away from the component *) 

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

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

1166 
let val k' = getIndex v ntc in 

1167 
if k' = k then 

1168 
sortEdges es (l::intern, extern) 

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

1170 

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

1172 
only added if 

1173 
 it is found for the first time 

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

1175 
 it is a < edge 

1176 
*) 

23577  1177 
fun insert (h: int,l) [] = [(h,l)] 
14445  1178 
 insert (h,l) ((k',l')::es) = if h = k' then ( 
1179 
case l of (Less (_, _, _)) => (h,l)::es 

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

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

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

1183 

1184 
(* Reorganise list of edges such that 

1185 
 duplicate edges are removed 

1186 
 if a < edge and a <= edge exist at the same time, 

1187 
remove <= edge *) 

1188 
fun reOrganizeEdges [] sorted = sorted: (int * less) list 

1189 
 reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted); 

1190 

1191 
(* construct the subgraph forming the strongly connected component 

1192 
from the edge list *) 

1193 
fun sccSubGraph [] g = g 

1194 
 sccSubGraph (l::ls) g = 

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

1196 

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

1198 
val subGraph = sccSubGraph intern []; 

1199 

1200 
in 

15531  1201 
case findContr neqEdges of SOME e => handleContr e subGraph 
14445  1202 
 _ => ((k, (reOrganizeEdges (extern) [])), subGraph) 
1203 
end; 

1204 

1205 
val tmp = map processComponent IndexComp 

1206 
in 

1207 
( (map fst tmp), (map snd tmp)) 

1208 
end; 

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

1209 

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

1210 

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

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

1212 

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

1213 
fun gen_solve mkconcl sign (asms, concl) = 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1214 
let 
14445  1215 
val (leqG, neqG, neqE) = mkGraphs asms 
1216 
val components = scc_term leqG 

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

1217 
val ntc = indexNodes (indexComps components) 
14445  1218 
val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1219 
in 
14445  1220 
let 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

1222 
fun solve facts less = 
15531  1223 
(case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less 
1224 
 SOME prf => prf ) 

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

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

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

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

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

1229 

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

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

1231 

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

1232 
SUBGOAL (fn (A, n, sign) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

1234 
val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1235 
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1236 
val C = subst_bounds (rfrees, Logic.strip_assums_concl A) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1237 
val lesss = List.concat (ListPair.map (mkasm decomp less_thms sign) (Hs, 0 upto (length Hs  1))) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1238 
val prfs = gen_solve mkconcl sign (lesss, C); 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1239 
val (subgoals, prf) = mkconcl decomp less_thms sign C; 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

1241 
METAHYPS (fn asms => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1242 
let val thms = map (prove asms) prfs 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1243 
in rtac (prove thms prf) 1 end) n 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

1245 
handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1246 
 Cannot => no_tac 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

1248 

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

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

1250 

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

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

1253 

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

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

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

1256 

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

1257 

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

1258 
end; 