author  wenzelm 
Mon, 05 Jun 2006 21:54:21 +0200  
changeset 19775  06cb6743adf6 
parent 19425  e0d7d9373faf 
child 19806  f860b7a98445 
permissions  rwrr 
9460  1 
(* Title: Pure/logic.ML 
0  2 
ID: $Id$ 
9460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright Cambridge University 1992 
5 

9460  6 
Abstract syntax operations of the Pure metalogic. 
0  7 
*) 
8 

9460  9 
signature LOGIC = 
4345  10 
sig 
18181  11 
val is_all: term > bool 
18762  12 
val dest_all: term > typ * term 
18181  13 
val mk_equals: term * term > term 
14 
val dest_equals: term > term * term 

15 
val is_equals: term > bool 

16 
val mk_implies: term * term > term 

17 
val dest_implies: term > term * term 

18 
val is_implies: term > bool 

19 
val list_implies: term list * term > term 

20 
val strip_imp_prems: term > term list 

21 
val strip_imp_concl: term > term 

22 
val strip_prems: int * term list * term > term list * term 

23 
val count_prems: term * int > int 

24 
val nth_prem: int * term > term 

19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

25 
val conjunction: term 
18181  26 
val mk_conjunction: term * term > term 
12757  27 
val mk_conjunction_list: term list > term 
18499  28 
val mk_conjunction_list2: term list list > term 
18469  29 
val dest_conjunction: term > term * term 
19425  30 
val dest_conjunction_list: term > term list 
18469  31 
val dest_conjunctions: term > term list 
18181  32 
val strip_horn: term > term list * term 
18938  33 
val dest_type: term > typ 
34 
val const_of_class: class > string 

35 
val class_of_const: string > class 

36 
val mk_inclass: typ * class > term 

37 
val dest_inclass: term > typ * class 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

38 
val mk_classrel: class * class > term 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

39 
val dest_classrel: term > class * class 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

40 
val mk_arities: string * sort list * sort > term list 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

41 
val dest_arity: term > string * sort list * class 
18938  42 
val dest_def: Pretty.pp > (term > bool) > (string > bool) > (string > bool) > 
43 
term > (term * term) * term 

44 
val abs_def: term > term * term 

18181  45 
val mk_cond_defpair: term list > term * term > string * term 
46 
val mk_defpair: term * term > string * term 

47 
val mk_type: typ > term 

48 
val protectC: term 

49 
val protect: term > term 

50 
val unprotect: term > term 

19775  51 
val mk_term: term > term 
52 
val dest_term: term > term 

18181  53 
val occs: term * term > bool 
54 
val close_form: term > term 

18938  55 
val combound: term * int * int > term 
56 
val rlist_abs: (string * typ) list * term > term 

18181  57 
val incr_indexes: typ list * int > term > term 
58 
val incr_tvar: int > typ > typ 

59 
val lift_abs: int > term > term > term 

60 
val lift_all: int > term > term > term 

61 
val strip_assums_hyp: term > term list 

9460  62 
val strip_assums_concl: term > term 
18181  63 
val strip_params: term > (string * typ) list 
64 
val has_meta_prems: term > int > bool 

65 
val flatten_params: int > term > term 

66 
val auto_rename: bool ref 

67 
val set_rename_prefix: string > unit 

0  68 
val list_rename_params: string list * term > term 
18181  69 
val assum_pairs: int * term > (term*term)list 
70 
val varify: term > term 

71 
val unvarify: term > term 

72 
val get_goal: term > int > term 

73 
val goal_params: term > int > term * term list 

74 
val prems_of_goal: term > int > term list 

75 
val concl_of_goal: term > int > term 

4345  76 
end; 
0  77 

1500  78 
structure Logic : LOGIC = 
0  79 
struct 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

80 

4345  81 

0  82 
(*** Abstract syntax operations on the metaconnectives ***) 
83 

5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

84 
(** all **) 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

85 

a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

86 
fun is_all (Const ("all", _) $ _) = true 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

87 
 is_all _ = false; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

88 

18762  89 
fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A) 
90 
 dest_all t = raise TERM ("dest_all", [t]); 

91 

92 

5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

93 

0  94 
(** equality **) 
95 

1835  96 
(*Make an equality. DOES NOT CHECK TYPE OF u*) 
64
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset

97 
fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; 
0  98 

99 
fun dest_equals (Const("==",_) $ t $ u) = (t,u) 

