author  wenzelm 
Tue, 13 Jul 1999 13:53:34 +0200  
changeset 6995  d824a86266a9 
parent 6946  309276732ee1 
child 7248  322151fe6f02 
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 

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

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

5903  11 
signature BASIC_DRULE = 
3766  12 
sig 
4285  13 
val dest_implies : cterm > cterm * cterm 
14 
val skip_flexpairs : cterm > cterm 

15 
val strip_imp_prems : cterm > cterm list 

1460  16 
val cprems_of : thm > cterm list 
4285  17 
val read_insts : 
18 
Sign.sg > (indexname > typ option) * (indexname > sort option) 

19 
> (indexname > typ option) * (indexname > sort option) 

20 
> string list > (string*string)list 

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

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

1460  23 
val forall_intr_list : cterm list > thm > thm 
24 
val forall_intr_frees : thm > thm 

25 
val forall_intr_vars : thm > thm 

26 
val forall_elim_list : cterm list > thm > thm 

27 
val forall_elim_var : int > thm > thm 

28 
val forall_elim_vars : int > thm > thm 

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

29 
val freeze_thaw : thm > thm * (thm > thm) 
1460  30 
val implies_elim_list : thm > thm list > thm 
31 
val implies_intr_list : cterm list > thm > thm 

4285  32 
val zero_var_indexes : thm > thm 
33 
val standard : thm > thm 

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

34 
val rotate_prems : int > thm > thm 
4285  35 
val assume_ax : theory > string > thm 
36 
val RSN : thm * (int * thm) > thm 

37 
val RS : thm * thm > thm 

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

39 
val RL : thm list * thm list > thm list 

40 
val MRS : thm list * thm > thm 

1460  41 
val MRL : thm list list * thm list > thm list 
4285  42 
val compose : thm * int * thm > thm list 
43 
val COMP : thm * thm > thm 

0  44 
val read_instantiate_sg: Sign.sg > (string*string)list > thm > thm 
4285  45 
val read_instantiate : (string*string)list > thm > thm 
46 
val cterm_instantiate : (cterm*cterm)list > thm > thm 

47 
val weak_eq_thm : thm * thm > bool 

48 
val eq_thm_sg : thm * thm > bool 

49 
val size_of_thm : thm > int 

1460  50 
val reflexive_thm : thm 
4285  51 
val symmetric_thm : thm 
52 
val transitive_thm : thm 

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

53 
val refl_implies : thm 
4679  54 
val symmetric_fun : thm > thm 
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

55 
val rewrite_rule_aux : (meta_simpset > thm > thm option) > thm list > thm > thm 
4713  56 
val rewrite_thm : bool * bool * bool 
57 
> (meta_simpset > thm > thm option) 

58 
> meta_simpset > thm > thm 

5079  59 
val rewrite_cterm : bool * bool * bool 
60 
> (meta_simpset > thm > thm option) 

61 
> meta_simpset > cterm > thm 

4285  62 
val rewrite_goals_rule_aux: (meta_simpset > thm > thm option) > thm list > thm > thm 
4713  63 
val rewrite_goal_rule : bool* bool * bool 
64 
> (meta_simpset > thm > thm option) 

65 
> meta_simpset > int > thm > thm 

4285  66 
val equal_abs_elim : cterm > thm > thm 
67 
val equal_abs_elim_list: cterm list > thm > thm 

68 
val flexpair_abs_elim_list: cterm list > thm > thm 

69 
val asm_rl : thm 

70 
val cut_rl : thm 

71 
val revcut_rl : thm 

72 
val thin_rl : thm 

73 
val triv_forall_equality: thm 

1756  74 
val swap_prems_rl : thm 
4285  75 
val equal_intr_rule : thm 
5903  76 
val instantiate' : ctyp option list > cterm option list > thm > thm 
6435  77 
val incr_indexes : int > thm > thm 
78 
val incr_indexes_wrt : int list > ctyp list > cterm list > thm list > thm > thm 

5903  79 
end; 
80 

81 
signature DRULE = 

82 
sig 

83 
include BASIC_DRULE 

6946  84 
val compose_single : thm * int * thm > thm 
5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5079
diff
changeset

85 
val triv_goal : thm 
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5079
diff
changeset

86 
val rev_triv_goal : thm 
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5079
diff
changeset

87 
val mk_triv_goal : cterm > thm 
6995  88 
val mk_cgoal : cterm > cterm 
89 
val assume_goal : cterm > thm 

5903  90 
val tvars_of_terms : term list > (indexname * sort) list 
91 
val vars_of_terms : term list > (indexname * typ) list 

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

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

