1signature ConseqConv = 2sig 3 4include Abbrev 5 6 7(* 8 trace "DEPTH_CONSEQ_CONV" can be used to get debug information 9 on DEPTH_CONSEQ_CONV and related conversions 10*) 11 12 13(* A consequence conversion is a function 14 that given a term t returns a theorem of the form 15 16 |- t' ==> t (STRENGTHEN) or 17 |- t ==> t' (WEAKEN) or 18 |- t <=> t' (EQUIVALENT) 19*) 20type conseq_conv = term -> thm; 21 22 23(* Directed consequence conversions allow specifying, whether 24 strengthening or weakening is desired. *) 25datatype CONSEQ_CONV_direction = 26 CONSEQ_CONV_STRENGTHEN_direction 27 | CONSEQ_CONV_WEAKEN_direction 28 | CONSEQ_CONV_UNKNOWN_direction; 29 30type directed_conseq_conv = CONSEQ_CONV_direction -> conseq_conv; 31 32 33(* Some basic consequence conversions. Most are trivial, 34 but useful building blocks for writing more interesting ones. *) 35val FALSE_CONSEQ_CONV : conseq_conv; 36val TRUE_CONSEQ_CONV : conseq_conv; 37val REFL_CONSEQ_CONV : conseq_conv; 38val FORALL_EQ___CONSEQ_CONV : conseq_conv; 39val EXISTS_EQ___CONSEQ_CONV : conseq_conv; 40 41val TRUE_FALSE_REFL_CONSEQ_CONV : directed_conseq_conv 42 43(* Consequence Conversions can be combined. There are similar 44 operations as for conversions. *) 45 46val CHANGED_CONSEQ_CONV : conseq_conv -> conseq_conv; 47val QCHANGED_CONSEQ_CONV : conseq_conv -> conseq_conv; 48val ORELSE_CONSEQ_CONV : conseq_conv -> conseq_conv -> conseq_conv 49val THEN_CONSEQ_CONV : conseq_conv -> conseq_conv -> conseq_conv; 50val FIRST_CONSEQ_CONV : conseq_conv list -> conseq_conv; 51val EVERY_CONSEQ_CONV : conseq_conv list -> conseq_conv; 52 53val FORALL_CONSEQ_CONV : conseq_conv -> conseq_conv; 54val EXISTS_CONSEQ_CONV : conseq_conv -> conseq_conv; 55val QUANT_CONSEQ_CONV : conseq_conv -> conseq_conv; 56 57(* Enforce a consequence conversion to operate in only one direction *) 58val STRENGTHEN_CONSEQ_CONV : conseq_conv -> directed_conseq_conv; 59val WEAKEN_CONSEQ_CONV : conseq_conv -> directed_conseq_conv; 60 61 62(* Rules *) 63val STRENGTHEN_CONSEQ_CONV_RULE : directed_conseq_conv -> thm -> thm; 64val WEAKEN_CONSEQ_CONV_RULE : directed_conseq_conv -> thm -> thm; 65 66 67(* Tactics *) 68val CONSEQ_CONV_TAC : directed_conseq_conv -> tactic; 69val ASM_CONSEQ_CONV_TAC : (thm list -> directed_conseq_conv) -> tactic 70val DISCH_ASM_CONSEQ_CONV_TAC : directed_conseq_conv -> tactic; 71 72 73 74(* DEPTH_CONSEQ_CONV 75 76 For equality, it is comparatively simple to write a conversion that 77 looks at subterms. For consequence conversion one needs to exploit 78 semantic information about boolean operations one wants operate on. 79 80 However, for the common operators 81 82 - conjunction 83 - disjunction 84 - negation 85 - implication 86 - if-then-else 87 - universal quantification 88 - existential quantification 89 90 this is provided by the ConseqConv library. This leads to easily usable 91 consequence conversions and corresponding tactics that traverse a term. 92*) 93 94val DEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv; 95val REDEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv; 96val ONCE_DEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv; 97 98val DEPTH_CONSEQ_CONV_TAC : directed_conseq_conv -> tactic; 99val REDEPTH_CONSEQ_CONV_TAC : directed_conseq_conv -> tactic; 100val ONCE_DEPTH_CONSEQ_CONV_TAC : directed_conseq_conv -> tactic; 101 102val DEPTH_STRENGTHEN_CONSEQ_CONV : conseq_conv -> conseq_conv; 103val REDEPTH_STRENGTHEN_CONSEQ_CONV : conseq_conv -> conseq_conv; 104 105 106(* A bit uncommon is a generalisation of ONCE_DEPTH_CONSEQ_CONV, which at most 107 performs 1 step. This generalisation allows specifying how many steps should 108 at most be taken. *) 109val NUM_DEPTH_CONSEQ_CONV : directed_conseq_conv -> int -> 110 directed_conseq_conv; 111val NUM_REDEPTH_CONSEQ_CONV: directed_conseq_conv -> int -> 112 directed_conseq_conv 113 114 115(* The most common application of DEPTH_CONSEQ_CONV is a tool similar to 116 REWRITE_CONV. The directed consequence conversion CONSEQ_TOP_REWRITE_CONV gets 117 a triple (both_thmL,strengthen_thmL,weaken_thmL) of theorem lists. The theorem 118 lists are preprocessed (most prominently by getting their body conjuncts, but 119 also by moving quantifiers around a bit). Moreover, equivalence theorems 120 might be split into two implications. The resulting theorems lists are used as follows: 121 122 123 strengthen_thmL: 124 These theorems are used for strengthening. This means, given a term "t0" and 125 a theorem "|- t' ==> t" in the preprocessed strengthen list. Then CONSEQ_TOP_REWRITE_CONV 126 tries to match t0 with t, which would result in a theorem "|- t0' ==> t0". 127 128 weaken_thmL: 129 These theorems are used for weakening. 130 131 both_thmL: 132 These theorems are used for both strengthening and weakening. 133 134 CONSEQ_TOP_REWRITE_CONV searches (depending on the given direction) for a theorem to 135 strengthen or weaken its input term with. The first one it finds is applied and the 136 resulting theorem returned. If none is found, UNCHANGED is raised. 137 138 CONSEQ_TOP_HO_REWRITE_CONV is similar, but uses higher order matching instead of 139 first order one. 140*) 141 142val CONSEQ_TOP_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv; 143val CONSEQ_TOP_HO_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv; 144 145 146(* Combined with various versions of DEPTH_CONSEQ_CONV, this leads to a powerful tools for 147 applying implicational theorems. *) 148 149val CONSEQ_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv; 150val CONSEQ_HO_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv; 151val ONCE_CONSEQ_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv; 152val ONCE_CONSEQ_HO_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv; 153 154val CONSEQ_REWRITE_TAC : (thm list * thm list * thm list) -> tactic; 155val CONSEQ_HO_REWRITE_TAC : (thm list * thm list * thm list) -> tactic; 156val ONCE_CONSEQ_REWRITE_TAC : (thm list * thm list * thm list) -> tactic; 157val ONCE_CONSEQ_HO_REWRITE_TAC : (thm list * thm list * thm list) -> tactic; 158 159val CONSEQ_TOP_REWRITE_TAC : (thm list * thm list * thm list) -> tactic; 160val CONSEQ_TOP_HO_REWRITE_TAC : (thm list * thm list * thm list) -> tactic; 161 162 163(* General rules and tactics. These were implemented to might be useful in general *) 164val GEN_ASSUM : term -> thm -> thm; 165val GEN_IMP : term -> thm -> thm; 166val LIST_GEN_IMP : term list -> thm -> thm; 167val GEN_EQ : term -> thm -> thm; 168val LIST_GEN_EQ : term list -> thm -> thm; 169val EXISTS_INTRO_IMP : term -> thm -> thm; 170val LIST_EXISTS_INTRO_IMP : term list -> thm -> thm; 171 172val SPEC_ALL_TAC : tactic; 173val REMOVE_TRUE_TAC : tactic; 174val DISCH_ASM_CONV_TAC : conv -> tactic; 175 176 177 178(******************************************************************) 179(******************************************************************) 180(* ADVANCED USAGE *) 181(******************************************************************) 182(******************************************************************) 183 184 185(* The functionality shown above mimics for implications some of the 186 infrastructure for equations. However, for equational reasoning the 187 simplifier is available, which allows to use context 188 information. Something like is also beneficial for reasoning with 189 implications. The implementation underlying the simple DEPTH 190 conversions above allows in it's full detail: 191 192 - using context information 193 - providing a list of congruence rules 194 - caching intermediate steps 195 - fine control over counting steps 196 - control over reiterating of already modified subterms 197*) 198 199type conseq_conv_congruence_syscall = 200 term list -> thm list -> int -> CONSEQ_CONV_direction -> term -> (int * thm option) 201 202type conseq_conv_congruence = 203 thm list -> conseq_conv_congruence_syscall -> 204 CONSEQ_CONV_direction -> term -> (int * thm) 205 206type depth_conseq_conv_cache 207 208type depth_conseq_conv_cache_opt = 209 ((unit -> depth_conseq_conv_cache) * ((term * (int * thm option)) -> bool)) option 210 211val EXT_DEPTH_NUM_CONSEQ_CONV : 212 conseq_conv_congruence list -> (*congruence_list*) 213 depth_conseq_conv_cache_opt -> (*use cache*) 214 int option -> (*max no of steps, NONE for unbounded *) 215 bool -> (*redepth ?*) 216 (bool * int option * (thm list -> directed_conseq_conv)) list -> 217 (*conversion list: 218 (1: true : apply before descending into subterms 219 false : apply after returning from descend 220 2: weight, how many steps are counted, 0 means that it does 221 not count 222 3: context -> conversion 223 *) 224 thm list -> (*context that might be used*) 225 CONSEQ_CONV_direction -> term -> 226 (int * thm option) 227 (* number of steps taken + theorem option. NONE might be returned if nothing changed. *) 228 229 230(***************) 231(* Congruences *) 232(***************) 233 234(* conseq_conv_congruences are used for moving consequence conversions 235 through boolean terms. 236 237 A congruence gets 4 arguments 238 239 context : thm list 240 A list of theorems from the context it may use. 241 242 sys : conseq_conv_congruence_syscall 243 A callback for actually trying to work on subterms (see below) 244 245 dir : CONSEQ_CONV_direction 246 The direction it should work in. 247 248 t : term 249 The term to work on 250 251 It results in the number of steps performed and a resulting theorem. 252 If the congruence fails, it raises an exception. 253 254 The job of a congruence is to call the system callback sys on suitable 255 subterms and recombine the results. 256 257 The system callback gets the following arguments 258 259 new_context : term list 260 new context information that may be assumed theorems are build 261 via ASSUME from these terms, it's the job of the congruence to 262 remove the resulting assumptions 263 264 old_context : thm list 265 the old context theorems that can be used 266 267 m : int 268 number of steps already taken so far 269 270 dir : CONSEQ_CONV_direction 271 the direction 272 273 t : term 274 term to work on 275 276 The syscall returns the number of steps performed as well a 277 potential resulting theorem. 278*) 279 280 281 282(* For the common operations, i.e. for 283 284 - conjunction 285 - disjunction 286 - negation 287 - implication 288 - if-then-else 289 - universal quantification 290 - existential quantification 291 292 there are already defined congruences. These come with 293 different levels of using context information. If more 294 context is used, potentially more can be done. However, 295 there is a speed penalty. CONSEQ_CONV_get_context_congruences 296 returns lists of congruences for these operations for 297 different levels of using context information. 298*) 299 300 301datatype CONSEQ_CONV_context = 302 (* do not use context at all *) 303 CONSEQ_CONV_NO_CONTEXT 304 305 (* use just the antecedents of implications *) 306| CONSEQ_CONV_IMP_CONTEXT 307 308 (* use all available context (from and, or, ...) *) 309| CONSEQ_CONV_FULL_CONTEXT; 310 311 312val CONSEQ_CONV_get_context_congruences : 313 CONSEQ_CONV_context -> conseq_conv_congruence list; 314 315 316 317(***************) 318(* Cashing *) 319(***************) 320 321(* There is support for caching results. A depth_conseq_conv_cache 322 is a reference a dictionary for looking up previously recorded results. *) 323 324(* make a new, empty cache *) 325val mk_DEPTH_CONSEQ_CONV_CACHE : unit -> depth_conseq_conv_cache; 326 327(* clear an existing cache, i.e. remove all entries *) 328val clear_CONSEQ_CONV_CACHE : depth_conseq_conv_cache -> unit 329 330 331(* However, at top-level, no cache, but a depth_conseq_conv_cache_opt is 332 passed around. If such an option is NONE, no caching is used. 333 Otherwise, it consists of a function for getting a cache and a 334 predicate that determines which new results are added to the cache. 335 336 The result for getting the cache is called once before traversing 337 the term begins. It can create a fresh cache or return a previously 338 used cache containing already useful results. If a result is not 339 found in the cache and newly computed, the predicate passed 340 determines, whether it is added to the cache. *) 341 342 343(* The default cache-option. It always creates a fresh cache and 344 stores all results in this cache. *) 345val CONSEQ_CONV_default_cache_opt : depth_conseq_conv_cache_opt 346 347(* Always create a fresh cache and use given predicate. *) 348val mk_DEPTH_CONSEQ_CONV_CACHE_OPT : ((term * (int * thm option)) -> bool) -> depth_conseq_conv_cache_opt; 349 350(* Create a cache just once and keep it for multiple calls. 351 Use the given predicate. *) 352val mk_PERSISTENT_DEPTH_CONSEQ_CONV_CACHE_OPT : ((term * (int * thm option)) -> bool) -> depth_conseq_conv_cache_opt; 353 354(* A function to clear the cache of a persistent cache-option. *) 355val clear_CONSEQ_CONV_CACHE_OPT : depth_conseq_conv_cache_opt -> unit 356 357 358 359(********************) 360(* Derived DEPTH *) 361(* consequence *) 362(* conversions *) 363(********************) 364 365(* ignore the number of steps result and raise UNCHANGED, if no thm is returned *) 366val EXT_DEPTH_CONSEQ_CONV : 367 conseq_conv_congruence list -> (*congruence_list*) 368 depth_conseq_conv_cache_opt -> (*use cache*) 369 int option -> (*no of steps, NONE for unbounded *) 370 bool -> (*redepth ?*) 371 (bool * int option * (thm list -> directed_conseq_conv)) list -> 372 (*conversion list: 373 (1: apply before or after descending in subterms 374 2: weight, how many steps are counted, 0 means that it does 375 not count 376 3: context -> conversion 377 *) 378 thm list -> (*context that might be used*) 379 directed_conseq_conv 380 381(* Use congruences for given context level and argument consequence consequence conv 382 might use context. *) 383val CONTEXT_DEPTH_CONSEQ_CONV : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> directed_conseq_conv; 384val CONTEXT_REDEPTH_CONSEQ_CONV : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> directed_conseq_conv; 385val CONTEXT_ONCE_DEPTH_CONSEQ_CONV : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> directed_conseq_conv; 386val CONTEXT_NUM_DEPTH_CONSEQ_CONV : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> int -> 387 directed_conseq_conv; 388val CONTEXT_NUM_REDEPTH_CONSEQ_CONV: (thm list -> directed_conseq_conv) -> int -> 389 directed_conseq_conv 390 391 392 393 394(**********************) 395(* Fancy REWRITE *) 396(**********************) 397 398(* Allowing full access to all parameters leads for 399 CONSEQ_REWRITE_CONV to the following function. 400 401 Most arguments are known from EXT_DEPTH_NUM_CONSEQ_CONV or 402 CONSEQ_REWRITE_CONV. the list of conversions corresponds to the 403 list of directed_conseq_conv for EXT_DEPTH_NUM_CONSEQ_CONV. 404 However, here really conversions, not consequence conversions are 405 required. *) 406 407val FULL_EXT_CONSEQ_REWRITE_CONV : 408 conseq_conv_congruence list -> (* congruences *) 409 depth_conseq_conv_cache_opt -> (* cache *) 410 int option -> (* steps *) 411 bool -> (* redepth *) 412 bool -> (* higher order rewriting ? *) 413 thm list -> (* context *) 414 (bool * int option * (thm list -> conv)) list -> (* conversions *) 415 (thm list * thm list * thm list) -> (*consequence rewrites *) 416 directed_conseq_conv 417 418 419(* Derived functions *) 420val EXT_CONSEQ_REWRITE_CONV : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv; 421val EXT_CONSEQ_HO_REWRITE_CONV : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv; 422val EXT_CONTEXT_CONSEQ_REWRITE_CONV : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv; 423val EXT_CONTEXT_CONSEQ_HO_REWRITE_CONV : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv; 424 425val EXT_CONSEQ_REWRITE_TAC : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic; 426val EXT_CONTEXT_CONSEQ_REWRITE_TAC : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic; 427val EXT_CONSEQ_HO_REWRITE_TAC : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic; 428val EXT_CONTEXT_CONSEQ_HO_REWRITE_TAC : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic; 429 430 431 432 433(*************************************************************************) 434(* Technical Stuff for writing own, low level consequence conversion *) 435(*************************************************************************) 436 437val asm_marker_tm : term 438val dest_asm_marker : term -> term * term 439val is_asm_marker : term -> bool 440val mk_asm_marker : term -> term -> term 441val mk_asm_marker_random : term -> term 442val dest_neg_asm_marker : term -> term * term 443val is_neg_asm_marker : term -> bool 444val asm_marker_ELIM_CONV : conv 445val asm_marker_INTRO_CONV : term -> conv 446 447 448val CONSEQ_CONV_DIRECTION_NEGATE : CONSEQ_CONV_direction -> CONSEQ_CONV_direction; 449val CONSEQ_CONV___GET_SIMPLIFIED_TERM : thm -> term -> term; 450val CONSEQ_CONV___GET_DIRECTION : thm -> term -> CONSEQ_CONV_direction; 451val THEN_CONSEQ_CONV___combine : thm -> thm -> term -> thm; 452val CONSEQ_CONV___APPLY_CONV_RULE : thm -> term -> (term -> thm) -> thm; 453 454 455val step_opt_sub : int option -> int -> int option 456val step_opt_allows_steps : int option -> int -> int option -> bool 457 458 459end 460