author  berghofe 
Wed, 31 Oct 2001 19:32:05 +0100  
changeset 11997  402ae1a172ae 
parent 11975  129c6679e8c4 
child 12005  291593391010 
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 

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

42 
val standard' : thm > thm 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

43 
val rotate_prems : int > thm > thm 
11163  44 
val rearrange_prems : int list > thm > thm 
8328  45 
val assume_ax : theory > string > thm 
46 
val RSN : thm * (int * thm) > thm 

47 
val RS : thm * thm > thm 

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

49 
val RL : thm list * thm list > thm list 

50 
val MRS : thm list * thm > thm 

51 
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

52 
val OF : thm * thm list > thm 
8328  53 
val compose : thm * int * thm > thm list 
54 
val COMP : thm * thm > thm 

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

58 
val weak_eq_thm : thm * thm > bool 

59 
val eq_thm_sg : thm * thm > bool 

60 
val size_of_thm : thm > int 

61 
val reflexive_thm : thm 

62 
val symmetric_thm : thm 

63 
val transitive_thm : thm 

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

64 
val refl_implies : thm 
4679  65 
val symmetric_fun : thm > thm 
11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

66 
val extensional : thm > thm 
10414  67 
val imp_cong : thm 
68 
val swap_prems_eq : thm 

8328  69 
val equal_abs_elim : cterm > thm > thm 
4285  70 
val equal_abs_elim_list: cterm list > thm > thm 
71 
val flexpair_abs_elim_list: cterm list > thm > thm 

8328  72 
val asm_rl : thm 
73 
val cut_rl : thm 

74 
val revcut_rl : thm 

75 
val thin_rl : thm 

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

79 
val inst : string > string > thm > thm 
8328  80 
val instantiate' : ctyp option list > cterm option list > thm > thm 
81 
val incr_indexes_wrt : int list > ctyp list > cterm list > thm list > thm > thm 

5903  82 
end; 
83 

84 
signature DRULE = 

85 
sig 

86 
include BASIC_DRULE 

11975  87 
val rule_attribute: ('a > thm > thm) > 'a attribute 
88 
val tag_rule: tag > thm > thm 

89 
val untag_rule: string > thm > thm 

90 
val tag: tag > 'a attribute 

91 
val untag: string > 'a attribute 

92 
val get_kind: thm > string 

93 
val kind: string > 'a attribute 

94 
val theoremK: string 

95 
val lemmaK: string 

96 
val corollaryK: string 

97 
val internalK: string 

98 
val kind_internal: 'a attribute 

99 
val has_internal: tag list > bool 

100 
val impose_hyps: cterm list > thm > thm 

101 
val close_derivation: thm > thm 

102 
val compose_single: thm * int * thm > thm 

103 
val add_rules: thm list > thm list > thm list 

104 
val del_rules: thm list > thm list > thm list 

105 
val merge_rules: thm list * thm list > thm list 

106 
val norm_hhf_eq: thm 

107 
val triv_goal: thm 

108 
val rev_triv_goal: thm 

11815  109 
val implies_intr_goals: cterm list > thm > thm 
11975  110 
val freeze_all: thm > thm 
111 
val mk_triv_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 

118 
val tvars_intr_list: string list > thm > thm 

119 
val conj_intr: thm > thm > thm 

120 
val conj_intr_list: thm list > thm 

121 
val conj_elim: thm > thm * thm 

122 
val conj_elim_list: thm > thm list 

3766  123 
end; 
0  124 

5903  125 
structure Drule: DRULE = 
0  126 
struct 
127 

3991  128 

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

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

130 

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

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

132 

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

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

134 
fun dest_implies ct = 
8328  135 
case term_of ct of 
136 
(Const("==>", _) $ _ $ _) => 

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

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

138 
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

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

140 

10414  141 
fun dest_equals ct = 
142 
case term_of ct of 

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

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

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

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

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

148 

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

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

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

151 
case term_of ct of 
8328  152 
(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) => 
153 
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

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

155 

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

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

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

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

159 
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

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

161 

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

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

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

165 
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

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

167 

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

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

169 
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

170 

9547  171 
val proto_sign = Theory.sign_of ProtoPure.thy; 
172 

173 
val implies = cterm_of proto_sign Term.implies; 

174 

175 
(*cterm version of mk_implies*) 

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

176 
fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B; 
9547  177 

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

179 
fun list_implies([], B) = B 

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

181 

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

182 

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

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

184 

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

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

186 
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

187 

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

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

189 
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

190 

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

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

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

196 
 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

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

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

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

200 
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

201 
val T = Sign.read_typ (sign,sorts) st; 
10403  202 
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

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

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

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

206 
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

207 
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

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

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

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

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

212 
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

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

214 
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

215 
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

216 
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

217 
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

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

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

220 

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

221 

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

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

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

226 
***) 

