author  berghofe 
Wed, 14 Feb 2001 19:27:49 +0100  
changeset 11120  5254d35e4f7c 
parent 10815  dd5fb02ff872 
child 11163  14732e3eaa6e 
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 

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

9 
infix 0 RS RSN RL RLN MRS MRL OF COMP; 
0  10 

5903  11 
signature BASIC_DRULE = 
3766  12 
sig 
9547  13 
val mk_implies : cterm * cterm > cterm 
14 
val list_implies : cterm list * cterm > cterm 

4285  15 
val dest_implies : cterm > cterm * cterm 
10414  16 
val dest_equals : cterm > cterm * cterm 
8328  17 
val skip_flexpairs : cterm > cterm 
18 
val strip_imp_prems : cterm > cterm list 

10414  19 
val strip_imp_concl : cterm > cterm 
8328  20 
val cprems_of : thm > cterm list 
21 
val read_insts : 

4285  22 
Sign.sg > (indexname > typ option) * (indexname > sort option) 
23 
> (indexname > typ option) * (indexname > sort option) 

24 
> string list > (string*string)list 

25 
> (indexname*ctyp)list * (cterm*cterm)list 

26 
val types_sorts: thm > (indexname> typ option) * (indexname> sort option) 

7636  27 
val strip_shyps_warning : thm > thm 
8328  28 
val forall_intr_list : cterm list > thm > thm 
29 
val forall_intr_frees : thm > thm 

30 
val forall_intr_vars : thm > thm 

31 
val forall_elim_list : cterm list > thm > thm 

32 
val forall_elim_var : int > thm > thm 

33 
val forall_elim_vars : int > thm > thm 

9554  34 
val forall_elim_vars_safe : thm > thm 
8328  35 
val freeze_thaw : thm > thm * (thm > thm) 
36 
val implies_elim_list : thm > thm list > thm 

37 
val implies_intr_list : cterm list > thm > thm 

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

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

39 
(indexname * ctyp) list * (cterm * cterm) list > thm > thm 
8328  40 
val zero_var_indexes : thm > thm 
41 
val standard : thm > thm 

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

42 
val rotate_prems : int > thm > thm 
8328  43 
val assume_ax : theory > string > thm 
44 
val RSN : thm * (int * thm) > thm 

45 
val RS : thm * thm > thm 

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

47 
val RL : thm list * thm list > thm list 

48 
val MRS : thm list * thm > thm 

49 
val MRL : thm list list * thm list > thm list 

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

50 
val OF : thm * thm list > thm 
8328  51 
val compose : thm * int * thm > thm list 
52 
val COMP : thm * thm > thm 

0  53 
val read_instantiate_sg: Sign.sg > (string*string)list > thm > thm 
8328  54 
val read_instantiate : (string*string)list > thm > thm 
55 
val cterm_instantiate : (cterm*cterm)list > thm > thm 

56 
val weak_eq_thm : thm * thm > bool 

57 
val eq_thm_sg : thm * thm > bool 

58 
val size_of_thm : thm > int 

59 
val reflexive_thm : thm 

60 
val symmetric_thm : thm 

61 
val transitive_thm : thm 

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

62 
val refl_implies : thm 
4679  63 
val symmetric_fun : thm > thm 
10414  64 
val imp_cong : thm 
65 
val swap_prems_eq : thm 

8328  66 
val equal_abs_elim : cterm > thm > thm 
4285  67 
val equal_abs_elim_list: cterm list > thm > thm 
68 
val flexpair_abs_elim_list: cterm list > thm > thm 

8328  69 
val asm_rl : thm 
70 
val cut_rl : thm 

71 
val revcut_rl : thm 

72 
val thin_rl : thm 

4285  73 
val triv_forall_equality: thm 
1756  74 
val swap_prems_rl : thm 
4285  75 
val equal_intr_rule : thm 
8550
b44c185f8018
new metarule "inst", a shorthand for read_instantiate_sg
paulson
parents:
8496
diff
changeset

