author  wenzelm 
Tue, 05 Sep 2000 18:50:52 +0200  
changeset 9862  96138f29545e 
parent 9829  bf49c3796599 
child 10403  2955ee2424ce 
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 
8328  16 
val skip_flexpairs : cterm > cterm 
17 
val strip_imp_prems : cterm > cterm list 

18 
val cprems_of : thm > cterm list 

19 
val read_insts : 

4285  20 
Sign.sg > (indexname > typ option) * (indexname > sort option) 
21 
> (indexname > typ option) * (indexname > sort option) 

22 
> string list > (string*string)list 

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

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

7636  25 
val strip_shyps_warning : thm > thm 
8328  26 
val forall_intr_list : cterm list > thm > thm 
27 
val forall_intr_frees : thm > thm 

28 
val forall_intr_vars : thm > thm 

29 
val forall_elim_list : cterm list > thm > thm 

30 
val forall_elim_var : int > thm > thm 

31 
val forall_elim_vars : int > thm > thm 

9554  32 
val forall_elim_vars_safe : thm > thm 
8328  33 
val freeze_thaw : thm > thm * (thm > thm) 
34 
val implies_elim_list : thm > thm list > thm 

35 
val implies_intr_list : cterm list > thm > thm 

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

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

37 
(indexname * ctyp) list * (cterm * cterm) list > thm > thm 
8328  38 
val zero_var_indexes : thm > thm 
39 
val standard : thm > thm 

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

40 
val rotate_prems : int > thm > thm 
8328  41 
val assume_ax : theory > string > thm 
42 
val RSN : thm * (int * thm) > thm 

43 
val RS : thm * thm > thm 

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

45 
val RL : thm list * thm list > thm list 

46 
val MRS : thm list * thm > thm 

47 
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

48 
val OF : thm * thm list > thm 
8328  49 
val compose : thm * int * thm > thm list 
50 
val COMP : thm * thm > thm 

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

54 
val weak_eq_thm : thm * thm > bool 

55 
val eq_thm_sg : thm * thm > bool 

56 
val size_of_thm : thm > int 

57 
val reflexive_thm : thm 

58 
val symmetric_thm : thm 

59 
val transitive_thm : thm 

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

60 
val refl_implies : thm 
4679  61 
val symmetric_fun : thm > thm 
8328  62 
val rewrite_rule_aux : (meta_simpset > thm > thm option) > thm list > thm > thm 
63 
val rewrite_thm : bool * bool * bool 

4713  64 
> (meta_simpset > thm > thm option) 
65 
> meta_simpset > thm > thm 

8328  66 
val rewrite_cterm : bool * bool * bool 
5079  67 
> (meta_simpset > thm > thm option) 
68 
> meta_simpset > cterm > thm 

4285  69 
val rewrite_goals_rule_aux: (meta_simpset > thm > thm option) > thm list > thm > thm 
8328  70 
val rewrite_goal_rule : bool* bool * bool 
4713  71 
> (meta_simpset > thm > thm option) 
72 
> meta_simpset > int > thm > thm 

8328  73 
val equal_abs_elim : cterm > thm > thm 
4285  74 
val equal_abs_elim_list: cterm list > thm > thm 
75 
val flexpair_abs_elim_list: cterm list > thm > thm 

8328  76 
val asm_rl : thm 
77 
val cut_rl : thm 

78 
val revcut_rl : thm 

79 
val thin_rl : thm 

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

83 
val inst : string > string > thm > thm 
8328  84 
val instantiate' : ctyp option list > cterm option list > thm > thm 
85 
val incr_indexes : int > thm > thm 

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

5903  87 
end; 
88 

89 
signature DRULE = 

90 
sig 

91 
include BASIC_DRULE 

