author  paulson 
Thu, 28 Nov 1996 10:44:24 +0100  
changeset 2266  82aef6857c5b 
parent 2180  934572a94139 
child 2672  85d7e800d754 
permissions  rwrr 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

1 
(* Title: Pure/drule.ML 
0  2 
ID: $Id$ 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
Derived rules and other operations on theorems and theories 

7 
*) 

8 

11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

9 
infix 0 RS RSN RL RLN MRS MRL COMP; 
0  10 

11 
signature DRULE = 

12 
sig 

1460  13 
val add_defs : (string * string) list > theory > theory 
14 
val add_defs_i : (string * term) list > theory > theory 

15 
val asm_rl : thm 

16 
val assume_ax : theory > string > thm 

17 
val COMP : thm * thm > thm 

18 
val compose : thm * int * thm > thm list 

19 
val cprems_of : thm > cterm list 

20 
val cterm_instantiate : (cterm*cterm)list > thm > thm 

21 
val cut_rl : thm 

22 
val equal_abs_elim : cterm > thm > thm 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

23 
val equal_abs_elim_list: cterm list > thm > thm 
1460  24 
val eq_thm : thm * thm > bool 
25 
val same_thm : thm * thm > bool 

26 
val eq_thm_sg : thm * thm > bool 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

27 
val flexpair_abs_elim_list: cterm list > thm > thm 
1460  28 
val forall_intr_list : cterm list > thm > thm 
29 
val forall_intr_frees : thm > thm 

30 
val forall_intr_vars : thm > thm 

31 
val forall_elim_list : cterm list > thm > thm 

32 
val forall_elim_var : int > thm > thm 

33 
val forall_elim_vars : int > thm > thm 

34 
val implies_elim_list : thm > thm list > thm 

35 
val implies_intr_list : cterm list > thm > thm 

2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

36 
val dest_implies : cterm > cterm * cterm 
1460  37 
val MRL : thm list list * thm list > thm list 
38 
val MRS : thm list * thm > thm 

39 
val read_instantiate : (string*string)list > thm > thm 

0  40 
val read_instantiate_sg: Sign.sg > (string*string)list > thm > thm 
1460  41 
val read_insts : 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

42 
Sign.sg > (indexname > typ option) * (indexname > sort option) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

43 
> (indexname > typ option) * (indexname > sort option) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

44 
> string list > (string*string)list 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

45 
> (indexname*ctyp)list * (cterm*cterm)list 
1460  46 
val reflexive_thm : thm 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

47 
val refl_implies : thm 
1460  48 
val revcut_rl : thm 
49 
val rewrite_goal_rule : bool*bool > (meta_simpset > thm > thm option) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

50 
> meta_simpset > int > thm > thm 
0  51 
val rewrite_goals_rule: thm list > thm > thm 
1460  52 
val rewrite_rule : thm list > thm > thm 
53 
val RS : thm * thm > thm 

54 
val RSN : thm * (int * thm) > thm 

55 
val RL : thm list * thm list > thm list 

56 
val RLN : thm list * (int * thm list) > thm list 

57 
val size_of_thm : thm > int 

2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

58 
val skip_flexpairs : cterm > cterm 
1460  59 
val standard : thm > thm 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

60 
val strip_imp_prems : cterm > cterm list 
1756  61 
val swap_prems_rl : thm 
1460  62 
val symmetric_thm : thm 
63 
val thin_rl : thm 

64 
val transitive_thm : thm 

0  65 
val triv_forall_equality: thm 
66 
val types_sorts: thm > (indexname> typ option) * (indexname> sort option) 

1460  67 
val zero_var_indexes : thm > thm 
0  68 
end; 
69 

668  70 

1499  71 
structure Drule : DRULE = 
0  72 
struct 
73 

561  74 
(**** Extend Theories ****) 
75 

76 
(** add constant definitions **) 

77 

78 
(* all_axioms_of *) 

79 

80 
(*results may contain duplicates!*) 

81 

82 
fun ancestry_of thy = 

83 
thy :: flat (map ancestry_of (parents_of thy)); 

84 

1237  85 
val all_axioms_of = 
776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
708
diff
changeset

86 
flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of; 
561  87 

88 

