src/Pure/drule.ML
author nipkow
Tue Mar 14 10:40:04 1995 +0100 (1995-03-14)
changeset 952 9e10962866b0
parent 949 83c588d6fee9
child 1194 563ecd14c1d8
permissions -rw-r--r--
Removed an old bug which made some simultaneous instantiations fail if they
were given in the "wrong" order.

Rewrote sign/infer_types.

Fixed some comments.
     1 (*  Title:      Pure/drule.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Derived rules and other operations on theorems and theories
     7 *)
     8 
     9 infix 0 RS RSN RL RLN MRS MRL COMP;
    10 
    11 signature DRULE =
    12   sig
    13   structure Thm : THM
    14   local open Thm  in
    15   val add_defs		: (string * string) list -> theory -> theory
    16   val add_defs_i	: (string * term) list -> theory -> theory
    17   val asm_rl		: thm
    18   val assume_ax		: theory -> string -> thm
    19   val COMP		: thm * thm -> thm
    20   val compose		: thm * int * thm -> thm list
    21   val cprems_of		: thm -> cterm list
    22   val cskip_flexpairs	: cterm -> cterm
    23   val cstrip_imp_prems	: cterm -> cterm list
    24   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    25   val cut_rl		: thm
    26   val equal_abs_elim	: cterm  -> thm -> thm
    27   val equal_abs_elim_list: cterm list -> thm -> thm
    28   val eq_thm		: thm * thm -> bool
    29   val eq_thm_sg		: thm * thm -> bool
    30   val flexpair_abs_elim_list: cterm list -> thm -> thm
    31   val forall_intr_list	: cterm list -> thm -> thm
    32   val forall_intr_frees	: thm -> thm
    33   val forall_elim_list	: cterm list -> thm -> thm
    34   val forall_elim_var	: int -> thm -> thm
    35   val forall_elim_vars	: int -> thm -> thm
    36   val implies_elim_list	: thm -> thm list -> thm
    37   val implies_intr_list	: cterm list -> thm -> thm
    38   val MRL		: thm list list * thm list -> thm list
    39   val MRS		: thm list * thm -> thm
    40   val pprint_cterm	: cterm -> pprint_args -> unit
    41   val pprint_ctyp	: ctyp -> pprint_args -> unit
    42   val pprint_theory	: theory -> pprint_args -> unit
    43   val pprint_thm	: thm -> pprint_args -> unit
    44   val pretty_thm	: thm -> Sign.Syntax.Pretty.T
    45   val print_cterm	: cterm -> unit
    46   val print_ctyp	: ctyp -> unit
    47   val print_goals	: int -> thm -> unit
    48   val print_goals_ref	: (int -> thm -> unit) ref
    49   val print_syntax	: theory -> unit
    50   val print_theory	: theory -> unit
    51   val print_thm		: thm -> unit
    52   val prth		: thm -> thm
    53   val prthq		: thm Sequence.seq -> thm Sequence.seq
    54   val prths		: thm list -> thm list
    55   val read_instantiate	: (string*string)list -> thm -> thm
    56   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    57   val read_insts	:
    58           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    59                   -> (indexname -> typ option) * (indexname -> sort option)
    60                   -> string list -> (string*string)list
    61                   -> (indexname*ctyp)list * (cterm*cterm)list
    62   val reflexive_thm	: thm
    63   val revcut_rl		: thm
    64   val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
    65         -> meta_simpset -> int -> thm -> thm
    66   val rewrite_goals_rule: thm list -> thm -> thm
    67   val rewrite_rule	: thm list -> thm -> thm
    68   val RS		: thm * thm -> thm
    69   val RSN		: thm * (int * thm) -> thm
    70   val RL		: thm list * thm list -> thm list
    71   val RLN		: thm list * (int * thm list) -> thm list
    72   val show_hyps		: bool ref
    73   val size_of_thm	: thm -> int
    74   val standard		: thm -> thm
    75   val string_of_cterm	: cterm -> string
    76   val string_of_ctyp	: ctyp -> string
    77   val string_of_thm	: thm -> string
    78   val symmetric_thm	: thm
    79   val thin_rl		: thm
    80   val transitive_thm	: thm
    81   val triv_forall_equality: thm
    82   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    83   val zero_var_indexes	: thm -> thm
    84   end
    85   end;
    86 
    87 
    88 functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE =
    89 struct
    90 structure Thm = Thm;
    91 structure Sign = Thm.Sign;
    92 structure Type = Sign.Type;
    93 structure Syntax = Sign.Syntax;
    94 structure Pretty = Syntax.Pretty
    95 structure Symtab = Sign.Symtab;
    96 
    97 local open Thm
    98 in
    99 
   100 (**** Extend Theories ****)
   101 
   102 (** add constant definitions **)
   103 
   104 (* all_axioms_of *)
   105 
   106 (*results may contain duplicates!*)
   107 
   108 fun ancestry_of thy =
   109   thy :: flat (map ancestry_of (parents_of thy));
   110 
   111 val all_axioms_of = 
   112   flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
   113 
   114 
   115 (* clash_types, clash_consts *)
   116 
   117 (*check if types have common instance (ignoring sorts)*)
   118 
   119 fun clash_types ty1 ty2 =
   120   let
   121     val ty1' = Type.varifyT ty1;
   122     val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
   123   in
   124     Type.raw_unify (ty1', ty2')
   125   end;
   126 
   127 fun clash_consts (c1, ty1) (c2, ty2) =
   128   c1 = c2 andalso clash_types ty1 ty2;
   129 
   130 
   131 (* clash_defns *)
   132 
   133 fun clash_defn c_ty (name, tm) =
   134   let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in
   135     if clash_consts c_ty (c, ty') then Some (name, ty') else None
   136   end handle TERM _ => None;
   137 
   138 fun clash_defns c_ty axms =
   139   distinct (mapfilter (clash_defn c_ty) axms);
   140 
   141 
   142 (* dest_defn *)
   143 
   144 fun dest_defn tm =
   145   let
   146     fun err msg = raise_term msg [tm];
   147 
   148     val (lhs, rhs) = Logic.dest_equals tm
   149       handle TERM _ => err "Not a meta-equality (==)";
   150     val (head, args) = strip_comb lhs;
   151     val (c, ty) = dest_Const head
   152       handle TERM _ => err "Head of lhs not a constant";
   153 
   154     fun occs_const (Const c_ty') = (c_ty' = (c, ty))
   155       | occs_const (Abs (_, _, t)) = occs_const t
   156       | occs_const (t $ u) = occs_const t orelse occs_const u
   157       | occs_const _ = false;
   158 
   159     val show_frees = commas_quote o map (fst o dest_Free);
   160     val show_tfrees = commas_quote o map fst;
   161 
   162     val lhs_dups = duplicates args;
   163     val rhs_extras = gen_rems (op =) (term_frees rhs, args);
   164     val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
   165   in
   166     if not (forall is_Free args) then
   167       err "Arguments of lhs have to be variables"
   168     else if not (null lhs_dups) then
   169       err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
   170     else if not (null rhs_extras) then
   171       err ("Extra variables on rhs: " ^ show_frees rhs_extras)
   172     else if not (null rhs_extrasT) then
   173       err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
   174     else if occs_const rhs then
   175       err ("Constant to be defined occurs on rhs")
   176     else (c, ty)
   177   end;
   178 
   179 
   180 (* check_defn *)
   181 
   182 fun err_in_defn name msg =
   183   (writeln msg; error ("The error(s) above occurred in definition " ^ quote name));
   184 
   185 fun check_defn sign (axms, (name, tm)) =
   186   let
   187     fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block
   188       [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty]));
   189 
   190     fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn;
   191     fun show_defns c = commas o map (show_defn c);
   192 
   193     val (c, ty) = dest_defn tm
   194       handle TERM (msg, _) => err_in_defn name msg;
   195     val defns = clash_defns (c, ty) axms;
   196   in
   197     if not (null defns) then
   198       err_in_defn name ("Definition of " ^ show_const (c, ty) ^
   199         " clashes with " ^ show_defns c defns)
   200     else (name, tm) :: axms
   201   end;
   202 
   203 
   204 (* add_defs *)
   205 
   206 fun ext_defns prep_axm raw_axms thy =
   207   let
   208     val axms = map (prep_axm (sign_of thy)) raw_axms;
   209     val all_axms = all_axioms_of thy;
   210   in
   211     foldl (check_defn (sign_of thy)) (all_axms, axms);
   212     add_axioms_i axms thy
   213   end;
   214 
   215 val add_defs_i = ext_defns cert_axm;
   216 val add_defs = ext_defns read_axm;
   217 
   218 
   219 
   220 (**** More derived rules and operations on theorems ****)
   221 
   222 (** some cterm->cterm operations: much faster than calling cterm_of! **)
   223 
   224 (*Discard flexflex pairs; return a cterm*)
   225 fun cskip_flexpairs ct =
   226     case term_of ct of
   227 	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
   228 	    cskip_flexpairs (#2 (dest_cimplies ct))
   229       | _ => ct;
   230 
   231 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   232 fun cstrip_imp_prems ct =
   233     let val (cA,cB) = dest_cimplies ct
   234     in  cA :: cstrip_imp_prems cB  end
   235     handle TERM _ => [];
   236 
   237 (*The premises of a theorem, as a cterm list*)
   238 val cprems_of = cstrip_imp_prems o cskip_flexpairs o cprop_of;
   239 
   240 
   241 (** reading of instantiations **)
   242 
   243 fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
   244         | _ => error("Lexical error in variable name " ^ quote (implode cs));
   245 
   246 fun absent ixn =
   247   error("No such variable in term: " ^ Syntax.string_of_vname ixn);
   248 
   249 fun inst_failure ixn =
   250   error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
   251 
   252 (* this code is a bit of a mess. add_cterm could be simplified greatly if
   253    simultaneous instantiations were read or at least type checked
   254    simultaneously rather than one after the other. This would make the tricky
   255    composition of implicit type instantiations (parameter tye) superfluous.
   256 *)
   257 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
   258 let val {tsig,...} = Sign.rep_sg sign
   259     fun split([],tvs,vs) = (tvs,vs)
   260       | split((sv,st)::l,tvs,vs) = (case explode sv of
   261                   "'"::cs => split(l,(indexname cs,st)::tvs,vs)
   262                 | cs => split(l,tvs,(indexname cs,st)::vs));
   263     val (tvs,vs) = split(insts,[],[]);
   264     fun readT((a,i),st) =
   265         let val ixn = ("'" ^ a,i);
   266             val S = case rsorts ixn of Some S => S | None => absent ixn;
   267             val T = Sign.read_typ (sign,sorts) st;
   268         in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   269            else inst_failure ixn
   270         end
   271     val tye = map readT tvs;
   272     fun add_cterm ((cts,tye,used), (ixn,st)) =
   273         let val T = case rtypes ixn of
   274                       Some T => typ_subst_TVars tye T
   275                     | None => absent ixn;
   276             val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T);
   277             val cts' = (ixn,T,ct)::cts
   278             fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct)
   279             val used' = add_term_tvarnames(term_of ct,used);
   280         in (map inst cts',tye2 @ tye,used') end
   281     val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs);
   282 in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
   283     map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms)
   284 end;
   285 
   286 
   287 
   288 (*** Printing of theories, theorems, etc. ***)
   289 
   290 (*If false, hypotheses are printed as dots*)
   291 val show_hyps = ref true;
   292 
   293 fun pretty_thm th =
   294 let val {sign, hyps, prop,...} = rep_thm th
   295     val hsymbs = if null hyps then []
   296                  else if !show_hyps then
   297                       [Pretty.brk 2,
   298                        Pretty.lst("[","]") (map (Sign.pretty_term sign) hyps)]
   299                  else Pretty.str" [" :: map (fn _ => Pretty.str".") hyps @
   300                       [Pretty.str"]"];
   301 in Pretty.blk(0, Sign.pretty_term sign prop :: hsymbs) end;
   302 
   303 val string_of_thm = Pretty.string_of o pretty_thm;
   304 
   305 val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
   306 
   307 
   308 (** Top-level commands for printing theorems **)
   309 val print_thm = writeln o string_of_thm;
   310 
   311 fun prth th = (print_thm th; th);
   312 
   313 (*Print and return a sequence of theorems, separated by blank lines. *)
   314 fun prthq thseq =
   315   (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq);
   316 
   317 (*Print and return a list of theorems, separated by blank lines. *)
   318 fun prths ths = (print_list_ln print_thm ths; ths);
   319 
   320 
   321 (* other printing commands *)
   322 
   323 fun pprint_ctyp cT =
   324   let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end;
   325 
   326 fun string_of_ctyp cT =
   327   let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end;
   328 
   329 val print_ctyp = writeln o string_of_ctyp;
   330 
   331 fun pprint_cterm ct =
   332   let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end;
   333 
   334 fun string_of_cterm ct =
   335   let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end;
   336 
   337 val print_cterm = writeln o string_of_cterm;
   338 
   339 
   340 (* print theory *)
   341 
   342 val pprint_theory = Sign.pprint_sg o sign_of;
   343 
   344 val print_syntax = Syntax.print_syntax o syn_of;
   345 
   346 fun print_axioms thy =
   347   let
   348     val {sign, new_axioms, ...} = rep_theory thy;
   349     val axioms = Symtab.dest new_axioms;
   350 
   351     fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
   352       Pretty.quote (Sign.pretty_term sign t)];
   353   in
   354     Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms))
   355   end;
   356 
   357 fun print_theory thy = (Sign.print_sg (sign_of thy); print_axioms thy);
   358 
   359 
   360 
   361 (** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **)
   362 
   363 (* get type_env, sort_env of term *)
   364 
   365 local
   366   open Syntax;
   367 
   368   fun ins_entry (x, y) [] = [(x, [y])]
   369     | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
   370         if x = x' then (x', y ins ys') :: pairs
   371         else pair :: ins_entry (x, y) pairs;
   372 
   373   fun add_type_env (Free (x, T), env) = ins_entry (T, x) env
   374     | add_type_env (Var (xi, T), env) = ins_entry (T, string_of_vname xi) env
   375     | add_type_env (Abs (_, _, t), env) = add_type_env (t, env)
   376     | add_type_env (t $ u, env) = add_type_env (u, add_type_env (t, env))
   377     | add_type_env (_, env) = env;
   378 
   379   fun add_sort_env (Type (_, Ts), env) = foldr add_sort_env (Ts, env)
   380     | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env
   381     | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env;
   382 
   383   val sort = map (apsnd sort_strings);
   384 in
   385   fun type_env t = sort (add_type_env (t, []));
   386   fun sort_env t = rev (sort (it_term_types add_sort_env (t, [])));
   387 end;
   388 
   389 
   390 (* print_goals *)
   391 
   392 fun print_goals maxgoals state =
   393   let
   394     open Syntax;
   395 
   396     val {sign, prop, ...} = rep_thm state;
   397 
   398     val pretty_term = Sign.pretty_term sign;
   399     val pretty_typ = Sign.pretty_typ sign;
   400     val pretty_sort = Sign.pretty_sort;
   401 
   402     fun pretty_vars prtf (X, vs) = Pretty.block
   403       [Pretty.block (Pretty.commas (map Pretty.str vs)),
   404         Pretty.str " ::", Pretty.brk 1, prtf X];
   405 
   406     fun print_list _ _ [] = ()
   407       | print_list name prtf lst =
   408           (writeln ""; Pretty.writeln (Pretty.big_list name (map prtf lst)));
   409 
   410 
   411     fun print_goals (_, []) = ()
   412       | print_goals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
   413           [Pretty.str (" " ^ string_of_int n ^ ". "), pretty_term A]));
   414             print_goals (n + 1, As));
   415 
   416     val print_ffpairs =
   417       print_list "Flex-flex pairs:" (pretty_term o Logic.mk_flexpair);
   418 
   419     val print_types = print_list "Types:" (pretty_vars pretty_typ) o type_env;
   420     val print_sorts = print_list "Sorts:" (pretty_vars pretty_sort) o sort_env;
   421 
   422 
   423     val (tpairs, As, B) = Logic.strip_horn prop;
   424     val ngoals = length As;
   425 
   426     val orig_no_freeTs = ! show_no_free_types;
   427     val orig_sorts = ! show_sorts;
   428 
   429     fun restore () =
   430       (show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts);
   431   in
   432     (show_no_free_types := true; show_sorts := false;
   433       Pretty.writeln (pretty_term B);
   434       if ngoals = 0 then writeln "No subgoals!"
   435       else if ngoals > maxgoals then
   436         (print_goals (1, take (maxgoals, As));
   437           writeln ("A total of " ^ string_of_int ngoals ^ " subgoals..."))
   438       else print_goals (1, As);
   439 
   440       print_ffpairs tpairs;
   441 
   442       if orig_sorts then
   443         (print_types prop; print_sorts prop)
   444       else if ! show_types then
   445         print_types prop
   446       else ())
   447     handle exn => (restore (); raise exn);
   448     restore ()
   449   end;
   450 
   451 
   452 (*"hook" for user interfaces: allows print_goals to be replaced*)
   453 val print_goals_ref = ref print_goals;
   454 
   455 (*** Find the type (sort) associated with a (T)Var or (T)Free in a term
   456      Used for establishing default types (of variables) and sorts (of
   457      type variables) when reading another term.
   458      Index -1 indicates that a (T)Free rather than a (T)Var is wanted.
   459 ***)
   460 
   461 fun types_sorts thm =
   462     let val {prop,hyps,...} = rep_thm thm;
   463         val big = list_comb(prop,hyps); (* bogus term! *)
   464         val vars = map dest_Var (term_vars big);
   465         val frees = map dest_Free (term_frees big);
   466         val tvars = term_tvars big;
   467         val tfrees = term_tfrees big;
   468         fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i));
   469         fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
   470     in (typ,sort) end;
   471 
   472 (** Standardization of rules **)
   473 
   474 (*Generalization over a list of variables, IGNORING bad ones*)
   475 fun forall_intr_list [] th = th
   476   | forall_intr_list (y::ys) th =
   477         let val gth = forall_intr_list ys th
   478         in  forall_intr y gth   handle THM _ =>  gth  end;
   479 
   480 (*Generalization over all suitable Free variables*)
   481 fun forall_intr_frees th =
   482     let val {prop,sign,...} = rep_thm th
   483     in  forall_intr_list
   484          (map (cterm_of sign) (sort atless (term_frees prop)))
   485          th
   486     end;
   487 
   488 (*Replace outermost quantified variable by Var of given index.
   489     Could clash with Vars already present.*)
   490 fun forall_elim_var i th =
   491     let val {prop,sign,...} = rep_thm th
   492     in case prop of
   493           Const("all",_) $ Abs(a,T,_) =>
   494               forall_elim (cterm_of sign (Var((a,i), T)))  th
   495         | _ => raise THM("forall_elim_var", i, [th])
   496     end;
   497 
   498 (*Repeat forall_elim_var until all outer quantifiers are removed*)
   499 fun forall_elim_vars i th =
   500     forall_elim_vars i (forall_elim_var i th)
   501         handle THM _ => th;
   502 
   503 (*Specialization over a list of cterms*)
   504 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
   505 
   506 (* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
   507 fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
   508 
   509 (* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
   510 fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths);
   511 
   512 (*Reset Var indexes to zero, renaming to preserve distinctness*)
   513 fun zero_var_indexes th =
   514     let val {prop,sign,...} = rep_thm th;
   515         val vars = term_vars prop
   516         val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars)
   517         val inrs = add_term_tvars(prop,[]);
   518         val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
   519         val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms')
   520         val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
   521         fun varpairs([],[]) = []
   522           | varpairs((var as Var(v,T)) :: vars, b::bs) =
   523                 let val T' = typ_subst_TVars tye T
   524                 in (cterm_of sign (Var(v,T')),
   525                     cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
   526                 end
   527           | varpairs _ = raise TERM("varpairs", []);
   528     in instantiate (ctye, varpairs(vars,rev bs)) th end;
   529 
   530 
   531 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
   532     all generality expressed by Vars having index 0.*)
   533 fun standard th =
   534     let val {maxidx,...} = rep_thm th
   535     in  varifyT (zero_var_indexes (forall_elim_vars(maxidx+1)
   536                          (forall_intr_frees(implies_intr_hyps th))))
   537     end;
   538 
   539 (*Assume a new formula, read following the same conventions as axioms.
   540   Generalizes over Free variables,
   541   creates the assumption, and then strips quantifiers.
   542   Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
   543              [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
   544 fun assume_ax thy sP =
   545     let val sign = sign_of thy
   546         val prop = Logic.close_form (term_of (read_cterm sign
   547                          (sP, propT)))
   548     in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
   549 
   550 (*Resolution: exactly one resolvent must be produced.*)
   551 fun tha RSN (i,thb) =
   552   case Sequence.chop (2, biresolution false [(false,tha)] i thb) of
   553       ([th],_) => th
   554     | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
   555     |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
   556 
   557 (*resolution: P==>Q, Q==>R gives P==>R. *)
   558 fun tha RS thb = tha RSN (1,thb);
   559 
   560 (*For joining lists of rules*)
   561 fun thas RLN (i,thbs) =
   562   let val resolve = biresolution false (map (pair false) thas) i
   563       fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
   564   in  flat (map resb thbs)  end;
   565 
   566 fun thas RL thbs = thas RLN (1,thbs);
   567 
   568 (*Resolve a list of rules against bottom_rl from right to left;
   569   makes proof trees*)
   570 fun rls MRS bottom_rl =
   571   let fun rs_aux i [] = bottom_rl
   572         | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
   573   in  rs_aux 1 rls  end;
   574 
   575 (*As above, but for rule lists*)
   576 fun rlss MRL bottom_rls =
   577   let fun rs_aux i [] = bottom_rls
   578         | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
   579   in  rs_aux 1 rlss  end;
   580 
   581 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
   582   with no lifting or renaming!  Q may contain ==> or meta-quants
   583   ALWAYS deletes premise i *)
   584 fun compose(tha,i,thb) =
   585     Sequence.list_of_s (bicompose false (false,tha,0) i thb);
   586 
   587 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
   588 fun tha COMP thb =
   589     case compose(tha,1,thb) of
   590         [th] => th
   591       | _ =>   raise THM("COMP", 1, [tha,thb]);
   592 
   593 (*Instantiate theorem th, reading instantiations under signature sg*)
   594 fun read_instantiate_sg sg sinsts th =
   595     let val ts = types_sorts th;
   596         val used = add_term_tvarnames(#prop(rep_thm th),[]);
   597     in  instantiate (read_insts sg ts ts used sinsts) th  end;
   598 
   599 (*Instantiate theorem th, reading instantiations under theory of th*)
   600 fun read_instantiate sinsts th =
   601     read_instantiate_sg (#sign (rep_thm th)) sinsts th;
   602 
   603 
   604 (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   605   Instantiates distinct Vars by terms, inferring type instantiations. *)
   606 local
   607   fun add_types ((ct,cu), (sign,tye)) =
   608     let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
   609         and {sign=signu, t=u, T= U, ...} = rep_cterm cu
   610         val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   611         val tye' = Type.unify (#tsig(Sign.rep_sg sign')) ((T,U), tye)
   612           handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
   613     in  (sign', tye')  end;
   614 in
   615 fun cterm_instantiate ctpairs0 th =
   616   let val (sign,tye) = foldr add_types (ctpairs0, (#sign(rep_thm th),[]))
   617       val tsig = #tsig(Sign.rep_sg sign);
   618       fun instT(ct,cu) = let val inst = subst_TVars tye
   619                          in (cterm_fun inst ct, cterm_fun inst cu) end
   620       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   621   in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
   622   handle TERM _ =>
   623            raise THM("cterm_instantiate: incompatible signatures",0,[th])
   624        | TYPE _ => raise THM("cterm_instantiate: types", 0, [th])
   625 end;
   626 
   627 
   628 (** theorem equality test is exported and used by BEST_FIRST **)
   629 
   630 (*equality of theorems uses equality of signatures and
   631   the a-convertible test for terms*)
   632 fun eq_thm (th1,th2) =
   633     let val {sign=sg1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
   634         and {sign=sg2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
   635     in  Sign.eq_sg (sg1,sg2) andalso
   636         aconvs(hyps1,hyps2) andalso
   637         prop1 aconv prop2
   638     end;
   639 
   640 (*Do the two theorems have the same signature?*)
   641 fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
   642 
   643 (*Useful "distance" function for BEST_FIRST*)
   644 val size_of_thm = size_of_term o #prop o rep_thm;
   645 
   646 
   647 (*** Meta-Rewriting Rules ***)
   648 
   649 
   650 val reflexive_thm =
   651   let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
   652   in Thm.reflexive cx end;
   653 
   654 val symmetric_thm =
   655   let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
   656   in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
   657 
   658 val transitive_thm =
   659   let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
   660       val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
   661       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   662   in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   663 
   664 (** Below, a "conversion" has type cterm -> thm **)
   665 
   666 val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies);
   667 
   668 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   669 (*Do not rewrite flex-flex pairs*)
   670 fun goals_conv pred cv =
   671   let fun gconv i ct =
   672         let val (A,B) = Thm.dest_cimplies ct
   673             val (thA,j) = case term_of A of
   674                   Const("=?=",_)$_$_ => (reflexive A, i)
   675                 | _ => (if pred i then cv A else reflexive A, i+1)
   676         in  combination (combination refl_cimplies thA) (gconv j B) end
   677         handle TERM _ => reflexive ct
   678   in gconv 1 end;
   679 
   680 (*Use a conversion to transform a theorem*)
   681 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   682 
   683 (*rewriting conversion*)
   684 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   685 
   686 (*Rewrite a theorem*)
   687 fun rewrite_rule thms =
   688   fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms));
   689 
   690 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   691 fun rewrite_goals_rule thms =
   692   fconv_rule (goals_conv (K true) (rew_conv (true,false) (K(K None))
   693              (Thm.mss_of thms)));
   694 
   695 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   696 fun rewrite_goal_rule mode prover mss i thm =
   697   if 0 < i  andalso  i <= nprems_of thm
   698   then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm
   699   else raise THM("rewrite_goal_rule",i,[thm]);
   700 
   701 
   702 (** Derived rules mainly for METAHYPS **)
   703 
   704 (*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
   705 fun equal_abs_elim ca eqth =
   706   let val {sign=signa, t=a, ...} = rep_cterm ca
   707       and combth = combination eqth (reflexive ca)
   708       val {sign,prop,...} = rep_thm eqth
   709       val (abst,absu) = Logic.dest_equals prop
   710       val cterm = cterm_of (Sign.merge (sign,signa))
   711   in  transitive (symmetric (beta_conversion (cterm (abst$a))))
   712            (transitive combth (beta_conversion (cterm (absu$a))))
   713   end
   714   handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   715 
   716 (*Calling equal_abs_elim with multiple terms*)
   717 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   718 
   719 local
   720   open Logic
   721   val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   722   fun err th = raise THM("flexpair_inst: ", 0, [th])
   723   fun flexpair_inst def th =
   724     let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
   725         val cterm = cterm_of sign
   726         fun cvar a = cterm(Var((a,0),alpha))
   727         val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
   728                    def
   729     in  equal_elim def' th
   730     end
   731     handle THM _ => err th | bind => err th
   732 in
   733 val flexpair_intr = flexpair_inst (symmetric flexpair_def)
   734 and flexpair_elim = flexpair_inst flexpair_def
   735 end;
   736 
   737 (*Version for flexflex pairs -- this supports lifting.*)
   738 fun flexpair_abs_elim_list cts =
   739     flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
   740 
   741 
   742 (*** Some useful meta-theorems ***)
   743 
   744 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   745 val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
   746 
   747 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   748 val cut_rl = trivial(read_cterm Sign.proto_pure
   749         ("PROP ?psi ==> PROP ?theta", propT));
   750 
   751 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   752      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   753 val revcut_rl =
   754   let val V = read_cterm Sign.proto_pure ("PROP V", propT)
   755       and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
   756   in  standard (implies_intr V
   757                 (implies_intr VW
   758                  (implies_elim (assume VW) (assume V))))
   759   end;
   760 
   761 (*for deleting an unwanted assumption*)
   762 val thin_rl =
   763   let val V = read_cterm Sign.proto_pure ("PROP V", propT)
   764       and W = read_cterm Sign.proto_pure ("PROP W", propT);
   765   in  standard (implies_intr V (implies_intr W (assume W)))
   766   end;
   767 
   768 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   769 val triv_forall_equality =
   770   let val V  = read_cterm Sign.proto_pure ("PROP V", propT)
   771       and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
   772       and x  = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
   773   in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   774                            (implies_intr V  (forall_intr x (assume V))))
   775   end;
   776 
   777 end
   778 end;
   779