src/HOL/Metis.thy
changeset 39946 78faa9b31202
child 39947 f95834c8bb4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Metis.thy	Mon Oct 04 22:45:09 2010 +0200
     1.3 @@ -0,0 +1,35 @@
     1.4 +(*  Title:      HOL/Metis.thy
     1.5 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     1.6 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8 +*)
     1.9 +
    1.10 +header {* Metis Proof Method *}
    1.11 +
    1.12 +theory Metis
    1.13 +imports Meson
    1.14 +uses "~~/src/Tools/Metis/metis.ML"
    1.15 +     ("Tools/Metis/metis_translate.ML")
    1.16 +     ("Tools/Metis/metis_reconstruct.ML")
    1.17 +     ("Tools/Metis/metis_tactics.ML")
    1.18 +begin
    1.19 +
    1.20 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.21 +"fequal X Y \<longleftrightarrow> (X = Y)"
    1.22 +
    1.23 +lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
    1.24 +by (simp add: fequal_def)
    1.25 +
    1.26 +lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
    1.27 +by (simp add: fequal_def)
    1.28 +
    1.29 +lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
    1.30 +by auto
    1.31 +
    1.32 +use "Tools/Metis/metis_translate.ML"
    1.33 +use "Tools/Metis/metis_reconstruct.ML"
    1.34 +use "Tools/Metis/metis_tactics.ML"
    1.35 +
    1.36 +setup Metis_Tactics.setup
    1.37 +
    1.38 +end