author  berghofe 
Tue, 27 Nov 2007 15:43:31 +0100  
changeset 25470  ba5a2bb7a81a 
parent 24978  159b0f4dd1e9 
child 26424  a6cad32a27b0 
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 
18468  96 
val imp_cong_rule: thm > thm > thm 
22939  97 
val arg_cong_rule: cterm > thm > thm 
23568  98 
val binop_cong_rule: cterm > thm > thm > thm 
22939  99 
val fun_cong_rule: thm > cterm > thm 
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

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

105 
val norm_hhf: theory > term > term 
20298  106 
val norm_hhf_cterm: cterm > cterm 
18025  107 
val protect: cterm > cterm 
108 
val protectI: thm 

109 
val protectD: thm 

18179  110 
val protect_cong: thm 
18025  111 
val implies_intr_protected: cterm list > thm > thm 
19775  112 
val termI: thm 
113 
val mk_term: cterm > thm 

114 
val dest_term: thm > cterm 

21519  115 
val cterm_rule: (thm > thm) > cterm > cterm 
20881  116 
val term_rule: theory > (thm > thm) > term > term 
24005  117 
val dummy_thm: thm 
19523  118 
val sort_triv: theory > typ * sort > thm list 
19504  119 
val unconstrainTs: thm > thm 
23423  120 
val with_subgoal: int > (thm > thm) > thm > thm 
14081  121 
val rename_bvars: (string * string) list > thm > thm 
122 
val rename_bvars': string option list > thm > thm 

24426  123 
val incr_type_indexes: int > 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 

24848  274 
> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []); 
19523  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*) 
24978
159b0f4dd1e9
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
wenzelm
parents:
24947
diff
changeset

340 
fun implies_elim_list impth ths = fold Thm.elim_implies ths impth; 
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 
23439  367 
case distinct Thm.eq_thm (Seq.list_of (flexflex_rule th)) of 
368 
[th] => th 

369 
 [] => raise THM("flexflex_unique: impossible constraints", 0, [th]) 

370 
 _ => raise THM("flexflex_unique: multiple unifiers", 0, [th]); 

14387
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 
23178  404 
case List.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 
23178  426 
case List.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; 
23178  432 
val (alist, _) = List.foldr newName ([], Library.foldr add_term_names 
15574
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*) 
23537  445 
fun rotate_prems 0 = I 
446 
 rotate_prems k = permute_prems 0 k; 

447 

23423  448 
fun with_subgoal i f = rotate_prems (i  1) #> f #> rotate_prems (1  i); 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

449 

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

452 
Any remaining trailing positions are left unchanged. *) 

453 
val rearrange_prems = let 

454 
fun rearr new [] thm = thm 

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

458 
in rearr 0 end; 

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

459 

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

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

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

466 

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

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

469 

470 
(*For joining lists of rules*) 

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

471 
fun thas RLN (i,thbs) = 
0  472 
let val resolve = biresolution false (map (pair false) thas) i 
4270  473 
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

474 
in maps resb thbs end; 
0  475 

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

477 

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

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

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

480 
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

481 
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

482 
 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

483 
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

484 

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

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

486 
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

487 
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

488 
 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

489 
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

490 

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

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

492 
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

493 

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

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

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

497 
fun compose(tha,i,thb) = 
24426  498 
distinct Thm.eq_thm (Seq.list_of (bicompose false (false,tha,0) i thb)); 
0  499 

6946  500 
fun compose_single (tha,i,thb) = 
24426  501 
case compose (tha,i,thb) of 
6946  502 
[th] => th 
24426  503 
 _ => raise THM ("compose: unique result expected", i, [tha,thb]); 
6946  504 

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

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

508 
[th] => th 
0  509 
 _ => raise THM("COMP", 1, [tha,thb]); 
510 

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

511 

4016  512 
(** theorem equality **) 
0  513 

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

16720  515 
val size_of_thm = size_of_term o Thm.full_prop_of; 
0  516 

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

517 

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

518 

0  519 
(*** MetaRewriting Rules ***) 
520 

24241  521 
val read_prop = Thm.cterm_of ProtoPure.thy o SimpleSyntax.read_prop; 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

522 

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

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

4016  527 

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

532 
val symmetric_thm = 

24241  533 
let val xy = read_prop "x::'a == y::'a" 
16595  534 
in store_standard_thm_open "symmetric" (Thm.implies_intr xy (Thm.symmetric (Thm.assume xy))) end; 
0  535 

536 
val transitive_thm = 

24241  537 
let val xy = read_prop "x::'a == y::'a" 
538 
val yz = read_prop "y::'a == z::'a" 

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

4679  542 
fun symmetric_fun thm = thm RS symmetric_thm; 
543 

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

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

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

546 
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

547 
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

548 

