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 

11221

22 
And similarly for the bounded quantifiers.


23 

4319

24 
Gries etc call this the "1 point rules"


25 
*)


26 


27 
signature QUANTIFIER1_DATA =


28 
sig


29 
(*abstract syntax*)


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


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


32 
val conj: term


33 
val imp: term


34 
(*rules*)


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


36 
val iffI: thm


37 
val sym: thm


38 
val conjI: thm


39 
val conjE: thm


40 
val impI: thm


41 
val impE: thm


42 
val mp: thm


43 
val exI: thm


44 
val exE: thm


45 
val allI: thm


46 
val allE: thm


47 
end;


48 


49 
signature QUANTIFIER1 =


50 
sig

11221

51 
val prove_one_point_all_tac: tactic


52 
val prove_one_point_ex_tac: tactic

4319

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


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

11221

55 
val rearrange_ball: tactic > Sign.sg > thm list > term > thm option


56 
val rearrange_bex: tactic > Sign.sg > thm list > term > thm option

4319

57 
end;


58 


59 
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =


60 
struct


61 


62 
open Data;


63 


64 
fun def eq = case dest_eq eq of


65 
Some(c,s,t) =>


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


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


68 
else None


69 
 None => None;


70 


71 
fun extract conj = case dest_conj conj of


72 
Some(conj,P,Q) =>


73 
(case def P of


74 
Some eq => Some(eq,Q)


75 
 None =>


76 
(case def Q of


77 
Some eq => Some(eq,P)


78 
 None =>


79 
(case extract P of


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


81 
 None =>


82 
(case extract Q of


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


84 
 None => None))))


85 
 None => None;


86 


87 
fun prove_conv tac sg tu =


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


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


90 
handle ERROR =>


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


92 
string_of_cterm meta_eq)


93 
end;


94 

11221

95 
(* Proves (? x. ... & x = t & ...) = (? x. x = t & ... & ...)


96 
Better: instantiate exI


97 
*)


98 
val prove_one_point_ex_tac = rtac iffI 1 THEN


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


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


101 


102 
(* Proves (! x. (... & x = t & ...) > P x) =


103 
(! x. x = t > (... & ...) > P x)


104 
*)


105 
val prove_one_point_all_tac = EVERY1[rtac iffI,

4319

106 
rtac allI, etac allE, rtac impI, rtac impI, etac mp,


107 
REPEAT o (etac conjE),


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


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


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


111 
REPEAT o (ares_tac [conjI])];


112 


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


114 
(case extract P of


115 
None => None


116 
 Some(eq,P') =>


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

11221

118 
in Some(prove_conv prove_one_point_all_tac sg (F,all$Abs(x,T,R))) end)

4319

119 
 rearrange_all _ _ _ = None;


120 

11221

121 
fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,(* > *)_ $ P $ Q)) =


122 
(case extract P of


123 
None => None


124 
 Some(eq,P') =>


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


126 
in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)


127 
 rearrange_ball _ _ _ _ = None;

4319

128 


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


130 
(case extract P of


131 
None => None


132 
 Some(eq,Q) =>

11221

133 
Some(prove_conv prove_one_point_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))

4319

134 
 rearrange_ex _ _ _ = None;


135 

11221

136 
fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =


137 
(case extract P of


138 
None => None


139 
 Some(eq,Q) =>


140 
Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))


141 
 rearrange_bex _ _ _ _ = None;


142 

4319

143 
end;