100 
 dest_equals t = raise TERM("dest_equals", [t]); 

101 

637  102 
fun is_equals (Const ("==", _) $ _ $ _) = true 
103 
 is_equals _ = false; 

104 

105 

0  106 
(** implies **) 
107 

108 
fun mk_implies(A,B) = implies $ A $ B; 

109 

110 
fun dest_implies (Const("==>",_) $ A $ B) = (A,B) 

111 
 dest_implies A = raise TERM("dest_implies", [A]); 

112 

5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

113 
fun is_implies (Const ("==>", _) $ _ $ _) = true 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

114 
 is_implies _ = false; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

115 

4822  116 

0  117 
(** nested implications **) 
118 

119 
(* [A1,...,An], B goes to A1==>...An==>B *) 

18181  120 
fun list_implies ([], B) = B 
121 
 list_implies (A::As, B) = implies $ A $ list_implies(As,B); 

0  122 

123 
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 

124 
fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B 

125 
 strip_imp_prems _ = []; 

126 

127 
(* A1==>...An==>B goes to B, where B is not an implication *) 

128 
fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B 

129 
 strip_imp_concl A = A : term; 

130 

131 
(*Strip and return premises: (i, [], A1==>...Ai==>B) 

9460  132 
goes to ([Ai, A(i1),...,A1] , B) (REVERSED) 
0  133 
if i<0 or else i too big then raises TERM*) 
9460  134 
fun strip_prems (0, As, B) = (As, B) 
135 
 strip_prems (i, As, Const("==>", _) $ A $ B) = 

136 
strip_prems (i1, A::As, B) 

0  137 
 strip_prems (_, As, A) = raise TERM("strip_prems", A::As); 
138 

16130  139 
(*Count premises  quicker than (length o strip_prems) *) 
0  140 
fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1) 
141 
 count_prems (_,n) = n; 

142 

16130  143 
(*Select Ai from A1 ==>...Ai==>B*) 
144 
fun nth_prem (1, Const ("==>", _) $ A $ _) = A 

145 
 nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i  1, B) 

146 
 nth_prem (_, A) = raise TERM ("nth_prem", [A]); 

147 

13659
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

148 
(*strip a proof state (Horn clause): 
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

149 
B1 ==> ... Bn ==> C goes to ([B1, ..., Bn], C) *) 
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

150 
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); 
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

151 

4822  152 

12137  153 
(** conjunction **) 
154 

19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

155 
val conjunction = Const ("ProtoPure.conjunction", propT > propT > propT); 
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

156 

18499  157 
(*A && B*) 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

158 
fun mk_conjunction (A, B) = conjunction $ A $ B; 
12137  159 

18499  160 
(*A && B && C  improper*) 
12757  161 
fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)) 
162 
 mk_conjunction_list ts = foldr1 mk_conjunction ts; 

12137  163 

18499  164 
(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3  improper*) 
165 
fun mk_conjunction_list2 tss = 

166 
mk_conjunction_list (map mk_conjunction_list (filter_out null tss)); 

167 

168 
(*A && B*) 

19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

169 
fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B) 
18469  170 
 dest_conjunction t = raise TERM ("dest_conjunction", [t]); 
171 

19425  172 
(*A && B && C  improper*) 
173 
fun dest_conjunction_list t = 

174 
(case try dest_conjunction t of 

175 
NONE => [t] 

176 
 SOME (A, B) => A :: dest_conjunction_list B); 

177 

18499  178 
(*((A && B) && C) && D && E  flat*) 
18469  179 
fun dest_conjunctions t = 
180 
(case try dest_conjunction t of 

181 
NONE => [t] 

182 
 SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); 

183 

184 

12137  185 

398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

186 
(** types as terms **) 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

187 

19391  188 
fun mk_type ty = Const ("TYPE", Term.itselfT ty); 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

189 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

190 
fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

191 
 dest_type t = raise TERM ("dest_type", [t]); 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

192 

4822  193 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

194 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

195 
(** type classes **) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

196 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

197 
(* const names *) 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

198 

18938  199 
val classN = "_class"; 
200 

201 
val const_of_class = suffix classN; 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

202 

18938  203 
fun class_of_const c = unsuffix classN c 
204 
handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []); 

205 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

206 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

207 
(* class constraints *) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

208 

398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

209 
fun mk_inclass (ty, c) = 
19391  210 
Const (const_of_class c, Term.itselfT ty > propT) $ mk_type ty; 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

