src/HOL/TPTP/CASC_Setup.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46365 547d1a1dcaf6
child 47790 2e1636e45770
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
cddab94eeb14 renamed theory to make its purpose clearer
blanchet
parents: 42213
diff changeset
     5
Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and
cddab94eeb14 renamed theory to make its purpose clearer
blanchet
parents: 42213
diff changeset
     6
TNT divisions. This theory file should be loaded by the Isabelle theory files
cddab94eeb14 renamed theory to make its purpose clearer
blanchet
parents: 42213
diff changeset
     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
cddab94eeb14 renamed theory to make its purpose clearer
blanchet
parents: 42213
diff changeset
    10
theory CASC_Setup
43805
0349175384f8 pull in arithmetic theories
blanchet
parents: 43804
diff changeset
    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 = 1-50, 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
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43161
diff changeset
   131
   SOLVE_TIMEOUT (max_secs div 10) "metis"
46365
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46320
diff changeset
   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
8bfdcaf30551 provide isabellep as a method
blanchet
parents: 42800
diff changeset
   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
8bfdcaf30551 provide isabellep as a method
blanchet
parents: 42800
diff changeset
   147
    (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m))
43161
27dcda8fc89b tuned CASC method
blanchet
parents: 42827
diff changeset
   148
*} "combination of Isabelle provers and oracles for CASC"
42827
8bfdcaf30551 provide isabellep as a method
blanchet
parents: 42800
diff changeset
   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