1 module ThmTactics where 2 3 import Lookup 4 5 import Tactics 6 7 import Tacticals 8 9 import Kernel 10 11 import Tree 12 13 import Core_datatype 14 15 import DerivedRules 16 17 import Goals 18 19 import Vtslib 20 21 import Type_defs 22 23 import Parse 24 25 import X_interface 26 27 import Edlib 28 29 import Globals 30 31 import Tags -- partain 32 33 import Sub_Core1 34 35 import Sub_Core2 36 37 import Sub_Core3 38 39 import Sub_Core4 40 41 import Unparse 42 43 import Attributes 44 45 {- 46 rewrite_tac = Tactic "Rewrite" rewrite_input rewrite_subgoal 47 beta_tac = Tactic "Beta" beta_input beta_subgoal 48 eta_tac = Tactic "Eta" eta_input eta_subgoal 49 recurse_tac = Tactic "Recurse" recurse_input recurse_subgoal 50 -} 51 52 53 {- 54 create_name s i dc@(Symbol_dec t attL) 55 = case get_att Name_Style attL of 56 SOME _ -> (dc,i) 57 NONE -> (Symbol_dec t attL' , i+1) 58 where 59 nm = Name (s ++ nprimes i) 60 att = set_att Name_Style (Symbol_Name nm) 61 attL' = att : attL 62 63 64 create_name s i dc@(Axiom_dec t attL) 65 = case get_att Name_Style attL of 66 SOME _ -> (dc,i) 67 NONE -> (Axiom_dec t attL' , i+1) 68 where 69 nm = Name (s ++ nprimes i) 70 att = set_att Name_Style (Symbol_Name nm) 71 attL' = att : attL 72 -} 73 74 create_name s i (Decpair dc1 dc2 attL) 75 = (Decpair dc1' dc2' attL, i3) 76 where 77 (dc1',i2) = create_name s i dc1 78 (dc2',i3) = create_name s i2 dc2 79 80 create_name s i dc = (dc,i) 81 82 83 84 --nprimes i = take i ( repeat '\39' ) 85 86 {- 87 (******************************************************************************) 88 (* complete_thm *) 89 (* *) 90 (* ô *) 91 (* --------- Complete (ø : ô) *) 92 (* *) 93 (******************************************************************************) 94 -} 95 96 complete_tac = Tactic "Complete" complete_thm_input complete_thm 97 98 99 100 complete_thm gst sg lt (SOME [dv]) (ThmSpec itm) 101 = if not (is_valid_Thm th ) 102 then Bad mesg 103 else if eq_trm th_itm itm 104 then Ok ([], complete_thm_valid th) 105 else Bad ("Derivation does not prove given goal\n" ++ 106 "proves: " ++ unparse_trm sg ps th_itm ) 107 where 108 ps = fetch_ps gst 109 th = parse_Thm sg ps dv 110 ( TH_Err mesg ) = th 111 ( th_itm , _ ) = internal_Thm th 112 113 complete_thm _ _ _ _ _ = Bad "Goal is not a theorem" 114 115 116 117 118 complete_thm_valid th [] 119 = SOME (ThmDone th) 120 121 complete_thm_valid _ _ = NONE 122 123 124 125 complete_thm_input lt gst (ThmSpec tm) 126 = x_form True form /./ 127 exp 128 where 129 exp NONE = reTurn NONE 130 exp ( SOME [OutText s]) = reTurn ( SOME [s] ) 131 form = [InComment "Complete Theorem", InMultiText "Derivation" ""] 132 133 {- 134 (******************************************************************************) 135 (* gen_subgoal *) 136 (* *) 137 (* ±ë.ô *) 138 (* ------------ Gen *) 139 (* ë, Ûë] ô *) 140 (* *) 141 (******************************************************************************) 142 -} 143 144 gen_tac = OrdTactic "Gen" null_arg_fn gen_subgoal 145 146 gen_subgoal gst sg lt args (ThmSpec (Binder Forall dc tm _ _)) 147 = Ok (subgoals, [lt,lt], rwL, gen_valid sg ) 148 where 149 (dc',_) = create_name "xxx" 0 dc 150 subgoals = [DecSpec dc', ThmSpec tm] 151 rwL = [True, False] 152 -- ltL = [lt, extend_lookup_table true dc' lt] 153 154 gen_subgoal _ _ _ _ _ 155 = Bad "Cannot apply tactic to given goal" 156 157 158 159 160 gen_valid sg dnL rwL 161 = case (dnL, rwL) of 162 ([SOME (DecDone dc), SOME (ThmDone th)],_) 163 -> (rwL,[sg,extend dc sg],SOME (ThmDone (generalise th))) 164 ([SOME (DecDone dc), NONE], [true,_]) 165 -> ([True,True],[sg,extend dc sg],NONE) 166 _ -> (rwL,[sg,sg],NONE) 167 168 {- 169 (******************************************************************************) 170 (* disch_subgoal *) 171 (* *) 172 (* [ë] ¶ ô *) 173 (* -------------- Dischage *) 174 (* ë, ÛkÝ t *) 175 (******************************************************************************) 176 -} 177 178 disch_tac = OrdTactic "Disch" null_arg_fn disch_subgoal 179 180 disch_subgoal gst sg lt args (ThmSpec (Binder Imp dc tm _ _)) 181 = Ok (subgoals, [lt,lt], rwL, disch_valid sg) 182 where 183 (dc',_) = create_name "hhh" 0 dc 184 subgoals = [DecSpec dc', ThmSpec tm] 185 rwL = [True, False] 186 187 disch_subgoal _ _ _ _ _ 188 = Bad "Cannot apply 'Disch' to specified goal" 189 190 disch_valid sg dnL rwL 191 = case (dnL, rwL) of 192 ([SOME (DecDone dc), SOME (ThmDone th)],_) 193 -> (rwL,[sg,extend dc sg],SOME (ThmDone (discharge th))) 194 ([SOME (DecDone dc), NONE], [true,_]) 195 -> ([True,True],[sg,extend dc sg],NONE) 196 _ -> (rwL,[sg,sg],NONE) 197 198 {- 199 (******************************************************************************) 200 (* conj_subgoal *) 201 (* *) 202 (* æ ³ ù *) 203 (* ----- Conjunction *) 204 (* æ, ù *) 205 (******************************************************************************) 206 -} 207 208 conj_tac = Tactic "Conjunction" null_arg_fn conj_subgoal 209 210 conj_subgoal gst sg lt args (ThmSpec (Binary' And tm1 tm2 _ _)) 211 = Ok ([ThmSpec tm1, ThmSpec tm2], conj_valid) 212 213 conj_subgoal _ _ _ _ _ 214 = Bad "cannot apply tactic to specified goal" 215 216 217 conj_valid [SOME (ThmDone th1), SOME (ThmDone th2)] 218 = SOME (ThmDone (conj th1 th2)) 219 220 conj_valid _ = NONE 221 222 {- 223 (******************************************************************************) 224 (* disj_subgoal *) 225 (* *) 226 (* c *) 227 (* --------- Disjunction (ø : a´b) give either ø or a´b *) 228 (* a¶c, b¶c *) 229 (******************************************************************************) 230 -} 231 232 disj_tac = Tactic "Disjunction" disj_input disj_subgoal 233 234 disj_subgoal gst sg lt (SOME args) (ThmSpec tm) 235 = case args of 236 ["Derivation", dv] 237 -> if is_valid_Thm th 238 then case internal_Thm th of 239 (Binary' Or tm1 tm2 _ _ , _) 240 -> Ok ([ThmSpec tm4, ThmSpec tm5], 241 disj_dv_valid th) 242 where 243 dc1 = Axiom_dec tm1 [] 244 dc2 = Axiom_dec tm2 [] 245 tm3 = shift_trm [] 1 tm 246 tm4 = Binder Imp dc1 tm3 [] [] 247 tm5 = Binder Imp dc2 tm3 [] [] 248 _ -> Bad "Goal is not a disjunction" 249 else Bad mesg 250 where 251 ps = fetch_ps gst 252 th = parse_Thm sg ps dv 253 ( TH_Err mesg ) = th 254 255 ["Specification",tm_rep] 256 -> parse_trm sg ps tm_rep ||| 257 exp 258 where 259 exp tm6@(Binary' Or tm1 tm2 _ _) 260 = Ok ([ThmSpec tm4, ThmSpec tm5, 261 ThmSpec tm6], disj_tm_valid) 262 where 263 dc1 = Axiom_dec tm1 [] 264 dc2 = Axiom_dec tm2 [] 265 tm3 = shift_trm [] 1 tm 266 tm4 = Binder Imp dc1 tm3 [] [] 267 tm5 = Binder Imp dc2 tm3 [] [] 268 exp _ = Bad "Specification is not a disjunction" 269 ps = fetch_ps gst 270 _ -> Bad "No selection" 271 272 disj_subgoal _ _ _ _ _ = Bad "Cannot apply 'disjunction'" 273 274 275 disj_dv_valid th [SOME (ThmDone th1), SOME (ThmDone th2)] 276 = SOME (ThmDone (disj th th1 th2)) 277 278 disj_dv_valid _ _ = NONE 279 280 281 282 283 disj_tm_valid [SOME (ThmDone th1), SOME (ThmDone th2), SOME (ThmDone th3)] 284 = SOME (ThmDone (disj th3 th1 th2)) 285 286 disj_tm_valid _ = NONE 287 288 289 290 291 disj_input lt gst _ 292 = x_form True form /./ 293 exp 294 where 295 exp NONE = reTurn NONE 296 297 exp ( SOME [OutRadio s1,OutText s2] ) 298 = reTurn ( SOME [s1,s2] ) 299 300 form = [InComment "Disjunction", 301 InRadio "Argument Type" 0 ["Derivation","Specification"], 302 InMultiText "" ""] 303 304 {- 305 (******************************************************************************) 306 (* reflex_subgoal *) 307 (* *) 308 (* ô = ô *) 309 (* ----- Reflex *) 310 (* *) 311 (******************************************************************************) 312 -} 313 314 reflex_tac = Tactic "Reflex" null_arg_fn reflex_subgoal 315 316 reflex_subgoal gst sg lt args (ThmSpec (Binary' Eq' tm1 tm2 _ _)) 317 | eq_trm tm1 tm2 = Ok ([], reflex_valid (reflex (trm_to_Trm sg tm1))) 318 | otherwise = Bad "Terms not equal" 319 320 reflex_subgoal _ _ _ _ _ 321 = Bad "cannot apply 'reflex' to specified goal" 322 323 324 325 reflex_valid th [] = SOME (ThmDone th) 326 327 reflex_valid _ _ = NONE 328 329 {- 330 {- 331 (******************************************************************************) 332 (* rewrite_subgoal *) 333 (* *) 334 (* P[a]i *) 335 (* ----- Rewrite (ø : a = b) supply either ø or a=b *) 336 (* P[b]i *) 337 (* *) 338 (******************************************************************************) 339 -} 340 341 rewrite_subgoal gst sg lt (SOME [index,spec,spec_type]) (ThmSpec tm) 342 = case spec_type of 343 "Derivation" 344 -> case internal_Thm th of 345 (Binary' Eq' tm2 tm3 _ _ ,_) 346 | eq_trm tm1 tm2 347 -> Ok ([ThmSpec tm4], rewrite_th_valid iL th) 348 where 349 tm4 = replace_trm tm tm3 iL 350 | otherwise 351 -> Bad "LHS does not match subgoal" 352 _ -> Bad "Theorem not an equality" 353 where 354 iL = parse_index index 355 (tm1,dcL) = select_trm tm iL 356 sg1 = foldl ext_Sg sg dcL 357 ps = fetch_ps gst 358 th = parse_Thm sg ps spec 359 360 "Specification" 361 -> case parse_trm sg spec of -- add ps to parse 362 th_tm@(Binary' Eq' tm2 tm3 _ _) 363 | eq_trm tm1 tm2 364 -> Ok ([ThmSpec tm4, ThmSpec th_tm], 365 rewrite_tm_valid iL) 366 where 367 tm4 = replace_trm tm tm3 iL 368 | otherwise 369 -> Bad "LHS does not match subgoal" 370 _ -> Bad "Term not an equality" 371 where 372 iL = parse_index index 373 (tm1,dcL) = select_trm tm iL 374 sg1 = foldl ext_sg (internal_Sgn sg) dcL 375 ps = fetch_ps gst 376 377 rewrite_th_valid iL th [SOME (ThmDone th1)] 378 = SOME (ThmDone (subterm_rw th1 (symmetry th) iL)) 379 380 rewrite_tm_valid iL [SOME (ThmDone th1), SOME (ThmDone th2)] 381 = SOME (ThmDone (subterm_rw th1 (symmetry th2) iL)) 382 383 384 rewrite_input gst lt (ThmSpec tm) 385 = error "rewrite_input not implemented" 386 {- 387 = x_form True form /./ 388 exp 389 where 390 exp NONE -> reTurn NONE 391 392 exp ( SOME [OutSubterm s1,OutText s2,OutRadio s3] ) 393 = reTurn ( SOME [s1,s2,s3] ) 394 395 exp _ = return_err "Unexected arguments returned" 396 397 attL = get_attributes gst 398 (s,data) = unparse_trm_data ust1 tm 399 form = [InComment "Rewrite", 400 InSubterm s data, 401 InMultiText "Rewrite Theorem" "", 402 InRadio "Type of Input " 0 ["Derivation","Specification"]] 403 -} 404 405 406 parse_index inp 407 = case next_tk inp of 408 (SOME tk, inp1) -> read tk : parse_index inp1 409 (NONE, _) -> [] 410 411 ext_Sg sg dc = extend (dec_to_Dec sg dc) sg 412 413 ext_sg sg dc = Extend dc sg [] 414 415 -} 416 417 induction_tac= Tactic "Induction" null_arg_fn ind_subgoal 418 419 ind_subgoal gst sg lt args (ThmSpec (Binder Forall dc tm _ attL)) 420 = Ok ( gL , ind_valid ind_thm pL ) 421 where 422 tm1 = Binder Lambda dc tm [] attL 423 ( Symbol_dec st attL ) = dc 424 (i,j,spec,dcL,parmL) = get_datatype_info (internal_Sgn sg) st 425 specL = map (trm_to_Trm sg) spec 426 ind_thm = foldl specialise (induction (constructor sg i j 0)) specL 427 (Binder _ dec tm2 _ _ , _) = internal_Thm ind_thm 428 (spec_thm,pL) = find_betas (subst_trm dec tm2 tm1) 429 gL = map ThmSpec (reduce_ind spec_thm) ++ [TrmSpec tm1] 430 431 ind_subgoal _ _ _ _ _ 432 = Bad "Goal is not universally quantified" 433 434 435 436 reduce_ind (Binder Imp dc tm _ _) 437 = typ_of_dec dc : reduce_ind (shift_trm [] (-1) tm) 438 439 reduce_ind _ = [] 440 441 442 443 444 ind_valid th pL dnL 445 = SOME (ThmDone (foldl mp th1 dnL1)) 446 where 447 i = length dnL - 1 448 dnL1 = take i dnL 449 SOME (TrmDone tm) = head (drop i dnL) 450 th1 = rep_beta (specialise th tm) pL 451 mp th1 (SOME (ThmDone th2)) = modus_ponens th1 th2 452 453 454 455 456 457 458 459 460 461 462 axiom_tac = Tactic "Axiom" axiom_arg_fn axiom_subgoal 463 464 axiom_arg_fn gst lt (ThmSpec tm) 465 = x_form True form /./ 466 exp 467 where 468 exp NONE = reTurn NONE 469 470 exp ( SOME [OutText s] ) = reTurn ( SOME [s] ) 471 472 form = [InComment "Tactic: Axiom", InSingleText "Name Of Axiom" ""] 473 474 475 476 axiom_subgoal gst sg lt (SOME [name]) obj 477 = case lookup_name sg name of 478 SOME (Sym i j _ _) 479 -> if ( is_valid_Thm app_axiom ) 480 then Ok ([], axiom_valid app_axiom ) 481 else Bad ("Axiom: " ++ show i ++ " " ++ show j) 482 where 483 app_axiom = axiom sg i j 484 _ -> Bad ("No Such Axiom Name: " ++ name) 485 486 axiom_subgoal _ _ _ _ _ 487 = Bad "Hmm: it's failed, no name supplied perhaps?" 488 489 490 491 axiom_valid th [] = SOME (ThmDone th) 492 493 axiom_valid _ _ = NONE 494 495 496 497 498 499 500 501 502 503 hyp_tac = Tactic "Hyp" null_arg_fn find_hyp 504 505 find_hyp gst sg lt NONE (ThmSpec tm) 506 = case filter (find_match tm) hyps of 507 [] -> Bad "Can't find match" 508 (th : _) -> Ok ([], axiom_valid th) 509 where 510 hyps = get_hyp_from_sgn sg (internal_Sgn sg) 0 511 512 find_hyp _ _ _ _ _ 513 = Bad "goal is not a theorem specification" 514 515 516 517 get_hyp_from_sgn sg (Empty _) i = [] 518 519 get_hyp_from_sgn sg (Extend dc isg _) i 520 = l ++ get_hyp_from_sgn sg isg (i + 1) 521 where 522 (_, l) = get_hyp_from_dec sg dc i 0 523 524 get_hyp_from_sgn sg _ i = [] 525 526 527 528 get_hyp_from_dec sg (Axiom_dec _ _ ) i j = (j, [axiom sg i j]) 529 530 get_hyp_from_dec sg (Def _ _ _) i j = (j, [axiom sg i j]) 531 532 get_hyp_from_dec sg (Decpair dc1 dc2 _) i j 533 = (j'', l ++ l') 534 where 535 (j', l) = get_hyp_from_dec sg dc1 i (j+1) 536 (j'',l') = get_hyp_from_dec sg dc2 i (j' + 1) 537 538 get_hyp_from_dec _ _ _ j = (j, []) 539 540 541 542 find_match tm th 543 = eq_trm tm tm' 544 where 545 (tm',_) = internal_Thm th 546 547 548 549 550 551 {- 552 (******************************************************************************) 553 (* eq_subgoal *) 554 (* *) 555 (* a=b *) 556 (* --------- *) 557 (* a¶b b¶a *) 558 (******************************************************************************) 559 -} 560 561 eq_tac = Tactic "Eq" null_arg_fn eq_subgoal 562 563 eq_subgoal gst sg lt args (ThmSpec (Binary' Eq' itm1 itm2 _ _)) 564 = if eq_trm ty1 ty2 && eq_trm ty1 (Constant Bool' [] []) 565 then Ok ([ThmSpec tm3, ThmSpec tm4],eq_valid gst lt sg tm1 tm2) 566 else Bad "Equality not on booleans" 567 where 568 dc1 = Axiom_dec itm1 [] 569 dc2 = Axiom_dec itm2 [] 570 tm3 = Binder Imp dc1 (shift_trm [] 1 itm2) [] [] 571 tm4 = Binder Imp dc2 (shift_trm [] 1 itm1) [] [] 572 tm1 = trm_to_Trm sg itm1 573 tm2 = trm_to_Trm sg itm2 574 (ty1,_,_) = internal_Trm (typ_of_Trm tm1) 575 (ty2,_,_) = internal_Trm (typ_of_Trm tm2) 576 577 eq_subgoal _ _ _ _ _ = Bad "Cannot apply tactic to given goal" 578 579 580 581 eq_valid gst lt sg tm1 tm2 [SOME (ThmDone th1), SOME (ThmDone th2)] 582 = SOME (ThmDone th6) 583 where 584 inp = "\186(\177a:bool.\177b:bool.(a\182b)\182(b\182a)\182(a=b))" 585 ps = fetch_ps gst 586 eq_th = parse_Thm sg ps inp 587 th3 = specialise eq_th tm1 588 th4 = specialise th3 tm2 589 th5 = modus_ponens th4 th1 590 th6 = modus_ponens th5 th2 591 592 eq_valid _ _ _ _ _ _ = NONE 593 594 {- 595 (******************************************************************************) 596 (* or_subgoal *) 597 (* *) 598 (* a ³ b *) 599 (* ------- *) 600 (* µ a ¶ b *) 601 (******************************************************************************) 602 -} 603 604 or_tac = Tactic "Or" null_arg_fn or_subgoal 605 606 or_subgoal gst sg lt NONE (ThmSpec (Binary' Or tm1 tm2 _ _)) 607 = Ok ([ThmSpec tm3], or_valid gst lt sg tM1 tM2) 608 where 609 dc = Axiom_dec (Unary Not tm1 [] []) [] 610 tm3 = Binder Imp dc (shift_trm [] 1 tm2) [] [] 611 tM1 = trm_to_Trm sg tm1 612 tM2 = trm_to_Trm sg tm2 613 614 or_subgoal _ _ _ _ _ = Bad "Goal is not a disjunction" 615 616 617 618 or_valid gst lt sg tm1 tm2 [SOME (ThmDone th)] 619 = SOME (ThmDone th2) 620 where 621 inp = "\186(\177a:bool.\177b:bool.(\181a\182b)=(a\180b))" 622 ps = fetch_ps gst 623 or_th = parse_Thm sg ps inp 624 th1 = specialise (specialise or_th tm1) tm2 625 th2 = subterm_rw th th1 [] 626 627 or_valid _ _ _ _ _ _ = NONE 628 629 {- 630 (******************************************************************************) 631 (* not_subgoal *) 632 (* *) 633 (* µ µ a *) 634 (* ------- *) 635 (* a *) 636 (******************************************************************************) 637 -} 638 639 not_tac = Tactic "Not" null_arg_fn not_subgoal 640 641 not_subgoal gst sg lt NONE (ThmSpec (Unary Not (Unary Not tm1 _ _) _ _)) 642 = Ok ([ThmSpec tm1], not_valid gst lt sg tM1) 643 where 644 tM1 = trm_to_Trm sg tm1 645 646 not_subgoal _ _ _ _ _ = Bad "cannot apply 'Not' to given goal" 647 648 649 650 not_valid gst lt sg tm1 [SOME (ThmDone th)] 651 = SOME (ThmDone th2) 652 where 653 inp = "\186(\177a:bool.a=\181\181a)" 654 ps = fetch_ps gst 655 not_th = parse_Thm sg ps inp 656 th1 = specialise not_th tm1 657 th2 = subterm_rw th th1 [] 658 659 not_valid _ _ _ _ _ = NONE 660 661 662 {- 663 (******************************************************************************) 664 (* lemma-subgoal *) 665 (* *) 666 (* a *) 667 (* ------------ b *) 668 (* b ¶ a, b *) 669 (******************************************************************************) 670 -} 671 672 lemma_tac = Tactic "Lemma" lemma_input lemma_subgoal 673 674 lemma_subgoal gst sg lt (SOME [nm,spec]) (ThmSpec tm) 675 = parse_trm sg ps spec ||| 676 exp 677 where 678 ps = fetch_ps gst 679 exp lemma = Ok ( [g1,g2], lemma_valid ) 680 where 681 g1 = ThmSpec (Binder Imp dc tm' [] []) 682 where 683 rnm = Name nm 684 dc = Axiom_dec lemma [sym_nm rnm] 685 tm' = shift_trm [] 1 tm 686 g2 = ThmSpec lemma 687 688 lemma_subgoal _ _ _ _ _ = Bad "Goal is not a theorem specification" 689 690 691 692 lemma_valid [SOME (ThmDone th1), SOME (ThmDone th2)] 693 = SOME (ThmDone (modus_ponens th1 th2)) 694 695 lemma_valid _ = NONE 696 697 698 699 lemma_input gst lt (ThmSpec tm) 700 = x_form True form /./ 701 exp 702 where 703 exp NONE = reTurn NONE 704 705 exp ( SOME [OutText s1,OutText s2] ) 706 = reTurn ( SOME [s1,s2] ) 707 708 form = [InComment "Add lemma", 709 InSingleText "Name " "", 710 InMultiText "Lemma" ""] 711 712 {- 713 714 rw_input str gst lt (ThmSpec tm) 715 = error "re_input not implemented" 716 {- 717 = x_form True form /./ 718 exp 719 where` 720 exp NONE = reTurn NONE 721 722 exp ( SOME [OutSubterm s] ) = reTurn ( SOME [s] ) 723 724 exp _ = return_err "Unexected arguments returned" 725 726 attL = get_attributes gst 727 ust = get_default_us gst 728 val ust1 = U.set_defaults (U.set_lookup_table ust lt) attL 729 val (s,data) = unparse_trm_data ust1 tm 730 form = [InComment str, InSubterm s data] 731 -} 732 733 734 beta_subgoal gst sg lt (SOME [index]) (ThmSpec tm) 735 = Ok ( [ ThmSpec tm3 ] , beta_valid th iL ) 736 where 737 iL = parse_index index 738 (App (Binder Lambda dc tm1 _ _) tm2 _ _ ,dcL) 739 = select_trm tm iL 740 tm3 = replace_trm tm (subst_trm dc tm1 tm2) iL 741 th = reflex (trm_to_Trm sg tm) 742 743 744 745 beta_valid th iL [SOME (ThmDone th')] 746 = SOME (ThmDone (subterm_rw th' (beta_rw th (0:iL)) [])) 747 748 beta_valid _ _ _ = NONE 749 750 751 752 beta_input = rw_input "â Rewrite" 753 754 {- 755 fun eta_subgoal gst sg lt (SOME [index]) (ThmSpec tm) = 756 let val iL = parse_index (strings_to_input [index]) 757 val (Binder(Lambda,dc,App (tm1,Sym(0,0,_,_),_,_),_,_),dcL) = 758 select_trm tm iL 759 in if occurs 0 tm1 760 then fail "Not è-reducducable" 761 else 762 let val tm3 = replace_trm tm (shift_trm [] ~1 tm1) iL 763 val th = reflex (trm_to_Trm sg tm) 764 in ( [ ThmSpec tm3 ] , eta_valid th iL ) end 765 end 766 767 and eta_valid th iL [SOME (ThmDone th')] = 768 SOME (ThmDone (subterm_rw th' (eta_rw th (0::iL)) [])) 769 770 val eta_input = rw_input "è Rewrite" 771 -} 772 773 {- 774 fun recurse_subgoal gst sg lt (SOME [index]) (ThmSpec tm) = 775 let val iL = parse_index (strings_to_input [index]) 776 val (App (Recurse _,_,_,_),dcL) = select_trm tm iL 777 val th = recurse_rw (reflex (trm_to_Trm sg tm)) (0::iL) 778 val (Binary' (Eq',tm3,_,_,_), _) = internal_Thm th 779 in ( [ ThmSpec tm3 ] , recurse_valid th ) end 780 781 and recurse_valid th [SOME (ThmDone th')] = 782 SOME (ThmDone (subterm_rw th' th [])) 783 784 val recurse_input = rw_input "Recurse Rewrite" 785 -} 786 -} 787 788 taut_tac = Tactic "Taut" null_arg_fn taut_subgoal 789 790 taut_subgoal gst sg lt _ (ThmSpec tm) 791 = if is_valid_Thm th 792 then Ok ( [] , taut_valid th ) 793 else Bad mesg 794 where 795 th = taut (trm_to_Trm sg tm) 796 ( TH_Err mesg ) = th 797 798 taut_subgoal _ _ _ _ _ = Bad "goal is not a theorem specification" 799 800 801 802 taut_valid th [] = SOME (ThmDone th) 803 804 taut_valid _ _ = NONE 805 806 807 808 {- 809 (******************************************************************************) 810 (* exists_subgoal *) 811 (* *) 812 (* p *) 813 (* ------ ø : ²x.q *) 814 (* ±x.q¶p *) 815 (******************************************************************************) 816 -} 817 818 exists_elim_tac = Tactic "ExistsElim" exists_elim_input exists_elim_subgoal 819 820 exists_elim_subgoal gst sg lt (SOME [s1,"Derivation"]) (ThmSpec tm) 821 = parse_Thm_M sg ps s1 ||| 822 exp 823 where 824 ps = fetch_ps gst 825 exp th = Ok ( [ ThmSpec tm''' ] , exists_elim_valid th ) 826 where 827 (Binder Exists dc tm' _ _ ,_) = internal_Thm th 828 tm'' = Binder Imp (Axiom_dec tm' [])(shift_trm [] 2 tm) [] [] 829 tm''' = Binder Forall dc tm'' [] [] 830 831 exists_elim_subgoal gst sg lt (SOME [s1,"Specification"]) (ThmSpec tm) 832 = parse_trm sg ps s1 ||| 833 exp 834 where 835 ps = fetch_ps gst 836 exp tm1@(Binder Exists dc tm' _ _) 837 = Ok ( [ ThmSpec tm''', ThmSpec tm1 ] , exists_elim_valid' ) 838 where 839 tm'' = Binder Imp (Axiom_dec tm' []) (shift_trm [] 2 tm) [] [] 840 tm''' = Binder Forall dc tm'' [] [] 841 exp _ = Bad "term is not an existential" 842 843 exists_elim_subgoal _ _ _ _ _ 844 = Bad "Invalid application of 'ExistsElim'" 845 846 847 848 849 exists_elim_valid th' [SOME (ThmDone th)] 850 = SOME (ThmDone (exists_elim th' th)) 851 852 exists_elim_valid _ _ = NONE 853 854 855 856 exists_elim_valid' [SOME (ThmDone th1), SOME (ThmDone th2)] 857 = SOME (ThmDone (exists_elim th1 th2)) 858 859 exists_elim_valid' _ = NONE 860 861 862 863 864 865 exists_elim_input gst lt (ThmSpec tm) 866 = x_form True form /./ 867 exp 868 where 869 exp ( SOME [OutText s1,OutRadio s2] ) 870 = reTurn ( SOME [s1,s2] ) 871 872 exp _ = reTurn NONE 873 874 form = [InComment "Exists Elimination", 875 InMultiText "Existential Object" "", 876 InRadio "Type of Object" 0 ["Derivation","Specification"]] 877 878 879 strip split_tac auto_tac 880 = repeat_tac (snd (lift_tactic reflex_tac) `orelse` 881 snd (lift_tactic hyp_tac) `orelse` 882 -- snd (lift_tactic taut_tac) `orelse` 883 snd (lift_ordtactic gen_tac) `orelse` 884 snd (lift_ordtactic disch_tac) `orelse` 885 snd (lift_tactic conj_tac) `orelse` 886 snd (lift_tactic or_tac) `orelse` 887 snd (lift_tactic not_tac) `orelse` 888 snd (lift_tactic eq_tac) `orelse` 889 snd (lift_tactic auto_tac) ) -- `orelse` 890 -- snd (lift_ordtactic split_tac) ) 891 892 triv auto_tac 893 = snd (lift_tactic reflex_tac) `orelse` 894 snd (lift_tactic hyp_tac) `orelse` 895 snd (lift_tactic auto_tac) `orelse` 896 snd (lift_tactic taut_tac) `orelse` 897 ( \ trst -> reTurn trst ) 898