author | wenzelm |
Thu, 28 Jul 2005 15:19:49 +0200 | |
changeset 16934 | 9ef19e3c7fdd |
parent 16857 | 6389511d4609 |
child 17203 | 29b2563f5c11 |
permissions | -rw-r--r-- |
15481 | 1 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
16179 | 2 |
(* Title: Pure/IsaPlanner/term_lib.ML |
3 |
ID: $Id$ |
|
15481 | 4 |
Author: Lucas Dixon, University of Edinburgh |
5 |
lucasd@dai.ed.ac.uk |
|
6 |
Created: 17 Aug 2002 |
|
7 |
*) |
|
8 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
9 |
(* DESCRIPTION: |
|
10 |
||
11 |
Additional code to work with terms. |
|
12 |
||
13 |
*) |
|
14 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
15 |
signature TERM_LIB = |
|
16 |
sig |
|
17 |
val fo_term_height : Term.term -> int |
|
18 |
val ho_term_height : Term.term -> int |
|
19 |
||
20 |
val current_sign : unit -> Sign.sg |
|
21 |
||
22 |
(* Matching/unification with exceptions handled *) |
|
23 |
val clean_match : Type.tsig -> Term.term * Term.term |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
24 |
-> ((Term.indexname * (Term.sort * Term.typ)) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
25 |
* (Term.indexname * (Term.typ * Term.term)) list) option |
15481 | 26 |
val clean_unify : Sign.sg -> int -> Term.term * Term.term |
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
27 |
-> ((Term.indexname * (Term.sort * Term.typ)) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
28 |
* (Term.indexname * (Term.typ * Term.term)) list) Seq.seq |
15481 | 29 |
|
30 |
(* managing variables in terms, can doing conversions *) |
|
31 |
val bounds_to_frees : Term.term -> Term.term |
|
32 |
val bounds_to_frees_with_vars : |
|
33 |
(string * Term.typ) list -> Term.term -> Term.term |
|
34 |
||
35 |
val change_bounds_to_frees : Term.term -> Term.term |
|
36 |
val change_frees_to_vars : Term.term -> Term.term |
|
37 |
val change_vars_to_frees : Term.term -> Term.term |
|
38 |
val loose_bnds_to_frees : |
|
39 |
(string * Term.typ) list -> Term.term -> Term.term |
|
40 |
||
41 |
(* make all variables named uniquely *) |
|
42 |
val unique_namify : Term.term -> Term.term |
|
43 |
||
44 |
(* breasking up a term and putting it into a normal form |
|
45 |
independent of internal term context *) |
|
46 |
val cleaned_term_conc : Term.term -> Term.term |
|
47 |
val cleaned_term_parts : Term.term -> Term.term list * Term.term |
|
48 |
val cterm_of_term : Term.term -> Thm.cterm |
|
49 |
||
50 |
(* terms of theorems and subgoals *) |
|
51 |
val term_of_thm : Thm.thm -> Term.term |
|
52 |
val get_prems_of_sg_term : Term.term -> Term.term list |
|
53 |
val triv_thm_from_string : string -> Thm.thm |
|
54 |
||
55 |
(* some common term manipulations *) |
|
56 |
val try_dest_Goal : Term.term -> Term.term |
|
57 |
val try_dest_Trueprop : Term.term -> Term.term |
|
58 |
||
59 |
val bot_left_leaf_of : Term.term -> Term.term |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
60 |
val bot_left_leaf_noabs_of : Term.term -> Term.term |
15481 | 61 |
|
62 |
(* term containing another term - an embedding check *) |
|
63 |
val term_contains : Term.term -> Term.term -> bool |
|
64 |
||
65 |
(* name-convertable checking - like ae-convertable, but allows for |
|
66 |
var's and free's to be mixed - and doesn't used buggy code. :-) *) |
|
67 |
val get_name_eq_member : Term.term -> Term.term list -> Term.term option |
|
68 |
val name_eq_member : Term.term -> Term.term list -> bool |
|
69 |
val term_name_eq : |
|
70 |
Term.term -> |
|
71 |
Term.term -> |
|
72 |
(Term.term * Term.term) list -> |
|
15531 | 73 |
(Term.term * Term.term) list option |
15481 | 74 |
|
75 |
(* is the typ a function or is it atomic *) |
|
76 |
val is_fun_typ : Term.typ -> bool |
|
77 |
val is_atomic_typ : Term.typ -> bool |
|
78 |
||
79 |
(* variable analysis *) |
|
80 |
val is_some_kind_of_var : Term.term -> bool |
|
81 |
val same_var_check : |
|
15531 | 82 |
''a -> ''b -> (''a * ''b) list -> (''a * ''b) list option |
15481 | 83 |
val has_new_vars : Term.term * Term.term -> bool |
84 |
val has_new_typ_vars : Term.term * Term.term -> bool |
|
85 |
(* checks to see if the lhs -> rhs is a invalid rewrite rule *) |
|
86 |
val is_not_valid_rwrule : Type.tsig -> (Term.term * Term.term) -> bool |
|
87 |
||
88 |
(* get the frees in a term that are of atomic type, ie non-functions *) |
|
89 |
val atomic_frees_of_term : Term.term -> (string * Term.typ) list |
|
90 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
91 |
(* get used names in a theorem to avoid upon instantiation. *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
92 |
val usednames_of_term : Term.term -> string list |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
93 |
val usednames_of_thm : Thm.thm -> string list |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
94 |
|
15481 | 95 |
(* Isar term skolemisationm and unsolemisation *) |
96 |
(* I think this is written also in IsarRTechn and also in somewhere else *) |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
97 |
(* val skolemise_term : (string,Term.typ) list -> Term.term -> Term.term *) |
15481 | 98 |
val unskolemise_all_term : |
99 |
Term.term -> |
|
100 |
(((string * Term.typ) * string) list * Term.term) |
|
101 |
||
102 |
(* given a string describing term then a string for its type, returns |
|
103 |
read term *) |
|
104 |
val readwty : string -> string -> Term.term |
|
105 |
||
106 |
(* pretty stuff *) |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
107 |
val print_term : Term.term -> unit |
15481 | 108 |
val pretty_print_sort : string list -> string |
109 |
val pretty_print_term : Term.term -> string |
|
110 |
val pretty_print_type : Term.typ -> string |
|
111 |
val pretty_print_typelist : |
|
112 |
Term.typ list -> (Term.typ -> string) -> string |
|
113 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
114 |
(* for debugging: quickly get a string of a term w.r.t the_context() *) |
15481 | 115 |
val string_of_term : Term.term -> string |
116 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
117 |
(* Pretty printing in a way that allows them to be parsed by ML. |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
118 |
these are perhaps redundent, check the standard basis |
15481 | 119 |
lib for generic versions for any datatype? *) |
120 |
val writesort : string list -> unit |
|
121 |
val writeterm : Term.term -> unit |
|
122 |
val writetype : Term.typ -> unit |
|
123 |
end |
|
124 |
||
125 |
||
126 |
structure TermLib : TERM_LIB = |
|
127 |
struct |
|
128 |
||
129 |
(* Two kinds of depth measure for HOAS terms, a first order (flat) and a |
|
130 |
higher order one. |
|
131 |
Note: not stable of eta-contraction: embedding eta-expands term, |
|
132 |
thus we assume eta-expanded *) |
|
133 |
fun fo_term_height (a $ b) = |
|
134 |
IsaPLib.max (1 + fo_term_height b, (fo_term_height a)) |
|
135 |
| fo_term_height (Abs(_,_,t)) = fo_term_height t |
|
136 |
| fo_term_height _ = 0; |
|
137 |
||
138 |
fun ho_term_height (a $ b) = |
|
139 |
1 + (IsaPLib.max (ho_term_height b, ho_term_height a)) |
|
140 |
| ho_term_height (Abs(_,_,t)) = ho_term_height t |
|
141 |
| ho_term_height _ = 0; |
|
142 |
||
15928
66b165ee016c
lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
dixon
parents:
15915
diff
changeset
|
143 |
|
15481 | 144 |
(* Higher order matching with exception handled *) |
145 |
(* returns optional instantiation *) |
|
146 |
fun clean_match tsig (a as (pat, t)) = |
|
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
147 |
let val (tyenv, tenv) = Pattern.match tsig a |
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
148 |
in SOME (Vartab.dest tyenv, Vartab.dest tenv) |
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
149 |
end handle Pattern.MATCH => NONE; |
15481 | 150 |
(* Higher order unification with exception handled, return the instantiations *) |
151 |
(* given Signature, max var index, pat, tgt *) |
|
152 |
(* returns Seq of instantiations *) |
|
153 |
fun clean_unify sgn ix (a as (pat, tgt)) = |
|
154 |
let |
|
155 |
(* type info will be re-derived, maybe this can be cached |
|
156 |
for efficiency? *) |
|
157 |
val pat_ty = Term.type_of pat; |
|
158 |
val tgt_ty = Term.type_of tgt; |
|
159 |
(* is it OK to ignore the type instantiation info? |
|
160 |
or should I be using it? *) |
|
161 |
val typs_unify = |
|
16934 | 162 |
SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix)) |
163 |
handle Type.TUNIFY => NONE; |
|
15481 | 164 |
in |
165 |
case typs_unify of |
|
15531 | 166 |
SOME (typinsttab, ix2) => |
15481 | 167 |
let |
15570 | 168 |
(* is it right to throw away the flexes? |
15481 | 169 |
or should I be using them somehow? *) |
15928
66b165ee016c
lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
dixon
parents:
15915
diff
changeset
|
170 |
fun mk_insts env = |
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
171 |
(Vartab.dest (Envir.type_env env), |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
172 |
Envir.alist_of env); |
15481 | 173 |
val initenv = Envir.Envir {asol = Vartab.empty, |
174 |
iTs = typinsttab, maxidx = ix2}; |
|
15928
66b165ee016c
lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
dixon
parents:
15915
diff
changeset
|
175 |
val useq = (Unify.smash_unifiers (sgn,initenv,[a])) |
66b165ee016c
lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
dixon
parents:
15915
diff
changeset
|
176 |
handle UnequalLengths => Seq.empty |
66b165ee016c
lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
dixon
parents:
15915
diff
changeset
|
177 |
| Term.TERM _ => Seq.empty; |
15481 | 178 |
fun clean_unify' useq () = |
179 |
(case (Seq.pull useq) of |
|
15531 | 180 |
NONE => NONE |
181 |
| SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t))) |
|
15570 | 182 |
handle UnequalLengths => NONE |
15531 | 183 |
| Term.TERM _ => NONE; |
15481 | 184 |
in |
185 |
(Seq.make (clean_unify' useq)) |
|
186 |
end |
|
15531 | 187 |
| NONE => Seq.empty |
15481 | 188 |
end; |
189 |
||
190 |
fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t)); |
|
191 |
fun asm_read s = |
|
192 |
(Thm.assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT))); |
|
193 |
||
194 |
||
195 |
(* more pretty printing code for Isabelle terms etc *) |
|
196 |
||
197 |
||
198 |
(* pretty_print_typelist l f = print a typelist. |
|
199 |
l = list of types to print : typ list |
|
200 |
f = function used to print a single type : typ -> string |
|
201 |
*) |
|
202 |
fun pretty_print_typelist [] f = "" |
|
203 |
| pretty_print_typelist [(h: typ)] (f : typ -> string) = (f h) |
|
204 |
| pretty_print_typelist ((h: typ) :: t) (f : typ -> string) = |
|
205 |
(f h) ^ ", " ^ (pretty_print_typelist t f); |
|
206 |
||
207 |
||
208 |
||
209 |
(* pretty_print_sort s = print a sort |
|
210 |
s = sort to print : string list |
|
211 |
*) |
|
212 |
fun pretty_print_sort [] = "" |
|
213 |
| pretty_print_sort ([h]) = "\"" ^ h ^ "\"" |
|
214 |
| pretty_print_sort (h :: t) = "\"" ^ h ^ "\"," ^ (pretty_print_sort t); |
|
215 |
||
216 |
||
217 |
(* pretty_print_type t = print a type |
|
218 |
t = type to print : type |
|
219 |
*) |
|
220 |
fun pretty_print_type (Type (n, l)) = |
|
221 |
"Type(\"" ^ n ^ "\", [" ^ (pretty_print_typelist l pretty_print_type) ^ "])" |
|
222 |
| pretty_print_type (TFree (n, s)) = |
|
223 |
"TFree(\"" ^ n ^ "\", [" ^ (pretty_print_sort s) ^ "])" |
|
224 |
| pretty_print_type (TVar ((n, i), s)) = |
|
225 |
"TVar( (\"" ^ n ^ "\", " ^ (string_of_int i) ^ "), [" ^ (pretty_print_sort s) ^ "])"; |
|
226 |
||
227 |
||
228 |
(* pretty_print_term t = print a term prints types and sorts too. |
|
229 |
t = term to print : term |
|
230 |
*) |
|
231 |
fun pretty_print_term (Const (s, t)) = |
|
232 |
"Const(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")" |
|
233 |
| pretty_print_term (Free (s, t)) = |
|
234 |
"Free(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")" |
|
235 |
| pretty_print_term (Var ((n, i), t)) = |
|
236 |
"Var( (\"" ^ n ^ "\"," ^ (string_of_int i) ^ "), " ^ (pretty_print_type t) ^ ")" |
|
237 |
| pretty_print_term (Bound i) = |
|
238 |
"Bound(" ^ (string_of_int i) ^ ")" |
|
239 |
| pretty_print_term (Abs (s, t, r)) = |
|
240 |
"Abs(\"" ^ s ^ "\"," ^ (pretty_print_type t) ^ ", \n " ^ (pretty_print_term r) ^ ")" |
|
241 |
| pretty_print_term (op $ (t1, t2)) = |
|
242 |
"(" ^ (pretty_print_term t1) ^ ") $\n (" ^ (pretty_print_term t2) ^ ")"; |
|
243 |
||
244 |
(* Write the term out nicly instead of just creating a string for it *) |
|
245 |
fun writeterm t = writeln (pretty_print_term t); |
|
246 |
fun writetype t = writeln (pretty_print_type t); |
|
247 |
fun writesort s = writeln (pretty_print_sort s); |
|
248 |
||
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
249 |
fun current_sign () = Theory.sign_of (the_context()); |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
250 |
fun cterm_of_term (t : term) = Thm.cterm_of (current_sign()) t; |
15481 | 251 |
fun term_of_thm t = (Thm.prop_of t); |
252 |
||
253 |
fun string_of_term t = |
|
254 |
(Sign.string_of_term (current_sign()) t); |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
255 |
fun print_term t = writeln (string_of_term t); |
15481 | 256 |
|
257 |
(* create a trivial HOL thm from anything... *) |
|
258 |
fun triv_thm_from_string s = |
|
259 |
Thm.trivial (cterm_of (current_sign()) (read s)); |
|
260 |
||
261 |
(* Checks if vars could be the same - alpha convertable |
|
262 |
w.r.t. previous vars, a and b are assumed to be vars, |
|
263 |
free vars, but not bound vars, |
|
264 |
Note frees and vars must all have unique names. *) |
|
265 |
fun same_var_check a b L = |
|
266 |
let |
|
15531 | 267 |
fun bterm_from t [] = NONE |
15481 | 268 |
| bterm_from t ((a,b)::m) = |
15531 | 269 |
if t = a then SOME b else bterm_from t m |
15481 | 270 |
|
271 |
val bl_opt = bterm_from a L |
|
272 |
in |
|
273 |
case bterm_from a L of |
|
15531 | 274 |
NONE => SOME ((a,b)::L) |
275 |
| SOME b2 => if b2 = b then SOME L else NONE |
|
15481 | 276 |
end; |
277 |
||
278 |
(* FIXME: make more efficient, only require a single new var! *) |
|
279 |
(* check if the new term has any meta variables not in the old term *) |
|
280 |
fun has_new_vars (old, new) = |
|
281 |
(case IsaPLib.lrem (op =) (Term.term_vars old) (Term.term_vars new) of |
|
282 |
[] => false |
|
283 |
| (_::_) => true); |
|
284 |
(* check if the new term has any meta variables not in the old term *) |
|
285 |
fun has_new_typ_vars (old, new) = |
|
286 |
(case IsaPLib.lrem (op =) (Term.term_tvars old) (Term.term_tvars new) of |
|
287 |
[] => false |
|
288 |
| (_::_) => true); |
|
289 |
||
15570 | 290 |
(* This version avoids name conflicts that might be introduced by |
15481 | 291 |
unskolemisation, and returns a list of (string * Term.typ) * string, |
292 |
where the outer string is the original name, and the inner string is |
|
293 |
the new name, and the type is the type of the free variable that was |
|
294 |
renamed. *) |
|
295 |
local |
|
296 |
fun myadd (n,ty) (L as (renames, names)) = |
|
297 |
let val n' = Syntax.dest_skolem n in |
|
298 |
case (Library.find_first (fn (_,n2) => (n2 = n)) renames) of |
|
15531 | 299 |
NONE => |
15481 | 300 |
let val renamedn = Term.variant names n' in |
301 |
(renamedn, (((renamedn, ty), n) :: renames, |
|
302 |
renamedn :: names)) end |
|
15531 | 303 |
| (SOME ((renamedn, _), _)) => (renamedn, L) |
15481 | 304 |
end |
15570 | 305 |
handle Fail _ => (n, L); |
15481 | 306 |
|
307 |
fun unsk (L,f) (t1 $ t2) = |
|
308 |
let val (L', t1') = unsk (L, I) t1 |
|
309 |
in unsk (L', (fn x => f (t1' $ x))) t2 end |
|
310 |
| unsk (L,f) (Abs(n,ty,t)) = |
|
311 |
unsk (L, (fn x => Abs(n,ty,x))) t |
|
312 |
| unsk (L, f) (Free (n,ty)) = |
|
313 |
let val (renamed_n, L') = myadd (n ,ty) L |
|
314 |
in (L', f (Free (renamed_n, ty))) end |
|
315 |
| unsk (L, f) l = (L, f l); |
|
316 |
in |
|
317 |
fun unskolemise_all_term t = |
|
318 |
let |
|
319 |
val names = Term.add_term_names (t,[]) |
|
320 |
val ((renames,names'),t') = unsk (([], names),I) t |
|
321 |
in (renames,t') end; |
|
322 |
end |
|
323 |
||
324 |
(* true if the type t is a function *) |
|
325 |
fun is_fun_typ (Type(s, l)) = |
|
326 |
if s = "fun" then true else false |
|
327 |
| is_fun_typ _ = false; |
|
328 |
||
329 |
val is_atomic_typ = not o is_fun_typ; |
|
330 |
||
331 |
(* get the frees in a term that are of atomic type, ie non-functions *) |
|
332 |
val atomic_frees_of_term = |
|
15570 | 333 |
List.filter (is_atomic_typ o snd) |
15481 | 334 |
o map Term.dest_Free |
335 |
o Term.term_frees; |
|
336 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
337 |
fun usednames_of_term t = Term.add_term_names (t,[]); |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
338 |
fun usednames_of_thm th = |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
339 |
let val rep = Thm.rep_thm th |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
340 |
val hyps = #hyps rep |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
341 |
val (tpairl,tpairr) = Library.split_list (#tpairs rep) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
342 |
val prop = #prop rep |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
343 |
in |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
344 |
List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps))) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
345 |
end; |
15481 | 346 |
|
347 |
(* read in a string and a top-level type and this will give back a term *) |
|
348 |
fun readwty tstr tystr = |
|
349 |
let |
|
350 |
val sgn = Theory.sign_of (the_context()) |
|
351 |
in |
|
15531 | 352 |
Sign.simple_read_term sgn (Sign.read_typ (sgn, K NONE) tystr) tstr |
15481 | 353 |
end; |
354 |
||
355 |
||
356 |
(* first term is equal to the second in some name convertable |
|
357 |
way... Note: This differs from the aeconv in the Term.ML file of |
|
358 |
Isabelle in that it allows a var to be alpha-equiv to a free var. |
|
359 |
||
360 |
Also, the isabelle term.ML version of aeconv uses a |
|
361 |
function that it claims doesn't work! *) |
|
362 |
fun term_name_eq (Abs(_,ty1,t1)) (Abs(_,ty2,t2)) l = |
|
363 |
if ty1 = ty2 then term_name_eq t1 t2 l |
|
15531 | 364 |
else NONE |
15481 | 365 |
| term_name_eq (ah $ at) (bh $ bt) l = |
366 |
let |
|
367 |
val lopt = (term_name_eq ah bh l) |
|
368 |
in |
|
15570 | 369 |
if isSome lopt then |
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
370 |
term_name_eq at bt (valOf lopt) |
15481 | 371 |
else |
15531 | 372 |
NONE |
15481 | 373 |
end |
374 |
| term_name_eq (Const(a,T)) (Const(b,U)) l = |
|
15531 | 375 |
if a=b andalso T=U then SOME l |
376 |
else NONE |
|
15481 | 377 |
| term_name_eq (a as Free(s1,ty1)) (b as Free(s2,ty2)) l = |
378 |
same_var_check a b l |
|
379 |
| term_name_eq (a as Free(s1,ty1)) (b as Var(n2,ty2)) l = |
|
380 |
same_var_check a b l |
|
381 |
| term_name_eq (a as Var(n1,ty1)) (b as Free(s2,ty2)) l = |
|
382 |
same_var_check a b l |
|
383 |
| term_name_eq (a as Var(n1,ty1)) (b as Var(n2,ty2)) l = |
|
384 |
same_var_check a b l |
|
385 |
| term_name_eq (Bound i) (Bound j) l = |
|
15531 | 386 |
if i = j then SOME l else NONE |
387 |
| term_name_eq a b l = ((*writeln ("unchecked case:\n" ^ "a:\n" ^ (pretty_print_term a) ^ "\nb:\n" ^ (pretty_print_term b));*) NONE); |
|
15481 | 388 |
|
389 |
(* checks to see if the term in a name-equivalent member of the list of terms. *) |
|
15531 | 390 |
fun get_name_eq_member a [] = NONE |
15481 | 391 |
| get_name_eq_member a (h :: t) = |
15570 | 392 |
if isSome (term_name_eq a h []) then SOME h |
15481 | 393 |
else get_name_eq_member a t; |
394 |
||
395 |
fun name_eq_member a [] = false |
|
396 |
| name_eq_member a (h :: t) = |
|
15570 | 397 |
if isSome (term_name_eq a h []) then true |
15481 | 398 |
else name_eq_member a t; |
399 |
||
400 |
(* true if term is a variable *) |
|
401 |
fun is_some_kind_of_var (Free(s, ty)) = true |
|
402 |
| is_some_kind_of_var (Var(i, ty)) = true |
|
403 |
| is_some_kind_of_var (Bound(i)) = true |
|
404 |
| is_some_kind_of_var _ = false; |
|
405 |
||
406 |
(* checks to see if the lhs -> rhs is a invalid rewrite rule *) |
|
407 |
(* FIXME: we should really check that there is a subterm on the lhs |
|
408 |
which embeds into the rhs, this would be much closer to the normal |
|
409 |
notion of valid wave rule - ie there exists at least one case where it |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
410 |
is a valid wave rule... *) |
15481 | 411 |
fun is_not_valid_rwrule tysig (lhs, rhs) = |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
412 |
Term.is_Var (Term.head_of lhs) (* if lhs is essentially just a var *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
413 |
orelse has_new_vars (lhs,rhs) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
414 |
orelse has_new_typ_vars (lhs,rhs) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
415 |
orelse Pattern.matches_subterm tysig (lhs, rhs); |
15481 | 416 |
|
417 |
||
418 |
(* first term contains the second in some name convertable way... *) |
|
419 |
(* note: this is equivalent to an alpha-convertable emedding *) |
|
420 |
(* takes as args: term containing a, term contained b, |
|
421 |
(bound vars of a, bound vars of b), |
|
422 |
current alpha-conversion-pairs, |
|
423 |
returns: bool:can convert, new alpha-conversion table *) |
|
424 |
(* in bellow: we *don't* use: a loose notion that only requires |
|
425 |
variables to match variables, and doesn't worry about the actual |
|
426 |
pattern in the variables. *) |
|
427 |
fun term_contains1 (Bs, FVs) (Abs(s,ty,t)) (Abs(s2,ty2,t2)) = |
|
428 |
if ty = ty2 then |
|
15531 | 429 |
term_contains1 ((SOME(s,s2,ty)::Bs), FVs) t t2 |
15481 | 430 |
else [] |
431 |
||
432 |
| term_contains1 T t1 (Abs(s2,ty2,t2)) = [] |
|
433 |
||
434 |
| term_contains1 (Bs, FVs) (Abs(s,ty,t)) t2 = |
|
15531 | 435 |
term_contains1 (NONE::Bs, FVs) t t2 |
15481 | 436 |
|
437 |
| term_contains1 T (ah $ at) (bh $ bt) = |
|
438 |
(term_contains1 T ah (bh $ bt)) @ |
|
439 |
(term_contains1 T at (bh $ bt)) @ |
|
15570 | 440 |
(List.concat (map (fn inT => (term_contains1 inT at bt)) |
15481 | 441 |
(term_contains1 T ah bh))) |
442 |
||
443 |
| term_contains1 T a (bh $ bt) = [] |
|
444 |
||
445 |
| term_contains1 T (ah $ at) b = |
|
446 |
(term_contains1 T ah b) @ (term_contains1 T at b) |
|
447 |
||
448 |
| term_contains1 T a b = |
|
449 |
(* simple list table lookup to check if a named variable has been |
|
450 |
mapped to a variable, if not adds the mapping and return some new |
|
451 |
list mapping, if it is then it checks that the pair are mapped to |
|
452 |
each other, if so returns the current mapping list, else none. *) |
|
453 |
let |
|
15531 | 454 |
fun bterm_from t [] = NONE |
15481 | 455 |
| bterm_from t ((a,b)::m) = |
15531 | 456 |
if t = a then SOME b else bterm_from t m |
15481 | 457 |
|
458 |
(* check to see if, w.r.t. the variable mapping, two terms are leaf |
|
459 |
terms and are mapped to each other. Note constants are only mapped |
|
460 |
to the same constant. *) |
|
461 |
fun same_leaf_check (T as (Bs,FVs)) (Bound i) (Bound j) = |
|
462 |
let |
|
463 |
fun aux_chk (i1,i2) [] = false |
|
15531 | 464 |
| aux_chk (0,0) ((SOME _) :: bnds) = true |
465 |
| aux_chk (i1,0) (NONE :: bnds) = false |
|
466 |
| aux_chk (i1,i2) ((SOME _) :: bnds) = |
|
15481 | 467 |
aux_chk (i1 - 1,i2 - 1) bnds |
15531 | 468 |
| aux_chk (i1,i2) (NONE :: bnds) = |
15481 | 469 |
aux_chk (i1,i2 - 1) bnds |
470 |
in |
|
471 |
if (aux_chk (i,j) Bs) then [T] |
|
472 |
else [] |
|
473 |
end |
|
474 |
| same_leaf_check (T as (Bs,(Fs,Vs))) |
|
475 |
(a as (Free (an,aty))) |
|
476 |
(b as (Free (bn,bty))) = |
|
477 |
(case bterm_from an Fs of |
|
15531 | 478 |
SOME b2n => if bn = b2n then [T] |
15481 | 479 |
else [] (* conflict of var name *) |
15531 | 480 |
| NONE => [(Bs,((an,bn)::Fs,Vs))]) |
15481 | 481 |
| same_leaf_check (T as (Bs,(Fs,Vs))) |
482 |
(a as (Var (an,aty))) |
|
483 |
(b as (Var (bn,bty))) = |
|
484 |
(case bterm_from an Vs of |
|
15531 | 485 |
SOME b2n => if bn = b2n then [T] |
15481 | 486 |
else [] (* conflict of var name *) |
15531 | 487 |
| NONE => [(Bs,(Fs,(an,bn)::Vs))]) |
15481 | 488 |
| same_leaf_check T (a as (Const _)) (b as (Const _)) = |
489 |
if a = b then [T] else [] |
|
490 |
| same_leaf_check T _ _ = [] |
|
491 |
||
492 |
in |
|
493 |
same_leaf_check T a b |
|
494 |
end; |
|
495 |
||
496 |
(* wrapper for term_contains1: checks if the term "a" contains in |
|
497 |
some embedded way, (w.r.t. name -convertable) the term "b" *) |
|
498 |
fun term_contains a b = |
|
499 |
case term_contains1 ([],([],[])) a b of |
|
500 |
(_ :: _) => true |
|
501 |
| [] => false; |
|
502 |
||
503 |
(* change all bound variables to see ones with appropriate name and |
|
504 |
type *) |
|
505 |
(* naming convention is OK as we use 'variant' from term.ML *) |
|
506 |
(* Note "bounds_to_frees" defined below, its better and quicker, but |
|
507 |
keeps the quantifiers handing about, and changes all bounds, not |
|
508 |
just universally quantified ones. *) |
|
509 |
fun change_bounds_to_frees t = |
|
510 |
let |
|
511 |
val vars = strip_all_vars t |
|
512 |
val frees_names = map (fn Free(s,n) => s | _ => "") (term_frees t) |
|
513 |
val body = strip_all_body t |
|
514 |
||
515 |
fun bnds_to_frees [] _ acc = acc |
|
516 |
| bnds_to_frees ((name,ty)::more) names acc = |
|
517 |
let |
|
518 |
val new_name = variant names name |
|
519 |
in |
|
520 |
bnds_to_frees more (new_name::names) (Free(new_name,ty)::acc) |
|
521 |
end |
|
522 |
in |
|
523 |
(subst_bounds ((bnds_to_frees vars frees_names []), body)) |
|
524 |
end; |
|
525 |
||
526 |
(* a runtime-quick function which makes sure that every variable has a |
|
527 |
unique name *) |
|
528 |
fun unique_namify_aux (ntab,(Abs(s,ty,t))) = |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
529 |
(case (Symtab.lookup (ntab,s)) of |
15531 | 530 |
NONE => |
15481 | 531 |
let |
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
532 |
val (ntab2,t2) = unique_namify_aux ((Symtab.update ((s,s),ntab)), t) |
15481 | 533 |
in |
534 |
(ntab2,Abs(s,ty,t2)) |
|
535 |
end |
|
15531 | 536 |
| SOME s2 => |
15481 | 537 |
let |
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
538 |
val s_new = (Term.variant (Symtab.keys ntab) s) |
15481 | 539 |
val (ntab2,t2) = |
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
540 |
unique_namify_aux ((Symtab.update ((s_new,s_new),ntab)), t) |
15481 | 541 |
in |
542 |
(ntab2,Abs(s_new,ty,t2)) |
|
543 |
end) |
|
544 |
| unique_namify_aux (ntab,(a $ b)) = |
|
545 |
let |
|
546 |
val (ntab1,t1) = unique_namify_aux (ntab,a) |
|
547 |
val (ntab2,t2) = unique_namify_aux (ntab1,b) |
|
548 |
in |
|
549 |
(ntab2, t1$t2) |
|
550 |
end |
|
551 |
| unique_namify_aux (nt as (ntab,Const x)) = nt |
|
552 |
| unique_namify_aux (nt as (ntab,f as Free (s,ty))) = |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
553 |
(case (Symtab.lookup (ntab,s)) of |
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
554 |
NONE => ((Symtab.update ((s,s),ntab)), f) |
15531 | 555 |
| SOME _ => nt) |
15481 | 556 |
| unique_namify_aux (nt as (ntab,v as Var ((s,i),ty))) = |
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
557 |
(case (Symtab.lookup (ntab,s)) of |
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
558 |
NONE => ((Symtab.update ((s,s),ntab)), v) |
15531 | 559 |
| SOME _ => nt) |
15481 | 560 |
| unique_namify_aux (nt as (ntab, Bound i)) = nt; |
561 |
||
562 |
fun unique_namify t = |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
563 |
#2 (unique_namify_aux (Symtab.empty, t)); |
15481 | 564 |
|
565 |
(* a runtime-quick function which makes sure that every variable has a |
|
566 |
unique name and also changes bound variables to free variables, used |
|
567 |
for embedding checks, Note that this is a pretty naughty term |
|
568 |
manipulation, which doesn't have necessary relation to the original |
|
569 |
sematics of the term. This is really a trick for our embedding code. *) |
|
570 |
||
571 |
fun bounds_to_frees_aux T (ntab,(Abs(s,ty,t))) = |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
572 |
(case (Symtab.lookup (ntab,s)) of |
15531 | 573 |
NONE => |
15481 | 574 |
let |
575 |
val (ntab2,t2) = bounds_to_frees_aux ((s,ty)::T) |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
576 |
((Symtab.update ((s,s),ntab)), t) |
15481 | 577 |
in |
578 |
(ntab2,Abs(s,ty,t2)) |
|
579 |
end |
|
15531 | 580 |
| SOME s2 => |
15481 | 581 |
let |
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
582 |
val s_new = (Term.variant (Symtab.keys ntab) s) |
15481 | 583 |
val (ntab2,t2) = |
584 |
bounds_to_frees_aux ((s_new,ty)::T) |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
585 |
(Symtab.update (((s_new,s_new),ntab)), t) |
15481 | 586 |
in |
587 |
(ntab2,Abs(s_new,ty,t2)) |
|
588 |
end) |
|
589 |
| bounds_to_frees_aux T (ntab,(a $ b)) = |
|
590 |
let |
|
591 |
val (ntab1,t1) = bounds_to_frees_aux T (ntab,a) |
|
592 |
val (ntab2,t2) = bounds_to_frees_aux T (ntab1,b) |
|
593 |
in |
|
594 |
(ntab2, t1$t2) |
|
595 |
end |
|
596 |
| bounds_to_frees_aux T (nt as (ntab,Const x)) = nt |
|
597 |
| bounds_to_frees_aux T (nt as (ntab,f as Free (s,ty))) = |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
598 |
(case (Symtab.lookup (ntab,s)) of |
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
599 |
NONE => ((Symtab.update ((s,s),ntab)), f) |
15531 | 600 |
| SOME _ => nt) |
15481 | 601 |
| bounds_to_frees_aux T (nt as (ntab,v as Var ((s,i),ty))) = |
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
602 |
(case (Symtab.lookup (ntab,s)) of |
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
603 |
NONE => ((Symtab.update ((s,s),ntab)), v) |
15531 | 604 |
| SOME _ => nt) |
15481 | 605 |
| bounds_to_frees_aux T (nt as (ntab, Bound i)) = |
606 |
let |
|
15570 | 607 |
val (s,ty) = List.nth (T,i) |
15481 | 608 |
in |
609 |
(ntab, Free (s,ty)) |
|
610 |
end; |
|
611 |
||
612 |
||
613 |
fun bounds_to_frees t = |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
614 |
#2 (bounds_to_frees_aux [] (Symtab.empty,t)); |
15481 | 615 |
|
616 |
fun bounds_to_frees_with_vars vars t = |
|
16857
6389511d4609
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
dixon
parents:
16179
diff
changeset
|
617 |
#2 (bounds_to_frees_aux vars (Symtab.empty,t)); |
15481 | 618 |
|
619 |
||
620 |
||
621 |
(* loose bounds to frees *) |
|
622 |
fun loose_bnds_to_frees_aux (bnds,vars) (Abs(s,ty,t)) = |
|
623 |
Abs(s,ty,loose_bnds_to_frees_aux (bnds + 1,vars) t) |
|
624 |
| loose_bnds_to_frees_aux (bnds,vars) (a $ b) = |
|
625 |
(loose_bnds_to_frees_aux (bnds,vars) a) |
|
626 |
$ (loose_bnds_to_frees_aux (bnds,vars) b) |
|
627 |
| loose_bnds_to_frees_aux (bnds,vars) (t as (Bound i)) = |
|
15570 | 628 |
if (bnds <= i) then Free (List.nth (vars,i - bnds)) |
15481 | 629 |
else t |
630 |
| loose_bnds_to_frees_aux (bnds,vars) t = t; |
|
631 |
||
632 |
||
633 |
fun loose_bnds_to_frees vars t = |
|
634 |
loose_bnds_to_frees_aux (0,vars) t; |
|
635 |
||
636 |
||
637 |
fun try_dest_Goal (Const("Goal", _) $ T) = T |
|
638 |
| try_dest_Goal T = T; |
|
639 |
||
640 |
fun try_dest_Trueprop (Const("Trueprop", _) $ T) = T |
|
641 |
| try_dest_Trueprop T = T; |
|
642 |
||
643 |
fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l |
|
644 |
| bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t |
|
645 |
| bot_left_leaf_of x = x; |
|
646 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
647 |
fun bot_left_leaf_noabs_of (l $ r) = bot_left_leaf_noabs_of l |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
648 |
| bot_left_leaf_noabs_of x = x; |
15481 | 649 |
|
650 |
(* cleaned up normal form version of the subgoal terms conclusion *) |
|
651 |
fun cleaned_term_conc t = |
|
652 |
let |
|
653 |
val concl = Logic.strip_imp_concl (change_bounds_to_frees t) |
|
654 |
in |
|
655 |
(try_dest_Trueprop (try_dest_Goal concl)) |
|
656 |
end; |
|
657 |
||
658 |
(* fun get_prems_of_sg_term t = |
|
659 |
map opt_dest_Trueprop (Logic.strip_imp_prems t); *) |
|
660 |
||
661 |
fun get_prems_of_sg_term t = |
|
662 |
map try_dest_Trueprop (Logic.strip_assums_hyp t); |
|
663 |
||
664 |
||
665 |
(* drop premices, clean bound var stuff, and make a trueprop... *) |
|
666 |
fun cleaned_term_parts t = |
|
667 |
let |
|
668 |
val t2 = (change_bounds_to_frees t) |
|
669 |
val concl = Logic.strip_imp_concl t2 |
|
670 |
val prems = map try_dest_Trueprop (Logic.strip_imp_prems t2) |
|
671 |
in |
|
672 |
(prems, (try_dest_Trueprop (try_dest_Goal concl))) |
|
673 |
end; |
|
674 |
||
675 |
(* change free variables to vars and visa versa *) |
|
676 |
(* *** check naming is OK, can we just use the vasr old name? *) |
|
677 |
(* *** Check: Logic.varify and Logic.unvarify *) |
|
678 |
fun change_vars_to_frees (a$b) = |
|
679 |
(change_vars_to_frees a) $ (change_vars_to_frees b) |
|
680 |
| change_vars_to_frees (Abs(s,ty,t)) = |
|
681 |
(Abs(s,Type.varifyT ty,change_vars_to_frees t)) |
|
682 |
| change_vars_to_frees (Var((s,i),ty)) = (Free(s,Type.unvarifyT ty)) |
|
683 |
| change_vars_to_frees l = l; |
|
684 |
||
685 |
fun change_frees_to_vars (a$b) = |
|
686 |
(change_frees_to_vars a) $ (change_frees_to_vars b) |
|
687 |
| change_frees_to_vars (Abs(s,ty,t)) = |
|
688 |
(Abs(s,Type.varifyT ty,change_frees_to_vars t)) |
|
689 |
| change_frees_to_vars (Free(s,ty)) = (Var((s,0),Type.varifyT ty)) |
|
690 |
| change_frees_to_vars l = l; |
|
691 |
||
692 |
||
16934 | 693 |
end; |