1structure stateLib :> stateLib = 2struct 3 4open HolKernel boolLib bossLib 5open updateLib utilsLib 6open stateTheory temporal_stateTheory 7open helperLib progSyntax temporalSyntax temporal_stateSyntax 8 9structure Parse = struct 10 open Parse 11 val (Type, Term) = 12 parse_from_grammars temporal_stateTheory.temporal_state_grammars 13end 14open Parse 15 16val ERR = Feedback.mk_HOL_ERR "stateLib" 17 18(* ------------------------------------------------------------------------ *) 19 20(* Versions of operations in helperLib that are generalise to cover 21 TEMPORAL_NEXT as well as SPEC *) 22 23fun SPECC_FRAME_RULE frame th = 24 Thm.SPEC frame 25 (Drule.MATCH_MP progTheory.SPEC_FRAME th 26 handle HOL_ERR _ => 27 Drule.MATCH_MP temporal_stateTheory.TEMPORAL_NEXT_FRAME th) 28 29fun SPECL_FRAME_RULE l th = 30 let 31 val p = temporal_stateSyntax.dest_pre' (Thm.concl th) 32 val xs = progSyntax.strip_star p 33 val lx = 34 List.filter 35 (fn t => not (Lib.exists (Lib.can (Term.match_term t)) xs)) l 36 in 37 List.foldl (Lib.uncurry SPECC_FRAME_RULE) th lx 38 end 39 40val MOVE_COND_CONV = 41 Conv.REWR_CONV (GSYM progTheory.SPEC_MOVE_COND) 42 ORELSEC Conv.REWR_CONV (GSYM temporal_stateTheory.TEMPORAL_NEXT_MOVE_COND) 43 44local 45 val cond_T = Q.prove ( 46 `!p : 'a set set. (set_sep$cond T * p = p) /\ (p * set_sep$cond T = p)`, 47 REWRITE_TAC [set_sepTheory.SEP_CLAUSES]) 48 val rule1 = 49 helperLib.PRE_POST_RULE (REWRITE_CONV [cond_T]) o 50 Conv.CONV_RULE MOVE_COND_CONV 51 fun COND_RW_CONV atm = 52 let 53 val cnv = Conv.RAND_CONV (PURE_REWRITE_CONV [ASSUME atm]) 54 in 55 fn tm => if progSyntax.is_cond tm then cnv tm else NO_CONV tm 56 end 57in 58 fun MOVE_COND_RULE tm thm = 59 let 60 val thm1 = Conv.CONV_RULE (Conv.DEPTH_CONV (COND_RW_CONV tm)) thm 61 in 62 case Thm.hyp thm1 of 63 [t] => if t = tm then rule1 (Thm.DISCH t thm1) else thm 64 | _ => thm 65 end 66end 67 68fun PRE_COND_CONV cnv = 69 helperLib.PRE_CONV 70 (Conv.ONCE_DEPTH_CONV 71 (fn tm => if progSyntax.is_cond tm 72 then Conv.RAND_CONV cnv tm 73 else raise ERR "PRE_COND_CONV" "") 74 THENC PURE_ONCE_REWRITE_CONV [stateTheory.cond_true_elim]) 75 76(* Some syntax functions *) 77 78fun mk_state_pred x = 79 pred_setSyntax.mk_set [pred_setSyntax.mk_set [pairSyntax.mk_pair x]] 80 81(* ------------------------------------------------------------------------ 82 update_frame_state_thm: Generate theorem with conjuncts of the form 83 84 !a w s x. 85 f a IN x ==> (FRAME_STATE m x (u s a w) = FRAME_STATE m x (r s)) 86 87 where "m" is a projection map and "u" is a state update function. 88 ------------------------------------------------------------------------ *) 89 90local 91 val concat_ = String.concat o Lib.separate "_" 92 val dom_of = utilsLib.dom o Term.type_of 93 val rng_of = utilsLib.rng o Term.type_of 94 val ty_name = #Tyop o Type.dest_thy_type o Term.type_of 95in 96 fun update_frame_state_thm proj_def = 97 let 98 val tac = 99 Cases THEN SRW_TAC [] [proj_def, combinTheory.APPLY_UPDATE_THM] 100 val proj = utilsLib.get_function proj_def 101 val th = Drule.ISPEC proj stateTheory.UPDATE_FRAME_STATE 102 val {Thy = p_thy, Name = n, Ty = ty, ...} = Term.dest_thy_const proj 103 val isa = if String.isSuffix "_proj" n 104 then String.extract (n, 0, SOME (String.size n - 5)) 105 else raise ERR "update_frame_state_thm" 106 "unexpected proj name" 107 val state_ty = fst (Type.dom_rng ty) 108 val {Thy = thy, ...} = Type.dest_thy_type state_ty 109 val s = Term.mk_var ("s", state_ty) 110 fun frame_state_thm component = 111 let 112 val l = String.tokens (Lib.equal #".") component 113 val c_name = concat_ (isa :: "c" :: l) 114 val c = Term.prim_mk_const {Name = c_name, Thy = p_thy} 115 val (f, aty, not_map) = 116 case Lib.total dom_of c of 117 SOME ty => (c, ty, false) 118 | NONE => 119 (combinSyntax.mk_K_1 (c, Type.alpha), Type.alpha, true) 120 val a = Term.mk_var ("a", aty) 121 val w = ref boolSyntax.T 122 fun iter rest tm = 123 fn [] => if rest 124 then tm 125 else if not_map 126 then (w := Term.mk_var ("w", Term.type_of tm); !w) 127 else ( w := Term.mk_var ("w", rng_of tm) 128 ; Term.mk_comb 129 (combinSyntax.mk_update (a, !w), tm) 130 ) 131 | h :: t => 132 let 133 val fupd_name = concat_ [ty_name tm, h, "fupd"] 134 val fupd = 135 Term.prim_mk_const {Name = fupd_name, Thy = thy} 136 val d = utilsLib.dom (dom_of fupd) 137 val v = Term.mk_var (utilsLib.lowercase h, d) 138 in 139 Term.list_mk_comb 140 (fupd, [combinSyntax.mk_K_1 (iter rest v t, d), tm]) 141 end 142 val u = iter false s l 143 val u = Term.list_mk_abs ([s, a, !w], u) 144 val l = if not_map then Lib.butlast l else l 145 val r = Term.mk_abs (s, iter true s l) 146 val thm = th |> Drule.ISPECL [f, u, r] |> SIMP_RULE (srw_ss()) [] 147 val p = fst (boolSyntax.dest_imp (Thm.concl thm)) 148 val p_thm = Tactical.prove (p, tac) 149 in 150 Drule.GEN_ALL (MATCH_MP thm p_thm) 151 end 152 in 153 Drule.LIST_CONJ o List.map frame_state_thm 154 end 155end 156 157(* ------------------------------------------------------------------------ 158 update_hidden_frame_state_thm: Generate theorem with conjuncts of the form 159 160 !x y s. (FRAME_STATE m x (s with ? := x) = FRAME_STATE m x s) 161 162 where "m" is a projection map. 163 ------------------------------------------------------------------------ *) 164 165local 166 val tac = 167 NTAC 2 STRIP_TAC 168 THEN REWRITE_TAC [stateTheory.FRAME_STATE_def, stateTheory.STATE_def, 169 stateTheory.SELECT_STATE_def, set_sepTheory.fun2set_def] 170 THEN SRW_TAC [] [pred_setTheory.EXTENSION, pred_setTheory.GSPECIFICATION] 171 THEN EQ_TAC 172 THEN STRIP_TAC 173 THEN Q.EXISTS_TAC `a` 174 THEN Cases_on `a` 175 fun prove_hidden thm u = 176 let 177 val p = utilsLib.get_function thm 178 val t = tac THEN FULL_SIMP_TAC (srw_ss()) [thm] 179 in 180 Drule.GEN_ALL 181 (Q.prove (`!y s. FRAME_STATE ^p y ^u = FRAME_STATE ^p y s`, t)) 182 end 183in 184 fun update_hidden_frame_state_thm proj_def = 185 utilsLib.map_conv (prove_hidden proj_def) 186end 187 188(* ------------------------------------------------------------------------ 189 star_select_state_thm: Generate theorems of the form 190 191 !cd m p s x. 192 ({cd} * p) (SELECT_STATE m x s) = 193 (!c d. (c, d) IN cd ==> (m s c = d)) /\ IMAGE FST cd SUBSET x /\ 194 p (SELECT_STATE m (x DIFF IMAGE FST cd) s) 195 196 pool_select_state_thm: Generate theorems of the form 197 198 !cd m p s x. 199 {cd} (SELECT_STATE m x s) = 200 (!c d. (c, d) IN cd ==> (m s c = d)) /\ IMAGE FST cd SUBSET x /\ 201 (x DIFF IMAGE FST cd = {}) 202 203 ------------------------------------------------------------------------ *) 204 205local 206 val EXPAND_lem = Q.prove( 207 `!x:'a # 'b y m s:'c c:'d. 208 (!c d. (c, d) IN set (x :: y) ==> (m s c = d)) = 209 (!c d. ((c, d) = x) ==> (m s c = d)) /\ 210 (!c d. ((c, d) IN set y) ==> (m s c = d))`, 211 SRW_TAC [] [] \\ utilsLib.qm_tac []) 212 val EXPAND_lem2 = Q.prove( 213 `!x:'a # 'b y m s:'c c:'d. 214 (!c d. (c, d) IN x INSERT y ==> (m s c = d)) = 215 (!c d. ((c, d) = x) ==> (m s c = d)) /\ 216 (!c d. ((c, d) IN y) ==> (m s c = d))`, 217 SRW_TAC [] [] \\ utilsLib.qm_tac []) 218 val emp_thm = 219 set_sepTheory.SEP_CLAUSES 220 |> Drule.SPEC_ALL 221 |> Drule.CONJUNCTS 222 |> List.last 223in 224 fun star_select_state_thm proj_def thms (l, thm) = 225 let 226 val proj_tm = utilsLib.get_function proj_def 227 val tm = thm |> Thm.concl |> boolSyntax.strip_forall |> snd 228 |> boolSyntax.rhs |> pred_setSyntax.strip_set |> List.hd 229 val tm_thm = (REWRITE_CONV thms THENC Conv.CHANGED_CONV EVAL) tm 230 handle HOL_ERR {origin_function = "CHANGED_CONV", ...} => 231 combinTheory.I_THM 232 in 233 STAR_SELECT_STATE 234 |> Drule.ISPECL ([tm, proj_tm] @ l) 235 |> Conv.CONV_RULE (Conv.STRIP_QUANT_CONV 236 (Conv.FORK_CONV 237 (REWRITE_CONV [GSYM thm, emp_thm], 238 REWRITE_CONV [tm_thm, EXPAND_lem, EXPAND_lem2] 239 THENC SIMP_CONV (srw_ss()) [proj_def, emp_SELECT_STATE]))) 240 |> Drule.GEN_ALL 241 end 242 fun pool_select_state_thm proj_def thms instr_def = 243 let 244 val tm = utilsLib.get_function proj_def 245 val ty = utilsLib.rng (Term.type_of tm) 246 val ty = 247 (pairSyntax.mk_prod (Type.dom_rng ty) --> Type.bool) --> Type.bool 248 val emp = Term.mk_const ("emp", ty) 249 in 250 star_select_state_thm proj_def thms ([emp], instr_def) 251 end 252end 253 254(* ------------------------------------------------------------------------ 255 sep_definitions sthy expnd thm 256 257 Generate a state component map for a given next state function, where 258 259 sthy: name of model (used as a prefix tag), e.g. "x86" 260 expnd: specifies which record components should be expanded 261 (be given separate component names). For example, [["CPSR"]] 262 thm: the next state function 263 ------------------------------------------------------------------------ *) 264 265local 266 fun def_suffix s = s ^ "_def" 267 268 val comp_names = 269 List.map (def_suffix o fst o Term.dest_const o utilsLib.get_function) 270 271 fun mk_state_var ty = Term.mk_var ("s", ty) 272 273 fun make_component_name sthy = 274 String.concat o Lib.cons (sthy ^ "_c_") o Lib.separate "_" o List.rev 275 276 fun make_assert_name sthy tm = 277 sthy ^ String.extract (fst (Term.dest_const tm), 278 String.size sthy + 2, NONE) 279 280 fun component (n, ty) = 281 let 282 val (a, r) = HolKernel.strip_fun ty 283 in 284 ((n, List.map ParseDatatype.dAQ a), r) 285 end 286 287 fun build_names (sthy, expnd, hide, state_ty) = 288 let 289 val s = mk_state_var state_ty 290 fun loop (x as ((path, ty), tm), es, hs) = 291 case Lib.total TypeBase.fields_of ty of 292 NONE => [x] 293 | SOME [] => [x] 294 | SOME l => 295 let 296 val l = ListPair.zip (l, utilsLib.accessor_fns ty) 297 fun process n = 298 List.map List.tl o 299 List.filter (Lib.equal (SOME n) o Lib.total List.hd) 300 val (nd, dn) = 301 List.foldl 302 (fn ((x as ((n, t), f)), (nd, dn)) => 303 let 304 val hs' = process n hs 305 val es' = process n es 306 val ahide = Lib.mem [] hs' 307 val y = ((n :: path, t), Term.mk_comb (f, tm)) 308 in 309 if List.null es' 310 then (nd, if ahide then dn else y :: dn) 311 else ((y, es', hs') :: nd, dn) 312 end) ([], []) l 313 in 314 dn @ List.concat (List.map loop nd) 315 end 316 val (l1, tms) = 317 ListPair.unzip (loop ((([], state_ty), s), expnd, hide)) 318 val (components, data) = 319 ListPair.unzip 320 (List.map (component o (make_component_name sthy ## Lib.I)) l1) 321 in 322 (components, Lib.mk_set data, tms) 323 end 324 325 fun data_constructor ty = 326 case Type.dest_thy_type ty of 327 {Thy = "fcp", Args = [_, n], Tyop = "cart"} => 328 "word" ^ Arbnum.toString (fcpSyntax.dest_numeric_type n) 329 | {Thy = "min", Args = [_, b], Tyop = "fun"} => 330 data_constructor b 331 | {Thy = "pair", Args = [a, b], Tyop = "prod"} => 332 data_constructor a ^ "_X_" ^ data_constructor b 333 | {Thy = "option", Args = [a], Tyop = "option"} => 334 data_constructor a ^ "_option" 335 | {Thy = "list", Args = [a], Tyop = "list"} => 336 data_constructor a ^ "_list" 337 | {Args = [], Tyop = s, ...} => s 338 | _ => raise ERR "data_constructor" "incompatible type" 339 340 fun define_assert0 sthy pred_ty (tm1, tm2) = 341 let 342 val dty = utilsLib.dom (Term.type_of tm2) 343 val d = Term.mk_var ("d", dty) 344 val tm_d = Term.mk_comb (tm2, d) 345 val s = make_assert_name sthy tm1 346 val l = Term.mk_comb (Term.mk_var (s, dty --> pred_ty), d) 347 val r = mk_state_pred (tm1, tm_d) 348 in 349 Definition.new_definition (def_suffix s, boolSyntax.mk_eq (l, r)) 350 end 351 352 fun define_assert1 sthy pred_ty (tm1, tm2, vs) = 353 let 354 val cs = 355 case vs of 356 [v] => [Term.mk_var ("c", Term.type_of v)] 357 | l => List.tabulate 358 (List.length vs, 359 fn i => Term.mk_var ("c" ^ Int.toString i, 360 Term.type_of (List.nth (vs, i)))) 361 val tm1 = Term.subst (List.map (op |->) (ListPair.zip (vs, cs))) tm1 362 val dty = utilsLib.dom (Term.type_of tm2) 363 val d = Term.mk_var ("d", dty) 364 val tm_d = Term.mk_comb (tm2, d) 365 val s = make_assert_name sthy (fst (boolSyntax.strip_comb tm1)) 366 val tys = List.map Term.type_of cs 367 val ty = List.foldl (op -->) pred_ty (dty :: List.rev tys) 368 val l = Term.list_mk_comb (Term.mk_var (s, ty), cs @ [d]) 369 val r = mk_state_pred (tm1, tm_d) 370 in 371 Definition.new_definition (def_suffix s, boolSyntax.mk_eq (l, r)) 372 end 373in 374 fun sep_definitions sthy expnd hide thm = 375 let 376 val next_tm = utilsLib.get_function thm 377 val state_ty = utilsLib.dom (Term.type_of next_tm) 378 val (components, data, tms) = build_names (sthy, expnd, hide, state_ty) 379 fun dc ty = sthy ^ "_d_" ^ data_constructor ty 380 val data_cons = List.map (fn d => (dc d, [ParseDatatype.dAQ d])) data 381 val s_c = sthy ^ "_component" 382 val s_d = sthy ^ "_data" 383 val () = Datatype.astHol_datatype 384 [(s_c, ParseDatatype.Constructors components)] 385 val () = Datatype.astHol_datatype 386 [(s_d, ParseDatatype.Constructors data_cons)] 387 val cty = Type.mk_type (s_c, []) 388 val dty = Type.mk_type (s_d, []) 389 val pred_ty = 390 pred_setSyntax.mk_set_type 391 (pred_setSyntax.mk_set_type (pairSyntax.mk_prod (cty, dty))) 392 fun mk_dc ty = Term.mk_const (dc ty, ty --> dty) 393 val n = ref 0 394 val a0 = define_assert0 sthy pred_ty 395 val a1 = define_assert1 sthy pred_ty 396 val define_component = 397 fn ((s, []), tm) => 398 let 399 val tm1 = Term.mk_const (s, cty) 400 val tm2 = mk_dc (type_of tm) 401 in 402 ((tm1, Term.mk_comb (tm2, tm)), a0 (tm1, tm2)) 403 end 404 | ((s, ptys), tm) => 405 let 406 val tys = List.map ParseDatatype.pretypeToType ptys 407 val vs = 408 List.map 409 (fn ty => Term.mk_var ("v" ^ Int.toString (!n), ty) 410 before Portable.inc n) tys 411 val tm_v = Term.list_mk_comb (tm, vs) 412 val bty = snd (HolKernel.strip_fun (Term.type_of tm)) 413 val aty = List.foldl (op -->) cty (List.rev tys) 414 val tm1 = Term.list_mk_comb (Term.mk_const (s, aty), vs) 415 val tm2 = mk_dc (Term.type_of tm_v) 416 in 417 ((tm1, Term.mk_comb (tm2, tm_v)), a1 (tm1, tm2, vs)) 418 end 419 val l = List.map define_component (ListPair.zip (components, tms)) 420 val (cs, defs) = ListPair.unzip l 421 val proj_r = TypeBase.mk_pattern_fn cs 422 val proj_s = sthy ^ "_proj" 423 val proj_f = Term.mk_var (proj_s, state_ty --> cty --> dty) 424 val proj_l = Term.mk_comb (proj_f, mk_state_var state_ty) 425 val proj_def = 426 Definition.new_definition 427 (sthy ^ "_proj_def", boolSyntax.mk_eq (proj_l, proj_r)) 428 val () = 429 Theory.adjoin_to_theory 430 {sig_ps = 431 SOME (fn _ => 432 PP.add_string "val component_defs: thm list"), 433 struct_ps = 434 SOME (fn _ => 435 PP.block PP.CONSISTENT 2 [ 436 PP.add_string "val component_defs =", 437 PP.add_break(1,0), 438 PP.block PP.INCONSISTENT 1 ( 439 PP.add_string "[" :: 440 PP.pr_list 441 PP.add_string 442 [PP.add_string ",", PP.add_break (1, 0)] 443 (comp_names defs) @ 444 [PP.add_string "]"] 445 ), 446 PP.add_newline 447 ] 448 ) 449 } 450 in 451 proj_def :: defs 452 end 453end 454 455(* 456 457open arm_stepTheory 458 459val sthy = "arm" 460val expnd = [["CPSR"], ["FP", "FPSCR"]] 461val hide = [["undefined"], ["CurrentCondition"]] 462val thm = arm_stepTheory.NextStateARM_def 463 464val (x as ((path, ty), tm), es) = ((([], state_ty), s), expnd) 465val SOME l = Lib.total TypeBase.fields_of ty 466val (x as ((n, t), f)) = hd l 467 468val hs = [["Architecture"]] 469 470*) 471 472(* ------------------------------------------------------------------------ 473 define_map_component (name, f, def) 474 475 Given a definition of the form 476 477 |- !c d. model_X c d = {{(model_c_X, model_d_Y)}} 478 479 this function generates a map version, as defined by 480 481 !df f. name df f = {BIGUNION {BIGUNION (model_X c (f c)) | c IN df}} 482 483 and it also derives the theorem 484 485 |- c IN df ==> (model_X c d * name (df DELETE c) f = name df ((c =+ d) f)) 486 487 ------------------------------------------------------------------------ *) 488 489fun define_map_component (s, f, def) = 490 let 491 val thm = Drule.MATCH_MP stateTheory.MAPPED_COMPONENT_INSERT_OPT def 492 handle HOL_ERR _ => 493 Drule.MATCH_MP stateTheory.MAPPED_COMPONENT_INSERT1 def 494 val map_c = fst (boolSyntax.dest_forall (Thm.concl thm)) 495 val map_c = Term.mk_var (s, Term.type_of map_c) 496 val (tm_11, def_tm) = thm |> Thm.SPEC map_c 497 |> Thm.concl 498 |> boolSyntax.dest_imp |> fst 499 |> boolSyntax.dest_conj 500 val comp_11 = simpLib.SIMP_PROVE (srw_ss()) [] tm_11 501 val (v_df, def_tm) = boolSyntax.dest_forall def_tm 502 val (v_f, def_tm) = boolSyntax.dest_forall def_tm 503 val v_df' = Term.mk_var ("d" ^ f, Term.type_of v_df) 504 val v_f' = Term.mk_var (f, Term.type_of v_f) 505 val def_tm = Term.subst [v_df |-> v_df', v_f |-> v_f'] def_tm 506 val mdef = Definition.new_definition (s ^ "_def", def_tm) 507 val thm = Theory.save_thm 508 (s ^ "_INSERT", 509 Drule.SPECL [v_f', v_df'] 510 (MATCH_MP thm (Thm.CONJ comp_11 mdef))) 511 in 512 (mdef, thm) 513 end 514 handle HOL_ERR {message, ...} => raise ERR "define_map_component" message 515 516(* ------------------------------------------------------------------------ 517 mk_code_pool: make term ``CODE_POOL f {(v, opc)}`` 518 ------------------------------------------------------------------------ *) 519 520local 521 val code_pool_tm = Term.prim_mk_const {Thy = "prog", Name = "CODE_POOL"} 522in 523 fun mk_code_pool (f, v, opc) = 524 let 525 val x = pred_setSyntax.mk_set [pairSyntax.mk_pair (v, opc)] 526 in 527 boolSyntax.list_mk_icomb (code_pool_tm, [f, x]) 528 end 529 handle HOL_ERR {message, ...} => raise ERR "mk_code_pool" message 530end 531 532(* ------------------------------------------------------------------------ 533 list_mk_code_pool: make term ``CODE_POOL f {(v, [opc0, ...])}`` 534 ------------------------------------------------------------------------ *) 535 536fun list_mk_code_pool (f, v, l) = 537 mk_code_pool (f, v, listSyntax.mk_list (l, Term.type_of (hd l))) 538 539(* ------------------------------------------------------------------------ 540 is_code_access: 541 test if term is of the form ``s.mem v`` or ``s.mems (v + x)`` 542 ------------------------------------------------------------------------ *) 543 544fun is_code_access (s, v) tm = 545 case boolSyntax.dest_strip_comb tm of 546 (c, [_, a]) => 547 c = s andalso 548 (a = v orelse 549 (case Lib.total wordsSyntax.dest_word_add a of 550 SOME (x, y) => x = v andalso wordsSyntax.is_word_literal y 551 | NONE => false)) 552 | _ => false 553 554(* ------------------------------------------------------------------------ 555 dest_code_access: 556 ``s.mem a = r`` -> (0, ``r``) 557 ``s.mem (a + i) = r`` -> (i, ``r``) 558 ------------------------------------------------------------------------ *) 559 560fun dest_code_access tm = 561 let 562 val (l, r) = boolSyntax.dest_eq tm 563 val a = boolSyntax.rand l 564 val a = case Lib.total (snd o wordsSyntax.dest_word_add) a of 565 SOME x => wordsSyntax.uint_of_word x 566 | NONE => 0 567 in 568 (a, case Lib.total optionSyntax.dest_some r of SOME v => v | NONE => r) 569 end 570 571(* ------------------------------------------------------------------------ 572 read_footprint proj_def comp_defs cpool extras 573 574 Generate a map from step-theorem to 575 576 (component pre-conditions, 577 code-pool, 578 Boolean pre-condition, 579 processed next-state term) 580 581 ------------------------------------------------------------------------ *) 582 583local 584 val vnum = 585 ref (Redblackmap.mkDict String.compare : (string, int) Redblackmap.dict) 586 fun is_gen s = String.sub (s, 0) = #"%" 587in 588 fun gvar s ty = 589 let 590 val i = case Redblackmap.peek (!vnum, s) of 591 SOME i => (vnum := Redblackmap.insert (!vnum, s, i + 1) 592 ; Int.toString i) 593 | NONE => (vnum := Redblackmap.insert (!vnum, s, 0); "") 594 in 595 Term.mk_var (s ^ i, ty) 596 end 597 val vvar = gvar "%v" 598 fun varReset () = vnum := Redblackmap.mkDict String.compare 599 fun is_vvar tm = 600 case Lib.total Term.dest_var tm of 601 SOME (s, _) => is_gen s 602 | NONE => false 603 fun is_nvvar tm = 604 case Lib.total Term.dest_var tm of 605 SOME (s, _) => not (is_gen s) 606 | NONE => false 607 fun build_assert (f: term * term -> term) g = 608 fn ((d, (c, pat)), (a, tm)) => 609 let 610 val v = vvar (utilsLib.dom (Term.type_of d)) 611 in 612 (f (c, Term.mk_comb (d, v)) :: a, Term.subst [pat |-> g v] tm) 613 end 614end 615 616type footprint_extra = (term * term) * (term -> term) * (term -> term) 617 618local 619 fun entry (c, d) = let val (d, pat) = Term.dest_comb d in (d, (c, pat)) end 620 621 fun component_assoc_list proj_def = 622 proj_def |> Thm.concl 623 |> boolSyntax.strip_forall |> snd 624 |> boolSyntax.rhs 625 |> Term.dest_abs |> snd 626 |> TypeBase.strip_case |> snd 627 |> List.map entry 628 |> List.partition (fn (_, (t, _)) => Term.is_comb t) 629 630 fun prim_pat_match (c, pat) tm = 631 HolKernel.bvk_find_term (K true) 632 (fn t => 633 let val m = fst (Term.match_term pat t) in (Term.subst m c, t) end) 634 tm 635 636 fun pat_match s_tm (c, pat) tm = 637 HolKernel.bvk_find_term (Term.is_comb o snd) 638 (fn t => 639 let 640 val m = fst (Term.match_term pat t) 641 val _ = List.length (HolKernel.find_terms (Lib.equal s_tm) t) < 2 642 orelse raise ERR "" "" 643 in 644 (Term.subst m c, t) 645 end) tm 646 647 fun read_extra x = 648 fn [] => x 649 | l as ((cpat, f, g) :: r) => 650 (case prim_pat_match cpat (snd x) of 651 SOME (d, pat) => 652 read_extra 653 (build_assert (f o snd) g ((d, (boolSyntax.T, pat)), x)) l 654 | NONE => read_extra x r) 655 656 fun map_rws rws = 657 List.concat o 658 (List.map (boolSyntax.strip_conj o utilsLib.rhsc o 659 Conv.QCONV (REWRITE_CONV rws))) 660 661 val tidyup = map_rws [optionTheory.SOME_11] 662 663 fun is_ok_rhs tm = 664 is_nvvar tm orelse 665 (case Lib.total optionSyntax.dest_some tm of 666 SOME v => is_nvvar v 667 | NONE => List.null (Term.free_vars tm)) 668 669 fun mk_rewrite1 (l, r) = 670 Lib.assert 671 (fn {redex, residue} => 672 Term.is_var redex andalso is_ok_rhs residue andalso 673 Term.type_of redex = Term.type_of residue) (l |-> r) 674 675 fun mk_rewrite tm = 676 case Lib.total boolSyntax.dest_eq tm of 677 SOME x => mk_rewrite1 x 678 | NONE => (case Lib.total boolSyntax.dest_neg tm of 679 SOME v => mk_rewrite1 (v, boolSyntax.F) 680 | NONE => mk_rewrite1 (tm, boolSyntax.T)) 681 682 val is_rewrite = Lib.can mk_rewrite 683 684 fun make_subst tms = 685 tms |> List.map mk_rewrite 686 |> List.partition (Term.is_var o #residue) 687 |> (fn (l1, l2) => Term.subst (l2 @ l1)) 688 689 fun not_some_none tm = 690 case Lib.total optionSyntax.dest_is_some tm of 691 SOME t => not (optionSyntax.is_some t) 692 | NONE => true 693in 694 fun read_footprint proj_def comp_defs cpool (extras: footprint_extra list) = 695 let 696 val (l1, l2) = component_assoc_list proj_def 697 val sty = utilsLib.dom (Term.type_of (utilsLib.get_function proj_def)) 698 val b_assert = 699 build_assert 700 (utilsLib.rhsc o REWRITE_CONV (List.map GSYM comp_defs) o 701 mk_state_pred) Lib.I 702 val mtch = pat_match (Term.mk_var ("s", sty)) 703 in 704 fn thm: thm => 705 let 706 val () = varReset () 707 val (b, c: term, tm) = cpool thm 708 val x = 709 List.foldl 710 (fn e as ((_, cpat), x) => 711 if Option.isSome (prim_pat_match cpat (snd x)) 712 then b_assert e 713 else x) ([], tm) l2 714 fun loop modified x = 715 fn [] => if modified then loop false x l1 else x 716 | l as ((d, cpat) :: r) => 717 (case mtch cpat (snd x) of 718 NONE => loop modified x r 719 | SOME m => loop true (b_assert ((d, m), x)) l) 720 val (a, tm) = read_extra (loop false x l1) extras 721 val a = b :: a 722 val (p, tm) = boolSyntax.strip_imp tm 723 val (eqs, rest) = List.partition is_rewrite (tidyup p) 724 val rest = List.filter not_some_none rest 725 val sbst = make_subst eqs 726 val a = List.map sbst a 727 val p = if List.null rest 728 then boolSyntax.T 729 else sbst (boolSyntax.list_mk_conj rest) 730 in 731 (a, c, p, sbst (optionSyntax.dest_some (boolSyntax.rhs tm))) 732 end 733 end 734end 735 736(* ------------------------------------------------------------------------ 737 write_footprint syntax1 syntax2 l1 l2 l3 l4 P (p, q, tm) 738 739 Extend p (pre) and q (post) proposition lists with entries for 740 component updates. 741 742 l1 is a list of updates for map components 743 l2 is a list of updates for regular components 744 l3 is a list of updates for regular components (known to be read) 745 l4 is a list of user defined updates for sub components 746 747 P is a predicate this is used to test whether all updates have been 748 considered 749 ------------------------------------------------------------------------ *) 750 751local 752 fun strip_assign (a, b) = 753 let 754 val (x, y) = combinSyntax.strip_update (combinSyntax.dest_K_1 a) 755 in 756 if b <> y 757 then (Parse.print_term b 758 ; print "\n\n" 759 ; Parse.print_term y 760 ; raise ERR "write_footprint" "strip_assign") 761 else () 762 ; x 763 end 764 fun not_in_asserts p (dst: term -> term) = 765 List.filter 766 (fn x => 767 let 768 val d = dst x 769 in 770 not (Lib.exists (fn y => case Lib.total dst y of 771 SOME c => c = d 772 | NONE => false) p) 773 end) 774 val prefix = 775 HolKernel.list_mk_comb o (Lib.I ## Lib.butlast) o boolSyntax.strip_comb 776 fun fillIn f ty = 777 fn []: term list => [] 778 | _ => [f (vvar ty)]: term list 779 datatype footprint = 780 MapComponent of 781 term * (term * term -> term) * (term -> term) * (term -> term) 782 | Component of term list * term list * term -> term list * term list 783 fun mk_map_footprint syntax2 (c:string, t) = 784 let 785 val (tm, mk, dst:term -> term * term, _:term -> bool) = syntax2 c 786 val ty = utilsLib.dom (utilsLib.rng (Term.type_of tm)) 787 val c = fst o dst 788 fun d tm = mk (c tm, vvar ty) 789 in 790 MapComponent (t, mk, c, d) 791 end 792 fun mk_footprint1 syntax1 (c:string) = 793 let 794 val (tm, mk, _:term -> term, _:term -> bool) = syntax1 c 795 val ty = utilsLib.dom (Term.type_of tm) 796 in 797 Component 798 (fn (p, q, v) => 799 let 800 val x = mk v 801 val l = fillIn mk ty (not_in_asserts p Term.rator [x]) 802 in 803 (l @ p, x :: q) 804 end) 805 end 806 fun mk_footprint1b syntax1 (c:string) = 807 let 808 val (_, mk, _, _) = syntax1 c 809 in 810 Component (fn (p, q, v) => (p, mk v :: q)) 811 end 812in 813 fun sort_finish psort (p, q) = 814 let 815 val q = psort (q @ not_in_asserts q prefix p) 816 in 817 (psort p, q) 818 end 819 fun write_footprint syntax1 syntax2 l1 l2 l3 l4 P = 820 let 821 val mk_map_f = mk_map_footprint syntax2 822 val l1 = List.map (fn (s, c, tm) => (s, mk_map_f (c, tm))) l1 823 val l2 = List.map (I ## mk_footprint1 syntax1) l2 824 val l3 = List.map (I ## mk_footprint1b syntax1) l3 825 val l4 = List.map (I ## Component) l4 826 val m = Redblackmap.fromList String.compare (l1 @ l2 @ l3 @ l4) 827 fun default (s, l, p, q) = 828 if P (s, l) then (p, q) else raise ERR "write_footprint" s 829 fun loop (p, q, tm) = 830 (case boolSyntax.dest_strip_comb tm of 831 (f_upd, l as [v, rst]) => 832 (case Redblackmap.peek (m, f_upd) of 833 SOME (Component f) => 834 let 835 val (p', q') = f (p, q, combinSyntax.dest_K_1 v) 836 in 837 loop (p', q', rst) 838 end 839 | SOME (MapComponent (t, mk, c, d)) => 840 let 841 val l = List.map mk (strip_assign (v, t)) 842 val l2 = List.map d (not_in_asserts p c l) 843 in 844 loop (l2 @ p, l @ q, rst) 845 end 846 | NONE => default (f_upd, l, p, q)) 847 | (s, l) => default (s, l, p, q) : (term list * term list)) 848 handle HOL_ERR {origin_function = "dest_thy_const", ...} => (p, q) 849 in 850 loop 851 end 852end 853 854(* ------------------------------------------------------------------------ 855 mk_pre_post 856 857 Generate pre-codition, code-pool and post-condition for step-theorem 858 ------------------------------------------------------------------------ *) 859 860local 861 val temporal = ref false 862in 863 fun set_temporal b = temporal := b 864 fun generate_temporal () = !temporal 865end 866 867local 868 fun get_def tm = 869 let 870 val {Name, Thy, ...} = Term.dest_thy_const (Term.rand tm) 871 in 872 DB.fetch Thy (Name ^ "_def") 873 end 874in 875 fun mk_pre_post model_def comp_defs cpool extras write_fn psort = 876 let 877 val (model_tm, tm) = boolSyntax.dest_eq (Thm.concl model_def) 878 val proj_def = case pairSyntax.strip_pair tm of 879 [a, _, _, _, _] => get_def a 880 | _ => raise ERR "mk_pre_post" "bad model definition" 881 val read = read_footprint proj_def comp_defs cpool extras 882 val mk_spec_or_temporal_next = 883 temporal_stateSyntax.mk_spec_or_temporal_next model_tm 884 val write = (progSyntax.list_mk_star ## progSyntax.list_mk_star) o 885 sort_finish psort o write_fn 886 in 887 fn thm: thm => 888 let 889 val (p, pool, c, tm) = read thm 890 val (p, q) = write (p, []: term list, tm) 891 val p = if c = boolSyntax.T 892 then p 893 else progSyntax.mk_star (progSyntax.mk_cond c, p) 894 in 895 mk_spec_or_temporal_next (generate_temporal()) (p, pool, q) 896 end 897 end 898end 899 900(* ------------------------------------------------------------------------ 901 rename_vars: 902 903 Rename generated variables "%v" in a SPEC theorem. 904 ------------------------------------------------------------------------ *) 905 906fun rename_vars (rmap, bump) = 907 let 908 fun rename f tm = 909 case boolSyntax.dest_strip_comb tm of 910 (_, []) => NONE 911 | (c, l) => 912 let 913 val (x, v) = Lib.front_last l 914 in 915 if is_vvar v 916 then case rmap c of 917 SOME g => 918 (case Lib.total g x of 919 SOME s => SOME (v |-> f (s, Term.type_of v)) 920 | NONE => NONE) 921 | NONE => NONE 922 else NONE 923 end 924 in 925 fn thm => 926 let 927 val p = temporal_stateSyntax.dest_pre' (Thm.concl thm) 928 val () = varReset () 929 val () = List.app (fn s => General.ignore (gvar s Type.alpha)) bump 930 val avoid = utilsLib.avoid_name_clashes p o Lib.uncurry gvar 931 val p = progSyntax.strip_star p 932 in 933 Thm.INST (List.mapPartial (rename avoid) p) thm 934 end 935 handle e as HOL_ERR _ => Raise e 936 end 937 938(* ------------------------------------------------------------------------ 939 introduce_triple_definition (duplicate, thm_def) thm 940 941 Given a thm_def of the form 942 943 |- !x. f x = p1 * ... * pn * cond c1 * ... * cond cm 944 945 (where the conds need not be at the end) and a theorem "thm" of the form 946 947 |- SPEC (cond r * p) c q 948 949 the function introduce_triple_definition gives a theorem of form 950 951 |- SPEC (cond r' * p' * f x1) c (q' * f x2) 952 953 The condition "r'" is related to "r" but will no longer incorporate 954 conditions found in "c1" to "cm". Similarly "p'" and "q'" will no 955 longer contain components "p1" to "pn". 956 957 The "duplicate" flag controls whether or not conditions in "r" are 958 added to the postcondition in order to introduce "f". 959 ------------------------------------------------------------------------ *) 960 961local 962 val get_conds = List.filter progSyntax.is_cond o progSyntax.strip_star 963 val err = ERR "introduce_triple" 964 fun move_match (pat, t) = 965 MOVE_COND_RULE 966 (case Lib.mk_set (find_terms (Lib.can (Term.match_term pat)) t) of 967 [] => raise (err "missing condition") 968 | [m] => m 969 | l => Lib.with_exn (Lib.first (Lib.equal pat)) l 970 (err "ambiguous condition")) 971in 972 fun introduce_triple_definition (duplicate, thm_def) = 973 let 974 val ts = thm_def 975 |> Thm.concl 976 |> boolSyntax.strip_forall |> snd 977 |> boolSyntax.dest_eq |> snd 978 |> progSyntax.strip_star 979 val (cs, ps) = List.partition progSyntax.is_cond ts 980 val cs = List.map progSyntax.dest_cond cs 981 val rule = 982 helperLib.PRE_POST_RULE (helperLib.STAR_REWRITE_CONV (GSYM thm_def)) 983 fun d_rule th = 984 if duplicate 985 then MATCH_MP progTheory.SPEC_DUPLICATE_COND th 986 handle HOL_ERR _ => 987 MATCH_MP 988 temporal_stateTheory.TEMPORAL_NEXT_DUPLICATE_COND th 989 else th 990 in 991 fn thm => 992 let 993 val p = temporal_stateSyntax.dest_pre' (Thm.concl thm) 994 val move_cs = 995 List.map 996 (fn t => List.map (fn c => d_rule o move_match (c, t)) cs) 997 (get_conds p) 998 in 999 thm |> SPECL_FRAME_RULE ps 1000 |> Lib.C (List.foldl (fn (f, t) => f t)) 1001 (List.concat move_cs) 1002 |> rule 1003 end 1004 end 1005end 1006 1007(* ------------------------------------------------------------------------ 1008 introduce_map_definition (insert_thm, dom_eq_conv) thm 1009 1010 Given an insert_thm of the form 1011 1012 |- c IN df ==> (model_X c d * name (df DELETE c) f = name df ((c =+ d) f)) 1013 1014 (which may be generated by define_map_component) and a theorem "thm" of the 1015 form 1016 1017 |- SPEC (cond r * p) c q 1018 1019 where "p" and "q" contain instances of "model_X c d", a theorem new is 1020 generated of the form 1021 1022 |- SPEC (p' * name df f * cond (r /\ z)) x (q' * name df f') 1023 1024 where "p'" and "q'" are modified versions of "p" and "q" that no longer 1025 contain any instances of "model_X c d". 1026 1027 The predicate "z" will specify which values are contained in "df", 1028 which represents the domain of the newly intoruced map "f". 1029 1030 The conversion "dom_eq_conv" can be used to simplify "z" by deciding 1031 equality over elements of the domain of "f". 1032 ------------------------------------------------------------------------ *) 1033 1034local 1035 fun strip2 f = case boolSyntax.strip_comb f of 1036 (f, [a, b]) => (f, (a, b)) 1037 | _ => raise ERR "strip2" "" 1038 val tidy_up_rule = 1039 helperLib.MERGE_CONDS_RULE o 1040 PURE_REWRITE_RULE [GSYM progTheory.SPEC_MOVE_COND, 1041 GSYM temporal_stateTheory.TEMPORAL_NEXT_MOVE_COND] o 1042 Drule.DISCH_ALL 1043 val is_ineq = Lib.can (boolSyntax.dest_eq o boolSyntax.dest_neg) 1044 val apply_id_rule = PURE_REWRITE_RULE [updateTheory.APPLY_UPDATE_ID] 1045in 1046 fun introduce_map_definition (insert_thm, dom_eq_conv) = 1047 let 1048 val insert_thm = Drule.SPEC_ALL insert_thm 1049 val ((f_tm, (c, d)), (m_tm, (df, f))) = 1050 insert_thm 1051 |> Thm.concl 1052 |> boolSyntax.dest_imp |> snd 1053 |> boolSyntax.dest_eq |> fst 1054 |> progSyntax.dest_star 1055 |> (strip2 ## strip2) 1056 val is_f = Lib.equal f_tm o fst o boolSyntax.strip_comb 1057 val get_f = 1058 List.filter is_f o progSyntax.strip_star o 1059 temporal_stateSyntax.dest_pre' o Thm.concl 1060 val c_ty = Term.type_of c 1061 val d_ty = Term.type_of d 1062 val c_set_ty = pred_setSyntax.mk_set_type c_ty 1063 val df = fst (pred_setSyntax.dest_delete df) 1064 val df_intro = List.foldl (pred_setSyntax.mk_delete o Lib.swap) df 1065 fun mk_frame cs = Term.mk_comb (Term.mk_comb (m_tm, df_intro cs), f) 1066 val insert_conv = 1067 utilsLib.ALL_HYP_CONV_RULE 1068 (PURE_REWRITE_CONV [pred_setTheory.IN_DELETE]) o 1069 utilsLib.INST_REWRITE_CONV [Drule.UNDISCH_ALL insert_thm] 1070 val (mk_dvar, mk_subst) = 1071 case Lib.total optionSyntax.dest_option d_ty of 1072 SOME ty => 1073 (fn () => optionSyntax.mk_some (Term.genvar ty), 1074 fn (d, c) => optionSyntax.dest_some d |-> Term.mk_comb (f, c)) 1075 | NONE => 1076 (fn () => Term.genvar d_ty, 1077 fn (d, c) => d |-> Term.mk_comb (f, c)) 1078 val update_ss = 1079 bool_ss ++ 1080 simpLib.rewrites 1081 [updateTheory.APPLY_UPDATE_ID, combinTheory.UPDATE_APPLY, 1082 combinTheory.UPDATE_APPLY_IMP_ID] 1083 in 1084 fn th => 1085 let 1086 val xs = get_f th 1087 in 1088 if List.null xs 1089 then th 1090 else let 1091 val xs = 1092 List.map 1093 (fn t => 1094 let 1095 val (g, d) = Term.dest_comb t 1096 val c = Term.rand g 1097 in 1098 (Term.mk_comb (g, mk_dvar ()), 1099 (Term.rand g, mk_subst (d, c))) 1100 end) xs 1101 val (xs, cs_ds) = ListPair.unzip xs 1102 val (cs, ds) = ListPair.unzip cs_ds 1103 val frame = mk_frame cs 1104 val rwt = 1105 insert_conv (List.foldr progSyntax.mk_star frame xs) 1106 val ineqs = 1107 rwt |> Thm.hyp 1108 |> List.map boolSyntax.strip_conj 1109 |> List.concat 1110 |> List.filter is_ineq 1111 |> List.map 1112 (utilsLib.ALL_HYP_CONV_RULE dom_eq_conv o 1113 ASSUME) 1114 val (rwt, rule) = 1115 if List.null ineqs 1116 then (rwt, apply_id_rule) 1117 else (utilsLib.ALL_HYP_CONV_RULE 1118 (REWRITE_CONV ineqs) rwt, 1119 SIMP_RULE (update_ss++simpLib.rewrites ineqs)[]) 1120 in 1121 th |> SPECC_FRAME_RULE frame 1122 |> helperLib.PRE_POST_RULE 1123 (helperLib.STAR_REWRITE_CONV rwt) 1124 |> Thm.INST ds 1125 |> rule 1126 |> tidy_up_rule 1127 end 1128 end 1129 end 1130 handle HOL_ERR _ => raise ERR "introduce_map_definition" "" 1131end 1132 1133(* ------------------------------------------------------------------------ 1134 fix_precond 1135 1136 Given a list of theorems of the form 1137 1138 [ 1139 |- SPEC m (p1 * cond (... /\ c /\ ...)) code q1, 1140 |- SPEC m (p2 * cond ~c) code q2 1141 ] 1142 1143 (where the "cond" terms are not necessarily outermost) return theorems 1144 1145 [ 1146 |- SPEC m (p1 * cond (...) * precond c) code q1, 1147 |- SPEC m (p2 * precond ~c) code q2 1148 ] 1149 1150 Is an identity function for single element lists and raises and error 1151 for all other lists. 1152 ------------------------------------------------------------------------ *) 1153 1154local 1155 val pecond_rule = 1156 Conv.CONV_RULE 1157 (Conv.TRY_CONV 1158 (helperLib.PRE_CONV 1159 (Conv.RAND_CONV 1160 (Conv.RATOR_CONV 1161 (Conv.REWR_CONV (GSYM set_sepTheory.precond_def)))))) 1162 fun rule c th = pecond_rule (MOVE_COND_RULE c th) 1163 val get_cond = 1164 Term.rand o Lib.first progSyntax.is_cond o progSyntax.strip_star o 1165 temporal_stateSyntax.dest_pre' o Thm.concl 1166in 1167 val fix_precond = 1168 fn [th1, th2] => 1169 let 1170 val c = get_cond th2 1171 in 1172 [rule (utilsLib.mk_negation c) th1, rule c th2] 1173 end 1174 | thms as [_] => thms 1175 | _ => raise ERR "fix_precond" "" 1176end 1177 1178(* ------------------------------------------------------------------------ 1179 split_cond pre dst_f th 1180 1181 Given a theorem th of the form 1182 1183 |- SPEC m (p * cond c) code (q * f (if b then x else y)), 1184 1185 this routine returns theorems of the form 1186 1187 [ 1188 |- SPEC m (p1 * cond c1 * precond b) code (q1 * f x) , 1189 |- SPEC m (p2 * cond c2 * precond ~b) code (q2 * f y) 1190 ] 1191 1192 when pre is true and 1193 1194 [ 1195 |- SPEC m (p1 * cond (c1 /\ b)) code (q1 * f x), 1196 |- SPEC m (p2 * cond (c2 /\ ~b)) code (q2 * f y) 1197 ] 1198 1199 when pre is false. The expressions p1, q1, c1 are p, q, c rewritten assuming 1200 b = T and p2, q2, c2 are p, q, c rewritten assuming b = F. 1201 1202 cond T assertions are eliminated. 1203 1204 ------------------------------------------------------------------------ *) 1205 1206local 1207 val move_cond = GSYM progTheory.SPEC_MOVE_COND 1208 val move_precond = REWRITE_RULE [GSYM set_sepTheory.precond_def] move_cond 1209 val cond_true_elim = REWRITE_RULE [stateTheory.cond_true_elim] 1210 fun rule pre = 1211 cond_true_elim o (if pre then Lib.I else helperLib.MERGE_CONDS_RULE) o 1212 Conv.CONV_RULE 1213 (Conv.REWR_CONV 1214 (if pre then move_precond else move_cond)) o Lib.uncurry Thm.DISCH 1215 fun spec_cases pre b th = 1216 let 1217 val nb = boolSyntax.mk_neg b 1218 val pt = Drule.EQT_INTRO (Thm.ASSUME b) 1219 val nt = Drule.EQF_INTRO (Thm.ASSUME nb) 1220 val pth = PURE_REWRITE_RULE [pt, boolTheory.COND_CLAUSES] th 1221 val _ = Thm.hyp pth = [b] orelse raise ERR "spec_cases" "" 1222 val nth = PURE_REWRITE_RULE [nt, boolTheory.COND_CLAUSES] th 1223 val r = rule pre 1224 in 1225 [r (b, pth), r (nb, nth)] 1226 end 1227in 1228 fun split_cond pre dst th = 1229 let 1230 val p = progSyntax.strip_star (progSyntax.dest_post (Thm.concl th)) 1231 in 1232 case List.mapPartial (Lib.total dst) p of 1233 [t] => (case Lib.total boolSyntax.dest_cond t of 1234 SOME (b, _, _) => spec_cases pre b th 1235 | NONE => [th]) 1236 | _ => [th] 1237 end 1238end 1239 1240(* ------------------------------------------------------------------------ 1241 get_delta pc_var pc 1242 get_pc_delta is_pc 1243 ------------------------------------------------------------------------ *) 1244 1245fun get_delta pc_var pc = 1246 case Lib.total wordsSyntax.dest_word_add pc of 1247 SOME (x, n) => 1248 if x = pc_var 1249 then Lib.total wordsSyntax.uint_of_word n 1250 else NONE 1251 | NONE => 1252 (case Lib.total wordsSyntax.dest_word_sub pc of 1253 SOME (x, n) => 1254 if x = pc_var 1255 then Lib.total (Int.~ o wordsSyntax.uint_of_word) n 1256 else NONE 1257 | NONE => if pc = pc_var then SOME 0 else NONE) 1258 1259fun get_pc_delta is_pc = 1260 let 1261 val get_pc = Term.rand o Lib.first is_pc o progSyntax.strip_star 1262 in 1263 fn th => 1264 let 1265 val (p, q) = progSyntax.dest_pre_post (Thm.concl th) 1266 in 1267 get_delta (get_pc p) (get_pc q) 1268 end 1269 end 1270 1271(* ------------------------------------------------------------------------ 1272 PC_CONV 1273 ------------------------------------------------------------------------ *) 1274 1275local 1276 fun f q = 1277 boolTheory.COND_RAND |> Q.ISPEC q |> SIMP_RULE std_ss [] |> Drule.GEN_ALL 1278 val COND_RAND_CONV = 1279 PURE_REWRITE_CONV 1280 (List.map f [`\n : 'a word. n + z`, `\n : 'a word. z + n`, 1281 `\n : 'a word. n - z`, `\n : 'a word. z - n`]) 1282 val cnv = wordsLib.WORD_ARITH_CONV THENC wordsLib.WORD_SUB_CONV 1283 fun ARITH_SUB_CONV tm = 1284 (if boolSyntax.is_cond tm then 1285 Conv.RAND_CONV ARITH_SUB_CONV 1286 THENC Conv.RATOR_CONV (Conv.RAND_CONV ARITH_SUB_CONV) 1287 else cnv) tm 1288 val PC_CONV0 = Conv.RAND_CONV (COND_RAND_CONV THENC ARITH_SUB_CONV) 1289 fun is_word_lit tm = 1290 case Lib.total wordsSyntax.dest_mod_word_literal tm of 1291 SOME (n, s) => 1292 n = wordsSyntax.dest_word_literal tm andalso 1293 Lib.funpow (Arbnum.toInt s - 1) Arbnum.div2 n = Arbnum.zero 1294 | NONE => false 1295 fun is_irreducible tm = 1296 Term.is_var tm orelse 1297 (case Lib.total wordsSyntax.dest_word_add tm of 1298 SOME (p, i) => Term.is_var p andalso is_word_lit i 1299 | NONE => false) orelse 1300 (case Lib.total wordsSyntax.dest_word_sub tm of 1301 SOME (p, i) => Term.is_var p andalso is_word_lit i 1302 | NONE => false) orelse 1303 (case Lib.total boolSyntax.dest_cond tm of 1304 SOME (_, x, y) => is_irreducible x andalso is_irreducible y 1305 | NONE => false) 1306in 1307 fun PC_CONV s = 1308 Conv.ONCE_DEPTH_CONV 1309 (fn tm => 1310 case boolSyntax.dest_strip_comb tm of 1311 (c, [t]) => 1312 if c = s andalso not (is_irreducible t) 1313 then PC_CONV0 tm 1314 else raise ERR "PC_CONV" "" 1315 | _ => raise ERR "PC_CONV" "") 1316end 1317 1318(* ------------------------------------------------------------------------ 1319 group_into_chunks (dst, n, mk, is_big_end) l 1320 1321 Helper function for collecting together multiple map accesses. Assumes 1322 that the list "l" is suitably ordered. 1323 1324 dst - identifies the access, e.g. arm_MEM 1325 n - number of accesses to be grouped togther, e.g. 4 bytes 1326 mk - used when reversing endianness 1327 is_big_end - identify big-endian mode 1328 ------------------------------------------------------------------------ *) 1329 1330local 1331 fun err i = ERR "group_into_chunks" ("missing chunk: " ^ Int.toString i) 1332 fun get i l = 1333 if i = 0 1334 then snd (hd l) : term 1335 else case Lib.total (wordsSyntax.dest_word_add ## I) (List.nth (l, i)) of 1336 SOME ((a, b), d) => 1337 ( wordsSyntax.uint_of_word b = i orelse raise (err i) 1338 ; d 1339 ) 1340 | NONE => raise (err i) 1341 fun mk_chunk (w, ty) = 1342 fn (h, l) => 1343 let 1344 val hi = numSyntax.term_of_int h 1345 val li = numSyntax.term_of_int l 1346 in 1347 wordsSyntax.mk_word_extract (hi, li, w, ty) 1348 end 1349 fun prim_mk_word_var (i, ty) = Term.mk_var ("w" ^ Int.toString i, ty) 1350 fun mk_word_var (d, i, ty) = 1351 case Lib.total wordsSyntax.dest_word_extract d of 1352 SOME (_, _, v, _) => v 1353 | NONE => prim_mk_word_var (i, ty) 1354 fun process be n j = 1355 fn [] => raise ERR "group_into_n_chunks" "empty" 1356 | l as ((a, d) :: _) => 1357 let 1358 val dty = wordsSyntax.dest_word_type (Term.type_of d) 1359 val dsz = fcpSyntax.dest_int_numeric_type dty 1360 val ty = wordsSyntax.mk_int_word_type (dsz * n) 1361 val w = mk_word_var (d, j, ty) 1362 val mk = mk_chunk (w, dty) 1363 fun mk_i i = let val l = i * dsz in mk (l + dsz - 1, l) end 1364 in 1365 (List.rev 1366 (List.tabulate 1367 (n, fn i => get i l |-> mk_i (if be then n - 1 - i else i))), 1368 (w, a)) 1369 end 1370 fun group_into_n n = 1371 let 1372 fun iter a l = 1373 if List.null l 1374 then List.rev a 1375 else iter (List.take (l, n) :: a) (List.drop (l, n)) 1376 handle General.Subscript => raise ERR "group_into_n" "too few" 1377 in 1378 iter [] 1379 end 1380in 1381 fun group_into_chunks (dst, n, be) = 1382 ListPair.unzip o Lib.mapi (process be n) o 1383 group_into_n n o List.mapPartial (Lib.total dst) 1384end 1385 1386(* ------------------------------------------------------------------------ 1387 ------------------------------------------------------------------------ *) 1388 1389fun pick_endian_rule (is_big_end, rule1, rule2) = 1390 let 1391 val P = List.exists is_big_end o progSyntax.strip_star o 1392 temporal_stateSyntax.dest_pre' o Thm.concl 1393 in 1394 fn th => if P th then rule1 th else rule2 th : thm 1395 end 1396 1397fun chunk_for m_def = 1398 let 1399 val (l, r) = boolSyntax.dest_eq (Thm.concl (Drule.SPEC_ALL m_def)) 1400 val m_tm = fst (boolSyntax.strip_comb l) 1401 val (c_tm, n) = case progSyntax.strip_star r of 1402 [] => raise ERR "chunks_intro" "" 1403 | l as h :: _ => 1404 (fst (boolSyntax.strip_comb h), List.length l) 1405 in 1406 (HolKernel.dest_binop c_tm (ERR "dest" "chunks"), n, m_tm) 1407 end 1408 1409fun not_refl thm = 1410 case Lib.total (boolSyntax.dest_eq o Thm.concl) thm of 1411 SOME (l, r) => l <> r 1412 | NONE => false 1413 1414fun chunks_intro_pre_process m_def = 1415 let 1416 val (dst, n, _) = chunk_for m_def 1417 val dst = fst o dst 1418 in 1419 fn thm => 1420 let 1421 val p = temporal_stateSyntax.dest_pre' (Thm.concl thm) 1422 val l = List.filter (Lib.can dst) (progSyntax.strip_star p) 1423 in 1424 if List.null l 1425 then thm 1426 else let 1427 val base = dst (hd l) 1428 val ty = wordsSyntax.dim_of base 1429 fun lit i = wordsSyntax.mk_n2w (numLib.term_of_int i, ty) 1430 fun mk0 i = wordsSyntax.mk_word_add (base, lit i) 1431 fun mk (0, 0) = base 1432 | mk (0, j) = mk0 j 1433 | mk (i, 0) = mk0 i 1434 | mk (i, j) = wordsSyntax.mk_word_add (mk0 i, lit j) 1435 fun rwt tm (i, j) = 1436 let 1437 val r = 1438 Drule.EQT_ELIM 1439 (wordsLib.WORD_ARITH_CONV 1440 (boolSyntax.mk_eq (dst tm, mk (i, j)))) 1441 in 1442 Conv.RATOR_CONV (Conv.RAND_CONV (Conv.REWR_CONV r)) tm 1443 end 1444 val (rwts, _) = 1445 List.foldl 1446 (fn (tm, (acc, (i, j))) => 1447 let 1448 val r = rwt tm (i, j) 1449 in 1450 (if not_refl r then r :: acc else acc, 1451 if j = n - 1 then (i + n, 0) else (i, j + 1)) 1452 end) ([], (0, 0)) l 1453 in 1454 PURE_REWRITE_RULE rwts thm 1455 end 1456 handle HOL_ERR {origin_function = "EQT_ELIM", ...} => thm 1457 end 1458 end 1459 1460fun chunks_intro be m_def = 1461 let 1462 val (dst, n, _) = chunk_for m_def 1463 val chunks = group_into_chunks (dst, n, be) 1464 val cnv = REPEATC (helperLib.STAR_REWRITE_CONV (GSYM m_def)) 1465 in 1466 fn thm => 1467 let 1468 val p = temporal_stateSyntax.dest_pre' (Thm.concl thm) 1469 val (s, wa) = chunks (progSyntax.strip_star p) 1470 in 1471 if List.null wa 1472 then thm 1473 else helperLib.PRE_POST_RULE cnv (Thm.INST (List.concat s) thm) 1474 end 1475 handle HOL_ERR {origin_function = "group_into_n", 1476 message = "too few", ...} => thm 1477 end 1478 1479(* ------------------------------------------------------------------------ 1480 sep_array_intro mk_rev is_big_end m_def rwts 1481 1482 Introduce a SEP_ARRAY. 1483 ------------------------------------------------------------------------ *) 1484 1485local 1486 val (sep_array_tm, mk_sep_array, dest_sep_array, _) = 1487 HolKernel.syntax_fns 1488 {n = 5, dest = HolKernel.dest_quadop, make = HolKernel.mk_quadop} 1489 "set_sep" "SEP_ARRAY" 1490 val list_mk_concat = 1491 HolKernel.list_mk_rbinop (Lib.curry wordsSyntax.mk_word_concat) 1492 val list_mk_add = 1493 HolKernel.list_mk_lbinop (Lib.curry wordsSyntax.mk_word_add) 1494 val emp_right = set_sepTheory.SEP_CLAUSES |> SPEC_ALL |> CONJUNCTS |> last 1495 fun mk_array prj be (s1: (term, term) subst list) = 1496 let 1497 val f = if be then List.rev else Lib.I 1498 in 1499 List.map (fn l => list_mk_concat (List.map prj (f l))) s1 1500 end 1501 val mk_array1 = mk_array (#residue) 1502 val mk_array2 = mk_array (#redex) 1503 fun array_iter_rwts base wa delta = 1504 Lib.mapi (fn i => fn (_, a) => 1505 let 1506 val t = list_mk_add (base :: List.tabulate (i, K delta)) 1507 in 1508 if t = a then boolTheory.TRUTH 1509 else wordsLib.WORD_ARITH_PROVE (boolSyntax.mk_eq (t, a)) 1510 end) wa 1511 val cnv1 = REWRITE_CONV [emp_right, set_sepTheory.SEP_ARRAY_def] 1512 fun frame_rule thm = 1513 Drule.SPEC_ALL 1514 (MATCH_MP (if generate_temporal () 1515 then temporal_stateTheory.SEP_ARRAY_TEMPORAL_FRAME 1516 else stateTheory.SEP_ARRAY_FRAME) thm) 1517 fun length_list rwt = 1518 let 1519 val (_, _, _, l) = dest_sep_array (utilsLib.rhsc rwt) 1520 in 1521 listSyntax.mk_length l 1522 end 1523 val length_eq = 1524 Drule.EQT_ELIM o 1525 (Conv.BINOP_CONV listLib.LENGTH_CONV THENC reduceLib.NEQ_CONV) o 1526 boolSyntax.mk_eq 1527in 1528 fun sep_array_intro be m_def rwts = 1529 let 1530 val (dst, n, m_tm) = chunk_for m_def 1531 val chunks = group_into_chunks (dst, n, be) 1532 val rule = SYM o PURE_REWRITE_RULE rwts 1533 val cnv1 = REWRITE_CONV [m_def, emp_right, set_sepTheory.SEP_ARRAY_def] 1534 fun star rwt = helperLib.STAR_REWRITE_CONV rwt 1535 THENC PURE_REWRITE_CONV rwts 1536 in 1537 fn thm => 1538 let 1539 val p = temporal_stateSyntax.dest_pre' (Thm.concl thm) 1540 val (s, wa) = chunks (progSyntax.strip_star p) 1541 in 1542 if List.null wa 1543 then thm 1544 else let 1545 val (w, base) = hd wa 1546 val sz = wordsSyntax.size_of base 1547 val delta = wordsSyntax.mk_word (Arbnum.fromInt n, sz) 1548 val iter_rwts = array_iter_rwts base wa delta 1549 val r = rule o (cnv1 THENC PURE_REWRITE_CONV iter_rwts) 1550 val l1_tm = 1551 listSyntax.mk_list (mk_array1 be s, Term.type_of w) 1552 val sep_array1 = mk_sep_array (m_tm, delta, base, l1_tm) 1553 val rwt1 = r sep_array1 1554 val thm' = Thm.INST (List.concat s) thm 1555 val lq = 1556 progSyntax.strip_star 1557 (temporal_stateSyntax.dest_post' (Thm.concl thm')) 1558 val (s2, _) = chunks lq 1559 val array = 1560 (if s = s2 then mk_array2 else mk_array1) be s2 1561 val l2_tm = listSyntax.mk_list (array, Term.type_of w) 1562 val sep_array2 = mk_sep_array (m_tm, delta, base, l2_tm) 1563 val rwt2 = r sep_array2 1564 val length_l2_l1 = 1565 length_eq (length_list rwt2, length_list rwt1) 1566 in 1567 frame_rule 1568 (Thm.CONJ length_l2_l1 1569 (Conv.CONV_RULE 1570 (helperLib.PRE_CONV (star rwt1) 1571 THENC helperLib.POST_CONV (star rwt2)) thm')) 1572 end 1573 end 1574 handle HOL_ERR {origin_function = "group_into_n", 1575 message = "too few", ...} => thm 1576 end 1577end 1578 1579(* ------------------------------------------------------------------------ 1580 register_combinations 1581 1582 Take a next-state (step) theorem and SPEC term and generate all valid 1583 variants based on register equivalences. 1584 ------------------------------------------------------------------------ *) 1585 1586local 1587 fun concat_unzip l = (List.concat ## List.concat) (ListPair.unzip l) 1588 fun instantiate (a, b) = 1589 if Term.is_var a then SOME (a |-> b) 1590 else if a = b then NONE else raise ERR "instantiate" "bad constant match" 1591 fun mk_assign f (p, q) = 1592 List.map 1593 (fn ((r1, a), (r2, b)) => (Lib.assert (op =) (r1, r2); (r1, a, b))) 1594 (ListPair.zip (f p, f q)) 1595 fun takeWhile P = 1596 let 1597 fun iter [] = [] 1598 | iter (h :: t) = if P h then h :: iter t else [] 1599 in 1600 iter 1601 end 1602in 1603 fun register_combinations 1604 (dest_reg, reg_width, proj_reg, reg_conv, ok_conv, asm, model_tm) = 1605 let 1606 val mk = temporal_stateSyntax.mk_spec_or_temporal_next model_tm 1607 val regs = List.mapPartial (Lib.total dest_reg) 1608 val reg_rule = utilsLib.FULL_CONV_RULE reg_conv 1609 val bits = List.map bitstringSyntax.mk_b o 1610 utilsLib.padLeft false reg_width o 1611 bitstringSyntax.num_to_bitlist o 1612 Arbnum.fromInt 1613 fun proj_reg0 tm = 1614 case Lib.total (fst o bitstringSyntax.dest_v2w) tm of 1615 SOME l => fst (listSyntax.dest_list l) 1616 | NONE => bits (wordsSyntax.uint_of_word tm) 1617 val proj = case proj_reg of 1618 SOME f => 1619 (fn t => case Lib.total f t of 1620 SOME i => bits i 1621 | NONE => proj_reg0 (Term.rand t)) 1622 | NONE => proj_reg0 1623 fun err s = ERR "register_combinations: explode_reg" s 1624 fun explode_reg tm = 1625 let 1626 val l = proj tm 1627 in 1628 List.length l = reg_width orelse raise (err "assertion failed") 1629 ; l 1630 end 1631 handle HOL_ERR {message = s, ...} => raise (err s) 1632 fun match_register (tm1, v1, _) (tm2, v2, v3) = 1633 let 1634 val _ = v3 = v2 orelse raise ERR "match_register" "changed" 1635 val l = ListPair.zip (explode_reg tm2, explode_reg tm1) 1636 in 1637 ((v2 |-> v1) :: List.mapPartial instantiate l, [tm2]) 1638 end 1639 val frees = List.filter Term.is_var o explode_reg 1640 fun no_free (t, _: term, _: term) = List.null (frees t) 1641 val exists_free = List.exists (not o no_free) 1642 fun no_good l = List.length (takeWhile no_free l) > 1 1643 fun groupings ok rs = 1644 let 1645 val (cs, vs) = List.partition no_free rs 1646 in 1647 (cs @ vs) 1648 |> utilsLib.partitions 1649 |> List.filter (not o Lib.exists no_good) 1650 |> List.map 1651 (List.mapPartial 1652 (fn l => 1653 let 1654 val (unchanged, changed) = 1655 List.partition (fn (_, a, b) => a = b) l 1656 in 1657 if 1 < List.length l 1658 andalso List.length changed < 2 1659 andalso exists_free l 1660 then SOME (changed @ unchanged) 1661 else NONE 1662 end)) 1663 |> Lib.mk_set 1664 |> Lib.mapfilter 1665 (fn p => 1666 concat_unzip 1667 (List.map 1668 (fn l => 1669 let 1670 val (h, t) = 1671 Lib.pluck no_free l 1672 handle 1673 HOL_ERR 1674 {message = "predicate not satisfied", 1675 ...} => (hd l, tl l) 1676 fun mtch x = 1677 let 1678 val s = match_register h x 1679 in 1680 Lib.assert ok (fst s); s 1681 end 1682 in 1683 concat_unzip (List.map mtch t) 1684 end) p)) 1685 end 1686 (* check that the pre-condition predictate (from "cond P" terms) is not 1687 violated *) 1688 val conv = reg_conv THENC ok_conv 1689 fun assign_ok p = 1690 let 1691 val l = List.mapPartial (Lib.total progSyntax.dest_cond) p 1692 val c = boolSyntax.list_mk_conj l 1693 in 1694 fn s => utilsLib.rhsc (conv (Term.subst s c)) <> boolSyntax.F 1695 end 1696 fun star_subst s = List.map (utilsLib.rhsc o reg_conv o Term.subst s) 1697 in 1698 fn (thm, t) => 1699 let 1700 val (_, p, c, q) = temporal_stateSyntax.dest_spec' t 1701 val pl = progSyntax.strip_star p 1702 val ql = progSyntax.strip_star q 1703 val rs = mk_assign regs (pl, ql) 1704 val groups = groupings (assign_ok pl) rs 1705 in 1706 if List.null groups 1707 then [(thm, t)] 1708 else List.map 1709 (fn (s, d) => 1710 let 1711 val do_reg = 1712 star_subst s o 1713 List.filter 1714 (fn tm => 1715 case Lib.total dest_reg tm of 1716 SOME (a, _) => not (Lib.mem a d) 1717 | NONE => true) 1718 val pl' = do_reg pl 1719 val p' = progSyntax.list_mk_star pl' 1720 val q' = progSyntax.list_mk_star (do_reg ql) 1721 val rwts = Lib.mapfilter (asm o Term.rand o fst) 1722 (regs pl') 1723 val asm_conv = Conv.QCONV (REWRITE_CONV rwts) 1724 in 1725 (Conv.CONV_RULE asm_conv 1726 (reg_rule (Thm.INST s thm)), 1727 mk (generate_temporal()) 1728 (p', Term.subst s c, 1729 utilsLib.rhsc (asm_conv q')): Term.term) 1730 end) groups 1731 end 1732 end 1733end 1734 1735(* ------------------------------------------------------------------------ 1736 spec 1737 1738 Generate a tool for proving theorems of the form 1739 1740 |- SPEC p c q 1741 1742 The goal is expected to be generated by mk_pre_post based on a 1743 step-theorem, which is in turn used to prove the goal. 1744 ------------------------------------------------------------------------ *) 1745 1746(* 1747val () = set_trace "Goalstack.print_goal_at_top" 0 1748val () = set_trace "Goalstack.print_goal_at_top" 1 1749val () = set_trace "stateLib.spec" 1 1750*) 1751 1752local 1753 val spec_debug = ref false 1754 val () = Feedback.register_btrace ("stateLib.spec", spec_debug) 1755 val PRINT_TAC = 1756 RULE_ASSUM_TAC (CONV_RULE PRINT_CONV) THEN CONV_TAC PRINT_CONV 1757 val WEAK_STRIP_TAC = DISCH_THEN (REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) 1758 val AND_IMP_INTRO_RULE = 1759 Conv.CONV_RULE (Conv.DEPTH_CONV Conv.AND_IMP_INTRO_CONV) 1760 fun is_ineq tys = 1761 fn thm => 1762 (thm |> Thm.concl 1763 |> boolSyntax.dest_neg 1764 |> boolSyntax.dest_eq |> fst 1765 |> Term.type_of 1766 |> Lib.C Lib.mem tys) 1767 handle HOL_ERR _ => false 1768 val ADDRESS_EQ_CONV = 1769 PURE_REWRITE_CONV [wordsTheory.WORD_EQ_ADD_LCANCEL, 1770 wordsTheory.WORD_ADD_INV_0_EQ] 1771 THENC (Conv.TRY_CONV wordsLib.word_EQ_CONV) 1772 fun UPDATE_TAC tys = 1773 fn thms => 1774 CONV_TAC 1775 (Conv.DEPTH_CONV 1776 (updateLib.UPDATE_APPLY_CONV 1777 (PURE_REWRITE_CONV (List.filter (is_ineq tys) thms) 1778 THENC ADDRESS_EQ_CONV))) 1779 val cond_STAR1 = CONJUNCT1 (Drule.SPEC_ALL set_sepTheory.cond_STAR) 1780 val STAR_ASSOC_CONV = 1781 Conv.REDEPTH_CONV (Conv.REWR_CONV (GSYM set_sepTheory.STAR_ASSOC)) 1782 val cond_STAR1_I = 1783 utilsLib.qm [cond_STAR1, combinTheory.I_THM] 1784 ``(set_sep$cond c * p) (s:'a set) = I c /\ p s`` 1785in 1786 fun spec imp_spec imp_temp read_thms write_thms select_state_thms frame_thms 1787 component_11 map_tys EXTRA_TAC STATE_TAC = 1788 let 1789 val sthms = cond_STAR1_I :: select_state_thms 1790 val pthms = [boolTheory.DE_MORGAN_THM, pred_setTheory.NOT_IN_EMPTY, 1791 pred_setTheory.IN_DIFF, pred_setTheory.IN_INSERT] 1792 val UPD_TAC = UPDATE_TAC map_tys 1793 val PRE_TAC = 1794 GEN_TAC 1795 \\ GEN_TAC 1796 \\ CONV_TAC 1797 (Conv.LAND_CONV 1798 (Conv.RATOR_CONV STAR_ASSOC_CONV 1799 THENC REWRITE_CONV (component_11 @ sthms @ pthms))) 1800 \\ WEAK_STRIP_TAC 1801 val POST_TAC = 1802 PURE_ASM_REWRITE_TAC write_thms 1803 \\ Tactical.REVERSE CONJ_TAC 1804 >- ( 1805 ASM_SIMP_TAC (pure_ss++simpLib.rewrites frame_thms) [] 1806 \\ ( 1807 REFL_TAC 1808 ORELSE (RW_TAC pure_ss frame_thms 1809 \\ (REFL_TAC ORELSE PRINT_TAC)) 1810 ) 1811 ) 1812 \\ CONV_TAC (Conv.RATOR_CONV STAR_ASSOC_CONV) 1813 (* For testing: 1814 val tac = ref ALL_TAC 1815 ASSUM_LIST (fn thms => (tac := UPD_TAC thms; ALL_TAC)) 1816 val update_TAC = !tac 1817 *) 1818 \\ ASSUM_LIST 1819 (fn thms => 1820 let 1821 val update_TAC = UPD_TAC thms 1822 in 1823 REPEAT 1824 ( 1825 ONCE_REWRITE_TAC sthms 1826 \\ CONJ_TAC 1827 >- ( 1828 STATE_TAC 1829 \\ update_TAC 1830 \\ ASM_REWRITE_TAC [boolTheory.COND_ID] 1831 ) 1832 \\ CONJ_TAC 1833 >- ASM_REWRITE_TAC (component_11 @ pthms) 1834 ) 1835 end 1836 ) 1837 \\ POP_ASSUM SUBST1_TAC 1838 \\ (REFL_TAC ORELSE ALL_TAC) 1839 val NEXT_TAC = 1840 RULE_ASSUM_TAC (PURE_REWRITE_RULE [combinTheory.I_THM]) 1841 \\ ASM_REWRITE_TAC read_thms 1842 \\ EXTRA_TAC 1843 \\ PRINT_TAC 1844 fun tac (v, dthm) = 1845 MATCH_MP_TAC (if generate_temporal () then imp_temp else imp_spec) 1846 \\ PRE_TAC 1847 \\ Tactic.EXISTS_TAC v 1848 \\ CONJ_TAC 1849 >- ( 1850 MATCH_MP_TAC dthm 1851 \\ NEXT_TAC 1852 ) 1853 \\ POST_TAC 1854 in 1855 fn (thm, t) => 1856 let 1857 val v = optionSyntax.dest_some (utilsLib.rhsc thm) 1858 val dthm = AND_IMP_INTRO_RULE (Drule.DISCH_ALL thm) 1859 in 1860 (* 1861 set_goal ([], t) 1862 *) 1863 prove (t, tac (v, dthm)) 1864 end 1865 handle e as HOL_ERR _ => 1866 (if !spec_debug 1867 then (proofManagerLib.set_goal ([], t); thm) 1868 else raise e) 1869 end 1870end 1871 1872(* ------------------------------------------------------------------------ *) 1873 1874end 1875