author  wenzelm 
Wed, 15 Feb 2006 21:35:02 +0100  
changeset 19051  5212516f1a98 
parent 18929  d81435108688 
child 19124  d9ac560a7bc8 
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 

82 
val inst: string > string > thm > thm 

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

84 
val incr_indexes: thm > thm > thm 

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

5903  86 
end; 
87 

88 
signature DRULE = 

89 
sig 

90 
include BASIC_DRULE 

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 
11975  100 
val compose_single: thm * int * thm > thm 
12373  101 
val add_rule: thm > thm list > thm list 
102 
val del_rule: thm > thm list > thm list 

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

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

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

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

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

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

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

118 
val protectD: thm 

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

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

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

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

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

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

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

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

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

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

139 
val conj_elim: thm > thm * thm 

140 
val conj_elim_list: thm > thm list 

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

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

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

5903  149 
structure Drule: DRULE = 
0  150 
struct 
151 

3991  152 

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

154 

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

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

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

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

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 
164 
(Const ("==", _) $ _ $ _) => 

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

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

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

10414  168 

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

169 

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

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

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

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

173 
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

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

175 

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

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

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

179 
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

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

181 

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

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

183 
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

184 

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

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

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

189 
fun ctyp_fun f cT = 

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

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

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

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

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

195 
(*cterm version of mk_implies*) 

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

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

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

199 
fun list_implies([], B) = B 

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

201 

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

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

205 

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

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

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

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

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

211 
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

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

213 

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

216 
Type ("fun", _) => 

217 
let 

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

219 
val (cTs, cT') = strip_type cT2 

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

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

222 

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

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

15875  228 
fun plain_prop_of raw_thm = 
229 
let 

230 
val thm = Thm.strip_shyps raw_thm; 

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

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

233 
in 

234 
if not (null hyps) then 

235 
err "theorem may not contain hypotheses" 

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

237 
err "theorem may not contain sort hypotheses" 

238 
else if not (null tpairs) then 

239 
err "theorem may not contain flexflex pairs" 

240 
else prop 

241 
end; 

242 

243 

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

244 

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

245 
(** reading of instantiations **) 
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 absent ixn = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

248 
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

249 

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

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

251 
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

252 

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

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

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

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

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

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

262 
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

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

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

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

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

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

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

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

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

272 
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

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

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

275 
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

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

277 
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

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

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

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

281 

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

282 

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

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

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

287 
***) 

288 

289 
fun types_sorts thm = 

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

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

294 
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

295 
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

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

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

0  300 
in (typ,sort) end; 
301 

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

304 
add_term_tvarnames (prop, used) 

305 
> fold (curry add_term_tvarnames) hyps 

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

307 
end; 

308 

7636  309 

9455  310 

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

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

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

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

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

318 

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

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

322 

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

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

325 

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

328 
let 

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

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

332 
in 

333 
if null xshyps then () 

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

335 
thm' 

336 
end; 

337 

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

340 
 forall_intr_list (y::ys) th = 

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

341 
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

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

344 
(*Generalization over all suitable Free variables*) 

345 
fun forall_intr_frees th = 

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

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

351 

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

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

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

356 

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

0  359 

18025  360 
fun outer_params t = 
361 
let 

362 
val vs = Term.strip_all_vars t; 

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

366 
(*generalize outermost parameters*) 

367 
fun gen_all th = 

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

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

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

372 
in fold elim (outer_params prop) th end; 

373 

