author  wenzelm 
Fri, 14 Dec 2001 11:51:01 +0100  
changeset 12495  89f97fa683f5 
parent 12373  704e50ab65af 
child 12527  d6c91bc3e49c 
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 

12005  102 
val local_standard: thm > thm 
11975  103 
val compose_single: thm * int * thm > thm 
12373  104 
val add_rule: thm > thm list > thm list 
105 
val del_rule: thm > thm list > thm list 

11975  106 
val add_rules: thm list > thm list > thm list 
107 
val del_rules: thm list > thm list > thm list 

108 
val merge_rules: thm list * thm list > thm list 

109 
val norm_hhf_eq: thm 

110 
val triv_goal: thm 

111 
val rev_triv_goal: thm 

11815  112 
val implies_intr_goals: cterm list > thm > thm 
11975  113 
val freeze_all: thm > thm 
114 
val mk_triv_goal: cterm > thm 

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

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

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

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

119 
val unvarifyT: thm > thm 

120 
val unvarify: thm > thm 

12495  121 
val tvars_intr_list: string list > thm > thm * (string * indexname) list 
12297  122 
val remdups_rl: thm 
11975  123 
val conj_intr: thm > thm > thm 
124 
val conj_intr_list: thm list > thm 

125 
val conj_elim: thm > thm * thm 

126 
val conj_elim_list: thm > thm list 

12135  127 
val conj_elim_precise: int > thm > thm list 
128 
val conj_intr_thm: thm 

3766  129 
end; 
0  130 

5903  131 
structure Drule: DRULE = 
0  132 
struct 
133 

3991  134 

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

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

136 

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

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

138 

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

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

140 
fun dest_implies ct = 
8328  141 
case term_of ct of 
142 
(Const("==>", _) $ _ $ _) => 

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

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

144 
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

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

146 

10414  147 
fun dest_equals ct = 
148 
case term_of ct of 

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

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

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

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

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

154 

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

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

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

157 
case term_of ct of 
8328  158 
(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) => 
159 
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

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

161 

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

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

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

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

165 
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

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

167 

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

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

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

171 
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

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

173 

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

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

175 
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

176 

9547  177 
val proto_sign = Theory.sign_of ProtoPure.thy; 
178 

179 
val implies = cterm_of proto_sign Term.implies; 

180 

181 
(*cterm version of mk_implies*) 

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

182 
fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B; 
9547  183 

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

185 
fun list_implies([], B) = B 

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

187 

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

188 

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

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

190 

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

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

192 
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

193 

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

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

195 
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

196 

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

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

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

202 
 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

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

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

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

206 
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

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

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

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

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

212 
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

213 
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

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

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

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

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

218 
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

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

220 
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

221 
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

222 
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

223 
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

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

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

226 

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

227 

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

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

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

232 
***) 

233 

234 
fun types_sorts thm = 

235 
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

236 
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

237 
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

238 
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

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

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

241 
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

242 
fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); 
0  243 
in (typ,sort) end; 
244 

7636  245 

9455  246 

247 
(** basic attributes **) 

248 

249 
(* dependent rules *) 

250 

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

252 

253 

254 
(* add / delete tags *) 

255 

256 
fun map_tags f thm = 

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

258 

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

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

261 

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

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

264 

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

266 

11741  267 

268 
(* theorem kinds *) 

269 

270 
val theoremK = "theorem"; 

271 
val lemmaK = "lemma"; 

272 
val corollaryK = "corollary"; 

273 
val internalK = "internal"; 

9455  274 

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

277 
Some (k :: _) => k 

278 
 _ => "unknown"); 

279 

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

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

282 
fun kind_internal x = kind internalK x; 

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

9455  284 

285 

286 

0  287 
(** Standardization of rules **) 
288 

7636  289 
(*Strip extraneous shyps as far as possible*) 
290 
fun strip_shyps_warning thm = 

291 
let 

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

293 
val thm' = Thm.strip_shyps thm; 

294 
val xshyps = Thm.extra_shyps thm'; 

295 
in 

296 
if null xshyps then () 

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

298 
thm' 

299 
end; 

300 

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

303 
 forall_intr_list (y::ys) th = 

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

304 
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

305 
in forall_intr y gth handle THM _ => gth end; 
0  306 

307 
(*Generalization over all suitable Free variables*) 

308 
fun forall_intr_frees th = 

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

310 
in forall_intr_list 

4440  311 
(map (cterm_of sign) (sort (make_ord atless) (term_frees prop))) 
0  312 
th 
313 
end; 

314 

7898  315 
val forall_elim_var = PureThy.forall_elim_var; 
316 
val forall_elim_vars = PureThy.forall_elim_vars; 

0  317 

9554  318 
fun forall_elim_vars_safe th = 
319 
forall_elim_vars_safe (forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th) 

