author  wenzelm 
Tue, 29 Sep 2009 22:48:24 +0200  
changeset 32765  3032c0308019 
parent 32026  9898880061df 
child 32784  1a5dde5079ac 
permissions  rwrr 
9460  1 
(* Title: Pure/logic.ML 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

29276  3 
Author: Makarius 
0  4 

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

9460  8 
signature LOGIC = 
4345  9 
sig 
27334  10 
val all: term > term > term 
11 
val is_all: term > bool 

12 
val dest_all: term > (string * typ) * term 

18181  13 
val mk_equals: term * term > term 
14 
val dest_equals: term > term * term 

27334  15 
val implies: term 
18181  16 
val mk_implies: term * term > term 
17 
val dest_implies: term > term * term 

18 
val list_implies: term list * term > term 

19 
val strip_imp_prems: term > term list 

20 
val strip_imp_concl: term > term 

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

21576  22 
val count_prems: term > int 
18181  23 
val nth_prem: int * term > term 
23418  24 
val true_prop: 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 
23418  28 
val mk_conjunction_balanced: term list > term 
18469  29 
val dest_conjunction: term > term * term 
19425  30 
val dest_conjunction_list: term > term list 
23418  31 
val dest_conjunction_balanced: int > term > term list 
18469  32 
val dest_conjunctions: term > term list 
18181  33 
val strip_horn: term > term list * term 
21520  34 
val mk_type: typ > term 
18938  35 
val dest_type: term > typ 
21520  36 
val type_map: (term > term) > typ > typ 
18938  37 
val const_of_class: class > string 
38 
val class_of_const: string > class 

31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

39 
val mk_of_class: typ * class > term 
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

40 
val dest_of_class: term > typ * class 
20630  41 
val name_classrel: string * string > string 
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

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

43 
val dest_classrel: term > class * class 
20630  44 
val name_arities: arity > string list 
45 
val name_arity: string * sort list * class > string 

46 
val mk_arities: arity > term list 

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

47 
val dest_arity: term > string * sort list * class 
18181  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 

32023  57 
val incr_tvar_same: int > typ Same.operation 
58 
val incr_tvar: int > typ > typ 

32026  59 
val incr_indexes_same: typ list * int > term Same.operation 
18181  60 
val incr_indexes: typ list * int > term > term 
61 
val lift_abs: int > term > term > term 

62 
val lift_all: int > term > term > term 

63 
val strip_assums_hyp: term > term list 

9460  64 
val strip_assums_concl: term > term 
18181  65 
val strip_params: term > (string * typ) list 
23597  66 
val has_meta_prems: term > bool 
18181  67 
val flatten_params: int > term > term 
0  68 
val list_rename_params: string list * term > term 
18181  69 
val assum_pairs: int * term > (term*term)list 
30554
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

70 
val assum_problems: int * term > (term > term) * term list * term 
19806  71 
val varifyT: typ > typ 
72 
val unvarifyT: typ > typ 

18181  73 
val varify: term > term 
74 
val unvarify: term > term 

75 
val get_goal: term > int > term 

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

77 
val prems_of_goal: term > int > term list 

78 
val concl_of_goal: term > int > term 

4345  79 
end; 
0  80 

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

83 

4345  84 

0  85 
(*** Abstract syntax operations on the metaconnectives ***) 
86 

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

88 

27334  89 
fun all v t = Const ("all", (Term.fastype_of v > propT) > propT) $ lambda v t; 
90 

91 
fun is_all (Const ("all", _) $ Abs _) = true 

92 
 is_all _ = false; 

93 

94 
fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) = 

95 
let val (x, b) = Term.dest_abs abs (*potentially slow*) 

96 
in ((x, T), b) end 

18762  97 
 dest_all t = raise TERM ("dest_all", [t]); 
98 

99 

0  100 
(** equality **) 
101 

27334  102 
fun mk_equals (t, u) = 
103 
let val T = Term.fastype_of t 

104 
in Const ("==", T > T > propT) $ t $ u end; 