76 
val inst : string > string > thm > thm 
8328  77 
val instantiate' : ctyp option list > cterm option list > thm > thm 
78 
val incr_indexes_wrt : int list > ctyp list > cterm list > thm list > thm > thm 

5903  79 
end; 
80 

81 
signature DRULE = 

82 
sig 

83 
include BASIC_DRULE 

9455  84 
val rule_attribute : ('a > thm > thm) > 'a attribute 
85 
val tag_rule : tag > thm > thm 

86 
val untag_rule : string > thm > thm 

87 
val tag : tag > 'a attribute 

88 
val untag : string > 'a attribute 

89 
val tag_lemma : 'a attribute 

90 
val tag_assumption : 'a attribute 

91 
val tag_internal : 'a attribute 

92 
val has_internal : tag list > bool 

10515  93 
val close_derivation : thm > thm 
8328  94 
val compose_single : thm * int * thm > thm 
9829  95 
val add_rules : thm list > thm list > thm list 
96 
val del_rules : thm list > thm list > thm list 

9418  97 
val merge_rules : thm list * thm list > thm list 
9554  98 
val norm_hhf_eq : thm 
8328  99 
val triv_goal : thm 
100 
val rev_triv_goal : thm 

101 
val freeze_all : thm > thm 

5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5079
diff
changeset

102 
val mk_triv_goal : cterm > thm 
8328  103 
val mk_cgoal : cterm > cterm 
104 
val assume_goal : cterm > thm 

105 
val tvars_of_terms : term list > (indexname * sort) list 

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

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

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

109 
val unvarifyT : thm > thm 

110 
val unvarify : thm > thm 

8605  111 
val tvars_intr_list : string list > thm > thm 
3766  112 
end; 
0  113 

5903  114 
structure Drule: DRULE = 
0  115 
struct 
116 

3991  117 

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

118 
(** some cterm>cterm operations: much faster than calling cterm_of! **) 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

119 

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

120 
(** SAME NAMES as in structure Logic: use compound identifiers! **) 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

121 

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

122 
(*dest_implies for cterms. Note T=prop below*) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

123 
fun dest_implies ct = 
8328  124 
case term_of ct of 
125 
(Const("==>", _) $ _ $ _) => 

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

126 
let val (ct1,ct2) = Thm.dest_comb ct 
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10667
diff
changeset

127 
in (#2 (Thm.dest_comb ct1), ct2) end 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

128 
 _ => raise TERM ("dest_implies", [term_of ct]) ; 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

129 

10414  130 
fun dest_equals ct = 
131 
case term_of ct of 

132 
(Const("==", _) $ _ $ _) => 

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

133 
let val (ct1,ct2) = Thm.dest_comb ct 
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10667
diff
changeset

134 
in (#2 (Thm.dest_comb ct1), ct2) end 
10414  135 
 _ => raise TERM ("dest_equals", [term_of ct]) ; 
136 

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

137 

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

138 
(*Discard flexflex pairs; return a cterm*) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

139 
fun skip_flexpairs ct = 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

140 
case term_of ct of 
8328  141 
(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) => 
142 
skip_flexpairs (#2 (dest_implies ct)) 

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

143 
 _ => ct; 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

144 

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

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

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

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

148 
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

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

150 

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

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

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

154 
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

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

156 

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

157 
(*The premises of a theorem, as a cterm list*) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

158 
val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of; 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

159 

9547  160 
val proto_sign = Theory.sign_of ProtoPure.thy; 
161 

162 
val implies = cterm_of proto_sign Term.implies; 

163 

164 
(*cterm version of mk_implies*) 

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

165 
fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B; 
9547  166 

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

168 
fun list_implies([], B) = B 

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

170 

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

171 

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

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

173 

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

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

175 
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

176 

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

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

178 
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

179 

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

180 
fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = 
10403  181 
let 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

182 
fun split([],tvs,vs) = (tvs,vs) 
4691  183 
 split((sv,st)::l,tvs,vs) = (case Symbol.explode sv of 
184 
"'"::cs => split(l,(Syntax.indexname cs,st)::tvs,vs) 

185 
 cs => split(l,tvs,(Syntax.indexname cs,st)::vs)); 

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

186 
val (tvs,vs) = split(insts,[],[]); 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

187 
fun readT((a,i),st) = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

188 
let val ixn = ("'" ^ a,i); 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

189 
val S = case rsorts ixn of Some S => S  None => absent ixn; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

190 
val T = Sign.read_typ (sign,sorts) st; 
10403  191 
in if Sign.typ_instance sign (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

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

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

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

195 
fun mkty(ixn,st) = (case rtypes ixn of 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

196 
Some T => (ixn,(st,typ_subst_TVars tye T)) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

197 
 None => absent ixn); 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

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

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

200 
and sTs = map snd ixnsTs 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

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

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

203 
let val U = typ_subst_TVars tye2 T 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

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

205 
val ixnTs = ListPair.zip(ixns, map snd sTs) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

206 
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) (tye2 @ tye), 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

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

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

209 

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

210 

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

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

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

215 
***) 

216 

217 
fun types_sorts thm = 

218 
let val {prop,hyps,...} = rep_thm thm; 

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

219 
val big = list_comb(prop,hyps); (* bogus term! *) 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

220 
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

221 
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

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

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

224 
fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i)); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

225 
fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); 
0  226 
in (typ,sort) end; 
227 

