src/HOL/ATP.thy
changeset 58406 539cc471186f
parent 58142 d6a2e3567f95
child 58407 111d801b5d5d
     1.1 --- a/src/HOL/ATP.thy	Sat Sep 20 10:44:23 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Sat Sep 20 10:44:24 2014 +0200
     1.3 @@ -133,10 +133,15 @@
     1.4  
     1.5  subsection {* Waldmeister helpers *}
     1.6  
     1.7 -(* Has all needed simplification lemmas for logic.
     1.8 -   "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
     1.9 -lemmas waldmeister_fol = simp_thms(1,2,4-8,11-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
    1.10 -  eq_ac disj_comms disj_assoc conj_comms conj_assoc
    1.11 +(* Has all needed simplification lemmas for logic. *)
    1.12 +lemma boolean_equality: "(P \<longleftrightarrow> P) = True"
    1.13 +  by simp
    1.14 +
    1.15 +lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)"
    1.16 +  by metis
    1.17 +
    1.18 +lemmas waldmeister_fol = boolean_equality boolean_comm
    1.19 +  simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc
    1.20  
    1.21  
    1.22  subsection {* Basic connection between ATPs and HOL *}
    1.23 @@ -148,6 +153,6 @@
    1.24  ML_file "Tools/ATP/atp_systems.ML"
    1.25  ML_file "Tools/ATP/atp_waldmeister.ML"
    1.26  
    1.27 -hide_fact (open) waldmeister_fol
    1.28 +hide_fact (open) waldmeister_fol boolean_equality boolean_comm
    1.29  
    1.30  end