227 

228 
fun types_sorts thm = 

229 
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

230 
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

231 
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

232 
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

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

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

235 
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

236 
fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); 
0  237 
in (typ,sort) end; 
238 

7636  239 

9455  240 

241 
(** basic attributes **) 

242 

243 
(* dependent rules *) 

244 

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

246 

247 

248 
(* add / delete tags *) 

249 

250 
fun map_tags f thm = 

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

252 

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

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

255 

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

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

258 

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

260 

11741  261 

262 
(* theorem kinds *) 

263 

264 
val theoremK = "theorem"; 

265 
val lemmaK = "lemma"; 

266 
val corollaryK = "corollary"; 

267 
val internalK = "internal"; 

9455  268 

11741  269 
fun get_kind thm = 
270 
(case Library.assoc (#2 (Thm.get_name_tags thm), "kind") of 

271 
Some (k :: _) => k 

272 
 _ => "unknown"); 

273 

274 
fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind"; 

275 
fun kind k x = rule_attribute (K (kind_rule k)) x; 

276 
fun kind_internal x = kind internalK x; 

277 
fun has_internal tags = exists (equal internalK o fst) tags; 

9455  278 

279 

280 

0  281 
(** Standardization of rules **) 
282 

7636  283 
(*Strip extraneous shyps as far as possible*) 
284 
fun strip_shyps_warning thm = 

285 
let 

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

287 
val thm' = Thm.strip_shyps thm; 

288 
val xshyps = Thm.extra_shyps thm'; 

289 
in 

290 
if null xshyps then () 

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

292 
thm' 

293 
end; 

294 

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

297 
 forall_intr_list (y::ys) th = 

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

298 
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

299 
in forall_intr y gth handle THM _ => gth end; 
0  300 

301 
(*Generalization over all suitable Free variables*) 

302 
fun forall_intr_frees th = 

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

304 
in forall_intr_list 

4440  305 
(map (cterm_of sign) (sort (make_ord atless) (term_frees prop))) 
0  306 
th 
307 
end; 

308 

7898  309 
val forall_elim_var = PureThy.forall_elim_var; 
310 
val forall_elim_vars = PureThy.forall_elim_vars; 

0  311 

9554  312 
fun forall_elim_vars_safe th = 
313 
forall_elim_vars_safe (forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th) 

314 
handle THM _ => th; 

315 

316 

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

319 

11815  320 
(* maps A1,...,An  B to [ A1;...;An ] ==> B *) 
0  321 
fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th); 
322 

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

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

325 

11960  326 
(* maps  B to A1,...,An  B *) 
327 
fun impose_hyps chyps th = 

328 
implies_elim_list (implies_intr_list chyps th) (map Thm.assume chyps); 

329 