7636  228 

9455  229 

230 
(** basic attributes **) 

231 

232 
(* dependent rules *) 

233 

234 
fun rule_attribute f (x, thm) = (x, (f x thm)); 

235 

236 

237 
(* add / delete tags *) 

238 

239 
fun map_tags f thm = 

240 
Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm; 

241 

242 
fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]); 

243 
fun untag_rule s = map_tags (filter_out (equal s o #1)); 

244 

245 
fun tag tg x = rule_attribute (K (tag_rule tg)) x; 

246 
fun untag s x = rule_attribute (K (untag_rule s)) x; 

247 

248 
fun simple_tag name x = tag (name, []) x; 

249 

250 
fun tag_lemma x = simple_tag "lemma" x; 

251 
fun tag_assumption x = simple_tag "assumption" x; 

252 

253 
val internal_tag = ("internal", []); 

254 
fun tag_internal x = tag internal_tag x; 

255 
fun has_internal tags = exists (equal internal_tag) tags; 

256 

257 

258 

0  259 
(** Standardization of rules **) 
260 

7636  261 
(*Strip extraneous shyps as far as possible*) 
262 
fun strip_shyps_warning thm = 

263 
let 

264 
val str_of_sort = Sign.str_of_sort (Thm.sign_of_thm thm); 

265 
val thm' = Thm.strip_shyps thm; 

266 
val xshyps = Thm.extra_shyps thm'; 

267 
in 

268 
if null xshyps then () 

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

270 
thm' 

271 
end; 

272 

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

275 
 forall_intr_list (y::ys) th = 

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

276 
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

277 
in forall_intr y gth handle THM _ => gth end; 
0  278 

279 
(*Generalization over all suitable Free variables*) 

280 
fun forall_intr_frees th = 

281 
let val {prop,sign,...} = rep_thm th 

282 
in forall_intr_list 

4440  283 
(map (cterm_of sign) (sort (make_ord atless) (term_frees prop))) 
0  284 
th 
285 
end; 

286 

7898  287 
val forall_elim_var = PureThy.forall_elim_var; 
288 
val forall_elim_vars = PureThy.forall_elim_vars; 

0  289 

9554  290 
fun forall_elim_vars_safe th = 
291 
forall_elim_vars_safe (forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th) 

292 
handle THM _ => th; 

293 

294 

0  295 
(*Specialization over a list of cterms*) 
296 
fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th); 

297 

298 
(* maps [A1,...,An], B to [ A1;...;An ] ==> B *) 

299 
fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th); 

