author  wenzelm 
Wed, 29 May 2013 18:25:11 +0200  
changeset 52223  5bb6ae8acb87 
parent 52131  366fa32ee2a3 
child 52224  6ba76ad4e679 
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 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 

3766  4 
Derived rules and other operations on theorems. 
0  5 
*) 
6 

46470
b0331b0d33a3
discontinued unused MRL  in correspondence with section "2.4.2 Rule composition" in the implementation manual;
wenzelm
parents:
46214
diff
changeset

7 
infix 0 RS RSN RL RLN MRS OF COMP INCR_COMP COMP_INCR; 
0  8 

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

13 
val strip_imp_prems: cterm > cterm list 

14 
val strip_imp_concl: cterm > cterm 

15 
val cprems_of: thm > cterm list 

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

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

18 
val forall_intr_list: cterm list > thm > thm 

19 
val forall_intr_vars: thm > thm 

20 
val forall_elim_list: cterm list > thm > thm 

21 
val gen_all: thm > thm 

22 
val lift_all: cterm > thm > thm 

23 
val implies_elim_list: thm > thm list > thm 

24 
val implies_intr_list: cterm list > thm > thm 

43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
43330
diff
changeset

25 
val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list > thm > thm 
21603  26 
val zero_var_indexes_list: thm list > thm list 
18179  27 
val zero_var_indexes: thm > thm 
28 
val implies_intr_hyps: thm > thm 

29 
val rotate_prems: int > thm > thm 

30 
val rearrange_prems: int list > thm > thm 

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

32 
val RS: thm * thm > thm 

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

34 
val RL: thm list * thm list > thm list 

35 
val MRS: thm list * thm > thm 

36 
val OF: thm * thm list > thm 

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

38 
val COMP: thm * thm > thm 

21578  39 
val INCR_COMP: thm * thm > thm 
40 
val COMP_INCR: thm * thm > thm 

46186  41 
val cterm_instantiate: (cterm * cterm) list > thm > thm 
18179  42 
val size_of_thm: thm > int 
43 
val reflexive_thm: thm 

44 
val symmetric_thm: thm 

45 
val transitive_thm: thm 

46 
val extensional: thm > thm 

47 
val asm_rl: thm 

48 
val cut_rl: thm 

49 
val revcut_rl: thm 

50 
val thin_rl: thm 

51 
val instantiate': ctyp option list > cterm option list > thm > thm 

5903  52 
end; 
53 

54 
signature DRULE = 

55 
sig 

56 
include BASIC_DRULE 

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

59 
val strip_comb: cterm > cterm * cterm list 
15262  60 
val strip_type: ctyp > ctyp list * ctyp 
15949  61 
val beta_conv: cterm > cterm > cterm 
27156  62 
val types_sorts: thm > (indexname> typ option) * (indexname> sort option) 
17713  63 
val flexflex_unique: thm > thm 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

64 
val export_without_context: thm > thm 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

65 
val export_without_context_open: thm > thm 
33277  66 
val store_thm: binding > thm > thm 
67 
val store_standard_thm: binding > thm > thm 

68 
val store_thm_open: binding > thm > thm 

69 
val store_standard_thm_open: binding > thm > thm 

47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

70 
val multi_resolve: thm list > thm > thm Seq.seq 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

71 
val multi_resolves: thm list > thm list > thm Seq.seq 
11975  72 
val compose_single: thm * int * thm > thm 
46186  73 
val equals_cong: thm 
74 
val imp_cong: thm 

75 
val swap_prems_eq: thm 

18468  76 
val imp_cong_rule: thm > thm > thm 
22939  77 
val arg_cong_rule: cterm > thm > thm 
23568  78 
val binop_cong_rule: cterm > thm > thm > thm 
22939  79 
val fun_cong_rule: thm > cterm > thm 
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

