src/HOL/Sledgehammer.thy
changeset 38606 3003ddbd46d9
parent 38282 319c59682c51
child 38988 483879af0643
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Aug 19 14:39:31 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Aug 19 18:16:47 2010 +0200
     1.3 @@ -31,28 +31,31 @@
     1.4  [no_atp]: "skolem_id = (\<lambda>x. x)"
     1.5  
     1.6  definition COMBI :: "'a \<Rightarrow> 'a" where
     1.7 -[no_atp]: "COMBI P \<equiv> P"
     1.8 +[no_atp]: "COMBI P = P"
     1.9  
    1.10  definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
    1.11 -[no_atp]: "COMBK P Q \<equiv> P"
    1.12 +[no_atp]: "COMBK P Q = P"
    1.13  
    1.14  definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
    1.15 -"COMBB P Q R \<equiv> P (Q R)"
    1.16 +"COMBB P Q R = P (Q R)"
    1.17  
    1.18  definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.19 -[no_atp]: "COMBC P Q R \<equiv> P R Q"
    1.20 +[no_atp]: "COMBC P Q R = P R Q"
    1.21  
    1.22  definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.23 -[no_atp]: "COMBS P Q R \<equiv> P R (Q R)"
    1.24 +[no_atp]: "COMBS P Q R = P R (Q R)"
    1.25  
    1.26  definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.27 -"fequal X Y \<equiv> (X = Y)"
    1.28 +"fequal X Y \<longleftrightarrow> (X = Y)"
    1.29 +
    1.30 +lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
    1.31 +by (simp add: fequal_def)
    1.32  
    1.33 -lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y"
    1.34 -  by (simp add: fequal_def)
    1.35 +lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
    1.36 +by (simp add: fequal_def)
    1.37  
    1.38 -lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
    1.39 -  by (simp add: fequal_def)
    1.40 +lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
    1.41 +by auto
    1.42  
    1.43  text{*Theorems for translation to combinators*}
    1.44