89 
(* clash_types, clash_consts *) 

90 

91 
(*check if types have common instance (ignoring sorts)*) 

92 

93 
fun clash_types ty1 ty2 = 

94 
let 

95 
val ty1' = Type.varifyT ty1; 

96 
val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2); 

97 
in 

98 
Type.raw_unify (ty1', ty2') 

99 
end; 

100 

101 
fun clash_consts (c1, ty1) (c2, ty2) = 

102 
c1 = c2 andalso clash_types ty1 ty2; 

103 

104 

105 
(* clash_defns *) 

106 

107 
fun clash_defn c_ty (name, tm) = 

108 
let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in 

109 
if clash_consts c_ty (c, ty') then Some (name, ty') else None 

110 
end handle TERM _ => None; 

111 

112 
fun clash_defns c_ty axms = 

113 
distinct (mapfilter (clash_defn c_ty) axms); 

114 

115 

116 
(* dest_defn *) 

117 

118 
fun dest_defn tm = 

119 
let 

120 
fun err msg = raise_term msg [tm]; 

121 

122 
val (lhs, rhs) = Logic.dest_equals tm 

123 
handle TERM _ => err "Not a metaequality (==)"; 

124 
val (head, args) = strip_comb lhs; 

125 
val (c, ty) = dest_Const head 

126 
handle TERM _ => err "Head of lhs not a constant"; 

127 

655  128 
fun occs_const (Const c_ty') = (c_ty' = (c, ty)) 
561  129 
 occs_const (Abs (_, _, t)) = occs_const t 
130 
 occs_const (t $ u) = occs_const t orelse occs_const u 

131 
 occs_const _ = false; 

641  132 

133 
val show_frees = commas_quote o map (fst o dest_Free); 

134 
val show_tfrees = commas_quote o map fst; 

135 

136 
val lhs_dups = duplicates args; 

137 
val rhs_extras = gen_rems (op =) (term_frees rhs, args); 

138 
val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty); 

561  139 
in 
140 
if not (forall is_Free args) then 

1906  141 
err "Arguments (on lhs) must be variables" 
641  142 
else if not (null lhs_dups) then 
143 
err ("Duplicate variables on lhs: " ^ show_frees lhs_dups) 

144 
else if not (null rhs_extras) then 

145 
err ("Extra variables on rhs: " ^ show_frees rhs_extras) 

146 
else if not (null rhs_extrasT) then 

147 
err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT) 

561  148 
else if occs_const rhs then 
655  149 
err ("Constant to be defined occurs on rhs") 
561  150 
else (c, ty) 
151 
end; 

152 

153 

154 
(* check_defn *) 

155 

641  156 
fun err_in_defn name msg = 
157 
(writeln msg; error ("The error(s) above occurred in definition " ^ quote name)); 

561  158 

159 
fun check_defn sign (axms, (name, tm)) = 

160 
let 

161 
fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block 

162 
[Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty])); 

163 

164 
fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn; 

1439  165 
fun show_defns c = cat_lines o map (show_defn c); 
561  166 

167 
val (c, ty) = dest_defn tm 

641  168 
handle TERM (msg, _) => err_in_defn name msg; 
561  169 
val defns = clash_defns (c, ty) axms; 
170 
in 

171 
if not (null defns) then 

641  172 
err_in_defn name ("Definition of " ^ show_const (c, ty) ^ 
1439  173 
"\nclashes with " ^ show_defns c defns) 
561  174 
else (name, tm) :: axms 
175 
end; 

176 

177 

178 
(* add_defs *) 

179 

180 
fun ext_defns prep_axm raw_axms thy = 

181 
let 

182 
val axms = map (prep_axm (sign_of thy)) raw_axms; 

183 
val all_axms = all_axioms_of thy; 

184 
in 

185 
foldl (check_defn (sign_of thy)) (all_axms, axms); 

186 
add_axioms_i axms thy 

187 
end; 

188 

189 
val add_defs_i = ext_defns cert_axm; 

190 
val add_defs = ext_defns read_axm; 

191 

192 

193 

0  194 
(**** More derived rules and operations on theorems ****) 
195 

708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

196 
(** some cterm>cterm operations: much faster than calling cterm_of! **) 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

197 

2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

198 
(** SAME NAMES as in structure Logic: use compound identifiers! **) 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

199 

1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

200 
(*dest_implies for cterms. Note T=prop below*) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

201 
fun dest_implies ct = 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

202 
case term_of ct of 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

203 
(Const("==>", _) $ _ $ _) => 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

204 
let val (ct1,ct2) = dest_comb ct 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

205 
in (#2 (dest_comb ct1), ct2) end 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

206 
 _ => raise TERM ("dest_implies", [term_of ct]) ; 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

207 

e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

208 

708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

209 
(*Discard flexflex pairs; return a cterm*) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

210 
fun skip_flexpairs ct = 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

211 
case term_of ct of 
1460  212 
(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) => 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

213 
skip_flexpairs (#2 (dest_implies ct)) 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

214 
 _ => ct; 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

215 

8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

216 
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

217 
fun strip_imp_prems ct = 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

218 
let val (cA,cB) = dest_implies ct 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

219 
in cA :: strip_imp_prems cB end 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

220 
handle TERM _ => []; 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

221 

2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

222 
(* A1==>...An==>B goes to B, where B is not an implication *) 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

223 
fun strip_imp_concl ct = 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

224 
case term_of ct of (Const("==>", _) $ _ $ _) => 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

225 
strip_imp_concl (#2 (dest_comb ct)) 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

226 
 _ => ct; 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

227 

708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

228 
(*The premises of a theorem, as a cterm list*) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

229 
val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of; 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

230 

8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

231 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

232 
(** reading of instantiations **) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

233 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

234 
fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

235 
 _ => error("Lexical error in variable name " ^ quote (implode cs)); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

236 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

237 
fun absent ixn = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

238 
error("No such variable in term: " ^ Syntax.string_of_vname ixn); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

239 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

240 
fun inst_failure ixn = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

241 
error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails"); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

242 

952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

243 
(* this code is a bit of a mess. add_cterm could be simplified greatly if 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

244 
simultaneous instantiations were read or at least type checked 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

245 
simultaneously rather than one after the other. This would make the tricky 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

246 
composition of implicit type instantiations (parameter tye) superfluous. 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

247 
*) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

248 
fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

249 
let val {tsig,...} = Sign.rep_sg sign 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

250 
fun split([],tvs,vs) = (tvs,vs) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

251 
 split((sv,st)::l,tvs,vs) = (case explode sv of 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

252 
"'"::cs => split(l,(indexname cs,st)::tvs,vs) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

253 
 cs => split(l,tvs,(indexname cs,st)::vs)); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

254 
val (tvs,vs) = split(insts,[],[]); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

255 
fun readT((a,i),st) = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

256 
let val ixn = ("'" ^ a,i); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

257 
val S = case rsorts ixn of Some S => S  None => absent ixn; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

258 
val T = Sign.read_typ (sign,sorts) st; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

259 
in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

260 
else inst_failure ixn 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

261 
end 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

262 
val tye = map readT tvs; 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

263 
fun add_cterm ((cts,tye,used), (ixn,st)) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

264 
let val T = case rtypes ixn of 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

265 
Some T => typ_subst_TVars tye T 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

266 
 None => absent ixn; 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

267 
val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T); 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

268 
val cts' = (ixn,T,ct)::cts 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

269 
fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

270 
val used' = add_term_tvarnames(term_of ct,used); 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

271 
in (map inst cts',tye2 @ tye,used') end 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

272 
val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs); 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

273 
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

274 
map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms) 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

275 
end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

276 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

277 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

278 
(*** Find the type (sort) associated with a (T)Var or (T)Free in a term 
0  279 
Used for establishing default types (of variables) and sorts (of 
280 
type variables) when reading another term. 

281 
Index 1 indicates that a (T)Free rather than a (T)Var is wanted. 

282 
***) 

283 

284 
fun types_sorts thm = 

285 
let val {prop,hyps,...} = rep_thm thm; 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

286 
val big = list_comb(prop,hyps); (* bogus term! *) 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

287 
val vars = map dest_Var (term_vars big); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

288 
val frees = map dest_Free (term_frees big); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

289 
val tvars = term_tvars big; 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

290 
val tfrees = term_tfrees big; 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

291 
fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i)); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

292 
fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); 
0  293 
in (typ,sort) end; 
294 

295 
(** Standardization of rules **) 

296 

297 
(*Generalization over a list of variables, IGNORING bad ones*) 

298 
fun forall_intr_list [] th = th 

299 
 forall_intr_list (y::ys) th = 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

300 
let val gth = forall_intr_list ys th 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

301 
in forall_intr y gth handle THM _ => gth end; 
0  302 

303 
(*Generalization over all suitable Free variables*) 

304 
fun forall_intr_frees th = 

305 
let val {prop,sign,...} = rep_thm th 

306 
in forall_intr_list 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

307 
(map (cterm_of sign) (sort atless (term_frees prop))) 
0  308 
th 
309 
end; 

310 

311 
(*Replace outermost quantified variable by Var of given index. 

312 
Could clash with Vars already present.*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

313 
fun forall_elim_var i th = 
0  314 
let val {prop,sign,...} = rep_thm th 
315 
in case prop of 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

316 
Const("all",_) $ Abs(a,T,_) => 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

317 
forall_elim (cterm_of sign (Var((a,i), T))) th 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

318 
 _ => raise THM("forall_elim_var", i, [th]) 
0  319 
end; 
320 

321 
(*Repeat forall_elim_var until all outer quantifiers are removed*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

322 
fun forall_elim_vars i th = 
0  323 
forall_elim_vars i (forall_elim_var i th) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

324 
handle THM _ => th; 
0  325 

326 
(*Specialization over a list of cterms*) 

327 
fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th); 

328 

329 
(* maps [A1,...,An], B to [ A1;...;An ] ==> B *) 

330 
fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th); 

331 

332 
(* maps [ A1;...;An ] ==> B and [A1,...,An] to B *) 

333 
fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths); 

334 