211 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

212 
fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

213 
 dest_inclass t = raise TERM ("dest_inclass", [t]); 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

214 

0  215 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

216 
(* class relations *) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

217 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

218 
fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2); 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

219 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

220 
fun dest_classrel tm = 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

221 
(case dest_inclass tm of 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

222 
(TVar (_, [c1]), c2) => (c1, c2) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

223 
 _ => raise TERM ("dest_classrel", [tm])); 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

224 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

225 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

226 
(* type arities *) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

227 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

228 
fun mk_arities (t, Ss, S) = 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

229 
let val T = Type (t, ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss)) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

230 
in map (fn c => mk_inclass (T, c)) S end; 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

231 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

232 
fun dest_arity tm = 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

233 
let 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

234 
fun err () = raise TERM ("dest_arity", [tm]); 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

235 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

236 
val (ty, c) = dest_inclass tm; 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

237 
val (t, tvars) = 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

238 
(case ty of 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

239 
Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ()) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

240 
 _ => err ()); 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

241 
val Ss = 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

242 
if has_duplicates (eq_fst (op =)) tvars then err () 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

243 
else map snd tvars; 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

244 
in (t, Ss, c) end; 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

245 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

246 

18938  247 

248 
(** definitions **) 

249 

19103  250 
fun term_kind (Const _) = "existing constant " 
251 
 term_kind (Free _) = "free variable " 

252 
 term_kind (Bound _) = "bound variable " 

253 
 term_kind _ = ""; 

254 

18938  255 
(*c x == t[x] to !!x. c x == t[x]*) 
256 
fun dest_def pp check_head is_fixed is_fixedT eq = 

257 
let 

258 
fun err msg = raise TERM (msg, [eq]); 

19071
fdffd7c40864
dest_def: actually return betaeta contracted equation;
wenzelm
parents:
18964
diff
changeset

259 
val eq_vars = Term.strip_all_vars eq; 
fdffd7c40864
dest_def: actually return betaeta contracted equation;
wenzelm
parents:
18964
diff
changeset

260 
val eq_body = Term.strip_all_body eq; 
fdffd7c40864
dest_def: actually return betaeta contracted equation;
wenzelm
parents:
18964
diff
changeset

261 

fdffd7c40864
dest_def: actually return betaeta contracted equation;
wenzelm
parents:
18964
diff
changeset

262 
val display_terms = commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars); 
18938  263 
val display_types = commas_quote o map (Pretty.string_of_typ pp); 
264 

19071
fdffd7c40864
dest_def: actually return betaeta contracted equation;
wenzelm
parents:
18964
diff
changeset

265 
val (raw_lhs, rhs) = dest_equals eq_body handle TERM _ => err "Not a metaequality (==)"; 
fdffd7c40864
dest_def: actually return betaeta contracted equation;
wenzelm
parents:
18964
diff
changeset

266 
val lhs = Envir.beta_eta_contract raw_lhs; 
fdffd7c40864
dest_def: actually return betaeta contracted equation;
wenzelm
parents:
18964
diff
changeset

267 
val (head, args) = Term.strip_comb lhs; 
18938  268 
val head_tfrees = Term.add_tfrees head []; 
269 

270 
fun check_arg (Bound _) = true 

271 
 check_arg (Free (x, _)) = not (is_fixed x) 

272 
 check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true 

273 
 check_arg _ = false; 

274 
fun close_arg (Bound _) t = t 

275 
 close_arg x t = Term.all (Term.fastype_of x) $ lambda x t; 

276 

277 
val lhs_bads = filter_out check_arg args; 

18964  278 
val lhs_dups = duplicates (op aconv) args; 
18938  279 
val rhs_extras = Term.fold_aterms (fn v as Free (x, _) => 
280 
if is_fixed x orelse member (op aconv) args v then I 

281 
else insert (op aconv) v  _ => I) rhs []; 

282 
val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) => 

283 
if is_fixedT a orelse member (op =) head_tfrees (a, S) then I 

284 
else insert (op =) v  _ => I)) rhs []; 

285 
in 

286 
if not (check_head head) then 

19103  287 
err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head]) 
18938  288 
else if not (null lhs_bads) then 
289 
err ("Bad arguments on lhs: " ^ display_terms lhs_bads) 

290 
else if not (null lhs_dups) then 

291 
err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups) 

292 
else if not (null rhs_extras) then 