80 
val beta_eta_conversion: cterm > thm 
15925  81 
val eta_long_conversion: cterm > thm 
20861  82 
val eta_contraction_rule: thm > thm 
11975  83 
val norm_hhf_eq: thm 
28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

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

86 
val norm_hhf: theory > term > term 
20298  87 
val norm_hhf_cterm: cterm > cterm 
18025  88 
val protect: cterm > cterm 
89 
val protectI: thm 

90 
val protectD: thm 

18179  91 
val protect_cong: thm 
18025  92 
val implies_intr_protected: cterm list > thm > thm 
19775  93 
val termI: thm 
94 
val mk_term: cterm > thm 

95 
val dest_term: thm > cterm 

21519  96 
val cterm_rule: (thm > thm) > cterm > cterm 
24005  97 
val dummy_thm: thm 
28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

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

99 
val sort_constraint_eq: thm 
23423  100 
val with_subgoal: int > (thm > thm) > thm > thm 
29344  101 
val comp_no_flatten: thm * int > int > thm > thm 
14081  102 
val rename_bvars: (string * string) list > thm > thm 
103 
val rename_bvars': string option list > thm > thm 

19124  104 
val incr_indexes: thm > thm > thm 
105 
val incr_indexes2: thm > thm > thm > thm 

46186  106 
val triv_forall_equality: thm 
107 
val distinct_prems_rl: thm 

108 
val equal_intr_rule: thm 

109 
val equal_elim_rule1: thm 

110 
val equal_elim_rule2: thm 

12297  111 
val remdups_rl: thm 
13325  112 
val abs_def: thm > thm 
3766  113 
end; 
0  114 

5903  115 
structure Drule: DRULE = 
0  116 
struct 
117 

3991  118 

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

120 

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

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

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

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

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

126 

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

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

128 
fun strip_imp_concl ct = 
20579  129 
(case Thm.term_of ct of 
130 
Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct) 

131 
 _ => ct); 

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

132 

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

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

134 
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

135 

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

136 
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

137 
fun ctyp_fun f cT = Thm.ctyp_of (Thm.theory_of_ctyp cT) (f (Thm.typ_of cT)); 
15797  138 

26487  139 
fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t; 
9547  140 

27333  141 
val implies = certify Logic.implies; 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46496
diff
changeset

142 
fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B; 
9547  143 

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

145 
fun list_implies([], B) = B 

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

147 

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

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46496
diff
changeset

150 
 list_comb (f, t::ts) = list_comb (Thm.apply f t, ts); 
15949  151 

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

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

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

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

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

157 
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

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

159 

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

162 
Type ("fun", _) => 

163 
let 

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

165 
val (cTs, cT') = strip_type cT2 

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

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

168 

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

18179  171 
fun beta_conv x y = 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46496
diff
changeset

172 
Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.apply x y))); 
15949  173 

15875  174 

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

175 

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

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

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

180 
***) 

181 

182 
fun types_sorts thm = 

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

184 
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

185 
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

186 
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

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

190 
fun sorts (a, i) = 

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

192 
in (types, sorts) end; 

0  193 

15669  194 

7636  195 

9455  196 

0  197 
(** Standardization of rules **) 
198 

19730  199 
(*Generalization over a list of variables*) 
36944  200 
val forall_intr_list = fold_rev Thm.forall_intr; 
0  201 

18535  202 
(*Generalization over Vars  canonical order*) 
203 
fun forall_intr_vars th = 

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

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

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

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

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

211 
(*generalize outermost parameters*) 

212 
fun gen_all th = 

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

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

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

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

218 
in fold elim (outer_params prop) th end; 

219 

220 
(*lift vars wrt. outermost goal parameters 

18118  221 
 reverses the effect of gen_all modulo higherorder unification*) 
18025  222 
fun lift_all goal th = 
223 
let 

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

225 
val cert = Thm.cterm_of thy; 

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

229 
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

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

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

234 
> fold_rev (Thm.forall_intr o cert) ps 

235 
end; 

