author nipkow Fri Nov 28 07:41:24 1997 +0100 (1997-11-28) changeset 4321 2a2956ccb86c parent 4320 24d9e6639cd4 child 4322 5f5df208b0e0
 src/HOL/simpdata.ML file | annotate | diff | revisions
```     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
```