author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46950  d0181abdbdac 
child 47946  33afcfad3f8d 
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 
uses "~~/src/Tools/Metis/metis.ML" 
46320  13 
("Tools/Metis/metis_generate.ML") 
39946  14 
("Tools/Metis/metis_reconstruct.ML") 
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
43085
diff
changeset

15 
("Tools/Metis/metis_tactic.ML") 
46641  16 
("Tools/try0.ML") 
39946  17 
begin 
18 

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

19 
subsection {* Literal selection and lambdalifting helpers *} 
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 
definition select :: "'a \<Rightarrow> 'a" where 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

22 
[no_atp]: "select = (\<lambda>x. x)" 
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 not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A" 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset

25 
by (cut_tac atomize_not [of "\<not> A"]) simp 
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 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

28 
unfolding select_def by (rule atomize_not) 
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 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

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

32 

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

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

34 

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

35 
definition lambda :: "'a \<Rightarrow> 'a" where 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

36 
[no_atp]: "lambda = (\<lambda>x. x)" 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

37 

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

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

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

40 

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

41 

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

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

43 

46320  44 
use "Tools/Metis/metis_generate.ML" 
39946  45 
use "Tools/Metis/metis_reconstruct.ML" 
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 
use "Tools/Metis/metis_tactic.ML" 
39980  47 

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

48 
setup {* Metis_Tactic.setup *} 
39946  49 

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

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

51 
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

52 
fequal_def select_def not_atomize atomize_not_select not_atomize_select 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
44651
diff
changeset

53 
select_FalseI lambda_def eq_lambdaI 
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 

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

59 

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

61 

39946  62 
end 