author  clasohm 
Mon, 29 Jan 1996 14:16:13 +0100  
changeset 1460  5a6f2aabd538 
parent 1458  fd510875fb71 
child 1499  01fdd1ea6324 
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 

13 
structure Thm : THM 

14 
local open Thm in 

1460  15 
val add_defs : (string * string) list > theory > theory 
16 
val add_defs_i : (string * term) list > theory > theory 

17 
val asm_rl : thm 

18 
val assume_ax : theory > string > thm 

19 
val COMP : thm * thm > thm 

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

21 
val cprems_of : thm > cterm list 

22 
val cskip_flexpairs : cterm > cterm 

23 
val cstrip_imp_prems : cterm > cterm list 

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

25 
val cut_rl : thm 

26 
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

27 
val equal_abs_elim_list: cterm list > thm > thm 
1460  28 
val eq_thm : thm * thm > bool 
29 
val same_thm : thm * thm > bool 

30 
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

31 
val flexpair_abs_elim_list: cterm list > thm > thm 
1460  32 
val forall_intr_list : cterm list > thm > thm 
33 
val forall_intr_frees : thm > thm 

34 
val forall_intr_vars : thm > thm 

35 
val forall_elim_list : cterm list > thm > thm 

36 
val forall_elim_var : int > thm > thm 

37 
val forall_elim_vars : int > thm > thm 

38 
val implies_elim_list : thm > thm list > thm 

39 
val implies_intr_list : cterm list > thm > thm 

40 
val MRL : thm list list * thm list > thm list 

41 
val MRS : thm list * thm > thm 

42 
val pprint_cterm : cterm > pprint_args > unit 

43 
val pprint_ctyp : ctyp > pprint_args > unit 

44 
val pprint_theory : theory > pprint_args > unit 

45 
val pprint_thm : thm > pprint_args > unit 

46 
val pretty_thm : thm > Sign.Syntax.Pretty.T 

47 
val print_cterm : cterm > unit 

48 
val print_ctyp : ctyp > unit 

49 
val print_goals : int > thm > unit 

50 
val print_goals_ref : (int > thm > unit) ref 

51 
val print_syntax : theory > unit 

52 
val print_theory : theory > unit 

53 
val print_thm : thm > unit 

54 
val prth : thm > thm 

55 
val prthq : thm Sequence.seq > thm Sequence.seq 

56 
val prths : thm list > thm list 

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

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

60 
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

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

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

63 
> (indexname*ctyp)list * (cterm*cterm)list 
1460  64 
val reflexive_thm : thm 
65 
val revcut_rl : thm 

66 
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

67 
> meta_simpset > int > thm > thm 
0  68 
val rewrite_goals_rule: thm list > thm > thm 
1460  69 
val rewrite_rule : thm list > thm > thm 
70 
val RS : thm * thm > thm 

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

72 
val RL : thm list * thm list > thm list 

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

74 
val show_hyps : bool ref 

75 
val size_of_thm : thm > int 

76 
val standard : thm > thm 

77 
val string_of_cterm : cterm > string 

78 
val string_of_ctyp : ctyp > string 

79 
val string_of_thm : thm > string 

80 
val symmetric_thm : thm 

81 
val thin_rl : thm 

82 
val transitive_thm : thm 

0  83 
val triv_forall_equality: thm 
84 
val types_sorts: thm > (indexname> typ option) * (indexname> sort option) 

1460  85 
val zero_var_indexes : thm > thm 
0  86 
end 
87 
end; 

88 

668  89 

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

90 
functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE = 
0  91 
struct 
92 
structure Thm = Thm; 

93 
structure Sign = Thm.Sign; 

94 
structure Type = Sign.Type; 

575  95 
structure Syntax = Sign.Syntax; 
96 
structure Pretty = Syntax.Pretty 

400  97 
structure Symtab = Sign.Symtab; 
98 

0  99 
local open Thm 
100 
in 

101 

561  102 
(**** Extend Theories ****) 
103 

104 
(** add constant definitions **) 

105 

106 
(* all_axioms_of *) 

107 

108 
(*results may contain duplicates!*) 

109 

110 
fun ancestry_of thy = 

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

112 

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

114 
flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of; 
561  115 

116 

117 
(* clash_types, clash_consts *) 

118 

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

120 

121 
fun clash_types ty1 ty2 = 

122 
let 

