src/HOL/simpdata.ML
changeset 4320 24d9e6639cd4
parent 4205 96632970d203
child 4321 2a2956ccb86c
     1.1 --- a/src/HOL/simpdata.ML	Fri Nov 28 07:35:47 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Nov 28 07:37:06 1997 +0100
     1.3 @@ -52,6 +52,31 @@
     1.4  val DelIffs = seq delIff
     1.5  end;
     1.6  
     1.7 +(** instantiate generic simp procs for `quantifier elimination': **)
     1.8 +structure Quantifier1 = Quantifier1Fun(
     1.9 +struct
    1.10 +  (*abstract syntax*)
    1.11 +  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
    1.12 +    | dest_eq _ = None;
    1.13 +  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
    1.14 +    | dest_conj _ = None;
    1.15 +  val conj = HOLogic.conj
    1.16 +  val imp  = HOLogic.imp
    1.17 +  (*rules*)
    1.18 +  val iff_reflection = eq_reflection
    1.19 +  val iffI = iffI
    1.20 +  val sym  = sym
    1.21 +  val conjI= conjI
    1.22 +  val conjE= conjE
    1.23 +  val impI = impI
    1.24 +  val impE = impE
    1.25 +  val mp   = mp
    1.26 +  val exI  = exI
    1.27 +  val exE  = exE
    1.28 +  val allI = allI
    1.29 +  val allE = allE
    1.30 +end);
    1.31 +
    1.32  
    1.33  local
    1.34  
    1.35 @@ -160,7 +185,6 @@
    1.36  NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"
    1.37     "!x. x=t --> P(x)" and "!x. t=x --> P(x)"
    1.38     must be taken care of by ordinary rewrite rules.
    1.39 -***)
    1.40  
    1.41  local
    1.42  
    1.43 @@ -227,6 +251,9 @@
    1.44  val defEX_regroup = mk_simproc "defined EX" [ex_pattern] rearrange_ex;
    1.45  val defALL_regroup = mk_simproc "defined ALL" [all_pattern] rearrange_all;
    1.46  end;
    1.47 +***)
    1.48 +
    1.49 +
    1.50  
    1.51  
    1.52  (* elimination of existential quantifiers in assumptions *)
    1.53 @@ -355,7 +382,20 @@
    1.54                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.55                     (fn _ => [rtac expand_if 1]);
    1.56  
    1.57 +(** make simp procs for quantifier elimination **)
    1.58 +local
    1.59 +val ex_pattern =
    1.60 +  read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
    1.61  
    1.62 +val all_pattern =
    1.63 +  read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.64 +
    1.65 +in
    1.66 +val defEX_regroup =
    1.67 +  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
    1.68 +val defALL_regroup =
    1.69 +  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
    1.70 +end;
    1.71  
    1.72  (** Case splitting **)
    1.73