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 cprems_of : thm -> cterm list |
21 val cprems_of : thm -> cterm list |
22 val cskip_flexpairs : cterm -> cterm |
22 val cskip_flexpairs : cterm -> cterm |
23 val cstrip_imp_prems : cterm -> cterm list |
23 val cstrip_imp_prems : cterm -> cterm list |
24 val cterm_instantiate : (cterm*cterm)list -> thm -> thm |
24 val cterm_instantiate : (cterm*cterm)list -> thm -> thm |
25 val cut_rl : thm |
25 val cut_rl : thm |
26 val equal_abs_elim : cterm -> thm -> thm |
26 val equal_abs_elim : cterm -> thm -> thm |
27 val equal_abs_elim_list: cterm list -> thm -> thm |
27 val equal_abs_elim_list: cterm list -> thm -> thm |
28 val eq_thm : thm * thm -> bool |
28 val eq_thm : thm * thm -> bool |
29 val same_thm : thm * thm -> bool |
29 val same_thm : thm * thm -> bool |
30 val eq_thm_sg : thm * thm -> bool |
30 val eq_thm_sg : thm * thm -> bool |
31 val flexpair_abs_elim_list: cterm list -> thm -> thm |
31 val flexpair_abs_elim_list: cterm list -> thm -> thm |
32 val forall_intr_list : cterm list -> thm -> thm |
32 val forall_intr_list : cterm list -> thm -> thm |
33 val forall_intr_frees : thm -> thm |
33 val forall_intr_frees : thm -> thm |
34 val forall_intr_vars : thm -> thm |
34 val forall_intr_vars : thm -> thm |
35 val forall_elim_list : cterm list -> thm -> thm |
35 val forall_elim_list : cterm list -> thm -> thm |
36 val forall_elim_var : int -> thm -> thm |
36 val forall_elim_var : int -> thm -> thm |
37 val forall_elim_vars : int -> thm -> thm |
37 val forall_elim_vars : int -> thm -> thm |
38 val implies_elim_list : thm -> thm list -> thm |
38 val implies_elim_list : thm -> thm list -> thm |
39 val implies_intr_list : cterm list -> thm -> thm |
39 val implies_intr_list : cterm list -> thm -> thm |
40 val MRL : thm list list * thm list -> thm list |
40 val MRL : thm list list * thm list -> thm list |
41 val MRS : thm list * thm -> thm |
41 val MRS : thm list * thm -> thm |
42 val pprint_cterm : cterm -> pprint_args -> unit |
42 val pprint_cterm : cterm -> pprint_args -> unit |
43 val pprint_ctyp : ctyp -> pprint_args -> unit |
43 val pprint_ctyp : ctyp -> pprint_args -> unit |
44 val pprint_theory : theory -> pprint_args -> unit |
44 val pprint_theory : theory -> pprint_args -> unit |
45 val pprint_thm : thm -> pprint_args -> unit |
45 val pprint_thm : thm -> pprint_args -> unit |
46 val pretty_thm : thm -> Sign.Syntax.Pretty.T |
46 val pretty_thm : thm -> Sign.Syntax.Pretty.T |
47 val print_cterm : cterm -> unit |
47 val print_cterm : cterm -> unit |
48 val print_ctyp : ctyp -> unit |
48 val print_ctyp : ctyp -> unit |
49 val print_goals : int -> thm -> unit |
49 val print_goals : int -> thm -> unit |
50 val print_goals_ref : (int -> thm -> unit) ref |
50 val print_goals_ref : (int -> thm -> unit) ref |
51 val print_syntax : theory -> unit |
51 val print_syntax : theory -> unit |
52 val print_theory : theory -> unit |
52 val print_theory : theory -> unit |
53 val print_thm : thm -> unit |
53 val print_thm : thm -> unit |
54 val prth : thm -> thm |
54 val prth : thm -> thm |
55 val prthq : thm Sequence.seq -> thm Sequence.seq |
55 val prthq : thm Sequence.seq -> thm Sequence.seq |
56 val prths : thm list -> thm list |
56 val prths : thm list -> thm list |
57 val read_instantiate : (string*string)list -> thm -> thm |
57 val read_instantiate : (string*string)list -> thm -> thm |
58 val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm |
58 val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm |
59 val read_insts : |
59 val read_insts : |
60 Sign.sg -> (indexname -> typ option) * (indexname -> sort option) |
60 Sign.sg -> (indexname -> typ option) * (indexname -> sort option) |
61 -> (indexname -> typ option) * (indexname -> sort option) |
61 -> (indexname -> typ option) * (indexname -> sort option) |
62 -> string list -> (string*string)list |
62 -> string list -> (string*string)list |
63 -> (indexname*ctyp)list * (cterm*cterm)list |
63 -> (indexname*ctyp)list * (cterm*cterm)list |
64 val reflexive_thm : thm |
64 val reflexive_thm : thm |
65 val revcut_rl : thm |
65 val revcut_rl : thm |
66 val rewrite_goal_rule : bool*bool -> (meta_simpset -> thm -> thm option) |
66 val rewrite_goal_rule : bool*bool -> (meta_simpset -> thm -> thm option) |
67 -> meta_simpset -> int -> thm -> thm |
67 -> meta_simpset -> int -> thm -> thm |
68 val rewrite_goals_rule: thm list -> thm -> thm |
68 val rewrite_goals_rule: thm list -> thm -> thm |
69 val rewrite_rule : thm list -> thm -> thm |
69 val rewrite_rule : thm list -> thm -> thm |
70 val RS : thm * thm -> thm |
70 val RS : thm * thm -> thm |
71 val RSN : thm * (int * thm) -> thm |
71 val RSN : thm * (int * thm) -> thm |
72 val RL : thm list * thm list -> thm list |
72 val RL : thm list * thm list -> thm list |
73 val RLN : thm list * (int * thm list) -> thm list |
73 val RLN : thm list * (int * thm list) -> thm list |
74 val show_hyps : bool ref |
74 val show_hyps : bool ref |
75 val size_of_thm : thm -> int |
75 val size_of_thm : thm -> int |
76 val standard : thm -> thm |
76 val standard : thm -> thm |
77 val string_of_cterm : cterm -> string |
77 val string_of_cterm : cterm -> string |
78 val string_of_ctyp : ctyp -> string |
78 val string_of_ctyp : ctyp -> string |
79 val string_of_thm : thm -> string |
79 val string_of_thm : thm -> string |
80 val symmetric_thm : thm |
80 val symmetric_thm : thm |
81 val thin_rl : thm |
81 val thin_rl : thm |
82 val transitive_thm : thm |
82 val transitive_thm : thm |
83 val triv_forall_equality: thm |
83 val triv_forall_equality: thm |
84 val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) |
84 val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) |
85 val zero_var_indexes : thm -> thm |
85 val zero_var_indexes : thm -> thm |
86 end |
86 end |
87 end; |
87 end; |
88 |
88 |
89 |
89 |
90 functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE = |
90 functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE = |
730 fun rew_conv mode prover mss = rewrite_cterm mode mss prover; |
730 fun rew_conv mode prover mss = rewrite_cterm mode mss prover; |
731 |
731 |
732 (*Rewrite a theorem*) |
732 (*Rewrite a theorem*) |
733 fun rewrite_rule [] th = th |
733 fun rewrite_rule [] th = th |
734 | rewrite_rule thms th = |
734 | rewrite_rule thms th = |
735 fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th; |
735 fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th; |
736 |
736 |
737 (*Rewrite the subgoals of a proof state (represented by a theorem) *) |
737 (*Rewrite the subgoals of a proof state (represented by a theorem) *) |
738 fun rewrite_goals_rule [] th = th |
738 fun rewrite_goals_rule [] th = th |
739 | rewrite_goals_rule thms th = |
739 | rewrite_goals_rule thms th = |
740 fconv_rule (goals_conv (K true) |
740 fconv_rule (goals_conv (K true) |
741 (rew_conv (true,false) (K(K None)) |
741 (rew_conv (true,false) (K(K None)) |
742 (Thm.mss_of thms))) |
742 (Thm.mss_of thms))) |
743 th; |
743 th; |
744 |
744 |
745 (*Rewrite the subgoal of a proof state (represented by a theorem) *) |
745 (*Rewrite the subgoal of a proof state (represented by a theorem) *) |
746 fun rewrite_goal_rule mode prover mss i thm = |
746 fun rewrite_goal_rule mode prover mss i thm = |
747 if 0 < i andalso i <= nprems_of thm |
747 if 0 < i andalso i <= nprems_of thm |
748 then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm |
748 then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm |