author  wenzelm 
Fri, 11 May 2007 18:47:08 +0200  
changeset 22938  454f1678bf5f 
parent 22906  195b7515911a 
child 22939  2afc93a3d8f4 
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 

3766  6 
Derived rules and other operations on theorems. 
0  7 
*) 
8 

21578  9 
infix 0 RS RSN RL RLN MRS MRL OF COMP INCR_COMP COMP_INCR; 
0  10 

5903  11 
signature BASIC_DRULE = 
3766  12 
sig 
18179  13 
val mk_implies: cterm * cterm > cterm 
14 
val list_implies: cterm list * cterm > cterm 

15 
val strip_imp_prems: cterm > cterm list 

16 
val strip_imp_concl: cterm > cterm 

17 
val cprems_of: thm > cterm list 

18 
val cterm_fun: (term > term) > (cterm > cterm) 

19 
val ctyp_fun: (typ > typ) > (ctyp > ctyp) 

18206  20 
val read_insts: theory > (indexname > typ option) * (indexname > sort option) > 
21 
(indexname > typ option) * (indexname > sort option) > string list > 

22 
(indexname * string) list > (ctyp * ctyp) list * (cterm * cterm) list 

4285  23 
val types_sorts: thm > (indexname> typ option) * (indexname> sort option) 
18179  24 
val forall_intr_list: cterm list > thm > thm 
25 
val forall_intr_frees: thm > thm 

26 
val forall_intr_vars: thm > thm 

27 
val forall_elim_list: cterm list > thm > thm 

28 
val forall_elim_var: int > thm > thm 

29 
val forall_elim_vars: int > thm > thm 

30 
val gen_all: thm > thm 

31 
val lift_all: cterm > thm > thm 

32 
val freeze_thaw: thm > thm * (thm > thm) 

15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

33 
val freeze_thaw_robust: thm > thm * (int > thm > thm) 
18179  34 
val implies_elim_list: thm > thm list > thm 
35 
val implies_intr_list: cterm list > thm > thm 

18206  36 
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list > thm > thm 
21603  37 
val zero_var_indexes_list: thm list > thm list 
18179  38 
val zero_var_indexes: thm > thm 
39 
val implies_intr_hyps: thm > thm 

40 
val standard: thm > thm 

41 
val standard': thm > thm 

42 
val rotate_prems: int > thm > thm 

43 
val rearrange_prems: int list > thm > thm 

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

45 
val RS: thm * thm > thm 

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

47 
val RL: thm list * thm list > thm list 

48 
val MRS: thm list * thm > thm 

49 
val MRL: thm list list * thm list > thm list 

50 
val OF: thm * thm list > thm 

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

52 
val COMP: thm * thm > thm 

21578  53 
val INCR_COMP: thm * thm > thm 
54 
val COMP_INCR: thm * thm > thm 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

55 
val read_instantiate_sg: theory > (string*string)list > thm > thm 
18179  56 
val read_instantiate: (string*string)list > thm > thm 
57 
val cterm_instantiate: (cterm*cterm)list > thm > thm 

58 
val size_of_thm: thm > int 

59 
val reflexive_thm: thm 

60 
val symmetric_thm: thm 

61 
val transitive_thm: thm 

62 
val symmetric_fun: thm > thm 

63 
val extensional: thm > thm 

18820  64 
val equals_cong: thm 
18179  65 
val imp_cong: thm 
66 
val swap_prems_eq: thm 

67 
val asm_rl: thm 

68 
val cut_rl: thm 

69 
val revcut_rl: thm 

70 
val thin_rl: thm 

4285  71 
val triv_forall_equality: thm 
19051  72 
val distinct_prems_rl: thm 
18179  73 
val swap_prems_rl: thm 
74 
val equal_intr_rule: thm 

75 
val equal_elim_rule1: thm 

19421  76 
val equal_elim_rule2: thm 
18179  77 
val instantiate': ctyp option list > cterm option list > thm > thm 
5903  78 
end; 
79 

80 
signature DRULE = 

81 
sig 

82 
include BASIC_DRULE 

19999  83 
val generalize: string list * string list > thm > thm 
15949  84 
val list_comb: cterm * cterm list > cterm 
12908
53bfe07a7916
New function strip_comb (cterm version of Term.strip_comb).
berghofe
parents:
12800
diff
changeset

85 
val strip_comb: cterm > cterm * cterm list 
15262  86 
val strip_type: ctyp > ctyp list * ctyp 
15949  87 
val beta_conv: cterm > cterm > cterm 
15669  88 
val add_used: thm > string list > string list 
17713  89 
val flexflex_unique: thm > thm 
11975  90 
val close_derivation: thm > thm 
19421  91 
val store_thm: bstring > thm > thm 
92 
val store_standard_thm: bstring > thm > thm 

93 
val store_thm_open: bstring > thm > thm 

94 
val store_standard_thm_open: bstring > thm > thm 

11975  95 
val compose_single: thm * int * thm > thm 
12373  96 
val add_rule: thm > thm list > thm list 
97 
val del_rule: thm > thm list > thm list 

11975  98 
val merge_rules: thm list * thm list > thm list 
18468  99 
val imp_cong_rule: thm > thm > thm 
22938  100 
val fun_cong_rule: cterm > thm > thm 
101 
val arg_cong_rule: thm > cterm > thm 

15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

102 
val beta_eta_conversion: cterm > thm 
15925  103 
val eta_long_conversion: cterm > thm 
20861  104 
val eta_contraction_rule: thm > thm 
11975  105 
val norm_hhf_eq: thm 
12800  106 
val is_norm_hhf: term > bool 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

107 
val norm_hhf: theory > term > term 
20298  108 
val norm_hhf_cterm: cterm > cterm 
19878  109 
val unvarify: thm > thm 
18025  110 
val protect: cterm > cterm 
111 
val protectI: thm 

112 
val protectD: thm 

