author  wenzelm 
Thu, 16 Oct 2008 22:44:27 +0200  
changeset 28618  fa09f7b8ffca 
parent 27865  27a8ad9612a3 
child 28674  08a77c495dc1 
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) 

20 
val forall_intr_list: cterm list > thm > thm 

21 
val forall_intr_frees: thm > thm 

22 
val forall_intr_vars: thm > thm 

23 
val forall_elim_list: cterm list > thm > thm 

24 
val gen_all: thm > thm 

25 
val lift_all: cterm > thm > thm 

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

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

27 
val freeze_thaw_robust: thm > thm * (int > thm > thm) 
18179  28 
val implies_elim_list: thm > thm list > thm 
29 
val implies_intr_list: cterm list > thm > thm 

18206  30 
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list > thm > thm 
21603  31 
val zero_var_indexes_list: thm list > thm list 
18179  32 
val zero_var_indexes: thm > thm 
33 
val implies_intr_hyps: thm > thm 

34 
val standard: thm > thm 

35 
val standard': thm > thm 

36 
val rotate_prems: int > thm > thm 

37 
val rearrange_prems: int list > thm > thm 

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

39 
val RS: thm * thm > thm 

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

41 
val RL: thm list * thm list > thm list 

42 
val MRS: thm list * thm > thm 

43 
val MRL: thm list list * thm list > thm list 

44 
val OF: thm * thm list > thm 

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

46 
val COMP: thm * thm > thm 

21578  47 
val INCR_COMP: thm * thm > thm 
48 
val COMP_INCR: thm * thm > thm 

18179  49 
val cterm_instantiate: (cterm*cterm)list > thm > thm 
50 
val size_of_thm: thm > int 

51 
val reflexive_thm: thm 

52 
val symmetric_thm: thm 

53 
val transitive_thm: thm 

54 
val symmetric_fun: thm > thm 

55 
val extensional: thm > thm 

18820  56 
val equals_cong: thm 
18179  57 
val imp_cong: thm 
58 
val swap_prems_eq: thm 

59 
val asm_rl: thm 

60 
val cut_rl: thm 

61 
val revcut_rl: thm 

62 
val thin_rl: thm 

4285  63 
val triv_forall_equality: thm 
19051  64 
val distinct_prems_rl: thm 
18179  65 
val swap_prems_rl: thm 
66 
val equal_intr_rule: thm 

67 
val equal_elim_rule1: thm 

19421  68 
val equal_elim_rule2: thm 
18179  69 
val instantiate': ctyp option list > cterm option list > thm > thm 
5903  70 
end; 
71 

72 
signature DRULE = 

73 
sig 

74 
include BASIC_DRULE 

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

77 
val strip_comb: cterm > cterm * cterm list 
15262  78 
val strip_type: ctyp > ctyp list * ctyp 
15949  79 
val beta_conv: cterm > cterm > cterm 
27156  80 
val types_sorts: thm > (indexname> typ option) * (indexname> sort option) 
17713  81 
val flexflex_unique: thm > thm 
19421  82 
val store_thm: bstring > thm > thm 
83 
val store_standard_thm: bstring > thm > thm 

84 
val store_thm_open: bstring > thm > thm 

85 
val store_standard_thm_open: bstring > thm > thm 

11975  86 
val compose_single: thm * int * thm > thm 
18468  87 
val imp_cong_rule: thm > thm > thm 
22939  88 
val arg_cong_rule: cterm > thm > thm 
23568  89 
val binop_cong_rule: cterm > thm > thm > thm 
22939  90 
val fun_cong_rule: thm > cterm > thm 
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

91 
val beta_eta_conversion: cterm > thm 
15925  92 
val eta_long_conversion: cterm > thm 
20861  93 
val eta_contraction_rule: thm > thm 
11975  94 
val norm_hhf_eq: thm 
28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

95 
val norm_hhf_eqs: thm list 
12800  96 
val is_norm_hhf: term > bool 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

97 
val norm_hhf: theory > term > term 
20298  98 
val norm_hhf_cterm: cterm > cterm 
18025  99 
val protect: cterm > cterm 
100 
val protectI: thm 

101 
val protectD: thm 

18179  102 
val protect_cong: thm 
18025  103 
val implies_intr_protected: cterm list > thm > thm 
19775  104 
val termI: thm 
105 
val mk_term: cterm > thm 

