author  wenzelm 
Mon, 06 Feb 2006 20:58:54 +0100  
changeset 18929  d81435108688 
parent 18922  b05a2952de73 
child 19051  5212516f1a98 
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 
18179  78 
val swap_prems_rl: thm 
79 
val equal_intr_rule: thm 

80 
val equal_elim_rule1: thm 

81 
val inst: string > string > thm > thm 

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

83 
val incr_indexes: thm > thm > thm 

84 
val incr_indexes_wrt: int list > ctyp list > cterm list > thm list > thm > thm 

5903  85 
end; 
86 

87 
signature DRULE = 

88 
sig 

89 
include BASIC_DRULE 

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

91 
val strip_comb: cterm > cterm * cterm list 
15262  92 
val strip_type: ctyp > ctyp list * ctyp 
15949  93 
val beta_conv: cterm > cterm > cterm 
15875  94 
val plain_prop_of: thm > term 
15669  95 
val add_used: thm > string list > string list 
17713  96 
val flexflex_unique: thm > thm 
11975  97 
val close_derivation: thm > thm 
12005  98 
val local_standard: thm > thm 
11975  99 
val compose_single: thm * int * thm > thm 
12373  100 
val add_rule: thm > thm list > thm list 
101 
val del_rule: thm > thm list > thm list 

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

104 
val beta_eta_conversion: cterm > thm 
15925  105 
val eta_long_conversion: cterm > thm 
18468  106 
val forall_conv: int > (cterm > thm) > cterm > thm 
107 
val concl_conv: int > (cterm > thm) > cterm > thm 

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

109 
val conjunction_conv: int > (int > cterm > thm) > cterm > thm 

18179  110 
val goals_conv: (int > bool) > (cterm > thm) > cterm > thm 
111 
val fconv_rule: (cterm > thm) > thm > thm 

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

114 
val norm_hhf: theory > term > term 
18025  115 
val protect: cterm > cterm 
116 
val protectI: thm 

117 
val protectD: thm 

18179  118 
val protect_cong: thm 
18025  119 
val implies_intr_protected: cterm list > thm > thm 
11975  120 
val freeze_all: thm > thm 
121 
val tvars_of_terms: term list > (indexname * sort) list 

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

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

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

18129  125 
val tfrees_of: thm > (string * sort) list 
126 
val frees_of: thm > (string * typ) list 

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

14081  128 
val rename_bvars: (string * string) list > thm > thm 
129 
val rename_bvars': string option list > thm > thm 

11975  130 
val unvarifyT: thm > thm 
131 
val unvarify: thm > thm 

18129  132 
val tvars_intr_list: string list > thm > (string * (indexname * sort)) list * thm 
12297  133 
val remdups_rl: thm 
18225  134 
val multi_resolve: thm list > thm > thm Seq.seq 
135 
val multi_resolves: thm list > thm list > thm Seq.seq 

11975  136 
val conj_intr: thm > thm > thm 
137 
val conj_intr_list: thm list > thm 

138 
val conj_elim: thm > thm * thm 

139 
val conj_elim_list: thm > thm list 

18498
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

140 
val conj_elim_precise: int list > thm > thm list list 
12135  141 
val conj_intr_thm: thm 
18206  142 
val conj_curry: thm > thm 
13325  143 
val abs_def: thm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

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

5903  148 
structure Drule: DRULE = 
0  149 
struct 
150 

3991  151 

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

153 

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

154 
fun dest_implies ct = 
16682  155 
(case Thm.term_of ct of 
156 
(Const ("==>", _) $ _ $ _) => 

157 
let val (ct1, ct2) = Thm.dest_comb ct 

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

159 
 _ => raise TERM ("dest_implies", [term_of ct])); 

1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

160 

10414  161 
fun dest_equals ct = 
16682  162 
(case Thm.term_of ct of 
163 
(Const ("==", _) $ _ $ _) => 

164 
let val (ct1, ct2) = Thm.dest_comb ct 

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

166 
 _ => raise TERM ("dest_equals", [term_of ct])); 

