src/HOL/ATP.thy
author webertj
Fri, 19 Oct 2012 15:12:52 +0200
changeset 49962 a8cc904a6820
parent 48891 c0eafbd55de3
child 51575 907efc894051
permissions -rw-r--r--
Renamed {left,right}_distrib to distrib_{right,left}.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39951
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/ATP.thy
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     4
*)
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     5
39958
88c9aa5666de tuned comments
blanchet
parents: 39951
diff changeset
     6
header {* Automatic Theorem Provers (ATPs) *}
39951
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     7
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     8
theory ATP
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
     9
imports Meson
39951
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
    10
begin
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
    11
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    12
ML_file "Tools/lambda_lifting.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    13
ML_file "Tools/monomorph.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    14
ML_file "Tools/ATP/atp_util.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    15
ML_file "Tools/ATP/atp_problem.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    16
ML_file "Tools/ATP/atp_proof.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    17
ML_file "Tools/ATP/atp_proof_redirect.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    18
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    19
subsection {* Higher-order reasoning helpers *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    20
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    21
definition fFalse :: bool where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    22
"fFalse \<longleftrightarrow> False"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    23
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    24
definition fTrue :: bool where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    25
"fTrue \<longleftrightarrow> True"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    26
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    27
definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    28
"fNot P \<longleftrightarrow> \<not> P"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    29
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    30
definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    31
"fComp P = (\<lambda>x. \<not> P x)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    32
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    33
definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    34
"fconj P Q \<longleftrightarrow> P \<and> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    35
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    36
definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    37
"fdisj P Q \<longleftrightarrow> P \<or> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    38
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    39
definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    40
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    41
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    42
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    43
"fequal x y \<longleftrightarrow> (x = y)"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    44
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    45
definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    46
"fAll P \<longleftrightarrow> All P"
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    47
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    48
definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    49
"fEx P \<longleftrightarrow> Ex P"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    50
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    51
lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    52
unfolding fFalse_def fTrue_def by simp
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    53
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    54
lemma fNot_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    55
"fNot fFalse = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    56
"fNot fTrue = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    57
unfolding fFalse_def fTrue_def fNot_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    58
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    59
lemma fconj_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    60
"fconj fFalse P = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    61
"fconj P fFalse = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    62
"fconj fTrue fTrue = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    63
unfolding fFalse_def fTrue_def fconj_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    64
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    65
lemma fdisj_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    66
"fdisj fTrue P = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    67
"fdisj P fTrue = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    68
"fdisj fFalse fFalse = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    69
unfolding fFalse_def fTrue_def fdisj_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    70
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    71
lemma fimplies_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    72
"fimplies P fTrue = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    73
"fimplies fFalse P = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    74
"fimplies fTrue fFalse = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    75
unfolding fFalse_def fTrue_def fimplies_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    76
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    77
lemma fequal_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    78
"fequal x x = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    79
"x = y \<or> fequal x y = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    80
unfolding fFalse_def fTrue_def fequal_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    81
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    82
lemma fAll_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    83
"Ex (fComp P) \<or> fAll P = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    84
"All P \<or> fAll P = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    85
unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    86
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    87
lemma fEx_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    88
"All (fComp P) \<or> fEx P = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    89
"Ex P \<or> fEx P = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    90
unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    91
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    92
lemma fNot_law:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    93
"fNot P \<noteq> P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    94
unfolding fNot_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    95
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    96
lemma fComp_law:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    97
"fComp P x \<longleftrightarrow> \<not> P x"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    98
unfolding fComp_def ..
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    99
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   100
lemma fconj_laws:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   101
"fconj P P \<longleftrightarrow> P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   102
"fconj P Q \<longleftrightarrow> fconj Q P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   103
"fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   104
unfolding fNot_def fconj_def fdisj_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   105
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   106
lemma fdisj_laws:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   107
"fdisj P P \<longleftrightarrow> P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   108
"fdisj P Q \<longleftrightarrow> fdisj Q P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   109
"fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   110
unfolding fNot_def fconj_def fdisj_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   111
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   112
lemma fimplies_laws:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   113
"fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   114
"fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   115
unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   116
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   117
lemma fequal_laws:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   118
"fequal x y = fequal y x"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   119
"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   120
"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   121
unfolding fFalse_def fTrue_def fequal_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   122
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   123
lemma fAll_law:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   124
"fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   125
unfolding fNot_def fComp_def fAll_def fEx_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   126
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   127
lemma fEx_law:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   128
"fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   129
unfolding fNot_def fComp_def fAll_def fEx_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   130
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
   131
subsection {* Setup *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
   132
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
   133
ML_file "Tools/ATP/atp_problem_generate.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
   134
ML_file "Tools/ATP/atp_proof_reconstruct.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
   135
ML_file "Tools/ATP/atp_systems.ML"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
   136
39951
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
   137
setup ATP_Systems.setup
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
   138
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
   139
end