author  paulson 
Thu, 21 Mar 1996 11:05:34 +0100  
changeset 1596  4a09f4698813 
parent 1499  01fdd1ea6324 
child 1703  e22ad43bab5f 
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 

6 
Derived rules and other operations on theorems and theories 

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 

11 
signature DRULE = 

12 
sig 

1460  13 
val add_defs : (string * string) list > theory > theory 
14 
val add_defs_i : (string * term) list > theory > theory 

15 
val asm_rl : thm 

16 
val assume_ax : theory > string > thm 

17 
val COMP : thm * thm > thm 

18 
val compose : thm * int * thm > thm list 

19 
val cprems_of : thm > cterm list 

20 
val cskip_flexpairs : cterm > cterm 

21 
val cstrip_imp_prems : cterm > cterm list 

22 
val cterm_instantiate : (cterm*cterm)list > thm > thm 

23 
val cut_rl : thm 

24 
val equal_abs_elim : cterm > thm > thm 

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

25 
val equal_abs_elim_list: cterm list > thm > thm 
1460  26 
val eq_thm : thm * thm > bool 
27 
val same_thm : thm * thm > bool 

28 
val eq_thm_sg : thm * thm > bool 

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

29 
val flexpair_abs_elim_list: cterm list > thm > thm 
1460  30 
val forall_intr_list : cterm list > thm > thm 
31 
val forall_intr_frees : thm > thm 

32 
val forall_intr_vars : thm > thm 

33 
val forall_elim_list : cterm list > thm > thm 

34 
val forall_elim_var : int > thm > thm 

35 
val forall_elim_vars : int > thm > thm 

36 
val implies_elim_list : thm > thm list > thm 

37 
val implies_intr_list : cterm list > thm > thm 

38 
val MRL : thm list list * thm list > thm list 

39 
val MRS : thm list * thm > thm 

40 
val read_instantiate : (string*string)list > thm > thm 

0  41 
val read_instantiate_sg: Sign.sg > (string*string)list > thm > thm 
1460  42 
val read_insts : 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

43 
Sign.sg > (indexname > typ option) * (indexname > sort option) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

44 
> (indexname > typ option) * (indexname > sort option) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

45 
> string list > (string*string)list 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

46 
> (indexname*ctyp)list * (cterm*cterm)list 
1460  47 
val reflexive_thm : thm 
48 
val revcut_rl : thm 

49 
val rewrite_goal_rule : bool*bool > (meta_simpset > thm > thm option) 

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

50 
> meta_simpset > int > thm > thm 
0  51 
val rewrite_goals_rule: thm list > thm > thm 
1460  52 
val rewrite_rule : thm list > thm > thm 
53 
val RS : thm * thm > thm 

54 
val RSN : thm * (int * thm) > thm 

55 
val RL : thm list * thm list > thm list 

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

57 
val size_of_thm : thm > int 

58 
val standard : thm > thm 

59 
val symmetric_thm : thm 

60 
val thin_rl : thm 

61 
val transitive_thm : thm 

0  62 
val triv_forall_equality: thm 
63 
val types_sorts: thm > (indexname> typ option) * (indexname> sort option) 

1460  64 
val zero_var_indexes : thm > thm 
0  65 
end; 
66 

668  67 

1499  68 
structure Drule : DRULE = 
0  69 
struct 
70 

561  71 
(**** Extend Theories ****) 
72 

73 
(** add constant definitions **) 

74 

75 
(* all_axioms_of *) 

76 

77 
(*results may contain duplicates!*) 

78 

79 
fun ancestry_of thy = 

80 
thy :: flat (map ancestry_of (parents_of thy)); 

81 

1237  82 
val all_axioms_of = 
776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
708
diff
changeset

83 
flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of; 
561  84 

85 

86 
(* clash_types, clash_consts *) 

87 

88 
(*check if types have common instance (ignoring sorts)*) 

89 

90 
fun clash_types ty1 ty2 = 

91 
let 