106 
val dest_term: thm > cterm 

21519  107 
val cterm_rule: (thm > thm) > cterm > cterm 
20881  108 
val term_rule: theory > (thm > thm) > term > term 
24005  109 
val dummy_thm: thm 
28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

110 
val sort_constraintI: thm 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

111 
val sort_constraint_eq: thm 
19523  112 
val sort_triv: theory > typ * sort > thm list 
19504  113 
val unconstrainTs: thm > thm 
23423  114 
val with_subgoal: int > (thm > thm) > thm > thm 
14081  115 
val rename_bvars: (string * string) list > thm > thm 
116 
val rename_bvars': string option list > thm > thm 

24426  117 
val incr_type_indexes: int > thm > thm 
19124  118 
val incr_indexes: thm > thm > thm 
119 
val incr_indexes2: thm > thm > thm > thm 

12297  120 
val remdups_rl: thm 
18225  121 
val multi_resolve: thm list > thm > thm Seq.seq 
122 
val multi_resolves: thm list > thm list > thm Seq.seq 

13325  123 
val abs_def: thm > thm 
3766  124 
end; 
0  125 

5903  126 
structure Drule: DRULE = 
0  127 
struct 
128 

3991  129 

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

131 

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

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

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

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

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

137 

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

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

139 
fun strip_imp_concl ct = 
20579  140 
(case Thm.term_of ct of 
141 
Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct) 

142 
 _ => ct); 

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

143 

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

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

145 
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

146 

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

147 
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

148 
fun ctyp_fun f cT = Thm.ctyp_of (Thm.theory_of_ctyp cT) (f (Thm.typ_of cT)); 
15797  149 

26487  150 
fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t; 
9547  151 

27333  152 
val implies = certify Logic.implies; 
19183  153 
fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B; 
9547  154 

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

156 
fun list_implies([], B) = B 

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

158 

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

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

162 

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

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

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

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

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

168 
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

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

170 

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

173 
Type ("fun", _) => 

174 
let 

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

176 
val (cTs, cT') = strip_type cT2 

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

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

179 

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

18179  182 
fun beta_conv x y = 
20579  183 
Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.capply x y))); 
15949  184 

15875  185 

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

186 

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

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

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

191 
***) 

192 

193 
fun types_sorts thm = 

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

195 
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

196 
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

197 
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

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

201 
fun sorts (a, i) = 

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

203 
in (types, sorts) end; 

0  204 

15669  205 

7636  206 

9455  207 

0  208 
(** Standardization of rules **) 
209 

19523  210 
(* type classes and sorts *) 
211 

212 
fun sort_triv thy (T, S) = 

213 
let 

214 
val certT = Thm.ctyp_of thy; 

215 
val cT = certT T; 

216 
fun class_triv c = 

217 
Thm.class_triv thy c 

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

19504  221 
fun unconstrainTs th = 
20298  222 
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

223 
(Thm.fold_terms Term.add_tvars th []) th; 
19504  224 

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

0  227 

228 
(*Generalization over all suitable Free variables*) 

229 
fun forall_intr_frees th = 

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

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

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

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

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

0  237 

18535  238 
(*Generalization over Vars  canonical order*) 
239 
fun forall_intr_vars th = 

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

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

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

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

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

247 
(*generalize outermost parameters*) 

248 
fun gen_all th = 

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

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

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

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

254 
in fold elim (outer_params prop) th end; 

255 

256 
(*lift vars wrt. outermost goal parameters 

18118  257 
 reverses the effect of gen_all modulo higherorder unification*) 
18025  258 
fun lift_all goal th = 
259 
let 

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

261 
val cert = Thm.cterm_of thy; 

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

265 
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

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

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

270 
> fold_rev (Thm.forall_intr o cert) ps 

271 
end; 

272 

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

9554  275 

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

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

277 
val forall_elim_list = fold forall_elim; 
0  278 

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

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

280 
val implies_intr_list = fold_rev implies_intr; 
0  281 

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

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

283 
fun implies_elim_list impth ths = fold Thm.elim_implies ths impth; 
0  284 

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

21603  286 
fun zero_var_indexes_list [] = [] 
287 
 zero_var_indexes_list ths = 

288 
let 

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

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

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

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

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

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

295 

296 
val zero_var_indexes = singleton zero_var_indexes_list; 

0  297 

298 

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

10515  301 