123 
val ty1' = Type.varifyT ty1; 

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

125 
in 

126 
Type.raw_unify (ty1', ty2') 

127 
end; 

128 

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

130 
c1 = c2 andalso clash_types ty1 ty2; 

131 

132 

133 
(* clash_defns *) 

134 

135 
fun clash_defn c_ty (name, tm) = 

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

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

138 
end handle TERM _ => None; 

139 

140 
fun clash_defns c_ty axms = 

141 
distinct (mapfilter (clash_defn c_ty) axms); 

142 

143 

144 
(* dest_defn *) 

145 

146 
fun dest_defn tm = 

147 
let 

148 
fun err msg = raise_term msg [tm]; 

149 

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

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

152 
val (head, args) = strip_comb lhs; 

153 
val (c, ty) = dest_Const head 

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

155 

655  156 
fun occs_const (Const c_ty') = (c_ty' = (c, ty)) 
561  157 
 occs_const (Abs (_, _, t)) = occs_const t 
158 
 occs_const (t $ u) = occs_const t orelse occs_const u 

159 
 occs_const _ = false; 

641  160 

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

162 
val show_tfrees = commas_quote o map fst; 

163 

164 
val lhs_dups = duplicates args; 

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

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

561  167 
in 
168 
if not (forall is_Free args) then 

169 
err "Arguments of lhs have to be variables" 

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

172 
else if not (null rhs_extras) then 

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

174 
else if not (null rhs_extrasT) then 

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

561  176 
else if occs_const rhs then 
655  177 
err ("Constant to be defined occurs on rhs") 
561  178 
else (c, ty) 
179 
end; 

180 

181 

182 
(* check_defn *) 

183 

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

561  186 

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

188 
let 

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

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

191 

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

1439  193 
fun show_defns c = cat_lines o map (show_defn c); 
561  194 

195 
val (c, ty) = dest_defn tm 

641  196 
handle TERM (msg, _) => err_in_defn name msg; 
561  197 
val defns = clash_defns (c, ty) axms; 
198 
in 

199 
if not (null defns) then 

641  200 
err_in_defn name ("Definition of " ^ show_const (c, ty) ^ 
1439  201 
"\nclashes with " ^ show_defns c defns) 
561  202 
else (name, tm) :: axms 
203 
end; 

204 

205 

206 
(* add_defs *) 

207 

208 
fun ext_defns prep_axm raw_axms thy = 

209 
let 

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

211 
val all_axms = all_axioms_of thy; 

212 
in 

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

214 
add_axioms_i axms thy 

215 
end; 

216 

217 
val add_defs_i = ext_defns cert_axm; 

218 
val add_defs = ext_defns read_axm; 

219 

220 

221 

0  222 
(**** More derived rules and operations on theorems ****) 
223 

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

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

225 

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

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

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

228 
case term_of ct of 
1460  229 
(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) => 
230 
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

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

232 

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

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

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

235 
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

236 
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

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

238 

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

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

240 
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

241 

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

242 

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

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

244 

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

245 
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

246 
 _ => 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

247 

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

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

249 
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

250 

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

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

252 
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

253 

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

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

255 
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

256 
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

257 
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

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

259 
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

260 
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

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

262 
 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

263 
"'"::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

264 
 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

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

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

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

268 
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

269 
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

270 
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

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

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

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

274 
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

275 
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

276 
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

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

278 
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

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

280 
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

281 
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

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

283 
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

284 
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

285 
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

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

287 

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

288 

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

289 

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

290 
(*** Printing of theories, theorems, etc. ***) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

291 

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

292 
(*If false, hypotheses are printed as dots*) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

293 
val show_hyps = ref true; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

294 

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

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

296 
let 
1237  297 
val {sign, hyps, prop, ...} = rep_thm th; 
298 
val xshyps = extra_shyps th; 

299 
val hlen = length xshyps + length hyps; 

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

300 
val hsymbs = 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

301 
if hlen = 0 then [] 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

302 
else if ! show_hyps then 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

303 
[Pretty.brk 2, Pretty.list "[" "]" 
1237  304 
(map (Sign.pretty_term sign) hyps @ map Sign.pretty_sort xshyps)] 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

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