0  105 

20883  106 
fun dest_equals (Const ("==", _) $ t $ u) = (t, u) 
107 
 dest_equals t = raise TERM ("dest_equals", [t]); 

637  108 

109 

0  110 
(** implies **) 
111 

27334  112 
val implies = Const ("==>", propT > propT > propT); 
113 

20883  114 
fun mk_implies (A, B) = implies $ A $ B; 
0  115 

20883  116 
fun dest_implies (Const ("==>", _) $ A $ B) = (A, B) 
117 
 dest_implies A = raise TERM ("dest_implies", [A]); 

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

118 

4822  119 

0  120 
(** nested implications **) 
121 

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

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

0  125 

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

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

128 
 strip_imp_prems _ = []; 

129 

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

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

132 
 strip_imp_concl A = A : term; 

133 

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

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

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

0  140 
 strip_prems (_, As, A) = raise TERM("strip_prems", A::As); 
141 

16130  142 
(*Count premises  quicker than (length o strip_prems) *) 
21576  143 
fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B 
144 
 count_prems _ = 0; 

0  145 

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

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

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

150 

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

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

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

153 
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

154 

4822  155 

23418  156 

12137  157 
(** conjunction **) 
158 

23418  159 
val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)); 
26424  160 
val conjunction = Const ("Pure.conjunction", propT > propT > propT); 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

161 

23418  162 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

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

164 
fun mk_conjunction (A, B) = conjunction $ A $ B; 
12137  165 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

166 
(*A &&& B &&& C  improper*) 
23418  167 
fun mk_conjunction_list [] = true_prop 
12757  168 
 mk_conjunction_list ts = foldr1 mk_conjunction ts; 
12137  169 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

170 
(*(A &&& B) &&& (C &&& D)  balanced*) 
23418  171 
fun mk_conjunction_balanced [] = true_prop 
32765  172 
 mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts; 
23418  173 

18499  174 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

175 
(*A &&& B*) 
26424  176 
fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B) 
18469  177 
 dest_conjunction t = raise TERM ("dest_conjunction", [t]); 
178 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

179 
(*A &&& B &&& C  improper*) 
19425  180 
fun dest_conjunction_list t = 
181 
(case try dest_conjunction t of 

182 
NONE => [t] 

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

184 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

185 
(*(A &&& B) &&& (C &&& D)  balanced*) 
23418  186 
fun dest_conjunction_balanced 0 _ = [] 
32765  187 
 dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t; 
23418  188 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

189 
(*((A &&& B) &&& C) &&& D &&& E  flat*) 
18469  190 
fun dest_conjunctions t = 
191 
(case try dest_conjunction t of 

192 
NONE => [t] 

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

194 

195 

12137  196 

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

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

198 

19391  199 
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

200 

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

201 
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

202 
 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

203 

21520  204 
fun type_map f = dest_type o f o mk_type; 
205 

4822  206 

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

207 

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

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

209 

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

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

211 

18938  212 
val classN = "_class"; 
213 

214 
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

215 

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

218 

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

219 

31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

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

221 

31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

222 
fun mk_of_class (ty, c) = 
19391  223 
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

224 

31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

225 
fun dest_of_class (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) 
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

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

227 

0  228 

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

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

230 

20630  231 
fun name_classrel (c1, c2) = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

232 
Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2; 
20630  233 

31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

234 
fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2); 
19406
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 
fun dest_classrel tm = 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

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

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

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

240 

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

241 

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

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

243 

20630  244 
fun name_arities (t, _, S) = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

245 
let val b = Long_Name.base_name t 
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

246 
in S > map (fn c => Long_Name.base_name c ^ "_" ^ b) end; 
20630  247 

248 
fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); 

249 

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

250 
fun mk_arities (t, Ss, S) = 
24848  251 
let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss)) 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

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

253 

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

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

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

256 
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

257 

31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset

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

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

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

261 
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

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

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

264 
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

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

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

267 

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

268 

18938  269 

28448  270 
(** protected propositions and embedded terms **) 
9460  271 

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

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

