src/HOL/Sledgehammer.thy
changeset 39946 78faa9b31202
parent 39942 1ae333bfef14
child 39947 f95834c8bb4d
     1.1 --- a/src/HOL/Sledgehammer.thy	Mon Oct 04 22:01:34 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Mon Oct 04 22:45:09 2010 +0200
     1.3 @@ -8,15 +8,11 @@
     1.4  header {* Sledgehammer: Isabelle--ATP Linkup *}
     1.5  
     1.6  theory Sledgehammer
     1.7 -imports Plain Hilbert_Choice
     1.8 +imports Plain
     1.9  uses
    1.10    ("Tools/ATP/atp_problem.ML")
    1.11    ("Tools/ATP/atp_proof.ML")
    1.12    ("Tools/ATP/atp_systems.ML")
    1.13 -  ("~~/src/Tools/Metis/metis.ML")
    1.14 -  ("Tools/Sledgehammer/metis_translate.ML")
    1.15 -  ("Tools/Sledgehammer/metis_reconstruct.ML")
    1.16 -  ("Tools/Sledgehammer/metis_tactics.ML")
    1.17    ("Tools/Sledgehammer/sledgehammer_util.ML")
    1.18    ("Tools/Sledgehammer/sledgehammer_filter.ML")
    1.19    ("Tools/Sledgehammer/sledgehammer_translate.ML")
    1.20 @@ -26,88 +22,11 @@
    1.21    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.22  begin
    1.23  
    1.24 -lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
    1.25 -by simp
    1.26 -
    1.27 -definition skolem :: "'a \<Rightarrow> 'a" where
    1.28 -[no_atp]: "skolem = (\<lambda>x. x)"
    1.29 -
    1.30 -definition COMBI :: "'a \<Rightarrow> 'a" where
    1.31 -[no_atp]: "COMBI P = P"
    1.32 -
    1.33 -definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
    1.34 -[no_atp]: "COMBK P Q = P"
    1.35 -
    1.36 -definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
    1.37 -"COMBB P Q R = P (Q R)"
    1.38 -
    1.39 -definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.40 -[no_atp]: "COMBC P Q R = P R Q"
    1.41 -
    1.42 -definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.43 -[no_atp]: "COMBS P Q R = P R (Q R)"
    1.44 -
    1.45 -definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.46 -"fequal X Y \<longleftrightarrow> (X = Y)"
    1.47 -
    1.48 -lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
    1.49 -by (simp add: fequal_def)
    1.50 -
    1.51 -lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
    1.52 -by (simp add: fequal_def)
    1.53 -
    1.54 -lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
    1.55 -by auto
    1.56 -
    1.57 -lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
    1.58 -unfolding skolem_def COMBK_def by (rule refl)
    1.59 -
    1.60 -lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
    1.61 -lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
    1.62 -
    1.63 -text{*Theorems for translation to combinators*}
    1.64 -
    1.65 -lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
    1.66 -apply (rule eq_reflection)
    1.67 -apply (rule ext) 
    1.68 -apply (simp add: COMBS_def) 
    1.69 -done
    1.70 -
    1.71 -lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
    1.72 -apply (rule eq_reflection)
    1.73 -apply (rule ext) 
    1.74 -apply (simp add: COMBI_def) 
    1.75 -done
    1.76 -
    1.77 -lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
    1.78 -apply (rule eq_reflection)
    1.79 -apply (rule ext) 
    1.80 -apply (simp add: COMBK_def) 
    1.81 -done
    1.82 -
    1.83 -lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
    1.84 -apply (rule eq_reflection)
    1.85 -apply (rule ext) 
    1.86 -apply (simp add: COMBB_def) 
    1.87 -done
    1.88 -
    1.89 -lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
    1.90 -apply (rule eq_reflection)
    1.91 -apply (rule ext) 
    1.92 -apply (simp add: COMBC_def) 
    1.93 -done
    1.94 -
    1.95  use "Tools/ATP/atp_problem.ML"
    1.96  use "Tools/ATP/atp_proof.ML"
    1.97  use "Tools/ATP/atp_systems.ML"
    1.98  setup ATP_Systems.setup
    1.99  
   1.100 -use "~~/src/Tools/Metis/metis.ML"
   1.101 -use "Tools/Sledgehammer/metis_translate.ML"
   1.102 -use "Tools/Sledgehammer/metis_reconstruct.ML"
   1.103 -use "Tools/Sledgehammer/metis_tactics.ML"
   1.104 -setup Metis_Tactics.setup
   1.105 -
   1.106  use "Tools/Sledgehammer/sledgehammer_util.ML"
   1.107  use "Tools/Sledgehammer/sledgehammer_filter.ML"
   1.108  use "Tools/Sledgehammer/sledgehammer_translate.ML"