300 

301 
(* maps [ A1;...;An ] ==> B and [A1,...,An] to B *) 

302 
fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths); 

303 

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

305 
fun zero_var_indexes th = 
0  306 
let val {prop,sign,...} = rep_thm th; 
307 
val vars = term_vars prop 

308 
val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars) 

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

309 
val inrs = add_term_tvars(prop,[]); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

310 
val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs)); 
2266  311 
val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs))) 
8328  312 
(inrs, nms') 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

313 
val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye; 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

314 
fun varpairs([],[]) = [] 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

315 
 varpairs((var as Var(v,T)) :: vars, b::bs) = 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

316 
let val T' = typ_subst_TVars tye T 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

317 
in (cterm_of sign (Var(v,T')), 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

318 
cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs) 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

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

320 
 varpairs _ = raise TERM("varpairs", []); 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

321 
in Thm.instantiate (ctye, varpairs(vars,rev bs)) th end; 
0  322 

323 

324 
(*Standard form of objectrule: no hypotheses, Frees, or outer quantifiers; 

325 
all generality expressed by Vars having index 0.*) 

10515  326 

327 
fun close_derivation thm = 

328 
if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm) 

329 
else thm; 

330 

0  331 
fun standard th = 
10515  332 
let val {maxidx,...} = rep_thm th in 
333 
th 

334 
> implies_intr_hyps 

335 
> forall_intr_frees > forall_elim_vars (maxidx + 1) 

336 
> strip_shyps_warning 

337 
> zero_var_indexes > Thm.varifyT > Thm.compress > close_derivation 

1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

338 
end; 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

339 

0  340 

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

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

343 
Similar code in type/freeze_thaw*) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

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

345 
let val fth = freezeT th 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

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

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

348 
case term_vars prop of 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

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

350 
 vars => 
8328  351 
let fun newName (Var(ix,_), (pairs,used)) = 
352 
let val v = variant used (string_of_indexname ix) 

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

354 
val (alist, _) = foldr newName 

355 
(vars, ([], add_term_names (prop, []))) 

356 
fun mk_inst (Var(v,T)) = 

357 
(cterm_of sign (Var(v,T)), 

358 
cterm_of sign (Free(the (assoc(alist,v)), T))) 

359 
val insts = map mk_inst vars 

360 
fun thaw th' = 

361 
th' > forall_intr_list (map #2 insts) 

362 
> forall_elim_list (map #1 insts) 

363 
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

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

365 

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

366 

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

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

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

369 

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

370 

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

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

374 
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

375 
[ !(A,P,a)[ ALL x:A. P(x) ] ==> [ P(a) ] ] *) 
0  376 
fun assume_ax thy sP = 
6390  377 
let val sign = Theory.sign_of thy 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

378 
val prop = Logic.close_form (term_of (read_cterm sign (sP, propT))) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

379 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  380 

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

381 
(*Resolution: exactly one resolvent must be produced.*) 
0  382 
fun tha RSN (i,thb) = 
4270  383 
case Seq.chop (2, biresolution false [(false,tha)] i thb) of 
0  384 
([th],_) => th 
385 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

387 

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

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

390 

391 
(*For joining lists of rules*) 

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

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

395 
in List.concat (map resb thbs) end; 
0  396 

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

398 

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

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

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

401 
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

402 
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

403 
 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

404 
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

405 

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

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

407 
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

408 
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

409 
 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

410 
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

411 

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

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

413 
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

414 

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

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

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

418 
fun compose(tha,i,thb) = 
4270  419 
Seq.list_of (bicompose false (false,tha,0) i thb); 
0  420 

6946  421 
fun compose_single (tha,i,thb) = 
422 
(case compose (tha,i,thb) of 

423 
[th] => th 

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

425 

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

428 
case compose(tha,1,thb) of 

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

429 
[th] => th 
0  430 
 _ => raise THM("COMP", 1, [tha,thb]); 
431 

4016  432 
(** theorem equality **) 
0  433 

434 
(*Do the two theorems have the same signature?*) 

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

435 
fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2)); 
0  436 

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

