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