src/Pure/thm.ML
author paulson
Wed Aug 18 10:54:44 1999 +0200 (1999-08-18)
changeset 7248 322151fe6f02
parent 7070 893e5a8a8d46
child 7264 d55cd903c93d
permissions -rw-r--r--
new primitive rule permute_prems to underlie defer_tac and rotate_prems
     1 (*  Title:      Pure/thm.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 The core of Isabelle's Meta Logic: certified types and terms, meta
     7 theorems, meta rules (including resolution and simplification).
     8 *)
     9 
    10 signature BASIC_THM =
    11   sig
    12   (*certified types*)
    13   type ctyp
    14   val rep_ctyp          : ctyp -> {sign: Sign.sg, T: typ}
    15   val typ_of            : ctyp -> typ
    16   val ctyp_of           : Sign.sg -> typ -> ctyp
    17   val read_ctyp         : Sign.sg -> string -> ctyp
    18 
    19   (*certified terms*)
    20   type cterm
    21   exception CTERM of string
    22   val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
    23   val crep_cterm        : cterm -> {sign: Sign.sg, t: term, T: ctyp, maxidx: int}
    24   val term_of           : cterm -> term
    25   val cterm_of          : Sign.sg -> term -> cterm
    26   val ctyp_of_term      : cterm -> ctyp
    27   val read_cterm        : Sign.sg -> string * typ -> cterm
    28   val cterm_fun         : (term -> term) -> (cterm -> cterm)
    29   val dest_comb         : cterm -> cterm * cterm
    30   val dest_abs          : cterm -> cterm * cterm
    31   val adjust_maxidx     : cterm -> cterm
    32   val capply            : cterm -> cterm -> cterm
    33   val cabs              : cterm -> cterm -> cterm
    34   val read_def_cterm    :
    35     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    36     string list -> bool -> string * typ -> cterm * (indexname * typ) list
    37   val read_def_cterms   :
    38     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    39     string list -> bool -> (string * typ)list
    40     -> cterm list * (indexname * typ)list
    41 
    42   (*proof terms [must DUPLICATE declaration as a specification]*)
    43   datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
    44   type tag		(* = string * string list *)
    45   val keep_derivs       : deriv_kind ref
    46   datatype rule = 
    47       MinProof                          
    48     | Oracle		  of string * Sign.sg * Object.T
    49     | Axiom               of string * tag list
    50     | Theorem             of string * tag list
    51     | Assume              of cterm
    52     | Implies_intr        of cterm
    53     | Implies_intr_shyps
    54     | Implies_intr_hyps
    55     | Implies_elim 
    56     | Forall_intr         of cterm
    57     | Forall_elim         of cterm
    58     | Reflexive           of cterm
    59     | Symmetric 
    60     | Transitive
    61     | Beta_conversion     of cterm
    62     | Extensional
    63     | Abstract_rule       of string * cterm
    64     | Combination
    65     | Equal_intr
    66     | Equal_elim
    67     | Trivial             of cterm
    68     | Lift_rule           of cterm * int 
    69     | Assumption          of int * Envir.env option
    70     | Rotate_rule         of int * int
    71     | Permute_prems       of int * int
    72     | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
    73     | Bicompose           of bool * bool * int * int * Envir.env
    74     | Flexflex_rule       of Envir.env            
    75     | Class_triv          of class       
    76     | VarifyT		  of string list
    77     | FreezeT
    78     | RewriteC            of cterm
    79     | CongC               of cterm
    80     | Rewrite_cterm       of cterm
    81     | Rename_params_rule  of string list * int;
    82   type deriv	(* = rule mtree *)
    83 
    84   (*meta theorems*)
    85   type thm
    86   val rep_thm           : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
    87                                   shyps: sort list, hyps: term list, 
    88                                   prop: term}
    89   val crep_thm          : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
    90                                   shyps: sort list, hyps: cterm list, 
    91                                   prop: cterm}
    92   exception THM of string * int * thm list
    93   type 'a attribute 	(* = 'a * thm -> 'a * thm *)
    94   val eq_thm		: thm * thm -> bool
    95   val sign_of_thm       : thm -> Sign.sg
    96   val transfer_sg	: Sign.sg -> thm -> thm
    97   val transfer		: theory -> thm -> thm
    98   val tpairs_of         : thm -> (term * term) list
    99   val prems_of          : thm -> term list
   100   val nprems_of         : thm -> int
   101   val concl_of          : thm -> term
   102   val cprop_of          : thm -> cterm
   103   val extra_shyps       : thm -> sort list
   104   val force_strip_shyps : bool ref      (* FIXME tmp (since 1995/08/01) *)
   105   val strip_shyps       : thm -> thm
   106   val implies_intr_shyps: thm -> thm
   107   val get_axiom         : theory -> xstring -> thm
   108   val def_name		: string -> string
   109   val get_def           : theory -> xstring -> thm
   110   val axioms_of         : theory -> (string * thm) list
   111 
   112   (*meta rules*)
   113   val assume            : cterm -> thm
   114   val compress          : thm -> thm
   115   val implies_intr      : cterm -> thm -> thm
   116   val implies_elim      : thm -> thm -> thm
   117   val forall_intr       : cterm -> thm -> thm
   118   val forall_elim       : cterm -> thm -> thm
   119   val reflexive         : cterm -> thm
   120   val symmetric         : thm -> thm
   121   val transitive        : thm -> thm -> thm
   122   val beta_conversion   : cterm -> thm
   123   val extensional       : thm -> thm
   124   val abstract_rule     : string -> cterm -> thm -> thm
   125   val combination       : thm -> thm -> thm
   126   val equal_intr        : thm -> thm -> thm
   127   val equal_elim        : thm -> thm -> thm
   128   val implies_intr_hyps : thm -> thm
   129   val flexflex_rule     : thm -> thm Seq.seq
   130   val instantiate       :
   131     (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
   132   val trivial           : cterm -> thm
   133   val class_triv        : Sign.sg -> class -> thm
   134   val varifyT           : thm -> thm
   135   val varifyT'          : string list -> thm -> thm
   136   val freezeT           : thm -> thm
   137   val dest_state        : thm * int ->
   138     (term * term) list * term list * term * term
   139   val lift_rule         : (thm * int) -> thm -> thm
   140   val assumption        : int -> thm -> thm Seq.seq
   141   val eq_assumption     : int -> thm -> thm
   142   val rotate_rule       : int -> int -> thm -> thm
   143   val permute_prems     : int -> int -> thm -> thm
   144   val rename_params_rule: string list * int -> thm -> thm
   145   val bicompose         : bool -> bool * thm * int ->
   146     int -> thm -> thm Seq.seq
   147   val biresolution      : bool -> (bool * thm) list ->
   148     int -> thm -> thm Seq.seq
   149 
   150   (*meta simplification*)
   151   exception SIMPLIFIER of string * thm
   152   type meta_simpset
   153   val dest_mss		: meta_simpset ->
   154     {simps: thm list, congs: thm list, procs: (string * cterm list) list}
   155   val empty_mss         : meta_simpset
   156   val clear_mss		: meta_simpset -> meta_simpset
   157   val merge_mss		: meta_simpset * meta_simpset -> meta_simpset
   158   val add_simps         : meta_simpset * thm list -> meta_simpset
   159   val del_simps         : meta_simpset * thm list -> meta_simpset
   160   val mss_of            : thm list -> meta_simpset
   161   val add_congs         : meta_simpset * thm list -> meta_simpset
   162   val del_congs         : meta_simpset * thm list -> meta_simpset
   163   val add_simprocs	: meta_simpset *
   164     (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
   165       -> meta_simpset
   166   val del_simprocs	: meta_simpset *
   167     (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
   168       -> meta_simpset
   169   val add_prems         : meta_simpset * thm list -> meta_simpset
   170   val prems_of_mss      : meta_simpset -> thm list
   171   val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
   172   val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
   173   val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
   174   val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
   175   val trace_simp        : bool ref
   176   val rewrite_cterm     : bool * bool * bool -> meta_simpset ->
   177                           (meta_simpset -> thm -> thm option) -> cterm -> thm
   178 
   179   val invoke_oracle     : theory -> xstring -> Sign.sg * Object.T -> thm
   180 end;
   181 
   182 signature THM =
   183 sig
   184   include BASIC_THM
   185   val no_attributes	: 'a -> 'a * 'b attribute list
   186   val apply_attributes	: ('a * thm) * 'a attribute list -> ('a * thm)
   187   val applys_attributes	: ('a * thm list) * 'a attribute list -> ('a * thm list)
   188   val get_name_tags	: thm -> string * tag list
   189   val put_name_tags	: string * tag list -> thm -> thm
   190   val name_of_thm	: thm -> string
   191   val tags_of_thm	: thm -> tag list
   192   val name_thm		: string * thm -> thm
   193 end;
   194 
   195 structure Thm: THM =
   196 struct
   197 
   198 (*** Certified terms and types ***)
   199 
   200 (** certified types **)
   201 
   202 (*certified typs under a signature*)
   203 
   204 datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};
   205 
   206 fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
   207 fun typ_of (Ctyp {T, ...}) = T;
   208 
   209 fun ctyp_of sign T =
   210   Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T};
   211 
   212 fun read_ctyp sign s =
   213   Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s};
   214 
   215 
   216 
   217 (** certified terms **)
   218 
   219 (*certified terms under a signature, with checked typ and maxidx of Vars*)
   220 
   221 datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};
   222 
   223 fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   224   {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};
   225 
   226 fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   227   {sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T},
   228     maxidx = maxidx};
   229 
   230 fun term_of (Cterm {t, ...}) = t;
   231 
   232 fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};
   233 
   234 (*create a cterm by checking a "raw" term with respect to a signature*)
   235 fun cterm_of sign tm =
   236   let val (t, T, maxidx) = Sign.certify_term sign tm
   237   in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
   238   end;
   239 
   240 fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t);
   241 
   242 
   243 exception CTERM of string;
   244 
   245 (*Destruct application in cterms*)
   246 fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) =
   247       let val typeA = fastype_of A;
   248           val typeB =
   249             case typeA of Type("fun",[S,T]) => S
   250                         | _ => error "Function type expected in dest_comb";
   251       in
   252       (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA},
   253        Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB})
   254       end
   255   | dest_comb _ = raise CTERM "dest_comb";
   256 
   257 (*Destruct abstraction in cterms*)
   258 fun dest_abs (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
   259       let val (y,N) = variant_abs (x,ty,M)
   260       in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)},
   261           Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N})
   262       end
   263   | dest_abs _ = raise CTERM "dest_abs";
   264 
   265 (*Makes maxidx precise: it is often too big*)
   266 fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) =
   267   if maxidx = ~1 then ct 
   268   else  Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t};
   269 
   270 (*Form cterm out of a function and an argument*)
   271 fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
   272            (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
   273       if T = dty then Cterm{t=f$x, sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
   274                             maxidx=Int.max(maxidx1, maxidx2)}
   275       else raise CTERM "capply: types don't agree"
   276   | capply _ _ = raise CTERM "capply: first arg is not a function"
   277 
   278 fun cabs (Cterm {t=Free(a,ty), sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
   279          (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
   280       Cterm {t=absfree(a,ty,t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
   281              T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)}
   282   | cabs _ _ = raise CTERM "cabs: first arg is not a free variable";
   283 
   284 
   285 
   286 (** read cterms **)   (*exception ERROR*)
   287 
   288 (*read terms, infer types, certify terms*)
   289 fun read_def_cterms (sign, types, sorts) used freeze sTs =
   290   let
   291     val syn = #syn (Sign.rep_sg sign)
   292     fun read(s,T) =
   293       let val T' = Sign.certify_typ sign T
   294                    handle TYPE (msg, _, _) => error msg
   295       in (Syntax.read syn T' s, T') end
   296     val tsTs = map read sTs
   297     val (ts',tye) = Sign.infer_types_simult sign types sorts used freeze tsTs;
   298     val cts = map (cterm_of sign) ts'
   299       handle TYPE (msg, _, _) => error msg
   300            | TERM (msg, _) => error msg;
   301   in (cts, tye) end;
   302 
   303 (*read term, infer types, certify term*)
   304 fun read_def_cterm args used freeze aT =
   305   let val ([ct],tye) = read_def_cterms args used freeze [aT]
   306   in (ct,tye) end;
   307 
   308 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
   309 
   310 
   311 
   312 (*** Derivations ***)
   313 
   314 (*tags provide additional comment, apart from the axiom/theorem name*)
   315 type tag = string * string list;
   316 
   317 (*Names of rules in derivations.  Includes logically trivial rules, if 
   318   executed in ML.*)
   319 datatype rule = 
   320     MinProof                            (*for building minimal proof terms*)
   321   | Oracle              of string * Sign.sg * Object.T       (*oracles*)
   322 (*Axioms/theorems*)
   323   | Axiom               of string * tag list
   324   | Theorem             of string * tag list
   325 (*primitive inferences and compound versions of them*)
   326   | Assume              of cterm
   327   | Implies_intr        of cterm
   328   | Implies_intr_shyps
   329   | Implies_intr_hyps
   330   | Implies_elim 
   331   | Forall_intr         of cterm
   332   | Forall_elim         of cterm
   333   | Reflexive           of cterm
   334   | Symmetric 
   335   | Transitive
   336   | Beta_conversion     of cterm
   337   | Extensional
   338   | Abstract_rule       of string * cterm
   339   | Combination
   340   | Equal_intr
   341   | Equal_elim
   342 (*derived rules for tactical proof*)
   343   | Trivial             of cterm
   344         (*For lift_rule, the proof state is not a premise.
   345           Use cterm instead of thm to avoid mutual recursion.*)
   346   | Lift_rule           of cterm * int 
   347   | Assumption          of int * Envir.env option (*includes eq_assumption*)
   348   | Rotate_rule         of int * int
   349   | Permute_prems       of int * int
   350   | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
   351   | Bicompose           of bool * bool * int * int * Envir.env
   352   | Flexflex_rule       of Envir.env            (*identifies unifier chosen*)
   353 (*other derived rules*)
   354   | Class_triv          of class
   355   | VarifyT		of string list
   356   | FreezeT
   357 (*for the simplifier*)
   358   | RewriteC            of cterm
   359   | CongC               of cterm
   360   | Rewrite_cterm       of cterm
   361 (*Logical identities, recorded since they are part of the proof process*)
   362   | Rename_params_rule  of string list * int;
   363 
   364 
   365 type deriv = rule mtree;
   366 
   367 datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
   368 
   369 val keep_derivs = ref MinDeriv;
   370 
   371 
   372 (*Build a minimal derivation.  Keep oracles; suppress atomic inferences;
   373   retain Theorems or their underlying links; keep anything else*)
   374 fun squash_derivs [] = []
   375   | squash_derivs (der::ders) =
   376      (case der of
   377           Join (Oracle _, _) => der :: squash_derivs ders
   378         | Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 
   379                                       then der :: squash_derivs ders
   380                                       else squash_derivs (der'::ders)
   381         | Join (Axiom _, _) => if !keep_derivs=ThmDeriv 
   382                                then der :: squash_derivs ders
   383                                else squash_derivs ders
   384         | Join (_, [])      => squash_derivs ders
   385         | _                 => der :: squash_derivs ders);
   386 
   387 
   388 (*Ensure sharing of the most likely derivation, the empty one!*)
   389 val min_infer = Join (MinProof, []);
   390 
   391 (*Make a minimal inference*)
   392 fun make_min_infer []    = min_infer
   393   | make_min_infer [der] = der
   394   | make_min_infer ders  = Join (MinProof, ders);
   395 
   396 fun infer_derivs (rl, [])   = Join (rl, [])
   397   | infer_derivs (rl, ders) =
   398     if !keep_derivs=FullDeriv then Join (rl, ders)
   399     else make_min_infer (squash_derivs ders);
   400 
   401 
   402 
   403 (*** Meta theorems ***)
   404 
   405 datatype thm = Thm of
   406  {sign_ref: Sign.sg_ref,       (*mutable reference to signature*)
   407   der: deriv,                  (*derivation*)
   408   maxidx: int,                 (*maximum index of any Var or TVar*)
   409   shyps: sort list,            (*sort hypotheses*)
   410   hyps: term list,             (*hypotheses*)
   411   prop: term};                 (*conclusion*)
   412 
   413 fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   414   {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
   415     shyps = shyps, hyps = hyps, prop = prop};
   416 
   417 (*Version of rep_thm returning cterms instead of terms*)
   418 fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   419   let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max};
   420   in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps,
   421       hyps = map (ctermf ~1) hyps,
   422       prop = ctermf maxidx prop}
   423   end;
   424 
   425 (*errors involving theorems*)
   426 exception THM of string * int * thm list;
   427 
   428 (*attributes subsume any kind of rules or addXXXs modifiers*)
   429 type 'a attribute = 'a * thm -> 'a * thm;
   430 
   431 fun no_attributes x = (x, []);
   432 fun apply_attributes (x_th, atts) = Library.apply atts x_th;
   433 fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
   434 
   435 (*equality of theorems uses equality of signatures and the
   436   a-convertible test for terms*)
   437 fun eq_thm (th1, th2) =
   438   let
   439     val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, ...} = rep_thm th1;
   440     val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, ...} = rep_thm th2;
   441   in
   442     Sign.eq_sg (sg1, sg2) andalso
   443     eq_set_sort (shyps1, shyps2) andalso
   444     aconvs (hyps1, hyps2) andalso
   445     prop1 aconv prop2
   446   end;
   447 
   448 fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
   449 
   450 (*merge signatures of two theorems; raise exception if incompatible*)
   451 fun merge_thm_sgs
   452     (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
   453   Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
   454 
   455 (*transfer thm to super theory (non-destructive)*)
   456 fun transfer_sg sign' thm =
   457   let
   458     val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   459     val sign = Sign.deref sign_ref;
   460   in
   461     if Sign.eq_sg (sign, sign') then thm
   462     else if Sign.subsig (sign, sign') then
   463       Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
   464         shyps = shyps, hyps = hyps, prop = prop}
   465     else raise THM ("transfer: not a super theory", 0, [thm])
   466   end;
   467 
   468 val transfer = transfer_sg o Theory.sign_of;
   469 
   470 (*maps object-rule to tpairs*)
   471 fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);
   472 
   473 (*maps object-rule to premises*)
   474 fun prems_of (Thm {prop, ...}) =
   475   Logic.strip_imp_prems (Logic.skip_flexpairs prop);
   476 
   477 (*counts premises in a rule*)
   478 fun nprems_of (Thm {prop, ...}) =
   479   Logic.count_prems (Logic.skip_flexpairs prop, 0);
   480 
   481 (*maps object-rule to conclusion*)
   482 fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
   483 
   484 (*the statement of any thm is a cterm*)
   485 fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) =
   486   Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop};
   487 
   488 
   489 
   490 (** sort contexts of theorems **)
   491 
   492 (* basic utils *)
   493 
   494 (*accumulate sorts suppressing duplicates; these are coded low levelly
   495   to improve efficiency a bit*)
   496 
   497 fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss)
   498   | add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss)
   499   | add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss)
   500 and add_typs_sorts ([], Ss) = Ss
   501   | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss));
   502 
   503 fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss)
   504   | add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss)
   505   | add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss)
   506   | add_term_sorts (Bound _, Ss) = Ss
   507   | add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss))
   508   | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss));
   509 
   510 fun add_terms_sorts ([], Ss) = Ss
   511   | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));
   512 
   513 fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs;
   514 
   515 fun add_env_sorts (env, Ss) =
   516   add_terms_sorts (map snd (Envir.alist_of env),
   517     add_typs_sorts (env_codT env, Ss));
   518 
   519 fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) =
   520   add_terms_sorts (hyps, add_term_sorts (prop, Ss));
   521 
   522 fun add_thms_shyps ([], Ss) = Ss
   523   | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) =
   524       add_thms_shyps (ths, union_sort(shyps,Ss));
   525 
   526 
   527 (*get 'dangling' sort constraints of a thm*)
   528 fun extra_shyps (th as Thm {shyps, ...}) =
   529   shyps \\ add_thm_sorts (th, []);
   530 
   531 
   532 (* fix_shyps *)
   533 
   534 (*preserve sort contexts of rule premises and substituted types*)
   535 fun fix_shyps thms Ts thm =
   536   let
   537     val Thm {sign_ref, der, maxidx, hyps, prop, ...} = thm;
   538     val shyps =
   539       add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, [])));
   540   in
   541     Thm {sign_ref = sign_ref,
   542          der = der,             (*No new derivation, as other rules call this*)
   543          maxidx = maxidx,
   544          shyps = shyps, hyps = hyps, prop = prop}
   545   end;
   546 
   547 
   548 (* strip_shyps *)       (* FIXME improve? (e.g. only minimal extra sorts) *)
   549 
   550 val force_strip_shyps = ref true;  (* FIXME tmp (since 1995/08/01) *)
   551 
   552 (*remove extra sorts that are known to be syntactically non-empty*)
   553 fun strip_shyps thm =
   554   let
   555     val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   556     val sorts = add_thm_sorts (thm, []);
   557     val maybe_empty = not o Sign.nonempty_sort (Sign.deref sign_ref) sorts;
   558     val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps;
   559   in
   560     Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
   561          shyps =
   562          (if eq_set_sort (shyps',sorts) orelse 
   563              not (!force_strip_shyps) then shyps'
   564           else    (* FIXME tmp (since 1995/08/01) *)
   565               (warning ("Removed sort hypotheses: " ^
   566                         commas (map Sorts.str_of_sort (shyps' \\ sorts)));
   567                warning "Let's hope these sorts are non-empty!";
   568            sorts)),
   569       hyps = hyps, 
   570       prop = prop}
   571   end;
   572 
   573 
   574 (* implies_intr_shyps *)
   575 
   576 (*discharge all extra sort hypotheses*)
   577 fun implies_intr_shyps thm =
   578   (case extra_shyps thm of
   579     [] => thm
   580   | xshyps =>
   581       let
   582         val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   583         val shyps' = ins_sort (logicS, shyps \\ xshyps);
   584         val used_names = foldr add_term_tfree_names (prop :: hyps, []);
   585         val names =
   586           tl (variantlist (replicate (length xshyps + 1) "'", used_names));
   587         val tfrees = map (TFree o rpair logicS) names;
   588 
   589         fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S;
   590         val sort_hyps = List.concat (map2 mk_insort (tfrees, xshyps));
   591       in
   592         Thm {sign_ref = sign_ref, 
   593              der = infer_derivs (Implies_intr_shyps, [der]), 
   594              maxidx = maxidx, 
   595              shyps = shyps',
   596              hyps = hyps, 
   597              prop = Logic.list_implies (sort_hyps, prop)}
   598       end);
   599 
   600 
   601 (** Axioms **)
   602 
   603 (*look up the named axiom in the theory*)
   604 fun get_axiom theory raw_name =
   605   let
   606     val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name;
   607 
   608     fun get_ax [] = None
   609       | get_ax (thy :: thys) =
   610           let val {sign, axioms, ...} = Theory.rep_theory thy in
   611             (case Symtab.lookup (axioms, name) of
   612               Some t =>
   613                 Some (fix_shyps [] []
   614                   (Thm {sign_ref = Sign.self_ref sign,
   615                     der = infer_derivs (Axiom (name, []), []),
   616                     maxidx = maxidx_of_term t,
   617                     shyps = [], 
   618                     hyps = [], 
   619                     prop = t}))
   620             | None => get_ax thys)
   621           end;
   622   in
   623     (case get_ax (theory :: Theory.ancestors_of theory) of
   624       Some thm => thm
   625     | None => raise THEORY ("No axiom " ^ quote name, [theory]))
   626   end;
   627 
   628 fun def_name name = name ^ "_def";
   629 fun get_def thy = get_axiom thy o def_name;
   630 
   631 
   632 (*return additional axioms of this theory node*)
   633 fun axioms_of thy =
   634   map (fn (s, _) => (s, get_axiom thy s))
   635     (Symtab.dest (#axioms (Theory.rep_theory thy)));
   636 
   637 
   638 (* name and tags -- make proof objects more readable *)
   639 
   640 fun get_name_tags (Thm {der, ...}) =
   641   (case der of
   642     Join (Theorem x, _) => x
   643   | Join (Axiom x, _) => x
   644   | _ => ("", []));
   645 
   646 fun put_name_tags x (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   647   let
   648     val der' =
   649       (case der of
   650         Join (Theorem _, ds) => Join (Theorem x, ds)
   651       | Join (Axiom _, ds) => Join (Axiom x, ds)
   652       | _ => Join (Theorem x, [der]));
   653   in
   654     Thm {sign_ref = sign_ref, der = der', maxidx = maxidx,
   655       shyps = shyps, hyps = hyps, prop = prop}
   656   end;
   657 
   658 val name_of_thm = #1 o get_name_tags;
   659 val tags_of_thm = #2 o get_name_tags;
   660 
   661 fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm;
   662 
   663 
   664 (*Compression of theorems -- a separate rule, not integrated with the others,
   665   as it could be slow.*)
   666 fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
   667     Thm {sign_ref = sign_ref, 
   668          der = der,     (*No derivation recorded!*)
   669          maxidx = maxidx,
   670          shyps = shyps, 
   671          hyps = map Term.compress_term hyps, 
   672          prop = Term.compress_term prop};
   673 
   674 
   675 
   676 (*** Meta rules ***)
   677 
   678 (*Check that term does not contain same var with different typing/sorting.
   679   If this check must be made, recalculate maxidx in hope of preventing its
   680   recurrence.*)
   681 fun nodup_Vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s =
   682   (Sign.nodup_Vars prop; 
   683    Thm {sign_ref = sign_ref, 
   684          der = der,     
   685          maxidx = maxidx_of_term prop,
   686          shyps = shyps, 
   687          hyps = hyps, 
   688          prop = prop})
   689   handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);
   690 
   691 (** 'primitive' rules **)
   692 
   693 (*discharge all assumptions t from ts*)
   694 val disch = gen_rem (op aconv);
   695 
   696 (*The assumption rule A|-A in a theory*)
   697 fun assume raw_ct : thm =
   698   let val ct as Cterm {sign_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
   699   in  if T<>propT then
   700         raise THM("assume: assumptions must have type prop", 0, [])
   701       else if maxidx <> ~1 then
   702         raise THM("assume: assumptions may not contain scheme variables",
   703                   maxidx, [])
   704       else Thm{sign_ref   = sign_ref,
   705                der    = infer_derivs (Assume ct, []),
   706                maxidx = ~1, 
   707                shyps  = add_term_sorts(prop,[]), 
   708                hyps   = [prop], 
   709                prop   = prop}
   710   end;
   711 
   712 (*Implication introduction
   713     [A]
   714      :
   715      B
   716   -------
   717   A ==> B
   718 *)
   719 fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
   720   let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA
   721   in  if T<>propT then
   722         raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   723       else fix_shyps [thB] []
   724         (Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA),  
   725              der = infer_derivs (Implies_intr cA, [der]),
   726              maxidx = Int.max(maxidxA, maxidx),
   727              shyps = [],
   728              hyps = disch(hyps,A),
   729              prop = implies$A$prop})
   730       handle TERM _ =>
   731         raise THM("implies_intr: incompatible signatures", 0, [thB])
   732   end;
   733 
   734 
   735 (*Implication elimination
   736   A ==> B    A
   737   ------------
   738         B
   739 *)
   740 fun implies_elim thAB thA : thm =
   741     let val Thm{maxidx=maxA, der=derA, hyps=hypsA, prop=propA,...} = thA
   742         and Thm{sign_ref, der, maxidx, hyps, prop,...} = thAB;
   743         fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
   744     in  case prop of
   745             imp$A$B =>
   746                 if imp=implies andalso  A aconv propA
   747                 then fix_shyps [thAB, thA] []
   748                        (Thm{sign_ref= merge_thm_sgs(thAB,thA),
   749                             der = infer_derivs (Implies_elim, [der,derA]),
   750                             maxidx = Int.max(maxA,maxidx),
   751                             shyps = [],
   752                             hyps = union_term(hypsA,hyps),  (*dups suppressed*)
   753                             prop = B})
   754                 else err("major premise")
   755           | _ => err("major premise")
   756     end;
   757 
   758 (*Forall introduction.  The Free or Var x must not be free in the hypotheses.
   759     A
   760   -----
   761   !!x.A
   762 *)
   763 fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
   764   let val x = term_of cx;
   765       fun result(a,T) = fix_shyps [th] []
   766         (Thm{sign_ref = sign_ref, 
   767              der = infer_derivs (Forall_intr cx, [der]),
   768              maxidx = maxidx,
   769              shyps = [],
   770              hyps = hyps,
   771              prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
   772   in  case x of
   773         Free(a,T) =>
   774           if exists (apl(x, Logic.occs)) hyps
   775           then  raise THM("forall_intr: variable free in assumptions", 0, [th])
   776           else  result(a,T)
   777       | Var((a,_),T) => result(a,T)
   778       | _ => raise THM("forall_intr: not a variable", 0, [th])
   779   end;
   780 
   781 (*Forall elimination
   782   !!x.A
   783   ------
   784   A[t/x]
   785 *)
   786 fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
   787   let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct
   788   in  case prop of
   789         Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   790           if T<>qary then
   791               raise THM("forall_elim: type mismatch", 0, [th])
   792           else let val thm = fix_shyps [th] []
   793                     (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
   794                          der = infer_derivs (Forall_elim ct, [der]),
   795                          maxidx = Int.max(maxidx, maxt),
   796                          shyps = [],
   797                          hyps = hyps,  
   798                          prop = betapply(A,t)})
   799                in if maxt >= 0 andalso maxidx >= 0
   800                   then nodup_Vars thm "forall_elim" 
   801                   else thm (*no new Vars: no expensive check!*)
   802                end
   803       | _ => raise THM("forall_elim: not quantified", 0, [th])
   804   end
   805   handle TERM _ =>
   806          raise THM("forall_elim: incompatible signatures", 0, [th]);
   807 
   808 
   809 (* Equality *)
   810 
   811 (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   812 fun reflexive ct =
   813   let val Cterm {sign_ref, t, T, maxidx} = ct
   814   in  fix_shyps [] []
   815        (Thm{sign_ref= sign_ref, 
   816             der = infer_derivs (Reflexive ct, []),
   817             shyps = [],
   818             hyps = [], 
   819             maxidx = maxidx,
   820             prop = Logic.mk_equals(t,t)})
   821   end;
   822 
   823 (*The symmetry rule
   824   t==u
   825   ----
   826   u==t
   827 *)
   828 fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
   829   case prop of
   830       (eq as Const("==",_)) $ t $ u =>
   831         (*no fix_shyps*)
   832           Thm{sign_ref = sign_ref,
   833               der = infer_derivs (Symmetric, [der]),
   834               maxidx = maxidx,
   835               shyps = shyps,
   836               hyps = hyps,
   837               prop = eq$u$t}
   838     | _ => raise THM("symmetric", 0, [th]);
   839 
   840 (*The transitive rule
   841   t1==u    u==t2
   842   --------------
   843       t1==t2
   844 *)
   845 fun transitive th1 th2 =
   846   let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   847       and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   848       fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
   849   in case (prop1,prop2) of
   850        ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) =>
   851           if not (u aconv u') then err"middle term"
   852           else let val thm =      
   853               fix_shyps [th1, th2] []
   854                 (Thm{sign_ref= merge_thm_sgs(th1,th2), 
   855                      der = infer_derivs (Transitive, [der1, der2]),
   856                      maxidx = Int.max(max1,max2), 
   857                      shyps = [],
   858                      hyps = union_term(hyps1,hyps2),
   859                      prop = eq$t1$t2})
   860                  in if max1 >= 0 andalso max2 >= 0
   861                     then nodup_Vars thm "transitive" 
   862                     else thm (*no new Vars: no expensive check!*)
   863                  end
   864      | _ =>  err"premises"
   865   end;
   866 
   867 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *)
   868 fun beta_conversion ct =
   869   let val Cterm {sign_ref, t, T, maxidx} = ct
   870   in  case t of
   871           Abs(_,_,bodt) $ u => fix_shyps [] []
   872             (Thm{sign_ref = sign_ref,  
   873                  der = infer_derivs (Beta_conversion ct, []),
   874                  maxidx = maxidx,
   875                  shyps = [],
   876                  hyps = [],
   877                  prop = Logic.mk_equals(t, subst_bound (u,bodt))})
   878         | _ =>  raise THM("beta_conversion: not a redex", 0, [])
   879   end;
   880 
   881 (*The extensionality rule   (proviso: x not free in f, g, or hypotheses)
   882   f(x) == g(x)
   883   ------------
   884      f == g
   885 *)
   886 fun extensional (th as Thm{sign_ref, der, maxidx,shyps,hyps,prop}) =
   887   case prop of
   888     (Const("==",_)) $ (f$x) $ (g$y) =>
   889       let fun err(msg) = raise THM("extensional: "^msg, 0, [th])
   890       in (if x<>y then err"different variables" else
   891           case y of
   892                 Free _ =>
   893                   if exists (apl(y, Logic.occs)) (f::g::hyps)
   894                   then err"variable free in hyps or functions"    else  ()
   895               | Var _ =>
   896                   if Logic.occs(y,f)  orelse  Logic.occs(y,g)
   897                   then err"variable free in functions"   else  ()
   898               | _ => err"not a variable");
   899           (*no fix_shyps*)
   900           Thm{sign_ref = sign_ref,
   901               der = infer_derivs (Extensional, [der]),
   902               maxidx = maxidx,
   903               shyps = shyps,
   904               hyps = hyps, 
   905               prop = Logic.mk_equals(f,g)}
   906       end
   907  | _ =>  raise THM("extensional: premise", 0, [th]);
   908 
   909 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   910   The bound variable will be named "a" (since x will be something like x320)
   911      t == u
   912   ------------
   913   %x.t == %x.u
   914 *)
   915 fun abstract_rule a cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
   916   let val x = term_of cx;
   917       val (t,u) = Logic.dest_equals prop
   918             handle TERM _ =>
   919                 raise THM("abstract_rule: premise not an equality", 0, [th])
   920       fun result T = fix_shyps [th] []
   921           (Thm{sign_ref = sign_ref,
   922                der = infer_derivs (Abstract_rule (a,cx), [der]),
   923                maxidx = maxidx, 
   924                shyps = [], 
   925                hyps = hyps,
   926                prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   927                                       Abs(a, T, abstract_over (x,u)))})
   928   in  case x of
   929         Free(_,T) =>
   930          if exists (apl(x, Logic.occs)) hyps
   931          then raise THM("abstract_rule: variable free in assumptions", 0, [th])
   932          else result T
   933       | Var(_,T) => result T
   934       | _ => raise THM("abstract_rule: not a variable", 0, [th])
   935   end;
   936 
   937 (*The combination rule
   938   f == g  t == u
   939   --------------
   940    f(t) == g(u)
   941 *)
   942 fun combination th1 th2 =
   943   let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
   944               prop=prop1,...} = th1
   945       and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   946               prop=prop2,...} = th2
   947       fun chktypes (f,t) =
   948             (case fastype_of f of
   949                 Type("fun",[T1,T2]) => 
   950                     if T1 <> fastype_of t then
   951                          raise THM("combination: types", 0, [th1,th2])
   952                     else ()
   953                 | _ => raise THM("combination: not function type", 0, 
   954                                  [th1,th2]))
   955   in case (prop1,prop2)  of
   956        (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
   957           let val _   = chktypes (f,t)
   958               val thm = (*no fix_shyps*)
   959                         Thm{sign_ref = merge_thm_sgs(th1,th2), 
   960                             der = infer_derivs (Combination, [der1, der2]),
   961                             maxidx = Int.max(max1,max2), 
   962                             shyps = union_sort(shyps1,shyps2),
   963                             hyps = union_term(hyps1,hyps2),
   964                             prop = Logic.mk_equals(f$t, g$u)}
   965           in if max1 >= 0 andalso max2 >= 0
   966              then nodup_Vars thm "combination" 
   967              else thm (*no new Vars: no expensive check!*)  
   968           end
   969      | _ =>  raise THM("combination: premises", 0, [th1,th2])
   970   end;
   971 
   972 
   973 (* Equality introduction
   974   A ==> B  B ==> A
   975   ----------------
   976        A == B
   977 *)
   978 fun equal_intr th1 th2 =
   979   let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
   980               prop=prop1,...} = th1
   981       and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   982               prop=prop2,...} = th2;
   983       fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
   984   in case (prop1,prop2) of
   985        (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A')  =>
   986           if A aconv A' andalso B aconv B'
   987           then
   988             (*no fix_shyps*)
   989               Thm{sign_ref = merge_thm_sgs(th1,th2),
   990                   der = infer_derivs (Equal_intr, [der1, der2]),
   991                   maxidx = Int.max(max1,max2),
   992                   shyps = union_sort(shyps1,shyps2),
   993                   hyps = union_term(hyps1,hyps2),
   994                   prop = Logic.mk_equals(A,B)}
   995           else err"not equal"
   996      | _ =>  err"premises"
   997   end;
   998 
   999 
  1000 (*The equal propositions rule
  1001   A == B  A
  1002   ---------
  1003       B
  1004 *)
  1005 fun equal_elim th1 th2 =
  1006   let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
  1007       and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
  1008       fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2])
  1009   in  case prop1  of
  1010        Const("==",_) $ A $ B =>
  1011           if not (prop2 aconv A) then err"not equal"  else
  1012             fix_shyps [th1, th2] []
  1013               (Thm{sign_ref= merge_thm_sgs(th1,th2), 
  1014                    der = infer_derivs (Equal_elim, [der1, der2]),
  1015                    maxidx = Int.max(max1,max2),
  1016                    shyps = [],
  1017                    hyps = union_term(hyps1,hyps2),
  1018                    prop = B})
  1019      | _ =>  err"major premise"
  1020   end;
  1021 
  1022 
  1023 
  1024 (**** Derived rules ****)
  1025 
  1026 (*Discharge all hypotheses.  Need not verify cterms or call fix_shyps.
  1027   Repeated hypotheses are discharged only once;  fold cannot do this*)
  1028 fun implies_intr_hyps (Thm{sign_ref, der, maxidx, shyps, hyps=A::As, prop}) =
  1029       implies_intr_hyps (*no fix_shyps*)
  1030             (Thm{sign_ref = sign_ref, 
  1031                  der = infer_derivs (Implies_intr_hyps, [der]), 
  1032                  maxidx = maxidx, 
  1033                  shyps = shyps,
  1034                  hyps = disch(As,A),  
  1035                  prop = implies$A$prop})
  1036   | implies_intr_hyps th = th;
  1037 
  1038 (*Smash" unifies the list of term pairs leaving no flex-flex pairs.
  1039   Instantiates the theorem and deletes trivial tpairs.
  1040   Resulting sequence may contain multiple elements if the tpairs are
  1041     not all flex-flex. *)
  1042 fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) =
  1043   let fun newthm env =
  1044           if Envir.is_empty env then th
  1045           else
  1046           let val (tpairs,horn) =
  1047                         Logic.strip_flexpairs (Envir.norm_term env prop)
  1048                 (*Remove trivial tpairs, of the form t=t*)
  1049               val distpairs = filter (not o op aconv) tpairs
  1050               val newprop = Logic.list_flexpairs(distpairs, horn)
  1051           in  fix_shyps [th] (env_codT env)
  1052                 (Thm{sign_ref = sign_ref, 
  1053                      der = infer_derivs (Flexflex_rule env, [der]), 
  1054                      maxidx = maxidx_of_term newprop, 
  1055                      shyps = [], 
  1056                      hyps = hyps,
  1057                      prop = newprop})
  1058           end;
  1059       val (tpairs,_) = Logic.strip_flexpairs prop
  1060   in Seq.map newthm
  1061             (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
  1062   end;
  1063 
  1064 (*Instantiation of Vars
  1065            A
  1066   -------------------
  1067   A[t1/v1,....,tn/vn]
  1068 *)
  1069 
  1070 local
  1071 
  1072 (*Check that all the terms are Vars and are distinct*)
  1073 fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
  1074 
  1075 fun prt_typing sg_ref t T =
  1076   let val sg = Sign.deref sg_ref in
  1077     Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T]
  1078   end;
  1079 
  1080 (*For instantiate: process pair of cterms, merge theories*)
  1081 fun add_ctpair ((ct,cu), (sign_ref,tpairs)) =
  1082   let
  1083     val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct
  1084     and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu;
  1085     val sign_ref_merged = Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu));
  1086   in
  1087     if T=U then (sign_ref_merged, (t,u)::tpairs)
  1088     else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict",
  1089       Pretty.fbrk, prt_typing sign_ref_merged t T,
  1090       Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u])
  1091   end;
  1092 
  1093 fun add_ctyp ((v,ctyp), (sign_ref',vTs)) =
  1094   let val Ctyp {T,sign_ref} = ctyp
  1095   in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end;
  1096 
  1097 in
  1098 
  1099 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
  1100   Instantiates distinct Vars by terms of same type.
  1101   Normalizes the new theorem! *)
  1102 fun instantiate ([], []) th = th
  1103   | instantiate (vcTs,ctpairs)  (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
  1104   let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[]));
  1105       val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[]));
  1106       val newprop =
  1107             Envir.norm_term (Envir.empty 0)
  1108               (subst_atomic tpairs
  1109                (Type.inst_term_tvars(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop))
  1110       val newth =
  1111             fix_shyps [th] (map snd vTs)
  1112               (Thm{sign_ref = newsign_ref, 
  1113                    der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
  1114                    maxidx = maxidx_of_term newprop, 
  1115                    shyps = [],
  1116                    hyps = hyps,
  1117                    prop = newprop})
  1118   in  if not(instl_ok(map #1 tpairs))
  1119       then raise THM("instantiate: variables not distinct", 0, [th])
  1120       else if not(null(findrep(map #1 vTs)))
  1121       then raise THM("instantiate: type variables not distinct", 0, [th])
  1122       else nodup_Vars newth "instantiate"
  1123   end
  1124   handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th])
  1125        | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
  1126 
  1127 end;
  1128 
  1129 
  1130 (*The trivial implication A==>A, justified by assume and forall rules.
  1131   A can contain Vars, not so for assume!   *)
  1132 fun trivial ct : thm =
  1133   let val Cterm {sign_ref, t=A, T, maxidx} = ct
  1134   in  if T<>propT then
  1135             raise THM("trivial: the term must have type prop", 0, [])
  1136       else fix_shyps [] []
  1137         (Thm{sign_ref = sign_ref, 
  1138              der = infer_derivs (Trivial ct, []), 
  1139              maxidx = maxidx, 
  1140              shyps = [], 
  1141              hyps = [],
  1142              prop = implies$A$A})
  1143   end;
  1144 
  1145 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
  1146 fun class_triv sign c =
  1147   let val Cterm {sign_ref, t, maxidx, ...} =
  1148     cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
  1149       handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
  1150   in
  1151     fix_shyps [] []
  1152       (Thm {sign_ref = sign_ref, 
  1153             der = infer_derivs (Class_triv c, []), 
  1154             maxidx = maxidx, 
  1155             shyps = [], 
  1156             hyps = [], 
  1157             prop = t})
  1158   end;
  1159 
  1160 
  1161 (* Replace all TFrees not fixed or in the hyps by new TVars *)
  1162 fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
  1163   let val tfrees = foldr add_term_tfree_names (hyps,fixed)
  1164   in let val thm = (*no fix_shyps*)
  1165     Thm{sign_ref = sign_ref, 
  1166         der = infer_derivs (VarifyT fixed, [der]), 
  1167         maxidx = Int.max(0,maxidx), 
  1168         shyps = shyps, 
  1169         hyps = hyps,
  1170         prop = Type.varify(prop,tfrees)}
  1171      in nodup_Vars thm "varifyT" end
  1172 (* this nodup_Vars check can be removed if thms are guaranteed not to contain
  1173 duplicate TVars with differnt sorts *)
  1174   end;
  1175 
  1176 val varifyT = varifyT' [];
  1177 
  1178 (* Replace all TVars by new TFrees *)
  1179 fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
  1180   let val (prop',_) = Type.freeze_thaw prop
  1181   in (*no fix_shyps*)
  1182     Thm{sign_ref = sign_ref, 
  1183         der = infer_derivs (FreezeT, [der]),
  1184         maxidx = maxidx_of_term prop',
  1185         shyps = shyps,
  1186         hyps = hyps,
  1187         prop = prop'}
  1188   end;
  1189 
  1190 
  1191 (*** Inference rules for tactics ***)
  1192 
  1193 (*Destruct proof state into constraints, other goals, goal(i), rest *)
  1194 fun dest_state (state as Thm{prop,...}, i) =
  1195   let val (tpairs,horn) = Logic.strip_flexpairs prop
  1196   in  case  Logic.strip_prems(i, [], horn) of
  1197           (B::rBs, C) => (tpairs, rev rBs, B, C)
  1198         | _ => raise THM("dest_state", i, [state])
  1199   end
  1200   handle TERM _ => raise THM("dest_state", i, [state]);
  1201 
  1202 (*Increment variables and parameters of orule as required for
  1203   resolution with goal i of state. *)
  1204 fun lift_rule (state, i) orule =
  1205   let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state
  1206       val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)
  1207         handle TERM _ => raise THM("lift_rule", i, [orule,state])
  1208       val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi}
  1209       val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1)
  1210       val (Thm{sign_ref, der, maxidx,shyps,hyps,prop}) = orule
  1211       val (tpairs,As,B) = Logic.strip_horn prop
  1212   in  (*no fix_shyps*)
  1213       Thm{sign_ref = merge_thm_sgs(state,orule),
  1214           der = infer_derivs (Lift_rule(ct_Bi, i), [der]),
  1215           maxidx = maxidx+smax+1,
  1216           shyps=union_sort(sshyps,shyps), 
  1217           hyps=hyps, 
  1218           prop = Logic.rule_of (map (pairself lift_abs) tpairs,
  1219                                 map lift_all As,    
  1220                                 lift_all B)}
  1221   end;
  1222 
  1223 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
  1224 fun assumption i state =
  1225   let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
  1226       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1227       fun newth (env as Envir.Envir{maxidx, ...}, tpairs) =
  1228         fix_shyps [state] (env_codT env)
  1229           (Thm{sign_ref = sign_ref, 
  1230                der = infer_derivs (Assumption (i, Some env), [der]),
  1231                maxidx = maxidx,
  1232                shyps = [],
  1233                hyps = hyps,
  1234                prop = 
  1235                if Envir.is_empty env then (*avoid wasted normalizations*)
  1236                    Logic.rule_of (tpairs, Bs, C)
  1237                else (*normalize the new rule fully*)
  1238                    Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
  1239       fun addprfs [] = Seq.empty
  1240         | addprfs ((t,u)::apairs) = Seq.make (fn()=> Seq.pull
  1241              (Seq.mapp newth
  1242                 (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
  1243                 (addprfs apairs)))
  1244   in  addprfs (Logic.assum_pairs Bi)  end;
  1245 
  1246 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
  1247   Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
  1248 fun eq_assumption i state =
  1249   let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
  1250       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1251   in  if exists (op aconv) (Logic.assum_pairs Bi)
  1252       then fix_shyps [state] []
  1253              (Thm{sign_ref = sign_ref, 
  1254                   der = infer_derivs (Assumption (i,None), [der]),
  1255                   maxidx = maxidx,
  1256                   shyps = [],
  1257                   hyps = hyps,
  1258                   prop = Logic.rule_of(tpairs, Bs, C)})
  1259       else  raise THM("eq_assumption", 0, [state])
  1260   end;
  1261 
  1262 
  1263 (*For rotate_tac: fast rotation of assumptions of subgoal i*)
  1264 fun rotate_rule k i state =
  1265   let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = state;
  1266       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1267       val params = Logic.strip_params Bi
  1268       and asms   = Logic.strip_assums_hyp Bi
  1269       and concl  = Logic.strip_assums_concl Bi
  1270       val n      = length asms
  1271       fun rot m  = if 0=m orelse m=n then Bi
  1272 		   else if 0<m andalso m<n 
  1273 		   then list_all 
  1274 			   (params, 
  1275 			    Logic.list_implies(List.drop(asms, m) @ 
  1276 					       List.take(asms, m),
  1277 					       concl))
  1278 		   else raise THM("rotate_rule", k, [state])
  1279   in  Thm{sign_ref = sign_ref, 
  1280 	  der = infer_derivs (Rotate_rule (k,i), [der]),
  1281 	  maxidx = maxidx,
  1282 	  shyps = shyps,
  1283 	  hyps = hyps,
  1284 	  prop = Logic.rule_of(tpairs, Bs@[rot (if k<0 then n+k else k)], C)}
  1285   end;
  1286 
  1287 
  1288 (*Rotates a rule's premises to the left by k, leaving the first j premises
  1289   unchanged.  Does nothing if k=0 or if k equals n-j, where n is the
  1290   number of premises.  Useful with etac and underlies tactic/defer_tac*)
  1291 fun permute_prems j k rl =
  1292   let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = rl
  1293       val prems  = Logic.strip_imp_prems prop
  1294       and concl  = Logic.strip_imp_concl prop
  1295       val moved_prems = List.drop(prems, j)
  1296       and fixed_prems = List.take(prems, j)
  1297         handle Subscript => raise THM("permute_prems:j", j, [rl])
  1298       val n_j    = length moved_prems
  1299       fun rot m  = if 0 = m orelse m = n_j then prop
  1300 		   else if 0<m andalso m<n_j 
  1301 		   then Logic.list_implies(fixed_prems @
  1302 					   List.drop(moved_prems, m) @ 
  1303 					   List.take(moved_prems, m),
  1304 					   concl)
  1305 		   else raise THM("permute_prems:k", k, [rl])
  1306   in  Thm{sign_ref = sign_ref, 
  1307 	  der = infer_derivs (Permute_prems (j,k), [der]),
  1308 	  maxidx = maxidx,
  1309 	  shyps = shyps,
  1310 	  hyps = hyps,
  1311 	  prop = rot (if k<0 then n_j + k else k)}
  1312   end;
  1313 
  1314 
  1315 (** User renaming of parameters in a subgoal **)
  1316 
  1317 (*Calls error rather than raising an exception because it is intended
  1318   for top-level use -- exception handling would not make sense here.
  1319   The names in cs, if distinct, are used for the innermost parameters;
  1320    preceding parameters may be renamed to make all params distinct.*)
  1321 fun rename_params_rule (cs, i) state =
  1322   let val Thm{sign_ref,der,maxidx,hyps,...} = state
  1323       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1324       val iparams = map #1 (Logic.strip_params Bi)
  1325       val short = length iparams - length cs
  1326       val newnames =
  1327             if short<0 then error"More names than abstractions!"
  1328             else variantlist(take (short,iparams), cs) @ cs
  1329       val freenames = map (#1 o dest_Free) (term_frees Bi)
  1330       val newBi = Logic.list_rename_params (newnames, Bi)
  1331   in
  1332   case findrep cs of
  1333      c::_ => (warning ("Can't rename.  Bound variables not distinct: " ^ c); 
  1334 	      state)
  1335    | [] => (case cs inter_string freenames of
  1336        a::_ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); 
  1337 		state)
  1338      | [] => fix_shyps [state] []
  1339                 (Thm{sign_ref = sign_ref,
  1340                      der = infer_derivs (Rename_params_rule(cs,i), [der]),
  1341                      maxidx = maxidx,
  1342                      shyps = [],
  1343                      hyps = hyps,
  1344                      prop = Logic.rule_of(tpairs, Bs@[newBi], C)}))
  1345   end;
  1346 
  1347 (*** Preservation of bound variable names ***)
  1348 
  1349 (*Scan a pair of terms; while they are similar,
  1350   accumulate corresponding bound vars in "al"*)
  1351 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
  1352       match_bvs(s, t, if x="" orelse y="" then al
  1353                                           else (x,y)::al)
  1354   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
  1355   | match_bvs(_,_,al) = al;
  1356 
  1357 (* strip abstractions created by parameters *)
  1358 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
  1359 
  1360 
  1361 (* strip_apply f A(,B) strips off all assumptions/parameters from A
  1362    introduced by lifting over B, and applies f to remaining part of A*)
  1363 fun strip_apply f =
  1364   let fun strip(Const("==>",_)$ A1 $ B1,
  1365                 Const("==>",_)$ _  $ B2) = implies $ A1 $ strip(B1,B2)
  1366         | strip((c as Const("all",_)) $ Abs(a,T,t1),
  1367                       Const("all",_)  $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))
  1368         | strip(A,_) = f A
  1369   in strip end;
  1370 
  1371 (*Use the alist to rename all bound variables and some unknowns in a term
  1372   dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
  1373   Preserves unknowns in tpairs and on lhs of dpairs. *)
  1374 fun rename_bvs([],_,_,_) = I
  1375   | rename_bvs(al,dpairs,tpairs,B) =
  1376     let val vars = foldr add_term_vars
  1377                         (map fst dpairs @ map fst tpairs @ map snd tpairs, [])
  1378         (*unknowns appearing elsewhere be preserved!*)
  1379         val vids = map (#1 o #1 o dest_Var) vars;
  1380         fun rename(t as Var((x,i),T)) =
  1381                 (case assoc(al,x) of
  1382                    Some(y) => if x mem_string vids orelse y mem_string vids then t
  1383                               else Var((y,i),T)
  1384                  | None=> t)
  1385           | rename(Abs(x,T,t)) =
  1386               Abs(case assoc_string(al,x) of Some(y) => y | None => x,
  1387                   T, rename t)
  1388           | rename(f$t) = rename f $ rename t
  1389           | rename(t) = t;
  1390         fun strip_ren Ai = strip_apply rename (Ai,B)
  1391     in strip_ren end;
  1392 
  1393 (*Function to rename bounds/unknowns in the argument, lifted over B*)
  1394 fun rename_bvars(dpairs, tpairs, B) =
  1395         rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B);
  1396 
  1397 
  1398 (*** RESOLUTION ***)
  1399 
  1400 (** Lifting optimizations **)
  1401 
  1402 (*strip off pairs of assumptions/parameters in parallel -- they are
  1403   identical because of lifting*)
  1404 fun strip_assums2 (Const("==>", _) $ _ $ B1,
  1405                    Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
  1406   | strip_assums2 (Const("all",_)$Abs(a,T,t1),
  1407                    Const("all",_)$Abs(_,_,t2)) =
  1408       let val (B1,B2) = strip_assums2 (t1,t2)
  1409       in  (Abs(a,T,B1), Abs(a,T,B2))  end
  1410   | strip_assums2 BB = BB;
  1411 
  1412 
  1413 (*Faster normalization: skip assumptions that were lifted over*)
  1414 fun norm_term_skip env 0 t = Envir.norm_term env t
  1415   | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
  1416         let val Envir.Envir{iTs, ...} = env
  1417             val T' = typ_subst_TVars iTs T
  1418             (*Must instantiate types of parameters because they are flattened;
  1419               this could be a NEW parameter*)
  1420         in  all T' $ Abs(a, T', norm_term_skip env n t)  end
  1421   | norm_term_skip env n (Const("==>", _) $ A $ B) =
  1422         implies $ A $ norm_term_skip env (n-1) B
  1423   | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
  1424 
  1425 
  1426 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
  1427   Unifies B with Bi, replacing subgoal i    (1 <= i <= n)
  1428   If match then forbid instantiations in proof state
  1429   If lifted then shorten the dpair using strip_assums2.
  1430   If eres_flg then simultaneously proves A1 by assumption.
  1431   nsubgoal is the number of new subgoals (written m above).
  1432   Curried so that resolution calls dest_state only once.
  1433 *)
  1434 local exception COMPOSE
  1435 in
  1436 fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
  1437                         (eres_flg, orule, nsubgoal) =
  1438  let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state
  1439      and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 
  1440              prop=rprop,...} = orule
  1441          (*How many hyps to skip over during normalization*)
  1442      and nlift = Logic.count_prems(strip_all_body Bi,
  1443                                    if eres_flg then ~1 else 0)
  1444      val sign_ref = merge_thm_sgs(state,orule);
  1445      val sign = Sign.deref sign_ref;
  1446      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
  1447      fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
  1448        let val normt = Envir.norm_term env;
  1449            (*perform minimal copying here by examining env*)
  1450            val normp =
  1451              if Envir.is_empty env then (tpairs, Bs @ As, C)
  1452              else
  1453              let val ntps = map (pairself normt) tpairs
  1454              in if Envir.above (smax, env) then
  1455                   (*no assignments in state; normalize the rule only*)
  1456                   if lifted
  1457                   then (ntps, Bs @ map (norm_term_skip env nlift) As, C)
  1458                   else (ntps, Bs @ map normt As, C)
  1459                 else if match then raise COMPOSE
  1460                 else (*normalize the new rule fully*)
  1461                   (ntps, map normt (Bs @ As), normt C)
  1462              end
  1463            val th = (*tuned fix_shyps*)
  1464              Thm{sign_ref = sign_ref,
  1465                  der = infer_derivs (Bicompose(match, eres_flg,
  1466                                                1 + length Bs, nsubgoal, env),
  1467                                      [rder,sder]),
  1468                  maxidx = maxidx,
  1469                  shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
  1470                  hyps = union_term(rhyps,shyps),
  1471                  prop = Logic.rule_of normp}
  1472         in  Seq.cons(th, thq)  end  handle COMPOSE => thq
  1473      val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
  1474      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
  1475        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
  1476      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
  1477      fun newAs(As0, n, dpairs, tpairs) =
  1478        let val As1 = if !Logic.auto_rename orelse not lifted then As0
  1479                      else map (rename_bvars(dpairs,tpairs,B)) As0
  1480        in (map (Logic.flatten_params n) As1)
  1481           handle TERM _ =>
  1482           raise THM("bicompose: 1st premise", 0, [orule])
  1483        end;
  1484      val env = Envir.empty(Int.max(rmax,smax));
  1485      val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
  1486      val dpairs = BBi :: (rtpairs@stpairs);
  1487      (*elim-resolution: try each assumption in turn.  Initially n=1*)
  1488      fun tryasms (_, _, []) = Seq.empty
  1489        | tryasms (As, n, (t,u)::apairs) =
  1490           (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
  1491                None                   => tryasms (As, n+1, apairs)
  1492              | cell as Some((_,tpairs),_) =>
  1493                    Seq.it_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
  1494                        (Seq.make (fn()=> cell),
  1495                         Seq.make (fn()=> Seq.pull (tryasms (As, n+1, apairs)))));
  1496      fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
  1497        | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);
  1498      (*ordinary resolution*)
  1499      fun res(None) = Seq.empty
  1500        | res(cell as Some((_,tpairs),_)) =
  1501              Seq.it_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
  1502                        (Seq.make (fn()=> cell), Seq.empty)
  1503  in  if eres_flg then eres(rev rAs)
  1504      else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
  1505  end;
  1506 end;  (*open Sequence*)
  1507 
  1508 
  1509 fun bicompose match arg i state =
  1510     bicompose_aux match (state, dest_state(state,i), false) arg;
  1511 
  1512 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
  1513   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
  1514 fun could_bires (Hs, B, eres_flg, rule) =
  1515     let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs
  1516           | could_reshyp [] = false;  (*no premise -- illegal*)
  1517     in  could_unify(concl_of rule, B) andalso
  1518         (not eres_flg  orelse  could_reshyp (prems_of rule))
  1519     end;
  1520 
  1521 (*Bi-resolution of a state with a list of (flag,rule) pairs.
  1522   Puts the rule above:  rule/state.  Renames vars in the rules. *)
  1523 fun biresolution match brules i state =
  1524     let val lift = lift_rule(state, i);
  1525         val (stpairs, Bs, Bi, C) = dest_state(state,i)
  1526         val B = Logic.strip_assums_concl Bi;
  1527         val Hs = Logic.strip_assums_hyp Bi;
  1528         val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
  1529         fun res [] = Seq.empty
  1530           | res ((eres_flg, rule)::brules) =
  1531               if could_bires (Hs, B, eres_flg, rule)
  1532               then Seq.make (*delay processing remainder till needed*)
  1533                   (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
  1534                                res brules))
  1535               else res brules
  1536     in  Seq.flat (res brules)  end;
  1537 
  1538 
  1539 
  1540 (*** Meta Simplification ***)
  1541 
  1542 (** diagnostics **)
  1543 
  1544 exception SIMPLIFIER of string * thm;
  1545 
  1546 fun prnt warn a = if warn then warning a else writeln a;
  1547 
  1548 fun prtm warn a sign t =
  1549   (prnt warn a; prnt warn (Sign.string_of_term sign t));
  1550 
  1551 fun prthm warn a (thm as Thm{sign_ref, prop, ...}) =
  1552   (prtm warn a (Sign.deref sign_ref) prop);
  1553 
  1554 val trace_simp = ref false;
  1555 
  1556 fun trace warn a = if !trace_simp then prnt warn a else ();
  1557 
  1558 fun trace_term warn a sign t =
  1559   if !trace_simp then prtm warn a sign t else ();
  1560 
  1561 fun trace_thm warn a (thm as Thm{sign_ref, prop, ...}) =
  1562   (trace_term warn a (Sign.deref sign_ref) prop);
  1563 
  1564 
  1565 
  1566 (** meta simp sets **)
  1567 
  1568 (* basic components *)
  1569 
  1570 type rrule = {thm: thm, lhs: term, elhs: term, fo: bool, perm: bool};
  1571 type cong = {thm: thm, lhs: term};
  1572 type simproc =
  1573  {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
  1574 
  1575 fun eq_rrule ({thm = Thm {prop = p1, ...}, ...}: rrule,
  1576   {thm = Thm {prop = p2, ...}, ...}: rrule) = p1 aconv p2;
  1577 
  1578 fun eq_cong ({thm = Thm {prop = p1, ...}, ...}: cong,
  1579   {thm = Thm {prop = p2, ...}, ...}: cong) = p1 aconv p2;
  1580 
  1581 fun eq_prem (Thm {prop = p1, ...}, Thm {prop = p2, ...}) = p1 aconv p2;
  1582 
  1583 fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
  1584 
  1585 fun mk_simproc (name, proc, lhs, id) =
  1586   {name = name, proc = proc, lhs = lhs, id = id};
  1587 
  1588 
  1589 (* datatype mss *)
  1590 
  1591 (*
  1592   A "mss" contains data needed during conversion:
  1593     rules: discrimination net of rewrite rules;
  1594     congs: association list of congruence rules and
  1595            a list of `weak' congruence constants.
  1596            A congruence is `weak' if it avoids normalization of some argument.
  1597     procs: discrimination net of simplification procedures
  1598       (functions that prove rewrite rules on the fly);
  1599     bounds: names of bound variables already used
  1600       (for generating new names when rewriting under lambda abstractions);
  1601     prems: current premises;
  1602     mk_rews: mk: turns simplification thms into rewrite rules;
  1603              mk_sym: turns == around; (needs Drule!)
  1604              mk_eq_True: turns P into P == True - logic specific;
  1605     termless: relation for ordered rewriting;
  1606 *)
  1607 
  1608 datatype meta_simpset =
  1609   Mss of {
  1610     rules: rrule Net.net,
  1611     congs: (string * cong) list * string list,
  1612     procs: simproc Net.net,
  1613     bounds: string list,
  1614     prems: thm list,
  1615     mk_rews: {mk: thm -> thm list,
  1616               mk_sym: thm -> thm option,
  1617               mk_eq_True: thm -> thm option},
  1618     termless: term * term -> bool};
  1619 
  1620 fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless) =
  1621   Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
  1622        prems=prems, mk_rews=mk_rews, termless=termless};
  1623 
  1624 fun upd_rules(Mss{rules,congs,procs,bounds,prems,mk_rews,termless}, rules') =
  1625   mk_mss(rules',congs,procs,bounds,prems,mk_rews,termless);
  1626 
  1627 val empty_mss =
  1628   let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None}
  1629   in mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, Term.termless) end;
  1630 
  1631 fun clear_mss (Mss {mk_rews, termless, ...}) =
  1632   mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless);
  1633 
  1634 
  1635 
  1636 (** simpset operations **)
  1637 
  1638 (* term variables *)
  1639 
  1640 val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
  1641 fun term_varnames t = add_term_varnames ([], t);
  1642 
  1643 
  1644 (* dest_mss *)
  1645 
  1646 fun dest_mss (Mss {rules, congs, procs, ...}) =
  1647   {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules),
  1648    congs = map (fn (_, {thm, ...}) => thm) (fst congs),
  1649    procs =
  1650      map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
  1651      |> partition_eq eq_snd
  1652      |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))};
  1653 
  1654 
  1655 (* merge_mss *)		(*NOTE: ignores mk_rews and termless of 2nd mss*)
  1656 
  1657 fun merge_mss
  1658  (Mss {rules = rules1, congs = (congs1,weak1), procs = procs1,
  1659        bounds = bounds1, prems = prems1, mk_rews, termless},
  1660   Mss {rules = rules2, congs = (congs2,weak2), procs = procs2,
  1661        bounds = bounds2, prems = prems2, ...}) =
  1662       mk_mss
  1663        (Net.merge (rules1, rules2, eq_rrule),
  1664         (generic_merge (eq_cong o pairself snd) I I congs1 congs2,
  1665         merge_lists weak1 weak2),
  1666         Net.merge (procs1, procs2, eq_simproc),
  1667         merge_lists bounds1 bounds2,
  1668         generic_merge eq_prem I I prems1 prems2,
  1669         mk_rews, termless);
  1670 
  1671 
  1672 (* add_simps *)
  1673 
  1674 fun mk_rrule2{thm,lhs,perm} =
  1675   let val elhs = Pattern.eta_contract lhs
  1676       val fo = Pattern.first_order elhs orelse not(Pattern.pattern elhs)
  1677   in {thm=thm,lhs=lhs,elhs=elhs,fo=fo,perm=perm} end
  1678 
  1679 fun insert_rrule(mss as Mss {rules,...},
  1680                  rrule as {thm,lhs,perm}) =
  1681   (trace_thm false "Adding rewrite rule:" thm;
  1682    let val rrule2 as {elhs,...} = mk_rrule2 rrule
  1683        val rules' = Net.insert_term ((elhs, rrule2), rules, eq_rrule)
  1684    in upd_rules(mss,rules') end
  1685    handle Net.INSERT =>
  1686      (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
  1687 
  1688 fun vperm (Var _, Var _) = true
  1689   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
  1690   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
  1691   | vperm (t, u) = (t = u);
  1692 
  1693 fun var_perm (t, u) =
  1694   vperm (t, u) andalso eq_set (term_varnames t, term_varnames u);
  1695 
  1696 (* FIXME: it seems that the conditions on extra variables are too liberal if
  1697 prems are nonempty: does solving the prems really guarantee instantiation of
  1698 all its Vars? Better: a dynamic check each time a rule is applied.
  1699 *)
  1700 fun rewrite_rule_extra_vars prems elhs erhs =
  1701   not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems))
  1702   orelse
  1703   not ((term_tvars erhs) subset
  1704        (term_tvars elhs  union  List.concat(map term_tvars prems)));
  1705 
  1706 (*Simple test for looping rewrite rules and stupid orientations*)
  1707 fun reorient sign prems lhs rhs =
  1708    rewrite_rule_extra_vars prems lhs rhs
  1709   orelse
  1710    is_Var (head_of lhs)
  1711   orelse
  1712    (exists (apl (lhs, Logic.occs)) (rhs :: prems))
  1713   orelse
  1714    (null prems andalso
  1715     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
  1716     (*the condition "null prems" is necessary because conditional rewrites
  1717       with extra variables in the conditions may terminate although
  1718       the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
  1719   orelse
  1720    (is_Const lhs andalso not(is_Const rhs))
  1721 
  1722 fun decomp_simp(thm as Thm {sign_ref, prop, ...}) =
  1723   let val sign = Sign.deref sign_ref;
  1724       val prems = Logic.strip_imp_prems prop;
  1725       val concl = Logic.strip_imp_concl prop;
  1726       val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
  1727         raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm)
  1728       val elhs = Pattern.eta_contract lhs;
  1729       val erhs = Pattern.eta_contract rhs;
  1730       val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
  1731                  andalso not (is_Var elhs)
  1732   in (sign,prems,lhs,rhs,perm) end;
  1733 
  1734 fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
  1735   case mk_eq_True thm of
  1736     None => []
  1737   | Some eq_True => let val (_,_,lhs,_,_) = decomp_simp eq_True
  1738                     in [{thm=eq_True, lhs=lhs, perm=false}] end;
  1739 
  1740 (* create the rewrite rule and possibly also the ==True variant,
  1741    in case there are extra vars on the rhs *)
  1742 fun rrule_eq_True(thm,lhs,rhs,mss,thm2) =
  1743   let val rrule = {thm=thm, lhs=lhs, perm=false}
  1744   in if (term_varnames rhs)  subset (term_varnames lhs) andalso
  1745         (term_tvars rhs) subset (term_tvars lhs)
  1746      then [rrule]
  1747      else mk_eq_True mss thm2 @ [rrule]
  1748   end;
  1749 
  1750 fun mk_rrule mss thm =
  1751   let val (_,prems,lhs,rhs,perm) = decomp_simp thm
  1752   in if perm then [{thm=thm, lhs=lhs, perm=true}] else
  1753      (* weak test for loops: *)
  1754      if rewrite_rule_extra_vars prems lhs rhs orelse
  1755         is_Var (head_of lhs) (* mk_cases may do this! *)
  1756      then mk_eq_True mss thm
  1757      else rrule_eq_True(thm,lhs,rhs,mss,thm)
  1758   end;
  1759 
  1760 fun orient_rrule mss thm =
  1761   let val (sign,prems,lhs,rhs,perm) = decomp_simp thm
  1762   in if perm then [{thm=thm,lhs=lhs,perm=true}]
  1763      else if reorient sign prems lhs rhs
  1764           then if reorient sign prems rhs lhs
  1765                then mk_eq_True mss thm
  1766                else let val Mss{mk_rews={mk_sym,...},...} = mss
  1767                     in case mk_sym thm of
  1768                          None => []
  1769                        | Some thm' =>
  1770                            let val (_,_,lhs',rhs',_) = decomp_simp thm'
  1771                            in rrule_eq_True(thm',lhs',rhs',mss,thm) end
  1772                     end
  1773           else rrule_eq_True(thm,lhs,rhs,mss,thm)
  1774   end;
  1775 
  1776 fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
  1777 
  1778 fun orient_comb_simps comb mk_rrule (mss,thms) =
  1779   let val rews = extract_rews(mss,thms)
  1780       val rrules = flat (map mk_rrule rews)
  1781   in foldl comb (mss,rrules) end
  1782 
  1783 (* Add rewrite rules explicitly; do not reorient! *)
  1784 fun add_simps(mss,thms) =
  1785   orient_comb_simps insert_rrule (mk_rrule mss) (mss,thms);
  1786 
  1787 fun mss_of thms =
  1788   foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms));
  1789 
  1790 fun extract_safe_rrules(mss,thm) =
  1791   flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
  1792 
  1793 fun add_safe_simp(mss,thm) =
  1794   foldl insert_rrule (mss, extract_safe_rrules(mss,thm))
  1795 
  1796 (* del_simps *)
  1797 
  1798 fun del_rrule(mss as Mss {rules,...},
  1799               rrule as {thm, elhs, ...}) =
  1800   (upd_rules(mss, Net.delete_term ((elhs, rrule), rules, eq_rrule))
  1801    handle Net.DELETE =>
  1802      (prthm true "Rewrite rule not in simpset:" thm; mss));
  1803 
  1804 fun del_simps(mss,thms) =
  1805   orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule mss) (mss,thms);
  1806 
  1807 
  1808 (* add_congs *)
  1809 
  1810 (*FIXME -> term.ML *)
  1811 fun is_Bound (Bound _) = true
  1812 fun is_Bound _         = false;
  1813 
  1814 fun is_full_cong_prems [] varpairs = null varpairs
  1815   | is_full_cong_prems (p::prems) varpairs =
  1816     (case Logic.strip_assums_concl p of
  1817        Const("==",_) $ lhs $ rhs =>
  1818          let val (x,xs) = strip_comb lhs and (y,ys) = strip_comb rhs
  1819          in is_Var x  andalso  forall is_Bound xs  andalso
  1820             null(findrep(xs))  andalso xs=ys andalso
  1821             (x,y) mem varpairs andalso
  1822             is_full_cong_prems (p::prems) (varpairs\(x,y))
  1823          end
  1824      | _ => false);
  1825 
  1826 fun is_full_cong (Thm{prop,...}) =
  1827 let val prems = Logic.strip_imp_prems prop
  1828     and concl = Logic.strip_imp_concl prop
  1829     val (lhs,rhs) = Logic.dest_equals concl
  1830     val (f,xs) = strip_comb lhs
  1831     and (g,ys) = strip_comb rhs
  1832 in
  1833   f=g andalso null(findrep(xs@ys)) andalso length xs = length ys andalso
  1834   is_full_cong_prems prems (xs ~~ ys)
  1835 end
  1836 
  1837 fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
  1838   let
  1839     val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
  1840       raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  1841 (*   val lhs = Pattern.eta_contract lhs; *)
  1842     val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
  1843       raise SIMPLIFIER ("Congruence must start with a constant", thm);
  1844     val (alist,weak) = congs
  1845     val weak2 = if is_full_cong thm then weak else a::weak
  1846   in
  1847     mk_mss (rules, ((a, {lhs = lhs, thm = thm}) :: alist, weak2),
  1848             procs, bounds, prems, mk_rews, termless)
  1849   end;
  1850 
  1851 val (op add_congs) = foldl add_cong;
  1852 
  1853 
  1854 (* del_congs *)
  1855 
  1856 fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
  1857   let
  1858     val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
  1859       raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  1860 (*   val lhs = Pattern.eta_contract lhs; *)
  1861     val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
  1862       raise SIMPLIFIER ("Congruence must start with a constant", thm);
  1863     val (alist,_) = congs
  1864     val alist2 = filter (fn (x,_)=> x<>a) alist
  1865     val weak2 = mapfilter (fn(a,{thm,...}) => if is_full_cong thm then None
  1866                                               else Some a)
  1867                    alist2
  1868   in
  1869     mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
  1870   end;
  1871 
  1872 val (op del_congs) = foldl del_cong;
  1873 
  1874 
  1875 (* add_simprocs *)
  1876 
  1877 fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
  1878     (name, lhs as Cterm {sign_ref, t, ...}, proc, id)) =
  1879   (trace_term false ("Adding simplification procedure " ^ quote name ^ " for")
  1880       (Sign.deref sign_ref) t;
  1881     mk_mss (rules, congs,
  1882       Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
  1883         handle Net.INSERT => 
  1884 	    (warning ("Ignoring duplicate simplification procedure \"" 
  1885 	              ^ name ^ "\""); 
  1886 	     procs),
  1887         bounds, prems, mk_rews, termless));
  1888 
  1889 fun add_simproc (mss, (name, lhss, proc, id)) =
  1890   foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
  1891 
  1892 val add_simprocs = foldl add_simproc;
  1893 
  1894 
  1895 (* del_simprocs *)
  1896 
  1897 fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
  1898     (name, lhs as Cterm {t, ...}, proc, id)) =
  1899   mk_mss (rules, congs,
  1900     Net.delete_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
  1901       handle Net.DELETE => 
  1902 	  (warning ("Simplification procedure \"" ^ name ^
  1903 		       "\" not in simpset"); procs),
  1904       bounds, prems, mk_rews, termless);
  1905 
  1906 fun del_simproc (mss, (name, lhss, proc, id)) =
  1907   foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
  1908 
  1909 val del_simprocs = foldl del_simproc;
  1910 
  1911 
  1912 (* prems *)
  1913 
  1914 fun add_prems (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thms) =
  1915   mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless);
  1916 
  1917 fun prems_of_mss (Mss {prems, ...}) = prems;
  1918 
  1919 
  1920 (* mk_rews *)
  1921 
  1922 fun set_mk_rews
  1923   (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk) =
  1924     mk_mss (rules, congs, procs, bounds, prems,
  1925             {mk=mk, mk_sym= #mk_sym mk_rews, mk_eq_True= #mk_eq_True mk_rews},
  1926             termless);
  1927 
  1928 fun set_mk_sym
  1929   (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_sym) =
  1930     mk_mss (rules, congs, procs, bounds, prems,
  1931             {mk= #mk mk_rews, mk_sym= mk_sym, mk_eq_True= #mk_eq_True mk_rews},
  1932             termless);
  1933 
  1934 fun set_mk_eq_True
  1935   (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_eq_True) =
  1936     mk_mss (rules, congs, procs, bounds, prems,
  1937             {mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
  1938             termless);
  1939 
  1940 (* termless *)
  1941 
  1942 fun set_termless
  1943   (Mss {rules, congs, procs, bounds, prems, mk_rews, termless = _}, termless) =
  1944     mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless);
  1945 
  1946 
  1947 
  1948 (** rewriting **)
  1949 
  1950 (*
  1951   Uses conversions, omitting proofs for efficiency.  See:
  1952     L C Paulson, A higher-order implementation of rewriting,
  1953     Science of Computer Programming 3 (1983), pages 119-149.
  1954 *)
  1955 
  1956 type prover = meta_simpset -> thm -> thm option;
  1957 type termrec = (Sign.sg_ref * term list) * term;
  1958 type conv = meta_simpset -> termrec -> termrec;
  1959 
  1960 fun check_conv
  1961       (thm as Thm{shyps,hyps,prop,sign_ref,der,...}, prop0, ders) =
  1962   let fun err() = (trace_thm false "Proved wrong thm (Check subgoaler?)" thm;
  1963                    trace_term false "Should have proved:" (Sign.deref sign_ref) prop0;
  1964                    None)
  1965       val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
  1966   in case prop of
  1967        Const("==",_) $ lhs $ rhs =>
  1968          if (lhs = lhs0) orelse
  1969             (lhs aconv Envir.norm_term (Envir.empty 0) lhs0)
  1970          then (trace_thm false "SUCCEEDED" thm; 
  1971                Some(rhs, (shyps, hyps, der::ders)))
  1972          else err()
  1973      | _ => err()
  1974   end;
  1975 
  1976 fun ren_inst(insts,prop,pat,obj) =
  1977   let val ren = match_bvs(pat,obj,[])
  1978       fun renAbs(Abs(x,T,b)) =
  1979             Abs(case assoc_string(ren,x) of None => x | Some(y) => y, T, renAbs(b))
  1980         | renAbs(f$t) = renAbs(f) $ renAbs(t)
  1981         | renAbs(t) = t
  1982   in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
  1983 
  1984 fun incr_insts i (in1:(indexname*typ)list,in2:(indexname*term)list) =
  1985   let fun incr ((a,n),x) = ((a,n+i),x)
  1986   in (map incr in1, map incr in2) end;
  1987 
  1988 fun add_insts_sorts ((iTs, is), Ss) =
  1989   add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));
  1990 
  1991 
  1992 (* mk_procrule *)
  1993 
  1994 fun mk_procrule thm =
  1995   let val (_,prems,lhs,rhs,_) = decomp_simp thm
  1996   in if rewrite_rule_extra_vars prems lhs rhs
  1997      then (prthm true "Extra vars on rhs:" thm; [])
  1998      else [mk_rrule2{thm = thm, lhs = lhs, perm = false}]
  1999   end;
  2000 
  2001 
  2002 (* conversion to apply the meta simpset to a term *)
  2003 
  2004 (* Since the rewriting strategy is bottom-up, we avoid re-normalizing already
  2005    normalized terms by carrying around the rhs of the rewrite rule just
  2006    applied. This is called the `skeleton'. It is decomposed in parallel
  2007    with the term. Once a Var is encountered, the corresponding term is
  2008    already in normal form.
  2009    skel0 is a dummy skeleton that is to enforce complete normalization.
  2010 *)
  2011 val skel0 = Bound 0;
  2012 
  2013 (* Use rhs as skeleton only if the lhs does not contain unnormalized bits.
  2014    The latter may happen iff there are weak congruence rules for constants
  2015    in the lhs.
  2016 *)
  2017 fun uncond_skel((_,weak),(lhs,rhs)) =
  2018   if null weak then rhs (* optimization *)
  2019   else if exists_Const (fn (c,_) => c mem weak) lhs then skel0
  2020        else rhs;
  2021 
  2022 (* Behaves like unconditional rule if rhs does not contain vars not in the lhs.
  2023    Otherwise those vars may become instantiated with unnormalized terms
  2024    while the premises are solved.
  2025 *)
  2026 fun cond_skel(args as (congs,(lhs,rhs))) =
  2027   if term_varnames rhs subset term_varnames lhs then uncond_skel(args)
  2028   else skel0;
  2029 
  2030 (*
  2031   we try in order:
  2032     (1) beta reduction
  2033     (2) unconditional rewrite rules
  2034     (3) conditional rewrite rules
  2035     (4) simplification procedures
  2036 
  2037   IMPORTANT: rewrite rules must not introduce new Vars or TVars!
  2038 
  2039 *)
  2040 
  2041 fun rewritec (prover,sign_reft,maxt)
  2042              (mss as Mss{rules, procs, termless, prems, congs, ...}) 
  2043              (t:term,etc as (shypst,hypst,ders)) =
  2044   let
  2045     val eta_t = Pattern.eta_contract t;
  2046     val signt = Sign.deref sign_reft;
  2047     val tsigt = Sign.tsig_of signt;
  2048     fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...},
  2049             lhs, elhs, fo, perm} =
  2050       let
  2051         val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
  2052                 else (prthm true "Rewrite rule from different theory:" thm;
  2053                       raise Pattern.MATCH);
  2054         val rprop = if maxt = ~1 then prop
  2055                     else Logic.incr_indexes([],maxt+1) prop;
  2056         val insts = if fo then Pattern.first_order_match tsigt (elhs,eta_t)
  2057                           else Pattern.match             tsigt (elhs,eta_t);
  2058         val insts = if maxt = ~1 then insts else incr_insts (maxt+1) insts
  2059         val prop' = ren_inst(insts,rprop,lhs,eta_t);
  2060         val hyps' = union_term(hyps,hypst);
  2061         val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
  2062         val unconditional = (Logic.count_prems(prop',0) = 0);
  2063         val maxidx' = if unconditional then maxt else maxidx+maxt+1
  2064         val ct' = Cterm{sign_ref = sign_reft,       (*used for deriv only*)
  2065                         t = prop', T = propT, maxidx = maxidx'}
  2066         val der' = infer_derivs (RewriteC ct', [der]);
  2067         val thm' = Thm{sign_ref = sign_reft, der = der', shyps = shyps',
  2068                        hyps = hyps', prop = prop', maxidx = maxidx'}
  2069         val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
  2070       in
  2071         if perm andalso not(termless(rhs',lhs')) then None
  2072         else
  2073           (trace_thm false "Applying instance of rewrite rule:" thm;
  2074            if unconditional
  2075            then
  2076              (trace_thm false "Rewriting:" thm';
  2077               let val lr = Logic.dest_equals prop
  2078                   val trec' = (rhs', (shyps', hyps', der'::ders))
  2079               in Some(trec',uncond_skel(congs,lr)) end)
  2080            else
  2081              (trace_thm false "Trying to rewrite:" thm';
  2082               case prover mss thm' of
  2083                 None       => (trace_thm false "FAILED" thm'; None)
  2084               | Some(thm2) =>
  2085                   (case check_conv(thm2,prop',ders) of
  2086                      None => None |
  2087                      Some trec =>
  2088                        let val concl = Logic.strip_imp_concl prop
  2089                            val lr = Logic.dest_equals concl
  2090                        in Some(trec,cond_skel(congs,lr)) end)))
  2091       end
  2092 
  2093     fun rews [] = None
  2094       | rews (rrule :: rrules) =
  2095           let val opt = rew rrule handle Pattern.MATCH => None
  2096           in case opt of None => rews rrules | some => some end;
  2097 
  2098     fun sort_rrules rrs = let
  2099       fun is_simple({thm as Thm{prop,...}, ...}:rrule) = case prop of 
  2100                                       Const("==",_) $ _ $ _ => true
  2101                                       | _                   => false 
  2102       fun sort []        (re1,re2) = re1 @ re2
  2103         | sort (rr::rrs) (re1,re2) = if is_simple rr 
  2104                                      then sort rrs (rr::re1,re2)
  2105                                      else sort rrs (re1,rr::re2)
  2106     in sort rrs ([],[]) end
  2107 
  2108     fun proc_rews ([]:simproc list) = None
  2109       | proc_rews ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
  2110           if Pattern.matches tsigt (plhs, t) then
  2111             (trace_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
  2112              case proc signt prems eta_t of
  2113                None => (trace false "FAILED"; proc_rews ps)
  2114              | Some raw_thm =>
  2115                  (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
  2116                   (case rews (mk_procrule raw_thm) of
  2117                     None => (trace false "IGNORED"; proc_rews ps)
  2118                   | some => some)))
  2119           else proc_rews ps;
  2120   in case eta_t of
  2121        Abs (_, _, body) $ u => Some ((subst_bound (u, body), etc),skel0)
  2122      | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
  2123                None => proc_rews (Net.match_term procs eta_t)
  2124              | some => some)
  2125   end;
  2126 
  2127 
  2128 (* conversion to apply a congruence rule to a term *)
  2129 
  2130 fun congc (prover,sign_reft,maxt) {thm=cong,lhs=lhs} (t,(shypst,hypst,ders)) =
  2131   let val signt = Sign.deref sign_reft;
  2132       val tsig = Sign.tsig_of signt;
  2133       val Thm{sign_ref,der,shyps,hyps,maxidx,prop,...} = cong
  2134       val _ = if Sign.subsig(Sign.deref sign_ref,signt) then ()
  2135                  else error("Congruence rule from different theory")
  2136       val rprop = if maxt = ~1 then prop
  2137                   else Logic.incr_indexes([],maxt+1) prop;
  2138       val rlhs = if maxt = ~1 then lhs
  2139                  else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
  2140       val insts = Pattern.match tsig (rlhs,t)
  2141       (* Pattern.match can raise Pattern.MATCH;
  2142          is handled when congc is called *)
  2143       val prop' = ren_inst(insts,rprop,rlhs,t);
  2144       val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst))
  2145       val maxidx' = maxidx_of_term prop'
  2146       val ct' = Cterm{sign_ref = sign_reft,     (*used for deriv only*)
  2147                       t = prop',
  2148                       T = propT,
  2149                       maxidx = maxidx'}
  2150       val thm' = Thm{sign_ref = sign_reft, 
  2151                      der = infer_derivs (CongC ct', [der]),
  2152                      shyps = shyps',
  2153                      hyps = union_term(hyps,hypst),
  2154                      prop = prop',
  2155                      maxidx = maxidx'};
  2156       val unit = trace_thm false "Applying congruence rule:" thm';
  2157       fun err() = error("Failed congruence proof!")
  2158 
  2159   in case prover thm' of
  2160        None => err()
  2161      | Some(thm2) => (case check_conv(thm2,prop',ders) of
  2162                         None => err() | some => some)
  2163   end;
  2164 
  2165 fun bottomc ((simprem,useprem,mutsimp),prover,sign_ref,maxidx) =
  2166   let
  2167     fun botc fail skel mss trec =
  2168           if is_Var skel then if fail then None else Some(trec)
  2169           else
  2170           (case subc skel mss trec of
  2171              some as Some(trec1) =>
  2172                (case rewritec (prover,sign_ref,maxidx) mss trec1 of
  2173                   Some(trec2,skel2) => botc false skel2 mss trec2
  2174                 | None => some)
  2175            | None =>
  2176                (case rewritec (prover,sign_ref,maxidx) mss trec of
  2177                   Some(trec2,skel2) => botc false skel2 mss trec2
  2178                 | None => if fail then None else Some(trec)))
  2179 
  2180     and try_botc mss trec =
  2181           (case botc true skel0 mss trec of
  2182              Some(trec1) => trec1 | None => trec)
  2183 
  2184     and subc skel
  2185              (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless})
  2186              (trec as (t0:term,etc:sort list*term list * rule mtree list)) =
  2187        (case t0 of
  2188            Abs(a,T,t) =>
  2189              let val b = variant bounds a
  2190                  val v = Free("." ^ b,T)
  2191                  val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
  2192                  val skel' = case skel of Abs(_,_,sk) => sk | _ => skel0
  2193              in case botc true skel' mss' (subst_bound(v,t),etc) of
  2194                   Some(t',etc') => Some(Abs(a, T, abstract_over(v,t')), etc')
  2195                 | None => None
  2196              end
  2197          | t$u => (case t of
  2198              Const("==>",_)$s  => Some(impc(s,u,mss,etc))
  2199            | Abs(_,_,body) =>
  2200                let val trec = (subst_bound(u,body), etc)
  2201                in case subc skel0 mss trec of
  2202                     None => Some(trec)
  2203                   | trec => trec
  2204                end
  2205            | _  =>
  2206                let fun appc() =
  2207                      let val (tskel,uskel) =
  2208                                 case skel of tskel$uskel => (tskel,uskel)
  2209                                            | _ => (skel0,skel0)
  2210                      in
  2211                      (case botc true tskel mss (t,etc) of
  2212                         Some(t1,etc1) =>
  2213                           (case botc true uskel mss (u,etc1) of
  2214                              Some(u1,etc2) => Some(t1$u1, etc2)
  2215                            | None => Some(t1$u, etc1))
  2216                       | None =>
  2217                           (case botc true uskel mss (u,etc) of
  2218                              Some(u1,etc1) => Some(t$u1, etc1)
  2219                            | None => None))
  2220                      end
  2221                    val (h,ts) = strip_comb t
  2222                in case h of
  2223                     Const(a,_) =>
  2224                       (case assoc_string(fst congs,a) of
  2225                          None => appc()
  2226                        | Some(cong) =>
  2227                            (congc (prover mss,sign_ref,maxidx) cong trec
  2228                             handle Pattern.MATCH => appc() ) )
  2229                   | _ => appc()
  2230                end)
  2231          | _ => None)
  2232 
  2233     and impc args =
  2234       if mutsimp
  2235       then let val (prem, conc, mss, etc) = args
  2236            in snd(mut_impc([], prem, conc, mss, etc)) end
  2237       else nonmut_impc args
  2238 
  2239     and mut_impc (prems, prem, conc, mss, etc) =
  2240       let val (prem1,etc1) = try_botc mss (prem,etc)
  2241       in mut_impc1(prems, prem1, conc, mss, etc1) end
  2242 
  2243     and mut_impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) =
  2244       let
  2245         fun uncond({thm,lhs,perm}) =
  2246           if nprems_of thm = 0 then Some lhs else None
  2247 
  2248         val (lhss1,mss1) =
  2249           if maxidx_of_term prem1 <> ~1
  2250           then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:"
  2251                            (Sign.deref sign_ref) prem1;
  2252                 ([],mss))
  2253           else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1, 
  2254                                            T=propT, maxidx= ~1})
  2255                    val rrules1 = extract_safe_rrules(mss,thm)
  2256                    val lhss1 = mapfilter uncond rrules1
  2257                    val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1)
  2258                in (lhss1, mss1) end
  2259 
  2260         fun disch1(conc2,(shyps2,hyps2,ders2)) =
  2261           let val hyps2' = if gen_mem (op aconv) (prem1, hyps1)
  2262                            then hyps2 else hyps2\prem1
  2263           in (Logic.mk_implies(prem1,conc2),(shyps2,hyps2',ders2)) end
  2264 
  2265         fun rebuild trec2 =
  2266           let val trec = disch1 trec2
  2267           in case rewritec (prover,sign_ref,maxidx) mss trec of
  2268                None => (None,trec)
  2269              | Some((Const("==>",_)$prem$conc,etc),_) =>
  2270                  mut_impc(prems,prem,conc,mss,etc)
  2271              | Some(trec',_) => (None,trec')
  2272           end
  2273 
  2274         fun simpconc() =
  2275           case conc of
  2276             Const("==>",_)$s$t =>
  2277               (case mut_impc(prems@[prem1],s,t,mss1,etc1) of
  2278                  (Some(i,prem),trec2) =>
  2279                     let val trec2' = disch1 trec2
  2280                     in if i=0 then mut_impc1(prems,prem,fst trec2',mss,snd trec2')
  2281                        else (Some(i-1,prem),trec2')
  2282                     end
  2283                | (None,trec) => rebuild(trec))
  2284           | _ => rebuild(try_botc mss1 (conc,etc1))
  2285 
  2286       in let val sg = Sign.deref sign_ref
  2287                   val tsig = #tsig(Sign.rep_sg sg)
  2288                   fun reducible t =
  2289                     exists (fn lhs => Pattern.matches_subterm tsig (lhs,t))
  2290                            lhss1;
  2291               in case dropwhile (not o reducible) prems of
  2292                    [] => simpconc()
  2293                  | red::rest => (trace_term false "Can now reduce premise:" sg
  2294                                             red;
  2295                                  (Some(length rest,prem1),(conc,etc1)))
  2296               end
  2297       end
  2298 
  2299      (* legacy code - only for backwards compatibility *)
  2300      and nonmut_impc(prem, conc, mss, etc as (_,hyps1,_)) =
  2301        let val (prem1,etc1) = if simprem then try_botc mss (prem,etc)
  2302                               else (prem,etc)
  2303            val maxidx1 = maxidx_of_term prem1
  2304            val mss1 =
  2305              if not useprem then mss else
  2306              if maxidx1 <> ~1
  2307              then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:"
  2308                               (Sign.deref sign_ref) prem1;
  2309                    mss)
  2310              else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1, 
  2311                                               T=propT, maxidx= ~1})
  2312                   in add_safe_simp(add_prems(mss,[thm]), thm) end
  2313            val (conc2,(shyps2,hyps2,ders2)) = try_botc mss1 (conc,etc1)
  2314            val hyps2' = if prem1 mem hyps1 then hyps2 else hyps2\prem1
  2315        in (Logic.mk_implies(prem1,conc2), (shyps2, hyps2', ders2)) end
  2316 
  2317  in try_botc end;
  2318 
  2319 
  2320 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
  2321 
  2322 (*
  2323   Parameters:
  2324     mode = (simplify A,
  2325             use A in simplifying B,
  2326             use prems of B (if B is again a meta-impl.) to simplify A)
  2327            when simplifying A ==> B
  2328     mss: contains equality theorems of the form [|p1,...|] ==> t==u
  2329     prover: how to solve premises in conditional rewrites and congruences
  2330 *)
  2331 
  2332 (* FIXME: check that #bounds(mss) does not "occur" in ct alread *)
  2333 
  2334 fun rewrite_cterm mode mss prover ct =
  2335   let val Cterm {sign_ref, t, T, maxidx} = ct;
  2336       val (u,(shyps,hyps,ders)) = bottomc (mode,prover, sign_ref, maxidx) mss 
  2337                                           (t, (add_term_sorts(t,[]), [], []));
  2338       val prop = Logic.mk_equals(t,u)
  2339   in
  2340       Thm{sign_ref = sign_ref, 
  2341           der = infer_derivs (Rewrite_cterm ct, ders),
  2342           maxidx = maxidx,
  2343           shyps = shyps, 
  2344           hyps = hyps, 
  2345           prop = prop}
  2346   end;
  2347 
  2348 
  2349 
  2350 (*** Oracles ***)
  2351 
  2352 fun invoke_oracle thy raw_name =
  2353   let
  2354     val {sign = sg, oracles, ...} = Theory.rep_theory thy;
  2355     val name = Sign.intern sg Theory.oracleK raw_name;
  2356     val oracle =
  2357       (case Symtab.lookup (oracles, name) of
  2358         None => raise THM ("Unknown oracle: " ^ name, 0, [])
  2359       | Some (f, _) => f);
  2360   in
  2361     fn (sign, exn) =>
  2362       let
  2363         val sign_ref' = Sign.merge_refs (Sign.self_ref sg, Sign.self_ref sign);
  2364         val sign' = Sign.deref sign_ref';
  2365         val (prop, T, maxidx) = Sign.certify_term sign' (oracle (sign', exn));
  2366       in
  2367         if T <> propT then
  2368           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
  2369         else fix_shyps [] []
  2370           (Thm {sign_ref = sign_ref', 
  2371             der = Join (Oracle (name, sign, exn), []),
  2372             maxidx = maxidx,
  2373             shyps = [], 
  2374             hyps = [], 
  2375             prop = prop})
  2376       end
  2377   end;
  2378 
  2379 
  2380 end;
  2381 
  2382 
  2383 structure BasicThm: BASIC_THM = Thm;
  2384 open BasicThm;