5688  94 
val unvarifyT : thm > thm 
95 
val unvarify : thm > thm 

6086
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

96 
val rule_attribute : ('a > thm > thm) > 'a attribute 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

97 
val tag : tag > 'a attribute 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

98 
val untag : tag > 'a attribute 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

99 
val tag_lemma : 'a attribute 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

100 
val tag_assumption : 'a attribute 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

101 
val tag_internal : 'a attribute 
3766  102 
end; 
0  103 

5903  104 
structure Drule: DRULE = 
0  105 
struct 
106 

3991  107 

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

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

109 

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

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

111 

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

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

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

114 
case term_of ct of 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

115 
(Const("==>", _) $ _ $ _) => 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

116 
let val (ct1,ct2) = dest_comb ct 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

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

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

119 

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

120 

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

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

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

123 
case term_of ct of 
1460  124 
(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) => 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

125 
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

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

127 

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

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

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

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

131 
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

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

133 

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

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

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

136 
case term_of ct of (Const("==>", _) $ _ $ _) => 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

137 
strip_imp_concl (#2 (dest_comb ct)) 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

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

139 

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

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

141 
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

142 

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

143 

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

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

145 

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

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

147 
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

148 

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

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

150 
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

151 

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

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

153 
let val {tsig,...} = Sign.rep_sg sign 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

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

157 
 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

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

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

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

161 
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

162 
val T = Sign.read_typ (sign,sorts) st; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

163 
in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

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

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

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

167 
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

168 
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

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

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

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

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

173 
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

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

175 
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

176 
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

177 
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

178 
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

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

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

181 

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

182 

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

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

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

187 
***) 

188 

189 
fun types_sorts thm = 

190 
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

191 
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

192 
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

193 
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

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

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

196 
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

197 
fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); 
0  198 
in (typ,sort) end; 
199 

200 
(** Standardization of rules **) 

201 

202 
(*Generalization over a list of variables, IGNORING bad ones*) 

203 
fun forall_intr_list [] th = th 

204 
 forall_intr_list (y::ys) th = 

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

205 
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

206 
in forall_intr y gth handle THM _ => gth end; 
0  207 

208 
(*Generalization over all suitable Free variables*) 

209 
fun forall_intr_frees th = 

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

211 
in forall_intr_list 

4440  212 
(map (cterm_of sign) (sort (make_ord atless) (term_frees prop))) 
0  213 
th 
214 
end; 

215 

216 
(*Replace outermost quantified variable by Var of given index. 

217 
Could clash with Vars already present.*) 

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

218 
fun forall_elim_var i th = 
0  219 
let val {prop,sign,...} = rep_thm th 
220 
in case prop of 

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

221 
Const("all",_) $ Abs(a,T,_) => 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

222 
forall_elim (cterm_of sign (Var((a,i), T))) th 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

223 
 _ => raise THM("forall_elim_var", i, [th]) 
0  224 
end; 
225 

226 
(*Repeat forall_elim_var until all outer quantifiers are removed*) 

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

227 
fun forall_elim_vars i th = 
0  228 
forall_elim_vars i (forall_elim_var i th) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

229 
handle THM _ => th; 
0  230 

231 
(*Specialization over a list of cterms*) 

232 
fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th); 

233 

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

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

236 

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

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

239 

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

241 
fun zero_var_indexes th = 
0  242 
let val {prop,sign,...} = rep_thm th; 
243 
val vars = term_vars prop 

244 
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

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

