# HG changeset patch # User wenzelm # Date 1206567601 -3600 # Node ID cd74690f3bfbe6139c81f10b14b8e1300a0c89f1 # Parent 40932ee97ff83716330c0ce2311cbe738ba32381 pass imp_elim, swap to classical prover; diff -r 40932ee97ff8 -r cd74690f3bfb src/FOL/FOL.thy --- a/src/FOL/FOL.thy Wed Mar 26 22:39:58 2008 +0100 +++ b/src/FOL/FOL.thy Wed Mar 26 22:40:01 2008 +0100 @@ -163,6 +163,12 @@ qed qed +lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R" + by (rule classical) iprover + +lemma swap: "~ P ==> (~ R ==> P) ==> R" + by (rule classical) iprover + use "cladata.ML" setup Cla.setup setup cla_setup diff -r 40932ee97ff8 -r cd74690f3bfb src/FOL/cladata.ML --- a/src/FOL/cladata.ML Wed Mar 26 22:39:58 2008 +0100 +++ b/src/FOL/cladata.ML Wed Mar 26 22:40:01 2008 +0100 @@ -10,13 +10,14 @@ (*** Applying ClassicalFun to create a classical prover ***) structure Classical_Data = - struct - val mp = @{thm mp} +struct + val imp_elim = @{thm imp_elim} val not_elim = @{thm notE} + val swap = @{thm swap} val classical = @{thm classical} val sizef = size_of_thm val hyp_subst_tacs=[hyp_subst_tac] - end; +end; structure Cla = ClassicalFun(Classical_Data); structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; diff -r 40932ee97ff8 -r cd74690f3bfb src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Mar 26 22:39:58 2008 +0100 +++ b/src/HOL/HOL.thy Wed Mar 26 22:40:01 2008 +0100 @@ -883,6 +883,12 @@ subsubsection {* Classical Reasoner setup *} +lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R" + by (rule classical) iprover + +lemma swap: "~ P ==> (~ R ==> P) ==> R" + by (rule classical) iprover + lemma thin_refl: "\X. \ x=x; PROP W \ \ PROP W" . @@ -893,21 +899,22 @@ val dest_eq = HOLogic.dest_eq val dest_Trueprop = HOLogic.dest_Trueprop val dest_imp = HOLogic.dest_imp - val eq_reflection = @{thm HOL.eq_reflection} - val rev_eq_reflection = @{thm HOL.meta_eq_to_obj_eq} - val imp_intr = @{thm HOL.impI} - val rev_mp = @{thm HOL.rev_mp} - val subst = @{thm HOL.subst} - val sym = @{thm HOL.sym} + val eq_reflection = @{thm eq_reflection} + val rev_eq_reflection = @{thm meta_eq_to_obj_eq} + val imp_intr = @{thm impI} + val rev_mp = @{thm rev_mp} + val subst = @{thm subst} + val sym = @{thm sym} val thin_refl = @{thm thin_refl}; end); open Hypsubst; structure Classical = ClassicalFun( struct - val mp = @{thm HOL.mp} - val not_elim = @{thm HOL.notE} - val classical = @{thm HOL.classical} + val imp_elim = @{thm imp_elim} + val not_elim = @{thm notE} + val swap = @{thm swap} + val classical = @{thm classical} val sizef = Drule.size_of_thm val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] end); @@ -996,8 +1003,8 @@ type claset = Classical.claset val equality_name = @{const_name "op ="} val not_name = @{const_name Not} - val notE = @{thm HOL.notE} - val ccontr = @{thm HOL.ccontr} + val notE = @{thm notE} + val ccontr = @{thm ccontr} val contr_tac = Classical.contr_tac val dup_intr = Classical.dup_intr val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac