src/Pure/primitive_defs.ML
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (20 months ago)
changeset 67131 85d10959c2e4
parent 64596 51f8e259de50
child 67721 5348bea4accd
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/primitive_defs.ML
     2     Author:     Makarius
     3 
     4 Primitive definition forms.
     5 *)
     6 
     7 signature PRIMITIVE_DEFS =
     8 sig
     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
    16 end;
    17 
    18 structure Primitive_Defs: PRIMITIVE_DEFS =
    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 
    26 (*c x == t[x] to !!x. c x == t[x]*)
    27 fun 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 (*!!x. c x == t[x] to c == %x. t[x]*)
    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;
    82     val rhs' = fold_rev (absfree o dest_Free) args rhs;
    83   in (lhs', rhs') end;
    84 
    85 end;