18179  113 
val protect_cong: thm 
18025  114 
val implies_intr_protected: cterm list > thm > thm 
19775  115 
val termI: thm 
116 
val mk_term: cterm > thm 

117 
val dest_term: thm > cterm 

21519  118 
val cterm_rule: (thm > thm) > cterm > cterm 
20881  119 
val term_rule: theory > (thm > thm) > term > term 
19523  120 
val sort_triv: theory > typ * sort > thm list 
19504  121 
val unconstrainTs: thm > thm 
14081  122 
val rename_bvars: (string * string) list > thm > thm 
123 
val rename_bvars': string option list > thm > thm 

19124  124 
val incr_indexes: thm > thm > thm 
125 
val incr_indexes2: thm > thm > thm > thm 

12297  126 
val remdups_rl: thm 
18225  127 
val multi_resolve: thm list > thm > thm Seq.seq 
128 
val multi_resolves: thm list > thm list > thm Seq.seq 

13325  129 
val abs_def: thm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

130 
val read_instantiate_sg': theory > (indexname * string) list > thm > thm 
15797  131 
val read_instantiate': (indexname * string) list > thm > thm 
3766  132 
end; 
0  133 

5903  134 
structure Drule: DRULE = 
0  135 
struct 
136 

3991  137 

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

139 

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

140 
(* 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

141 
fun strip_imp_prems ct = 
22906
195b7515911a
moved some operations to more_thm.ML and conv.ML;
wenzelm
parents:
22695
diff
changeset

142 
let val (cA, cB) = Thm.dest_implies ct 
20579  143 
in cA :: strip_imp_prems cB end 
144 
handle TERM _ => []; 

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

145 

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

146 
(* 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

147 
fun strip_imp_concl ct = 
20579  148 
(case Thm.term_of ct of 
149 
Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct) 

150 
 _ => ct); 

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

151 

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

152 
(*The premises of a theorem, as a cterm list*) 
13659
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
13650
diff
changeset

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

154 

15797  155 
fun cterm_fun f ct = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

156 
let val {t, thy, ...} = Thm.rep_cterm ct 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

157 
in Thm.cterm_of thy (f t) end; 
15797  158 

159 
fun ctyp_fun f cT = 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

160 
let val {T, thy, ...} = Thm.rep_ctyp cT 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

161 
in Thm.ctyp_of thy (f T) end; 
15797  162 

19421  163 
val cert = cterm_of ProtoPure.thy; 
9547  164 

19421  165 
val implies = cert Term.implies; 
19183  166 
fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B; 
9547  167 

168 
(*cterm version of list_implies: [A1,...,An], B goes to [A1;==>;An]==>B *) 

169 
fun list_implies([], B) = B 

170 
 list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B)); 

171 

15949  172 
(*cterm version of list_comb: maps (f, [t1,...,tn]) to f(t1,...,tn) *) 
173 
fun list_comb (f, []) = f 

174 
 list_comb (f, t::ts) = list_comb (Thm.capply f t, ts); 

175 

12908
53bfe07a7916
New function strip_comb (cterm version of Term.strip_comb).
berghofe
parents:
12800
diff
changeset

176 
(*cterm version of strip_comb: maps f(t1,...,tn) to (f, [t1,...,tn]) *) 
18179  177 
fun strip_comb ct = 
12908
53bfe07a7916
New function strip_comb (cterm version of Term.strip_comb).
berghofe
parents:
12800
diff
changeset

178 
let 
53bfe07a7916
New function strip_comb (cterm version of Term.strip_comb).
berghofe
parents:
12800
diff
changeset

179 
fun stripc (p as (ct, cts)) = 
53bfe07a7916
New function strip_comb (cterm version of Term.strip_comb).
berghofe
parents:
12800
diff
changeset

180 
let val (ct1, ct2) = Thm.dest_comb ct 
53bfe07a7916
New function strip_comb (cterm version of Term.strip_comb).
berghofe
parents:
12800
diff
changeset

181 
in stripc (ct1, ct2 :: cts) end handle CTERM _ => p 
53bfe07a7916
New function strip_comb (cterm version of Term.strip_comb).
berghofe
parents:
12800
diff
changeset

182 
in stripc (ct, []) end; 
53bfe07a7916
New function strip_comb (cterm version of Term.strip_comb).
berghofe
parents:
12800
diff
changeset

183 

15262  184 
(* cterm version of strip_type: maps [T1,...,Tn]>T to ([T1,T2,...,Tn], T) *) 
185 
fun strip_type cT = (case Thm.typ_of cT of 

186 
Type ("fun", _) => 

187 
let 

188 
val [cT1, cT2] = Thm.dest_ctyp cT; 

189 
val (cTs, cT') = strip_type cT2 

190 
in (cT1 :: cTs, cT') end 

191 
 _ => ([], cT)); 

192 

15949  193 
(*Betaconversion for cterms, where x is an abstraction. Simply returns the rhs 
194 
of the metaequality returned by the beta_conversion rule.*) 

18179  195 
fun beta_conv x y = 
20579  196 
Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.capply x y))); 
15949  197 

15875  198 

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

199 

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

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

201 

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

202 
fun absent ixn = 
22681
9d42e5365ad1
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22561
diff
changeset

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

204 

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

205 
fun inst_failure ixn = 
22681
9d42e5365ad1
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22561
diff
changeset

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

207 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

208 
fun read_insts thy (rtypes,rsorts) (types,sorts) used insts = 
10403  209 
let 
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15262
diff
changeset

210 
fun is_tv ((a, _), _) = 
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15262
diff
changeset

211 
(case Symbol.explode a of "'" :: _ => true  _ => false); 
15570  212 
val (tvs, vs) = List.partition is_tv insts; 
15797  213 
fun sort_of ixn = case rsorts ixn of SOME S => S  NONE => absent ixn; 
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15262
diff
changeset

214 
fun readT (ixn, st) = 
15797  215 
let val S = sort_of ixn; 
22681
9d42e5365ad1
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22561
diff
changeset

