4319

1 
(* Title: Provers/quantifier1


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1997 TU Munich


5 


6 
Simplification procedures for turning


7 


8 
? x. ... & x = t & ...


9 
into ? x. x = t & ... & ...


10 
where the `? x. x = t &' in the latter formula is eliminated


11 
by ordinary simplification.


12 


13 
and ! x. (... & x = t & ...) > P x


14 
into ! x. x = t > (... & ...) > P x


15 
where the `!x. x=t >' in the latter formula is eliminated


16 
by ordinary simplification.


17 


18 
NB Simproc is only triggered by "!x. P(x) & P'(x) > Q(x)";


19 
"!x. x=t > P(x)" is covered by the congreunce rule for >;


20 
"!x. t=x > P(x)" must be taken care of by an ordinary rewrite rule.


21 


22 
Gries etc call this the "1 point rules"


23 
*)


24 


25 
signature QUANTIFIER1_DATA =


26 
sig


27 
(*abstract syntax*)


28 
val dest_eq: term > (term*term*term)option


29 
val dest_conj: term > (term*term*term)option


30 
val conj: term


31 
val imp: term


32 
(*rules*)


33 
val iff_reflection: thm (* P <> Q ==> P == Q *)


34 
val iffI: thm


35 
val sym: thm


36 
val conjI: thm


37 
val conjE: thm


38 
val impI: thm


39 
val impE: thm


40 
val mp: thm


41 
val exI: thm


42 
val exE: thm


43 
val allI: thm


44 
val allE: thm


45 
end;


46 


47 
signature QUANTIFIER1 =


48 
sig


49 
val rearrange_all: Sign.sg > thm list > term > thm option


50 
val rearrange_ex: Sign.sg > thm list > term > thm option


51 
end;


52 


53 
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =


54 
struct


55 


56 
open Data;


57 


58 
fun def eq = case dest_eq eq of


59 
Some(c,s,t) =>


60 
if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else


61 
if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c$t$s)


62 
else None


63 
 None => None;


64 


65 
fun extract conj = case dest_conj conj of


66 
Some(conj,P,Q) =>


67 
(case def P of


68 
Some eq => Some(eq,Q)


69 
 None =>


70 
(case def Q of


71 
Some eq => Some(eq,P)


72 
 None =>


73 
(case extract P of


74 
Some(eq,P') => Some(eq, conj $ P' $ Q)


75 
 None =>


76 
(case extract Q of


77 
Some(eq,Q') => Some(eq,conj $ P $ Q')


78 
 None => None))))


79 
 None => None;


80 


81 
fun prove_conv tac sg tu =


82 
let val meta_eq = cterm_of sg (Logic.mk_equals tu)


83 
in prove_goalw_cterm [] meta_eq (K [rtac iff_reflection 1, tac])


84 
handle ERROR =>


85 
error("The error(s) above occurred while trying to prove " ^


86 
string_of_cterm meta_eq)


87 
end;


88 


89 
val prove_all_tac = EVERY1[rtac iffI,


90 
rtac allI, etac allE, rtac impI, rtac impI, etac mp,


91 
REPEAT o (etac conjE),


92 
REPEAT o (ares_tac [conjI] ORELSE' etac sym),


93 
rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),


94 
etac impE, atac ORELSE' etac sym, etac mp,


95 
REPEAT o (ares_tac [conjI])];


96 


97 
fun rearrange_all sg _ (F as all $ Abs(x,T,(* > *)_ $ P $ Q)) =


98 
(case extract P of


99 
None => None


100 
 Some(eq,P') =>


101 
let val R = imp $ eq $ (imp $ P' $ Q)


102 
in Some(prove_conv prove_all_tac sg (F,all$Abs(x,T,R))) end)


103 
 rearrange_all _ _ _ = None;


104 

7951

105 
(* Better: instantiate exI *)

4319

106 
val prove_ex_tac = rtac iffI 1 THEN

7951

107 
ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,


108 
DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);

4319

109 


110 
fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =


111 
(case extract P of


112 
None => None


113 
 Some(eq,Q) =>


114 
Some(prove_conv prove_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))


115 
 rearrange_ex _ _ _ = None;


116 


117 
end;
