Removed dead code.
authornipkow
Fri Nov 28 07:41:24 1997 +0100 (1997-11-28)
changeset 43212a2956ccb86c
parent 4320 24d9e6639cd4
child 4322 5f5df208b0e0
Removed dead code.
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Fri Nov 28 07:37:06 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Nov 28 07:41:24 1997 +0100
     1.3 @@ -170,91 +170,6 @@
     1.4                   "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
     1.5                   "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];
     1.6  
     1.7 -(*** Simplification procedures for turning
     1.8 -
     1.9 -            ? x. ... & x = t & ...
    1.10 -     into   ? x. x = t & ... & ...
    1.11 -     where the `? x. x = t &' in the latter formula is eliminated
    1.12 -           by ordinary simplification. 
    1.13 -
    1.14 -     and   ! x. (... & x = t & ...) --> P x
    1.15 -     into  ! x. x = t --> (... & ...) --> P x
    1.16 -     where the `!x. x=t -->' in the latter formula is eliminated
    1.17 -           by ordinary simplification.
    1.18 -
    1.19 -NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"
    1.20 -   "!x. x=t --> P(x)" and "!x. t=x --> P(x)"
    1.21 -   must be taken care of by ordinary rewrite rules.
    1.22 -
    1.23 -local
    1.24 -
    1.25 -fun def(eq as (c as Const("op =",_)) $ s $ t) =
    1.26 -      if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
    1.27 -      if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c$t$s)
    1.28 -      else None
    1.29 -  | def _ = None;
    1.30 -
    1.31 -fun extract(Const("op &",_) $ P $ Q) =
    1.32 -      (case def P of
    1.33 -         Some eq => Some(eq,Q)
    1.34 -       | None => (case def Q of
    1.35 -                   Some eq => Some(eq,P)
    1.36 -                 | None =>
    1.37 -       (case extract P of
    1.38 -         Some(eq,P') => Some(eq, HOLogic.conj $ P' $ Q)
    1.39 -       | None => (case extract Q of
    1.40 -                   Some(eq,Q') => Some(eq,HOLogic.conj $ P $ Q')
    1.41 -                 | None => None))))
    1.42 -  | extract _ = None;
    1.43 -
    1.44 -fun prove_ex_eq(ceqt) =
    1.45 -  let val tac = rtac eq_reflection 1 THEN rtac iffI 1 THEN
    1.46 -                ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
    1.47 -                 rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
    1.48 -  in rule_by_tactic tac (trivial ceqt) end;
    1.49 -
    1.50 -fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
    1.51 -     (case extract P of
    1.52 -        None => None
    1.53 -      | Some(eq,Q) =>
    1.54 -          let val ceqt = cterm_of sg
    1.55 -                       (Logic.mk_equals(F,ex $ Abs(x,T,HOLogic.conj$eq$Q)))
    1.56 -          in Some(prove_ex_eq ceqt) end)
    1.57 -  | rearrange_ex _ _ _ = None;
    1.58 -
    1.59 -val ex_pattern =
    1.60 -  read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
    1.61 -
    1.62 -fun prove_all_eq(ceqt) =
    1.63 -  let fun tac _ = [EVERY1[rtac eq_reflection, rtac iffI,
    1.64 -                       rtac allI, etac allE, rtac impI, rtac impI, etac mp,
    1.65 -                          REPEAT o (etac conjE),
    1.66 -                          REPEAT o (ares_tac [conjI] ORELSE' etac sym),
    1.67 -                       rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
    1.68 -                          etac impE, atac ORELSE' etac sym, etac mp,
    1.69 -                          REPEAT o (ares_tac [conjI])]]
    1.70 -  in prove_goalw_cterm [] ceqt tac end;
    1.71 -
    1.72 -fun rearrange_all sg _ (F as all $ Abs(x,T,Const("op -->",_)$P$Q)) =
    1.73 -     (case extract P of
    1.74 -        None => None
    1.75 -      | Some(eq,P') =>
    1.76 -          let val R = HOLogic.imp $ eq $ (HOLogic.imp $ P' $ Q)
    1.77 -              val ceqt = cterm_of sg (Logic.mk_equals(F,all$Abs(x,T,R)))
    1.78 -          in Some(prove_all_eq ceqt) end)
    1.79 -  | rearrange_all _ _ _ = None;
    1.80 -
    1.81 -val all_pattern =
    1.82 -  read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.83 -
    1.84 -in
    1.85 -val defEX_regroup = mk_simproc "defined EX" [ex_pattern] rearrange_ex;
    1.86 -val defALL_regroup = mk_simproc "defined ALL" [all_pattern] rearrange_all;
    1.87 -end;
    1.88 -***)
    1.89 -
    1.90 -
    1.91 -
    1.92  
    1.93  (* elimination of existential quantifiers in assumptions *)
    1.94