216 
val T = Sign.read_def_typ (thy,sorts) st; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

217 
in if Sign.typ_instance thy (T, TVar(ixn,S)) then (ixn,T) 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

218 
else inst_failure ixn 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

219 
end 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

220 
val tye = map readT tvs; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

221 
fun mkty(ixn,st) = (case rtypes ixn of 
15531  222 
SOME T => (ixn,(st,typ_subst_TVars tye T)) 
223 
 NONE => absent ixn); 

4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

224 
val ixnsTs = map mkty vs; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

225 
val ixns = map fst ixnsTs 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

226 
and sTs = map snd ixnsTs 
22681
9d42e5365ad1
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22561
diff
changeset

227 
val (cts,tye2) = Thm.read_def_cterms(thy,types,sorts) used false sTs; 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

228 
fun mkcVar(ixn,T) = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

229 
let val U = typ_subst_TVars tye2 T 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

230 
in cterm_of thy (Var(ixn,U)) end 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

231 
val ixnTs = ListPair.zip(ixns, map snd sTs) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

232 
in (map (fn (ixn, T) => (ctyp_of thy (TVar (ixn, sort_of ixn)), 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

233 
ctyp_of thy T)) (tye2 @ tye), 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

234 
ListPair.zip(map mkcVar ixnTs,cts)) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

235 
end; 
229
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 

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

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

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

242 
***) 

243 

244 
fun types_sorts thm = 

20329  245 
let 
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

246 
val vars = Thm.fold_terms Term.add_vars thm []; 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

247 
val frees = Thm.fold_terms Term.add_frees thm []; 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

248 
val tvars = Thm.fold_terms Term.add_tvars thm []; 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

249 
val tfrees = Thm.fold_terms Term.add_tfrees thm []; 
20329  250 
fun types (a, i) = 
251 
if i < 0 then AList.lookup (op =) frees a else AList.lookup (op =) vars (a, i); 

252 
fun sorts (a, i) = 

253 
if i < 0 then AList.lookup (op =) tfrees a else AList.lookup (op =) tvars (a, i); 

254 
in (types, sorts) end; 

0  255 

20329  256 
val add_used = 
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

257 
(Thm.fold_terms o fold_types o fold_atyps) 
20329  258 
(fn TFree (a, _) => insert (op =) a 
259 
 TVar ((a, _), _) => insert (op =) a 

260 
 _ => I); 

15669  261 

7636  262 

9455  263 

0  264 
(** Standardization of rules **) 
265 

19523  266 
(* type classes and sorts *) 
267 

268 
fun sort_triv thy (T, S) = 

269 
let 

270 
val certT = Thm.ctyp_of thy; 

271 
val cT = certT T; 

272 
fun class_triv c = 

273 
Thm.class_triv thy c 

274 
> Thm.instantiate ([(certT (TVar (("'a", 0), [c])), cT)], []); 

275 
in map class_triv S end; 

276 

19504  277 
fun unconstrainTs th = 
20298  278 
fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar) 
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

279 
(Thm.fold_terms Term.add_tvars th []) th; 
19504  280 

19730  281 
(*Generalization over a list of variables*) 
282 
val forall_intr_list = fold_rev forall_intr; 

0  283 

284 
(*Generalization over all suitable Free variables*) 

285 
fun forall_intr_frees th = 

19730  286 
let 
287 
val {prop, hyps, tpairs, thy,...} = rep_thm th; 

288 
val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) []; 

289 
val frees = Term.fold_aterms (fn Free v => 

290 
if member (op =) fixed v then I else insert (op =) v  _ => I) prop []; 

291 
in fold (forall_intr o cterm_of thy o Free) frees th end; 

0  292 

18535  293 
(*Generalization over Vars  canonical order*) 
294 
fun forall_intr_vars th = 

20298  295 
fold forall_intr 
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

296 
(map (Thm.cterm_of (Thm.theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th [])) th; 
18535  297 

7898  298 
val forall_elim_var = PureThy.forall_elim_var; 
299 
val forall_elim_vars = PureThy.forall_elim_vars; 

0  300 

18025  301 
fun outer_params t = 
20077
4fc9a4fef219
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19999
diff
changeset

302 
let val vs = Term.strip_all_vars t 
4fc9a4fef219
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19999
diff
changeset

303 
in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end; 
18025  304 

305 
(*generalize outermost parameters*) 

306 
fun gen_all th = 

12719
41e0d086f8b6
improved forall_elim_vars_safe (no longer invents new indexes);
wenzelm
parents:
12710
diff
changeset

307 
let 
18025  308 
val {thy, prop, maxidx, ...} = Thm.rep_thm th; 
309 
val cert = Thm.cterm_of thy; 

310 
fun elim (x, T) = Thm.forall_elim (cert (Var ((x, maxidx + 1), T))); 

311 
in fold elim (outer_params prop) th end; 

312 

313 
(*lift vars wrt. outermost goal parameters 

18118  314 
 reverses the effect of gen_all modulo higherorder unification*) 
18025  315 
fun lift_all goal th = 
316 
let 

317 
val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th); 

318 
val cert = Thm.cterm_of thy; 

19421  319 
val maxidx = Thm.maxidx_of th; 
18025  320 
val ps = outer_params (Thm.term_of goal) 
321 
> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T)); 

322 
val Ts = map Term.fastype_of ps; 

22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

323 
val inst = Thm.fold_terms Term.add_vars th [] > map (fn (xi, T) => 
18025  324 
(cert (Var (xi, T)), cert (Term.list_comb (Var (xi, Ts > T), ps)))); 
325 
in 

326 
th > Thm.instantiate ([], inst) 

327 
> fold_rev (Thm.forall_intr o cert) ps 

328 
end; 

329 

19999  330 
(*direct generalization*) 
331 
fun generalize names th = Thm.generalize names (Thm.maxidx_of th + 1) th; 

9554  332 

16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

