author  blanchet 
Tue, 13 May 2014 11:10:23 +0200  
changeset 56946  10d9bd4ea94f 
parent 56281  03c3d1a7c3b8 
child 58818  ee85e7b82d00 
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 

56946  17 

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

18 
subsection {* Literal selection and lambdalifting helpers *} 
42349
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 
54148  21 
"select = (\<lambda>x. x)" 
42349
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 

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

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

36 

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

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

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

39 

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

40 

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

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

42 

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

45 
ML_file "Tools/Metis/metis_tactic.ML" 

39980  46 

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

47 
setup {* Metis_Tactic.setup *} 
39946  48 

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

51 
fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def 

52 
fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table fAll_table fEx_table 

53 
fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws fimplies_laws 

54 
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 