8 |
8 |
9 infix 0 RS RSN RL RLN MRS MRL OF COMP; |
9 infix 0 RS RSN RL RLN MRS MRL OF COMP; |
10 |
10 |
11 signature BASIC_DRULE = |
11 signature BASIC_DRULE = |
12 sig |
12 sig |
13 val mk_implies : cterm * cterm -> cterm |
13 val mk_implies: cterm * cterm -> cterm |
14 val list_implies : cterm list * cterm -> cterm |
14 val list_implies: cterm list * cterm -> cterm |
15 val dest_implies : cterm -> cterm * cterm |
15 val dest_implies: cterm -> cterm * cterm |
16 val dest_equals : cterm -> cterm * cterm |
16 val dest_equals: cterm -> cterm * cterm |
17 val strip_imp_prems : cterm -> cterm list |
17 val strip_imp_prems: cterm -> cterm list |
18 val strip_imp_concl : cterm -> cterm |
18 val strip_imp_concl: cterm -> cterm |
19 val cprems_of : thm -> cterm list |
19 val cprems_of: thm -> cterm list |
20 val cterm_fun : (term -> term) -> (cterm -> cterm) |
20 val cterm_fun: (term -> term) -> (cterm -> cterm) |
21 val ctyp_fun : (typ -> typ) -> (ctyp -> ctyp) |
21 val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp) |
22 val read_insts : |
22 val read_insts: |
23 theory -> (indexname -> typ option) * (indexname -> sort option) |
23 theory -> (indexname -> typ option) * (indexname -> sort option) |
24 -> (indexname -> typ option) * (indexname -> sort option) |
24 -> (indexname -> typ option) * (indexname -> sort option) |
25 -> string list -> (indexname * string) list |
25 -> string list -> (indexname * string) list |
26 -> (ctyp * ctyp) list * (cterm * cterm) list |
26 -> (ctyp * ctyp) list * (cterm * cterm) list |
27 val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) |
27 val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) |
28 val strip_shyps_warning : thm -> thm |
28 val strip_shyps_warning: thm -> thm |
29 val forall_intr_list : cterm list -> thm -> thm |
29 val forall_intr_list: cterm list -> thm -> thm |
30 val forall_intr_frees : thm -> thm |
30 val forall_intr_frees: thm -> thm |
31 val forall_intr_vars : thm -> thm |
31 val forall_intr_vars: thm -> thm |
32 val forall_elim_list : cterm list -> thm -> thm |
32 val forall_elim_list: cterm list -> thm -> thm |
33 val forall_elim_var : int -> thm -> thm |
33 val forall_elim_var: int -> thm -> thm |
34 val forall_elim_vars : int -> thm -> thm |
34 val forall_elim_vars: int -> thm -> thm |
35 val gen_all : thm -> thm |
35 val gen_all: thm -> thm |
36 val lift_all : cterm -> thm -> thm |
36 val lift_all: cterm -> thm -> thm |
37 val freeze_thaw : thm -> thm * (thm -> thm) |
37 val freeze_thaw: thm -> thm * (thm -> thm) |
38 val freeze_thaw_robust: thm -> thm * (int -> thm -> thm) |
38 val freeze_thaw_robust: thm -> thm * (int -> thm -> thm) |
39 val implies_elim_list : thm -> thm list -> thm |
39 val implies_elim_list: thm -> thm list -> thm |
40 val implies_intr_list : cterm list -> thm -> thm |
40 val implies_intr_list: cterm list -> thm -> thm |
41 val instantiate : |
41 val instantiate: |
42 (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm |
42 (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm |
43 val zero_var_indexes : thm -> thm |
43 val zero_var_indexes: thm -> thm |
44 val implies_intr_hyps : thm -> thm |
44 val implies_intr_hyps: thm -> thm |
45 val standard : thm -> thm |
45 val standard: thm -> thm |
46 val standard' : thm -> thm |
46 val standard': thm -> thm |
47 val rotate_prems : int -> thm -> thm |
47 val rotate_prems: int -> thm -> thm |
48 val rearrange_prems : int list -> thm -> thm |
48 val rearrange_prems: int list -> thm -> thm |
49 val assume_ax : theory -> string -> thm |
49 val assume_ax: theory -> string -> thm |
50 val RSN : thm * (int * thm) -> thm |
50 val RSN: thm * (int * thm) -> thm |
51 val RS : thm * thm -> thm |
51 val RS: thm * thm -> thm |
52 val RLN : thm list * (int * thm list) -> thm list |
52 val RLN: thm list * (int * thm list) -> thm list |
53 val RL : thm list * thm list -> thm list |
53 val RL: thm list * thm list -> thm list |
54 val MRS : thm list * thm -> thm |
54 val MRS: thm list * thm -> thm |
55 val MRL : thm list list * thm list -> thm list |
55 val MRL: thm list list * thm list -> thm list |
56 val OF : thm * thm list -> thm |
56 val OF: thm * thm list -> thm |
57 val compose : thm * int * thm -> thm list |
57 val compose: thm * int * thm -> thm list |
58 val COMP : thm * thm -> thm |
58 val COMP: thm * thm -> thm |
59 val read_instantiate_sg: theory -> (string*string)list -> thm -> thm |
59 val read_instantiate_sg: theory -> (string*string)list -> thm -> thm |
60 val read_instantiate : (string*string)list -> thm -> thm |
60 val read_instantiate: (string*string)list -> thm -> thm |
61 val cterm_instantiate : (cterm*cterm)list -> thm -> thm |
61 val cterm_instantiate: (cterm*cterm)list -> thm -> thm |
62 val eq_thm_thy : thm * thm -> bool |
62 val eq_thm_thy: thm * thm -> bool |
63 val eq_thm_prop : thm * thm -> bool |
63 val eq_thm_prop: thm * thm -> bool |
64 val weak_eq_thm : thm * thm -> bool |
64 val weak_eq_thm: thm * thm -> bool |
65 val size_of_thm : thm -> int |
65 val size_of_thm: thm -> int |
66 val reflexive_thm : thm |
66 val reflexive_thm: thm |
67 val symmetric_thm : thm |
67 val symmetric_thm: thm |
68 val transitive_thm : thm |
68 val transitive_thm: thm |
69 val symmetric_fun : thm -> thm |
69 val symmetric_fun: thm -> thm |
70 val extensional : thm -> thm |
70 val extensional: thm -> thm |
71 val imp_cong : thm |
71 val imp_cong: thm |
72 val swap_prems_eq : thm |
72 val swap_prems_eq: thm |
73 val equal_abs_elim : cterm -> thm -> thm |
73 val equal_abs_elim: cterm -> thm -> thm |
74 val equal_abs_elim_list: cterm list -> thm -> thm |
74 val equal_abs_elim_list: cterm list -> thm -> thm |
75 val asm_rl : thm |
75 val asm_rl: thm |
76 val cut_rl : thm |
76 val cut_rl: thm |
77 val revcut_rl : thm |
77 val revcut_rl: thm |
78 val thin_rl : thm |
78 val thin_rl: thm |
79 val triv_forall_equality: thm |
79 val triv_forall_equality: thm |
80 val swap_prems_rl : thm |
80 val swap_prems_rl: thm |
81 val equal_intr_rule : thm |
81 val equal_intr_rule: thm |
82 val equal_elim_rule1 : thm |
82 val equal_elim_rule1: thm |
83 val inst : string -> string -> thm -> thm |
83 val inst: string -> string -> thm -> thm |
84 val instantiate' : ctyp option list -> cterm option list -> thm -> thm |
84 val instantiate': ctyp option list -> cterm option list -> thm -> thm |
85 val incr_indexes : thm -> thm -> thm |
85 val incr_indexes: thm -> thm -> thm |
86 val incr_indexes_wrt : int list -> ctyp list -> cterm list -> thm list -> thm -> thm |
86 val incr_indexes_wrt: int list -> ctyp list -> cterm list -> thm list -> thm -> thm |
87 end; |
87 end; |
88 |
88 |
89 signature DRULE = |
89 signature DRULE = |
90 sig |
90 sig |
91 include BASIC_DRULE |
91 include BASIC_DRULE |
115 val add_rule: thm -> thm list -> thm list |
115 val add_rule: thm -> thm list -> thm list |
116 val del_rule: thm -> thm list -> thm list |
116 val del_rule: thm -> thm list -> thm list |
117 val add_rules: thm list -> thm list -> thm list |
117 val add_rules: thm list -> thm list -> thm list |
118 val del_rules: thm list -> thm list -> thm list |
118 val del_rules: thm list -> thm list -> thm list |
119 val merge_rules: thm list * thm list -> thm list |
119 val merge_rules: thm list * thm list -> thm list |
120 val imp_cong' : thm -> thm -> thm |
120 val imp_cong': thm -> thm -> thm |
121 val beta_eta_conversion: cterm -> thm |
121 val beta_eta_conversion: cterm -> thm |
122 val eta_long_conversion: cterm -> thm |
122 val eta_long_conversion: cterm -> thm |
123 val goals_conv : (int -> bool) -> (cterm -> thm) -> cterm -> thm |
123 val goals_conv: (int -> bool) -> (cterm -> thm) -> cterm -> thm |
124 val forall_conv : (cterm -> thm) -> cterm -> thm |
124 val forall_conv: (cterm -> thm) -> cterm -> thm |
125 val fconv_rule : (cterm -> thm) -> thm -> thm |
125 val fconv_rule: (cterm -> thm) -> thm -> thm |
126 val norm_hhf_eq: thm |
126 val norm_hhf_eq: thm |
127 val is_norm_hhf: term -> bool |
127 val is_norm_hhf: term -> bool |
128 val norm_hhf: theory -> term -> term |
128 val norm_hhf: theory -> term -> term |
129 val protect: cterm -> cterm |
129 val protect: cterm -> cterm |
130 val protectI: thm |
130 val protectI: thm |
131 val protectD: thm |
131 val protectD: thm |
|
132 val protect_cong: thm |
132 val implies_intr_protected: cterm list -> thm -> thm |
133 val implies_intr_protected: cterm list -> thm -> thm |
133 val freeze_all: thm -> thm |
134 val freeze_all: thm -> thm |
134 val tvars_of_terms: term list -> (indexname * sort) list |
135 val tvars_of_terms: term list -> (indexname * sort) list |
135 val vars_of_terms: term list -> (indexname * typ) list |
136 val vars_of_terms: term list -> (indexname * typ) list |
136 val tvars_of: thm -> (indexname * sort) list |
137 val tvars_of: thm -> (indexname * sort) list |
213 (*cterm version of list_comb: maps (f, [t1,...,tn]) to f(t1,...,tn) *) |
215 (*cterm version of list_comb: maps (f, [t1,...,tn]) to f(t1,...,tn) *) |
214 fun list_comb (f, []) = f |
216 fun list_comb (f, []) = f |
215 | list_comb (f, t::ts) = list_comb (Thm.capply f t, ts); |
217 | list_comb (f, t::ts) = list_comb (Thm.capply f t, ts); |
216 |
218 |
217 (*cterm version of strip_comb: maps f(t1,...,tn) to (f, [t1,...,tn]) *) |
219 (*cterm version of strip_comb: maps f(t1,...,tn) to (f, [t1,...,tn]) *) |
218 fun strip_comb ct = |
220 fun strip_comb ct = |
219 let |
221 let |
220 fun stripc (p as (ct, cts)) = |
222 fun stripc (p as (ct, cts)) = |
221 let val (ct1, ct2) = Thm.dest_comb ct |
223 let val (ct1, ct2) = Thm.dest_comb ct |
222 in stripc (ct1, ct2 :: cts) end handle CTERM _ => p |
224 in stripc (ct1, ct2 :: cts) end handle CTERM _ => p |
223 in stripc (ct, []) end; |
225 in stripc (ct, []) end; |
924 handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u]) |
929 handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u]) |
925 in (thy', tye', maxi') end; |
930 in (thy', tye', maxi') end; |
926 in |
931 in |
927 fun cterm_instantiate ctpairs0 th = |
932 fun cterm_instantiate ctpairs0 th = |
928 let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0 |
933 let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0 |
929 fun instT(ct,cu) = |
934 fun instT(ct,cu) = |
930 let val inst = cterm_of thy o Envir.subst_TVars tye o term_of |
935 let val inst = cterm_of thy o Envir.subst_TVars tye o term_of |
931 in (inst ct, inst cu) end |
936 in (inst ct, inst cu) end |
932 fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T) |
937 fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T) |
933 in instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end |
938 in instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end |
934 handle TERM _ => |
939 handle TERM _ => |