10414  167 

1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

168 

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

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

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

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

172 
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

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

174 

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

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

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

178 
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

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

180 

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

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

182 
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

183 

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

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

186 
in Thm.cterm_of thy (f t) end; 
15797  187 

188 
fun ctyp_fun f cT = 

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

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

190 
in Thm.ctyp_of thy (f T) end; 
15797  191 

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

192 
val implies = cterm_of ProtoPure.thy Term.implies; 
9547  193 

194 
(*cterm version of mk_implies*) 

10767
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10667
diff
changeset

195 
fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B; 
9547  196 

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

198 
fun list_implies([], B) = B 

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

200 

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

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

204 

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

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

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

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

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

210 
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

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

212 

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

215 
Type ("fun", _) => 

216 
let 

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

218 
val (cTs, cT') = strip_type cT2 

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

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

221 

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

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

15875  227 
fun plain_prop_of raw_thm = 
228 
let 

229 
val thm = Thm.strip_shyps raw_thm; 

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

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

232 
in 

233 
if not (null hyps) then 

234 
err "theorem may not contain hypotheses" 

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

236 
err "theorem may not contain sort hypotheses" 

237 
else if not (null tpairs) then 

238 
err "theorem may not contain flexflex pairs" 

239 
else prop 

240 
end; 

241 

242 

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

243 

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

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

245 

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

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

247 
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

248 

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

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

250 
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

251 

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

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

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

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

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

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

261 
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

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

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

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

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

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

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

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

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

271 
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

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

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

274 
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

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

276 
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

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

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

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

280 

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

281 

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

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

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

286 
***) 

287 

288 
fun types_sorts thm = 

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

18179  291 
val big = Term.list_comb 
15949  292 
(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

293 
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

294 
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

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

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

0  299 
in (typ,sort) end; 
300 

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

303 
add_term_tvarnames (prop, used) 

304 
> fold (curry add_term_tvarnames) hyps 

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

306 
end; 

307 

7636  308 

9455  309 

0  310 
(** Standardization of rules **) 
311 

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

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

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

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

317 

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

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

321 

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

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

324 

7636  325 
(*Strip extraneous shyps as far as possible*) 
326 
fun strip_shyps_warning thm = 

327 
let 

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

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

331 
in 

332 
if null xshyps then () 

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

334 
thm' 

335 
end; 

336 

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

339 
 forall_intr_list (y::ys) th = 

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

340 
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

341 
in forall_intr y gth handle THM _ => gth end; 
0  342 

343 
(*Generalization over all suitable Free variables*) 

344 
fun forall_intr_frees th = 

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

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

350 

18535  351 
(*Generalization over Vars  canonical order*) 
352 
fun forall_intr_vars th = 

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

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

355 

7898  356 
val forall_elim_var = PureThy.forall_elim_var; 
357 
val forall_elim_vars = PureThy.forall_elim_vars; 

0  358 

18025  359 
fun outer_params t = 
360 
let 

361 
val vs = Term.strip_all_vars t; 

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

365 
(*generalize outermost parameters*) 

366 
fun gen_all th = 

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

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

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

371 
in fold elim (outer_params prop) th end; 

372 

373 
(*lift vars wrt. outermost goal parameters 

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

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

378 
val cert = Thm.cterm_of thy; 

379 
val {maxidx, ...} = Thm.rep_thm th; 

380 
val ps = outer_params (Thm.term_of goal) 

381 
> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T)); 

382 
val Ts = map Term.fastype_of ps; 

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

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

385 
in 

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

387 
> fold_rev (Thm.forall_intr o cert) ps 

388 
end; 

389 

9554  390 

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

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

392 
val forall_elim_list = fold forall_elim; 
0  393 

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

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

