author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46365  547d1a1dcaf6 
child 47790  2e1636e45770 
permissions  rwrr 
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

1 
(* Title: HOL/TPTP/CASC_Setup.thy 
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset

2 
Author: Jasmin Blanchette 
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset

3 
Copyright 2011 
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset

4 

42601  5 
Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and 
6 
TNT divisions. This theory file should be loaded by the Isabelle theory files 

7 
generated by Geoff Sutcliffe's TPTP2X tool from the original THF0 files. 

42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset

8 
*) 
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset

9 

42601  10 
theory CASC_Setup 
43805  11 
imports Complex_Main 
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

12 
uses "../ex/sledgehammer_tactics.ML" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

13 
begin 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

14 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

15 
consts 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

16 
is_int :: "'a \<Rightarrow> bool" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

17 
is_rat :: "'a \<Rightarrow> bool" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

18 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

19 
overloading rat_is_int \<equiv> "is_int :: rat \<Rightarrow> bool" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

20 
begin 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

21 
definition "rat_is_int (q\<Colon>rat) \<longleftrightarrow> (\<exists>n\<Colon>int. q = of_int n)" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

22 
end 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

23 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

24 
overloading real_is_int \<equiv> "is_int :: real \<Rightarrow> bool" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

25 
begin 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

26 
definition "real_is_int (x\<Colon>real) \<longleftrightarrow> x \<in> \<int>" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

27 
end 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

28 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

29 
overloading real_is_rat \<equiv> "is_rat :: real \<Rightarrow> bool" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

30 
begin 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

31 
definition "real_is_rat (x\<Colon>real) \<longleftrightarrow> x \<in> \<rat>" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

32 
end 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

33 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

34 
consts 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

35 
to_int :: "'a \<Rightarrow> int" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

36 
to_rat :: "'a \<Rightarrow> rat" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

37 
to_real :: "'a \<Rightarrow> real" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

38 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

39 
overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

40 
begin 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

41 
definition "rat_to_int (q\<Colon>rat) = floor q" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

42 
end 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

43 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

44 
overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

45 
begin 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

46 
definition "real_to_int (x\<Colon>real) = floor x" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

47 
end 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

48 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

49 
overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat" 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

50 
begin 
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

51 
definition "int_to_rat (n\<Colon>int) = (of_int n\<Colon>rat)" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

52 
end 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

53 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

54 
overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

55 
begin 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

56 
definition "real_to_rat (x\<Colon>real) = (inv real x\<Colon>rat)" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

57 
end 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

58 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

59 
overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

60 
begin 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

61 
definition "int_to_real (n\<Colon>int) = real n" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

62 
end 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

63 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

64 
overloading rat_to_real \<equiv> "to_real :: rat \<Rightarrow> real" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

65 
begin 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

66 
definition "rat_to_real (x\<Colon>rat) = (of_rat x\<Colon>real)" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

67 
end 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

68 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

69 
declare 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

70 
rat_is_int_def [simp] 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

71 
real_is_int_def [simp] 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

72 
real_is_rat_def [simp] 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

73 
rat_to_int_def [simp] 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

74 
real_to_int_def [simp] 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

75 
int_to_rat_def [simp] 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

76 
real_to_rat_def [simp] 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

77 
int_to_real_def [simp] 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

78 
rat_to_real_def [simp] 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

79 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

80 
lemma to_rat_is_int [intro, simp]: "is_int (to_rat (n\<Colon>int))" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

81 
by (metis int_to_rat_def rat_is_int_def) 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

82 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

83 
lemma to_real_is_int [intro, simp]: "is_int (to_real (n\<Colon>int))" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

84 
by (metis Ints_real_of_int int_to_real_def real_is_int_def) 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

85 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

86 
lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q\<Colon>rat))" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

87 
by (metis Rats_of_rat rat_to_real_def real_is_rat_def) 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

88 

6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

89 
lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)" 
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset

