Moved the quantifier elimination simp procs into Provers.
authornipkow
Fri Nov 28 07:37:06 1997 +0100 (1997-11-28)
changeset 432024d9e6639cd4
parent 4319 afb60b8bf15e
child 4321 2a2956ccb86c
Moved the quantifier elimination simp procs into Provers.
src/HOL/ROOT.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/ROOT.ML	Fri Nov 28 07:35:47 1997 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Fri Nov 28 07:37:06 1997 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4  use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
     1.5  use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
     1.6  use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
     1.7 +use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
     1.8  
     1.9  use "thy_data.ML";
    1.10  
     2.1 --- a/src/HOL/simpdata.ML	Fri Nov 28 07:35:47 1997 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Fri Nov 28 07:37:06 1997 +0100
     2.3 @@ -52,6 +52,31 @@
     2.4  val DelIffs = seq delIff
     2.5  end;
     2.6  
     2.7 +(** instantiate generic simp procs for `quantifier elimination': **)
     2.8 +structure Quantifier1 = Quantifier1Fun(
     2.9 +struct
    2.10 +  (*abstract syntax*)
    2.11 +  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
    2.12 +    | dest_eq _ = None;
    2.13 +  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
    2.14 +    | dest_conj _ = None;
    2.15 +  val conj = HOLogic.conj
    2.16 +  val imp  = HOLogic.imp
    2.17 +  (*rules*)
    2.18 +  val iff_reflection = eq_reflection
    2.19 +  val iffI = iffI
    2.20 +  val sym  = sym
    2.21 +  val conjI= conjI
    2.22 +  val conjE= conjE
    2.23 +  val impI = impI
    2.24 +  val impE = impE
    2.25 +  val mp   = mp
    2.26 +  val exI  = exI
    2.27 +  val exE  = exE
    2.28 +  val allI = allI
    2.29 +  val allE = allE
    2.30 +end);
    2.31 +
    2.32  
    2.33  local
    2.34  
    2.35 @@ -160,7 +185,6 @@
    2.36  NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"
    2.37     "!x. x=t --> P(x)" and "!x. t=x --> P(x)"
    2.38     must be taken care of by ordinary rewrite rules.
    2.39 -***)
    2.40  
    2.41  local
    2.42  
    2.43 @@ -227,6 +251,9 @@
    2.44  val defEX_regroup = mk_simproc "defined EX" [ex_pattern] rearrange_ex;
    2.45  val defALL_regroup = mk_simproc "defined ALL" [all_pattern] rearrange_all;
    2.46  end;
    2.47 +***)
    2.48 +
    2.49 +
    2.50  
    2.51  
    2.52  (* elimination of existential quantifiers in assumptions *)
    2.53 @@ -355,7 +382,20 @@
    2.54                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    2.55                     (fn _ => [rtac expand_if 1]);
    2.56  
    2.57 +(** make simp procs for quantifier elimination **)
    2.58 +local
    2.59 +val ex_pattern =
    2.60 +  read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
    2.61  
    2.62 +val all_pattern =
    2.63 +  read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    2.64 +
    2.65 +in
    2.66 +val defEX_regroup =
    2.67 +  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
    2.68 +val defALL_regroup =
    2.69 +  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
    2.70 +end;
    2.71  
    2.72  (** Case splitting **)
    2.73