src/Pure/thm.ML
author wenzelm
Sat Nov 24 16:55:56 2001 +0100 (2001-11-24)
changeset 12284 131e743d168a
parent 11692 6d15ae4b1123
child 12500 0a6667d65e9b
permissions -rw-r--r--
added gen_merge_lists(') and merge_lists(');
removed obsolete generic_extend, generic_merge, extend_list;
     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 lifting and resolution).
     8 *)
     9 
    10 signature BASIC_THM =
    11   sig
    12   (*certified types*)
    13   type ctyp
    14   val rep_ctyp          : ctyp -> {sign: Sign.sg, T: typ}
    15   val typ_of            : ctyp -> typ
    16   val ctyp_of           : Sign.sg -> typ -> ctyp
    17   val read_ctyp         : Sign.sg -> string -> ctyp
    18 
    19   (*certified terms*)
    20   type cterm
    21   exception CTERM of string
    22   val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
    23   val crep_cterm        : cterm -> {sign: Sign.sg, t: term, T: ctyp, maxidx: int}
    24   val sign_of_cterm	: cterm -> Sign.sg
    25   val term_of           : cterm -> term
    26   val cterm_of          : Sign.sg -> term -> cterm
    27   val ctyp_of_term      : cterm -> ctyp
    28   val read_cterm        : Sign.sg -> string * typ -> cterm
    29   val cterm_fun         : (term -> term) -> (cterm -> cterm)
    30   val adjust_maxidx     : cterm -> cterm
    31   val read_def_cterm    :
    32     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    33     string list -> bool -> string * typ -> cterm * (indexname * typ) list
    34   val read_def_cterms   :
    35     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    36     string list -> bool -> (string * typ)list
    37     -> cterm list * (indexname * typ)list
    38 
    39   type tag		(* = string * string list *)
    40 
    41   (*meta theorems*)
    42   type thm
    43   val rep_thm           : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int,
    44                                   shyps: sort list, hyps: term list, 
    45                                   prop: term}
    46   val crep_thm          : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int,
    47                                   shyps: sort list, hyps: cterm list, 
    48                                   prop: cterm}
    49   exception THM of string * int * thm list
    50   type 'a attribute 	(* = 'a * thm -> 'a * thm *)
    51   val eq_thm		: thm * thm -> bool
    52   val sign_of_thm       : thm -> Sign.sg
    53   val transfer_sg	: Sign.sg -> thm -> thm
    54   val transfer		: theory -> thm -> thm
    55   val tpairs_of         : thm -> (term * term) list
    56   val prems_of          : thm -> term list
    57   val nprems_of         : thm -> int
    58   val concl_of          : thm -> term
    59   val cprop_of          : thm -> cterm
    60   val extra_shyps       : thm -> sort list
    61   val strip_shyps       : thm -> thm
    62   val get_axiom         : theory -> xstring -> thm
    63   val def_name		: string -> string
    64   val get_def           : theory -> xstring -> thm
    65   val axioms_of         : theory -> (string * thm) list
    66 
    67   (*meta rules*)
    68   val assume            : cterm -> thm
    69   val compress          : thm -> thm
    70   val implies_intr      : cterm -> thm -> thm
    71   val implies_elim      : thm -> thm -> thm
    72   val forall_intr       : cterm -> thm -> thm
    73   val forall_elim       : cterm -> thm -> thm
    74   val reflexive         : cterm -> thm
    75   val symmetric         : thm -> thm
    76   val transitive        : thm -> thm -> thm
    77   val beta_conversion   : bool -> cterm -> thm
    78   val eta_conversion    : cterm -> thm
    79   val abstract_rule     : string -> cterm -> thm -> thm
    80   val combination       : thm -> thm -> thm
    81   val equal_intr        : thm -> thm -> thm
    82   val equal_elim        : thm -> thm -> thm
    83   val implies_intr_hyps : thm -> thm
    84   val flexflex_rule     : thm -> thm Seq.seq
    85   val instantiate       :
    86     (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
    87   val trivial           : cterm -> thm
    88   val class_triv        : Sign.sg -> class -> thm
    89   val varifyT           : thm -> thm
    90   val varifyT'          : string list -> thm -> thm
    91   val freezeT           : thm -> thm
    92   val dest_state        : thm * int ->
    93     (term * term) list * term list * term * term
    94   val lift_rule         : (thm * int) -> thm -> thm
    95   val incr_indexes      : int -> thm -> thm
    96   val assumption        : int -> thm -> thm Seq.seq
    97   val eq_assumption     : int -> thm -> thm
    98   val rotate_rule       : int -> int -> thm -> thm
    99   val permute_prems     : int -> int -> thm -> thm
   100   val rename_params_rule: string list * int -> thm -> thm
   101   val bicompose         : bool -> bool * thm * int ->
   102     int -> thm -> thm Seq.seq
   103   val biresolution      : bool -> (bool * thm) list ->
   104     int -> thm -> thm Seq.seq
   105   val invoke_oracle     : theory -> xstring -> Sign.sg * Object.T -> thm
   106 end;
   107 
   108 signature THM =
   109 sig
   110   include BASIC_THM
   111   val dest_comb         : cterm -> cterm * cterm
   112   val dest_abs          : string option -> cterm -> cterm * cterm
   113   val capply            : cterm -> cterm -> cterm
   114   val cabs              : cterm -> cterm -> cterm
   115   val major_prem_of	: thm -> term
   116   val no_prems		: thm -> bool
   117   val no_attributes	: 'a -> 'a * 'b attribute list
   118   val apply_attributes	: ('a * thm) * 'a attribute list -> ('a * thm)
   119   val applys_attributes	: ('a * thm list) * 'a attribute list -> ('a * thm list)
   120   val get_name_tags	: thm -> string * tag list
   121   val put_name_tags	: string * tag list -> thm -> thm
   122   val name_of_thm	: thm -> string
   123   val tags_of_thm	: thm -> tag list
   124   val name_thm		: string * thm -> thm
   125   val rename_boundvars  : term -> term -> thm -> thm
   126   val cterm_match       : cterm * cterm ->
   127     (indexname * ctyp) list * (cterm * cterm) list
   128   val cterm_first_order_match : cterm * cterm ->
   129     (indexname * ctyp) list * (cterm * cterm) list
   130   val cterm_incr_indexes : int -> cterm -> cterm
   131 end;
   132 
   133 structure Thm: THM =
   134 struct
   135 
   136 (*** Certified terms and types ***)
   137 
   138 (** certified types **)
   139 
   140 (*certified typs under a signature*)
   141 
   142 datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};
   143 
   144 fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
   145 fun typ_of (Ctyp {T, ...}) = T;
   146 
   147 fun ctyp_of sign T =
   148   Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T};
   149 
   150 fun read_ctyp sign s =
   151   Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s};
   152 
   153 
   154 
   155 (** certified terms **)
   156 
   157 (*certified terms under a signature, with checked typ and maxidx of Vars*)
   158 
   159 datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};
   160 
   161 fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   162   {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};
   163 
   164 fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   165   {sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T},
   166     maxidx = maxidx};
   167 
   168 fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref;
   169 
   170 fun term_of (Cterm {t, ...}) = t;
   171 
   172 fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};
   173 
   174 (*create a cterm by checking a "raw" term with respect to a signature*)
   175 fun cterm_of sign tm =
   176   let val (t, T, maxidx) = Sign.certify_term sign tm
   177   in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
   178   end;
   179 
   180 fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t);
   181 
   182 
   183 exception CTERM of string;
   184 
   185 (*Destruct application in cterms*)
   186 fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) =
   187       let val typeA = fastype_of A;
   188           val typeB =
   189             case typeA of Type("fun",[S,T]) => S
   190                         | _ => error "Function type expected in dest_comb";
   191       in
   192       (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA},
   193        Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB})
   194       end
   195   | dest_comb _ = raise CTERM "dest_comb";
   196 
   197 (*Destruct abstraction in cterms*)
   198 fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
   199       let val (y,N) = variant_abs (if_none a x,ty,M)
   200       in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)},
   201           Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N})
   202       end
   203   | dest_abs _ _ = raise CTERM "dest_abs";
   204 
   205 (*Makes maxidx precise: it is often too big*)
   206 fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) =
   207   if maxidx = ~1 then ct 
   208   else  Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t};
   209 
   210 (*Form cterm out of a function and an argument*)
   211 fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
   212            (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
   213       if T = dty then
   214         Cterm{t=Sign.nodup_vars (f$x), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
   215           maxidx=Int.max(maxidx1, maxidx2)}
   216       else raise CTERM "capply: types don't agree"
   217   | capply _ _ = raise CTERM "capply: first arg is not a function"
   218 
   219 fun cabs (Cterm {t=Free(a,ty), sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
   220          (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
   221       Cterm {t=Sign.nodup_vars (absfree(a,ty,t2)), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
   222              T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)}
   223   | cabs _ _ = raise CTERM "cabs: first arg is not a free variable";
   224 
   225 (*Matching of cterms*)
   226 fun gen_cterm_match mtch
   227       (Cterm {sign_ref = sign_ref1, maxidx = maxidx1, t = t1, ...},
   228        Cterm {sign_ref = sign_ref2, maxidx = maxidx2, t = t2, ...}) =
   229   let
   230     val sign_ref = Sign.merge_refs (sign_ref1, sign_ref2);
   231     val tsig = Sign.tsig_of (Sign.deref sign_ref);
   232     val (Tinsts, tinsts) = mtch tsig (t1, t2);
   233     val maxidx = Int.max (maxidx1, maxidx2);
   234     val vars = map dest_Var (term_vars t1);
   235     fun mk_cTinsts (ixn, T) = (ixn, Ctyp {sign_ref = sign_ref, T = T});
   236     fun mk_ctinsts (ixn, t) =
   237       let val T = typ_subst_TVars Tinsts (the (assoc (vars, ixn)))
   238       in
   239         (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
   240          Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t})
   241       end;
   242   in (map mk_cTinsts Tinsts, map mk_ctinsts tinsts) end;
   243 
   244 val cterm_match = gen_cterm_match Pattern.match;
   245 val cterm_first_order_match = gen_cterm_match Pattern.first_order_match;
   246 
   247 (*Incrementing indexes*)
   248 fun cterm_incr_indexes i (ct as Cterm {sign_ref, maxidx, t, T}) =
   249   if i < 0 then raise CTERM "negative increment" else 
   250   if i = 0 then ct else
   251     Cterm {sign_ref = sign_ref, maxidx = maxidx + i,
   252       t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T};
   253 
   254 
   255 
   256 (** read cterms **)   (*exception ERROR*)
   257 
   258 (*read terms, infer types, certify terms*)
   259 fun read_def_cterms (sign, types, sorts) used freeze sTs =
   260   let
   261     val (ts', tye) = Sign.read_def_terms (sign, types, sorts) used freeze sTs;
   262     val cts = map (cterm_of sign) ts'
   263       handle TYPE (msg, _, _) => error msg
   264            | TERM (msg, _) => error msg;
   265   in (cts, tye) end;
   266 
   267 (*read term, infer types, certify term*)
   268 fun read_def_cterm args used freeze aT =
   269   let val ([ct],tye) = read_def_cterms args used freeze [aT]
   270   in (ct,tye) end;
   271 
   272 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
   273 
   274 
   275 (*tags provide additional comment, apart from the axiom/theorem name*)
   276 type tag = string * string list;
   277 
   278 
   279 (*** Meta theorems ***)
   280 
   281 structure Pt = Proofterm;
   282 
   283 datatype thm = Thm of
   284  {sign_ref: Sign.sg_ref,       (*mutable reference to signature*)
   285   der: bool * Pt.proof,        (*derivation*)
   286   maxidx: int,                 (*maximum index of any Var or TVar*)
   287   shyps: sort list,            (*sort hypotheses*)
   288   hyps: term list,             (*hypotheses*)
   289   prop: term};                 (*conclusion*)
   290 
   291 fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   292   {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
   293     shyps = shyps, hyps = hyps, prop = prop};
   294 
   295 (*Version of rep_thm returning cterms instead of terms*)
   296 fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   297   let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max};
   298   in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps,
   299       hyps = map (ctermf ~1) hyps,
   300       prop = ctermf maxidx prop}
   301   end;
   302 
   303 (*errors involving theorems*)
   304 exception THM of string * int * thm list;
   305 
   306 (*attributes subsume any kind of rules or addXXXs modifiers*)
   307 type 'a attribute = 'a * thm -> 'a * thm;
   308 
   309 fun no_attributes x = (x, []);
   310 fun apply_attributes (x_th, atts) = Library.apply atts x_th;
   311 fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
   312 
   313 fun eq_thm (th1, th2) =
   314   let
   315     val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, ...} =
   316       rep_thm th1;
   317     val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, ...} =
   318       rep_thm th2;
   319   in
   320     Sign.joinable (sg1, sg2) andalso
   321     eq_set_sort (shyps1, shyps2) andalso
   322     aconvs (hyps1, hyps2) andalso
   323     prop1 aconv prop2
   324   end;
   325 
   326 fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
   327 
   328 (*merge signatures of two theorems; raise exception if incompatible*)
   329 fun merge_thm_sgs
   330     (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
   331   Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
   332 
   333 (*transfer thm to super theory (non-destructive)*)
   334 fun transfer_sg sign' thm =
   335   let
   336     val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   337     val sign = Sign.deref sign_ref;
   338   in
   339     if Sign.eq_sg (sign, sign') then thm
   340     else if Sign.subsig (sign, sign') then
   341       Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
   342         shyps = shyps, hyps = hyps, prop = prop}
   343     else raise THM ("transfer: not a super theory", 0, [thm])
   344   end;
   345 
   346 val transfer = transfer_sg o Theory.sign_of;
   347 
   348 (*maps object-rule to tpairs*)
   349 fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);
   350 
   351 (*maps object-rule to premises*)
   352 fun prems_of (Thm {prop, ...}) =
   353   Logic.strip_imp_prems (Logic.skip_flexpairs prop);
   354 
   355 (*counts premises in a rule*)
   356 fun nprems_of (Thm {prop, ...}) =
   357   Logic.count_prems (Logic.skip_flexpairs prop, 0);
   358 
   359 fun major_prem_of thm =
   360   (case prems_of thm of
   361     prem :: _ => Logic.strip_assums_concl prem
   362   | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm]));
   363 
   364 fun no_prems thm = nprems_of thm = 0;
   365 
   366 (*maps object-rule to conclusion*)
   367 fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
   368 
   369 (*the statement of any thm is a cterm*)
   370 fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) =
   371   Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop};
   372 
   373 
   374 
   375 (** sort contexts of theorems **)
   376 
   377 (* basic utils *)
   378 
   379 (*accumulate sorts suppressing duplicates; these are coded low levelly
   380   to improve efficiency a bit*)
   381 
   382 fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss)
   383   | add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss)
   384   | add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss)
   385 and add_typs_sorts ([], Ss) = Ss
   386   | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss));
   387 
   388 fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss)
   389   | add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss)
   390   | add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss)
   391   | add_term_sorts (Bound _, Ss) = Ss
   392   | add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss))
   393   | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss));
   394 
   395 fun add_terms_sorts ([], Ss) = Ss
   396   | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));
   397 
   398 fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs);
   399 
   400 fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) =
   401   Vartab.foldl (add_term_sorts o swap o apsnd snd)
   402     (Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol);
   403 
   404 fun add_insts_sorts ((iTs, is), Ss) =
   405   add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));
   406 
   407 fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) =
   408   add_terms_sorts (hyps, add_term_sorts (prop, Ss));
   409 
   410 fun add_thms_shyps ([], Ss) = Ss
   411   | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) =
   412       add_thms_shyps (ths, union_sort (shyps, Ss));
   413 
   414 
   415 (*get 'dangling' sort constraints of a thm*)
   416 fun extra_shyps (th as Thm {shyps, ...}) =
   417   Term.rems_sort (shyps, add_thm_sorts (th, []));
   418 
   419 
   420 (* fix_shyps *)
   421 
   422 fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref));
   423 
   424 (*preserve sort contexts of rule premises and substituted types*)
   425 fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, prop, ...}) =
   426   Thm
   427    {sign_ref = sign_ref,
   428     der = der,             (*no new derivation, as other rules call this*)
   429     maxidx = maxidx,
   430     shyps =
   431       if all_sorts_nonempty sign_ref then []
   432       else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))),
   433     hyps = hyps, prop = prop}
   434 
   435 
   436 (* strip_shyps *)
   437 
   438 (*remove extra sorts that are non-empty by virtue of type signature information*)
   439 fun strip_shyps (thm as Thm {shyps = [], ...}) = thm
   440   | strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   441       let
   442         val sign = Sign.deref sign_ref;
   443 
   444         val present_sorts = add_thm_sorts (thm, []);
   445         val extra_shyps = Term.rems_sort (shyps, present_sorts);
   446         val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps;
   447       in
   448         Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
   449              shyps = Term.rems_sort (shyps, map #2 witnessed_shyps),
   450              hyps = hyps, prop = prop}
   451       end;
   452 
   453 
   454 
   455 (** Axioms **)
   456 
   457 (*look up the named axiom in the theory*)
   458 fun get_axiom theory raw_name =
   459   let
   460     val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name;
   461 
   462     fun get_ax [] = None
   463       | get_ax (thy :: thys) =
   464           let val {sign, axioms, ...} = Theory.rep_theory thy in
   465             (case Symtab.lookup (axioms, name) of
   466               Some t =>
   467                 Some (fix_shyps [] []
   468                   (Thm {sign_ref = Sign.self_ref sign,
   469                     der = Pt.infer_derivs' I
   470                       (false, Pt.axm_proof name t),
   471                     maxidx = maxidx_of_term t,
   472                     shyps = [], 
   473                     hyps = [], 
   474                     prop = t}))
   475             | None => get_ax thys)
   476           end;
   477   in
   478     (case get_ax (theory :: Theory.ancestors_of theory) of
   479       Some thm => thm
   480     | None => raise THEORY ("No axiom " ^ quote name, [theory]))
   481   end;
   482 
   483 fun def_name name = name ^ "_def";
   484 fun get_def thy = get_axiom thy o def_name;
   485 
   486 
   487 (*return additional axioms of this theory node*)
   488 fun axioms_of thy =
   489   map (fn (s, _) => (s, get_axiom thy s))
   490     (Symtab.dest (#axioms (Theory.rep_theory thy)));
   491 
   492 
   493 (* name and tags -- make proof objects more readable *)
   494 
   495 fun get_name_tags (Thm {prop, der = (_, prf), ...}) = Pt.get_name_tags prop prf;
   496 
   497 fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx, shyps, hyps, prop}) =
   498   Thm {sign_ref = sign_ref,
   499     der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf),
   500     maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop};
   501 
   502 val name_of_thm = #1 o get_name_tags;
   503 val tags_of_thm = #2 o get_name_tags;
   504 
   505 fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm;
   506 
   507 
   508 (*Compression of theorems -- a separate rule, not integrated with the others,
   509   as it could be slow.*)
   510 fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
   511     Thm {sign_ref = sign_ref, 
   512          der = der,     (*No derivation recorded!*)
   513          maxidx = maxidx,
   514          shyps = shyps, 
   515          hyps = map Term.compress_term hyps, 
   516          prop = Term.compress_term prop};
   517 
   518 
   519 
   520 (*** Meta rules ***)
   521 
   522 (*Check that term does not contain same var with different typing/sorting.
   523   If this check must be made, recalculate maxidx in hope of preventing its
   524   recurrence.*)
   525 fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s =
   526   Thm {sign_ref = sign_ref, 
   527          der = der,     
   528          maxidx = maxidx_of_term prop,
   529          shyps = shyps, 
   530          hyps = hyps, 
   531          prop = Sign.nodup_vars prop}
   532   handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);
   533 
   534 
   535 (** 'primitive' rules **)
   536 
   537 (*discharge all assumptions t from ts*)
   538 val disch = gen_rem (op aconv);
   539 
   540 (*The assumption rule A|-A in a theory*)
   541 fun assume raw_ct : thm =
   542   let val ct as Cterm {sign_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
   543   in  if T<>propT then
   544         raise THM("assume: assumptions must have type prop", 0, [])
   545       else if maxidx <> ~1 then
   546         raise THM("assume: assumptions may not contain scheme variables",
   547                   maxidx, [])
   548       else Thm{sign_ref   = sign_ref,
   549                der    = Pt.infer_derivs' I (false, Pt.Hyp prop),
   550                maxidx = ~1, 
   551                shyps  = add_term_sorts(prop,[]), 
   552                hyps   = [prop], 
   553                prop   = prop}
   554   end;
   555 
   556 (*Implication introduction
   557     [A]
   558      :
   559      B
   560   -------
   561   A ==> B
   562 *)
   563 fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,shyps,prop}) : thm =
   564   let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA
   565   in  if T<>propT then
   566         raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   567       else
   568          Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA),  
   569              der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
   570              maxidx = Int.max(maxidxA, maxidx),
   571              shyps = add_term_sorts (A, shyps),
   572              hyps = disch(hyps,A),
   573              prop = implies$A$prop}
   574       handle TERM _ =>
   575         raise THM("implies_intr: incompatible signatures", 0, [thB])
   576   end;
   577 
   578 
   579 (*Implication elimination
   580   A ==> B    A
   581   ------------
   582         B
   583 *)
   584 fun implies_elim thAB thA : thm =
   585     let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, prop=propA, ...} = thA
   586         and Thm{der, maxidx, hyps, shyps, prop, ...} = thAB;
   587         fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
   588     in  case prop of
   589             imp$A$B =>
   590                 if imp=implies andalso  A aconv propA
   591                 then
   592                   Thm{sign_ref= merge_thm_sgs(thAB,thA),
   593                       der = Pt.infer_derivs (curry Pt.%%) der derA,
   594                       maxidx = Int.max(maxA,maxidx),
   595                       shyps = union_sort (shypsA, shyps),
   596                       hyps = union_term(hypsA,hyps),  (*dups suppressed*)
   597                       prop = B}
   598                 else err("major premise")
   599           | _ => err("major premise")
   600     end;
   601 
   602 (*Forall introduction.  The Free or Var x must not be free in the hypotheses.
   603     A
   604   -----
   605   !!x.A
   606 *)
   607 fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
   608   let val x = term_of cx;
   609       fun result(a,T) = fix_shyps [th] []
   610         (Thm{sign_ref = sign_ref, 
   611              der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der,
   612              maxidx = maxidx,
   613              shyps = [],
   614              hyps = hyps,
   615              prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
   616   in  case x of
   617         Free(a,T) =>
   618           if exists (apl(x, Logic.occs)) hyps
   619           then  raise THM("forall_intr: variable free in assumptions", 0, [th])
   620           else  result(a,T)
   621       | Var((a,_),T) => result(a,T)
   622       | _ => raise THM("forall_intr: not a variable", 0, [th])
   623   end;
   624 
   625 (*Forall elimination
   626   !!x.A
   627   ------
   628   A[t/x]
   629 *)
   630 fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
   631   let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct
   632   in  case prop of
   633         Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   634           if T<>qary then
   635               raise THM("forall_elim: type mismatch", 0, [th])
   636           else let val thm = fix_shyps [th] []
   637                     (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
   638                          der = Pt.infer_derivs' (Pt.% o rpair (Some t)) der,
   639                          maxidx = Int.max(maxidx, maxt),
   640                          shyps = [],
   641                          hyps = hyps,  
   642                          prop = betapply(A,t)})
   643                in if maxt >= 0 andalso maxidx >= 0
   644                   then nodup_vars thm "forall_elim" 
   645                   else thm (*no new Vars: no expensive check!*)
   646                end
   647       | _ => raise THM("forall_elim: not quantified", 0, [th])
   648   end
   649   handle TERM _ =>
   650          raise THM("forall_elim: incompatible signatures", 0, [th]);
   651 
   652 
   653 (* Equality *)
   654 
   655 (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   656 fun reflexive ct =
   657   let val Cterm {sign_ref, t, T, maxidx} = ct
   658   in Thm{sign_ref= sign_ref, 
   659          der = Pt.infer_derivs' I (false, Pt.reflexive),
   660          shyps = add_term_sorts (t, []),
   661          hyps = [], 
   662          maxidx = maxidx,
   663          prop = Logic.mk_equals(t,t)}
   664   end;
   665 
   666 (*The symmetry rule
   667   t==u
   668   ----
   669   u==t
   670 *)
   671 fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
   672   case prop of
   673       (eq as Const("==", Type (_, [T, _]))) $ t $ u =>
   674         (*no fix_shyps*)
   675           Thm{sign_ref = sign_ref,
   676               der = Pt.infer_derivs' Pt.symmetric der,
   677               maxidx = maxidx,
   678               shyps = shyps,
   679               hyps = hyps,
   680               prop = eq$u$t}
   681     | _ => raise THM("symmetric", 0, [th]);
   682 
   683 (*The transitive rule
   684   t1==u    u==t2
   685   --------------
   686       t1==t2
   687 *)
   688 fun transitive th1 th2 =
   689   let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, prop=prop1,...} = th1
   690       and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, prop=prop2,...} = th2;
   691       fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
   692   in case (prop1,prop2) of
   693        ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) =>
   694           if not (u aconv u') then err"middle term"
   695           else let val thm =      
   696                  Thm{sign_ref= merge_thm_sgs(th1,th2), 
   697                      der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
   698                      maxidx = Int.max(max1,max2), 
   699                      shyps = union_sort (shyps1, shyps2),
   700                      hyps = union_term(hyps1,hyps2),
   701                      prop = eq$t1$t2}
   702                  in if max1 >= 0 andalso max2 >= 0
   703                     then nodup_vars thm "transitive" 
   704                     else thm (*no new Vars: no expensive check!*)
   705                  end
   706      | _ =>  err"premises"
   707   end;
   708 
   709 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x]
   710   Fully beta-reduces the term if full=true
   711 *)
   712 fun beta_conversion full ct =
   713   let val Cterm {sign_ref, t, T, maxidx} = ct
   714   in Thm
   715     {sign_ref = sign_ref,  
   716      der = Pt.infer_derivs' I (false, Pt.reflexive),
   717      maxidx = maxidx,
   718      shyps = add_term_sorts (t, []),
   719      hyps = [],
   720      prop = Logic.mk_equals (t, if full then Envir.beta_norm t
   721        else case t of
   722           Abs(_, _, bodt) $ u => subst_bound (u, bodt)
   723         | _ => raise THM ("beta_conversion: not a redex", 0, []))}
   724   end;
   725 
   726 fun eta_conversion ct =
   727   let val Cterm {sign_ref, t, T, maxidx} = ct
   728   in Thm
   729     {sign_ref = sign_ref,  
   730      der = Pt.infer_derivs' I (false, Pt.reflexive),
   731      maxidx = maxidx,
   732      shyps = add_term_sorts (t, []),
   733      hyps = [],
   734      prop = Logic.mk_equals (t, Pattern.eta_contract t)}
   735   end;
   736 
   737 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   738   The bound variable will be named "a" (since x will be something like x320)
   739      t == u
   740   ------------
   741   %x.t == %x.u
   742 *)
   743 fun abstract_rule a cx (th as Thm{sign_ref,der,maxidx,hyps,shyps,prop}) =
   744   let val x = term_of cx;
   745       val (t,u) = Logic.dest_equals prop
   746             handle TERM _ =>
   747                 raise THM("abstract_rule: premise not an equality", 0, [th])
   748       fun result T =
   749            Thm{sign_ref = sign_ref,
   750                der = Pt.infer_derivs' (Pt.abstract_rule x a) der,
   751                maxidx = maxidx, 
   752                shyps = add_typ_sorts (T, shyps), 
   753                hyps = hyps,
   754                prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   755                                       Abs(a, T, abstract_over (x,u)))}
   756   in  case x of
   757         Free(_,T) =>
   758          if exists (apl(x, Logic.occs)) hyps
   759          then raise THM("abstract_rule: variable free in assumptions", 0, [th])
   760          else result T
   761       | Var(_,T) => result T
   762       | _ => raise THM("abstract_rule: not a variable", 0, [th])
   763   end;
   764 
   765 (*The combination rule
   766   f == g  t == u
   767   --------------
   768    f(t) == g(u)
   769 *)
   770 fun combination th1 th2 =
   771   let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
   772               prop=prop1,...} = th1
   773       and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   774               prop=prop2,...} = th2
   775       fun chktypes fT tT =
   776             (case fT of
   777                 Type("fun",[T1,T2]) => 
   778                     if T1 <> tT then
   779                          raise THM("combination: types", 0, [th1,th2])
   780                     else ()
   781                 | _ => raise THM("combination: not function type", 0, 
   782                                  [th1,th2]))
   783   in case (prop1,prop2)  of
   784        (Const ("==", Type ("fun", [fT, _])) $ f $ g,
   785         Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
   786           let val _   = chktypes fT tT
   787               val thm = (*no fix_shyps*)
   788                         Thm{sign_ref = merge_thm_sgs(th1,th2), 
   789                             der = Pt.infer_derivs
   790                               (Pt.combination f g t u fT) der1 der2,
   791                             maxidx = Int.max(max1,max2), 
   792                             shyps = union_sort(shyps1,shyps2),
   793                             hyps = union_term(hyps1,hyps2),
   794                             prop = Logic.mk_equals(f$t, g$u)}
   795           in if max1 >= 0 andalso max2 >= 0
   796              then nodup_vars thm "combination" 
   797              else thm (*no new Vars: no expensive check!*)  
   798           end
   799      | _ =>  raise THM("combination: premises", 0, [th1,th2])
   800   end;
   801 
   802 
   803 (* Equality introduction
   804   A ==> B  B ==> A
   805   ----------------
   806        A == B
   807 *)
   808 fun equal_intr th1 th2 =
   809   let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
   810               prop=prop1,...} = th1
   811       and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   812               prop=prop2,...} = th2;
   813       fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
   814   in case (prop1,prop2) of
   815        (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A')  =>
   816           if A aconv A' andalso B aconv B'
   817           then
   818             (*no fix_shyps*)
   819               Thm{sign_ref = merge_thm_sgs(th1,th2),
   820                   der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
   821                   maxidx = Int.max(max1,max2),
   822                   shyps = union_sort(shyps1,shyps2),
   823                   hyps = union_term(hyps1,hyps2),
   824                   prop = Logic.mk_equals(A,B)}
   825           else err"not equal"
   826      | _ =>  err"premises"
   827   end;
   828 
   829 
   830 (*The equal propositions rule
   831   A == B  A
   832   ---------
   833       B
   834 *)
   835 fun equal_elim th1 th2 =
   836   let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   837       and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   838       fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2])
   839   in  case prop1  of
   840        Const("==",_) $ A $ B =>
   841           if not (prop2 aconv A) then err"not equal"  else
   842             fix_shyps [th1, th2] []
   843               (Thm{sign_ref= merge_thm_sgs(th1,th2), 
   844                    der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2,
   845                    maxidx = Int.max(max1,max2),
   846                    shyps = [],
   847                    hyps = union_term(hyps1,hyps2),
   848                    prop = B})
   849      | _ =>  err"major premise"
   850   end;
   851 
   852 
   853 
   854 (**** Derived rules ****)
   855 
   856 (*Discharge all hypotheses.  Need not verify cterms or call fix_shyps.
   857   Repeated hypotheses are discharged only once;  fold cannot do this*)
   858 fun implies_intr_hyps (Thm{sign_ref, der, maxidx, shyps, hyps=A::As, prop}) =
   859       implies_intr_hyps (*no fix_shyps*)
   860             (Thm{sign_ref = sign_ref, 
   861                  der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
   862                  maxidx = maxidx, 
   863                  shyps = shyps,
   864                  hyps = disch(As,A),  
   865                  prop = implies$A$prop})
   866   | implies_intr_hyps th = th;
   867 
   868 (*Smash" unifies the list of term pairs leaving no flex-flex pairs.
   869   Instantiates the theorem and deletes trivial tpairs.
   870   Resulting sequence may contain multiple elements if the tpairs are
   871     not all flex-flex. *)
   872 fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) =
   873   let fun newthm env =
   874           if Envir.is_empty env then th
   875           else
   876           let val (tpairs,horn) =
   877                         Logic.strip_flexpairs (Envir.norm_term env prop)
   878                 (*Remove trivial tpairs, of the form t=t*)
   879               val distpairs = filter (not o op aconv) tpairs
   880               val newprop = Logic.list_flexpairs(distpairs, horn)
   881           in  fix_shyps [th] (env_codT env)
   882                 (Thm{sign_ref = sign_ref, 
   883                      der = Pt.infer_derivs' (Pt.norm_proof' env) der,
   884                      maxidx = maxidx_of_term newprop, 
   885                      shyps = [], 
   886                      hyps = hyps,
   887                      prop = newprop})
   888           end;
   889       val (tpairs,_) = Logic.strip_flexpairs prop
   890   in Seq.map newthm
   891             (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
   892   end;
   893 
   894 (*Instantiation of Vars
   895            A
   896   -------------------
   897   A[t1/v1,....,tn/vn]
   898 *)
   899 
   900 local
   901 
   902 (*Check that all the terms are Vars and are distinct*)
   903 fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
   904 
   905 fun prt_typing sg_ref t T =
   906   let val sg = Sign.deref sg_ref in
   907     Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T]
   908   end;
   909 
   910 (*For instantiate: process pair of cterms, merge theories*)
   911 fun add_ctpair ((ct,cu), (sign_ref,tpairs)) =
   912   let
   913     val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct
   914     and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu;
   915     val sign_ref_merged = Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu));
   916   in
   917     if T=U then (sign_ref_merged, (t,u)::tpairs)
   918     else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict",
   919       Pretty.fbrk, prt_typing sign_ref_merged t T,
   920       Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u])
   921   end;
   922 
   923 fun add_ctyp ((v,ctyp), (sign_ref',vTs)) =
   924   let val Ctyp {T,sign_ref} = ctyp
   925   in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end;
   926 
   927 in
   928 
   929 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   930   Instantiates distinct Vars by terms of same type.
   931   No longer normalizes the new theorem! *)
   932 fun instantiate ([], []) th = th
   933   | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,prop}) =
   934   let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[]));
   935       val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[]));
   936       val newprop = subst_atomic tpairs
   937 	             (Type.inst_term_tvars
   938 		      (Sign.tsig_of (Sign.deref newsign_ref),vTs) prop)
   939       val newth =
   940             (Thm{sign_ref = newsign_ref, 
   941                  der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der,
   942                  maxidx = maxidx_of_term newprop, 
   943                  shyps = add_insts_sorts ((vTs, tpairs), shyps),
   944                  hyps = hyps,
   945                  prop = newprop})
   946   in  if not(instl_ok(map #1 tpairs))
   947       then raise THM("instantiate: variables not distinct", 0, [th])
   948       else if not(null(findrep(map #1 vTs)))
   949       then raise THM("instantiate: type variables not distinct", 0, [th])
   950       else nodup_vars newth "instantiate"
   951   end
   952   handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th])
   953        | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
   954 
   955 end;
   956 
   957 
   958 (*The trivial implication A==>A, justified by assume and forall rules.
   959   A can contain Vars, not so for assume!   *)
   960 fun trivial ct : thm =
   961   let val Cterm {sign_ref, t=A, T, maxidx} = ct
   962   in  if T<>propT then
   963             raise THM("trivial: the term must have type prop", 0, [])
   964       else fix_shyps [] []
   965         (Thm{sign_ref = sign_ref, 
   966              der = Pt.infer_derivs' I (false, Pt.AbsP ("H", None, Pt.PBound 0)),
   967              maxidx = maxidx, 
   968              shyps = [], 
   969              hyps = [],
   970              prop = implies$A$A})
   971   end;
   972 
   973 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
   974 fun class_triv sign c =
   975   let val Cterm {sign_ref, t, maxidx, ...} =
   976     cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
   977       handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   978   in
   979     fix_shyps [] []
   980       (Thm {sign_ref = sign_ref, 
   981             der = Pt.infer_derivs' I
   982               (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, Some [])),
   983             maxidx = maxidx, 
   984             shyps = [], 
   985             hyps = [], 
   986             prop = t})
   987   end;
   988 
   989 
   990 (* Replace all TFrees not fixed or in the hyps by new TVars *)
   991 fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
   992   let val tfrees = foldr add_term_tfree_names (hyps,fixed)
   993   in let val thm = (*no fix_shyps*)
   994     Thm{sign_ref = sign_ref, 
   995         der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
   996         maxidx = Int.max(0,maxidx), 
   997         shyps = shyps, 
   998         hyps = hyps,
   999         prop = Type.varify(prop,tfrees)}
  1000      in nodup_vars thm "varifyT" end
  1001 (* this nodup_vars check can be removed if thms are guaranteed not to contain
  1002 duplicate TVars with different sorts *)
  1003   end;
  1004 
  1005 val varifyT = varifyT' [];
  1006 
  1007 (* Replace all TVars by new TFrees *)
  1008 fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
  1009   let val (prop',_) = Type.freeze_thaw prop
  1010   in (*no fix_shyps*)
  1011     Thm{sign_ref = sign_ref, 
  1012         der = Pt.infer_derivs' (Pt.freezeT prop) der,
  1013         maxidx = maxidx_of_term prop',
  1014         shyps = shyps,
  1015         hyps = hyps,
  1016         prop = prop'}
  1017   end;
  1018 
  1019 
  1020 (*** Inference rules for tactics ***)
  1021 
  1022 (*Destruct proof state into constraints, other goals, goal(i), rest *)
  1023 fun dest_state (state as Thm{prop,...}, i) =
  1024   let val (tpairs,horn) = Logic.strip_flexpairs prop
  1025   in  case  Logic.strip_prems(i, [], horn) of
  1026           (B::rBs, C) => (tpairs, rev rBs, B, C)
  1027         | _ => raise THM("dest_state", i, [state])
  1028   end
  1029   handle TERM _ => raise THM("dest_state", i, [state]);
  1030 
  1031 (*Increment variables and parameters of orule as required for
  1032   resolution with goal i of state. *)
  1033 fun lift_rule (state, i) orule =
  1034   let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state
  1035       val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)
  1036         handle TERM _ => raise THM("lift_rule", i, [orule,state])
  1037       val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi}
  1038       val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1)
  1039       val (Thm{sign_ref, der, maxidx,shyps,hyps,prop}) = orule
  1040       val (tpairs,As,B) = Logic.strip_horn prop
  1041   in  (*no fix_shyps*)
  1042       Thm{sign_ref = merge_thm_sgs(state,orule),
  1043           der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der,
  1044           maxidx = maxidx+smax+1,
  1045           shyps=union_sort(sshyps,shyps), 
  1046           hyps=hyps, 
  1047           prop = Logic.rule_of (map (pairself lift_abs) tpairs,
  1048                                 map lift_all As,    
  1049                                 lift_all B)}
  1050   end;
  1051 
  1052 fun incr_indexes i (thm as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
  1053   if i < 0 then raise THM ("negative increment", 0, [thm]) else
  1054   if i = 0 then thm else
  1055     Thm {sign_ref = sign_ref,
  1056          der = Pt.infer_derivs' (Pt.map_proof_terms
  1057            (Logic.incr_indexes ([], i)) (incr_tvar i)) der,
  1058          maxidx = maxidx + i,
  1059          shyps = shyps,
  1060          hyps = hyps,
  1061          prop = Logic.incr_indexes ([], i) prop};
  1062 
  1063 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
  1064 fun assumption i state =
  1065   let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
  1066       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1067       fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) =
  1068         fix_shyps [state] (env_codT env)
  1069           (Thm{sign_ref = sign_ref, 
  1070                der = Pt.infer_derivs'
  1071                  ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
  1072                    Pt.assumption_proof Bs Bi n) der,
  1073                maxidx = maxidx,
  1074                shyps = [],
  1075                hyps = hyps,
  1076                prop = 
  1077                if Envir.is_empty env then (*avoid wasted normalizations*)
  1078                    Logic.rule_of (tpairs, Bs, C)
  1079                else (*normalize the new rule fully*)
  1080                    Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
  1081       fun addprfs [] _ = Seq.empty
  1082         | addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull
  1083              (Seq.mapp (newth n)
  1084                 (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
  1085                 (addprfs apairs (n+1))))
  1086   in  addprfs (Logic.assum_pairs Bi) 1 end;
  1087 
  1088 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
  1089   Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
  1090 fun eq_assumption i state =
  1091   let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
  1092       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1093   in  (case find_index (op aconv) (Logic.assum_pairs Bi) of
  1094          (~1) => raise THM("eq_assumption", 0, [state])
  1095        | n => fix_shyps [state] []
  1096                 (Thm{sign_ref = sign_ref, 
  1097                      der = Pt.infer_derivs'
  1098                        (Pt.assumption_proof Bs Bi (n+1)) der,
  1099                      maxidx = maxidx,
  1100                      shyps = [],
  1101                      hyps = hyps,
  1102                      prop = Logic.rule_of(tpairs, Bs, C)}))
  1103   end;
  1104 
  1105 
  1106 (*For rotate_tac: fast rotation of assumptions of subgoal i*)
  1107 fun rotate_rule k i state =
  1108   let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = state;
  1109       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1110       val params = Term.strip_all_vars Bi
  1111       and rest   = Term.strip_all_body Bi
  1112       val asms   = Logic.strip_imp_prems rest
  1113       and concl  = Logic.strip_imp_concl rest
  1114       val n      = length asms
  1115       val m      = if k<0 then n+k else k
  1116       val Bi'    = if 0=m orelse m=n then Bi
  1117 		   else if 0<m andalso m<n 
  1118 		   then list_all 
  1119 			   (params, 
  1120 			    Logic.list_implies(List.drop(asms, m) @ 
  1121 					       List.take(asms, m),
  1122 					       concl))
  1123 		   else raise THM("rotate_rule", k, [state])
  1124   in  (*no fix_shyps*)
  1125       Thm{sign_ref = sign_ref, 
  1126           der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
  1127 	  maxidx = maxidx,
  1128 	  shyps = shyps,
  1129 	  hyps = hyps,
  1130 	  prop = Logic.rule_of (tpairs, Bs @ [Bi'], C)}
  1131   end;
  1132 
  1133 
  1134 (*Rotates a rule's premises to the left by k, leaving the first j premises
  1135   unchanged.  Does nothing if k=0 or if k equals n-j, where n is the
  1136   number of premises.  Useful with etac and underlies tactic/defer_tac*)
  1137 fun permute_prems j k rl =
  1138   let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = rl
  1139       val prems  = Logic.strip_imp_prems prop
  1140       and concl  = Logic.strip_imp_concl prop
  1141       val moved_prems = List.drop(prems, j)
  1142       and fixed_prems = List.take(prems, j)
  1143         handle Subscript => raise THM("permute_prems:j", j, [rl])
  1144       val n_j    = length moved_prems
  1145       val m = if k<0 then n_j + k else k
  1146       val prop'  = if 0 = m orelse m = n_j then prop
  1147 		   else if 0<m andalso m<n_j 
  1148 		   then Logic.list_implies(fixed_prems @
  1149 					   List.drop(moved_prems, m) @ 
  1150 					   List.take(moved_prems, m),
  1151 					   concl)
  1152 		   else raise THM("permute_prems:k", k, [rl])
  1153   in  (*no fix_shyps*)
  1154       Thm{sign_ref = sign_ref, 
  1155           der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
  1156 	  maxidx = maxidx,
  1157 	  shyps = shyps,
  1158 	  hyps = hyps,
  1159 	  prop = prop'}
  1160   end;
  1161 
  1162 
  1163 (** User renaming of parameters in a subgoal **)
  1164 
  1165 (*Calls error rather than raising an exception because it is intended
  1166   for top-level use -- exception handling would not make sense here.
  1167   The names in cs, if distinct, are used for the innermost parameters;
  1168    preceding parameters may be renamed to make all params distinct.*)
  1169 fun rename_params_rule (cs, i) state =
  1170   let val Thm{sign_ref,der,maxidx,hyps,...} = state
  1171       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1172       val iparams = map #1 (Logic.strip_params Bi)
  1173       val short = length iparams - length cs
  1174       val newnames =
  1175             if short<0 then error"More names than abstractions!"
  1176             else variantlist(take (short,iparams), cs) @ cs
  1177       val freenames = map (#1 o dest_Free) (term_frees Bi)
  1178       val newBi = Logic.list_rename_params (newnames, Bi)
  1179   in
  1180   case findrep cs of
  1181      c::_ => (warning ("Can't rename.  Bound variables not distinct: " ^ c); 
  1182 	      state)
  1183    | [] => (case cs inter_string freenames of
  1184        a::_ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); 
  1185 		state)
  1186      | [] => fix_shyps [state] []
  1187                 (Thm{sign_ref = sign_ref,
  1188                      der = der,
  1189                      maxidx = maxidx,
  1190                      shyps = [],
  1191                      hyps = hyps,
  1192                      prop = Logic.rule_of(tpairs, Bs@[newBi], C)}))
  1193   end;
  1194 
  1195 (*** Preservation of bound variable names ***)
  1196 
  1197 (*Scan a pair of terms; while they are similar,
  1198   accumulate corresponding bound vars in "al"*)
  1199 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
  1200       match_bvs(s, t, if x="" orelse y="" then al
  1201                                           else (x,y)::al)
  1202   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
  1203   | match_bvs(_,_,al) = al;
  1204 
  1205 (* strip abstractions created by parameters *)
  1206 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
  1207 
  1208 fun rename_boundvars pat obj (thm as Thm {sign_ref,der,maxidx,hyps,shyps,prop}) =
  1209   let val ren = match_bvs (pat, obj, [])
  1210       fun renAbs (Abs (x, T, b)) =
  1211             Abs (if_none (assoc_string (ren, x)) x, T, renAbs b)
  1212         | renAbs (f $ t) = renAbs f $ renAbs t
  1213         | renAbs t = t
  1214   in if null ren then thm else Thm
  1215     {sign_ref = sign_ref,
  1216      der = der,
  1217      maxidx = maxidx,
  1218      hyps = hyps,
  1219      shyps = shyps,
  1220      prop = renAbs prop}
  1221   end;
  1222 
  1223 
  1224 (* strip_apply f A(,B) strips off all assumptions/parameters from A
  1225    introduced by lifting over B, and applies f to remaining part of A*)
  1226 fun strip_apply f =
  1227   let fun strip(Const("==>",_)$ A1 $ B1,
  1228                 Const("==>",_)$ _  $ B2) = implies $ A1 $ strip(B1,B2)
  1229         | strip((c as Const("all",_)) $ Abs(a,T,t1),
  1230                       Const("all",_)  $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))
  1231         | strip(A,_) = f A
  1232   in strip end;
  1233 
  1234 (*Use the alist to rename all bound variables and some unknowns in a term
  1235   dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
  1236   Preserves unknowns in tpairs and on lhs of dpairs. *)
  1237 fun rename_bvs([],_,_,_) = I
  1238   | rename_bvs(al,dpairs,tpairs,B) =
  1239     let val vars = foldr add_term_vars
  1240                         (map fst dpairs @ map fst tpairs @ map snd tpairs, [])
  1241         (*unknowns appearing elsewhere be preserved!*)
  1242         val vids = map (#1 o #1 o dest_Var) vars;
  1243         fun rename(t as Var((x,i),T)) =
  1244                 (case assoc(al,x) of
  1245                    Some(y) => if x mem_string vids orelse y mem_string vids then t
  1246                               else Var((y,i),T)
  1247                  | None=> t)
  1248           | rename(Abs(x,T,t)) =
  1249               Abs(if_none(assoc_string(al,x)) x, T, rename t)
  1250           | rename(f$t) = rename f $ rename t
  1251           | rename(t) = t;
  1252         fun strip_ren Ai = strip_apply rename (Ai,B)
  1253     in strip_ren end;
  1254 
  1255 (*Function to rename bounds/unknowns in the argument, lifted over B*)
  1256 fun rename_bvars(dpairs, tpairs, B) =
  1257         rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B);
  1258 
  1259 
  1260 (*** RESOLUTION ***)
  1261 
  1262 (** Lifting optimizations **)
  1263 
  1264 (*strip off pairs of assumptions/parameters in parallel -- they are
  1265   identical because of lifting*)
  1266 fun strip_assums2 (Const("==>", _) $ _ $ B1,
  1267                    Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
  1268   | strip_assums2 (Const("all",_)$Abs(a,T,t1),
  1269                    Const("all",_)$Abs(_,_,t2)) =
  1270       let val (B1,B2) = strip_assums2 (t1,t2)
  1271       in  (Abs(a,T,B1), Abs(a,T,B2))  end
  1272   | strip_assums2 BB = BB;
  1273 
  1274 
  1275 (*Faster normalization: skip assumptions that were lifted over*)
  1276 fun norm_term_skip env 0 t = Envir.norm_term env t
  1277   | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
  1278         let val Envir.Envir{iTs, ...} = env
  1279             val T' = typ_subst_TVars_Vartab iTs T
  1280             (*Must instantiate types of parameters because they are flattened;
  1281               this could be a NEW parameter*)
  1282         in  all T' $ Abs(a, T', norm_term_skip env n t)  end
  1283   | norm_term_skip env n (Const("==>", _) $ A $ B) =
  1284         implies $ A $ norm_term_skip env (n-1) B
  1285   | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
  1286 
  1287 
  1288 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
  1289   Unifies B with Bi, replacing subgoal i    (1 <= i <= n)
  1290   If match then forbid instantiations in proof state
  1291   If lifted then shorten the dpair using strip_assums2.
  1292   If eres_flg then simultaneously proves A1 by assumption.
  1293   nsubgoal is the number of new subgoals (written m above).
  1294   Curried so that resolution calls dest_state only once.
  1295 *)
  1296 local exception COMPOSE
  1297 in
  1298 fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
  1299                         (eres_flg, orule, nsubgoal) =
  1300  let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state
  1301      and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 
  1302              prop=rprop,...} = orule
  1303          (*How many hyps to skip over during normalization*)
  1304      and nlift = Logic.count_prems(strip_all_body Bi,
  1305                                    if eres_flg then ~1 else 0)
  1306      val sign_ref = merge_thm_sgs(state,orule);
  1307      val sign = Sign.deref sign_ref;
  1308      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
  1309      fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
  1310        let val normt = Envir.norm_term env;
  1311            (*perform minimal copying here by examining env*)
  1312            val normp =
  1313              if Envir.is_empty env then (tpairs, Bs @ As, C)
  1314              else
  1315              let val ntps = map (pairself normt) tpairs
  1316              in if Envir.above (smax, env) then
  1317                   (*no assignments in state; normalize the rule only*)
  1318                   if lifted
  1319                   then (ntps, Bs @ map (norm_term_skip env nlift) As, C)
  1320                   else (ntps, Bs @ map normt As, C)
  1321                 else if match then raise COMPOSE
  1322                 else (*normalize the new rule fully*)
  1323                   (ntps, map normt (Bs @ As), normt C)
  1324              end
  1325            val th = (*tuned fix_shyps*)
  1326              Thm{sign_ref = sign_ref,
  1327                  der = Pt.infer_derivs
  1328                    ((if Envir.is_empty env then I
  1329                      else if Envir.above (smax, env) then
  1330                        (fn f => fn der => f (Pt.norm_proof' env der))
  1331                      else
  1332                        curry op oo (Pt.norm_proof' env))
  1333                     (Pt.bicompose_proof Bs oldAs As A n)) rder' sder,
  1334                  maxidx = maxidx,
  1335                  shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
  1336                  hyps = union_term(rhyps,shyps),
  1337                  prop = Logic.rule_of normp}
  1338         in  Seq.cons(th, thq)  end  handle COMPOSE => thq;
  1339      val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
  1340      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
  1341        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
  1342      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
  1343      fun newAs(As0, n, dpairs, tpairs) =
  1344        let val (As1, rder') =
  1345          if !Logic.auto_rename orelse not lifted then (As0, rder)
  1346          else (map (rename_bvars(dpairs,tpairs,B)) As0,
  1347            Pt.infer_derivs' (Pt.map_proof_terms
  1348              (rename_bvars (dpairs, tpairs, Bound 0)) I) rder);
  1349        in (map (Logic.flatten_params n) As1, As1, rder', n)
  1350           handle TERM _ =>
  1351           raise THM("bicompose: 1st premise", 0, [orule])
  1352        end;
  1353      val env = Envir.empty(Int.max(rmax,smax));
  1354      val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
  1355      val dpairs = BBi :: (rtpairs@stpairs);
  1356      (*elim-resolution: try each assumption in turn.  Initially n=1*)
  1357      fun tryasms (_, _, _, []) = Seq.empty
  1358        | tryasms (A, As, n, (t,u)::apairs) =
  1359           (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
  1360                None                   => tryasms (A, As, n+1, apairs)
  1361              | cell as Some((_,tpairs),_) =>
  1362                    Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
  1363                        (Seq.make (fn()=> cell),
  1364                         Seq.make (fn()=> Seq.pull (tryasms (A, As, n+1, apairs)))));
  1365      fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
  1366        | eres (A1::As) = tryasms (Some A1, As, 1, Logic.assum_pairs A1);
  1367      (*ordinary resolution*)
  1368      fun res(None) = Seq.empty
  1369        | res(cell as Some((_,tpairs),_)) =
  1370              Seq.it_right (addth None (newAs(rev rAs, 0, [BBi], tpairs)))
  1371                        (Seq.make (fn()=> cell), Seq.empty)
  1372  in  if eres_flg then eres(rev rAs)
  1373      else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
  1374  end;
  1375 end;
  1376 
  1377 
  1378 fun bicompose match arg i state =
  1379     bicompose_aux match (state, dest_state(state,i), false) arg;
  1380 
  1381 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
  1382   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
  1383 fun could_bires (Hs, B, eres_flg, rule) =
  1384     let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs
  1385           | could_reshyp [] = false;  (*no premise -- illegal*)
  1386     in  could_unify(concl_of rule, B) andalso
  1387         (not eres_flg  orelse  could_reshyp (prems_of rule))
  1388     end;
  1389 
  1390 (*Bi-resolution of a state with a list of (flag,rule) pairs.
  1391   Puts the rule above:  rule/state.  Renames vars in the rules. *)
  1392 fun biresolution match brules i state =
  1393     let val lift = lift_rule(state, i);
  1394         val (stpairs, Bs, Bi, C) = dest_state(state,i)
  1395         val B = Logic.strip_assums_concl Bi;
  1396         val Hs = Logic.strip_assums_hyp Bi;
  1397         val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
  1398         fun res [] = Seq.empty
  1399           | res ((eres_flg, rule)::brules) =
  1400               if could_bires (Hs, B, eres_flg, rule)
  1401               then Seq.make (*delay processing remainder till needed*)
  1402                   (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
  1403                                res brules))
  1404               else res brules
  1405     in  Seq.flat (res brules)  end;
  1406 
  1407 
  1408 (*** Oracles ***)
  1409 
  1410 fun invoke_oracle thy raw_name =
  1411   let
  1412     val {sign = sg, oracles, ...} = Theory.rep_theory thy;
  1413     val name = Sign.intern sg Theory.oracleK raw_name;
  1414     val oracle =
  1415       (case Symtab.lookup (oracles, name) of
  1416         None => raise THM ("Unknown oracle: " ^ name, 0, [])
  1417       | Some (f, _) => f);
  1418   in
  1419     fn (sign, exn) =>
  1420       let
  1421         val sign_ref' = Sign.merge_refs (Sign.self_ref sg, Sign.self_ref sign);
  1422         val sign' = Sign.deref sign_ref';
  1423         val (prop, T, maxidx) = Sign.certify_term sign' (oracle (sign', exn));
  1424       in
  1425         if T <> propT then
  1426           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
  1427         else fix_shyps [] []
  1428           (Thm {sign_ref = sign_ref', 
  1429             der = (true, Pt.oracle_proof name prop),
  1430             maxidx = maxidx,
  1431             shyps = [], 
  1432             hyps = [], 
  1433             prop = prop})
  1434       end
  1435   end;
  1436 
  1437 
  1438 end;
  1439 
  1440 
  1441 structure BasicThm: BASIC_THM = Thm;
  1442 open BasicThm;