author  wenzelm 
Tue, 15 Apr 2008 16:12:05 +0200  
changeset 26653  60e0cf6bef89 
parent 26627  dac6d56b7c8d 
child 26939  1035c89b4c02 
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 gen_all: thm > thm 

29 
val lift_all: cterm > thm > thm 

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

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

31 
val freeze_thaw_robust: thm > thm * (int > thm > thm) 
18179  32 
val implies_elim_list: thm > thm list > thm 
33 
val implies_intr_list: cterm list > thm > thm 

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

38 
val standard: thm > thm 

39 
val standard': thm > thm 

40 
val rotate_prems: int > thm > thm 

41 
val rearrange_prems: int list > thm > thm 

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

43 
val RS: thm * thm > thm 

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

45 
val RL: thm list * thm list > thm list 

46 
val MRS: thm list * thm > thm 

47 
val MRL: thm list list * thm list > thm list 

48 
val OF: thm * thm list > thm 

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

50 
val COMP: thm * thm > thm 

21578  51 
val INCR_COMP: thm * thm > thm 
52 
val COMP_INCR: thm * thm > thm 

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

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

56 
val size_of_thm: thm > int 

57 
val reflexive_thm: thm 

58 
val symmetric_thm: thm 

59 
val transitive_thm: thm 

60 
val symmetric_fun: thm > thm 

61 
val extensional: thm > thm 

18820  62 
val equals_cong: thm 
18179  63 
val imp_cong: thm 
64 
val swap_prems_eq: thm 

65 
val asm_rl: thm 

66 
val cut_rl: thm 

67 
val revcut_rl: thm 

68 
val thin_rl: thm 

4285  69 
val triv_forall_equality: thm 
19051  70 
val distinct_prems_rl: thm 
18179  71 
val swap_prems_rl: thm 
72 
val equal_intr_rule: thm 

73 
val equal_elim_rule1: thm 

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

78 
signature DRULE = 

79 
sig 

80 
include BASIC_DRULE 

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

83 
val strip_comb: cterm > cterm * cterm list 
15262  84 
val strip_type: ctyp > ctyp list * ctyp 
15949  85 
val beta_conv: cterm > cterm > cterm 
15669  86 
val add_used: thm > string list > string list 
17713  87 
val flexflex_unique: thm > thm 
19421  88 
val store_thm: bstring > thm > thm 
89 
val store_standard_thm: bstring > thm > thm 

90 
val store_thm_open: bstring > thm > thm 

91 
val store_standard_thm_open: bstring > thm > thm 

11975  92 
val compose_single: thm * int * thm > thm 
18468  93 
val imp_cong_rule: thm > thm > thm 
22939  94 
val arg_cong_rule: cterm > thm > thm 
23568  95 
val binop_cong_rule: cterm > thm > thm > thm 
22939  96 
val fun_cong_rule: thm > cterm > thm 
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

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

102 
val norm_hhf: theory > term > term 
20298  103 
val norm_hhf_cterm: cterm > cterm 
18025  104 
val protect: cterm > cterm 
105 
val protectI: thm 

106 
val protectD: thm 

18179  107 
val protect_cong: thm 
18025  108 
val implies_intr_protected: cterm list > thm > thm 
19775  109 
val termI: thm 
110 
val mk_term: cterm > thm 

111 
val dest_term: thm > cterm 

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

24426  120 
val incr_type_indexes: int > thm > thm 
19124  121 
val incr_indexes: thm > thm > thm 
122 
val incr_indexes2: thm > thm > thm > thm 

12297  123 
val remdups_rl: thm 
18225  124 
val multi_resolve: thm list > thm > thm Seq.seq 
125 
val multi_resolves: thm list > thm list > thm Seq.seq 

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

127 
val read_instantiate_sg': theory > (indexname * string) list > thm > thm 
15797  128 
val read_instantiate': (indexname * string) list > thm > thm 
3766  129 
end; 
0  130 

5903  131 
structure Drule: DRULE = 
0  132 
struct 
133 

3991  134 

16682  135 
(** 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

136 

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

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

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

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

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

142 

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

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

144 
fun strip_imp_concl ct = 
20579  145 
(case Thm.term_of ct of 
146 
Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct) 

147 
 _ => ct); 

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

148 

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

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

150 
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

151 

26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

152 
fun cterm_fun f ct = Thm.cterm_of (Thm.theory_of_cterm ct) (f (Thm.term_of ct)); 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