374 
(*lift vars wrt. outermost goal parameters 

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

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

379 
val cert = Thm.cterm_of thy; 

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

381 
val ps = outer_params (Thm.term_of goal) 

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

383 
val Ts = map Term.fastype_of ps; 

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

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

386 
in 

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

388 
> fold_rev (Thm.forall_intr o cert) ps 

389 
end; 

390 

9554  391 

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

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

393 
val forall_elim_list = fold forall_elim; 
0  394 

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

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

396 
val implies_intr_list = fold_rev implies_intr; 
0  397 

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

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

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

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

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

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

405 
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

406 
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

407 
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

408 
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

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

411 

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

10515  414 

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

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

418 

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

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

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

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

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

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

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

427 

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

430 
else thm; 

431 

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

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

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

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

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

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

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

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

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

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

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

442 

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

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

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

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

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

447 

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

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

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

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

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

452 
#> close_derivation; 
12005  453 

0  454 

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

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

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

458 

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

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

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

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

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

463 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

479 

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

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

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

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

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

484 
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

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

486 
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

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

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

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

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

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

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

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

499 
th' > forall_intr_list (map #2 insts) 

500 
> forall_elim_list (map #1 insts) 

501 
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

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

503 

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

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

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

506 

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

509 
Any remaining trailing positions are left unchanged. *) 

510 
val rearrange_prems = let 

511 
fun rearr new [] thm = thm 

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

515 
in rearr 0 end; 

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

516 

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

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

520 
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

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

523 
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

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

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

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

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

532 

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

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

535 

536 
(*For joining lists of rules*) 

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

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

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

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

543 

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

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

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

546 
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

547 
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

548 
 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

549 
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

550 

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

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

552 
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

553 
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

554 
 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

555 
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

556 

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

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

558 
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

559 

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

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

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

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

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

568 
[th] => th 

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

570 

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

573 
case compose(tha,1,thb) of 

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

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

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

577 

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

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

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

581 
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

582 

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

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

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

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

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

592 
val merge_rules = Library.merge eq_thm_prop; 

9829  593 

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

595 
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

596 

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

597 

0  598 
(*** MetaRewriting Rules ***) 
599 

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

600 
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

601 

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

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

4016  606 

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

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

611 
val symmetric_thm = 

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

615 
val transitive_thm = 

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

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

4679  621 
fun symmetric_fun thm = thm RS symmetric_thm; 
622 

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

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

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

625 
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

626 
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

627 

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

630 

10414  631 
val imp_cong = 
632 
let 

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

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

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

636 
val A = read_prop "PROP A" 

637 
in 

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

641 
(implies_elim (assume AB) (assume A))))) 

642 
(implies_intr AC (implies_intr A 

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

644 
(implies_elim (assume AC) (assume A))))))) 

645 
end; 

646 

647 
val swap_prems_eq = 

648 
let 

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

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

651 
val A = read_prop "PROP A" 

652 
val B = read_prop "PROP B" 

653 
in 

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

657 
(implies_intr BAC (implies_intr A (implies_intr B 

658 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

659 
end; 

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

660 

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

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

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

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

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

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

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

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

669 
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

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

671 

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

674 

18337  675 
val abs_def = 
676 
let 

677 
fun contract_lhs th = 

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

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

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

18337  682 
in 
683 
contract_lhs 

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

685 
#> fold_rev abstract 

686 
#> contract_lhs 

687 
end; 

688 

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

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

694 
 SOME (A, B) => 

695 
(case (term_of A, term_of B) of 

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

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

698 
Thm.combination (Thm.reflexive A) 

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

700 
end 

701 
 _ => cv ct)); 

702 

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

704 
fun concl_conv 0 cv ct = cv ct 

705 
 concl_conv n cv ct = 

706 
(case try dest_implies ct of 

707 
NONE => cv ct 

708 
 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

709 

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

712 
 prems_conv n cv = 

713 
let 

714 
fun conv i ct = 

715 
if i = n + 1 then reflexive ct 

716 
else 

717 
(case try dest_implies ct of 

718 
NONE => reflexive ct 

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

720 
in conv 1 end; 

721 

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

723 
fun conjunction_conv 0 _ = reflexive 

724 
 conjunction_conv n cv = 

725 
let 

726 
fun conv i ct = 

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

728 
forall_conv 1 

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

730 
else cv i ct; 

731 
in conv 1 end; 

732 

733 

734 
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

735 
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

736 

18468  737 

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

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

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

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

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

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

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

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 VW = read_prop "PROP V ==> PROP W"; 
4016  754 
in 
12135  755 
store_standard_thm_open "revcut_rl" 
4016  756 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  757 
end; 
758 

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

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

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

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

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

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

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

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

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

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

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

19051  776 
(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==> 
777 
(PROP ?Phi ==> PROP ?Psi) 

778 
*) 

779 
val distinct_prems_rl = 

780 
let 

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

782 
val A = read_prop "PROP Phi"; 

783 
in 

784 
store_standard_thm_open "distinct_prems_rl" 

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

786 
end; 

787 

1756  788 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
789 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

791 
*) 

792 
val swap_prems_rl = 

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

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

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

797 
val cminor2 = read_prop "PROP PhiB"; 
1756  798 
val minor2 = assume cminor2; 
12135  799 
in store_standard_thm_open "swap_prems_rl" 
1756  800 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
801 
(implies_elim (implies_elim major minor1) minor2)))) 