246 
val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs)); 
2266  247 
val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs))) 
248 
(inrs, nms') 

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

249 
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

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

251 
 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

252 
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

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

254 
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

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

256 
 varpairs _ = raise TERM("varpairs", []); 
0  257 
in instantiate (ctye, varpairs(vars,rev bs)) th end; 
258 

259 

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

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

262 
fun standard th = 

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

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

265 
th > implies_intr_hyps 
1412  266 
> forall_intr_frees > forall_elim_vars (maxidx + 1) 
1439  267 
> Thm.strip_shyps > Thm.implies_intr_shyps 
1412  268 
> zero_var_indexes > Thm.varifyT > Thm.compress 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

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

270 

0  271 

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

272 
(*Convert all Vars in a theorem to Frees. Also return a function for 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

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

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

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

276 
let val fth = freezeT th 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

277 
val {prop,sign,...} = rep_thm fth 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

278 
val used = add_term_names (prop, []) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

279 
and vars = term_vars prop 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

280 
fun newName (Var(ix,_), (pairs,used)) = 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

281 
let val v = variant used (string_of_indexname ix) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

282 
in ((ix,v)::pairs, v::used) end; 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

283 
val (alist, _) = foldr newName (vars, ([], used)) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

284 
fun mk_inst (Var(v,T)) = 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

285 
(cterm_of sign (Var(v,T)), 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

286 
cterm_of sign (Free(the (assoc(alist,v)), T))) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

287 
val insts = map mk_inst vars 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

288 
fun thaw th' = 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

289 
th' > forall_intr_list (map #2 insts) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

290 
> forall_elim_list (map #1 insts) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

291 
in (instantiate ([],insts) fth, thaw) end; 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

292 

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

293 

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

294 
(*Rotates a rule's premises to the left by k. Does nothing if k=0 or 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

295 
if k equals the number of premises. Useful, for instance, with etac. 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

296 
Similar to tactic/defer_tac*) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

297 
fun rotate_prems k rl = 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

298 
let val (rl',thaw) = freeze_thaw rl 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

299 
val hyps = strip_imp_prems (adjust_maxidx (cprop_of rl')) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

300 
val hyps' = List.drop(hyps, k) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

301 
in implies_elim_list rl' (map assume hyps) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

302 
> implies_intr_list (hyps' @ List.take(hyps, k)) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

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

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

305 

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

306 

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

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

310 
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

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

314 
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

315 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  316 

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

317 
(*Resolution: exactly one resolvent must be produced.*) 
0  318 
fun tha RSN (i,thb) = 
4270  319 
case Seq.chop (2, biresolution false [(false,tha)] i thb) of 
0  320 
([th],_) => th 
321 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

323 

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

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

326 

327 
(*For joining lists of rules*) 

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

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

331 
in List.concat (map resb thbs) end; 
0  332 

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

334 

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

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

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

337 
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

338 
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

339 
 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

340 
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

341 

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

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

343 
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

344 
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

345 
 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

346 
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

347 

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

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

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

351 
fun compose(tha,i,thb) = 
4270  352 
Seq.list_of (bicompose false (false,tha,0) i thb); 
0  353 

6946  354 
fun compose_single (tha,i,thb) = 
355 
(case compose (tha,i,thb) of 

356 
[th] => th 

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

358 

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

361 
case compose(tha,1,thb) of 

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

362 
[th] => th 
0  363 
 _ => raise THM("COMP", 1, [tha,thb]); 
364 

365 
(*Instantiate theorem th, reading instantiations under signature sg*) 

366 
fun read_instantiate_sg sg sinsts th = 

367 
let val ts = types_sorts th; 

952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

368 
val used = add_term_tvarnames(#prop(rep_thm th),[]); 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

369 
in instantiate (read_insts sg ts ts used sinsts) th end; 
0  370 

371 
(*Instantiate theorem th, reading instantiations under theory of th*) 

372 
fun read_instantiate sinsts th = 

373 
read_instantiate_sg (#sign (rep_thm th)) sinsts th; 

374 

375 

376 
(*Lefttoright replacements: tpairs = [...,(vi,ti),...]. 

377 
Instantiates distinct Vars by terms, inferring type instantiations. *) 

378 
local 

1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

379 
fun add_types ((ct,cu), (sign,tye,maxidx)) = 
2152  380 
let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct 
381 
and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu; 

382 
val maxi = Int.max(maxidx, Int.max(maxt, maxu)); 

0  383 
val sign' = Sign.merge(sign, Sign.merge(signt, signu)) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

384 
val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

385 
handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u]) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

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

388 
fun cterm_instantiate ctpairs0 th = 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

389 
let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0)) 
0  390 
val tsig = #tsig(Sign.rep_sg sign); 
391 
fun instT(ct,cu) = let val inst = subst_TVars tye 

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

392 
in (cterm_fun inst ct, cterm_fun inst cu) end 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

393 
fun ctyp2 (ix,T) = (ix, ctyp_of sign T) 
0  394 
in instantiate (map ctyp2 tye, map instT ctpairs0) th end 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

395 
handle TERM _ => 
0  396 
raise THM("cterm_instantiate: incompatible signatures",0,[th]) 
6930  397 
 TYPE (msg, _, _) => raise THM(msg, 0, [th]) 
0  398 
end; 
399 

400 

4016  401 
(** theorem equality **) 
0  402 

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

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

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

407 
val size_of_thm = size_of_term o #prop o rep_thm; 

408 

409 

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

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

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

412 

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

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

414 
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

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

416 
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

417 
 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

418 
 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

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

420 

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

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

422 
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

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

424 
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

425 

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

427 
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

428 

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

429 

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

430 

0  431 
(*** MetaRewriting Rules ***) 
432 

6390  433 
val proto_sign = Theory.sign_of ProtoPure.thy; 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

434 

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

435 
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

436 

4016  437 
fun store_thm name thm = PureThy.smart_store_thm (name, standard thm); 
438 

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

440 
let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS))) 
4016  441 
in store_thm "reflexive" (Thm.reflexive cx) end; 
0  442 

443 
val symmetric_thm = 

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

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

445 
in store_thm "symmetric" 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

446 
(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

447 
end; 
0  448 

449 
val transitive_thm = 

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

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

451 
val yz = read_prop "y::'a::logic == z" 
0  452 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

453 
in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

454 
end; 
0  455 

4679  456 
fun symmetric_fun thm = thm RS symmetric_thm; 
457 

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

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

459 

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

460 
val refl_implies = reflexive (cterm_of proto_sign implies); 
0  461 

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

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

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

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

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

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

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

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

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

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

471 
handle TERM _ => reflexive ct 
0  472 
in gconv 1 end; 
473 

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

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

475 
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; 
0  476 

477 
(*rewriting conversion*) 

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

478 
fun rew_conv mode prover mss = rewrite_cterm mode mss prover; 
0  479 

480 
(*Rewrite a theorem*) 

3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

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

482 
 rewrite_rule_aux prover thms th = 
4713  483 
fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th; 
0  484 

3555  485 
fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss); 
5079  486 
fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover; 
3555  487 

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

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

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

492 
(Thm.mss_of thms))) th; 
0  493 

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

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

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

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

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

498 
else raise THM("rewrite_goal_rule",i,[thm]); 
0  499 

500 

501 
(** Derived rules mainly for METAHYPS **) 

502 

503 
(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*) 

504 
fun equal_abs_elim ca eqth = 

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

505 
let val {sign=signa, t=a, ...} = rep_cterm ca 
0  506 
and combth = combination eqth (reflexive ca) 
507 
val {sign,prop,...} = rep_thm eqth 

508 
val (abst,absu) = Logic.dest_equals prop 

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

509 
val cterm = cterm_of (Sign.merge (sign,signa)) 
0  510 
in transitive (symmetric (beta_conversion (cterm (abst$a)))) 
511 
(transitive combth (beta_conversion (cterm (absu$a)))) 

512 
end 

513 
handle THM _ => raise THM("equal_abs_elim", 0, [eqth]); 

514 

515 
(*Calling equal_abs_elim with multiple terms*) 

516 
fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th); 