16595  302 
(*Discharge all hypotheses.*) 
303 
fun implies_intr_hyps th = 

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

305 

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

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

308 
fun flexflex_unique th = 
17713  309 
if null (tpairs_of th) then th else 
23439  310 
case distinct Thm.eq_thm (Seq.list_of (flexflex_rule th)) of 
311 
[th] => th 

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

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

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

314 

21603  315 

316 
(* legacy standard operations *) 

317 

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

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

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

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

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

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

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

327 

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

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

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

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

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

332 

0  333 

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

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

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

337 

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

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

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

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

342 
in 
23178  343 
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

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

345 
 vars => 
19753  346 
let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix)) 
347 
val alist = map newName vars 

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

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

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

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

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

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

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

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

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

357 

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

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

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

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

364 
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

365 
in 
23178  366 
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

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

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

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

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

375 
(cterm_of thy (Var(v,T)), 
17325  376 
cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) 
8328  377 
val insts = map mk_inst vars 
378 
fun thaw th' = 

379 
th' > forall_intr_list (map #2 insts) 

380 
> forall_elim_list (map #1 insts) 

381 
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

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

383 

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

384 
(*Rotates a rule's premises to the left by k*) 
23537  385 
fun rotate_prems 0 = I 
386 
 rotate_prems k = permute_prems 0 k; 

387 

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

389 

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

392 
Any remaining trailing positions are left unchanged. *) 

393 
val rearrange_prems = let 

394 
fun rearr new [] thm = thm 

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

398 
in rearr 0 end; 

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

399 

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

400 
(*Resolution: exactly one resolvent must be produced.*) 
0  401 
fun tha RSN (i,thb) = 
19861  402 
case Seq.chop 2 (biresolution false [(false,tha)] i thb) of 
0  403 
([th],_) => th 
404 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

406 

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

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

409 

410 
(*For joining lists of rules*) 

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

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

414 
in maps resb thbs end; 
0  415 

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

417 

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

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

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

420 
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

421 
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

422 
 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

423 
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

424 

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

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

426 
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

427 
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

428 
 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

429 
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

430 

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

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

432 
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

433 

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

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

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

437 
fun compose(tha,i,thb) = 
24426  438 
distinct Thm.eq_thm (Seq.list_of (bicompose false (false,tha,0) i thb)); 
0  439 

6946  440 
fun compose_single (tha,i,thb) = 
24426  441 
case compose (tha,i,thb) of 
6946  442 
[th] => th 
24426  443 
 _ => raise THM ("compose: unique result expected", i, [tha,thb]); 
6946  444 

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

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

448 
[th] => th 
0  449 
 _ => raise THM("COMP", 1, [tha,thb]); 
450 

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

451 

4016  452 
(** theorem equality **) 
0  453 

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

16720  455 
val size_of_thm = size_of_term o Thm.full_prop_of; 
0  456 

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

457 

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

458 

0  459 
(*** MetaRewriting Rules ***) 
460 

26487  461 
val read_prop = certify o SimpleSyntax.read_prop; 
462 

463 
fun store_thm name th = 

464 
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

465 

26487  466 
fun store_thm_open name th = 
467 
Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th))); 

468 

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

12135  470 
fun store_standard_thm_open name thm = store_thm_open name (standard' thm); 
4016  471 

0  472 
val reflexive_thm = 
26487  473 
let val cx = certify (Var(("x",0),TVar(("'a",0),[]))) 
12135  474 
in store_standard_thm_open "reflexive" (Thm.reflexive cx) end; 
0  475 

476 
val symmetric_thm = 

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

480 
val transitive_thm = 

24241  481 
let val xy = read_prop "x::'a == y::'a" 
482 
val yz = read_prop "y::'a == z::'a" 

0  483 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
12135  484 
in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 
0  485 

4679  486 
fun symmetric_fun thm = thm RS symmetric_thm; 
487 

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

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

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

490 
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

491 
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

492 

18820  493 
val equals_cong = 
24241  494 
store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x::'a == y::'a")); 
18820  495 

10414  496 
val imp_cong = 
497 
let 

24241  498 
val ABC = read_prop "A ==> B::prop == C::prop" 
499 
val AB = read_prop "A ==> B" 

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

501 
val A = read_prop "A" 

10414  502 
in 
12135  503 
store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr 
10414  504 
(implies_intr AB (implies_intr A 
505 
(equal_elim (implies_elim (assume ABC) (assume A)) 

506 
(implies_elim (assume AB) (assume A))))) 

507 
(implies_intr AC (implies_intr A 

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

509 
(implies_elim (assume AC) (assume A))))))) 