438 
val size_of_thm = size_of_term o #prop o rep_thm; 

439 

9829  440 
(*maintain lists of theorems  preserving canonical order*) 
441 
fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs); 

9862  442 
fun add_rules rs rules = rs @ del_rules rs rules; 
9829  443 
fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2; 
444 

0  445 

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

446 
(** Mark Staples's weaker version of eq_thm: ignores variable renaming and 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

447 
(some) type variable renaming **) 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

448 

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

449 
(* Can't use term_vars, because it sorts the resulting list of variable names. 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

450 
We instead need the unique list noramlised by the order of appearance 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

451 
in the term. *) 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

452 
fun term_vars' (t as Var(v,T)) = [t] 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

453 
 term_vars' (Abs(_,_,b)) = term_vars' b 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

454 
 term_vars' (f$a) = (term_vars' f) @ (term_vars' a) 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

455 
 term_vars' _ = []; 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

456 

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

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

458 
let val {prop,sign,...} = rep_thm th; 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

459 
val vars = distinct (term_vars' prop); 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

460 
in forall_intr_list (map (cterm_of sign) vars) th end; 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

461 

1237  462 
fun weak_eq_thm (tha,thb) = 
1194
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

463 
eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb)); 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

464 

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

465 

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

466 

0  467 
(*** MetaRewriting Rules ***) 
468 

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

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

470 

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

4016  473 

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

475 
let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS))) 
9455  476 
in store_standard_thm "reflexive" (Thm.reflexive cx) end; 
0  477 

478 
val symmetric_thm = 

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

479 
let val xy = read_prop "x::'a::logic == y" 
9455  480 
in store_standard_thm "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end; 
0  481 

482 
val transitive_thm = 

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

483 
let val xy = read_prop "x::'a::logic == y" 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

484 
val yz = read_prop "y::'a::logic == z" 
0  485 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
9455  486 
in store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 
0  487 

4679  488 
fun symmetric_fun thm = thm RS symmetric_thm; 
489 

10414  490 
val imp_cong = 
491 
let 

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

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

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

495 
val A = read_prop "PROP A" 

496 
in 

11120  497 
store_standard_thm "imp_cong" (implies_intr ABC (equal_intr 
10414  498 
(implies_intr AB (implies_intr A 
499 
(equal_elim (implies_elim (assume ABC) (assume A)) 

500 
(implies_elim (assume AB) (assume A))))) 

501 
(implies_intr AC (implies_intr A 

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

503 
(implies_elim (assume AC) (assume A))))))) 

504 
end; 

505 

506 
val swap_prems_eq = 

507 
let 

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

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

510 
val A = read_prop "PROP A" 

511 
val B = read_prop "PROP B" 

512 
in 

