diff -r 000000000000 -r a5a9c433f639 src/Pure/drule.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/drule.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,465 @@ +(* Title: drule + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Derived rules and other operations on theorems and theories +*) + +infix 0 RS RSN RL RLN COMP; + +signature DRULE = + sig + structure Thm : THM + local open Thm in + val asm_rl: thm + val assume_ax: theory -> string -> thm + val COMP: thm * thm -> thm + val compose: thm * int * thm -> thm list + val cterm_instantiate: (Sign.cterm*Sign.cterm)list -> thm -> thm + val cut_rl: thm + val equal_abs_elim: Sign.cterm -> thm -> thm + val equal_abs_elim_list: Sign.cterm list -> thm -> thm + val eq_sg: Sign.sg * Sign.sg -> bool + val eq_thm: thm * thm -> bool + val eq_thm_sg: thm * thm -> bool + val flexpair_abs_elim_list: Sign.cterm list -> thm -> thm + val forall_intr_list: Sign.cterm list -> thm -> thm + val forall_intr_frees: thm -> thm + val forall_elim_list: Sign.cterm list -> thm -> thm + val forall_elim_var: int -> thm -> thm + val forall_elim_vars: int -> thm -> thm + val implies_elim_list: thm -> thm list -> thm + val implies_intr_list: Sign.cterm list -> thm -> thm + val print_cterm: Sign.cterm -> unit + val print_ctyp: Sign.ctyp -> unit + val print_goals: int -> thm -> unit + val print_sg: Sign.sg -> unit + val print_theory: theory -> unit + val pprint_sg: Sign.sg -> pprint_args -> unit + val pprint_theory: theory -> pprint_args -> unit + val print_thm: thm -> unit + val prth: thm -> thm + val prthq: thm Sequence.seq -> thm Sequence.seq + val prths: thm list -> thm list + val read_instantiate: (string*string)list -> thm -> thm + val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm + val reflexive_thm: thm + val revcut_rl: thm + val rewrite_goal_rule: (meta_simpset -> thm -> thm option) -> meta_simpset -> + int -> thm -> thm + val rewrite_goals_rule: thm list -> thm -> thm + val rewrite_rule: thm list -> thm -> thm + val RS: thm * thm -> thm + val RSN: thm * (int * thm) -> thm + val RL: thm list * thm list -> thm list + val RLN: thm list * (int * thm list) -> thm list + val show_hyps: bool ref + val size_of_thm: thm -> int + val standard: thm -> thm + val string_of_thm: thm -> string + val symmetric_thm: thm + val pprint_thm: thm -> pprint_args -> unit + val transitive_thm: thm + val triv_forall_equality: thm + val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) + val zero_var_indexes: thm -> thm + end + end; + +functor DruleFun (structure Logic: LOGIC and Thm: THM) : DRULE = +struct +structure Thm = Thm; +structure Sign = Thm.Sign; +structure Type = Sign.Type; +structure Pretty = Sign.Syntax.Pretty +local open Thm +in + +(**** More derived rules and operations on theorems ****) + +(*** Find the type (sort) associated with a (T)Var or (T)Free in a term + Used for establishing default types (of variables) and sorts (of + type variables) when reading another term. + Index -1 indicates that a (T)Free rather than a (T)Var is wanted. +***) + +fun types_sorts thm = + let val {prop,hyps,...} = rep_thm thm; + val big = list_comb(prop,hyps); (* bogus term! *) + val vars = map dest_Var (term_vars big); + val frees = map dest_Free (term_frees big); + val tvars = term_tvars big; + val tfrees = term_tfrees big; + fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i)); + fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); + in (typ,sort) end; + +(** Standardization of rules **) + +(*Generalization over a list of variables, IGNORING bad ones*) +fun forall_intr_list [] th = th + | forall_intr_list (y::ys) th = + let val gth = forall_intr_list ys th + in forall_intr y gth handle THM _ => gth end; + +(*Generalization over all suitable Free variables*) +fun forall_intr_frees th = + let val {prop,sign,...} = rep_thm th + in forall_intr_list + (map (Sign.cterm_of sign) (sort atless (term_frees prop))) + th + end; + +(*Replace outermost quantified variable by Var of given index. + Could clash with Vars already present.*) +fun forall_elim_var i th = + let val {prop,sign,...} = rep_thm th + in case prop of + Const("all",_) $ Abs(a,T,_) => + forall_elim (Sign.cterm_of sign (Var((a,i), T))) th + | _ => raise THM("forall_elim_var", i, [th]) + end; + +(*Repeat forall_elim_var until all outer quantifiers are removed*) +fun forall_elim_vars i th = + forall_elim_vars i (forall_elim_var i th) + handle THM _ => th; + +(*Specialization over a list of cterms*) +fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th); + +(* maps [A1,...,An], B to [| A1;...;An |] ==> B *) +fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th); + +(* maps [| A1;...;An |] ==> B and [A1,...,An] to B *) +fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths); + +(*Reset Var indexes to zero, renaming to preserve distinctness*) +fun zero_var_indexes th = + let val {prop,sign,...} = rep_thm th; + val vars = term_vars prop + val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars) + val inrs = add_term_tvars(prop,[]); + val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs)); + val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms') + val ctye = map (fn (v,T) => (v,Sign.ctyp_of sign T)) tye; + fun varpairs([],[]) = [] + | varpairs((var as Var(v,T)) :: vars, b::bs) = + let val T' = typ_subst_TVars tye T + in (Sign.cterm_of sign (Var(v,T')), + Sign.cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs) + end + | varpairs _ = raise TERM("varpairs", []); + in instantiate (ctye, varpairs(vars,rev bs)) th end; + + +(*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers; + all generality expressed by Vars having index 0.*) +fun standard th = + let val {maxidx,...} = rep_thm th + in varifyT (zero_var_indexes (forall_elim_vars(maxidx+1) + (forall_intr_frees(implies_intr_hyps th)))) + end; + +(*Assume a new formula, read following the same conventions as axioms. + Generalizes over Free variables, + creates the assumption, and then strips quantifiers. + Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |] + [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ] *) +fun assume_ax thy sP = + let val sign = sign_of thy + val prop = Logic.close_form (Sign.term_of (Sign.read_cterm sign + (sP, propT))) + in forall_elim_vars 0 (assume (Sign.cterm_of sign prop)) end; + +(*Resolution: exactly one resolvent must be produced.*) +fun tha RSN (i,thb) = + case Sequence.chop (2, biresolution false [(false,tha)] i thb) of + ([th],_) => th + | ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) + | _ => raise THM("RSN: multiple unifiers", i, [tha,thb]); + +(*resolution: P==>Q, Q==>R gives P==>R. *) +fun tha RS thb = tha RSN (1,thb); + +(*For joining lists of rules*) +fun thas RLN (i,thbs) = + let val resolve = biresolution false (map (pair false) thas) i + fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => [] + in flat (map resb thbs) end; + +fun thas RL thbs = thas RLN (1,thbs); + +(*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R + with no lifting or renaming! Q may contain ==> or meta-quants + ALWAYS deletes premise i *) +fun compose(tha,i,thb) = + Sequence.list_of_s (bicompose false (false,tha,0) i thb); + +(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) +fun tha COMP thb = + case compose(tha,1,thb) of + [th] => th + | _ => raise THM("COMP", 1, [tha,thb]); + +(*Instantiate theorem th, reading instantiations under signature sg*) +fun read_instantiate_sg sg sinsts th = + let val ts = types_sorts th; + val instpair = Sign.read_insts sg ts ts sinsts + in instantiate instpair th end; + +(*Instantiate theorem th, reading instantiations under theory of th*) +fun read_instantiate sinsts th = + read_instantiate_sg (#sign (rep_thm th)) sinsts th; + + +(*Left-to-right replacements: tpairs = [...,(vi,ti),...]. + Instantiates distinct Vars by terms, inferring type instantiations. *) +local + fun add_types ((ct,cu), (sign,tye)) = + let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct + and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu + val sign' = Sign.merge(sign, Sign.merge(signt, signu)) + val tye' = Type.unify (#tsig(Sign.rep_sg sign')) ((T,U), tye) + handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u]) + in (sign', tye') end; +in +fun cterm_instantiate ctpairs0 th = + let val (sign,tye) = foldr add_types (ctpairs0, (#sign(rep_thm th),[])) + val tsig = #tsig(Sign.rep_sg sign); + fun instT(ct,cu) = let val inst = subst_TVars tye + in (Sign.cfun inst ct, Sign.cfun inst cu) end + fun ctyp2 (ix,T) = (ix, Sign.ctyp_of sign T) + in instantiate (map ctyp2 tye, map instT ctpairs0) th end + handle TERM _ => + raise THM("cterm_instantiate: incompatible signatures",0,[th]) + | TYPE _ => raise THM("cterm_instantiate: types", 0, [th]) +end; + + +(*** Printing of theorems ***) + +(*If false, hypotheses are printed as dots*) +val show_hyps = ref true; + +fun pretty_thm th = +let val {sign, hyps, prop,...} = rep_thm th + val hsymbs = if null hyps then [] + else if !show_hyps then + [Pretty.brk 2, + Pretty.lst("[","]") (map (Sign.pretty_term sign) hyps)] + else Pretty.str" [" :: map (fn _ => Pretty.str".") hyps @ + [Pretty.str"]"]; +in Pretty.blk(0, Sign.pretty_term sign prop :: hsymbs) end; + +val string_of_thm = Pretty.string_of o pretty_thm; + +val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm; + + +(** Top-level commands for printing theorems **) +val print_thm = writeln o string_of_thm; + +fun prth th = (print_thm th; th); + +(*Print and return a sequence of theorems, separated by blank lines. *) +fun prthq thseq = + (Sequence.prints (fn _ => print_thm) 100000 thseq; + thseq); + +(*Print and return a list of theorems, separated by blank lines. *) +fun prths ths = (print_list_ln print_thm ths; ths); + +(*Other printing commands*) +val print_cterm = writeln o Sign.string_of_cterm; +val print_ctyp = writeln o Sign.string_of_ctyp; +fun pretty_sg sg = + Pretty.lst ("{", "}") (map (Pretty.str o !) (#stamps (Sign.rep_sg sg))); + +val pprint_sg = Pretty.pprint o pretty_sg; + +val pprint_theory = pprint_sg o sign_of; + +val print_sg = writeln o Pretty.string_of o pretty_sg; +val print_theory = print_sg o sign_of; + + +(** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **) + +fun prettyprints es = writeln(Pretty.string_of(Pretty.blk(0,es))); + +fun print_goals maxgoals th : unit = +let val {sign, hyps, prop,...} = rep_thm th; + fun printgoals (_, []) = () + | printgoals (n, A::As) = + let val prettyn = Pretty.str(" " ^ string_of_int n ^ ". "); + val prettyA = Sign.pretty_term sign A + in prettyprints[prettyn,prettyA]; + printgoals (n+1,As) + end; + fun prettypair(t,u) = + Pretty.blk(0, [Sign.pretty_term sign t, Pretty.str" =?=", Pretty.brk 1, + Sign.pretty_term sign u]); + fun printff [] = () + | printff tpairs = + writeln("\nFlex-flex pairs:\n" ^ + Pretty.string_of(Pretty.lst("","") (map prettypair tpairs))) + val (tpairs,As,B) = Logic.strip_horn(prop); + val ngoals = length As +in + writeln (Sign.string_of_term sign B); + if ngoals=0 then writeln"No subgoals!" + else if ngoals>maxgoals + then (printgoals (1, take(maxgoals,As)); + writeln("A total of " ^ string_of_int ngoals ^ " subgoals...")) + else printgoals (1, As); + printff tpairs +end; + + +(** theorem equality test is exported and used by BEST_FIRST **) + +(*equality of signatures means exact identity -- by ref equality*) +fun eq_sg (sg1,sg2) = (#stamps(Sign.rep_sg sg1) = #stamps(Sign.rep_sg sg2)); + +(*equality of theorems uses equality of signatures and + the a-convertible test for terms*) +fun eq_thm (th1,th2) = + let val {sign=sg1, hyps=hyps1, prop=prop1, ...} = rep_thm th1 + and {sign=sg2, hyps=hyps2, prop=prop2, ...} = rep_thm th2 + in eq_sg (sg1,sg2) andalso + aconvs(hyps1,hyps2) andalso + prop1 aconv prop2 + end; + +(*Do the two theorems have the same signature?*) +fun eq_thm_sg (th1,th2) = eq_sg(#sign(rep_thm th1), #sign(rep_thm th2)); + +(*Useful "distance" function for BEST_FIRST*) +val size_of_thm = size_of_term o #prop o rep_thm; + + +(*** Meta-Rewriting Rules ***) + + +val reflexive_thm = + let val cx = Sign.cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),["logic"]))) + in Thm.reflexive cx end; + +val symmetric_thm = + let val xy = Sign.read_cterm Sign.pure ("x::'a::logic == y",propT) + in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end; + +val transitive_thm = + let val xy = Sign.read_cterm Sign.pure ("x::'a::logic == y",propT) + val yz = Sign.read_cterm Sign.pure ("y::'a::logic == z",propT) + val xythm = Thm.assume xy and yzthm = Thm.assume yz + in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; + + +(** Below, a "conversion" has type sign->term->thm **) + +(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*) +fun goals_conv pred cv sign = + let val triv = reflexive o Sign.cterm_of sign + fun gconv i t = + let val (A,B) = Logic.dest_implies t + val thA = if (pred i) then (cv sign A) else (triv A) + in combination (combination (triv implies) thA) + (gconv (i+1) B) + end + handle TERM _ => triv t + in gconv 1 end; + +(*Use a conversion to transform a theorem*) +fun fconv_rule cv th = + let val {sign,prop,...} = rep_thm th + in equal_elim (cv sign prop) th end; + +(*rewriting conversion*) +fun rew_conv prover mss sign t = + rewrite_cterm mss prover (Sign.cterm_of sign t); + +(*Rewrite a theorem*) +fun rewrite_rule thms = fconv_rule (rew_conv (K(K None)) (Thm.mss_of thms)); + +(*Rewrite the subgoals of a proof state (represented by a theorem) *) +fun rewrite_goals_rule thms = + fconv_rule (goals_conv (K true) (rew_conv (K(K None)) (Thm.mss_of thms))); + +(*Rewrite the subgoal of a proof state (represented by a theorem) *) +fun rewrite_goal_rule prover mss i = + fconv_rule (goals_conv (fn j => j=i) (rew_conv prover mss)); + + +(** Derived rules mainly for METAHYPS **) + +(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*) +fun equal_abs_elim ca eqth = + let val {sign=signa, t=a, ...} = Sign.rep_cterm ca + and combth = combination eqth (reflexive ca) + val {sign,prop,...} = rep_thm eqth + val (abst,absu) = Logic.dest_equals prop + val cterm = Sign.cterm_of (Sign.merge (sign,signa)) + in transitive (symmetric (beta_conversion (cterm (abst$a)))) + (transitive combth (beta_conversion (cterm (absu$a)))) + end + handle THM _ => raise THM("equal_abs_elim", 0, [eqth]); + +(*Calling equal_abs_elim with multiple terms*) +fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th); + +local + open Logic + val alpha = TVar(("'a",0), []) (* type ?'a::{} *) + fun err th = raise THM("flexpair_inst: ", 0, [th]) + fun flexpair_inst def th = + let val {prop = Const _ $ t $ u, sign,...} = rep_thm th + val cterm = Sign.cterm_of sign + fun cvar a = cterm(Var((a,0),alpha)) + val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] + def + in equal_elim def' th + end + handle THM _ => err th | bind => err th +in +val flexpair_intr = flexpair_inst (symmetric flexpair_def) +and flexpair_elim = flexpair_inst flexpair_def +end; + +(*Version for flexflex pairs -- this supports lifting.*) +fun flexpair_abs_elim_list cts = + flexpair_intr o equal_abs_elim_list cts o flexpair_elim; + + +(*** Some useful meta-theorems ***) + +(*The rule V/V, obtains assumption solving for eresolve_tac*) +val asm_rl = trivial(Sign.read_cterm Sign.pure ("PROP ?psi",propT)); + +(*Meta-level cut rule: [| V==>W; V |] ==> W *) +val cut_rl = trivial(Sign.read_cterm Sign.pure + ("PROP ?psi ==> PROP ?theta", propT)); + +(*Generalized elim rule for one conclusion; cut_rl with reversed premises: + [| PROP V; PROP V ==> PROP W |] ==> PROP W *) +val revcut_rl = + let val V = Sign.read_cterm Sign.pure ("PROP V", propT) + and VW = Sign.read_cterm Sign.pure ("PROP V ==> PROP W", propT); + in standard (implies_intr V + (implies_intr VW + (implies_elim (assume VW) (assume V)))) + end; + +(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*) +val triv_forall_equality = + let val V = Sign.read_cterm Sign.pure ("PROP V", propT) + and QV = Sign.read_cterm Sign.pure ("!!x::'a. PROP V", propT) + and x = Sign.read_cterm Sign.pure ("x", TFree("'a",["logic"])); + in standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) + (implies_intr V (forall_intr x (assume V)))) + end; + +end +end;