author  wenzelm 
Sun, 30 Nov 2008 14:43:29 +0100  
changeset 28917  20f43e0e0958 
parent 26834  87a5b9ec3863 
child 29276  94b1ffec9201 
permissions  rwrr 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

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

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

7 

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

9 

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

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

11 

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

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

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

14 

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

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

16 

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

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

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

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

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

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

22 

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

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

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

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

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

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

28 

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

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

30 

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

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

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

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

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

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

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

37 

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

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

39 
val partial_tac: 
24704
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24639
diff
changeset

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

41 
val linear_tac: 
24704
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24639
diff
changeset

42 
(theory > term > (term * string * term) option) > less_arith > 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 

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

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

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

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

269 

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

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

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

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

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

274 

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

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

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

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

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

280 

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

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

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

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

285 

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

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

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

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

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

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

291 

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

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

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

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

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

296 

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

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

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

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

300 

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

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

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

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

304 

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

305 

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

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

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

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

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

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

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

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

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

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

315 

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

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

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

319 
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

333 

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

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

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

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

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

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

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

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

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

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

343 

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

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

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

347 
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

352 
raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms))) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

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

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

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

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

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

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

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

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

363 

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

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

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

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

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

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

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

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

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

372 

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

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

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

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

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

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

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

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

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

383 

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

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

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

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

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

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

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

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

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

392 

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

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

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

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

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

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

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

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

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

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

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

405 

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

406 

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

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

408 

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

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

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

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

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

413 

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

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

415 

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

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

417 

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

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

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

420 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

437 

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

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

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

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

441 
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

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

443 
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

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

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

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

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

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

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

450 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

464 

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

465 

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

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

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

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

469 

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

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

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

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

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

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

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

476 

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

477 

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

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

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

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

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

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

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

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

487 
(* ******************************************************************* *) 
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 
fun transPath ([],lesss) = lesss 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

492 
else error "linear/partial_tac: internal error transpath"; 
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 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

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

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

501 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

515 
 _ subsumes _ = false; 
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 
(* *) 
15531  519 
(* triv_solv less1 : less > proof option *) 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

526 
if x aconv x' then SOME (Thm ([], #le_refl less_thms)) 
15531  527 
else NONE 
528 
 triv_solv _ = NONE; 

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

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

533 

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

534 

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

535 

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

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

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

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

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

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

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

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

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

545 
(* assumption. *) 
14445  546 
(*  Used to compute strongly connected components *) 
547 
(*  Used to compute component subgraphs *) 

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

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

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

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

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

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

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

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

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

558 

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

559 

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

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

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

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

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

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 
(* mkGraphs constructs from a list of objects of type less a graph g, *) 
571 
(* by taking all edges that are candidate for a <=, and a list neqE, by *) 

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

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

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

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

575 

14445  576 
fun mkGraphs [] = ([],[],[]) 
577 
 mkGraphs lessList = 

578 
let 

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

579 

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

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

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

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

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

585 
 (Le (x,y,p)) => 
14445  586 
buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) 
587 
 (NotEq (x,y,p)) => 

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

589 

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

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

591 

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

592 

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

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

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

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

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

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

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

600 

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

603 
 adjacent _ [] _ = [] 

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

604 

14445  605 

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

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

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

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

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

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

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

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

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

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

615 

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

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

618 
(* Compute list of reversed edges for each adjacency list *) 
14445  619 
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

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

621 

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

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

623 
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

624 
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

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

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

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

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

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

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

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

633 

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

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

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

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

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

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

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

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

641 

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

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

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

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

645 

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

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

647 

14445  648 
(* *********************************************************************** *) 
649 
(* *) 

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

651 
(* *) 

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

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

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

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

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

657 
(* *) 

658 
(* *) 

659 
(* *********************************************************************** *) 

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

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

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

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

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

666 

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

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

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

669 

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

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

671 

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

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

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

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

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

676 

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

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

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

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

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

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

682 
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

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

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

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

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

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

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

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

690 

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

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

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

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

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

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

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

697 

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

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

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

701 

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

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

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

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

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

707 
if been_visited u then comps 
14445  708 
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

709 
end; 
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 

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

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

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

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

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

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

720 

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

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

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

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

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

725 

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

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

727 

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

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

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

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

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

732 
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

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

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

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

736 

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

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

738 

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

739 

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

740 
fun indexComps components = 
14445  741 
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

742 

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

