Tidying and some comments
authorpaulson
Wed Dec 03 10:50:02 1997 +0100 (1997-12-03)
changeset 435136b28f78ed1b
parent 4350 1983e4054fd8
child 4352 7ac9f3e8a97d
Tidying and some comments
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Wed Dec 03 10:49:33 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Dec 03 10:50:02 1997 +0100
     1.3 @@ -52,32 +52,6 @@
     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    fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
    1.36 @@ -135,13 +109,17 @@
    1.37     "(P | ~P) = True",    "(~P | P) = True",
    1.38     "((~P) = (~Q)) = (P=Q)",
    1.39     "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", 
    1.40 -   "(? x. x=t & P(x)) = P(t)",
    1.41 -   "(! x. t=x --> P(x)) = P(t)" ];
    1.42 +(*two needed for the one-point-rule quantifier simplification procs*)
    1.43 +   "(? x. x=t & P(x)) = P(t)",		(*essential for termination!!*)
    1.44 +   "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)
    1.45  
    1.46  (*Add congruence rules for = (instead of ==) *)
    1.47  infix 4 addcongs delcongs;
    1.48 -fun ss addcongs congs = ss addeqcongs (map standard (congs RL [eq_reflection]));
    1.49 -fun ss delcongs congs = ss deleqcongs (map standard (congs RL [eq_reflection]));
    1.50 +fun ss addcongs congs = ss addeqcongs 
    1.51 +                        (map standard (congs RL [eq_reflection]));
    1.52 +
    1.53 +fun ss delcongs congs = ss deleqcongs 
    1.54 +                        (map standard (congs RL [eq_reflection]));
    1.55  
    1.56  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    1.57  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    1.58 @@ -297,13 +275,39 @@
    1.59                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.60                     (fn _ => [rtac expand_if 1]);
    1.61  
    1.62 -(** make simp procs for quantifier elimination **)
    1.63 +
    1.64 +(*** make simplification procedures for quantifier elimination ***)
    1.65 +
    1.66 +structure Quantifier1 = Quantifier1Fun(
    1.67 +struct
    1.68 +  (*abstract syntax*)
    1.69 +  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
    1.70 +    | dest_eq _ = None;
    1.71 +  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
    1.72 +    | dest_conj _ = None;
    1.73 +  val conj = HOLogic.conj
    1.74 +  val imp  = HOLogic.imp
    1.75 +  (*rules*)
    1.76 +  val iff_reflection = eq_reflection
    1.77 +  val iffI = iffI
    1.78 +  val sym  = sym
    1.79 +  val conjI= conjI
    1.80 +  val conjE= conjE
    1.81 +  val impI = impI
    1.82 +  val impE = impE
    1.83 +  val mp   = mp
    1.84 +  val exI  = exI
    1.85 +  val exE  = exE
    1.86 +  val allI = allI
    1.87 +  val allE = allE
    1.88 +end);
    1.89 +
    1.90  local
    1.91  val ex_pattern =
    1.92 -  read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
    1.93 +  read_cterm (sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
    1.94  
    1.95  val all_pattern =
    1.96 -  read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.97 +  read_cterm (sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.98  
    1.99  in
   1.100  val defEX_regroup =
   1.101 @@ -312,7 +316,8 @@
   1.102    mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
   1.103  end;
   1.104  
   1.105 -(** Case splitting **)
   1.106 +
   1.107 +(*** Case splitting ***)
   1.108  
   1.109  local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
   1.110  in