90 
by (metis injI of_rat_eq_iff rat_to_real_def) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

91 

a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

92 
declare [[smt_oracle]] 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

93 

42106
ed1d40888b1b
specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet
parents:
42078
diff
changeset

94 
refute_params [maxtime = 10000, no_assms, expect = genuine] 
ed1d40888b1b
specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet
parents:
42078
diff
changeset

95 
nitpick_params [timeout = none, card = 150, verbose, dont_box, no_assms, 
42211
9e2673711c77
make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option
blanchet
parents:
42106
diff
changeset

96 
batch_size = 1, expect = genuine] 
42106
ed1d40888b1b
specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet
parents:
42078
diff
changeset

97 

42078
d5bf0ce40bd7
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
wenzelm
parents:
42071
diff
changeset

98 
ML {* Proofterm.proofs := 0 *} 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

99 

a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

100 
ML {* 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

101 
fun SOLVE_TIMEOUT seconds name tac st = 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

102 
let 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

103 
val result = 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

104 
TimeLimit.timeLimit (Time.fromSeconds seconds) 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

105 
(fn () => SINGLE (SOLVE tac) st) () 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

106 
handle TimeLimit.TimeOut => NONE 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

107 
 ERROR _ => NONE 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

108 
in 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

109 
(case result of 
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset

110 
NONE => (warning ("FAILURE: " ^ name); Seq.empty) 
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset

111 
 SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st')) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

112 
end 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

113 
*} 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

114 

a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

115 
ML {* 
42800
df2dc9406287
just one universal Proof.context  discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset

116 
fun isabellep_tac ctxt max_secs = 
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset

117 
SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

118 
ORELSE 
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset

119 
SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44432
diff
changeset

120 
(ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44432
diff
changeset

121 
Sledgehammer_Filter.no_relevance_override)) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

122 
ORELSE 
42800
df2dc9406287
just one universal Proof.context  discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset

123 
SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) 
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset

124 
ORELSE 
42800
df2dc9406287
just one universal Proof.context  discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset

125 
SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

126 
ORELSE 
42800
df2dc9406287
just one universal Proof.context  discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset

127 
SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44432
diff
changeset

128 
THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44432
diff
changeset

129 
Sledgehammer_Filter.no_relevance_override)) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

130 
ORELSE 
43205  131 
SOLVE_TIMEOUT (max_secs div 10) "metis" 
46365  132 
(ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt [])) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

133 
ORELSE 
42800
df2dc9406287
just one universal Proof.context  discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset

134 
SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

135 
ORELSE 
43807
bfad30568d40
added arithmetic decision procedure to CASC setup
blanchet
parents:
43806
diff
changeset

136 
SOLVE_TIMEOUT (max_secs div 20) "best" (ALLGOALS (best_tac ctxt)) 
bfad30568d40
added arithmetic decision procedure to CASC setup
blanchet
parents:
43806
diff
changeset

137 
ORELSE 
bfad30568d40
added arithmetic decision procedure to CASC setup
blanchet
parents:
43806
diff
changeset

138 
SOLVE_TIMEOUT (max_secs div 20) "arith" (ALLGOALS (Arith_Data.arith_tac ctxt)) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

139 
ORELSE 
42800
df2dc9406287
just one universal Proof.context  discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset

140 
SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt)) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

141 
ORELSE 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44651
diff
changeset

142 
SOLVE_TIMEOUT max_secs "fastforce" (ALLGOALS (fast_force_tac ctxt)) 
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

143 
*} 
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

144 

42827  145 
method_setup isabellep = {* 
43807
bfad30568d40
added arithmetic decision procedure to CASC setup
blanchet
parents:
43806
diff
changeset

146 
Scan.lift (Scan.optional Parse.nat 6000) >> 
42827  147 
(fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m)) 
43161  148 
*} "combination of Isabelle provers and oracles for CASC" 
42827  149 

42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset

150 
end 