1.1 --- a/src/Pure/drule.ML Wed Nov 16 17:45:24 2005 +0100
1.2 +++ b/src/Pure/drule.ML Wed Nov 16 17:45:25 2005 +0100
1.3 @@ -10,80 +10,80 @@
1.4
1.5 signature BASIC_DRULE =
1.6 sig
1.7 - val mk_implies : cterm * cterm -> cterm
1.8 - val list_implies : cterm list * cterm -> cterm
1.9 - val dest_implies : cterm -> cterm * cterm
1.10 - val dest_equals : cterm -> cterm * cterm
1.11 - val strip_imp_prems : cterm -> cterm list
1.12 - val strip_imp_concl : cterm -> cterm
1.13 - val cprems_of : thm -> cterm list
1.14 - val cterm_fun : (term -> term) -> (cterm -> cterm)
1.15 - val ctyp_fun : (typ -> typ) -> (ctyp -> ctyp)
1.16 - val read_insts :
1.17 + val mk_implies: cterm * cterm -> cterm
1.18 + val list_implies: cterm list * cterm -> cterm
1.19 + val dest_implies: cterm -> cterm * cterm
1.20 + val dest_equals: cterm -> cterm * cterm
1.21 + val strip_imp_prems: cterm -> cterm list
1.22 + val strip_imp_concl: cterm -> cterm
1.23 + val cprems_of: thm -> cterm list
1.24 + val cterm_fun: (term -> term) -> (cterm -> cterm)
1.25 + val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
1.26 + val read_insts:
1.27 theory -> (indexname -> typ option) * (indexname -> sort option)
1.28 -> (indexname -> typ option) * (indexname -> sort option)
1.29 -> string list -> (indexname * string) list
1.30 -> (ctyp * ctyp) list * (cterm * cterm) list
1.31 val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
1.32 - val strip_shyps_warning : thm -> thm
1.33 - val forall_intr_list : cterm list -> thm -> thm
1.34 - val forall_intr_frees : thm -> thm
1.35 - val forall_intr_vars : thm -> thm
1.36 - val forall_elim_list : cterm list -> thm -> thm
1.37 - val forall_elim_var : int -> thm -> thm
1.38 - val forall_elim_vars : int -> thm -> thm
1.39 - val gen_all : thm -> thm
1.40 - val lift_all : cterm -> thm -> thm
1.41 - val freeze_thaw : thm -> thm * (thm -> thm)
1.42 + val strip_shyps_warning: thm -> thm
1.43 + val forall_intr_list: cterm list -> thm -> thm
1.44 + val forall_intr_frees: thm -> thm
1.45 + val forall_intr_vars: thm -> thm
1.46 + val forall_elim_list: cterm list -> thm -> thm
1.47 + val forall_elim_var: int -> thm -> thm
1.48 + val forall_elim_vars: int -> thm -> thm
1.49 + val gen_all: thm -> thm
1.50 + val lift_all: cterm -> thm -> thm
1.51 + val freeze_thaw: thm -> thm * (thm -> thm)
1.52 val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
1.53 - val implies_elim_list : thm -> thm list -> thm
1.54 - val implies_intr_list : cterm list -> thm -> thm
1.55 - val instantiate :
1.56 + val implies_elim_list: thm -> thm list -> thm
1.57 + val implies_intr_list: cterm list -> thm -> thm
1.58 + val instantiate:
1.59 (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
1.60 - val zero_var_indexes : thm -> thm
1.61 - val implies_intr_hyps : thm -> thm
1.62 - val standard : thm -> thm
1.63 - val standard' : thm -> thm
1.64 - val rotate_prems : int -> thm -> thm
1.65 - val rearrange_prems : int list -> thm -> thm
1.66 - val assume_ax : theory -> string -> thm
1.67 - val RSN : thm * (int * thm) -> thm
1.68 - val RS : thm * thm -> thm
1.69 - val RLN : thm list * (int * thm list) -> thm list
1.70 - val RL : thm list * thm list -> thm list
1.71 - val MRS : thm list * thm -> thm
1.72 - val MRL : thm list list * thm list -> thm list
1.73 - val OF : thm * thm list -> thm
1.74 - val compose : thm * int * thm -> thm list
1.75 - val COMP : thm * thm -> thm
1.76 + val zero_var_indexes: thm -> thm
1.77 + val implies_intr_hyps: thm -> thm
1.78 + val standard: thm -> thm
1.79 + val standard': thm -> thm
1.80 + val rotate_prems: int -> thm -> thm
1.81 + val rearrange_prems: int list -> thm -> thm
1.82 + val assume_ax: theory -> string -> thm
1.83 + val RSN: thm * (int * thm) -> thm
1.84 + val RS: thm * thm -> thm
1.85 + val RLN: thm list * (int * thm list) -> thm list
1.86 + val RL: thm list * thm list -> thm list
1.87 + val MRS: thm list * thm -> thm
1.88 + val MRL: thm list list * thm list -> thm list
1.89 + val OF: thm * thm list -> thm
1.90 + val compose: thm * int * thm -> thm list
1.91 + val COMP: thm * thm -> thm
1.92 val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
1.93 - val read_instantiate : (string*string)list -> thm -> thm
1.94 - val cterm_instantiate : (cterm*cterm)list -> thm -> thm
1.95 - val eq_thm_thy : thm * thm -> bool
1.96 - val eq_thm_prop : thm * thm -> bool
1.97 - val weak_eq_thm : thm * thm -> bool
1.98 - val size_of_thm : thm -> int
1.99 - val reflexive_thm : thm
1.100 - val symmetric_thm : thm
1.101 - val transitive_thm : thm
1.102 - val symmetric_fun : thm -> thm
1.103 - val extensional : thm -> thm
1.104 - val imp_cong : thm
1.105 - val swap_prems_eq : thm
1.106 - val equal_abs_elim : cterm -> thm -> thm
1.107 + val read_instantiate: (string*string)list -> thm -> thm
1.108 + val cterm_instantiate: (cterm*cterm)list -> thm -> thm
1.109 + val eq_thm_thy: thm * thm -> bool
1.110 + val eq_thm_prop: thm * thm -> bool
1.111 + val weak_eq_thm: thm * thm -> bool
1.112 + val size_of_thm: thm -> int
1.113 + val reflexive_thm: thm
1.114 + val symmetric_thm: thm
1.115 + val transitive_thm: thm
1.116 + val symmetric_fun: thm -> thm
1.117 + val extensional: thm -> thm
1.118 + val imp_cong: thm
1.119 + val swap_prems_eq: thm
1.120 + val equal_abs_elim: cterm -> thm -> thm
1.121 val equal_abs_elim_list: cterm list -> thm -> thm
1.122 - val asm_rl : thm
1.123 - val cut_rl : thm
1.124 - val revcut_rl : thm
1.125 - val thin_rl : thm
1.126 + val asm_rl: thm
1.127 + val cut_rl: thm
1.128 + val revcut_rl: thm
1.129 + val thin_rl: thm
1.130 val triv_forall_equality: thm
1.131 - val swap_prems_rl : thm
1.132 - val equal_intr_rule : thm
1.133 - val equal_elim_rule1 : thm
1.134 - val inst : string -> string -> thm -> thm
1.135 - val instantiate' : ctyp option list -> cterm option list -> thm -> thm
1.136 - val incr_indexes : thm -> thm -> thm
1.137 - val incr_indexes_wrt : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
1.138 + val swap_prems_rl: thm
1.139 + val equal_intr_rule: thm
1.140 + val equal_elim_rule1: thm
1.141 + val inst: string -> string -> thm -> thm
1.142 + val instantiate': ctyp option list -> cterm option list -> thm -> thm
1.143 + val incr_indexes: thm -> thm -> thm
1.144 + val incr_indexes_wrt: int list -> ctyp list -> cterm list -> thm list -> thm -> thm
1.145 end;
1.146
1.147 signature DRULE =
1.148 @@ -117,18 +117,19 @@
1.149 val add_rules: thm list -> thm list -> thm list
1.150 val del_rules: thm list -> thm list -> thm list
1.151 val merge_rules: thm list * thm list -> thm list
1.152 - val imp_cong' : thm -> thm -> thm
1.153 + val imp_cong': thm -> thm -> thm
1.154 val beta_eta_conversion: cterm -> thm
1.155 val eta_long_conversion: cterm -> thm
1.156 - val goals_conv : (int -> bool) -> (cterm -> thm) -> cterm -> thm
1.157 - val forall_conv : (cterm -> thm) -> cterm -> thm
1.158 - val fconv_rule : (cterm -> thm) -> thm -> thm
1.159 + val goals_conv: (int -> bool) -> (cterm -> thm) -> cterm -> thm
1.160 + val forall_conv: (cterm -> thm) -> cterm -> thm
1.161 + val fconv_rule: (cterm -> thm) -> thm -> thm
1.162 val norm_hhf_eq: thm
1.163 val is_norm_hhf: term -> bool
1.164 val norm_hhf: theory -> term -> term
1.165 val protect: cterm -> cterm
1.166 val protectI: thm
1.167 val protectD: thm
1.168 + val protect_cong: thm
1.169 val implies_intr_protected: cterm list -> thm -> thm
1.170 val freeze_all: thm -> thm
1.171 val tvars_of_terms: term list -> (indexname * sort) list
1.172 @@ -150,6 +151,7 @@
1.173 val conj_elim_list: thm -> thm list
1.174 val conj_elim_precise: int -> thm -> thm list
1.175 val conj_intr_thm: thm
1.176 + val conj_mono_thm: thm
1.177 val abs_def: thm -> thm
1.178 val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm
1.179 val read_instantiate': (indexname * string) list -> thm -> thm
1.180 @@ -215,7 +217,7 @@
1.181 | list_comb (f, t::ts) = list_comb (Thm.capply f t, ts);
1.182
1.183 (*cterm version of strip_comb: maps f(t1,...,tn) to (f, [t1,...,tn]) *)
1.184 -fun strip_comb ct =
1.185 +fun strip_comb ct =
1.186 let
1.187 fun stripc (p as (ct, cts)) =
1.188 let val (ct1, ct2) = Thm.dest_comb ct
1.189 @@ -233,7 +235,7 @@
1.190
1.191 (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
1.192 of the meta-equality returned by the beta_conversion rule.*)
1.193 -fun beta_conv x y =
1.194 +fun beta_conv x y =
1.195 #2 (Thm.dest_comb (cprop_of (Thm.beta_conversion false (Thm.capply x y))));
1.196
1.197 fun plain_prop_of raw_thm =
1.198 @@ -300,7 +302,7 @@
1.199 fun types_sorts thm =
1.200 let val {prop, hyps, tpairs, ...} = Thm.rep_thm thm;
1.201 (* bogus term! *)
1.202 - val big = Term.list_comb
1.203 + val big = Term.list_comb
1.204 (Term.list_comb (prop, hyps), Thm.terms_of_tpairs tpairs);
1.205 val vars = map dest_Var (term_vars big);
1.206 val frees = map dest_Free (term_frees big);
1.207 @@ -406,7 +408,7 @@
1.208 fun outer_params t =
1.209 let
1.210 val vs = Term.strip_all_vars t;
1.211 - val xs = Term.variantlist (map #1 vs, []);
1.212 + val xs = Term.variantlist (map (Syntax.deskolem o #1) vs, []);
1.213 in xs ~~ map #2 vs end;
1.214
1.215 (*generalize outermost parameters*)
1.216 @@ -878,6 +880,8 @@
1.217 |> store_standard_thm_open "norm_hhf_eq"
1.218 end;
1.219
1.220 +val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);
1.221 +
1.222 fun is_norm_hhf tm =
1.223 let
1.224 fun is_norm (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false
1.225 @@ -888,7 +892,8 @@
1.226
1.227 fun norm_hhf thy t =
1.228 if is_norm_hhf t then t
1.229 - else Pattern.rewrite_term thy [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
1.230 + else Pattern.rewrite_term thy [norm_hhf_prop] [] t;
1.231 +
1.232
1.233
1.234 (*** Instantiate theorem th, reading instantiations in theory thy ****)
1.235 @@ -926,7 +931,7 @@
1.236 in
1.237 fun cterm_instantiate ctpairs0 th =
1.238 let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
1.239 - fun instT(ct,cu) =
1.240 + fun instT(ct,cu) =
1.241 let val inst = cterm_of thy o Envir.subst_TVars tye o term_of
1.242 in (inst ct, inst cu) end
1.243 fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
1.244 @@ -967,6 +972,7 @@
1.245 (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
1.246 val protectD = store_thm "protectD" (kind_rule internalK (standard
1.247 (Thm.equal_elim prop_def (Thm.assume (protect A)))));
1.248 + val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
1.249 end;
1.250
1.251 fun implies_intr_protected asms th =
1.252 @@ -1121,7 +1127,11 @@
1.253 val A = read_prop "PROP A";
1.254 val B = read_prop "PROP B";
1.255 val C = read_prop "PROP C";
1.256 + val D = read_prop "PROP D";
1.257 + val AC = read_prop "PROP A ==> PROP C";
1.258 + val BD = read_prop "PROP B ==> PROP D";
1.259 val ABC = read_prop "PROP A ==> PROP B ==> PROP C";
1.260 + val A_B = read_prop "!!X. (PROP A ==> PROP B ==> PROP X) ==> PROP X";
1.261
1.262 val proj1 =
1.263 forall_intr_list [A, B] (implies_intr_list [A, B] (Thm.assume A))
1.264 @@ -1160,6 +1170,13 @@
1.265 val conj_intr_thm = store_standard_thm_open "conjunctionI"
1.266 (implies_intr_list [A, B] (conj_intr (Thm.assume A) (Thm.assume B)));
1.267
1.268 +val conj_mono_thm = store_standard_thm_open "conjunction_mono"
1.269 + (Thm.assume A_B |> conj_elim |> (fn (a, b) =>
1.270 + conj_intr
1.271 + (Thm.implies_elim (Thm.assume AC) a)
1.272 + (Thm.implies_elim (Thm.assume BD) b))
1.273 + |> implies_intr_list [AC, BD, A_B]);
1.274 +
1.275 end;
1.276
1.277 end;