author  wenzelm 
Sat, 04 Sep 1999 20:59:33 +0200  
changeset 7467  71e5d8671e7b 
parent 7404  e488cf3da60a 
child 7636  102a4b6b83a6 
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 = 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

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

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

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

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

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

281 
 vars => 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

282 
let fun newName (Var(ix,_), (pairs,used)) = 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

283 
let val v = variant used (string_of_indexname ix) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

284 
in ((ix,v)::pairs, v::used) end; 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

285 
val (alist, _) = foldr newName 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

286 
(vars, ([], add_term_names (prop, []))) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

287 
fun mk_inst (Var(v,T)) = 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

288 
(cterm_of sign (Var(v,T)), 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

289 
cterm_of sign (Free(the (assoc(alist,v)), T))) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

290 
val insts = map mk_inst vars 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

291 
fun thaw th' = 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

292 
th' > forall_intr_list (map #2 insts) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

293 
> forall_elim_list (map #1 insts) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

294 
in (instantiate ([],insts) fth, thaw) end 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6995
diff
changeset

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

296 

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

297 

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

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

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

300 

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

301 

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

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

305 
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

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

309 
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

310 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  311 

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

312 
(*Resolution: exactly one resolvent must be produced.*) 
0  313 
fun tha RSN (i,thb) = 
4270  314 
case Seq.chop (2, biresolution false [(false,tha)] i thb) of 
0  315 
([th],_) => th 
316 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

318 

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

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

321 

322 
(*For joining lists of rules*) 

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

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

326 
in List.concat (map resb thbs) end; 
0  327 

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

329 

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

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

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

332 
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

333 
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

334 
 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

335 
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

336 

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

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

338 
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

339 
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

340 
 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

341 
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

342 

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

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

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

346 
fun compose(tha,i,thb) = 
4270  347 
Seq.list_of (bicompose false (false,tha,0) i thb); 
0  348 

6946  349 
fun compose_single (tha,i,thb) = 
350 
(case compose (tha,i,thb) of 

351 
[th] => th 

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

353 

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

356 
case compose(tha,1,thb) of 

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

357 
[th] => th 
0  358 
 _ => raise THM("COMP", 1, [tha,thb]); 
359 

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

361 
fun read_instantiate_sg sg sinsts th = 

362 
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

363 
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

364 
in instantiate (read_insts sg ts ts used sinsts) th end; 
0  365 

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

367 
fun read_instantiate sinsts th = 

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

369 

370 

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

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

373 
local 

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

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

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

0  378 
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

379 
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

380 
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

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

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

384 
let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0)) 
0  385 
val tsig = #tsig(Sign.rep_sg sign); 
386 
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

387 
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

388 
fun ctyp2 (ix,T) = (ix, ctyp_of sign T) 
0  389 
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

390 
handle TERM _ => 
0  391 
raise THM("cterm_instantiate: incompatible signatures",0,[th]) 
6930  392 
 TYPE (msg, _, _) => raise THM(msg, 0, [th]) 
0  393 
end; 
394 

395 

4016  396 
(** theorem equality **) 
0  397 

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

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

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

402 
val size_of_thm = size_of_term o #prop o rep_thm; 

403 

404 

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

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

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

407 

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

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

409 
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

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

411 
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

412 
 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

413 
 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

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

415 

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

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

417 
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

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

419 
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

420 

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

422 
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

423 

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

424 

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

425 

0  426 
(*** MetaRewriting Rules ***) 
427 

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

429 

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

430 
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

431 

7404  432 
fun store_thm name thm = hd (PureThy.smart_store_thms (name, [standard thm])); 
4016  433 

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

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

438 
val symmetric_thm = 

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

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

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

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

442 
end; 
0  443 

444 
val transitive_thm = 

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

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

446 
val yz = read_prop "y::'a::logic == z" 
0  447 
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

448 
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

449 
end; 
0  450 

4679  451 
fun symmetric_fun thm = thm RS symmetric_thm; 
452 

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

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

454 

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

455 
val refl_implies = reflexive (cterm_of proto_sign implies); 
0  456 

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

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

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

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

461 
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

462 
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

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

464 
 _ => (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

465 
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

466 
handle TERM _ => reflexive ct 
0  467 
in gconv 1 end; 
468 

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

470 
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; 
0  471 

472 
(*rewriting conversion*) 

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

473 
fun rew_conv mode prover mss = rewrite_cterm mode mss prover; 
0  474 

475 
(*Rewrite a theorem*) 

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

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

477 
 rewrite_rule_aux prover thms th = 
4713  478 
fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th; 
0  479 

3555  480 
fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss); 
5079  481 
fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover; 
3555  482 

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

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

485 
 rewrite_goals_rule_aux prover thms th = 
4713  486 
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

487 
(Thm.mss_of thms))) th; 
0  488 

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

490 
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

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

492 
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

493 
else raise THM("rewrite_goal_rule",i,[thm]); 
0  494 

495 

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

497 

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

499 
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

500 
let val {sign=signa, t=a, ...} = rep_cterm ca 
0  501 
and combth = combination eqth (reflexive ca) 
502 
val {sign,prop,...} = rep_thm eqth 

503 
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

504 
val cterm = cterm_of (Sign.merge (sign,signa)) 
0  505 
in transitive (symmetric (beta_conversion (cterm (abst$a)))) 
506 
(transitive combth (beta_conversion (cterm (absu$a)))) 

