author  wenzelm 
Thu, 13 Apr 2006 12:00:59 +0200  
changeset 19421  1051bde222db 
parent 19183  3421668ae316 
child 19482  9f11af8f7ef9 
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 

13606
2f121149acfe
Removed nRS again because extract_rews now takes care of preserving names.
berghofe
parents:
13569
diff
changeset

9 
infix 0 RS RSN RL RLN MRS MRL OF COMP; 
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 dest_implies: cterm > cterm * cterm 

16 
val dest_equals: cterm > cterm * cterm 

17 
val strip_imp_prems: cterm > cterm list 

18 
val strip_imp_concl: cterm > cterm 

19 
val cprems_of: thm > cterm list 

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

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

18206  22 
val read_insts: theory > (indexname > typ option) * (indexname > sort option) > 
23 
(indexname > typ option) * (indexname > sort option) > string list > 

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

4285  25 
val types_sorts: thm > (indexname> typ option) * (indexname> sort option) 
18179  26 
val strip_shyps_warning: thm > thm 
27 
val forall_intr_list: cterm list > thm > thm 

28 
val forall_intr_frees: thm > thm 

29 
val forall_intr_vars: thm > thm 

30 
val forall_elim_list: cterm list > thm > thm 

31 
val forall_elim_var: int > thm > thm 

32 
val forall_elim_vars: int > thm > thm 

33 
val gen_all: thm > thm 

34 
val lift_all: cterm > thm > thm 

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

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

36 
val freeze_thaw_robust: thm > thm * (int > thm > thm) 
18179  37 
val implies_elim_list: thm > thm list > thm 
38 
val implies_intr_list: cterm list > thm > thm 

18206  39 
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list > thm > thm 
18179  40 
val zero_var_indexes: thm > thm 
41 
val implies_intr_hyps: thm > thm 

42 
val standard: thm > thm 

43 
val standard': thm > thm 

44 
val rotate_prems: int > thm > thm 

45 
val rearrange_prems: int list > thm > thm 

46 
val assume_ax: theory > string > thm 

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

48 
val RS: thm * thm > thm 

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

50 
val RL: thm list * thm list > thm list 

51 
val MRS: thm list * thm > thm 

52 
val MRL: thm list list * thm list > thm list 

53 
val OF: thm * thm list > thm 

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

55 
val COMP: thm * thm > thm 

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

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

59 
val eq_thm_thy: thm * thm > bool 

60 
val eq_thm_prop: thm * thm > bool 

61 
val weak_eq_thm: thm * thm > bool 

62 
val size_of_thm: thm > int 

63 
val reflexive_thm: thm 

64 
val symmetric_thm: thm 

65 
val transitive_thm: thm 

66 
val symmetric_fun: thm > thm 

67 
val extensional: thm > thm 

18820  68 
val equals_cong: thm 
18179  69 
val imp_cong: thm 
70 
val swap_prems_eq: thm 

71 
val equal_abs_elim: cterm > thm > thm 

4285  72 
val equal_abs_elim_list: cterm list > thm > thm 
18179  73 
val asm_rl: thm 
74 
val cut_rl: thm 

75 
val revcut_rl: thm 

76 
val thin_rl: thm 

4285  77 
val triv_forall_equality: thm 
19051  78 
val distinct_prems_rl: thm 
18179  79 
val swap_prems_rl: thm 
80 
val equal_intr_rule: thm 

81 
val equal_elim_rule1: thm 

19421  82 
val equal_elim_rule2: thm 
18179  83 
val inst: string > string > thm > thm 
84 
val instantiate': ctyp option list > cterm option list > thm > thm 

5903  85 
end; 
86 

87 
signature DRULE = 

88 
sig 

89 
include BASIC_DRULE 

19421  90 
val dest_binop: cterm > cterm * cterm 
15949  91 
val list_comb: cterm * cterm list > cterm 
12908
53bfe07a7916
New function strip_comb (cterm version of Term.strip_comb).
berghofe
parents:
12800
diff
changeset

92 
val strip_comb: cterm > cterm * cterm list 
15262  93 
val strip_type: ctyp > ctyp list * ctyp 
15949  94 
val beta_conv: cterm > cterm > cterm 
15875  95 
val plain_prop_of: thm > term 
15669  96 
val add_used: thm > string list > string list 
17713  97 
val flexflex_unique: thm > thm 
11975  98 
val close_derivation: thm > thm 
12005  99 
val local_standard: thm > thm 
19421  100 
val store_thm: bstring > thm > thm 
101 
val store_standard_thm: bstring > thm > thm 

102 
val store_thm_open: bstring > thm > thm 

103 
val store_standard_thm_open: bstring > thm > thm 

11975  104 
val compose_single: thm * int * thm > thm 
12373  105 
val add_rule: thm > thm list > thm list 
106 
val del_rule: thm > thm list > thm list 