306 
[Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")]; 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

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

308 
Pretty.block (Sign.pretty_term sign prop :: hsymbs) 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

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

310 

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

311 
val string_of_thm = Pretty.string_of o pretty_thm; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

312 
val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

313 

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

314 

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

315 
(** Toplevel commands for printing theorems **) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

316 
val print_thm = writeln o string_of_thm; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

317 

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

318 
fun prth th = (print_thm th; th); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

319 

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

320 
(*Print and return a sequence of theorems, separated by blank lines. *) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

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

322 
(Sequence.prints (fn _ => print_thm) 100000 thseq; thseq); 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

323 

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

324 
(*Print and return a list of theorems, separated by blank lines. *) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

325 
fun prths ths = (print_list_ln print_thm ths; ths); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

326 

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

327 

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

328 
(* other printing commands *) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

329 

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

330 
fun pprint_ctyp cT = 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

331 
let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end; 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

332 

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

333 
fun string_of_ctyp cT = 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

334 
let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

335 

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

336 
val print_ctyp = writeln o string_of_ctyp; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

337 

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

338 
fun pprint_cterm ct = 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

339 
let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

340 

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

341 
fun string_of_cterm ct = 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

342 
let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

343 

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

344 
val print_cterm = writeln o string_of_cterm; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

345 

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

346 

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

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

348 

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

349 
val pprint_theory = Sign.pprint_sg o sign_of; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

350 

575  351 
val print_syntax = Syntax.print_syntax o syn_of; 
352 

385  353 
fun print_axioms thy = 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

354 
let 
400  355 
val {sign, new_axioms, ...} = rep_theory thy; 
356 
val axioms = Symtab.dest new_axioms; 

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

357 

385  358 
fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, 
359 
Pretty.quote (Sign.pretty_term sign t)]; 

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

360 
in 
385  361 
Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms)) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

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

363 

843  364 
fun print_theory thy = (Sign.print_sg (sign_of thy); print_axioms thy); 
385  365 

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

366 

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

367 

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

368 
(** Print thm A1,...,An/B in "goal style"  premises as numbered subgoals **) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

369 

641  370 
(* get type_env, sort_env of term *) 
371 

372 
local 

373 
open Syntax; 

374 

375 
fun ins_entry (x, y) [] = [(x, [y])] 

376 
 ins_entry (x, y) ((pair as (x', ys')) :: pairs) = 

377 
if x = x' then (x', y ins ys') :: pairs 

378 
else pair :: ins_entry (x, y) pairs; 

379 

380 
fun add_type_env (Free (x, T), env) = ins_entry (T, x) env 

381 
 add_type_env (Var (xi, T), env) = ins_entry (T, string_of_vname xi) env 

382 
 add_type_env (Abs (_, _, t), env) = add_type_env (t, env) 

383 
 add_type_env (t $ u, env) = add_type_env (u, add_type_env (t, env)) 

384 
 add_type_env (_, env) = env; 

385 

386 
fun add_sort_env (Type (_, Ts), env) = foldr add_sort_env (Ts, env) 

387 
 add_sort_env (TFree (x, S), env) = ins_entry (S, x) env 

388 
 add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env; 

389 

390 
val sort = map (apsnd sort_strings); 

391 
in 

392 
fun type_env t = sort (add_type_env (t, [])); 

393 
fun sort_env t = rev (sort (it_term_types add_sort_env (t, []))); 

394 
end; 

395 

396 

397 
(* print_goals *) 

398 

399 
fun print_goals maxgoals state = 

400 
let 

401 
open Syntax; 

402 

403 
val {sign, prop, ...} = rep_thm state; 

404 

405 
val pretty_term = Sign.pretty_term sign; 

406 
val pretty_typ = Sign.pretty_typ sign; 

407 
val pretty_sort = Sign.pretty_sort; 

408 

409 
fun pretty_vars prtf (X, vs) = Pretty.block 

410 
[Pretty.block (Pretty.commas (map Pretty.str vs)), 

411 
Pretty.str " ::", Pretty.brk 1, prtf X]; 

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

412 

641  413 
fun print_list _ _ [] = () 
414 
 print_list name prtf lst = 

415 
(writeln ""; Pretty.writeln (Pretty.big_list name (map prtf lst))); 

416 

417 

418 
fun print_goals (_, []) = () 

419 
 print_goals (n, A :: As) = (Pretty.writeln (Pretty.blk (0, 

420 
[Pretty.str (" " ^ string_of_int n ^ ". "), pretty_term A])); 

421 
print_goals (n + 1, As)); 

422 