802 
end; 

803 

3653  804 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
805 
==> PROP ?phi == PROP ?psi 

8328  806 
Introduction rule for == as a metatheorem. 
3653  807 
*) 
808 
val equal_intr_rule = 

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

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

810 
and QP = read_prop "PROP psi ==> PROP phi" 
4016  811 
in 
12135  812 
store_standard_thm_open "equal_intr_rule" 
4016  813 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  814 
end; 
815 

13368  816 
(* [ PROP ?phi == PROP ?psi; PROP ?phi ] ==> PROP ?psi *) 
817 
val equal_elim_rule1 = 

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

819 
and P = read_prop "PROP phi" 

820 
in store_standard_thm_open "equal_elim_rule1" 

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

822 
end; 

4285  823 

12297  824 
(* "[ PROP ?phi; PROP ?phi; PROP ?psi ] ==> PROP ?psi" *) 
825 

826 
val remdups_rl = 

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

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

829 

830 

9554  831 
(*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) 
12297  832 
Rewrite rule for HHF normalization.*) 
9554  833 

834 
val norm_hhf_eq = 

835 
let 

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

836 
val cert = Thm.cterm_of ProtoPure.thy; 
14854  837 
val aT = TFree ("'a", []); 
9554  838 
val all = Term.all aT; 
839 
val x = Free ("x", aT); 

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

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

842 

843 
val cx = cert x; 

844 
val cphi = cert phi; 

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

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

847 
in 

848 
Thm.equal_intr 

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

850 
> Thm.forall_elim cx 

851 
> Thm.implies_intr cphi 

852 
> Thm.forall_intr cx 

853 
> Thm.implies_intr lhs) 

854 
(Thm.implies_elim 

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

856 
> Thm.forall_intr cx 

857 
> Thm.implies_intr cphi 

858 
> Thm.implies_intr rhs) 

12135  859 
> store_standard_thm_open "norm_hhf_eq" 
9554  860 
end; 
861 

18179  862 
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); 
863 

12800  864 
fun is_norm_hhf tm = 
865 
let 

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

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

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

869 
 is_norm _ = true; 

18929  870 
in is_norm (Envir.beta_eta_contract tm) end; 
12800  871 

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

872 
fun norm_hhf thy t = 
12800  873 
if is_norm_hhf t then t 
18179  874 
else Pattern.rewrite_term thy [norm_hhf_prop] [] t; 
875 

12800  876 

9554  877 

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

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

879 

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

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

881 
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

882 

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

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

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

886 
in instantiate (read_insts thy ts ts used sinsts) th end; 
15797  887 

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

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

889 
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

890 

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

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

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

893 
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

894 

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

896 
read_instantiate_sg' (Thm.theory_of_thm th) sinsts th; 
15797  897 

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

898 

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

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

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

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

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

903 
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

904 
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

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

906 
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

907 
val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) 
10403  908 
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

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

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

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

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

914 
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

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

916 
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

917 
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

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

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

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

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

922 

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