11975  107 
val merge_rules: thm list * thm list > thm list 
18468  108 
val imp_cong_rule: thm > thm > thm 
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

109 
val beta_eta_conversion: cterm > thm 
15925  110 
val eta_long_conversion: cterm > thm 
18468  111 
val forall_conv: int > (cterm > thm) > cterm > thm 
112 
val concl_conv: int > (cterm > thm) > cterm > thm 

113 
val prems_conv: int > (int > cterm > thm) > cterm > thm 

18179  114 
val goals_conv: (int > bool) > (cterm > thm) > cterm > thm 
115 
val fconv_rule: (cterm > thm) > thm > thm 

11975  116 
val norm_hhf_eq: thm 
12800  117 
val is_norm_hhf: term > bool 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

118 
val norm_hhf: theory > term > term 
18025  119 
val protect: cterm > cterm 
120 
val protectI: thm 

121 
val protectD: thm 

18179  122 
val protect_cong: thm 
18025  123 
val implies_intr_protected: cterm list > thm > thm 
11975  124 
val freeze_all: thm > thm 
125 
val tvars_of_terms: term list > (indexname * sort) list 

126 
val vars_of_terms: term list > (indexname * typ) list 

127 
val tvars_of: thm > (indexname * sort) list 

128 
val vars_of: thm > (indexname * typ) list 

18129  129 
val tfrees_of: thm > (string * sort) list 
130 
val frees_of: thm > (string * typ) list 

131 
val fold_terms: (term > 'a > 'a) > thm > 'a > 'a 

14081  132 
val rename_bvars: (string * string) list > thm > thm 
133 
val rename_bvars': string option list > thm > thm 

11975  134 
val unvarifyT: thm > thm 
135 
val unvarify: thm > thm 

18129  136 
val tvars_intr_list: string list > thm > (string * (indexname * sort)) list * thm 
19124  137 
val incr_indexes: thm > thm > thm 
138 
val incr_indexes2: thm > thm > thm > thm 

12297  139 
val remdups_rl: thm 
18225  140 
val multi_resolve: thm list > thm > thm Seq.seq 
141 
val multi_resolves: thm list > thm list > thm Seq.seq 

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

143 
val read_instantiate_sg': theory > (indexname * string) list > thm > thm 
15797  144 
val read_instantiate': (indexname * string) list > thm > thm 
3766  145 
end; 
0  146 

5903  147 
structure Drule: DRULE = 
0  148 
struct 
149 

3991  150 

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

152 

19124  153 
fun dest_binop ct = 
154 
let val (ct1, ct2) = Thm.dest_comb ct 