9455  92 
val rule_attribute : ('a > thm > thm) > 'a attribute 
93 
val tag_rule : tag > thm > thm 

94 
val untag_rule : string > thm > thm 

95 
val tag : tag > 'a attribute 

96 
val untag : string > 'a attribute 

97 
val tag_lemma : 'a attribute 

98 
val tag_assumption : 'a attribute 

99 
val tag_internal : 'a attribute 

100 
val has_internal : tag list > bool 

8328  101 
val compose_single : thm * int * thm > thm 
9829  102 
val add_rules : thm list > thm list > thm list 
103 
val del_rules : thm list > thm list > thm list 

9418  104 
val merge_rules : thm list * thm list > thm list 
9554  105 
val norm_hhf_eq : thm 
8328  106 
val triv_goal : thm 
107 
val rev_triv_goal : thm 

108 
val freeze_all : thm > thm 

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

109 
val mk_triv_goal : cterm > thm 
8328  110 
val mk_cgoal : cterm > cterm 
111 
val assume_goal : cterm > thm 

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

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

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

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

116 
val unvarifyT : thm > thm 

117 
val unvarify : thm > thm 

8605  118 
val tvars_intr_list : string list > thm > thm 
3766  119 
end; 
0  120 

5903  121 
structure Drule: DRULE = 
0  122 
struct 
123 

3991  124 

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

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

126 

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

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

128 

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

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

130 
fun dest_implies ct = 
8328  131 
case term_of ct of 
132 
(Const("==>", _) $ _ $ _) => 

133 
let val (ct1,ct2) = dest_comb ct 

134 
in (#2 (dest_comb ct1), ct2) end 

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

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

136 

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("==>", _) $ _ $ _) => 
154 
strip_imp_concl (#2 (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*) 

165 
fun mk_implies(A,B) = capply (capply implies A) B; 

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 = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

181 
let val {tsig,...} = Sign.rep_sg sign 
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; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

191 
in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) 
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.*) 

326 
fun standard th = 

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

327 
let val {maxidx,...} = rep_thm th 
1237  328 
in 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

329 
th > implies_intr_hyps 
1412  330 
> forall_intr_frees > forall_elim_vars (maxidx + 1) 
7636  331 
> strip_shyps_warning 
1412  332 
> zero_var_indexes > Thm.varifyT > Thm.compress 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

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

334 

0  335 

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

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

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

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

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

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

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

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

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

345 
 vars => 
8328  346 
let fun newName (Var(ix,_), (pairs,used)) = 
347 
let val v = variant used (string_of_indexname ix) 

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

349 
val (alist, _) = foldr newName 

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

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

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

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

354 
val insts = map mk_inst vars 

355 
fun thaw th' = 

356 
th' > forall_intr_list (map #2 insts) 

357 
> forall_elim_list (map #1 insts) 

358 
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

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

360 

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

361 

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

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

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

364 

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

365 

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

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

369 
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

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

373 
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

374 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  375 

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

376 
(*Resolution: exactly one resolvent must be produced.*) 
0  377 
fun tha RSN (i,thb) = 
4270  378 
case Seq.chop (2, biresolution false [(false,tha)] i thb) of 
0  379 
([th],_) => th 
380 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

382 

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

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

385 

386 
(*For joining lists of rules*) 

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

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

390 
in List.concat (map resb thbs) end; 
0  391 

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

393 

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

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

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

396 
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

397 
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

398 
 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

399 
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

400 

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

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

402 
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

403 
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

404 
 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

405 
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

406 

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

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

408 
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

409 

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

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

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

413 
fun compose(tha,i,thb) = 
4270  414 
Seq.list_of (bicompose false (false,tha,0) i thb); 
0  415 

6946  416 
fun compose_single (tha,i,thb) = 
417 
(case compose (tha,i,thb) of 

418 
[th] => th 

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

420 

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

423 
case compose(tha,1,thb) of 

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

424 
[th] => th 
0  425 
 _ => raise THM("COMP", 1, [tha,thb]); 
426 

4016  427 
(** theorem equality **) 
0  428 

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

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

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

433 
val size_of_thm = size_of_term o #prop o rep_thm; 

434 

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

9862  437 
fun add_rules rs rules = rs @ del_rules rs rules; 
9829  438 
fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2; 
439 

0  440 

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

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

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

443 

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

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

445 
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

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

447 
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

448 
 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

449 
 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

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

451 

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

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

453 
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

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

455 
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

456 

1237  457 
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

458 
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

459 

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

460 

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

461 

0  462 
(*** MetaRewriting Rules ***) 
463 

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

464 
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

465 

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

4016  468 

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

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

473 
val symmetric_thm = 

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

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

477 
val transitive_thm = 

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

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

479 
val yz = read_prop "y::'a::logic == z" 
0  480 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
9455  481 
in store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 
0  482 

4679  483 
fun symmetric_fun thm = thm RS symmetric_thm; 
484 

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

485 
(** Below, a "conversion" has type cterm > thm **) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

486 

9547  487 
val refl_implies = reflexive implies; 
0  488 

489 
(*In [A1,...,An]==>B, rewrite the selected A's only  for rewrite_goals_tac*) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

490 
(*Do not rewrite flexflex pairs*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

491 
fun goals_conv pred cv = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

492 
let fun gconv i ct = 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

493 
let val (A,B) = dest_implies ct 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

494 
val (thA,j) = case term_of A of 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

495 
Const("=?=",_)$_$_ => (reflexive A, i) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

496 
 _ => (if pred i then cv A else reflexive A, i+1) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

497 
in combination (combination refl_implies thA) (gconv j B) end 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

498 
handle TERM _ => reflexive ct 
0  499 
in gconv 1 end; 
500 

501 
(*Use a conversion to transform a theorem*) 

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

502 
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; 
0  503 

504 
(*rewriting conversion*) 

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

505 
fun rew_conv mode prover mss = rewrite_cterm mode mss prover; 
0  506 

507 
(*Rewrite a theorem*) 

9554  508 
fun rewrite_rule_aux _ [] = (fn th => th) 
509 
 rewrite_rule_aux prover thms = 

510 
fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)); 

0  511 

3555  512 
fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss); 
5079  513 
fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover; 
3555  514 

0  515 
(*Rewrite the subgoals of a proof state (represented by a theorem) *) 
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

516 
fun rewrite_goals_rule_aux _ [] th = th 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

517 
 rewrite_goals_rule_aux prover thms th = 
4713  518 
fconv_rule (goals_conv (K true) (rew_conv (true, true, false) prover 
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

519 
(Thm.mss_of thms))) th; 
0  520 

521 
(*Rewrite the subgoal of a proof state (represented by a theorem) *) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

522 
fun rewrite_goal_rule mode prover mss i thm = 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

523 
if 0 < i andalso i <= nprems_of thm 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

524 
then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

525 
else raise THM("rewrite_goal_rule",i,[thm]); 
0  526 

527 

528 
(*** Some useful metatheorems ***) 

529 

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

9455  531 
val asm_rl = store_standard_thm "asm_rl" (Thm.trivial (read_prop "PROP ?psi")); 
7380  532 
val _ = store_thm "_" asm_rl; 
0  533 

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

4016  535 
val cut_rl = 
9455  536 
store_standard_thm "cut_rl" 
537 
(Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta")); 

0  538 

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

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

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

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

543 
and VW = read_prop "PROP V ==> PROP W"; 
4016  544 
in 
9455  545 
store_standard_thm "revcut_rl" 
4016  546 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  547 
end; 
548 

668  549 
(*for deleting an unwanted assumption*) 
550 
val thin_rl = 

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

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

552 
and W = read_prop "PROP W"; 
9455  553 
in store_standard_thm "thin_rl" (implies_intr V (implies_intr W (assume W))) 
668  554 
end; 
555 

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

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

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

559 
and QV = read_prop "!!x::'a. PROP V" 
8086  560 
and x = read_cterm proto_sign ("x", TypeInfer.logicT); 
4016  561 
in 
9455  562 
store_standard_thm "triv_forall_equality" 
563 
(standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) 

564 
(implies_intr V (forall_intr x (assume V))))) 