293 
err ("Extra variables on rhs: " ^ display_terms rhs_extras) 

294 
else if not (null rhs_extrasT) then 

295 
err ("Extra type variables on rhs: " ^ display_types rhs_extrasT) 

296 
else if exists_subterm (fn t => t aconv head) rhs then 

297 
err "Entity to be defined occurs on rhs" 

19071
fdffd7c40864
dest_def: actually return betaeta contracted equation;
wenzelm
parents:
18964
diff
changeset

298 
else ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (mk_equals (lhs, rhs))))) 
18938  299 
end; 
300 

301 
(*!!x. c x == t[x] to c == %x. t[x]*) 

302 
fun abs_def eq = 

303 
let 

304 
val body = Term.strip_all_body eq; 

305 
val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); 

306 
val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body)); 

307 
val (lhs', args) = Term.strip_comb lhs; 

308 
val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs); 

309 
in (lhs', rhs') end; 

310 

311 
fun mk_cond_defpair As (lhs, rhs) = 

312 
(case Term.head_of lhs of 

313 
Const (name, _) => 

314 
(NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs))) 

315 
 _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); 

316 

317 
fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs; 

318 

319 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

320 

19775  321 
(** protected propositions and embedded terms **) 
9460  322 

18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

323 
val protectC = Const ("prop", propT > propT); 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

324 
fun protect t = protectC $ t; 
9460  325 

18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

326 
fun unprotect (Const ("prop", _) $ t) = t 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

327 
 unprotect t = raise TERM ("unprotect", [t]); 
9460  328 

329 

19775  330 
fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t > propT) $ t; 
331 

332 
fun dest_term (Const ("ProtoPure.term", _) $ t) = t 

333 
 dest_term t = raise TERM ("dest_term", [t]); 

334 

335 

18181  336 

0  337 
(*** Lowlevel term operations ***) 
338 

339 
(*Does t occur in u? Or is alphaconvertible to u? 

340 
The term t must contain no loose bound variables*) 

16846  341 
fun occs (t, u) = exists_subterm (fn s => t aconv s) u; 
0  342 

343 
(*Close up a formula over all free variables by quantification*) 

344 
fun close_form A = 

19425  345 
Term.list_all_free (rev (Term.add_frees A []), A); 
0  346 

347 

18938  348 

0  349 
(*** Specialized operations for resolution... ***) 
350 

18938  351 
(*computes t(Bound(n+k1),...,Bound(n)) *) 
352 
fun combound (t, n, k) = 

353 
if k>0 then combound (t,n+1,k1) $ (Bound n) else t; 

354 

355 
(* ([xn,...,x1], t) ======> (x1,...,xn)t *) 

356 
fun rlist_abs ([], body) = body 

357 
 rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); 

358 

359 

16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

360 
local exception SAME in 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

361 

b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

362 
fun incrT k = 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

363 
let 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

364 
fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

365 
 incr (Type (a, Ts)) = Type (a, incrs Ts) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

366 
 incr _ = raise SAME 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

367 
and incrs (T :: Ts) = 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

368 
(incr T :: (incrs Ts handle SAME => Ts) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

369 
handle SAME => T :: incrs Ts) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

370 
 incrs [] = raise SAME; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

371 
in incr end; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

372 

0  373 
(*For all variables in the term, increment indexnames and lift over the Us 
374 
result is ?Gidx(B.(lev+n1),...,B.lev) where lev is abstraction level *) 

17120  375 
fun incr_indexes ([], 0) t = t 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

376 
 incr_indexes (Ts, k) t = 
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

377 
let 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

378 
val n = length Ts; 
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

379 
val incrT = if k = 0 then I else incrT k; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

380 

b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

381 
fun incr lev (Var ((x, i), T)) = 
18938  382 
combound (Var ((x, i + k), Ts > (incrT T handle SAME => T)), lev, n) 
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

383 
 incr lev (Abs (x, T, body)) = 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

384 
(Abs (x, incrT T, incr (lev + 1) body handle SAME => body) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

385 
handle SAME => Abs (x, T, incr (lev + 1) body)) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

386 
 incr lev (t $ u) = 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

387 
(incr lev t $ (incr lev u handle SAME => u) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

388 
handle SAME => t $ incr lev u) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

389 
 incr _ (Const (c, T)) = Const (c, incrT T) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

390 
 incr _ (Free (x, T)) = Free (x, incrT T) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

