author  blanchet 
Fri, 18 Oct 2013 10:43:21 +0200  
changeset 54148  c8cc5ab4a863 
parent 52641  c56b6fa636e8 
child 55178  318cd8ac1817 
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 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46641
diff
changeset

11 
keywords "try0" :: diag 
39946  12 
begin 
13 

48891  14 
ML_file "~~/src/Tools/Metis/metis.ML" 
15 

45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

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

17 

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

18 
definition select :: "'a \<Rightarrow> 'a" where 
54148  19 
"select = (\<lambda>x. x)" 
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

20 

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

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

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

23 

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

24 
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

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

26 

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

27 
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

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

29 

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

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

31 

45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

32 
definition lambda :: "'a \<Rightarrow> 'a" where 
54148  33 
"lambda = (\<lambda>x. x)" 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

34 

9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

35 
lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y" 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

36 
unfolding lambda_def by assumption 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

37 

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

38 

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

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

40 

48891  41 
ML_file "Tools/Metis/metis_generate.ML" 
42 
ML_file "Tools/Metis/metis_reconstruct.ML" 

43 
ML_file "Tools/Metis/metis_tactic.ML" 

39980  44 

44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
43085
diff
changeset

45 
setup {* Metis_Tactic.setup *} 
39946  46 

47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46950
diff
changeset

47 
hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46950
diff
changeset

48 
lambda 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46950
diff
changeset

49 
hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46950
diff
changeset

50 
select_FalseI fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46950
diff
changeset

51 
fequal_def fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46950
diff
changeset

52 
fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46950
diff
changeset

53 
fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

54 

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

55 

46641  56 
subsection {* Try0 *} 
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

57 

48891  58 
ML_file "Tools/try0.ML" 
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

59 

39946  60 
end 