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 & ... & ...

11232

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

4319

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 

11232

18 
And analogously for t=x, but the eqn is not turned around!


19 

4319

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


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


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

11232

23 
As must be "? x. t=x & P(x)".

4319

24 

11232

25 

11221

26 
And similarly for the bounded quantifiers.


27 

4319

28 
Gries etc call this the "1 point rules"


29 
*)


30 


31 
signature QUANTIFIER1_DATA =


32 
sig


33 
(*abstract syntax*)


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


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

11232

36 
val dest_imp: term > (term*term*term)option

4319

37 
val conj: term


38 
val imp: term


39 
(*rules*)


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


41 
val iffI: thm


42 
val conjI: thm


43 
val conjE: thm


44 
val impI: thm


45 
val mp: thm


46 
val exI: thm


47 
val exE: thm

11232

48 
val uncurry: thm (* P > Q > R ==> P & Q > R *)


49 
val iff_allI: thm (* !!x. P x <> Q x ==> (!x. P x) = (!x. Q x) *)

4319

50 
end;


51 


52 
signature QUANTIFIER1 =


53 
sig

11221

54 
val prove_one_point_all_tac: tactic


55 
val prove_one_point_ex_tac: tactic

4319

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


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

11221

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


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

4319

60 
end;


61 


62 
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =


63 
struct


64 


65 
open Data;


66 

11232

67 
(* FIXME: only test! *)

4319

68 
fun def eq = case dest_eq eq of


69 
Some(c,s,t) =>

11232

70 
s = Bound 0 andalso not(loose_bvar1(t,0)) orelse


71 
t = Bound 0 andalso not(loose_bvar1(s,0))


72 
 None => false;

4319

73 

11232

74 
fun extract_conj t = case dest_conj t of None => None


75 
 Some(conj,P,Q) =>


76 
(if def P then Some(P,Q) else


77 
if def Q then Some(Q,P) else


78 
(case extract_conj P of


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


80 
 None => (case extract_conj Q of


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


82 
 None => None)));


83 


84 
fun extract_imp t = case dest_imp t of None => None


85 
 Some(imp,P,Q) => if def P then Some(P,Q)


86 
else (case extract_conj P of


87 
Some(eq,P') => Some(eq, imp $ P' $ Q)


88 
 None => (case extract_imp Q of


89 
None => None


90 
 Some(eq,Q') => Some(eq, imp$P$Q')));


91 

4319

92 


93 
fun prove_conv tac sg tu =


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


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


96 
handle ERROR =>


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


98 
string_of_cterm meta_eq)


99 
end;


100 

11221

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


102 
Better: instantiate exI


103 
*)


104 
val prove_one_point_ex_tac = rtac iffI 1 THEN


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

11232

106 
DEPTH_SOLVE_1 o (ares_tac [conjI])]);

11221

107 


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


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


110 
*)

11232

111 
local


112 
val tac = SELECT_GOAL


113 
(EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,


114 
REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])


115 
in


116 
val prove_one_point_all_tac = EVERY1[rtac iff_allI, rtac iffI, tac, tac]


117 
end

4319

118 

11232

119 
fun rearrange_all sg _ (F as all $ Abs(x,T, P)) =


120 
(case extract_imp P of

4319

121 
None => None

11232

122 
 Some(eq,Q) =>


123 
let val R = imp $ eq $ Q

11221

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

4319

125 
 rearrange_all _ _ _ = None;


126 

11232

127 
fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =


128 
(case extract_imp P of

11221

129 
None => None

11232

130 
 Some(eq,Q) =>


131 
let val R = imp $ eq $ Q

11221

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


133 
 rearrange_ball _ _ _ _ = None;

4319

134 


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

11232

136 
(case extract_conj P of

4319

137 
None => None


138 
 Some(eq,Q) =>

11221

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

4319

140 
 rearrange_ex _ _ _ = None;


141 

11221

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

11232

143 
(case extract_conj P of

11221

144 
None => None


145 
 Some(eq,Q) =>


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


147 
 rearrange_bex _ _ _ _ = None;


148 

4319

149 
end;