155 
in (#2 (Thm.dest_comb ct1), ct2) end; 

156 

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

157 
fun dest_implies ct = 
16682  158 
(case Thm.term_of ct of 
19124  159 
(Const ("==>", _) $ _ $ _) => dest_binop ct 
16682  160 
 _ => raise TERM ("dest_implies", [term_of ct])); 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

161 

10414  162 
fun dest_equals ct = 
16682  163 
(case Thm.term_of ct of 
19124  164 
(Const ("==", _) $ _ $ _) => dest_binop ct 
16682  165 
 _ => raise TERM ("dest_equals", [term_of ct])); 
10414  166 

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

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

168 
fun strip_imp_prems ct = 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

169 
let val (cA,cB) = dest_implies ct 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

170 
in cA :: strip_imp_prems cB end 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

171 
handle TERM _ => []; 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

172 

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

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

174 
fun strip_imp_concl ct = 
8328  175 
case term_of ct of (Const("==>", _) $ _ $ _) => 
10767
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10667
diff
changeset

176 
strip_imp_concl (#2 (Thm.dest_comb ct)) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

177 
 _ => ct; 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

178 

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

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

180 
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

181 

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

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

184 
in Thm.cterm_of thy (f t) end; 
15797  185 

186 
fun ctyp_fun f cT = 

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

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

188 
in Thm.ctyp_of thy (f T) end; 
15797  189 

19421  190 
val cert = cterm_of ProtoPure.thy; 
9547  191 

19421  192 
val implies = cert Term.implies; 
19183  193 
fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B; 
9547  194 

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

196 
fun list_implies([], B) = B 

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

198 

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

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

202 

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

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

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

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

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

208 
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

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

210 

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

213 
Type ("fun", _) => 

214 
let 

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

216 
val (cTs, cT') = strip_type cT2 

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

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

219 

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

18179  222 
fun beta_conv x y = 
15949  223 
#2 (Thm.dest_comb (cprop_of (Thm.beta_conversion false (Thm.capply x y)))); 
224 

15875  225 
fun plain_prop_of raw_thm = 
226 
let 

227 
val thm = Thm.strip_shyps raw_thm; 

228 
fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); 

229 
val {hyps, prop, tpairs, ...} = Thm.rep_thm thm; 

230 
in 

231 
if not (null hyps) then 

232 
err "theorem may not contain hypotheses" 

233 
else if not (null (Thm.extra_shyps thm)) then 

234 
err "theorem may not contain sort hypotheses" 

235 
else if not (null tpairs) then 

236 
err "theorem may not contain flexflex pairs" 

237 
else prop 

238 
end; 

239 

240 

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

241 

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

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

243 

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

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

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

246 

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

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

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

249 

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

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

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

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

256 
fun readT (ixn, st) = 
15797  257 
let val S = sort_of ixn; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

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

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

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

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

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

263 
fun mkty(ixn,st) = (case rtypes ixn of 
15531  264 
SOME T => (ixn,(st,typ_subst_TVars tye T)) 
265 
 NONE => absent ixn); 

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

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

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

268 
and sTs = map snd ixnsTs 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

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

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

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

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

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

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

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

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

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

278 

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

279 

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

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

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

284 
***) 

285 

286 
fun types_sorts thm = 

15669  287 
let val {prop, hyps, tpairs, ...} = Thm.rep_thm thm; 
288 
(* bogus term! *) 

18179  289 
val big = Term.list_comb 
15949  290 
(Term.list_comb (prop, hyps), Thm.terms_of_tpairs tpairs); 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

291 
val vars = map dest_Var (term_vars big); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

292 
val frees = map dest_Free (term_frees big); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

293 
val tvars = term_tvars big; 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

294 
val tfrees = term_tfrees big; 
17325  295 
fun typ(a,i) = if i<0 then AList.lookup (op =) frees a else AList.lookup (op =) vars (a,i); 
296 
fun sort(a,i) = if i<0 then AList.lookup (op =) tfrees a else AList.lookup (op =) tvars (a,i); 

0  297 
in (typ,sort) end; 
298 

15669  299 
fun add_used thm used = 
300 
let val {prop, hyps, tpairs, ...} = Thm.rep_thm thm in 

301 
add_term_tvarnames (prop, used) 

302 
> fold (curry add_term_tvarnames) hyps 

303 
> fold (curry add_term_tvarnames) (Thm.terms_of_tpairs tpairs) 

304 
end; 

305 

7636  306 

9455  307 

0  308 
(** Standardization of rules **) 
309 

18025  310 
(*vars in lefttoright order*) 
311 
fun tvars_of_terms ts = rev (fold Term.add_tvars ts []); 

312 
fun vars_of_terms ts = rev (fold Term.add_vars ts []); 

313 
fun tvars_of thm = tvars_of_terms [Thm.full_prop_of thm]; 

314 
fun vars_of thm = vars_of_terms [Thm.full_prop_of thm]; 

315 

18129  316 
fun fold_terms f th = 
317 
let val {hyps, tpairs, prop, ...} = Thm.rep_thm th 

318 
in f prop #> fold (fn (t, u) => f t #> f u) tpairs #> fold f hyps end; 

319 

320 
fun tfrees_of th = rev (fold_terms Term.add_tfrees th []); 

321 
fun frees_of th = rev (fold_terms Term.add_frees th []); 

322 

7636  323 
(*Strip extraneous shyps as far as possible*) 
324 
fun strip_shyps_warning thm = 

325 
let 

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

326 
val str_of_sort = Pretty.str_of o Sign.pretty_sort (Thm.theory_of_thm thm); 
7636  327 
val thm' = Thm.strip_shyps thm; 
328 
val xshyps = Thm.extra_shyps thm'; 

329 
in 

330 
if null xshyps then () 

331 
else warning ("Pending sort hypotheses: " ^ commas (map str_of_sort xshyps)); 

332 
thm' 

333 
end; 

334 

0  335 
(*Generalization over a list of variables, IGNORING bad ones*) 
336 
fun forall_intr_list [] th = th 

337 
 forall_intr_list (y::ys) th = 

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

338 
let val gth = forall_intr_list ys th 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

339 
in forall_intr y gth handle THM _ => gth end; 
0  340 

341 
(*Generalization over all suitable Free variables*) 

342 
fun forall_intr_frees th = 

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

343 
let val {prop,thy,...} = rep_thm th 
0  344 
in forall_intr_list 
16983  345 
(map (cterm_of thy) (sort Term.term_ord (term_frees prop))) 
0  346 
th 
347 
end; 

348 

18535  349 
(*Generalization over Vars  canonical order*) 
350 
fun forall_intr_vars th = 

351 
let val cert = Thm.cterm_of (Thm.theory_of_thm th) 

352 
in forall_intr_list (map (cert o Var) (vars_of th)) th end; 

353 

7898  354 
val forall_elim_var = PureThy.forall_elim_var; 
355 
val forall_elim_vars = PureThy.forall_elim_vars; 

0  356 

18025  357 
fun outer_params t = 
358 
let 

359 
val vs = Term.strip_all_vars t; 

18375  360 
val xs = Term.variantlist (map (perhaps (try Syntax.dest_skolem) o #1) vs, []); 
18025  361 
in xs ~~ map #2 vs end; 
362 

363 
(*generalize outermost parameters*) 

364 
fun gen_all th = 

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

365 
let 
18025  366 
val {thy, prop, maxidx, ...} = Thm.rep_thm th; 
367 
val cert = Thm.cterm_of thy; 

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

369 
in fold elim (outer_params prop) th end; 

370 

371 
(*lift vars wrt. outermost goal parameters 

18118  372 
 reverses the effect of gen_all modulo higherorder unification*) 
18025  373 
fun lift_all goal th = 
374 
let 

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

376 
val cert = Thm.cterm_of thy; 

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

380 
val Ts = map Term.fastype_of ps; 

381 
val inst = vars_of th > map (fn (xi, T) => 

382 
(cert (Var (xi, T)), cert (Term.list_comb (Var (xi, Ts > T), ps)))); 

383 
in 

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

385 
> fold_rev (Thm.forall_intr o cert) ps 

386 
end; 

387 

9554  388 

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

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

390 
val forall_elim_list = fold forall_elim; 
0  391 

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

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

393 
val implies_intr_list = fold_rev implies_intr; 
0  394 

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

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

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

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

399 
fun zero_var_indexes th = 
16949
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

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

401 
val thy = Thm.theory_of_thm th; 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

402 
val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy; 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

403 
val (instT, inst) = Term.zero_var_indexes_inst (Thm.full_prop_of th); 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

404 
val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT; 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

405 
val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst; 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

406 
in Thm.adjust_maxidx_thm (Thm.instantiate (cinstT, cinst) th) end; 
0  407 

408 

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

10515  411 

16595  412 
(*Discharge all hypotheses.*) 
413 
fun implies_intr_hyps th = 

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

415 

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

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

418 
fun flexflex_unique th = 
17713  419 
if null (tpairs_of th) then th else 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14340
diff
changeset

420 
case Seq.chop (2, flexflex_rule th) of 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14340
diff
changeset

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

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

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

424 

10515  425 
fun close_derivation thm = 
426 
if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm) 

427 
else thm; 

428 

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

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

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

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

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

434 
forall_elim_vars (maxidx + 1) 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

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

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

437 
#> Thm.varifyT 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

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

439 

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

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

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

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

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

444 

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

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

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

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

448 
#> Thm.compress 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

449 
#> close_derivation; 
12005  450 

0  451 

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

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

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

455 

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

456 
fun freeze_thaw_robust th = 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

457 
let val fth = freezeT th 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

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

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

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

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

462 
 vars => 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

463 
let fun newName (Var(ix,_), pairs) = 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

464 
let val v = gensym (string_of_indexname ix) 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

465 
in ((ix,v)::pairs) end; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

466 
val alist = foldr newName [] vars 
15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

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

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

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

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

472 
th' > forall_intr_list (map #2 insts) 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

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

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

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

476 

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

477 
(*Basic version of the function above. No option to rename Vars apart in thaw. 
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15442
diff
changeset

478 
The Frees created from Vars have nice names.*) 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

479 
fun freeze_thaw th = 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

480 
let val fth = freezeT th 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

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

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

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

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

485 
 vars => 
8328  486 
let fun newName (Var(ix,_), (pairs,used)) = 
487 
let val v = variant used (string_of_indexname ix) 

488 
in ((ix,v)::pairs, v::used) end; 

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

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

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

492 
(cterm_of thy (Var(v,T)), 
17325  493 
cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) 
8328  494 
val insts = map mk_inst vars 
495 
fun thaw th' = 

496 
th' > forall_intr_list (map #2 insts) 

497 
> forall_elim_list (map #1 insts) 

498 
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

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

500 

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

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

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

503 

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

506 
Any remaining trailing positions are left unchanged. *) 

507 
val rearrange_prems = let 

508 
fun rearr new [] thm = thm 

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

512 
in rearr 0 end; 

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

513 

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

514 
(*Assume a new formula, read following the same conventions as axioms. 
0  515 
Generalizes over Free variables, 
516 
creates the assumption, and then strips quantifiers. 

517 
Example is [ ALL x:?A. ?P(x) ] ==> [ ?P(?a) ] 

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

518 
[ !(A,P,a)[ ALL x:A. P(x) ] ==> [ P(a) ] ] *) 
0  519 
fun assume_ax thy sP = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

520 
let val prop = Logic.close_form (term_of (read_cterm thy (sP, propT))) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

521 
in forall_elim_vars 0 (Thm.assume (cterm_of thy prop)) end; 
0  522 

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

523 
(*Resolution: exactly one resolvent must be produced.*) 
0  524 
fun tha RSN (i,thb) = 
4270  525 
case Seq.chop (2, biresolution false [(false,tha)] i thb) of 
0  526 
([th],_) => th 
527 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

529 

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

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

532 

533 
(*For joining lists of rules*) 

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

534 
fun thas RLN (i,thbs) = 
0  535 
let val resolve = biresolution false (map (pair false) thas) i 
4270  536 
fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] 
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2266
diff
changeset

537 
in List.concat (map resb thbs) end; 
0  538 

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

540 

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

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

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

543 
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

544 
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

545 
 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

546 
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

547 

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

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

549 
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

550 
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

551 
 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

552 
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

553 

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

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

555 
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

556 

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

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

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

560 
fun compose(tha,i,thb) = 
4270  561 
Seq.list_of (bicompose false (false,tha,0) i thb); 
0  562 

6946  563 
fun compose_single (tha,i,thb) = 
564 
(case compose (tha,i,thb) of 

565 
[th] => th 

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

567 

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

570 
case compose(tha,1,thb) of 

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

571 
[th] => th 
0  572 
 _ => raise THM("COMP", 1, [tha,thb]); 
573 

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

574 

4016  575 
(** theorem equality **) 
0  576 

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

577 
(*True if the two theorems have the same theory.*) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

578 
val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm; 
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13606
diff
changeset

579 

31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13606
diff
changeset

580 
(*True if the two theorems have the same prop field, ignoring hyps, der, etc.*) 
16720  581 
val eq_thm_prop = op aconv o pairself Thm.full_prop_of; 
0  582 

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

16720  584 
val size_of_thm = size_of_term o Thm.full_prop_of; 
0  585 

9829  586 
(*maintain lists of theorems  preserving canonical order*) 
18922  587 
val del_rule = remove eq_thm_prop; 
588 
fun add_rule th = cons th o del_rule th; 

589 
val merge_rules = Library.merge eq_thm_prop; 

9829  590 

18535  591 
(*weak_eq_thm: ignores variable renaming and (some) type variable renaming*) 
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12908
diff
changeset

592 
val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT); 
1194
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

593 

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

594 

0  595 
(*** MetaRewriting Rules ***) 
596 

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

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

598 

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

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

4016  603 

0  604 
val reflexive_thm = 
19421  605 
let val cx = cert (Var(("x",0),TVar(("'a",0),[]))) 
12135  606 
in store_standard_thm_open "reflexive" (Thm.reflexive cx) end; 
0  607 

608 
val symmetric_thm = 

14854  609 
let val xy = read_prop "x == y" 
16595  610 
in store_standard_thm_open "symmetric" (Thm.implies_intr xy (Thm.symmetric (Thm.assume xy))) end; 
0  611 

612 
val transitive_thm = 

14854  613 
let val xy = read_prop "x == y" 
614 
val yz = read_prop "y == z" 

0  615 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
12135  616 
in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 
0  617 

4679  618 
fun symmetric_fun thm = thm RS symmetric_thm; 
619 

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

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

621 
let val eq' = 
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

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

623 
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

624 

18820  625 
val equals_cong = 
626 
store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x == y")); 

627 

10414  628 
val imp_cong = 
629 
let 

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

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

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

633 
val A = read_prop "PROP A" 

634 
in 

12135  635 
store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr 
10414  636 
(implies_intr AB (implies_intr A 
637 
(equal_elim (implies_elim (assume ABC) (assume A)) 

638 
(implies_elim (assume AB) (assume A))))) 

639 
(implies_intr AC (implies_intr A 

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

641 
(implies_elim (assume AC) (assume A))))))) 

