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