236 

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

9554  239 

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

240 
(*specialization over a list of cterms*) 
36944  241 
val forall_elim_list = fold Thm.forall_elim; 
0  242 

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

243 
(*maps A1,...,An  B to [ A1;...;An ] ==> B*) 
36944  244 
val implies_intr_list = fold_rev Thm.implies_intr; 
0  245 

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

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

247 
fun implies_elim_list impth ths = fold Thm.elim_implies ths impth; 
0  248 

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

21603  250 
fun zero_var_indexes_list [] = [] 
251 
 zero_var_indexes_list ths = 

252 
let 

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

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

31977  255 
val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths); 
21603  256 
val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT; 
257 
val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst; 

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

259 

260 
val zero_var_indexes = singleton zero_var_indexes_list; 

0  261 

262 

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

10515  265 

16595  266 
(*Discharge all hypotheses.*) 
267 
fun implies_intr_hyps th = 

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

269 

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

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

272 
fun flexflex_unique th = 
38709  273 
if null (Thm.tpairs_of th) then th else 
36944  274 
case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule th)) of 
23439  275 
[th] => th 
276 
 [] => raise THM("flexflex_unique: impossible constraints", 0, [th]) 

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

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

278 

21603  279 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

280 
(* oldstyle export without context *) 
21603  281 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

282 
val export_without_context_open = 
16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

283 
implies_intr_hyps 
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35897
diff
changeset

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

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

289 
#> zero_var_indexes 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35237
diff
changeset

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

291 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

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

293 
flexflex_unique 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

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

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

296 

0  297 

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

298 
(*Rotates a rule's premises to the left by k*) 
23537  299 
fun rotate_prems 0 = I 
31945  300 
 rotate_prems k = Thm.permute_prems 0 k; 
23537  301 

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

303 

31945  304 
(*Permute prems, where the ith position in the argument list (counting from 0) 
305 
gives the position within the original thm to be transferred to position i. 

306 
Any remaining trailing positions are left unchanged.*) 

307 
val rearrange_prems = 

308 
let 

309 
fun rearr new [] thm = thm 

310 
 rearr new (p :: ps) thm = 

311 
rearr (new + 1) 

312 
(map (fn q => if new <= q andalso q < p then q + 1 else q) ps) 

313 
(Thm.permute_prems (new + 1) (new  p) (Thm.permute_prems new (p  new) thm)) 

11163  314 
in rearr 0 end; 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

315 

47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

316 

0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

317 
(*Resolution: multiple arguments, multiple results*) 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

318 
local 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

319 
fun res th i rule = 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

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

47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

322 
fun multi_res _ [] rule = Seq.single rule 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

323 
 multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule); 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

324 
in 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

325 
val multi_resolve = multi_res 1; 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

326 
fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules); 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

327 
end; 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

328 

0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

329 
(*Resolution: exactly one resolvent must be produced*) 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

330 
fun tha RSN (i, thb) = 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

331 
(case Seq.chop 2 (Thm.biresolution false [(false, tha)] i thb) of 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

332 
([th], _) => th 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

333 
 ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb]) 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

334 
 _ => raise THM ("RSN: multiple unifiers", i, [tha, thb])); 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

335 

0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

336 
(*Resolution: P==>Q, Q==>R gives P==>R*) 
0  337 
fun tha RS thb = tha RSN (1,thb); 
338 

339 
(*For joining lists of rules*) 

47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

340 
fun thas RLN (i, thbs) = 
31945  341 
let val resolve = Thm.biresolution false (map (pair false) thas) i 
4270  342 
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

343 
in maps resb thbs end; 
0  344 

47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

345 
fun thas RL thbs = thas RLN (1, thbs); 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

346 

0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

347 
(*Isarstyle multiresolution*) 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

348 
fun bottom_rl OF rls = 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

349 
(case Seq.chop 2 (multi_resolve rls bottom_rl) of 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

350 
([th], _) => th 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

351 
 ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls) 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