153 
fun ctyp_fun f cT = Thm.ctyp_of (Thm.theory_of_ctyp cT) (f (Thm.typ_of cT)); 
15797  154 

26487  155 
fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t; 
9547  156 

26487  157 
val implies = certify Term.implies; 
19183  158 
fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B; 
9547  159 

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

161 
fun list_implies([], B) = B 

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

163 

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

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

167 

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

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

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

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

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

173 
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

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

175 

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

178 
Type ("fun", _) => 

179 
let 

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

181 
val (cTs, cT') = strip_type cT2 

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

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

184 

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

18179  187 
fun beta_conv x y = 
20579  188 
Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.capply x y))); 
15949  189 

15875  190 

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

191 

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

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

193 

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

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

195 
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

196 

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

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

198 
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

199 

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

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

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

203 
(case Symbol.explode a of "'" :: _ => true  _ => false); 
15570  204 
val (tvs, vs) = List.partition is_tv insts; 
15797  205 
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

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

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

209 
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

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

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

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

213 
fun mkty(ixn,st) = (case rtypes ixn of 
15531  214 
SOME T => (ixn,(st,typ_subst_TVars tye T)) 
215 
 NONE => absent ixn); 

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

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

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

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

219 
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

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

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

222 
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

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

224 
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

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

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

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

228 

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

229 

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

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

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

234 
***) 

235 

236 
fun types_sorts thm = 

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

238 
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

239 
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

240 
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

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

244 
fun sorts (a, i) = 

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

246 
in (types, sorts) end; 

0  247 

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

249 
(Thm.fold_terms o fold_types o fold_atyps) 
20329  250 
(fn TFree (a, _) => insert (op =) a 
251 
 TVar ((a, _), _) => insert (op =) a 

252 
 _ => I); 

15669  253 

7636  254 

9455  255 

0  256 
(** Standardization of rules **) 
257 

19523  258 
(* type classes and sorts *) 
259 

260 
fun sort_triv thy (T, S) = 

261 
let 

262 
val certT = Thm.ctyp_of thy; 

263 
val cT = certT T; 

264 
fun class_triv c = 

265 
Thm.class_triv thy c 

24848  266 
> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []); 
19523  267 
in map class_triv S end; 
268 

19504  269 
fun unconstrainTs th = 
20298  270 
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

271 
(Thm.fold_terms Term.add_tvars th []) th; 
19504  272 

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

0  275 

276 
(*Generalization over all suitable Free variables*) 

277 
fun forall_intr_frees th = 

19730  278 
let 
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

279 
val thy = Thm.theory_of_thm th; 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

280 
val {prop, hyps, tpairs, ...} = rep_thm th; 
19730  281 
val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) []; 
282 
val frees = Term.fold_aterms (fn Free v => 

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

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

0  285 

18535  286 
(*Generalization over Vars  canonical order*) 
287 
fun forall_intr_vars th = 

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

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

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

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

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

295 
(*generalize outermost parameters*) 

296 
fun gen_all th = 

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

297 
let 
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

298 
val thy = Thm.theory_of_thm th; 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

299 
val {prop, maxidx, ...} = Thm.rep_thm th; 
18025  300 
val cert = Thm.cterm_of thy; 
301 
fun elim (x, T) = Thm.forall_elim (cert (Var ((x, maxidx + 1), T))); 

302 
in fold elim (outer_params prop) th end; 

303 

304 
(*lift vars wrt. outermost goal parameters 

18118  305 
 reverses the effect of gen_all modulo higherorder unification*) 
18025  306 
fun lift_all goal th = 
307 
let 

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

309 
val cert = Thm.cterm_of thy; 

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

313 
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

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

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

318 
> fold_rev (Thm.forall_intr o cert) ps 

319 
end; 

320 

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

9554  323 

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

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

325 
val forall_elim_list = fold forall_elim; 
0  326 

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

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

328 
val implies_intr_list = fold_rev implies_intr; 
0  329 

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

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

331 
fun implies_elim_list impth ths = fold Thm.elim_implies ths impth; 
0  332 

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

21603  334 
fun zero_var_indexes_list [] = [] 
335 
 zero_var_indexes_list ths = 

336 
let 

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

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

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

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

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

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

343 

344 
val zero_var_indexes = singleton zero_var_indexes_list; 

0  345 

346 

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

10515  349 

16595  350 
(*Discharge all hypotheses.*) 
351 
fun implies_intr_hyps th = 

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

353 

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

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

356 
fun flexflex_unique th = 
17713  357 
if null (tpairs_of th) then th else 
23439  358 
case distinct Thm.eq_thm (Seq.list_of (flexflex_rule th)) of 
359 
[th] => th 

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

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

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

362 

21603  363 

364 
(* legacy standard operations *) 

365 

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

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

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

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

370 
#> (fn maxidx => 
26653  371 
Thm.forall_elim_vars (maxidx + 1) 
20904  372 
#> Thm.strip_shyps 
16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

373 
#> zero_var_indexes 
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

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

375 

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

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

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

378 
#> standard' 
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

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

380 

0  381 

8328  382 
(*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

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

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

385 

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

386 
fun freeze_thaw_robust th = 
19878  387 
let val fth = Thm.freezeT th 
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

388 
val thy = Thm.theory_of_thm fth 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

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

390 
in 
23178  391 
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

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

393 
 vars => 
19753  394 
let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix)) 
395 
val alist = map newName vars 

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

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