423 
val print_ffpairs = 

424 
print_list "Flexflex pairs:" (pretty_term o Logic.mk_flexpair); 

425 

426 
val print_types = print_list "Types:" (pretty_vars pretty_typ) o type_env; 

427 
val print_sorts = print_list "Sorts:" (pretty_vars pretty_sort) o sort_env; 

428 

429 

430 
val (tpairs, As, B) = Logic.strip_horn prop; 

431 
val ngoals = length As; 

432 

433 
val orig_no_freeTs = ! show_no_free_types; 

434 
val orig_sorts = ! show_sorts; 

435 

436 
fun restore () = 

437 
(show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts); 

438 
in 

439 
(show_no_free_types := true; show_sorts := false; 

440 
Pretty.writeln (pretty_term B); 

441 
if ngoals = 0 then writeln "No subgoals!" 

442 
else if ngoals > maxgoals then 

443 
(print_goals (1, take (maxgoals, As)); 

444 
writeln ("A total of " ^ string_of_int ngoals ^ " subgoals...")) 

445 
else print_goals (1, As); 

446 

447 
print_ffpairs tpairs; 

448 

449 
if orig_sorts then 

450 
(print_types prop; print_sorts prop) 

451 
else if ! show_types then 

452 
print_types prop 

453 
else ()) 

454 
handle exn => (restore (); raise exn); 

455 
restore () 

456 
end; 

457 

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

458 

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

459 
(*"hook" for user interfaces: allows print_goals to be replaced*) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

460 
val print_goals_ref = ref print_goals; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

461 

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

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

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

466 
***) 

467 

468 
fun types_sorts thm = 

469 
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

470 
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

471 
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

472 
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

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

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

475 
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

476 
fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); 
0  477 
in (typ,sort) end; 
478 

479 
(** Standardization of rules **) 

480 

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

482 
fun forall_intr_list [] th = th 

483 
 forall_intr_list (y::ys) th = 

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

484 
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

485 
in forall_intr y gth handle THM _ => gth end; 
0  486 

487 
(*Generalization over all suitable Free variables*) 

488 
fun forall_intr_frees th = 

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

490 
in forall_intr_list 

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

491 
(map (cterm_of sign) (sort atless (term_frees prop))) 
0  492 
th 
493 
end; 

494 

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

496 
Could clash with Vars already present.*) 

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

497 
fun forall_elim_var i th = 
0  498 
let val {prop,sign,...} = rep_thm th 
499 
in case prop of 

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

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

501 
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

502 
 _ => raise THM("forall_elim_var", i, [th]) 
0  503 
end; 
504 

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

506 
fun forall_elim_vars i th = 
0  507 
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

508 
handle THM _ => th; 
0  509 

510 
(*Specialization over a list of cterms*) 

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

512 

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

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

515 

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

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

518 

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

520 
fun zero_var_indexes th = 
0  521 
let val {prop,sign,...} = rep_thm th; 
522 
val vars = term_vars prop 

523 
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

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

525 
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

526 
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

527 
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

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

529 
 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

530 
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

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

532 
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

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

534 
 varpairs _ = raise TERM("varpairs", []); 
0  535 
in instantiate (ctye, varpairs(vars,rev bs)) th end; 
536 

537 

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

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

540 
fun standard th = 

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

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

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

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

548 

0  549 

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

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

553 
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

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

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

557 
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

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

559 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  560 

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

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

564 
([th],_) => th 

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

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

567 

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

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

570 

571 
(*For joining lists of rules*) 

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

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

575 
in flat (map resb thbs) end; 

576 

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

578 

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

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

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

581 
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

582 
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

583 
 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

584 
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

585 

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

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

587 
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

588 
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

589 
 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

590 
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

591 

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

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

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

595 
fun compose(tha,i,thb) = 
0  596 
Sequence.list_of_s (bicompose false (false,tha,0) i thb); 
597 

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

599 
fun tha COMP thb = 

600 
case compose(tha,1,thb) of 

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

601 
[th] => th 
0  602 
 _ => raise THM("COMP", 1, [tha,thb]); 
603 

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

605 
fun read_instantiate_sg sg sinsts th = 

606 
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

607 
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

608 
in instantiate (read_insts sg ts ts used sinsts) th end; 
0  609 

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

611 
fun read_instantiate sinsts th = 

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

613 

614 

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

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

617 
local 

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

618 
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

