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"