92 
val ty1' = Type.varifyT ty1; 

93 
val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2); 

94 
in 

95 
Type.raw_unify (ty1', ty2') 

96 
end; 

97 

98 
fun clash_consts (c1, ty1) (c2, ty2) = 

99 
c1 = c2 andalso clash_types ty1 ty2; 

100 

101 

102 
(* clash_defns *) 

103 

104 
fun clash_defn c_ty (name, tm) = 

105 
let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in 

106 
if clash_consts c_ty (c, ty') then Some (name, ty') else None 

107 
end handle TERM _ => None; 

108 

109 
fun clash_defns c_ty axms = 

110 
distinct (mapfilter (clash_defn c_ty) axms); 

111 

112 

113 
(* dest_defn *) 

114 

115 
fun dest_defn tm = 

116 
let 

117 
fun err msg = raise_term msg [tm]; 

118 

119 
val (lhs, rhs) = Logic.dest_equals tm 

120 
handle TERM _ => err "Not a metaequality (==)"; 

121 
val (head, args) = strip_comb lhs; 

122 
val (c, ty) = dest_Const head 

123 
handle TERM _ => err "Head of lhs not a constant"; 

124 

655  125 
fun occs_const (Const c_ty') = (c_ty' = (c, ty)) 
561  126 
 occs_const (Abs (_, _, t)) = occs_const t 
127 
 occs_const (t $ u) = occs_const t orelse occs_const u 

128 
 occs_const _ = false; 

641  129 

130 
val show_frees = commas_quote o map (fst o dest_Free); 

131 
val show_tfrees = commas_quote o map fst; 

132 

133 
val lhs_dups = duplicates args; 

134 
val rhs_extras = gen_rems (op =) (term_frees rhs, args); 

135 
val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty); 

561  136 
in 
137 
if not (forall is_Free args) then 

138 
err "Arguments of lhs have to be variables" 

641  139 
else if not (null lhs_dups) then 
140 
err ("Duplicate variables on lhs: " ^ show_frees lhs_dups) 

141 
else if not (null rhs_extras) then 

142 
err ("Extra variables on rhs: " ^ show_frees rhs_extras) 

143 
else if not (null rhs_extrasT) then 

144 
err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT) 

561  145 
else if occs_const rhs then 
655  146 
err ("Constant to be defined occurs on rhs") 
561  147 
else (c, ty) 
148 
end; 

149 

150 

151 
(* check_defn *) 

152 

641  153 
fun err_in_defn name msg = 
154 
(writeln msg; error ("The error(s) above occurred in definition " ^ quote name)); 

561  155 

156 
fun check_defn sign (axms, (name, tm)) = 

157 
let 

158 
fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block 

159 
[Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty])); 

160 

161 
fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn; 

1439  162 
fun show_defns c = cat_lines o map (show_defn c); 
561  163 

164 
val (c, ty) = dest_defn tm 

641  165 
handle TERM (msg, _) => err_in_defn name msg; 
561  166 
val defns = clash_defns (c, ty) axms; 
167 
in 

168 
if not (null defns) then 

641  169 
err_in_defn name ("Definition of " ^ show_const (c, ty) ^ 
1439  170 
"\nclashes with " ^ show_defns c defns) 
561  171 
else (name, tm) :: axms 
172 
end; 

173 

174 

175 
(* add_defs *) 

176 

177 
fun ext_defns prep_axm raw_axms thy = 

178 
let 

179 
val axms = map (prep_axm (sign_of thy)) raw_axms; 

180 
val all_axms = all_axioms_of thy; 

181 
in 

182 
foldl (check_defn (sign_of thy)) (all_axms, axms); 

183 
add_axioms_i axms thy 

184 
end; 

185 

186 
val add_defs_i = ext_defns cert_axm; 

187 
val add_defs = ext_defns read_axm; 

188 

189 

190 

0  191 
(**** More derived rules and operations on theorems ****) 
192 

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

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

194 

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