397 
(cterm_of thy (Var(v,T)), 
17325  398 
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

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

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

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

402 
> 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

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

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

405 

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

406 
(*Basic version of the function above. No option to rename Vars apart in thaw. 
19999  407 
The Frees created from Vars have nice names. FIXME: does not check for 
19753  408 
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

409 
fun freeze_thaw th = 
19878  410 
let val fth = Thm.freezeT th 
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

411 
val thy = Thm.theory_of_thm fth 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

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

413 
in 
23178  414 
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

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

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

418 
let val v = Name.variant used (string_of_indexname ix) 
8328  419 
in ((ix,v)::pairs, v::used) end; 
23178  420 
val (alist, _) = List.foldr newName ([], Library.foldr add_term_names 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

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

423 
(cterm_of thy (Var(v,T)), 
17325  424 
cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) 
8328  425 
val insts = map mk_inst vars 
426 
fun thaw th' = 

427 
th' > forall_intr_list (map #2 insts) 

428 
> forall_elim_list (map #1 insts) 

429 
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

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

431 

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

432 
(*Rotates a rule's premises to the left by k*) 
23537  433 
fun rotate_prems 0 = I 
434 
 rotate_prems k = permute_prems 0 k; 

435 

23423  436 
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

437 

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

440 
Any remaining trailing positions are left unchanged. *) 

441 
val rearrange_prems = let 

442 
fun rearr new [] thm = thm 

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

446 
in rearr 0 end; 

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

447 

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

448 
(*Resolution: exactly one resolvent must be produced.*) 
0  449 
fun tha RSN (i,thb) = 
19861  450 
case Seq.chop 2 (biresolution false [(false,tha)] i thb) of 
0  451 
([th],_) => th 
452 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

454 

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

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

457 

458 
(*For joining lists of rules*) 

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

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

462 
in maps resb thbs end; 
0  463 

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

465 

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

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

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

468 
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

469 
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

470 
 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

471 
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

472 

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

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

474 
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

475 
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

476 
 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

477 
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

478 

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

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

480 
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

481 

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

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

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

485 
fun compose(tha,i,thb) = 
24426  486 
distinct Thm.eq_thm (Seq.list_of (bicompose false (false,tha,0) i thb)); 
0  487 

6946  488 
fun compose_single (tha,i,thb) = 
24426  489 
case compose (tha,i,thb) of 
6946  490 
[th] => th 
24426  491 
 _ => raise THM ("compose: unique result expected", i, [tha,thb]); 
6946  492 

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

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

496 
[th] => th 
0  497 
 _ => raise THM("COMP", 1, [tha,thb]); 
498 

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

499 

4016  500 
(** theorem equality **) 
0  501 

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

16720  503 
val size_of_thm = size_of_term o Thm.full_prop_of; 
0  504 

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

505 

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

506 

0  507 
(*** MetaRewriting Rules ***) 
508 

26487  509 
val read_prop = certify o SimpleSyntax.read_prop; 
510 

511 
fun store_thm name th = 

512 
Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th))); 

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

513 

26487  514 
fun store_thm_open name th = 
515 
Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th))); 

516 

517 
fun store_standard_thm name th = store_thm name (standard th); 

