src/Pure/drule.ML
changeset 668 0d0923eb0f0d
parent 655 9748dbcd4157
child 708 8422e50adce0
equal deleted inserted replaced
667:661fc2e9c945 668:0d0923eb0f0d
    10 
    10 
    11 signature DRULE =
    11 signature DRULE =
    12   sig
    12   sig
    13   structure Thm : THM
    13   structure Thm : THM
    14   local open Thm  in
    14   local open Thm  in
    15   val add_defs: (string * string) list -> theory -> theory
    15   val add_defs		: (string * string) list -> theory -> theory
    16   val add_defs_i: (string * term) list -> theory -> theory
    16   val add_defs_i	: (string * term) list -> theory -> theory
    17   val asm_rl: thm
    17   val asm_rl		: thm
    18   val assume_ax: theory -> string -> thm
    18   val assume_ax		: theory -> string -> thm
    19   val COMP: thm * thm -> thm
    19   val COMP		: thm * thm -> thm
    20   val compose: thm * int * thm -> thm list
    20   val compose		: thm * int * thm -> thm list
    21   val cterm_instantiate: (cterm*cterm)list -> thm -> thm
    21   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    22   val cut_rl: thm
    22   val cut_rl		: thm
    23   val equal_abs_elim: cterm  -> thm -> thm
    23   val equal_abs_elim	: cterm  -> thm -> thm
    24   val equal_abs_elim_list: cterm list -> thm -> thm
    24   val equal_abs_elim_list: cterm list -> thm -> thm
    25   val eq_thm: thm * thm -> bool
    25   val eq_thm		: thm * thm -> bool
    26   val eq_thm_sg: thm * thm -> bool
    26   val eq_thm_sg		: thm * thm -> bool
    27   val flexpair_abs_elim_list: cterm list -> thm -> thm
    27   val flexpair_abs_elim_list: cterm list -> thm -> thm
    28   val forall_intr_list: cterm list -> thm -> thm
    28   val forall_intr_list	: cterm list -> thm -> thm
    29   val forall_intr_frees: thm -> thm
    29   val forall_intr_frees	: thm -> thm
    30   val forall_elim_list: cterm list -> thm -> thm
    30   val forall_elim_list	: cterm list -> thm -> thm
    31   val forall_elim_var: int -> thm -> thm
    31   val forall_elim_var	: int -> thm -> thm
    32   val forall_elim_vars: int -> thm -> thm
    32   val forall_elim_vars	: int -> thm -> thm
    33   val implies_elim_list: thm -> thm list -> thm
    33   val implies_elim_list	: thm -> thm list -> thm
    34   val implies_intr_list: cterm list -> thm -> thm
    34   val implies_intr_list	: cterm list -> thm -> thm
    35   val MRL: thm list list * thm list -> thm list
    35   val MRL		: thm list list * thm list -> thm list
    36   val MRS: thm list * thm -> thm
    36   val MRS		: thm list * thm -> thm
    37   val pprint_cterm: cterm -> pprint_args -> unit
    37   val pprint_cterm	: cterm -> pprint_args -> unit
    38   val pprint_ctyp: ctyp -> pprint_args -> unit
    38   val pprint_ctyp	: ctyp -> pprint_args -> unit
    39   val pprint_theory: theory -> pprint_args -> unit
    39   val pprint_theory	: theory -> pprint_args -> unit
    40   val pprint_thm: thm -> pprint_args -> unit
    40   val pprint_thm	: thm -> pprint_args -> unit
    41   val pretty_thm: thm -> Sign.Syntax.Pretty.T
    41   val pretty_thm	: thm -> Sign.Syntax.Pretty.T
    42   val print_cterm: cterm -> unit
    42   val print_cterm	: cterm -> unit
    43   val print_ctyp: ctyp -> unit
    43   val print_ctyp	: ctyp -> unit
    44   val print_goals: int -> thm -> unit
    44   val print_goals	: int -> thm -> unit
    45   val print_goals_ref: (int -> thm -> unit) ref
    45   val print_goals_ref	: (int -> thm -> unit) ref
    46   val print_syntax: theory -> unit
    46   val print_syntax	: theory -> unit
    47   val print_sign: theory -> unit
    47   val print_sign	: theory -> unit
    48   val print_axioms: theory -> unit
    48   val print_axioms	: theory -> unit
    49   val print_theory: theory -> unit
    49   val print_theory	: theory -> unit
    50   val print_thm: thm -> unit
    50   val print_thm		: thm -> unit
    51   val prth: thm -> thm
    51   val prth		: thm -> thm
    52   val prthq: thm Sequence.seq -> thm Sequence.seq
    52   val prthq		: thm Sequence.seq -> thm Sequence.seq
    53   val prths: thm list -> thm list
    53   val prths		: thm list -> thm list
    54   val read_instantiate: (string*string)list -> thm -> thm
    54   val read_instantiate	: (string*string)list -> thm -> thm
    55   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    55   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    56   val read_insts:
    56   val read_insts	:
    57           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    57           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    58                   -> (indexname -> typ option) * (indexname -> sort option)
    58                   -> (indexname -> typ option) * (indexname -> sort option)
    59                   -> (string*string)list
    59                   -> (string*string)list
    60                   -> (indexname*ctyp)list * (cterm*cterm)list
    60                   -> (indexname*ctyp)list * (cterm*cterm)list
    61   val reflexive_thm: thm
    61   val reflexive_thm	: thm
    62   val revcut_rl: thm
    62   val revcut_rl		: thm
    63   val rewrite_goal_rule: bool*bool -> (meta_simpset -> thm -> thm option)
    63   val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
    64         -> meta_simpset -> int -> thm -> thm
    64         -> meta_simpset -> int -> thm -> thm
    65   val rewrite_goals_rule: thm list -> thm -> thm
    65   val rewrite_goals_rule: thm list -> thm -> thm
    66   val rewrite_rule: thm list -> thm -> thm
    66   val rewrite_rule	: thm list -> thm -> thm
    67   val RS: thm * thm -> thm
    67   val RS		: thm * thm -> thm
    68   val RSN: thm * (int * thm) -> thm
    68   val RSN		: thm * (int * thm) -> thm
    69   val RL: thm list * thm list -> thm list
    69   val RL		: thm list * thm list -> thm list
    70   val RLN: thm list * (int * thm list) -> thm list
    70   val RLN		: thm list * (int * thm list) -> thm list
    71   val show_hyps: bool ref
    71   val show_hyps		: bool ref
    72   val size_of_thm: thm -> int
    72   val size_of_thm	: thm -> int
    73   val standard: thm -> thm
    73   val standard		: thm -> thm
    74   val string_of_cterm: cterm -> string
    74   val string_of_cterm	: cterm -> string
    75   val string_of_ctyp: ctyp -> string
    75   val string_of_ctyp	: ctyp -> string
    76   val string_of_thm: thm -> string
    76   val string_of_thm	: thm -> string
    77   val symmetric_thm: thm
    77   val symmetric_thm	: thm
    78   val transitive_thm: thm
    78   val thin_rl		: thm
       
    79   val transitive_thm	: thm
    79   val triv_forall_equality: thm
    80   val triv_forall_equality: thm
    80   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    81   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    81   val zero_var_indexes: thm -> thm
    82   val zero_var_indexes	: thm -> thm
    82   end
    83   end
    83   end;
    84   end;
       
    85 
    84 
    86 
    85 functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE =
    87 functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE =
    86 struct
    88 struct
    87 structure Thm = Thm;
    89 structure Thm = Thm;
    88 structure Sign = Thm.Sign;
    90 structure Sign = Thm.Sign;
   727   in  standard (implies_intr V
   729   in  standard (implies_intr V
   728                 (implies_intr VW
   730                 (implies_intr VW
   729                  (implies_elim (assume VW) (assume V))))
   731                  (implies_elim (assume VW) (assume V))))
   730   end;
   732   end;
   731 
   733 
       
   734 (*for deleting an unwanted assumption*)
       
   735 val thin_rl =
       
   736   let val V = read_cterm Sign.pure ("PROP V", propT)
       
   737       and W = read_cterm Sign.pure ("PROP W", propT);
       
   738   in  standard (implies_intr V (implies_intr W (assume W)))
       
   739   end;
       
   740 
   732 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   741 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   733 val triv_forall_equality =
   742 val triv_forall_equality =
   734   let val V  = read_cterm Sign.pure ("PROP V", propT)
   743   let val V  = read_cterm Sign.pure ("PROP V", propT)
   735       and QV = read_cterm Sign.pure ("!!x::'a. PROP V", propT)
   744       and QV = read_cterm Sign.pure ("!!x::'a. PROP V", propT)
   736       and x  = read_cterm Sign.pure ("x", TFree("'a",logicS));
   745       and x  = read_cterm Sign.pure ("x", TFree("'a",logicS));