320 
handle THM _ => th; 

321 

322 

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

325 

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

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

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

331 

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

12092  334 
let val chyps' = gen_rems (op aconv o apfst Thm.term_of) (chyps, #hyps (Thm.rep_thm th)) 
335 
in implies_elim_list (implies_intr_list chyps' th) (map Thm.assume chyps') end; 

11960  336 

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

338 
fun zero_var_indexes th = 
0  339 
let val {prop,sign,...} = rep_thm th; 
340 
val vars = term_vars prop 

341 
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

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

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

346 
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

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

348 
 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

349 
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

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

351 
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

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

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

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

356 

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

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

10515  359 

360 
fun close_derivation thm = 

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

362 
else thm; 

363 

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

364 
fun standard' th = 
10515  365 
let val {maxidx,...} = rep_thm th in 
366 
th 

367 
> implies_intr_hyps 

368 
> forall_intr_frees > forall_elim_vars (maxidx + 1) 

369 
> strip_shyps_warning 

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

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

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

372 

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

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

374 

12005  375 
fun local_standard th = 
12221
cc31140bba16
local_standard: plain strip_shyps instead of strip_shyps_warning;
wenzelm
parents:
12135
diff
changeset

376 
th > strip_shyps > zero_var_indexes 
12005  377 
> Thm.compress > close_derivation; 
378 

0  379 

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

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

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

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

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

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

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

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

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

389 
 vars => 
8328  390 
let fun newName (Var(ix,_), (pairs,used)) = 
391 
let val v = variant used (string_of_indexname ix) 

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

393 
val (alist, _) = foldr newName 

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

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

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

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

398 
val insts = map mk_inst vars 

399 
fun thaw th' = 

400 
th' > forall_intr_list (map #2 insts) 

401 
> forall_elim_list (map #1 insts) 

402 
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

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

404 

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

405 

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

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

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

408 

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

411 
Any remaining trailing positions are left unchanged. *) 

412 
val rearrange_prems = let 

413 
fun rearr new [] thm = thm 

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

417 
in rearr 0 end; 

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

418 

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

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

422 
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

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

426 
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

427 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  428 

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

429 
(*Resolution: exactly one resolvent must be produced.*) 
0  430 
fun tha RSN (i,thb) = 
4270  431 
case Seq.chop (2, biresolution false [(false,tha)] i thb) of 
0  432 
([th],_) => th 
433 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

435 

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

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

438 

439 
(*For joining lists of rules*) 

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

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

443 
in List.concat (map resb thbs) end; 
0  444 

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

446 

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

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

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

449 
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

450 
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

451 
 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

452 
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

453 

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

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

455 
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

456 
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

457 
 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

458 
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

459 

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

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

461 
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

462 

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

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

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

466 
fun compose(tha,i,thb) = 
4270  467 
Seq.list_of (bicompose false (false,tha,0) i thb); 
0  468 

6946  469 
fun compose_single (tha,i,thb) = 
470 
(case compose (tha,i,thb) of 

471 
[th] => th 

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

473 

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

476 
case compose(tha,1,thb) of 

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

477 
[th] => th 
0  478 
 _ => raise THM("COMP", 1, [tha,thb]); 
479 

4016  480 
(** theorem equality **) 
0  481 

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

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

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

486 
val size_of_thm = size_of_term o #prop o rep_thm; 

487 

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

9862  490 
fun add_rules rs rules = rs @ del_rules rs rules; 
12373  491 
val del_rule = del_rules o single; 
492 
val add_rule = add_rules o single; 

12283  493 
fun merge_rules (rules1, rules2) = gen_merge_lists' Thm.eq_thm rules1 rules2; 
9829  494 

0  495 

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

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

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

498 

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

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

500 
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

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

502 
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

503 
 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

504 
 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

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

506 

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

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

508 
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

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

510 
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

511 

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

513 
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

514 

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

515 

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

516 

0  517 
(*** MetaRewriting Rules ***) 
518 

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

519 
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

520 

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

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

4016  525 

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

527 
let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS))) 
12135  528 
in store_standard_thm_open "reflexive" (Thm.reflexive cx) end; 
0  529 

530 
val symmetric_thm = 

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

531 
let val xy = read_prop "x::'a::logic == y" 
12135  532 
in store_standard_thm_open "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end; 
0  533 

534 
val transitive_thm = 

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

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

536 
val yz = read_prop "y::'a::logic == z" 
0  537 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
12135  538 
in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 
0  539 

4679  540 
fun symmetric_fun thm = thm RS symmetric_thm; 
541 

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

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

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

544 
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

545 
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

546 

10414  547 
val imp_cong = 
548 
let 

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

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

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

552 
val A = read_prop "PROP A" 

553 
in 

