--- 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)