395 
val implies_intr_list = fold_rev implies_intr; 
0  396 

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

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

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

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

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

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

404 
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

405 
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

406 
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

407 
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

408 
in Thm.adjust_maxidx_thm (Thm.instantiate (cinstT, cinst) th) end; 
0  409 

410 

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

10515  413 

16595  414 
(*Discharge all hypotheses.*) 
415 
fun implies_intr_hyps th = 

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

417 

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

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

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

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

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

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

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

426 

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

429 
else thm; 

430 

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

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

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

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

434 
#> `(#maxidx o Thm.rep_thm) 
ea65d75e0ce1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
wenzelm
parents:
16861
diff
changeset

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

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

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

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

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

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

441 

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

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

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

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

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

446 

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

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

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

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

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

451 
#> close_derivation; 
12005  452 

0  453 

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

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

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

457 

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

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

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

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

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

462 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

478 

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

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

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

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

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

483 
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

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

485 
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

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

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

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

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

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

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

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

498 
th' > forall_intr_list (map #2 insts) 

499 
> forall_elim_list (map #1 insts) 

500 
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

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

502 

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

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

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

505 

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

508 
Any remaining trailing positions are left unchanged. *) 

509 
val rearrange_prems = let 

510 
fun rearr new [] thm = thm 

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

514 
in rearr 0 end; 

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

515 

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

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

519 
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

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

522 
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

523 
in forall_elim_vars 0 (Thm.assume (cterm_of thy prop)) end; 
0  524 

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

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

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

531 

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

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

534 

535 
(*For joining lists of rules*) 

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

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

539 
in List.concat (map resb thbs) end; 
0  540 

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

542 

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

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

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

545 
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

546 
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

547 
 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

548 
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

549 

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

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

551 
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

552 
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

553 
 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

554 
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

555 

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

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

557 
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

558 

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

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

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

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

6946  565 
fun compose_single (tha,i,thb) = 
566 
(case compose (tha,i,thb) of 

567 
[th] => th 

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

569 

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

572 
case compose(tha,1,thb) of 

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

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

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

576 

4016  577 
(** theorem equality **) 
0  578 

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

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

580 
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

581 

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

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

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

16720  586 
val size_of_thm = size_of_term o Thm.full_prop_of; 
0  587 

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

591 
val merge_rules = Library.merge eq_thm_prop; 

9829  592 

18535  593 
(*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

594 
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

595 

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

596 

0  597 
(*** MetaRewriting Rules ***) 
598 

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

599 
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

600 

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

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

4016  605 

0  606 
val reflexive_thm = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

607 
let val cx = cterm_of ProtoPure.thy (Var(("x",0),TVar(("'a",0),[]))) 
12135  608 
in store_standard_thm_open "reflexive" (Thm.reflexive cx) end; 
0  609 

610 
val symmetric_thm = 

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

614 
val transitive_thm = 

14854  615 
let val xy = read_prop "x == y" 
616 
val yz = read_prop "y == z" 

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

4679  620 
fun symmetric_fun thm = thm RS symmetric_thm; 
621 

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

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

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

624 
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

625 
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

626 

18820  627 
val equals_cong = 
628 
store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x == y")); 

629 

10414  630 
val imp_cong = 
631 
let 

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

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

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

635 
val A = read_prop "PROP A" 

636 
in 

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

640 
(implies_elim (assume AB) (assume A))))) 

641 
(implies_intr AC (implies_intr A 

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

643 
(implies_elim (assume AC) (assume A))))))) 

644 
end; 

645 

646 
val swap_prems_eq = 

647 
let 

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

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

650 
val A = read_prop "PROP A" 

651 
val B = read_prop "PROP B" 

652 
in 

