author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 43278  1fbdcebb364b 
child 58839  ccda99401bc8 
permissions  rwrr 
37744  1 
(* Title: Provers/order.ML 
2 
Author: Oliver Kutter, TU Muenchen 

29276  3 

4 
Transitivity reasoner for partial and linear orders. 

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

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

6 

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

8 

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

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

10 

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

11 
The package provides tactics partial_tac and linear_tac that use all 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

13 

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

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

15 

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

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

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

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

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

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

21 

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

22 
The package is not limited to the relation <= and friends. It can be 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

23 
instantiated to any partial and/or linear order  for example, the 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

25 
a partial order only, supply dummy theorems to the rules for linear 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

26 
orders, and don't use linear_tac! 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

27 

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

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

29 

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

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

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

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

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

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

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

36 

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

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

38 
val partial_tac: 
32215  39 
(theory > term > (term * string * term) option) > less_arith > 
40 
Proof.context > thm list > int > tactic 

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

41 
val linear_tac: 
32215  42 
(theory > term > (term * string * term) option) > less_arith > 
43 
Proof.context > thm list > int > tactic 

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

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

45 

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

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

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

48 

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

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

50 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

67 

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

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

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

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

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

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

73 

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

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

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

76 
eq_neq_eq_imp_neq : thm (* [ x = u ; u ~= v ; v = z] ==> x ~= z *) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

78 

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

79 
fun empty dummy_thm = 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

80 
{less_reflE= dummy_thm, le_refl= dummy_thm, less_imp_le= dummy_thm, eqI= dummy_thm, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

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

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

85 
not_lessD= dummy_thm, not_leD= dummy_thm, not_lessI= dummy_thm, not_leI= dummy_thm, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

86 
less_imp_neq = dummy_thm, eq_neq_eq_imp_neq = dummy_thm} 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

87 

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

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

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

90 
val {less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

91 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

92 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

95 
less_le_trans', le_less_trans', le_trans', le_neq_trans', neq_le_trans', 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

96 
not_sym', not_lessD', not_leD', not_lessI', not_leI', less_imp_neq', 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

99 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

100 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

103 
less_imp_le = less_imp_le', eqI = eqI', eqD1 = eqD1', eqD2 = eqD2', 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

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

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

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

109 
less_imp_neq = less_imp_neq', eq_neq_eq_imp_neq = eq_neq_eq_imp_neq'} 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

111 

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

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

113 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

114 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

115 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

118 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

119 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

121 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

122 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

123 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

126 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

127 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

129 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

130 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

131 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

134 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

135 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

137 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

138 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

139 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

142 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

143 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

145 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

146 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

147 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

150 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

151 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

153 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

154 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

155 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

158 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

159 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

161 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

162 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

163 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

166 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

167 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

169 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

170 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

171 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

174 
thm, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

175 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

177 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

178 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

179 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

182 
less_le_trans, thm, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

183 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

185 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

186 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

187 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

190 
less_le_trans, le_less_trans, thm, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

191 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

193 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

194 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

195 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

198 
less_le_trans, le_less_trans, le_trans, thm, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

199 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

201 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

202 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

203 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

206 
less_le_trans, le_less_trans, le_trans, le_neq_trans, thm, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

207 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

209 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

210 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

211 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

214 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

215 
thm, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

217 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

218 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

219 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

222 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

223 
not_sym, thm, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

225 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

226 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

227 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

230 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

231 
not_sym, not_lessD, thm, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

233 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

234 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

235 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

238 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

239 
not_sym, not_lessD, not_leD, thm, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

241 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

242 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

243 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

246 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

247 
not_sym, not_lessD, not_leD, not_lessI, thm, less_imp_neq, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

249 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

250 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

251 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

254 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

255 
not_sym, not_lessD, not_leD, not_lessI, not_leI, thm, eq_neq_eq_imp_neq)) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

257 
change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

258 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

259 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

262 
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

263 
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, thm)); 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

264 

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

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

266 
datatype proof 
32215  267 
= Asm of int 
268 
 Thm of proof list * thm; 

269 

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

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

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

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

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

275 

32215  276 
fun prove asms = 
42364  277 
let 
278 
fun pr (Asm i) = nth asms i 

279 
 pr (Thm (prfs, thm)) = map pr prfs MRS thm; 

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

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

281 

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

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

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

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

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

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

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

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

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

292 

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

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

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

295 
 upper (NotEq (_,y,_)) = y; 
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 getprf (Less (_, _, p)) = p 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

300 

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

301 

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

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

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

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

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

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

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

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

311 

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

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

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

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

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

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

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

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

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

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

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

329 

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

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

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