273 
fun protect t = protectC $ t; 
9460  274 

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

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

276 
 unprotect t = raise TERM ("unprotect", [t]); 
9460  277 

278 

26424  279 
fun mk_term t = Const ("Pure.term", Term.fastype_of t > propT) $ t; 
19775  280 

26424  281 
fun dest_term (Const ("Pure.term", _) $ t) = t 
19775  282 
 dest_term t = raise TERM ("dest_term", [t]); 
283 

284 

18181  285 

0  286 
(*** Lowlevel term operations ***) 
287 

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

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

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

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

293 
fun close_form A = 

19425  294 
Term.list_all_free (rev (Term.add_frees A []), A); 
0  295 

296 

18938  297 

0  298 
(*** Specialized operations for resolution... ***) 
299 

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

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

303 

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

305 
fun rlist_abs ([], body) = body 

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

307 

32026  308 
fun incr_tvar_same 0 = Same.same 
309 
 incr_tvar_same k = Term_Subst.map_atypsT_same 

310 
(fn TVar ((a, i), S) => TVar ((a, i + k), S) 

311 
 _ => raise Same.SAME); 

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

312 

32026  313 
fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T; 
32023  314 

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

32026  317 
fun incr_indexes_same ([], 0) = Same.same 
318 
 incr_indexes_same (Ts, k) = 

32020  319 
let 
320 
val n = length Ts; 

32026  321 
val incrT = incr_tvar_same k; 
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

322 

32020  323 
fun incr lev (Var ((x, i), T)) = 
324 
combound (Var ((x, i + k), Ts > Same.commit incrT T), lev, n) 

325 
 incr lev (Abs (x, T, body)) = 

326 
(Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body) 

327 
handle Same.SAME => Abs (x, T, incr (lev + 1) body)) 

328 
 incr lev (t $ u) = 

329 
(incr lev t $ (incr lev u handle Same.SAME => u) 

330 
handle Same.SAME => t $ incr lev u) 

331 
 incr _ (Const (c, T)) = Const (c, incrT T) 

332 
 incr _ (Free (x, T)) = Free (x, incrT T) 

32026  333 
 incr _ (Bound _) = raise Same.SAME; 
334 
in incr 0 end; 

335 

336 
fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t; 

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

337 

0  338 

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

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

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

342 

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

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

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

345 
fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t 
18248  346 
 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

347 
 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

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

349 

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

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

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

352 
fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t 
18248  353 
 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

354 
 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

355 
in lift [] end; 
0  356 

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

21016
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

358 
fun strip_assums_hyp B = 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

359 
let 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

360 
fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

361 
 strip Hs (Const ("all", _) $ Abs (a, T, t)) = 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

362 
strip (map (incr_boundvars 1) Hs) t 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

363 
 strip Hs B = rev Hs 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

364 
in strip [] B end; 
0  365 

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

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

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

369 
 strip_assums_concl B = B; 

370 

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

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

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

374 
 strip_params B = []; 

375 

23597  376 
(*test for nested meta connectives in prems*) 
377 
val has_meta_prems = 

9667  378 
let 
23597  379 
fun is_meta (Const ("==", _) $ _ $ _) = true 
380 
 is_meta (Const ("==>", _) $ _ $ _) = true 

9667  381 
 is_meta (Const ("all", _) $ _) = true 
382 
 is_meta _ = false; 

23597  383 
fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B 
384 
 ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B 

385 
 ex_meta _ = false; 

386 
in ex_meta end; 

9483  387 

0  388 
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, 
9460  389 
where j is the total number of parameters (precomputed) 
0  390 
If n>0 then deletes assumption n. *) 
9460  391 
fun remove_params j n A = 
0  392 
if j=0 andalso n<=0 then A (*nothing left to do...*) 
393 
else case A of 

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

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

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

399 
else A; 

400 

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

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

403 
fun flatten_params n A = 

404 
let val params = strip_params A; 