510 
end; 

511 

512 
val swap_prems_eq = 

513 
let 

24241  514 
val ABC = read_prop "A ==> B ==> C" 
515 
val BAC = read_prop "B ==> A ==> C" 

516 
val A = read_prop "A" 

517 
val B = read_prop "B" 

10414  518 
in 
12135  519 
store_standard_thm_open "swap_prems_eq" (equal_intr 
10414  520 
(implies_intr ABC (implies_intr B (implies_intr A 
521 
(implies_elim (implies_elim (assume ABC) (assume A)) (assume B))))) 

522 
(implies_intr BAC (implies_intr A (implies_intr B 

523 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

524 
end; 

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

525 

22938  526 
val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies); 
527 

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

23568  530 
fun binop_cong_rule ct th1 th2 = Thm.combination (arg_cong_rule ct th1) th2; 
0  531 

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

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

533 
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

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

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

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

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

538 
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

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

540 

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

543 

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

546 
equal_elim (eta_conversion (cprop_of th)) th; 

547 

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

548 

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

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

550 

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

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

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

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

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

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

556 

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

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

558 

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

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

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

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

562 

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

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

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

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

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

567 
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

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

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

570 

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

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

572 

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

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

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

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

577 
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

578 

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

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

580 

18337  581 

18468  582 

15669  583 
(*** Some useful metatheorems ***) 
0  584 

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

24241  586 
val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi")); 
7380  587 
val _ = store_thm "_" asm_rl; 
0  588 

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

4016  590 
val cut_rl = 
12135  591 
store_standard_thm_open "cut_rl" 
24241  592 
(Thm.trivial (read_prop "?psi ==> ?theta")); 
0  593 

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

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

24241  597 
let val V = read_prop "V" 
598 
and VW = read_prop "V ==> W"; 

4016  599 
in 
12135  600 
store_standard_thm_open "revcut_rl" 
4016  601 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  602 
end; 
603 

668  604 
(*for deleting an unwanted assumption*) 
605 
val thin_rl = 

24241  606 
let val V = read_prop "V" 
607 
and W = read_prop "W"; 

12135  608 
in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end; 
668  609 

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

24241  612 
let val V = read_prop "V" 
613 
and QV = read_prop "!!x::'a. V" 

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

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

618 
(implies_intr V (forall_intr x (assume V)))) 
0  619 
end; 
620 

19051  621 
(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==> 
622 
(PROP ?Phi ==> PROP ?Psi) 

623 
*) 

624 
val distinct_prems_rl = 

625 
let 

24241  626 
val AAB = read_prop "Phi ==> Phi ==> Psi" 
627 
val A = read_prop "Phi"; 

19051  628 
in 
629 
store_standard_thm_open "distinct_prems_rl" 

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

631 
end; 

632 

1756  633 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
634 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

636 
*) 

637 
val swap_prems_rl = 

24241  638 
let val cmajor = read_prop "PhiA ==> PhiB ==> Psi"; 
1756  639 
val major = assume cmajor; 
24241  640 
val cminor1 = read_prop "PhiA"; 
1756  641 
val minor1 = assume cminor1; 
24241  642 
val cminor2 = read_prop "PhiB"; 
1756  643 
val minor2 = assume cminor2; 
12135  644 
in store_standard_thm_open "swap_prems_rl" 
1756  645 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
646 
(implies_elim (implies_elim major minor1) minor2)))) 

647 
end; 

648 

3653  649 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
650 
==> PROP ?phi == PROP ?psi 

8328  651 
Introduction rule for == as a metatheorem. 
3653  652 
*) 
653 
val equal_intr_rule = 

24241  654 
let val PQ = read_prop "phi ==> psi" 
655 
and QP = read_prop "psi ==> phi" 

4016  656 
in 
12135  657 
store_standard_thm_open "equal_intr_rule" 
4016  658 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  659 
end; 
660 

19421  661 
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *) 
13368  662 
val equal_elim_rule1 = 
24241  663 
let val eq = read_prop "phi::prop == psi::prop" 
664 
and P = read_prop "phi" 

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

667 
end; 

4285  668 

19421  669 
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *) 
670 
val equal_elim_rule2 = 

