1structure ARM_proverLib :> ARM_proverLib = 2struct 3 4open Abbrev HolKernel boolLib bossLib Parse proofManagerLib; 5open arm_seq_monadTheory ; 6open tacticsLib inference_rulesTheory; 7 8(***************************************************************) 9(* ARM-PROVER: A Tool To Reason On ARM Model *) 10(* Narges *) 11(***************************************************************) 12 13 14exception not_matched_pattern; 15 16fun proof_progress s = if !Globals.interactive then TextIO.print s else () 17val let_ss = simpLib.mk_simpset [boolSimps.LET_ss] ; 18val words_ss = simpLib.mk_simpset [wordsLib.WORD_ss]; 19val global_mode = ref ``16w:bool[5]``; 20val simp_thms_list = ref ([]:(Theory.thm list)); 21 22val mode_changing_comp_list = 23 ref [``take_undef_instr_exception``, ``take_svc_exception``]; 24fun mode_changing_comp_list_rec lst opr = 25 case lst of 26 (x::rlst) => (same_const opr x) orelse mode_changing_comp_list_rec rlst opr 27 | _ => false; 28 29fun generate_uncurry_abs a = 30 case dest_term a of 31 (COMB (c,b)) => 32 if (same_const c ``UNCURRY``) then 33 let val (d,e) = 34 case dest_term b of 35 (LAMB(d,e)) => (d,e) 36 | _ => Raise not_matched_pattern 37 val (e_abs,e_trm) = generate_uncurry_abs e 38 in 39 (List.concat [[d],e_abs], e_trm) 40 end 41 else 42 ([], b) 43 | (LAMB(c,b)) => 44 ([c] , b) 45 | _ => ([], a); 46 47fun decompose_term a = 48 let val (opr, acs) = 49 case dest_term a of 50 (LAMB (b,c)) => 51 strip_comb c 52 | (* (COMB (b,c)) *) _ => 53 strip_comb a 54 in 55 if (length acs < 2) then 56 (opr,opr,opr) 57 else 58 let val l = List.nth(acs,0) 59 val r = List.nth(acs,1) 60 in 61 if (same_const opr (``$>>=``)) 62 then 63 let val (_,r_body) = pairLib.dest_pabs r 64 in 65 (l,r,r_body) 66 end 67 else 68 if (same_const opr ``$|||``) 69 then 70 (l,r,r) 71 else (opr,opr,opr) 72 end 73 end; 74 75 76 77fun get_monad_type tp = 78 let val (str , fst , snd) = 79 case dest_type (tp) of 80 (str , [fst , snd]) => (str , fst , snd) 81 | _ => Raise not_matched_pattern 82 val (str , tp_type, b) = 83 case dest_type snd of 84 (str , [tp_type, b]) => (str , tp_type, b) 85 | _ => Raise not_matched_pattern 86 in 87 tp_type 88 end; 89 90fun generate_uncurry_abs_from_abs a = 91 case dest_term a of 92 (LAMB (d,e)) => 93 let val (e_abs,e_trm) = generate_uncurry_abs_from_abs e 94 in 95 (List.concat [[d],e_abs], e_trm) 96 end 97 | _ => 98 ([] , a) ; 99 100fun get_action_from_goal gl = 101 let val (asm ,con) = gl 102 val (c1,d1) = if (is_comb con) 103 then 104 strip_comb con 105 else 106 Raise not_matched_pattern 107 (* val (c2,d2) = strip_comb (List.nth(d1,0)) *) 108 (* val (b,c) = if (is_comb (List.nth(d1,0))) *) 109 (* then *) 110 (* strip_comb (List.nth(d1,0)) *) 111 (* else *) 112 (* strip_comb (List.nth(d1,0)) *) 113 in 114 List.nth(d1,0) 115 end 116 117(* changed by Oliver *) 118 119 120fun find_mode_update cpsr_with_x = 121 let 122 val (update_indicator, [constant, rest]) = strip_comb cpsr_with_x 123 in 124 if (update_indicator = ``ARMpsr_M_fupd``) 125 then constant 126 else find_mode_update rest 127 end; 128 129 130fun get_mode_from_action_without_lambda a = 131 let 132 val (c1,d1) = strip_comb a 133 val found = find_mode_update (List.nth(d1,1)) 134 val (c3,d3) = strip_comb (found) 135 in 136 (List.nth(d3,0)) 137 end 138 139fun get_mode_from_action a = 140 (* let val _ = debug_out "get mode from action" [a] in *) 141 case dest_term a of 142 (LAMB (c,b)) => get_mode_from_action_without_lambda b 143 | _ => get_mode_from_action_without_lambda a 144(* end *); 145 146(* end of changes by Oliver *) 147 148 149fun get_trg_invr_mode_from_goal (asm,con) = 150 let 151 val (x,trg_inv) = 152 case dest_term con of 153 COMB(x,trg_inv) => (x,trg_inv) 154 | _ => Raise not_matched_pattern 155 156 val (x,trg_mode) = 157 case dest_term x of 158 COMB(x,trg_mode) => (x,trg_mode) 159 | _ => Raise not_matched_pattern 160 in 161 trg_mode 162 end; 163 164 165fun get_invrs_from_goal (asm,con) = 166 let 167 val (x,trg_inv) = 168 case dest_term con of 169 COMB(y,trg_inv) => 170 (case dest_term y of 171 COMB(z,trg_inv) => 172 ( case dest_term z of 173 COMB(k,trg_inv) => (k,trg_inv) 174 | _ => Raise not_matched_pattern) 175 | _ => Raise not_matched_pattern) 176 | _ => Raise not_matched_pattern 177 178 val (b,src_inv) = 179 case dest_term x of 180 COMB(b,src_inv) => 181 (b,src_inv) 182 | _ => Raise not_matched_pattern 183 in 184 (src_inv,trg_inv) 185 end; 186 187(* 188fun exists_theorem thy x = 189 let val thms = theorems thy 190 val thm = List.find (fn (s,t) => (s=x)) thms 191 in 192 case thm of 193 SOME (p,q) => true 194 | NONE => false 195 end;*) 196 197fun exists_theorem thy x = 198 let 199 val db_x = DB.find x 200 val res = List.find (fn ((s,t),p) => (t=x)) db_x in 201 case res of 202 SOME ((s,t),(p,q)) => true 203 |NONE => false 204 end; 205 206 207 208fun find_theorem x = 209 let 210 val _ = proof_progress ("Searching for the theorem " ^ (x) ^ "\n") 211 val db_x = DB.find x 212 val res = List.find (fn ((s,t),p) => (t=x)) db_x in 213 case res of 214 SOME ((s,t),(p,q)) => 215 let val _ = proof_progress ("The theorem " ^ x ^ " was found\n ") in 216 p 217 end 218 |NONE => 219 let val _ = proof_progress ("The theorem " ^ x ^ " was not found\n ") in 220 ASSUME ``T`` 221 end 222 end; 223 224 225fun prove_simple_action opr a uargs pthms = 226 let 227 val mode_changing_comp = 228 fn (opr) => 229 (mode_changing_comp_list_rec (! mode_changing_comp_list) opr) (*changed by Oliver *) 230 231 val uf_fun = List.nth(uargs,0) 232 val uy_fun = List.nth(uargs,1) 233 val cm = List.nth(uargs,2) 234 val ext = term_to_string(List.nth(uargs,3)) 235 236 val (src_inv,trg_inv) = get_invrs_from_goal(top_goal()); 237 val same_mode = (term_eq src_inv trg_inv); 238 val thrm = 239 if (same_mode (* andalso (! global_mode=``16w:bool[5]``) *)) orelse 240 (same_const opr ``write_cpsr``) 241 then 242 (* (DB.fetch (current_theory()) ((Hol_pp.term_to_string (opr)) ^ ext)) *) 243 find_theorem ((Hol_pp.term_to_string (opr)) ^ ext) 244 else 245 (* (DB.fetch (current_theory()) ((Hol_pp.term_to_string (opr)) ^ "_comb"^ ext))*) 246 find_theorem ((Hol_pp.term_to_string (opr)) ^ "_comb"^ ext) 247 val _ = if (same_mode (* andalso (! global_mode=``16w:bool[5]``) *)) 248 then 249 proof_progress ("\nTheorem " ^ (term_to_string opr) ^ ext ^ " is applied!\n ") 250 else 251 proof_progress ("\nTheorem " ^ (term_to_string opr) ^ "_comb" ^ ext ^ " is applied!\n ") 252 ; 253 val tacs = 254 if (same_const opr ``write_cpsr``) 255 then 256 RW_TAC (srw_ss()) [SPECL [``16w:bool[5]``,(get_mode_from_action a )] thrm] 257 else 258 if (same_mode orelse (mode_changing_comp opr)) 259 then 260 RW_TAC (srw_ss()) [thrm] 261 else 262 let 263 val b_thm = if (same_const opr ``errorT``) 264 then 265 let 266 val (c,str) = 267 case dest_term a of 268 COMB(c,str) => (c,str) 269 |_ => Raise not_matched_pattern 270 in 271 if (same_mode) 272 then 273 SPECL [uf_fun,uy_fun] ( 274 INST_TYPE [alpha |-> 275 get_monad_type(type_of(a))] thrm) 276 else 277 SPECL [src_inv, trg_inv, 278 str,uf_fun,uy_fun] 279 (INST_TYPE [alpha |-> 280 get_monad_type(type_of(a))] thrm) 281 end 282 else 283 let val a_thm = SPECL [``assert_mode 16w``, 284 ``assert_mode ^cm``, 285 trg_inv, ``assert_mode 16w``, a, uf_fun,uy_fun] 286 (INST_TYPE [alpha |-> get_monad_type(type_of(a))] 287 preserve_relation_comb_thm1) 288 289 val _ = proof_progress ("\nTheorem " ^ (term_to_string (concl a_thm)) ^ " \n\n\n ") 290 in 291 LIST_MP [thrm, 292 SPECL [``16w:bool[5]``, cm] comb_mode_thm] a_thm 293 end 294 in 295 RW_TAC (srw_ss()) [b_thm] 296 end 297 298 val _ = e (tacs) 299 val proved_a = top_thm() 300 val _ = proofManagerLib.drop() 301 302 val cm' = (same_const opr ``write_cpsr``); 303 val new_mode = 304 if (cm') 305 then 306 ``^cm:bool[5]`` 307 else 308 !global_mode; 309 val () = global_mode := new_mode 310 val _ = proof_progress ("\nProof of theorem: " ^ (term_to_string a) ^ " is completed!\n "^ 311 "global mode is " ^ (term_to_string (!global_mode))) 312 in 313 (proved_a , tacs) 314 end; 315 316 317 318fun decompose a src_inv trg_inv uargs = 319 let val (opr, acs) = 320 case dest_term a of 321 (LAMB (b,c)) => 322 strip_comb c 323 | (* (COMB (b,c)) *) _ => 324 strip_comb a 325 val ext = term_to_string(List.nth(uargs,3)) 326 327 val thm_exists = if ((term_eq src_inv trg_inv)) orelse 328 ((same_const opr ``write_cpsr``) ) 329 then 330 exists_theorem (current_theory()) (term_to_string opr ^ ext) 331 else 332 exists_theorem (current_theory()) (term_to_string opr ^ "_comb" ^ ext) 333 334 val flag = ((same_const opr ``$>>=``) orelse 335 (same_const opr ``$|||``) orelse 336 (same_const opr ``constT``) orelse 337 (same_const opr ``COND``) orelse 338 (same_const opr ``condT``) orelse 339 (same_const opr ``forT``) orelse 340 (TypeBase.is_case a ) orelse 341 thm_exists) 342 in 343 if (length acs < 2) then 344 (flag,opr,opr,opr) 345 else 346 let val l = List.nth(acs,0) 347 val r = List.nth(acs,1) 348 in 349 if (same_const opr (``$>>=``)) 350 then (flag,l,r,opr) 351 else 352 if (same_const opr ``$|||``) then 353 (flag,l,r,opr) 354 else (flag,opr,opr,opr) 355 end 356 end; 357 358(* should be modified to save untouching and preserving lemmas as two separate lemmas*) 359 360fun save_proof name a tacs = 361 let val _ = TextIO.print ("Do you like to save the following theorem? \n " ^ 362 (term_to_string (a)) ^ " \n") 363 (* val _ = valOf (TextIO.inputLine TextIO.stdIn) *) 364 val str = valOf (TextIO.inputLine TextIO.stdIn) 365 in 366 case str of 367 "y\n" => 368 let val _ = store_thm (((term_to_string (name)) ^ "_thm"), ``preserve_relation_mmu ^a``, tacs) 369 in 370 store_thm (((term_to_string (name)) ^ "_ut_thm"), ``preserve_relation_mmu ^a``, tacs) 371 end 372 | _ => 373 store_thm ("tatulogy", ``T``, DECIDE_TAC) 374 end; 375 376 377 378val get_type_inst = 379 fn (t, i) => 380 case dest_type (t) of 381 (str , [fst , snd]) => 382 if(i) 383 then 384 fst 385 else 386 snd 387 |_ => Raise not_matched_pattern; 388 389(*TODO: use some sort of pattern mathiching instead of list lenght!!!*) 390fun get_uncurried_theorem thm l = 391 let val (asm,con) = dest_thm thm 392 in 393 if( l = 1) 394 then 395 thm 396 else 397 let 398 val con = concl thm 399 val res_thm1 = PairRules.SWAP_PFORALL_CONV con 400 val res_thm2 = REWRITE_RULE [res_thm1] thm 401 val con1 = concl res_thm1 402 val (a,b) = dest_eq con1 403 val res_thm3 = PairRules.UNCURRY_FORALL_CONV b 404 val res_thm = REWRITE_RULE [res_thm3] res_thm2 405 in 406 get_uncurried_theorem res_thm (l-1) 407 end 408 end; 409 410fun generalize_theorem thm a = 411 let 412 val (a_abs,a_body) = pairLib.dest_pabs a 413 val (abs_args, abs_body) = generate_uncurry_abs a 414 val generalized_curried_thm = PairRules.PGENL (List.rev(abs_args)) thm 415 val generalized_uncurried_thm = 416 get_uncurried_theorem generalized_curried_thm (List.length(abs_args)) 417 val abs_type = type_of a_abs 418 val gen_var = (mk_var("y", abs_type)) 419 val spec_thm= PairRules.PSPEC gen_var generalized_uncurried_thm 420 val generalized_thm = GEN gen_var spec_thm 421 in 422 generalized_thm 423 end; 424 425fun build_right_hand_side (src_inv, trg_inv, 426 rsrc_inv, rtrg_inv, 427 lsrc_inv, ltrg_inv, 428 l, r, a, 429 right_hand_thm,(* is_write_cpsr, *) 430 flg,uargs,trans_uf_thm) = 431 let 432 val uf_fun = List.nth(uargs,0) 433 val uy_fun = List.nth(uargs,1) 434 val cm = List.nth(uargs,2) 435 436 val l_type = get_monad_type(type_of(l)); 437 val r_type = 438 if(flg) 439 then 440 (get_monad_type ( get_type_inst (type_of(r) ,false))) 441 else 442 get_monad_type (type_of(r)) 443 val same_whole_mode = (term_eq src_inv trg_inv); 444 val same_right_mode = (term_eq rsrc_inv rtrg_inv); 445 val same_left_mode = (term_eq lsrc_inv ltrg_inv); 446 447 val r_type' = if ( same_right_mode ) 448 then 449 r_type 450 else 451 get_monad_type (type_of(r)) 452 453 val base_thm = if (flg) 454 then 455 if ( same_whole_mode orelse 456 (same_right_mode andalso same_left_mode)) 457 then 458 seqT_preserves_relation_uu_thm 459 else 460 if(same_right_mode orelse (not same_left_mode)) 461 then 462 seqT_preserves_relation_up2_thm 463 else 464 seqT_preserves_relation_uc_thm 465 466 else 467 if (same_whole_mode) 468 then 469 parT_preserves_relation_uu_thm 470 else 471 parT_preserves_relation_up_thm 472 473 in 474 (*************************************************************************) 475 (*for computations in user mode BEFORE seeing take_exception or write_cpsr*) 476 (*************************************************************************) 477 if (same_whole_mode) 478 then 479 let 480 val operator_tac = 481 ASSUME_TAC (SPECL [l,r, !global_mode,uf_fun,uy_fun] 482 (INST_TYPE [alpha |-> l_type, 483 beta |-> r_type'] 484 base_thm)) 485 in 486 ASSUME_TAC right_hand_thm 487 THEN operator_tac 488 THEN ASSUME_TAC trans_uf_thm 489 THEN ASSUME_TAC (SPEC rtrg_inv comb_monot_thm) 490 THEN RES_TAC 491 end 492 else 493 (*************************************************************************) 494 (*for computations AFTER seeing take_exception or write_cpsr*) 495 (*************************************************************************) 496 ASSUME_TAC right_hand_thm 497 THEN ASSUME_TAC trans_uf_thm 498 THEN 499 (if (same_left_mode) 500 then 501 if (same_right_mode) 502 then 503 IMP_RES_TAC (SPECL [l,r, 504 !global_mode,uf_fun,uy_fun] 505 (INST_TYPE [alpha |-> l_type, 506 beta |-> r_type] 507 base_thm 508 )) 509 THEN ASSUME_TAC (SPECL [!global_mode, cm] comb_mode_thm) 510 THEN ASSUME_TAC (SPECL [src_inv,``(assert_mode ^cm)``, 511 trg_inv,src_inv,a , 512 uf_fun,uy_fun] 513 (INST_TYPE [alpha |-> get_monad_type(type_of(a))] 514 preserve_relation_comb_v2_thm)) 515 else 516 ASSUME_TAC (SPECL [``16w:bool[5]``,cm] comb_mode_thm) 517 THEN IMP_RES_TAC 518 (SPECL [src_inv,``(assert_mode ^cm)``, 519 trg_inv,src_inv,r ,uf_fun,uy_fun] 520 (INST_TYPE [alpha |-> l_type, 521 beta |-> get_monad_type(type_of(a))] 522 preserve_relation_comb_abs_thm)) 523 THEN ASSUME_TAC (SPECL [l,r, ``16w:bool[5]``, cm, 524 trg_inv ,uf_fun,uy_fun] 525 (INST_TYPE [alpha |-> l_type, 526 beta |-> r_type] 527 base_thm)) 528 else 529 ASSUME_TAC (SPECL [l,r, ``16w:bool[5]``, 530 !global_mode, 531 uf_fun,uy_fun] 532 (INST_TYPE [alpha |-> l_type, 533 beta |-> r_type] 534 base_thm))) 535 536 end 537 538 539 540 541fun prove a src_inv trg_inv uargs pthms = 542 let 543 val prove_COND_action = 544 fn (if_part,else_part,condition,a,src_inv,trg_inv,uargs,pthms) => 545 let val _ = proof_progress ("A Conditional action\n\n\n") 546 547 val (if_part_thm,tc) = prove if_part src_inv trg_inv uargs pthms; 548 val (else_part_thm,tc') = prove else_part src_inv trg_inv uargs pthms; 549 val tacs = (ASSUME_TAC if_part_thm) 550 THEN (ASSUME_TAC else_part_thm) 551 THEN (IF_CASES_TAC ) 552 THEN (FULL_SIMP_TAC (srw_ss()) []) 553 THEN (FULL_SIMP_TAC (srw_ss()) []) 554 val _ = e (tacs) 555 val proved_b = top_thm() 556 val _ = proofManagerLib.drop() 557 in 558 (proved_b, tacs) 559 end 560 561 562 val prove_composite_action = 563 fn (l, r, opr, a, src_inv, trg_inv,uargs,pthms) => 564 let val _ = proof_progress ("\n\nProof of the compositional action:\n" 565 ^(term_to_string a)^"\n\n") 566 val cm = List.nth(uargs,2) 567 568 (* val (f,ll ,lr , oprr) = decompose r src_inv trg_inv uargs; *) 569 570 (* proof of the left part*) 571 val (lsrc_inv,ltrg_inv) = 572 ( ``assert_mode ^(!global_mode)`` , 573 ``assert_mode ^(!global_mode)``); 574 575 val (left_hand_thm , tc) = prove l lsrc_inv ltrg_inv uargs pthms 576 val tacs = (ASSUME_TAC left_hand_thm) 577 val _ = e (tacs) 578 579 (* proof of the right part*) 580 val (rsrc_inv , rtrg_inv ) = 581 if (String.isSubstring "take_undef_instr_exception" 582 (Hol_pp.term_to_string r)) orelse 583 (String.isSubstring "take_svc_exception_part2" 584 (Hol_pp.term_to_string r)) 585 then 586 (src_inv , trg_inv) 587 else 588 ( ``assert_mode ^(!global_mode)`` , 589 ``assert_mode ^(!global_mode)``); 590 val (right_hand_thm, tc) = prove r rsrc_inv rtrg_inv uargs pthms; 591 592 (* combining the left and right parts *) 593 val tacsb = 594 (if (same_const opr ``$>>=``) 595 then 596 build_right_hand_side (src_inv, trg_inv, 597 rsrc_inv, rtrg_inv, 598 lsrc_inv, ltrg_inv, 599 l , r, a, right_hand_thm, 600 (* is_write_cpsr, *) true,uargs, 601 List.nth(pthms,0)) 602 else 603 build_right_hand_side (src_inv, trg_inv, 604 rsrc_inv, rtrg_inv, 605 lsrc_inv, ltrg_inv, 606 l, r, a, right_hand_thm, 607 (* is_write_cpsr , *)false,uargs, 608 List.nth(pthms,0))) 609 THEN RES_TAC 610 THEN (RW_TAC (srw_ss()) []) 611 612 val _ = e (tacsb) 613 val thrm = top_thm() 614 val _ = proofManagerLib.drop() 615 in 616 (thrm,tacs THEN tacsb) 617 end 618 619 620 val prove_constT_action = 621 fn (a,src_inv, trg_inv,uargs,pthms) => 622 let 623 val (opr, arg) = 624 case dest_term a of 625 COMB (opr, arg) => (opr, arg) 626 |_ => Raise not_matched_pattern 627 val trans_uf_thm = List.nth(pthms,1) 628 val tac = ASSUME_TAC ((* SPEC (!global_mode) *) trans_uf_thm) 629 THEN RW_TAC (srw_ss()) 630 [(SPECL [src_inv,arg, 631 List.nth(uargs,0), List.nth(uargs,1)] 632 (INST_TYPE [alpha |-> (type_of arg)] 633 constT_preserves_relation_thm))] 634 val _ = e (tac) 635 val proved_thm = top_thm() 636 val _ = proofManagerLib.drop() 637 in 638 (proved_thm, tac) 639 end 640 val prove_forT_action = 641 fn (a,src_inv,trg_inv, uargs,pthms) => 642 let 643 val (opr, l,r,action) = 644 case strip_comb a of 645 (opr, [l,r,action]) => (opr, l,r,action) 646 |_ => Raise not_matched_pattern 647 648 val (sub_thm , aub_tac) = prove action src_inv trg_inv uargs pthms 649 val snd = get_type_inst (type_of(action), false) 650 (*val (str , [fst , snd]) = dest_type (type_of(action))*) 651 val r_type = get_monad_type(snd) 652 val tacs = ASSUME_TAC sub_thm 653 THEN ASSUME_TAC (List.nth(pthms,0)) 654 THEN ASSUME_TAC (List.nth(pthms,1)) 655 THEN ASSUME_TAC (List.nth(pthms,5)) 656 THEN ASSUME_TAC (SPECL [action, ``16w:word5``, (List.nth(uargs,0)), (List.nth(uargs,1))] (INST_TYPE [alpha |-> r_type] forT_preserving_thm)) 657 THEN RW_TAC (srw_ss()) [] (*changed by Oliver to enable loops *) 658 val _ = e (tacs) 659 val proved_thm = top_thm() 660 val _ = proofManagerLib.drop() 661 in 662 (proved_thm, tacs) 663 end 664 val prove_condT_action = 665 fn (a,src_inv,trg_inv,uargs,pthms) => 666 let val (opr, acs) = strip_comb a 667 668 val reflex_uf_thm = List.nth(pthms,1) 669 val (arg_thm,tc) = prove (List.nth(acs,1)) src_inv trg_inv uargs pthms 670 val tacs = ASSUME_TAC arg_thm 671 THEN ASSUME_TAC reflex_uf_thm 672 THEN RW_TAC (srw_ss()) [condT_preserves_relation_thm] 673 val _ = e (tacs) 674 val proved_thm = top_thm() 675 val _ = proofManagerLib.drop() 676 in 677 (proved_thm,tc) 678 end 679 val prove_case_body = 680 fn (opt,body,flag,src_inv,trg_inv,uargs,pthms) => 681 let val (body_thm,body_tac) = prove body src_inv trg_inv uargs pthms 682 val tacs = if (flag) then 683 CASE_TAC 684 THEN FULL_SIMP_TAC (srw_ss()) [] 685 THEN1 (ASSUME_TAC body_thm 686 THEN FULL_SIMP_TAC (srw_ss()) [preserve_relation_mmu_def] 687 THEN (FULL_SIMP_TAC (srw_ss()) [])) 688 else 689 (ASSUME_TAC body_thm 690 THEN FULL_SIMP_TAC (srw_ss()) [preserve_relation_mmu_def] 691 THEN (FULL_SIMP_TAC (srw_ss()) [])) 692 val _ = e (tacs) 693 in 694 (body_thm, tacs) 695 end 696 697 (* TODO: it does not return the tactic list correctly *) 698 val prove_case_action = 699 fn (a ,src_inv,trg_inv,uargs,pthms) => 700 let val tacs = FULL_SIMP_TAC bool_ss [preserve_relation_mmu_def] THEN CASE_TAC 701 val _ = e (tacs) 702 val (case_tag, case_options) = TypeBase.strip_case a 703 in 704 if (List.length(top_goals()) =2) 705 then 706 let val _ = proofManagerLib.backup() 707 val cases = tl ((List.rev(case_options))) 708 val proved_cases = 709 map (fn (opt, body) => 710 prove_case_body (opt, body,true,src_inv,trg_inv,uargs,pthms)) cases 711 val (opt , body) = hd(List.rev(case_options)) 712 val (body_thm,body_tac) = prove body src_inv trg_inv uargs pthms 713 val tacsb = (ASSUME_TAC body_thm 714 THEN FULL_SIMP_TAC (srw_ss()) [preserve_relation_mmu_def] 715 THEN (FULL_SIMP_TAC (srw_ss()) [] ORELSE METIS_TAC [])) 716 val _ = e (tacsb) 717 val (proved_thm) = top_thm() 718 val _ = proofManagerLib.drop() 719 in 720 (proved_thm, tacs 721 THEN (foldl (fn ((thm,tac),tacsc) => tacsc THEN tac) (NO_TAC) proved_cases) 722 THEN tacsb) 723 end 724 else 725 let val proved_cases = map (fn (opt, body) => 726 prove_case_body (opt, body,false,src_inv, trg_inv,uargs,pthms)) case_options 727 val (proved_thm) = top_thm() 728 val _ = proofManagerLib.drop() 729 in 730 (proved_thm, NO_TAC) 731 end 732 end 733 734 val analyze_action = 735 fn (a, l , r, opr,src_inv,trg_inv,uargs,pthms) => 736 if ((same_const opr ``$>>=``) orelse 737 (same_const opr ``$|||``)) 738 then 739 prove_composite_action (l, r, opr ,a,src_inv,trg_inv,uargs,pthms) 740 else 741 if (same_const opr ``COND``) then 742 let 743 val (opr, acs) = strip_comb a 744 val (if_part,else_part) = (List.nth(acs,1),List.nth(acs,2)) ; 745 in 746 prove_COND_action (if_part, else_part,List.nth(acs,0),a,src_inv,trg_inv,uargs,pthms) 747 end 748 else 749 if (same_const opr ``constT``) then 750 prove_constT_action (a,src_inv,trg_inv,uargs,pthms) 751 else if (same_const opr ``forT``) then 752 prove_forT_action (a,src_inv,trg_inv,uargs,pthms) 753 else 754 if (TypeBase.is_case a) then 755 prove_case_action (a,src_inv,trg_inv,uargs,pthms) 756 else 757 let val _ = proof_progress ("\n\nProof of a simple action:\n "^(term_to_string l)^"\n\n") 758 759 val thm_exist = ((exists_theorem (current_theory()) 760 (term_to_string l ^ "_thm")) 761 orelse (exists_theorem (current_theory()) 762 (term_to_string l ^ "_comb_thm"))) in 763 if (thm_exist) 764 then 765 prove_simple_action l a uargs pthms 766 else 767 prove_condT_action (a,src_inv,trg_inv,uargs,pthms) 768 end 769 val prove_abs_action = 770 fn (a,src_inv,trg_inv,uargs,pthms) => 771 let 772 val uf_fun = List.nth(uargs,0) 773 val uy_fun = List.nth(uargs,1) 774 val (a_abs,a_body) = pairLib.dest_pabs a; 775 val _ = set_goal([], `` 776 (preserve_relation_mmu_abs ^a ^src_inv ^trg_inv ^uf_fun ^uy_fun) ``) 777 val _ = e (FULL_SIMP_TAC (let_ss) (!simp_thms_list)) (*change of Oliver*) 778 val (proved_a,b) = prove a_body src_inv trg_inv uargs pthms 779 780 val unbeta_thm= (PairRules.UNPBETA_CONV a_abs a_body) 781 val unbeta_a = mk_comb (a, a_abs) 782 val snd = get_type_inst (type_of(a_body) , false) 783 val a_body_type = get_type_inst (snd, true) 784 785 val proved_unbeta_lemma = 786 Tactical.prove (``(preserve_relation_mmu ^a_body ^src_inv ^trg_inv ^uf_fun ^uy_fun)= 787 (preserve_relation_mmu ^unbeta_a ^src_inv ^trg_inv ^uf_fun ^uy_fun)``, 788 (ASSUME_TAC (SPECL [a_body,``^unbeta_a``,src_inv,trg_inv,uf_fun,uy_fun] 789 (INST_TYPE[alpha |-> a_body_type] first_abs_lemma))) 790 THEN (ASSUME_TAC unbeta_thm) 791 THEN (RES_TAC)) 792 793 val proved_preserve_unbeta_a = 794 Tactical.prove (`` (preserve_relation_mmu ^unbeta_a ^src_inv ^trg_inv ^uf_fun ^uy_fun)``, 795 (ASSUME_TAC (proved_unbeta_lemma)) 796 THEN (ASSUME_TAC proved_a) 797 THEN (FULL_SIMP_TAC (srw_ss()) [])) 798 799 val abs_type = type_of a_abs 800 val (abs_args, abs_body) = generate_uncurry_abs a 801 val tacs = (ASSUME_TAC proved_preserve_unbeta_a) 802 val gen_preserve_unbeta_thm = generalize_theorem proved_preserve_unbeta_a a 803 val tacs = tacs THEN (ASSUME_TAC gen_preserve_unbeta_thm) 804 THEN (ASSUME_TAC ( 805 SPECL[a, src_inv,trg_inv, uf_fun, uy_fun] 806 (INST_TYPE [alpha |-> abs_type, 807 beta |-> a_body_type] second_abs_lemma))) 808 THEN (RW_TAC (srw_ss()) []) 809 THEN (FULL_SIMP_TAC (srw_ss()) []) 810 THEN (UNDISCH_ALL_TAC THEN 811 (RW_TAC (srw_ss()) []) 812 THEN (FULL_SIMP_TAC (srw_ss()) [])) 813 val _ = e (tacs) 814 val proved_thm = top_thm() 815 val _ = proofManagerLib.drop() 816 in 817 (proved_thm,tacs) 818 end 819 820 val prove_simple_unproved_action = 821 fn (a, opr ,uargs, pthms) => 822 let val a_name = opr 823 val _ = if !Globals.interactive then 824 TextIO.print ("Do you have a theorem to prove " ^ (term_to_string (a)) ^ " theorem? \n\n") 825 else () 826 val simp_thms = [List.nth(pthms,2), 827 List.nth(pthms,3)] 828 in 829 if (same_const opr ``readT``) 830 then 831 let val tac = RW_TAC (srw_ss()) 832 (simp_thms@[preserve_relation_mmu_def,similar_def,readT_def, 833 equal_user_register_def, 834 comb_def,comb_mode_def,assert_mode_def]) 835 THEN FULL_SIMP_TAC (let_ss) 836 (simp_thms@ [untouched_def, readT_def]) 837 THEN FULL_SIMP_TAC (srw_ss()) 838 (simp_thms@[untouched_def, readT_def]) 839 THEN (REPEAT (RW_TAC (srw_ss()) [])) 840 841 val _ = e (tac) 842 val (proved_thm) = top_thm() 843 val _ = proofManagerLib.drop() 844 in 845 (proved_thm, tac) 846 end 847 else 848 849 let 850 val simp_thm = find_theorem ((term_to_string (opr))^"_def") 851 val tacs = (FULL_SIMP_TAC (srw_ss()) [simp_thm,writeT_def]) 852 val _ = e (tacs) 853 val (asm,con) = top_goal() 854 val a' = get_action_from_goal (top_goal()) 855 val (flag,l ,r , opr) = decompose a' src_inv trg_inv uargs 856 val (proved_a, tacb) = 857 if (flag) 858 then 859 analyze_action (a', l, r, opr,src_inv,trg_inv,uargs,pthms) 860 else 861 let 862 val (next_proof , next_tac) = prove a' src_inv trg_inv uargs pthms 863 val tac = RW_TAC (srw_ss()) [next_proof] 864 val _ = e (tac) 865 val (proved_thm) = top_thm() 866 val _ = proofManagerLib.drop() 867 in 868 (proved_thm, tac) 869 end 870 val tacs = tacs THEN tacb 871 in 872 (proved_a, tacs) 873 end 874 end 875 in 876 let val (proved_thm,tacs) = 877 case dest_term a of 878 (LAMB (c,b)) => 879 prove_abs_action (a,src_inv,trg_inv,uargs,pthms) 880 | COMB (c,b) => 881 if (same_const c ``UNCURRY``) 882 then 883 prove_abs_action (a,src_inv,trg_inv,uargs,pthms) 884 else 885 let val uf_fun = List.nth(uargs,0) 886 val uy_fun = List.nth(uargs,1) 887 val _ = proof_progress ("current action:\n\n"^(term_to_string(a)^ "\n")) 888 val _ = (set_goal([], `` 889 preserve_relation_mmu ^a ^src_inv ^trg_inv ^uf_fun ^uy_fun``)) 890 val tac = FULL_SIMP_TAC (let_ss) [] THEN FULL_SIMP_TAC (srw_ss()) [] 891 val _ = e (tac) 892 val tac = FULL_SIMP_TAC (srw_ss()) 893 (List.drop(pthms,4)@(!simp_thms_list)) 894 val tac = foldl (fn (thm,tc) => tc THEN (MP_TAC thm)) (tac) 895 (List.drop(pthms,4)); 896 val tac = tac THEN RW_TAC (srw_ss()) []; 897 val _ = e (tac); 898 in 899 if (can top_thm()) 900 then 901 let val (proved_thm) = top_thm() 902 val _ = proofManagerLib.drop() 903 in 904 (proved_thm, tac) 905 end 906 else 907 let val _ = proofManagerLib.b() 908 val a' = get_action_from_goal (top_goal()); 909 val (flag,l ,r , opr) = decompose a' src_inv trg_inv uargs; 910 in 911 if (flag) 912 then 913 analyze_action (a' , l, r, opr,src_inv,trg_inv,uargs,pthms) 914 else 915 if (same_const opr ``UNCURRY``) 916 then 917 prove_abs_action (a',src_inv,trg_inv,uargs,pthms) 918 else 919 prove_simple_unproved_action (a', l,uargs,pthms) 920 end 921 end 922 | _ => (ASSUME ``T``, NO_TAC) 923 val () = simp_thms_list := ([proved_thm]@(!simp_thms_list)) 924 in 925 (proved_thm,tacs) 926 end 927 end; 928 929 930end 931