1 (* Title: HOL/TPTP/CASC_Setup.thy |
|
2 Author: Jasmin Blanchette |
|
3 Copyright 2011 |
|
4 |
|
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. |
|
8 *) |
|
9 |
|
10 theory CASC_Setup |
|
11 imports Complex_Main |
|
12 uses "sledgehammer_tactics.ML" |
|
13 begin |
|
14 |
|
15 consts |
|
16 is_int :: "'a \<Rightarrow> bool" |
|
17 is_rat :: "'a \<Rightarrow> bool" |
|
18 |
|
19 overloading rat_is_int \<equiv> "is_int :: rat \<Rightarrow> bool" |
|
20 begin |
|
21 definition "rat_is_int (q\<Colon>rat) \<longleftrightarrow> (\<exists>n\<Colon>int. q = of_int n)" |
|
22 end |
|
23 |
|
24 overloading real_is_int \<equiv> "is_int :: real \<Rightarrow> bool" |
|
25 begin |
|
26 definition "real_is_int (x\<Colon>real) \<longleftrightarrow> x \<in> \<int>" |
|
27 end |
|
28 |
|
29 overloading real_is_rat \<equiv> "is_rat :: real \<Rightarrow> bool" |
|
30 begin |
|
31 definition "real_is_rat (x\<Colon>real) \<longleftrightarrow> x \<in> \<rat>" |
|
32 end |
|
33 |
|
34 consts |
|
35 to_int :: "'a \<Rightarrow> int" |
|
36 to_rat :: "'a \<Rightarrow> rat" |
|
37 to_real :: "'a \<Rightarrow> real" |
|
38 |
|
39 overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int" |
|
40 begin |
|
41 definition "rat_to_int (q\<Colon>rat) = floor q" |
|
42 end |
|
43 |
|
44 overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int" |
|
45 begin |
|
46 definition "real_to_int (x\<Colon>real) = floor x" |
|
47 end |
|
48 |
|
49 overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat" |
|
50 begin |
|
51 definition "int_to_rat (n\<Colon>int) = (of_int n\<Colon>rat)" |
|
52 end |
|
53 |
|
54 overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat" |
|
55 begin |
|
56 definition "real_to_rat (x\<Colon>real) = (inv real x\<Colon>rat)" |
|
57 end |
|
58 |
|
59 overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real" |
|
60 begin |
|
61 definition "int_to_real (n\<Colon>int) = real n" |
|
62 end |
|
63 |
|
64 overloading rat_to_real \<equiv> "to_real :: rat \<Rightarrow> real" |
|
65 begin |
|
66 definition "rat_to_real (x\<Colon>rat) = (of_rat x\<Colon>real)" |
|
67 end |
|
68 |
|
69 declare |
|
70 rat_is_int_def [simp] |
|
71 real_is_int_def [simp] |
|
72 real_is_rat_def [simp] |
|
73 rat_to_int_def [simp] |
|
74 real_to_int_def [simp] |
|
75 int_to_rat_def [simp] |
|
76 real_to_rat_def [simp] |
|
77 int_to_real_def [simp] |
|
78 rat_to_real_def [simp] |
|
79 |
|
80 lemma to_rat_is_int [intro, simp]: "is_int (to_rat (n\<Colon>int))" |
|
81 by (metis int_to_rat_def rat_is_int_def) |
|
82 |
|
83 lemma to_real_is_int [intro, simp]: "is_int (to_real (n\<Colon>int))" |
|
84 by (metis Ints_real_of_int int_to_real_def real_is_int_def) |
|
85 |
|
86 lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q\<Colon>rat))" |
|
87 by (metis Rats_of_rat rat_to_real_def real_is_rat_def) |
|
88 |
|
89 lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)" |
|
90 by (metis injI of_rat_eq_iff rat_to_real_def) |
|
91 |
|
92 declare [[smt_oracle]] |
|
93 |
|
94 refute_params [maxtime = 10000, no_assms, expect = genuine] |
|
95 nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms, |
|
96 batch_size = 1, expect = genuine] |
|
97 |
|
98 ML {* Proofterm.proofs := 0 *} |
|
99 |
|
100 ML {* |
|
101 fun SOLVE_TIMEOUT seconds name tac st = |
|
102 let |
|
103 val result = |
|
104 TimeLimit.timeLimit (Time.fromSeconds seconds) |
|
105 (fn () => SINGLE (SOLVE tac) st) () |
|
106 handle TimeLimit.TimeOut => NONE |
|
107 | ERROR _ => NONE |
|
108 in |
|
109 (case result of |
|
110 NONE => (warning ("FAILURE: " ^ name); Seq.empty) |
|
111 | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st')) |
|
112 end |
|
113 *} |
|
114 |
|
115 ML {* |
|
116 fun isabellep_tac ctxt max_secs = |
|
117 SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) |
|
118 ORELSE |
|
119 SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
|
120 (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] |
|
121 Sledgehammer_Filter.no_relevance_override)) |
|
122 ORELSE |
|
123 SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) |
|
124 ORELSE |
|
125 SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) |
|
126 ORELSE |
|
127 SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt |
|
128 THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] |
|
129 Sledgehammer_Filter.no_relevance_override)) |
|
130 ORELSE |
|
131 SOLVE_TIMEOUT (max_secs div 10) "metis" |
|
132 (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt [])) |
|
133 ORELSE |
|
134 SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) |
|
135 ORELSE |
|
136 SOLVE_TIMEOUT (max_secs div 20) "best" (ALLGOALS (best_tac ctxt)) |
|
137 ORELSE |
|
138 SOLVE_TIMEOUT (max_secs div 20) "arith" (ALLGOALS (Arith_Data.arith_tac ctxt)) |
|
139 ORELSE |
|
140 SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt)) |
|
141 ORELSE |
|
142 SOLVE_TIMEOUT max_secs "fastforce" (ALLGOALS (fast_force_tac ctxt)) |
|
143 *} |
|
144 |
|
145 method_setup isabellep = {* |
|
146 Scan.lift (Scan.optional Parse.nat 6000) >> |
|
147 (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m)) |
|
148 *} "combination of Isabelle provers and oracles for CASC" |
|
149 |
|
150 end |
|