src/HOL/ATP_Linkup.thy
author paulson
Wed, 03 Jan 2007 10:59:06 +0100
changeset 21977 7f7177a95189
parent 21453 03ca07d478be
child 21999 0cf192e489e2
permissions -rw-r--r--
first version of structured proof reconstruction
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ATP_Linkup.thy
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     4
    Author:     Jia Meng, NICTA
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     5
*)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     6
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     7
header{* The Isabelle-ATP Linkup *}
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     8
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
     9
theory ATP_Linkup
21453
03ca07d478be removed Extraction dependency
haftmann
parents: 21254
diff changeset
    10
imports Map Hilbert_Choice
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    11
uses
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    12
  "Tools/polyhash.ML"
21977
7f7177a95189 first version of structured proof reconstruction
paulson
parents: 21453
diff changeset
    13
  "Tools/res_clause.ML"
7f7177a95189 first version of structured proof reconstruction
paulson
parents: 21453
diff changeset
    14
  "Tools/res_reconstruct.ML"
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    15
  "Tools/ATP/watcher.ML"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    16
  "Tools/ATP/reduce_axiomsN.ML"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    17
  ("Tools/res_hol_clause.ML")
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    18
  ("Tools/res_axioms.ML")
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    19
  ("Tools/res_atp.ML")
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    20
  ("Tools/res_atp_provers.ML")
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    21
  ("Tools/res_atp_methods.ML")
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    22
begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    23
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    24
constdefs
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    25
  COMBI :: "'a => 'a"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    26
    "COMBI P == P"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    27
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    28
  COMBK :: "'a => 'b => 'a"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    29
    "COMBK P Q == P"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    30
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    31
  COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    32
    "COMBB P Q R == P (Q R)"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    33
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    34
  COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    35
    "COMBC P Q R == P R Q"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    36
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    37
  COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    38
    "COMBS P Q R == P R (Q R)"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    39
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    40
  COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    41
    "COMBB' M P Q R == M (P (Q R))"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    42
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    43
  COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    44
    "COMBC' M P Q R == M (P R) Q"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    45
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    46
  COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    47
    "COMBS' M P Q R == M (P R) (Q R)"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    48
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    49
  fequal :: "'a => 'a => bool"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    50
    "fequal X Y == (X=Y)"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    51
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    52
lemma fequal_imp_equal: "fequal X Y ==> X=Y"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    53
  by (simp add: fequal_def)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    54
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    55
lemma equal_imp_fequal: "X=Y ==> fequal X Y"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    56
  by (simp add: fequal_def)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    57
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    58
lemma K_simp: "COMBK P == (%Q. P)"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    59
apply (rule eq_reflection)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    60
apply (rule ext)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    61
apply (simp add: COMBK_def)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    62
done
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    63
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    64
lemma I_simp: "COMBI == (%P. P)"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    65
apply (rule eq_reflection)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    66
apply (rule ext)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    67
apply (simp add: COMBI_def)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    68
done
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    69
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    70
lemma B_simp: "COMBB P Q == %R. P (Q R)"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    71
apply (rule eq_reflection)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    72
apply (rule ext)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    73
apply (simp add: COMBB_def)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    74
done
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    75
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    76
text{*These two represent the equivalence between Boolean equality and iff.
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    77
They can't be converted to clauses automatically, as the iff would be
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    78
expanded...*}
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    79
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    80
lemma iff_positive: "P | Q | P=Q"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    81
by blast
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    82
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    83
lemma iff_negative: "~P | ~Q | P=Q"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    84
by blast
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    85
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    86
use "Tools/res_axioms.ML"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    87
use "Tools/res_hol_clause.ML"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    88
use "Tools/res_atp.ML"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    89
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    90
setup ResAxioms.meson_method_setup
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    91
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    92
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    93
subsection {* Setup for Vampire, E prover and SPASS *}
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    94
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    95
use "Tools/res_atp_provers.ML"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    96
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    97
oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    98
oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
    99
oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
   100
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
   101
use "Tools/res_atp_methods.ML"
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
   102
setup ResAtpMethods.ResAtps_setup
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
   103
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff changeset
   104
end