src/HOL/ATP.thy
changeset 47946 33afcfad3f8d
parent 46320 0b8b73b49848
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/ATP.thy	Mon May 21 10:39:31 2012 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon May 21 10:39:32 2012 +0200
     1.3 @@ -29,6 +29,9 @@
     1.4  definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
     1.5  "fNot P \<longleftrightarrow> \<not> P"
     1.6  
     1.7 +definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
     1.8 +"fComp P = (\<lambda>x. \<not> P x)"
     1.9 +
    1.10  definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.11  "fconj P Q \<longleftrightarrow> P \<and> Q"
    1.12  
    1.13 @@ -47,6 +50,86 @@
    1.14  definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    1.15  "fEx P \<longleftrightarrow> Ex P"
    1.16  
    1.17 +lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
    1.18 +unfolding fFalse_def fTrue_def by simp
    1.19 +
    1.20 +lemma fNot_table:
    1.21 +"fNot fFalse = fTrue"
    1.22 +"fNot fTrue = fFalse"
    1.23 +unfolding fFalse_def fTrue_def fNot_def by auto
    1.24 +
    1.25 +lemma fconj_table:
    1.26 +"fconj fFalse P = fFalse"
    1.27 +"fconj P fFalse = fFalse"
    1.28 +"fconj fTrue fTrue = fTrue"
    1.29 +unfolding fFalse_def fTrue_def fconj_def by auto
    1.30 +
    1.31 +lemma fdisj_table:
    1.32 +"fdisj fTrue P = fTrue"
    1.33 +"fdisj P fTrue = fTrue"
    1.34 +"fdisj fFalse fFalse = fFalse"
    1.35 +unfolding fFalse_def fTrue_def fdisj_def by auto
    1.36 +
    1.37 +lemma fimplies_table:
    1.38 +"fimplies P fTrue = fTrue"
    1.39 +"fimplies fFalse P = fTrue"
    1.40 +"fimplies fTrue fFalse = fFalse"
    1.41 +unfolding fFalse_def fTrue_def fimplies_def by auto
    1.42 +
    1.43 +lemma fequal_table:
    1.44 +"fequal x x = fTrue"
    1.45 +"x = y \<or> fequal x y = fFalse"
    1.46 +unfolding fFalse_def fTrue_def fequal_def by auto
    1.47 +
    1.48 +lemma fAll_table:
    1.49 +"Ex (fComp P) \<or> fAll P = fTrue"
    1.50 +"All P \<or> fAll P = fFalse"
    1.51 +unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
    1.52 +
    1.53 +lemma fEx_table:
    1.54 +"All (fComp P) \<or> fEx P = fTrue"
    1.55 +"Ex P \<or> fEx P = fFalse"
    1.56 +unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
    1.57 +
    1.58 +lemma fNot_law:
    1.59 +"fNot P \<noteq> P"
    1.60 +unfolding fNot_def by auto
    1.61 +
    1.62 +lemma fComp_law:
    1.63 +"fComp P x \<longleftrightarrow> \<not> P x"
    1.64 +unfolding fComp_def ..
    1.65 +
    1.66 +lemma fconj_laws:
    1.67 +"fconj P P \<longleftrightarrow> P"
    1.68 +"fconj P Q \<longleftrightarrow> fconj Q P"
    1.69 +"fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)"
    1.70 +unfolding fNot_def fconj_def fdisj_def by auto
    1.71 +
    1.72 +lemma fdisj_laws:
    1.73 +"fdisj P P \<longleftrightarrow> P"
    1.74 +"fdisj P Q \<longleftrightarrow> fdisj Q P"
    1.75 +"fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)"
    1.76 +unfolding fNot_def fconj_def fdisj_def by auto
    1.77 +
    1.78 +lemma fimplies_laws:
    1.79 +"fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
    1.80 +"fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
    1.81 +unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
    1.82 +
    1.83 +lemma fequal_laws:
    1.84 +"fequal x y = fequal y x"
    1.85 +"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
    1.86 +"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
    1.87 +unfolding fFalse_def fTrue_def fequal_def by auto
    1.88 +
    1.89 +lemma fAll_law:
    1.90 +"fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
    1.91 +unfolding fNot_def fComp_def fAll_def fEx_def by auto
    1.92 +
    1.93 +lemma fEx_law:
    1.94 +"fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
    1.95 +unfolding fNot_def fComp_def fAll_def fEx_def by auto
    1.96 +
    1.97  subsection {* Setup *}
    1.98  
    1.99  use "Tools/ATP/atp_problem_generate.ML"