352 
 _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls)); 
0  353 

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

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

355 
makes proof trees*) 
47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

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

357 

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

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

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

361 
fun compose(tha,i,thb) = 
52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52131
diff
changeset

362 
distinct Thm.eq_thm 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52131
diff
changeset

363 
(Seq.list_of 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52131
diff
changeset

364 
(Thm.bicompose {flatten = true, match = false, incremented = false} (false, tha, 0) i thb)); 
0  365 

6946  366 
fun compose_single (tha,i,thb) = 
47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

367 
(case compose (tha,i,thb) of 
6946  368 
[th] => th 
47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

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

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

47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

373 
(case compose(tha, 1, thb) of 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

374 
[th] => th 
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47239
diff
changeset

375 
 _ => raise THM ("COMP", 1, [tha, thb])); 
0  376 

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

377 

4016  378 
(** theorem equality **) 
0  379 

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

16720  381 
val size_of_thm = size_of_term o Thm.full_prop_of; 
0  382 

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

383 

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

384 

0  385 
(*** MetaRewriting Rules ***) 
386 

33384  387 
val read_prop = certify o Simple_Syntax.read_prop; 
26487  388 

389 
fun store_thm name th = 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38709
diff
changeset

390 
Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th))); 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

391 

26487  392 
fun store_thm_open name th = 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38709
diff
changeset

393 
Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th))); 
26487  394 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

395 
fun store_standard_thm name th = store_thm name (export_without_context th); 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

396 
fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm); 
4016  397 

0  398 
val reflexive_thm = 
26487  399 
let val cx = certify (Var(("x",0),TVar(("'a",0),[]))) 
33277  400 
in store_standard_thm_open (Binding.name "reflexive") (Thm.reflexive cx) end; 
0  401 

402 
val symmetric_thm = 

33277  403 
let 
404 
val xy = read_prop "x::'a == y::'a"; 

405 
val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy)); 

406 
in store_standard_thm_open (Binding.name "symmetric") thm end; 

0  407 

408 
val transitive_thm = 

33277  409 
let 
410 
val xy = read_prop "x::'a == y::'a"; 

411 
val yz = read_prop "y::'a == z::'a"; 

412 
val xythm = Thm.assume xy; 

413 
val yzthm = Thm.assume yz; 

414 
val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm); 

415 
in store_standard_thm_open (Binding.name "transitive") thm end; 

0  416 

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

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

418 
let val eq' = 
36944  419 
Thm.abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq 
420 
in Thm.equal_elim (Thm.eta_conversion (cprop_of eq')) eq' end; 

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

421 

18820  422 
val equals_cong = 
33277  423 
store_standard_thm_open (Binding.name "equals_cong") 
424 
(Thm.reflexive (read_prop "x::'a == y::'a")); 

18820  425 

10414  426 
val imp_cong = 
427 
let 

24241  428 
val ABC = read_prop "A ==> B::prop == C::prop" 
429 
val AB = read_prop "A ==> B" 

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

431 
val A = read_prop "A" 

10414  432 
in 
36944  433 
store_standard_thm_open (Binding.name "imp_cong") (Thm.implies_intr ABC (Thm.equal_intr 
434 
(Thm.implies_intr AB (Thm.implies_intr A 

435 
(Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) 

436 
(Thm.implies_elim (Thm.assume AB) (Thm.assume A))))) 

437 
(Thm.implies_intr AC (Thm.implies_intr A 

438 
(Thm.equal_elim (Thm.symmetric (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))) 

439 
(Thm.implies_elim (Thm.assume AC) (Thm.assume A))))))) 

10414  440 
end; 
441 

442 
val swap_prems_eq = 

443 
let 

24241  444 
val ABC = read_prop "A ==> B ==> C" 
445 
val BAC = read_prop "B ==> A ==> C" 

446 
val A = read_prop "A" 

