1structure ARM_prover_extLib :> ARM_prover_extLib = 2struct 3 4(*********************************************************************************) 5(* A Tool To Reason On ARM Model (privilaged mode constraints) *) 6(* Narges *) 7(*********************************************************************************) 8 9open Abbrev HolKernel boolLib bossLib Parse; 10open tacticsLib proofManagerLib arm_seq_monadTheory List; 11(*open arm_parserLib arm_encoderLib arm_disassemblerLib;*) 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 simplist = ref []; 20 21fun decompose_term a = 22 let val (opr, acs) = 23 case dest_term a of 24 (LAMB (b,c)) => 25 strip_comb c 26 | (* (COMB (b,c)) *) _ => 27 strip_comb a 28 in 29 if (length acs < 2) then 30 (opr,opr,opr) 31 else 32 let val l = List.nth(acs,0) 33 val r = List.nth(acs,1) 34 in 35 if (same_const opr (``$>>=``)) 36 then 37 let val (_,r_body) = pairLib.dest_pabs r 38 in 39 (l,r,r_body) 40 end 41 else 42 if (same_const opr ``$|||``) 43 then 44 (l,r,r) 45 else (opr,opr,opr) 46 end 47 end; 48 49(*******should be defined as local *************) 50val mk_spec_list = 51 fn a => 52 [``(SND (SND (SND (SND ^a)))):CP15sctlr``, 53 ``(FST (SND (SND (SND ^a)))):CP15scr``, 54 ``(FST (^a)):word32``, 55 ``(FST (SND (SND (^a)))):ARMpsr``, 56 ``FST (SND ^a):word32`` 57 ]; 58val mk_spec_list2 = 59 fn a => 60 [``(SND (SND (SND (SND ^a)))):CP15sctlr``, 61 ``(FST (SND (SND (SND (^a))))):CP15scr``, 62 ``(FST (SND (SND (^a)))):ARMpsr``, 63 ``FST (SND ^a):word32``, 64 ``(FST (^a)):word32`` 65 ]; 66 67val mk_spec_list3 = 68 fn a => 69 [``(SND (SND (SND (SND (SND ^a))))):CP15sctlr``, 70 ``(FST (SND (SND (SND (SND ^a))))):CP15scr``, 71 ``(FST (^a)):word32``, 72 ``(FST (SND (SND (^a)))):bool``, 73 ``(FST (SND (SND (SND (^a))))):ARMpsr``, 74 ``(FST (SND ^a)):word32`` 75 ]; 76 77val mk_spec_list4 = 78 fn a => 79 [``(SND (SND (SND (SND (SND ^a))))):CP15sctlr``, 80 ``(FST (SND (SND (SND (SND ^a))))):CP15scr``, 81 ``(FST (SND (SND (SND (^a))))):ARMpsr``, 82 ``(FST (SND (SND (^a)))):bool``, 83 ``(FST (SND ^a)):word32``, 84 ``(FST (^a)):word32`` 85 ]; 86 87 88fun mode_changing_comp_list_rec lst opr = case lst of 89 (x::rlst) => (same_const opr x) orelse mode_changing_comp_list_rec rlst opr 90 | _ => false; 91 92fun generate_uncurry_abs a = 93 case dest_term a of 94 (COMB (c,b)) => 95 if (same_const c ``UNCURRY``) then 96 let val (d,e) = 97 case dest_term b of 98 (LAMB(d,e)) => (d,e) 99 | _ => Raise not_matched_pattern 100 val (e_abs,e_trm) = generate_uncurry_abs e 101 in 102 (List.concat [[d],e_abs], e_trm) 103 end 104 else 105 ([], b) 106 | (LAMB(c,b)) => 107 ([c] , b) 108 | _ => ([], a); 109 110 111fun get_monad_type tp = 112 let val (str , fst , snd) = 113 case dest_type (tp) of 114 (str , [fst , snd]) => (str , fst , snd) 115 | _ => Raise not_matched_pattern 116 val (str , tp_type, b) = 117 case dest_type snd of 118 (str , [tp_type, b]) => (str , tp_type, b) 119 | _ => Raise not_matched_pattern 120 in 121 tp_type 122 end; 123fun generate_uncurry_abs_from_abs a = 124 case dest_term a of 125 (LAMB (d,e)) => 126 let val (e_abs,e_trm) = generate_uncurry_abs_from_abs e 127 in 128 (List.concat [[d],e_abs], e_trm) 129 end 130 | _ => 131 ([] , a) ; 132 133fun get_action_from_goal g = 134 let val (asm ,con) = g 135 val (c1,d1) = strip_comb con 136 (* val (c2,d2) = strip_comb (List.nth(d1,1)) *) 137 (* val (b,c) = if (is_comb (List.nth(d1,0))) *) 138 (* then *) 139 (* strip_comb (List.nth(d1,0)) *) 140 (* else *) 141 (* strip_comb (List.nth(d1,0)) *) 142 in 143 List.nth(d1,0) 144 end 145 146fun prove_simple_action opr a expr postfix = 147 let 148 149 val thrm = SPEC (List.nth(expr,0)) (DB.fetch (current_theory()) ((Hol_pp.term_to_string (opr)) ^ postfix)) 150 151 val _ = proof_progress ("\nTheorem " ^ (term_to_string opr) ^ postfix ^"thm is applied!\n ") 152 153 val tacs = RW_TAC (srw_ss()) [thrm] THEN 154 (ASSUME_TAC thrm THEN 155 UNDISCH_ALL_TAC THEN 156 RW_TAC (srw_ss()) []) 157 158 val _ = e (tacs) 159 val proved_a = top_thm() 160 val _ = proofManagerLib.drop() 161 162 val _ = proof_progress ("\nProof of theorem: " ^ (term_to_string a) ^ " is completed!\n ") 163 in 164 (proved_a , tacs) 165 end; 166 167 168fun exists_theorem thy x = 169 let val thms = theorems thy 170 val thm = List.find (fn (s,t) => (s=x)) thms 171 in 172 case thm of 173 SOME (p,q) => true 174 | NONE => false 175 end; 176 177fun find_theorem x = 178 let val _ = proof_progress ("Searching for the theorem " ^ (x) ^ "\n") 179 val db_x = DB.find x 180 val res = List.find (fn ((s,t),p) => (t=x)) db_x in 181 case res of 182 SOME ((s,t),(p,q)) => 183 let val _ = proof_progress ("The theorem " ^ x ^ " was found\n ") in 184 p 185 end 186 |NONE => 187 let val _ = proof_progress ("The theorem " ^ x ^ " was not found\n ") in 188 ASSUME ``T`` 189 end 190 end; 191 192 193fun decompose a postfix = 194 let val (opr, acs) = 195 case dest_term a of 196 (LAMB (b,c)) => 197 strip_comb c 198 | (* (COMB (b,c)) *) _ => 199 strip_comb a 200 201 val thm_exists = (* if (* ((* !global_mode = ``16w:bool[5]`` andalso *)(term_eq src_inv trg_inv)) orelse *) *) 202 (* ((same_const opr ``write_cpsr``) ) *) 203 (* then *) 204 exists_theorem (current_theory()) (term_to_string opr ^ postfix ) 205 (* else *) 206 (* exists_theorem (current_theory()) (term_to_string opr ^ "_comb" ^ postfix) *) 207 208 val flag = ((same_const opr ``$>>=``) orelse 209 (same_const opr ``$|||``) orelse 210 (same_const opr ``constT``) orelse 211 (same_const opr ``COND``) orelse 212 (same_const opr ``condT``) orelse 213 (same_const opr ``forT``) orelse 214 (TypeBase.is_case a ) orelse 215 thm_exists) 216 in 217 if (length acs < 2) then 218 (flag,opr,opr,opr) 219 else 220 let val l = List.nth(acs,0) 221 val r = List.nth(acs,1) 222 in 223 if (same_const opr (``$>>=``)) 224 then (flag,l,r,opr) 225 else 226 if (same_const opr ``$|||``) then 227 (flag,l,r,opr) 228 else (flag,opr,opr,opr) 229 end 230 end; 231 232 233(*TODO: use some sort of pattern mathiching instead of list lenght!!!*) 234fun get_uncurried_theorem thm l = 235 let val (asm,con) = dest_thm thm 236 in 237 if( l = 1) 238 then 239 thm 240 else 241 let 242 val con = concl thm 243 val res_thm1 = PairRules.SWAP_PFORALL_CONV con 244 val res_thm2 = REWRITE_RULE [res_thm1] thm 245 val con1 = concl res_thm1 246 val (a,b) = dest_eq con1 247 val res_thm3 = PairRules.UNCURRY_FORALL_CONV b 248 val res_thm = REWRITE_RULE [res_thm3] res_thm2 249 in 250 get_uncurried_theorem res_thm (l-1) 251 end 252 end; 253 254fun generalize_theorem thm a = 255 let 256 val (a_abs,a_body) = pairLib.dest_pabs a 257 val (abs_args, abs_body) = generate_uncurry_abs a 258 val generalized_curried_thm = PairRules.PGENL (List.rev(abs_args)) thm 259 val generalized_uncurried_thm = 260 get_uncurried_theorem generalized_curried_thm (List.length(abs_args)) 261 val abs_type = type_of a_abs 262 val gen_var = (mk_var("y", abs_type)) 263 val spec_thm= PairRules.PSPEC gen_var generalized_uncurried_thm 264 val generalized_thm = GEN gen_var spec_thm 265 in 266 generalized_thm 267 end; 268 269(* for types of form k->pM, if i=true then returns k otherwise p*) 270val get_type_inst = 271 fn (t, i) => 272 case dest_type (t) of 273 (str , [fst , snd]) => 274 if(i) 275 then 276 fst 277 else 278 snd 279 |_ => Raise not_matched_pattern; 280 281 282 283fun prove_const a pred expr cm postfix thms = 284 let 285 286 val prove_COND_action = 287 fn (if_part,else_part,condition,a,pred,expr,cm,postfix,thms) => 288 let val _ = proof_progress ("A Conditional action\n\n\n") 289 290 val (if_part_thm,tc) = prove_const if_part pred expr cm postfix thms; 291 val (else_part_thm,tc') = prove_const else_part pred expr cm postfix thms; 292 val tacs = (ASSUME_TAC if_part_thm) 293 THEN (ASSUME_TAC else_part_thm) 294 THEN (IF_CASES_TAC ) 295 THEN (FULL_SIMP_TAC (srw_ss()) []) 296 THEN (FULL_SIMP_TAC (srw_ss()) []) 297 val _ = e (tacs) 298 val proved_b = top_thm() 299 val _ = proofManagerLib.drop() 300 in 301 (proved_b, tacs) 302 end 303 304 305 val prove_composite_action = 306 fn (l, r, opr, a,pred,expr, cm,postfix,thms) => 307 let val _ = proof_progress ("\n\nProof of the compositional action:\n"^(term_to_string a)^"\n\n") 308 (* val (left_hand_thm , tc) = prove l pred expr cm postfix *) 309 (* val tacs = (ASSUME_TAC left_hand_thm) *) 310 (* val _ = e (tacs) *) 311 312 (* proof of the right part*) 313 314 315 (* combining the left and right parts *) 316 val l_type = get_monad_type(type_of(l)); 317 val snd = type_of(r); 318 319 val (part , comb_thm) = 320 if (same_const opr ``$>>=``) 321 then 322 let 323 val (_,r_body) = pairLib.dest_pabs r 324 val (_,_,_,oprr) = decompose r_body ""; 325 in 326 if (same_const oprr ``constT``) 327 then 328 (l , SPECL [l,List.nth(expr,0)] 329 (List.nth(thms, 6))) 330 else 331 (r , SPECL [ r, l, List.nth(expr,0)] 332 (INST_TYPE [alpha |-> l_type, 333 beta |-> get_monad_type(get_type_inst(snd , false))] 334 (List.nth(thms, 1)))) 335 end 336 else 337 (r , SPECL [ r,l, List.nth(expr,0)] 338 (INST_TYPE [alpha |-> get_monad_type(snd), 339 beta |-> l_type] 340 (List.nth(thms, 2)))) 341 val (right_hand_thm, tc) = prove_const part pred expr cm postfix thms 342 val tacsb = 343 ASSUME_TAC right_hand_thm 344 THEN ASSUME_TAC comb_thm 345 (* THEN ASSUME_TAC (SPEC l (INST_TYPE [alpha |-> ``:arm_state``, 346 beta |-> l_type] 347 no_access_violation_thm)) 348 *) THEN RES_TAC 349 THEN (RW_TAC (srw_ss()) []) 350 val _ = e (tacsb) 351 val thrm = top_thm() 352 val _ = proofManagerLib.drop() 353 in 354 (thrm,tacsb) 355 end; 356 357 358 val prove_constT_action = 359 fn (a,src_inv, trg_inv) => 360 let 361 val (opr, arg) = 362 case dest_term a of 363 COMB (opr, arg) => (opr, arg) 364 |_ => Raise not_matched_pattern 365 val tac = RW_TAC (srw_ss()) 366 [] 367 val _ = e (tac) 368 val proved_thm = top_thm() 369 val _ = proofManagerLib.drop() 370 in 371 (proved_thm, tac) 372 end 373 374 val prove_condT_action = 375 fn (a, pred, expr, cm, postfix,thms) => 376 let val (opr, acs) = strip_comb a 377 val (arg_thm,tc) = prove_const (List.nth(acs,1)) pred expr cm postfix thms 378 val tacs = ASSUME_TAC arg_thm 379 THEN RW_TAC (srw_ss()) [List.nth(thms, 3)] 380 val _ = e (tacs) 381 val proved_thm = top_thm() 382 val _ = proofManagerLib.drop() 383 in 384 (proved_thm,tc) 385 end 386 (*thms*) 387 388 val prove_case_body = 389 fn (opt,body,flag,pred, expr, cm, postfix,thms) => 390 let val (body_thm,body_tac) = prove_const body pred expr cm postfix thms 391 val tacs = if (flag) then 392 CASE_TAC 393 THEN FULL_SIMP_TAC (srw_ss()) [] 394 THEN1 (ASSUME_TAC body_thm 395 THEN FULL_SIMP_TAC (srw_ss()) [List.nth(thms, 0)] 396 THEN (FULL_SIMP_TAC (srw_ss()) [])) 397 else 398 (ASSUME_TAC body_thm 399 THEN FULL_SIMP_TAC (srw_ss()) [List.nth(thms, 0)] 400 THEN (FULL_SIMP_TAC (srw_ss()) [])) 401 val _ = e (tacs) 402 in 403 (body_thm, tacs) 404 end 405 406 val analyze_action = 407 fn (a, l , r, opr,pred,expr,cm,postfix,thms) => 408 if ((same_const opr ``$>>=``) orelse 409 (same_const opr ``$|||``)) 410 then 411 prove_composite_action (l, r, opr ,a, pred, expr,cm,postfix,thms) 412 else 413 let val _ = proof_progress ("\n\nProof of a simple action:\n "^(term_to_string l)^"\n\n") 414 415 val thm_exist = ((exists_theorem (current_theory()) (term_to_string l ^ postfix))) in 416 (* if (thm_exist) *) 417 (* then *) 418 prove_simple_action l a expr postfix 419 (* else *) 420 (* prove_condT_action (a,pred,expr,cm) *) 421 end 422 val prove_abs_action = 423 fn (a, pred ,expr ,cm ,postfix ,thms) => 424 let 425 val (a_abs,a_body) = pairLib.dest_pabs a; 426 val _ = List.nth(pred,1) a expr 427 428 val _ = e (FULL_SIMP_TAC (let_ss) []) (*change of Oliver*) 429 val (proved_a,b) = prove_const a_body pred expr cm postfix thms 430 431 val unbeta_thm= (PairRules.UNPBETA_CONV a_abs a_body) 432 val unbeta_a = mk_comb (a, a_abs) 433 (*val (str , [fst , snd]) = dest_type (type_of a_body) *) 434 (* val (str , [a_body_type, b]) = dest_type snd;*) 435 val snd = get_type_inst (type_of(a_body) , false) 436 val a_body_type = get_type_inst (snd, true) 437 val expr_elm = List.nth(expr,0) 438 439 val proved_unbeta_lemma = prove(``(priv_cpsr_flags_constraints ^a_body ^expr_elm)= 440 (priv_cpsr_flags_constraints ^unbeta_a ^expr_elm)``, 441 (ASSUME_TAC (SPECL [a_body,``^unbeta_a``, expr_elm] 442 (INST_TYPE [beta |-> a_body_type, 443 alpha |-> ``:arm_state``] 444 (List.nth(thms,3))))) 445 THEN ASSUME_TAC unbeta_thm 446 THEN RES_TAC) 447 448 val proved_preserve_unbeta_a = 449 store_thm ("proved_preserve_unbeta_a", 450 `` ( priv_cpsr_flags_constraints ^unbeta_a ^expr_elm)``, 451 (ASSUME_TAC (proved_unbeta_lemma)) 452 THEN (ASSUME_TAC proved_a) 453 THEN (FULL_SIMP_TAC (srw_ss()) [])) 454 455 val abs_type = type_of a_abs 456 val (abs_args, abs_body) = generate_uncurry_abs a 457 val tacs = (ASSUME_TAC proved_preserve_unbeta_a) 458 val gen_preserve_unbeta_thm = generalize_theorem proved_preserve_unbeta_a a 459 val tacs = tacs THEN (ASSUME_TAC gen_preserve_unbeta_thm) 460 THEN (ASSUME_TAC ( 461 SPECL[a, List.nth(expr,0)] 462 (INST_TYPE [alpha |-> abs_type, 463 beta |-> ``:arm_state``, 464 gamma |-> a_body_type] 465 (List.nth(thms,4))))) 466 THEN (RW_TAC (srw_ss()) []) 467 THEN (FULL_SIMP_TAC (srw_ss()) []) 468 THEN (UNDISCH_ALL_TAC THEN 469 (RW_TAC (srw_ss()) []) 470 THEN (FULL_SIMP_TAC (srw_ss()) [])) 471 val _ = e (tacs) 472 val proved_thm = top_thm() 473 val _ = proofManagerLib.drop() 474 in 475 (proved_thm,tacs) 476 end 477 478 val prove_simple_unproved_action = 479 fn (a, opr,cm ) => 480 let val a_name = opr 481 val _ = if !Globals.interactive then 482 TextIO.print ("Do you have a theorem to prove " ^ (term_to_string (a)) ^ " theorem? \n\n") 483 else () 484 (* val resp = valOf (TextIO.inputLine TextIO.stdIn) *) 485 in 486 if (same_const opr ``readT``) 487 then 488 let val tac = RW_TAC (srw_ss()) 489 [] 490 THEN FULL_SIMP_TAC (srw_ss()) [readT_def] 491 THEN PAT_X_ASSUM ``���ii reg.X`` (fn thm => ASSUME_TAC (SPECL [``<|proc:=0|>``] thm)) 492 THEN FULL_SIMP_TAC (srw_ss()) [readT_def] THEN (REPEAT (RW_TAC (srw_ss()) [])) 493 494 val _ = e (tac) 495 val (proved_thm) = top_thm() 496 val _ = proofManagerLib.drop() 497 in 498 (proved_thm, tac) 499 end 500 else 501 502 let (* val _ = (set_goal([], ``preserve_relation ^a``)) *) 503 val simp_thm = find_theorem ((term_to_string (opr))^"_def") 504 val tacs = (FULL_SIMP_TAC (srw_ss()) [simp_thm,writeT_def]) 505 val _ = e (tacs) 506 val (asm,con) = top_goal() 507 val a' = get_action_from_goal (top_goal()) 508 val (flag,l ,r , opr) = decompose a' postfix; 509 val (proved_a, tacb) = 510 if (flag) 511 then 512 analyze_action (a', l, r, opr,pred,expr,cm,postfix,thms) 513 else 514 let 515 val (next_proof , next_tac) = prove_const a' pred expr cm postfix thms 516 val tac = RW_TAC (srw_ss()) [next_proof] 517 val _ = e (tac) 518 val (proved_thm) = top_thm() 519 val _ = proofManagerLib.drop() 520 in 521 (proved_thm, tac) 522 end 523 val tacs = tacs THEN tacb 524 (* val _ = save_proof a_name a (tacs) *) 525 in 526 (proved_a, tacs) 527 end 528 end 529 in 530 case dest_term a of 531 (LAMB (c,b)) => 532 prove_abs_action (a, pred ,expr ,cm ,postfix ,thms) 533 | COMB (c,b) => 534 if (same_const c ``UNCURRY``) 535 then 536 prove_abs_action (a, pred ,expr ,cm ,postfix ,thms) 537 else 538 let val _ = proof_progress ("current action:\n\n"^(term_to_string(a)^ "\n")) 539 val _ = List.nth(pred,0) a expr 540 val tac = FULL_SIMP_TAC (let_ss) [] 541 THEN FULL_SIMP_TAC (srw_ss()) [List.nth(thms,5)] 542 THEN TRY (ASSUME_TAC (List.nth(thms,5)) 543 THEN FULL_SIMP_TAC (srw_ss()) []) 544 val _ = e (tac) 545 in 546 if (can top_thm()) 547 then 548 let val (proved_thm) = top_thm() 549 val _ = proofManagerLib.drop() 550 in 551 (proved_thm, tac) 552 end 553 else 554 let val _ = proofManagerLib.b() 555 val a' = get_action_from_goal (top_goal()); 556 val (flag,l ,r , opr) = decompose a' postfix; 557 in 558 if (flag) 559 then 560 analyze_action (a' , l, r, opr,pred,expr,cm,postfix,thms) 561 else 562 (* if (same_const opr ``UNCURRY``) *) 563 (* then *) 564 (* prove_abs_action (a',pred,expr,cm) *) 565 (* else *) 566 prove_simple_unproved_action (a',l,cm) 567 end 568 end 569 | _ => (ASSUME ``T``, NO_TAC) 570 end; 571fun get_first_cpc_lemmma abody expr_elm unbeta_a unbeta_thm thms = 572 let val snd = get_type_inst (type_of(abody) , false) 573 val abody_type = get_type_inst (snd, true) 574 val proved_unbeta_lemma = 575 prove (``(priv_cpsr_flags_constraints ^abody ^expr_elm)= 576 (priv_cpsr_flags_constraints ^unbeta_a ^expr_elm)``, 577 (ASSUME_TAC (SPECL [abody,``^unbeta_a``, expr_elm] 578 (INST_TYPE [beta |-> abody_type, 579 alpha |-> ``:arm_state``] 580 (List.nth(thms,3))))) 581 THEN ASSUME_TAC unbeta_thm 582 THEN RES_TAC) 583 in 584 proved_unbeta_lemma 585 end; 586 587 588fun get_second_lemmma proved_a expr_elm unbeta_a proved_unbeta_lemma = 589 store_thm ("proved_preserve_unbeta_a", 590 `` ( priv_cpsr_flags_constraints ^unbeta_a ^expr_elm)``, 591 (ASSUME_TAC (proved_unbeta_lemma)) 592 THEN (ASSUME_TAC proved_a) 593 THEN (FULL_SIMP_TAC (srw_ss()) [])); 594 595 596fun get_first_spc_lemma abody expr unbeta_a unbeta_thm thms = 597 let val snd = get_type_inst (type_of(abody) , false) 598 val mode = List.nth(expr,0) 599 val bvt = List.nth(expr,1) 600 val abody_type = get_type_inst (snd, true) 601 val proved_unbeta_lemma = 602 prove (``(set_pc_to ^abody ^mode ^bvt)= 603 (set_pc_to ^unbeta_a ^mode ^bvt)``, 604 (ASSUME_TAC (SPECL [abody,``^unbeta_a``, mode] 605 (INST_TYPE [beta |-> abody_type, 606 alpha |-> ``:arm_state``] 607 (List.nth(thms,3))))) 608 THEN ASSUME_TAC unbeta_thm 609 THEN RES_TAC) 610 in 611 proved_unbeta_lemma 612 end; 613 614 615fun get_second_spc_lemma proved_a expr unbeta_a proved_unbeta_lemma = 616 let val mode = List.nth(expr,0) 617 val bvt = List.nth(expr,1) 618 in 619 store_thm ("proved_preserve_unbeta_a", 620 `` (set_pc_to ^unbeta_a ^mode ^bvt)``, 621 (ASSUME_TAC (proved_unbeta_lemma)) 622 THEN (ASSUME_TAC proved_a) 623 THEN (FULL_SIMP_TAC (srw_ss()) [])) 624 end; 625 626 fun prove_abs_action (a, pred ,expr ,proved_a,thms, unbetaf1, unbetaf2) = 627 let 628 val (a_abs,a_body) = pairLib.dest_pabs a; 629 val _ = List.nth(pred,1) a expr 630 631 val _ = e (FULL_SIMP_TAC (let_ss) []) (*change of Oliver*) 632 633 val unbeta_thm= (PairRules.UNPBETA_CONV a_abs a_body) 634 val unbeta_a = mk_comb (a, a_abs) 635 (*val (str , [fst , snd]) = dest_type (type_of a_body) *) 636 (* val (str , [a_body_type, b]) = dest_type snd;*) 637 val snd = get_type_inst (type_of(a_body) , false) 638 val a_body_type = get_type_inst (snd, true) 639 val expr_elm = List.nth(expr,0) 640 641 val proved_unbeta_lemma = unbetaf1 a_body expr unbeta_a unbeta_thm thms 642 643 val proved_preserve_unbeta_a = unbetaf2 proved_a expr unbeta_a proved_unbeta_lemma 644 645 val abs_type = type_of a_abs 646 val (abs_args, abs_body) = generate_uncurry_abs a 647 val tacs = ASSUME_TAC proved_preserve_unbeta_a 648 val gen_preserve_unbeta_thm = generalize_theorem proved_preserve_unbeta_a a 649 val tacs = tacs THEN (ASSUME_TAC gen_preserve_unbeta_thm) 650 THEN (ASSUME_TAC ( 651 SPECL[a, List.nth(expr,0)] 652 (INST_TYPE [alpha |-> abs_type, 653 beta |-> ``:arm_state``, 654 gamma |-> a_body_type] 655 (List.nth(thms,4))))) 656 THEN (RW_TAC (srw_ss()) []) 657 THEN (FULL_SIMP_TAC (srw_ss()) []) 658 THEN (UNDISCH_ALL_TAC THEN 659 (RW_TAC (srw_ss()) []) 660 THEN (FULL_SIMP_TAC (srw_ss()) [])) 661 val _ = e (tacs) 662 val proved_thm = top_thm() 663 val _ = proofManagerLib.drop() 664 in 665 (proved_thm,tacs) 666 end 667end 668