642 
end; 

643 

644 
val swap_prems_eq = 

645 
let 

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

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

648 
val A = read_prop "PROP A" 

649 
val B = read_prop "PROP B" 

650 
in 

12135  651 
store_standard_thm_open "swap_prems_eq" (equal_intr 
10414  652 
(implies_intr ABC (implies_intr B (implies_intr A 
653 
(implies_elim (implies_elim (assume ABC) (assume A)) (assume B))))) 

654 
(implies_intr BAC (implies_intr A (implies_intr B 

655 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

656 
end; 

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

657 

18468  658 
val imp_cong_rule = combination o combination (reflexive implies); 
0  659 

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

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

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

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

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

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

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

666 
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

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

668 

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

671 

18337  672 
val abs_def = 
673 
let 

674 
fun contract_lhs th = 

675 
Thm.transitive (Thm.symmetric (beta_eta_conversion (fst (dest_equals (cprop_of th))))) th; 

18777  676 
fun abstract cx th = Thm.abstract_rule 
677 
(case Thm.term_of cx of Var ((x, _), _) => x  Free (x, _) => x  _ => "x") cx th 

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

18337  679 
in 
680 
contract_lhs 

681 
#> `(snd o strip_comb o fst o dest_equals o cprop_of) 

682 
#> fold_rev abstract 

683 
#> contract_lhs 

684 
end; 

685 

18468  686 
(*rewrite B in !!x1 ... xn. B*) 
18251  687 
fun forall_conv 0 cv ct = cv ct 
688 
 forall_conv n cv ct = 

18468  689 
(case try Thm.dest_comb ct of 
690 
NONE => cv ct 

691 
 SOME (A, B) => 

692 
(case (term_of A, term_of B) of 

693 
(Const ("all", _), Abs (x, _, _)) => 

694 
let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in 

695 
Thm.combination (Thm.reflexive A) 

696 
(Thm.abstract_rule x v (forall_conv (n  1) cv B')) 

697 
end 

698 
 _ => cv ct)); 

699 

700 
(*rewrite B in A1 ==> ... ==> An ==> B*) 

701 
fun concl_conv 0 cv ct = cv ct 

702 
 concl_conv n cv ct = 

703 
(case try dest_implies ct of 

704 
NONE => cv ct 

705 
 SOME (A, B) => imp_cong_rule (reflexive A) (concl_conv (n  1) cv B)); 

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

706 

18468  707 
(*rewrite the A's in A1 ==> ... ==> An ==> B*) 
708 
fun prems_conv 0 _ = reflexive 

709 
 prems_conv n cv = 

710 
let 

711 
fun conv i ct = 

712 
if i = n + 1 then reflexive ct 

713 
else 

714 
(case try dest_implies ct of 

715 
NONE => reflexive ct 

716 
 SOME (A, B) => imp_cong_rule (cv i A) (conv (i + 1) B)); 

717 
in conv 1 end; 

718 

719 
fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else reflexive); 

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

720 
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; 
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14854
diff
changeset

721 

18468  722 

15669  723 
(*** Some useful metatheorems ***) 
0  724 

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

12135  726 
val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi")); 
7380  727 
val _ = store_thm "_" asm_rl; 
0  728 

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

4016  730 
val cut_rl = 
12135  731 
store_standard_thm_open "cut_rl" 
9455  732 
(Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta")); 
0  733 

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

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

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

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

738 
and VW = read_prop "PROP V ==> PROP W"; 
4016  739 
in 
12135  740 
store_standard_thm_open "revcut_rl" 
4016  741 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  742 
end; 
743 

668  744 
(*for deleting an unwanted assumption*) 
745 
val thin_rl = 

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

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

747 
and W = read_prop "PROP W"; 
12135  748 
in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end; 
668  749 

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

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

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

753 
and QV = read_prop "!!x::'a. PROP V" 
19421  754 
and x = cert (Free ("x", Term.aT [])); 
4016  755 
in 
12135  756 
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

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

758 
(implies_intr V (forall_intr x (assume V)))) 
0  759 
end; 
760 

19051  761 
(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==> 
762 
(PROP ?Phi ==> PROP ?Psi) 

763 
*) 

764 
val distinct_prems_rl = 

765 
let 

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

767 
val A = read_prop "PROP Phi"; 

768 
in 

769 
store_standard_thm_open "distinct_prems_rl" 

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

771 
end; 

772 

1756  773 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
774 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

776 
*) 

777 
val swap_prems_rl = 

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

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

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

782 
val cminor2 = read_prop "PROP PhiB"; 
1756  783 
val minor2 = assume cminor2; 
12135  784 
in store_standard_thm_open "swap_prems_rl" 
1756  785 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
786 
(implies_elim (implies_elim major minor1) minor2)))) 

787 
end; 

788 

3653  789 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
790 
==> PROP ?phi == PROP ?psi 

8328  791 
Introduction rule for == as a metatheorem. 
3653  792 
*) 
793 
val equal_intr_rule = 

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

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

795 
and QP = read_prop "PROP psi ==> PROP phi" 
4016  796 
in 
12135  797 
store_standard_thm_open "equal_intr_rule" 
4016  798 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  799 
end; 
800 

19421  801 
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *) 
13368  802 
val equal_elim_rule1 = 
803 
let val eq = read_prop "PROP phi == PROP psi" 

