1(*  Title:      Pure/primitive_defs.ML
2    Author:     Makarius
3
4Primitive definition forms.
5*)
6
7signature PRIMITIVE_DEFS =
8sig
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} ->
14    term -> (term * term) * term list * term
15  val abs_def: term -> term * term
16end;
17
18structure Primitive_Defs: PRIMITIVE_DEFS =
19struct
20
21fun term_kind (Const _) = "existing constant "
22  | term_kind (Free _) = "free variable "
23  | term_kind (Bound _) = "bound variable "
24  | term_kind _ = "";
25
26(*c x \<equiv> t[x] to \<And>x. c x \<equiv> t[x]*)
27fun dest_def ctxt {check_head, check_free_lhs, check_free_rhs, check_tfree} eq =
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 =
34      commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
35    val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
36
37    val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
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
43      | check_arg (Free (x, _)) = check_free_lhs x
44      | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true
45      | check_arg _ = false;
46    fun close_arg (Bound _) t = t
47      | close_arg x t = Logic.all x t;
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, _) =>
52      if check_free_rhs x orelse member (op aconv) args v then I
53      else insert (op aconv) v | _ => I) rhs [];
54    val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
55      if check_tfree a orelse member (op =) head_tfrees (a, S) then I
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
71      ((lhs, rhs), args,
72        fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
73  end;
74
75(*\<And>x. c x \<equiv> t[x] to c \<equiv> \<lambda>x. t[x]*)
76fun 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;
82    val rhs' = fold_rev (absfree o dest_Free) args rhs;
83  in (lhs', rhs') end;
84
85end;
86