18820  549 
val equals_cong = 
24241  550 
store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x::'a == y::'a")); 
18820  551 

10414  552 
val imp_cong = 
553 
let 

24241  554 
val ABC = read_prop "A ==> B::prop == C::prop" 
555 
val AB = read_prop "A ==> B" 

556 
val AC = read_prop "A ==> C" 

557 
val A = read_prop "A" 

10414  558 
in 
12135  559 
store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr 
10414  560 
(implies_intr AB (implies_intr A 
561 
(equal_elim (implies_elim (assume ABC) (assume A)) 

562 
(implies_elim (assume AB) (assume A))))) 

563 
(implies_intr AC (implies_intr A 

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

565 
(implies_elim (assume AC) (assume A))))))) 

566 
end; 

567 

568 
val swap_prems_eq = 

569 
let 

24241  570 
val ABC = read_prop "A ==> B ==> C" 
571 
val BAC = read_prop "B ==> A ==> C" 

572 
val A = read_prop "A" 

573 
val B = read_prop "B" 

10414  574 
in 
12135  575 
store_standard_thm_open "swap_prems_eq" (equal_intr 
10414  576 
(implies_intr ABC (implies_intr B (implies_intr A 
577 
(implies_elim (implies_elim (assume ABC) (assume A)) (assume B))))) 

578 
(implies_intr BAC (implies_intr A (implies_intr B 

579 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

580 
end; 

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

581 

22938  582 
val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies); 
583 

23537  584 
fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th; (*AP_TERM in LCF/HOL*) 
585 
fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct); (*AP_THM in LCF/HOL*) 

23568  586 
fun binop_cong_rule ct th1 th2 = Thm.combination (arg_cong_rule ct th1) th2; 
0  587 

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

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

589 
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

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

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

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

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

594 
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

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

596 

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

599 

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

602 
equal_elim (eta_conversion (cprop_of th)) th; 

603 

24947
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

604 

b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

605 
(* abs_def *) 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

606 

b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

607 
(* 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

608 
f ?x1 ... ?xn == u 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

609 
 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

610 
f == %x1 ... xn. u 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

611 
*) 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

612 

b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

613 
local 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

614 

b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

615 
fun contract_lhs th = 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

616 
Thm.transitive (Thm.symmetric (beta_eta_conversion 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

617 
(fst (Thm.dest_equals (cprop_of th))))) th; 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

618 

b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

619 
fun var_args ct = 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

620 
(case try Thm.dest_comb ct of 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

621 
SOME (f, arg) => 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

622 
(case Thm.term_of arg of 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

623 
Var ((x, _), _) => update (eq_snd (op aconvc)) (x, arg) (var_args f) 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

624 
 _ => []) 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

625 
 NONE => []); 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

626 

b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

627 
in 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

628 

b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

629 
fun abs_def th = 
18337  630 
let 
24947
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

631 
val th' = contract_lhs th; 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

632 
val args = var_args (Thm.lhs_of th'); 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

633 
in contract_lhs (fold (uncurry Thm.abstract_rule) args th') end; 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

634 

b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

635 
end; 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

636 

18337  637 

18468  638 

15669  639 
(*** Some useful metatheorems ***) 
0  640 

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

24241  642 
val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi")); 
7380  643 
val _ = store_thm "_" asm_rl; 
0  644 

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

4016  646 
val cut_rl = 
12135  647 
store_standard_thm_open "cut_rl" 
24241  648 
(Thm.trivial (read_prop "?psi ==> ?theta")); 
0  649 

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

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

24241  653 
let val V = read_prop "V" 
654 
and VW = read_prop "V ==> W"; 

4016  655 
in 
12135  656 
store_standard_thm_open "revcut_rl" 
4016  657 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  658 
end; 
659 

668  660 
(*for deleting an unwanted assumption*) 
661 
val thin_rl = 

24241  662 
let val V = read_prop "V" 
663 
and W = read_prop "W"; 

12135  664 
in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end; 
668  665 

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

24241  668 
let val V = read_prop "V" 
669 
and QV = read_prop "!!x::'a. V" 

19421  670 
and x = cert (Free ("x", Term.aT [])); 
4016  671 
in 
12135  672 
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

673 
(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

674 
(implies_intr V (forall_intr x (assume V)))) 
0  675 
end; 
676 

19051  677 
(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==> 
678 
(PROP ?Phi ==> PROP ?Psi) 

679 
*) 

680 
val distinct_prems_rl = 

681 
let 

24241  682 
val AAB = read_prop "Phi ==> Phi ==> Psi" 
683 
val A = read_prop "Phi"; 

19051  684 
in 
685 
store_standard_thm_open "distinct_prems_rl" 

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

687 
end; 

688 

1756  689 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
690 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

692 
*) 

693 
val swap_prems_rl = 

24241  694 
let val cmajor = read_prop "PhiA ==> PhiB ==> Psi"; 
1756  695 
val major = assume cmajor; 
24241  696 
val cminor1 = read_prop "PhiA"; 
1756  697 
val minor1 = assume cminor1; 
24241  698 
val cminor2 = read_prop "PhiB"; 
1756  699 
val minor2 = assume cminor2; 
12135  700 
in store_standard_thm_open "swap_prems_rl" 
1756  701 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
702 
(implies_elim (implies_elim major minor1) minor2)))) 