517 

518 
local 

519 
val alpha = TVar(("'a",0), []) (* type ?'a::{} *) 

520 
fun err th = raise THM("flexpair_inst: ", 0, [th]) 

521 
fun flexpair_inst def th = 

522 
let val {prop = Const _ $ t $ u, sign,...} = rep_thm th 

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

523 
val cterm = cterm_of sign 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

524 
fun cvar a = cterm(Var((a,0),alpha)) 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

525 
val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

526 
def 
0  527 
in equal_elim def' th 
528 
end 

529 
handle THM _ => err th  bind => err th 

530 
in 

3991  531 
val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def) 
532 
and flexpair_elim = flexpair_inst ProtoPure.flexpair_def 

0  533 
end; 
534 

535 
(*Version for flexflex pairs  this supports lifting.*) 

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

536 
fun flexpair_abs_elim_list cts = 
0  537 
flexpair_intr o equal_abs_elim_list cts o flexpair_elim; 
538 

539 

540 
(*** Some useful metatheorems ***) 

541 

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

4016  543 
val asm_rl = 
4610
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

544 
store_thm "asm_rl" (trivial(read_prop "PROP ?psi")); 
0  545 

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

4016  547 
val cut_rl = 
548 
store_thm "cut_rl" 

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

549 
(trivial(read_prop "PROP ?psi ==> PROP ?theta")); 
0  550 

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

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

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

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

555 
and VW = read_prop "PROP V ==> PROP W"; 
4016  556 
in 
557 
store_thm "revcut_rl" 

558 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 

0  559 
end; 
560 

668  561 
(*for deleting an unwanted assumption*) 
562 
val thin_rl = 

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

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

564 
and W = read_prop "PROP W"; 
4016  565 
in store_thm "thin_rl" (implies_intr V (implies_intr W (assume W))) 
668  566 
end; 
567 

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

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

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

571 
and QV = read_prop "!!x::'a. PROP V" 
b1322be47244
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
paulson
parents:
4588
diff
changeset