12135  518 
fun store_standard_thm_open name thm = store_thm_open name (standard' thm); 
4016  519 

0  520 
val reflexive_thm = 
26487  521 
let val cx = certify (Var(("x",0),TVar(("'a",0),[]))) 
12135  522 
in store_standard_thm_open "reflexive" (Thm.reflexive cx) end; 
0  523 

524 
val symmetric_thm = 

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

528 
val transitive_thm = 

24241  529 
let val xy = read_prop "x::'a == y::'a" 
530 
val yz = read_prop "y::'a == z::'a" 

0  531 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
12135  532 
in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 
0  533 

4679  534 
fun symmetric_fun thm = thm RS symmetric_thm; 
535 

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

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

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

538 
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

539 
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

540 

18820  541 
val equals_cong = 
24241  542 
store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x::'a == y::'a")); 
18820  543 

10414  544 
val imp_cong = 
545 
let 

24241  546 
val ABC = read_prop "A ==> B::prop == C::prop" 
547 
val AB = read_prop "A ==> B" 

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

549 
val A = read_prop "A" 

10414  550 
in 
12135  551 
store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr 
10414  552 
(implies_intr AB (implies_intr A 
553 
(equal_elim (implies_elim (assume ABC) (assume A)) 

554 
(implies_elim (assume AB) (assume A))))) 

555 
(implies_intr AC (implies_intr A 

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

557 
(implies_elim (assume AC) (assume A))))))) 

558 
end; 

559 

560 
val swap_prems_eq = 

561 
let 

24241  562 
val ABC = read_prop "A ==> B ==> C" 
563 
val BAC = read_prop "B ==> A ==> C" 

564 
val A = read_prop "A" 

565 
val B = read_prop "B" 

10414  566 
in 
12135  567 
store_standard_thm_open "swap_prems_eq" (equal_intr 
10414  568 
(implies_intr ABC (implies_intr B (implies_intr A 
569 
(implies_elim (implies_elim (assume ABC) (assume A)) (assume B))))) 

570 
(implies_intr BAC (implies_intr A (implies_intr B 

571 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

572 
end; 

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

573 

22938  574 
val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies); 
575 

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

23568  578 
fun binop_cong_rule ct th1 th2 = Thm.combination (arg_cong_rule ct th1) th2; 
0  579 

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

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

581 
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

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

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

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

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

586 
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

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

588 

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

591 

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

594 
equal_elim (eta_conversion (cprop_of th)) th; 

595 

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

596 

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

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

598 

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

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

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

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

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

603 
*) 
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 
local 
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 
fun contract_lhs th = 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

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

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

610 

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

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

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

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

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

615 
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

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

617 
 NONE => []); 
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 
in 
b7e990e1706a
improved abs_def: only abstract over outermost (unique) Vars;
wenzelm
parents:
24848
diff
changeset

620 

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

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

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

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

625 
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

626 

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

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

628 

18337  629 

18468  630 

15669  631 
(*** Some useful metatheorems ***) 
0  632 

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

24241  634 
val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi")); 
7380  635 
val _ = store_thm "_" asm_rl; 
0  636 

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

4016  638 
val cut_rl = 
12135  639 
store_standard_thm_open "cut_rl" 
24241  640 
(Thm.trivial (read_prop "?psi ==> ?theta")); 
0  641 

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

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

24241  645 
let val V = read_prop "V" 
646 
and VW = read_prop "V ==> W"; 

4016  647 
in 
12135  648 
store_standard_thm_open "revcut_rl" 
4016  649 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  650 
end; 
651 

668  652 
(*for deleting an unwanted assumption*) 
653 
val thin_rl = 

24241  654 
let val V = read_prop "V" 
655 
and W = read_prop "W"; 

12135  656 
in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end; 
668  657 

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

24241  660 
let val V = read_prop "V" 
661 
and QV = read_prop "!!x::'a. V" 

26487  662 
and x = certify (Free ("x", Term.aT [])); 
4016  663 
in 
12135  664 
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

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

666 
(implies_intr V (forall_intr x (assume V)))) 
0  667 
end; 
668 

19051  669 
(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==> 
670 
(PROP ?Phi ==> PROP ?Psi) 

671 
*) 

672 
val distinct_prems_rl = 

673 
let 

24241  674 
val AAB = read_prop "Phi ==> Phi ==> Psi" 
675 
val A = read_prop "Phi"; 

19051  676 
in 
677 
store_standard_thm_open "distinct_prems_rl" 

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

679 
end; 

680 

1756  681 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
682 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