507 
end 

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

509 

510 
(*Calling equal_abs_elim with multiple terms*) 

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

512 

513 
local 

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

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

516 
fun flexpair_inst def th = 

517 
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

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

519 
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

520 
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

521 
def 
0  522 
in equal_elim def' th 
523 
end 

7467  524 
handle THM _ => err th  Bind => err th 
0  525 
in 
3991  526 
val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def) 
527 
and flexpair_elim = flexpair_inst ProtoPure.flexpair_def 

0  528 
end; 
529 

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

531 
fun flexpair_abs_elim_list cts = 
0  532 
flexpair_intr o equal_abs_elim_list cts o flexpair_elim; 
533 

534 

535 
(*** Some useful metatheorems ***) 

536 

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

7380  538 
val asm_rl = store_thm "asm_rl" (trivial(read_prop "PROP ?psi")); 
539 
val _ = store_thm "_" asm_rl; 

0  540 

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

4016  542 
val cut_rl = 
543 
store_thm "cut_rl" 

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

544 
(trivial(read_prop "PROP ?psi ==> PROP ?theta")); 
0  545 

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

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

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

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

550 
and VW = read_prop "PROP V ==> PROP W"; 
4016  551 
in 
552 
store_thm "revcut_rl" 

553 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 

0  554 
end; 
555 

668  556 
(*for deleting an unwanted assumption*) 
557 
val thin_rl = 

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

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

559 
and W = read_prop "PROP W"; 
4016  560 
in store_thm "thin_rl" (implies_intr V (implies_intr W (assume W))) 
668  561 
end; 
562 

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

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

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

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

567 
and x = read_cterm proto_sign ("x", TFree("'a",logicS)); 
4016  568 
in 
569 
store_thm "triv_forall_equality" 

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

571 
(implies_intr V (forall_intr x (assume V)))) 

0  572 
end; 
573 

1756  574 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
575 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

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

577 
*) 

578 
val swap_prems_rl = 

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

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

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

583 
val cminor2 = read_prop "PROP PhiB"; 
1756  584 
val minor2 = assume cminor2; 
4016  585 
in store_thm "swap_prems_rl" 
1756  586 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
587 
(implies_elim (implies_elim major minor1) minor2)))) 

588 
end; 

589 

3653  590 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
591 
==> PROP ?phi == PROP ?psi 

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

592 
Introduction rule for == as a metatheorem. 
3653  593 
*) 
594 
val equal_intr_rule = 

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

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

596 
and QP = read_prop "PROP psi ==> PROP phi" 
4016  597 
in 
598 
store_thm "equal_intr_rule" 

599 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 

3653  600 
end; 
601 

4285  602 

4789  603 
(* GOAL (PROP A) <==> PROP A *) 
604 

605 
local 

606 
val A = read_prop "PROP A"; 

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

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

609 
in 

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

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

612 
end; 

613 

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

616 

4789  617 

4285  618 

5688  619 
(** variations on instantiate **) 
4285  620 

621 
(* collect vars *) 

622 

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

624 
val add_tvars = foldl_types add_tvarsT; 

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

626 

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

629 

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

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

4285  632 

633 

634 
(* instantiate by lefttoright occurrence of variables *) 

635 

636 
fun instantiate' cTs cts thm = 

637 
let 

638 
fun err msg = 

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

640 
mapfilter (apsome Thm.typ_of) cTs, 

641 
mapfilter (apsome Thm.term_of) cts); 

642 

643 
fun inst_of (v, ct) = 

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

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

646 

647 
fun zip_vars _ [] = [] 

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

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

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

651 

652 
(*instantiate types first!*) 

653 
val thm' = 

654 
if forall is_none cTs then thm 

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

656 
in 

657 
if forall is_none cts then thm' 

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

659 
end; 

660 

661 

5688  662 
(* unvarify(T) *) 
663 

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

665 

666 
fun unvarifyT thm = 

667 
let 

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

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

670 
in instantiate' tfrees [] thm end; 

671 

672 
fun unvarify raw_thm = 

673 
let 

674 
val thm = unvarifyT raw_thm; 

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

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

677 
in instantiate' [] frees thm end; 

678 

679 

6435  680 
(* increment var indexes *) 
681 

682 
fun incr_indexes 0 thm = thm 

683 
 incr_indexes inc thm = 

684 
let 

685 
val sign = Thm.sign_of_thm thm; 

686 

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

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

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

691 
in thm'' end; 

6435  692 

693 
fun incr_indexes_wrt is cTs cts thms = 

694 
let 

695 
val maxidx = 

696 
foldl Int.max (~1, is @ 

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

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

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

700 
in incr_indexes (maxidx + 1) end; 

701 

702 

5688  703 
(* mk_triv_goal *) 
704 

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

706 
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

707 

5688  708 

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

709 

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

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

711 

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

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

713 

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

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

715 

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 
(* add / delete tags *) 
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 map_tags f thm = 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

720 
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

721 

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

722 
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

723 
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

724 

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

725 
fun simple_tag name x = tag (name, []) x; 
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_lemma x = simple_tag "lemma" x; 
8cd4190e633a
added rule_attribute: ('a > thm > thm) > 'a attribute;
wenzelm
parents:
5903
diff
changeset

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

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

730 

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

731 

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

733 

5903  734 

735 
structure BasicDrule: BASIC_DRULE = Drule; 

736 
open BasicDrule; 