diff -r 9b672ea2dfe7 -r afb60b8bf15e src/Provers/quantifier1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Provers/quantifier1.ML Fri Nov 28 07:35:47 1997 +0100 @@ -0,0 +1,116 @@ +(* Title: Provers/quantifier1 + ID: \$Id\$ + Author: Tobias Nipkow + Copyright 1997 TU Munich + +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. + +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 rearrange_all: Sign.sg -> thm list -> term -> thm option + val rearrange_ex: 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; + +val prove_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_all_tac sg (F,all\$Abs(x,T,R))) end) + | rearrange_all _ _ _ = None; + +val prove_ex_tac = rtac iffI 1 THEN + ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE), + rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)]); + +fun rearrange_ex sg _ (F as ex \$ Abs(x,T,P)) = + (case extract P of + None => None + | Some(eq,Q) => + Some(prove_conv prove_ex_tac sg (F,ex \$ Abs(x,T,conj\$eq\$Q)))) + | rearrange_ex _ _ _ = None; + +end;