447 
val B = read_prop "B" 

10414  448 
in 
33277  449 
store_standard_thm_open (Binding.name "swap_prems_eq") 
36944  450 
(Thm.equal_intr 
451 
(Thm.implies_intr ABC (Thm.implies_intr B (Thm.implies_intr A 

452 
(Thm.implies_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.assume B))))) 

453 
(Thm.implies_intr BAC (Thm.implies_intr A (Thm.implies_intr B 

454 
(Thm.implies_elim (Thm.implies_elim (Thm.assume BAC) (Thm.assume B)) (Thm.assume A)))))) 

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

456 

22938  457 
val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies); 
458 

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

23568  461 
fun binop_cong_rule ct th1 th2 = Thm.combination (arg_cong_rule ct th1) th2; 
0  462 

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

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

464 
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

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

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

467 
fun beta_eta_conversion t = 
36944  468 
let val thm = Thm.beta_conversion true t 
469 
in Thm.transitive thm (Thm.eta_conversion (rhs_of thm)) end 

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

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

471 

36944  472 
fun eta_long_conversion ct = 
473 
Thm.transitive 

474 
(beta_eta_conversion ct) 

52131  475 
(Thm.symmetric (beta_eta_conversion (cterm_fun (Envir.eta_long []) ct))); 
15925  476 

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

36944  479 
Thm.equal_elim (Thm.eta_conversion (cprop_of th)) th; 
20861  480 

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

481 

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

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

483 

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

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

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

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

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

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

489 

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

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

491 

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

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

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

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

495 

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

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

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

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

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

500 
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

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

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

503 

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

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

505 

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

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

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

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

510 
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

511 

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

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

513 

18337  514 

18468  515 

15669  516 
(*** Some useful metatheorems ***) 
0  517 

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

33277  519 
val asm_rl = store_standard_thm_open (Binding.name "asm_rl") (Thm.trivial (read_prop "?psi")); 
0  520 

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

4016  522 
val cut_rl = 
33277  523 
store_standard_thm_open (Binding.name "cut_rl") 
24241  524 
(Thm.trivial (read_prop "?psi ==> ?theta")); 
0  525 

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

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

33277  529 
let 
530 
val V = read_prop "V"; 

531 
val VW = read_prop "V ==> W"; 

4016  532 
in 
33277  533 
store_standard_thm_open (Binding.name "revcut_rl") 
36944  534 
(Thm.implies_intr V (Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V)))) 
0  535 
end; 
536 

668  537 
(*for deleting an unwanted assumption*) 
538 
val thin_rl = 

33277  539 
let 
540 
val V = read_prop "V"; 

541 
val W = read_prop "W"; 

36944  542 
val thm = Thm.implies_intr V (Thm.implies_intr W (Thm.assume W)); 
33277  543 
in store_standard_thm_open (Binding.name "thin_rl") thm end; 
668  544 

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

33277  547 
let 
548 
val V = read_prop "V"; 

549 
val QV = read_prop "!!x::'a. V"; 

550 
val x = certify (Free ("x", Term.aT [])); 

4016  551 
in 
33277  552 
store_standard_thm_open (Binding.name "triv_forall_equality") 
36944  553 
(Thm.equal_intr (Thm.implies_intr QV (Thm.forall_elim x (Thm.assume QV))) 
554 
(Thm.implies_intr V (Thm.forall_intr x (Thm.assume V)))) 

0  555 
end; 
556 

19051  557 
(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==> 
558 
(PROP ?Phi ==> PROP ?Psi) 

559 
*) 

560 
val distinct_prems_rl = 

561 
let 

33277  562 
val AAB = read_prop "Phi ==> Phi ==> Psi"; 
24241  563 
val A = read_prop "Phi"; 
19051  564 
in 
33277  565 
store_standard_thm_open (Binding.name "distinct_prems_rl") 
36944  566 
(implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A])) 
19051  567 
end; 
568 