25939  405 
val vars = ListPair.zip (Name.variant_list [] (map #1 params), 
406 
map #2 params) 

0  407 
in list_all (vars, remove_params (length vars) n A) 
408 
end; 

409 

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

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

412 
implies $ A $ list_rename_params (cs, B) 

27334  413 
 list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) = 
414 
a $ Abs(c, T, list_rename_params (cs, t)) 

0  415 
 list_rename_params (cs, B) = B; 
416 

32008  417 

418 

19806  419 
(*** Treatment of "assume", "erule", etc. ***) 
0  420 

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

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

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

423 
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

424 
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

425 
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

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

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

430 
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

431 
 strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = 
15454  432 
strip_assums_imp (nasms1, H::Hs, B) 
433 
 strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) 

434 

32008  435 
(*Strips OUTER parameters only.*) 
15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

436 
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

437 
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

438 
 strip_assums_all (params, B) = (params, B); 
0  439 

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

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

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

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

445 
fun assum_pairs(nasms,A) = 

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

446 
let val (params, A') = strip_assums_all ([],A) 
15454  447 
val (Hs,B) = strip_assums_imp (nasms,[],A') 
18938  448 
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

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

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

451 
 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

452 
in pairrev (Hs,[]) 
0  453 
end; 
454 

30554
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

455 
fun assum_problems (nasms, A) = 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

456 
let 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

457 
val (params, A') = strip_assums_all ([], A) 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

458 
val (Hs, B) = strip_assums_imp (nasms, [], A') 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

459 
fun abspar t = rlist_abs (params, t) 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

460 
in (abspar, rev Hs, B) end; 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

461 

19806  462 

463 
(* global schematic variables *) 

464 

465 
fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi); 

466 
fun bad_fixed x = "Illegal fixed variable: " ^ quote x; 

467 

32020  468 
fun varifyT_same ty = ty 
469 
> Term_Subst.map_atypsT_same 

470 
(fn TFree (a, S) => TVar ((a, 0), S) 

31981
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset

471 
 TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])); 
19806  472 

32020  473 
fun unvarifyT_same ty = ty 
474 
> Term_Subst.map_atypsT_same 

475 
(fn TVar ((a, 0), S) => TFree (a, S) 

31981
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset

476 
 TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []) 
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset

477 
 TFree (a, _) => raise TYPE (bad_fixed a, [ty], [])); 
0  478 

32020  479 
val varifyT = Same.commit varifyT_same; 
480 
val unvarifyT = Same.commit unvarifyT_same; 

31981
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset

481 

9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset

482 
fun varify tm = tm 
32020  483 
> Same.commit (Term_Subst.map_aterms_same 
484 
(fn Free (x, T) => Var ((x, 0), T) 

19806  485 
 Var (xi, _) => raise TERM (bad_schematic xi, [tm]) 
32020  486 
 _ => raise Same.SAME)) 
487 
> Same.commit (Term_Subst.map_types_same varifyT_same) 

19879  488 
handle TYPE (msg, _, _) => raise TERM (msg, [tm]); 
19806  489 

31981
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset

490 
fun unvarify tm = tm 
32020  491 
> Same.commit (Term_Subst.map_aterms_same 
492 
(fn Var ((x, 0), T) => Free (x, T) 

19806  493 
 Var (xi, _) => raise TERM (bad_schematic xi, [tm]) 
494 
 Free (x, _) => raise TERM (bad_fixed x, [tm]) 

32020  495 
 _ => raise Same.SAME)) 
496 
> Same.commit (Term_Subst.map_types_same unvarifyT_same) 

19879  497 
handle TYPE (msg, _, _) => raise TERM (msg, [tm]); 
19806  498 

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

499 

16862  500 
(* goal states *) 
501 

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

503 
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

504 

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

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

506 
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

507 
let val gi = get_goal st i 
29276  508 
val rfrees = map Free (Term.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

509 
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

510 

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

511 
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

512 
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

513 
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

514 
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

515 

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

516 
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

517 
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

518 
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

519 
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

520 

0  521 
end; 