0  565 
end; 
566 

1756  567 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
568 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

570 
*) 

571 
val swap_prems_rl = 

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

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

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

576 
val cminor2 = read_prop "PROP PhiB"; 
1756  577 
val minor2 = assume cminor2; 
9455  578 
in store_standard_thm "swap_prems_rl" 
1756  579 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
580 
(implies_elim (implies_elim major minor1) minor2)))) 

581 
end; 

582 

3653  583 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
584 
==> PROP ?phi == PROP ?psi 

8328  585 
Introduction rule for == as a metatheorem. 
3653  586 
*) 
587 
val equal_intr_rule = 

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

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

589 
and QP = read_prop "PROP psi ==> PROP phi" 
4016  590 
in 
9455  591 
store_standard_thm "equal_intr_rule" 
4016  592 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  593 
end; 
594 

4285  595 

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

598 

599 
Note: the syntax of ProtoPure is insufficient to handle this 

600 
statement; storing it would be asking for trouble, e.g. when someone 

601 
tries to print the theory later. 

602 
*) 

603 

604 
val norm_hhf_eq = 

605 
let 

606 
val cert = Thm.cterm_of proto_sign; 

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

608 
val all = Term.all aT; 

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

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

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

612 

613 
val cx = cert x; 

614 
val cphi = cert phi; 

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

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

617 
in 

618 
Thm.equal_intr 

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

620 
> Thm.forall_elim cx 

621 
> Thm.implies_intr cphi 

622 
> Thm.forall_intr cx 

623 
> Thm.implies_intr lhs) 

624 
(Thm.implies_elim 

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

626 
> Thm.forall_intr cx 

627 
> Thm.implies_intr cphi 

628 
> Thm.implies_intr rhs) 

629 
> standard > curry Thm.name_thm "ProtoPure.norm_hhf_eq" 

630 
end; 

631 

632 

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

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

634 

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

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

636 
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

637 

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

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

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

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

641 
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

642 

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

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

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

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

646 

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

647 

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

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

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

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

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

652 
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

653 
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

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

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

656 
val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