804 
and P = read_prop "PROP phi" 

805 
in store_standard_thm_open "equal_elim_rule1" 

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

807 
end; 

4285  808 

19421  809 
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *) 
810 
val equal_elim_rule2 = 

811 
store_standard_thm_open "equal_elim_rule2" (symmetric_thm RS equal_elim_rule1); 

812 

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

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

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

817 

818 

9554  819 
(*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) 
12297  820 
Rewrite rule for HHF normalization.*) 
9554  821 

822 
val norm_hhf_eq = 

823 
let 

14854  824 
val aT = TFree ("'a", []); 
9554  825 
val all = Term.all aT; 
826 
val x = Free ("x", aT); 

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

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

829 

830 
val cx = cert x; 

831 
val cphi = cert phi; 

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

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

834 
in 

835 
Thm.equal_intr 

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

837 
> Thm.forall_elim cx 

838 
> Thm.implies_intr cphi 

839 
> Thm.forall_intr cx 

840 
> Thm.implies_intr lhs) 

841 
(Thm.implies_elim 

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

843 
> Thm.forall_intr cx 

844 
> Thm.implies_intr cphi 

845 
> Thm.implies_intr rhs) 

12135  846 
> store_standard_thm_open "norm_hhf_eq" 
9554  847 
end; 
848 

