author  wenzelm 
Sun, 26 Jul 2009 22:28:31 +0200  
changeset 32215  87806301a813 
parent 30190  479806475f3c 
child 32283  3bebc195c124 
permissions  rwrr 
29276  1 
(* Author: Oliver Kutter, TU Muenchen 
2 

3 
Transitivity reasoner for partial and linear orders. 

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

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

5 

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

7 

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 

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

10 
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

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

12 

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

13 
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

14 

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

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

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

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

18 
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

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

20 

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

21 
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

22 
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

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

24 
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

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

26 

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 

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

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

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

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

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

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

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

35 

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

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

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

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

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

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

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

44 

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

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

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

47 

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

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

49 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

66 

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

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

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

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

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

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

72 

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

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

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

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

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

77 

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

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

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

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

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

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

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

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

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

86 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

110 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

263 

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

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

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

268 

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

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

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

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

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

274 

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

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

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

279 

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

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

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

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

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

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

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

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

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

290 

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

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

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

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

294 

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

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

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

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

298 

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

299 

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

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

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

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

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

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

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

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

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

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

309 

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

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

311 
case decomp sign t of 
15531  312 
SOME (x, rel, y) => (case rel of 
32215  313 
"<" => 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

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

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

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

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

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

321 
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

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

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

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

327 

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

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

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

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

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

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

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

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

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

336 
(* ************************************************************************ *) 
32215  337 

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

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

339 
case decomp sign t of 
15531  340 
SOME (x, rel, y) => (case rel of 
32215  341 
"<" => 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

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

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

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

347 
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

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

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

351 
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

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

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

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

357 

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

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

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

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

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

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

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

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

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

366 

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

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

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

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

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

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

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

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

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

377 

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

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

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

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

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

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

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

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

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

386 

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

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

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

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

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

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

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

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

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

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

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

399 

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

400 

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

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

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

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

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

407 

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

409 

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

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

411 

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

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

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

414 

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

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

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

417 
(* mergeLess *) 
14398
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 
(* 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

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

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

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

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

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

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

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

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

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

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

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

431 

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

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

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

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

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

437 
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

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

440 
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

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

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

444 
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

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

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

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

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

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

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

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

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

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

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

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

458 

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

459 

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

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

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

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

463 

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

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

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

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

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

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

469 
 _ tr _ = false; 
32215  470 

471 

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

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

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

474 
(* transPath (Lesslist, Less): (less list * less) > less *) 
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 
(* 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

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

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

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

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

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

482 

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

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

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

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

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

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

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

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

490 
(* less1 subsumes less2 : less > less > bool *) 
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 
(* subsumes checks whether less1 implies less2 *) 
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 
(* ******************************************************************* *) 
32215  495 

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

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

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

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

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

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

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

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

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

510 

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

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

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

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

515 
(* Solves trivial goal x <= x. *) 
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 
(* ******************************************************************* *) 
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 
fun triv_solv (Le (x, x', _)) = 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

523 

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

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

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

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

527 

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

528 

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 
(* General: *) 
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 
(* Inequalities are represented by various types of graphs. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

552 

32215  553 

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

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

555 
(* Functions for constructing graphs *) 
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 

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

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

32215  561 

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

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

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

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

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

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

569 

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

573 

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

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

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

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

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

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

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

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

585 

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

586 

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

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

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

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

591 
(* List of successors of u in graph g *) 
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 
(* *********************************************************************** *) 
32215  594 

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

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

599 

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

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

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

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

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

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

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

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

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

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

609 

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

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

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

614 
 flip (_,nil) = nil 
32215  615 

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

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

617 
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

618 
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

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

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

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

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

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

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

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

627 

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

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

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

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

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

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

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

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

635 

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

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

637 
and concatenate these lists. *) 
30190  638 
val flipped = List.foldr (op @) nil (map flip g) 
32215  639 

640 
in assemble g flipped end 

641 

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

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

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

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

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

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

14445  652 
(* *) 
653 
(* *********************************************************************** *) 

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

654 

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

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

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

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

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

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

660 

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

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

662 
val visited : term list ref = ref nil 
32215  663 

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

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

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

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

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

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

670 

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

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

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

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

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

675 
val descendents = 
30190  676 
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

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

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

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

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

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

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

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

684 

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

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

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

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

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

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

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

691 

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

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

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

695 

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

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

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

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

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

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

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

704 

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

705 

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

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

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

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

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

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

714 

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

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

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

718 
val visited : int list ref = ref nil 
32215  719 

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

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

721 

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

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

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

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

725 
val descendents = 
30190  726 
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

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

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

729 
in descendents end 
32215  730 

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

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

732 

32215  733 

734 
fun indexComps components = 

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

736 

32215  737 
fun indexNodes IndexComp = 
15570  738 
List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp); 
32215  739 

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

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

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

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

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

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

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

752 
(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) 
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 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

755 

32215  756 
fun dfs eq_comp g u v = 
757 
let 

14445  758 
val pred = ref nil; 
759 
val visited = ref nil; 

32215  760 

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

763 
fun dfs_visit u' = 

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

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

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

768 
in if been_visited v then () 

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

32215  773 
in 
774 
dfs_visit u; 

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

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

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

777 

32215  778 

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

781 
(* completeTermPath u v g: *) 
32215  782 
(* 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

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

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

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

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

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

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

791 

32215  792 

793 
fun completeTermPath u v g = 

794 
let 

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

32215  797 

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

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

799 
let 
32215  800 

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

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

802 

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

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

804 
 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

805 

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

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

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

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

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

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

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

814 
in rev_path y end; 
32215  815 

816 
in 

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

817 
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

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

820 

32215  821 

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

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

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

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

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

828 
(* *) 
14445  829 
(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a *) 
830 
(* 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

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

832 
(* *********************************************************************** *) 
32215  833 

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

835 
let 
32215  836 

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

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

840 
val xi = getIndex x ntc 

841 
val yi = getIndex y ntc 

842 

843 
fun lookup k [] = raise Cannot 

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

845 

846 
fun rev_completeComponentPath y' = 

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

848 
val u = lower edge 

849 
val v = upper edge 

850 
in 

851 
if (getIndex u ntc) = xi then 

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

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

854 
else (rev_completeComponentPath u)@[edge] 

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

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

856 
end 
32215  857 
in 
858 
if x aconv y then 

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

859 
[(Le (x, y, (Thm ([], #le_refl less_thms))))] 
15570  860 
else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi)) 
32215  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 

877 
if ui mem xreachable andalso vi mem xreachable andalso 

14445  878 
ui mem yreachable andalso vi mem yreachable 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 (_, _,_)) => ( 
32215  1021 
let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) ) 
1022 
val xyLesss = transPath (tl xypath, hd xypath) 

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

1024 
 _ => ( 

1025 
let 

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

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

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

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

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

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

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

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

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

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

1036 
in 

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

1038 
end 

1039 
) 

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

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

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

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

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

1045 
 _ => ( 

1046 

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

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

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

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

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

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

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

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

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

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

1057 
in 

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

1059 
end 

1060 
) 

1061 
) else ( 

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

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

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

15531  1066 
 NONE => ( 
32215  1067 
let 
1068 
val yr = dfs_int_reachable sccGraph yi 

1069 
val xr = dfs_int_reachable sccGraph_transpose xi 

1070 
in 

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

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

1073 
 _ => processNeqEdges es 
32215  1074 
end) 
1075 
) end) 

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

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

1079 

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

1080 

14445  1081 
(* ******************************************************************* *) 
1082 
(* *) 

1083 
(* mk_sccGraphs components leqG neqG ntc : *) 

1084 
(* Term.term list list > *) 

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

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

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

1088 
(* (int * (int * less) list) list * *) 

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

1090 
(* *) 

1091 
(* *) 

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

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

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

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

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

1097 
(* *) 

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

1099 
(* that leads to a contradiction. *) 

1100 
(* *) 

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

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

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

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

1105 
(* *) 

1106 
(* ******************************************************************* *) 

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

1107 

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

1112 
val IndexComp = indexComps components; 

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

1113 

32215  1114 

1115 
fun handleContr edge g = 

1116 
(case edge of 

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

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

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

1121 
val q = getprf xxLesss 

1122 
in 

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

1124 
end 

1125 
) 

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

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

1129 
val yxpath = (completeTermPath y x g ) 

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

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

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

1133 
in 

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

1135 
end 

1136 
) 

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

1138 

1139 

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

1141 

1142 
fun processComponent (k, comp) = 

1143 
let 

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

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

1148 

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

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

1154 
in 

1155 
if ui = vi then SOME e 

1156 
else findContr es 

1157 
end; 

1158 

1159 
(* sort edges into component internal edges and 

1160 
edges pointing away from the component *) 

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

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

1163 
let val k' = getIndex v ntc in 

1164 
if k' = k then 

1165 
sortEdges es (l::intern, extern) 

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

1167 

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

14445  1169 
only added if 
1170 
 it is found for the first time 

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

1172 
 it is a < edge 

1173 
*) 

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

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

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

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

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

1180 

1181 
(* Reorganise list of edges such that 

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

1184 
remove <= edge *) 

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

1187 

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

1191 
 sccSubGraph (l::ls) g = 

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

1193 

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

14445  1195 
val subGraph = sccSubGraph intern []; 
32215  1196 

1197 
in 

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

1201 

1202 
val tmp = map processComponent IndexComp 

1203 
in 

1204 
( (map fst tmp), (map snd tmp)) 

1205 
end; 

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

1206 

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

1207 

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

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

1209 

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

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

1214 
val ntc = indexNodes (indexComps components) 
14445  1215 
val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

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

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

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

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

1226 

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

1227 
in 
32215  1228 
SUBGOAL (fn (A, n) => fn st => 
1229 
let 

1230 
val thy = ProofContext.theory_of ctxt; 

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

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

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

1234 
val lesss = List.concat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs  1))) 

1235 
val prfs = gen_solve mkconcl thy (lesss, C); 

1236 
val (subgoals, prf) = mkconcl decomp less_thms thy C; 

1237 
in 

1238 
FOCUS (fn {prems = asms, ...} => 

1239 
let val thms = map (prove (prems @ asms)) prfs 

1240 
in rtac (prove thms prf) 1 end) ctxt n st 

1241 
end 

1242 
handle Contr p => 

1243 
(FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st 

1244 
handle Subscript => Seq.empty) 

1245 
 Cannot => Seq.empty 

1246 
 Subscript => Seq.empty) 

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

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

1248 

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

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

1251 

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

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

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

1254 

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

1255 
end; 