src/Pure/logic.ML

moved basic algebra of long names from structure NameSpace to Long_Name;

(*  Title:      Pure/logic.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Makarius

Abstract syntax operations of the Pure meta-logic.
*)

signature LOGIC =
sig
  val all: term -> term -> term
  val is_all: term -> bool
  val dest_all: term -> (string * typ) * term
  val mk_equals: term * term -> term
  val dest_equals: term -> term * term
  val implies: term
  val mk_implies: term * term -> term
  val dest_implies: term -> term * term
  val list_implies: term list * term -> term
  val strip_imp_prems: term -> term list
  val strip_imp_concl: term -> term
  val strip_prems: int * term list * term -> term list * term
  val count_prems: term -> int
  val nth_prem: int * term -> term
  val true_prop: term
  val conjunction: term
  val mk_conjunction: term * term -> term
  val mk_conjunction_list: term list -> term
  val mk_conjunction_balanced: term list -> term
  val dest_conjunction: term -> term * term
  val dest_conjunction_list: term -> term list
  val dest_conjunction_balanced: int -> term -> term list
  val dest_conjunctions: term -> term list
  val strip_horn: term -> term list * term
  val mk_type: typ -> term
  val dest_type: term -> typ
  val type_map: (term -> term) -> typ -> 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 name_classrel: string * string -> string
  val mk_classrel: class * class -> term
  val dest_classrel: term -> class * class
  val name_arities: arity -> string list
  val name_arity: string * sort list * class -> string
  val mk_arities: arity -> term list
  val dest_arity: term -> string * sort list * class
  val protectC: term
  val protect: term -> term
  val unprotect: term -> term
  val mk_term: term -> term
  val dest_term: 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
  val lift_all: int -> term -> term -> term
  val strip_assums_hyp: term -> term list
  val strip_assums_concl: term -> term
  val strip_params: term -> (string * typ) list
  val has_meta_prems: term -> bool
  val flatten_params: int -> term -> term
  val list_rename_params: string list * term -> term
  val assum_pairs: int * term -> (term*term)list
  val varifyT: typ -> typ
  val unvarifyT: typ -> typ
  val varify: term -> term
  val unvarify: term -> term
  val legacy_varifyT: typ -> typ
  val legacy_unvarifyT: typ -> typ
  val legacy_varify: term -> term
  val legacy_unvarify: term -> term
  val get_goal: term -> int -> term
  val goal_params: term -> int -> term * term list
  val prems_of_goal: term -> int -> term list
  val concl_of_goal: term -> int -> term
end;

structure Logic : LOGIC =
struct


(*** Abstract syntax operations on the meta-connectives ***)

(** all **)

fun all v t = Const ("all", (Term.fastype_of v --> propT) --> propT) $ lambda v t;

fun is_all (Const ("all", _) $ Abs _) = true
  | is_all _ = false;

fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) =
      let val (x, b) = Term.dest_abs abs  (*potentially slow*)
      in ((x, T), b) end
  | dest_all t = raise TERM ("dest_all", [t]);


(** equality **)

fun mk_equals (t, u) =
  let val T = Term.fastype_of t
  in Const ("==", T --> T --> propT) $ t $ u end;

fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
  | dest_equals t = raise TERM ("dest_equals", [t]);


(** implies **)

val implies = Const ("==>", propT --> propT --> propT);

fun mk_implies (A, B) = implies $ A $ B;

fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
  | dest_implies A = raise TERM ("dest_implies", [A]);


(** nested implications **)

(* [A1,...,An], B  goes to  A1==>...An==>B  *)
fun list_implies ([], B) = B
  | list_implies (A::As, B) = implies $ A $ list_implies(As,B);

(* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
  | strip_imp_prems _ = [];

(* A1==>...An==>B  goes to B, where B is not an implication *)
fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
  | strip_imp_concl A = A : term;

(*Strip and return premises: (i, [], A1==>...Ai==>B)
    goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
  if  i<0 or else i too big then raises  TERM*)
fun strip_prems (0, As, B) = (As, B)
  | strip_prems (i, As, Const("==>", _) $ A $ B) =
        strip_prems (i-1, A::As, B)
  | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);

(*Count premises -- quicker than (length o strip_prems) *)
fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
  | count_prems _ = 0;

(*Select Ai from A1 ==>...Ai==>B*)
fun nth_prem (1, Const ("==>", _) $ A $ _) = A
  | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
  | nth_prem (_, A) = raise TERM ("nth_prem", [A]);

(*strip a proof state (Horn clause):
  B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);



(** conjunction **)

val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);


(*A &&& B*)
fun mk_conjunction (A, B) = conjunction $ A $ B;