195 
(*Discard flexflex pairs; return a cterm*) 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

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

197 
case term_of ct of 
1460  198 
(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) => 
199 
cskip_flexpairs (#2 (dest_cimplies ct)) 

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

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

201 

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

202 
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

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

204 
let val (cA,cB) = dest_cimplies ct 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

205 
in cA :: cstrip_imp_prems cB end 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

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

207 

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

208 
(*The premises of a theorem, as a cterm list*) 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

209 
val cprems_of = cstrip_imp_prems o cskip_flexpairs o cprop_of; 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

210 

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

211 

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

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

213 

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

214 
fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

215 
 _ => error("Lexical error in variable name " ^ quote (implode cs)); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

216 

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

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

218 
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

219 

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

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

221 
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

222 

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

223 
(* this code is a bit of a mess. add_cterm could be simplified greatly if 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

224 
simultaneous instantiations were read or at least type checked 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

225 
simultaneously rather than one after the other. This would make the tricky 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

226 
composition of implicit type instantiations (parameter tye) superfluous. 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

227 
*) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

228 
fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

229 
let val {tsig,...} = Sign.rep_sg sign 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

230 
fun split([],tvs,vs) = (tvs,vs) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

231 
 split((sv,st)::l,tvs,vs) = (case explode sv of 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

232 
"'"::cs => split(l,(indexname cs,st)::tvs,vs) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

233 
 cs => split(l,tvs,(indexname cs,st)::vs)); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

234 
val (tvs,vs) = split(insts,[],[]); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

235 
fun readT((a,i),st) = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

236 
let val ixn = ("'" ^ a,i); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

237 
val S = case rsorts ixn of Some S => S  None => absent ixn; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

238 
val T = Sign.read_typ (sign,sorts) st; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

239 
in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

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

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

242 
val tye = map readT tvs; 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

243 
fun add_cterm ((cts,tye,used), (ixn,st)) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

244 
let val T = case rtypes ixn of 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

245 
Some T => typ_subst_TVars tye T 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

246 
 None => absent ixn; 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

247 
val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T); 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

248 
val cts' = (ixn,T,ct)::cts 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

249 
fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

250 
val used' = add_term_tvarnames(term_of ct,used); 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

251 
in (map inst cts',tye2 @ tye,used') end 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

252 
val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs); 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

253 
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

254 
map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms) 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

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

256 

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

257 

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

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

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

262 
***) 

263 

264 
fun types_sorts thm = 

265 
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

266 
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

267 
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

268 
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

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

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

271 
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

272 
fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); 
0  273 
in (typ,sort) end; 
274 

275 
(** Standardization of rules **) 

276 

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

278 
fun forall_intr_list [] th = th 

279 
 forall_intr_list (y::ys) th = 

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

280 
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

281 
in forall_intr y gth handle THM _ => gth end; 
0  282 

283 
(*Generalization over all suitable Free variables*) 

284 
fun forall_intr_frees th = 

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

286 
in forall_intr_list 

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

287 
(map (cterm_of sign) (sort atless (term_frees prop))) 
0  288 
th 
289 
end; 

290 

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

292 
Could clash with Vars already present.*) 

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

293 
fun forall_elim_var i th = 
0  294 
let val {prop,sign,...} = rep_thm th 
295 
in case prop of 

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

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

297 
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

298 
 _ => raise THM("forall_elim_var", i, [th]) 
0  299 
end; 
300 

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

302 
fun forall_elim_vars i th = 
0  303 
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

304 
handle THM _ => th; 
0  305 

306 
(*Specialization over a list of cterms*) 

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

308 

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

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

311 

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

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

314 

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

316 
fun zero_var_indexes th = 
0  317 
let val {prop,sign,...} = rep_thm th; 
318 
val vars = term_vars prop 

319 
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

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

321 
val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs)); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

322 
val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms') 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

323 
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

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

325 
 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

326 
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

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

328 
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

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

330 
 varpairs _ = raise TERM("varpairs", []); 