335 
(*Reset Var indexes to zero, renaming to preserve distinctness*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

336 
fun zero_var_indexes th = 
0  337 
let val {prop,sign,...} = rep_thm th; 
338 
val vars = term_vars prop 

339 
val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

340 
val inrs = add_term_tvars(prop,[]); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

341 
val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs)); 
2266  342 
val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs))) 
343 
(inrs, nms') 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

344 
val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye; 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

345 
fun varpairs([],[]) = [] 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

346 
 varpairs((var as Var(v,T)) :: vars, b::bs) = 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

347 
let val T' = typ_subst_TVars tye T 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

348 
in (cterm_of sign (Var(v,T')), 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

349 
cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs) 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

350 
end 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

351 
 varpairs _ = raise TERM("varpairs", []); 
0  352 
in instantiate (ctye, varpairs(vars,rev bs)) th end; 
353 

354 

355 
(*Standard form of objectrule: no hypotheses, Frees, or outer quantifiers; 

356 
all generality expressed by Vars having index 0.*) 

357 
fun standard th = 

1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

358 
let val {maxidx,...} = rep_thm th 
1237  359 
in 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

360 
th > implies_intr_hyps 
1412  361 
> forall_intr_frees > forall_elim_vars (maxidx + 1) 
1439  362 
> Thm.strip_shyps > Thm.implies_intr_shyps 
1412  363 
> zero_var_indexes > Thm.varifyT > Thm.compress 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

364 
end; 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

365 

0  366 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

367 
(*Assume a new formula, read following the same conventions as axioms. 
0  368 
Generalizes over Free variables, 
369 
creates the assumption, and then strips quantifiers. 

370 
Example is [ ALL x:?A. ?P(x) ] ==> [ ?P(?a) ] 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

371 
[ !(A,P,a)[ ALL x:A. P(x) ] ==> [ P(a) ] ] *) 
0  372 
fun assume_ax thy sP = 
373 
let val sign = sign_of thy 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

374 
val prop = Logic.close_form (term_of (read_cterm sign 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

375 
(sP, propT))) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

376 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  377 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

378 
(*Resolution: exactly one resolvent must be produced.*) 
0  379 
fun tha RSN (i,thb) = 
380 
case Sequence.chop (2, biresolution false [(false,tha)] i thb) of 

381 
([th],_) => th 

382 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

383 
 _ => raise THM("RSN: multiple unifiers", i, [tha,thb]); 

384 

385 
(*resolution: P==>Q, Q==>R gives P==>R. *) 

386 
fun tha RS thb = tha RSN (1,thb); 

387 

388 
(*For joining lists of rules*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

389 
fun thas RLN (i,thbs) = 
0  390 
let val resolve = biresolution false (map (pair false) thas) i 
391 
fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => [] 

392 
in flat (map resb thbs) end; 

393 

394 
fun thas RL thbs = thas RLN (1,thbs); 

395 

11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

396 
(*Resolve a list of rules against bottom_rl from right to left; 
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

397 
makes proof trees*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

398 
fun rls MRS bottom_rl = 
11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

399 
let fun rs_aux i [] = bottom_rl 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

400 
 rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls) 
11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

401 
in rs_aux 1 rls end; 
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

402 

d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

403 
(*As above, but for rule lists*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

404 
fun rlss MRL bottom_rls = 
11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

405 
let fun rs_aux i [] = bottom_rls 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

406 
 rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss) 
11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

407 
in rs_aux 1 rlss end; 
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

408 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

409 
(*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R 
0  410 
with no lifting or renaming! Q may contain ==> or metaquants 
411 
ALWAYS deletes premise i *) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

412 
fun compose(tha,i,thb) = 
0  413 
Sequence.list_of_s (bicompose false (false,tha,0) i thb); 
414 

415 
(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) 

416 
fun tha COMP thb = 

417 
case compose(tha,1,thb) of 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

418 
[th] => th 
0  419 
 _ => raise THM("COMP", 1, [tha,thb]); 
420 

421 
(*Instantiate theorem th, reading instantiations under signature sg*) 

422 
fun read_instantiate_sg sg sinsts th = 

423 
let val ts = types_sorts th; 

952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

424 
val used = add_term_tvarnames(#prop(rep_thm th),[]); 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

425 
in instantiate (read_insts sg ts ts used sinsts) th end; 
0  426 

427 
(*Instantiate theorem th, reading instantiations under theory of th*) 

428 
fun read_instantiate sinsts th = 

429 
read_instantiate_sg (#sign (rep_thm th)) sinsts th; 

430 

431 

432 
(*Lefttoright replacements: tpairs = [...,(vi,ti),...]. 

433 
Instantiates distinct Vars by terms, inferring type instantiations. *) 

434 
local 

1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

435 
fun add_types ((ct,cu), (sign,tye,maxidx)) = 
2152  436 
let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct 
437 
and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu; 

438 
val maxi = Int.max(maxidx, Int.max(maxt, maxu)); 

0  439 
val sign' = Sign.merge(sign, Sign.merge(signt, signu)) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

440 
val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

441 
handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u]) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

442 
in (sign', tye', maxi') end; 
0  443 
in 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

444 
fun cterm_instantiate ctpairs0 th = 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

445 
let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0)) 
0  446 
val tsig = #tsig(Sign.rep_sg sign); 
447 
fun instT(ct,cu) = let val inst = subst_TVars tye 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

448 
in (cterm_fun inst ct, cterm_fun inst cu) end 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

449 
fun ctyp2 (ix,T) = (ix, ctyp_of sign T) 
0  450 
in instantiate (map ctyp2 tye, map instT ctpairs0) th end 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

451 
handle TERM _ => 
0  452 
raise THM("cterm_instantiate: incompatible signatures",0,[th]) 
453 
 TYPE _ => raise THM("cterm_instantiate: types", 0, [th]) 

454 
end; 

455 

456 

457 
(** theorem equality test is exported and used by BEST_FIRST **) 

458 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

459 
(*equality of theorems uses equality of signatures and 
0  460 
the aconvertible test for terms*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

461 
fun eq_thm (th1,th2) = 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

462 
let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

463 
and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

464 
in Sign.eq_sg (sg1,sg2) andalso 
2180
934572a94139
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2152
diff
changeset

465 
eq_set_sort (shyps1, shyps2) andalso 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

466 
aconvs(hyps1,hyps2) andalso 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

467 
prop1 aconv prop2 
0  468 
end; 
469 

1241  470 
(*equality of theorems using similarity of signatures, 
471 
i.e. the theorems belong to the same theory but not necessarily to the same 

472 
version of this theory*) 

473 
fun same_thm (th1,th2) = 

474 
let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1 

475 
and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2 

476 
in Sign.same_sg (sg1,sg2) andalso 

2180
934572a94139
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2152
diff
changeset

477 
eq_set_sort (shyps1, shyps2) andalso 
1241  478 
aconvs(hyps1,hyps2) andalso 
479 
prop1 aconv prop2 

480 
end; 

481 

0  482 
(*Do the two theorems have the same signature?*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

483 
fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2)); 
0  484 

485 
(*Useful "distance" function for BEST_FIRST*) 

486 
val size_of_thm = size_of_term o #prop o rep_thm; 

487 

488 

1194
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

489 
(** Mark Staples's weaker version of eq_thm: ignores variable renaming and 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

490 
(some) type variable renaming **) 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

491 

563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

492 
(* Can't use term_vars, because it sorts the resulting list of variable names. 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

493 
We instead need the unique list noramlised by the order of appearance 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

494 
in the term. *) 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

495 
fun term_vars' (t as Var(v,T)) = [t] 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

496 
 term_vars' (Abs(_,_,b)) = term_vars' b 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

497 
 term_vars' (f$a) = (term_vars' f) @ (term_vars' a) 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

498 
 term_vars' _ = []; 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

499 

563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

500 
fun forall_intr_vars th = 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

501 
let val {prop,sign,...} = rep_thm th; 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

502 
val vars = distinct (term_vars' prop); 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

503 
in forall_intr_list (map (cterm_of sign) vars) th end; 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

504 

1237  505 
fun weak_eq_thm (tha,thb) = 
1194
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

506 
eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb)); 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

507 

563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

508 

563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

509 

0  510 
(*** MetaRewriting Rules ***) 
511 

512 

513 
val reflexive_thm = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

514 
let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS))) 
0  515 
in Thm.reflexive cx end; 
516 

