author  haftmann 
Mon, 23 Aug 2010 11:09:48 +0200  
changeset 38668  e8236c4aff16 
parent 36936  c52d1c130898 
child 41248  bb28bf635202 
permissions  rwrr 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/conv.ML 
32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset

2 
Author: Amine Chaieb, TU Muenchen 
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

3 
Author: Sascha Boehme, TU Muenchen 
32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset

4 
Author: Makarius 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

5 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

6 
Conversions: primitive equality reasoning. 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

7 
*) 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

8 

22937  9 
infix 1 then_conv; 
10 
infix 0 else_conv; 

23169  11 

30136
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset

12 
signature BASIC_CONV = 
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset

13 
sig 
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset

14 
val then_conv: conv * conv > conv 
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset

15 
val else_conv: conv * conv > conv 
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset

16 
end; 
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset

17 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

18 
signature CONV = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

19 
sig 
30136
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset

20 
include BASIC_CONV 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

21 
val no_conv: conv 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

22 
val all_conv: conv 
22926  23 
val first_conv: conv list > conv 
24 
val every_conv: conv list > conv 

22937  25 
val try_conv: conv > conv 
26 
val repeat_conv: conv > conv 

32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset

27 
val cache_conv: conv > conv 
26571  28 
val abs_conv: (cterm * Proof.context > conv) > Proof.context > conv 
22926  29 
val combination_conv: conv > conv > conv 
30 
val comb_conv: conv > conv 

31 
val arg_conv: conv > conv 

32 
val fun_conv: conv > conv 

33 
val arg1_conv: conv > conv 

34 
val fun2_conv: conv > conv 

23034  35 
val binop_conv: conv > conv 
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

36 
val binder_conv: (cterm * Proof.context > conv) > Proof.context > conv 
26571  37 
val forall_conv: (cterm * Proof.context > conv) > Proof.context > conv 
38 
val implies_conv: conv > conv > conv 

39 
val implies_concl_conv: conv > conv 

40 
val rewr_conv: thm > conv 

36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

41 
val rewrs_conv: thm list > conv 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

42 
val sub_conv: (Proof.context > conv) > Proof.context > conv 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

43 
val bottom_conv: (Proof.context > conv) > Proof.context > conv 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

44 
val top_conv: (Proof.context > conv) > Proof.context > conv 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

45 
val top_sweep_conv: (Proof.context > conv) > Proof.context > conv 
26571  46 
val params_conv: int > (Proof.context > conv) > Proof.context > conv 
47 
val prems_conv: int > conv > conv 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

48 
val concl_conv: int > conv > conv 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

49 
val fconv_rule: conv > thm > thm 
23583
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

50 
val gconv_rule: conv > int > thm > thm 
38668  51 
val tap_thy: (theory > conv) > conv 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

52 
end; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

53 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

54 
structure Conv: CONV = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

55 
struct 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

56 

32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset

57 
(* basic conversionals *) 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

58 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

59 
fun no_conv _ = raise CTERM ("no conversion", []); 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

60 
val all_conv = Thm.reflexive; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

61 

22937  62 
fun (cv1 then_conv cv2) ct = 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

63 
let 
22926  64 
val eq1 = cv1 ct; 
65 
val eq2 = cv2 (Thm.rhs_of eq1); 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

66 
in 
23596  67 
if Thm.is_reflexive eq1 then eq2 
68 
else if Thm.is_reflexive eq2 then eq1 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

69 
else Thm.transitive eq1 eq2 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

70 
end; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

71 

22937  72 
fun (cv1 else_conv cv2) ct = 
23583
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

73 
(cv1 ct 
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

74 
handle THM _ => cv2 ct 
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

75 
 CTERM _ => cv2 ct 
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

76 
 TERM _ => cv2 ct 
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

77 
 TYPE _ => cv2 ct); 
22926  78 

22937  79 
fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv; 
80 
fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv; 

22926  81 

22937  82 
fun try_conv cv = cv else_conv all_conv; 
83 
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; 

22926  84 

32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset

85 
fun cache_conv (cv: conv) = Thm.cterm_cache cv; 
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset

86 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

87 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

88 

22926  89 
(** Pure conversions **) 
90 

91 
(* lambda terms *) 

92 

24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

