author | wenzelm |
Sun, 22 Jul 2012 12:26:41 +0200 | |
changeset 48423 | 0ccf143a2a69 |
parent 46218 | ecf6375e2abb |
child 56243 | 2e10a36b8d46 |
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 |
|
24981
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24259
diff
changeset
|
9 |
val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) -> |
24259 | 10 |
term -> (term * term) * term |
11 |
val abs_def: term -> term * term |
|
12 |
end; |
|
13 |
||
33385 | 14 |
structure Primitive_Defs: PRIMITIVE_DEFS = |
24259 | 15 |
struct |
16 |
||
17 |
fun term_kind (Const _) = "existing constant " |
|
18 |
| term_kind (Free _) = "free variable " |
|
19 |
| term_kind (Bound _) = "bound variable " |
|
20 |
| term_kind _ = ""; |
|
21 |
||
22 |
(*c x == t[x] to !!x. c x == t[x]*) |
|
24981
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24259
diff
changeset
|
23 |
fun dest_def ctxt check_head is_fixed is_fixedT eq = |
24259 | 24 |
let |
25 |
fun err msg = raise TERM (msg, [eq]); |
|
26 |
val eq_vars = Term.strip_all_vars eq; |
|
27 |
val eq_body = Term.strip_all_body eq; |
|
28 |
||
29 |
val display_terms = |
|
42284 | 30 |
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
|
31 |
val display_types = commas_quote o map (Syntax.string_of_typ ctxt); |
24259 | 32 |
|
33 |
val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)"; |
|
34 |
val lhs = Envir.beta_eta_contract raw_lhs; |
|
35 |
val (head, args) = Term.strip_comb lhs; |
|
36 |
val head_tfrees = Term.add_tfrees head []; |
|
37 |
||
38 |
fun check_arg (Bound _) = true |
|
39 |
| check_arg (Free (x, _)) = not (is_fixed x) |
|
40 |
| check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true |
|
41 |
| check_arg _ = false; |
|
42 |
fun close_arg (Bound _) t = t |
|
46214 | 43 |
| close_arg x t = Logic.all x t; |
24259 | 44 |
|
45 |
val lhs_bads = filter_out check_arg args; |
|
46 |
val lhs_dups = duplicates (op aconv) args; |
|
47 |
val rhs_extras = Term.fold_aterms (fn v as Free (x, _) => |
|
48 |
if is_fixed x orelse member (op aconv) args v then I |
|
49 |
else insert (op aconv) v | _ => I) rhs []; |
|
50 |
val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) => |
|
51 |
if is_fixedT a orelse member (op =) head_tfrees (a, S) then I |
|
52 |
else insert (op =) v | _ => I)) rhs []; |
|
53 |
in |
|
54 |
if not (check_head head) then |
|
55 |
err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head]) |
|
56 |
else if not (null lhs_bads) then |
|
57 |
err ("Bad arguments on lhs: " ^ display_terms lhs_bads) |
|
58 |
else if not (null lhs_dups) then |
|
59 |
err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups) |
|
60 |
else if not (null rhs_extras) then |
|
61 |
err ("Extra variables on rhs: " ^ display_terms rhs_extras) |
|
62 |
else if not (null rhs_extrasT) then |
|
63 |
err ("Extra type variables on rhs: " ^ display_types rhs_extrasT) |
|
64 |
else if exists_subterm (fn t => t aconv head) rhs then |
|
65 |
err "Entity to be defined occurs on rhs" |
|
66 |
else |
|
46218
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
46214
diff
changeset
|
67 |
((lhs, rhs), fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs))))) |
24259 | 68 |
end; |
69 |
||
70 |
(*!!x. c x == t[x] to c == %x. t[x]*) |
|
71 |
fun abs_def eq = |
|
72 |
let |
|
73 |
val body = Term.strip_all_body eq; |
|
74 |
val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); |
|
75 |
val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body)); |
|
76 |
val (lhs', args) = Term.strip_comb lhs; |
|
44241 | 77 |
val rhs' = fold_rev (absfree o dest_Free) args rhs; |
24259 | 78 |
in (lhs', rhs') end; |
79 |
||
80 |
end; |