author  wenzelm 
Sat, 26 Mar 2016 12:22:15 +0100  
changeset 62711  09df6a51ad3c 
parent 62672  068b430e678f 
child 69605  a96320074298 
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 

60758  7 
section \<open>Metis Proof Method\<close> 
39946  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 

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

56946  15 

60758  16 
subsection \<open>Literal selection and lambdalifting helpers\<close> 
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 

60758  39 
subsection \<open>Metis package\<close> 
42349
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 

56946  45 
hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda 
46 
hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI 

47 
fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def 

48 
fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table fAll_table fEx_table 

49 
fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws fimplies_laws 

50 
fequal_laws fAll_law fEx_law lambda_def eq_lambdaI 

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

51 

39946  52 
end 