0  331 
in instantiate (ctye, varpairs(vars,rev bs)) th end; 
332 

333 

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

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

336 
fun standard th = 

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

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

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

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

344 

0  345 

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

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

349 
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

350 
[ !(A,P,a)[ ALL x:A. P(x) ] ==> [ P(a) ] ] *) 
0  351 
fun assume_ax thy sP = 
352 
let val sign = sign_of thy 

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

353 
val prop = Logic.close_form (term_of (read_cterm sign 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

354 
(sP, propT))) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

355 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  356 

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

357 
(*Resolution: exactly one resolvent must be produced.*) 
0  358 
fun tha RSN (i,thb) = 
359 
case Sequence.chop (2, biresolution false [(false,tha)] i thb) of 

360 
([th],_) => th 

361 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

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

363 

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

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

366 

367 
(*For joining lists of rules*) 

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

368 
fun thas RLN (i,thbs) = 
0  369 
let val resolve = biresolution false (map (pair false) thas) i 
370 
fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => [] 

371 
in flat (map resb thbs) end; 

372 

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

374 

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

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

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

377 
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

378 
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

379 
 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

380 
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

381 

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

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

383 
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

384 
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

385 
 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

386 
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

387 

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

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

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

391 
fun compose(tha,i,thb) = 
0  392 
Sequence.list_of_s (bicompose false (false,tha,0) i thb); 
393 

394 
(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) 

395 
fun tha COMP thb = 

396 
case compose(tha,1,thb) of 

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

397 
[th] => th 
0  398 
 _ => raise THM("COMP", 1, [tha,thb]); 
399 

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

401 
fun read_instantiate_sg sg sinsts th = 

402 
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

403 
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

404 
in instantiate (read_insts sg ts ts used sinsts) th end; 
0  405 

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

407 
fun read_instantiate sinsts th = 

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

409 

410 

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

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

413 
local 

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

414 
fun add_types ((ct,cu), (sign,tye,maxidx)) = 
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

415 
let val {sign=signt, t=t, T= T, maxidx=maxidxt,...} = rep_cterm ct 
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

416 
and {sign=signu, t=u, T= U, maxidx=maxidxu,...} = rep_cterm cu; 
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

417 
val maxi = max[maxidx,maxidxt,maxidxu]; 
0  418 
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

419 
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

420 
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

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

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

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

427 
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

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

430 
handle TERM _ => 
0  431 
raise THM("cterm_instantiate: incompatible signatures",0,[th]) 
432 
 TYPE _ => raise THM("cterm_instantiate: types", 0, [th]) 

433 
end; 

434 

435 

436 
(** theorem equality test is exported and used by BEST_FIRST **) 

437 

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

438 
(*equality of theorems uses equality of signatures and 
0  439 
the aconvertible test for terms*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

440 
fun eq_thm (th1,th2) = 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

441 
let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

442 
and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

443 
in Sign.eq_sg (sg1,sg2) andalso 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

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

445 
aconvs(hyps1,hyps2) andalso 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

446 
prop1 aconv prop2 
0  447 
end; 
448 

1241  449 
(*equality of theorems using similarity of signatures, 
450 
i.e. the theorems belong to the same theory but not necessarily to the same 

451 
version of this theory*) 

452 
fun same_thm (th1,th2) = 

453 
let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1 

454 
and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2 

455 
in Sign.same_sg (sg1,sg2) andalso 

456 
eq_set (shyps1, shyps2) andalso 

457 
aconvs(hyps1,hyps2) andalso 

458 
prop1 aconv prop2 

459 
end; 

460 

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

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

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

465 
val size_of_thm = size_of_term o #prop o rep_thm; 

466 

467 

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

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

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

470 

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

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

472 
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

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

474 
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

475 
 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

476 
 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

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

478 

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

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

480 
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

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

482 
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

483 

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

485 
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

486 

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

487 

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

488 

0  489 
(*** MetaRewriting Rules ***) 
490 

491 

492 
val reflexive_thm = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

493 
let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS))) 
0  494 
in Thm.reflexive cx end; 
495 