703 
end; 

704 

3653  705 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
706 
==> PROP ?phi == PROP ?psi 

8328  707 
Introduction rule for == as a metatheorem. 
3653  708 
*) 
709 
val equal_intr_rule = 

24241  710 
let val PQ = read_prop "phi ==> psi" 
711 
and QP = read_prop "psi ==> phi" 

4016  712 
in 
12135  713 
store_standard_thm_open "equal_intr_rule" 
4016  714 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  715 
end; 
716 

19421  717 
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *) 
13368  718 
val equal_elim_rule1 = 
24241  719 
let val eq = read_prop "phi::prop == psi::prop" 
720 
and P = read_prop "phi" 

13368  721 
in store_standard_thm_open "equal_elim_rule1" 
722 
(Thm.equal_elim (assume eq) (assume P) > implies_intr_list [eq, P]) 

723 
end; 

4285  724 

19421  725 
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *) 
726 
val equal_elim_rule2 = 

727 
store_standard_thm_open "equal_elim_rule2" (symmetric_thm RS equal_elim_rule1); 

728 

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

24241  731 
let val P = read_prop "phi" and Q = read_prop "psi"; 
12297  732 
in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end; 
733 

734 

9554  735 
(*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) 
12297  736 
Rewrite rule for HHF normalization.*) 
9554  737 

738 
val norm_hhf_eq = 

739 
let 

14854  740 
val aT = TFree ("'a", []); 
9554  741 
val all = Term.all aT; 
742 
val x = Free ("x", aT); 

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

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

745 

746 
val cx = cert x; 

747 
val cphi = cert phi; 

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

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

750 
in 

751 
Thm.equal_intr 

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

753 
> Thm.forall_elim cx 

754 
> Thm.implies_intr cphi 

755 
> Thm.forall_intr cx 

756 
> Thm.implies_intr lhs) 

757 
(Thm.implies_elim 

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

759 
> Thm.forall_intr cx 

760 
> Thm.implies_intr cphi 

761 
> Thm.implies_intr rhs) 

12135  762 
> store_standard_thm_open "norm_hhf_eq" 
9554  763 
end; 
764 

18179  765 
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); 
766 

12800  767 
fun is_norm_hhf tm = 
768 
let 

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

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

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

772 
 is_norm _ = true; 

18929  773 
in is_norm (Envir.beta_eta_contract tm) end; 
12800  774 

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

775 
fun norm_hhf thy t = 
12800  776 
if is_norm_hhf t then t 
18179  777 
else Pattern.rewrite_term thy [norm_hhf_prop] [] t; 
778 

20298  779 
fun norm_hhf_cterm ct = 
780 
if is_norm_hhf (Thm.term_of ct) then ct 

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

782 

12800  783 

21603  784 
(* var indexes *) 
785 

24426  786 
(*Increment the indexes of only the type variables*) 
787 
fun incr_type_indexes inc th = 

788 
let val tvs = term_tvars (prop_of th) 

789 
and thy = theory_of_thm th 

790 
fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s)) 

791 
in Thm.instantiate (map inc_tvar tvs, []) th end; 

792 

21603  793 
fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1); 
794 

795 
fun incr_indexes2 th1 th2 = 

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

797 

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

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

800 

9554  801 

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

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

803 

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

804 
(*Version that normalizes the result: Thm.instantiate no longer does that*) 
21603  805 
fun instantiate instpair th = 
806 
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

807 

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

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

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

811 
in instantiate (read_insts thy ts ts used sinsts) th end; 
15797  812 

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

813 
fun read_instantiate_sg thy sinsts th = 
20298  814 
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

815 

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

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

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

818 
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

819 

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

821 
read_instantiate_sg' (Thm.theory_of_thm th) sinsts th; 
15797  822 

8129
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 
(*Lefttoright replacements: tpairs = [...,(vi,ti),...]. 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

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

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

828 
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

829 
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

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

831 
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

832 
val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) 
25470  833 
handle Type.TUNIFY => raise TYPE ("Illtyped instantiation:\nType\n" ^ 
834 
Sign.string_of_typ thy' (Envir.norm_type tye T) ^ 

835 
"\nof variable " ^ 

836 
Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) t) ^ 