0  330 
(*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

331 
fun zero_var_indexes th = 
0  332 
let val {prop,sign,...} = rep_thm th; 
333 
val vars = term_vars prop 

334 
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

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

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

339 
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

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

341 
 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

342 
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

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

344 
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

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

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

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

349 

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

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

10515  352 

353 
fun close_derivation thm = 

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

355 
else thm; 

356 

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

357 
fun standard' th = 
10515  358 
let val {maxidx,...} = rep_thm th in 
359 
th 

360 
> implies_intr_hyps 

361 
> forall_intr_frees > forall_elim_vars (maxidx + 1) 

362 
> strip_shyps_warning 

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

363 
> zero_var_indexes > Thm.varifyT > Thm.compress 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

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

365 

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

366 
val standard = close_derivation o standard'; 
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

367 

0  368 

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

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

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

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

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

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

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

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

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

378 
 vars => 
8328  379 
let fun newName (Var(ix,_), (pairs,used)) = 
380 
let val v = variant used (string_of_indexname ix) 

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

382 
val (alist, _) = foldr newName 

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

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

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

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

387 
val insts = map mk_inst vars 

388 
fun thaw th' = 

389 
th' > forall_intr_list (map #2 insts) 

390 
> forall_elim_list (map #1 insts) 

391 
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

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

393 

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

394 

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

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

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

397 

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

400 
Any remaining trailing positions are left unchanged. *) 

401 
val rearrange_prems = let 

402 
fun rearr new [] thm = thm 

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

406 
in rearr 0 end; 

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

407 

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

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

411 
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

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

415 
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

416 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  417 

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

418 
(*Resolution: exactly one resolvent must be produced.*) 
0  419 
fun tha RSN (i,thb) = 
4270  420 
case Seq.chop (2, biresolution false [(false,tha)] i thb) of 
0  421 
([th],_) => th 
422 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

424 

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

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

427 

428 
(*For joining lists of rules*) 

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

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

432 
in List.concat (map resb thbs) end; 
0  433 

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

435 

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

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

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

438 
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

439 
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

440 
 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

441 
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

442 

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

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

444 
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

445 
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

446 
 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

447 
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

448 

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

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

450 
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

451 

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

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

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

455 
fun compose(tha,i,thb) = 
4270  456 
Seq.list_of (bicompose false (false,tha,0) i thb); 
0  457 

6946  458 
fun compose_single (tha,i,thb) = 
459 
(case compose (tha,i,thb) of 

460 
[th] => th 

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

462 

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

465 
case compose(tha,1,thb) of 

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

466 
[th] => th 
0  467 
 _ => raise THM("COMP", 1, [tha,thb]); 
468 

4016  469 
(** theorem equality **) 
0  470 

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

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

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

475 
val size_of_thm = size_of_term o #prop o rep_thm; 

476 

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

9862  479 
fun add_rules rs rules = rs @ del_rules rs rules; 
9829  480 
fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2; 
481 

0  482 

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

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

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

485 

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

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

487 
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

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

489 
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

490 
 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

491 
 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

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

493 

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

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

495 
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

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

497 
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

498 

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

500 
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

501 

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

502 

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

503 

0  504 
(*** MetaRewriting Rules ***) 
505 

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

506 
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

507 

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

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

510 
fun open_store_thm name thm = hd (PureThy.open_smart_store_thms (name, [thm])); 
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

511 
fun open_store_standard_thm name thm = open_store_thm name (standard' thm); 
4016  512 

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

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

517 
val symmetric_thm = 

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

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

521 
val transitive_thm = 

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

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

523 
val yz = read_prop "y::'a::logic == z" 
0  524 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
9455  525 
in store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 
0  526 

4679  527 
fun symmetric_fun thm = thm RS symmetric_thm; 
528 

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

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

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

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

532 
in equal_elim (eta_conversion (cprop_of eq')) eq' end; 
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

533 

10414  534 
val imp_cong = 
535 
let 

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

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

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

539 
val A = read_prop "PROP A" 

540 
in 

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

541 
open_store_standard_thm "imp_cong" (implies_intr ABC (equal_intr 
10414  542 
(implies_intr AB (implies_intr A 
543 
(equal_elim (implies_elim (assume ABC) (assume A)) 

544 
(implies_elim (assume AB) (assume A))))) 

545 
(implies_intr AC (implies_intr A 

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

547 
(implies_elim (assume AC) (assume A))))))) 

548 
end; 

549 

550 
val swap_prems_eq = 

551 
let 

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

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

554 
val A = read_prop "PROP A" 

555 
val B = read_prop "PROP B" 

556 
in 

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

557 
open_store_standard_thm "swap_prems_eq" (equal_intr 
10414  558 
(implies_intr ABC (implies_intr B (implies_intr A 
559 
(implies_elim (implies_elim (assume ABC) (assume A)) (assume B))))) 

560 
(implies_intr BAC (implies_intr A (implies_intr B 

561 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

562 
end; 

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

563 

9547  564 
val refl_implies = reflexive implies; 
0  565 

566 

567 
(*** Some useful metatheorems ***) 

568 

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

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

570 
val asm_rl = open_store_standard_thm "asm_rl" (Thm.trivial (read_prop "PROP ?psi")); 
7380  571 
val _ = store_thm "_" asm_rl; 
0  572 

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

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

575 
open_store_standard_thm "cut_rl" 
9455  576 
(Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta")); 
0  577 

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

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

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

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

582 
and VW = read_prop "PROP V ==> PROP W"; 
4016  583 
in 
11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

584 
open_store_standard_thm "revcut_rl" 
4016  585 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  586 
end; 
587 

668  588 
(*for deleting an unwanted assumption*) 
589 
val thin_rl = 

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

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

591 
and W = read_prop "PROP W"; 
11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

592 
in open_store_standard_thm "thin_rl" (implies_intr V (implies_intr W (assume W))) 
668  593 
end; 
594 

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

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

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

598 
and QV = read_prop "!!x::'a. PROP V" 
8086  599 
and x = read_cterm proto_sign ("x", TypeInfer.logicT); 
4016  600 
in 
11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

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

602 
(equal_intr (implies_intr QV (forall_elim x (assume QV))) 
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

603 
(implies_intr V (forall_intr x (assume V)))) 
0  604 
end; 
605 

1756  606 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
607 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

609 
*) 

610 
val swap_prems_rl = 

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

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

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

615 
val cminor2 = read_prop "PROP PhiB"; 
1756  616 
val minor2 = assume cminor2; 
11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

617 
in open_store_standard_thm "swap_prems_rl" 
1756  618 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
619 
(implies_elim (implies_elim major minor1) minor2)))) 

620 
end; 

621 

3653  622 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
623 
==> PROP ?phi == PROP ?psi 

8328  624 
Introduction rule for == as a metatheorem. 
3653  625 
*) 
626 
val equal_intr_rule = 

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

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

628 
and QP = read_prop "PROP psi ==> PROP phi" 
4016  629 
in 
11512
da3a96ab5630
Some basic rules are now stored with "open" derivations, to facilitate
berghofe
parents:
11163
diff
changeset

630 
open_store_standard_thm "equal_intr_rule" 
4016  631 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  632 
end; 
633 

4285  634 

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

637 
*) 

638 

639 
val norm_hhf_eq = 

640 
let 

641 
val cert = Thm.cterm_of proto_sign; 

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

643 
val all = Term.all aT; 

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

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

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

647 

648 
val cx = cert x; 

649 
val cphi = cert phi; 

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

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

652 
in 

653 
Thm.equal_intr 

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

655 
> Thm.forall_elim cx 

656 
> Thm.implies_intr cphi 

657 
> Thm.forall_intr cx 

658 
> Thm.implies_intr lhs) 

659 
(Thm.implies_elim 

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

661 
> Thm.forall_intr cx 

662 
> Thm.implies_intr cphi 

663 
> Thm.implies_intr rhs) 

11997
402ae1a172ae
norm_hhf_eq is now stored using open_store_standard_thm.
berghofe
parents:
11975
diff
changeset

664 
> open_store_standard_thm "norm_hhf_eq" 
9554  665 
end; 
666 

667 

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

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

669 

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

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

671 
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

672 

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

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

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

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

676 
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

677 

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

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

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

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

681 

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

682 

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

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

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

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

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

687 
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

688 
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

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

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

691 
val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U) 
10403  692 
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

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

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

695 
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

696 
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

697 
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

698 
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

699 
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

700 
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

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

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

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

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

705 

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 
(** Derived rules mainly for METAHYPS **) 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8086
diff
changeset

708 

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

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

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

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

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

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

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

715 
val cterm = cterm_of (Sign.merge (sign,signa)) 
10414  716 
in transitive (symmetric (beta_conversion false (cterm (abst$a)))) 
717 
(transitive combth (beta_conversion false (cterm (absu$a)))) 

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

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

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

720 

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

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

722 
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

723 

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

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

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

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

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

728 
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

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

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

731 
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

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

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

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

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

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

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

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

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

740 

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

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

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

743 
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

744 

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

745 

10667  746 
(*** Goal (PROP A) <==> PROP A ***) 
4789  747 

748 
local 

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

751 
val G = Logic.mk_goal A; 

4789  752 
val (G_def, _) = freeze_thaw ProtoPure.Goal_def; 
753 
in 

11741  754 
val triv_goal = store_thm "triv_goal" (kind_rule internalK (standard 
10667  755 
(Thm.equal_elim (Thm.symmetric G_def) (Thm.assume (cert A))))); 
11741  756 
val rev_triv_goal = store_thm "rev_triv_goal" (kind_rule internalK (standard 
10667  757 
(Thm.equal_elim G_def (Thm.assume (cert G))))); 
4789  758 
end; 
759 

9460  760 
val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const); 
6995  761 
fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal; 
762 

