src/Pure/logic.ML
changeset 18938 b401ee1cda14
parent 18762 9098c92a945f
child 18964 67f572e03236
     1.1 --- a/src/Pure/logic.ML	Mon Feb 06 20:59:04 2006 +0100
     1.2 +++ b/src/Pure/logic.ML	Mon Feb 06 20:59:05 2006 +0100
     1.3 @@ -28,17 +28,24 @@
     1.4    val dest_conjunction: term -> term * term
     1.5    val dest_conjunctions: term -> term list
     1.6    val strip_horn: term -> term list * term
     1.7 +  val dest_type: term -> typ
     1.8 +  val const_of_class: class -> string
     1.9 +  val class_of_const: string -> class
    1.10 +  val mk_inclass: typ * class -> term
    1.11 +  val dest_inclass: term -> typ * class
    1.12 +  val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
    1.13 +    term -> (term * term) * term
    1.14 +  val abs_def: term -> term * term
    1.15    val mk_cond_defpair: term list -> term * term -> string * term
    1.16    val mk_defpair: term * term -> string * term
    1.17    val mk_type: typ -> term
    1.18 -  val dest_type: term -> typ
    1.19 -  val mk_inclass: typ * class -> term
    1.20 -  val dest_inclass: term -> typ * class
    1.21    val protectC: term
    1.22    val protect: term -> term
    1.23    val unprotect: term -> term
    1.24    val occs: term * term -> bool
    1.25    val close_form: term -> term
    1.26 +  val combound: term * int * int -> term
    1.27 +  val rlist_abs: (string * typ) list * term -> term
    1.28    val incr_indexes: typ list * int -> term -> term
    1.29    val incr_tvar: int -> typ -> typ
    1.30    val lift_abs: int -> term -> term -> term
    1.31 @@ -167,17 +174,6 @@
    1.32  
    1.33  
    1.34  
    1.35 -(** definitions **)
    1.36 -
    1.37 -fun mk_cond_defpair As (lhs, rhs) =
    1.38 -  (case Term.head_of lhs of
    1.39 -    Const (name, _) =>
    1.40 -      (Sign.base_name name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
    1.41 -  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    1.42 -
    1.43 -fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
    1.44 -
    1.45 -
    1.46  (** types as terms **)
    1.47  
    1.48  fun mk_type ty = Const ("TYPE", itselfT ty);
    1.49 @@ -188,15 +184,87 @@
    1.50  
    1.51  (** class constraints **)
    1.52  
    1.53 +val classN = "_class";
    1.54 +
    1.55 +val const_of_class = suffix classN;
    1.56 +fun class_of_const c = unsuffix classN c
    1.57 +  handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
    1.58 +
    1.59  fun mk_inclass (ty, c) =
    1.60 -  Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty;
    1.61 +  Const (const_of_class c, itselfT ty --> propT) $ mk_type ty;
    1.62  
    1.63  fun dest_inclass (t as Const (c_class, _) $ ty) =
    1.64 -      ((dest_type ty, Sign.class_of_const c_class)
    1.65 +      ((dest_type ty, class_of_const c_class)
    1.66          handle TERM _ => raise TERM ("dest_inclass", [t]))
    1.67    | dest_inclass t = raise TERM ("dest_inclass", [t]);
    1.68  
    1.69  
    1.70 +
    1.71 +(** definitions **)
    1.72 +
    1.73 +(*c x == t[x] to !!x. c x == t[x]*)
    1.74 +fun dest_def pp check_head is_fixed is_fixedT eq =
    1.75 +  let
    1.76 +    fun err msg = raise TERM (msg, [eq]);
    1.77 +    val bound_vars = Syntax.bound_vars (Term.strip_all_vars eq);
    1.78 +    val display_terms = commas_quote o map (Pretty.string_of_term pp o bound_vars);
    1.79 +    val display_types = commas_quote o map (Pretty.string_of_typ pp);
    1.80 +
    1.81 +    val (lhs, rhs) = dest_equals (Term.strip_all_body eq)
    1.82 +      handle TERM _ => err "Not a meta-equality (==)";
    1.83 +    val (head, args) = Term.strip_comb (Envir.beta_eta_contract lhs);
    1.84 +    val head_tfrees = Term.add_tfrees head [];
    1.85 +
    1.86 +    fun check_arg (Bound _) = true
    1.87 +      | check_arg (Free (x, _)) = not (is_fixed x)
    1.88 +      | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
    1.89 +      | check_arg _ = false;
    1.90 +    fun close_arg (Bound _) t = t
    1.91 +      | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
    1.92 +
    1.93 +    val lhs_bads = filter_out check_arg args;
    1.94 +    val lhs_dups = gen_duplicates (op aconv) args;
    1.95 +    val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
    1.96 +      if is_fixed x orelse member (op aconv) args v then I
    1.97 +      else insert (op aconv) v | _ => I) rhs [];
    1.98 +    val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
    1.99 +      if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
   1.100 +      else insert (op =) v | _ => I)) rhs [];
   1.101 +  in
   1.102 +    if not (check_head head) then
   1.103 +      err ("Bad head of lhs: " ^ display_terms [head])
   1.104 +    else if not (null lhs_bads) then
   1.105 +      err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
   1.106 +    else if not (null lhs_dups) then
   1.107 +      err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
   1.108 +    else if not (null rhs_extras) then
   1.109 +      err ("Extra variables on rhs: " ^ display_terms rhs_extras)
   1.110 +    else if not (null rhs_extrasT) then
   1.111 +      err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
   1.112 +    else if exists_subterm (fn t => t aconv head) rhs then
   1.113 +      err "Entity to be defined occurs on rhs"
   1.114 +    else ((lhs, rhs), fold_rev close_arg args eq)
   1.115 +  end;
   1.116 +
   1.117 +(*!!x. c x == t[x] to c == %x. t[x]*)
   1.118 +fun abs_def eq =
   1.119 +  let
   1.120 +    val body = Term.strip_all_body eq;
   1.121 +    val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
   1.122 +    val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body));
   1.123 +    val (lhs', args) = Term.strip_comb lhs;
   1.124 +    val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
   1.125 +  in (lhs', rhs') end;
   1.126 +
   1.127 +fun mk_cond_defpair As (lhs, rhs) =
   1.128 +  (case Term.head_of lhs of
   1.129 +    Const (name, _) =>
   1.130 +      (NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
   1.131 +  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   1.132 +
   1.133 +fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
   1.134 +
   1.135 +
   1.136  (** protected propositions **)
   1.137  
   1.138  val protectC = Const ("prop", propT --> propT);
   1.139 @@ -218,8 +286,18 @@
   1.140    list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
   1.141  
   1.142  
   1.143 +
   1.144  (*** Specialized operations for resolution... ***)
   1.145  
   1.146 +(*computes t(Bound(n+k-1),...,Bound(n))  *)
   1.147 +fun combound (t, n, k) =
   1.148 +    if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   1.149 +
   1.150 +(* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   1.151 +fun rlist_abs ([], body) = body
   1.152 +  | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   1.153 +
   1.154 +
   1.155  local exception SAME in
   1.156  
   1.157  fun incrT k =
   1.158 @@ -242,7 +320,7 @@
   1.159      val incrT = if k = 0 then I else incrT k;
   1.160  
   1.161      fun incr lev (Var ((x, i), T)) =
   1.162 -          Unify.combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   1.163 +          combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   1.164        | incr lev (Abs (x, T, body)) =
   1.165            (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   1.166              handle SAME => Abs (x, T, incr (lev + 1) body))
   1.167 @@ -385,15 +463,14 @@
   1.168  fun assum_pairs(nasms,A) =
   1.169    let val (params, A') = strip_assums_all ([],A)
   1.170        val (Hs,B) = strip_assums_imp (nasms,[],A')
   1.171 -      fun abspar t = Unify.rlist_abs(params, t)
   1.172 +      fun abspar t = rlist_abs(params, t)
   1.173        val D = abspar B
   1.174        fun pairrev ([], pairs) = pairs
   1.175          | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   1.176    in  pairrev (Hs,[])
   1.177    end;
   1.178  
   1.179 -(*Converts Frees to Vars and TFrees to TVars so that axioms can be written
   1.180 -  without (?) everywhere*)
   1.181 +(*Converts Frees to Vars and TFrees to TVars*)
   1.182  fun varify (Const(a, T)) = Const (a, Type.varifyT T)
   1.183    | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T)
   1.184    | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T)
   1.185 @@ -401,7 +478,7 @@
   1.186    | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body)
   1.187    | varify (f $ t) = varify f $ varify t;
   1.188  
   1.189 -(*Inverse of varify.  Converts axioms back to their original form.*)
   1.190 +(*Inverse of varify.*)
   1.191  fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T)
   1.192    | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T)
   1.193    | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)