923 

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

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

925 

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

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

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

928 
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

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

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

931 
val (abst,absu) = Logic.dest_equals prop 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15949
diff
changeset

932 
val cterm = cterm_of (Theory.merge (thy,thya)) 
10414  933 
in transitive (symmetric (beta_conversion false (cterm (abst$a)))) 
934 
(transitive combth (beta_conversion false (cterm (absu$a)))) 

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

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

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

937 

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

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

939 
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

940 

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

941 

18025  942 
(** protected propositions **) 
4789  943 

944 
local 

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

945 
val cert = Thm.cterm_of ProtoPure.thy; 
18025  946 
val A = cert (Free ("A", propT)); 
947 
val prop_def = #1 (freeze_thaw ProtoPure.prop_def); 

4789  948 
in 
18025  949 
val protect = Thm.capply (cert Logic.protectC); 
18799  950 
val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard 
18025  951 
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)))); 
18799  952 
val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard 
18025  953 
(Thm.equal_elim prop_def (Thm.assume (protect A))))); 
18179  954 
val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A)); 
4789  955 
end; 
956 

18025  957 
fun implies_intr_protected asms th = 
18118  958 
let val asms' = map protect asms in 
959 
implies_elim_list 

960 
(implies_intr_list asms th) 

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

962 
> implies_intr_list asms' 

963 
end; 

11815  964 

4789  965 

5688  966 
(** variations on instantiate **) 
4285  967 

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

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

969 
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

970 

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

971 

4285  972 
(* instantiate by lefttoright occurrence of variables *) 
973 

974 
fun instantiate' cTs cts thm = 

975 
let 

976 
fun err msg = 

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

15570  978 
List.mapPartial (Option.map Thm.typ_of) cTs, 
979 
List.mapPartial (Option.map Thm.term_of) cts); 

4285  980 

981 
fun inst_of (v, ct) = 

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

982 
(Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct) 
4285  983 
handle TYPE (msg, _, _) => err msg; 
984 

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

986 
(Thm.ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT) 
15797  987 
handle TYPE (msg, _, _) => err msg; 
988 

4285  989 
fun zip_vars _ [] = [] 
15531  990 
 zip_vars (_ :: vs) (NONE :: opt_ts) = zip_vars vs opt_ts 
991 
 zip_vars (v :: vs) (SOME t :: opt_ts) = (v, t) :: zip_vars vs opt_ts 

4285  992 
 zip_vars [] _ = err "more instantiations than variables in thm"; 
993 

994 
(*instantiate types first!*) 

995 
val thm' = 

996 
if forall is_none cTs then thm 

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

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

1001 
end; 

1002 

1003 

14081  1004 

1005 
(** renaming of bound variables **) 

1006 

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

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

1009 

1010 
fun rename_bvars [] thm = thm 

1011 
 rename_bvars vs thm = 

1012 
let 

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

1013 
val {thy, prop, ...} = rep_thm thm; 
17325  1014 
fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x > the_default x, T, ren t) 
14081  1015 
 ren (t $ u) = ren t $ ren u 
1016 
 ren t = t; 

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

1017 
in equal_elim (reflexive (cterm_of thy (ren prop))) thm end; 
14081  1018 

1019 

1020 
(* renaming in lefttoright order *) 

1021 

1022 
fun rename_bvars' xs thm = 

1023 
let 

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

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

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