18179  849 
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); 
850 

12800  851 
fun is_norm_hhf tm = 
852 
let 

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

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

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

856 
 is_norm _ = true; 

18929  857 
in is_norm (Envir.beta_eta_contract tm) end; 
12800  858 

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

859 
fun norm_hhf thy t = 
12800  860 
if is_norm_hhf t then t 
18179  861 
else Pattern.rewrite_term thy [norm_hhf_prop] [] t; 
862 

12800  863 

9554  864 

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

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

866 

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

867 
(*Version that normalizes the result: Thm.instantiate no longer does that*) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

868 
fun instantiate instpair th = Thm.instantiate instpair th COMP asm_rl; 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

869 

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

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

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

873 
in instantiate (read_insts thy ts ts used sinsts) th end; 
15797  874 

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

875 
fun read_instantiate_sg thy sinsts th = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

876 
read_instantiate_sg' thy (map (apfst Syntax.indexname) sinsts) th; 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

877 

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

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

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

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

881 

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

883 
read_instantiate_sg' (Thm.theory_of_thm th) sinsts th; 
15797  884 

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

885 

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

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

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

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

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

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

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

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

893 
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

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

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

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

898 
fun cterm_instantiate ctpairs0 th = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

899 
let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0 
18179  900 
fun instT(ct,cu) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

