src/Provers/quantifier1.ML
 author nipkow Fri, 23 Mar 2001 10:12:12 +0100 changeset 11221 60c6e91f6079 parent 7951 b36913c35699 child 11232 558a4feebb04 permissions -rw-r--r--
```
(*  Title:      Provers/quantifier1
ID:         \$Id\$
Author:     Tobias Nipkow

Simplification procedures for turning

? x. ... & x = t & ...
into   ? x. x = t & ... & ...
where the `? x. x = t &' in the latter formula is eliminated
by ordinary simplification.

and   ! x. (... & x = t & ...) --> P x
into  ! x. x = t --> (... & ...) --> P x
where the `!x. x=t -->' in the latter formula is eliminated
by ordinary simplification.

NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
"!x. x=t --> P(x)" is covered by the congreunce rule for -->;
"!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.

And similarly for the bounded quantifiers.

Gries etc call this the "1 point rules"
*)

signature QUANTIFIER1_DATA =
sig
(*abstract syntax*)
val dest_eq: term -> (term*term*term)option
val dest_conj: term -> (term*term*term)option
val conj: term
val imp:  term
(*rules*)
val iff_reflection: thm (* P <-> Q ==> P == Q *)
val iffI:  thm
val sym:   thm
val conjI: thm
val conjE: thm
val impI:  thm
val impE:  thm
val mp:    thm
val exI:   thm
val exE:   thm
val allI:  thm
val allE:  thm
end;

signature QUANTIFIER1 =
sig
val prove_one_point_all_tac: tactic
val prove_one_point_ex_tac: tactic
val rearrange_all: Sign.sg -> thm list -> term -> thm option
val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
val rearrange_ball: tactic -> Sign.sg -> thm list -> term -> thm option
val rearrange_bex:  tactic -> Sign.sg -> thm list -> term -> thm option
end;

functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
struct

open Data;

fun def eq = case dest_eq eq of
Some(c,s,t) =>
if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c\$t\$s)
else None
| None => None;

fun extract conj = case dest_conj conj of
Some(conj,P,Q) =>
(case def P of
Some eq => Some(eq,Q)
| None =>
(case def Q of
Some eq => Some(eq,P)
| None =>
(case extract P of
Some(eq,P') => Some(eq, conj \$ P' \$ Q)
| None =>
(case extract Q of
Some(eq,Q') => Some(eq,conj \$ P \$ Q')
| None => None))))
| None => None;

fun prove_conv tac sg tu =
let val meta_eq = cterm_of sg (Logic.mk_equals tu)
in prove_goalw_cterm [] meta_eq (K [rtac iff_reflection 1, tac])
handle ERROR =>
error("The error(s) above occurred while trying to prove " ^
string_of_cterm meta_eq)
end;

(* Proves (? x. ... & x = t & ...) = (? x. x = t & ... & ...)
Better: instantiate exI
*)
val prove_one_point_ex_tac = rtac iffI 1 THEN
ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);

(* Proves (! x. (... & x = t & ...) --> P x) =
(! x. x = t --> (... & ...) --> P x)
*)
val prove_one_point_all_tac = EVERY1[rtac iffI,
rtac allI, etac allE, rtac impI, rtac impI, etac mp,
REPEAT o (etac conjE),
REPEAT o (ares_tac [conjI] ORELSE' etac sym),
rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
etac impE, atac ORELSE' etac sym, etac mp,
REPEAT o (ares_tac [conjI])];

fun rearrange_all sg _ (F as all \$ Abs(x,T,(* --> *)_ \$ P \$ Q)) =
(case extract P of
None => None
| Some(eq,P') =>
let val R = imp \$ eq \$ (imp \$ P' \$ Q)
in Some(prove_conv prove_one_point_all_tac sg (F,all\$Abs(x,T,R))) end)
| rearrange_all _ _ _ = None;

fun rearrange_ball tac sg _ (F as Ball \$ A \$ Abs(x,T,(* --> *)_ \$ P \$ Q)) =
(case extract P of
None => None
| Some(eq,P') =>
let val R = imp \$ eq \$ (imp \$ P' \$ Q)
in Some(prove_conv tac sg (F,Ball \$ A \$ Abs(x,T,R))) end)
| rearrange_ball _ _ _ _ = None;

fun rearrange_ex sg _ (F as ex \$ Abs(x,T,P)) =
(case extract P of
None => None
| Some(eq,Q) =>
Some(prove_conv prove_one_point_ex_tac sg (F,ex \$ Abs(x,T,conj\$eq\$Q))))
| rearrange_ex _ _ _ = None;

fun rearrange_bex tac sg _ (F as Bex \$ A \$ Abs(x,T,P)) =
(case extract P of
None => None
| Some(eq,Q) =>
Some(prove_conv tac sg (F,Bex \$ A \$ Abs(x,T,conj\$eq\$Q))))
| rearrange_bex _ _ _ _ = None;

end;
```