11815  763 
fun implies_intr_goals cprops thm = 
764 
implies_elim_list (implies_intr_list cprops thm) (map assume_goal cprops) 

765 
> implies_intr_list (map mk_cgoal cprops); 

766 

4789  767 

4285  768 

5688  769 
(** variations on instantiate **) 
4285  770 

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

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

772 
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

773 

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

774 

4285  775 
(* collect vars *) 
776 

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

778 
val add_tvars = foldl_types add_tvarsT; 

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

780 

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

783 

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

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

4285  786 

787 

788 
(* instantiate by lefttoright occurrence of variables *) 

789 

790 
fun instantiate' cTs cts thm = 

791 
let 

792 
fun err msg = 

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

794 
mapfilter (apsome Thm.typ_of) cTs, 

795 
mapfilter (apsome Thm.term_of) cts); 

796 

797 
fun inst_of (v, ct) = 

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

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

800 

801 
fun zip_vars _ [] = [] 

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

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

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

805 

806 
(*instantiate types first!*) 

807 
val thm' = 

808 
if forall is_none cTs then thm 

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

810 
in 

811 
if forall is_none cts then thm' 

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

813 
end; 

814 

815 

5688  816 
(* unvarify(T) *) 
817 

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

819 

820 
fun unvarifyT thm = 

