author  blanchet 
Wed, 15 Dec 2010 11:26:28 +0100  
changeset 41140  9c68004b8c9d 
parent 41042  8275f52ac991 
child 42349  721e85fd2db3 
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 

10 
imports Meson 

11 
uses "~~/src/Tools/Metis/metis.ML" 

12 
("Tools/Metis/metis_translate.ML") 

13 
("Tools/Metis/metis_reconstruct.ML") 

14 
("Tools/Metis/metis_tactics.ML") 

41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

15 
("Tools/try.ML") 
39946  16 
begin 
17 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

18 
definition fFalse :: bool where [no_atp]: 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

19 
"fFalse \<longleftrightarrow> False" 
39946  20 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

21 
definition fTrue :: bool where [no_atp]: 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

22 
"fTrue \<longleftrightarrow> True" 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

23 

9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

24 
definition fNot :: "bool \<Rightarrow> bool" where [no_atp]: 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

25 
"fNot P \<longleftrightarrow> \<not> P" 
39946  26 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

27 
definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]: 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

28 
"fconj P Q \<longleftrightarrow> P \<and> Q" 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

29 

9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

30 
definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]: 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

31 
"fdisj P Q \<longleftrightarrow> P \<or> Q" 
39946  32 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

33 
definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]: 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

34 
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)" 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

35 

9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

36 
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]: 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

37 
"fequal x y \<longleftrightarrow> (x = y)" 
39946  38 

39 
use "Tools/Metis/metis_translate.ML" 

40 
use "Tools/Metis/metis_reconstruct.ML" 

41 
use "Tools/Metis/metis_tactics.ML" 

39980  42 

43 
setup {* 

44 
Metis_Reconstruct.setup 

45 
#> Metis_Tactics.setup 

46 
*} 

39946  47 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

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

49 
hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41042
diff
changeset

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

51 

41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

52 
subsection {* Try *} 
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

53 

8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

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

55 

8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset

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

57 

39946  58 
end 