333 
(*specialization over a list of cterms*) 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

334 
val forall_elim_list = fold forall_elim; 
0  335 

16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

336 
(*maps A1,...,An  B to [ A1;...;An ] ==> B*) 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

337 
val implies_intr_list = fold_rev implies_intr; 
0  338 

16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

339 
(*maps [ A1;...;An ] ==> B and [A1,...,An] to B*) 
15570  340 
fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths); 
0  341 

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

21603  343 
fun zero_var_indexes_list [] = [] 
344 
 zero_var_indexes_list ths = 

345 
let 

346 
val thy = Theory.merge_list (map Thm.theory_of_thm ths); 

347 
val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy; 

348 
val (instT, inst) = TermSubst.zero_var_indexes_inst (map Thm.full_prop_of ths); 

349 
val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT; 

350 
val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst; 

351 
in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end; 

352 

353 
val zero_var_indexes = singleton zero_var_indexes_list; 

0  354 

355 

14394  356 
(** Standard form of objectrule: no hypotheses, flexflex constraints, 
357 
Frees, or outer quantifiers; all generality expressed by Vars of index 0.**) 

10515  358 

16595  359 
(*Discharge all hypotheses.*) 
360 
fun implies_intr_hyps th = 

361 
fold Thm.implies_intr (#hyps (Thm.crep_thm th)) th; 

362 

14394  363 
(*Squash a theorem's flexflex constraints provided it can be done uniquely. 
364 
This step can lose information.*) 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14340
diff
changeset

365 
fun flexflex_unique th = 
17713  366 
if null (tpairs_of th) then th else 
19861  367 
case Seq.chop 2 (flexflex_rule th) of 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14340
diff
changeset

368 
([th],_) => th 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14340
diff
changeset

369 
 ([],_) => raise THM("flexflex_unique: impossible constraints", 0, [th]) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14340
diff
changeset

370 
 _ => raise THM("flexflex_unique: multiple unifiers", 0, [th]); 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14340
diff
changeset

371 

10515  372 
fun close_derivation thm = 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21603
diff
changeset

373 
if Thm.get_name thm = "" then Thm.put_name "" thm 
10515  374 
else thm; 
375 

21603  376 

377 
(* legacy standard operations *) 

378 

16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

379 
val standard' = 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

380 
implies_intr_hyps 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

381 
#> forall_intr_frees 
19421  382 
#> `Thm.maxidx_of 
16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

383 
#> (fn maxidx => 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

384 
forall_elim_vars (maxidx + 1) 
20904  385 
#> Thm.strip_shyps 
16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

386 
#> zero_var_indexes 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

387 
#> Thm.varifyT 
21600
222810ce6b05
*** bad commit  reverted to previous version ***
wenzelm
parents:
21596
diff
changeset

388 
#> Thm.compress); 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

389 

16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

390 
val standard = 
21600
222810ce6b05
*** bad commit  reverted to previous version ***
wenzelm
parents:
21596
diff
changeset

391 
flexflex_unique 
16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

392 
#> standard' 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

393 
#> close_derivation; 
11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

394 

0  395 

8328  396 
(*Convert all Vars in a theorem to Frees. Also return a function for 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

397 
reversing that operation. DOES NOT WORK FOR TYPE VARIABLES. 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

398 
Similar code in type/freeze_thaw*) 
15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

399 

50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

400 
fun freeze_thaw_robust th = 
19878  401 
let val fth = Thm.freezeT th 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

402 
val {prop, tpairs, thy, ...} = rep_thm fth 
15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

403 
in 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

404 
case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of 
15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

405 
[] => (fth, fn i => fn x => x) (*No vars: nothing to do!*) 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

406 
 vars => 
19753  407 
let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix)) 
408 
val alist = map newName vars 

15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

409 
fun mk_inst (Var(v,T)) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

410 
(cterm_of thy (Var(v,T)), 
17325  411 
cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) 
15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

412 
val insts = map mk_inst vars 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

413 
fun thaw i th' = (*i is nonnegative increment for Var indexes*) 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

414 
th' > forall_intr_list (map #2 insts) 
22906
195b7515911a
moved some operations to more_thm.ML and conv.ML;
wenzelm
parents:
22695
diff
changeset

415 
> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts) 
15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

416 
in (Thm.instantiate ([],insts) fth, thaw) end 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

417 
end; 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

418 

50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

419 
(*Basic version of the function above. No option to rename Vars apart in thaw. 
19999  420 
The Frees created from Vars have nice names. FIXME: does not check for 
19753  421 
clashes with variables in the assumptions, so delete and use freeze_thaw_robust instead?*) 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

422 
fun freeze_thaw th = 
19878  423 
let val fth = Thm.freezeT th 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

424 
val {prop, tpairs, thy, ...} = rep_thm fth 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

425 
in 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

426 
case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

427 
[] => (fth, fn x => x) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

428 
 vars => 
8328  429 
let fun newName (Var(ix,_), (pairs,used)) = 
20077
4fc9a4fef219
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19999
diff
changeset

430 
let val v = Name.variant used (string_of_indexname ix) 
8328  431 
in ((ix,v)::pairs, v::used) end; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

432 
val (alist, _) = foldr newName ([], Library.foldr add_term_names 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

433 
(prop :: Thm.terms_of_tpairs tpairs, [])) vars 
8328  434 
fun mk_inst (Var(v,T)) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

435 
(cterm_of thy (Var(v,T)), 
17325  436 
cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) 
8328  437 
val insts = map mk_inst vars 
438 
fun thaw th' = 

439 
th' > forall_intr_list (map #2 insts) 

