1(* Title: Provers/classical.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 4Theorem prover for classical reasoning, including predicate calculus, set 5theory, etc. 6 7Rules must be classified as intro, elim, safe, unsafe. 8 9A rule is unsafe unless it can be applied blindly without harmful results. 10For a rule to be safe, its premises and conclusion should be logically 11equivalent. There should be no variables in the premises that are not in 12the conclusion. 13*) 14 15(*higher precedence than := facilitates use of references*) 16infix 4 addSIs addSEs addSDs addIs addEs addDs delrules 17 addSWrapper delSWrapper addWrapper delWrapper 18 addSbefore addSafter addbefore addafter 19 addD2 addE2 addSD2 addSE2; 20 21signature CLASSICAL_DATA = 22sig 23 val imp_elim: thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) 24 val not_elim: thm (* ~P ==> P ==> R *) 25 val swap: thm (* ~ P ==> (~ R ==> P) ==> R *) 26 val classical: thm (* (~ P ==> P) ==> P *) 27 val sizef: thm -> int (* size function for BEST_FIRST, typically size_of_thm *) 28 val hyp_subst_tacs: (Proof.context -> int -> tactic) list (* optional tactics for 29 substitution in the hypotheses; assumed to be safe! *) 30end; 31 32signature BASIC_CLASSICAL = 33sig 34 type wrapper = (int -> tactic) -> int -> tactic 35 type claset 36 val print_claset: Proof.context -> unit 37 val addDs: Proof.context * thm list -> Proof.context 38 val addEs: Proof.context * thm list -> Proof.context 39 val addIs: Proof.context * thm list -> Proof.context 40 val addSDs: Proof.context * thm list -> Proof.context 41 val addSEs: Proof.context * thm list -> Proof.context 42 val addSIs: Proof.context * thm list -> Proof.context 43 val delrules: Proof.context * thm list -> Proof.context 44 val addSWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context 45 val delSWrapper: Proof.context * string -> Proof.context 46 val addWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context 47 val delWrapper: Proof.context * string -> Proof.context 48 val addSbefore: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context 49 val addSafter: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context 50 val addbefore: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context 51 val addafter: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context 52 val addD2: Proof.context * (string * thm) -> Proof.context 53 val addE2: Proof.context * (string * thm) -> Proof.context 54 val addSD2: Proof.context * (string * thm) -> Proof.context 55 val addSE2: Proof.context * (string * thm) -> Proof.context 56 val appSWrappers: Proof.context -> wrapper 57 val appWrappers: Proof.context -> wrapper 58 59 val claset_of: Proof.context -> claset 60 val put_claset: claset -> Proof.context -> Proof.context 61 62 val map_theory_claset: (Proof.context -> Proof.context) -> theory -> theory 63 64 val fast_tac: Proof.context -> int -> tactic 65 val slow_tac: Proof.context -> int -> tactic 66 val astar_tac: Proof.context -> int -> tactic 67 val slow_astar_tac: Proof.context -> int -> tactic 68 val best_tac: Proof.context -> int -> tactic 69 val first_best_tac: Proof.context -> int -> tactic 70 val slow_best_tac: Proof.context -> int -> tactic 71 val depth_tac: Proof.context -> int -> int -> tactic 72 val deepen_tac: Proof.context -> int -> int -> tactic 73 74 val contr_tac: Proof.context -> int -> tactic 75 val dup_elim: Proof.context -> thm -> thm 76 val dup_intr: thm -> thm 77 val dup_step_tac: Proof.context -> int -> tactic 78 val eq_mp_tac: Proof.context -> int -> tactic 79 val unsafe_step_tac: Proof.context -> int -> tactic 80 val mp_tac: Proof.context -> int -> tactic 81 val safe_tac: Proof.context -> tactic 82 val safe_steps_tac: Proof.context -> int -> tactic 83 val safe_step_tac: Proof.context -> int -> tactic 84 val clarify_tac: Proof.context -> int -> tactic 85 val clarify_step_tac: Proof.context -> int -> tactic 86 val step_tac: Proof.context -> int -> tactic 87 val slow_step_tac: Proof.context -> int -> tactic 88 val swapify: thm list -> thm list 89 val swap_res_tac: Proof.context -> thm list -> int -> tactic 90 val inst_step_tac: Proof.context -> int -> tactic 91 val inst0_step_tac: Proof.context -> int -> tactic 92 val instp_step_tac: Proof.context -> int -> tactic 93end; 94 95signature CLASSICAL = 96sig 97 include BASIC_CLASSICAL 98 val classical_rule: Proof.context -> thm -> thm 99 type rule = thm * (thm * thm list) * (thm * thm list) 100 type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net 101 val rep_cs: claset -> 102 {safeIs: rule Item_Net.T, 103 safeEs: rule Item_Net.T, 104 unsafeIs: rule Item_Net.T, 105 unsafeEs: rule Item_Net.T, 106 swrappers: (string * (Proof.context -> wrapper)) list, 107 uwrappers: (string * (Proof.context -> wrapper)) list, 108 safe0_netpair: netpair, 109 safep_netpair: netpair, 110 unsafe_netpair: netpair, 111 dup_netpair: netpair, 112 extra_netpair: Context_Rules.netpair} 113 val get_cs: Context.generic -> claset 114 val map_cs: (claset -> claset) -> Context.generic -> Context.generic 115 val safe_dest: int option -> attribute 116 val safe_elim: int option -> attribute 117 val safe_intro: int option -> attribute 118 val unsafe_dest: int option -> attribute 119 val unsafe_elim: int option -> attribute 120 val unsafe_intro: int option -> attribute 121 val rule_del: attribute 122 val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic 123 val standard_tac: Proof.context -> thm list -> tactic 124 val cla_modifiers: Method.modifier parser list 125 val cla_method: 126 (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser 127 val cla_method': 128 (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser 129end; 130 131 132functor Classical(Data: CLASSICAL_DATA): CLASSICAL = 133struct 134 135(** classical elimination rules **) 136 137(* 138Classical reasoning requires stronger elimination rules. For 139instance, make_elim of Pure transforms the HOL rule injD into 140 141 [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W 142 143Such rules can cause fast_tac to fail and blast_tac to report "PROOF 144FAILED"; classical_rule will strengthen this to 145 146 [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W 147*) 148 149fun classical_rule ctxt rule = 150 if is_some (Object_Logic.elim_concl ctxt rule) then 151 let 152 val thy = Proof_Context.theory_of ctxt; 153 val rule' = rule RS Data.classical; 154 val concl' = Thm.concl_of rule'; 155 fun redundant_hyp goal = 156 concl' aconv Logic.strip_assums_concl goal orelse 157 (case Logic.strip_assums_hyp goal of 158 hyp :: hyps => exists (fn t => t aconv hyp) hyps 159 | _ => false); 160 val rule'' = 161 rule' |> ALLGOALS (SUBGOAL (fn (goal, i) => 162 if i = 1 orelse redundant_hyp goal 163 then eresolve_tac ctxt [thin_rl] i 164 else all_tac)) 165 |> Seq.hd 166 |> Drule.zero_var_indexes; 167 in if Thm.equiv_thm thy (rule, rule'') then rule else rule'' end 168 else rule; 169 170(*flatten nested meta connectives in prems*) 171fun flat_rule ctxt = 172 Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)); 173 174 175(*** Useful tactics for classical reasoning ***) 176 177(*Prove goal that assumes both P and ~P. 178 No backtracking if it finds an equal assumption. Perhaps should call 179 ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) 180fun contr_tac ctxt = 181 eresolve_tac ctxt [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac ctxt); 182 183(*Finds P-->Q and P in the assumptions, replaces implication by Q. 184 Could do the same thing for P<->Q and P... *) 185fun mp_tac ctxt i = 186 eresolve_tac ctxt [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i; 187 188(*Like mp_tac but instantiates no variables*) 189fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i; 190 191(*Creates rules to eliminate ~A, from rules to introduce A*) 192fun swapify intrs = intrs RLN (2, [Data.swap]); 193val swapped = Thm.rule_attribute [] (fn _ => fn th => th RSN (2, Data.swap)); 194 195(*Uses introduction rules in the normal way, or on negated assumptions, 196 trying rules in order. *) 197fun swap_res_tac ctxt rls = 198 let 199 val transfer = Thm.transfer' ctxt; 200 fun addrl rl brls = (false, transfer rl) :: (true, transfer rl RSN (2, Data.swap)) :: brls; 201 in 202 assume_tac ctxt ORELSE' 203 contr_tac ctxt ORELSE' 204 biresolve_tac ctxt (fold_rev addrl rls []) 205 end; 206 207(*Duplication of unsafe rules, for complete provers*) 208fun dup_intr th = zero_var_indexes (th RS Data.classical); 209 210fun dup_elim ctxt th = 211 let val rl = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd; 212 in rule_by_tactic ctxt (TRYALL (eresolve_tac ctxt [revcut_rl])) rl end; 213 214 215(**** Classical rule sets ****) 216 217type rule = thm * (thm * thm list) * (thm * thm list); 218 (*external form, internal form (possibly swapped), dup form (possibly swapped)*) 219 220type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; 221type wrapper = (int -> tactic) -> int -> tactic; 222 223datatype claset = 224 CS of 225 {safeIs: rule Item_Net.T, (*safe introduction rules*) 226 safeEs: rule Item_Net.T, (*safe elimination rules*) 227 unsafeIs: rule Item_Net.T, (*unsafe introduction rules*) 228 unsafeEs: rule Item_Net.T, (*unsafe elimination rules*) 229 swrappers: (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*) 230 uwrappers: (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*) 231 safe0_netpair: netpair, (*nets for trivial cases*) 232 safep_netpair: netpair, (*nets for >0 subgoals*) 233 unsafe_netpair: netpair, (*nets for unsafe rules*) 234 dup_netpair: netpair, (*nets for duplication*) 235 extra_netpair: Context_Rules.netpair}; (*nets for extra rules*) 236 237val empty_rules: rule Item_Net.T = 238 Item_Net.init (Thm.eq_thm_prop o apply2 #1) (single o Thm.full_prop_of o #1); 239 240val empty_netpair = (Net.empty, Net.empty); 241 242val empty_cs = 243 CS 244 {safeIs = empty_rules, 245 safeEs = empty_rules, 246 unsafeIs = empty_rules, 247 unsafeEs = empty_rules, 248 swrappers = [], 249 uwrappers = [], 250 safe0_netpair = empty_netpair, 251 safep_netpair = empty_netpair, 252 unsafe_netpair = empty_netpair, 253 dup_netpair = empty_netpair, 254 extra_netpair = empty_netpair}; 255 256fun rep_cs (CS args) = args; 257 258 259(*** Adding (un)safe introduction or elimination rules. 260 261 In case of overlap, new rules are tried BEFORE old ones!! 262***) 263 264fun joinrules (intrs, elims) = map (pair true) elims @ map (pair false) intrs; 265 266(*Priority: prefer rules with fewest subgoals, 267 then rules added most recently (preferring the head of the list).*) 268fun tag_brls k [] = [] 269 | tag_brls k (brl::brls) = 270 (1000000*subgoals_of_brl brl + k, brl) :: 271 tag_brls (k+1) brls; 272 273fun tag_brls' _ _ [] = [] 274 | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls; 275 276fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls; 277 278(*Insert into netpair that already has nI intr rules and nE elim rules. 279 Count the intr rules double (to account for swapify). Negate to give the 280 new insertions the lowest priority.*) 281fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; 282fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules; 283 284fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 285fun delete x = delete_tagged_list (joinrules x); 286 287fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); 288 289fun make_elim ctxt th = 290 if has_fewer_prems 1 th then bad_thm ctxt "Ill-formed destruction rule" th 291 else Tactic.make_elim th; 292 293fun warn_thm ctxt msg th = 294 if Context_Position.is_really_visible ctxt 295 then warning (msg ^ Thm.string_of_thm ctxt th) else (); 296 297fun warn_rules ctxt msg rules (r: rule) = 298 Item_Net.member rules r andalso (warn_thm ctxt msg (#1 r); true); 299 300fun warn_claset ctxt r (CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = 301 warn_rules ctxt "Rule already declared as safe introduction (intro!)\n" safeIs r orelse 302 warn_rules ctxt "Rule already declared as safe elimination (elim!)\n" safeEs r orelse 303 warn_rules ctxt "Rule already declared as introduction (intro)\n" unsafeIs r orelse 304 warn_rules ctxt "Rule already declared as elimination (elim)\n" unsafeEs r; 305 306 307(*** add rules ***) 308 309fun add_safe_intro w r 310 (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 311 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 312 if Item_Net.member safeIs r then cs 313 else 314 let 315 val (th, rl, _) = r; 316 val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 317 List.partition (Thm.no_prems o fst) [rl]; 318 val nI = Item_Net.length safeIs + 1; 319 val nE = Item_Net.length safeEs; 320 in 321 CS 322 {safeIs = Item_Net.update r safeIs, 323 safe0_netpair = insert (nI, nE) (map fst safe0_rls, maps snd safe0_rls) safe0_netpair, 324 safep_netpair = insert (nI, nE) (map fst safep_rls, maps snd safep_rls) safep_netpair, 325 safeEs = safeEs, 326 unsafeIs = unsafeIs, 327 unsafeEs = unsafeEs, 328 swrappers = swrappers, 329 uwrappers = uwrappers, 330 unsafe_netpair = unsafe_netpair, 331 dup_netpair = dup_netpair, 332 extra_netpair = insert' (the_default 0 w) (nI, nE) ([th], []) extra_netpair} 333 end; 334 335fun add_safe_elim w r 336 (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 337 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 338 if Item_Net.member safeEs r then cs 339 else 340 let 341 val (th, rl, _) = r; 342 val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 343 List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl]; 344 val nI = Item_Net.length safeIs; 345 val nE = Item_Net.length safeEs + 1; 346 in 347 CS 348 {safeEs = Item_Net.update r safeEs, 349 safe0_netpair = insert (nI, nE) ([], map fst safe0_rls) safe0_netpair, 350 safep_netpair = insert (nI, nE) ([], map fst safep_rls) safep_netpair, 351 safeIs = safeIs, 352 unsafeIs = unsafeIs, 353 unsafeEs = unsafeEs, 354 swrappers = swrappers, 355 uwrappers = uwrappers, 356 unsafe_netpair = unsafe_netpair, 357 dup_netpair = dup_netpair, 358 extra_netpair = insert' (the_default 0 w) (nI, nE) ([], [th]) extra_netpair} 359 end; 360 361fun add_unsafe_intro w r 362 (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 363 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 364 if Item_Net.member unsafeIs r then cs 365 else 366 let 367 val (th, rl, dup_rl) = r; 368 val nI = Item_Net.length unsafeIs + 1; 369 val nE = Item_Net.length unsafeEs; 370 in 371 CS 372 {unsafeIs = Item_Net.update r unsafeIs, 373 unsafe_netpair = insert (nI, nE) ([fst rl], snd rl) unsafe_netpair, 374 dup_netpair = insert (nI, nE) ([fst dup_rl], snd dup_rl) dup_netpair, 375 safeIs = safeIs, 376 safeEs = safeEs, 377 unsafeEs = unsafeEs, 378 swrappers = swrappers, 379 uwrappers = uwrappers, 380 safe0_netpair = safe0_netpair, 381 safep_netpair = safep_netpair, 382 extra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) extra_netpair} 383 end; 384 385fun add_unsafe_elim w r 386 (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 387 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 388 if Item_Net.member unsafeEs r then cs 389 else 390 let 391 val (th, rl, dup_rl) = r; 392 val nI = Item_Net.length unsafeIs; 393 val nE = Item_Net.length unsafeEs + 1; 394 in 395 CS 396 {unsafeEs = Item_Net.update r unsafeEs, 397 unsafe_netpair = insert (nI, nE) ([], [fst rl]) unsafe_netpair, 398 dup_netpair = insert (nI, nE) ([], [fst dup_rl]) dup_netpair, 399 safeIs = safeIs, 400 safeEs = safeEs, 401 unsafeIs = unsafeIs, 402 swrappers = swrappers, 403 uwrappers = uwrappers, 404 safe0_netpair = safe0_netpair, 405 safep_netpair = safep_netpair, 406 extra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) extra_netpair} 407 end; 408 409fun trim_context (th, (th1, ths1), (th2, ths2)) = 410 (Thm.trim_context th, 411 (Thm.trim_context th1, map Thm.trim_context ths1), 412 (Thm.trim_context th2, map Thm.trim_context ths2)); 413 414fun addSI w ctxt th (cs as CS {safeIs, ...}) = 415 let 416 val th' = flat_rule ctxt th; 417 val rl = (th', swapify [th']); 418 val r = trim_context (th, rl, rl); 419 val _ = 420 warn_rules ctxt "Ignoring duplicate safe introduction (intro!)\n" safeIs r orelse 421 warn_claset ctxt r cs; 422 in add_safe_intro w r cs end; 423 424fun addSE w ctxt th (cs as CS {safeEs, ...}) = 425 let 426 val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th; 427 val th' = classical_rule ctxt (flat_rule ctxt th); 428 val rl = (th', []); 429 val r = trim_context (th, rl, rl); 430 val _ = 431 warn_rules ctxt "Ignoring duplicate safe elimination (elim!)\n" safeEs r orelse 432 warn_claset ctxt r cs; 433 in add_safe_elim w r cs end; 434 435fun addSD w ctxt th = addSE w ctxt (make_elim ctxt th); 436 437fun addI w ctxt th (cs as CS {unsafeIs, ...}) = 438 let 439 val th' = flat_rule ctxt th; 440 val dup_th' = dup_intr th' handle THM _ => bad_thm ctxt "Ill-formed introduction rule" th; 441 val r = trim_context (th, (th', swapify [th']), (dup_th', swapify [dup_th'])); 442 val _ = 443 warn_rules ctxt "Ignoring duplicate introduction (intro)\n" unsafeIs r orelse 444 warn_claset ctxt r cs; 445 in add_unsafe_intro w r cs end; 446 447fun addE w ctxt th (cs as CS {unsafeEs, ...}) = 448 let 449 val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th; 450 val th' = classical_rule ctxt (flat_rule ctxt th); 451 val dup_th' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Ill-formed elimination rule" th; 452 val r = trim_context (th, (th', []), (dup_th', [])); 453 val _ = 454 warn_rules ctxt "Ignoring duplicate elimination (elim)\n" unsafeEs r orelse 455 warn_claset ctxt r cs; 456 in add_unsafe_elim w r cs end; 457 458fun addD w ctxt th = addE w ctxt (make_elim ctxt th); 459 460 461(*** delete rules ***) 462 463local 464 465fun del_safe_intro (r: rule) 466 (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 467 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 468 let 469 val (th, rl, _) = r; 470 val (safe0_rls, safep_rls) = List.partition (Thm.no_prems o fst) [rl]; 471 in 472 CS 473 {safe0_netpair = delete (map fst safe0_rls, maps snd safe0_rls) safe0_netpair, 474 safep_netpair = delete (map fst safep_rls, maps snd safep_rls) safep_netpair, 475 safeIs = Item_Net.remove r safeIs, 476 safeEs = safeEs, 477 unsafeIs = unsafeIs, 478 unsafeEs = unsafeEs, 479 swrappers = swrappers, 480 uwrappers = uwrappers, 481 unsafe_netpair = unsafe_netpair, 482 dup_netpair = dup_netpair, 483 extra_netpair = delete ([th], []) extra_netpair} 484 end; 485 486fun del_safe_elim (r: rule) 487 (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 488 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 489 let 490 val (th, rl, _) = r; 491 val (safe0_rls, safep_rls) = List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl]; 492 in 493 CS 494 {safe0_netpair = delete ([], map fst safe0_rls) safe0_netpair, 495 safep_netpair = delete ([], map fst safep_rls) safep_netpair, 496 safeIs = safeIs, 497 safeEs = Item_Net.remove r safeEs, 498 unsafeIs = unsafeIs, 499 unsafeEs = unsafeEs, 500 swrappers = swrappers, 501 uwrappers = uwrappers, 502 unsafe_netpair = unsafe_netpair, 503 dup_netpair = dup_netpair, 504 extra_netpair = delete ([], [th]) extra_netpair} 505 end; 506 507fun del_unsafe_intro (r as (th, (th', swapped_th'), (dup_th', swapped_dup_th'))) 508 (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 509 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 510 CS 511 {unsafe_netpair = delete ([th'], swapped_th') unsafe_netpair, 512 dup_netpair = delete ([dup_th'], swapped_dup_th') dup_netpair, 513 safeIs = safeIs, 514 safeEs = safeEs, 515 unsafeIs = Item_Net.remove r unsafeIs, 516 unsafeEs = unsafeEs, 517 swrappers = swrappers, 518 uwrappers = uwrappers, 519 safe0_netpair = safe0_netpair, 520 safep_netpair = safep_netpair, 521 extra_netpair = delete ([th], []) extra_netpair}; 522 523fun del_unsafe_elim (r as (th, (th', _), (dup_th', _))) 524 (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 525 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 526 CS 527 {unsafe_netpair = delete ([], [th']) unsafe_netpair, 528 dup_netpair = delete ([], [dup_th']) dup_netpair, 529 safeIs = safeIs, 530 safeEs = safeEs, 531 unsafeIs = unsafeIs, 532 unsafeEs = Item_Net.remove r unsafeEs, 533 swrappers = swrappers, 534 uwrappers = uwrappers, 535 safe0_netpair = safe0_netpair, 536 safep_netpair = safep_netpair, 537 extra_netpair = delete ([], [th]) extra_netpair}; 538 539fun del f rules th cs = 540 fold f (Item_Net.lookup rules (th, (th, []), (th, []))) cs; 541 542in 543 544fun delrule ctxt th (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = 545 let 546 val th' = Tactic.make_elim th; 547 val r = (th, (th, []), (th, [])); 548 val r' = (th', (th', []), (th', [])); 549 in 550 if Item_Net.member safeIs r orelse Item_Net.member safeEs r orelse 551 Item_Net.member unsafeIs r orelse Item_Net.member unsafeEs r orelse 552 Item_Net.member safeEs r' orelse Item_Net.member unsafeEs r' 553 then 554 cs 555 |> del del_safe_intro safeIs th 556 |> del del_safe_elim safeEs th 557 |> del del_safe_elim safeEs th' 558 |> del del_unsafe_intro unsafeIs th 559 |> del del_unsafe_elim unsafeEs th 560 |> del del_unsafe_elim unsafeEs th' 561 else (warn_thm ctxt "Undeclared classical rule\n" th; cs) 562 end; 563 564end; 565 566 567 568(** claset data **) 569 570(* wrappers *) 571 572fun map_swrappers f 573 (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 574 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 575 CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, 576 swrappers = f swrappers, uwrappers = uwrappers, 577 safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 578 unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; 579 580fun map_uwrappers f 581 (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 582 safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 583 CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, 584 swrappers = swrappers, uwrappers = f uwrappers, 585 safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 586 unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; 587 588 589(* merge_cs *) 590 591(*Merge works by adding all new rules of the 2nd claset into the 1st claset, 592 in order to preserve priorities reliably.*) 593 594fun merge_thms add thms1 thms2 = 595 fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2); 596 597fun merge_cs (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}, 598 cs' as CS {safeIs = safeIs2, safeEs = safeEs2, unsafeIs = unsafeIs2, unsafeEs = unsafeEs2, 599 swrappers, uwrappers, ...}) = 600 if pointer_eq (cs, cs') then cs 601 else 602 cs 603 |> merge_thms (add_safe_intro NONE) safeIs safeIs2 604 |> merge_thms (add_safe_elim NONE) safeEs safeEs2 605 |> merge_thms (add_unsafe_intro NONE) unsafeIs unsafeIs2 606 |> merge_thms (add_unsafe_elim NONE) unsafeEs unsafeEs2 607 |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) 608 |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)); 609 610 611(* data *) 612 613structure Claset = Generic_Data 614( 615 type T = claset; 616 val empty = empty_cs; 617 val extend = I; 618 val merge = merge_cs; 619); 620 621val claset_of = Claset.get o Context.Proof; 622val rep_claset_of = rep_cs o claset_of; 623 624val get_cs = Claset.get; 625val map_cs = Claset.map; 626 627fun map_theory_claset f thy = 628 let 629 val ctxt' = f (Proof_Context.init_global thy); 630 val thy' = Proof_Context.theory_of ctxt'; 631 in Context.theory_map (Claset.map (K (claset_of ctxt'))) thy' end; 632 633fun map_claset f = Context.proof_map (map_cs f); 634fun put_claset cs = map_claset (K cs); 635 636fun print_claset ctxt = 637 let 638 val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; 639 val pretty_thms = map (Thm.pretty_thm_item ctxt o #1) o Item_Net.content; 640 in 641 [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), 642 Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs), 643 Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), 644 Pretty.big_list "elimination rules (elim):" (pretty_thms unsafeEs), 645 Pretty.strs ("safe wrappers:" :: map #1 swrappers), 646 Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] 647 |> Pretty.writeln_chunks 648 end; 649 650 651(* old-style declarations *) 652 653fun decl f (ctxt, ths) = map_claset (fold_rev (f ctxt) ths) ctxt; 654 655val op addSIs = decl (addSI NONE); 656val op addSEs = decl (addSE NONE); 657val op addSDs = decl (addSD NONE); 658val op addIs = decl (addI NONE); 659val op addEs = decl (addE NONE); 660val op addDs = decl (addD NONE); 661val op delrules = decl delrule; 662 663 664 665(*** Modifying the wrapper tacticals ***) 666 667fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt)); 668fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt)); 669 670fun update_warn msg (p as (key : string, _)) xs = 671 (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs); 672 673fun delete_warn msg (key : string) xs = 674 if AList.defined (op =) xs key then AList.delete (op =) key xs 675 else (warning msg; xs); 676 677(*Add/replace a safe wrapper*) 678fun ctxt addSWrapper new_swrapper = ctxt |> map_claset 679 (map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper)); 680 681(*Add/replace an unsafe wrapper*) 682fun ctxt addWrapper new_uwrapper = ctxt |> map_claset 683 (map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper)); 684 685(*Remove a safe wrapper*) 686fun ctxt delSWrapper name = ctxt |> map_claset 687 (map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name)); 688 689(*Remove an unsafe wrapper*) 690fun ctxt delWrapper name = ctxt |> map_claset 691 (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name)); 692 693(* compose a safe tactic alternatively before/after safe_step_tac *) 694fun ctxt addSbefore (name, tac1) = 695 ctxt addSWrapper (name, fn ctxt => fn tac2 => tac1 ctxt ORELSE' tac2); 696fun ctxt addSafter (name, tac2) = 697 ctxt addSWrapper (name, fn ctxt => fn tac1 => tac1 ORELSE' tac2 ctxt); 698 699(*compose a tactic alternatively before/after the step tactic *) 700fun ctxt addbefore (name, tac1) = 701 ctxt addWrapper (name, fn ctxt => fn tac2 => tac1 ctxt APPEND' tac2); 702fun ctxt addafter (name, tac2) = 703 ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt); 704 705fun ctxt addD2 (name, thm) = 706 ctxt addafter (name, fn ctxt' => dresolve_tac ctxt' [thm] THEN' assume_tac ctxt'); 707fun ctxt addE2 (name, thm) = 708 ctxt addafter (name, fn ctxt' => eresolve_tac ctxt' [thm] THEN' assume_tac ctxt'); 709fun ctxt addSD2 (name, thm) = 710 ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac); 711fun ctxt addSE2 (name, thm) = 712 ctxt addSafter (name, fn ctxt' => ematch_tac ctxt' [thm] THEN' eq_assume_tac); 713 714 715 716(**** Simple tactics for theorem proving ****) 717 718(*Attack subgoals using safe inferences -- matching, not resolution*) 719fun safe_step_tac ctxt = 720 let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in 721 appSWrappers ctxt 722 (FIRST' 723 [eq_assume_tac, 724 eq_mp_tac ctxt, 725 bimatch_from_nets_tac ctxt safe0_netpair, 726 FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), 727 bimatch_from_nets_tac ctxt safep_netpair]) 728 end; 729 730(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*) 731fun safe_steps_tac ctxt = 732 REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i)); 733 734(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) 735fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt)); 736 737 738(*** Clarify_tac: do safe steps without causing branching ***) 739 740fun nsubgoalsP n (k, brl) = (subgoals_of_brl brl = n); 741 742(*version of bimatch_from_nets_tac that only applies rules that 743 create precisely n subgoals.*) 744fun n_bimatch_from_nets_tac ctxt n = 745 biresolution_from_nets_tac ctxt (order_list o filter (nsubgoalsP n)) true; 746 747fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i; 748fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt; 749 750(*Two-way branching is allowed only if one of the branches immediately closes*) 751fun bimatch2_tac ctxt netpair i = 752 n_bimatch_from_nets_tac ctxt 2 netpair i THEN 753 (eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1)); 754 755(*Attack subgoals using safe inferences -- matching, not resolution*) 756fun clarify_step_tac ctxt = 757 let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in 758 appSWrappers ctxt 759 (FIRST' 760 [eq_assume_contr_tac ctxt, 761 bimatch_from_nets_tac ctxt safe0_netpair, 762 FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), 763 n_bimatch_from_nets_tac ctxt 1 safep_netpair, 764 bimatch2_tac ctxt safep_netpair]) 765 end; 766 767fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1)); 768 769 770(*** Unsafe steps instantiate variables or lose information ***) 771 772(*Backtracking is allowed among the various these unsafe ways of 773 proving a subgoal. *) 774fun inst0_step_tac ctxt = 775 assume_tac ctxt APPEND' 776 contr_tac ctxt APPEND' 777 biresolve_from_nets_tac ctxt (#safe0_netpair (rep_claset_of ctxt)); 778 779(*These unsafe steps could generate more subgoals.*) 780fun instp_step_tac ctxt = 781 biresolve_from_nets_tac ctxt (#safep_netpair (rep_claset_of ctxt)); 782 783(*These steps could instantiate variables and are therefore unsafe.*) 784fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt; 785 786fun unsafe_step_tac ctxt = 787 biresolve_from_nets_tac ctxt (#unsafe_netpair (rep_claset_of ctxt)); 788 789(*Single step for the prover. FAILS unless it makes progress. *) 790fun step_tac ctxt i = 791 safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' unsafe_step_tac ctxt) i; 792 793(*Using a "safe" rule to instantiate variables is unsafe. This tactic 794 allows backtracking from "safe" rules to "unsafe" rules here.*) 795fun slow_step_tac ctxt i = 796 safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' unsafe_step_tac ctxt) i; 797 798 799(**** The following tactics all fail unless they solve one goal ****) 800 801(*Dumb but fast*) 802fun fast_tac ctxt = 803 Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); 804 805(*Slower but smarter than fast_tac*) 806fun best_tac ctxt = 807 Object_Logic.atomize_prems_tac ctxt THEN' 808 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1)); 809 810(*even a bit smarter than best_tac*) 811fun first_best_tac ctxt = 812 Object_Logic.atomize_prems_tac ctxt THEN' 813 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt))); 814 815fun slow_tac ctxt = 816 Object_Logic.atomize_prems_tac ctxt THEN' 817 SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1)); 818 819fun slow_best_tac ctxt = 820 Object_Logic.atomize_prems_tac ctxt THEN' 821 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1)); 822 823 824(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 825 826val weight_ASTAR = 5; 827 828fun astar_tac ctxt = 829 Object_Logic.atomize_prems_tac ctxt THEN' 830 SELECT_GOAL 831 (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) 832 (step_tac ctxt 1)); 833 834fun slow_astar_tac ctxt = 835 Object_Logic.atomize_prems_tac ctxt THEN' 836 SELECT_GOAL 837 (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) 838 (slow_step_tac ctxt 1)); 839 840 841(**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome 842 of much experimentation! Changing APPEND to ORELSE below would prove 843 easy theorems faster, but loses completeness -- and many of the harder 844 theorems such as 43. ****) 845 846(*Non-deterministic! Could always expand the first unsafe connective. 847 That's hard to implement and did not perform better in experiments, due to 848 greater search depth required.*) 849fun dup_step_tac ctxt = 850 biresolve_from_nets_tac ctxt (#dup_netpair (rep_claset_of ctxt)); 851 852(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 853local 854 fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt); 855in 856 fun depth_tac ctxt m i state = SELECT_GOAL 857 (safe_steps_tac ctxt 1 THEN_ELSE 858 (DEPTH_SOLVE (depth_tac ctxt m 1), 859 inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac 860 (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state; 861end; 862 863(*Search, with depth bound m. 864 This is the "entry point", which does safe inferences first.*) 865fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) => 866 let 867 val deti = (*No Vars in the goal? No need to backtrack between goals.*) 868 if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I; 869 in 870 SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i 871 end); 872 873fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt); 874 875 876(* attributes *) 877 878fun attrib f = 879 Thm.declaration_attribute (fn th => fn context => 880 map_cs (f (Context.proof_of context) th) context); 881 882val safe_elim = attrib o addSE; 883val safe_intro = attrib o addSI; 884val safe_dest = attrib o addSD; 885val unsafe_elim = attrib o addE; 886val unsafe_intro = attrib o addI; 887val unsafe_dest = attrib o addD; 888 889val rule_del = 890 Thm.declaration_attribute (fn th => fn context => 891 context 892 |> map_cs (delrule (Context.proof_of context) th) 893 |> Thm.attribute_declaration Context_Rules.rule_del th); 894 895 896 897(** concrete syntax of attributes **) 898 899val introN = "intro"; 900val elimN = "elim"; 901val destN = "dest"; 902 903val _ = 904 Theory.setup 905 (Attrib.setup \<^binding>\<open>swapped\<close> (Scan.succeed swapped) 906 "classical swap of introduction rule" #> 907 Attrib.setup \<^binding>\<open>dest\<close> (Context_Rules.add safe_dest unsafe_dest Context_Rules.dest_query) 908 "declaration of Classical destruction rule" #> 909 Attrib.setup \<^binding>\<open>elim\<close> (Context_Rules.add safe_elim unsafe_elim Context_Rules.elim_query) 910 "declaration of Classical elimination rule" #> 911 Attrib.setup \<^binding>\<open>intro\<close> (Context_Rules.add safe_intro unsafe_intro Context_Rules.intro_query) 912 "declaration of Classical introduction rule" #> 913 Attrib.setup \<^binding>\<open>rule\<close> (Scan.lift Args.del >> K rule_del) 914 "remove declaration of intro/elim/dest rule"); 915 916 917 918(** proof methods **) 919 920local 921 922fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => 923 let 924 val [rules1, rules2, rules4] = Context_Rules.find_rules ctxt false facts goal; 925 val {extra_netpair, ...} = rep_claset_of ctxt; 926 val rules3 = Context_Rules.find_rules_netpair ctxt true facts goal extra_netpair; 927 val rules = rules1 @ rules2 @ rules3 @ rules4; 928 val ruleq = Drule.multi_resolves (SOME ctxt) facts rules; 929 val _ = Method.trace ctxt rules; 930 in 931 fn st => Seq.maps (fn rule => resolve_tac ctxt [rule] i st) ruleq 932 end) 933 THEN_ALL_NEW Goal.norm_hhf_tac ctxt; 934 935in 936 937fun rule_tac ctxt [] facts = some_rule_tac ctxt facts 938 | rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts; 939 940fun standard_tac ctxt facts = 941 HEADGOAL (some_rule_tac ctxt facts) ORELSE 942 Class.standard_intro_classes_tac ctxt facts; 943 944end; 945 946 947(* automatic methods *) 948 949val cla_modifiers = 950 [Args.$$$ destN -- Args.bang_colon >> K (Method.modifier (safe_dest NONE) \<^here>), 951 Args.$$$ destN -- Args.colon >> K (Method.modifier (unsafe_dest NONE) \<^here>), 952 Args.$$$ elimN -- Args.bang_colon >> K (Method.modifier (safe_elim NONE) \<^here>), 953 Args.$$$ elimN -- Args.colon >> K (Method.modifier (unsafe_elim NONE) \<^here>), 954 Args.$$$ introN -- Args.bang_colon >> K (Method.modifier (safe_intro NONE) \<^here>), 955 Args.$$$ introN -- Args.colon >> K (Method.modifier (unsafe_intro NONE) \<^here>), 956 Args.del -- Args.colon >> K (Method.modifier rule_del \<^here>)]; 957 958fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac); 959fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac); 960 961 962 963(** method setup **) 964 965val _ = 966 Theory.setup 967 (Method.setup \<^binding>\<open>standard\<close> (Scan.succeed (METHOD o standard_tac)) 968 "standard proof step: classical intro/elim rule or class introduction" #> 969 Method.setup \<^binding>\<open>rule\<close> 970 (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules))) 971 "apply some intro/elim rule (potentially classical)" #> 972 Method.setup \<^binding>\<open>contradiction\<close> 973 (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])) 974 "proof by contradiction" #> 975 Method.setup \<^binding>\<open>clarify\<close> (cla_method' (CHANGED_PROP oo clarify_tac)) 976 "repeatedly apply safe steps" #> 977 Method.setup \<^binding>\<open>fast\<close> (cla_method' fast_tac) "classical prover (depth-first)" #> 978 Method.setup \<^binding>\<open>slow\<close> (cla_method' slow_tac) "classical prover (slow depth-first)" #> 979 Method.setup \<^binding>\<open>best\<close> (cla_method' best_tac) "classical prover (best-first)" #> 980 Method.setup \<^binding>\<open>deepen\<close> 981 (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers 982 >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n))) 983 "classical prover (iterative deepening)" #> 984 Method.setup \<^binding>\<open>safe\<close> (cla_method (CHANGED_PROP o safe_tac)) 985 "classical prover (apply safe rules)" #> 986 Method.setup \<^binding>\<open>safe_step\<close> (cla_method' safe_step_tac) 987 "single classical step (safe rules)" #> 988 Method.setup \<^binding>\<open>inst_step\<close> (cla_method' inst_step_tac) 989 "single classical step (safe rules, allow instantiations)" #> 990 Method.setup \<^binding>\<open>step\<close> (cla_method' step_tac) 991 "single classical step (safe and unsafe rules)" #> 992 Method.setup \<^binding>\<open>slow_step\<close> (cla_method' slow_step_tac) 993 "single classical step (safe and unsafe rules, allow backtracking)" #> 994 Method.setup \<^binding>\<open>clarify_step\<close> (cla_method' clarify_step_tac) 995 "single classical step (safe rules, without splitting)"); 996 997 998(** outer syntax **) 999 1000val _ = 1001 Outer_Syntax.command \<^command_keyword>\<open>print_claset\<close> "print context of Classical Reasoner" 1002 (Scan.succeed (Toplevel.keep (print_claset o Toplevel.context_of))); 1003 1004end; 1005