513 
store_standard_thm "swap_prems_eq" (equal_intr 

514 
(implies_intr ABC (implies_intr B (implies_intr A 

515 
(implies_elim (implies_elim (assume ABC) (assume A)) (assume B))))) 

516 
(implies_intr BAC (implies_intr A (implies_intr B 

517 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

518 
end; 

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

519 

9547  520 
val refl_implies = reflexive implies; 
0  521 

522 

523 
(*** Some useful metatheorems ***) 

524 

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

9455  526 
val asm_rl = store_standard_thm "asm_rl" (Thm.trivial (read_prop "PROP ?psi")); 
7380  527 
val _ = store_thm "_" asm_rl; 
0  528 

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

4016  530 
val cut_rl = 
9455  531 
store_standard_thm "cut_rl" 
532 
(Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta")); 

0  533 

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

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

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

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

538 
and VW = read_prop "PROP V ==> PROP W"; 
4016  539 
in 
9455  540 
store_standard_thm "revcut_rl" 
4016  541 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  542 
end; 
543 

668  544 
(*for deleting an unwanted assumption*) 
545 
val thin_rl = 

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

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

547 
and W = read_prop "PROP W"; 
9455  548 
in store_standard_thm "thin_rl" (implies_intr V (implies_intr W (assume W))) 
668  549 
end; 
550 

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

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

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

554 
and QV = read_prop "!!x::'a. PROP V" 
8086  555 
and x = read_cterm proto_sign ("x", TypeInfer.logicT); 
4016  556 
in 
9455  557 
store_standard_thm "triv_forall_equality" 
558 
(standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) 

559 
(implies_intr V (forall_intr x (assume V))))) 

0  560 
end; 
561 

1756  562 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
563 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

565 
*) 

566 
val swap_prems_rl = 

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

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

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

571 
val cminor2 = read_prop "PROP PhiB"; 
1756  572 
val minor2 = assume cminor2; 
9455  573 
in store_standard_thm "swap_prems_rl" 
1756  574 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
575 
(implies_elim (implies_elim major minor1) minor2)))) 

576 
end; 

577 

3653  578 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
579 
==> PROP ?phi == PROP ?psi 

8328  580 
Introduction rule for == as a metatheorem. 
3653  581 
*) 
582 
val equal_intr_rule = 

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

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

584 
and QP = read_prop "PROP psi ==> PROP phi" 
4016  585 
in 
9455  586 
store_standard_thm "equal_intr_rule" 
4016  587 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  588 
end; 
589 

4285  590 

9554  591 
(*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) 
592 
Rewrite rule for HHF normalization. 

593 
*) 

594 

595 
val norm_hhf_eq = 

596 
let 

597 
val cert = Thm.cterm_of proto_sign; 

598 
val aT = TFree ("'a", Term.logicS); 

599 
val all = Term.all aT; 

600 
val x = Free ("x", aT); 

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

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

603 

604 
val cx = cert x; 

605 
val cphi = cert phi; 

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

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

608 
in 

609 
Thm.equal_intr 

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

611 
> Thm.forall_elim cx 

612 
> Thm.implies_intr cphi 

613 
> Thm.forall_intr cx 

614 
> Thm.implies_intr lhs) 

615 
(Thm.implies_elim 

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

617 
> Thm.forall_intr cx 

618 
> Thm.implies_intr cphi 

619 
> Thm.implies_intr rhs) 

10441  620 
> store_standard_thm "norm_hhf_eq" 
9554  621 
end; 
622 

623 

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

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

625 

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

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

627 
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

628 

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

629 
fun read_instantiate_sg sg sinsts th = 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

630 
let val ts = types_sorts th; 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

631 
val used = add_term_tvarnames(#prop(rep_thm th),[]); 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

632 
in instantiate (read_insts sg ts ts used sinsts) th end; 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

633 

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

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

635 
fun read_instantiate sinsts th = 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

636 
read_instantiate_sg (#sign (rep_thm th)) sinsts th; 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

637 

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

638 

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

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

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

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

642 
fun add_types ((ct,cu), (sign,tye,maxidx)) = 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

643 
let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

645 
val maxi = Int.max(maxidx, Int.max(maxt, maxu)); 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

646 
val sign' = Sign.merge(sign, Sign.merge(signt, signu)) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

647 
val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U) 
10403  648 
handle Type.TUNIFY => raise TYPE("Illtyped instantiation", [T,U], [t,u]) 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

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

651 
fun cterm_instantiate ctpairs0 th = 
8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
8365
diff
changeset

652 
let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0)) 
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
8365
diff
changeset

653 
fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