496 
val symmetric_thm = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

497 
let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT) 
0  498 
in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end; 
499 

500 
val transitive_thm = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

501 
let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

502 
val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT) 
0  503 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
504 
in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 

505 

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

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

507 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

508 
val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies); 
0  509 

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

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

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

513 
let fun gconv i ct = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

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

515 
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

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

517 
 _ => (if pred i then cv A else reflexive A, i+1) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

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

519 
handle TERM _ => reflexive ct 
0  520 
in gconv 1 end; 
521 

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

523 
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; 
0  524 

525 
(*rewriting conversion*) 

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

526 
fun rew_conv mode prover mss = rewrite_cterm mode mss prover; 
0  527 

528 
(*Rewrite a theorem*) 

1412  529 
fun rewrite_rule [] th = th 
530 
 rewrite_rule thms th = 

1460  531 
fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th; 
0  532 

533 
(*Rewrite the subgoals of a proof state (represented by a theorem) *) 

1412  534 
fun rewrite_goals_rule [] th = th 
535 
 rewrite_goals_rule thms th = 

1460  536 
fconv_rule (goals_conv (K true) 
537 
(rew_conv (true,false) (K(K None)) 

538 
(Thm.mss_of thms))) 

539 
th; 

0  540 

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

542 
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

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

544 
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

545 
else raise THM("rewrite_goal_rule",i,[thm]); 
0  546 

547 

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

549 

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

551 
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

552 
let val {sign=signa, t=a, ...} = rep_cterm ca 
0  553 
and combth = combination eqth (reflexive ca) 
554 
val {sign,prop,...} = rep_thm eqth 

555 
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

556 
val cterm = cterm_of (Sign.merge (sign,signa)) 
0  557 
in transitive (symmetric (beta_conversion (cterm (abst$a)))) 
558 
(transitive combth (beta_conversion (cterm (absu$a)))) 

559 
end 

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

561 

562 
(*Calling equal_abs_elim with multiple terms*) 

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

564 

565 
local 

566 
open Logic 

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

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

569 
fun flexpair_inst def th = 

570 
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

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

572 
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

573 
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

574 
def 
0  575 
in equal_elim def' th 
576 
end 

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

578 
in 

579 
val flexpair_intr = flexpair_inst (symmetric flexpair_def) 

580 
and flexpair_elim = flexpair_inst flexpair_def 

581 
end; 

582 

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

584 
fun flexpair_abs_elim_list cts = 
0  585 
flexpair_intr o equal_abs_elim_list cts o flexpair_elim; 
586 

587 

588 
(*** Some useful metatheorems ***) 

589 

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

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

591 
val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT)); 
0  592 

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

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

594 
val cut_rl = trivial(read_cterm Sign.proto_pure 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

595 
("PROP ?psi ==> PROP ?theta", propT)); 
0  596 

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

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

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

600 
let val V = read_cterm Sign.proto_pure ("PROP V", propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

601 
and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT); 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

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

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

604 
(implies_elim (assume VW) (assume V)))) 
0  605 
end; 
606 

668  607 
(*for deleting an unwanted assumption*) 
608 
val thin_rl = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

609 
let val V = read_cterm Sign.proto_pure ("PROP V", propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

610 
and W = read_cterm Sign.proto_pure ("PROP W", propT); 
668  611 
in standard (implies_intr V (implies_intr W (assume W))) 
612 
end; 

613 

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

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

616 
let val V = read_cterm Sign.proto_pure ("PROP V", propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

617 
and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
843
diff
changeset

618 
and x = read_cterm Sign.proto_pure ("x", TFree("'a",logicS)); 
0  619 
in standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

620 
(implies_intr V (forall_intr x (assume V)))) 
0  621 
end; 
622 

623 
end; 

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

624 

1499  625 
open Drule; 