moved support for primitive defs to primitive_defs.ML;
authorwenzelm
Tue Aug 14 13:20:16 2007 +0200 (2007-08-14)
changeset 242582f399483535a
parent 24257 15a43b494878
child 24259 c9e05c49d02c
moved support for primitive defs to primitive_defs.ML;
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Tue Aug 14 13:20:15 2007 +0200
     1.2 +++ b/src/Pure/logic.ML	Tue Aug 14 13:20:16 2007 +0200
     1.3 @@ -43,10 +43,6 @@
     1.4    val name_arity: string * sort list * class -> string
     1.5    val mk_arities: arity -> term list
     1.6    val dest_arity: term -> string * sort list * class
     1.7 -  val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
     1.8 -    term -> (term * term) * term
     1.9 -  val abs_def: term -> term * term
    1.10 -  val mk_defpair: term * term -> string * term
    1.11    val protectC: term
    1.12    val protect: term -> term
    1.13    val unprotect: term -> term
    1.14 @@ -261,78 +257,7 @@
    1.15  
    1.16  
    1.17  
    1.18 -(** definitions **)
    1.19 -
    1.20 -fun term_kind (Const _) = "existing constant "
    1.21 -  | term_kind (Free _) = "free variable "
    1.22 -  | term_kind (Bound _) = "bound variable "
    1.23 -  | term_kind _ = "";
    1.24 -
    1.25 -(*c x == t[x] to !!x. c x == t[x]*)
    1.26 -fun dest_def pp check_head is_fixed is_fixedT eq =
    1.27 -  let
    1.28 -    fun err msg = raise TERM (msg, [eq]);
    1.29 -    val eq_vars = Term.strip_all_vars eq;
    1.30 -    val eq_body = Term.strip_all_body eq;
    1.31 -
    1.32 -    val display_terms = commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
    1.33 -    val display_types = commas_quote o map (Pretty.string_of_typ pp);
    1.34 -
    1.35 -    val (raw_lhs, rhs) = dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
    1.36 -    val lhs = Envir.beta_eta_contract raw_lhs;
    1.37 -    val (head, args) = Term.strip_comb lhs;
    1.38 -    val head_tfrees = Term.add_tfrees head [];
    1.39 -
    1.40 -    fun check_arg (Bound _) = true
    1.41 -      | check_arg (Free (x, _)) = not (is_fixed x)
    1.42 -      | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
    1.43 -      | check_arg _ = false;
    1.44 -    fun close_arg (Bound _) t = t
    1.45 -      | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
    1.46 -
    1.47 -    val lhs_bads = filter_out check_arg args;
    1.48 -    val lhs_dups = duplicates (op aconv) args;
    1.49 -    val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
    1.50 -      if is_fixed x orelse member (op aconv) args v then I
    1.51 -      else insert (op aconv) v | _ => I) rhs [];
    1.52 -    val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
    1.53 -      if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
    1.54 -      else insert (op =) v | _ => I)) rhs [];
    1.55 -  in
    1.56 -    if not (check_head head) then
    1.57 -      err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
    1.58 -    else if not (null lhs_bads) then
    1.59 -      err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
    1.60 -    else if not (null lhs_dups) then
    1.61 -      err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
    1.62 -    else if not (null rhs_extras) then
    1.63 -      err ("Extra variables on rhs: " ^ display_terms rhs_extras)
    1.64 -    else if not (null rhs_extrasT) then
    1.65 -      err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
    1.66 -    else if exists_subterm (fn t => t aconv head) rhs then
    1.67 -      err "Entity to be defined occurs on rhs"
    1.68 -    else ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (mk_equals (lhs, rhs)))))
    1.69 -  end;
    1.70 -
    1.71 -(*!!x. c x == t[x] to c == %x. t[x]*)
    1.72 -fun abs_def eq =
    1.73 -  let
    1.74 -    val body = Term.strip_all_body eq;
    1.75 -    val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
    1.76 -    val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body));
    1.77 -    val (lhs', args) = Term.strip_comb lhs;
    1.78 -    val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
    1.79 -  in (lhs', rhs') end;
    1.80 -
    1.81 -fun mk_defpair (lhs, rhs) =
    1.82 -  (case Term.head_of lhs of
    1.83 -    Const (name, _) =>
    1.84 -      (NameSpace.base name ^ "_def", mk_equals (lhs, rhs))
    1.85 -  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    1.86 -
    1.87 -
    1.88 -
    1.89 -(** protected propositions and embedded terms **)
    1.90 +  (** protected propositions and embedded terms **)
    1.91  
    1.92  val protectC = Const ("prop", propT --> propT);
    1.93  fun protect t = protectC $ t;