901 
let val inst = cterm_of thy o Envir.subst_TVars tye o term_of 
14340
bc93ffa674cc
correction to cterm_instantiate by Christoph Leuth
paulson
parents:
14081
diff
changeset

902 
in (inst ct, inst cu) end 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

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

904 
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

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

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

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

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

909 

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

910 

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

911 
(** Derived rules mainly for METAHYPS **) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

912 

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

913 
(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

914 
fun equal_abs_elim ca eqth = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

915 
let val {thy=thya, t=a, ...} = rep_cterm ca 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

916 
and combth = combination eqth (reflexive ca) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

917 
val {thy,prop,...} = rep_thm eqth 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

918 
val (abst,absu) = Logic.dest_equals prop 
19421  919 
val cert = cterm_of (Theory.merge (thy,thya)) 
920 
in transitive (symmetric (beta_conversion false (cert (abst$a)))) 

921 
(transitive combth (beta_conversion false (cert (absu$a)))) 

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

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

923 
handle THM _ => raise THM("equal_abs_elim", 0, [eqth]); 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

924 

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

925 
(*Calling equal_abs_elim with multiple terms*) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

926 
fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) th (rev cts); 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

927 

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

928 

18025  929 
(** protected propositions **) 
4789  930 

931 
local 

18025  932 
val A = cert (Free ("A", propT)); 
933 
val prop_def = #1 (freeze_thaw ProtoPure.prop_def); 

4789  934 
in 
18025  935 
val protect = Thm.capply (cert Logic.protectC); 
18799  936 
val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard 
18025  937 
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)))); 
18799  938 
val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard 
18025  939 
(Thm.equal_elim prop_def (Thm.assume (protect A))))); 
18179  940 
val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A)); 
4789  941 
end; 
942 

18025  943 
fun implies_intr_protected asms th = 
18118  944 
let val asms' = map protect asms in 
945 
implies_elim_list 

946 
(implies_intr_list asms th) 

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

948 
> implies_intr_list asms' 

949 
end; 

11815  950 

4789  951 

5688  952 
(** variations on instantiate **) 
4285  953 

8550
b44c185f8018
new metarule "inst", a shorthand for read_instantiate_sg
paulson
parents:
8496
diff
changeset

954 
(*shorthand for instantiating just one variable in the current theory*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

955 
fun inst x t = read_instantiate_sg (the_context()) [(x,t)]; 
8550
b44c185f8018
new metarule "inst", a shorthand for read_instantiate_sg
paulson
parents:
8496
diff
changeset

956 

b44c185f8018
new metarule "inst", a shorthand for read_instantiate_sg
paulson
parents:
8496
diff
changeset

957 

4285  958 
(* instantiate by lefttoright occurrence of variables *) 
959 

960 
fun instantiate' cTs cts thm = 

961 
let 

962 
fun err msg = 

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

15570  964 
List.mapPartial (Option.map Thm.typ_of) cTs, 
965 
List.mapPartial (Option.map Thm.term_of) cts); 

4285  966 

967 
fun inst_of (v, ct) = 

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

