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