(*A &&& B &&& C -- improper*)
fun mk_conjunction_list [] = true_prop
  | mk_conjunction_list ts = foldr1 mk_conjunction ts;

(*(A &&& B) &&& (C &&& D) -- balanced*)
fun mk_conjunction_balanced [] = true_prop
  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;


(*A &&& B*)
fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
  | dest_conjunction t = raise TERM ("dest_conjunction", [t]);

(*A &&& B &&& C -- improper*)
fun dest_conjunction_list t =
  (case try dest_conjunction t of
    NONE => [t]
  | SOME (A, B) => A :: dest_conjunction_list B);

(*(A &&& B) &&& (C &&& D) -- balanced*)
fun dest_conjunction_balanced 0 _ = []
  | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;

(*((A &&& B) &&& C) &&& D &&& E -- flat*)
fun dest_conjunctions t =
  (case try dest_conjunction t of
    NONE => [t]
  | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);



(** types as terms **)

fun mk_type ty = Const ("TYPE", Term.itselfT ty);

fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
  | dest_type t = raise TERM ("dest_type", [t]);

fun type_map f = dest_type o f o mk_type;



(** type classes **)

(* const names *)

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, []);


(* class constraints *)

fun mk_inclass (ty, c) =
  Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;

fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
  | dest_inclass t = raise TERM ("dest_inclass", [t]);


(* class relations *)

fun name_classrel (c1, c2) =
  Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;

fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);

fun dest_classrel tm =
  (case dest_inclass tm of
    (TVar (_, [c1]), c2) => (c1, c2)
  | _ => raise TERM ("dest_classrel", [tm]));


(* type arities *)

fun name_arities (t, _, S) =
  let val b = Long_Name.base_name t
  in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;

fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));

fun mk_arities (t, Ss, S) =
  let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
  in map (fn c => mk_inclass (T, c)) S end;

fun dest_arity tm =
  let
    fun err () = raise TERM ("dest_arity", [tm]);

    val (ty, c) = dest_inclass tm;
    val (t, tvars) =
      (case ty of
        Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
      | _ => err ());
    val Ss =
      if has_duplicates (eq_fst (op =)) tvars then err ()
      else map snd tvars;
  in (t, Ss, c) end;



(** protected propositions and embedded terms **)

val protectC = Const ("prop", propT --> propT);
fun protect t = protectC $ t;

fun unprotect (Const ("prop", _) $ t) = t
  | unprotect t = raise TERM ("unprotect", [t]);


fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;

fun dest_term (Const ("Pure.term", _) $ t) = t
  | dest_term t = raise TERM ("dest_term", [t]);



(*** Low-level term operations ***)

(*Does t occur in u?  Or is alpha-convertible to u?
  The term t must contain no loose bound variables*)
fun occs (t, u) = exists_subterm (fn s => t aconv s) u;