654 
in (cterm_fun inst ct, cterm_fun inst cu) end 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

655 
fun ctyp2 (ix,T) = (ix, ctyp_of sign T) 
8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
8365
diff
changeset

656 
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

657 
handle TERM _ => 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

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

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

661 

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

662 

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

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

664 

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

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

666 
fun equal_abs_elim ca eqth = 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

667 
let val {sign=signa, t=a, ...} = rep_cterm ca 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

668 
and combth = combination eqth (reflexive ca) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

670 
val (abst,absu) = Logic.dest_equals prop 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

671 
val cterm = cterm_of (Sign.merge (sign,signa)) 
10414  672 
in transitive (symmetric (beta_conversion false (cterm (abst$a)))) 
673 
(transitive combth (beta_conversion false (cterm (absu$a)))) 

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

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

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

676 

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

677 
(*Calling equal_abs_elim with multiple terms*) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

679 

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

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

681 
val alpha = TVar(("'a",0), []) (* type ?'a::{} *) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

682 
fun err th = raise THM("flexpair_inst: ", 0, [th]) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

683 
fun flexpair_inst def th = 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

684 
let val {prop = Const _ $ t $ u, sign,...} = rep_thm th 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

685 
val cterm = cterm_of sign 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

686 
fun cvar a = cterm(Var((a,0),alpha)) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

687 
val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

689 
in equal_elim def' th 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

691 
handle THM _ => err th  Bind => err th 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

693 
val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

694 
and flexpair_elim = flexpair_inst ProtoPure.flexpair_def 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

696 

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

697 
(*Version for flexflex pairs  this supports lifting.*) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

698 
fun flexpair_abs_elim_list cts = 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

699 
flexpair_intr o equal_abs_elim_list cts o flexpair_elim; 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

700 

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

701 

10667  702 
(*** Goal (PROP A) <==> PROP A ***) 
4789  703 

704 
local 

10667  705 
val cert = Thm.cterm_of proto_sign; 
706 
val A = Free ("A", propT); 

707 
val G = Logic.mk_goal A; 

4789  708 
val (G_def, _) = freeze_thaw ProtoPure.Goal_def; 
709 
in 

10667  710 
val triv_goal = store_thm "triv_goal" (tag_rule internal_tag (standard 
711 
(Thm.equal_elim (Thm.symmetric G_def) (Thm.assume (cert A))))); 

712 
val rev_triv_goal = store_thm "rev_triv_goal" (tag_rule internal_tag (standard 

713 
(Thm.equal_elim G_def (Thm.assume (cert G))))); 

4789  714 
end; 
715 

9460  716 
val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const); 
6995  717 
fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal; 
718 

4789  719 

4285  720 

5688  721 
(** variations on instantiate **) 
4285  722 

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

723 
(*shorthand for instantiating just one variable in the current theory*) 
b44c185f8018
new metarule "inst", a shorthand for read_instantiate_sg
paulson
parents:
8496
diff
changeset

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

725 

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

726 

4285  727 
(* collect vars *) 
728 

729 
val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs  (vs, _) => vs); 

730 
val add_tvars = foldl_types add_tvarsT; 

731 
val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs  (vs, _) => vs); 

732 

5903  733 
fun tvars_of_terms ts = rev (foldl add_tvars ([], ts)); 
734 
fun vars_of_terms ts = rev (foldl add_vars ([], ts)); 

735 

