wenzelm@398: (* Title: Pure/logic.ML clasohm@0: ID: $Id$ clasohm@0: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: Copyright Cambridge University 1992 clasohm@0: clasohm@0: Supporting code for defining the abstract type "thm" clasohm@0: *) clasohm@0: clasohm@0: infix occs; clasohm@0: clasohm@0: signature LOGIC = clasohm@0: sig clasohm@0: val assum_pairs: term -> (term*term)list clasohm@0: val auto_rename: bool ref clasohm@0: val close_form: term -> term clasohm@0: val count_prems: term * int -> int clasohm@0: val dest_equals: term -> term * term clasohm@0: val dest_flexpair: term -> term * term clasohm@0: val dest_implies: term -> term * term wenzelm@398: val dest_inclass: term -> typ * class wenzelm@398: val dest_type: term -> typ clasohm@0: val flatten_params: int -> term -> term clasohm@0: val freeze_vars: term -> term clasohm@0: val incr_indexes: typ list * int -> term -> term clasohm@0: val lift_fns: term * int -> (term -> term) * (term -> term) clasohm@0: val list_flexpairs: (term*term)list * term -> term clasohm@0: val list_implies: term list * term -> term clasohm@0: val list_rename_params: string list * term -> term clasohm@0: val mk_equals: term * term -> term clasohm@0: val mk_flexpair: term * term -> term clasohm@0: val mk_implies: term * term -> term wenzelm@398: val mk_inclass: typ * class -> term wenzelm@398: val mk_type: typ -> term clasohm@0: val occs: term * term -> bool clasohm@0: val rule_of: (term*term)list * term list * term -> term clasohm@0: val set_rename_prefix: string -> unit clasohm@0: val skip_flexpairs: term -> term clasohm@0: val strip_assums_concl: term -> term clasohm@0: val strip_assums_hyp: term -> term list clasohm@0: val strip_flexpairs: term -> (term*term)list * term clasohm@0: val strip_horn: term -> (term*term)list * term list * term clasohm@0: val strip_imp_concl: term -> term clasohm@0: val strip_imp_prems: term -> term list clasohm@0: val strip_params: term -> (string * typ) list clasohm@0: val strip_prems: int * term list * term -> term list * term clasohm@0: val thaw_vars: term -> term clasohm@0: val varify: term -> term clasohm@0: end; clasohm@0: wenzelm@398: functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC = clasohm@0: struct wenzelm@398: wenzelm@398: structure Sign = Unify.Sign; wenzelm@398: structure Type = Sign.Type; clasohm@0: clasohm@0: (*** Abstract syntax operations on the meta-connectives ***) clasohm@0: clasohm@0: (** equality **) clasohm@0: lcp@64: (*Make an equality.*) lcp@64: fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; clasohm@0: clasohm@0: fun dest_equals (Const("==",_) $ t $ u) = (t,u) clasohm@0: | dest_equals t = raise TERM("dest_equals", [t]); clasohm@0: clasohm@0: (** implies **) clasohm@0: clasohm@0: fun mk_implies(A,B) = implies $ A $ B; clasohm@0: clasohm@0: fun dest_implies (Const("==>",_) $ A $ B) = (A,B) clasohm@0: | dest_implies A = raise TERM("dest_implies", [A]); clasohm@0: clasohm@0: (** nested implications **) clasohm@0: clasohm@0: (* [A1,...,An], B goes to A1==>...An==>B *) clasohm@0: fun list_implies ([], B) = B : term clasohm@0: | list_implies (A::AS, B) = implies $ A $ list_implies(AS,B); clasohm@0: clasohm@0: (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) clasohm@0: fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B clasohm@0: | strip_imp_prems _ = []; clasohm@0: clasohm@0: (* A1==>...An==>B goes to B, where B is not an implication *) clasohm@0: fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B clasohm@0: | strip_imp_concl A = A : term; clasohm@0: clasohm@0: (*Strip and return premises: (i, [], A1==>...Ai==>B) clasohm@0: goes to ([Ai, A(i-1),...,A1] , B) (REVERSED) clasohm@0: if i<0 or else i too big then raises TERM*) clasohm@0: fun strip_prems (0, As, B) = (As, B) clasohm@0: | strip_prems (i, As, Const("==>", _) $ A $ B) = clasohm@0: strip_prems (i-1, A::As, B) clasohm@0: | strip_prems (_, As, A) = raise TERM("strip_prems", A::As); clasohm@0: clasohm@0: (*Count premises -- quicker than (length ostrip_prems) *) clasohm@0: fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1) clasohm@0: | count_prems (_,n) = n; clasohm@0: clasohm@0: (** flex-flex constraints **) clasohm@0: lcp@64: (*Make a constraint.*) lcp@64: fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u; clasohm@0: clasohm@0: fun dest_flexpair (Const("=?=",_) $ t $ u) = (t,u) clasohm@0: | dest_flexpair t = raise TERM("dest_flexpair", [t]); clasohm@0: clasohm@0: (*make flexflex antecedents: ( [(a1,b1),...,(an,bn)] , C ) clasohm@0: goes to (a1=?=b1) ==>...(an=?=bn)==>C *) clasohm@0: fun list_flexpairs ([], A) = A clasohm@0: | list_flexpairs ((t,u)::pairs, A) = clasohm@0: implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A); clasohm@0: clasohm@0: (*Make the object-rule tpairs==>As==>B *) clasohm@0: fun rule_of (tpairs, As, B) = list_flexpairs(tpairs, list_implies(As, B)); clasohm@0: clasohm@0: (*Remove and return flexflex pairs: clasohm@0: (a1=?=b1)==>...(an=?=bn)==>C to ( [(a1,b1),...,(an,bn)] , C ) clasohm@0: [Tail recursive in order to return a pair of results] *) clasohm@0: fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) = clasohm@0: strip_flex_aux ((t,u)::pairs, C) clasohm@0: | strip_flex_aux (pairs,C) = (rev pairs, C); clasohm@0: clasohm@0: fun strip_flexpairs A = strip_flex_aux([], A); clasohm@0: clasohm@0: (*Discard flexflex pairs*) clasohm@0: fun skip_flexpairs (Const("==>", _) $ (Const("=?=",_)$_$_) $ C) = clasohm@0: skip_flexpairs C clasohm@0: | skip_flexpairs C = C; clasohm@0: clasohm@0: (*strip a proof state (Horn clause): clasohm@0: (a1==b1)==>...(am==bm)==>B1==>...Bn==>C clasohm@0: goes to ( [(a1,b1),...,(am,bm)] , [B1,...,Bn] , C) *) clasohm@0: fun strip_horn A = clasohm@0: let val (tpairs,horn) = strip_flexpairs A clasohm@0: in (tpairs, strip_imp_prems horn, strip_imp_concl horn) end; clasohm@0: wenzelm@398: (** types as terms **) wenzelm@398: wenzelm@398: fun mk_type ty = Const ("TYPE", itselfT ty); wenzelm@398: wenzelm@398: fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty wenzelm@398: | dest_type t = raise TERM ("dest_type", [t]); wenzelm@398: wenzelm@447: (** class constraints **) wenzelm@398: wenzelm@398: fun mk_inclass (ty, c) = wenzelm@398: Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty; wenzelm@398: wenzelm@398: fun dest_inclass (t as Const (c_class, _) $ ty) = wenzelm@398: ((dest_type ty, Sign.class_of_const c_class) wenzelm@398: handle TERM _ => raise TERM ("dest_inclass", [t])) wenzelm@398: | dest_inclass t = raise TERM ("dest_inclass", [t]); wenzelm@398: clasohm@0: clasohm@0: (*** Low-level term operations ***) clasohm@0: clasohm@0: (*Does t occur in u? Or is alpha-convertible to u? clasohm@0: The term t must contain no loose bound variables*) clasohm@0: fun t occs u = (t aconv u) orelse clasohm@0: (case u of clasohm@0: Abs(_,_,body) => t occs body clasohm@0: | f$t' => t occs f orelse t occs t' clasohm@0: | _ => false); clasohm@0: clasohm@0: (*Close up a formula over all free variables by quantification*) clasohm@0: fun close_form A = clasohm@0: list_all_free (map dest_Free (sort atless (term_frees A)), clasohm@0: A); clasohm@0: clasohm@0: clasohm@0: (*Freeze all (T)Vars by turning them into (T)Frees*) clasohm@0: fun freeze_vars(Var(ixn,T)) = Free(Syntax.string_of_vname ixn, clasohm@0: Type.freeze_vars T) clasohm@0: | freeze_vars(Const(a,T)) = Const(a,Type.freeze_vars T) clasohm@0: | freeze_vars(Free(a,T)) = Free(a,Type.freeze_vars T) clasohm@0: | freeze_vars(s$t) = freeze_vars s $ freeze_vars t clasohm@0: | freeze_vars(Abs(a,T,t)) = Abs(a,Type.freeze_vars T,freeze_vars t) clasohm@0: | freeze_vars(b) = b; clasohm@0: clasohm@0: (*Reverse the effect of freeze_vars*) clasohm@0: fun thaw_vars(Const(a,T)) = Const(a,Type.thaw_vars T) clasohm@0: | thaw_vars(Free(a,T)) = clasohm@0: let val T' = Type.thaw_vars T clasohm@0: in case explode a of clasohm@0: "?"::vn => let val (ixn,_) = Syntax.scan_varname vn clasohm@0: in Var(ixn,T') end clasohm@0: | _ => Free(a,T') clasohm@0: end clasohm@0: | thaw_vars(Abs(a,T,t)) = Abs(a,Type.thaw_vars T, thaw_vars t) clasohm@0: | thaw_vars(s$t) = thaw_vars s $ thaw_vars t clasohm@0: | thaw_vars(b) = b; clasohm@0: clasohm@0: clasohm@0: (*** Specialized operations for resolution... ***) clasohm@0: clasohm@0: (*For all variables in the term, increment indexnames and lift over the Us clasohm@0: result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *) clasohm@0: fun incr_indexes (Us: typ list, inc:int) t = clasohm@0: let fun incr (Var ((a,i), T), lev) = clasohm@0: Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T), clasohm@0: lev, length Us) clasohm@0: | incr (Abs (a,T,body), lev) = clasohm@0: Abs (a, incr_tvar inc T, incr(body,lev+1)) clasohm@0: | incr (Const(a,T),_) = Const(a, incr_tvar inc T) clasohm@0: | incr (Free(a,T),_) = Free(a, incr_tvar inc T) clasohm@0: | incr (f$t, lev) = incr(f,lev) $ incr(t,lev) clasohm@0: | incr (t,lev) = t clasohm@0: in incr(t,0) end; clasohm@0: clasohm@0: (*Make lifting functions from subgoal and increment. clasohm@0: lift_abs operates on tpairs (unification constraints) clasohm@0: lift_all operates on propositions *) clasohm@0: fun lift_fns (B,inc) = clasohm@0: let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u clasohm@0: | lift_abs (Us, Const("all",_)$Abs(a,T,t)) u = clasohm@0: Abs(a, T, lift_abs (T::Us, t) u) clasohm@0: | lift_abs (Us, _) u = incr_indexes(rev Us, inc) u clasohm@0: fun lift_all (Us, Const("==>", _) $ A $ B) u = clasohm@0: implies $ A $ lift_all (Us,B) u clasohm@0: | lift_all (Us, Const("all",_)$Abs(a,T,t)) u = clasohm@0: all T $ Abs(a, T, lift_all (T::Us,t) u) clasohm@0: | lift_all (Us, _) u = incr_indexes(rev Us, inc) u; clasohm@0: in (lift_abs([],B), lift_all([],B)) end; clasohm@0: clasohm@0: (*Strips assumptions in goal, yielding list of hypotheses. *) clasohm@0: fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B clasohm@0: | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t clasohm@0: | strip_assums_hyp B = []; clasohm@0: clasohm@0: (*Strips assumptions in goal, yielding conclusion. *) clasohm@0: fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B clasohm@0: | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t clasohm@0: | strip_assums_concl B = B; clasohm@0: clasohm@0: (*Make a list of all the parameters in a subgoal, even if nested*) clasohm@0: fun strip_params (Const("==>", _) $ H $ B) = strip_params B clasohm@0: | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t clasohm@0: | strip_params B = []; clasohm@0: clasohm@0: (*Removes the parameters from a subgoal and renumber bvars in hypotheses, clasohm@0: where j is the total number of parameters (precomputed) clasohm@0: If n>0 then deletes assumption n. *) clasohm@0: fun remove_params j n A = clasohm@0: if j=0 andalso n<=0 then A (*nothing left to do...*) clasohm@0: else case A of clasohm@0: Const("==>", _) $ H $ B => clasohm@0: if n=1 then (remove_params j (n-1) B) clasohm@0: else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B) clasohm@0: | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t clasohm@0: | _ => if n>0 then raise TERM("remove_params", [A]) clasohm@0: else A; clasohm@0: clasohm@0: (** Auto-renaming of parameters in subgoals **) clasohm@0: clasohm@0: val auto_rename = ref false clasohm@0: and rename_prefix = ref "ka"; clasohm@0: clasohm@0: (*rename_prefix is not exported; it is set by this function.*) clasohm@0: fun set_rename_prefix a = clasohm@0: if a<>"" andalso forall is_letter (explode a) clasohm@0: then (rename_prefix := a; auto_rename := true) clasohm@0: else error"rename prefix must be nonempty and consist of letters"; clasohm@0: clasohm@0: (*Makes parameters in a goal have distinctive names (not guaranteed unique!) clasohm@0: A name clash could cause the printer to rename bound vars; clasohm@0: then res_inst_tac would not work properly.*) clasohm@0: fun rename_vars (a, []) = [] clasohm@0: | rename_vars (a, (_,T)::vars) = clasohm@0: (a,T) :: rename_vars (bump_string a, vars); clasohm@0: clasohm@0: (*Move all parameters to the front of the subgoal, renaming them apart; clasohm@0: if n>0 then deletes assumption n. *) clasohm@0: fun flatten_params n A = clasohm@0: let val params = strip_params A; clasohm@0: val vars = if !auto_rename clasohm@0: then rename_vars (!rename_prefix, params) clasohm@0: else variantlist(map #1 params,[]) ~~ map #2 params clasohm@0: in list_all (vars, remove_params (length vars) n A) clasohm@0: end; clasohm@0: clasohm@0: (*Makes parameters in a goal have the names supplied by the list cs.*) clasohm@0: fun list_rename_params (cs, Const("==>", _) $ A $ B) = clasohm@0: implies $ A $ list_rename_params (cs, B) clasohm@0: | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = clasohm@0: all T $ Abs(c, T, list_rename_params (cs, t)) clasohm@0: | list_rename_params (cs, B) = B; clasohm@0: clasohm@0: (*Strips assumptions in goal yielding ( [Hn,...,H1], [xm,...,x1], B ) clasohm@0: where H1,...,Hn are the hypotheses and x1...xm are the parameters. *) clasohm@0: fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) = clasohm@0: strip_assums_aux (H::Hs, params, B) clasohm@0: | strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) = clasohm@0: strip_assums_aux (Hs, (a,T)::params, t) clasohm@0: | strip_assums_aux (Hs, params, B) = (Hs, params, B); clasohm@0: clasohm@0: fun strip_assums A = strip_assums_aux ([],[],A); clasohm@0: clasohm@0: clasohm@0: (*Produces disagreement pairs, one for each assumption proof, in order. clasohm@0: A is the first premise of the lifted rule, and thus has the form clasohm@0: H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B) *) clasohm@0: fun assum_pairs A = clasohm@0: let val (Hs, params, B) = strip_assums A clasohm@0: val D = Unify.rlist_abs(params, B) clasohm@0: fun pairrev ([],pairs) = pairs clasohm@0: | pairrev (H::Hs,pairs) = clasohm@0: pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs) clasohm@0: in pairrev (Hs,[]) (*WAS: map pair (rev Hs) *) clasohm@0: end; clasohm@0: clasohm@0: clasohm@0: (*Converts Frees to Vars and TFrees to TVars so that axioms can be written clasohm@0: without (?) everywhere*) clasohm@0: fun varify (Const(a,T)) = Const(a, Type.varifyT T) clasohm@0: | varify (Free(a,T)) = Var((a,0), Type.varifyT T) clasohm@0: | varify (Var(ixn,T)) = Var(ixn, Type.varifyT T) clasohm@0: | varify (Abs (a,T,body)) = Abs (a, Type.varifyT T, varify body) clasohm@0: | varify (f$t) = varify f $ varify t clasohm@0: | varify t = t; clasohm@0: clasohm@0: end;