440 
> forall_elim_list (map #1 insts) 

441 
in (Thm.instantiate ([],insts) fth, thaw) end 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

442 
end; 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

443 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

444 
(*Rotates a rule's premises to the left by k*) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

445 
val rotate_prems = permute_prems 0; 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

446 

11163  447 
(* permute prems, where the ith position in the argument list (counting from 0) 
448 
gives the position within the original thm to be transferred to position i. 

449 
Any remaining trailing positions are left unchanged. *) 

450 
val rearrange_prems = let 

451 
fun rearr new [] thm = thm 

11815  452 
 rearr new (p::ps) thm = rearr (new+1) 
11163  453 
(map (fn q => if new<=q andalso q<p then q+1 else q) ps) 
454 
(permute_prems (new+1) (newp) (permute_prems new (pnew) thm)) 

455 
in rearr 0 end; 

4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

456 

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

457 
(*Resolution: exactly one resolvent must be produced.*) 
0  458 
fun tha RSN (i,thb) = 
19861  459 
case Seq.chop 2 (biresolution false [(false,tha)] i thb) of 
0  460 
([th],_) => th 
461 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

463 

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

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

466 

467 
(*For joining lists of rules*) 

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

468 
fun thas RLN (i,thbs) = 
0  469 
let val resolve = biresolution false (map (pair false) thas) i 
4270  470 
fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19421
diff
changeset

471 
in maps resb thbs end; 
0  472 

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

474 

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

475 
(*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

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

477 
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

478 
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

479 
 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

480 
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

481 

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

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

483 
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

484 
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

485 
 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

486 
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

487 

9288
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
8605
diff
changeset

488 
(*A version of MRS with more appropriate argument order*) 
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
8605
diff
changeset

489 
fun bottom_rl OF rls = rls MRS bottom_rl; 
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
8605
diff
changeset

490 

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

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

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

494 
fun compose(tha,i,thb) = 
4270  495 
Seq.list_of (bicompose false (false,tha,0) i thb); 
0  496 

6946  497 
fun compose_single (tha,i,thb) = 
498 
(case compose (tha,i,thb) of 

499 
[th] => th 

500 
 _ => raise THM ("compose: unique result expected", i, [tha,thb])); 

501 

0  502 
(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) 
503 
fun tha COMP thb = 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22310
diff
changeset

504 
case distinct Thm.eq_thm (compose(tha,1,thb)) of 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

505 
[th] => th 
0  506 
 _ => raise THM("COMP", 1, [tha,thb]); 
507 

13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12908
diff
changeset

508 

4016  509 
(** theorem equality **) 
0  510 

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

16720  512 
val size_of_thm = size_of_term o Thm.full_prop_of; 
0  513 

9829  514 
(*maintain lists of theorems  preserving canonical order*) 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22310
diff
changeset

515 
val del_rule = remove Thm.eq_thm_prop; 
18922  516 
fun add_rule th = cons th o del_rule th; 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22310
diff
changeset

517 
val merge_rules = Library.merge Thm.eq_thm_prop; 
9829  518 

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

519 

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

520 

0  521 
(*** MetaRewriting Rules ***) 
522 

22681
9d42e5365ad1
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22561
diff
changeset

523 
fun read_prop s = Thm.read_cterm ProtoPure.thy (s, propT); 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

524 

9455  525 
fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm])); 
526 
fun store_standard_thm name thm = store_thm name (standard thm); 

