src/Pure/primitive_defs.ML
author haftmann
Wed Jan 21 16:47:31 2009 +0100 (2009-01-21)
changeset 29580 117b88da143c
parent 24981 4ec3f95190bf
child 30280 eb98b49ef835
permissions -rw-r--r--
dropped ID
wenzelm@24259
     1
(*  Title:      Pure/primitive_defs.ML
wenzelm@24259
     2
    Author:     Makarius
wenzelm@24259
     3
wenzelm@24259
     4
Primitive definition forms.
wenzelm@24259
     5
*)
wenzelm@24259
     6
wenzelm@24259
     7
signature PRIMITIVE_DEFS =
wenzelm@24259
     8
sig
wenzelm@24981
     9
  val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
wenzelm@24259
    10
    term -> (term * term) * term
wenzelm@24259
    11
  val abs_def: term -> term * term
wenzelm@24259
    12
  val mk_defpair: term * term -> string * term
wenzelm@24259
    13
end;
wenzelm@24259
    14
wenzelm@24259
    15
structure PrimitiveDefs: PRIMITIVE_DEFS =
wenzelm@24259
    16
struct
wenzelm@24259
    17
wenzelm@24259
    18
fun term_kind (Const _) = "existing constant "
wenzelm@24259
    19
  | term_kind (Free _) = "free variable "
wenzelm@24259
    20
  | term_kind (Bound _) = "bound variable "
wenzelm@24259
    21
  | term_kind _ = "";
wenzelm@24259
    22
wenzelm@24259
    23
(*c x == t[x] to !!x. c x == t[x]*)
wenzelm@24981
    24
fun dest_def ctxt check_head is_fixed is_fixedT eq =
wenzelm@24259
    25
  let
wenzelm@24259
    26
    fun err msg = raise TERM (msg, [eq]);
wenzelm@24259
    27
    val eq_vars = Term.strip_all_vars eq;
wenzelm@24259
    28
    val eq_body = Term.strip_all_body eq;
wenzelm@24259
    29
wenzelm@24259
    30
    val display_terms =
wenzelm@24981
    31
      commas_quote o map (Syntax.string_of_term ctxt o Syntax.bound_vars eq_vars);
wenzelm@24981
    32
    val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
wenzelm@24259
    33
wenzelm@24259
    34
    val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
wenzelm@24259
    35
    val lhs = Envir.beta_eta_contract raw_lhs;
wenzelm@24259
    36
    val (head, args) = Term.strip_comb lhs;
wenzelm@24259
    37
    val head_tfrees = Term.add_tfrees head [];
wenzelm@24259
    38
wenzelm@24259
    39
    fun check_arg (Bound _) = true
wenzelm@24259
    40
      | check_arg (Free (x, _)) = not (is_fixed x)
wenzelm@24259
    41
      | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
wenzelm@24259
    42
      | check_arg _ = false;
wenzelm@24259
    43
    fun close_arg (Bound _) t = t
wenzelm@24259
    44
      | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
wenzelm@24259
    45
wenzelm@24259
    46
    val lhs_bads = filter_out check_arg args;
wenzelm@24259
    47
    val lhs_dups = duplicates (op aconv) args;
wenzelm@24259
    48
    val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
wenzelm@24259
    49
      if is_fixed x orelse member (op aconv) args v then I
wenzelm@24259
    50
      else insert (op aconv) v | _ => I) rhs [];
wenzelm@24259
    51
    val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
wenzelm@24259
    52
      if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
wenzelm@24259
    53
      else insert (op =) v | _ => I)) rhs [];
wenzelm@24259
    54
  in
wenzelm@24259
    55
    if not (check_head head) then
wenzelm@24259
    56
      err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
wenzelm@24259
    57
    else if not (null lhs_bads) then
wenzelm@24259
    58
      err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
wenzelm@24259
    59
    else if not (null lhs_dups) then
wenzelm@24259
    60
      err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
wenzelm@24259
    61
    else if not (null rhs_extras) then
wenzelm@24259
    62
      err ("Extra variables on rhs: " ^ display_terms rhs_extras)
wenzelm@24259
    63
    else if not (null rhs_extrasT) then
wenzelm@24259
    64
      err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
wenzelm@24259
    65
    else if exists_subterm (fn t => t aconv head) rhs then
wenzelm@24259
    66
      err "Entity to be defined occurs on rhs"
wenzelm@24259
    67
    else
wenzelm@24259
    68
      ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
wenzelm@24259
    69
  end;
wenzelm@24259
    70
wenzelm@24259
    71
(*!!x. c x == t[x] to c == %x. t[x]*)
wenzelm@24259
    72
fun abs_def eq =
wenzelm@24259
    73
  let
wenzelm@24259
    74
    val body = Term.strip_all_body eq;
wenzelm@24259
    75
    val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
wenzelm@24259
    76
    val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
wenzelm@24259
    77
    val (lhs', args) = Term.strip_comb lhs;
wenzelm@24259
    78
    val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
wenzelm@24259
    79
  in (lhs', rhs') end;
wenzelm@24259
    80
wenzelm@24259
    81
fun mk_defpair (lhs, rhs) =
wenzelm@24259
    82
  (case Term.head_of lhs of
wenzelm@24259
    83
    Const (name, _) =>
wenzelm@24259
    84
      (NameSpace.base name ^ "_def", Logic.mk_equals (lhs, rhs))
wenzelm@24259
    85
  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
wenzelm@24259
    86
wenzelm@24259
    87
end;