821 
let 

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

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

824 
in instantiate' tfrees [] thm end; 

825 

826 
fun unvarify raw_thm = 

827 
let 

828 
val thm = unvarifyT raw_thm; 

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

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

831 
in instantiate' [] frees thm end; 

832 

833 

8605  834 
(* tvars_intr_list *) 
835 

836 
fun tfrees_of thm = 

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

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

839 

840 
fun tvars_intr_list tfrees thm = 

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

842 

843 

6435  844 
(* increment var indexes *) 
845 

846 
fun incr_indexes_wrt is cTs cts thms = 

847 
let 

848 
val maxidx = 

849 
foldl Int.max (~1, is @ 

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

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

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

10414  853 
in Thm.incr_indexes (maxidx + 1) end; 
6435  854 

855 

8328  856 
(* freeze_all *) 
857 

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

859 

860 
fun freeze_all_TVars thm = 

861 
(case tvars_of thm of 

862 
[] => thm 

863 
 tvars => 

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

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

866 

867 
fun freeze_all_Vars thm = 

868 
(case vars_of thm of 

869 
[] => thm 

870 
 vars => 

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

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

873 

874 
val freeze_all = freeze_all_Vars o freeze_all_TVars; 

875 

876 

5688  877 
(* mk_triv_goal *) 
878 

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

880 
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

881 

11975  882 

883 

884 
(** metalevel conjunction **) 

885 

886 
local 

887 
val A = read_prop "PROP A"; 

888 
val B = read_prop "PROP B"; 

889 
val C = read_prop "PROP C"; 

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

891 

892 
val proj1 = 

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

894 
> forall_elim_vars 0; 

895 

896 
val proj2 = 

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

898 
> forall_elim_vars 0; 

899 

900 
val conj_intr_rule = 

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

902 
(Thm.forall_intr C (Thm.implies_intr ABC 

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

904 
> forall_elim_vars 0; 

905 

906 
val incr = incr_indexes_wrt [] [] []; 

907 
in 

908 

909 
fun conj_intr tha thb = thb COMP (tha COMP incr [tha, thb] conj_intr_rule); 

910 
val conj_intr_list = foldr1 (uncurry conj_intr); 

911 

912 
fun conj_elim th = 

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

914 
in (incr [th'] proj1 COMP th', incr [th'] proj2 COMP th') end; 

915 

916 
fun conj_elim_list th = 

917 
let val (th1, th2) = conj_elim th 

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

919 

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

921 

11975  922 
end; 
5903  923 

924 
structure BasicDrule: BASIC_DRULE = Drule; 

925 
open BasicDrule; 