391 
 incr _ (t as Bound _) = t; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

392 
in incr 0 t handle SAME => t end; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

393 

b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

394 
fun incr_tvar 0 T = T 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

395 
 incr_tvar k T = incrT k T handle SAME => T; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

396 

b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

397 
end; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

398 

0  399 

18248  400 
(* Lifting functions from subgoal and increment: 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

401 
lift_abs operates on terms 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

402 
lift_all operates on propositions *) 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

403 

19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

404 
fun lift_abs inc = 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

405 
let 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

406 
fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t 
18248  407 
 lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t) 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

408 
 lift Ts _ t = incr_indexes (rev Ts, inc) t; 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

409 
in lift [] end; 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

410 

19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

411 
fun lift_all inc = 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

412 
let 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

413 
fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t 
18248  414 
 lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t) 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

415 
 lift Ts _ t = incr_indexes (rev Ts, inc) t; 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

416 
in lift [] end; 
0  417 

418 
(*Strips assumptions in goal, yielding list of hypotheses. *) 

419 
fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B 

420 
 strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t 

421 
 strip_assums_hyp B = []; 

422 

423 
(*Strips assumptions in goal, yielding conclusion. *) 

424 
fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B 

425 
 strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t 

426 
 strip_assums_concl B = B; 

427 

428 
(*Make a list of all the parameters in a subgoal, even if nested*) 

429 
fun strip_params (Const("==>", _) $ H $ B) = strip_params B 

430 
 strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t 

431 
 strip_params B = []; 

432 

9667  433 
(*test for meta connectives in prems of a 'subgoal'*) 
434 
fun has_meta_prems prop i = 

435 
let 

436 
fun is_meta (Const ("==>", _) $ _ $ _) = true 

10442  437 
 is_meta (Const ("==", _) $ _ $ _) = true 
9667  438 
 is_meta (Const ("all", _) $ _) = true 
439 
 is_meta _ = false; 

440 
in 

13659
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

441 
(case strip_prems (i, [], prop) of 
9667  442 
(B :: _, _) => exists is_meta (strip_assums_hyp B) 
443 
 _ => false) handle TERM _ => false 

444 
end; 

9483  445 

0  446 
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, 
9460  447 
where j is the total number of parameters (precomputed) 
0  448 
If n>0 then deletes assumption n. *) 
9460  449 
fun remove_params j n A = 
0  450 
if j=0 andalso n<=0 then A (*nothing left to do...*) 
451 
else case A of 

9460  452 
Const("==>", _) $ H $ B => 
453 
if n=1 then (remove_params j (n1) B) 

454 
else implies $ (incr_boundvars j H) $ (remove_params j (n1) B) 

0  455 
 Const("all",_)$Abs(a,T,t) => remove_params (j1) n t 
456 
 _ => if n>0 then raise TERM("remove_params", [A]) 

457 
else A; 

458 

459 
(** Autorenaming of parameters in subgoals **) 

460 

461 
val auto_rename = ref false 

462 
and rename_prefix = ref "ka"; 

463 

464 
(*rename_prefix is not exported; it is set by this function.*) 

465 
fun set_rename_prefix a = 

4693  466 
if a<>"" andalso forall Symbol.is_letter (Symbol.explode a) 
0  467 
then (rename_prefix := a; auto_rename := true) 
468 
else error"rename prefix must be nonempty and consist of letters"; 

469 

470 
(*Makes parameters in a goal have distinctive names (not guaranteed unique!) 

471 
A name clash could cause the printer to rename bound vars; 

472 
then res_inst_tac would not work properly.*) 

473 
fun rename_vars (a, []) = [] 

474 
 rename_vars (a, (_,T)::vars) = 

12902  475 
(a,T) :: rename_vars (Symbol.bump_string a, vars); 
0  476 

477 
(*Move all parameters to the front of the subgoal, renaming them apart; 

478 
if n>0 then deletes assumption n. *) 

479 
fun flatten_params n A = 

480 
let val params = strip_params A; 

9460  481 
val vars = if !auto_rename 
482 
then rename_vars (!rename_prefix, params) 