12135  554 
store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr 
10414  555 
(implies_intr AB (implies_intr A 
556 
(equal_elim (implies_elim (assume ABC) (assume A)) 

557 
(implies_elim (assume AB) (assume A))))) 

558 
(implies_intr AC (implies_intr A 

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

560 
(implies_elim (assume AC) (assume A))))))) 

561 
end; 

562 

563 
val swap_prems_eq = 

564 
let 

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

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

567 
val A = read_prop "PROP A" 

568 
val B = read_prop "PROP B" 

569 
in 

12135  570 
store_standard_thm_open "swap_prems_eq" (equal_intr 
10414  571 
(implies_intr ABC (implies_intr B (implies_intr A 
572 
(implies_elim (implies_elim (assume ABC) (assume A)) (assume B))))) 

573 
(implies_intr BAC (implies_intr A (implies_intr B 

574 
(implies_elim (implies_elim (assume BAC) (assume B)) (assume A)))))) 

575 
end; 

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

576 

9547  577 
val refl_implies = reflexive implies; 
0  578 

579 

580 
(*** Some useful metatheorems ***) 

581 

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

12135  583 
val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi")); 
7380  584 
val _ = store_thm "_" asm_rl; 
0  585 

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

4016  587 
val cut_rl = 
12135  588 
store_standard_thm_open "cut_rl" 
9455  589 
(Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta")); 
0  590 

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

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

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

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

595 
and VW = read_prop "PROP V ==> PROP W"; 
4016  596 
in 
12135  597 
store_standard_thm_open "revcut_rl" 
4016  598 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 
0  599 
end; 
600 

668  601 
(*for deleting an unwanted assumption*) 
602 
val thin_rl = 

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

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

604 
and W = read_prop "PROP W"; 
12135  605 
in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end; 
668  606 

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

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

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

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

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

615 
(implies_intr V (forall_intr x (assume V)))) 
0  616 
end; 
617 

1756  618 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
619 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

621 
*) 

622 
val swap_prems_rl = 

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

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

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

627 
val cminor2 = read_prop "PROP PhiB"; 
1756  628 
val minor2 = assume cminor2; 
12135  629 
in store_standard_thm_open "swap_prems_rl" 
1756  630 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
631 
(implies_elim (implies_elim major minor1) minor2)))) 

632 
end; 

633 

3653  634 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
635 
==> PROP ?phi == PROP ?psi 

8328  636 
Introduction rule for == as a metatheorem. 
3653  637 
*) 
638 
val equal_intr_rule = 

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

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

640 
and QP = read_prop "PROP psi ==> PROP phi" 
4016  641 
in 
12135  642 
store_standard_thm_open "equal_intr_rule" 
4016  643 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 
3653  644 
end; 
645 

4285  646 

12297  647 
(* "[ PROP ?phi; PROP ?phi; PROP ?psi ] ==> PROP ?psi" *) 
648 

649 
val remdups_rl = 

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

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

652 

653 

9554  654 
(*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) 
12297  655 
Rewrite rule for HHF normalization.*) 
9554  656 

657 
val norm_hhf_eq = 

658 
let 

659 
val cert = Thm.cterm_of proto_sign; 

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

661 
val all = Term.all aT; 

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

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

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

665 

666 
val cx = cert x; 

667 
val cphi = cert phi; 

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

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

670 
in 

671 
Thm.equal_intr 

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

673 
> Thm.forall_elim cx 

674 
> Thm.implies_intr cphi 

675 
> Thm.forall_intr cx 

676 
> Thm.implies_intr lhs) 

677 
(Thm.implies_elim 

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

679 
> Thm.forall_intr cx 

680 
> Thm.implies_intr cphi 

681 
> Thm.implies_intr rhs) 

12135  682 
> store_standard_thm_open "norm_hhf_eq" 
9554  683 
end; 
684 

685 

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

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

687 

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

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

689 
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

690 

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

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

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

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

694 
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

695 

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

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

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

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

699 

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

700 

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

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

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

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

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

705 
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

706 
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

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

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

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

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

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

713 
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

714 
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

715 
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

716 
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

717 
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

718 
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

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

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

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

722 
end; 
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 

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

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

726 

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

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

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

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

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

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

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

733 
val cterm = cterm_of (Sign.merge (sign,signa)) 
10414  734 
in transitive (symmetric (beta_conversion false (cterm (abst$a)))) 
735 
(transitive combth (beta_conversion false (cterm (absu$a)))) 

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

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

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

738 

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

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

740 
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

741 

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

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

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

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

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

746 
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

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

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

749 
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

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

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

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

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

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

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

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

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

758 

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

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

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

761 
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

762 

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

763 

10667  764 
(*** Goal (PROP A) <==> PROP A ***) 
4789  765 

766 
local 

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

769 
val G = Logic.mk_goal A; 