671 
store_standard_thm_open "equal_elim_rule2" (symmetric_thm RS equal_elim_rule1); 

672 

28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

673 
(* PROP ?phi ==> PROP ?phi ==> PROP ?psi ==> PROP ?psi *) 
12297  674 
val remdups_rl = 
24241  675 
let val P = read_prop "phi" and Q = read_prop "psi"; 
12297  676 
in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end; 
677 

678 

28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

679 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

680 
(** embedded terms and types **) 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

681 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

682 
local 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

683 
val A = certify (Free ("A", propT)); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

684 
val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ())); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

685 
val prop_def = get_axiom "prop_def"; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

686 
val term_def = get_axiom "term_def"; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

687 
val sort_constraint_def = get_axiom "sort_constraint_def"; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

688 
val C = Thm.lhs_of sort_constraint_def; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

689 
val T = Thm.dest_arg C; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

690 
val CA = mk_implies (C, A); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

691 
in 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

692 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

693 
(* protect *) 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

694 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

695 
val protect = Thm.capply (certify Logic.protectC); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

696 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

697 
val protectI = store_thm "protectI" (Thm.kind_rule Thm.internalK (standard 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

698 
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)))); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

699 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

700 
val protectD = store_thm "protectD" (Thm.kind_rule Thm.internalK (standard 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

701 
(Thm.equal_elim prop_def (Thm.assume (protect A))))); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

702 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

703 
val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A)); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

704 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

705 
fun implies_intr_protected asms th = 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

706 
let val asms' = map protect asms in 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

707 
implies_elim_list 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

708 
(implies_intr_list asms th) 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

709 
(map (fn asm' => Thm.assume asm' RS protectD) asms') 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

710 
> implies_intr_list asms' 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

711 
end; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

712 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

713 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

714 
(* term *) 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

715 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

716 
val termI = store_thm "termI" (Thm.kind_rule Thm.internalK (standard 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

717 
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))))); 
9554  718 

28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

719 
fun mk_term ct = 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

720 
let 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

721 
val thy = Thm.theory_of_cterm ct; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

722 
val cert = Thm.cterm_of thy; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

723 
val certT = Thm.ctyp_of thy; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

724 
val T = Thm.typ_of (Thm.ctyp_of_term ct); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

725 
val a = certT (TVar (("'a", 0), [])); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

726 
val x = cert (Var (("x", 0), T)); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

727 
in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

728 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

729 
fun dest_term th = 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

730 
let val cprop = strip_imp_concl (Thm.cprop_of th) in 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

731 
if can Logic.dest_term (Thm.term_of cprop) then 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

732 
Thm.dest_arg cprop 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

733 
else raise THM ("dest_term", 0, [th]) 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

734 
end; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

735 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

736 
fun cterm_rule f = dest_term o f o mk_term; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

737 
fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t)); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

738 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

739 
val dummy_thm = mk_term (certify (Term.dummy_pattern propT)); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

740 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

741 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

742 
(* sort_constraint *) 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

743 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

744 
val sort_constraintI = store_thm "sort_constraintI" (Thm.kind_rule Thm.internalK (standard 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

745 
(Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)))); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

746 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

747 
val sort_constraint_eq = store_thm "sort_constraint_eq" (Thm.kind_rule Thm.internalK (standard 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

748 
(Thm.equal_intr 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

749 
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI))) 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

750 
(implies_intr_list [A, C] (Thm.assume A))))); 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

751 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

752 
end; 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

753 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

754 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

755 
(* HHF normalization *) 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

756 

fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

757 
(* (PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) *) 
9554  758 
val norm_hhf_eq = 
759 
let 

14854  760 
val aT = TFree ("'a", []); 
9554  761 
val all = Term.all aT; 
762 
val x = Free ("x", aT); 

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

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

765 

26487  766 
val cx = certify x; 
767 
val cphi = certify phi; 

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

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

9554  770 
in 
771 
Thm.equal_intr 

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

773 
> Thm.forall_elim cx 

774 
> Thm.implies_intr cphi 

775 
> Thm.forall_intr cx 

776 
> Thm.implies_intr lhs) 

777 
(Thm.implies_elim 

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

779 
> Thm.forall_intr cx 

780 
> Thm.implies_intr cphi 

781 
> Thm.implies_intr rhs) 

12135  782 
> store_standard_thm_open "norm_hhf_eq" 
9554  783 
end; 
784 