483 
else ListPair.zip (variantlist(map #1 params,[]), 

484 
map #2 params) 

0  485 
in list_all (vars, remove_params (length vars) n A) 
486 
end; 

487 

488 
(*Makes parameters in a goal have the names supplied by the list cs.*) 

489 
fun list_rename_params (cs, Const("==>", _) $ A $ B) = 

490 
implies $ A $ list_rename_params (cs, B) 

9460  491 
 list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = 
0  492 
all T $ Abs(c, T, list_rename_params (cs, t)) 
493 
 list_rename_params (cs, B) = B; 

494 

15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

495 
(*** Treatmsent of "assume", "erule", etc. ***) 
0  496 

16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

497 
(*Strips assumptions in goal yielding 
15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

498 
HS = [Hn,...,H1], params = [xm,...,x1], and B, 
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

499 
where x1...xm are the parameters. This version (21.1.2005) REQUIRES 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

500 
the the parameters to be flattened, but it allows erule to work on 
15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

501 
assumptions of the form !!x. phi. Any !! after the outermost string 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

502 
will be regarded as belonging to the conclusion, and left untouched. 
15454  503 
Used ONLY by assum_pairs. 
504 
Unless nasms<0, it can terminate the recursion early; that allows 

505 
erule to work on assumptions of the form P==>Q.*) 

506 
fun strip_assums_imp (0, Hs, B) = (Hs, B) (*recursion terminated by nasms*) 

16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

507 
 strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = 
15454  508 
strip_assums_imp (nasms1, H::Hs, B) 
509 
 strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) 

510 

0  511 

15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

512 
(*Strips OUTER parameters only, unlike similar legacy versions.*) 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

513 
fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) = 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

514 
strip_assums_all ((a,T)::params, t) 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

515 
 strip_assums_all (params, B) = (params, B); 
0  516 

517 
(*Produces disagreement pairs, one for each assumption proof, in order. 

518 
A is the first premise of the lifted rule, and thus has the form 

15454  519 
H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B). 
520 
nasms is the number of assumptions in the original subgoal, needed when B 

521 
has the form B1 ==> B2: it stops B1 from being taken as an assumption. *) 

522 
fun assum_pairs(nasms,A) = 

15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

523 
let val (params, A') = strip_assums_all ([],A) 
15454  524 
val (Hs,B) = strip_assums_imp (nasms,[],A') 
18938  525 
fun abspar t = rlist_abs(params, t) 
15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

526 
val D = abspar B 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

527 
fun pairrev ([], pairs) = pairs 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

528 
 pairrev (H::Hs, pairs) = pairrev(Hs, (abspar H, D) :: pairs) 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

529 
in pairrev (Hs,[]) 
0  530 
end; 
531 

18938  532 
(*Converts Frees to Vars and TFrees to TVars*) 
16862  533 
fun varify (Const(a, T)) = Const (a, Type.varifyT T) 
534 
 varify (Free (a, T)) = Var ((a, 0), Type.varifyT T) 

535 
 varify (Var (ixn, T)) = Var (ixn, Type.varifyT T) 

536 
 varify (t as Bound _) = t 

537 
 varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body) 

538 
 varify (f $ t) = varify f $ varify t; 

0  539 

18938  540 
(*Inverse of varify.*) 
16862  541 
fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T) 
542 
 unvarify (Free (a, T)) = Free (a, Type.unvarifyT T) 

543 
 unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T) 

544 
 unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T) (*non0 index!*) 

545 
 unvarify (t as Bound _) = t 

546 
 unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body) 

547 
 unvarify (f $ t) = unvarify f $ unvarify t; 

546  548 

13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

549 

16862  550 
(* goal states *) 
551 

552 
fun get_goal st i = nth_prem (i, st) 

553 
handle TERM _ => error "Goal number out of range"; 

13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

554 

77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

555 
(*reverses parameters for substitution*) 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

556 
fun goal_params st i = 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

557 
let val gi = get_goal st i 
14137
c57ec95e7763
Removed extraneous rev in function goal_params (the list of parameters
berghofe
parents:
14107
diff
changeset

558 
val rfrees = map Free (rename_wrt_term gi (strip_params gi)) 
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

559 
in (gi, rfrees) end; 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

560 

77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

561 
fun concl_of_goal st i = 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

562 
let val (gi, rfrees) = goal_params st i 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

563 
val B = strip_assums_concl gi 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

564 
in subst_bounds (rfrees, B) end; 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

565 

77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

566 
fun prems_of_goal st i = 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

567 
let val (gi, rfrees) = goal_params st i 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

568 
val As = strip_assums_hyp gi 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

569 
in map (fn A => subst_bounds (rfrees, A)) As end; 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

570 

0  571 
end; 