332 
(* mkasm_linear *) 
14398
c5c47703f763
Efficient, 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 
(* 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

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

336 
(* Linear orders only. *) 
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 
(* ************************************************************************ *) 
32215  339 

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

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

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

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

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

349 
else [Less (y, x, Thm ([Asm n], #not_leD less_thms))] 

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

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

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

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

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

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

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

359 

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

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

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

362 
(* mkconcl_partial *) 
14398
c5c47703f763
Efficient, 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 
(* Translates conclusion t to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

368 

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

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

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

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

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

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

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

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

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

379 

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

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

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

382 
(* mkconcl_linear *) 
14398
c5c47703f763
Efficient, 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 
(* Translates conclusion t to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

388 

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

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

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

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

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

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

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

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

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

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

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

401 

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

402 

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

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

404 

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

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

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

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

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

409 

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

411 

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

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

413 

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

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

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

416 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

433 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

460 

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

461 

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

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

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

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

465 

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

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

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

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

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

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

471 
 _ tr _ = false; 
32215  472 

473 

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

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

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

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

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

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

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

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

484 

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

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

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

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

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

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

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

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

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

496 
(* ******************************************************************* *) 
32215  497 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

512 

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

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

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

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

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

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

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

520 

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

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

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

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

525 

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

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

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

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

529 

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

530 

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

531 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

554 

32215  555 

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

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

559 

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

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

32215  563 

14398
c5c47703f763
Efficient, 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 
(* *) 
32215  566 
(* mkGraphs constructs from a list of objects of type less a graph g, *) 
14445  567 
(* by taking all edges that are candidate for a <=, and a list neqE, by *) 
568 
(* taking all edges that are candiate for a ~= *) 

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

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

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

571 

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

575 

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

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

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

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

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

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

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

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

587 

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

588 

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

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

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

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

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

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

595 
(* *********************************************************************** *) 
32215  596 

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

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

601 

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

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

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

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

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

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

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

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

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

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

611 

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

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

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

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

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

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

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

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

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

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

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

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

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

629 

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

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

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

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

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

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

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

637 

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

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

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

642 
in assemble g flipped end 

643 

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

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

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

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

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

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

14445  654 
(* *) 
655 
(* *********************************************************************** *) 

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

656 

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

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

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

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

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

662 

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

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

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

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

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

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

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

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

672 

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

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

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

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

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

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

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

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

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

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

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

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

686 

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

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

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

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

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

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

693 

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

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

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

697 

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

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

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

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

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

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

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

706 

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

707 

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

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

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

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

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

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

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

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

716 

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

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

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

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

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

723 

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

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

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

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

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

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

731 
in descendents end 
32215  732 

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

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

734 

32215  735 

736 
fun indexNodes IndexComp = 

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

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

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

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

742 

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

743 

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

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

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

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

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

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

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

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

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

754 

32215  755 
fun dfs eq_comp g u v = 
756 
let 

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

32215  759 

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

762 
fun dfs_visit u' = 

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

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

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

767 
in if been_visited v then () 

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

32215  772 
in 
773 
dfs_visit u; 

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

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

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

776 

32215  777 

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

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

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

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

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

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

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

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

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

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

790 

32215  791 

792 
fun completeTermPath u v g = 

793 
let 

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

32215  796 

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

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

798 
let 
32215  799 

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

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

801 

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

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

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

804 

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

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

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

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

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

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

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

813 
in rev_path y end; 
32215  814 

815 
in 

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

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

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

819 

32215  820 

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

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

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

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

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

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

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

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

831 
(* *********************************************************************** *) 
32215  832 

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

834 
let 
32215  835 

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

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

839 
val xi = getIndex x ntc 

840 
val yi = getIndex y ntc 

841 

842 
fun lookup k [] = raise Cannot 

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

844 

845 
fun rev_completeComponentPath y' = 

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

847 
val u = lower edge 

848 
val v = upper edge 

849 
in 

850 
if (getIndex u ntc) = xi then 

42364  851 
completeTermPath x u (nth sccSubgraphs xi) @ [edge] @ 
852 
completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc)) 

853 
else 

854 
rev_completeComponentPath u @ [edge] @ 

855 
completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc)) 

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

856 
end 
32215  857 
in 
42364  858 
if x aconv y then 
859 
[(Le (x, y, (Thm ([], #le_refl less_thms))))] 

860 
else if xi = yi then completeTermPath x y (nth sccSubgraphs xi) 

861 
else rev_completeComponentPath y 

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

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

863 

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

865 
(* findLess e x y xi yi xreachable yreachable *) 
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 
(* Find a path from x through e to y, of weight < *) 
32215  868 
(* ******************************************************************* *) 
869 

870 
fun findLess e x y xi yi xreachable yreachable = 

871 
let val u = lower e 

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

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

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

874 
val vi = getIndex v ntc 
32215  875 

876 
in 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
33245
diff
changeset

877 
if member (op =) xreachable ui andalso member (op =) xreachable vi andalso 
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
33245
diff
changeset

878 
member (op =) yreachable ui andalso member (op =) yreachable vi then ( 
32215  879 

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

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

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

885 
let 

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

887 
in 

888 
if vyfound then ( 

889 
let 

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

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

892 
in 

893 
if xyLesss subsumes subgoal then SOME (getprf xyLesss) 

15531  894 
else NONE 
32215  895 
end) 
896 
else NONE 

897 
end) 

898 
else NONE 

899 
end 

900 
 _ => 

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

902 
in 

903 
if uvfound then ( 

904 
let 

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

906 
in 

907 
if xufound then ( 

908 
let 

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

910 
in 

911 
if vyfound then ( 

912 
let 

913 
val uvpath = completeComponentPath u v uvpred 

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

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

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

917 
in 

918 
if xyLesss subsumes subgoal then SOME (getprf xyLesss) 

15531  919 
else NONE 
32215  920 
end ) 
921 
else NONE 

922 
end) 

923 
else NONE 

924 
end ) 

925 
else NONE 

926 
end ) 

15531  927 
) else NONE 
32215  928 
end; 
929 

930 

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

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

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

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

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

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

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

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

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

944 
in 

945 
(case xyLesss of 

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

947 
else raise Cannot 

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

949 
else raise Cannot) 

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

950 
end ) 
32215  951 
else raise Cannot 
952 
end 

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

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

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

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

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

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

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

964 
val xreachable = dfs_int_reachable sccGraph xi 

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

966 
val yreachable = dfs_int_reachable sccGraph_transpose yi 

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

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

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

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

971 
 _ => processNeqEdges es 
32215  972 

973 
in 

974 
processNeqEdges neqE 

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

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

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

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

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

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

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

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

993 
let val xi = getIndex x ntc 

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

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

999 
fun processNeqEdges [] = raise Cannot 

1000 
 processNeqEdges (e::es) = ( 

1001 
let val u = lower e 

1002 
val v = upper e 

1003 
val ui = getIndex u ntc 

1004 
val vi = getIndex v ntc 

1005 

1006 
in 

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

1008 
if e subsumes subgoal then ( 

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

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

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

1012 
) 

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

1014 
if u aconv x andalso v aconv y then q 

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

1016 
) 

1017 
) 

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

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

1020 
case e of (Less (_, _,_)) => ( 
42364  1021 
let 
1022 
val xypath = 

1023 
completeTermPath x u (nth sccSubgraphs ui) @ [e] @ 

1024 
completeTermPath v y (nth sccSubgraphs vi) 

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

32215  1026 
in (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end) 
1027 
 _ => ( 

1028 
let 

42364  1029 
val xupath = completeTermPath x u (nth sccSubgraphs ui) 
1030 
val uxpath = completeTermPath u x (nth sccSubgraphs ui) 

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

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

32215  1033 
val xuLesss = transPath (tl xupath, hd xupath) 
1034 
val uxLesss = transPath (tl uxpath, hd uxpath) 

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

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

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

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

1039 
in 

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

1041 
end 

1042 
) 

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

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

42364  1045 
let 
1046 
val xypath = 

1047 
completeTermPath y u (nth sccSubgraphs ui) @ [e] @ 

1048 
completeTermPath v x (nth sccSubgraphs vi) 

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

32215  1050 
in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end ) 
1051 
 _ => ( 

1052 

42364  1053 
let val yupath = completeTermPath y u (nth sccSubgraphs ui) 
1054 
val uypath = completeTermPath u y (nth sccSubgraphs ui) 

1055 
val vxpath = completeTermPath v x (nth sccSubgraphs vi) 

1056 
val xvpath = completeTermPath x v (nth sccSubgraphs vi) 

32215  1057 
val yuLesss = transPath (tl yupath, hd yupath) 
1058 
val uyLesss = transPath (tl uypath, hd uypath) 

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

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

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

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

1063 
in 

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

1065 
end 

1066 
) 

1067 
) else ( 

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

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

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

15531  1072 
 NONE => ( 
32215  1073 
let 
1074 
val yr = dfs_int_reachable sccGraph yi 

1075 
val xr = dfs_int_reachable sccGraph_transpose xi 

1076 
in 

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

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

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

1079 
 _ => processNeqEdges es 
32215  1080 
end) 
1081 
) end) 

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

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

1085 

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

1086 

14445  1087 
(* ******************************************************************* *) 
1088 
(* *) 

1089 
(* mk_sccGraphs components leqG neqG ntc : *) 

1090 
(* Term.term list list > *) 

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

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

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

1094 
(* (int * (int * less) list) list * *) 

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

1096 
(* *) 

1097 
(* *) 

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

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

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

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

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

1103 
(* *) 

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

1105 
(* that leads to a contradiction. *) 

1106 
(* *) 

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

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

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

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

1111 
(* *) 

1112 
(* ******************************************************************* *) 

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

1113 

14445  1114 
fun mk_sccGraphs _ [] _ _ = ([],[]) 
32215  1115 
 mk_sccGraphs components leqG neqG ntc = 
14445  1116 
let 
1117 
(* Liste (Index der Komponente, Komponente *) 

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

1119 

32215  1120 

1121 
fun handleContr edge g = 

1122 
(case edge of 

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

1123 
(Less (x, y, _)) => ( 
32215  1124 
let 
1125 
val xxpath = edge :: (completeTermPath y x g ) 

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

1127 
val q = getprf xxLesss 

1128 
in 

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

1130 
end 

1131 
) 

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

1132 
 (NotEq (x, y, _)) => ( 
32215  1133 
let 
1134 
val xypath = (completeTermPath x y g ) 

1135 
val yxpath = (completeTermPath y x g ) 

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

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

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

1139 
in 

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

1141 
end 

1142 
) 

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

1144 

1145 

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

1147 

1148 
fun processComponent (k, comp) = 

1149 
let 

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

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

1154 

32215  1155 
(* find an edge leading to a contradiction *) 
15531  1156 
fun findContr [] = NONE 
32215  1157 
 findContr (e::es) = 
1158 
let val ui = (getIndex (lower e) ntc) 

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

1160 
in 

1161 
if ui = vi then SOME e 

1162 
else findContr es 

1163 
end; 

1164 

1165 
(* sort edges into component internal edges and 

1166 
edges pointing away from the component *) 

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

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

1169 
let val k' = getIndex v ntc in 

1170 
if k' = k then 

1171 
sortEdges es (l::intern, extern) 

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

1173 

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

14445  1175 
only added if 
1176 
 it is found for the first time 

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

1178 
 it is a < edge 

1179 
*) 

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

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

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

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

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

1186 

1187 
(* Reorganise list of edges such that 

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

1190 
remove <= edge *) 

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

1193 

14445  1194 
(* construct the subgraph forming the strongly connected component 
32215  1195 
from the edge list *) 
1196 
fun sccSubGraph [] g = g 

1197 
 sccSubGraph (l::ls) g = 

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

1199 

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

14445  1201 
val subGraph = sccSubGraph intern []; 
32215  1202 

1203 
in 

15531  1204 
case findContr neqEdges of SOME e => handleContr e subGraph 
32215  1205 
 _ => ((k, (reOrganizeEdges (extern) [])), subGraph) 
1206 
end; 

1207 

1208 
val tmp = map processComponent IndexComp 

1209 
in 

1210 
( (map fst tmp), (map snd tmp)) 

1211 
end; 

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

1212 

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

1213 

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

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

1215 

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

1216 
fun gen_solve mkconcl sign (asms, concl) = 
32215  1217 
let 
14445  1218 
val (leqG, neqG, neqE) = mkGraphs asms 
32215  1219 
val components = scc_term leqG 
33063  1220 
val ntc = indexNodes (map_index I components) 
14445  1221 
val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

1225 
fun solve facts less = 
15531  1226 
(case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less 
1227 
 SOME prf => prf ) 

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

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

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

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

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

1232 

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

1233 
in 
32215  1234 
SUBGOAL (fn (A, n) => fn st => 
1235 
let 

42361  1236 
val thy = Proof_Context.theory_of ctxt; 
32215  1237 
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); 
1238 
val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) 

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

33206  1240 
val lesss = flat (map_index (mkasm decomp less_thms thy) Hs) 
32215  1241 
val prfs = gen_solve mkconcl thy (lesss, C); 
1242 
val (subgoals, prf) = mkconcl decomp less_thms thy C; 

1243 
in 

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

1247 
end 

1248 
handle Contr p => 

32283  1249 
(Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st 
43278  1250 
handle General.Subscript => Seq.empty) 
32215  1251 
 Cannot => Seq.empty 
43278  1252 
 General.Subscript => Seq.empty) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

1254 

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

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

1257 

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

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

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

1260 

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

1261 
end; 