src/HOL/ATP.thy
 changeset 56946 10d9bd4ea94f parent 54148 c8cc5ab4a863 child 57255 488046fdda59
```     1.1 --- a/src/HOL/ATP.thy	Tue May 13 11:10:22 2014 +0200
1.2 +++ b/src/HOL/ATP.thy	Tue May 13 11:10:23 2014 +0200
1.3 @@ -16,6 +16,7 @@
1.4  ML_file "Tools/ATP/atp_proof.ML"
1.5  ML_file "Tools/ATP/atp_proof_redirect.ML"
1.6
1.7 +
1.8  subsection {* Higher-order reasoning helpers *}
1.9
1.10  definition fFalse :: bool where
1.11 @@ -39,15 +40,15 @@
1.12  definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
1.13  "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
1.14
1.15 -definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
1.16 -"fequal x y \<longleftrightarrow> (x = y)"
1.17 -
1.18  definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
1.19  "fAll P \<longleftrightarrow> All P"
1.20
1.21  definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
1.22  "fEx P \<longleftrightarrow> Ex P"
1.23
1.24 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
1.25 +"fequal x y \<longleftrightarrow> (x = y)"
1.26 +
1.27  lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
1.28  unfolding fFalse_def fTrue_def by simp
1.29
1.30 @@ -74,11 +75,6 @@
1.31  "fimplies fTrue fFalse = fFalse"
1.32  unfolding fFalse_def fTrue_def fimplies_def by auto
1.33
1.34 -lemma fequal_table:
1.35 -"fequal x x = fTrue"
1.36 -"x = y \<or> fequal x y = fFalse"
1.37 -unfolding fFalse_def fTrue_def fequal_def by auto
1.38 -
1.39  lemma fAll_table:
1.40  "Ex (fComp P) \<or> fAll P = fTrue"
1.41  "All P \<or> fAll P = fFalse"
1.42 @@ -89,6 +85,11 @@
1.43  "Ex P \<or> fEx P = fFalse"
1.44  unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
1.45
1.46 +lemma fequal_table:
1.47 +"fequal x x = fTrue"
1.48 +"x = y \<or> fequal x y = fFalse"
1.49 +unfolding fFalse_def fTrue_def fequal_def by auto
1.50 +
1.51  lemma fNot_law:
1.52  "fNot P \<noteq> P"
1.53  unfolding fNot_def by auto
1.54 @@ -114,12 +115,6 @@
1.55  "fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
1.56  unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
1.57
1.58 -lemma fequal_laws:
1.59 -"fequal x y = fequal y x"
1.60 -"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
1.61 -"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
1.62 -unfolding fFalse_def fTrue_def fequal_def by auto
1.63 -
1.64  lemma fAll_law:
1.65  "fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
1.66  unfolding fNot_def fComp_def fAll_def fEx_def by auto
1.67 @@ -128,6 +123,13 @@
1.68  "fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
1.69  unfolding fNot_def fComp_def fAll_def fEx_def by auto
1.70
1.71 +lemma fequal_laws:
1.72 +"fequal x y = fequal y x"
1.73 +"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
1.74 +"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
1.75 +unfolding fFalse_def fTrue_def fequal_def by auto
1.76 +
1.77 +
1.78  subsection {* Setup *}
1.79
1.80  ML_file "Tools/ATP/atp_problem_generate.ML"
```