author  wenzelm 
Tue, 25 Mar 2014 19:03:02 +0100  
changeset 56281  03c3d1a7c3b8 
parent 55509  bd67ebe275e0 
child 56946  10d9bd4ea94f 
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 
begin 
12 

56281  13 
declare [[ML_print_depth = 0]] 
48891  14 
ML_file "~~/src/Tools/Metis/metis.ML" 
56281  15 
declare [[ML_print_depth = 10]] 
48891  16 

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

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

18 

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

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

21 

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

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

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

24 

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

25 
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

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

27 

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

28 
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

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

30 

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

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

32 

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

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

35 

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

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

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

38 

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

39 

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

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

41 

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

44 
ML_file "Tools/Metis/metis_tactic.ML" 

39980  45 

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

46 
setup {* Metis_Tactic.setup *} 
39946  47 

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

48 
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

49 
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

50 
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

51 
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

52 
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

53 
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

54 
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

55 

39946  56 
end 