517 
val symmetric_thm = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

518 
let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT) 
0  519 
in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end; 
520 

521 
val transitive_thm = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

522 
let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

523 
val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT) 
0  524 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
525 
in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 

526 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

527 
(** Below, a "conversion" has type cterm > thm **) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

528 

2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

529 
val refl_implies = reflexive (cterm_of Sign.proto_pure implies); 
0  530 

531 
(*In [A1,...,An]==>B, rewrite the selected A's only  for rewrite_goals_tac*) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

532 
(*Do not rewrite flexflex pairs*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

533 
fun goals_conv pred cv = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

534 
let fun gconv i ct = 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

535 
let val (A,B) = dest_implies ct 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

536 
val (thA,j) = case term_of A of 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

537 
Const("=?=",_)$_$_ => (reflexive A, i) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

538 
 _ => (if pred i then cv A else reflexive A, i+1) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

539 
in combination (combination refl_implies thA) (gconv j B) end 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

540 
handle TERM _ => reflexive ct 
0  541 
in gconv 1 end; 
542 

543 
(*Use a conversion to transform a theorem*) 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

544 
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; 
0  545 

546 
(*rewriting conversion*) 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

547 
fun rew_conv mode prover mss = rewrite_cterm mode mss prover; 
0  548 

549 
(*Rewrite a theorem*) 

1412  550 
fun rewrite_rule [] th = th 
551 
 rewrite_rule thms th = 

1460  552 
fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th; 
0  553 

554 
(*Rewrite the subgoals of a proof state (represented by a theorem) *) 

1412  555 
fun rewrite_goals_rule [] th = th 
556 
 rewrite_goals_rule thms th = 

1460  557 
fconv_rule (goals_conv (K true) 
558 
(rew_conv (true,false) (K(K None)) 

559 
(Thm.mss_of thms))) 

560 
th; 

0  561 

562 
(*Rewrite the subgoal of a proof state (represented by a theorem) *) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

563 
fun rewrite_goal_rule mode prover mss i thm = 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

564 
if 0 < i andalso i <= nprems_of thm 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

565 
then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

566 
else raise THM("rewrite_goal_rule",i,[thm]); 
0  567 

568 

569 
(** Derived rules mainly for METAHYPS **) 

570 

571 
(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*) 

572 
fun equal_abs_elim ca eqth = 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

573 
let val {sign=signa, t=a, ...} = rep_cterm ca 
0  574 
and combth = combination eqth (reflexive ca) 
575 
val {sign,prop,...} = rep_thm eqth 

576 
val (abst,absu) = Logic.dest_equals prop 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

577 
val cterm = cterm_of (Sign.merge (sign,signa)) 
0  578 
in transitive (symmetric (beta_conversion (cterm (abst$a)))) 
579 
(transitive combth (beta_conversion (cterm (absu$a)))) 

580 
end 

581 
handle THM _ => raise THM("equal_abs_elim", 0, [eqth]); 

582 

583 
(*Calling equal_abs_elim with multiple terms*) 

584 
fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th); 

585 

586 
local 

587 
val alpha = TVar(("'a",0), []) (* type ?'a::{} *) 

588 
fun err th = raise THM("flexpair_inst: ", 0, [th]) 

589 
fun flexpair_inst def th = 

590 
let val {prop = Const _ $ t $ u, sign,...} = rep_thm th 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

591 
val cterm = cterm_of sign 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

592 
fun cvar a = cterm(Var((a,0),alpha)) 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

593 
val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

594 
def 
0  595 
in equal_elim def' th 
596 
end 

597 
handle THM _ => err th  bind => err th 

598 
in 

599 
val flexpair_intr = flexpair_inst (symmetric flexpair_def) 

600 
and flexpair_elim = flexpair_inst flexpair_def 

601 
end; 

602 

603 
(*Version for flexflex pairs  this supports lifting.*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

604 
fun flexpair_abs_elim_list cts = 
0  605 
flexpair_intr o equal_abs_elim_list cts o flexpair_elim; 
606 

607 

608 
(*** Some useful metatheorems ***) 

609 

610 
(*The rule V/V, obtains assumption solving for eresolve_tac*) 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

611 
val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT)); 
0  612 

613 
(*Metalevel cut rule: [ V==>W; V ] ==> W *) 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

614 
val cut_rl = trivial(read_cterm Sign.proto_pure 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

615 
("PROP ?psi ==> PROP ?theta", propT)); 
0  616 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

617 
(*Generalized elim rule for one conclusion; cut_rl with reversed premises: 
0  618 
[ PROP V; PROP V ==> PROP W ] ==> PROP W *) 
619 
val revcut_rl = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

620 
let val V = read_cterm Sign.proto_pure ("PROP V", propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

621 
and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT); 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

622 
in standard (implies_intr V 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

623 
(implies_intr VW 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

624 
(implies_elim (assume VW) (assume V)))) 
0  625 
end; 
626 

668  627 
(*for deleting an unwanted assumption*) 
628 
val thin_rl = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

629 
let val V = read_cterm Sign.proto_pure ("PROP V", propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

630 
and W = read_cterm Sign.proto_pure ("PROP W", propT); 
668  631 
in standard (implies_intr V (implies_intr W (assume W))) 
632 
end; 

633 

0  634 
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*) 
635 
val triv_forall_equality = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

636 
let val V = read_cterm Sign.proto_pure ("PROP V", propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

637 
and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

638 
and x = read_cterm Sign.proto_pure ("x", TFree("'a",logicS)); 
0  639 
in standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

640 
(implies_intr V (forall_intr x (assume V)))) 
0  641 
end; 
642 

1756  643 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
644 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

645 
`thm COMP swap_prems_rl' swaps the first two premises of `thm' 

646 
*) 

647 
val swap_prems_rl = 

648 
let val cmajor = read_cterm Sign.proto_pure 

649 
("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT); 

650 
val major = assume cmajor; 

651 
val cminor1 = read_cterm Sign.proto_pure ("PROP PhiA", propT); 

652 
val minor1 = assume cminor1; 

653 
val cminor2 = read_cterm Sign.proto_pure ("PROP PhiB", propT); 

654 
val minor2 = assume cminor2; 

655 
in standard 

656 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 

657 
(implies_elim (implies_elim major minor1) minor2)))) 

658 
end; 

659 

0  660 
end; 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

661 

1499  662 
open Drule; 