736 
fun tvars_of thm = tvars_of_terms [#prop (Thm.rep_thm thm)]; 

737 
fun vars_of thm = vars_of_terms [#prop (Thm.rep_thm thm)]; 

4285  738 

739 

740 
(* instantiate by lefttoright occurrence of variables *) 

741 

742 
fun instantiate' cTs cts thm = 

743 
let 

744 
fun err msg = 

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

746 
mapfilter (apsome Thm.typ_of) cTs, 

747 
mapfilter (apsome Thm.term_of) cts); 

748 

749 
fun inst_of (v, ct) = 

750 
(Thm.cterm_of (#sign (Thm.rep_cterm ct)) (Var v), ct) 

751 
handle TYPE (msg, _, _) => err msg; 

752 

753 
fun zip_vars _ [] = [] 

754 
 zip_vars (_ :: vs) (None :: opt_ts) = zip_vars vs opt_ts 

755 
 zip_vars (v :: vs) (Some t :: opt_ts) = (v, t) :: zip_vars vs opt_ts 

756 
 zip_vars [] _ = err "more instantiations than variables in thm"; 

757 

758 
(*instantiate types first!*) 

759 
val thm' = 

760 
if forall is_none cTs then thm 

761 
else Thm.instantiate (zip_vars (map fst (tvars_of thm)) cTs, []) thm; 

762 
in 

763 
if forall is_none cts then thm' 

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

765 
end; 

766 

767 

5688  768 
(* unvarify(T) *) 
769 

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

771 

772 
fun unvarifyT thm = 

773 
let 

774 
val cT = Thm.ctyp_of (Thm.sign_of_thm thm); 

775 
val tfrees = map (fn ((x, _), S) => Some (cT (TFree (x, S)))) (tvars_of thm); 

776 
in instantiate' tfrees [] thm end; 

777 

778 
fun unvarify raw_thm = 

779 
let 

780 
val thm = unvarifyT raw_thm; 

781 
val ct = Thm.cterm_of (Thm.sign_of_thm thm); 

782 
val frees = map (fn ((x, _), T) => Some (ct (Free (x, T)))) (vars_of thm); 

783 
in instantiate' [] frees thm end; 

784 

785 

8605  786 
(* tvars_intr_list *) 
787 

788 
fun tfrees_of thm = 

789 
let val {hyps, prop, ...} = Thm.rep_thm thm 

790 
in foldr Term.add_term_tfree_names (prop :: hyps, []) end; 

791 

792 
fun tvars_intr_list tfrees thm = 

793 
Thm.varifyT' (tfrees_of thm \\ tfrees) thm; 

794 

795 

6435  796 
(* increment var indexes *) 
797 

798 
fun incr_indexes_wrt is cTs cts thms = 

799 
let 

800 
val maxidx = 

801 
foldl Int.max (~1, is @ 

802 
map (maxidx_of_typ o #T o Thm.rep_ctyp) cTs @ 

803 
map (#maxidx o Thm.rep_cterm) cts @ 

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

10414  805 
in Thm.incr_indexes (maxidx + 1) end; 
6435  806 

807 

8328  808 
(* freeze_all *) 
809 

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

811 

812 
fun freeze_all_TVars thm = 

813 
(case tvars_of thm of 

814 
[] => thm 

815 
 tvars => 

816 
let val cert = Thm.ctyp_of (Thm.sign_of_thm thm) 

817 
in instantiate' (map (fn ((x, _), S) => Some (cert (TFree (x, S)))) tvars) [] thm end); 

818 

819 
fun freeze_all_Vars thm = 

820 
(case vars_of thm of 

821 
[] => thm 

822 
 vars => 

823 
let val cert = Thm.cterm_of (Thm.sign_of_thm thm) 

824 
in instantiate' [] (map (fn ((x, _), T) => Some (cert (Free (x, T)))) vars) thm end); 

825 

826 
val freeze_all = freeze_all_Vars o freeze_all_TVars; 

827 

828 

5688  829 
(* mk_triv_goal *) 
830 

831 
(*make an initial proof state, "PROP A ==> (PROP A)" *) 

5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5079
diff
changeset

832 
fun mk_triv_goal ct = instantiate' [] [Some ct] triv_goal; 
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5079
diff
changeset

833 

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

835 

5903  836 

837 
structure BasicDrule: BASIC_DRULE = Drule; 

838 
open BasicDrule; 