572 
and x = read_cterm proto_sign ("x", TFree("'a",logicS)); 
4016  573 
in 
574 
store_thm "triv_forall_equality" 

575 
(equal_intr (implies_intr QV (forall_elim x (assume QV))) 

576 
(implies_intr V (forall_intr x (assume V)))) 

0  577 
end; 
578 

1756  579 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
580 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

582 
*) 

583 
val swap_prems_rl = 

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

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

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

588 
val cminor2 = read_prop "PROP PhiB"; 
1756  589 
val minor2 = assume cminor2; 
4016  590 
in store_thm "swap_prems_rl" 
1756  591 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
592 
(implies_elim (implies_elim major minor1) minor2)))) 

593 
end; 

594 

3653  595 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
596 
==> PROP ?phi == PROP ?psi 

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

597 
Introduction rule for == as a metatheorem. 
3653  598 
*) 
599 
val equal_intr_rule = 

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

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

601 
and QP = read_prop "PROP psi ==> PROP phi" 
4016  602 
in 
603 
store_thm "equal_intr_rule" 

604 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 

3653  605 
end; 
606 

4285  607 

4789  608 
(* GOAL (PROP A) <==> PROP A *) 
609 

610 
local 

611 
val A = read_prop "PROP A"; 

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

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

614 
in 

615 
val triv_goal = store_thm "triv_goal" (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume A)); 

616 
val rev_triv_goal = store_thm "rev_triv_goal" (Thm.equal_elim G_def (Thm.assume G)); 

617 
end; 

618 

6995  619 
val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign (Const ("Goal", propT > propT))); 
620 
fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal; 

621 

4789  622 

4285  623 

5688  624 
(** variations on instantiate **) 
4285  625 

626 
(* collect vars *) 

627 

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

629 
val add_tvars = foldl_types add_tvarsT; 

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

631 

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

634 

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

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

4285  637 

638 

639 
(* instantiate by lefttoright occurrence of variables *) 

640 

641 
fun instantiate' cTs cts thm = 

642 
let 

643 
fun err msg = 

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

645 
mapfilter (apsome Thm.typ_of) cTs, 

646 
mapfilter (apsome Thm.term_of) cts); 

647 

648 
fun inst_of (v, ct) = 

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

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

651 

652 
fun zip_vars _ [] = [] 

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

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

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

656 

657 
(*instantiate types first!*) 

658 
val thm' = 

659 
if forall is_none cTs then thm 

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

661 
in 

662 
if forall is_none cts then thm' 

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

664 
end; 

665 

666 

5688  667 
(* unvarify(T) *) 
668 

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

670 

671 
fun unvarifyT thm = 

672 
let 

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

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

675 
in instantiate' tfrees [] thm end; 

676 

677 
fun unvarify raw_thm = 

678 
let 

679 
val thm = unvarifyT raw_thm; 

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

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

682 
in instantiate' [] frees thm end; 

683 

684 

6435  685 
(* increment var indexes *) 
686 

687 
fun incr_indexes 0 thm = thm 

688 
 incr_indexes inc thm = 

689 
let 

690 
val sign = Thm.sign_of_thm thm; 

691 

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

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

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

696 
in thm'' end; 

6435  697 

698 
fun incr_indexes_wrt is cTs cts thms = 

699 
let 

700 
val maxidx = 

701 
foldl Int.max (~1, is @ 

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

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

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

705 
in incr_indexes (maxidx + 1) end; 

706 

707 

5688  708 
(* mk_triv_goal *) 
709 

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

711 
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

712 

5688  713 

6086
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

714 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

715 
(** basic attributes **) 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

716 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

717 
(* dependent rules *) 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

718 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

719 
fun rule_attribute f (x, thm) = (x, (f x thm)); 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

720 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

721 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

722 
(* add / delete tags *) 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

723 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

724 
fun map_tags f thm = 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

725 
Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm; 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

726 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

727 
fun tag tg x = rule_attribute (K (map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]))) x; 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

728 
fun untag tg x = rule_attribute (K (map_tags (fn tgs => tgs \ tg))) x; 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

729 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

730 
fun simple_tag name x = tag (name, []) x; 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

731 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

732 
fun tag_lemma x = simple_tag "lemma" x; 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

733 
fun tag_assumption x = simple_tag "assumption" x; 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

734 
fun tag_internal x = simple_tag "internal" x; 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

735 

8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

736 

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

738 

5903  739 

740 
structure BasicDrule: BASIC_DRULE = Drule; 

741 
open BasicDrule; 