18929  1028 
in (xs', Abs (the_default x x', T, t')) end 
14081  1029 
 rename xs (t $ u) = 
1030 
let 

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

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

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

1034 
 rename xs t = (xs, t); 

1035 
in case rename xs prop of 

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

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

1039 

1040 

1041 

5688  1042 
(* unvarify(T) *) 
1043 

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

1045 

1046 
fun unvarifyT thm = 

1047 
let 

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

1048 
val cT = Thm.ctyp_of (Thm.theory_of_thm thm); 
15531  1049 
val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (tvars_of thm); 
5688  1050 
in instantiate' tfrees [] thm end; 
1051 

1052 
fun unvarify raw_thm = 

1053 
let 

1054 
val thm = unvarifyT raw_thm; 

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

1055 
val ct = Thm.cterm_of (Thm.theory_of_thm thm); 
15531  1056 
val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (vars_of thm); 
5688  1057 
in instantiate' [] frees thm end; 
1058 

1059 

8605  1060 
(* tvars_intr_list *) 
1061 

1062 
fun tvars_intr_list tfrees thm = 

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

1066 

6435  1067 
(* increment var indexes *) 
1068 

18025  1069 
fun incr_indexes th = Thm.incr_indexes (#maxidx (Thm.rep_thm th) + 1); 
1070 

6435  1071 
fun incr_indexes_wrt is cTs cts thms = 
1072 
let 

1073 
val maxidx = 

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

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

10414  1078 
in Thm.incr_indexes (maxidx + 1) end; 
6435  1079 

1080 

8328  1081 
(* freeze_all *) 
1082 

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

1084 

1085 
fun freeze_all_TVars thm = 

1086 
(case tvars_of thm of 

1087 
[] => thm 

1088 
 tvars => 

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

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

1092 
fun freeze_all_Vars thm = 

1093 
(case vars_of thm of 

1094 
[] => thm 

1095 
 vars => 

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

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

1099 
val freeze_all = freeze_all_Vars o freeze_all_TVars; 

1100 

1101 

11975  1102 

18225  1103 
(** multi_resolve **) 
1104 

1105 
local 

1106 

1107 
fun res th i rule = 

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

1109 

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

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

1112 

1113 
in 

1114 

1115 
val multi_resolve = multi_res 1; 

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

1117 

1118 
end; 

1119 

1120 

1121 

11975  1122 
(** metalevel conjunction **) 
1123 

1124 
local 

1125 
val A = read_prop "PROP A"; 

1126 
val B = read_prop "PROP B"; 

1127 
val C = read_prop "PROP C"; 

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

1129 

1130 
val proj1 = 

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

1132 
> forall_elim_vars 0; 

1133 

1134 
val proj2 = 

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

1136 
> forall_elim_vars 0; 

1137 

1138 
val conj_intr_rule = 

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

1140 
(Thm.forall_intr C (Thm.implies_intr ABC 

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

1142 
> forall_elim_vars 0; 

1143 
in 

1144 

18025  1145 
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

1146 

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

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

1148 
 conj_intr_list ths = foldr1 (uncurry conj_intr) ths; 
11975  1149 

1150 
fun conj_elim th = 

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

18025  1152 
in (incr_indexes th' proj1 COMP th', incr_indexes th' proj2 COMP th') end; 
11975  1153 

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

1154 
(*((A && B) && C) && D && E  flat*) 
11975  1155 
fun conj_elim_list th = 
1156 
let val (th1, th2) = conj_elim th 

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

1158 

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

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

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

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

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

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

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

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

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

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

1168 
 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

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

1170 
in elims spans o elim (length (filter_out (equal 0) spans)) end; 
12135  1171 

1172 
val conj_intr_thm = store_standard_thm_open "conjunctionI" 

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

1174 

18206  1175 
end; 
18179  1176 

18206  1177 
fun conj_curry th = 
1178 
let 

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

1180 
val n = Thm.nprems_of th; 

1181 
in 

1182 
if n < 2 then th 

1183 
else 

1184 
let 

1185 
val cert = Thm.cterm_of thy; 

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

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

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

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

1190 
val rule = 

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

1192 
> implies_intr_list [D, C] 

1193 
> forall_intr_frees 

1194 
> forall_elim_vars (maxidx + 1) 

1195 
in Thm.adjust_maxidx_thm (th COMP rule) end 

1196 
end; 

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

1197 

11975  1198 
end; 
5903  1199 

1200 
structure BasicDrule: BASIC_DRULE = Drule; 

1201 
open BasicDrule; 