# HG changeset patch # User nipkow # Date 880699026 -3600 # Node ID 24d9e6639cd4bf080f311d4d3e35d7b8b4421198 # Parent afb60b8bf15e2f5bc8a1d8e50c3c900ef23c18ec Moved the quantifier elimination simp procs into Provers. diff -r afb60b8bf15e -r 24d9e6639cd4 src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Fri Nov 28 07:35:47 1997 +0100 +++ b/src/HOL/ROOT.ML Fri Nov 28 07:37:06 1997 +0100 @@ -24,6 +24,7 @@ use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML"; use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML"; use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML"; +use "$ISABELLE_HOME/src/Provers/quantifier1.ML"; use "thy_data.ML"; diff -r afb60b8bf15e -r 24d9e6639cd4 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Fri Nov 28 07:35:47 1997 +0100 +++ b/src/HOL/simpdata.ML Fri Nov 28 07:37:06 1997 +0100 @@ -52,6 +52,31 @@ val DelIffs = seq delIff end; +(** instantiate generic simp procs for `quantifier elimination': **) +structure Quantifier1 = Quantifier1Fun( +struct + (*abstract syntax*) + fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t) + | dest_eq _ = None; + fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t) + | dest_conj _ = None; + val conj = HOLogic.conj + val imp = HOLogic.imp + (*rules*) + val iff_reflection = eq_reflection + val iffI = iffI + val sym = sym + val conjI= conjI + val conjE= conjE + val impI = impI + val impE = impE + val mp = mp + val exI = exI + val exE = exE + val allI = allI + val allE = allE +end); + local @@ -160,7 +185,6 @@ NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)" "!x. x=t --> P(x)" and "!x. t=x --> P(x)" must be taken care of by ordinary rewrite rules. -***) local @@ -227,6 +251,9 @@ val defEX_regroup = mk_simproc "defined EX" [ex_pattern] rearrange_ex; val defALL_regroup = mk_simproc "defined ALL" [all_pattern] rearrange_all; end; +***) + + (* elimination of existential quantifiers in assumptions *) @@ -355,7 +382,20 @@ "(if P then Q else R) = ((P-->Q) & (~P-->R))" (fn _ => [rtac expand_if 1]); +(** make simp procs for quantifier elimination **) +local +val ex_pattern = + read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT) +val all_pattern = + read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT) + +in +val defEX_regroup = + mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex; +val defALL_regroup = + mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all; +end; (** Case splitting **)