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