(*Close up a formula over all free variables by quantification*)
fun close_form A =
  Term.list_all_free (rev (Term.add_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 =
  let
    fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
      | incr (Type (a, Ts)) = Type (a, incrs Ts)
      | incr _ = raise SAME
    and incrs (T :: Ts) =
        (incr T :: (incrs Ts handle SAME => Ts)
          handle SAME => T :: incrs Ts)
      | incrs [] = raise SAME;
  in incr end;

(*For all variables in the term, increment indexnames and lift over the Us
    result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
fun incr_indexes ([], 0) t = t
  | incr_indexes (Ts, k) t =
  let
    val n = length Ts;
    val incrT = if k = 0 then I else incrT k;

    fun incr lev (Var ((x, i), T)) =
          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))
      | incr lev (t $ u) =
          (incr lev t $ (incr lev u handle SAME => u)
            handle SAME => t $ incr lev u)
      | incr _ (Const (c, T)) = Const (c, incrT T)
      | incr _ (Free (x, T)) = Free (x, incrT T)
      | incr _ (t as Bound _) = t;
  in incr 0 t handle SAME => t end;

fun incr_tvar 0 T = T
  | incr_tvar k T = incrT k T handle SAME => T;

end;


(* Lifting functions from subgoal and increment:
    lift_abs operates on terms
    lift_all operates on propositions *)

fun lift_abs inc =
  let
    fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
      | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
  in lift [] end;

fun lift_all inc =
  let
    fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
      | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
  in lift [] end;

(*Strips assumptions in goal, yielding list of hypotheses.   *)
fun strip_assums_hyp B =
  let
    fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
      | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
          strip (map (incr_boundvars 1) Hs) t
      | strip Hs B = rev Hs
  in strip [] B end;

(*Strips assumptions in goal, yielding conclusion.   *)
fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
  | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
  | strip_assums_concl B = B;

(*Make a list of all the parameters in a subgoal, even if nested*)
fun strip_params (Const("==>", _) $ H $ B) = strip_params B
  | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
  | strip_params B = [];

(*test for nested meta connectives in prems*)
val has_meta_prems =
  let
    fun is_meta (Const ("==", _) $ _ $ _) = true
      | is_meta (Const ("==>", _) $ _ $ _) = true
      | is_meta (Const ("all", _) $ _) = true
      | is_meta _ = false;
    fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
      | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
      | ex_meta _ = false;
  in ex_meta end;

(*Removes the parameters from a subgoal and renumber bvars in hypotheses,
    where j is the total number of parameters (precomputed)
  If n>0 then deletes assumption n. *)
fun remove_params j n A =
    if j=0 andalso n<=0 then A  (*nothing left to do...*)
    else case A of
        Const("==>", _) $ H $ B =>
          if n=1 then                           (remove_params j (n-1) B)
          else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
      | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
      | _ => if n>0 then raise TERM("remove_params", [A])
             else A;

(*Move all parameters to the front of the subgoal, renaming them apart;
  if n>0 then deletes assumption n. *)
fun flatten_params n A =
    let val params = strip_params A;
        val vars = ListPair.zip (Name.variant_list [] (map #1 params),
                                 map #2 params)
    in  list_all (vars, remove_params (length vars) n A)
    end;

(*Makes parameters in a goal have the names supplied by the list cs.*)
fun list_rename_params (cs, Const("==>", _) $ A $ B) =
      implies $ A $ list_rename_params (cs, B)
  | list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) =
      a $ Abs(c, T, list_rename_params (cs, t))
  | list_rename_params (cs, B) = B;

(*** Treatment of "assume", "erule", etc. ***)

(*Strips assumptions in goal yielding
   HS = [Hn,...,H1],   params = [xm,...,x1], and B,
  where x1...xm are the parameters. This version (21.1.2005) REQUIRES
  the the parameters to be flattened, but it allows erule to work on
  assumptions of the form !!x. phi. Any !! after the outermost string
  will be regarded as belonging to the conclusion, and left untouched.
  Used ONLY by assum_pairs.
      Unless nasms<0, it can terminate the recursion early; that allows
  erule to work on assumptions of the form P==>Q.*)
fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
  | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
      strip_assums_imp (nasms-1, H::Hs, B)
  | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)


(*Strips OUTER parameters only, unlike similar legacy versions.*)
fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
      strip_assums_all ((a,T)::params, t)
  | strip_assums_all (params, B) = (params, B);

(*Produces disagreement pairs, one for each assumption proof, in order.
  A is the first premise of the lifted rule, and thus has the form
    H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
  nasms is the number of assumptions in the original subgoal, needed when B
    has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
fun assum_pairs(nasms,A) =
  let val (params, A') = strip_assums_all ([],A)
      val (Hs,B) = strip_assums_imp (nasms,[],A')
      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;


(* global schematic variables *)

fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
fun bad_fixed x = "Illegal fixed variable: " ^ quote x;

fun varifyT ty = ty |> Term.map_atyps
  (fn TFree (a, S) => TVar ((a, 0), S)
    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));

fun unvarifyT ty = ty |> Term.map_atyps
  (fn TVar ((a, 0), S) => TFree (a, S)
    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
    | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));

fun varify tm =
  tm |> Term.map_aterms
    (fn Free (x, T) => Var ((x, 0), T)
      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
      | t => t)
  |> Term.map_types varifyT
  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);

fun unvarify tm =
  tm |> Term.map_aterms
    (fn Var ((x, 0), T) => Free (x, T)
      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
      | Free (x, _) => raise TERM (bad_fixed x, [tm])
      | t => t)
  |> Term.map_types unvarifyT
  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);

val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);

val legacy_varify =
  Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
  Term.map_types legacy_varifyT;

val legacy_unvarify =
  Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
  Term.map_types legacy_unvarifyT;


(* goal states *)

fun get_goal st i = nth_prem (i, st)
  handle TERM _ => error "Goal number out of range";

(*reverses parameters for substitution*)
fun goal_params st i =
  let val gi = get_goal st i
      val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi))
  in (gi, rfrees) end;

fun concl_of_goal st i =
  let val (gi, rfrees) = goal_params st i
      val B = strip_assums_concl gi
  in subst_bounds (rfrees, B) end;

fun prems_of_goal st i =
  let val (gi, rfrees) = goal_params st i
      val As = strip_assums_hyp gi
  in map (fn A => subst_bounds (rfrees, A)) As end;

end;