684 
*) 

685 
val swap_prems_rl = 

24241  686 
let val cmajor = read_prop "PhiA ==> PhiB ==> Psi"; 
1756  687 
val major = assume cmajor; 
24241  688 
val cminor1 = read_prop "PhiA"; 
1756  689 
val minor1 = assume cminor1; 
24241  690 
val cminor2 = read_prop "PhiB"; 
1756  691 
val minor2 = assume cminor2; 
12135  692 
in store_standard_thm_open "swap_prems_rl" 
1756  693 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
694 
(implies_elim (implies_elim major minor1) minor2)))) 

695 
end; 

696 

3653  697 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
698 
==> PROP ?phi == PROP ?psi 

8328  699 
Introduction rule for == as a metatheorem. 
3653  700 
*) 
701 
val equal_intr_rule = 

24241  702 
let val PQ = read_prop "phi ==> psi" 
703 
and QP = read_prop "psi ==> phi" 

4016  704 
in 
12135  705 
store_standard_thm_open "equal_intr_rule" 
4016  706 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  707 
end; 
708 

19421  709 
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *) 
13368  710 
val equal_elim_rule1 = 
24241  711 
let val eq = read_prop "phi::prop == psi::prop" 
712 
and P = read_prop "phi" 

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

715 
end; 

4285  716 

19421  717 
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *) 
718 
val equal_elim_rule2 = 

719 
store_standard_thm_open "equal_elim_rule2" (symmetric_thm RS equal_elim_rule1); 

720 

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

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

726 

9554  727 
(*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) 
12297  728 
Rewrite rule for HHF normalization.*) 
9554  729 

730 
val norm_hhf_eq = 

731 
let 

14854  732 
val aT = TFree ("'a", []); 
9554  733 
val all = Term.all aT; 
734 
val x = Free ("x", aT); 

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

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

737 

26487  738 
val cx = certify x; 
739 
val cphi = certify phi; 

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

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

9554  742 
in 
743 
Thm.equal_intr 

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

745 
> Thm.forall_elim cx 

746 
> Thm.implies_intr cphi 

747 
> Thm.forall_intr cx 

748 
> Thm.implies_intr lhs) 

749 
(Thm.implies_elim 

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

751 
> Thm.forall_intr cx 

752 
> Thm.implies_intr cphi 

753 
> Thm.implies_intr rhs) 

12135  754 
> store_standard_thm_open "norm_hhf_eq" 
9554  755 
end; 
756 

18179  757 
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); 
758 

12800  759 
fun is_norm_hhf tm = 
760 
let 

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

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

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

764 
 is_norm _ = true; 

18929  765 
in is_norm (Envir.beta_eta_contract tm) end; 
12800  766 

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

767 
fun norm_hhf thy t = 
12800  768 
if is_norm_hhf t then t 
18179  769 
else Pattern.rewrite_term thy [norm_hhf_prop] [] t; 
770 

20298  771 
fun norm_hhf_cterm ct = 
772 
if is_norm_hhf (Thm.term_of ct) then ct 

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

774 

12800  775 

21603  776 
(* var indexes *) 
777 

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

780 
let val tvs = term_tvars (prop_of th) 

781 
and thy = theory_of_thm th 

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

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

784 

21603  785 
fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1); 
786 

787 
fun incr_indexes2 th1 th2 = 

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

789 

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

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

792 

9554  793 

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

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

795 

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

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

799 

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

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

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

803 
in instantiate (read_insts thy ts ts used sinsts) th end; 
15797  804 

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

805 
fun read_instantiate_sg thy sinsts th = 
20298  806 
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

807 

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

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

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

810 
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

811 

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

813 
read_instantiate_sg' (Thm.theory_of_thm th) sinsts th; 
15797  814 

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

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

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

819 
fun add_types ((ct,cu), (thy,tye,maxidx)) = 
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

820 
let 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

821 
val thyt = Thm.theory_of_cterm ct; 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

822 
val thyu = Thm.theory_of_cterm cu; 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

823 
val {t, T, maxidx = maxt, ...} = Thm.rep_cterm ct; 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

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

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

826 
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

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

830 
"\nof variable " ^ 

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

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

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

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

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

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

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

837 
in 
22561  838 
fun cterm_instantiate [] th = th 
839 
 cterm_instantiate ctpairs0 th = 

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

842 
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

843 
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

844 
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

845 
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

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

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

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

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