12135  527 
fun store_thm_open name thm = hd (PureThy.smart_store_thms_open (name, [thm])); 
528 
fun store_standard_thm_open name thm = store_thm_open name (standard' thm); 

4016  529 

0  530 
val reflexive_thm = 
19421  531 
let val cx = cert (Var(("x",0),TVar(("'a",0),[]))) 
12135  532 
in store_standard_thm_open "reflexive" (Thm.reflexive cx) end; 
0  533 

534 
val symmetric_thm = 

14854  535 
let val xy = read_prop "x == y" 
16595  536 
in store_standard_thm_open "symmetric" (Thm.implies_intr xy (Thm.symmetric (Thm.assume xy))) end; 
0  537 

538 
val transitive_thm = 

14854  539 
let val xy = read_prop "x == y" 
540 
val yz = read_prop "y == z" 

0  541 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
12135  542 
in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 
0  543 

4679  544 
fun symmetric_fun thm = thm RS symmetric_thm; 
545 

11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

546 
fun extensional eq = 
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

547 
let val eq' = 
22906
195b7515911a
moved some operations to more_thm.ML and conv.ML;
wenzelm
parents:
22695
diff
changeset

548 
abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq 
11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

549 
in equal_elim (eta_conversion (cprop_of eq')) eq' end; 
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

550 

18820  551 
val equals_cong = 
552 
store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x == y")); 

553 

10414  554 
val imp_cong = 
555 
let 

556 
val ABC = read_prop "PROP A ==> PROP B == PROP C" 

557 
val AB = read_prop "PROP A ==> PROP B" 

558 
val AC = read_prop "PROP A ==> PROP C" 

559 
val A = read_prop "PROP A" 

560 
in 

12135  561 
store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr 
10414  562 
(implies_intr AB (implies_intr A 
563 
(equal_elim (implies_elim (assume ABC) (assume A)) 

564 
(implies_elim (assume AB) (assume A))))) 

565 
(implies_intr AC (implies_intr A 

566 
(equal_elim (symmetric (implies_elim (assume ABC) (assume A))) 

567 
(implies_elim (assume AC) (assume A))))))) 

568 
end; 

569 

570 
val swap_prems_eq = 

571 
let 

572 
val ABC = read_prop "PROP A ==> PROP B ==> PROP C" 

573 
val BAC = read_prop "PROP B ==> PROP A ==> PROP C" 

574 
val A = read_prop "PROP A" 

575 
val B = read_prop "PROP B" 

576 
in 

12135  577 
store_standard_thm_open "swap_prems_eq" (equal_intr 
10414  578 
(implies_intr ABC (implies_intr B (implies_intr A 
579 
(implies_elim (implies_elim (assume ABC) (assume A)) (assume B))))) 

580 
(implies_intr BAC (implies_intr A (implies_intr B 

581 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

582 
end; 

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

583 

22938  584 
val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies); 
585 

586 
fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th; (*AP_TERM*) 

587 
fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct); (*AP_THM*) 

0  588 

15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

589 
local 
22906
195b7515911a
moved some operations to more_thm.ML and conv.ML;
wenzelm
parents:
22695
diff
changeset

590 
val dest_eq = Thm.dest_equals o cprop_of 
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

591 
val rhs_of = snd o dest_eq 
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

592 
in 
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

593 
fun beta_eta_conversion t = 
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

594 
let val thm = beta_conversion true t 
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

595 
in transitive thm (eta_conversion (rhs_of thm)) end 
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

596 
end; 
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

597 

15925  598 
fun eta_long_conversion ct = transitive (beta_eta_conversion ct) 
599 
(symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct))); 

600 

20861  601 
(*Contract all etaredexes in the theorem, lest they give rise to needless abstractions*) 
602 
fun eta_contraction_rule th = 

603 
equal_elim (eta_conversion (cprop_of th)) th; 

604 

18337  605 
val abs_def = 
606 
let 

607 
fun contract_lhs th = 

22906
195b7515911a
moved some operations to more_thm.ML and conv.ML;
wenzelm
parents:
22695
diff
changeset

608 
Thm.transitive (Thm.symmetric (beta_eta_conversion 
195b7515911a
moved some operations to more_thm.ML and conv.ML;
wenzelm
parents:
22695
diff
changeset

609 
(fst (Thm.dest_equals (cprop_of th))))) th; 
18777  610 
fun abstract cx th = Thm.abstract_rule 
611 
(case Thm.term_of cx of Var ((x, _), _) => x  Free (x, _) => x  _ => "x") cx th 

612 
handle THM _ => raise THM ("Malformed definitional equation", 0, [th]); 

18337  613 
in 
614 
contract_lhs 

22906
195b7515911a
moved some operations to more_thm.ML and conv.ML;
wenzelm
parents:
22695
diff
changeset

615 
#> `(snd o strip_comb o fst o Thm.dest_equals o cprop_of) 
18337  616 
#> fold_rev abstract 
617 
#> contract_lhs 

618 
end; 

619 

18468  620 

15669  621 
(*** Some useful metatheorems ***) 
0  622 

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

12135  624 
val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi")); 
7380  625 
val _ = store_thm "_" asm_rl; 
0  626 

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

4016  628 
val cut_rl = 
12135  629 
store_standard_thm_open "cut_rl" 
9455  630 
(Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta")); 
0  631 

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

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

4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

635 
let val V = read_prop "PROP V" 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

636 
and VW = read_prop "PROP V ==> PROP W"; 
4016  637 
in 
12135  638 
store_standard_thm_open "revcut_rl" 
4016  639 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  640 
end; 
641 

668  642 
(*for deleting an unwanted assumption*) 
643 
val thin_rl = 

4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

644 
let val V = read_prop "PROP V" 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

645 
and W = read_prop "PROP W"; 
12135  646 
in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end; 
668  647 

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

4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

650 
let val V = read_prop "PROP V" 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

651 
and QV = read_prop "!!x::'a. PROP V" 
19421  652 
and x = cert (Free ("x", Term.aT [])); 
4016  653 
in 
12135  654 
store_standard_thm_open "triv_forall_equality" 
11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

655 
(equal_intr (implies_intr QV (forall_elim x (assume QV))) 
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

656 
(implies_intr V (forall_intr x (assume V)))) 
0  657 
end; 
658 

19051  659 
(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==> 
660 
(PROP ?Phi ==> PROP ?Psi) 

661 
*) 

662 
val distinct_prems_rl = 

663 
let 

664 
val AAB = read_prop "PROP Phi ==> PROP Phi ==> PROP Psi" 

665 
val A = read_prop "PROP Phi"; 

666 
in 

667 
store_standard_thm_open "distinct_prems_rl" 

668 
(implies_intr_list [AAB, A] (implies_elim_list (assume AAB) [assume A, assume A])) 

669 
end; 

670 

1756  671 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
672 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

674 
*) 

675 
val swap_prems_rl = 

4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

676 
let val cmajor = read_prop "PROP PhiA ==> PROP PhiB ==> PROP Psi"; 
1756  677 
val major = assume cmajor; 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

678 
val cminor1 = read_prop "PROP PhiA"; 
1756  679 
val minor1 = assume cminor1; 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

680 
val cminor2 = read_prop "PROP PhiB"; 
1756  681 
val minor2 = assume cminor2; 
12135  682 
in store_standard_thm_open "swap_prems_rl" 
1756  683 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
684 
(implies_elim (implies_elim major minor1) minor2)))) 

685 
end; 

686 

3653  687 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
688 
==> PROP ?phi == PROP ?psi 

8328  689 
Introduction rule for == as a metatheorem. 
3653  690 
*) 
691 
val equal_intr_rule = 

4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

692 
let val PQ = read_prop "PROP phi ==> PROP psi" 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

693 
and QP = read_prop "PROP psi ==> PROP phi" 
4016  694 
in 
12135  695 
store_standard_thm_open "equal_intr_rule" 
4016  696 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  697 
end; 
698 

19421  699 
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *) 
13368  700 
val equal_elim_rule1 = 
701 
let val eq = read_prop "PROP phi == PROP psi" 

702 
and P = read_prop "PROP phi" 

703 
in store_standard_thm_open "equal_elim_rule1" 

704 
(Thm.equal_elim (assume eq) (assume P) > implies_intr_list [eq, P]) 

705 
end; 

4285  706 

19421  707 
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *) 
708 
val equal_elim_rule2 = 

709 
store_standard_thm_open "equal_elim_rule2" (symmetric_thm RS equal_elim_rule1); 

710 

12297  711 
(* "[ PROP ?phi; PROP ?phi; PROP ?psi ] ==> PROP ?psi" *) 
712 
val remdups_rl = 

713 
let val P = read_prop "PROP phi" and Q = read_prop "PROP psi"; 

