# HG changeset patch # User wenzelm # Date 880558539 -3600 # Node ID 05af145a61d4c3a07a38fd2f21e8ca455e409c39 # Parent eb65491ae776d06b7ef4662806a05f5ed1d36033 cleaned signature; added instantiate': ctyp option list -> cterm option list -> thm -> thm; diff -r eb65491ae776 -r 05af145a61d4 src/Pure/drule.ML --- a/src/Pure/drule.ML Wed Nov 26 16:34:13 1997 +0100 +++ b/src/Pure/drule.ML Wed Nov 26 16:35:39 1997 +0100 @@ -10,20 +10,16 @@ signature DRULE = sig - val asm_rl : thm - val assume_ax : theory -> string -> thm - val COMP : thm * thm -> thm - val compose : thm * int * thm -> thm list + val dest_implies : cterm -> cterm * cterm + val skip_flexpairs : cterm -> cterm + val strip_imp_prems : cterm -> cterm list val cprems_of : thm -> cterm list - val cterm_instantiate : (cterm*cterm)list -> thm -> thm - val cut_rl : thm - val equal_abs_elim : cterm -> thm -> thm - val equal_abs_elim_list: cterm list -> thm -> thm - val equal_intr_rule : thm - val eq_thm : thm * thm -> bool - val same_thm : thm * thm -> bool - val eq_thm_sg : thm * thm -> bool - val flexpair_abs_elim_list: cterm list -> thm -> thm + val read_insts : + Sign.sg -> (indexname -> typ option) * (indexname -> sort option) + -> (indexname -> typ option) * (indexname -> sort option) + -> string list -> (string*string)list + -> (indexname*ctyp)list * (cterm*cterm)list + val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) val forall_intr_list : cterm list -> thm -> thm val forall_intr_frees : thm -> thm val forall_intr_vars : thm -> thm @@ -32,40 +28,46 @@ val forall_elim_vars : int -> thm -> thm val implies_elim_list : thm -> thm list -> thm val implies_intr_list : cterm list -> thm -> thm - val dest_implies : cterm -> cterm * cterm + val zero_var_indexes : thm -> thm + val standard : thm -> thm + val assume_ax : theory -> string -> thm + val RSN : thm * (int * thm) -> thm + val RS : thm * 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 MRL : thm list list * thm list -> thm list - val MRS : thm list * thm -> thm - val read_instantiate : (string*string)list -> thm -> thm + val compose : thm * int * thm -> thm list + val COMP : thm * thm -> thm val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm - val read_insts : - Sign.sg -> (indexname -> typ option) * (indexname -> sort option) - -> (indexname -> typ option) * (indexname -> sort option) - -> string list -> (string*string)list - -> (indexname*ctyp)list * (cterm*cterm)list + val read_instantiate : (string*string)list -> thm -> thm + val cterm_instantiate : (cterm*cterm)list -> thm -> thm + val same_thm : thm * thm -> bool + val weak_eq_thm : thm * thm -> bool + val eq_thm_sg : thm * thm -> bool + val size_of_thm : thm -> int val reflexive_thm : thm + val symmetric_thm : thm + val transitive_thm : thm val refl_implies : thm - val revcut_rl : thm - val rewrite_goal_rule : bool * bool -> (meta_simpset -> thm -> thm option) - -> meta_simpset -> int -> thm -> thm - val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm val rewrite_rule_aux : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm val rewrite_thm : bool * bool -> (meta_simpset -> thm -> thm option) -> meta_simpset -> thm -> thm - val RS : thm * thm -> thm - val RSN : thm * (int * thm) -> thm - val RL : thm list * thm list -> thm list - val RLN : thm list * (int * thm list) -> thm list - val size_of_thm : thm -> int - val skip_flexpairs : cterm -> cterm - val standard : thm -> thm - val strip_imp_prems : cterm -> cterm list + val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm + val rewrite_goal_rule : bool * bool -> (meta_simpset -> thm -> thm option) + -> meta_simpset -> int -> thm -> thm + + val equal_abs_elim : cterm -> thm -> thm + val equal_abs_elim_list: cterm list -> thm -> thm + val flexpair_abs_elim_list: cterm list -> thm -> thm + val asm_rl : thm + val cut_rl : thm + val revcut_rl : thm + val thin_rl : thm + val triv_forall_equality: thm val swap_prems_rl : thm - val symmetric_thm : thm - val thin_rl : thm - val transitive_thm : thm - val triv_forall_equality: thm - val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) - val zero_var_indexes : thm -> thm + val equal_intr_rule : thm + val instantiate': ctyp option list -> cterm option list -> thm -> thm end; structure Drule : DRULE = @@ -575,6 +577,48 @@ (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) end; + + +(** instantiate' rule **) + +(* collect vars *) + +val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs); +val add_tvars = foldl_types add_tvarsT; +val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs); + +fun tvars_of thm = rev (add_tvars ([], #prop (Thm.rep_thm thm))); +fun vars_of thm = rev (add_vars ([], #prop (Thm.rep_thm thm))); + + +(* instantiate by left-to-right occurrence of variables *) + +fun instantiate' cTs cts thm = + let + fun err msg = + raise TYPE ("instantiate': " ^ msg, + mapfilter (apsome Thm.typ_of) cTs, + mapfilter (apsome Thm.term_of) cts); + + fun inst_of (v, ct) = + (Thm.cterm_of (#sign (Thm.rep_cterm ct)) (Var v), ct) + handle TYPE (msg, _, _) => err msg; + + fun zip_vars _ [] = [] + | zip_vars (_ :: vs) (None :: opt_ts) = zip_vars vs opt_ts + | zip_vars (v :: vs) (Some t :: opt_ts) = (v, t) :: zip_vars vs opt_ts + | zip_vars [] _ = err "more instantiations than variables in thm"; + + (*instantiate types first!*) + val thm' = + if forall is_none cTs then thm + else Thm.instantiate (zip_vars (map fst (tvars_of thm)) cTs, []) thm; + in + if forall is_none cts then thm' + else Thm.instantiate ([], map inst_of (zip_vars (vars_of thm') cts)) thm' + end; + + end; open Drule;