12135  653 
store_standard_thm_open "swap_prems_eq" (equal_intr 
10414  654 
(implies_intr ABC (implies_intr B (implies_intr A 
655 
(implies_elim (implies_elim (assume ABC) (assume A)) (assume B))))) 

656 
(implies_intr BAC (implies_intr A (implies_intr B 

657 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

658 
end; 

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

659 

18468  660 
val imp_cong_rule = combination o combination (reflexive implies); 
0  661 

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

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

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

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

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

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

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

668 
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

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

670 

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

673 

18337  674 
val abs_def = 
675 
let 

676 
fun contract_lhs th = 

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

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

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

18337  681 
in 
682 
contract_lhs 

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

684 
#> fold_rev abstract 

685 
#> contract_lhs 

686 
end; 

687 

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

18468  691 
(case try Thm.dest_comb ct of 
692 
NONE => cv ct 

693 
 SOME (A, B) => 

694 
(case (term_of A, term_of B) of 

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

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

697 
Thm.combination (Thm.reflexive A) 

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

699 
end 

700 
 _ => cv ct)); 

701 

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

703 
fun concl_conv 0 cv ct = cv ct 

704 
 concl_conv n cv ct = 

705 
(case try dest_implies ct of 

706 
NONE => cv ct 

707 
 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

708 

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

711 
 prems_conv n cv = 

712 
let 

713 
fun conv i ct = 

714 
if i = n + 1 then reflexive ct 

715 
else 

716 
(case try dest_implies ct of 

717 
NONE => reflexive ct 

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

719 
in conv 1 end; 

720 

721 
(*rewrite the A's in A1 && ... && An*) 

722 
fun conjunction_conv 0 _ = reflexive 

723 
 conjunction_conv n cv = 

724 
let 

725 
fun conv i ct = 

726 
if i <> n andalso can Logic.dest_conjunction (term_of ct) then 

727 
forall_conv 1 

728 
(prems_conv 1 (K (prems_conv 2 (fn 1 => cv i  2 => conv (i + 1))))) ct 

729 
else cv i ct; 

730 
in conv 1 end; 

731 

732 

733 
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

734 
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

735 

18468  736 

15669  737 
(*** Some useful metatheorems ***) 
0  738 

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

12135  740 
val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi")); 
7380  741 
val _ = store_thm "_" asm_rl; 
0  742 

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

4016  744 
val cut_rl = 
12135  745 
store_standard_thm_open "cut_rl" 
9455  746 
(Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta")); 
0  747 

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

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

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

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

752 
and VW = read_prop "PROP V ==> PROP W"; 
4016  753 
in 
12135  754 
store_standard_thm_open "revcut_rl" 
4016  755 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  756 
end; 
757 

668  758 
(*for deleting an unwanted assumption*) 
759 
val thin_rl = 

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

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

761 
and W = read_prop "PROP W"; 
12135  762 
in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end; 
668  763 

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

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

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

767 
and QV = read_prop "!!x::'a. PROP V" 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

768 
and x = read_cterm ProtoPure.thy ("x", TypeInfer.logicT); 
4016  769 
in 
12135  770 
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

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

772 
(implies_intr V (forall_intr x (assume V)))) 
0  773 
end; 
774 

1756  775 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
776 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

778 
*) 

779 
val swap_prems_rl = 

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

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

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

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

789 
end; 

790 

3653  791 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
792 
==> PROP ?phi == PROP ?psi 

8328  793 
Introduction rule for == as a metatheorem. 
3653  794 
*) 
795 
val equal_intr_rule = 

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

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

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

13368  803 
(* [ PROP ?phi == PROP ?psi; PROP ?phi ] ==> PROP ?psi *) 
804 
val equal_elim_rule1 = 

805 
let val eq = read_prop "PROP phi == PROP psi" 

806 
and P = read_prop "PROP phi" 

807 
in store_standard_thm_open "equal_elim_rule1" 

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

809 
end; 

4285  810 

12297  811 
(* "[ PROP ?phi; PROP ?phi; PROP ?psi ] ==> PROP ?psi" *) 
812 

813 
val remdups_rl = 

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

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

816 

817 

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

821 
val norm_hhf_eq = 

822 
let 

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

823 
val cert = Thm.cterm_of ProtoPure.thy; 
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 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

919 
val cterm = cterm_of (Theory.merge (thy,thya)) 
10414  920 
in transitive (symmetric (beta_conversion false (cterm (abst$a)))) 
921 
(transitive combth (beta_conversion false (cterm (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 

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

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

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

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

947 
(implies_intr_list asms th) 

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

949 
> implies_intr_list asms' 

950 
end; 

11815  951 

4789  952 

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

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

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

956 
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

957 

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

958 

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

961 
fun instantiate' cTs cts thm = 

962 
let 

963 
fun err msg = 

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

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

4285  967 

968 
fun inst_of (v, ct) = 

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

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

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

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

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

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

981 
(*instantiate types first!*) 

982 
val thm' = 

983 
if forall is_none cTs then thm 

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

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

988 
end; 

989 

990 

14081  991 

992 
(** renaming of bound variables **) 

993 

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

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

996 

997 
fun rename_bvars [] thm = thm 

998 
 rename_bvars vs thm = 

999 
let 

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

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

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

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

1006 

1007 
(* renaming in lefttoright order *) 

1008 

1009 
fun rename_bvars' xs thm = 

1010 
let 

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

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

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

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

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

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

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

1021 
 rename xs t = (xs, t); 

1022 
in case rename xs prop of 

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

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

1026 

1027 

1028 

5688  1029 
(* unvarify(T) *) 
1030 

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

1032 

1033 
fun unvarifyT thm = 

1034 
let 

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

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

1039 
fun unvarify raw_thm = 

1040 
let 

1041 
val thm = unvarifyT raw_thm; 

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

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

1046 

8605  1047 
(* tvars_intr_list *) 
1048 

1049 
fun tvars_intr_list tfrees thm = 

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

1053 

6435  1054 
(* increment var indexes *) 
1055 

18025  1056 
fun incr_indexes th = Thm.incr_indexes (#maxidx (Thm.rep_thm th) + 1); 
1057 

6435  1058 
fun incr_indexes_wrt is cTs cts thms = 
1059 
let 

1060 
val maxidx = 

15570  1061 
Library.foldl Int.max (~1, is @ 
6435  1062 
map (maxidx_of_typ o #T o Thm.rep_ctyp) cTs @ 
1063 
map (#maxidx o Thm.rep_cterm) cts @ 

1064 
map (#maxidx o Thm.rep_thm) thms); 

10414  1065 
in Thm.incr_indexes (maxidx + 1) end; 
6435  1066 

1067 

8328  1068 
(* freeze_all *) 
1069 

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

1071 

1072 
fun freeze_all_TVars thm = 

1073 
(case tvars_of thm of 

1074 
[] => thm 

1075 
 tvars => 

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

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

1079 
fun freeze_all_Vars thm = 

1080 
(case vars_of thm of 

1081 
[] => thm 

1082 
 vars => 

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

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

1086 
val freeze_all = freeze_all_Vars o freeze_all_TVars; 

1087 

1088 

11975  1089 

18225  1090 
(** multi_resolve **) 
1091 

1092 
local 

1093 

1094 
fun res th i rule = 

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

1096 

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

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

1099 

1100 
in 

1101 

1102 
val multi_resolve = multi_res 1; 

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

1104 

1105 
end; 

1106 

1107 

1108 

11975  1109 
(** metalevel conjunction **) 
1110 

1111 
local 

1112 
val A = read_prop "PROP A"; 

1113 
val B = read_prop "PROP B"; 

1114 
val C = read_prop "PROP C"; 

1115 
val ABC = read_prop "PROP A ==> PROP B ==> PROP C"; 

1116 

1117 
val proj1 = 

1118 
forall_intr_list [A, B] (implies_intr_list [A, B] (Thm.assume A)) 

1119 
> forall_elim_vars 0; 

1120 

1121 
val proj2 = 

1122 
forall_intr_list [A, B] (implies_intr_list [A, B] (Thm.assume B)) 

1123 
> forall_elim_vars 0; 

1124 

1125 
val conj_intr_rule = 

1126 
forall_intr_list [A, B] (implies_intr_list [A, B] 

1127 
(Thm.forall_intr C (Thm.implies_intr ABC 

1128 
(implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))) 

1129 
> forall_elim_vars 0; 

1130 
in 

1131 

18025  1132 
fun conj_intr tha thb = thb COMP (tha COMP incr_indexes_wrt [] [] [] [tha, thb] conj_intr_rule); 
12756
08bf3d911968
conj_intr_list and conj_elim_precise: cover 0 conjuncts;
wenzelm
parents:
12725
diff
changeset

1133 

08bf3d911968
conj_intr_list and conj_elim_precise: cover 0 conjuncts;
wenzelm
parents:
12725
diff
changeset

1134 
fun conj_intr_list [] = asm_rl 
08bf3d911968
conj_intr_list and conj_elim_precise: cover 0 conjuncts;
wenzelm
parents:
12725
diff
changeset

1135 
 conj_intr_list ths = foldr1 (uncurry conj_intr) ths; 
11975  1136 

1137 
fun conj_elim th = 

1138 
let val th' = forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th 

18025  1139 
in (incr_indexes th' proj1 COMP th', incr_indexes th' proj2 COMP th') end; 
11975  1140 

18498
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1141 
(*((A && B) && C) && D && E  flat*) 
11975  1142 
fun conj_elim_list th = 
1143 
let val (th1, th2) = conj_elim th 

1144 
in conj_elim_list th1 @ conj_elim_list th2 end handle THM _ => [th]; 

1145 

18498
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1146 
(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3  improper*) 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1147 
fun conj_elim_precise spans = 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1148 
let 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1149 
fun elim 0 _ = [] 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1150 
 elim 1 th = [th] 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1151 
 elim n th = 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1152 
let val (th1, th2) = conj_elim th 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1153 
in th1 :: elim (n  1) th2 end; 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1154 
fun elims (0 :: ns) ths = [] :: elims ns ths 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1155 
 elims (n :: ns) (th :: ths) = elim n th :: elims ns ths 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1156 
 elims _ _ = []; 
466351242c6f
conj_elim_precise: proper treatment of nested conjunctions;
wenzelm
parents:
18468
diff
changeset

1157 
in elims spans o elim (length (filter_out (equal 0) spans)) end; 
12135  1158 

1159 
val conj_intr_thm = store_standard_thm_open "conjunctionI" 

1160 
(implies_intr_list [A, B] (conj_intr (Thm.assume A) (Thm.assume B))); 

1161 

18206  1162 
end; 
18179  1163 

18206  1164 
fun conj_curry th = 
1165 
let 

1166 
val {thy, maxidx, ...} = Thm.rep_thm th; 

1167 
val n = Thm.nprems_of th; 

1168 
in 

1169 
if n < 2 then th 

1170 
else 

1171 
let 

1172 
val cert = Thm.cterm_of thy; 

1173 
val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto n); 

1174 
val B = Free ("B", propT); 

1175 
val C = cert (Logic.mk_conjunction_list As); 

1176 
val D = cert (Logic.list_implies (As, B)); 

1177 
val rule = 

1178 
implies_elim_list (Thm.assume D) (conj_elim_list (Thm.assume C)) 

1179 
> implies_intr_list [D, C] 

1180 
> forall_intr_frees 

1181 
> forall_elim_vars (maxidx + 1) 

1182 
in Thm.adjust_maxidx_thm (th COMP rule) end 

1183 
end; 

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

1184 

11975  1185 
end; 
5903  1186 

1187 
structure BasicDrule: BASIC_DRULE = Drule; 

1188 
open BasicDrule; 