3653  569 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
570 
==> PROP ?phi == PROP ?psi 

8328  571 
Introduction rule for == as a metatheorem. 
3653  572 
*) 
573 
val equal_intr_rule = 

33277  574 
let 
575 
val PQ = read_prop "phi ==> psi"; 

576 
val QP = read_prop "psi ==> phi"; 

4016  577 
in 
33277  578 
store_standard_thm_open (Binding.name "equal_intr_rule") 
36944  579 
(Thm.implies_intr PQ (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP)))) 
3653  580 
end; 
581 

19421  582 
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *) 
13368  583 
val equal_elim_rule1 = 
33277  584 
let 
585 
val eq = read_prop "phi::prop == psi::prop"; 

586 
val P = read_prop "phi"; 

587 
in 

588 
store_standard_thm_open (Binding.name "equal_elim_rule1") 

36944  589 
(Thm.equal_elim (Thm.assume eq) (Thm.assume P) > implies_intr_list [eq, P]) 
13368  590 
end; 
4285  591 

19421  592 
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *) 
593 
val equal_elim_rule2 = 

33277  594 
store_standard_thm_open (Binding.name "equal_elim_rule2") 
595 
(symmetric_thm RS equal_elim_rule1); 

19421  596 

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

597 
(* PROP ?phi ==> PROP ?phi ==> PROP ?psi ==> PROP ?psi *) 
12297  598 
val remdups_rl = 
33277  599 
let 
600 
val P = read_prop "phi"; 

601 
val Q = read_prop "psi"; 

602 
val thm = implies_intr_list [P, P, Q] (Thm.assume Q); 

603 
in store_standard_thm_open (Binding.name "remdups_rl") thm end; 

12297  604 

605 

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

606 

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

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

608 

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

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

610 
val A = certify (Free ("A", propT)); 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35237
diff
changeset

611 
val axiom = Thm.unvarify_global o Thm.axiom (Context.the_theory (Context.the_thread_data ())); 
28674  612 
val prop_def = axiom "Pure.prop_def"; 
613 
val term_def = axiom "Pure.term_def"; 

614 
val sort_constraint_def = axiom "Pure.sort_constraint_def"; 

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

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

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

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

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

619 

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

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

621 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46496
diff
changeset

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

623 

33277  624 
val protectI = 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

625 
store_standard_thm (Binding.conceal (Binding.name "protectI")) 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

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

627 

33277  628 
val protectD = 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

629 
store_standard_thm (Binding.conceal (Binding.name "protectD")) 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

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

631 

33277  632 
val protect_cong = 
633 
store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A)); 

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

634 

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

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

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

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

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

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

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

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

642 

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

643 

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

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

645 

33277  646 
val termI = 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

647 
store_standard_thm (Binding.conceal (Binding.name "termI")) 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

648 
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))); 
9554  649 

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

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

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

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

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

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

655 
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

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

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

658 
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

659 

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

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

661 
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

662 
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

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

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

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

666 

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

667 
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

668 

45156  669 
val dummy_thm = mk_term (certify Term.dummy_prop); 
28618
fa09f7b8ffca
added rules for sort_constraint, include in norm_hhf_eqs;
wenzelm
parents:
27865
diff
changeset

670 

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

671 

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

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

673 

33277  674 
val sort_constraintI = 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

675 
store_standard_thm (Binding.conceal (Binding.name "sort_constraintI")) 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

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

677 

33277  678 
val sort_constraint_eq = 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

679 
store_standard_thm (Binding.conceal (Binding.name "sort_constraint_eq")) 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

680 
(Thm.equal_intr 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35237
diff
changeset

681 
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) 
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35237
diff
changeset

682 
(Thm.unvarify_global sort_constraintI))) 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

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

684 

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

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

686 

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

687 

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

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

689 