619 
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

620 
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

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

623 
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

624 
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

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

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

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

631 
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

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

634 
handle TERM _ => 
0  635 
raise THM("cterm_instantiate: incompatible signatures",0,[th]) 
636 
 TYPE _ => raise THM("cterm_instantiate: types", 0, [th]) 

637 
end; 

638 

639 

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

641 

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

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

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

645 
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

646 
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

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

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

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

650 
prop1 aconv prop2 
0  651 
end; 
652 

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

655 
version of this theory*) 

656 
fun same_thm (th1,th2) = 

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

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

659 
in Sign.same_sg (sg1,sg2) andalso 

660 
eq_set (shyps1, shyps2) andalso 

661 
aconvs(hyps1,hyps2) andalso 

662 
prop1 aconv prop2 

663 
end; 

664 

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

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

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

669 
val size_of_thm = size_of_term o #prop o rep_thm; 

670 

671 

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

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

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

674 

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

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

676 
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

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

678 
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

679 
 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

680 
 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

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

682 

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

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

684 
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

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

686 
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

687 

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

689 
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

690 

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

691 

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

692 

0  693 
(*** MetaRewriting Rules ***) 
694 

695 

696 
val reflexive_thm = 

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

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

700 
val symmetric_thm = 

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

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

704 
val transitive_thm = 

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

705 
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

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

709 

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

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

711 

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

712 
val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies); 
0  713 

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

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

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

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

718 
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

719 
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

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

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

722 
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

723 
handle TERM _ => reflexive ct 
0  724 
in gconv 1 end; 
725 

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

727 
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; 
0  728 

729 
(*rewriting conversion*) 

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

730 
fun rew_conv mode prover mss = rewrite_cterm mode mss prover; 
0  731 

732 
(*Rewrite a theorem*) 

1412  733 
fun rewrite_rule [] th = th 
734 
 rewrite_rule thms th = 

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

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

1412  738 
fun rewrite_goals_rule [] th = th 
739 
 rewrite_goals_rule thms th = 

1460  740 
fconv_rule (goals_conv (K true) 
741 
(rew_conv (true,false) (K(K None)) 

742 
(Thm.mss_of thms))) 

743 
th; 

0  744 

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

746 
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

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

748 
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

749 
else raise THM("rewrite_goal_rule",i,[thm]); 
0  750 

751 

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

753 

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

755 
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

756 
let val {sign=signa, t=a, ...} = rep_cterm ca 
0  757 
and combth = combination eqth (reflexive ca) 
758 
val {sign,prop,...} = rep_thm eqth 

759 
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

760 
val cterm = cterm_of (Sign.merge (sign,signa)) 
0  761 
in transitive (symmetric (beta_conversion (cterm (abst$a)))) 
762 
(transitive combth (beta_conversion (cterm (absu$a)))) 

763 
end 

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

765 

766 
(*Calling equal_abs_elim with multiple terms*) 

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

768 

769 
local 

770 
open Logic 

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

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

773 
fun flexpair_inst def th = 

774 
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

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

776 
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

777 
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

778 
def 
0  779 
in equal_elim def' th 
780 
end 

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

782 
in 

783 
val flexpair_intr = flexpair_inst (symmetric flexpair_def) 

784 
and flexpair_elim = flexpair_inst flexpair_def 

785 
end; 

786 

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

788 
fun flexpair_abs_elim_list cts = 
0  789 
flexpair_intr o equal_abs_elim_list cts o flexpair_elim; 
790 

791 

792 
(*** Some useful metatheorems ***) 

793 

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

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

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

798 
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

799 
("PROP ?psi ==> PROP ?theta", propT)); 
0  800 

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

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

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

804 
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

805 
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

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

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

808 
(implies_elim (assume VW) (assume V)))) 
0  809 
end; 
810 

668  811 
(*for deleting an unwanted assumption*) 
812 
val thin_rl = 

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

813 
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

814 
and W = read_cterm Sign.proto_pure ("PROP W", propT); 
668  815 
in standard (implies_intr V (implies_intr W (assume W))) 
816 
end; 

817 

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

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

820 
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

821 
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

822 
and x = read_cterm Sign.proto_pure ("x", TFree("'a",logicS)); 
0  823 
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

824 
(implies_intr V (forall_intr x (assume V)))) 
0  825 
end; 
826 

827 
end 

828 
end; 

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

829 