author | paulson <lp15@cam.ac.uk> |
Sun, 20 May 2018 18:37:34 +0100 | |
changeset 68239 | 0764ee22a4d1 |
parent 67721 | 5348bea4accd |
child 74230 | d637611b41bd |
permissions | -rw-r--r-- |
24259 | 1 |
(* Title: Pure/primitive_defs.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Primitive definition forms. |
|
5 |
*) |
|
6 |
||
7 |
signature PRIMITIVE_DEFS = |
|
8 |
sig |
|
63042 | 9 |
val dest_def: Proof.context -> |
10 |
{check_head: term -> bool, |
|
11 |
check_free_lhs: string -> bool, |
|
12 |
check_free_rhs: string -> bool, |
|
13 |
check_tfree: string -> bool} -> |
|
63395 | 14 |
term -> (term * term) * term list * term |
24259 | 15 |
val abs_def: term -> term * term |
16 |
end; |
|
17 |
||
33385 | 18 |
structure Primitive_Defs: PRIMITIVE_DEFS = |
24259 | 19 |
struct |
20 |
||
21 |
fun term_kind (Const _) = "existing constant " |
|
22 |
| term_kind (Free _) = "free variable " |
|
23 |
| term_kind (Bound _) = "bound variable " |
|
24 |
| term_kind _ = ""; |
|
25 |
||
67721 | 26 |
(*c x \<equiv> t[x] to \<And>x. c x \<equiv> t[x]*) |
63042 | 27 |
fun dest_def ctxt {check_head, check_free_lhs, check_free_rhs, check_tfree} eq = |
24259 | 28 |
let |
29 |
fun err msg = raise TERM (msg, [eq]); |
|
30 |
val eq_vars = Term.strip_all_vars eq; |
|
31 |
val eq_body = Term.strip_all_body eq; |
|
32 |
||
33 |
val display_terms = |
|
42284 | 34 |
commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars); |
24981
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24259
diff
changeset
|
35 |
val display_types = commas_quote o map (Syntax.string_of_typ ctxt); |
24259 | 36 |
|
64596 | 37 |
val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)"; |
24259 | 38 |
val lhs = Envir.beta_eta_contract raw_lhs; |
39 |
val (head, args) = Term.strip_comb lhs; |
|
40 |
val head_tfrees = Term.add_tfrees head []; |
|
41 |
||
42 |
fun check_arg (Bound _) = true |
|
63042 | 43 |
| check_arg (Free (x, _)) = check_free_lhs x |
56243 | 44 |
| check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true |
24259 | 45 |
| check_arg _ = false; |
46 |
fun close_arg (Bound _) t = t |
|
46214 | 47 |
| close_arg x t = Logic.all x t; |
24259 | 48 |
|
49 |
val lhs_bads = filter_out check_arg args; |
|
50 |
val lhs_dups = duplicates (op aconv) args; |
|
51 |
val rhs_extras = Term.fold_aterms (fn v as Free (x, _) => |
|
63042 | 52 |
if check_free_rhs x orelse member (op aconv) args v then I |
24259 | 53 |
else insert (op aconv) v | _ => I) rhs []; |
54 |
val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) => |
|
63042 | 55 |
if check_tfree a orelse member (op =) head_tfrees (a, S) then I |
24259 | 56 |
else insert (op =) v | _ => I)) rhs []; |
57 |
in |
|
58 |
if not (check_head head) then |
|
59 |
err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head]) |
|
60 |
else if not (null lhs_bads) then |
|
61 |
err ("Bad arguments on lhs: " ^ display_terms lhs_bads) |
|
62 |
else if not (null lhs_dups) then |
|
63 |
err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups) |
|
64 |
else if not (null rhs_extras) then |
|
65 |
err ("Extra variables on rhs: " ^ display_terms rhs_extras) |
|
66 |
else if not (null rhs_extrasT) then |
|
67 |
err ("Extra type variables on rhs: " ^ display_types rhs_extrasT) |
|
68 |
else if exists_subterm (fn t => t aconv head) rhs then |
|
69 |
err "Entity to be defined occurs on rhs" |
|
70 |
else |
|
63395 | 71 |
((lhs, rhs), args, |
72 |
fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs))))) |
|
24259 | 73 |
end; |
74 |
||
67721 | 75 |
(*\<And>x. c x \<equiv> t[x] to c \<equiv> \<lambda>x. t[x]*) |
24259 | 76 |
fun abs_def eq = |
77 |
let |
|
78 |
val body = Term.strip_all_body eq; |
|
79 |
val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); |
|
80 |
val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body)); |
|
81 |
val (lhs', args) = Term.strip_comb lhs; |
|
44241 | 82 |
val rhs' = fold_rev (absfree o dest_Free) args rhs; |
24259 | 83 |
in (lhs', rhs') end; |
84 |
||
85 |
end; |