wenzelm@250: (* Title: Pure/thm.ML clasohm@0: ID: $Id$ wenzelm@250: Author: Lawrence C Paulson, Cambridge University Computer Laboratory lcp@229: Copyright 1994 University of Cambridge lcp@229: wenzelm@1160: The core of Isabelle's Meta Logic: certified types and terms, meta paulson@1529: theorems, meta rules (including resolution and simplification). clasohm@0: *) clasohm@0: wenzelm@250: signature THM = paulson@1503: sig wenzelm@1160: (*certified types*) wenzelm@387: type ctyp wenzelm@1238: val rep_ctyp : ctyp -> {sign: Sign.sg, T: typ} wenzelm@1238: val typ_of : ctyp -> typ wenzelm@1238: val ctyp_of : Sign.sg -> typ -> ctyp wenzelm@1238: val read_ctyp : Sign.sg -> string -> ctyp wenzelm@1160: wenzelm@1160: (*certified terms*) wenzelm@1160: type cterm clasohm@1493: exception CTERM of string clasohm@1493: val rep_cterm : cterm -> {sign: Sign.sg, t: term, T: typ, clasohm@1493: maxidx: int} wenzelm@1238: val term_of : cterm -> term wenzelm@1238: val cterm_of : Sign.sg -> term -> cterm paulson@2671: val ctyp_of_term : cterm -> ctyp wenzelm@1238: val read_cterm : Sign.sg -> string * typ -> cterm paulson@1394: val read_cterms : Sign.sg -> string list * typ list -> cterm list wenzelm@1238: val cterm_fun : (term -> term) -> (cterm -> cterm) clasohm@1493: val dest_comb : cterm -> cterm * cterm clasohm@1493: val dest_abs : cterm -> cterm * cterm clasohm@1703: val adjust_maxidx : cterm -> cterm clasohm@1516: val capply : cterm -> cterm -> cterm clasohm@1517: val cabs : cterm -> cterm -> cterm wenzelm@1238: val read_def_cterm : wenzelm@1160: Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> wenzelm@1160: string list -> bool -> string * typ -> cterm * (indexname * typ) list wenzelm@1160: paulson@1529: (*theories*) paulson@1529: paulson@2671: (*proof terms [must DUPLICATE declaration as a specification]*) paulson@1597: datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv; wenzelm@2386: val keep_derivs : deriv_kind ref paulson@1529: datatype rule = wenzelm@2386: MinProof paulson@1597: | Oracle of theory * Sign.sg * exn paulson@2671: | Axiom of theory * string paulson@2671: | Theorem of string paulson@2671: | Assume of cterm paulson@2671: | Implies_intr of cterm paulson@1529: | Implies_intr_shyps paulson@1529: | Implies_intr_hyps paulson@1529: | Implies_elim paulson@2671: | Forall_intr of cterm paulson@2671: | Forall_elim of cterm paulson@2671: | Reflexive of cterm paulson@1529: | Symmetric paulson@1529: | Transitive paulson@2671: | Beta_conversion of cterm paulson@1529: | Extensional paulson@2671: | Abstract_rule of string * cterm paulson@1529: | Combination paulson@1529: | Equal_intr paulson@1529: | Equal_elim paulson@2671: | Trivial of cterm paulson@2671: | Lift_rule of cterm * int paulson@2671: | Assumption of int * Envir.env option paulson@2671: | Rotate_rule of int * int paulson@2671: | Instantiate of (indexname * ctyp) list * (cterm * cterm) list paulson@2671: | Bicompose of bool * bool * int * int * Envir.env paulson@2671: | Flexflex_rule of Envir.env paulson@2671: | Class_triv of theory * class paulson@1529: | VarifyT paulson@1529: | FreezeT paulson@2671: | RewriteC of cterm paulson@2671: | CongC of cterm paulson@2671: | Rewrite_cterm of cterm paulson@2671: | Rename_params_rule of string list * int; paulson@1529: paulson@1597: type deriv (* = rule mtree *) paulson@1529: wenzelm@1160: (*meta theorems*) wenzelm@1160: type thm wenzelm@1160: exception THM of string * int * thm list paulson@1529: val rep_thm : thm -> {sign: Sign.sg, der: deriv, maxidx: int, wenzelm@2386: shyps: sort list, hyps: term list, wenzelm@2386: prop: term} paulson@1529: val crep_thm : thm -> {sign: Sign.sg, der: deriv, maxidx: int, wenzelm@2386: shyps: sort list, hyps: cterm list, wenzelm@2386: prop: cterm} wenzelm@1238: val stamps_of_thm : thm -> string ref list wenzelm@1238: val tpairs_of : thm -> (term * term) list wenzelm@1238: val prems_of : thm -> term list wenzelm@1238: val nprems_of : thm -> int wenzelm@1238: val concl_of : thm -> term wenzelm@1238: val cprop_of : thm -> cterm wenzelm@1238: val extra_shyps : thm -> sort list wenzelm@3061: val force_strip_shyps : bool ref (* FIXME tmp (since 1995/08/01) *) wenzelm@1238: val strip_shyps : thm -> thm wenzelm@1238: val implies_intr_shyps: thm -> thm wenzelm@1238: val get_axiom : theory -> string -> thm paulson@1597: val name_thm : string * thm -> thm wenzelm@1238: val axioms_of : theory -> (string * thm) list wenzelm@1160: wenzelm@1160: (*meta rules*) wenzelm@1238: val assume : cterm -> thm paulson@1416: val compress : thm -> thm wenzelm@1238: val implies_intr : cterm -> thm -> thm wenzelm@1238: val implies_elim : thm -> thm -> thm wenzelm@1238: val forall_intr : cterm -> thm -> thm wenzelm@1238: val forall_elim : cterm -> thm -> thm wenzelm@1238: val flexpair_def : thm wenzelm@1238: val reflexive : cterm -> thm wenzelm@1238: val symmetric : thm -> thm wenzelm@1238: val transitive : thm -> thm -> thm wenzelm@1238: val beta_conversion : cterm -> thm wenzelm@1238: val extensional : thm -> thm wenzelm@1238: val abstract_rule : string -> cterm -> thm -> thm wenzelm@1238: val combination : thm -> thm -> thm wenzelm@1238: val equal_intr : thm -> thm -> thm wenzelm@1238: val equal_elim : thm -> thm -> thm wenzelm@1238: val implies_intr_hyps : thm -> thm wenzelm@1238: val flexflex_rule : thm -> thm Sequence.seq wenzelm@1238: val instantiate : wenzelm@1160: (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm wenzelm@1238: val trivial : cterm -> thm wenzelm@1238: val class_triv : theory -> class -> thm wenzelm@1238: val varifyT : thm -> thm wenzelm@1238: val freezeT : thm -> thm wenzelm@1238: val dest_state : thm * int -> wenzelm@1160: (term * term) list * term list * term * term wenzelm@1238: val lift_rule : (thm * int) -> thm -> thm wenzelm@1238: val assumption : int -> thm -> thm Sequence.seq wenzelm@1238: val eq_assumption : int -> thm -> thm paulson@2671: val rotate_rule : int -> int -> thm -> thm wenzelm@1160: val rename_params_rule: string list * int -> thm -> thm wenzelm@1238: val bicompose : bool -> bool * thm * int -> wenzelm@1160: int -> thm -> thm Sequence.seq wenzelm@1238: val biresolution : bool -> (bool * thm) list -> wenzelm@1160: int -> thm -> thm Sequence.seq wenzelm@1160: wenzelm@1160: (*meta simplification*) wenzelm@1160: type meta_simpset wenzelm@1160: exception SIMPLIFIER of string * thm wenzelm@1238: val empty_mss : meta_simpset wenzelm@1238: val add_simps : meta_simpset * thm list -> meta_simpset wenzelm@1238: val del_simps : meta_simpset * thm list -> meta_simpset wenzelm@1238: val mss_of : thm list -> meta_simpset wenzelm@1238: val add_congs : meta_simpset * thm list -> meta_simpset oheimb@2626: val del_congs : meta_simpset * thm list -> meta_simpset wenzelm@2509: val add_simprocs : meta_simpset * wenzelm@2509: (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset wenzelm@2509: val del_simprocs : meta_simpset * wenzelm@2509: (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset wenzelm@1238: val add_prems : meta_simpset * thm list -> meta_simpset wenzelm@1238: val prems_of_mss : meta_simpset -> thm list wenzelm@1238: val set_mk_rews : meta_simpset * (thm -> thm list) -> meta_simpset wenzelm@1238: val mk_rews_of_mss : meta_simpset -> thm -> thm list wenzelm@2509: val set_termless : meta_simpset * (term * term -> bool) -> meta_simpset wenzelm@1238: val trace_simp : bool ref wenzelm@1238: val rewrite_cterm : bool * bool -> meta_simpset -> paulson@1529: (meta_simpset -> thm -> thm option) -> cterm -> thm paulson@1539: wenzelm@2386: val invoke_oracle : theory * Sign.sg * exn -> thm wenzelm@250: end; clasohm@0: paulson@1503: structure Thm : THM = clasohm@0: struct wenzelm@250: wenzelm@387: (*** Certified terms and types ***) wenzelm@387: wenzelm@250: (** certified types **) wenzelm@250: wenzelm@250: (*certified typs under a signature*) wenzelm@250: wenzelm@250: datatype ctyp = Ctyp of {sign: Sign.sg, T: typ}; wenzelm@250: wenzelm@250: fun rep_ctyp (Ctyp args) = args; wenzelm@250: fun typ_of (Ctyp {T, ...}) = T; wenzelm@250: wenzelm@250: fun ctyp_of sign T = wenzelm@250: Ctyp {sign = sign, T = Sign.certify_typ sign T}; wenzelm@250: wenzelm@250: fun read_ctyp sign s = wenzelm@250: Ctyp {sign = sign, T = Sign.read_typ (sign, K None) s}; lcp@229: lcp@229: lcp@229: wenzelm@250: (** certified terms **) lcp@229: wenzelm@250: (*certified terms under a signature, with checked typ and maxidx of Vars*) lcp@229: wenzelm@250: datatype cterm = Cterm of {sign: Sign.sg, t: term, T: typ, maxidx: int}; lcp@229: lcp@229: fun rep_cterm (Cterm args) = args; wenzelm@250: fun term_of (Cterm {t, ...}) = t; lcp@229: paulson@2671: fun ctyp_of_term (Cterm {sign, T, ...}) = Ctyp {sign=sign, T=T}; paulson@2671: wenzelm@250: (*create a cterm by checking a "raw" term with respect to a signature*) wenzelm@250: fun cterm_of sign tm = wenzelm@250: let val (t, T, maxidx) = Sign.certify_term sign tm paulson@1394: in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} paulson@1394: end; lcp@229: wenzelm@250: fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t); wenzelm@250: lcp@229: clasohm@1493: exception CTERM of string; clasohm@1493: clasohm@1493: (*Destruct application in cterms*) clasohm@1493: fun dest_comb (Cterm{sign, T, maxidx, t = A $ B}) = clasohm@1493: let val typeA = fastype_of A; clasohm@1493: val typeB = clasohm@1493: case typeA of Type("fun",[S,T]) => S clasohm@1493: | _ => error "Function type expected in dest_comb"; clasohm@1493: in clasohm@1493: (Cterm {sign=sign, maxidx=maxidx, t=A, T=typeA}, clasohm@1493: Cterm {sign=sign, maxidx=maxidx, t=B, T=typeB}) clasohm@1493: end clasohm@1493: | dest_comb _ = raise CTERM "dest_comb"; clasohm@1493: clasohm@1493: (*Destruct abstraction in cterms*) clasohm@1516: fun dest_abs (Cterm {sign, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = clasohm@1516: let val (y,N) = variant_abs (x,ty,M) clasohm@1516: in (Cterm {sign = sign, T = ty, maxidx = 0, t = Free(y,ty)}, clasohm@1516: Cterm {sign = sign, T = S, maxidx = maxidx, t = N}) clasohm@1493: end clasohm@1493: | dest_abs _ = raise CTERM "dest_abs"; clasohm@1493: paulson@2147: (*Makes maxidx precise: it is often too big*) paulson@2147: fun adjust_maxidx (ct as Cterm {sign, T, t, maxidx, ...}) = paulson@2147: if maxidx = ~1 then ct paulson@2147: else Cterm {sign = sign, T = T, maxidx = maxidx_of_term t, t = t}; clasohm@1703: clasohm@1516: (*Form cterm out of a function and an argument*) clasohm@1516: fun capply (Cterm {t=f, sign=sign1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) clasohm@1516: (Cterm {t=x, sign=sign2, T, maxidx=maxidx2}) = clasohm@1516: if T = dty then Cterm{t=f$x, sign=Sign.merge(sign1,sign2), T=rty, paulson@2147: maxidx=Int.max(maxidx1, maxidx2)} clasohm@1516: else raise CTERM "capply: types don't agree" clasohm@1516: | capply _ _ = raise CTERM "capply: first arg is not a function" wenzelm@250: clasohm@1517: fun cabs (Cterm {t=Free(a,ty), sign=sign1, T=T1, maxidx=maxidx1}) clasohm@1517: (Cterm {t=t2, sign=sign2, T=T2, maxidx=maxidx2}) = clasohm@1517: Cterm {t=absfree(a,ty,t2), sign=Sign.merge(sign1,sign2), paulson@2147: T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)} clasohm@1517: | cabs _ _ = raise CTERM "cabs: first arg is not a free variable"; lcp@229: wenzelm@2509: wenzelm@2509: wenzelm@574: (** read cterms **) (*exception ERROR*) wenzelm@250: wenzelm@250: (*read term, infer types, certify term*) nipkow@949: fun read_def_cterm (sign, types, sorts) used freeze (a, T) = wenzelm@250: let wenzelm@574: val T' = Sign.certify_typ sign T wenzelm@574: handle TYPE (msg, _, _) => error msg; clasohm@623: val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a; nipkow@949: val (_, t', tye) = clasohm@959: Sign.infer_types sign types sorts used freeze (ts, T'); wenzelm@574: val ct = cterm_of sign t' wenzelm@2979: handle TYPE (msg, _, _) => error msg wenzelm@2386: | TERM (msg, _) => error msg; wenzelm@250: in (ct, tye) end; lcp@229: nipkow@949: fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true; lcp@229: paulson@1394: (*read a list of terms, matching them against a list of expected types. paulson@1394: NO disambiguation of alternative parses via type-checking -- it is just paulson@1394: not practical.*) paulson@1394: fun read_cterms sign (bs, Ts) = paulson@1394: let wenzelm@2979: val {tsig, syn, ...} = Sign.rep_sg sign; wenzelm@2979: fun read (b, T) = wenzelm@2979: (case Syntax.read syn T b of wenzelm@2979: [t] => t wenzelm@2979: | _ => error ("Error or ambiguity in parsing of " ^ b)); wenzelm@2979: wenzelm@2979: val prt = setmp Syntax.show_brackets true (Sign.pretty_term sign); wenzelm@2979: val prT = Sign.pretty_typ sign; wenzelm@2979: val (us, _) = wenzelm@2979: Type.infer_types prt prT tsig (Sign.const_type sign) wenzelm@2979: (K None) (K None) [] true (map (Sign.certify_typ sign) Ts) wenzelm@2979: (ListPair.map read (bs, Ts)); wenzelm@2979: in map (cterm_of sign) us end wenzelm@2979: handle TYPE (msg, _, _) => error msg paulson@1394: | TERM (msg, _) => error msg; paulson@1394: wenzelm@250: wenzelm@250: paulson@1529: (*** Derivations ***) paulson@1529: paulson@1529: (*Names of rules in derivations. Includes logically trivial rules, if paulson@1529: executed in ML.*) paulson@1529: datatype rule = wenzelm@2386: MinProof (*for building minimal proof terms*) wenzelm@2386: | Oracle of theory * Sign.sg * exn (*oracles*) paulson@1529: (*Axioms/theorems*) wenzelm@2386: | Axiom of theory * string wenzelm@2386: | Theorem of string paulson@1529: (*primitive inferences and compound versions of them*) wenzelm@2386: | Assume of cterm wenzelm@2386: | Implies_intr of cterm paulson@1529: | Implies_intr_shyps paulson@1529: | Implies_intr_hyps paulson@1529: | Implies_elim wenzelm@2386: | Forall_intr of cterm wenzelm@2386: | Forall_elim of cterm wenzelm@2386: | Reflexive of cterm paulson@1529: | Symmetric paulson@1529: | Transitive wenzelm@2386: | Beta_conversion of cterm paulson@1529: | Extensional wenzelm@2386: | Abstract_rule of string * cterm paulson@1529: | Combination paulson@1529: | Equal_intr paulson@1529: | Equal_elim paulson@1529: (*derived rules for tactical proof*) wenzelm@2386: | Trivial of cterm wenzelm@2386: (*For lift_rule, the proof state is not a premise. wenzelm@2386: Use cterm instead of thm to avoid mutual recursion.*) wenzelm@2386: | Lift_rule of cterm * int wenzelm@2386: | Assumption of int * Envir.env option (*includes eq_assumption*) paulson@2671: | Rotate_rule of int * int wenzelm@2386: | Instantiate of (indexname * ctyp) list * (cterm * cterm) list wenzelm@2386: | Bicompose of bool * bool * int * int * Envir.env wenzelm@2386: | Flexflex_rule of Envir.env (*identifies unifier chosen*) paulson@1529: (*other derived rules*) wenzelm@2509: | Class_triv of theory * class paulson@1529: | VarifyT paulson@1529: | FreezeT paulson@1529: (*for the simplifier*) wenzelm@2386: | RewriteC of cterm wenzelm@2386: | CongC of cterm wenzelm@2386: | Rewrite_cterm of cterm paulson@1529: (*Logical identities, recorded since they are part of the proof process*) wenzelm@2386: | Rename_params_rule of string list * int; paulson@1529: paulson@1529: paulson@1597: type deriv = rule mtree; paulson@1529: paulson@1597: datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv; paulson@1529: paulson@1597: val keep_derivs = ref MinDeriv; paulson@1529: paulson@1529: paulson@1597: (*Build a minimal derivation. Keep oracles; suppress atomic inferences; paulson@1597: retain Theorems or their underlying links; keep anything else*) paulson@1597: fun squash_derivs [] = [] paulson@1597: | squash_derivs (der::ders) = paulson@1597: (case der of wenzelm@2386: Join (Oracle _, _) => der :: squash_derivs ders wenzelm@2386: | Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv wenzelm@2386: then der :: squash_derivs ders wenzelm@2386: else squash_derivs (der'::ders) wenzelm@2386: | Join (Axiom _, _) => if !keep_derivs=ThmDeriv wenzelm@2386: then der :: squash_derivs ders wenzelm@2386: else squash_derivs ders wenzelm@2386: | Join (_, []) => squash_derivs ders wenzelm@2386: | _ => der :: squash_derivs ders); paulson@1597: paulson@1529: paulson@1529: (*Ensure sharing of the most likely derivation, the empty one!*) paulson@1597: val min_infer = Join (MinProof, []); paulson@1529: paulson@1529: (*Make a minimal inference*) paulson@1529: fun make_min_infer [] = min_infer paulson@1529: | make_min_infer [der] = der paulson@1597: | make_min_infer ders = Join (MinProof, ders); paulson@1529: paulson@1597: fun infer_derivs (rl, []) = Join (rl, []) paulson@1529: | infer_derivs (rl, ders) = paulson@1597: if !keep_derivs=FullDeriv then Join (rl, ders) paulson@1529: else make_min_infer (squash_derivs ders); paulson@1529: paulson@1529: wenzelm@2509: wenzelm@387: (*** Meta theorems ***) lcp@229: clasohm@0: datatype thm = Thm of wenzelm@2386: {sign: Sign.sg, (*signature for hyps and prop*) wenzelm@2386: der: deriv, (*derivation*) wenzelm@2386: maxidx: int, (*maximum index of any Var or TVar*) wenzelm@2386: shyps: sort list, (*sort hypotheses*) wenzelm@2386: hyps: term list, (*hypotheses*) wenzelm@2386: prop: term}; (*conclusion*) clasohm@0: wenzelm@250: fun rep_thm (Thm args) = args; clasohm@0: paulson@1529: (*Version of rep_thm returning cterms instead of terms*) paulson@1529: fun crep_thm (Thm {sign, der, maxidx, shyps, hyps, prop}) = paulson@1529: let fun ctermf max t = Cterm{sign=sign, t=t, T=propT, maxidx=max}; paulson@1529: in {sign=sign, der=der, maxidx=maxidx, shyps=shyps, paulson@1529: hyps = map (ctermf ~1) hyps, paulson@1529: prop = ctermf maxidx prop} clasohm@1517: end; clasohm@1517: wenzelm@387: (*errors involving theorems*) clasohm@0: exception THM of string * int * thm list; clasohm@0: wenzelm@387: paulson@1597: val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm; clasohm@0: wenzelm@387: (*merge signatures of two theorems; raise exception if incompatible*) wenzelm@387: fun merge_thm_sgs (th1, th2) = paulson@1597: Sign.merge (pairself (#sign o rep_thm) (th1, th2)) wenzelm@574: handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]); wenzelm@387: wenzelm@387: wenzelm@387: (*maps object-rule to tpairs*) wenzelm@387: fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop); wenzelm@387: wenzelm@387: (*maps object-rule to premises*) wenzelm@387: fun prems_of (Thm {prop, ...}) = wenzelm@387: Logic.strip_imp_prems (Logic.skip_flexpairs prop); clasohm@0: clasohm@0: (*counts premises in a rule*) wenzelm@387: fun nprems_of (Thm {prop, ...}) = wenzelm@387: Logic.count_prems (Logic.skip_flexpairs prop, 0); clasohm@0: wenzelm@387: (*maps object-rule to conclusion*) wenzelm@387: fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; clasohm@0: wenzelm@387: (*the statement of any thm is a cterm*) wenzelm@1160: fun cprop_of (Thm {sign, maxidx, prop, ...}) = wenzelm@387: Cterm {sign = sign, maxidx = maxidx, T = propT, t = prop}; lcp@229: wenzelm@387: clasohm@0: wenzelm@1238: (** sort contexts of theorems **) wenzelm@1238: wenzelm@1238: (* basic utils *) wenzelm@1238: wenzelm@2163: (*accumulate sorts suppressing duplicates; these are coded low levelly wenzelm@1238: to improve efficiency a bit*) wenzelm@1238: wenzelm@1238: fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss) paulson@2177: | add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss) paulson@2177: | add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) wenzelm@1238: and add_typs_sorts ([], Ss) = Ss wenzelm@1238: | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); wenzelm@1238: wenzelm@1238: fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss) wenzelm@1238: | add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss) wenzelm@1238: | add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss) wenzelm@1238: | add_term_sorts (Bound _, Ss) = Ss paulson@2177: | add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) wenzelm@1238: | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); wenzelm@1238: wenzelm@1238: fun add_terms_sorts ([], Ss) = Ss paulson@2177: | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); wenzelm@1238: wenzelm@1258: fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; wenzelm@1258: wenzelm@1258: fun add_env_sorts (env, Ss) = wenzelm@1258: add_terms_sorts (map snd (Envir.alist_of env), wenzelm@1258: add_typs_sorts (env_codT env, Ss)); wenzelm@1258: wenzelm@1238: fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) = wenzelm@1238: add_terms_sorts (hyps, add_term_sorts (prop, Ss)); wenzelm@1238: wenzelm@1238: fun add_thms_shyps ([], Ss) = Ss wenzelm@1238: | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) = paulson@2177: add_thms_shyps (ths, union_sort(shyps,Ss)); wenzelm@1238: wenzelm@1238: wenzelm@1238: (*get 'dangling' sort constraints of a thm*) wenzelm@1238: fun extra_shyps (th as Thm {shyps, ...}) = wenzelm@1238: shyps \\ add_thm_sorts (th, []); wenzelm@1238: wenzelm@1238: wenzelm@1238: (* fix_shyps *) wenzelm@1238: wenzelm@1238: (*preserve sort contexts of rule premises and substituted types*) wenzelm@1238: fun fix_shyps thms Ts thm = wenzelm@1238: let paulson@1529: val Thm {sign, der, maxidx, hyps, prop, ...} = thm; wenzelm@1238: val shyps = wenzelm@1238: add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))); wenzelm@1238: in paulson@1529: Thm {sign = sign, wenzelm@2386: der = der, (*No new derivation, as other rules call this*) wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = shyps, hyps = hyps, prop = prop} wenzelm@1238: end; wenzelm@1238: wenzelm@1238: wenzelm@1238: (* strip_shyps *) (* FIXME improve? (e.g. only minimal extra sorts) *) wenzelm@1238: wenzelm@3061: val force_strip_shyps = ref true; (* FIXME tmp (since 1995/08/01) *) wenzelm@1238: wenzelm@1238: (*remove extra sorts that are known to be syntactically non-empty*) wenzelm@1238: fun strip_shyps thm = wenzelm@1238: let paulson@1529: val Thm {sign, der, maxidx, shyps, hyps, prop} = thm; wenzelm@1238: val sorts = add_thm_sorts (thm, []); wenzelm@1238: val maybe_empty = not o Sign.nonempty_sort sign sorts; paulson@2177: val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps; wenzelm@1238: in paulson@1529: Thm {sign = sign, der = der, maxidx = maxidx, wenzelm@2386: shyps = wenzelm@2386: (if eq_set_sort (shyps',sorts) orelse wenzelm@2386: not (!force_strip_shyps) then shyps' wenzelm@3061: else (* FIXME tmp (since 1995/08/01) *) wenzelm@2386: (warning ("Removed sort hypotheses: " ^ wenzelm@2962: commas (map Sorts.str_of_sort (shyps' \\ sorts))); wenzelm@2386: warning "Let's hope these sorts are non-empty!"; wenzelm@1238: sorts)), paulson@1529: hyps = hyps, paulson@1529: prop = prop} wenzelm@1238: end; wenzelm@1238: wenzelm@1238: wenzelm@1238: (* implies_intr_shyps *) wenzelm@1238: wenzelm@1238: (*discharge all extra sort hypotheses*) wenzelm@1238: fun implies_intr_shyps thm = wenzelm@1238: (case extra_shyps thm of wenzelm@1238: [] => thm wenzelm@1238: | xshyps => wenzelm@1238: let paulson@1529: val Thm {sign, der, maxidx, shyps, hyps, prop} = thm; paulson@2182: val shyps' = ins_sort (logicS, shyps \\ xshyps); wenzelm@1238: val used_names = foldr add_term_tfree_names (prop :: hyps, []); wenzelm@1238: val names = wenzelm@1238: tl (variantlist (replicate (length xshyps + 1) "'", used_names)); wenzelm@1238: val tfrees = map (TFree o rpair logicS) names; wenzelm@1238: wenzelm@1238: fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S; paulson@2671: val sort_hyps = List.concat (map2 mk_insort (tfrees, xshyps)); wenzelm@1238: in paulson@1529: Thm {sign = sign, wenzelm@2386: der = infer_derivs (Implies_intr_shyps, [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = shyps', wenzelm@2386: hyps = hyps, wenzelm@2386: prop = Logic.list_implies (sort_hyps, prop)} wenzelm@1238: end); wenzelm@1238: wenzelm@1238: paulson@1529: (** Axioms **) wenzelm@387: wenzelm@387: (*look up the named axiom in the theory*) wenzelm@387: fun get_axiom theory name = wenzelm@387: let wenzelm@387: fun get_ax [] = raise Match paulson@1529: | get_ax (thy :: thys) = wenzelm@2386: let val {sign, new_axioms, parents, ...} = rep_theory thy paulson@1529: in case Symtab.lookup (new_axioms, name) of wenzelm@2386: Some t => fix_shyps [] [] wenzelm@2386: (Thm {sign = sign, wenzelm@2386: der = infer_derivs (Axiom(theory,name), []), wenzelm@2386: maxidx = maxidx_of_term t, wenzelm@2386: shyps = [], wenzelm@2386: hyps = [], wenzelm@2386: prop = t}) wenzelm@2386: | None => get_ax parents handle Match => get_ax thys paulson@1529: end; wenzelm@387: in wenzelm@387: get_ax [theory] handle Match wenzelm@387: => raise THEORY ("get_axiom: no axiom " ^ quote name, [theory]) wenzelm@387: end; wenzelm@387: paulson@1529: wenzelm@776: (*return additional axioms of this theory node*) wenzelm@776: fun axioms_of thy = wenzelm@776: map (fn (s, _) => (s, get_axiom thy s)) wenzelm@776: (Symtab.dest (#new_axioms (rep_theory thy))); wenzelm@776: paulson@1597: (*Attach a label to a theorem to make proof objects more readable*) paulson@1597: fun name_thm (name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = paulson@1597: Thm {sign = sign, wenzelm@2386: der = Join (Theorem name, [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = shyps, wenzelm@2386: hyps = hyps, wenzelm@2386: prop = prop}; clasohm@0: clasohm@0: paulson@1529: (*Compression of theorems -- a separate rule, not integrated with the others, paulson@1529: as it could be slow.*) paulson@1529: fun compress (Thm {sign, der, maxidx, shyps, hyps, prop}) = paulson@1529: Thm {sign = sign, wenzelm@2386: der = der, (*No derivation recorded!*) wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = shyps, wenzelm@2386: hyps = map Term.compress_term hyps, wenzelm@2386: prop = Term.compress_term prop}; wenzelm@564: wenzelm@387: wenzelm@2509: paulson@1529: (*** Meta rules ***) clasohm@0: paulson@2147: (*Check that term does not contain same var with different typing/sorting. paulson@2147: If this check must be made, recalculate maxidx in hope of preventing its paulson@2147: recurrence.*) paulson@2147: fun nodup_Vars (thm as Thm{sign, der, maxidx, shyps, hyps, prop}) s = paulson@2147: (Sign.nodup_Vars prop; paulson@2147: Thm {sign = sign, wenzelm@2386: der = der, wenzelm@2386: maxidx = maxidx_of_term prop, wenzelm@2386: shyps = shyps, wenzelm@2386: hyps = hyps, wenzelm@2386: prop = prop}) paulson@2147: handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts); nipkow@1495: wenzelm@1220: (** 'primitive' rules **) wenzelm@1220: wenzelm@1220: (*discharge all assumptions t from ts*) clasohm@0: val disch = gen_rem (op aconv); clasohm@0: wenzelm@1220: (*The assumption rule A|-A in a theory*) wenzelm@250: fun assume ct : thm = lcp@229: let val {sign, t=prop, T, maxidx} = rep_cterm ct wenzelm@250: in if T<>propT then wenzelm@250: raise THM("assume: assumptions must have type prop", 0, []) clasohm@0: else if maxidx <> ~1 then wenzelm@250: raise THM("assume: assumptions may not contain scheme variables", wenzelm@250: maxidx, []) paulson@1529: else Thm{sign = sign, wenzelm@2386: der = infer_derivs (Assume ct, []), wenzelm@2386: maxidx = ~1, wenzelm@2386: shyps = add_term_sorts(prop,[]), wenzelm@2386: hyps = [prop], wenzelm@2386: prop = prop} clasohm@0: end; clasohm@0: wenzelm@1220: (*Implication introduction wenzelm@1220: A |- B wenzelm@1220: ------- wenzelm@1220: A ==> B wenzelm@1220: *) paulson@1529: fun implies_intr cA (thB as Thm{sign,der,maxidx,hyps,prop,...}) : thm = lcp@229: let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA clasohm@0: in if T<>propT then wenzelm@250: raise THM("implies_intr: assumptions must have type prop", 0, [thB]) wenzelm@1238: else fix_shyps [thB] [] paulson@1529: (Thm{sign = Sign.merge (sign,signA), wenzelm@2386: der = infer_derivs (Implies_intr cA, [der]), wenzelm@2386: maxidx = Int.max(maxidxA, maxidx), wenzelm@2386: shyps = [], wenzelm@2386: hyps = disch(hyps,A), wenzelm@2386: prop = implies$A$prop}) clasohm@0: handle TERM _ => clasohm@0: raise THM("implies_intr: incompatible signatures", 0, [thB]) clasohm@0: end; clasohm@0: paulson@1529: wenzelm@1220: (*Implication elimination wenzelm@1220: A ==> B A wenzelm@1220: ------------ wenzelm@1220: B wenzelm@1220: *) clasohm@0: fun implies_elim thAB thA : thm = paulson@1529: let val Thm{maxidx=maxA, der=derA, hyps=hypsA, prop=propA,...} = thA paulson@1529: and Thm{sign, der, maxidx, hyps, prop,...} = thAB; wenzelm@250: fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) clasohm@0: in case prop of wenzelm@250: imp$A$B => wenzelm@250: if imp=implies andalso A aconv propA wenzelm@1220: then fix_shyps [thAB, thA] [] wenzelm@1220: (Thm{sign= merge_thm_sgs(thAB,thA), wenzelm@2386: der = infer_derivs (Implies_elim, [der,derA]), wenzelm@2386: maxidx = Int.max(maxA,maxidx), wenzelm@2386: shyps = [], wenzelm@2386: hyps = union_term(hypsA,hyps), (*dups suppressed*) wenzelm@2386: prop = B}) wenzelm@250: else err("major premise") wenzelm@250: | _ => err("major premise") clasohm@0: end; wenzelm@250: wenzelm@1220: (*Forall introduction. The Free or Var x must not be free in the hypotheses. wenzelm@1220: A wenzelm@1220: ----- wenzelm@1220: !!x.A wenzelm@1220: *) paulson@1529: fun forall_intr cx (th as Thm{sign,der,maxidx,hyps,prop,...}) = lcp@229: let val x = term_of cx; wenzelm@1238: fun result(a,T) = fix_shyps [th] [] paulson@1529: (Thm{sign = sign, wenzelm@2386: der = infer_derivs (Forall_intr cx, [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = [], wenzelm@2386: hyps = hyps, wenzelm@2386: prop = all(T) $ Abs(a, T, abstract_over (x,prop))}) clasohm@0: in case x of wenzelm@250: Free(a,T) => wenzelm@250: if exists (apl(x, Logic.occs)) hyps wenzelm@250: then raise THM("forall_intr: variable free in assumptions", 0, [th]) wenzelm@250: else result(a,T) clasohm@0: | Var((a,_),T) => result(a,T) clasohm@0: | _ => raise THM("forall_intr: not a variable", 0, [th]) clasohm@0: end; clasohm@0: wenzelm@1220: (*Forall elimination wenzelm@1220: !!x.A wenzelm@1220: ------ wenzelm@1220: A[t/x] wenzelm@1220: *) paulson@1529: fun forall_elim ct (th as Thm{sign,der,maxidx,hyps,prop,...}) : thm = lcp@229: let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct clasohm@0: in case prop of wenzelm@2386: Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => wenzelm@2386: if T<>qary then wenzelm@2386: raise THM("forall_elim: type mismatch", 0, [th]) wenzelm@2386: else let val thm = fix_shyps [th] [] wenzelm@2386: (Thm{sign= Sign.merge(sign,signt), wenzelm@2386: der = infer_derivs (Forall_elim ct, [der]), wenzelm@2386: maxidx = Int.max(maxidx, maxt), wenzelm@2386: shyps = [], wenzelm@2386: hyps = hyps, wenzelm@2386: prop = betapply(A,t)}) wenzelm@2386: in if maxt >= 0 andalso maxidx >= 0 wenzelm@2386: then nodup_Vars thm "forall_elim" wenzelm@2386: else thm (*no new Vars: no expensive check!*) wenzelm@2386: end paulson@2147: | _ => raise THM("forall_elim: not quantified", 0, [th]) clasohm@0: end clasohm@0: handle TERM _ => wenzelm@250: raise THM("forall_elim: incompatible signatures", 0, [th]); clasohm@0: clasohm@0: wenzelm@1220: (* Equality *) clasohm@0: wenzelm@1220: (* Definition of the relation =?= *) wenzelm@1238: val flexpair_def = fix_shyps [] [] paulson@1529: (Thm{sign= Sign.proto_pure, paulson@1597: der = Join(Axiom(pure_thy, "flexpair_def"), []), paulson@1529: shyps = [], paulson@1529: hyps = [], paulson@1529: maxidx = 0, paulson@1529: prop = term_of (read_cterm Sign.proto_pure wenzelm@2386: ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}); clasohm@0: clasohm@0: (*The reflexivity rule: maps t to the theorem t==t *) wenzelm@250: fun reflexive ct = lcp@229: let val {sign, t, T, maxidx} = rep_cterm ct wenzelm@1238: in fix_shyps [] [] paulson@1529: (Thm{sign= sign, wenzelm@2386: der = infer_derivs (Reflexive ct, []), wenzelm@2386: shyps = [], wenzelm@2386: hyps = [], wenzelm@2386: maxidx = maxidx, wenzelm@2386: prop = Logic.mk_equals(t,t)}) clasohm@0: end; clasohm@0: clasohm@0: (*The symmetry rule wenzelm@1220: t==u wenzelm@1220: ---- wenzelm@1220: u==t wenzelm@1220: *) paulson@1529: fun symmetric (th as Thm{sign,der,maxidx,shyps,hyps,prop}) = clasohm@0: case prop of clasohm@0: (eq as Const("==",_)) $ t $ u => wenzelm@1238: (*no fix_shyps*) wenzelm@2386: Thm{sign = sign, wenzelm@2386: der = infer_derivs (Symmetric, [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = shyps, wenzelm@2386: hyps = hyps, wenzelm@2386: prop = eq$u$t} clasohm@0: | _ => raise THM("symmetric", 0, [th]); clasohm@0: clasohm@0: (*The transitive rule wenzelm@1220: t1==u u==t2 wenzelm@1220: -------------- wenzelm@1220: t1==t2 wenzelm@1220: *) clasohm@0: fun transitive th1 th2 = paulson@1529: let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 paulson@1529: and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; clasohm@0: fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) clasohm@0: in case (prop1,prop2) of clasohm@0: ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) => nipkow@1634: if not (u aconv u') then err"middle term" nipkow@1634: else let val thm = wenzelm@1220: fix_shyps [th1, th2] [] paulson@1529: (Thm{sign= merge_thm_sgs(th1,th2), wenzelm@2386: der = infer_derivs (Transitive, [der1, der2]), paulson@2147: maxidx = Int.max(max1,max2), wenzelm@2386: shyps = [], wenzelm@2386: hyps = union_term(hyps1,hyps2), wenzelm@2386: prop = eq$t1$t2}) paulson@2139: in if max1 >= 0 andalso max2 >= 0 paulson@2147: then nodup_Vars thm "transitive" paulson@2147: else thm (*no new Vars: no expensive check!*) paulson@2139: end clasohm@0: | _ => err"premises" clasohm@0: end; clasohm@0: wenzelm@1160: (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *) wenzelm@250: fun beta_conversion ct = lcp@229: let val {sign, t, T, maxidx} = rep_cterm ct clasohm@0: in case t of wenzelm@1238: Abs(_,_,bodt) $ u => fix_shyps [] [] paulson@1529: (Thm{sign = sign, wenzelm@2386: der = infer_derivs (Beta_conversion ct, []), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = [], wenzelm@2386: hyps = [], wenzelm@2386: prop = Logic.mk_equals(t, subst_bound (u,bodt))}) wenzelm@250: | _ => raise THM("beta_conversion: not a redex", 0, []) clasohm@0: end; clasohm@0: clasohm@0: (*The extensionality rule (proviso: x not free in f, g, or hypotheses) wenzelm@1220: f(x) == g(x) wenzelm@1220: ------------ wenzelm@1220: f == g wenzelm@1220: *) paulson@1529: fun extensional (th as Thm{sign, der, maxidx,shyps,hyps,prop}) = clasohm@0: case prop of clasohm@0: (Const("==",_)) $ (f$x) $ (g$y) => wenzelm@250: let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) clasohm@0: in (if x<>y then err"different variables" else clasohm@0: case y of wenzelm@250: Free _ => wenzelm@250: if exists (apl(y, Logic.occs)) (f::g::hyps) wenzelm@250: then err"variable free in hyps or functions" else () wenzelm@250: | Var _ => wenzelm@250: if Logic.occs(y,f) orelse Logic.occs(y,g) wenzelm@250: then err"variable free in functions" else () wenzelm@250: | _ => err"not a variable"); wenzelm@1238: (*no fix_shyps*) paulson@1529: Thm{sign = sign, wenzelm@2386: der = infer_derivs (Extensional, [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = shyps, wenzelm@2386: hyps = hyps, paulson@1529: prop = Logic.mk_equals(f,g)} clasohm@0: end clasohm@0: | _ => raise THM("extensional: premise", 0, [th]); clasohm@0: clasohm@0: (*The abstraction rule. The Free or Var x must not be free in the hypotheses. clasohm@0: The bound variable will be named "a" (since x will be something like x320) wenzelm@1220: t == u wenzelm@1220: ------------ wenzelm@1220: %x.t == %x.u wenzelm@1220: *) paulson@1529: fun abstract_rule a cx (th as Thm{sign,der,maxidx,hyps,prop,...}) = lcp@229: let val x = term_of cx; wenzelm@250: val (t,u) = Logic.dest_equals prop wenzelm@250: handle TERM _ => wenzelm@250: raise THM("abstract_rule: premise not an equality", 0, [th]) wenzelm@1238: fun result T = fix_shyps [th] [] wenzelm@2386: (Thm{sign = sign, wenzelm@2386: der = infer_derivs (Abstract_rule (a,cx), [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = [], wenzelm@2386: hyps = hyps, wenzelm@2386: prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)), wenzelm@2386: Abs(a, T, abstract_over (x,u)))}) clasohm@0: in case x of wenzelm@250: Free(_,T) => wenzelm@250: if exists (apl(x, Logic.occs)) hyps wenzelm@250: then raise THM("abstract_rule: variable free in assumptions", 0, [th]) wenzelm@250: else result T clasohm@0: | Var(_,T) => result T clasohm@0: | _ => raise THM("abstract_rule: not a variable", 0, [th]) clasohm@0: end; clasohm@0: clasohm@0: (*The combination rule wenzelm@1220: f==g t==u wenzelm@1220: ------------ wenzelm@1220: f(t)==g(u) wenzelm@1220: *) clasohm@0: fun combination th1 th2 = paulson@1529: let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, wenzelm@2386: prop=prop1,...} = th1 paulson@1529: and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, wenzelm@2386: prop=prop2,...} = th2 paulson@1836: fun chktypes (f,t) = wenzelm@2386: (case fastype_of f of wenzelm@2386: Type("fun",[T1,T2]) => wenzelm@2386: if T1 <> fastype_of t then wenzelm@2386: raise THM("combination: types", 0, [th1,th2]) wenzelm@2386: else () wenzelm@2386: | _ => raise THM("combination: not function type", 0, wenzelm@2386: [th1,th2])) nipkow@1495: in case (prop1,prop2) of clasohm@0: (Const("==",_) $ f $ g, Const("==",_) $ t $ u) => paulson@1836: let val _ = chktypes (f,t) wenzelm@2386: val thm = (*no fix_shyps*) wenzelm@2386: Thm{sign = merge_thm_sgs(th1,th2), wenzelm@2386: der = infer_derivs (Combination, [der1, der2]), wenzelm@2386: maxidx = Int.max(max1,max2), wenzelm@2386: shyps = union_sort(shyps1,shyps2), wenzelm@2386: hyps = union_term(hyps1,hyps2), wenzelm@2386: prop = Logic.mk_equals(f$t, g$u)} paulson@2139: in if max1 >= 0 andalso max2 >= 0 paulson@2139: then nodup_Vars thm "combination" wenzelm@2386: else thm (*no new Vars: no expensive check!*) paulson@2139: end clasohm@0: | _ => raise THM("combination: premises", 0, [th1,th2]) clasohm@0: end; clasohm@0: clasohm@0: clasohm@0: (* Equality introduction wenzelm@1220: A==>B B==>A wenzelm@1220: -------------- wenzelm@1220: A==B wenzelm@1220: *) clasohm@0: fun equal_intr th1 th2 = paulson@1529: let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, wenzelm@2386: prop=prop1,...} = th1 paulson@1529: and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, wenzelm@2386: prop=prop2,...} = th2; paulson@1529: fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) paulson@1529: in case (prop1,prop2) of paulson@1529: (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') => wenzelm@2386: if A aconv A' andalso B aconv B' wenzelm@2386: then wenzelm@2386: (*no fix_shyps*) wenzelm@2386: Thm{sign = merge_thm_sgs(th1,th2), wenzelm@2386: der = infer_derivs (Equal_intr, [der1, der2]), wenzelm@2386: maxidx = Int.max(max1,max2), wenzelm@2386: shyps = union_sort(shyps1,shyps2), wenzelm@2386: hyps = union_term(hyps1,hyps2), wenzelm@2386: prop = Logic.mk_equals(A,B)} wenzelm@2386: else err"not equal" paulson@1529: | _ => err"premises" paulson@1529: end; paulson@1529: paulson@1529: paulson@1529: (*The equal propositions rule paulson@1529: A==B A paulson@1529: --------- paulson@1529: B paulson@1529: *) paulson@1529: fun equal_elim th1 th2 = paulson@1529: let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 paulson@1529: and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; paulson@1529: fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) paulson@1529: in case prop1 of paulson@1529: Const("==",_) $ A $ B => paulson@1529: if not (prop2 aconv A) then err"not equal" else paulson@1529: fix_shyps [th1, th2] [] paulson@1529: (Thm{sign= merge_thm_sgs(th1,th2), wenzelm@2386: der = infer_derivs (Equal_elim, [der1, der2]), wenzelm@2386: maxidx = Int.max(max1,max2), wenzelm@2386: shyps = [], wenzelm@2386: hyps = union_term(hyps1,hyps2), wenzelm@2386: prop = B}) paulson@1529: | _ => err"major premise" paulson@1529: end; clasohm@0: wenzelm@1220: wenzelm@1220: clasohm@0: (**** Derived rules ****) clasohm@0: paulson@1503: (*Discharge all hypotheses. Need not verify cterms or call fix_shyps. clasohm@0: Repeated hypotheses are discharged only once; fold cannot do this*) paulson@1529: fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) = wenzelm@1238: implies_intr_hyps (*no fix_shyps*) paulson@1529: (Thm{sign = sign, wenzelm@2386: der = infer_derivs (Implies_intr_hyps, [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = shyps, paulson@1529: hyps = disch(As,A), wenzelm@2386: prop = implies$A$prop}) clasohm@0: | implies_intr_hyps th = th; clasohm@0: clasohm@0: (*Smash" unifies the list of term pairs leaving no flex-flex pairs. wenzelm@250: Instantiates the theorem and deletes trivial tpairs. clasohm@0: Resulting sequence may contain multiple elements if the tpairs are clasohm@0: not all flex-flex. *) paulson@1529: fun flexflex_rule (th as Thm{sign, der, maxidx, hyps, prop,...}) = wenzelm@250: let fun newthm env = paulson@1529: if Envir.is_empty env then th paulson@1529: else wenzelm@250: let val (tpairs,horn) = wenzelm@250: Logic.strip_flexpairs (Envir.norm_term env prop) wenzelm@250: (*Remove trivial tpairs, of the form t=t*) wenzelm@250: val distpairs = filter (not o op aconv) tpairs wenzelm@250: val newprop = Logic.list_flexpairs(distpairs, horn) wenzelm@1220: in fix_shyps [th] (env_codT env) paulson@1529: (Thm{sign = sign, wenzelm@2386: der = infer_derivs (Flexflex_rule env, [der]), wenzelm@2386: maxidx = maxidx_of_term newprop, wenzelm@2386: shyps = [], wenzelm@2386: hyps = hyps, wenzelm@2386: prop = newprop}) wenzelm@250: end; clasohm@0: val (tpairs,_) = Logic.strip_flexpairs prop clasohm@0: in Sequence.maps newthm wenzelm@250: (Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) clasohm@0: end; clasohm@0: clasohm@0: (*Instantiation of Vars wenzelm@1220: A wenzelm@1220: ------------------- wenzelm@1220: A[t1/v1,....,tn/vn] wenzelm@1220: *) clasohm@0: clasohm@0: (*Check that all the terms are Vars and are distinct*) clasohm@0: fun instl_ok ts = forall is_Var ts andalso null(findrep ts); clasohm@0: clasohm@0: (*For instantiate: process pair of cterms, merge theories*) clasohm@0: fun add_ctpair ((ct,cu), (sign,tpairs)) = lcp@229: let val {sign=signt, t=t, T= T, ...} = rep_cterm ct lcp@229: and {sign=signu, t=u, T= U, ...} = rep_cterm cu clasohm@0: in if T=U then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs) clasohm@0: else raise TYPE("add_ctpair", [T,U], [t,u]) clasohm@0: end; clasohm@0: clasohm@0: fun add_ctyp ((v,ctyp), (sign',vTs)) = lcp@229: let val {T,sign} = rep_ctyp ctyp clasohm@0: in (Sign.merge(sign,sign'), (v,T)::vTs) end; clasohm@0: clasohm@0: (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. clasohm@0: Instantiates distinct Vars by terms of same type. clasohm@0: Normalizes the new theorem! *) paulson@1529: fun instantiate ([], []) th = th paulson@1529: | instantiate (vcTs,ctpairs) (th as Thm{sign,der,maxidx,hyps,prop,...}) = clasohm@0: let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[])); clasohm@0: val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[])); wenzelm@250: val newprop = wenzelm@250: Envir.norm_term (Envir.empty 0) wenzelm@250: (subst_atomic tpairs wenzelm@250: (Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop)) wenzelm@1220: val newth = wenzelm@1220: fix_shyps [th] (map snd vTs) paulson@1529: (Thm{sign = newsign, wenzelm@2386: der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), wenzelm@2386: maxidx = maxidx_of_term newprop, wenzelm@2386: shyps = [], wenzelm@2386: hyps = hyps, wenzelm@2386: prop = newprop}) wenzelm@250: in if not(instl_ok(map #1 tpairs)) nipkow@193: then raise THM("instantiate: variables not distinct", 0, [th]) nipkow@193: else if not(null(findrep(map #1 vTs))) nipkow@193: then raise THM("instantiate: type variables not distinct", 0, [th]) paulson@2147: else nodup_Vars newth "instantiate" clasohm@0: end wenzelm@250: handle TERM _ => clasohm@0: raise THM("instantiate: incompatible signatures",0,[th]) paulson@2671: | TYPE (msg,_,_) => raise THM("instantiate: type conflict: " ^ msg, paulson@2671: 0, [th]); clasohm@0: clasohm@0: (*The trivial implication A==>A, justified by assume and forall rules. clasohm@0: A can contain Vars, not so for assume! *) wenzelm@250: fun trivial ct : thm = lcp@229: let val {sign, t=A, T, maxidx} = rep_cterm ct wenzelm@250: in if T<>propT then wenzelm@250: raise THM("trivial: the term must have type prop", 0, []) wenzelm@1238: else fix_shyps [] [] paulson@1529: (Thm{sign = sign, wenzelm@2386: der = infer_derivs (Trivial ct, []), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = [], wenzelm@2386: hyps = [], wenzelm@2386: prop = implies$A$A}) clasohm@0: end; clasohm@0: paulson@1503: (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) wenzelm@399: fun class_triv thy c = paulson@1529: let val sign = sign_of thy; paulson@1529: val Cterm {t, maxidx, ...} = wenzelm@2386: cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) wenzelm@2386: handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); wenzelm@399: in wenzelm@1238: fix_shyps [] [] paulson@1529: (Thm {sign = sign, wenzelm@2386: der = infer_derivs (Class_triv(thy,c), []), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = [], wenzelm@2386: hyps = [], wenzelm@2386: prop = t}) wenzelm@399: end; wenzelm@399: wenzelm@399: clasohm@0: (* Replace all TFrees not in the hyps by new TVars *) paulson@1529: fun varifyT(Thm{sign,der,maxidx,shyps,hyps,prop}) = clasohm@0: let val tfrees = foldr add_term_tfree_names (hyps,[]) nipkow@1634: in let val thm = (*no fix_shyps*) paulson@1529: Thm{sign = sign, wenzelm@2386: der = infer_derivs (VarifyT, [der]), wenzelm@2386: maxidx = Int.max(0,maxidx), wenzelm@2386: shyps = shyps, wenzelm@2386: hyps = hyps, paulson@1529: prop = Type.varify(prop,tfrees)} paulson@2147: in nodup_Vars thm "varifyT" end nipkow@1634: (* this nodup_Vars check can be removed if thms are guaranteed not to contain nipkow@1634: duplicate TVars with differnt sorts *) clasohm@0: end; clasohm@0: clasohm@0: (* Replace all TVars by new TFrees *) paulson@1529: fun freezeT(Thm{sign,der,maxidx,shyps,hyps,prop}) = nipkow@949: let val prop' = Type.freeze prop wenzelm@1238: in (*no fix_shyps*) paulson@1529: Thm{sign = sign, wenzelm@2386: der = infer_derivs (FreezeT, [der]), wenzelm@2386: maxidx = maxidx_of_term prop', wenzelm@2386: shyps = shyps, wenzelm@2386: hyps = hyps, paulson@1529: prop = prop'} wenzelm@1220: end; clasohm@0: clasohm@0: clasohm@0: (*** Inference rules for tactics ***) clasohm@0: clasohm@0: (*Destruct proof state into constraints, other goals, goal(i), rest *) clasohm@0: fun dest_state (state as Thm{prop,...}, i) = clasohm@0: let val (tpairs,horn) = Logic.strip_flexpairs prop clasohm@0: in case Logic.strip_prems(i, [], horn) of clasohm@0: (B::rBs, C) => (tpairs, rev rBs, B, C) clasohm@0: | _ => raise THM("dest_state", i, [state]) clasohm@0: end clasohm@0: handle TERM _ => raise THM("dest_state", i, [state]); clasohm@0: lcp@309: (*Increment variables and parameters of orule as required for clasohm@0: resolution with goal i of state. *) clasohm@0: fun lift_rule (state, i) orule = paulson@1529: let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign=ssign,...} = state clasohm@0: val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) paulson@1529: handle TERM _ => raise THM("lift_rule", i, [orule,state]) paulson@1529: val ct_Bi = Cterm {sign=ssign, maxidx=smax, T=propT, t=Bi} paulson@1529: val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) paulson@1529: val (Thm{sign, der, maxidx,shyps,hyps,prop}) = orule clasohm@0: val (tpairs,As,B) = Logic.strip_horn prop wenzelm@1238: in (*no fix_shyps*) paulson@1529: Thm{sign = merge_thm_sgs(state,orule), wenzelm@2386: der = infer_derivs (Lift_rule(ct_Bi, i), [der]), wenzelm@2386: maxidx = maxidx+smax+1, paulson@2177: shyps=union_sort(sshyps,shyps), wenzelm@2386: hyps=hyps, paulson@1529: prop = Logic.rule_of (map (pairself lift_abs) tpairs, wenzelm@2386: map lift_all As, wenzelm@2386: lift_all B)} clasohm@0: end; clasohm@0: clasohm@0: (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) clasohm@0: fun assumption i state = paulson@1529: let val Thm{sign,der,maxidx,hyps,prop,...} = state; clasohm@0: val (tpairs, Bs, Bi, C) = dest_state(state,i) wenzelm@250: fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = wenzelm@1220: fix_shyps [state] (env_codT env) paulson@1529: (Thm{sign = sign, wenzelm@2386: der = infer_derivs (Assumption (i, Some env), [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = [], wenzelm@2386: hyps = hyps, wenzelm@2386: prop = wenzelm@2386: if Envir.is_empty env then (*avoid wasted normalizations*) wenzelm@2386: Logic.rule_of (tpairs, Bs, C) wenzelm@2386: else (*normalize the new rule fully*) wenzelm@2386: Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))}); clasohm@0: fun addprfs [] = Sequence.null clasohm@0: | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull clasohm@0: (Sequence.mapp newth wenzelm@250: (Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs)) wenzelm@250: (addprfs apairs))) clasohm@0: in addprfs (Logic.assum_pairs Bi) end; clasohm@0: wenzelm@250: (*Solve subgoal Bi of proof state B1...Bn/C by assumption. clasohm@0: Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) clasohm@0: fun eq_assumption i state = paulson@1529: let val Thm{sign,der,maxidx,hyps,prop,...} = state; clasohm@0: val (tpairs, Bs, Bi, C) = dest_state(state,i) clasohm@0: in if exists (op aconv) (Logic.assum_pairs Bi) wenzelm@1220: then fix_shyps [state] [] paulson@1529: (Thm{sign = sign, wenzelm@2386: der = infer_derivs (Assumption (i,None), [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = [], wenzelm@2386: hyps = hyps, wenzelm@2386: prop = Logic.rule_of(tpairs, Bs, C)}) clasohm@0: else raise THM("eq_assumption", 0, [state]) clasohm@0: end; clasohm@0: clasohm@0: paulson@2671: (*For rotate_tac: fast rotation of assumptions of subgoal i*) paulson@2671: fun rotate_rule k i state = paulson@2671: let val Thm{sign,der,maxidx,hyps,prop,shyps} = state; paulson@2671: val (tpairs, Bs, Bi, C) = dest_state(state,i) paulson@2671: val params = Logic.strip_params Bi paulson@2671: and asms = Logic.strip_assums_hyp Bi paulson@2671: and concl = Logic.strip_assums_concl Bi paulson@2671: val n = length asms paulson@2671: fun rot m = if 0=m orelse m=n then Bi paulson@2671: else if 0 error ("Bound variables not distinct: " ^ c) berghofe@1576: | [] => (case cs inter_string freenames of clasohm@0: a::_ => error ("Bound/Free variable clash: " ^ a) wenzelm@1220: | [] => fix_shyps [state] [] wenzelm@2386: (Thm{sign = sign, wenzelm@2386: der = infer_derivs (Rename_params_rule(cs,i), [der]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = [], wenzelm@2386: hyps = hyps, wenzelm@2386: prop = Logic.rule_of(tpairs, Bs@[newBi], C)})) clasohm@0: end; clasohm@0: clasohm@0: (*** Preservation of bound variable names ***) clasohm@0: wenzelm@250: (*Scan a pair of terms; while they are similar, clasohm@0: accumulate corresponding bound vars in "al"*) wenzelm@1238: fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = lcp@1195: match_bvs(s, t, if x="" orelse y="" then al wenzelm@1238: else (x,y)::al) clasohm@0: | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) clasohm@0: | match_bvs(_,_,al) = al; clasohm@0: clasohm@0: (* strip abstractions created by parameters *) clasohm@0: fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); clasohm@0: clasohm@0: wenzelm@250: (* strip_apply f A(,B) strips off all assumptions/parameters from A clasohm@0: introduced by lifting over B, and applies f to remaining part of A*) clasohm@0: fun strip_apply f = clasohm@0: let fun strip(Const("==>",_)$ A1 $ B1, wenzelm@250: Const("==>",_)$ _ $ B2) = implies $ A1 $ strip(B1,B2) wenzelm@250: | strip((c as Const("all",_)) $ Abs(a,T,t1), wenzelm@250: Const("all",_) $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2)) wenzelm@250: | strip(A,_) = f A clasohm@0: in strip end; clasohm@0: clasohm@0: (*Use the alist to rename all bound variables and some unknowns in a term clasohm@0: dpairs = current disagreement pairs; tpairs = permanent ones (flexflex); clasohm@0: Preserves unknowns in tpairs and on lhs of dpairs. *) clasohm@0: fun rename_bvs([],_,_,_) = I clasohm@0: | rename_bvs(al,dpairs,tpairs,B) = wenzelm@250: let val vars = foldr add_term_vars wenzelm@250: (map fst dpairs @ map fst tpairs @ map snd tpairs, []) wenzelm@250: (*unknowns appearing elsewhere be preserved!*) wenzelm@250: val vids = map (#1 o #1 o dest_Var) vars; wenzelm@250: fun rename(t as Var((x,i),T)) = wenzelm@250: (case assoc(al,x) of berghofe@1576: Some(y) => if x mem_string vids orelse y mem_string vids then t wenzelm@250: else Var((y,i),T) wenzelm@250: | None=> t) clasohm@0: | rename(Abs(x,T,t)) = berghofe@1576: Abs(case assoc_string(al,x) of Some(y) => y | None => x, wenzelm@250: T, rename t) clasohm@0: | rename(f$t) = rename f $ rename t clasohm@0: | rename(t) = t; wenzelm@250: fun strip_ren Ai = strip_apply rename (Ai,B) clasohm@0: in strip_ren end; clasohm@0: clasohm@0: (*Function to rename bounds/unknowns in the argument, lifted over B*) clasohm@0: fun rename_bvars(dpairs, tpairs, B) = wenzelm@250: rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); clasohm@0: clasohm@0: clasohm@0: (*** RESOLUTION ***) clasohm@0: lcp@721: (** Lifting optimizations **) lcp@721: clasohm@0: (*strip off pairs of assumptions/parameters in parallel -- they are clasohm@0: identical because of lifting*) wenzelm@250: fun strip_assums2 (Const("==>", _) $ _ $ B1, wenzelm@250: Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) clasohm@0: | strip_assums2 (Const("all",_)$Abs(a,T,t1), wenzelm@250: Const("all",_)$Abs(_,_,t2)) = clasohm@0: let val (B1,B2) = strip_assums2 (t1,t2) clasohm@0: in (Abs(a,T,B1), Abs(a,T,B2)) end clasohm@0: | strip_assums2 BB = BB; clasohm@0: clasohm@0: lcp@721: (*Faster normalization: skip assumptions that were lifted over*) lcp@721: fun norm_term_skip env 0 t = Envir.norm_term env t lcp@721: | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) = lcp@721: let val Envir.Envir{iTs, ...} = env wenzelm@1238: val T' = typ_subst_TVars iTs T wenzelm@1238: (*Must instantiate types of parameters because they are flattened; lcp@721: this could be a NEW parameter*) lcp@721: in all T' $ Abs(a, T', norm_term_skip env n t) end lcp@721: | norm_term_skip env n (Const("==>", _) $ A $ B) = wenzelm@1238: implies $ A $ norm_term_skip env (n-1) B lcp@721: | norm_term_skip env n t = error"norm_term_skip: too few assumptions??"; lcp@721: lcp@721: clasohm@0: (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) wenzelm@250: Unifies B with Bi, replacing subgoal i (1 <= i <= n) clasohm@0: If match then forbid instantiations in proof state clasohm@0: If lifted then shorten the dpair using strip_assums2. clasohm@0: If eres_flg then simultaneously proves A1 by assumption. wenzelm@250: nsubgoal is the number of new subgoals (written m above). clasohm@0: Curried so that resolution calls dest_state only once. clasohm@0: *) paulson@1529: local open Sequence; exception COMPOSE clasohm@0: in wenzelm@250: fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) clasohm@0: (eres_flg, orule, nsubgoal) = paulson@1529: let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state paulson@1529: and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, wenzelm@2386: prop=rprop,...} = orule paulson@1529: (*How many hyps to skip over during normalization*) wenzelm@1238: and nlift = Logic.count_prems(strip_all_body Bi, wenzelm@1238: if eres_flg then ~1 else 0) wenzelm@387: val sign = merge_thm_sgs(state,orule); clasohm@0: (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **) wenzelm@250: fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = wenzelm@250: let val normt = Envir.norm_term env; wenzelm@250: (*perform minimal copying here by examining env*) wenzelm@250: val normp = wenzelm@250: if Envir.is_empty env then (tpairs, Bs @ As, C) wenzelm@250: else wenzelm@250: let val ntps = map (pairself normt) tpairs paulson@2147: in if Envir.above (smax, env) then wenzelm@1238: (*no assignments in state; normalize the rule only*) wenzelm@1238: if lifted wenzelm@1238: then (ntps, Bs @ map (norm_term_skip env nlift) As, C) wenzelm@1238: else (ntps, Bs @ map normt As, C) paulson@1529: else if match then raise COMPOSE wenzelm@250: else (*normalize the new rule fully*) wenzelm@250: (ntps, map normt (Bs @ As), normt C) wenzelm@250: end wenzelm@1258: val th = (*tuned fix_shyps*) paulson@1529: Thm{sign = sign, wenzelm@2386: der = infer_derivs (Bicompose(match, eres_flg, wenzelm@2386: 1 + length Bs, nsubgoal, env), wenzelm@2386: [rder,sder]), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = add_env_sorts (env, union_sort(rshyps,sshyps)), wenzelm@2386: hyps = union_term(rhyps,shyps), wenzelm@2386: prop = Logic.rule_of normp} paulson@1529: in cons(th, thq) end handle COMPOSE => thq clasohm@0: val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); clasohm@0: val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) clasohm@0: handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); clasohm@0: (*Modify assumptions, deleting n-th if n>0 for e-resolution*) clasohm@0: fun newAs(As0, n, dpairs, tpairs) = clasohm@0: let val As1 = if !Logic.auto_rename orelse not lifted then As0 wenzelm@250: else map (rename_bvars(dpairs,tpairs,B)) As0 clasohm@0: in (map (Logic.flatten_params n) As1) wenzelm@250: handle TERM _ => wenzelm@250: raise THM("bicompose: 1st premise", 0, [orule]) clasohm@0: end; paulson@2147: val env = Envir.empty(Int.max(rmax,smax)); clasohm@0: val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); clasohm@0: val dpairs = BBi :: (rtpairs@stpairs); clasohm@0: (*elim-resolution: try each assumption in turn. Initially n=1*) clasohm@0: fun tryasms (_, _, []) = null clasohm@0: | tryasms (As, n, (t,u)::apairs) = wenzelm@250: (case pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of wenzelm@250: None => tryasms (As, n+1, apairs) wenzelm@250: | cell as Some((_,tpairs),_) => wenzelm@250: its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs))) wenzelm@250: (seqof (fn()=> cell), wenzelm@250: seqof (fn()=> pull (tryasms (As, n+1, apairs))))); clasohm@0: fun eres [] = raise THM("bicompose: no premises", 0, [orule,state]) clasohm@0: | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1); clasohm@0: (*ordinary resolution*) clasohm@0: fun res(None) = null wenzelm@250: | res(cell as Some((_,tpairs),_)) = wenzelm@250: its_right (addth(newAs(rev rAs, 0, [BBi], tpairs))) wenzelm@250: (seqof (fn()=> cell), null) clasohm@0: in if eres_flg then eres(rev rAs) clasohm@0: else res(pull(Unify.unifiers(sign, env, dpairs))) clasohm@0: end; clasohm@0: end; (*open Sequence*) clasohm@0: clasohm@0: clasohm@0: fun bicompose match arg i state = clasohm@0: bicompose_aux match (state, dest_state(state,i), false) arg; clasohm@0: clasohm@0: (*Quick test whether rule is resolvable with the subgoal with hyps Hs clasohm@0: and conclusion B. If eres_flg then checks 1st premise of rule also*) clasohm@0: fun could_bires (Hs, B, eres_flg, rule) = clasohm@0: let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs wenzelm@250: | could_reshyp [] = false; (*no premise -- illegal*) wenzelm@250: in could_unify(concl_of rule, B) andalso wenzelm@250: (not eres_flg orelse could_reshyp (prems_of rule)) clasohm@0: end; clasohm@0: clasohm@0: (*Bi-resolution of a state with a list of (flag,rule) pairs. clasohm@0: Puts the rule above: rule/state. Renames vars in the rules. *) wenzelm@250: fun biresolution match brules i state = clasohm@0: let val lift = lift_rule(state, i); wenzelm@250: val (stpairs, Bs, Bi, C) = dest_state(state,i) wenzelm@250: val B = Logic.strip_assums_concl Bi; wenzelm@250: val Hs = Logic.strip_assums_hyp Bi; wenzelm@250: val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true); wenzelm@250: fun res [] = Sequence.null wenzelm@250: | res ((eres_flg, rule)::brules) = wenzelm@250: if could_bires (Hs, B, eres_flg, rule) wenzelm@1160: then Sequence.seqof (*delay processing remainder till needed*) wenzelm@250: (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule), wenzelm@250: res brules)) wenzelm@250: else res brules clasohm@0: in Sequence.flats (res brules) end; clasohm@0: clasohm@0: clasohm@0: wenzelm@2509: (*** Meta Simplification ***) clasohm@0: wenzelm@2509: (** diagnostics **) clasohm@0: clasohm@0: exception SIMPLIFIER of string * thm; clasohm@0: wenzelm@2509: fun prtm a sign t = (writeln a; writeln (Sign.string_of_term sign t)); berghofe@1580: fun prtm_warning a sign t = warning (a ^ "\n" ^ (Sign.string_of_term sign t)); berghofe@1580: nipkow@209: val trace_simp = ref false; nipkow@209: wenzelm@2509: fun trace_warning a = if ! trace_simp then warning a else (); wenzelm@2509: fun trace_term a sign t = if ! trace_simp then prtm a sign t else (); wenzelm@2509: fun trace_term_warning a sign t = if ! trace_simp then prtm_warning a sign t else (); wenzelm@2509: fun trace_thm a (Thm {sign, prop, ...}) = trace_term a sign prop; wenzelm@2509: fun trace_thm_warning a (Thm {sign, prop, ...}) = trace_term_warning a sign prop; nipkow@209: nipkow@209: berghofe@1580: wenzelm@2509: (** meta simp sets **) wenzelm@2509: wenzelm@2509: (* basic components *) berghofe@1580: wenzelm@2509: type rrule = {thm: thm, lhs: term, perm: bool}; wenzelm@2509: type cong = {thm: thm, lhs: term}; wenzelm@2509: type simproc = (Sign.sg -> term -> thm option) * stamp; nipkow@288: wenzelm@2509: fun eq_rrule ({thm = Thm{prop = p1, ...}, ...}: rrule, wenzelm@2509: {thm = Thm {prop = p2, ...}, ...}: rrule) = p1 aconv p2; wenzelm@2509: wenzelm@2509: val eq_simproc = eq_snd; wenzelm@2509: wenzelm@2509: wenzelm@2509: (* datatype mss *) nipkow@288: wenzelm@2509: (* wenzelm@2509: A "mss" contains data needed during conversion: wenzelm@2509: rules: discrimination net of rewrite rules; wenzelm@2509: congs: association list of congruence rules; wenzelm@2509: procs: discrimination net of simplification procedures wenzelm@2509: (functions that prove rewrite rules on the fly); wenzelm@2509: bounds: names of bound variables already used wenzelm@2509: (for generating new names when rewriting under lambda abstractions); wenzelm@2509: prems: current premises; wenzelm@2509: mk_rews: turns simplification thms into rewrite rules; wenzelm@2509: termless: relation for ordered rewriting; nipkow@1028: *) clasohm@0: wenzelm@2509: datatype meta_simpset = wenzelm@2509: Mss of { wenzelm@2509: rules: rrule Net.net, wenzelm@2509: congs: (string * cong) list, wenzelm@2509: procs: simproc Net.net, wenzelm@2509: bounds: string list, wenzelm@2509: prems: thm list, wenzelm@2509: mk_rews: thm -> thm list, wenzelm@2509: termless: term * term -> bool}; wenzelm@2509: wenzelm@2509: fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless) = wenzelm@2509: Mss {rules = rules, congs = congs, procs = procs, bounds = bounds, wenzelm@2509: prems = prems, mk_rews = mk_rews, termless = termless}; wenzelm@2509: wenzelm@2509: val empty_mss = wenzelm@2509: mk_mss (Net.empty, [], Net.empty, [], [], K [], Logic.termless); wenzelm@2509: wenzelm@2509: wenzelm@2509: wenzelm@2509: (** simpset operations **) wenzelm@2509: wenzelm@2509: (* mk_rrule *) wenzelm@2509: wenzelm@2509: fun vperm (Var _, Var _) = true wenzelm@2509: | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) wenzelm@2509: | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) wenzelm@2509: | vperm (t, u) = (t = u); wenzelm@2509: wenzelm@2509: fun var_perm (t, u) = wenzelm@2509: vperm (t, u) andalso eq_set_term (term_vars t, term_vars u); wenzelm@2509: wenzelm@2509: (*simple test for looping rewrite*) wenzelm@2509: fun loops sign prems (lhs, rhs) = nipkow@2792: is_Var (head_of lhs) wenzelm@2509: orelse wenzelm@2509: (exists (apl (lhs, Logic.occs)) (rhs :: prems)) wenzelm@2509: orelse wenzelm@2509: (null prems andalso wenzelm@2509: Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs)); wenzelm@2509: (*the condition "null prems" in the last case is necessary because wenzelm@2509: conditional rewrites with extra variables in the conditions may terminate wenzelm@2509: although the rhs is an instance of the lhs. Example: wenzelm@2509: ?m < ?n ==> f(?n) == f(?m)*) wenzelm@2509: wenzelm@2509: fun mk_rrule (thm as Thm {sign, prop, ...}) = wenzelm@1238: let wenzelm@2509: val prems = Logic.strip_imp_prems prop; wenzelm@2509: val concl = Logic.strip_imp_concl prop; wenzelm@2509: val (lhs, _) = Logic.dest_equals concl handle TERM _ => wenzelm@2509: raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm); wenzelm@2509: val econcl = Pattern.eta_contract concl; wenzelm@2509: val (elhs, erhs) = Logic.dest_equals econcl; wenzelm@2509: val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs) wenzelm@2509: andalso not (is_Var elhs); wenzelm@2509: in wenzelm@2509: if not ((term_vars erhs) subset paulson@2671: (union_term (term_vars elhs, List.concat(map term_vars prems)))) then wenzelm@2509: (prtm_warning "extra Var(s) on rhs" sign prop; None) wenzelm@2509: else if not perm andalso loops sign prems (elhs, erhs) then wenzelm@2509: (prtm_warning "ignoring looping rewrite rule" sign prop; None) wenzelm@2509: else Some {thm = thm, lhs = lhs, perm = perm} clasohm@0: end; clasohm@0: wenzelm@2509: wenzelm@2509: (* add_simps *) nipkow@87: wenzelm@2509: fun add_simp wenzelm@2509: (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, wenzelm@2509: thm as Thm {sign, prop, ...}) = wenzelm@2509: (case mk_rrule thm of nipkow@87: None => mss wenzelm@2509: | Some (rrule as {lhs, ...}) => nipkow@209: (trace_thm "Adding rewrite rule:" thm; wenzelm@2509: mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule) handle Net.INSERT => wenzelm@2509: (prtm_warning "ignoring duplicate rewrite rule" sign prop; rules), wenzelm@2509: congs, procs, bounds, prems, mk_rews, termless))); clasohm@0: clasohm@0: val add_simps = foldl add_simp; wenzelm@2509: wenzelm@2509: fun mss_of thms = add_simps (empty_mss, thms); wenzelm@2509: wenzelm@2509: wenzelm@2509: (* del_simps *) wenzelm@2509: wenzelm@2509: fun del_simp wenzelm@2509: (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, wenzelm@2509: thm as Thm {sign, prop, ...}) = wenzelm@2509: (case mk_rrule thm of wenzelm@2509: None => mss wenzelm@2509: | Some (rrule as {lhs, ...}) => wenzelm@2509: mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule) handle Net.DELETE => wenzelm@2509: (prtm_warning "rewrite rule not in simpset" sign prop; rules), wenzelm@2509: congs, procs, bounds, prems, mk_rews, termless)); wenzelm@2509: nipkow@87: val del_simps = foldl del_simp; clasohm@0: wenzelm@2509: oheimb@2626: (* add_congs *) clasohm@0: wenzelm@2509: fun add_cong (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thm) = wenzelm@2509: let wenzelm@2509: val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ => wenzelm@2509: raise SIMPLIFIER ("Congruence not a meta-equality", thm); wenzelm@2509: (* val lhs = Pattern.eta_contract lhs; *) wenzelm@2509: val (a, _) = dest_Const (head_of lhs) handle TERM _ => wenzelm@2509: raise SIMPLIFIER ("Congruence must start with a constant", thm); wenzelm@2509: in wenzelm@2509: mk_mss (rules, (a, {lhs = lhs, thm = thm}) :: congs, procs, bounds, wenzelm@2509: prems, mk_rews, termless) clasohm@0: end; clasohm@0: clasohm@0: val (op add_congs) = foldl add_cong; clasohm@0: wenzelm@2509: oheimb@2626: (* del_congs *) oheimb@2626: oheimb@2626: fun del_cong (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thm) = oheimb@2626: let oheimb@2626: val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ => oheimb@2626: raise SIMPLIFIER ("Congruence not a meta-equality", thm); oheimb@2626: (* val lhs = Pattern.eta_contract lhs; *) oheimb@2626: val (a, _) = dest_Const (head_of lhs) handle TERM _ => oheimb@2626: raise SIMPLIFIER ("Congruence must start with a constant", thm); oheimb@2626: in oheimb@2626: mk_mss (rules, filter (fn (x,_)=> x<>a) congs, procs, bounds, oheimb@2626: prems, mk_rews, termless) oheimb@2626: end; oheimb@2626: oheimb@2626: val (op del_congs) = foldl del_cong; oheimb@2626: oheimb@2626: wenzelm@2509: (* add_simprocs *) wenzelm@2509: wenzelm@2509: fun add_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, wenzelm@2509: (sign, lhs, proc, id)) = wenzelm@2509: (trace_term "Adding simplification procedure for:" sign lhs; wenzelm@2509: mk_mss (rules, congs, wenzelm@2509: Net.insert_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.INSERT => wenzelm@2509: (trace_warning "ignored duplicate"; procs), wenzelm@2509: bounds, prems, mk_rews, termless)); clasohm@0: wenzelm@2509: val add_simprocs = foldl add_simproc; wenzelm@2509: wenzelm@2509: wenzelm@2509: (* del_simprocs *) clasohm@0: wenzelm@2509: fun del_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, wenzelm@3012: (sign:Sign.sg, lhs, proc, id)) = wenzelm@2509: mk_mss (rules, congs, wenzelm@2509: Net.delete_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.DELETE => wenzelm@2509: (trace_warning "simplification procedure not in simpset"; procs), wenzelm@2509: bounds, prems, mk_rews, termless); wenzelm@2509: wenzelm@2509: val del_simprocs = foldl del_simproc; clasohm@0: clasohm@0: wenzelm@2509: (* prems *) wenzelm@2509: wenzelm@2509: fun add_prems (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thms) = wenzelm@2509: mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless); wenzelm@2509: wenzelm@2509: fun prems_of_mss (Mss {prems, ...}) = prems; wenzelm@2509: wenzelm@2509: wenzelm@2509: (* mk_rews *) wenzelm@2509: wenzelm@2509: fun set_mk_rews wenzelm@2509: (Mss {rules, congs, procs, bounds, prems, mk_rews = _, termless}, mk_rews) = wenzelm@2509: mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless); wenzelm@2509: wenzelm@2509: fun mk_rews_of_mss (Mss {mk_rews, ...}) = mk_rews; wenzelm@2509: wenzelm@2509: wenzelm@2509: (* termless *) wenzelm@2509: wenzelm@2509: fun set_termless wenzelm@2509: (Mss {rules, congs, procs, bounds, prems, mk_rews, termless = _}, termless) = wenzelm@2509: mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless); wenzelm@2509: wenzelm@2509: wenzelm@2509: wenzelm@2509: (** rewriting **) wenzelm@2509: wenzelm@2509: (* wenzelm@2509: Uses conversions, omitting proofs for efficiency. See: wenzelm@2509: L C Paulson, A higher-order implementation of rewriting, wenzelm@2509: Science of Computer Programming 3 (1983), pages 119-149. wenzelm@2509: *) clasohm@0: clasohm@0: type prover = meta_simpset -> thm -> thm option; clasohm@0: type termrec = (Sign.sg * term list) * term; clasohm@0: type conv = meta_simpset -> termrec -> termrec; clasohm@0: paulson@1529: fun check_conv (thm as Thm{shyps,hyps,prop,sign,der,maxidx,...}, prop0, ders) = nipkow@432: let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; nipkow@432: trace_term "Should have proved" sign prop0; nipkow@432: None) clasohm@0: val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0) clasohm@0: in case prop of clasohm@0: Const("==",_) $ lhs $ rhs => clasohm@0: if (lhs = lhs0) orelse nipkow@427: (lhs aconv Envir.norm_term (Envir.empty 0) lhs0) paulson@1529: then (trace_thm "SUCCEEDED" thm; wenzelm@2386: Some(shyps, hyps, maxidx, rhs, der::ders)) clasohm@0: else err() clasohm@0: | _ => err() clasohm@0: end; clasohm@0: nipkow@659: fun ren_inst(insts,prop,pat,obj) = nipkow@659: let val ren = match_bvs(pat,obj,[]) nipkow@659: fun renAbs(Abs(x,T,b)) = berghofe@1576: Abs(case assoc_string(ren,x) of None => x | Some(y) => y, T, renAbs(b)) nipkow@659: | renAbs(f$t) = renAbs(f) $ renAbs(t) nipkow@659: | renAbs(t) = t nipkow@659: in subst_vars insts (if null(ren) then prop else renAbs(prop)) end; nipkow@678: wenzelm@1258: fun add_insts_sorts ((iTs, is), Ss) = wenzelm@1258: add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss)); wenzelm@1258: nipkow@659: wenzelm@2509: (* mk_procrule *) wenzelm@2509: wenzelm@2509: fun mk_procrule (thm as Thm {sign, prop, ...}) = wenzelm@2509: let wenzelm@2509: val prems = Logic.strip_imp_prems prop; wenzelm@2509: val concl = Logic.strip_imp_concl prop; wenzelm@2509: val (lhs, _) = Logic.dest_equals concl handle TERM _ => wenzelm@2509: raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm); wenzelm@2509: val econcl = Pattern.eta_contract concl; wenzelm@2509: val (elhs, erhs) = Logic.dest_equals econcl; wenzelm@2509: in wenzelm@2509: if not ((term_vars erhs) subset paulson@2671: (union_term (term_vars elhs, List.concat(map term_vars prems)))) paulson@2671: then (prtm_warning "extra Var(s) on rhs" sign prop; []) wenzelm@2509: else [{thm = thm, lhs = lhs, perm = false}] wenzelm@2509: end; wenzelm@2509: wenzelm@2509: wenzelm@2509: (* conversion to apply the meta simpset to a term *) wenzelm@2509: wenzelm@2509: (* wenzelm@2509: we try in order: wenzelm@2509: (1) beta reduction wenzelm@2509: (2) unconditional rewrite rules wenzelm@2509: (3) conditional rewrite rules wenzelm@2509: (4) simplification procedures (* FIXME (un-)conditional !! *) wenzelm@2509: *) wenzelm@2509: wenzelm@2509: fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, ...}) paulson@2147: (shypst,hypst,maxt,t,ders) = nipkow@2792: let fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} = wenzelm@250: let val unit = if Sign.subsig(sign,signt) then () berghofe@1580: else (trace_thm_warning "rewrite rule from different theory" clasohm@446: thm; nipkow@208: raise Pattern.MATCH) paulson@2147: val rprop = if maxt = ~1 then prop paulson@2147: else Logic.incr_indexes([],maxt+1) prop; paulson@2147: val rlhs = if maxt = ~1 then lhs nipkow@1065: else fst(Logic.dest_equals(Logic.strip_imp_concl rprop)) nipkow@2792: val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,t) nipkow@1065: val prop' = ren_inst(insts,rprop,rlhs,t); paulson@2177: val hyps' = union_term(hyps,hypst); paulson@2177: val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst)); nipkow@1065: val maxidx' = maxidx_of_term prop' wenzelm@2386: val ct' = Cterm{sign = signt, (*used for deriv only*) wenzelm@2386: t = prop', wenzelm@2386: T = propT, wenzelm@2386: maxidx = maxidx'} wenzelm@2509: val der' = infer_derivs (RewriteC ct', [der]) (* FIXME fix!? *) paulson@1529: val thm' = Thm{sign = signt, wenzelm@2386: der = der', wenzelm@2386: shyps = shyps', wenzelm@2386: hyps = hyps', paulson@1529: prop = prop', wenzelm@2386: maxidx = maxidx'} nipkow@427: val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop') nipkow@427: in if perm andalso not(termless(rhs',lhs')) then None else nipkow@427: if Logic.count_prems(prop',0) = 0 paulson@1529: then (trace_thm "Rewriting:" thm'; wenzelm@2386: Some(shyps', hyps', maxidx', rhs', der'::ders)) clasohm@0: else (trace_thm "Trying to rewrite:" thm'; clasohm@0: case prover mss thm' of clasohm@0: None => (trace_thm "FAILED" thm'; None) paulson@1529: | Some(thm2) => check_conv(thm2,prop',ders)) clasohm@0: end clasohm@0: nipkow@225: fun rews [] = None wenzelm@2509: | rews (rrule :: rrules) = nipkow@225: let val opt = rew rrule handle Pattern.MATCH => None nipkow@225: in case opt of None => rews rrules | some => some end; oheimb@1659: fun sort_rrules rrs = let wenzelm@2386: fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of wenzelm@2386: Const("==",_) $ _ $ _ => true wenzelm@2386: | _ => false wenzelm@2386: fun sort [] (re1,re2) = re1 @ re2 wenzelm@2386: | sort (rr::rrs) (re1,re2) = if is_simple rr wenzelm@2386: then sort rrs (rr::re1,re2) wenzelm@2386: else sort rrs (re1,rr::re2) oheimb@1659: in sort rrs ([],[]) oheimb@1659: end wenzelm@2509: wenzelm@3012: fun proc_rews _ [] = None wenzelm@3012: | proc_rews eta_t ((f, _) :: fs) = wenzelm@3012: (case f signt eta_t of wenzelm@3012: None => proc_rews eta_t fs wenzelm@2509: | Some raw_thm => wenzelm@2509: (trace_thm "Proved rewrite rule: " raw_thm; wenzelm@2509: (case rews (mk_procrule raw_thm) of wenzelm@3012: None => proc_rews eta_t fs wenzelm@2509: | some => some))); wenzelm@2509: in nipkow@2792: (case t of wenzelm@2509: Abs (_, _, body) $ u => (* FIXME bug!? (because of beta/eta overlap) *) wenzelm@2509: Some (shypst, hypst, maxt, subst_bound (u, body), ders) wenzelm@2509: | _ => nipkow@2792: (case rews (sort_rrules (Net.match_term rules t)) of wenzelm@3012: None => proc_rews (Pattern.eta_contract t) (Net.match_term procs t) wenzelm@2509: | some => some)) clasohm@0: end; clasohm@0: wenzelm@2509: wenzelm@2509: (* conversion to apply a congruence rule to a term *) wenzelm@2509: paulson@2147: fun congc (prover,signt) {thm=cong,lhs=lhs} (shypst,hypst,maxt,t,ders) = paulson@1529: let val Thm{sign,der,shyps,hyps,maxidx,prop,...} = cong nipkow@208: val unit = if Sign.subsig(sign,signt) then () nipkow@208: else error("Congruence rule from different theory") nipkow@208: val tsig = #tsig(Sign.rep_sg signt) paulson@2147: val rprop = if maxt = ~1 then prop paulson@2147: else Logic.incr_indexes([],maxt+1) prop; paulson@2147: val rlhs = if maxt = ~1 then lhs nipkow@1065: else fst(Logic.dest_equals(Logic.strip_imp_concl rprop)) nipkow@1569: val insts = Pattern.match tsig (rlhs,t) nipkow@1569: (* Pattern.match can raise Pattern.MATCH; nipkow@1569: is handled when congc is called *) nipkow@1065: val prop' = ren_inst(insts,rprop,rlhs,t); paulson@2177: val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst)) paulson@1529: val maxidx' = maxidx_of_term prop' wenzelm@2386: val ct' = Cterm{sign = signt, (*used for deriv only*) wenzelm@2386: t = prop', wenzelm@2386: T = propT, wenzelm@2386: maxidx = maxidx'} paulson@1529: val thm' = Thm{sign = signt, wenzelm@2509: der = infer_derivs (CongC ct', [der]), (* FIXME fix!? *) wenzelm@2386: shyps = shyps', wenzelm@2386: hyps = union_term(hyps,hypst), paulson@1529: prop = prop', wenzelm@2386: maxidx = maxidx'}; clasohm@0: val unit = trace_thm "Applying congruence rule" thm'; nipkow@112: fun err() = error("Failed congruence proof!") clasohm@0: clasohm@0: in case prover thm' of nipkow@112: None => err() paulson@1529: | Some(thm2) => (case check_conv(thm2,prop',ders) of nipkow@405: None => err() | some => some) clasohm@0: end; clasohm@0: clasohm@0: nipkow@405: nipkow@214: fun bottomc ((simprem,useprem),prover,sign) = paulson@1529: let fun botc fail mss trec = wenzelm@2386: (case subc mss trec of wenzelm@2386: some as Some(trec1) => wenzelm@2386: (case rewritec (prover,sign) mss trec1 of wenzelm@2386: Some(trec2) => botc false mss trec2 wenzelm@2386: | None => some) wenzelm@2386: | None => wenzelm@2386: (case rewritec (prover,sign) mss trec of wenzelm@2386: Some(trec2) => botc false mss trec2 wenzelm@2386: | None => if fail then None else Some(trec))) clasohm@0: paulson@1529: and try_botc mss trec = (case botc true mss trec of wenzelm@2386: Some(trec1) => trec1 wenzelm@2386: | None => trec) nipkow@405: wenzelm@2509: and subc (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) wenzelm@2386: (trec as (shyps,hyps,maxidx,t0,ders)) = paulson@1529: (case t0 of wenzelm@2386: Abs(a,T,t) => wenzelm@2386: let val b = variant bounds a wenzelm@2386: val v = Free("." ^ b,T) wenzelm@2509: val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless) wenzelm@2386: in case botc true mss' wenzelm@2386: (shyps,hyps,maxidx,subst_bound (v,t),ders) of wenzelm@2386: Some(shyps',hyps',maxidx',t',ders') => wenzelm@2386: Some(shyps', hyps', maxidx', wenzelm@2386: Abs(a, T, abstract_over(v,t')), wenzelm@2386: ders') wenzelm@2386: | None => None wenzelm@2386: end wenzelm@2386: | t$u => (case t of wenzelm@2386: Const("==>",_)$s => Some(impc(shyps,hyps,maxidx,s,u,mss,ders)) wenzelm@2386: | Abs(_,_,body) => wenzelm@2386: let val trec = (shyps,hyps,maxidx,subst_bound (u,body),ders) wenzelm@2386: in case subc mss trec of wenzelm@2386: None => Some(trec) wenzelm@2386: | trec => trec wenzelm@2386: end wenzelm@2386: | _ => wenzelm@2386: let fun appc() = wenzelm@2386: (case botc true mss (shyps,hyps,maxidx,t,ders) of wenzelm@2386: Some(shyps1,hyps1,maxidx1,t1,ders1) => wenzelm@2386: (case botc true mss (shyps1,hyps1,maxidx,u,ders1) of wenzelm@2386: Some(shyps2,hyps2,maxidx2,u1,ders2) => wenzelm@2386: Some(shyps2, hyps2, Int.max(maxidx1,maxidx2), wenzelm@2386: t1$u1, ders2) wenzelm@2386: | None => wenzelm@2386: Some(shyps1, hyps1, Int.max(maxidx1,maxidx), t1$u, wenzelm@2386: ders1)) wenzelm@2386: | None => wenzelm@2386: (case botc true mss (shyps,hyps,maxidx,u,ders) of wenzelm@2386: Some(shyps1,hyps1,maxidx1,u1,ders1) => wenzelm@2386: Some(shyps1, hyps1, Int.max(maxidx,maxidx1), wenzelm@2386: t$u1, ders1) wenzelm@2386: | None => None)) wenzelm@2386: val (h,ts) = strip_comb t wenzelm@2386: in case h of wenzelm@2386: Const(a,_) => wenzelm@2386: (case assoc_string(congs,a) of wenzelm@2386: None => appc() wenzelm@2386: | Some(cong) => (congc (prover mss,sign) cong trec nipkow@1569: handle Pattern.MATCH => appc() ) ) wenzelm@2386: | _ => appc() wenzelm@2386: end) wenzelm@2386: | _ => None) clasohm@0: paulson@1529: and impc(shyps, hyps, maxidx, s, u, mss as Mss{mk_rews,...}, ders) = paulson@1529: let val (shyps1,hyps1,_,s1,ders1) = wenzelm@2386: if simprem then try_botc mss (shyps,hyps,maxidx,s,ders) wenzelm@2386: else (shyps,hyps,0,s,ders); wenzelm@2386: val maxidx1 = maxidx_of_term s1 wenzelm@2386: val mss1 = nipkow@2535: if not useprem then mss else nipkow@2620: if maxidx1 <> ~1 then (trace_term_warning nipkow@2535: "Cannot add premise as rewrite rule because it contains (type) unknowns:" nipkow@2535: sign s1; mss) wenzelm@2386: else let val thm = assume (Cterm{sign=sign, t=s1, wenzelm@2386: T=propT, maxidx=maxidx1}) wenzelm@2386: in add_simps(add_prems(mss,[thm]), mk_rews thm) end wenzelm@2386: val (shyps2,hyps2,maxidx2,u1,ders2) = wenzelm@2386: try_botc mss1 (shyps1,hyps1,maxidx,u,ders1) wenzelm@2386: val hyps3 = if gen_mem (op aconv) (s1, hyps1) wenzelm@2386: then hyps2 else hyps2\s1 paulson@2147: in (shyps2, hyps3, Int.max(maxidx1,maxidx2), wenzelm@2386: Logic.mk_implies(s1,u1), ders2) paulson@1529: end clasohm@0: paulson@1529: in try_botc end; clasohm@0: clasohm@0: clasohm@0: (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***) wenzelm@2509: wenzelm@2509: (* wenzelm@2509: Parameters: wenzelm@2509: mode = (simplify A, use A in simplifying B) when simplifying A ==> B wenzelm@2509: mss: contains equality theorems of the form [|p1,...|] ==> t==u wenzelm@2509: prover: how to solve premises in conditional rewrites and congruences clasohm@0: *) wenzelm@2509: wenzelm@2509: (* FIXME: check that #bounds(mss) does not "occur" in ct alread *) wenzelm@2509: nipkow@214: fun rewrite_cterm mode mss prover ct = lcp@229: let val {sign, t, T, maxidx} = rep_cterm ct; paulson@2147: val (shyps,hyps,maxu,u,ders) = paulson@1529: bottomc (mode,prover,sign) mss wenzelm@2386: (add_term_sorts(t,[]), [], maxidx, t, []); clasohm@0: val prop = Logic.mk_equals(t,u) wenzelm@1258: in paulson@1529: Thm{sign = sign, wenzelm@2386: der = infer_derivs (Rewrite_cterm ct, ders), wenzelm@2386: maxidx = Int.max (maxidx,maxu), wenzelm@2386: shyps = shyps, wenzelm@2386: hyps = hyps, paulson@1529: prop = prop} clasohm@0: end clasohm@0: paulson@1539: wenzelm@2509: wenzelm@2509: (*** Oracles ***) wenzelm@2509: paulson@1539: fun invoke_oracle (thy, sign, exn) = paulson@1539: case #oraopt(rep_theory thy) of wenzelm@2386: None => raise THM ("No oracle in supplied theory", 0, []) paulson@1539: | Some oracle => wenzelm@2386: let val sign' = Sign.merge(sign_of thy, sign) wenzelm@2386: val (prop, T, maxidx) = wenzelm@2386: Sign.certify_term sign' (oracle (sign', exn)) paulson@1539: in if T<>propT then paulson@1539: raise THM("Oracle's result must have type prop", 0, []) wenzelm@2386: else fix_shyps [] [] wenzelm@2386: (Thm {sign = sign', wenzelm@2386: der = Join (Oracle(thy,sign,exn), []), wenzelm@2386: maxidx = maxidx, wenzelm@2386: shyps = [], wenzelm@2386: hyps = [], wenzelm@2386: prop = prop}) paulson@1539: end; paulson@1539: clasohm@0: end; paulson@1503: paulson@1503: open Thm;