714 
in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end; 

715 

716 

9554  717 
(*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) 
12297  718 
Rewrite rule for HHF normalization.*) 
9554  719 

720 
val norm_hhf_eq = 

721 
let 

14854  722 
val aT = TFree ("'a", []); 
9554  723 
val all = Term.all aT; 
724 
val x = Free ("x", aT); 

725 
val phi = Free ("phi", propT); 

726 
val psi = Free ("psi", aT > propT); 

727 

728 
val cx = cert x; 

729 
val cphi = cert phi; 

730 
val lhs = cert (Logic.mk_implies (phi, all $ Abs ("x", aT, psi $ Bound 0))); 

731 
val rhs = cert (all $ Abs ("x", aT, Logic.mk_implies (phi, psi $ Bound 0))); 

732 
in 

733 
Thm.equal_intr 

734 
(Thm.implies_elim (Thm.assume lhs) (Thm.assume cphi) 

735 
> Thm.forall_elim cx 

736 
> Thm.implies_intr cphi 

737 
> Thm.forall_intr cx 

738 
> Thm.implies_intr lhs) 

739 
(Thm.implies_elim 

740 
(Thm.assume rhs > Thm.forall_elim cx) (Thm.assume cphi) 

741 
> Thm.forall_intr cx 

742 
> Thm.implies_intr cphi 

743 
> Thm.implies_intr rhs) 

12135  744 
> store_standard_thm_open "norm_hhf_eq" 
9554  745 
end; 
746 

18179  747 
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); 
748 

12800  749 
fun is_norm_hhf tm = 
750 
let 

751 
fun is_norm (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false 

752 
 is_norm (t $ u) = is_norm t andalso is_norm u 

753 
 is_norm (Abs (_, _, t)) = is_norm t 

754 
 is_norm _ = true; 

18929  755 
in is_norm (Envir.beta_eta_contract tm) end; 
12800  756 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

757 
fun norm_hhf thy t = 
12800  758 
if is_norm_hhf t then t 
18179  759 
else Pattern.rewrite_term thy [norm_hhf_prop] [] t; 
760 

20298  761 
fun norm_hhf_cterm ct = 
762 
if is_norm_hhf (Thm.term_of ct) then ct 

763 
else cterm_fun (Pattern.rewrite_term (Thm.theory_of_cterm ct) [norm_hhf_prop] []) ct; 

764 

12800  765 

21603  766 
(* var indexes *) 
767 

768 
fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1); 

769 

770 
fun incr_indexes2 th1 th2 = 

771 
Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1); 

772 

773 
fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2; 

774 
fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2; 

775 

9554  776 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

777 
(*** Instantiate theorem th, reading instantiations in theory thy ****) 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

778 

29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

779 
(*Version that normalizes the result: Thm.instantiate no longer does that*) 
21603  780 
fun instantiate instpair th = 
781 
Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); 

8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

782 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

783 
fun read_instantiate_sg' thy sinsts th = 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

784 
let val ts = types_sorts th; 
15669  785 
val used = add_used th []; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

786 
in instantiate (read_insts thy ts ts used sinsts) th end; 
15797  787 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

788 
fun read_instantiate_sg thy sinsts th = 
20298  789 
read_instantiate_sg' thy (map (apfst Syntax.read_indexname) sinsts) th; 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

790 

29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

791 
(*Instantiate theorem th, reading instantiations under theory of th*) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

792 
fun read_instantiate sinsts th = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

793 
read_instantiate_sg (Thm.theory_of_thm th) sinsts th; 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

794 

15797  795 
fun read_instantiate' sinsts th = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

796 
read_instantiate_sg' (Thm.theory_of_thm th) sinsts th; 
15797  797 

8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

798 

29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

799 
(*Lefttoright replacements: tpairs = [...,(vi,ti),...]. 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

800 
Instantiates distinct Vars by terms, inferring type instantiations. *) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

801 
local 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

802 
fun add_types ((ct,cu), (thy,tye,maxidx)) = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

803 
let val {thy=thyt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

804 
and {thy=thyu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu; 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

805 
val maxi = Int.max(maxidx, Int.max(maxt, maxu)); 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

806 
val thy' = Theory.merge(thy, Theory.merge(thyt, thyu)) 
16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

807 
val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) 
10403  808 
handle Type.TUNIFY => raise TYPE("Illtyped instantiation", [T,U], [t,u]) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

809 
in (thy', tye', maxi') end; 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

810 
in 
22561  811 
fun cterm_instantiate [] th = th 
812 
 cterm_instantiate ctpairs0 th = 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

813 
let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0 
18179  814 
fun instT(ct,cu) = 
22287
9985a79735c7
cterm_instantiate was calling a type instantiation function that works only for matching,
paulson
parents:
22109
diff
changeset

815 
let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of 
14340
bc93ffa674cc
correction to cterm_instantiate by Christoph Leuth
paulson
parents:
14081
diff
changeset

816 
in (inst ct, inst cu) end 
22307
bb31094b4879
Completing the bug fix from the previous update: the result of unifying type
paulson
parents:
22287
diff
changeset

817 
fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy (Envir.norm_type tye T)) 
8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
8365
diff
changeset

818 
in instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

819 
handle TERM _ => 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

820 
raise THM("cterm_instantiate: incompatible theories",0,[th]) 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

821 
 TYPE (msg, _, _) => raise THM(msg, 0, [th]) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

822 
end; 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

823 

29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

824 

19878  825 
(* global schematic variables *) 
826 

827 
fun unvarify th = 

828 
let 

829 
val thy = Thm.theory_of_thm th; 

830 
val cert = Thm.cterm_of thy; 

831 
val certT = Thm.ctyp_of thy; 

832 

833 
val prop = Thm.full_prop_of th; 

834 
val _ = map Logic.unvarify (prop :: Thm.hyps_of th) 

835 
handle TERM (msg, _) => raise THM (msg, 0, [th]); 

836 

837 
val instT0 = rev (Term.add_tvars prop []) > map (fn v as ((a, _), S) => (v, TFree (a, S))); 

838 
val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0; 

839 
val inst = rev (Term.add_vars prop []) > map (fn ((a, i), T) => 

20509  840 
let val T' = TermSubst.instantiateT instT0 T 
19878  841 
in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end); 
842 
in Thm.instantiate (instT, inst) th end; 

843 

844 

19775  845 
(** protected propositions and embedded terms **) 
4789  846 

847 
local 

18025  848 
val A = cert (Free ("A", propT)); 
19878  849 
val prop_def = unvarify ProtoPure.prop_def; 
850 
val term_def = unvarify ProtoPure.term_def; 

4789  851 
in 
18025  852 
val protect = Thm.capply (cert Logic.protectC); 
21437  853 
val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard 
18025  854 
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)))); 
21437  855 
val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard 
18025  856 
(Thm.equal_elim prop_def (Thm.assume (protect A))))); 
18179  857 
val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A)); 
19775  858 

