src/HOL/Sledgehammer.thy
changeset 36569 3a29eb7606c3
parent 36394 1a48d18449d8
child 37399 34f080a12063
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Apr 29 19:08:02 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Apr 30 09:36:45 2010 +0200
     1.3 @@ -25,28 +25,28 @@
     1.4    ("Tools/Sledgehammer/metis_tactics.ML")
     1.5  begin
     1.6  
     1.7 -definition COMBI :: "'a \<Rightarrow> 'a"
     1.8 -  where "COMBI P \<equiv> P"
     1.9 +definition COMBI :: "'a \<Rightarrow> 'a" where
    1.10 +[no_atp]: "COMBI P \<equiv> P"
    1.11  
    1.12 -definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
    1.13 -  where "COMBK P Q \<equiv> P"
    1.14 +definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
    1.15 +[no_atp]: "COMBK P Q \<equiv> P"
    1.16  
    1.17 -definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.18 -  where "COMBB P Q R \<equiv> P (Q R)"
    1.19 +definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
    1.20 +"COMBB P Q R \<equiv> P (Q R)"
    1.21  
    1.22 -definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
    1.23 -  where "COMBC P Q R \<equiv> P R Q"
    1.24 +definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.25 +[no_atp]: "COMBC P Q R \<equiv> P R Q"
    1.26  
    1.27 -definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.28 -  where "COMBS P Q R \<equiv> P R (Q R)"
    1.29 +definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.30 +[no_atp]: "COMBS P Q R \<equiv> P R (Q R)"
    1.31  
    1.32 -definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.33 -  where "fequal X Y \<equiv> (X = Y)"
    1.34 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.35 +"fequal X Y \<equiv> (X = Y)"
    1.36  
    1.37 -lemma fequal_imp_equal: "fequal X Y \<Longrightarrow> X = Y"
    1.38 +lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y"
    1.39    by (simp add: fequal_def)
    1.40  
    1.41 -lemma equal_imp_fequal: "X = Y \<Longrightarrow> fequal X Y"
    1.42 +lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
    1.43    by (simp add: fequal_def)
    1.44  
    1.45  text{*These two represent the equivalence between Boolean equality and iff.
    1.46 @@ -61,31 +61,31 @@
    1.47  
    1.48  text{*Theorems for translation to combinators*}
    1.49  
    1.50 -lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
    1.51 +lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
    1.52  apply (rule eq_reflection)
    1.53  apply (rule ext) 
    1.54  apply (simp add: COMBS_def) 
    1.55  done
    1.56  
    1.57 -lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
    1.58 +lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
    1.59  apply (rule eq_reflection)
    1.60  apply (rule ext) 
    1.61  apply (simp add: COMBI_def) 
    1.62  done
    1.63  
    1.64 -lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
    1.65 +lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
    1.66  apply (rule eq_reflection)
    1.67  apply (rule ext) 
    1.68  apply (simp add: COMBK_def) 
    1.69  done
    1.70  
    1.71 -lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
    1.72 +lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
    1.73  apply (rule eq_reflection)
    1.74  apply (rule ext) 
    1.75  apply (simp add: COMBB_def) 
    1.76  done
    1.77  
    1.78 -lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
    1.79 +lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
    1.80  apply (rule eq_reflection)
    1.81  apply (rule ext) 
    1.82  apply (simp add: COMBC_def)