850 

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

851 

19775  852 
(** protected propositions and embedded terms **) 
4789  853 

854 
local 

26487  855 
val A = certify (Free ("A", propT)); 
26424  856 
val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ())); 
857 
val prop_def = get_axiom "prop_def"; 

858 
val term_def = get_axiom "term_def"; 

4789  859 
in 
26487  860 
val protect = Thm.capply (certify Logic.protectC); 
21437  861 
val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard 
18025  862 
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)))); 
21437  863 
val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard 
18025  864 
(Thm.equal_elim prop_def (Thm.assume (protect A))))); 
18179  865 
val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A)); 
19775  866 

21437  867 
val termI = store_thm "termI" (PureThy.kind_rule Thm.internalK (standard 
19775  868 
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))))); 
4789  869 
end; 
870 

18025  871 
fun implies_intr_protected asms th = 
18118  872 
let val asms' = map protect asms in 
873 
implies_elim_list 

874 
(implies_intr_list asms th) 

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

876 
> implies_intr_list asms' 

877 
end; 

11815  878 

19775  879 
fun mk_term ct = 
880 
let 

26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

881 
val thy = Thm.theory_of_cterm ct; 
19775  882 
val cert = Thm.cterm_of thy; 
883 
val certT = Thm.ctyp_of thy; 

26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

884 
val T = Thm.typ_of (Thm.ctyp_of_term ct); 
19775  885 
val a = certT (TVar (("'a", 0), [])); 
886 
val x = cert (Var (("x", 0), T)); 

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

888 

889 
fun dest_term th = 

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

895 

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

20881  898 

26487  899 
val dummy_thm = mk_term (certify (Term.dummy_pattern propT)); 
24005  900 

901 

4789  902 

5688  903 
(** variations on instantiate **) 
4285  904 

905 
(* instantiate by lefttoright occurrence of variables *) 

906 

907 
fun instantiate' cTs cts thm = 

908 
let 

909 
fun err msg = 

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

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

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

912 
map_filter (Option.map Thm.term_of) cts); 
4285  913 

914 
fun inst_of (v, ct) = 

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

915 
(Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct) 
4285  916 
handle TYPE (msg, _, _) => err msg; 
917 

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

919 
(Thm.ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT) 
15797  920 
handle TYPE (msg, _, _) => err msg; 
921 

20298  922 
fun zip_vars xs ys = 
923 
zip_options xs ys handle Library.UnequalLengths => 

924 
err "more instantiations than variables in thm"; 

4285  925 

926 
(*instantiate types first!*) 

927 
val thm' = 

928 
if forall is_none cTs then thm 

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

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

934 
([], map inst_of (zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts)) thm'; 
20298  935 
in thm'' end; 
4285  936 

937 

14081  938 

939 
(** renaming of bound variables **) 

940 

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

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

943 

944 
fun rename_bvars [] thm = thm 

945 
 rename_bvars vs thm = 

26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

946 
let 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

947 
val cert = Thm.cterm_of (Thm.theory_of_thm thm); 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

948 
fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x > the_default x, T, ren t) 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

949 
 ren (t $ u) = ren t $ ren u 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

950 
 ren t = t; 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

951 
in equal_elim (reflexive (cert (ren (Thm.prop_of thm)))) thm end; 
14081  952 

953 

954 
(* renaming in lefttoright order *) 

955 

956 
fun rename_bvars' xs thm = 

957 
let 

26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

958 
val cert = Thm.cterm_of (Thm.theory_of_thm thm); 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

959 
val prop = Thm.prop_of thm; 
14081  960 
fun rename [] t = ([], t) 
961 
 rename (x' :: xs) (Abs (x, T, t)) = 

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

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

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

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

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

969 
 rename xs t = (xs, t); 

970 
in case rename xs prop of 

26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26487
diff
changeset

971 
([], prop') => equal_elim (reflexive (cert prop')) thm 
14081  972 
 _ => error "More names than abstractions in theorem" 
973 
end; 

974 

975 

11975  976 

18225  977 
(** multi_resolve **) 
978 

979 
local 

980 

981 
fun res th i rule = 

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

983 

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

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

986 

987 
in 

988 

989 
val multi_resolve = multi_res 1; 

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

991 

992 
end; 

993 

11975  994 
end; 
5903  995 

996 
structure BasicDrule: BASIC_DRULE = Drule; 

997 
open BasicDrule; 