46214  690 
(* (PROP ?phi ==> (!!x. PROP ?psi x)) == (!!x. PROP ?phi ==> PROP ?psi x) *) 
9554  691 
val norm_hhf_eq = 
692 
let 

14854  693 
val aT = TFree ("'a", []); 
9554  694 
val x = Free ("x", aT); 
695 
val phi = Free ("phi", propT); 

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

697 

26487  698 
val cx = certify x; 
699 
val cphi = certify phi; 

46214  700 
val lhs = certify (Logic.mk_implies (phi, Logic.all x (psi $ x))); 
701 
val rhs = certify (Logic.all x (Logic.mk_implies (phi, psi $ x))); 

9554  702 
in 
703 
Thm.equal_intr 

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

705 
> Thm.forall_elim cx 

706 
> Thm.implies_intr cphi 

707 
> Thm.forall_intr cx 

708 
> Thm.implies_intr lhs) 

709 
(Thm.implies_elim 

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

711 
> Thm.forall_intr cx 

712 
> Thm.implies_intr cphi 

713 
> Thm.implies_intr rhs) 

33277  714 
> store_standard_thm_open (Binding.name "norm_hhf_eq") 
9554  715 
end; 
716 

18179  717 
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

718 
val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq]; 
18179  719 

30553
0709fda91b06
refined is_norm_hhf: reject betaredexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
wenzelm
parents:
30342
diff
changeset

720 
fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false 
0709fda91b06
refined is_norm_hhf: reject betaredexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
wenzelm
parents:
30342
diff
changeset

721 
 is_norm_hhf (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false 
0709fda91b06
refined is_norm_hhf: reject betaredexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
wenzelm
parents:
30342
diff
changeset

722 
 is_norm_hhf (Abs _ $ _) = false 
0709fda91b06
refined is_norm_hhf: reject betaredexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
wenzelm
parents:
30342
diff
changeset

723 
 is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u 
0709fda91b06
refined is_norm_hhf: reject betaredexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
wenzelm
parents:
30342
diff
changeset

724 
 is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t 
0709fda91b06
refined is_norm_hhf: reject betaredexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
wenzelm
parents:
30342
diff
changeset

725 
 is_norm_hhf _ = true; 
12800  726 

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

727 
fun norm_hhf thy t = 
12800  728 
if is_norm_hhf t then t 
18179  729 
else Pattern.rewrite_term thy [norm_hhf_prop] [] t; 
730 

20298  731 
fun norm_hhf_cterm ct = 
732 
if is_norm_hhf (Thm.term_of ct) then ct 

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

734 

12800  735 

21603  736 
(* var indexes *) 
737 

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

739 

740 
fun incr_indexes2 th1 th2 = 

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

742 

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

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

745 

29344  746 
fun comp_no_flatten (th, n) i rule = 
747 
(case distinct Thm.eq_thm (Seq.list_of 

52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52131
diff
changeset

748 
(Thm.bicompose {flatten = false, match = false, incremented = true} 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52131
diff
changeset

749 
(false, th, n) i (incr_indexes th rule))) of 
29344  750 
[th'] => th' 
751 
 [] => raise THM ("comp_no_flatten", i, [th, rule]) 

752 
 _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule])); 

753 

754 

9554  755 

45348
6976920b709c
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm
parents:
45347
diff
changeset

756 
(** variations on Thm.instantiate **) 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

757 

43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
43330
diff
changeset

758 
fun instantiate_normalize instpair th = 
21603  759 
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

760 

45347  761 
(*Lefttoright replacements: tpairs = [..., (vi, ti), ...]. 
762 
Instantiates distinct Vars by terms, inferring type instantiations.*) 

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

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

765 
let 
45347  766 
val {t, T, maxidx = maxt, ...} = Thm.rep_cterm ct; 
767 
val {t = u, T = U, maxidx = maxu, ...} = Thm.rep_cterm cu; 

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

769 
val thy' = Theory.merge (thy, Theory.merge (Thm.theory_of_cterm ct, Thm.theory_of_cterm cu)); 

