author  blanchet 
Tue, 31 May 2011 16:38:36 +0200  
changeset 43085  0a2f5b86bdd7 
parent 43016  42330f25142c 
child 44651  5d6a11e166cf 
permissions  rwrr 
39946  1 
(* Title: HOL/Metis.thy 
2 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 

3 
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA 

4 
Author: Jasmin Blanchette, TU Muenchen 

5 
*) 

6 

7 
header {* Metis Proof Method *} 

8 

9 
theory Metis 

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

10 
imports ATP 
39946  11 
uses "~~/src/Tools/Metis/metis.ML" 
12 
("Tools/Metis/metis_translate.ML") 

13 
("Tools/Metis/metis_reconstruct.ML") 

14 
("Tools/Metis/metis_tactics.ML") 

43016  15 
("Tools/try_methods.ML") 
39946  16 
begin 
17 

42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

18 
subsection {* Literal selection helpers *} 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

19 

721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

20 
definition select :: "'a \<Rightarrow> 'a" where 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

21 
[no_atp]: "select = (\<lambda>x. x)" 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

22 

721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

23 
lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A" 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

24 
by (cut_tac atomize_not [of "\<not> A"]) simp 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

25 

721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

26 
lemma atomize_not_select: "(A \<Longrightarrow> select False) \<equiv> Trueprop (\<not> A)" 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

27 
unfolding select_def by (rule atomize_not) 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

28 

721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

29 
lemma not_atomize_select: "(\<not> A \<Longrightarrow> select False) \<equiv> Trueprop A" 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

30 
unfolding select_def by (rule not_atomize) 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

31 

721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

32 
lemma select_FalseI: "False \<Longrightarrow> select False" by simp 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

33 

721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

34 

721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

35 
subsection {* Metis package *} 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

36 

39946  37 
use "Tools/Metis/metis_translate.ML" 
38 
use "Tools/Metis/metis_reconstruct.ML" 

39 
use "Tools/Metis/metis_tactics.ML" 

39980  40 

42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42349
diff
changeset

41 
setup {* Metis_Tactics.setup *} 
39946  42 

42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

43 
hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

44 
hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def 
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

45 
fequal_def select_def not_atomize atomize_not_select not_atomize_select 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

46 
select_FalseI 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39947
diff
changeset

47 

43016  48 
subsection {* Try Methods *} 
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

49 

43016  50 
use "Tools/try_methods.ML" 
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

51 

43016  52 
setup {* Try_Methods.setup *} 
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

53 

39946  54 
end 