23 ("Tools/Sledgehammer/sledgehammer_isar.ML") |
23 ("Tools/Sledgehammer/sledgehammer_isar.ML") |
24 ("Tools/Sledgehammer/meson_tactic.ML") |
24 ("Tools/Sledgehammer/meson_tactic.ML") |
25 ("Tools/Sledgehammer/metis_tactics.ML") |
25 ("Tools/Sledgehammer/metis_tactics.ML") |
26 begin |
26 begin |
27 |
27 |
28 definition COMBI :: "'a \<Rightarrow> 'a" |
28 definition COMBI :: "'a \<Rightarrow> 'a" where |
29 where "COMBI P \<equiv> P" |
29 [no_atp]: "COMBI P \<equiv> P" |
30 |
30 |
31 definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" |
31 definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where |
32 where "COMBK P Q \<equiv> P" |
32 [no_atp]: "COMBK P Q \<equiv> P" |
33 |
33 |
34 definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" |
34 definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]: |
35 where "COMBB P Q R \<equiv> P (Q R)" |
35 "COMBB P Q R \<equiv> P (Q R)" |
36 |
36 |
37 definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" |
37 definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where |
38 where "COMBC P Q R \<equiv> P R Q" |
38 [no_atp]: "COMBC P Q R \<equiv> P R Q" |
39 |
39 |
40 definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" |
40 definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where |
41 where "COMBS P Q R \<equiv> P R (Q R)" |
41 [no_atp]: "COMBS P Q R \<equiv> P R (Q R)" |
42 |
42 |
43 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
43 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]: |
44 where "fequal X Y \<equiv> (X = Y)" |
44 "fequal X Y \<equiv> (X = Y)" |
45 |
45 |
46 lemma fequal_imp_equal: "fequal X Y \<Longrightarrow> X = Y" |
46 lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y" |
47 by (simp add: fequal_def) |
47 by (simp add: fequal_def) |
48 |
48 |
49 lemma equal_imp_fequal: "X = Y \<Longrightarrow> fequal X Y" |
49 lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y" |
50 by (simp add: fequal_def) |
50 by (simp add: fequal_def) |
51 |
51 |
52 text{*These two represent the equivalence between Boolean equality and iff. |
52 text{*These two represent the equivalence between Boolean equality and iff. |
53 They can't be converted to clauses automatically, as the iff would be |
53 They can't be converted to clauses automatically, as the iff would be |
54 expanded...*} |
54 expanded...*} |
59 lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q" |
59 lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q" |
60 by blast |
60 by blast |
61 |
61 |
62 text{*Theorems for translation to combinators*} |
62 text{*Theorems for translation to combinators*} |
63 |
63 |
64 lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g" |
64 lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g" |
65 apply (rule eq_reflection) |
65 apply (rule eq_reflection) |
66 apply (rule ext) |
66 apply (rule ext) |
67 apply (simp add: COMBS_def) |
67 apply (simp add: COMBS_def) |
68 done |
68 done |
69 |
69 |
70 lemma abs_I: "\<lambda>x. x \<equiv> COMBI" |
70 lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI" |
71 apply (rule eq_reflection) |
71 apply (rule eq_reflection) |
72 apply (rule ext) |
72 apply (rule ext) |
73 apply (simp add: COMBI_def) |
73 apply (simp add: COMBI_def) |
74 done |
74 done |
75 |
75 |
76 lemma abs_K: "\<lambda>x. y \<equiv> COMBK y" |
76 lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y" |
77 apply (rule eq_reflection) |
77 apply (rule eq_reflection) |
78 apply (rule ext) |
78 apply (rule ext) |
79 apply (simp add: COMBK_def) |
79 apply (simp add: COMBK_def) |
80 done |
80 done |
81 |
81 |
82 lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g" |
82 lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g" |
83 apply (rule eq_reflection) |
83 apply (rule eq_reflection) |
84 apply (rule ext) |
84 apply (rule ext) |
85 apply (simp add: COMBB_def) |
85 apply (simp add: COMBB_def) |
86 done |
86 done |
87 |
87 |
88 lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b" |
88 lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b" |
89 apply (rule eq_reflection) |
89 apply (rule eq_reflection) |
90 apply (rule ext) |
90 apply (rule ext) |
91 apply (simp add: COMBC_def) |
91 apply (simp add: COMBC_def) |
92 done |
92 done |
93 |
93 |