968 
(Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct) 
4285  969 
handle TYPE (msg, _, _) => err msg; 
970 

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

972 
(Thm.ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT) 
15797  973 
handle TYPE (msg, _, _) => err msg; 
974 

4285  975 
fun zip_vars _ [] = [] 
15531  976 
 zip_vars (_ :: vs) (NONE :: opt_ts) = zip_vars vs opt_ts 
977 
 zip_vars (v :: vs) (SOME t :: opt_ts) = (v, t) :: zip_vars vs opt_ts 

4285  978 
 zip_vars [] _ = err "more instantiations than variables in thm"; 
979 

980 
(*instantiate types first!*) 

981 
val thm' = 

982 
if forall is_none cTs then thm 

15797  983 
else Thm.instantiate (map tyinst_of (zip_vars (tvars_of thm) cTs), []) thm; 
4285  984 
in 
985 
if forall is_none cts then thm' 

986 
else Thm.instantiate ([], map inst_of (zip_vars (vars_of thm') cts)) thm' 

987 
end; 

988 

989 

14081  990 

991 
(** renaming of bound variables **) 

992 

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

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

995 

996 
fun rename_bvars [] thm = thm 

997 
 rename_bvars vs thm = 

998 
let 

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

999 
val {thy, prop, ...} = rep_thm thm; 
17325  1000 
fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x > the_default x, T, ren t) 
14081  1001 
 ren (t $ u) = ren t $ ren u 
1002 
 ren t = t; 

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

1003 
in equal_elim (reflexive (cterm_of thy (ren prop))) thm end; 
14081  1004 

1005 

1006 
(* renaming in lefttoright order *) 

1007 

1008 
fun rename_bvars' xs thm = 

1009 
let 

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

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

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

18929  1014 
in (xs', Abs (the_default x x', T, t')) end 
14081  1015 
 rename xs (t $ u) = 
1016 
let 

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

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

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

1020 
 rename xs t = (xs, t); 

1021 
in case rename xs prop of 

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

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

1025 

1026 

1027 

5688  1028 
(* unvarify(T) *) 
1029 

1030 
(*assume thm in standard form, i.e. no frees, 0 var indexes*) 

1031 

1032 
fun unvarifyT thm = 

1033 
let 

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

1034 
val cT = Thm.ctyp_of (Thm.theory_of_thm thm); 
15531  1035 
val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (tvars_of thm); 
5688  1036 
in instantiate' tfrees [] thm end; 
1037 

1038 
fun unvarify raw_thm = 

1039 
let 

1040 
val thm = unvarifyT raw_thm; 

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

1041 
val ct = Thm.cterm_of (Thm.theory_of_thm thm); 
15531  1042 
val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (vars_of thm); 
5688  1043 
in instantiate' [] frees thm end; 
1044 

1045 

8605  1046 
(* tvars_intr_list *) 
1047 

1048 
fun tvars_intr_list tfrees thm = 

18129  1049 
apfst (map (fn ((s, S), ixn) => (s, (ixn, S)))) (Thm.varifyT' 
15797  1050 
(gen_rems (op = o apfst fst) (tfrees_of thm, tfrees)) thm); 
8605  1051 

1052 

6435  1053 
(* increment var indexes *) 
1054 

19421  1055 
fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1); 
18025  1056 

19124  1057 
fun incr_indexes2 th1 th2 = 
19421  1058 
Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1); 
6435  1059 

1060 

8328  1061 
(* freeze_all *) 
1062 

1063 
(*freeze all (T)Vars; assumes thm in standard form*) 

1064 

1065 
fun freeze_all_TVars thm = 

1066 
(case tvars_of thm of 

1067 
[] => thm 

1068 
 tvars => 

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

1069 
let val cert = Thm.ctyp_of (Thm.theory_of_thm thm) 
15531  1070 
in instantiate' (map (fn ((x, _), S) => SOME (cert (TFree (x, S)))) tvars) [] thm end); 
8328  1071 

1072 
fun freeze_all_Vars thm = 

1073 
(case vars_of thm of 

1074 
[] => thm 

1075 
 vars => 

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

1076 
let val cert = Thm.cterm_of (Thm.theory_of_thm thm) 
15531  1077 
in instantiate' [] (map (fn ((x, _), T) => SOME (cert (Free (x, T)))) vars) thm end); 
8328  1078 

1079 
val freeze_all = freeze_all_Vars o freeze_all_TVars; 

1080 

1081 

11975  1082 

18225  1083 
(** multi_resolve **) 
1084 

1085 
local 

1086 

1087 
fun res th i rule = 

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

1089 

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

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

1092 

1093 
in 

1094 

1095 
val multi_resolve = multi_res 1; 

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

1097 

1098 
end; 

1099 

11975  1100 
end; 
5903  1101 

1102 
structure BasicDrule: BASIC_DRULE = Drule; 

1103 
open BasicDrule; 