93 
fun abs_conv cv ctxt ct = 
23587  94 
(case Thm.term_of ct of 
22926  95 
Abs (x, _, _) => 
23596  96 
let 
24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

97 
val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt; 
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

98 
val (v, ct') = Thm.dest_abs (SOME u) ct; 
26571  99 
val eq = cv (v, ctxt') ct'; 
23596  100 
in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end 
22926  101 
 _ => raise CTERM ("abs_conv", [ct])); 
102 

103 
fun combination_conv cv1 cv2 ct = 

104 
let val (ct1, ct2) = Thm.dest_comb ct 

105 
in Thm.combination (cv1 ct1) (cv2 ct2) end; 

106 

107 
fun comb_conv cv = combination_conv cv cv; 

108 
fun arg_conv cv = combination_conv all_conv cv; 

109 
fun fun_conv cv = combination_conv cv all_conv; 

110 

111 
val arg1_conv = fun_conv o arg_conv; 

112 
val fun2_conv = fun_conv o fun_conv; 

113 

23034  114 
fun binop_conv cv = combination_conv (arg_conv cv) cv; 
22926  115 

36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

116 
fun binder_conv cv ctxt = arg_conv (abs_conv cv ctxt); 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

117 

c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

118 

c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

119 
(* subterm structure *) 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

120 

c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

121 
(*cf. SUB_CONV in HOL*) 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

122 
fun sub_conv conv ctxt = 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

123 
comb_conv (conv ctxt) else_conv 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

124 
abs_conv (conv o snd) ctxt else_conv 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

125 
all_conv; 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

126 

c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

127 
(*cf. BOTTOM_CONV in HOL*) 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

128 
fun bottom_conv conv ctxt ct = 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

129 
(sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct; 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

130 

c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

131 
(*cf. TOP_CONV in HOL*) 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

132 
fun top_conv conv ctxt ct = 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

133 
(conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct; 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

134 

c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

135 
(*cf. TOP_SWEEP_CONV in HOL*) 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

136 
fun top_sweep_conv conv ctxt ct = 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

137 
(conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct; 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

138 

23169  139 

26571  140 
(* primitive logic *) 
141 

142 
fun forall_conv cv ctxt ct = 

143 
(case Thm.term_of ct of 

144 
Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct 

145 
 _ => raise CTERM ("forall_conv", [ct])); 

146 

147 
fun implies_conv cv1 cv2 ct = 

148 
(case Thm.term_of ct of 

149 
Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct 

150 
 _ => raise CTERM ("implies_conv", [ct])); 

151 

152 
fun implies_concl_conv cv ct = 

153 
(case Thm.term_of ct of 

154 
Const ("==>", _) $ _ $ _ => arg_conv cv ct 

155 
 _ => raise CTERM ("implies_concl_conv", [ct])); 

156 

157 

158 
(* single rewrite step, cf. REWR_CONV in HOL *) 

159 

160 
fun rewr_conv rule ct = 

161 
let 

162 
val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule; 

163 
val lhs = Thm.lhs_of rule1; 

164 
val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1; 

165 
in 

166 
Drule.instantiate (Thm.match (lhs, ct)) rule2 

167 
handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct]) 

168 
end; 

169 

36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

170 
fun rewrs_conv rules = first_conv (map rewr_conv rules); 
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset

171 

26571  172 

173 
(* conversions on HHF rules *) 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

174 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

175 
(*rewrite B in !!x1 ... xn. B*) 
26571  176 
fun params_conv n cv ctxt ct = 
27332  177 
if n <> 0 andalso Logic.is_all (Thm.term_of ct) 
26571  178 
then arg_conv (abs_conv (params_conv (n  1) cv o #2) ctxt) ct 
24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

179 
else cv ctxt ct; 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

180 

26571  181 
(*rewrite the A's in A1 ==> ... ==> An ==> B*) 
182 
fun prems_conv 0 _ ct = all_conv ct 

183 
 prems_conv n cv ct = 

184 
(case try Thm.dest_implies ct of 

185 
NONE => all_conv ct 

186 
 SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n  1) cv B)); 

187 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

188 
(*rewrite B in A1 ==> ... ==> An ==> B*) 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

189 
fun concl_conv 0 cv ct = cv ct 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

190 
 concl_conv n cv ct = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

191 
(case try Thm.dest_implies ct of 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

192 
NONE => cv ct 
22926  193 
 SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n  1) cv B)); 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

194 

23596  195 

26571  196 
(* conversions as inference rules *) 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

197 

23596  198 
(*forward conversion, cf. FCONV_RULE in LCF*) 
199 
fun fconv_rule cv th = 

200 
let val eq = cv (Thm.cprop_of th) in 

201 
if Thm.is_reflexive eq then th 

202 
else Thm.equal_elim eq th 

203 
end; 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

204 

23596  205 
(*goal conversion*) 
206 
fun gconv_rule cv i th = 

207 
(case try (Thm.cprem_of th) i of 

208 
SOME ct => 

209 
let val eq = cv ct in 

210 
if Thm.is_reflexive eq then th 

211 
else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th 

212 
end 

213 
 NONE => raise THM ("gconv_rule", i, [th])); 

23411
c524900454f3
Added eta_conv and etaexpansion conversion: waiting for it to be in thm.ML; exported is_refl
chaieb
parents:
23169
diff
changeset

214 

38668  215 

216 
fun tap_thy conv ct = conv (Thm.theory_of_cterm ct) ct; 

217 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

218 
end; 
30136
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset

219 

32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset

220 
structure Basic_Conv: BASIC_CONV = Conv; 
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset

221 
open Basic_Conv; 