# HG changeset patch # User lcp # Date 783622543 -3600 # Node ID 0d0923eb0f0d050240edbc9a8bd5a82afc2f86d4 # Parent 661fc2e9c9458b897c4452f363e8ba21eacf3cea Pure/drule/thin_rl: new diff -r 661fc2e9c945 -r 0d0923eb0f0d src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Oct 31 17:14:42 1994 +0100 +++ b/src/Pure/drule.ML Mon Oct 31 17:55:43 1994 +0100 @@ -12,76 +12,78 @@ sig structure Thm : THM local open Thm in - val add_defs: (string * string) list -> theory -> theory - val add_defs_i: (string * term) list -> theory -> theory - val asm_rl: thm - val assume_ax: theory -> string -> thm - val COMP: thm * thm -> thm - val compose: thm * int * thm -> thm list - val cterm_instantiate: (cterm*cterm)list -> thm -> thm - val cut_rl: thm - val equal_abs_elim: cterm -> thm -> thm + val add_defs : (string * string) list -> theory -> theory + val add_defs_i : (string * term) list -> theory -> theory + val asm_rl : thm + val assume_ax : theory -> string -> thm + val COMP : thm * thm -> thm + val compose : thm * int * thm -> thm list + val cterm_instantiate : (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 eq_thm: thm * thm -> bool - val eq_thm_sg: thm * thm -> bool + val eq_thm : thm * thm -> bool + val eq_thm_sg : thm * thm -> bool val flexpair_abs_elim_list: cterm list -> thm -> thm - val forall_intr_list: cterm list -> thm -> thm - val forall_intr_frees: thm -> thm - val forall_elim_list: cterm list -> thm -> thm - val forall_elim_var: int -> thm -> thm - val forall_elim_vars: int -> thm -> thm - val implies_elim_list: thm -> thm list -> thm - val implies_intr_list: cterm list -> thm -> thm - val MRL: thm list list * thm list -> thm list - val MRS: thm list * thm -> thm - val pprint_cterm: cterm -> pprint_args -> unit - val pprint_ctyp: ctyp -> pprint_args -> unit - val pprint_theory: theory -> pprint_args -> unit - val pprint_thm: thm -> pprint_args -> unit - val pretty_thm: thm -> Sign.Syntax.Pretty.T - val print_cterm: cterm -> unit - val print_ctyp: ctyp -> unit - val print_goals: int -> thm -> unit - val print_goals_ref: (int -> thm -> unit) ref - val print_syntax: theory -> unit - val print_sign: theory -> unit - val print_axioms: theory -> unit - val print_theory: theory -> unit - val print_thm: thm -> unit - val prth: thm -> thm - val prthq: thm Sequence.seq -> thm Sequence.seq - val prths: thm list -> thm list - val read_instantiate: (string*string)list -> thm -> thm + val forall_intr_list : cterm list -> thm -> thm + val forall_intr_frees : thm -> thm + val forall_elim_list : cterm list -> thm -> thm + val forall_elim_var : int -> thm -> thm + val forall_elim_vars : int -> thm -> thm + val implies_elim_list : thm -> thm list -> thm + val implies_intr_list : cterm list -> thm -> thm + val MRL : thm list list * thm list -> thm list + val MRS : thm list * thm -> thm + val pprint_cterm : cterm -> pprint_args -> unit + val pprint_ctyp : ctyp -> pprint_args -> unit + val pprint_theory : theory -> pprint_args -> unit + val pprint_thm : thm -> pprint_args -> unit + val pretty_thm : thm -> Sign.Syntax.Pretty.T + val print_cterm : cterm -> unit + val print_ctyp : ctyp -> unit + val print_goals : int -> thm -> unit + val print_goals_ref : (int -> thm -> unit) ref + val print_syntax : theory -> unit + val print_sign : theory -> unit + val print_axioms : theory -> unit + val print_theory : theory -> unit + val print_thm : thm -> unit + val prth : thm -> thm + val prthq : thm Sequence.seq -> thm Sequence.seq + val prths : thm list -> thm list + val read_instantiate : (string*string)list -> thm -> thm val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm - val read_insts: + val read_insts : Sign.sg -> (indexname -> typ option) * (indexname -> sort option) -> (indexname -> typ option) * (indexname -> sort option) -> (string*string)list -> (indexname*ctyp)list * (cterm*cterm)list - val reflexive_thm: thm - val revcut_rl: thm - val rewrite_goal_rule: bool*bool -> (meta_simpset -> thm -> thm option) + val reflexive_thm : 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: thm list -> thm -> thm - val rewrite_rule: thm list -> thm -> thm - val RS: thm * thm -> thm - val RSN: thm * (int * thm) -> thm - val RL: thm list * thm list -> thm list - val RLN: thm list * (int * thm list) -> thm list - val show_hyps: bool ref - val size_of_thm: thm -> int - val standard: thm -> thm - val string_of_cterm: cterm -> string - val string_of_ctyp: ctyp -> string - val string_of_thm: thm -> string - val symmetric_thm: thm - val transitive_thm: thm + val rewrite_rule : thm list -> thm -> thm + val RS : thm * thm -> thm + val RSN : thm * (int * thm) -> thm + val RL : thm list * thm list -> thm list + val RLN : thm list * (int * thm list) -> thm list + val show_hyps : bool ref + val size_of_thm : thm -> int + val standard : thm -> thm + val string_of_cterm : cterm -> string + val string_of_ctyp : ctyp -> string + val string_of_thm : thm -> string + 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 zero_var_indexes : thm -> thm end end; + functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE = struct structure Thm = Thm; @@ -729,6 +731,13 @@ (implies_elim (assume VW) (assume V)))) end; +(*for deleting an unwanted assumption*) +val thin_rl = + let val V = read_cterm Sign.pure ("PROP V", propT) + and W = read_cterm Sign.pure ("PROP W", propT); + in standard (implies_intr V (implies_intr W (assume W))) + end; + (* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*) val triv_forall_equality = let val V = read_cterm Sign.pure ("PROP V", propT)