diff --git a/src/Pure/drule.ML b/src/Pure/drule.ML --- a/src/Pure/drule.ML +++ b/src/Pure/drule.ML @@ -1,840 +1,845 @@ (* Title: Pure/drule.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Derived rules and other operations on theorems. *) infix 0 RL RLN MRS OF COMP INCR_COMP COMP_INCR; signature BASIC_DRULE = sig val mk_implies: cterm * cterm -> cterm val list_implies: cterm list * cterm -> cterm val strip_imp_prems: cterm -> cterm list val strip_imp_concl: cterm -> cterm val cprems_of: thm -> cterm list val forall_intr_list: cterm list -> thm -> thm val forall_intr_vars: thm -> thm val forall_elim_list: cterm list -> thm -> thm val lift_all: Proof.context -> cterm -> thm -> thm val implies_elim_list: thm -> thm list -> thm val implies_intr_list: cterm list -> thm -> thm val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm val instantiate'_normalize: ctyp option list -> cterm option list -> thm -> thm val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm val infer_instantiate': Proof.context -> cterm option list -> thm -> thm val zero_var_indexes_list: thm list -> thm list val zero_var_indexes: thm -> thm val implies_intr_hyps: thm -> thm val rotate_prems: int -> thm -> thm val rearrange_prems: int list -> thm -> thm val RLN: thm list * (int * thm list) -> thm list val RL: thm list * thm list -> thm list val MRS: thm list * thm -> thm val OF: thm * thm list -> thm val COMP: thm * thm -> thm val INCR_COMP: thm * thm -> thm val COMP_INCR: thm * thm -> thm val size_of_thm: thm -> int val reflexive_thm: thm val symmetric_thm: thm val transitive_thm: thm val extensional: thm -> thm val asm_rl: thm val cut_rl: thm val revcut_rl: thm val thin_rl: thm end; signature DRULE = sig include BASIC_DRULE val outer_params: term -> (string * typ) list val generalize: Symtab.set * Symtab.set -> thm -> thm val list_comb: cterm * cterm list -> cterm val strip_comb: cterm -> cterm * cterm list val beta_conv: cterm -> cterm -> cterm val flexflex_unique: Proof.context option -> thm -> thm val export_without_context: thm -> thm val export_without_context_open: thm -> thm val store_thm: binding -> thm -> thm val store_standard_thm: binding -> thm -> thm val store_thm_open: binding -> thm -> thm val store_standard_thm_open: binding -> thm -> thm val multi_resolve: Proof.context option -> thm list -> thm -> thm Seq.seq val multi_resolves: Proof.context option -> thm list -> thm list -> thm Seq.seq val compose: thm * int * thm -> thm val equals_cong: thm val imp_cong: thm val swap_prems_eq: thm val imp_cong_rule: thm -> thm -> thm val arg_cong_rule: cterm -> thm -> thm val binop_cong_rule: cterm -> thm -> thm -> thm val fun_cong_rule: thm -> cterm -> thm val beta_eta_conversion: cterm -> thm val eta_contraction_rule: thm -> thm val norm_hhf_eq: thm val norm_hhf_eqs: thm list val is_norm_hhf: term -> bool val norm_hhf: theory -> term -> term val norm_hhf_cterm: Proof.context -> cterm -> cterm val protect: cterm -> cterm val protectI: thm val protectD: thm val protect_cong: thm val implies_intr_protected: cterm list -> thm -> thm val termI: thm val mk_term: cterm -> thm val dest_term: thm -> cterm val cterm_rule: (thm -> thm) -> cterm -> cterm val cterm_frees_of: cterm -> cterm list val dummy_thm: thm val free_dummy_thm: thm val is_sort_constraint: term -> bool val sort_constraintI: thm val sort_constraint_eq: thm val with_subgoal: int -> (thm -> thm) -> thm -> thm val comp_no_flatten: thm * int -> int -> thm -> thm val rename_bvars: (string * string) list -> thm -> thm val rename_bvars': string option list -> thm -> thm val incr_indexes: thm -> thm -> thm val incr_indexes2: thm -> thm -> thm -> thm val triv_forall_equality: thm val distinct_prems_rl: thm val equal_intr_rule: thm val equal_elim_rule1: thm val equal_elim_rule2: thm val remdups_rl: thm val abs_def: thm -> thm end; structure Drule: DRULE = struct (** some cterm->cterm operations: faster than calling cterm_of! **) (* A1\...An\B goes to [A1,...,An], where B is not an implication *) fun strip_imp_prems ct = let val (cA, cB) = Thm.dest_implies ct in cA :: strip_imp_prems cB end handle TERM _ => []; (* A1\...An\B goes to B, where B is not an implication *) fun strip_imp_concl ct = (case Thm.term_of ct of Const ("Pure.imp", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct) | _ => ct); (*The premises of a theorem, as a cterm list*) val cprems_of = strip_imp_prems o Thm.cprop_of; fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t; val implies = certify Logic.implies; fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B; (*cterm version of list_implies: [A1,...,An], B goes to \A1;...;An\\B *) fun list_implies([], B) = B | list_implies(A::As, B) = mk_implies (A, list_implies(As,B)); (*cterm version of list_comb: maps (f, [t1,...,tn]) to f(t1,...,tn) *) fun list_comb (f, []) = f | list_comb (f, t::ts) = list_comb (Thm.apply f t, ts); (*cterm version of strip_comb: maps f(t1,...,tn) to (f, [t1,...,tn]) *) fun strip_comb ct = let fun stripc (p as (ct, cts)) = let val (ct1, ct2) = Thm.dest_comb ct in stripc (ct1, ct2 :: cts) end handle CTERM _ => p in stripc (ct, []) end; (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs of the meta-equality returned by the beta_conversion rule.*) fun beta_conv x y = Thm.dest_arg (Thm.cprop_of (Thm.beta_conversion false (Thm.apply x y))); (** Standardization of rules **) (*Generalization over a list of variables*) val forall_intr_list = fold_rev Thm.forall_intr; (*Generalization over Vars -- canonical order*) -fun forall_intr_vars th = fold Thm.forall_intr (Thm.add_vars th []) th; +fun forall_intr_vars th = + let + val vs = + build (th |> Thm.fold_atomic_cterms {hyps = false} (fn a => + is_Var (Thm.term_of a) ? insert (op aconvc) a)); + in fold Thm.forall_intr vs th end; fun outer_params t = let val vs = Term.strip_all_vars t in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end; (*lift vars wrt. outermost goal parameters -- reverses the effect of gen_all modulo higher-order unification*) fun lift_all ctxt raw_goal raw_th = let val thy = Proof_Context.theory_of ctxt; val goal = Thm.transfer_cterm thy raw_goal; val th = Thm.transfer thy raw_th; val maxidx = Thm.maxidx_of th; val ps = outer_params (Thm.term_of goal) |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T)); val Ts = map Term.fastype_of ps; val inst = Term_Subst.Vars.build (th |> (Thm.fold_terms {hyps = false} o Term.fold_aterms) (fn t => fn inst => (case t of Var (xi, T) => if Term_Subst.Vars.defined inst (xi, T) then inst else let val ct = Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps)) in Term_Subst.Vars.update ((xi, T), ct) inst end | _ => inst))); in th |> Thm.instantiate ([], Term_Subst.Vars.dest inst) |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps end; (*direct generalization*) fun generalize names th = Thm.generalize names (Thm.maxidx_of th + 1) th; (*specialization over a list of cterms*) val forall_elim_list = fold Thm.forall_elim; (*maps A1,...,An |- B to \A1;...;An\ \ B*) val implies_intr_list = fold_rev Thm.implies_intr; (*maps \A1;...;An\ \ B and [A1,...,An] to B*) fun implies_elim_list impth ths = fold Thm.elim_implies ths impth; (*Reset Var indexes to zero, renaming to preserve distinctness*) fun zero_var_indexes_list [] = [] | zero_var_indexes_list ths = let val (instT, inst) = Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths); - val tvars = fold Thm.add_tvars ths []; - fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars); + val tvars = fold Thm.add_tvars ths Term_Subst.TVars.empty; + val the_tvar = the o Term_Subst.TVars.lookup tvars; val instT' = build (instT |> Term_Subst.TVars.fold (fn (v, TVar (b, _)) => cons (v, Thm.rename_tvar b (the_tvar v)))); - val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths []; - fun the_var v = the (find_first (fn ct => v = dest_Var (Thm.term_of ct)) vars); + val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths Term_Subst.Vars.empty; + val the_var = the o Term_Subst.Vars.lookup vars; val inst' = build (inst |> Term_Subst.Vars.fold (fn (v, Var (b, _)) => cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v))))); in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end; val zero_var_indexes = singleton zero_var_indexes_list; (** Standard form of object-rule: no hypotheses, flexflex constraints, Frees, or outer quantifiers; all generality expressed by Vars of index 0.**) (*Discharge all hypotheses.*) fun implies_intr_hyps th = fold Thm.implies_intr (Thm.chyps_of th) th; (*Squash a theorem's flexflex constraints provided it can be done uniquely. This step can lose information.*) fun flexflex_unique opt_ctxt th = if null (Thm.tpairs_of th) then th else (case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule opt_ctxt th)) of [th] => th | [] => raise THM ("flexflex_unique: impossible constraints", 0, [th]) | _ => raise THM ("flexflex_unique: multiple unifiers", 0, [th])); (* old-style export without context *) val export_without_context_open = implies_intr_hyps #> Thm.forall_intr_frees #> `Thm.maxidx_of #-> (fn maxidx => Thm.forall_elim_vars (maxidx + 1) #> Thm.strip_shyps #> zero_var_indexes #> Thm.varifyT_global); val export_without_context = flexflex_unique NONE #> export_without_context_open #> Thm.close_derivation \<^here>; (*Rotates a rule's premises to the left by k*) fun rotate_prems 0 = I | rotate_prems k = Thm.permute_prems 0 k; fun with_subgoal i f = rotate_prems (i - 1) #> f #> rotate_prems (1 - i); (*Permute prems, where the i-th position in the argument list (counting from 0) gives the position within the original thm to be transferred to position i. Any remaining trailing positions are left unchanged.*) val rearrange_prems = let fun rearr new [] thm = thm | rearr new (p :: ps) thm = rearr (new + 1) (map (fn q => if new <= q andalso q < p then q + 1 else q) ps) (Thm.permute_prems (new + 1) (new - p) (Thm.permute_prems new (p - new) thm)) in rearr 0 end; (*Resolution: multiple arguments, multiple results*) local fun res opt_ctxt th i rule = (Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty) |> Seq.map Thm.solve_constraints; fun multi_res _ _ [] rule = Seq.single rule | multi_res opt_ctxt i (th :: ths) rule = Seq.maps (res opt_ctxt th i) (multi_res opt_ctxt (i + 1) ths rule); in fun multi_resolve opt_ctxt = multi_res opt_ctxt 1; fun multi_resolves opt_ctxt facts rules = Seq.maps (multi_resolve opt_ctxt facts) (Seq.of_list rules); end; (*For joining lists of rules*) fun thas RLN (i, thbs) = let val resolve = Thm.biresolution NONE false (map (pair false) thas) i fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] in maps resb thbs |> map Thm.solve_constraints end; fun thas RL thbs = thas RLN (1, thbs); (*Isar-style multi-resolution*) fun bottom_rl OF rls = (case Seq.chop 2 (multi_resolve NONE rls bottom_rl) of ([th], _) => Thm.solve_constraints th | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls) | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls)); (*Resolve a list of rules against bottom_rl from right to left; makes proof trees*) fun rls MRS bottom_rl = bottom_rl OF rls; (*compose Q and \...,Qi,Q(i+1),...\ \ R to \...,Q(i+1),...\ \ R with no lifting or renaming! Q may contain \ or meta-quantifiers ALWAYS deletes premise i *) fun compose (tha, i, thb) = Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, tha, 0) i thb |> Seq.list_of |> distinct Thm.eq_thm |> (fn [th] => Thm.solve_constraints th | _ => raise THM ("compose: unique result expected", i, [tha, thb])); (** theorem equality **) (*Useful "distance" function for BEST_FIRST*) val size_of_thm = size_of_term o Thm.full_prop_of; (*** Meta-Rewriting Rules ***) val read_prop = certify o Simple_Syntax.read_prop; fun store_thm name th = Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th))); fun store_thm_open name th = Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th))); fun store_standard_thm name th = store_thm name (export_without_context th); fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th); val reflexive_thm = let val cx = certify (Var(("x",0),TVar(("'a",0),[]))) in store_standard_thm_open (Binding.make ("reflexive", \<^here>)) (Thm.reflexive cx) end; val symmetric_thm = let val xy = read_prop "x::'a \ y::'a"; val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy)); in store_standard_thm_open (Binding.make ("symmetric", \<^here>)) thm end; val transitive_thm = let val xy = read_prop "x::'a \ y::'a"; val yz = read_prop "y::'a \ z::'a"; val xythm = Thm.assume xy; val yzthm = Thm.assume yz; val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm); in store_standard_thm_open (Binding.make ("transitive", \<^here>)) thm end; fun extensional eq = let val eq' = Thm.abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (Thm.cprop_of eq)))) eq in Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of eq')) eq' end; val equals_cong = store_standard_thm_open (Binding.make ("equals_cong", \<^here>)) (Thm.reflexive (read_prop "x::'a \ y::'a")); val imp_cong = let val ABC = read_prop "A \ B::prop \ C::prop" val AB = read_prop "A \ B" val AC = read_prop "A \ C" val A = read_prop "A" in store_standard_thm_open (Binding.make ("imp_cong", \<^here>)) (Thm.implies_intr ABC (Thm.equal_intr (Thm.implies_intr AB (Thm.implies_intr A (Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.implies_elim (Thm.assume AB) (Thm.assume A))))) (Thm.implies_intr AC (Thm.implies_intr A (Thm.equal_elim (Thm.symmetric (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))) (Thm.implies_elim (Thm.assume AC) (Thm.assume A))))))) end; val swap_prems_eq = let val ABC = read_prop "A \ B \ C" val BAC = read_prop "B \ A \ C" val A = read_prop "A" val B = read_prop "B" in store_standard_thm_open (Binding.make ("swap_prems_eq", \<^here>)) (Thm.equal_intr (Thm.implies_intr ABC (Thm.implies_intr B (Thm.implies_intr A (Thm.implies_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.assume B))))) (Thm.implies_intr BAC (Thm.implies_intr A (Thm.implies_intr B (Thm.implies_elim (Thm.implies_elim (Thm.assume BAC) (Thm.assume B)) (Thm.assume A)))))) end; val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies); fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th; (*AP_TERM in LCF/HOL*) fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct); (*AP_THM in LCF/HOL*) fun binop_cong_rule ct th1 th2 = Thm.combination (arg_cong_rule ct th1) th2; fun beta_eta_conversion ct = let val thm = Thm.beta_conversion true ct in Thm.transitive thm (Thm.eta_conversion (Thm.rhs_of thm)) end; (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*) fun eta_contraction_rule th = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of th)) th; (* abs_def *) (* f ?x1 ... ?xn \ u -------------------- f \ \x1 ... xn. u *) local fun contract_lhs th = Thm.transitive (Thm.symmetric (beta_eta_conversion (#1 (Thm.dest_equals (Thm.cprop_of th))))) th; fun var_args ct = (case try Thm.dest_comb ct of SOME (f, arg) => (case Thm.term_of arg of Var ((x, _), _) => update (eq_snd (op aconvc)) (x, arg) (var_args f) | _ => []) | NONE => []); in fun abs_def th = let val th' = contract_lhs th; val args = var_args (Thm.lhs_of th'); in contract_lhs (fold (uncurry Thm.abstract_rule) args th') end; end; (*** Some useful meta-theorems ***) (*The rule V/V, obtains assumption solving for eresolve_tac*) val asm_rl = store_standard_thm_open (Binding.make ("asm_rl", \<^here>)) (Thm.trivial (read_prop "?psi")); (*Meta-level cut rule: \V \ W; V\ \ W *) val cut_rl = store_standard_thm_open (Binding.make ("cut_rl", \<^here>)) (Thm.trivial (read_prop "?psi \ ?theta")); (*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 = read_prop "V"; val VW = read_prop "V \ W"; in store_standard_thm_open (Binding.make ("revcut_rl", \<^here>)) (Thm.implies_intr V (Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V)))) end; (*for deleting an unwanted assumption*) val thin_rl = let val V = read_prop "V"; val W = read_prop "W"; val thm = Thm.implies_intr V (Thm.implies_intr W (Thm.assume W)); in store_standard_thm_open (Binding.make ("thin_rl", \<^here>)) thm end; (* (\x. PROP ?V) \ PROP ?V Allows removal of redundant parameters*) val triv_forall_equality = let val V = read_prop "V"; val QV = read_prop "\x::'a. V"; val x = certify (Free ("x", Term.aT [])); in store_standard_thm_open (Binding.make ("triv_forall_equality", \<^here>)) (Thm.equal_intr (Thm.implies_intr QV (Thm.forall_elim x (Thm.assume QV))) (Thm.implies_intr V (Thm.forall_intr x (Thm.assume V)))) end; (* (PROP ?Phi \ PROP ?Phi \ PROP ?Psi) \ (PROP ?Phi \ PROP ?Psi) *) val distinct_prems_rl = let val AAB = read_prop "Phi \ Phi \ Psi"; val A = read_prop "Phi"; in store_standard_thm_open (Binding.make ("distinct_prems_rl", \<^here>)) (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A])) end; (* \PROP ?phi \ PROP ?psi; PROP ?psi \ PROP ?phi\ \ PROP ?phi \ PROP ?psi Introduction rule for \ as a meta-theorem. *) val equal_intr_rule = let val PQ = read_prop "phi \ psi"; val QP = read_prop "psi \ phi"; in store_standard_thm_open (Binding.make ("equal_intr_rule", \<^here>)) (Thm.implies_intr PQ (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP)))) end; (* PROP ?phi \ PROP ?psi \ PROP ?phi \ PROP ?psi *) val equal_elim_rule1 = let val eq = read_prop "phi::prop \ psi::prop"; val P = read_prop "phi"; in store_standard_thm_open (Binding.make ("equal_elim_rule1", \<^here>)) (Thm.equal_elim (Thm.assume eq) (Thm.assume P) |> implies_intr_list [eq, P]) end; (* PROP ?psi \ PROP ?phi \ PROP ?phi \ PROP ?psi *) val equal_elim_rule2 = store_standard_thm_open (Binding.make ("equal_elim_rule2", \<^here>)) (symmetric_thm RS equal_elim_rule1); (* PROP ?phi \ PROP ?phi \ PROP ?psi \ PROP ?psi *) val remdups_rl = let val P = read_prop "phi"; val Q = read_prop "psi"; val thm = implies_intr_list [P, P, Q] (Thm.assume Q); in store_standard_thm_open (Binding.make ("remdups_rl", \<^here>)) thm end; (** embedded terms and types **) local val A = certify (Free ("A", propT)); val axiom = Thm.unvarify_axiom (Context.the_global_context ()); val prop_def = axiom "Pure.prop_def"; val term_def = axiom "Pure.term_def"; val sort_constraint_def = axiom "Pure.sort_constraint_def"; val C = Thm.lhs_of sort_constraint_def; val T = Thm.dest_arg C; val CA = mk_implies (C, A); in (* protect *) val protect = Thm.apply (certify Logic.protectC); val protectI = store_standard_thm (Binding.concealed (Binding.make ("protectI", \<^here>))) (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)); val protectD = store_standard_thm (Binding.concealed (Binding.make ("protectD", \<^here>))) (Thm.equal_elim prop_def (Thm.assume (protect A))); val protect_cong = store_standard_thm_open (Binding.make ("protect_cong", \<^here>)) (Thm.reflexive (protect A)); fun implies_intr_protected asms th = let val asms' = map protect asms in implies_elim_list (implies_intr_list asms th) (map (fn asm' => Thm.assume asm' RS protectD) asms') |> implies_intr_list asms' end; (* term *) val termI = store_standard_thm (Binding.concealed (Binding.make ("termI", \<^here>))) (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))); fun mk_term ct = let val cT = Thm.ctyp_of_cterm ct; val T = Thm.typ_of cT; in Thm.instantiate ([((("'a", 0), []), cT)], [((("x", 0), T), ct)]) termI end; fun dest_term th = let val cprop = strip_imp_concl (Thm.cprop_of th) in if can Logic.dest_term (Thm.term_of cprop) then Thm.dest_arg cprop else raise THM ("dest_term", 0, [th]) end; fun cterm_rule f = dest_term o f o mk_term; val cterm_frees_of = Thm.frees_of o mk_term; val dummy_thm = mk_term (certify Term.dummy_prop); val free_dummy_thm = Thm.tag_free_dummy dummy_thm; (* sort_constraint *) fun is_sort_constraint (Const ("Pure.sort_constraint", _) $ Const ("Pure.type", _)) = true | is_sort_constraint _ = false; val sort_constraintI = store_standard_thm (Binding.concealed (Binding.make ("sort_constraintI", \<^here>))) (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)); val sort_constraint_eq = store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", \<^here>))) (Thm.equal_intr (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI))) (implies_intr_list [A, C] (Thm.assume A))); end; (* HHF normalization *) (* (PROP ?phi \ (\x. PROP ?psi x)) \ (\x. PROP ?phi \ PROP ?psi x) *) val norm_hhf_eq = let val aT = TFree ("'a", []); val x = Free ("x", aT); val phi = Free ("phi", propT); val psi = Free ("psi", aT --> propT); val cx = certify x; val cphi = certify phi; val lhs = certify (Logic.mk_implies (phi, Logic.all x (psi $ x))); val rhs = certify (Logic.all x (Logic.mk_implies (phi, psi $ x))); in Thm.equal_intr (Thm.implies_elim (Thm.assume lhs) (Thm.assume cphi) |> Thm.forall_elim cx |> Thm.implies_intr cphi |> Thm.forall_intr cx |> Thm.implies_intr lhs) (Thm.implies_elim (Thm.assume rhs |> Thm.forall_elim cx) (Thm.assume cphi) |> Thm.forall_intr cx |> Thm.implies_intr cphi |> Thm.implies_intr rhs) |> store_standard_thm_open (Binding.make ("norm_hhf_eq", \<^here>)) end; val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq]; fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false | is_norm_hhf (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false | is_norm_hhf (Abs _ $ _) = false | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t | is_norm_hhf _ = true; fun norm_hhf thy t = if is_norm_hhf t then t else Pattern.rewrite_term thy [norm_hhf_prop] [] t; fun norm_hhf_cterm ctxt raw_ct = let val thy = Proof_Context.theory_of ctxt; val ct = Thm.transfer_cterm thy raw_ct; val t = Thm.term_of ct; in if is_norm_hhf t then ct else Thm.cterm_of ctxt (norm_hhf thy t) end; (* var indexes *) fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1); fun incr_indexes2 th1 th2 = Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1); local (*compose Q and \Q1,Q2,...,Qk\ \ R to \Q2,...,Qk\ \ R getting unique result*) fun comp incremented th1 th2 = Thm.bicompose NONE {flatten = true, match = false, incremented = incremented} (false, th1, 0) 1 th2 |> Seq.list_of |> distinct Thm.eq_thm |> (fn [th] => Thm.solve_constraints th | _ => raise THM ("COMP", 1, [th1, th2])); in fun th1 COMP th2 = comp false th1 th2; fun th1 INCR_COMP th2 = comp true (incr_indexes th2 th1) th2; fun th1 COMP_INCR th2 = comp true th1 (incr_indexes th1 th2); end; fun comp_no_flatten (th, n) i rule = (case distinct Thm.eq_thm (Seq.list_of (Thm.bicompose NONE {flatten = false, match = false, incremented = true} (false, th, n) i (incr_indexes th rule))) of [th'] => Thm.solve_constraints th' | [] => raise THM ("comp_no_flatten", i, [th, rule]) | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule])); (** variations on Thm.instantiate **) fun instantiate_normalize instpair th = Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); fun instantiate'_normalize Ts ts th = Thm.adjust_maxidx_thm ~1 (Thm.instantiate' Ts ts th COMP_INCR asm_rl); (*instantiation with type-inference for variables*) fun infer_instantiate_types _ [] th = th | infer_instantiate_types ctxt args raw_th = let val thy = Proof_Context.theory_of ctxt; val th = Thm.transfer thy raw_th; fun infer ((xi, T), cu) (tyenv, maxidx) = let val _ = Thm.ctyp_of ctxt T; val _ = Thm.transfer_cterm thy cu; val U = Thm.typ_of_cterm cu; val maxidx' = maxidx |> Integer.max (#2 xi) |> Term.maxidx_typ T |> Integer.max (Thm.maxidx_of_cterm cu); val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx') handle Type.TUNIFY => let val t = Var (xi, T); val u = Thm.term_of cu; in raise THM ("infer_instantiate_types: type " ^ Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^ Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^ "\ncannot be unified with type " ^ Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^ Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u), 0, [th]) end; in (tyenv', maxidx'') end; val (tyenv, _) = fold infer args (Vartab.empty, 0); val instT = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; val inst = args |> map (fn ((xi, T), cu) => ((xi, Envir.norm_type tyenv T), Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); in instantiate_normalize (instT, inst) th end handle CTERM (msg, _) => raise THM (msg, 0, [raw_th]) | TERM (msg, _) => raise THM (msg, 0, [raw_th]) | TYPE (msg, _, _) => raise THM (msg, 0, [raw_th]); fun infer_instantiate _ [] th = th | infer_instantiate ctxt args th = let val vars = Term.add_vars (Thm.full_prop_of th) []; val dups = duplicates (eq_fst op =) vars; val _ = null dups orelse raise THM ("infer_instantiate: inconsistent types for variables " ^ commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups), 0, [th]); val args' = args |> map_filter (fn (xi, cu) => AList.lookup (op =) vars xi |> Option.map (fn T => ((xi, T), cu))); in infer_instantiate_types ctxt args' th end; fun infer_instantiate' ctxt args th = let val vars = build_rev (Term.add_vars (Thm.full_prop_of th)); val args' = zip_options vars args handle ListPair.UnequalLengths => raise THM ("infer_instantiate': more instantiations than variables in thm", 0, [th]); in infer_instantiate_types ctxt args' th end; (** renaming of bound variables **) (* replace bound variables x_i in thm by y_i *) (* where vs = [(x_1, y_1), ..., (x_n, y_n)] *) fun rename_bvars [] thm = thm | rename_bvars vs thm = let fun rename (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, rename t) | rename (t $ u) = rename t $ rename u | rename a = a; in Thm.renamed_prop (rename (Thm.prop_of thm)) thm end; (* renaming in left-to-right order *) fun rename_bvars' xs thm = let fun rename [] t = ([], t) | rename (x' :: xs) (Abs (x, T, t)) = let val (xs', t') = rename xs t in (xs', Abs (the_default x x', T, t')) end | rename xs (t $ u) = let val (xs', t') = rename xs t; val (xs'', u') = rename xs' u; in (xs'', t' $ u') end | rename xs a = (xs, a); in (case rename xs (Thm.prop_of thm) of ([], prop') => Thm.renamed_prop prop' thm | _ => error "More names than abstractions in theorem") end; end; structure Basic_Drule: BASIC_DRULE = Drule; open Basic_Drule; diff --git a/src/Pure/more_thm.ML b/src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML +++ b/src/Pure/more_thm.ML @@ -1,777 +1,790 @@ (* Title: Pure/more_thm.ML Author: Makarius Further operations on type ctyp/cterm/thm, outside the inference kernel. *) infix aconvc; signature BASIC_THM = sig include BASIC_THM val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T structure Ctermtab: TABLE structure Thmtab: TABLE val aconvc: cterm * cterm -> bool type attribute = Context.generic * thm -> Context.generic option * thm option end; signature THM = sig include THM structure Ctermtab: TABLE structure Thmtab: TABLE val eq_ctyp: ctyp * ctyp -> bool val aconvc: cterm * cterm -> bool - val add_tvars: thm -> ctyp list -> ctyp list - val add_vars: thm -> cterm list -> cterm list + val add_tvars: thm -> ctyp Term_Subst.TVars.table -> ctyp Term_Subst.TVars.table + val add_vars: thm -> cterm Term_Subst.Vars.table -> cterm Term_Subst.Vars.table val frees_of: thm -> cterm list val dest_funT: ctyp -> ctyp * ctyp val strip_type: ctyp -> ctyp list * ctyp val all_name: Proof.context -> string * cterm -> cterm -> cterm val all: Proof.context -> cterm -> cterm -> cterm val mk_binop: cterm -> cterm -> cterm -> cterm val dest_binop: cterm -> cterm * cterm val dest_implies: cterm -> cterm * cterm val dest_equals: cterm -> cterm * cterm val dest_equals_lhs: cterm -> cterm val dest_equals_rhs: cterm -> cterm val lhs_of: thm -> cterm val rhs_of: thm -> cterm val fast_term_ord: cterm ord val term_ord: cterm ord val thm_ord: thm ord val cterm_cache: (cterm -> 'a) -> cterm -> 'a val thm_cache: (thm -> 'a) -> thm -> 'a val is_reflexive: thm -> bool val eq_thm: thm * thm -> bool val eq_thm_prop: thm * thm -> bool val eq_thm_strict: thm * thm -> bool val equiv_thm: theory -> thm * thm -> bool val class_triv: theory -> class -> thm val of_sort: ctyp * sort -> thm list val is_dummy: thm -> bool val add_thm: thm -> thm list -> thm list val del_thm: thm -> thm list -> thm list val merge_thms: thm list * thm list -> thm list val item_net: thm Item_Net.T val item_net_intro: thm Item_Net.T val item_net_elim: thm Item_Net.T val declare_hyps: cterm -> Proof.context -> Proof.context val assume_hyps: cterm -> Proof.context -> thm * Proof.context val unchecked_hyps: Proof.context -> Proof.context val restore_hyps: Proof.context -> Proof.context -> Proof.context val undeclared_hyps: Context.generic -> thm -> term list val check_hyps: Context.generic -> thm -> thm val declare_term_sorts: term -> Proof.context -> Proof.context val extra_shyps': Proof.context -> thm -> sort list val check_shyps: Proof.context -> thm -> thm val weaken_sorts': Proof.context -> cterm -> cterm val elim_implies: thm -> thm -> thm val forall_intr_name: string * cterm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm val instantiate': ctyp option list -> cterm option list -> thm -> thm val forall_intr_frees: thm -> thm val unvarify_global: theory -> thm -> thm val unvarify_axiom: theory -> string -> thm val rename_params_rule: string list * int -> thm -> thm val rename_boundvars: term -> term -> thm -> thm val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory val add_axiom_global: binding * term -> theory -> (string * thm) * theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory type attribute = Context.generic * thm -> Context.generic option * thm option type binding = binding * attribute list val tag_rule: string * string -> thm -> thm val untag_rule: string -> thm -> thm val is_free_dummy: thm -> bool val tag_free_dummy: thm -> thm val def_name: string -> string val def_name_optional: string -> string -> string val def_binding: Binding.binding -> Binding.binding val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding val make_def_binding: bool -> Binding.binding -> Binding.binding val has_name_hint: thm -> bool val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm val theoremK: string val legacy_get_kind: thm -> string val kind_rule: string -> thm -> thm val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic val theory_attributes: attribute list -> thm -> theory -> thm * theory val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list val tag: string * string -> attribute val untag: string -> attribute val kind: string -> attribute val register_proofs: thm list lazy -> theory -> theory val consolidate_theory: theory -> unit val expose_theory: theory -> unit val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val pretty_thm_item: Proof.context -> thm -> Pretty.T val pretty_thm_global: theory -> thm -> Pretty.T val string_of_thm: Proof.context -> thm -> string val string_of_thm_global: theory -> thm -> string end; structure Thm: THM = struct (** basic operations **) (* collecting ctyps and cterms *) val eq_ctyp = op = o apply2 Thm.typ_of; val op aconvc = op aconv o apply2 Thm.term_of; val add_tvars = - Thm.fold_atomic_ctyps {hyps = false} (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); + Thm.fold_atomic_ctyps {hyps = false} (fn cT => fn tab => + (case Thm.typ_of cT of + TVar v => + if not (Term_Subst.TVars.defined tab v) + then Term_Subst.TVars.update (v, cT) tab + else tab + | _ => tab)); + val add_vars = - Thm.fold_atomic_cterms {hyps = false} (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); + Thm.fold_atomic_cterms {hyps = false} (fn ct => fn tab => + (case Thm.term_of ct of + Var v => + if not (Term_Subst.Vars.defined tab v) + then Term_Subst.Vars.update (v, ct) tab + else tab + | _ => tab)); fun frees_of th = (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} (fn a => fn (set, list) => (case Thm.term_of a of Free v => if not (Term_Subst.Frees.defined set v) then (Term_Subst.Frees.add (v, ()) set, a :: list) else (set, list) | _ => (set, list))) |> #2; (* ctyp operations *) fun dest_funT cT = (case Thm.typ_of cT of Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end | T => raise TYPE ("dest_funT", [T], [])); (* ctyp version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *) fun strip_type cT = (case Thm.typ_of cT of Type ("fun", _) => let val (cT1, cT2) = dest_funT cT; val (cTs, cT') = strip_type cT2 in (cT1 :: cTs, cT') end | _ => ([], cT)); (* cterm operations *) fun all_name ctxt (x, t) A = let val T = Thm.typ_of_cterm t; val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT)); in Thm.apply all_const (Thm.lambda_name (x, t) A) end; fun all ctxt t A = all_name ctxt ("", t) A; fun mk_binop c a b = Thm.apply (Thm.apply c a) b; fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct); fun dest_implies ct = (case Thm.term_of ct of Const ("Pure.imp", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_implies", [Thm.term_of ct])); fun dest_equals ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_equals", [Thm.term_of ct])); fun dest_equals_lhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); fun dest_equals_rhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); val lhs_of = dest_equals_lhs o Thm.cprop_of; val rhs_of = dest_equals_rhs o Thm.cprop_of; (* certified term order *) val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of; val term_ord = Term_Ord.term_ord o apply2 Thm.term_of; (* thm order: ignores theory context! *) val thm_ord = Term_Ord.fast_term_ord o apply2 Thm.prop_of ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 Thm.tpairs_of ||| list_ord Term_Ord.fast_term_ord o apply2 Thm.hyps_of ||| list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of; (* tables and caches *) structure Ctermtab = Table(type key = cterm val ord = fast_term_ord); structure Thmtab = Table(type key = thm val ord = thm_ord); fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f; (* equality *) fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) handle TERM _ => false; val eq_thm = is_equal o thm_ord; val eq_thm_prop = op aconv o apply2 Thm.full_prop_of; fun eq_thm_strict ths = eq_thm ths andalso Context.eq_thy_id (apply2 Thm.theory_id ths) andalso op = (apply2 Thm.maxidx_of ths) andalso op = (apply2 Thm.get_tags ths); (* pattern equivalence *) fun equiv_thm thy ths = Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths); (* type classes and sorts *) fun class_triv thy c = Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c); fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S; (* misc operations *) fun is_dummy thm = (case try Logic.dest_term (Thm.concl_of thm) of NONE => false | SOME t => Term.is_dummy_pattern (Term.head_of t)); (* collections of theorems in canonical order *) val add_thm = update eq_thm_prop; val del_thm = remove eq_thm_prop; val merge_thms = merge eq_thm_prop; val item_net = Item_Net.init eq_thm_prop (single o Thm.full_prop_of); val item_net_intro = Item_Net.init eq_thm_prop (single o Thm.concl_of); val item_net_elim = Item_Net.init eq_thm_prop (single o Thm.major_prem_of); (** declared hyps and sort hyps **) structure Hyps = Proof_Data ( type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T}; fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []}; ); fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps) in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end); (* hyps *) fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) => let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct; val hyps' = Termtab.update (Thm.term_of ct, ()) hyps; in (checked_hyps, hyps', shyps) end); fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps)); fun restore_hyps ctxt = map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps)); fun undeclared_hyps context th = Thm.hyps_of th |> filter_out (case context of Context.Theory _ => K false | Context.Proof ctxt => (case Hyps.get ctxt of {checked_hyps = false, ...} => K true | {hyps, ...} => Termtab.defined hyps)); fun check_hyps context th = (case undeclared_hyps context th of [] => th | undeclared => error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared)))); (* shyps *) fun declare_term_sorts t = map_hyps (fn (checked_hyps, hyps, shyps) => (checked_hyps, hyps, Sorts.insert_term t shyps)); fun extra_shyps' ctxt th = Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); fun check_shyps ctxt raw_th = let val th = Thm.strip_shyps raw_th; val extra_shyps = extra_shyps' ctxt th; in if null extra_shyps then th else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) end; val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; (** basic derived rules **) (*Elimination of implication A A \ B ------------ B *) fun elim_implies thA thAB = Thm.implies_elim thAB thA; (* forall_intr_name *) fun forall_intr_name (a, x) th = let val th' = Thm.forall_intr x th; val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b)); in Thm.renamed_prop prop' th' end; (* forall_elim_var(s) *) local fun dest_all ct = (case Thm.term_of ct of Const ("Pure.all", _) $ Abs (a, _, _) => let val (x, ct') = Thm.dest_abs NONE (Thm.dest_arg ct) in SOME ((a, Thm.ctyp_of_cterm x), ct') end | _ => NONE); fun dest_all_list ct = (case dest_all ct of NONE => [] | SOME (v, ct') => v :: dest_all_list ct'); fun forall_elim_vars_list vars i th = let val used = (Thm.fold_terms {hyps = false} o Term.fold_aterms) (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th []; val vars' = (Name.variant_list used (map #1 vars), vars) |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T)); in fold Thm.forall_elim vars' th end; in fun forall_elim_vars i th = forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th; fun forall_elim_var i th = let val vars = (case dest_all (Thm.cprop_of th) of SOME (v, _) => [v] | NONE => raise THM ("forall_elim_var", i, [th])); in forall_elim_vars_list vars i th end; end; (* instantiate frees *) fun instantiate_frees ([], []) th = th | instantiate_frees (instT, inst) th = let val idx = Thm.maxidx_of th + 1; fun index ((a, A), b) = (((a, idx), A), b); val insts = (map index instT, map index inst); val tfrees = Symtab.build (fold (Symtab.insert_set o #1 o #1) instT); val frees = Symtab.build (fold (Symtab.insert_set o #1 o #1) inst); val hyps = Thm.chyps_of th; val inst_cterm = Thm.generalize_cterm (tfrees, frees) idx #> Thm.instantiate_cterm insts; in th |> fold_rev Thm.implies_intr hyps |> Thm.generalize (tfrees, frees) idx |> Thm.instantiate insts |> fold (elim_implies o Thm.assume o inst_cterm) hyps end; (* instantiate by left-to-right occurrence of variables *) fun instantiate' cTs cts thm = let fun err msg = raise TYPE ("instantiate': " ^ msg, map_filter (Option.map Thm.typ_of) cTs, map_filter (Option.map Thm.term_of) cts); fun zip_vars xs ys = zip_options xs ys handle ListPair.UnequalLengths => err "more instantiations than variables in thm"; val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs; val thm' = Thm.instantiate (instT, []) thm; val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts; in Thm.instantiate ([], inst) thm' end; (* forall_intr_frees: generalization over all suitable Free variables *) fun forall_intr_frees th = let val fixed0 = Term_Subst.Frees.build (fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #> fold Term_Subst.add_frees (Thm.hyps_of th)); val (_, frees) = (th, (fixed0, [])) |-> Thm.fold_atomic_cterms {hyps = false} (fn a => fn (fixed, frees) => (case Thm.term_of a of Free v => if not (Term_Subst.Frees.defined fixed v) then (Term_Subst.Frees.add (v, ()) fixed, a :: frees) else (fixed, frees) | _ => (fixed, frees))); in fold Thm.forall_intr frees th end; (* unvarify_global: global schematic variables *) fun unvarify_global thy th = let val prop = Thm.full_prop_of th; val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) handle TERM (msg, _) => raise THM (msg, 0, [th]); val cert = Thm.global_cterm_of thy; val certT = Thm.global_ctyp_of thy; val instT = Term_Subst.TVars.build (prop |> (Term.fold_types o Term.fold_atyps) (fn T => fn instT => (case T of TVar (v as ((a, _), S)) => if Term_Subst.TVars.defined instT v then instT else Term_Subst.TVars.update (v, TFree (a, S)) instT | _ => instT))); val cinstT = Term_Subst.TVars.map (K certT) instT; val cinst = Term_Subst.Vars.build (prop |> Term.fold_aterms (fn t => fn inst => (case t of Var ((x, i), T) => let val T' = Term_Subst.instantiateT instT T in Term_Subst.Vars.update (((x, i), T'), cert (Free ((x, T')))) inst end | _ => inst))); in Thm.instantiate (Term_Subst.TVars.dest cinstT, Term_Subst.Vars.dest cinst) th end; fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; (* user renaming of parameters in a subgoal *) (*The names, if distinct, are used for the innermost parameters of subgoal i; preceding parameters may be renamed to make all parameters distinct.*) fun rename_params_rule (names, i) st = let val (_, Bs, Bi, C) = Thm.dest_state (st, i); val params = map #1 (Logic.strip_params Bi); val short = length params - length names; val names' = if short < 0 then error "More names than parameters in subgoal!" else Name.variant_list names (take short params) @ names; val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; val Bi' = Logic.list_rename_params names' Bi; in (case duplicates (op =) names of a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); st) | [] => (case inter (op =) names free_names of a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); st) | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st)) end; (* preservation of bound variable names *) fun rename_boundvars pat obj th = (case Term.rename_abs pat obj (Thm.prop_of th) of NONE => th | SOME prop' => Thm.renamed_prop prop' th); (** specification primitives **) (* rules *) fun stripped_sorts thy t = let val tfrees = build_rev (Term.add_tfrees t); val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); val recover = map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) tfrees' tfrees; val strip = map (apply2 TFree) (tfrees ~~ tfrees'); val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; in (strip, recover, t') end; fun add_axiom ctxt (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val (strip, recover, prop') = stripped_sorts thy prop; val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip; val thy' = thy |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (recover, []) axm' |> unvarify_global thy' |> fold elim_implies of_sorts; in ((axm_name, thm), thy') end; fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (recover, []) axm' |> unvarify_global thy' |> fold_rev Thm.implies_intr prems; in ((axm_name, thm), thy') end; fun add_def_global unchecked overloaded arg thy = add_def (Defs.global_context thy) unchecked overloaded arg thy; (** theorem tags **) (* add / delete tags *) fun tag_rule tg = Thm.map_tags (insert (op =) tg); fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); (* free dummy thm -- for abstract closure *) val free_dummyN = "free_dummy"; fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; val tag_free_dummy = tag_rule (free_dummyN, ""); (* def_name *) fun def_name c = c ^ "_def"; fun def_name_optional c "" = def_name c | def_name_optional _ name = name; val def_binding = Binding.map_name def_name #> Binding.reset_pos; fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name; fun make_def_binding cond b = if cond then def_binding b else Binding.empty; (* unofficial theorem names *) fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); (* theorem kinds *) val theoremK = "theorem"; fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; (** attributes **) (*attributes subsume any kind of rules or context modifiers*) type attribute = Context.generic * thm -> Context.generic option * thm option; type binding = binding * attribute list; fun rule_attribute ths f (x, th) = (NONE, (case find_first is_free_dummy (th :: ths) of SOME th' => SOME th' | NONE => SOME (f x th))); fun declaration_attribute f (x, th) = (if is_free_dummy th then NONE else SOME (f th x), NONE); fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; fun apply_attribute (att: attribute) th x = let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th)) in (the_default th th', the_default x x') end; fun attribute_declaration att th x = #2 (apply_attribute att th x); fun apply_attributes mk dest = let fun app [] th x = (th, x) | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; in app end; val theory_attributes = apply_attributes Context.Theory Context.the_theory; val proof_attributes = apply_attributes Context.Proof Context.the_proof; fun no_attributes x = (x, []); fun simple_fact x = [(x, [])]; fun tag tg = rule_attribute [] (K (tag_rule tg)); fun untag s = rule_attribute [] (K (untag_rule s)); fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k)); (** forked proofs **) structure Proofs = Theory_Data ( type T = thm list lazy Inttab.table; val empty = Inttab.empty; val extend = I; val merge = Inttab.merge (K true); ); fun reset_proofs thy = if Inttab.is_empty (Proofs.get thy) then NONE else SOME (Proofs.put Inttab.empty thy); val _ = Theory.setup (Theory.at_begin reset_proofs); fun register_proofs ths thy = let val entry = (serial (), Lazy.map_finished (map Thm.trim_context) ths) in (Proofs.map o Inttab.update) entry thy end; fun force_proofs thy = Proofs.get thy |> Inttab.dest |> maps (map (Thm.transfer thy) o Lazy.force o #2); val consolidate_theory = Thm.consolidate o force_proofs; fun expose_theory thy = if Proofterm.export_enabled () then Thm.expose_proofs thy (force_proofs thy) else (); (** print theorems **) (* options *) val show_consts = Config.declare_option_bool ("show_consts", \<^here>); val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false); val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false); (* pretty_thm etc. *) fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; val pretty_tags = Pretty.list "[" "]" o map pretty_tag; fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = let val show_tags = Config.get ctxt show_tags; val show_hyps = Config.get ctxt show_hyps; val th = raw_th |> perhaps (try (Thm.transfer' ctxt)) |> perhaps (try Thm.strip_shyps); val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; val extra_shyps = extra_shyps' ctxt th; val tags = Thm.get_tags th; val tpairs = Thm.tpairs_of th; val q = if quote then Pretty.quote else I; val prt_term = q o Syntax.pretty_term ctxt; val hlen = length extra_shyps + length hyps + length tpairs; val hsymbs = if hlen = 0 then [] else if show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" (map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ map (Syntax.pretty_sort ctxt) extra_shyps)] else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; val tsymbs = if null tags orelse not show_tags then [] else [Pretty.brk 1, pretty_tags tags]; in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; fun pretty_thm_global thy = pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; val string_of_thm = Pretty.string_of oo pretty_thm; val string_of_thm_global = Pretty.string_of oo pretty_thm_global; open Thm; end; structure Basic_Thm: BASIC_THM = Thm; open Basic_Thm;