18179  785 
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); 
28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

786 
val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq]; 
18179  787 

12800  788 
fun is_norm_hhf tm = 
789 
let 

28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

790 
fun is_norm (Const ("Pure.sort_constraint", _)) = false 
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

791 
 is_norm (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false 
12800  792 
 is_norm (t $ u) = is_norm t andalso is_norm u 
793 
 is_norm (Abs (_, _, t)) = is_norm t 

794 
 is_norm _ = true; 

18929  795 
in is_norm (Envir.beta_eta_contract tm) end; 
12800  796 

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

797 
fun norm_hhf thy t = 
12800  798 
if is_norm_hhf t then t 
18179  799 
else Pattern.rewrite_term thy [norm_hhf_prop] [] t; 
800 

20298  801 
fun norm_hhf_cterm ct = 
802 
if is_norm_hhf (Thm.term_of ct) then ct 

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

804 

12800  805 

21603  806 
(* var indexes *) 
807 

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

810 
let val tvs = term_tvars (prop_of th) 

811 
and thy = theory_of_thm th 

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

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

814 

21603  815 
fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1); 
816 

817 
fun incr_indexes2 th1 th2 = 

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

819 

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

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

822 

9554  823 

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

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

825 

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

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

829 

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

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

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

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

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

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

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

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

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

838 
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

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

840 
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

841 
val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) 
25470  842 
handle Type.TUNIFY => raise TYPE ("Illtyped instantiation:\nType\n" ^ 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26653
diff
changeset

843 
Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^ 
25470  844 
"\nof variable " ^ 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26653
diff
changeset

845 
Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^ 
25470  846 
"\ncannot be unified with type\n" ^ 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26653
diff
changeset

847 
Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^ 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26653
diff
changeset

848 
Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u), 
25470  849 
[T, U], [t, u]) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

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

851 
in 
22561  852 
fun cterm_instantiate [] th = th 
853 
 cterm_instantiate ctpairs0 th = 

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

856 
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

857 
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

858 
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

859 
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

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

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

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

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

864 

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

865 

4789  866 

5688  867 
(** variations on instantiate **) 
4285  868 

869 
(* instantiate by lefttoright occurrence of variables *) 

870 

871 
fun instantiate' cTs cts thm = 

872 
let 

873 
fun err msg = 

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

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

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

876 
map_filter (Option.map Thm.term_of) cts); 
4285  877 

878 
fun inst_of (v, ct) = 

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

879 
(Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct) 
4285  880 
handle TYPE (msg, _, _) => err msg; 
881 

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

883 
(Thm.ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT) 
15797  884 
handle TYPE (msg, _, _) => err msg; 
885 

20298  886 
fun zip_vars xs ys = 
887 
zip_options xs ys handle Library.UnequalLengths => 

888 
err "more instantiations than variables in thm"; 

4285  889 

890 
(*instantiate types first!*) 

891 
val thm' = 

892 
if forall is_none cTs then thm 

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

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

898 
([], map inst_of (zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts)) thm'; 
20298  899 
in thm'' end; 
4285  900 

901 

14081  902 

903 
(** renaming of bound variables **) 

904 

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

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

907 

908 
fun rename_bvars [] thm = thm 

909 
 rename_bvars vs thm = 

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

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

911 
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

912 
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

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

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

915 
in equal_elim (reflexive (cert (ren (Thm.prop_of thm)))) thm end; 
14081  916 

917 

918 
(* renaming in lefttoright order *) 

919 

920 
fun rename_bvars' xs thm = 

921 
let 

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

922 
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

923 
val prop = Thm.prop_of thm; 
14081  924 
fun rename [] t = ([], t) 
925 
 rename (x' :: xs) (Abs (x, T, t)) = 

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

18929  927 
in (xs', Abs (the_default x x', T, t')) end 
14081  928 
 rename xs (t $ u) = 
929 
let 

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

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

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

933 
 rename xs t = (xs, t); 

934 
in case rename xs prop of 

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

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

938 

939 

11975  940 

18225  941 
(** multi_resolve **) 
942 

943 
local 

944 

945 
fun res th i rule = 

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

947 

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

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

950 

951 
in 

952 

953 
val multi_resolve = multi_res 1; 

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

955 

956 
end; 

957 

11975  958 
end; 
5903  959 

960 
structure BasicDrule: BASIC_DRULE = Drule; 

961 
open BasicDrule; 