657 
handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u]) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

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

660 
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

661 
let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0)) 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

662 
val tsig = #tsig(Sign.rep_sg sign); 
8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
8365
diff
changeset

663 
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

664 
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

665 
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

666 
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

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

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

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

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

671 

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

672 

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

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

674 

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

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

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

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

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

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

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

681 
val cterm = cterm_of (Sign.merge (sign,signa)) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

682 
in transitive (symmetric (beta_conversion (cterm (abst$a)))) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

683 
(transitive combth (beta_conversion (cterm (absu$a)))) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

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

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

686 

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

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

688 
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

689 

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

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

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

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

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

694 
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

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

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

697 
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

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

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

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

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

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

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

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

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

706 

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

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

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

709 
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

710 

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

711 

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

712 
(*** GOAL (PROP A) <==> PROP A ***) 
4789  713 

714 
local 

715 
val A = read_prop "PROP A"; 

716 
val G = read_prop "GOAL (PROP A)"; 

717 
val (G_def, _) = freeze_thaw ProtoPure.Goal_def; 

718 
in 

9455  719 
val triv_goal = store_thm "triv_goal" 
720 
(tag_rule internal_tag (standard (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume A)))); 

721 
val rev_triv_goal = store_thm "rev_triv_goal" 

722 
(tag_rule internal_tag (standard (Thm.equal_elim G_def (Thm.assume G)))); 

4789  723 
end; 
724 

9460  725 
val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const); 
6995  726 
fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal; 
727 

4789  728 

4285  729 

5688  730 
(** variations on instantiate **) 
4285  731 

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

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

733 
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

734 

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

735 

4285  736 
(* collect vars *) 
737 

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

739 
val add_tvars = foldl_types add_tvarsT; 

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

741 

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

744 

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

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

4285  747 

748 

749 
(* instantiate by lefttoright occurrence of variables *) 

750 

751 
fun instantiate' cTs cts thm = 

752 
let 

753 
fun err msg = 

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

755 
mapfilter (apsome Thm.typ_of) cTs, 

756 
mapfilter (apsome Thm.term_of) cts); 

757 

758 
fun inst_of (v, ct) = 

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

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

761 

762 
fun zip_vars _ [] = [] 

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

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

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

766 

767 
(*instantiate types first!*) 

768 
val thm' = 

769 
if forall is_none cTs then thm 

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

771 
in 

772 
if forall is_none cts then thm' 

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

774 
end; 

775 

776 

5688  777 
(* unvarify(T) *) 
778 

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

780 

781 
fun unvarifyT thm = 

782 
let 

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

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

785 
in instantiate' tfrees [] thm end; 

786 

787 
fun unvarify raw_thm = 

788 
let 

789 
val thm = unvarifyT raw_thm; 

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

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

792 
in instantiate' [] frees thm end; 

793 

794 

8605  795 
(* tvars_intr_list *) 
796 

797 
fun tfrees_of thm = 

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

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

800 

801 
fun tvars_intr_list tfrees thm = 

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

803 

804 

6435  805 
(* increment var indexes *) 
806 

807 
fun incr_indexes 0 thm = thm 

808 
 incr_indexes inc thm = 

809 
let 

810 
val sign = Thm.sign_of_thm thm; 

811 

812 
fun inc_tvar ((x, i), S) = Some (Thm.ctyp_of sign (TVar ((x, i + inc), S))); 

813 
fun inc_var ((x, i), T) = Some (Thm.cterm_of sign (Var ((x, i + inc), T))); 

6930  814 
val thm' = instantiate' (map inc_tvar (tvars_of thm)) [] thm; 
815 
val thm'' = instantiate' [] (map inc_var (vars_of thm')) thm'; 

816 
in thm'' end; 

6435  817 

818 
fun incr_indexes_wrt is cTs cts thms = 

819 
let 

820 
val maxidx = 

821 
foldl Int.max (~1, is @ 

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

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

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

825 
in incr_indexes (maxidx + 1) end; 

826 

827 

8328  828 
(* freeze_all *) 
829 

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

831 

832 
fun freeze_all_TVars thm = 

833 
(case tvars_of thm of 

834 
[] => thm 

835 
 tvars => 

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

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

838 

839 
fun freeze_all_Vars thm = 

840 
(case vars_of thm of 

841 
[] => thm 

842 
 vars => 

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

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

845 

846 
val freeze_all = freeze_all_Vars o freeze_all_TVars; 

847 

848 

5688  849 
(* mk_triv_goal *) 
850 

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

852 
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

853 

5688  854 

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

856 

5903  857 

858 
structure BasicDrule: BASIC_DRULE = Drule; 

859 
open BasicDrule; 