author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10126  1d428e891572 
child 11701  3d51fbf81c17 
permissions  rwrr 
7161  1 
(* Title: HOL/ex/svc_test.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson 

4 
Copyright 1999 University of Cambridge 

5 

6 
Demonstrating svc_tac: the interface to the Stanford Validity Checker 

7 

8 
SVC is assumed to be present if the environment variable SVC_HOME is nonempty. 

9 

10 
set Svc.trace; 

11 
*) 

12 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

13 
(** Propositional Logic **) 
7181  14 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

15 
(*Blast_tac's runtime for this type of problem appears to be exponential 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

16 
in its length, though Fast_tac manages*) 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

17 
Goal "P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P"; 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

18 
by (svc_tac 1); 
10126  19 
qed ""; 
7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

20 

55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

21 
(** Some big tautologies supplied by John Harrison **) 
7181  22 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

23 
(*Tautology name: puz013_1. Auto_tac manages; Blast_tac and Fast_tac take 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

24 
a minute or more.*) 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

25 
Goal "~(~v12 & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

26 
\ v0 & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

27 
\ v10 & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

28 
\ (v4  v5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

29 
\ (v9  v2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

30 
\ (v8  v1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

31 
\ (v7  v0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

32 
\ (v3  v12) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

33 
\ (v11  v10) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

34 
\ (~v12  ~v6  v7) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

35 
\ (~v10  ~v3  v1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

36 
\ (~v10  ~v0  ~v4  v11) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

37 
\ (~v5  ~v2  ~v8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

38 
\ (~v12  ~v9  ~v7) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

39 
\ (~v0  ~v1  v4) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

40 
\ (~v4  v7  v2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

41 
\ (~v12  ~v3  v8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

42 
\ (~v4  v5  v6) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

43 
\ (~v7  ~v8  v9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

44 
\ (~v10  ~v11  v12))"; 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

45 
by (svc_tac 1); 
10126  46 
qed ""; 
7161  47 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

48 
(*Tautology name: dk17_be*) 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

49 
Goal "(GE17 <> ~IN4 & ~IN3 & ~IN2 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

50 
\ (GE0 <> GE17 & ~IN5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

51 
\ (GE22 <> ~IN9 & ~IN7 & ~IN6 & IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

52 
\ (GE19 <> ~IN5 & ~IN4 & ~IN3 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

53 
\ (GE20 <> ~IN7 & ~IN6) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

54 
\ (GE18 <> ~IN6 & ~IN2 & ~IN1 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

55 
\ (GE21 <> IN9 & ~IN7 & IN6 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

56 
\ (GE23 <> GE22 & GE0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

57 
\ (GE25 <> ~IN9 & ~IN7 & IN6 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

58 
\ (GE26 <> IN9 & ~IN7 & ~IN6 & IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

59 
\ (GE2 <> GE20 & GE19) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

60 
\ (GE1 <> GE18 & ~IN7) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

61 
\ (GE24 <> GE23  GE21 & GE0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

62 
\ (GE5 <> ~IN5 & IN4  IN5 & ~IN4) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

63 
\ (GE6 <> GE0 & IN7 & ~IN6 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

64 
\ (GE12 <> GE26 & GE0  GE25 & GE0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

65 
\ (GE14 <> GE2 & IN8 & ~IN2 & IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

66 
\ (GE27 <> ~IN8 & IN5 & ~IN4 & ~IN3) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

67 
\ (GE9 <> GE1 & ~IN5 & ~IN4 & IN3) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

68 
\ (GE7 <> GE24  GE2 & IN2 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

69 
\ (GE10 <> GE6  GE5 & GE1 & ~IN3) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

70 
\ (GE15 <> ~IN8  IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

71 
\ (GE16 <> GE12  GE14 & ~IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

72 
\ (GE4 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

73 
\ GE5 & GE1 & IN8 & ~IN3  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

74 
\ GE0 & ~IN7 & IN6 & ~IN0  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

75 
\ GE2 & IN2 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

76 
\ (GE13 <> GE27 & GE1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

77 
\ (GE11 <> GE9  GE6 & ~IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

78 
\ (GE8 <> GE1 & ~IN5 & IN4 & ~IN3  GE2 & ~IN2 & IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

79 
\ (OUT0 <> GE7 & ~IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

80 
\ (OUT1 <> GE7 & IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

81 
\ (OUT2 <> GE8 & ~IN9  GE10 & IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

82 
\ (OUT3 <> GE8 & IN9 & ~IN8  GE11 & ~IN9  GE12 & ~IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

83 
\ (OUT4 <> GE11 & IN9  GE12 & IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

84 
\ (OUT5 <> GE14 & IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

85 
\ (OUT6 <> GE13 & ~IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

86 
\ (OUT7 <> GE13 & IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

87 
\ (OUT8 <> GE9 & ~IN8  GE15 & GE6  GE4 & IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

88 
\ (OUT9 <> GE9 & IN8  ~GE15 & GE10  GE16) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

89 
\ (OUT10 <> GE7) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

90 
\ (WRES0 <> ~IN5 & ~IN4 & ~IN3 & ~IN2 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

91 
\ (WRES1 <> ~IN7 & ~IN6 & ~IN2 & ~IN1 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

92 
\ (WRES2 <> ~IN7 & ~IN6 & ~IN5 & ~IN4 & ~IN3 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

93 
\ (WRES5 <> ~IN5 & IN4  IN5 & ~IN4) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

94 
\ (WRES6 <> WRES0 & IN7 & ~IN6 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

95 
\ (WRES9 <> WRES1 & ~IN5 & ~IN4 & IN3) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

96 
\ (WRES7 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

97 
\ WRES0 & ~IN9 & ~IN7 & ~IN6 & IN0  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

98 
\ WRES0 & IN9 & ~IN7 & IN6 & ~IN0  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

99 
\ WRES2 & IN2 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

100 
\ (WRES10 <> WRES6  WRES5 & WRES1 & ~IN3) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

101 
\ (WRES12 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

102 
\ WRES0 & IN9 & ~IN7 & ~IN6 & IN0  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

103 
\ WRES0 & ~IN9 & ~IN7 & IN6 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

104 
\ (WRES14 <> WRES2 & IN8 & ~IN2 & IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

105 
\ (WRES15 <> ~IN8  IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

106 
\ (WRES4 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

107 
\ WRES5 & WRES1 & IN8 & ~IN3  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

108 
\ WRES2 & IN2 & ~IN1  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

109 
\ WRES0 & ~IN7 & IN6 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

110 
\ (WRES13 <> WRES1 & ~IN8 & IN5 & ~IN4 & ~IN3) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

111 
\ (WRES11 <> WRES9  WRES6 & ~IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

112 
\ (WRES8 <> WRES1 & ~IN5 & IN4 & ~IN3  WRES2 & ~IN2 & IN1) \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

113 
\ > (OUT10 <> WRES7) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

114 
\ (OUT9 <> WRES9 & IN8  WRES12  WRES14 & ~IN9  ~WRES15 & WRES10) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

115 
\ (OUT8 <> WRES9 & ~IN8  WRES15 & WRES6  WRES4 & IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

116 
\ (OUT7 <> WRES13 & IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

117 
\ (OUT6 <> WRES13 & ~IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

118 
\ (OUT5 <> WRES14 & IN9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

119 
\ (OUT4 <> WRES11 & IN9  WRES12 & IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

120 
\ (OUT3 <> WRES8 & IN9 & ~IN8  WRES11 & ~IN9  WRES12 & ~IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

121 
\ (OUT2 <> WRES8 & ~IN9  WRES10 & IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

122 
\ (OUT1 <> WRES7 & IN8) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

123 
\ (OUT0 <> WRES7 & ~IN8)"; 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

124 
by (svc_tac 1); 
10126  125 
qed ""; 
7161  126 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

127 
(*Tautology name: sqn_be. Fast_tac only takes a couple of seconds.*) 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

128 
Goal "(GE0 <> IN6 & IN1  ~IN6 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

129 
\ (GE8 <> ~IN3 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

130 
\ (GE5 <> IN6  IN5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

131 
\ (GE9 <> ~GE0  IN2  ~IN5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

132 
\ (GE1 <> IN3  ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

133 
\ (GE11 <> GE8 & IN4) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

134 
\ (GE3 <> ~IN4  ~IN2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

135 
\ (GE34 <> ~GE5 & IN4  ~GE9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

136 
\ (GE2 <> ~IN4 & IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

137 
\ (GE14 <> ~GE1 & ~IN4) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

138 
\ (GE19 <> GE11 & ~GE5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

139 
\ (GE13 <> GE8 & ~GE3 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

140 
\ (GE20 <> ~IN5 & IN2  GE34) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

141 
\ (GE12 <> GE2 & ~IN3) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

142 
\ (GE27 <> GE14 & IN6  GE19) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

143 
\ (GE10 <> ~IN6  IN5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

144 
\ (GE28 <> GE13  GE20 & ~GE1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

145 
\ (GE6 <> ~IN5  IN6) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

146 
\ (GE15 <> GE2 & IN2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

147 
\ (GE29 <> GE27  GE12 & GE5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

148 
\ (GE4 <> IN3 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

149 
\ (GE21 <> ~GE10 & ~IN1  ~IN5 & ~IN2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

150 
\ (GE30 <> GE28  GE14 & IN2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

151 
\ (GE31 <> GE29  GE15 & ~GE6) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

152 
\ (GE7 <> ~IN6  ~IN5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

153 
\ (GE17 <> ~GE3 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

154 
\ (GE18 <> GE4 & IN2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

155 
\ (GE16 <> GE2 & IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

156 
\ (GE23 <> GE19  GE9 & ~GE1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

157 
\ (GE32 <> GE15 & ~IN6 & ~IN0  GE21 & GE4 & ~IN4  GE30  GE31) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

158 
\ (GE33 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

159 
\ GE18 & ~GE6 & ~IN4  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

160 
\ GE17 & ~GE7 & IN3  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

161 
\ ~GE7 & GE4 & ~GE3  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

162 
\ GE11 & IN5 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

163 
\ (GE25 <> GE14 & ~GE6  GE13 & ~GE5  GE16 & ~IN5  GE15 & GE1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

164 
\ (GE26 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

165 
\ GE12 & IN5 & ~IN2  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

166 
\ GE10 & GE4 & IN1  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

167 
\ GE17 & ~GE6 & IN0  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

168 
\ GE2 & ~IN6) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

169 
\ (GE24 <> GE23  GE16 & GE7) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

170 
\ (OUT0 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

171 
\ GE6 & IN4 & ~IN1 & IN0  GE18 & GE0 & ~IN5  GE12 & ~GE10  GE24) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

172 
\ (OUT1 <> GE26  GE25  ~GE5 & GE4 & GE3  GE7 & ~GE1 & IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

173 
\ (OUT2 <> GE33  GE32) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

174 
\ (WRES8 <> ~IN3 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

175 
\ (WRES0 <> IN6 & IN1  ~IN6 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

176 
\ (WRES2 <> ~IN4 & IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

177 
\ (WRES3 <> ~IN4  ~IN2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

178 
\ (WRES1 <> IN3  ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

179 
\ (WRES4 <> IN3 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

180 
\ (WRES5 <> IN6  IN5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

181 
\ (WRES11 <> WRES8 & IN4) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

182 
\ (WRES9 <> ~WRES0  IN2  ~IN5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

183 
\ (WRES10 <> ~IN6  IN5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

184 
\ (WRES6 <> ~IN5  IN6) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

185 
\ (WRES7 <> ~IN6  ~IN5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

186 
\ (WRES12 <> WRES2 & ~IN3) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

187 
\ (WRES13 <> WRES8 & ~WRES3 & ~IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

188 
\ (WRES14 <> ~WRES1 & ~IN4) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

189 
\ (WRES15 <> WRES2 & IN2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

190 
\ (WRES17 <> ~WRES3 & ~IN1) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

191 
\ (WRES18 <> WRES4 & IN2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

192 
\ (WRES19 <> WRES11 & ~WRES5) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

193 
\ (WRES20 <> ~IN5 & IN2  ~WRES5 & IN4  ~WRES9) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

194 
\ (WRES21 <> ~WRES10 & ~IN1  ~IN5 & ~IN2) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

195 
\ (WRES16 <> WRES2 & IN0) \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

196 
\ > (OUT2 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

197 
\ WRES11 & IN5 & ~IN0  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

198 
\ ~WRES7 & WRES4 & ~WRES3  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

199 
\ WRES12 & WRES5  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

200 
\ WRES13  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

201 
\ WRES14 & IN2  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

202 
\ WRES14 & IN6  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

203 
\ WRES15 & ~WRES6  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

204 
\ WRES15 & ~IN6 & ~IN0  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

205 
\ WRES17 & ~WRES7 & IN3  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

206 
\ WRES18 & ~WRES6 & ~IN4  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

207 
\ WRES20 & ~WRES1  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

208 
\ WRES21 & WRES4 & ~IN4  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

209 
\ WRES19) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

210 
\ (OUT1 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

211 
\ ~WRES5 & WRES4 & WRES3  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

212 
\ WRES7 & ~WRES1 & IN1  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

213 
\ WRES2 & ~IN6  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

214 
\ WRES10 & WRES4 & IN1  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

215 
\ WRES12 & IN5 & ~IN2  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

216 
\ WRES13 & ~WRES5  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

217 
\ WRES14 & ~WRES6  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

218 
\ WRES15 & WRES1  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

219 
\ WRES16 & ~IN5  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

220 
\ WRES17 & ~WRES6 & IN0) & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

221 
\ (OUT0 <> \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

222 
\ WRES6 & IN4 & ~IN1 & IN0  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

223 
\ WRES9 & ~WRES1  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

224 
\ WRES12 & ~WRES10  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

225 
\ WRES16 & WRES7  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

226 
\ WRES18 & WRES0 & ~IN5  \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

227 
\ WRES19)"; 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

228 
by (svc_tac 1); 
10126  229 
qed ""; 
7181  230 

231 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

232 
(** Linear arithmetic **) 
7161  233 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

234 
Goal "x ~= #14 & x ~= #13 & x ~= #12 & x ~= #11 & x ~= #10 & x ~= #9 & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

235 
\ x ~= #8 & x ~= #7 & x ~= #6 & x ~= #5 & x ~= #4 & x ~= #3 & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

236 
\ x ~= #2 & x ~= #1 & #0 < x & x < #16 > #15 = (x::int)"; 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

237 
by (svc_tac 1); 
10126  238 
qed ""; 
7161  239 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

240 
(*merely to test polarity handling in the presence of biconditionals*) 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

241 
Goal "(x < (y::int)) = (x+#1 <= y)"; 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

242 
by (svc_tac 1); 
10126  243 
qed ""; 
7161  244 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

245 
(** Natural number examples requiring implicit "nonnegative" assumptions*) 
7161  246 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

247 
Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \ 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

248 
\ a + #3*b <= #5 + #2*c > #2 + #3*b <= #2*a + #6*c"; 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

249 
by (svc_tac 1); 
10126  250 
qed ""; 
7161  251 

7189
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

252 
Goal "(n::nat) < #2 ==> (n = #0)  (n = #1)"; 
55f7679dc59a
the whole file is now loaded only if SVC is enabled
paulson
parents:
7181
diff
changeset

253 
by (svc_tac 1); 
10126  254 
qed ""; 