770 
val (tye', maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) 

771 
handle Type.TUNIFY => raise TYPE ("Illtyped instantiation:\nType\n" ^ 

772 
Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^ 

773 
"\nof variable " ^ 

774 
Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^ 

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

776 
Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^ 

777 
Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u), 

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

779 
in (thy', tye', maxi') end; 

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

780 
in 
45347  781 

22561  782 
fun cterm_instantiate [] th = th 
45348
6976920b709c
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm
parents:
45347
diff
changeset

783 
 cterm_instantiate ctpairs th = 
45347  784 
let 
45348
6976920b709c
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm
parents:
45347
diff
changeset

785 
val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0); 
45347  786 
val certT = ctyp_of thy; 
45348
6976920b709c
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm
parents:
45347
diff
changeset

787 
val instT = 
6976920b709c
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm
parents:
45347
diff
changeset

788 
Vartab.fold (fn (xi, (S, T)) => 
6976920b709c
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm
parents:
45347
diff
changeset

789 
cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye []; 
6976920b709c
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm
parents:
45347
diff
changeset

790 
val inst = map (pairself (Thm.instantiate_cterm (instT, []))) ctpairs; 
6976920b709c
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm
parents:
45347
diff
changeset

791 
in instantiate_normalize (instT, inst) th end 
6976920b709c
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm
parents:
45347
diff
changeset

792 
handle TERM (msg, _) => raise THM (msg, 0, [th]) 
45347  793 
 TYPE (msg, _, _) => raise THM (msg, 0, [th]); 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

794 
end; 
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 

4285  797 
(* instantiate by lefttoright occurrence of variables *) 
798 

799 
fun instantiate' cTs cts thm = 

800 
let 

801 
fun err msg = 

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

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

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

804 
map_filter (Option.map Thm.term_of) cts); 
4285  805 

806 
fun inst_of (v, ct) = 

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

807 
(Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct) 
4285  808 
handle TYPE (msg, _, _) => err msg; 
809 

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

811 
(Thm.ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT) 
15797  812 
handle TYPE (msg, _, _) => err msg; 
813 

20298  814 
fun zip_vars xs ys = 
40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
39557
diff
changeset

815 
zip_options xs ys handle ListPair.UnequalLengths => 
20298  816 
err "more instantiations than variables in thm"; 
4285  817 

818 
(*instantiate types first!*) 

819 
val thm' = 

820 
if forall is_none cTs then thm 

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

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

826 
([], map inst_of (zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts)) thm'; 
20298  827 
in thm'' end; 
4285  828 

829 

14081  830 

831 
(** renaming of bound variables **) 

832 

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

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

835 

836 
fun rename_bvars [] thm = thm 

837 
 rename_bvars vs thm = 

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

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

839 
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

840 
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

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

842 
 ren t = t; 
36944  843 
in Thm.equal_elim (Thm.reflexive (cert (ren (Thm.prop_of thm)))) thm end; 
14081  844 

845 

846 
(* renaming in lefttoright order *) 

847 

848 
fun rename_bvars' xs thm = 

849 
let 

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

850 
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

851 
val prop = Thm.prop_of thm; 
14081  852 
fun rename [] t = ([], t) 
853 
 rename (x' :: xs) (Abs (x, T, t)) = 

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

18929  855 
in (xs', Abs (the_default x x', T, t')) end 
14081  856 
 rename xs (t $ u) = 
857 
let 

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

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

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

861 
 rename xs t = (xs, t); 

862 
in case rename xs prop of 

36944  863 
([], prop') => Thm.equal_elim (Thm.reflexive (cert prop')) thm 
14081  864 
 _ => error "More names than abstractions in theorem" 
865 
end; 

866 

11975  867 
end; 
5903  868 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

869 
structure Basic_Drule: BASIC_DRULE = Drule; 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset

870 
open Basic_Drule; 