4789  770 
val (G_def, _) = freeze_thaw ProtoPure.Goal_def; 
771 
in 

11741  772 
val triv_goal = store_thm "triv_goal" (kind_rule internalK (standard 
10667  773 
(Thm.equal_elim (Thm.symmetric G_def) (Thm.assume (cert A))))); 
11741  774 
val rev_triv_goal = store_thm "rev_triv_goal" (kind_rule internalK (standard 
10667  775 
(Thm.equal_elim G_def (Thm.assume (cert G))))); 
4789  776 
end; 
777 

9460  778 
val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const); 
6995  779 
fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal; 
780 

11815  781 
fun implies_intr_goals cprops thm = 
782 
implies_elim_list (implies_intr_list cprops thm) (map assume_goal cprops) 

783 
> implies_intr_list (map mk_cgoal cprops); 

784 

4789  785 

4285  786 

5688  787 
(** variations on instantiate **) 
4285  788 

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

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

790 
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

791 

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

792 

12495  793 
(* collect vars in lefttoright order *) 
4285  794 

12495  795 
fun tvars_of_terms ts = rev (foldl Term.add_tvars ([], ts)); 
796 
fun vars_of_terms ts = rev (foldl Term.add_vars ([], ts)); 

5903  797 

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

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

4285  800 

801 

802 
(* instantiate by lefttoright occurrence of variables *) 

803 

804 
fun instantiate' cTs cts thm = 

805 
let 

806 
fun err msg = 

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

808 
mapfilter (apsome Thm.typ_of) cTs, 

809 
mapfilter (apsome Thm.term_of) cts); 

810 

811 
fun inst_of (v, ct) = 

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

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

814 

815 
fun zip_vars _ [] = [] 

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

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

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

819 

820 
(*instantiate types first!*) 

821 
val thm' = 

822 
if forall is_none cTs then thm 

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

824 
in 

825 
if forall is_none cts then thm' 

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

827 
end; 

828 

829 

5688  830 
(* unvarify(T) *) 
831 

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

833 

834 
fun unvarifyT thm = 

835 
let 

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

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

838 
in instantiate' tfrees [] thm end; 

839 

840 
fun unvarify raw_thm = 

841 
let 

842 
val thm = unvarifyT raw_thm; 

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

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

845 
in instantiate' [] frees thm end; 

846 

847 

8605  848 
(* tvars_intr_list *) 
849 

850 
fun tfrees_of thm = 

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

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

853 

854 
fun tvars_intr_list tfrees thm = 

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

856 

857 

6435  858 
(* increment var indexes *) 
859 

860 
fun incr_indexes_wrt is cTs cts thms = 

861 
let 

862 
val maxidx = 

863 
foldl Int.max (~1, is @ 

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

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

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

10414  867 
in Thm.incr_indexes (maxidx + 1) end; 
6435  868 

869 

8328  870 
(* freeze_all *) 
871 

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

873 

874 
fun freeze_all_TVars thm = 

875 
(case tvars_of thm of 

876 
[] => thm 

877 
 tvars => 

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

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

880 

881 
fun freeze_all_Vars thm = 

882 
(case vars_of thm of 

883 
[] => thm 

884 
 vars => 

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

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

887 

888 
val freeze_all = freeze_all_Vars o freeze_all_TVars; 

889 

890 

5688  891 
(* mk_triv_goal *) 
892 

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

894 
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

895 

11975  896 

897 

898 
(** metalevel conjunction **) 

899 

900 
local 

901 
val A = read_prop "PROP A"; 

902 
val B = read_prop "PROP B"; 

903 
val C = read_prop "PROP C"; 

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

905 

906 
val proj1 = 

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

908 
> forall_elim_vars 0; 

909 

910 
val proj2 = 

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

912 
> forall_elim_vars 0; 

913 

914 
val conj_intr_rule = 

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

916 
(Thm.forall_intr C (Thm.implies_intr ABC 

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

918 
> forall_elim_vars 0; 

919 

920 
val incr = incr_indexes_wrt [] [] []; 

921 
in 

922 

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

924 
val conj_intr_list = foldr1 (uncurry conj_intr); 

925 

926 
fun conj_elim th = 

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

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

929 

930 
fun conj_elim_list th = 

931 
let val (th1, th2) = conj_elim th 

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

933 

12135  934 
fun conj_elim_precise 1 th = [th] 
935 
 conj_elim_precise n th = 

936 
let val (th1, th2) = conj_elim th 

937 
in th1 :: conj_elim_precise (n  1) th2 end; 

938 

939 
val conj_intr_thm = store_standard_thm_open "conjunctionI" 

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

941 

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

943 

11975  944 
end; 
5903  945 

946 
structure BasicDrule: BASIC_DRULE = Drule; 

947 
open BasicDrule; 