837 
"\ncannot be unified with type\n" ^ 

838 
Sign.string_of_typ thy' (Envir.norm_type tye U) ^ "\nof term " ^ 

839 
Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) u), 

840 
[T, U], [t, u]) 

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

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

842 
in 
22561  843 
fun cterm_instantiate [] th = th 
844 
 cterm_instantiate ctpairs0 th = 

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

847 
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

848 
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

849 
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

850 
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

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

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

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

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

855 

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

856 

19775  857 
(** protected propositions and embedded terms **) 
4789  858 

859 
local 

18025  860 
val A = cert (Free ("A", propT)); 
24978
159b0f4dd1e9
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
wenzelm
parents:
24947
diff
changeset

861 
val prop_def = Thm.unvarify ProtoPure.prop_def; 
159b0f4dd1e9
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
wenzelm
parents:
24947
diff
changeset

862 
val term_def = Thm.unvarify ProtoPure.term_def; 
4789  863 
in 
18025  864 
val protect = Thm.capply (cert Logic.protectC); 
21437  865 
val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard 
18025  866 
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)))); 
21437  867 
val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard 
18025  868 
(Thm.equal_elim prop_def (Thm.assume (protect A))))); 
18179  869 
val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A)); 
19775  870 

21437  871 
val termI = store_thm "termI" (PureThy.kind_rule Thm.internalK (standard 
19775  872 
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))))); 
4789  873 
end; 
874 

18025  875 
fun implies_intr_protected asms th = 
18118  876 
let val asms' = map protect asms in 
877 
implies_elim_list 

878 
(implies_intr_list asms th) 

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

880 
> implies_intr_list asms' 

881 
end; 

11815  882 

19775  883 
fun mk_term ct = 
884 
let 

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

886 
val cert = Thm.cterm_of thy; 

887 
val certT = Thm.ctyp_of thy; 

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

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

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

891 

892 
fun dest_term th = 

21566  893 
let val cprop = strip_imp_concl (Thm.cprop_of th) in 
19775  894 
if can Logic.dest_term (Thm.term_of cprop) then 
20579  895 
Thm.dest_arg cprop 
19775  896 
else raise THM ("dest_term", 0, [th]) 
897 
end; 

898 

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

20881  901 

24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
24005
diff
changeset

902 
val dummy_thm = mk_term (Thm.cterm_of ProtoPure.thy (Term.dummy_pattern propT)); 
24005  903 

904 

4789  905 

5688  906 
(** variations on instantiate **) 
4285  907 

908 
(* instantiate by lefttoright occurrence of variables *) 

909 

910 
fun instantiate' cTs cts thm = 

911 
let 

912 
fun err msg = 

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

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

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

915 
map_filter (Option.map Thm.term_of) cts); 
4285  916 

917 
fun inst_of (v, ct) = 

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

918 
(Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct) 
4285  919 
handle TYPE (msg, _, _) => err msg; 
920 

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

922 
(Thm.ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT) 
15797  923 
handle TYPE (msg, _, _) => err msg; 
924 

20298  925 
fun zip_vars xs ys = 
926 
zip_options xs ys handle Library.UnequalLengths => 

927 
err "more instantiations than variables in thm"; 

4285  928 

929 
(*instantiate types first!*) 

930 
val thm' = 

931 
if forall is_none cTs then thm 

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

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

937 
([], map inst_of (zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts)) thm'; 
20298  938 
in thm'' end; 
4285  939 

940 

14081  941 

942 
(** renaming of bound variables **) 

943 

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

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

946 

947 
fun rename_bvars [] thm = thm 

948 
 rename_bvars vs thm = 

949 
let 

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

950 
val {thy, prop, ...} = rep_thm thm; 
17325  951 
fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x > the_default x, T, ren t) 
14081  952 
 ren (t $ u) = ren t $ ren u 
953 
 ren t = t; 

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

954 
in equal_elim (reflexive (cterm_of thy (ren prop))) thm end; 
14081  955 

956 

957 
(* renaming in lefttoright order *) 

958 

959 
fun rename_bvars' xs thm = 

960 
let 

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

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

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

18929  965 
in (xs', Abs (the_default x x', T, t')) end 
14081  966 
 rename xs (t $ u) = 
967 
let 

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

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

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

971 
 rename xs t = (xs, t); 

972 
in case rename xs prop of 

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

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

976 

977 

11975  978 

18225  979 
(** multi_resolve **) 
980 

981 
local 

982 

983 
fun res th i rule = 

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

985 

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

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

988 

989 
in 

990 

991 
val multi_resolve = multi_res 1; 

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

993 

994 
end; 

995 

11975  996 
end; 
5903  997 

998 
structure BasicDrule: BASIC_DRULE = Drule; 

999 
open BasicDrule; 