--- a/src/HOL/ATP.thy Tue May 13 11:10:22 2014 +0200
+++ b/src/HOL/ATP.thy Tue May 13 11:10:23 2014 +0200
@@ -16,6 +16,7 @@
ML_file "Tools/ATP/atp_proof.ML"
ML_file "Tools/ATP/atp_proof_redirect.ML"
+
subsection {* Higher-order reasoning helpers *}
definition fFalse :: bool where
@@ -39,15 +40,15 @@
definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
-"fequal x y \<longleftrightarrow> (x = y)"
-
definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
"fAll P \<longleftrightarrow> All P"
definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
"fEx P \<longleftrightarrow> Ex P"
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
+"fequal x y \<longleftrightarrow> (x = y)"
+
lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
unfolding fFalse_def fTrue_def by simp
@@ -74,11 +75,6 @@
"fimplies fTrue fFalse = fFalse"
unfolding fFalse_def fTrue_def fimplies_def by auto
-lemma fequal_table:
-"fequal x x = fTrue"
-"x = y \<or> fequal x y = fFalse"
-unfolding fFalse_def fTrue_def fequal_def by auto
-
lemma fAll_table:
"Ex (fComp P) \<or> fAll P = fTrue"
"All P \<or> fAll P = fFalse"
@@ -89,6 +85,11 @@
"Ex P \<or> fEx P = fFalse"
unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
+lemma fequal_table:
+"fequal x x = fTrue"
+"x = y \<or> fequal x y = fFalse"
+unfolding fFalse_def fTrue_def fequal_def by auto
+
lemma fNot_law:
"fNot P \<noteq> P"
unfolding fNot_def by auto
@@ -114,12 +115,6 @@
"fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
-lemma fequal_laws:
-"fequal x y = fequal y x"
-"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
-"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
-unfolding fFalse_def fTrue_def fequal_def by auto
-
lemma fAll_law:
"fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
unfolding fNot_def fComp_def fAll_def fEx_def by auto
@@ -128,6 +123,13 @@
"fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
unfolding fNot_def fComp_def fAll_def fEx_def by auto
+lemma fequal_laws:
+"fequal x y = fequal y x"
+"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
+"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
+unfolding fFalse_def fTrue_def fequal_def by auto
+
+
subsection {* Setup *}
ML_file "Tools/ATP/atp_problem_generate.ML"