author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46320  0b8b73b49848 
child 47946  33afcfad3f8d 
permissions  rwrr 
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  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 
44087
8e491cb8841c
load lambdalifting structure earlier, so it can be used in Metis
blanchet
parents:
43678
diff
changeset

10 
uses "Tools/lambda_lifting.ML" 
8e491cb8841c
load lambdalifting structure earlier, so it can be used in Metis
blanchet
parents:
43678
diff
changeset

11 
"Tools/monomorph.ML" 
43108
eb1e31eb7449
use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
blanchet
parents:
43085
diff
changeset

12 
"Tools/ATP/atp_util.ML" 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

13 
"Tools/ATP/atp_problem.ML" 
40178
00152d17855b
reverted e7a80c6752c9  there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40121
diff
changeset

14 
"Tools/ATP/atp_proof.ML" 
46320  15 
"Tools/ATP/atp_proof_redirect.ML" 
16 
("Tools/ATP/atp_problem_generate.ML") 

17 
("Tools/ATP/atp_proof_reconstruct.ML") 

45522  18 
("Tools/ATP/atp_systems.ML") 
39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

19 
begin 
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

20 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

21 
subsection {* Higherorder reasoning helpers *} 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

22 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

23 
definition fFalse :: bool where [no_atp]: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

24 
"fFalse \<longleftrightarrow> False" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

25 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

26 
definition fTrue :: bool where [no_atp]: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

27 
"fTrue \<longleftrightarrow> True" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

28 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

29 
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

30 
"fNot P \<longleftrightarrow> \<not> P" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

31 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

32 
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

33 
"fconj P Q \<longleftrightarrow> P \<and> Q" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

34 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

35 
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

36 
"fdisj P Q \<longleftrightarrow> P \<or> Q" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

37 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

38 
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

39 
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

40 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

41 
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

42 
"fequal x y \<longleftrightarrow> (x = y)" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

43 

43678  44 
definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]: 
45 
"fAll P \<longleftrightarrow> All P" 

46 

47 
definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]: 

48 
"fEx P \<longleftrightarrow> Ex P" 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

49 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

50 
subsection {* Setup *} 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

51 

46320  52 
use "Tools/ATP/atp_problem_generate.ML" 
53 
use "Tools/ATP/atp_proof_reconstruct.ML" 

45522  54 
use "Tools/ATP/atp_systems.ML" 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

55 

39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

56 
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

57 

ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

58 
end 