# HG changeset patch # User wenzelm # Date 1139255945 -3600 # Node ID b401ee1cda14ab97ab71088bb09b3bcd51358d00 # Parent 0eb35519f0f3188778a5512269afb00795262c26 added generic dest_def (mostly from theory.ML); added abs_def (from Isar/local_defs.ML); added const_of_class/class_of_const (from sign.ML); added combound, rlist_abs (from unify.ML); diff -r 0eb35519f0f3 -r b401ee1cda14 src/Pure/logic.ML --- a/src/Pure/logic.ML Mon Feb 06 20:59:04 2006 +0100 +++ b/src/Pure/logic.ML Mon Feb 06 20:59:05 2006 +0100 @@ -28,17 +28,24 @@ val dest_conjunction: term -> term * term val dest_conjunctions: term -> term list val strip_horn: term -> term list * term + val dest_type: term -> typ + val const_of_class: class -> string + val class_of_const: string -> class + val mk_inclass: typ * class -> term + val dest_inclass: term -> typ * class + val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) -> + term -> (term * term) * term + val abs_def: term -> term * term val mk_cond_defpair: term list -> term * term -> string * term val mk_defpair: term * term -> string * term val mk_type: typ -> term - val dest_type: term -> typ - val mk_inclass: typ * class -> term - val dest_inclass: term -> typ * class val protectC: term val protect: term -> term val unprotect: term -> term val occs: term * term -> bool val close_form: term -> term + val combound: term * int * int -> term + val rlist_abs: (string * typ) list * term -> term val incr_indexes: typ list * int -> term -> term val incr_tvar: int -> typ -> typ val lift_abs: int -> term -> term -> term @@ -167,17 +174,6 @@ -(** definitions **) - -fun mk_cond_defpair As (lhs, rhs) = - (case Term.head_of lhs of - Const (name, _) => - (Sign.base_name name ^ "_def", list_implies (As, mk_equals (lhs, rhs))) - | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); - -fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs; - - (** types as terms **) fun mk_type ty = Const ("TYPE", itselfT ty); @@ -188,15 +184,87 @@ (** class constraints **) +val classN = "_class"; + +val const_of_class = suffix classN; +fun class_of_const c = unsuffix classN c + handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []); + fun mk_inclass (ty, c) = - Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty; + Const (const_of_class c, itselfT ty --> propT) $ mk_type ty; fun dest_inclass (t as Const (c_class, _) $ ty) = - ((dest_type ty, Sign.class_of_const c_class) + ((dest_type ty, class_of_const c_class) handle TERM _ => raise TERM ("dest_inclass", [t])) | dest_inclass t = raise TERM ("dest_inclass", [t]); + +(** definitions **) + +(*c x == t[x] to !!x. c x == t[x]*) +fun dest_def pp check_head is_fixed is_fixedT eq = + let + fun err msg = raise TERM (msg, [eq]); + val bound_vars = Syntax.bound_vars (Term.strip_all_vars eq); + val display_terms = commas_quote o map (Pretty.string_of_term pp o bound_vars); + val display_types = commas_quote o map (Pretty.string_of_typ pp); + + val (lhs, rhs) = dest_equals (Term.strip_all_body eq) + handle TERM _ => err "Not a meta-equality (==)"; + val (head, args) = Term.strip_comb (Envir.beta_eta_contract lhs); + val head_tfrees = Term.add_tfrees head []; + + fun check_arg (Bound _) = true + | check_arg (Free (x, _)) = not (is_fixed x) + | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true + | check_arg _ = false; + fun close_arg (Bound _) t = t + | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t; + + val lhs_bads = filter_out check_arg args; + val lhs_dups = gen_duplicates (op aconv) args; + val rhs_extras = Term.fold_aterms (fn v as Free (x, _) => + if is_fixed x orelse member (op aconv) args v then I + else insert (op aconv) v | _ => I) rhs []; + val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) => + if is_fixedT a orelse member (op =) head_tfrees (a, S) then I + else insert (op =) v | _ => I)) rhs []; + in + if not (check_head head) then + err ("Bad head of lhs: " ^ display_terms [head]) + else if not (null lhs_bads) then + err ("Bad arguments on lhs: " ^ display_terms lhs_bads) + else if not (null lhs_dups) then + err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups) + else if not (null rhs_extras) then + err ("Extra variables on rhs: " ^ display_terms rhs_extras) + else if not (null rhs_extrasT) then + err ("Extra type variables on rhs: " ^ display_types rhs_extrasT) + else if exists_subterm (fn t => t aconv head) rhs then + err "Entity to be defined occurs on rhs" + else ((lhs, rhs), fold_rev close_arg args eq) + end; + +(*!!x. c x == t[x] to c == %x. t[x]*) +fun abs_def eq = + let + val body = Term.strip_all_body eq; + val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); + val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body)); + val (lhs', args) = Term.strip_comb lhs; + val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs); + in (lhs', rhs') end; + +fun mk_cond_defpair As (lhs, rhs) = + (case Term.head_of lhs of + Const (name, _) => + (NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs))) + | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); + +fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs; + + (** protected propositions **) val protectC = Const ("prop", propT --> propT); @@ -218,8 +286,18 @@ list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A); + (*** Specialized operations for resolution... ***) +(*computes t(Bound(n+k-1),...,Bound(n)) *) +fun combound (t, n, k) = + if k>0 then combound (t,n+1,k-1) $ (Bound n) else t; + +(* ([xn,...,x1], t) ======> (x1,...,xn)t *) +fun rlist_abs ([], body) = body + | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); + + local exception SAME in fun incrT k = @@ -242,7 +320,7 @@ val incrT = if k = 0 then I else incrT k; fun incr lev (Var ((x, i), T)) = - Unify.combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n) + combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n) | incr lev (Abs (x, T, body)) = (Abs (x, incrT T, incr (lev + 1) body handle SAME => body) handle SAME => Abs (x, T, incr (lev + 1) body)) @@ -385,15 +463,14 @@ fun assum_pairs(nasms,A) = let val (params, A') = strip_assums_all ([],A) val (Hs,B) = strip_assums_imp (nasms,[],A') - fun abspar t = Unify.rlist_abs(params, t) + fun abspar t = rlist_abs(params, t) val D = abspar B fun pairrev ([], pairs) = pairs | pairrev (H::Hs, pairs) = pairrev(Hs, (abspar H, D) :: pairs) in pairrev (Hs,[]) end; -(*Converts Frees to Vars and TFrees to TVars so that axioms can be written - without (?) everywhere*) +(*Converts Frees to Vars and TFrees to TVars*) fun varify (Const(a, T)) = Const (a, Type.varifyT T) | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T) | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T) @@ -401,7 +478,7 @@ | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body) | varify (f $ t) = varify f $ varify t; -(*Inverse of varify. Converts axioms back to their original form.*) +(*Inverse of varify.*) fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T) | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T) | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)