21437  859 
val termI = store_thm "termI" (PureThy.kind_rule Thm.internalK (standard 
19775  860 
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))))); 
4789  861 
end; 
862 

18025  863 
fun implies_intr_protected asms th = 
18118  864 
let val asms' = map protect asms in 
865 
implies_elim_list 

866 
(implies_intr_list asms th) 

867 
(map (fn asm' => Thm.assume asm' RS protectD) asms') 

868 
> implies_intr_list asms' 

869 
end; 

11815  870 

19775  871 
fun mk_term ct = 
872 
let 

873 
val {thy, T, ...} = Thm.rep_cterm ct; 

874 
val cert = Thm.cterm_of thy; 

875 
val certT = Thm.ctyp_of thy; 

876 
val a = certT (TVar (("'a", 0), [])); 

877 
val x = cert (Var (("x", 0), T)); 

878 
in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end; 

879 

880 
fun dest_term th = 

21566  881 
let val cprop = strip_imp_concl (Thm.cprop_of th) in 
19775  882 
if can Logic.dest_term (Thm.term_of cprop) then 
20579  883 
Thm.dest_arg cprop 
19775  884 
else raise THM ("dest_term", 0, [th]) 
885 
end; 

886 

21519  887 
fun cterm_rule f = dest_term o f o mk_term; 
888 
fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t)); 

20881  889 

19775  890 

4789  891 

5688  892 
(** variations on instantiate **) 
4285  893 

894 
(* instantiate by lefttoright occurrence of variables *) 

895 

896 
fun instantiate' cTs cts thm = 

897 
let 

898 
fun err msg = 

899 
raise TYPE ("instantiate': " ^ msg, 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19421
diff
changeset

900 
map_filter (Option.map Thm.typ_of) cTs, 
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19421
diff
changeset

901 
map_filter (Option.map Thm.term_of) cts); 
4285  902 

903 
fun inst_of (v, ct) = 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

904 
(Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct) 
4285  905 
handle TYPE (msg, _, _) => err msg; 
906 

15797  907 
fun tyinst_of (v, cT) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

908 
(Thm.ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT) 
15797  909 
handle TYPE (msg, _, _) => err msg; 
910 

20298  911 
fun zip_vars xs ys = 
912 
zip_options xs ys handle Library.UnequalLengths => 

913 
err "more instantiations than variables in thm"; 

4285  914 

915 
(*instantiate types first!*) 

916 
val thm' = 

917 
if forall is_none cTs then thm 

20298  918 
else Thm.instantiate 
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

919 
(map tyinst_of (zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; 
20579  920 
val thm'' = 
4285  921 
if forall is_none cts then thm' 
20298  922 
else Thm.instantiate 
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22681
diff
changeset

923 
([], map inst_of (zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts)) thm'; 
20298  924 
in thm'' end; 
4285  925 

926 

14081  927 

928 
(** renaming of bound variables **) 

929 

930 
(* replace bound variables x_i in thm by y_i *) 

931 
(* where vs = [(x_1, y_1), ..., (x_n, y_n)] *) 

932 

933 
fun rename_bvars [] thm = thm 

934 
 rename_bvars vs thm = 

935 
let 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

936 
val {thy, prop, ...} = rep_thm thm; 
17325  937 
fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x > the_default x, T, ren t) 
14081  938 
 ren (t $ u) = ren t $ ren u 
939 
 ren t = t; 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

940 
in equal_elim (reflexive (cterm_of thy (ren prop))) thm end; 
14081  941 

942 

943 
(* renaming in lefttoright order *) 

944 

945 
fun rename_bvars' xs thm = 

946 
let 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

947 
val {thy, prop, ...} = rep_thm thm; 
14081  948 
fun rename [] t = ([], t) 
949 
 rename (x' :: xs) (Abs (x, T, t)) = 

950 
let val (xs', t') = rename xs t 

18929  951 
in (xs', Abs (the_default x x', T, t')) end 
14081  952 
 rename xs (t $ u) = 
953 
let 

954 
val (xs', t') = rename xs t; 

955 
val (xs'', u') = rename xs' u 

956 
in (xs'', t' $ u') end 

957 
 rename xs t = (xs, t); 

958 
in case rename xs prop of 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

959 
([], prop') => equal_elim (reflexive (cterm_of thy prop')) thm 
14081  960 
 _ => error "More names than abstractions in theorem" 
961 
end; 

962 

963 

11975  964 

18225  965 
(** multi_resolve **) 
966 

967 
local 

968 

969 
fun res th i rule = 

970 
Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty; 

971 

972 
fun multi_res _ [] rule = Seq.single rule 

973 
 multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule); 

974 

975 
in 

976 

977 
val multi_resolve = multi_res 1; 

978 
fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules); 

979 

980 
end; 

981 

11975  982 
end; 
5903  983 

984 
structure BasicDrule: BASIC_DRULE = Drule; 

985 
open BasicDrule; 