743 
fun indexNodes IndexComp = 
15570  744 
List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp); 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

745 

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

746 
fun getIndex v [] = ~1 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

748 

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

749 

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

750 

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

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

752 
(* *) 
14445  753 
(* dfs eq_comp g u v: *) 
754 
(* ('a * 'a > bool) > ('a *( 'a * less) list) list > *) 

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

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

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

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

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

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

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

761 

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

763 
let 
14445  764 
val pred = ref nil; 
765 
val visited = ref nil; 

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

766 

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

768 

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

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

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

771 

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

773 

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

774 
in if been_visited v then () 
14445  775 
else (app (fn (v',l) => if been_visited v' then () else ( 
776 
update (v',l); 

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

778 
end 

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

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

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

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

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

783 

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

784 

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

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

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

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

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

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

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

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

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

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

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

797 

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

798 

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

800 
let 
14445  801 
val (found, tmp) = dfs (op aconv) g u v ; 
802 
val pred = map snd tmp; 

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

803 

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

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

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

806 

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

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

808 

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

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

810 
 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

811 

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

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

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

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

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

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

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

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

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

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

821 

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

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

823 
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

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

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

826 

14445  827 

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

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

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

831 
(* *) 
14445  832 
(* (int * (int * less) list) list * less list * (Term.term * int) list *) 
833 
(* * ((term * (term * less) list) list) list > Less > proof *) 

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

834 
(* *) 
14445  835 
(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a *) 
836 
(* 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

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

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

839 

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

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

842 

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

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

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

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

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

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

848 

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

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

851 

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

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

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

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

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

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

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

14445  860 
else (rev_completeComponentPath u)@[edge] 
15570  861 
@(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) 
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 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

869 

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

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

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

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

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

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

875 

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

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

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

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

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

881 

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

882 
in 
14445  883 
if ui mem xreachable andalso vi mem xreachable andalso 
884 
ui mem yreachable andalso vi mem yreachable then ( 

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

885 

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

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

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

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

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

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

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

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

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

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

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

898 
in 
15531  899 
if xyLesss subsumes subgoal then SOME (getprf xyLesss) 
900 
else NONE 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

923 
in 
15531  924 
if xyLesss subsumes subgoal then SOME (getprf xyLesss) 
925 
else NONE 

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

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

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

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

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

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

935 

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

936 

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

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

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

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

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

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

943 
val yi = getIndex y ntc 
14445  944 
(* searches in sccGraph a path from xi to yi *) 
945 
val (found, pred) = dfs (op =) sccGraph xi yi 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

967 
val yi = getIndex y ntc 
14445  968 
val sccGraph_transpose = transpose (op =) sccGraph 
969 
(* all components that can be reached from component xi *) 

970 
val xreachable = dfs_int_reachable sccGraph xi 

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

972 
val yreachable = dfs_int_reachable sccGraph_transpose yi 

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

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

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

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

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

978 

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

979 
in 
14445  980 
processNeqEdges neqE 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

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

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

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

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

994 
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

995 
else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms)) 
14445  996 
 _ => raise Cannot) 
997 
) else ( 

998 

999 
let val xi = getIndex x ntc 

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

1000 
val yi = getIndex y ntc 
14445  1001 
val sccGraph_transpose = transpose (op =) sccGraph 
1002 
val xreachable = dfs_int_reachable sccGraph xi 

1003 
val yreachable = dfs_int_reachable sccGraph_transpose yi 

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

1004 

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

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

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

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

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

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

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

1011 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1030 
 _ => ( 
14445  1031 
let 
15570  1032 
val xupath = completeTermPath x u (List.nth(sccSubgraphs, ui)) 
1033 
val uxpath = completeTermPath u x (List.nth(sccSubgraphs, ui)) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1052 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1073 
let 
14445  1074 
val yr = dfs_int_reachable sccGraph yi 
1075 
val xr = dfs_int_reachable sccGraph_transpose xi 

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

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

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

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

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

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

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

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

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

1085 

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

1086 

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

1089 
(* mk_sccGraphs components leqG neqG ntc : *) 

1090 
(* Term.term list list > *) 

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

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

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

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

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

1096 
(* *) 

1097 
(* *) 

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

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

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

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

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

1103 
(* *) 

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

1105 
(* that leads to a contradiction. *) 

1106 
(* *) 

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

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

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

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

1111 
(* *) 

1112 
(* ******************************************************************* *) 

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

1113 

14445  1114 
fun mk_sccGraphs _ [] _ _ = ([],[]) 
1115 
 mk_sccGraphs components leqG neqG ntc = 

1116 
let 

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

1118 
val IndexComp = indexComps components; 

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

1119 

14445  1120 

1121 
fun handleContr edge g = 

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

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

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

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

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

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

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

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

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

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

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

1133 
let 
14445  1134 
val xypath = (completeTermPath x y g ) 
1135 
val yxpath = (completeTermPath y x g ) 

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

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

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

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

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

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

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

1142 
) 
14445  1143 
 _ => error "trans_tac/handleContr: invalid Contradiction"); 
1144 

1145 

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

1147 

1148 
fun processComponent (k, comp) = 

1149 
let 

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

15570  1151 
val leqEdges = List.concat (map (adjacent (op aconv) leqG) comp); 
14445  1152 
(* all edges with weight ~= of the actual component *) 
15570  1153 
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

1154 

14445  1155 
(* find an edge leading to a contradiction *) 
15531  1156 
fun findContr [] = NONE 
14445  1157 
 findContr (e::es) = 
1158 
let val ui = (getIndex (lower e) ntc) 

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

1160 
in 

15531  1161 
if ui = vi then SOME e 
14445  1162 
else findContr es 
1163 
end; 

1164 

1165 
(* sort edges into component internal edges and 

1166 
edges pointing away from the component *) 

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

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

1169 
let val k' = getIndex v ntc in 

1170 
if k' = k then 

1171 
sortEdges es (l::intern, extern) 

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

1173 

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

1175 
only added if 

1176 
 it is found for the first time 

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

1178 
 it is a < edge 

1179 
*) 

23577  1180 
fun insert (h: int,l) [] = [(h,l)] 
14445  1181 
 insert (h,l) ((k',l')::es) = if h = k' then ( 
1182 
case l of (Less (_, _, _)) => (h,l)::es 

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

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

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

1186 

1187 
(* Reorganise list of edges such that 

1188 
 duplicate edges are removed 

1189 
 if a < edge and a <= edge exist at the same time, 

1190 
remove <= edge *) 

1191 
fun reOrganizeEdges [] sorted = sorted: (int * less) list 

1192 
 reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted); 

1193 

1194 
(* construct the subgraph forming the strongly connected component 

1195 
from the edge list *) 

1196 
fun sccSubGraph [] g = g 

1197 
 sccSubGraph (l::ls) g = 

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

1199 

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

1201 
val subGraph = sccSubGraph intern []; 

1202 

1203 
in 

15531  1204 
case findContr neqEdges of SOME e => handleContr e subGraph 
14445  1205 
 _ => ((k, (reOrganizeEdges (extern) [])), subGraph) 
1206 
end; 

1207 

1208 
val tmp = map processComponent IndexComp 

1209 
in 

1210 
( (map fst tmp), (map snd tmp)) 

1211 
end; 

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

1212 

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

1213 

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

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

1215 

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

1216 
fun gen_solve mkconcl sign (asms, concl) = 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1217 
let 
14445  1218 
val (leqG, neqG, neqE) = mkGraphs asms 
1219 
val components = scc_term leqG 

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

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

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

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

1225 
fun solve facts less = 
15531  1226 
(case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less 
1227 
 SOME prf => prf ) 

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

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

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

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

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

1232 

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

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

1234 

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

1235 
SUBGOAL (fn (A, n, sign) => 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

1237 
val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) 
24704
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24639
diff
changeset

1238 
val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1239 
val C = subst_bounds (rfrees, Logic.strip_assums_concl A) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1240 
val lesss = List.concat (ListPair.map (mkasm decomp less_thms sign) (Hs, 0 upto (length Hs  1))) 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1241 
val prfs = gen_solve mkconcl sign (lesss, C); 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1242 
val (subgoals, prf) = mkconcl decomp less_thms sign C; 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

1244 
METAHYPS (fn asms => 
24704
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24639
diff
changeset

1245 
let val thms = map (prove (prems @ asms)) prfs 
24639
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1246 
in rtac (prove thms prf) 1 end) n 
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 
handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

1249 
 Cannot => no_tac 
9b73bc9b05a1
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
ballarin
parents:
23577
diff
changeset

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

1251 

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

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

1253 

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

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

1256 

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

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

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

1259 

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

1260 

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

1261 
end; 