1 2functor vars_as_resourceFunctor (var_res_param : 3sig 4 include Abbrev; 5 6 val combinator_thmL : thm list 7 val predicate_ssfrag : int -> simpLib.ssfrag 8 val final_decision_procedure : thm list -> term -> thm; 9 val combinator_terms : term * term * term; 10 val resource_proccall_free_thmL : thm list 11 val inital_prop_rewrite_thmL : thm list 12 val abstrL : separationLogicLib.asl_program_abstraction list 13 val comments_step_convL : (conv->conv) list 14 val quantifier_heuristicsL : quantHeuristicsLib.quant_param list 15 val var_res_prop_implies___GENERATE : 16 (term list -> int -> (bool * simpLib.ssfrag) -> thm list -> term * term * term * term -> thm list) list 17 18 val hoare_triple_case_splitL : (term -> term) list 19 val frame_split_case_splitL : (term -> term) list 20 21 structure var_res_base : sig 22 include Abbrev; 23 24 val update_var_res_param : unit -> unit; 25 val var_res_prove : Abbrev.term -> Abbrev.thm 26 val var_res_prove___no_expn : Abbrev.term -> Abbrev.thm 27 val var_res_assumptions_prove : Abbrev.thm -> Abbrev.thm 28 val var_res_precondition_prove : Abbrev.thm -> Abbrev.thm 29 val var_res_precondition_assumption_prove : 30 Abbrev.term option -> Abbrev.thm -> Abbrev.thm 31 val raise_var_res_prove_expn : exn -> 'a 32 33 val COND_REWR_CONV : Abbrev.thm -> Abbrev.conv 34 val COND_REWRITE_CONV : bool -> Abbrev.thm list -> Abbrev.conv 35 val GUARDED_COND_REWRITE_CONV : bool -> (Abbrev.term -> bool) -> Abbrev.thm list -> Abbrev.conv 36 37 val VAR_RES_COND_HOARE_TRIPLE___PRECOND_CONV : conv -> conv 38 val VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV : conv -> conv 39 val VAR_RES_COND_HOARE_TRIPLE___FIND_RESORT_PRECOND_CONV : (term -> bool) -> conv 40 41 val var_res_prop___VAR_EQ_PROPAGATE : conv 42 val VAR_RES_COND_INFERENCE___CONST_INTRO___CONV : term -> string option -> term -> (bool * term * thm) 43 val VAR_RES_COND_INFERENCE___CONST_LIST_INTRO___CONV : (term * string option) list -> term -> thm 44 val VAR_RES_FRAME_SPLIT_INFERENCE___CONST_INTRO___CONV : term -> string option -> term -> thm 45 val VAR_RES_FRAME_SPLIT_INFERENCE___CONST_LIST_INTRO___CONV : (term * string option) list -> term -> thm 46 47 val var_res_prop_equal_unequal___NORMALISE_CONV : conv 48 val VAR_RES_PROP_REWRITE_CONV : (bool * simpLib.ssfrag) -> thm list -> term -> thm 49 val get_const_name_for_exp : string -> term -> string 50 51 val VAR_RES_COND_HOARE_TRIPLE___RESORT_PRECOND_CONV : int list -> conv 52 val var_res_prop___COND_RESORT_CONV : int list -> conv 53 54 val cond_rewrite___varlist_update : thm list -> conv 55 val GENERATE___var_res_exp_varlist_update___REWRITES : term -> term -> term -> (term * thm list) 56 val var_res_prop___var_res_prop_varlist_update___EVAL : term -> conv; 57 val VAR_RES_COND_INFERENCE___PRECOND_var_res_prop_varlist_update___EVAL : term -> conv 58 59 val BAG_NORMALISE_CONV : conv; 60 val VAR_RES_FRAME_SPLIT___imp_CONV : conv -> conv 61 val VAR_RES_FRAME_SPLIT___split_CONV : conv -> conv 62 val VAR_RES_FRAME_SPLIT___context_CONV : conv -> conv 63 val VAR_RES_FRAME_SPLIT___context_split_imp_CONV : conv -> conv 64 val VAR_RES_FRAME_SPLIT___PROP_CONV : conv -> conv 65 66 type var_res_inference_param = 67 {fast : bool, 68 do_prop_simps : bool, 69 prop_simp_ss : simpLib.ssfrag, 70 expands_level : int}; 71 72 type var_res_inference = var_res_inference_param -> thm list -> ConseqConv.directed_conseq_conv 73 74 val no_context_conseq_conv : ConseqConv.directed_conseq_conv -> var_res_inference; 75 val no_context_strengthen_conseq_conv : conv -> var_res_inference; 76 val context_strengthen_conseq_conv : (thm list -> conv) -> var_res_inference; 77 val simpset_strengthen_conseq_conv : ((bool * simpLib.ssfrag) -> thm list -> conv) -> var_res_inference; 78 val simpset_no_context_strengthen_conseq_conv : ((bool * simpLib.ssfrag) -> conv) -> var_res_inference; 79 val expands_strengthen_conseq_conv : (int -> (bool * simpLib.ssfrag) -> thm list -> conv) -> var_res_inference; 80 end 81 82 val INFERENCES_LIST___simulate_command : (string * var_res_base.var_res_inference) list 83 val INFERENCES_LIST___simulate_minor_command : (string * var_res_base.var_res_inference) list 84 val INFERENCES_LIST___expensive_simplifications : (string * var_res_base.var_res_inference) list 85 val INFERENCES_LIST___entailment_steps : (string * var_res_base.var_res_inference) list 86 87 val VAR_RES_IS_PURE_PROPOSITION___provers : (term -> term -> thm) list 88end) : 89sig 90 type var_res_inference_group = 91 (* group name (used for debug) *) 92 string * 93 (* group guard, inferences are just applied to 94 terms that satisfy this guard *) 95 (Abbrev.term -> bool) * 96 (* apply before working on subterms *) 97 bool * 98 (* use this inference group to clean up after a "bigger" step *) 99 bool * 100 (* the members of the group, each with a name for debugging *) 101 (string * var_res_param.var_res_base.var_res_inference) list; 102 103 type user_rewrite_param = (Abbrev.thm list * Abbrev.conv list * simpLib.ssfrag list); 104 type gen_step_param = {use_asms : bool, 105 do_case_splits : bool, 106 expands_level : int, 107 generate_vcs : bool, 108 fast : bool, 109 stop_evals : (Abbrev.term -> bool) list, 110 prop_simp_level: int, 111 inferences : (int * var_res_inference_group) list * 112 (int * var_res_inference_group) list * 113 (int * var_res_inference_group) list}; 114 115 datatype gen_step_tac_opt = 116 case_splits_flag of bool 117 | expands_level of int 118 | fast_flag of bool 119 | prop_simp_level of int 120 | use_asms_flag of bool 121 | generate_vcs_flag of bool 122 | add_rewrites of Abbrev.thm list 123 | add_convs of Abbrev.conv list 124 | add_ssfrags of simpLib.ssfrag list 125 | stop_evals of (Abbrev.term -> bool) list 126 | combined_gen_step_tac_opt of gen_step_tac_opt list 127 | add_inference_groups of (int * var_res_inference_group) list * 128 (int * var_res_inference_group) list * 129 (int * var_res_inference_group) list; 130 131 val no_case_splits : gen_step_tac_opt; 132 val do_case_splits : gen_step_tac_opt; 133 val no_expands : gen_step_tac_opt; 134 val do_expands : gen_step_tac_opt; 135 val full_expands : gen_step_tac_opt; 136 val no_case_split_expands : gen_step_tac_opt; 137 val generate_vcs : gen_step_tac_opt; 138 val dont_generate_vcs : gen_step_tac_opt; 139 val no_asms : gen_step_tac_opt; 140 val use_asms : gen_step_tac_opt; 141 val no_prop_simps : gen_step_tac_opt; 142 val simple_prop_simps : gen_step_tac_opt; 143 val conservative : gen_step_tac_opt; (* not fast *) 144 val careful : gen_step_tac_opt; (* no asms. no case splits, no expands *) 145 val stop_at_cond : gen_step_tac_opt; 146 val stop_at_while : gen_step_tac_opt; 147 val stop_at_abstraction : gen_step_tac_opt; 148 val stop_at_frame_calc : gen_step_tac_opt; 149 val stop_at_hoare_triple : gen_step_tac_opt; 150 val stop_at_block_spec : gen_step_tac_opt; 151 152 val gen_step_param___update_use_asms : gen_step_param -> bool -> gen_step_param 153 val gen_step_param___update_cs : gen_step_param -> bool -> gen_step_param 154 val gen_step_param___update_vcs : gen_step_param -> bool -> gen_step_param 155 val gen_step_param___update_expands : gen_step_param -> int -> gen_step_param 156 val gen_step_param___update_fast : gen_step_param -> bool -> gen_step_param 157 val gen_step_param___update_prop_simps : gen_step_param -> int -> gen_step_param 158 val gen_step_param___update_stop_evals : gen_step_param -> (Abbrev.term -> bool) list -> gen_step_param 159 val gen_step_param___update_inferences : gen_step_param -> ( 160 (int * var_res_inference_group) list * 161 (int * var_res_inference_group) list * 162 (int * var_res_inference_group) list) -> gen_step_param 163 164 val gen_step_param___add_inferences : gen_step_param -> ( 165 (int * var_res_inference_group) list * 166 (int * var_res_inference_group) list * 167 (int * var_res_inference_group) list) -> gen_step_param 168 169 val VAR_RES_GEN_STEP_CONSEQ_CONV : gen_step_param -> user_rewrite_param -> int option -> int -> Abbrev.thm list -> Abbrev.conv 170 val VAR_RES_GEN_STEP_TAC : gen_step_param -> user_rewrite_param -> int option -> int -> Abbrev.tactic 171 val xVAR_RES_GEN_STEP_CONSEQ_CONV: gen_step_tac_opt list -> int option -> int -> Abbrev.conv 172 val xVAR_RES_GEN_STEP_TAC : gen_step_tac_opt list -> int option -> int -> Abbrev.tactic 173 174 val VAR_RES_PURE_VC_TAC : Abbrev.tactic; 175 val VAR_RES_ELIM_COMMENTS_TAC : Abbrev.tactic 176 val VAR_RES_VC_TAC : Abbrev.tactic; 177 val VAR_RES_SPECIFICATION___CONSEQ_CONV : ConseqConv.conseq_conv 178 val VAR_RES_SPECIFICATION_TAC : Abbrev.tactic 179 val VAR_RES_ENTAILMENT_INIT___CONSEQ_CONV : ConseqConv.conseq_conv 180 val VAR_RES_ENTAILMENT_INIT_TAC : Abbrev.tactic 181end = 182struct 183 184(* 185quietdec := true; 186loadPath := 187 (Globals.HOLDIR ^ "/examples/separationLogic/src") :: 188 (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot") :: 189 !loadPath; 190 191show_assums := true; 192*) 193 194open HolKernel Parse boolLib bossLib; 195open generalHelpersTheory finite_mapTheory pred_setTheory 196 listTheory rich_listTheory pairTheory bagTheory 197open separationLogicTheory 198open separationLogicSyntax 199open vars_as_resourceSyntax 200open vars_as_resourceTheory 201open vars_as_resourceSyntax 202open quantHeuristicsLib 203open quantHeuristicsLibBase 204open ConseqConv 205open bagLib 206open separationLogicLib 207open Profile 208 209 210(* 211quietdec := false; 212*) 213 214(******************************************************************************) 215(* Get everything from base *) 216(******************************************************************************) 217 218open var_res_param.var_res_base; 219 220 221(******************************************************************************) 222(* Parameters *) 223(******************************************************************************) 224val verbose_level = ref 0 225val verbose_level_try = ref 0 226fun do_profile_ref () = ref (Profile.profile_with_exn) 227 228 229val _ = Feedback.register_trace ("holfoot verbose level", verbose_level, 6) 230val _ = Feedback.register_trace ("holfoot verbose level try", verbose_level_try, 6) 231 232(******************************************************************************) 233(* COND_PROP___STRONG_EXIST *) 234(******************************************************************************) 235 236fun COND_PROP___STRONG_EXISTS_NORMALISE_CONV___internally is_rec tt = 237let 238 val (v1, _) = dest_COND_PROP___STRONG_EXISTS tt handle HOL_ERR _ => raise UNCHANGED; 239 val thm0 = RAND_CONV pairTools.PABS_ELIM_CONV tt handle UNCHANGED => REFL tt; 240 val body = (snd o pairSyntax.dest_pabs o rand o rhs o concl) thm0 241in 242 if not (is_COND_PROP___STRONG_EXISTS body) then 243 if is_rec then (v1,thm0) else raise UNCHANGED 244 else let 245 val (v2, thm1) = COND_PROP___STRONG_EXISTS_NORMALISE_CONV___internally true body; 246 val thm2 = CONV_RULE ((RHS_CONV o RAND_CONV o ABS_CONV) (K thm1)) thm0; 247 val thm3 = CONV_RULE (RHS_CONV (HO_REWR_CONV COND_PROP___STRONG_EXISTS___UNION)) thm2; 248 in 249 (pairSyntax.mk_pair (v1,v2), thm3) 250 end 251end; 252 253fun COND_PROP___STRONG_EXISTS_NORMALISE_CONV tt = 254let 255 val (vc, thm0) = COND_PROP___STRONG_EXISTS_NORMALISE_CONV___internally false tt 256 val thm1 = CONV_RULE (RHS_CONV (RAND_CONV (pairTools.PABS_INTRO_CONV vc))) thm0 257in 258 thm1 259end handle HOL_ERR _ => raise UNCHANGED; 260 261 262fun COND_PROP___STRONG_EXISTS_INTRO___CONV ttt = 263let 264 val (vp, _) = dest_COND_PROP___STRONG_EXISTS ttt 265 val thm = (RAND_CONV (pairTools.PABS_ELIM_CONV)) ttt handle UNCHANGED => REFL ttt 266in 267 ((SOME vp), thm) 268end handle HOL_ERR _ => 269let 270 val v = genvar (Type `:unit`) 271 val thm_term = mk_icomb (COND_PROP___STRONG_EXISTS_term, mk_abs(v, ttt)) 272in 273 (NONE, 274 GSYM ((REWR_CONV COND_PROP___STRONG_EXISTS___ELIM) thm_term)) 275end; 276 277fun COND_PROP___STRONG_EXISTS_ELIM___CONV NONE ttt = 278 REWR_CONV COND_PROP___STRONG_EXISTS___ELIM ttt 279| COND_PROP___STRONG_EXISTS_ELIM___CONV (SOME vp) ttt = 280 (RAND_CONV (pairTools.PABS_INTRO_CONV vp)) ttt 281 282 283 284(****************************************************************) 285(* check that no proccalls and resources are used *) 286(****************************************************************) 287 288exception resource_and_proccall_free_PROVE___failed_expn of term * term option; 289 290(* 291val exp = (intro_cond_hoare_triple thm; UNCHANGED) handle x => x 292val exp = 293 (e HOLFOOT_SPECIFICATION_TAC; UNCHANGED) handle x => x; 294 295val resource_and_proc_call_free_PROVE___failed_expn(_, tt, _) = exp 296*) 297 298val resource_and_proccall_free_CONV = 299 EXT_CONSEQ_REWRITE_CONV 300 [K (DEPTH_CONV BETA_CONV)] [EVERY_DEF] 301 ([], append (var_res_param.resource_proccall_free_thmL) 302 [asl_prog_IS_RESOURCE_AND_PROCCALL_FREE___ASL_REWRITES, 303 asl_prog_IS_RESOURCE_AND_PROCCALL_FREE___VAR_RES_REWRITES], 304 []) CONSEQ_CONV_STRENGTHEN_direction; 305 306 307fun resource_and_proccall_free_PROVE tt = 308 let 309 val thm = resource_and_proccall_free_CONV tt 310 in 311 (MP thm TRUTH handle HOL_ERR _ => 312 raise resource_and_proccall_free_PROVE___failed_expn (tt, SOME 313 ((fst o dest_imp o concl) thm))) 314 end handle HOL_ERR _ => 315 raise resource_and_proccall_free_PROVE___failed_expn (tt, NONE); 316 317 318 319val proc_call_free_CONV = REWRITE_CONV [ 320 REWRITE_RULE [asl_prog_IS_RESOURCE_AND_PROCCALL_FREE___ALTERNATIVE_DEF] 321 asl_prog_IS_RESOURCE_AND_PROCCALL_FREE___var_res_bla]; 322 323 324(*************************************************************** 325 * Eliminate program abstractions and use hoare triples 326 ****************************************************************) 327 328fun ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_quant_bla_CONV tt = 329let 330 val (xenv,penv,prog,abst) = dest_ASL_PROGRAM_IS_ABSTRACTION tt 331 val (qP, qQ) = dest_var_res_prog_quant_best_local_action abst 332 333 val thm0 = ISPECL [xenv,penv,qP,prog,qQ] ASL_PROGRAM_IS_ABSTRACTION___var_res_quant_best_local_action 334 val thm1 = var_res_precondition_prove thm0 335 336 val (var_const, _) = pairSyntax.dest_pabs qP; 337 338 val thm2 = CONV_RULE (RHS_CONV (PairRules.GEN_PALPHA_CONV var_const)) thm1 339 val thm3 = CONV_RULE (RHS_CONV (DEPTH_CONV PairRules.PBETA_CONV)) thm2 handle UNCHANGED => thm2 340in 341 thm3 342end handle HOL_ERR _ => raise UNCHANGED; 343 344 345val LIST_UNROLL_GIVEN_ELEMENT_NAMES_term = Term `LIST_UNROLL_GIVEN_ELEMENT_NAMES:'a list -> label list -> bool`; 346val LIST_UNROLL_GIVEN_ELEMENT_NAMES___UNROLL_NULL = CONJUNCT1 LIST_UNROLL_GIVEN_ELEMENT_NAMES___UNROLL 347val LIST_UNROLL_GIVEN_ELEMENT_NAMES___UNROLL_CONS = CONJUNCT2 LIST_UNROLL_GIVEN_ELEMENT_NAMES___UNROLL 348 349local 350fun LIST_UNROLL_GIVEN_ELEMENT_NAMES_CONV_int tt = 351let 352 val (fun_term, argL) = strip_comb tt; 353 val _ = if (same_const fun_term LIST_UNROLL_GIVEN_ELEMENT_NAMES_term) andalso 354 (length argL = 2) then () else raise UNCHANGED; 355 val (x, xL) = (el 1 argL, el 2 argL); 356in 357 if (not (listSyntax.is_cons xL)) then 358 ISPEC x LIST_UNROLL_GIVEN_ELEMENT_NAMES___UNROLL_NULL 359 else 360 let 361 val (h,L) = listSyntax.dest_cons xL 362 val thm = ISPECL [x,h,L] LIST_UNROLL_GIVEN_ELEMENT_NAMES___UNROLL_CONS; 363 val new_name = fst (dest_var (fst (listSyntax.dest_cons xL))); 364 val thm2 = CONV_RULE (RHS_CONV (RENAME_VARS_CONV [new_name])) thm 365 366 367 val thm3 = CONV_RULE ((RHS_CONV o STRIP_QUANT_CONV o RAND_CONV) ( 368 (LIST_UNROLL_GIVEN_ELEMENT_NAMES_CONV_int))) thm2 369 370 val thm4 = CONV_RULE (RHS_CONV (STRIP_QUANT_CONV ( 371 REPEATC (STRIP_QUANT_CONV ( 372 RIGHT_AND_EXISTS_CONV))))) thm3 373 in 374 thm4 375 end 376end; 377in 378fun LIST_UNROLL_GIVEN_ELEMENT_NAMES_CONV tt = 379 CONV_RULE (RHS_CONV (DEPTH_CONV Unwind.UNWIND_EXISTS_CONV)) 380 (LIST_UNROLL_GIVEN_ELEMENT_NAMES_CONV_int tt) 381end; 382 383(* 384 val tref = ref [T] 385 val _ = tref := [] 386 val tt = (el (length (!tref)) (!tref)) 387 val tt = find_term is_var_res_prop_internal ((rhs o concl) thm1) 388 val tt = find_term 389 (fn t => is_ASL_PROGRAM_IS_ABSTRACTION (snd (strip_forall t))) 390 (concl current_theorem) 391 392current_theorem 393*) 394local 395 fun add_vars thm0 vs = 396 let 397 val xthm0 = CONV_RULE (RHS_CONV ( 398 pairTools.ELIM_TUPLED_QUANT_CONV)) thm0 399 handle UNCHANGED => thm0 400 | HOL_ERR _ => thm0; 401 val xthm1 = foldr (fn (v, thm) => PairRules.PFORALL_EQ v thm) xthm0 vs 402 in 403 xthm1 404 end; 405 406 val elim_names_wrapper_CONV = 407 let 408 val conv1 = REWRITE_CONV [pairTheory.FST, pairTheory.SND, 409 var_res_prop_input_ap_def, VAR_RES_HOARE_TRIPLE___comment___ELIM_preserve_names] 410 411 412 val elim_UNROLL_CONV = 413 let 414 val xconv1 = STRIP_QUANT_CONV 415 ((RATOR_CONV o RAND_CONV) LIST_UNROLL_GIVEN_ELEMENT_NAMES_CONV) THENC 416 (REPEATC (STRIP_QUANT_CONV LEFT_IMP_EXISTS_CONV)) 417 418 val xconv2 = RESORT_FORALL_CONV (fn l => (tl l) @ [hd l]) 419 val xconv3 = LAST_FORALL_CONV (HO_PART_MATCH lhs 420 UNWIND_FORALL_THM2) 421 in 422 xconv1 THENC xconv2 THENC xconv3 423 end; 424 425 val cs = computeLib.bool_compset (); 426 val _ = computeLib.add_thms [ 427 listTheory.HD, 428 listTheory.TL] cs 429 430 val conv2 = DEPTH_CONV PairRules.PBETA_CONV 431 val conv3 = computeLib.CBV_CONV cs 432 in 433 conv1 THENC elim_UNROLL_CONV THENC elim_UNROLL_CONV THENC conv2 THENC conv3 434 end; 435 436 fun intro_cond_hoare_triple thm = 437 let 438 val triple_term = (snd o strip_forall o rhs) (concl thm) 439 val xthm1 = PART_MATCH (lhs o rand) VAR_RES_COND_HOARE_TRIPLE_INTRO triple_term; 440 val precond = (fst o dest_imp) (concl xthm1) 441 val (precond1, precond2) = dest_conj precond; 442 val precond1_thm = resource_and_proccall_free_PROVE precond1 443 val precond2_thm = var_res_prove precond2 444 val precond_thm = CONJ precond1_thm precond2_thm 445 val xthm2 = MP xthm1 precond_thm 446 447 val xthm3 = (CONV_RULE 448 ((RHS_CONV o STRIP_QUANT_CONV) 449 (K xthm2))) thm 450 in 451 xthm3 452 end; 453 454in 455 456fun ASL_PROGRAM_IS_ABSTRACTION___forall_comment_var_res_prog_quant_bla_CONV tt = 457let 458 val (vs,body) = strip_forall tt; 459 val _ = if (null vs) then raise UNCHANGED else (); 460 461 (*to VAR_RES_HOARE_TRIPLE*) 462 val thm0 = ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_quant_bla_CONV body; 463 464 (*add vars again*) 465 val thm1 = add_vars thm0 vs; 466 467 (*elim procedure-call-preserve-names wrapper*) 468 val thm2 = CONV_RULE (RHS_CONV elim_names_wrapper_CONV) thm1; 469 470 (*introduce hoare triples *) 471 val thm3 = intro_cond_hoare_triple thm2 472in 473 thm3 474end handle HOL_ERR _ => raise UNCHANGED; 475 476end 477 478 479(******************************************************************************) 480(* transform var_res_prop_input ... *) 481(* *) 482(* *) 483(******************************************************************************) 484 485 486(* 487val tref = ref T; 488val ttt = !tref 489*) 490 491val all_distinct_cs = computeLib.bool_compset (); 492val _ = computeLib.add_thms [listTheory.ALL_DISTINCT, 493 listTheory.MEM] all_distinct_cs; 494val ALL_DISTINCT_EXPAND_CONV = 495 computeLib.CBV_CONV all_distinct_cs 496 497 498 499(* 500 val var_res_prop_internal___ELIM_CONV___failed_expn ttt = expn 501 val ttt = rhs (concl thm1) 502*) 503local 504 val asl_star___PROPS1 = var_res_precondition_prove ( 505 ISPEC (#1 var_res_param.combinator_terms) asl_star___PROPERTIES___EVAL) 506 val asl_star___PROPS2 = var_res_precondition_prove ( 507 ISPEC (#3 var_res_param.combinator_terms) asl_star___PROPERTIES___EVAL) 508 509 val cond_conv0 = REWRITE_CONV (append var_res_param.inital_prop_rewrite_thmL 510 [asl_star___PROPS1, asl_star___PROPS2]); 511 512 513 val cond_conv1a = (COND_REWRITE_CONV true [var_res_prop_internal___VARS_TO_BAGS]) 514 val cond_conv1b = (COND_REWR_CONV var_res_prop_internal___VARS_TO_BAGS___END) 515 val cond_conv1 = cond_conv1a THENC cond_conv1b 516 517 518 val cond_conv2a = (COND_REWRITE_CONV true [var_res_prop_internal___PROP_TO_BAG]) 519 val cond_conv2b = (COND_REWR_CONV var_res_prop_internal___PROP_TO_BAG___END) 520 val cond_conv2 = cond_conv2a THENC cond_conv2b 521in 522 523exception var_res_prop_internal___ELIM_CONV___failed_expn of term; 524fun var_res_prop_internal___ELIM_CONV ttt = 525if not (is_var_res_prop_internal ttt) then raise UNCHANGED else 526(let 527 val thm0 = ALL_DISTINCT_EXPAND_CONV ttt handle UNCHANGED => REFL ttt; 528 529 (*elim exists*) 530 val thm1 = RHS_CONV_RULE ( 531 Ho_Rewrite.REWRITE_CONV [var_res_prop_internal___EXISTS]) thm0; 532 533 (*find subterm to continue with*) 534 val ttt' = find_term is_var_res_prop_internal ((rhs o concl) thm1) 535 536 (*bring props in normal form*) 537 val thm1a = cond_conv0 ttt' handle UNCHANGED => REFL ttt'; 538 539 (*move vars to bag*) 540 val thm2 = RHS_CONV_RULE cond_conv1 thm1a; 541 542 (*move props to bag*) 543 val thm3 = RHS_CONV_RULE cond_conv2 thm2; 544 545 (*final step*) 546 val thm4 = RHS_CONV_RULE 547 (REWR_CONV (GSYM var_res_prop_def)) thm3; 548 549 (*prove assumptions*) 550 val thm5 = var_res_assumptions_prove thm4; 551 552 553 (*combine again*) 554 val thm6 = RHS_CONV_RULE (ONCE_REWRITE_CONV [thm5]) thm1 555 556in 557 thm6 558end handle Interrupt => raise Interrupt 559 | _ => raise (var_res_prop_internal___ELIM_CONV___failed_expn ttt)); 560 561end 562 563exception var_res_prop_input_distinct___ELIM_CONV___failed_expn of term; 564fun var_res_prop_input_distinct___ELIM_CONV a_opt tt = 565if not (is_var_res_prop_input_distinct tt) then raise UNCHANGED else 566(let 567 val thm0 = PART_MATCH (lhs o snd o dest_imp) var_res_prop_input_distinct___REWRITE tt 568 val thm1 = var_res_precondition_assumption_prove a_opt thm0 569 val thm2 = RHS_CONV_RULE (DEPTH_CONV (var_res_prop_internal___ELIM_CONV)) thm1 570in 571 thm2 572end handle Interrupt => raise Interrupt 573 | var_res_prop_internal___ELIM_CONV___failed_expn ttt => 574 raise var_res_prop_internal___ELIM_CONV___failed_expn ttt 575 | _ => raise (var_res_prop_input_distinct___ELIM_CONV___failed_expn tt)); 576 577 578 579(*************************************************************** 580 * PROGRAM ABSTRACTION 581 ****************************************************************) 582 583(* 584fun sys xenv penv t = SOME (prove_ASL_PROGRAM_ABSTRACTION_REFL xenv penv t) 585 586val t = ``ASL_PROGRAM_IS_ABSTRACTION xenv penv (var_res_prog_local_var (\v. body v 2))``; 587val xenv = el 1 (snd (strip_comb t)); 588val penv = el 2 (snd (strip_comb t)); 589val p = el 3 (snd (strip_comb t)); 590 591*) 592fun ASL_PROGRAM_ABSTRACTION___local_var pf abstL sys xenv penv p = 593 let 594 val (v, body) = dest_var_res_prog_local_var p 595 596 (*search abstraction*) 597 val body_thm_opt = sys xenv penv body; 598 val body_thm = if (isSome body_thm_opt) then valOf body_thm_opt else raise UNCHANGED; 599 val thm = GEN_ASSUM v body_thm 600 601 val thm0 = ISPECL [xenv, penv] ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_local_var___CONG 602 val thm1 = HO_MATCH_MP thm0 thm; 603 in 604 SOME thm1 605 end; 606 607 608(* 609fun sys xenv penv t = SOME (prove_ASL_PROGRAM_ABSTRACTION_REFL xenv penv t) 610 611val t = ``ASL_PROGRAM_IS_ABSTRACTION xenv penv (var_res_prog_call_by_value_arg (\v. body v 2) c)``; 612val xenv = el 1 (snd (strip_comb t)); 613val penv = el 2 (snd (strip_comb t)); 614val p = el 3 (snd (strip_comb t)); 615 616*) 617fun ASL_PROGRAM_ABSTRACTION___call_by_value_arg pf abstL sys xenv penv p = 618 let 619 val (c, v, body) = dest_var_res_prog_call_by_value_arg p 620 621 (*search abstraction*) 622 val body_thm_opt = sys xenv penv body; 623 val body_thm = if (isSome body_thm_opt) then valOf body_thm_opt else raise UNCHANGED; 624 val thm = GEN_ASSUM v body_thm 625 626 val thm0 = ISPECL [xenv,penv,c] ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_call_by_value_arg___CONG 627 val thm1 = HO_MATCH_MP thm0 thm; 628 in 629 SOME thm1 630 end; 631 632 633 634 635(* 636fun sys xenv penv t = SOME (prove_ASL_PROGRAM_ABSTRACTION_REFL xenv penv t) 637 638val t = ``ASL_PROGRAM_IS_ABSTRACTION 639 (HOLFOOT_SEPARATION_COMBINATOR, 640 LIST_TO_FUN (VAR_RES_LOCK_ENV_MAP DISJOINT_FMAP_UNION [])) penv 641 ((asl_prog_procedure_call "merge" ([EL 0 arg_refL],constL)):holfoot_program)`` 642val xenv = el 1 (snd (strip_comb t)); 643val penv = el 2 (snd (strip_comb t)); 644val p = el 3 (snd (strip_comb t)); 645*) 646 647fun ASL_PROGRAM_ABSTRACTION___eval_expressions pf abstL sys xenv penv p = 648 let 649 val (abs_body, expL) = dest_var_res_prog_eval_expressions p 650 val (v, body) = dest_abs abs_body; 651 652 (*search abstraction*) 653 val body_thm_opt = sys xenv penv body; 654 val body_thm = if (isSome body_thm_opt) then valOf body_thm_opt else raise UNCHANGED; 655 val thm = GEN_ASSUM v body_thm 656 657 val thm0 = ISPECL [xenv,penv,expL] ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_eval_expressions; 658 val thm1 = HO_MATCH_MP thm0 thm; 659 in 660 SOME thm1 661 end; 662 663 664 665(* 666val t = ``ASL_PROGRAM_IS_ABSTRACTION 667 (HOLFOOT_SEPARATION_COMBINATOR, 668 LIST_TO_FUN (VAR_RES_LOCK_ENV_MAP DISJOINT_FMAP_UNION [])) penv 669 ((var_res_prog_procedure_call "merge" ([EL 0 arg_refL],constL)):holfoot_program)`` 670 671val xenv = el 1 (snd (strip_comb t)); 672val penv = el 2 (snd (strip_comb t)); 673val p = el 3 (snd (strip_comb t)); 674val abstL = BODY_CONJUNCTS (ASSUME proc_abst_t) 675val sys = ASL_PROGRAM_ABSTRACTION___match abstL (); 676 677val t_opt = ref [] 678val (abstL, sys, xenv,penv,p) = el 3 (!t_opt) 679*) 680 681fun ASL_PROGRAM_ABSTRACTION___var_res_prog_procedure_call pf abstL sys xenv penv p = 682 let 683 val (name, args) = dest_var_res_prog_procedure_call p handle HOL_ERR _ => raise UNCHANGED; 684 val thm0 = ISPECL [xenv,penv,name,args] ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_procedure_call 685 686 (*search abstraction*) 687 val precond = (fst o dest_imp o snd o dest_forall) (concl thm0) 688 val (v,p1) = (I ## rator) (dest_forall precond); 689 690 val p1_thm = GEN v 691 (tryfind (fn thm => (PART_MATCH rator thm p1)) abstL) 692 handle HOL_ERR _ => raise UNCHANGED; 693 694 val thm1 = HO_MATCH_MP thm0 p1_thm; 695 696 (*intro abstraction comment*) 697 val c = term_to_string (pf p) 698 val thm2 = CONV_RULE (RAND_CONV (asl_comment_abstraction_INTRO_CONV c)) thm1 699 700 in 701 SOME thm2 702 end 703 704 705 706(* 707val t = ``ASL_PROGRAM_IS_ABSTRACTION 708 (HOLFOOT_SEPARATION_COMBINATOR, 709 LIST_TO_FUN (VAR_RES_LOCK_ENV_MAP DISJOINT_FMAP_UNION [])) penv 710 ((var_res_prog_procedure_call "merge" ([EL 0 arg_refL],constL)):holfoot_program)`` 711 712val xenv = el 1 (snd (strip_comb t)); 713val penv = el 2 (snd (strip_comb t)); 714val p = el 3 (snd (strip_comb t)); 715val abstL = BODY_CONJUNCTS (ASSUME proc_abst_t) 716val sys = ASL_PROGRAM_ABSTRACTION___match abstL (); 717 718val t_opt = ref NONE 719val SOME (abstL, xenv,penv,p) = !t_opt 720val combinatorRWL = [IS_VAR_RES_COMBINATOR___holfoot_separation_combinator, 721 GET_VAR_RES_COMBINATOR___holfoot_separation_combinator, 722 ] 723 724exception my_pointer_exp; 725*) 726 727fun ASL_PROGRAM_ABSTRACTION___var_res_prog_parallel_procedure_call pf abstL sys xenv penv p = 728 let 729 val (name1, args1, name2, args2) = dest_var_res_prog_parallel_procedure_call p handle HOL_ERR _ => raise UNCHANGED; 730 731 val thm0 = ISPECL [xenv,penv,args1,args2,name1,name2] 732 ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_parallel_procedure_call 733 734 (*elim combinator precond*) 735 val thm1 = var_res_precondition_prove thm0 736 737 738 (*find abstractions*) 739 val precond = (fst o dest_imp o snd o strip_forall) (concl thm1) 740 val (v1,p1) = (I ## rator) ((dest_forall o fst o dest_conj) precond); 741 val (v2,p2) = (I ## rator) ((dest_forall o snd o dest_conj) precond); 742 743 val p1_thm = GEN v1 744 (tryfind (fn thm => (PART_MATCH rator thm p1)) abstL) 745 handle HOL_ERR _ => raise UNCHANGED; 746 747 val p2_thm = GEN v2 748 (tryfind (fn thm => (PART_MATCH rator thm p2)) abstL) 749 handle HOL_ERR _ => raise UNCHANGED; 750 751 752 val precond_thm = CONV_RULE (DEPTH_CONV pairLib.GEN_BETA_CONV) 753 (CONJ p1_thm p2_thm) 754 755 val thm2 = HO_MATCH_MP thm1 precond_thm; 756 757 val thm3 = REWRITE_RULE [pairTheory.FST, pairTheory.SND] thm2 758 759 (*intro abstraction comment*) 760 val c = "("^(term_to_string (pf p))^")"; 761 val thm4 = CONV_RULE (RAND_CONV (asl_comment_abstraction_INTRO_CONV c)) thm3 762 in 763 SOME thm4 764 end 765 766 767 768(* 769val t = ``ASL_PROGRAM_IS_ABSTRACTION 770 (HOLFOOT_SEPARATION_COMBINATOR, 771 LIST_TO_FUN (VAR_RES_LOCK_ENV_MAP DISJOINT_FMAP_UNION [])) penv 772 ((var_res_prog_procedure_call "merge" ([EL 0 arg_refL],constL)):holfoot_program)`` 773 774val xenv = el 1 (snd (strip_comb t)); 775val penv = el 2 (snd (strip_comb t)); 776val p = el 3 (snd (strip_comb t)); 777val abstL = BODY_CONJUNCTS (ASSUME proc_abst_t) 778val sys = ASL_PROGRAM_ABSTRACTION___match abstL (); 779 780val t_opt = ref NONE 781 782val _ = t_opt := SOME (abstL, sys, xenv,penv,p); 783val SOME (abstL, sys, xenv,penv,p) = !t_opt 784val combinatorRWL = [IS_VAR_RES_COMBINATOR___holfoot_separation_combinator, 785 GET_VAR_RES_COMBINATOR___holfoot_separation_combinator] 786*) 787 788val critical_section_cs = computeLib.bool_compset (); 789val _ = computeLib.add_thms [listTheory.MAP, pairTheory.FST, 790 listTheory.ALL_DISTINCT, 791 listTheory.MEM] critical_section_cs; 792val _ = computeLib.add_conv (Term `($=):'a -> 'a -> bool`, 2, stringLib.string_EQ_CONV) critical_section_cs; 793 794fun ASL_PROGRAM_ABSTRACTION___var_res_cond_critical_section pf abstL sys xenv penv p = 795 let 796 val (res, cond, body) = dest_asl_prog_cond_critical_section p handle HOL_ERR _ => raise UNCHANGED; 797 798 (*destruct the xenv*) 799 val (_, lock_env) = pairLib.dest_pair xenv; 800 val lock_decls = rand (snd (dest_comb lock_env)) 801 802 val (wpL,P) = 803 (pairSyntax.dest_pair o snd o pairSyntax.dest_pair) ( 804 first (fn tt => 805 (fst (pairSyntax.dest_pair tt) = res)) 806 (fst (listSyntax.dest_list lock_decls))) 807 808 val thm0 = ISPECL [ 809 #2 var_res_param.combinator_terms, 810 #1 var_res_param.combinator_terms, 811 lock_decls, penv, res, cond, body, wpL, P] 812 ASL_PROGRAM_IS_ABSTRACTION___asl_prog_cond_critical_section___lock_decls_env___INTERNAL 813 814 815 (*elim preconds*) 816 val thm1a = var_res_precondition_prove thm0 817 val precond = (fst o dest_imp) (concl thm1a) 818 val precond_thm = EQT_ELIM (computeLib.CBV_CONV critical_section_cs precond) 819 val thm1 = MP thm1a precond_thm 820 821 (*normalise var_res_prop_input*) 822 val i_t = (rand o rand o rator o rand o rand o concl) thm1; 823 val wpL_t = (fst o dest_pair o rand o rator) i_t; 824 val wpL_thm = REWRITE_CONV [LIST_TO_SET_THM] wpL_t; 825 826 val i_thm = ((REWR_CONV var_res_prop_input_def) THENC 827 ((RATOR_CONV o RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 828 (K wpL_thm)) THENC 829 (var_res_prop_input_distinct___ELIM_CONV NONE)) i_t 830 831 (*use it to simplify aquire*) 832 val a_t = (rand o rator o rand o rand o concl) thm1; 833 val a_thm0 = RAND_CONV (K i_thm) a_t 834 val a_thm1 = PART_MATCH (lhs o snd o dest_imp) 835 var_res_prog_aquire_lock___INTRO (rhs (concl a_thm0)) 836 val a_thm2 = CONV_RULE ((RAND_CONV o LHS_CONV) (K (GSYM a_thm0))) a_thm1 837 838 val set_eq_precond = (fst o dest_imp o concl) a_thm2 839 val set_eq_precond_thm = EQT_ELIM (REWRITE_CONV [LIST_TO_SET_THM, SET_OF_BAG_INSERT, 840 BAG_OF_EMPTY, SET_EQ_SUBSET, SUBSET_REFL, 841 INSERT_SUBSET, IN_INSERT, NOT_IN_EMPTY, EMPTY_SUBSET] set_eq_precond) handle e => 842 (print "!!!could not prove set_eq_precond!"; raise e) 843 val a_thm3 = MP a_thm2 set_eq_precond_thm 844 val res_s = stringLib.fromHOLstring res 845 val a_c = "aquire-resource "^(term_to_string (pf cond))^" "^res_s 846 val a_thm = CONV_RULE (RHS_CONV (asl_comment_abstraction_INTRO_CONV a_c)) a_thm3 847 val thm2 = CONV_RULE ((RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 848 (K a_thm)) thm1 849 850 (*use it to simplify release*) 851 val r_t = (rand o rator o rand o rand o rand o rand o concl) thm1; 852 val r_thm0 = RAND_CONV (K i_thm) r_t 853 val r_thm1 = PART_MATCH (lhs o snd o dest_imp) 854 var_res_prog_release_lock___INTRO (rhs (concl r_thm0)) 855 val r_thm2 = CONV_RULE ((RAND_CONV o LHS_CONV) (K (GSYM r_thm0))) r_thm1 856 val r_thm3 = MP r_thm2 set_eq_precond_thm 857 val r_c = "release-resource "^res_s 858 val r_thm = CONV_RULE (RHS_CONV (asl_comment_abstraction_INTRO_CONV r_c)) r_thm3 859 860 val thm3 = CONV_RULE ((RAND_CONV o RAND_CONV o RAND_CONV o RAND_CONV o 861 RATOR_CONV o RAND_CONV) (K r_thm)) thm2 862 863 864 (*call sys recursively*) 865 val (_, _, p1, p2) = dest_ASL_PROGRAM_IS_ABSTRACTION (concl thm3); 866 867 val sys_thm_opt = sys xenv penv p2; 868 val thm4 = if not (isSome sys_thm_opt) then thm3 else 869 let 870 val xthm0 = valOf sys_thm_opt 871 val (_, _, _, p3) = dest_ASL_PROGRAM_IS_ABSTRACTION (concl xthm0); 872 val xthm1 = ISPECL [xenv, penv, p1, p2, p3] ASL_PROGRAM_IS_ABSTRACTION___TRANSITIVE; 873 in MP (MP xthm1 thm3) xthm0 end 874 875 in 876 (SOME thm4) 877 end 878 879 880 881 882(******************************************************************************) 883(* ELIMINATE EXISTENTIAL QUANTIFICATION FROM PRE-AND POST-CONDITIONS *) 884(******************************************************************************) 885 886fun VAR_RES_COND_INFERENCE___EXISTS_PRE___CONSEQ_CONV ttt = 887let 888 val (_,pre,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE ttt 889 val (vc, _) = dest_COND_PROP___STRONG_EXISTS pre 890 891 val thm0 = (PART_MATCH (snd o dest_imp) 892 VAR_RES_COND_INFERENCE___STRONG_COND_EXISTS_PRE) ttt 893 894 895 val apply_beta = (QUANT_CONV o RATOR_CONV o RATOR_CONV o RAND_CONV) 896 PairRules.PBETA_CONV 897 val elim_quant = pairTools.SPLIT_QUANT_CONV vc; 898 899 900 val thm1 = CONV_RULE ((RATOR_CONV o RAND_CONV) ( 901 (apply_beta THENC elim_quant))) thm0 902in 903 thm1 904end handle HOL_ERR _ => raise UNCHANGED; 905 906fun VAR_RES_COND_INFERENCE___EXISTS_POST___CONSEQ_CONV ttt = 907let 908 val (_,_,_,post) = dest_VAR_RES_COND_HOARE_TRIPLE ttt 909 val (vc, _) = dest_COND_PROP___STRONG_EXISTS post 910 911 val thm0 = (PART_MATCH (snd o dest_imp) 912 VAR_RES_COND_INFERENCE___STRONG_COND_EXISTS_POST) ttt 913 914 val apply_beta = (QUANT_CONV o RAND_CONV) 915 PairRules.PBETA_CONV 916 val elim_quant = pairTools.SPLIT_QUANT_CONV vc; 917 918 val thm1 = CONV_RULE ((RATOR_CONV o RAND_CONV) ( 919 (apply_beta THENC elim_quant))) thm0 920 921 val thm1 = CONV_RULE ((RATOR_CONV o RAND_CONV) ( 922 (apply_beta THENC elim_quant))) thm0 923 924in 925 thm1 926end handle HOL_ERR _ => raise UNCHANGED; 927 928 929 930(*************************************************************** 931 * HANDLE SPECIFICATIONS 932 * 933 * Eliminate function calls 934 ****************************************************************) 935 936(* 937val (_,t) = top_goal() 938*) 939 940 941local 942 val abstrL = append (var_res_param.abstrL) (append basic_asl_program_abstractions [ 943 ASL_PROGRAM_ABSTRACTION___local_var, 944 ASL_PROGRAM_ABSTRACTION___call_by_value_arg, 945 ASL_PROGRAM_ABSTRACTION___eval_expressions, 946 ASL_PROGRAM_ABSTRACTION___var_res_prog_procedure_call, 947 ASL_PROGRAM_ABSTRACTION___var_res_prog_parallel_procedure_call, 948 ASL_PROGRAM_ABSTRACTION___var_res_cond_critical_section]); 949 950 951 (*intro hoare triples*) 952 953 fun STRIP_CONJ_CONV c t = 954 if is_conj t then 955 BINOP_CONV (STRIP_CONJ_CONV c) t 956 else c t 957 958 val intro_hoare_triples = 959 ANTE_CONV_RULE ( 960 (QUANT_CONV (STRIP_CONJ_CONV 961 ASL_PROGRAM_IS_ABSTRACTION___forall_comment_var_res_prog_quant_bla_CONV)) THENC 962 (TRY_CONV FORALL_SIMP_CONV) 963 ) 964 965 (*bring pre and post conditions in normal form*) 966 val intro_var_res_prop = 967 ANTE_CONV_RULE 968 (ONCE_DEPTH_CONV (QCHANGED_CONV (var_res_prop_input_distinct___ELIM_CONV NONE))) 969 970 971 fun elim_exists_pre thm = 972 let 973 val thm1 = ANTE_CONV_RULE ( 974 ONCE_DEPTH_CONV (QCHANGED_CONV COND_PROP___STRONG_EXISTS_NORMALISE_CONV)) thm handle UNCHANGED => thm 975 in 976 (STRENGTHEN_CONSEQ_CONV_RULE ( 977 (DEPTH_CONSEQ_CONV (K VAR_RES_COND_INFERENCE___EXISTS_PRE___CONSEQ_CONV))) thm1) 978 handle UNCHANGED => thm1 979 end 980in 981 982fun VAR_RES_SPECIFICATION___CONSEQ_CONV t = let 983 (*execute*) 984 val current_theorem = ASL_SPECIFICATION___CONSEQ_CONV (proc_call_free_CONV, abstrL) t; 985 val current_theorem2 = intro_hoare_triples current_theorem 986 val current_theorem3 = intro_var_res_prop current_theorem2 987 val current_theorem4 = elim_exists_pre current_theorem3 988in 989 current_theorem4 990end 991 992end 993 994 995 996(******************************************************************************) 997(* HANDLE local vars and arguments *) 998(******************************************************************************) 999 1000(* 1001val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1002*) 1003local 1004 val conv1 = HO_PART_MATCH (snd o dest_imp_only) 1005 VAR_RES_COND_INFERENCE___prog_local_var 1006 val conv2 = HO_PART_MATCH (snd o dest_imp_only) 1007 VAR_RES_COND_INFERENCE___prog_call_by_value_arg 1008 val conv = ORELSE_CONSEQ_CONV conv1 conv2 1009 1010 fun strip_local_vars_args_CONV c p = 1011 if (is_var_res_prog_call_by_value_arg p) then 1012 ((RATOR_CONV o RAND_CONV o ABS_CONV) 1013 (strip_local_vars_args_CONV c)) p else 1014 if (is_var_res_prog_local_var p) then 1015 ((RAND_CONV o ABS_CONV) 1016 (strip_local_vars_args_CONV c)) p else 1017 c p 1018 1019in 1020 fun VAR_RES_COND_INFERENCE___local_vars_args___CONSEQ_CONV tt = 1021 let 1022 val (_, _, prog, post) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 1023 val (c, prog', prog_thm_fun) = save_dest_asl_comment_location prog; 1024 val _ = if (is_var_res_prog_call_by_value_arg prog' orelse 1025 is_var_res_prog_local_var prog') then () else raise UNCHANGED 1026 1027 val (vp, post_thm) = COND_PROP___STRONG_EXISTS_INTRO___CONV post; 1028 val prog_thm0 = prog_thm_fun () 1029 val prog_thm = CONV_RULE (RHS_CONV (strip_local_vars_args_CONV 1030 (asl_comment_location_BLOCK_INTRO_CONV (asl_comment_modify_INC c)))) prog_thm0 1031 1032 val thm0 = ((RAND_CONV (K post_thm)) THENC 1033 ((RATOR_CONV o RAND_CONV) (K prog_thm))) tt; 1034 1035 val thm1 = REDEPTH_CONSEQ_CONV (K conv) CONSEQ_CONV_STRENGTHEN_direction 1036 (rhs (concl thm0)); 1037 1038 val thm2 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm1 1039 1040 val thm3 = ANTE_CONV_RULE ((STRIP_QUANT_CONV o RAND_CONV) ( 1041 COND_PROP___STRONG_EXISTS_ELIM___CONV vp)) thm2 1042 in 1043 thm3 1044 end 1045end; 1046 1047 1048(******************************************************************************) 1049(* HANDLE comments for blocks *) 1050(******************************************************************************) 1051 1052(* 1053val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1054*) 1055fun VAR_RES_COND_INFERENCE___block_comment___CONV tt = 1056let 1057 val (_,_,prog,_) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 1058 val (c, prog') = dest_asl_comment_location prog; 1059 val _ = if is_asl_prog_block prog' then () else raise UNCHANGED 1060 1061 val conv1 = K (ISPECL [c, prog'] asl_comment_location_def) 1062 val conv2 = asl_comment_location_BLOCK_INTRO_CONV (asl_comment_modify_COPY_INIT c) 1063 val conv = conv1 THENC conv2 1064in 1065 RATOR_CONV (RAND_CONV conv) tt 1066end 1067 1068 1069 1070(******************************************************************************) 1071(* Flatten blocks *) 1072(******************************************************************************) 1073 1074(* 1075val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1076val tt = (snd o dest_conj o fst o dest_imp o concl) ttt 1077val tref = ref NONE 1078*) 1079fun VAR_RES_COND_INFERENCE___block_flatten___CONSEQ_CONV tt = 1080let 1081 val (f,P,prog1,Q) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 1082 val pL_t = dest_asl_prog_block prog1 1083 val (pL, _) = listSyntax.strip_cons pL_t 1084 val _ = if exists is_asl_prog_block pL then () else raise UNCHANGED 1085 1086 val (xenv, penv) = let (* a crude, but robust and simple way *) 1087 val thm0 = ISPECL [f, prog1] VAR_RES_PROGRAM_IS_ABSTRACTION_def 1088 val t0 = (rator o rator o rhs o snd o strip_forall o concl) thm0 1089 val penv = rand t0 1090 val xenv = rand (rator t0) 1091 in 1092 (xenv, penv) 1093 end; 1094 val abst_opt = 1095 ASL_PROGRAM_ABSTRACTION___block_flatten___no_rec xenv penv prog1 1096 val _ = if isSome abst_opt then () else raise UNCHANGED; 1097 1098 val abst_thm = CONV_RULE (REWR_CONV (GSYM VAR_RES_PROGRAM_IS_ABSTRACTION_def)) 1099 (valOf abst_opt); 1100 1101 val prog2 = (rand o concl) abst_thm 1102 val thm0 = ISPECL [f, P, prog1, prog2, Q] VAR_RES_COND_HOARE_TRIPLE___PROGRAM_ABSTRACTION_EVAL 1103 val thm1 = MP thm0 abst_thm 1104in 1105 thm1 1106end; 1107 1108 1109(******************************************************************************) 1110(* HANDLE conditional execution *) 1111(******************************************************************************) 1112 1113(* 1114val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1115*) 1116fun VAR_RES_COND_INFERENCE___cond___CONSEQ_CONV tt = 1117let 1118 val (p1,c_opt,_,_,_,thm0_fun) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt; 1119 val cond_t_opt = 1120 let 1121 val (cond_t, _, _) = dest_asl_prog_cond p1 1122 in SOME cond_t end handle HOL_ERR _ => 1123 let 1124 val _ = dest_asl_prog_choice p1; 1125 in NONE end; 1126 1127 (*apply inference*) 1128 val c = if isSome c_opt then valOf c_opt else empty_label_list 1129 val thm0 = if not (isSome c_opt) then REFL tt else 1130 VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV 1131 (K (ISPECL [c, p1] asl_comment_location_def)) tt 1132 val inf_thm = if isSome cond_t_opt then 1133 VAR_RES_COND_INFERENCE___prog_cond else 1134 VAR_RES_COND_INFERENCE___prog_choice 1135 val thm1a = 1136 HO_PART_MATCH (snd o dest_imp_only) inf_thm 1137 (rhs (concl thm0)); 1138 val thm1 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm1a 1139 1140 (*comments*) 1141 val (cond_s, neg_cond_s) = if isSome cond_t_opt then 1142 let 1143 val cond_t = valOf cond_t_opt 1144 val neg_cond_t = mk_icomb (asl_pred_neg_term, cond_t); 1145 in (term_to_string cond_t, term_to_string neg_cond_t) end 1146 else ("1", "2"); 1147 1148 val ct = asl_comment_modify_APPEND_INC ("case "^cond_s) c 1149 val cf = asl_comment_modify_APPEND_INC ("case "^neg_cond_s) c 1150 1151 val ttt = (fst o dest_conj o fst o dest_imp o concl) thm1 1152 1153 fun list_first_conv conv ttt = 1154 if (listSyntax.is_nil ttt) then conv ttt else 1155 (RATOR_CONV (RAND_CONV conv)) ttt 1156 fun comment_conv c = 1157 (TRY_CONV (REWR_CONV VAR_RES_COND_INFERENCE___prog_block3)) THENC 1158 (TRY_CONV (REWR_CONV VAR_RES_COND_INFERENCE___prog_block4)) THENC 1159 ((RATOR_CONV o RAND_CONV o RAND_CONV o (if isSome cond_t_opt then RAND_CONV else I)) 1160 (list_append_norm_CONV THENC 1161 list_first_conv (asl_comment_location_INTRO_CONV c))) 1162 1163 1164 val thm2 = CONV_RULE ( 1165 (RATOR_CONV o RAND_CONV) 1166 (RAND_CONV (comment_conv cf) THENC 1167 (RATOR_CONV (RAND_CONV (comment_conv ct))))) thm1 1168in 1169 thm2 1170end; 1171 1172(******************************************************************************) 1173(* HANDLE diverge *) 1174(******************************************************************************) 1175 1176(* 1177val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1178*) 1179fun VAR_RES_COND_INFERENCE___diverge___CONV tt = 1180let 1181 val (p1,c_opt,_,_,_,thm0_fun) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt; 1182 val _ = if same_const p1 asl_prog_diverge_term then () else Feedback.fail(); 1183 1184 (*apply inference*) 1185 val c = if isSome c_opt then valOf c_opt else empty_label_list 1186 val thm0 = if not (isSome c_opt) then REFL tt else 1187 VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV 1188 (K (ISPECL [c, p1] asl_comment_location_def)) tt; 1189 1190 val thm1a = 1191 HO_PART_MATCH I VAR_RES_COND_INFERENCE___prog_block_diverge 1192 (rhs (concl thm0)); 1193 val thm1 = TRANS thm0 (EQT_INTRO thm1a); 1194in 1195 thm1 1196end; 1197 1198 1199(******************************************************************************) 1200(* HANDLE assume *) 1201(******************************************************************************) 1202 1203val asl_prog_assume___INFERENCES = [ 1204VAR_RES_COND_INFERENCE___prog_assume_and, 1205VAR_RES_COND_INFERENCE___prog_assume_or, 1206VAR_RES_COND_INFERENCE___prog_assume_neg_and, 1207VAR_RES_COND_INFERENCE___prog_assume_neg_or, 1208VAR_RES_COND_INFERENCE___prog_assume_neg_neg, 1209VAR_RES_COND_INFERENCE___prog_assume_neg_pred_bin, 1210VAR_RES_COND_INFERENCE___prog_assume_neg_pred, 1211VAR_RES_COND_INFERENCE___prog_assume_pred_bin, 1212VAR_RES_COND_INFERENCE___prog_assume_pred, 1213VAR_RES_COND_INFERENCE___prog_assume_true, 1214VAR_RES_COND_INFERENCE___prog_assume_false, 1215VAR_RES_COND_INFERENCE___prog_assume_neg_true, 1216VAR_RES_COND_INFERENCE___prog_assume_neg_false] 1217 1218 1219val asl_prog_assume___INFERENCES_CONSEQ_CONVS = 1220map (fn thm => 1221let 1222 val tt = (snd o dest_imp o snd o strip_forall o concl) thm 1223in 1224 if (is_VAR_RES_COND_HOARE_TRIPLE tt) then 1225 PART_MATCH (snd o dest_imp) thm 1226 else 1227 PART_MATCH (snd o dest_imp o snd o dest_imp) thm 1228end) asl_prog_assume___INFERENCES 1229 1230(* 1231val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1232*) 1233fun VAR_RES_COND_INFERENCE___assume___internal tt = 1234let 1235 val (ap,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt; 1236 val _ = if (is_asl_prog_assume ap) then () else raise UNCHANGED; 1237 1238 val thm0 = tryfind (fn c => c tt) asl_prog_assume___INFERENCES_CONSEQ_CONVS 1239 val thm1 = if (is_imp_only ((snd o dest_imp o concl) thm0)) then 1240 var_res_precondition_prove thm0 1241 else thm0 1242 val thm2 = STRENGTHEN_CONSEQ_CONV_RULE 1243 (K (VAR_RES_COND_INFERENCE___assume___internal)) 1244 thm1 handle UNCHANGED => thm1 1245 | HOL_ERR _ => thm1 1246in 1247 thm2 1248end; 1249 1250 1251fun VAR_RES_COND_INFERENCE___assume___CONSEQ_CONV tt = 1252let 1253 val (ap,_,_,_,_,thm0_fun) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt; 1254 val _ = if (is_asl_prog_assume ap) then () else raise UNCHANGED; 1255 1256 fun conv_pre t = thm0_fun (); 1257 val conv_post = VAR_RES_COND_HOARE_TRIPLE___PRECOND_CONV ( 1258 DEPTH_CONV BETA_CONV THENC 1259 REWRITE_CONV [var_res_prop_binexpression_ELIM]) 1260in 1261 (EVERY_CONSEQ_CONV [conv_pre, 1262 VAR_RES_COND_INFERENCE___assume___internal, conv_post]) tt 1263end; 1264 1265 1266 1267(******************************************************************************) 1268(* Propagate equality *) 1269(******************************************************************************) 1270 1271fun var_res_prop___var_eq_const_BAG___INTRO f b = 1272let 1273 (*find the equations for rewriting*) 1274 val (sfs,_) = dest_bag b 1275 fun get_vcL n nL vcL [] = (rev nL, rev vcL) 1276 | get_vcL n nL vcL (p::pL) = 1277 let 1278 val (_,l,r) = dest_var_res_prop_equal p; 1279 val v = dest_var_res_exp_var l; 1280 val c = dest_var_res_exp_const r; 1281 val _ = if (exists (fn (v', _) => aconv v v') vcL) then 1282 Feedback.fail() else (); 1283 in 1284 get_vcL (n+1) (n::nL) ((v,c)::vcL) pL 1285 end handle HOL_ERR _ => 1286 get_vcL (n+1) nL vcL pL; 1287 1288 val (nL, vcL) = get_vcL 0 [] [] sfs 1289 val _ = if (null nL) then raise UNCHANGED else (); 1290 1291 val vcL_t = let 1292 val vcL_pL = map (pairSyntax.mk_pair) vcL; 1293 in 1294 listSyntax.mk_list (vcL_pL, type_of (hd vcL_pL)) 1295 end; 1296 1297 (*bring original term in right form*) 1298 val b_resort_thm = bagLib.BAG_RESORT_CONV nL b; 1299 val b' = rhs (concl b_resort_thm); 1300 1301 val b''_rest = (funpow (length nL) rand) b' 1302 val b''_start = list_mk_icomb(var_res_prop___var_eq_const_BAG_term, [f, vcL_t]) 1303 val b'' = bagSyntax.mk_union (b''_start, b''_rest) 1304 1305 val b''_eq_t = mk_eq (b', b''); 1306 val b''_eq_thm = EQT_ELIM (BAG_NORMALISE_CONV b''_eq_t) 1307 val b_thm = TRANS b_resort_thm b''_eq_thm 1308in 1309 (vcL_t, b_thm) 1310end; 1311 1312 1313fun var_res_prop___PROPAGATE_EQ___CONV pre = 1314let 1315 (*do some simple preprocessing bringing every equation in 1316 normal form*) 1317 val pre_thm = var_res_prop___VAR_EQ_PROPAGATE pre handle UNCHANGED => 1318 REFL pre 1319 val pre' = rhs (concl pre_thm); 1320 1321 1322 (*find the equations for rewriting*) 1323 val (f, wpb, rpb, sfb) = dest_var_res_prop pre'; 1324 val (vcL_t, sfb_thm) = var_res_prop___var_eq_const_BAG___INTRO f sfb; 1325 val pre_thm' = CONV_RULE (RHS_CONV 1326 (RAND_CONV (K sfb_thm))) pre_thm 1327 1328 1329 (*instantiate the rewrite thm*) 1330 val pre'' = rhs (concl pre_thm') 1331 val imp_thm0 = PART_MATCH (rand o rator) var_res_prop___equal_const pre'' 1332 val imp_thm1 = CONV_RULE ((RATOR_CONV o RAND_CONV) 1333 (K (GSYM pre_thm'))) imp_thm0 1334 1335 (*simplify it by removing the BAG_IMAGE and evaluating 1336 var_res_prop_varlist*) 1337 val imp_thm2 = CONV_RULE (RAND_CONV ((DEPTH_CONV BAG_IMAGE_CONV) THENC 1338 BAG_NORMALISE_CONV)) imp_thm1 1339 1340 val imp_thm3a = var_res_prop___var_res_prop_varlist_update___EVAL vcL_t 1341 (rand (concl imp_thm2)); 1342 val imp_thm3b = CONJUNCT1 (CONV_RULE (REWR_CONV COND_PROP___STRONG_EQUIV_def) imp_thm3a) 1343 val thm3 = MATCH_MP (MATCH_MP COND_PROP___STRONG_IMP___TRANS imp_thm2) imp_thm3b 1344in 1345 thm3 1346end; 1347 1348 1349 1350(* 1351val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1352*) 1353 1354fun VAR_RES_COND_INFERENCE___PROPAGATE_EQ___CONSEQ_CONV tt = 1355let 1356 val (f, P1, prog, Q) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 1357 val thm0 = var_res_prop___PROPAGATE_EQ___CONV P1 1358 val P2 = rand (concl thm0) 1359 1360 val thm1 = ISPECL [f, P1, P2, prog, Q] VAR_RES_COND_HOARE_TRIPLE___COND_PROP_STRONG_IMP 1361in 1362 MP thm1 thm0 1363end 1364 1365 1366fun VAR_RES_COND_INFERENCE___CONST_INTRO_PROPAGATE_EQ___CONSEQ_CONV inst_all_vars tt = 1367let 1368 val (f, P, prog, Q) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 1369 val (_, wp, rp, _, sfs) = dest_var_res_prop___propL P; 1370 1371 fun is_subterm st t = 1372 (find_term (aconv st) t; true) handle HOL_ERR _ => false 1373 fun var_is_needed v = 1374 let 1375 val sfs' = filter (is_subterm v) sfs; 1376 in 1377 if length sfs' > 1 then true else 1378 if length sfs' = 0 then inst_all_vars else 1379 let 1380 val (_, v', c) = dest_var_res_prop_equal (hd sfs'); 1381 val _ = dest_var_res_exp_const c 1382 val v'' = dest_var_res_exp_var v' 1383 in 1384 not (aconv v v'') 1385 end handle HOL_ERR _ => true 1386 end 1387 1388 val varsL = (fst (bagSyntax.dest_bag wp)) @ (fst (bagSyntax.dest_bag rp)) 1389 val needed_vars = filter var_is_needed varsL 1390 val _ = if null needed_vars then raise UNCHANGED else (); 1391 1392 1393 val expression_ty = 1394 mk_var_res_expr_type (fst (dest_var_res_ext_state_type ( 1395 dest_var_res_cond_proposition (type_of P)))) 1396 1397 (*instantiate needed constants*) 1398 val thm0 = VAR_RES_COND_INFERENCE___CONST_LIST_INTRO___CONV 1399 (map (fn v => (mk_var_res_exp_var v expression_ty, NONE)) needed_vars) tt; 1400 1401 val (vL, tt') = (strip_forall o rhs o concl) thm0 1402 val thm1a = VAR_RES_COND_INFERENCE___PROPAGATE_EQ___CONSEQ_CONV tt'; 1403 val thm1b = LIST_GEN_IMP vL thm1a 1404 val thm1 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm1b 1405in 1406 thm1 1407end; 1408 1409 1410 1411 1412(* 1413 val tL = find_terms is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1414 val tt = el 1 tL 1415val thm = VAR_RES_COND_INFERENCE___ALL_CONST_INTRO___CONV tt 1416*) 1417fun VAR_RES_COND_INFERENCE___ALL_CONST_INTRO___CONV tt = 1418let 1419 val (_, pre, _, _) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 1420 val (_, wpb, rpb, _) = dest_var_res_prop pre 1421 val var_list = append (fst (dest_bag wpb)) (fst (dest_bag rpb)) 1422 1423 val expression_ty = 1424 mk_var_res_expr_type (fst (dest_var_res_ext_state_type ( 1425 dest_var_res_cond_proposition (type_of pre)))) 1426 1427 val exp_list = map (fn v => (mk_var_res_exp_var v expression_ty, NONE)) var_list 1428in 1429 (CHANGED_CONV (VAR_RES_COND_INFERENCE___CONST_LIST_INTRO___CONV exp_list) tt) handle HOL_ERR _ => raise UNCHANGED 1430end; 1431 1432 1433(* while preparing for the introduction of a "VAR_RES_FRAME_SPLIT" 1434 predicate, existential quantifiers are moved to the outer level. 1435 This may cause trouble, because the choices for these variables have to 1436 hold under all other (later) case-splits. Therefore, obvious case splits 1437 are done first, like ones acoording to if-then-else. Moreover, 1438 concrete values for variables are introduced as well before the existential 1439 quantifiers. *) 1440 1441fun VAR_RES_COND_INFERENCE___PREPARE_FOR_FRAME___CONV tt = 1442let 1443 val (_, pre, _, _) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 1444 fun not_ok t = is_cond t orelse is_var_res_prop_binexpression_cond t 1445 val is_ok = (find_term not_ok pre; false) handle HOL_ERR _ => true; 1446 val _ = if (is_ok) then () else Feedback.fail(); 1447in 1448 VAR_RES_COND_INFERENCE___ALL_CONST_INTRO___CONV tt 1449end; 1450 1451 1452(* 1453 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 1454*) 1455fun VAR_RES_FRAME_SPLIT_INFERENCE___ALL_CONST_INTRO___CONV tt = 1456let 1457 val (_, _, wprpb, _, context_sfb,_,_,_) = dest_VAR_RES_FRAME_SPLIT tt; 1458 val (wpb, rpb) = pairSyntax.dest_pair wprpb 1459 val var_list = append (fst (dest_bag wpb)) (fst (dest_bag rpb)) 1460 1461 val expression_ty = 1462 mk_var_res_expr_type (fst (dest_var_res_ext_state_type ( 1463 dest_var_res_proposition (bagSyntax.base_type context_sfb)))) 1464 1465 val exp_list = map (fn v => (mk_var_res_exp_var v expression_ty, NONE)) var_list 1466in 1467 (CHANGED_CONV (VAR_RES_FRAME_SPLIT_INFERENCE___CONST_LIST_INTRO___CONV exp_list) tt) handle HOL_ERR _ => raise UNCHANGED 1468end; 1469 1470 1471 1472 1473(******************************************************************************) 1474(* Final step *) 1475(******************************************************************************) 1476 1477(* 1478 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1479*) 1480fun VAR_RES_COND_INFERENCE___final___CONSEQ_CONV tt = 1481let 1482 val (_,_,prog,_) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 1483 val bL = dest_asl_prog_block prog 1484 val (c, bL, bl_eq_fun) = save_dest_asl_comment_location bL 1485 val _ = if (listSyntax.is_nil bL) then () else raise UNCHANGED; 1486 1487 1488 (*elim comment / intro constants *) 1489 val thm0 = (((RATOR_CONV o RAND_CONV o RAND_CONV) (K (bl_eq_fun ()))) THENC 1490 VAR_RES_COND_INFERENCE___PREPARE_FOR_FRAME___CONV) tt 1491 val (vs, tt') = strip_forall (rhs (concl thm0)) 1492 1493 (*elim existentials in post-condition*) 1494 val thm1 = VAR_RES_COND_INFERENCE___EXISTS_POST___CONSEQ_CONV tt' 1495 handle UNCHANGED => REFL_CONSEQ_CONV tt'; 1496 1497 (*solve*) 1498 val pre = (fst o dest_imp o concl) thm1 1499 val (vL, trip) = strip_exists pre; 1500 1501 val new_comment = asl_comment_modify_APPEND "final" c; 1502 val rfc = pairSyntax.mk_pair (F, optionSyntax.mk_some new_comment) 1503 1504 val pre_thm0 = PART_MATCH (rand o rand) 1505 (SPEC rfc VAR_RES_COND_HOARE_TRIPLE___SOLVE) trip 1506 val pre_thm1 = var_res_precondition_prove pre_thm0 1507 1508 val pre_thm2 = LIST_EXISTS_INTRO_IMP vL pre_thm1 1509 val thm3 = IMP_TRANS pre_thm2 thm1 1510 1511 (*combine with thm0*) 1512 val thm4a = LIST_GEN_IMP vs thm3 1513 val thm4 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm4a 1514in 1515 thm4 1516end; 1517 1518 1519 1520(******************************************************************************) 1521(* HANDLE while loops *) 1522(******************************************************************************) 1523 1524(* 1525val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1526*) 1527fun VAR_RES_COND_INFERENCE___while___invariant___CONSEQ_CONV tt = 1528let 1529 (* destruct everything *) 1530 val (p1_0,c_opt,_,_,_,thm0_fun) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt; 1531 val (inv_t,p1) = dest_asl_comment_loop_invariant p1_0; 1532 val (vc, inv_body_t) = pairSyntax.dest_pabs inv_t 1533 1534 val (co, while_body') = dest_asl_prog_while p1; 1535 val while_body = dest_asl_prog_block while_body' 1536 val c = if isSome c_opt then valOf c_opt else empty_label_list; 1537 1538 (*introduce constants*) 1539 val thm_const = CONV_RULE (RHS_CONV 1540 VAR_RES_COND_INFERENCE___PREPARE_FOR_FRAME___CONV) (thm0_fun()) 1541 val (vs, tt') = strip_forall (rhs (concl thm_const)) 1542 1543 1544 (*apply inference*) 1545 val inv_thm = pairTools.PABS_ELIM_CONV inv_t handle UNCHANGED => REFL inv_t; 1546 val (v, inv_body_t') = dest_abs (rhs (concl inv_thm)) 1547 val (_, wprp, d, sfb) = dest_var_res_prop_input_ap_distinct inv_body_t' 1548 val (wp,rp) = pairSyntax.dest_pair wprp; 1549 1550 val thm0a = VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV ( 1551 (RATOR_CONV (RAND_CONV (K inv_thm)))) tt' 1552 1553 val pL = (rand o rand o rand o rator o rhs o concl) thm0a 1554 val (_,_,f,P,Q,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt'; 1555 1556 val thm0b = ISPECL [f, P, wp,rp, d, mk_abs (v, sfb), 1557 co, while_body, pL, Q] VAR_RES_COND_INFERENCE___prog_while 1558 1559 val thm0 = CONV_RULE ((RAND_CONV o RAND_CONV) ((DEPTH_CONV BETA_CONV) THENC 1560 (K (GSYM thm0a)))) thm0b 1561 1562 (*elim precond*) 1563 val precond = (fst o dest_imp o concl) thm0 1564 val precond_thm1 = PART_MATCH (fst o dest_imp) var_res_prop___IMPLIES_VAR_DISTINCT 1565 ((fst o dest_imp) precond) 1566 val precond_thm2_term = mk_imp ((snd o dest_imp o concl) precond_thm1, 1567 (snd o dest_imp) precond) 1568 val precond_thm2 = var_res_prove precond_thm2_term; 1569 val precond_thm = IMP_TRANS precond_thm1 precond_thm2; 1570 1571 val thm1 = MP thm0 precond_thm; 1572 1573 (*simplify invariant*) 1574 val inv_prop = (rand o snd o dest_forall o rand o rator o fst o dest_imp o concl) thm1; 1575 val inv_prop_thm = ((DEPTH_CONV BETA_CONV) THENC 1576 var_res_prop_input_distinct___ELIM_CONV NONE THENC 1577 COND_PROP___STRONG_EXISTS_NORMALISE_CONV) inv_prop; 1578 1579 val thm2 = CONV_RULE ((RATOR_CONV o RAND_CONV) (DEPTH_CONV (REWR_CONV inv_prop_thm))) thm1 1580 1581 (*reintroduce orginal variable names*) 1582 val thm3 = CONV_RULE ((RATOR_CONV o RAND_CONV) 1583 (((RAND_CONV) (pairTools.SPLIT_QUANT_CONV vc THENC 1584 TRY_CONV LIST_EXISTS_SIMP_CONV)) THENC 1585 ((RATOR_CONV o RAND_CONV) (pairTools.SPLIT_QUANT_CONV vc THENC 1586 TRY_CONV LIST_FORALL_SIMP_CONV)))) thm2 1587 1588 (*introduce comment while-abstraction*) 1589 val new_c1 = asl_comment_modify_APPEND ("abstracted while loop") c 1590 val thm4 = CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV o STRIP_QUANT_CONV o 1591 RATOR_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 1592 ((asl_comment_location2_INTRO_CONV new_c1) THENC 1593 (asl_comment_abstraction_INTRO_CONV "while-loop"))) thm3 1594 1595 1596 (*introduce comment while-body*) 1597 val new_c2 = asl_comment_modify_APPEND ("while loop") c 1598 val thm5 = CONV_RULE ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o STRIP_QUANT_CONV o 1599 RATOR_CONV o RAND_CONV o RAND_CONV o RAND_CONV o 1600 (fn conv => fn t => if listSyntax.is_nil t then conv t else 1601 (RATOR_CONV o RAND_CONV) conv t)) 1602 (asl_comment_location_INTRO_CONV new_c2)) thm4 1603 1604 (*combine with thm_const*) 1605 val thm6a = LIST_GEN_IMP vs thm5 1606 val thm6 = CONV_RULE (RAND_CONV (K (GSYM thm_const))) thm6a 1607in 1608 thm6 1609end; 1610 1611 1612 1613(* 1614val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1615*) 1616fun VAR_RES_COND_INFERENCE___while___loop_spec___CONSEQ_CONV tt = 1617let 1618 (* destruct everything *) 1619 val (p1_0,c_opt,_,_,_,thm0_fun) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt; 1620 val (PQ',p1) = dest_asl_comment_loop_spec p1_0; 1621 val (P',Q') = pairSyntax.dest_pair PQ'; 1622 1623 val (pL',_) = listSyntax.dest_list (dest_asl_prog_block p1); 1624 val (p1,pL) = (hd pL', tl pL'); 1625 1626 val (co, while_body') = dest_asl_prog_while p1; 1627 val while_body = dest_asl_prog_block while_body' 1628 val c = if isSome c_opt then valOf c_opt else empty_label_list; 1629 1630 (*introduce constants*) 1631 val thm_const = CONV_RULE (RHS_CONV 1632 VAR_RES_COND_INFERENCE___PREPARE_FOR_FRAME___CONV) (thm0_fun()) 1633 val (vs, tt') = strip_forall (rhs (concl thm_const)) 1634 1635 1636 (*apply inference*) 1637 val (vc, _) = pairSyntax.dest_pabs P'; 1638 val P_thm = pairTools.PABS_ELIM_CONV P' handle UNCHANGED => REFL P'; 1639 val Q_thm = pairTools.PABS_ELIM_CONV Q' handle UNCHANGED => REFL Q'; 1640 1641 val pair_PQ_CONV = (RAND_CONV (K Q_thm)) THENC 1642 (RATOR_CONV (RAND_CONV (K P_thm))) 1643 1644 val thm0a = VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV 1645 (RATOR_CONV (RAND_CONV pair_PQ_CONV)) tt' 1646 1647 val thm0b = HO_PART_MATCH (snd o dest_imp o snd o dest_imp) 1648 VAR_RES_COND_INFERENCE___loop_spec 1649 (rhs (concl thm0a)) 1650 1651 val thm0 = CONV_RULE ((RAND_CONV o RAND_CONV) ((DEPTH_CONV BETA_CONV) THENC 1652 (K (GSYM thm0a)))) thm0b 1653 1654 (*elim precond*) 1655 val precond = (fst o dest_imp o concl) thm0 1656 val precond_thm1 = PART_MATCH (fst o dest_imp) var_res_prop___IMPLIES_VAR_DISTINCT 1657 ((fst o dest_imp) precond) 1658 val precond_thm2_term = mk_imp ((snd o dest_imp o concl) precond_thm1, 1659 (snd o dest_imp) precond) 1660 val precond_thm2 = var_res_prove precond_thm2_term; 1661 val precond_thm = IMP_TRANS precond_thm1 precond_thm2; 1662 1663 val thm1 = MP thm0 precond_thm; 1664 1665 (*simplify invariant*) 1666 val post_prop = (rand o snd o dest_forall o rand o rator o fst o dest_imp o concl) thm1; 1667 val post_prop_thm = ((DEPTH_CONV BETA_CONV) THENC 1668 var_res_prop_input_distinct___ELIM_CONV NONE THENC 1669 COND_PROP___STRONG_EXISTS_NORMALISE_CONV) post_prop; 1670 1671 val pre_prop = (rand o rator o rator o snd o dest_forall o rand o rator o fst o dest_imp o concl) thm1; 1672 val pre_prop_thm = ((DEPTH_CONV BETA_CONV) THENC 1673 var_res_prop_input_distinct___ELIM_CONV NONE THENC 1674 COND_PROP___STRONG_EXISTS_NORMALISE_CONV) pre_prop; 1675 1676 val thm2 = CONV_RULE ((RATOR_CONV o RAND_CONV) (DEPTH_CONV ( 1677 (REWR_CONV pre_prop_thm) ORELSEC (REWR_CONV post_prop_thm)))) thm1 1678 1679 (*reintroduce orginal variable names*) 1680 val my_intro_conv = (pairTools.SPLIT_QUANT_CONV vc THENC 1681 TRY_CONV LIST_EXISTS_SIMP_CONV) 1682 val my_abs_intro_conv = pairTools.PABS_INTRO_CONV vc 1683 1684 val thm3 = CONV_RULE ((RATOR_CONV o RAND_CONV) 1685 ((RATOR_CONV (RAND_CONV my_intro_conv)) THENC 1686 (RAND_CONV (RAND_CONV (my_intro_conv)) THENC 1687 (RAND_CONV (RATOR_CONV (RAND_CONV ( 1688 my_intro_conv THENC 1689 ((STRIP_QUANT_CONV o RATOR_CONV o RAND_CONV o RAND_CONV o 1690 RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 1691 (RAND_CONV my_abs_intro_conv THENC 1692 RATOR_CONV (RAND_CONV my_abs_intro_conv)))))))))) thm2 1693 1694 (*introduce comment while-abstraction*) 1695 val new_c1 = asl_comment_modify_APPEND ("abstracted while-loop block") c 1696 val thm4a = CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV o RAND_CONV o 1697 STRIP_QUANT_CONV o 1698 RATOR_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 1699 ((asl_comment_location2_INTRO_CONV new_c1) THENC 1700 (asl_comment_abstraction_INTRO_CONV "while-loop block"))) thm3 1701 1702 (*introduce comment while-skip*) 1703 val new_c2 = asl_comment_modify_APPEND ("while-loop block unroll skip") c 1704 val thm4b = CONV_RULE ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o STRIP_QUANT_CONV o 1705 RATOR_CONV o RAND_CONV o RAND_CONV o RAND_CONV o 1706 (fn conv => fn t => if listSyntax.is_nil t then conv t else 1707 (RATOR_CONV o RAND_CONV) conv t)) 1708 (asl_comment_location_INTRO_CONV new_c2)) thm4a 1709 1710 1711 (*introduce comment while-*) 1712 val new_c3 = asl_comment_modify_APPEND ("while-loop block unroll iterate") c 1713 1714 fun block_list_CONV conv t = 1715 if listSyntax.is_nil t then conv t else 1716 (RATOR_CONV o RAND_CONV) conv t 1717 fun block_first_CONV conv t = 1718 if is_asl_prog_block t then RAND_CONV (block_list_CONV conv) t else 1719 conv t 1720 1721 val thm4c = CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o STRIP_QUANT_CONV o 1722 RATOR_CONV o RAND_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o 1723 block_first_CONV) 1724 (asl_comment_location_INTRO_CONV new_c3)) thm4b 1725 1726 val thm4d = CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o STRIP_QUANT_CONV o 1727 RATOR_CONV o RAND_CONV o RAND_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 1728 (asl_comment_abstraction_INTRO_CONV "re-enter while-loop")) thm4c 1729 1730 (*introduce flatten blocks-*) 1731 val block_flatten_conv = 1732 (REWR_CONV VAR_RES_COND_INFERENCE___prog_block3) THENC 1733 ((RATOR_CONV o RAND_CONV o RAND_CONV o RAND_CONV) 1734 (list_append_norm_CONV)) 1735 1736 val thm4 = CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o STRIP_QUANT_CONV) 1737 block_flatten_conv) thm4d handle HOL_ERR _ => thm4d 1738 1739 (*combine with thm_const*) 1740 val thm5a = LIST_GEN_IMP vs thm4 1741 val thm5 = CONV_RULE (RAND_CONV (K (GSYM thm_const))) thm5a 1742in 1743 thm5 1744end; 1745 1746 1747 1748 1749(* 1750VAR_RES_COND_INFERENCE___while_unroll 1751 1752val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1753*) 1754 1755fun VAR_RES_COND_INFERENCE___while___loop_unroll___CONSEQ_CONV tt = 1756let 1757 (* destruct everything *) 1758 val (p1_0,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt; 1759 val (c, p1_1, thm0_fun) = save_dest_asl_comment_location p1_0 1760 val (unroll_t,p1) = dest_asl_comment_loop_unroll p1_1; 1761 1762 (* elim comments *) 1763 val thm0a = CONV_RULE (RHS_CONV (REWR_CONV asl_comment_loop_unroll_def)) (thm0_fun ()); 1764 val thm0 = VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV (K thm0a) tt 1765 1766 1767 (* apply inference *) 1768 val inf_thm = if (is_asl_comment_loop_invariant p1) then 1769 VAR_RES_COND_INFERENCE___while_unroll___invariant 1770 else if (is_asl_comment_loop_spec p1) then 1771 VAR_RES_COND_INFERENCE___while_unroll___loop_spec 1772 else VAR_RES_COND_INFERENCE___while_unroll 1773 val thm1a = PART_MATCH (snd o dest_imp) inf_thm (rhs (concl thm0)) 1774 fun unroll_comment_intro t = 1775 let 1776 val unroll_n = numLib.int_of_term unroll_t 1777 in 1778 if unroll_n <= 1 then raise UNCHANGED else 1779 ISPECL [numLib.term_of_int (unroll_n - 1), t] (GSYM asl_comment_loop_unroll_def) 1780 end; 1781 1782 val thm1b = CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o 1783 RAND_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) unroll_comment_intro) thm1a 1784 1785 val thm1c = CONV_RULE ((RATOR_CONV o RAND_CONV) (REWRITE_CONV [ 1786 VAR_RES_COND_INFERENCE___prog_block3, APPEND])) thm1b 1787 val thm1 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm1c 1788 1789 1790 (* reintroduce comments *) 1791 val new_c2 = asl_comment_modify_APPEND ("while-loop unroll-skipped") c; 1792 val new_c3 = asl_comment_modify_APPEND ("while-loop unrolled") c; 1793 1794 fun block_list_CONV conv t = 1795 if listSyntax.is_nil t then conv t else 1796 if listSyntax.is_nil (rand t) then 1797 (RAND_CONV conv t) else 1798 (RAND_CONV o RATOR_CONV o RAND_CONV) conv t 1799 1800 fun block_second_CONV conv t = 1801 if is_asl_prog_block t then RAND_CONV (block_list_CONV conv) t else 1802 conv t 1803 1804 val thm2a = CONV_RULE ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 1805 (block_second_CONV (asl_comment_location_INTRO_CONV new_c2))) thm1 1806 1807 val thm2 = CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 1808 (block_second_CONV (asl_comment_location_INTRO_CONV new_c3))) thm2a 1809 1810in 1811 thm2 1812end; 1813 1814 1815 1816 1817(******************************************************************************) 1818(* HANDLE block specs *) 1819(******************************************************************************) 1820 1821(* 1822val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1823*) 1824fun VAR_RES_COND_INFERENCE___block_spec___CONSEQ_CONV tt = 1825let 1826 (* destruct everything *) 1827 val (p1_0,c_opt,_,_,_,thm0_fun) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt; 1828 val (PQ',p1) = dest_asl_comment_block_spec p1_0; 1829 val (P',Q') = pairSyntax.dest_pair PQ'; 1830 val c = if isSome c_opt then valOf c_opt else empty_label_list; 1831 1832 (*introduce constants*) 1833 val thm_const = CONV_RULE (RHS_CONV 1834 VAR_RES_COND_INFERENCE___PREPARE_FOR_FRAME___CONV) (thm0_fun()) 1835 val (vs, tt') = strip_forall (rhs (concl thm_const)) 1836 1837 1838 (*apply inference*) 1839 val (vc, _) = pairSyntax.dest_pabs P'; 1840 val P_thm = pairTools.PABS_ELIM_CONV P' handle UNCHANGED => REFL P'; 1841 val Q_thm = pairTools.PABS_ELIM_CONV Q' handle UNCHANGED => REFL Q'; 1842 1843 val pair_PQ_CONV = (RAND_CONV (K Q_thm)) THENC 1844 (RATOR_CONV (RAND_CONV (K P_thm))) 1845 1846 val thm0a = VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV 1847 (RATOR_CONV (RAND_CONV pair_PQ_CONV)) tt' 1848 1849 val thm0b = HO_PART_MATCH (snd o dest_imp o snd o dest_imp) 1850 VAR_RES_COND_INFERENCE___block_spec 1851 (rhs (concl thm0a)) 1852 1853 val thm0 = CONV_RULE ((RAND_CONV o RAND_CONV) ((DEPTH_CONV BETA_CONV) THENC 1854 (K (GSYM thm0a)))) thm0b 1855 1856 (*elim precond*) 1857 val precond = (fst o dest_imp o concl) thm0 1858 val precond_thm1 = PART_MATCH (fst o dest_imp) var_res_prop___IMPLIES_VAR_DISTINCT 1859 ((fst o dest_imp) precond) 1860 val precond_thm2_term = mk_imp ((snd o dest_imp o concl) precond_thm1, 1861 (snd o dest_imp) precond) 1862 val precond_thm2 = var_res_prove precond_thm2_term; 1863 val precond_thm = IMP_TRANS precond_thm1 precond_thm2; 1864 val thm1 = MP thm0 precond_thm; 1865 1866 (*simplify invariant*) 1867 val post_prop = (rand o snd o dest_forall o rand o rator o fst o dest_imp o concl) thm1; 1868 val post_prop_thm = ((DEPTH_CONV BETA_CONV) THENC 1869 var_res_prop_input_distinct___ELIM_CONV NONE THENC 1870 COND_PROP___STRONG_EXISTS_NORMALISE_CONV) post_prop; 1871 1872 val pre_prop = (rand o rator o rator o snd o dest_forall o rand o rator o fst o dest_imp o concl) thm1; 1873 val pre_prop_thm = ((DEPTH_CONV BETA_CONV) THENC 1874 var_res_prop_input_distinct___ELIM_CONV NONE THENC 1875 COND_PROP___STRONG_EXISTS_NORMALISE_CONV) pre_prop; 1876 1877 val thm2 = CONV_RULE ((RATOR_CONV o RAND_CONV) (DEPTH_CONV ( 1878 (REWR_CONV pre_prop_thm) ORELSEC (REWR_CONV post_prop_thm)))) thm1 1879 1880 (*reintroduce orginal variable names*) 1881 val my_intro_conv = (pairTools.SPLIT_QUANT_CONV vc THENC 1882 TRY_CONV LIST_EXISTS_SIMP_CONV) 1883 1884 val thm3 = CONV_RULE ((RATOR_CONV o RAND_CONV) 1885 ((RATOR_CONV (RAND_CONV my_intro_conv)) THENC 1886 (RAND_CONV (my_intro_conv)))) thm2 1887 1888 (*introduce comment while-abstraction*) 1889 val new_c1 = asl_comment_modify_APPEND ("abstracted block-spec") c 1890 val thm4a = CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV o 1891 STRIP_QUANT_CONV o 1892 RATOR_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 1893 ((asl_comment_location2_INTRO_CONV new_c1) THENC 1894 (asl_comment_abstraction_INTRO_CONV "block-spec"))) thm3 1895 1896 (*introduce comment while-skip*) 1897 val new_c2 = asl_comment_modify_APPEND ("block-spec body") c 1898 val thm4 = CONV_RULE ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o STRIP_QUANT_CONV o 1899 RATOR_CONV o RAND_CONV o RAND_CONV o 1900 (fn conv => fn t => if listSyntax.is_nil t then conv t else 1901 (RATOR_CONV o RAND_CONV) conv t)) 1902 (asl_comment_location_INTRO_CONV new_c2)) thm4a 1903 1904 (*combine with thm_const*) 1905 val thm5a = LIST_GEN_IMP vs thm4 1906 val thm5 = CONV_RULE (RAND_CONV (K (GSYM thm_const))) thm5a 1907in 1908 thm5 1909end; 1910 1911 1912 1913 1914 1915 1916(******************************************************************************) 1917(* HANDLE assignments *) 1918(******************************************************************************) 1919 1920(* 1921val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1922*) 1923 1924fun VAR_RES_COND_INFERENCE___assign___CONSEQ_CONV tt = 1925let 1926 val (p1, _, _, _, _, thm0_fun) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt; 1927 val (v, e) = dest_var_res_prog_assign p1 1928 1929 (* intro var *) 1930 val thm0a = thm0_fun(); 1931 val (intro, c, thm0b) = VAR_RES_COND_INFERENCE___CONST_INTRO___CONV 1932 (mk_var_res_exp_var v (type_of e)) NONE (rhs (concl thm0a)) 1933 val thm0 = TRANS thm0a thm0b 1934 val t' = let val ttt = rhs (concl thm0) in 1935 if intro then (snd (dest_forall ttt)) else ttt end 1936 1937 1938 val thm1a = PART_MATCH (snd o dest_imp o snd o dest_imp) 1939 VAR_RES_COND_INFERENCE___var_res_prog_assign t' 1940 val thm1b = var_res_precondition_prove thm1a; 1941 val thm1 = CONV_RULE ((RATOR_CONV o RAND_CONV o 1942 VAR_RES_COND_HOARE_TRIPLE___PRECOND_CONV o RAND_CONV) 1943 ((DEPTH_CONV BAG_IMAGE_CONV) THENC 1944 BAG_NORMALISE_CONV)) thm1b 1945 1946 1947 (* simplifying new precond *) 1948 val pre = (rand o rator o rator o fst o dest_imp o concl) thm1 1949 1950 val vc = pairSyntax.mk_pair (v, c); 1951 val vcL_t = listSyntax.mk_list ([vc], type_of vc); 1952 val pre_imp_thm = var_res_prop___var_res_prop_varlist_update___EVAL 1953 vcL_t pre 1954 1955 1956 val rw_thm = MATCH_MP VAR_RES_COND_HOARE_TRIPLE___COND_PROP_STRONG_EQUIV 1957 pre_imp_thm 1958 val thm2 = ANTE_CONV_RULE (REWR_CONV rw_thm) thm1 1959 1960 (* add new variable if necessary *) 1961 val thm3 = if intro then GEN_IMP c thm2 else thm2 1962 1963 (* recombine *) 1964 val thm4 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm3 1965 1966 (*eliminate new const, if not used*) 1967 val thm5 = ANTE_CONV_RULE (REWR_CONV FORALL_SIMP) thm4 handle 1968 UNCHANGED => thm4 1969 | HOL_ERR _ => thm4 1970in 1971 thm5 1972end; 1973 1974 1975(******************************************************************************) 1976(* HANDLE abstractions *) 1977(******************************************************************************) 1978 1979(*WARNING! Please remove! Just for debugging!!!*) 1980fun asl_comments_EQ_PROVE p1 p2 = REFL p1; 1981 1982(* 1983 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 1984*) 1985fun VAR_RES_COND_INFERENCE___abstracted_code___CONV tt = 1986let 1987 (*destruct*) 1988 val (p1,c_opt,_,_,_,thm0_fun) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt; 1989 1990 val (c2, body) = dest_asl_comment_abstraction p1 handle HOL_ERR _ => 1991 raise UNCHANGED; 1992 1993 (*update comments*) 1994 val c1_thm = ISPECL [c2,body] asl_comment_abstraction_def 1995 val c2_conv = if not (isSome c_opt) then ALL_CONV else 1996 let 1997 val new_c = asl_comment_modify_APPEND ("abstracted "^ 1998 (fst (dest_var c2))) (valOf c_opt) 1999 in 2000 asl_comment_location2_INTRO_CONV new_c 2001 end 2002 val c_conv = (K c1_thm) THENC c2_conv 2003 (*put into the context*) 2004 val thm0 = ((K (thm0_fun ())) THENC 2005 (VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV 2006 c_conv)) tt 2007in 2008 thm0 2009end; 2010 2011 2012(******************************************************************************) 2013(* HANDLE procedure_calls *) 2014(******************************************************************************) 2015 2016(* 2017 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 2018*) 2019local 2020val my_ss1 = simpLib.conv_ss {conv = K (K asl_procedure_call_preserve_names_wrapper_ELIM_CONV), 2021 key = NONE, name = "procedure_call_preserve_names_wrapper_ELIM", 2022 trace = 2} 2023 2024val my_ss2 = simpLib.conv_ss {conv = K (K pairLib.GEN_BETA_CONV), 2025 key = NONE, name = "GEN_BETA_CONV", 2026 trace = 2} 2027 2028val my_conv = SIMP_CONV (list_ss++my_ss1++my_ss2) [] 2029 2030in 2031fun VAR_RES_COND_INFERENCE___eval_expressions___CONV tt = 2032let 2033 (*destruct*) 2034 val (p1,pL,f,_,post) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt; 2035 val (c,p1',p1_thm_fun) = save_dest_asl_comment_location2 p1; 2036 val (p1'',expL_t) = dest_var_res_prog_eval_expressions p1' 2037 val (expL,_) = listSyntax.dest_list expL_t 2038 2039 (*introduce expressions if necessary*) 2040 val thm0a = VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV (K (p1_thm_fun ())) tt 2041 val thm0 = CONV_RULE (RHS_CONV (VAR_RES_COND_INFERENCE___CONST_LIST_INTRO___CONV 2042 (map (fn x => (x, NONE)) expL))) thm0a 2043 2044 (*destruct again*) 2045 val (vL, tt') = strip_forall (rhs (concl thm0)); 2046 val (_,_,_,pre,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt'; 2047 val (_, wpb, rpb, sfb, sfs) = dest_var_res_prop___propL pre 2048 2049 (*find constants*) 2050 fun var_res_exp___is_equals_const e n t = 2051 let 2052 val (_,l,r) = dest_var_res_prop_equal t 2053 in 2054 if (aconv l e) andalso (is_var_res_exp_const r) then 2055 SOME (dest_var_res_exp_const r) 2056 else if (aconv r e) andalso (is_var_res_exp_const l) then 2057 SOME (dest_var_res_exp_const l) 2058 else NONE 2059 end handle HOL_ERR _ => NONE; 2060 2061 fun get_const_for_exp e = 2062 if is_var_res_exp_const e then dest_var_res_exp_const e else 2063 let 2064 val found_opt = first_opt (var_res_exp___is_equals_const e) sfs; 2065 val _ = if isSome found_opt then () else raise UNCHANGED; 2066 val c = valOf found_opt 2067 in 2068 c 2069 end; 2070 val cL = map get_const_for_exp expL 2071 2072 (*build thm*) 2073 val thm1a = ISPECL [f,wpb,rpb,sfb,expL_t] VAR_RES_COND_INFERENCE___eval_expressions 2074 val cL_type = (listSyntax.dest_list_type o type_of o fst o dest_forall o concl) thm1a; 2075 val cL_t = listSyntax.mk_list (cL, cL_type) 2076 2077 val thm1b = ISPECL [cL_t,p1'',pL,post] thm1a 2078 2079 val thm1c = var_res_precondition_prove thm1b 2080 val thm1d = LIST_GEN_EQ vL thm1c 2081 2082 val thm2 = TRANS thm0 thm1d 2083 2084 (*simplify*) 2085 val thm3 = CONV_RULE ((RHS_CONV o STRIP_QUANT_CONV o RATOR_CONV o 2086 RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 2087 my_conv) thm2 2088 2089 (*reintroduce comment*) 2090 val (p1''',_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND 2091 (snd (strip_forall (rhs (concl thm3)))); 2092 2093 val p1'''_thm = GSYM (ISPECL [c, p1'''] asl_comment_location2_def) 2094 val thm4 = CONV_RULE (STRIP_QUANT_CONV (RHS_CONV 2095 (VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV (K p1'''_thm)))) thm3 2096in 2097 thm4 2098end 2099end; 2100 2101 2102(* 2103 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 2104*) 2105fun VAR_RES_COND_INFERENCE___quant_best_local_action___CONSEQ_CONV tt = 2106let 2107 (*destruct*) 2108 val (p1,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt; 2109 val (c,p1',p1_thm_fun) = save_dest_asl_comment_location2 p1 2110 val (has_cond, (pre, _)) = 2111 (false, dest_var_res_prog_quant_best_local_action p1') handle HOL_ERR _ => 2112 (true, dest_var_res_prog_cond_quant_best_local_action p1') 2113 val vc = fst (pairSyntax.dest_pabs pre) 2114 2115 (*elim comment*) 2116 val thm0a = p1_thm_fun (); 2117 val thm0 = (VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV (K thm0a) 2118 THENC VAR_RES_COND_INFERENCE___PREPARE_FOR_FRAME___CONV) tt 2119 val (vs, tt') = strip_forall (rhs (concl thm0)) 2120 2121 2122 (*apply inference*) 2123 val base_thm = if has_cond then 2124 VAR_RES_COND_INFERENCE___var_res_prog_cond_quant_best_local_action else 2125 VAR_RES_COND_INFERENCE___var_res_prog_quant_best_local_action 2126 val thm1 = (HO_PART_MATCH (snd o dest_imp) base_thm) tt' 2127 2128 (*use PBETA_CONV*) 2129 val thm2 = ANTE_CONV_RULE 2130 (VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV 2131 (TRY_CONV (RAND_CONV PairRules.PBETA_CONV) THENC 2132 TRY_CONV (RATOR_CONV (RAND_CONV PairRules.PBETA_CONV)))) 2133 thm1 2134 2135 (*introduce comments*) 2136 val (p1'',_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND 2137 ((snd o dest_exists o fst o dest_imp o concl) thm2); 2138 val p1''_thm = ISPECL [c, p1''] asl_comment_location2_def; 2139 2140 val thm3 = CONV_RULE ( 2141 (RATOR_CONV o RAND_CONV o QUANT_CONV o 2142 VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV) 2143 (K (GSYM p1''_thm))) thm2 2144 2145 2146 (*use correct vars*) 2147 val thm4 = ANTE_CONV_RULE (pairTools.SPLIT_QUANT_CONV vc) thm3 2148 2149 (*combine with thm0*) 2150 val thm5a = LIST_GEN_IMP vs thm4 2151 val thm5 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm5a 2152 2153in 2154 thm5 2155end 2156 2157 2158(* 2159 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 2160*) 2161fun VAR_RES_COND_INFERENCE___best_local_action___CONV tt = 2162let 2163 (*destruct*) 2164 val (p1,progL,f,P,Q) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt; 2165 val (c,p1',p1_thm_fun) = save_dest_asl_comment_location2 p1 2166 val need_star = is_asl_star (rand p1') 2167 2168 (*apply_rewrite*) 2169 val thm1a = HO_PART_MATCH (lhs o snd o dest_imp) 2170 (if need_star then 2171 var_res_prog_cond_best_local_action_INTRO_star 2172 else 2173 var_res_prog_cond_best_local_action_INTRO) p1'; 2174 val a = (fst o dest_imp o concl) thm1a; 2175 val thm1b = UNDISCH thm1a; 2176 val thm1 = RAND_CONV (K thm1b) (mk_asl_comment_location2 (c, p1')) 2177 2178 (*normalise pre- / post-cond and reintroduce pabs*) 2179 val norm_conv = var_res_prop_input_distinct___ELIM_CONV (SOME a) THENC 2180 TRY_CONV COND_PROP___STRONG_EXISTS_NORMALISE_CONV 2181 val thm2 = DISCH a (CONV_RULE (RHS_CONV (DEPTH_CONV norm_conv)) thm1) 2182 2183 (*put it in context*) 2184 val p1' = (rhs o snd o dest_imp o concl) thm2; 2185 val (_, wpb, rpb, sfb) = dest_var_res_prop P 2186 2187 val thm3a = ISPECL [f, p1, p1', wpb, rpb, sfb, progL, Q] 2188 VAR_RES_COND_INFERENCE___first_command_REWRITE 2189 val precond = (fst o dest_imp o fst o dest_imp o concl) thm3a 2190 val precond_thm0 = var_res_prove (mk_imp (precond, a)); 2191 val precond_thm = IMP_TRANS precond_thm0 thm2 2192 2193 val thm3 = MP thm3a precond_thm 2194in 2195 thm3 2196end 2197 2198(* 2199 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 2200*) 2201fun VAR_RES_COND_INFERENCE___cond_best_local_action___CONV tt = 2202let 2203 (*destruct*) 2204 val (p1,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt; 2205 val (c,p1',p1_thm_fun) = save_dest_asl_comment_location2 p1 2206 val (pre,post) = dest_var_res_prog_cond_best_local_action p1'; 2207 2208 2209 2210 (*bring exists in p1 in normal form*) 2211 val (vc_pre, pre_thm) = COND_PROP___STRONG_EXISTS_INTRO___CONV pre; 2212 val (vc_post, post_thm) = COND_PROP___STRONG_EXISTS_INTRO___CONV post; 2213 2214 val thm0 = ((VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV 2215 ((K (p1_thm_fun ())) THENC 2216 RAND_CONV (K post_thm) THENC 2217 RATOR_CONV (RAND_CONV (K pre_thm))))) tt 2218 2219 (*apply inference*) 2220 val new_comment = asl_comment_modify_APPEND "final" c; 2221 val rfc = pairSyntax.mk_pair (T, optionSyntax.mk_some new_comment) 2222 2223 val thm1a = HO_PART_MATCH (snd o dest_imp o snd o dest_imp) 2224 (ISPEC rfc VAR_RES_COND_INFERENCE___var_res_prog_cond_best_local_action___EXISTS_VAR_CHANGE) 2225 (rhs (concl thm0)) 2226 val thm1b = var_res_precondition_prove thm1a; 2227 val thm1 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm1b 2228 2229 2230 (*get original existential vars back*) 2231 val new_tt = (fst o dest_imp o concl) thm1 2232 fun quant_restore_CONV NONE = (REWR_CONV boolTheory.FORALL_SIMP) ORELSEC (REWR_CONV boolTheory.EXISTS_SIMP) 2233 | quant_restore_CONV (SOME vc) = pairTools.SPLIT_QUANT_CONV vc 2234 2235 val new_tt_thm = (quant_restore_CONV vc_pre THENC 2236 ((STRIP_QUANT_CONV o RAND_CONV o ABS_CONV) 2237 (quant_restore_CONV vc_post))) new_tt 2238 val thm2 = ANTE_CONV_RULE (K new_tt_thm) thm1 2239in 2240 thm2 2241end 2242 2243local 2244 2245 fun COND_PROP___STRONG_IMP___strong_exists_asl_cond_star___ELIM exists_cond_term = 2246 let 2247 val (v, cond_term) = dest_COND_PROP___STRONG_EXISTS exists_cond_term; 2248 2249 val thm0 = PART_MATCH (rand o rator o snd o dest_imp) 2250 COND_PROP___STRONG_IMP___asl_cond_star___var_res_prop 2251 cond_term 2252 val bag_conv = bagLib.SIMPLE_BAG_NORMALISE_CONV 2253 val thm1 = CONV_RULE ((RAND_CONV o RAND_CONV) 2254 (RAND_CONV bag_conv THENC 2255 ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) bag_conv))) thm0 2256 2257 val precond = (fst o dest_imp o concl) thm1 2258 2259 val thm2 = GEN v (UNDISCH thm1) 2260 val thm3 = HO_MATCH_MP COND_PROP___STRONG_EXISTS___COND_PROP___STRONG_IMP thm2 2261 in 2262 (thm3, precond) 2263 end; 2264 2265in 2266 2267(* 2268 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 2269*) 2270fun VAR_RES_COND_INFERENCE___cond_best_local_action___asl_cond_star___CONSEQ_CONV tt = 2271let 2272 (*destruct*) 2273 val (p1,pL,f,P,Q) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt; 2274 val (_, wpb, rpb, sfb) = dest_var_res_prop P; 2275 2276 val (c,p1',p1_thm_fun) = save_dest_asl_comment_location2 p1; 2277 val (pre,post) = dest_var_res_prog_cond_best_local_action p1'; 2278 val _ = if (is_asl_cond_star pre) andalso (is_asl_cond_star post) then () else raise UNCHANGED; 2279 2280 (*bring COND_PROP___STRONG_EXISTS in normal form*) 2281 val (vc_pre1, pre1_thm) = COND_PROP___STRONG_EXISTS_INTRO___CONV ((rand o rator) pre); 2282 val (vc_pre2, pre2_thm) = COND_PROP___STRONG_EXISTS_INTRO___CONV (rand pre); 2283 2284 val (vc_post1, post1_thm) = COND_PROP___STRONG_EXISTS_INTRO___CONV ((rand o rator) post); 2285 val (vc_post2, post2_thm) = COND_PROP___STRONG_EXISTS_INTRO___CONV (rand post); 2286 2287 2288 val pre_thm0 = (((RAND_CONV (K pre2_thm)) THENC 2289 ((RATOR_CONV (RAND_CONV (K pre1_thm))))) pre) 2290 val pre_thm = CONV_RULE (RHS_CONV ( 2291 (HO_PART_MATCH lhs asl_cond_star___COND_PROP___STRONG_EXISTS___BOTH))) pre_thm0 2292 2293 val post_thm0 = (((RAND_CONV (K post2_thm)) THENC 2294 ((RATOR_CONV (RAND_CONV (K post1_thm))))) post) 2295 val post_thm = CONV_RULE (RHS_CONV ( 2296 (HO_PART_MATCH lhs asl_cond_star___COND_PROP___STRONG_EXISTS___BOTH))) post_thm0 2297 2298 val thm0a = p1_thm_fun (); 2299 val thm0 = (VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV 2300 ((K thm0a) THENC 2301 RAND_CONV (K post_thm) THENC 2302 RATOR_CONV (RAND_CONV (K pre_thm)))) tt 2303 2304 (*remove asl_cond_star*) 2305 val (cond_pre, cond_post) = 2306 (dest_var_res_prog_cond_best_local_action o #1 o 2307 dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND o rhs o concl) thm0 2308 2309 val (cond_pre_thm, pre_pre) = COND_PROP___STRONG_IMP___strong_exists_asl_cond_star___ELIM cond_pre 2310 val (cond_post_thm, pre_post) = COND_PROP___STRONG_IMP___strong_exists_asl_cond_star___ELIM cond_post 2311 2312 2313 val thm1a = (MATCH_MP (ISPEC f var_res_prog_cond_best_local_action___STRONG_IMP___pre_post) 2314 (CONJ cond_pre_thm cond_post_thm)); 2315 val (pre,thm1b) = if (aconv pre_pre pre_post) then (pre_pre,thm1a) else 2316 let 2317 val pre = mk_conj (pre_pre, pre_post); 2318 val pre_thm = ASSUME pre 2319 val xthm1 = MP (DISCH pre_pre thm1a) (CONJUNCT1 pre_thm) 2320 val xthm2 = MP (DISCH pre_post xthm1) (CONJUNCT2 pre_thm) 2321 in 2322 (pre, xthm2) 2323 end; 2324 2325 2326 val pre_imp_t = mk_imp (bagSyntax.mk_all_distinct (bagSyntax.mk_union (wpb,rpb)), pre); 2327 val pre_imp_thm = var_res_prove pre_imp_t; 2328 val thm1c = DISCH (fst (dest_imp pre_imp_t)) (MP (DISCH pre thm1b) (UNDISCH pre_imp_thm)) 2329 val thm1d = ISPECL [sfb, pL, Q] 2330 (MATCH_MP VAR_RES_COND_HOARE_TRIPLE___PROGRAM_ABSTRACTION_first_block thm1c) 2331 val thm1 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm1d 2332 2333 (*apply inference*) 2334 val new_comment = asl_comment_modify_APPEND " - final" c; 2335 val rfc = pairSyntax.mk_pair (T, optionSyntax.mk_some new_comment) 2336 2337 val thm2a = HO_PART_MATCH (snd o dest_imp o snd o dest_imp) 2338 (ISPEC rfc VAR_RES_COND_INFERENCE___var_res_prog_cond_best_local_action___EXISTS_VAR_CHANGE) 2339 ((fst o dest_imp o concl) thm1) 2340 val thm2b = var_res_precondition_prove thm2a; 2341 val bag_conv = bagLib.SIMPLE_BAG_NORMALISE_CONV 2342 val thm2c = CONV_RULE ((RATOR_CONV o RAND_CONV o QUANT_CONV o RAND_CONV o 2343 ABS_CONV o QUANT_CONV o RATOR_CONV o RATOR_CONV o RAND_CONV o 2344 RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 2345 bag_conv) thm2b 2346 2347 val thm2 = IMP_TRANS thm2c thm1 2348 2349 2350 (*get original existential vars back*) 2351 val new_tt = (fst o dest_imp o concl) thm2 2352 fun quant_restore_CONV NONE = (REWR_CONV boolTheory.FORALL_SIMP) ORELSEC (REWR_CONV boolTheory.EXISTS_SIMP) 2353 | quant_restore_CONV (SOME vc) = 2354 pairTools.SPLIT_QUANT_CONV vc 2355 2356 2357 fun mk_vc NONE NONE = NONE 2358 | mk_vc vc1_opt vc2_opt = 2359 let 2360 val vc1 = if isSome vc1_opt then (valOf vc1_opt) else (genvar (Type `:unit`)); 2361 val vc2 = if isSome vc2_opt then (valOf vc2_opt) else (genvar (Type `:unit`)); 2362 val (_,sub) = quantHeuristicsTools.list_variant (free_vars vc1) (free_vars vc2) 2363 val vc2' = subst sub vc2; 2364 in 2365 SOME (pairSyntax.mk_pair(vc1, vc2')) 2366 end 2367 2368 val vc_pre = mk_vc vc_pre1 vc_pre2 2369 val vc_post = mk_vc vc_post1 vc_post2 2370 val new_tt_thm = (quant_restore_CONV vc_pre THENC 2371 ((STRIP_QUANT_CONV o RAND_CONV o ABS_CONV) 2372 (quant_restore_CONV vc_post))) new_tt 2373 val thm3 = ANTE_CONV_RULE (K new_tt_thm) thm2 2374 2375in 2376 thm3 2377end 2378 2379end 2380 2381(******************************************************************************) 2382(* Assert *) 2383(******************************************************************************) 2384 2385(* 2386 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 2387*) 2388fun VAR_RES_COND_INFERENCE___assert___CONSEQ_CONV tt = 2389let 2390 (* destruct everything *) 2391 val (p1_0,c_opt,_,_,_,thm0_fun) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location tt; 2392 val P' = dest_asl_comment_assert p1_0; 2393 val c = if isSome c_opt then valOf c_opt else empty_label_list; 2394 2395 (*introduce constants*) 2396 val thm_const = CONV_RULE (RHS_CONV 2397 VAR_RES_COND_INFERENCE___PREPARE_FOR_FRAME___CONV) (thm0_fun()) 2398 val (vs, tt') = strip_forall (rhs (concl thm_const)) 2399 2400 (*apply inference*) 2401 val (vc, _) = pairSyntax.dest_pabs P'; 2402 val P_thm = pairTools.PABS_ELIM_CONV P' handle UNCHANGED => REFL P'; 2403 2404 val thm0a = VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV 2405 (RAND_CONV (K P_thm)) tt' 2406 2407 val thm0b = HO_PART_MATCH (snd o dest_imp) 2408 VAR_RES_COND_INFERENCE___comment_assert 2409 (rhs (concl thm0a)) 2410 2411 val thm0 = CONV_RULE ((RAND_CONV) ((DEPTH_CONV BETA_CONV) THENC 2412 (K (GSYM thm0a)))) thm0b 2413 2414 (*simplify assertion*) 2415 val a_prop = (rand o rand o rator o rand o rand o rator o snd o dest_exists o fst o dest_imp o concl) thm0; 2416 val a_prop_thm = ((DEPTH_CONV BETA_CONV) THENC 2417 var_res_prop_internal___ELIM_CONV THENC 2418 COND_PROP___STRONG_EXISTS_NORMALISE_CONV) a_prop; 2419 2420 val thm1 = CONV_RULE ((RATOR_CONV o RAND_CONV o QUANT_CONV o 2421 VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV) 2422 (DEPTH_CONV (REWR_CONV a_prop_thm))) thm0 2423 2424 (*reintroduce orginal variable names*) 2425 val my_intro_conv = (pairTools.SPLIT_QUANT_CONV vc THENC 2426 TRY_CONV LIST_EXISTS_SIMP_CONV) 2427 2428 val thm2 = CONV_RULE ((RATOR_CONV o RAND_CONV) my_intro_conv) thm1 2429 2430 (*introduce comment*) 2431 val new_c1 = asl_comment_modify_APPEND ("assertion") c 2432 val thm3 = CONV_RULE ((RATOR_CONV o RAND_CONV o 2433 STRIP_QUANT_CONV o 2434 RATOR_CONV o RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 2435 ((asl_comment_location2_INTRO_CONV new_c1))) thm2 2436 2437 (*combine with thm_const*) 2438 val thm4a = LIST_GEN_IMP vs thm3 2439 val thm4 = CONV_RULE (RAND_CONV (K (GSYM thm_const))) thm4a 2440in 2441 thm4 2442end 2443 2444 2445(******************************************************************************) 2446(* Locks *) 2447(******************************************************************************) 2448 2449(* 2450 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 2451*) 2452fun VAR_RES_COND_INFERENCE___release_lock___CONV tt = 2453let 2454 (*destruct*) 2455 val (p1,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt; 2456 val (p1', c, thm0a) = let 2457 val (c, p1') = dest_asl_comment_location2 p1 2458 val _ = if is_var_res_prog_release_lock p1' then () else raise UNCHANGED 2459 val c_thm = ISPECL [c, p1'] asl_comment_location2_def; 2460 val thm0a = VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV (K c_thm) tt 2461 in 2462 (p1', c, thm0a) 2463 end handle UNCHANGED => 2464 if is_var_res_prog_release_lock p1 then (p1, empty_label_list, REFL tt) else raise UNCHANGED 2465 val thm0 = CONV_RULE (RHS_CONV VAR_RES_COND_INFERENCE___ALL_CONST_INTRO___CONV) thm0a 2466 val (vs, tt') = strip_forall (rhs (concl thm0)) 2467 2468 2469 (*apply inference*) 2470 val rfc = pairSyntax.mk_pair (T, optionSyntax.mk_some c) 2471 val thm1a = HO_PART_MATCH (snd o dest_imp o snd o dest_imp) 2472 (SPEC rfc VAR_RES_COND_INFERENCE___var_res_prog_release_lock) tt' 2473 val thm1 = var_res_precondition_prove thm1a; 2474 2475 (*combine with thm0*) 2476 val thm2a = LIST_GEN_IMP vs thm1 2477 val thm2 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm2a 2478in 2479 thm2 2480end 2481 2482 2483(* 2484 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 2485*) 2486fun VAR_RES_COND_INFERENCE___aquire_lock___CONV tt = 2487let 2488 (*destruct*) 2489 val (p1,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND tt; 2490 val (p1', thm0a) = let 2491 val (c, p1') = dest_asl_comment_location2 p1 2492 val _ = if is_var_res_prog_aquire_lock p1' then () else raise UNCHANGED 2493 val c_thm = ISPECL [c, p1'] asl_comment_location2_def; 2494 val thm0a = VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV (K c_thm) tt 2495 in 2496 (p1', thm0a) 2497 end handle UNCHANGED => 2498 if is_var_res_prog_aquire_lock p1 then (p1, REFL tt) else raise UNCHANGED 2499 val thm0 = CONV_RULE (RHS_CONV VAR_RES_COND_INFERENCE___ALL_CONST_INTRO___CONV) thm0a 2500 val (vs, tt') = strip_forall (rhs (concl thm0)) 2501 2502 (*apply inference*) 2503 val thm1a = HO_PART_MATCH (snd o dest_imp o snd o dest_imp) 2504 VAR_RES_COND_INFERENCE___var_res_prog_aquire_lock 2505 (rhs (concl thm0)) 2506 val thm1 = var_res_precondition_prove thm1a; 2507 2508 2509 (*simplify*) 2510 val bag_conv = bagLib.SIMPLE_BAG_NORMALISE_CONV 2511 val thm2 = CONV_RULE ((RATOR_CONV o RAND_CONV o VAR_RES_COND_HOARE_TRIPLE___PRECOND_CONV) 2512 ((RAND_CONV bag_conv) THENC 2513 ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) bag_conv))) thm1 2514 2515 (*combine with thm0*) 2516 val thm3a = LIST_GEN_IMP vs thm2 2517 val thm3 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm3a 2518in 2519 thm3 2520end 2521 2522(******************************************************************************) 2523(* Simplify preconds *) 2524(******************************************************************************) 2525(* 2526 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 2527*) 2528fun VAR_RES_COND_INFERENCE___PRECOND_bool_pred___CONV ss context tt = 2529let 2530 val thm0 = VAR_RES_COND_HOARE_TRIPLE___FIND_RESORT_PRECOND_CONV 2531 is_var_res_bool_proposition tt 2532 val thm1 = CONV_RULE (RHS_CONV ( 2533 REWR_CONV VAR_RES_COND_INFERENCE___var_res_bool_proposition)) thm0 2534 val thm2 = CONV_RULE ((RHS_CONV o RATOR_CONV o RAND_CONV) 2535 (VAR_RES_PROP_REWRITE_CONV ss context)) thm1 2536in 2537 thm2 2538end; 2539 2540fun VAR_RES_COND_INFERENCE___PRECOND_trivial_cond___CONV tt = 2541let 2542 val thm0 = VAR_RES_COND_HOARE_TRIPLE___FIND_RESORT_PRECOND_CONV 2543 is_asl_trivial_cond tt 2544 val thm1 = CONV_RULE (RHS_CONV ( 2545 REWR_CONV VAR_RES_COND_INFERENCE___asl_trivial_cond)) thm0 2546in 2547 thm1 2548end; 2549 2550 2551fun VAR_RES_COND_INFERENCE___PRECOND_stack_true___CONV tt = 2552let 2553 val thm0 = VAR_RES_COND_HOARE_TRIPLE___FIND_RESORT_PRECOND_CONV 2554 is_var_res_prop_stack_true tt 2555 val thm1 = CONV_RULE (RHS_CONV ( 2556 REWR_CONV VAR_RES_COND_INFERENCE___var_res_prop_stack_true)) thm0 2557in 2558 thm1 2559end; 2560 2561 2562fun VAR_RES_COND_INFERENCE___PRECOND_false___CONV tt = 2563let 2564 val thm0 = VAR_RES_COND_HOARE_TRIPLE___FIND_RESORT_PRECOND_CONV 2565 is_asl_false tt 2566 val thm1 = EQT_INTRO (PART_MATCH I VAR_RES_COND_INFERENCE___false_precond (rhs (concl thm0))) 2567 val thm2 = TRANS thm0 thm1 2568in 2569 thm2 2570end; 2571 2572 2573fun VAR_RES_COND_INFERENCE___PRECOND_REWRITE___CONV ss context t = 2574 VAR_RES_COND_HOARE_TRIPLE___PRECOND_CONV 2575 (VAR_RES_PROP_REWRITE_CONV ss context) t; 2576 2577 2578 2579fun VAR_RES_COND_INFERENCE___PRECOND_asl_exists___CONV tt = 2580let 2581 val thm0 = VAR_RES_COND_HOARE_TRIPLE___FIND_RESORT_PRECOND_CONV 2582 is_asl_exists tt 2583 2584 val thm1 = HO_PART_MATCH (lhs o snd o dest_imp) VAR_RES_COND_INFERENCE___asl_exists_pre 2585 (rhs (concl thm0)) 2586 val thm2 = var_res_precondition_prove thm1 handle e => raise_var_res_prove_expn e 2587 val thm3 = TRANS thm0 thm2 2588in 2589 thm3 2590end; 2591 2592 2593fun VAR_RES_COND_INFERENCE___PRECOND_asl_star___CONV tt = 2594let 2595 val thm0 = VAR_RES_COND_HOARE_TRIPLE___FIND_RESORT_PRECOND_CONV 2596 is_asl_star tt 2597 2598 val thm1 = PART_MATCH (lhs o snd o dest_imp) VAR_RES_COND_INFERENCE___asl_star_pre 2599 (rhs (concl thm0)) 2600 val thm2 = var_res_precondition_prove thm1; 2601 val thm3 = TRANS thm0 thm2 2602in 2603 thm3 2604end; 2605 2606 2607 2608(******************************************************************************) 2609(* ENTAILMENTS *) 2610(******************************************************************************) 2611 2612fun VAR_RES_FRAME_SPLIT_INFERENCE___PROP_REWRITE___CONV ss context t = 2613 VAR_RES_FRAME_SPLIT___PROP_CONV 2614 (VAR_RES_PROP_REWRITE_CONV ss context) t; 2615 2616 2617(* 2618 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2619*) 2620fun VAR_RES_FRAME_SPLIT_INFERENCE___VAR_EQ_CONST_TO_CONTEXT___CONV tt = 2621let 2622 val (f, _, _, _, _, split_sfb, _, _) = dest_VAR_RES_FRAME_SPLIT tt; 2623 2624 (* sort all equations out *) 2625 val (vcL_t, split_thm) = var_res_prop___var_eq_const_BAG___INTRO f split_sfb; 2626 val thm0 = VAR_RES_FRAME_SPLIT___split_CONV (K split_thm) tt 2627 2628 (* apply the inference *) 2629 val thm1a = PART_MATCH (snd o dest_imp) VAR_RES_FRAME_SPLIT___equal_const (rhs (concl thm0)) 2630 val thm1 = CONV_RULE (RAND_CONV (K (GSYM thm0))) thm1a 2631 2632 (* simplify *) 2633 val thm2 = ANTE_CONV_RULE (VAR_RES_FRAME_SPLIT___context_split_imp_CONV 2634 ((DEPTH_CONV BAG_IMAGE_CONV) THENC BAG_NORMALISE_CONV)) thm1 2635 2636 2637 (*update vars*) 2638 val (_, _, wr, _, context_sfb, split_sfb, imp_sfb, _) = 2639 dest_VAR_RES_FRAME_SPLIT ((fst o dest_imp) (concl thm2)); 2640 val (wpb,rpb) = dest_pair wr 2641 val (precond, rewrL) = GENERATE___var_res_exp_varlist_update___REWRITES wpb rpb vcL_t; 2642 2643 fun save_conv t = (cond_rewrite___varlist_update rewrL t) handle UNCHANGED => REFL t 2644 val context_thm = save_conv context_sfb 2645 val split_thm = save_conv split_sfb 2646 val imp_thm = save_conv imp_sfb 2647 val conj_thm0 = DISCH precond (LIST_CONJ [context_thm, split_thm, imp_thm]) 2648 val conj_thm = var_res_assumptions_prove conj_thm0 2649 2650 val thm3a = 2651 MATCH_MP ( 2652 ISPEC f VAR_RES_FRAME_SPLIT___WEAK_COND_REWRITE) conj_thm 2653 val thm3 = ANTE_CONV_RULE (PART_MATCH lhs thm3a) thm2 2654in 2655 thm3 2656end; 2657 2658 2659 2660(* searches common terms in two lists of terms and returns the positions*) 2661 2662 2663(* 2664 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2665*) 2666fun VAR_RES_FRAME_SPLIT_INFERENCE___FRAME___CONV tt = 2667let 2668 val (_, _, _, _, _, split_sfb, imp_sfb, _) = dest_VAR_RES_FRAME_SPLIT tt; 2669 2670 (* find a proposition that occurs in both *) 2671 val (n1l, n2l) = get_resort_lists___pred_pair aconv split_sfb imp_sfb 2672 val _ = if null n1l then raise UNCHANGED else (); 2673 (*resort*) 2674 2675 (*apply inference*) 2676 val thm0 = (VAR_RES_FRAME_SPLIT___split_CONV (BAG_RESORT_CONV n1l) THENC 2677 VAR_RES_FRAME_SPLIT___imp_CONV (BAG_RESORT_CONV n2l) THENC 2678 REPEATC (PART_MATCH lhs VAR_RES_FRAME_SPLIT___FRAME)) tt 2679in 2680 thm0 2681end; 2682 2683 2684 2685(* 2686 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2687*) 2688fun VAR_RES_FRAME_SPLIT_INFERENCE___stack_true___CONV tt = 2689let 2690 val (_, _, _, _, context_sfb, split_sfb, imp_sfb, _) = dest_VAR_RES_FRAME_SPLIT tt; 2691 2692 fun resort_list sfb = get_resort_list___pred is_var_res_prop_stack_true sfb 2693 val context_nl = resort_list context_sfb 2694 val split_nl = resort_list split_sfb 2695 val imp_nl = resort_list imp_sfb 2696 2697 val _ = if (null context_nl) andalso (null split_nl) andalso (null imp_nl) then 2698 raise UNCHANGED else () 2699 (*resort*) 2700 2701 (*apply inference*) 2702 val conv_context = if null context_nl then ALL_CONV else 2703 (VAR_RES_FRAME_SPLIT___context_CONV (BAG_RESORT_CONV context_nl) THENC 2704 REPEATC (PART_MATCH lhs VAR_RES_FRAME_SPLIT___stack_true___context)) 2705 val conv_split = if null split_nl then ALL_CONV else 2706 (VAR_RES_FRAME_SPLIT___split_CONV (BAG_RESORT_CONV split_nl) THENC 2707 REPEATC (PART_MATCH lhs VAR_RES_FRAME_SPLIT___stack_true___split)) 2708 val conv_imp = if null imp_nl then ALL_CONV else 2709 (VAR_RES_FRAME_SPLIT___imp_CONV (BAG_RESORT_CONV imp_nl) THENC 2710 REPEATC (PART_MATCH lhs VAR_RES_FRAME_SPLIT___stack_true___imp)) 2711 2712 val thm0 = (conv_context THENC conv_split THENC conv_imp) tt 2713in 2714 thm0 2715end; 2716 2717 2718(* 2719 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2720*) 2721fun VAR_RES_FRAME_SPLIT_INFERENCE___bool_pred___CONV ss context tt = 2722let 2723 val (_, _, _, _, context_sfb, split_sfb, imp_sfb, _) = dest_VAR_RES_FRAME_SPLIT tt; 2724 2725 fun resort_list sfb = get_resort_list___pred is_var_res_bool_proposition sfb 2726 val context_nl = resort_list context_sfb 2727 val split_nl = resort_list split_sfb 2728 val imp_nl = resort_list imp_sfb 2729 2730 val _ = if (null context_nl) andalso (null split_nl) andalso (null imp_nl) then 2731 raise UNCHANGED else () 2732 2733 (*apply inference*) 2734 val precond_simp_conv = (RATOR_CONV (RAND_CONV (VAR_RES_PROP_REWRITE_CONV ss context))) 2735 fun conv_context1 t = ((PART_MATCH lhs VAR_RES_FRAME_SPLIT___bool_proposition___context) THENC 2736 precond_simp_conv THENC 2737 (TRY_CONV (RAND_CONV conv_context1))) t 2738 val conv_context = if null context_nl then ALL_CONV else 2739 (VAR_RES_FRAME_SPLIT___context_CONV (BAG_RESORT_CONV context_nl) THENC 2740 conv_context1) 2741 fun conv_split1 t = ((PART_MATCH lhs VAR_RES_FRAME_SPLIT___bool_proposition___split) THENC 2742 precond_simp_conv THENC 2743 (TRY_CONV (RAND_CONV conv_split1))) t 2744 2745 val conv_split = if null split_nl then ALL_CONV else 2746 (VAR_RES_FRAME_SPLIT___split_CONV (BAG_RESORT_CONV split_nl) THENC 2747 conv_split1) 2748 2749 val conv_imp = if (length imp_nl) < 2 then ALL_CONV else 2750 (VAR_RES_FRAME_SPLIT___imp_CONV (BAG_RESORT_CONV imp_nl) THENC 2751 REPEATC (PART_MATCH lhs VAR_RES_FRAME_SPLIT___bool_proposition___imp)) 2752 2753 val thm0 = (conv_imp THENC conv_split THENC ONCE_DEPTH_CONV conv_context) tt 2754in 2755 thm0 2756end; 2757 2758 2759(* 2760 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2761*) 2762fun VAR_RES_FRAME_SPLIT_INFERENCE___asl_star___CONV tt = 2763let 2764 val (_, _, _, _, context_sfb, split_sfb, imp_sfb, _) = dest_VAR_RES_FRAME_SPLIT tt; 2765 2766 fun get_resort_thm [] = raise UNCHANGED 2767 | get_resort_thm ((sfb, c, thm)::L) = 2768 let 2769 val nl = get_resort_list___pred is_asl_star sfb; 2770 in 2771 if null nl then get_resort_thm L else 2772 (c (BAG_RESORT_CONV nl) tt, thm) 2773 end; 2774 2775 val (resort_thm, thm) = get_resort_thm 2776 [(context_sfb, VAR_RES_FRAME_SPLIT___context_CONV, VAR_RES_FRAME_SPLIT___asl_star___context), 2777 (imp_sfb, VAR_RES_FRAME_SPLIT___imp_CONV, VAR_RES_FRAME_SPLIT___asl_star___imp), 2778 (split_sfb, VAR_RES_FRAME_SPLIT___split_CONV, VAR_RES_FRAME_SPLIT___asl_star___split)] 2779 2780 2781 2782 val thm1 = PART_MATCH (lhs o snd o dest_imp) thm (rhs (concl resort_thm)); 2783 val thm2 = var_res_precondition_prove thm1 2784 val thm3 = TRANS resort_thm thm2 2785in 2786 thm3 2787end; 2788 2789 2790 2791(* 2792 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2793*) 2794fun VAR_RES_FRAME_SPLIT_INFERENCE___asl_trivial_cond___CONV tt = 2795let 2796 val (_, _, _, _, context_sfb, split_sfb, imp_sfb, _) = dest_VAR_RES_FRAME_SPLIT tt; 2797 2798 fun get_resort_thm [] = raise UNCHANGED 2799 | get_resort_thm ((sfb, c, thm, has_precond)::L) = 2800 let 2801 val nl = get_resort_list___pred is_asl_trivial_cond sfb; 2802 in 2803 if null nl then get_resort_thm L else 2804 (c (BAG_RESORT_CONV nl) tt, thm, has_precond) 2805 end; 2806 2807 val (resort_thm, thm, has_precond) = get_resort_thm 2808 [(context_sfb, VAR_RES_FRAME_SPLIT___context_CONV, VAR_RES_FRAME_SPLIT___trivial_cond___context, false), 2809 (imp_sfb, VAR_RES_FRAME_SPLIT___imp_CONV, VAR_RES_FRAME_SPLIT___trivial_cond___imp, true), 2810 (split_sfb, VAR_RES_FRAME_SPLIT___split_CONV, VAR_RES_FRAME_SPLIT___trivial_cond___split, false)] 2811 2812 val dest_fun = if (has_precond) then (snd o dest_imp) else I 2813 val thm1 = PART_MATCH (lhs o dest_fun) thm (rhs (concl resort_thm)); 2814 val thm2 = if has_precond then var_res_precondition_prove thm1 else thm1 2815 val thm3 = TRANS resort_thm thm2 2816in 2817 thm3 2818end; 2819 2820 2821(* 2822 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2823*) 2824fun VAR_RES_FRAME_SPLIT_INFERENCE___asl_false___CONV tt = 2825let 2826 val (_, _, _, _, context_sfb, split_sfb, _, _) = dest_VAR_RES_FRAME_SPLIT tt; 2827 2828 fun get_resort_thm [] = raise UNCHANGED 2829 | get_resort_thm ((sfb, c, thm)::L) = 2830 let 2831 val nl = get_resort_list___pred is_asl_false sfb; 2832 in 2833 if null nl then get_resort_thm L else 2834 (c (BAG_RESORT_CONV nl) tt, thm) 2835 end; 2836 2837 val (resort_thm, thm) = get_resort_thm 2838 [(context_sfb, VAR_RES_FRAME_SPLIT___context_CONV, VAR_RES_FRAME_SPLIT___asl_false___context), 2839 (split_sfb, VAR_RES_FRAME_SPLIT___split_CONV, VAR_RES_FRAME_SPLIT___asl_false___split)] 2840 2841 val thm1 = PART_MATCH I thm (rhs (concl resort_thm)); 2842 val thm2 = TRANS resort_thm (EQT_INTRO thm1) 2843in 2844 thm2 2845end; 2846 2847 2848fun VAR_RES_FRAME_SPLIT_INFERENCE___asl_exists___CONSEQ_CONV tt = 2849let 2850 val (_, _, _, _, context_sfb, split_sfb, imp_sfb, _) = dest_VAR_RES_FRAME_SPLIT tt; 2851 2852 fun get_resort_thm [] = raise UNCHANGED 2853 | get_resort_thm ((sfb, c, thm)::L) = 2854 let 2855 val nl = get_resort_list___pred is_asl_exists sfb; 2856 in 2857 if null nl then get_resort_thm L else 2858 (c (BAG_RESORT_CONV nl) tt, thm) 2859 end; 2860 2861 val (resort_thm, thm) = get_resort_thm 2862 [(context_sfb, VAR_RES_FRAME_SPLIT___context_CONV, VAR_RES_FRAME_SPLIT___asl_exists___context), 2863 (imp_sfb, VAR_RES_FRAME_SPLIT___imp_CONV, VAR_RES_FRAME_SPLIT___asl_exists___imp), 2864 (split_sfb, VAR_RES_FRAME_SPLIT___split_CONV, VAR_RES_FRAME_SPLIT___asl_exists___split)] 2865 2866 val thm1 = HO_PART_MATCH (snd o dest_imp o snd o dest_imp) thm (rhs (concl resort_thm)); 2867 val thm2 = var_res_precondition_prove thm1 2868 val thm3 = CONV_RULE (RAND_CONV (K (GSYM resort_thm))) thm2 2869in 2870 thm3 2871end; 2872 2873(******************************************************************************) 2874(* Case splits *) 2875(******************************************************************************) 2876 2877 2878val case_split_thm = prove (Term `!c B. 2879(B = ((c ==> B) /\ (~c ==> B)))`, Cases_on `c` THEN REWRITE_TAC[]) 2880 2881fun case_split_heuristic___is_cond ttt = 2882let 2883 val cond_term = find_term (fn t => is_cond t) ttt 2884 val (c, _, _) = dest_cond cond_term; 2885 val (c',_) = strip_neg c; 2886 val _ = REWRITE_CONV [ASSUME c'] ttt 2887in 2888 c' 2889end; 2890 2891fun VAR_RES_COND_INFERENCE___case_split___CONV tt = 2892let 2893 val (_,pre,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE tt 2894 val heuristicL = (fn _ => case_split_heuristic___is_cond pre):: 2895 var_res_param.hoare_triple_case_splitL 2896 val c = tryfind (fn h => h tt) heuristicL; 2897in 2898 ISPECL [c, tt] case_split_thm 2899end; 2900 2901(* 2902 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2903*) 2904fun VAR_RES_FRAME_SPLIT_INFERENCE___case_split___CONV tt = 2905let 2906 val _ = if is_VAR_RES_FRAME_SPLIT tt then () else raise UNCHANGED; 2907 val heuristicL = (case_split_heuristic___is_cond):: 2908 var_res_param.frame_split_case_splitL 2909 val c = tryfind (fn h => h (rator tt)) heuristicL; 2910in 2911 ISPECL [c, tt] case_split_thm 2912end; 2913 2914 2915(******************************************************************************) 2916(* Strong stack proposition *) 2917(******************************************************************************) 2918local 2919 val ssp_conv = REWRITE_CONV [VAR_RES_IS_PURE_PROPOSITION___BASIC_PROPS] 2920in 2921 2922fun VAR_RES_IS_PURE_PROPOSITION___prove___BASIC f p = 2923let 2924 val ttt = mk_VAR_RES_IS_PURE_PROPOSITION f p 2925in 2926 EQT_ELIM (ssp_conv ttt) 2927end; 2928 2929end 2930 2931 2932fun VAR_RES_IS_PURE_PROPOSITION___prove f p = 2933 tryfind (fn pr => pr f p) 2934 ([VAR_RES_IS_PURE_PROPOSITION___prove___BASIC]@ 2935 (var_res_param.VAR_RES_IS_PURE_PROPOSITION___provers)) 2936 2937(* 2938 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2939*) 2940fun VAR_RES_FRAME_SPLIT_INFERENCE___strong_stack_proposition_to_context___CONV tt = 2941let 2942 val (f, _, _, _, context_sfb, split_sfb, _, _) = dest_VAR_RES_FRAME_SPLIT tt; 2943 val (split_sfs,_) = dest_bag split_sfb 2944 2945 val found_opt = first_opt (fn n => fn ttt => 2946 SOME (n, VAR_RES_IS_PURE_PROPOSITION___prove f ttt)) split_sfs 2947 val _ = if isSome found_opt then () else raise UNCHANGED 2948 val (pos,ssp_thm) = valOf found_opt 2949 2950 (*resort*) 2951 val thm0 = VAR_RES_FRAME_SPLIT___split_CONV (BAG_RESORT_CONV [pos]) tt 2952 2953 (*apply inference*) 2954 val thm1 = PART_MATCH (lhs o snd o dest_imp) 2955 VAR_RES_FRAME_SPLIT___PURE_PROPOSITION___TO_CONTEXT 2956 ((rhs o concl) thm0) 2957 val thm2 = MP thm1 ssp_thm 2958 val thm3 = TRANS thm0 thm2 2959in 2960 thm3 2961end; 2962 2963 2964 2965(******************************************************************************) 2966(* solving entailments *) 2967(******************************************************************************) 2968 2969(* 2970 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 2971*) 2972 2973local 2974 2975val BAG_EVERY_INSERT_IMP = prove (Term 2976 `!P b e. BAG_EVERY P b ==> (P (e:'a) ==> BAG_EVERY P (BAG_INSERT e b))`, 2977 SIMP_TAC std_ss [BAG_EVERY_THM]); 2978 2979 2980fun VAR_RES_FRAME_SPLIT___strong_stack_proposition_to_split (entail_thm, imprecise_thm) = 2981let 2982 val tt = rhs (concl entail_thm) 2983 val (f, _, _, _, context_sfb, _, _, _) = dest_VAR_RES_FRAME_SPLIT tt; 2984 val (context_sfs,_) = dest_bag context_sfb 2985 val imprecise_t = (rand o rator o concl) imprecise_thm 2986 2987 val found_opt = first_opt (fn n => fn ttt => 2988 let 2989 val ssp_thm = VAR_RES_IS_PURE_PROPOSITION___prove f ttt; 2990 val imp_thm = var_res_prove___no_expn (mk_comb (imprecise_t, ttt)) 2991 in 2992 SOME (n, ssp_thm, imp_thm, ttt) 2993 end) context_sfs 2994 val _ = if isSome found_opt then () else Feedback.fail(); 2995 val (pos,ssp_thm,imp_thm,sf) = valOf found_opt 2996 2997 (*resort*) 2998 val thm0 = VAR_RES_FRAME_SPLIT___context_CONV (BAG_RESORT_CONV [pos]) tt 2999 3000 (*apply inference*) 3001 val thm1 = PART_MATCH (lhs o snd o dest_imp) 3002 (GSYM VAR_RES_FRAME_SPLIT___PURE_PROPOSITION___TO_CONTEXT) 3003 ((rhs o concl) thm0) 3004 val thm2 = MP thm1 ssp_thm 3005 val thm3 = TRANS thm0 thm2 3006 3007 (*construct new thms*) 3008 val entail_thm' = TRANS entail_thm thm3 3009 3010 val BAG_EVERY_INSERT_IMP' = ISPECL [imprecise_t, 3011 rand (concl imprecise_thm), sf] BAG_EVERY_INSERT_IMP 3012 val imprecise_thm' = MP (MP BAG_EVERY_INSERT_IMP' imprecise_thm) imp_thm 3013in 3014 VAR_RES_FRAME_SPLIT___strong_stack_proposition_to_split (entail_thm', imprecise_thm') 3015end handle HOL_ERR _ => (entail_thm, imprecise_thm) 3016 3017 3018val IMP_CLAUSES_XT = prove (Term `!t. (t ==> T) = T`, REWRITE_TAC[]); 3019fun imp_true_simp t = 3020let 3021 val (t1, t2) = dest_imp_only t 3022in 3023 if (same_const t2 T) then 3024 SPEC t1 IMP_CLAUSES_XT 3025 else Feedback.fail() 3026end 3027 3028in 3029 3030 3031 3032 3033(* 3034 val do_bool = true; 3035 val preserve_fallback = true 3036 REPEAT STRIP_TAC 3037 val context = map ASSUME (fst (top_goal ())) 3038 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 3039 3040*) 3041 3042fun VAR_RES_FRAME_SPLIT_INFERENCE___SOLVE___CONSEQ_CONV do_bool preserve_fallback context tt = 3043let 3044 val (f,sr, wpbrpb, wpb', _, _, imp_sfb, _) = dest_VAR_RES_FRAME_SPLIT tt; 3045 val split_term = fst (strip_comb tt); 3046 fun split tt = 3047 (split o snd o dest_forall) tt handle HOL_ERR _ => 3048 (split o snd o dest_imp_only) tt handle HOL_ERR _ => 3049 tt; 3050 3051 fun split_thm_inst thm = 3052 let 3053 val ttt = (fst o strip_comb o split o concl) thm 3054 val thm2 = INST_TYPE (snd (match_term ttt split_term)) thm 3055 in 3056 thm2 3057 end; 3058 3059 3060 (*check whether it can be solved*) 3061 val (solve_thm0,has_bool) = if bagSyntax.is_empty imp_sfb then 3062 (split_thm_inst (if preserve_fallback then VAR_RES_FRAME_SPLIT___SOLVE else 3063 VAR_RES_FRAME_SPLIT___SOLVE_WEAK), false) 3064 else 3065 let 3066 val _ = if not (do_bool) then Feedback.fail() else (); 3067 val (bp, rb) = bagSyntax.dest_insert imp_sfb handle HOL_ERR _ => raise UNCHANGED; 3068 val _ = if bagSyntax.is_empty rb then () else raise UNCHANGED 3069 val (_, b) = dest_var_res_bool_proposition bp handle HOL_ERR _ => raise UNCHANGED 3070 val b_thm_opt = SOME (var_res_param.final_decision_procedure context b) handle HOL_ERR _ => NONE; 3071 in 3072 if (isSome b_thm_opt) then let 3073 val inf_thm = SPEC b (split_thm_inst (if preserve_fallback then VAR_RES_FRAME_SPLIT___SOLVE___bool_prop___MP else VAR_RES_FRAME_SPLIT___SOLVE_WEAK___bool_prop___MP)) 3074 val xthm0 = MP inf_thm (valOf b_thm_opt) 3075 in 3076 (xthm0, false) 3077 end else 3078 (SPEC b (split_thm_inst (if preserve_fallback then VAR_RES_FRAME_SPLIT___SOLVE___bool_prop else VAR_RES_FRAME_SPLIT___SOLVE_WEAK___bool_prop)), true) 3079 end; 3080 3081 val (wpb,rpb) = dest_pair wpbrpb; 3082 val solve_thm1 = ISPECL [sr, f,wpb,rpb,wpb'] solve_thm0 3083 val solve_thm = CONV_RULE 3084 ((STRIP_QUANT_CONV o RATOR_CONV o RAND_CONV o 3085 RATOR_CONV o RAND_CONV o RAND_CONV o RAND_CONV) 3086 SIMPLE_BAG_NORMALISE_CONV) solve_thm1 3087 val imprecise_t = (rand o rator o fst o dest_imp o snd o strip_forall o concl) solve_thm 3088 3089 (*move strong_stack_propositions to context*) 3090 val thm0 = (REPEATC VAR_RES_FRAME_SPLIT_INFERENCE___strong_stack_proposition_to_context___CONV) tt 3091 handle UNCHANGED => REFL tt 3092 3093 (*check whether variable conditions are met*) 3094 val (_, sr, _, _, _, split_sfb, _, _) = dest_VAR_RES_FRAME_SPLIT (rhs (concl thm0)); 3095 val sr_b = aconv (fst (pairSyntax.dest_pair sr)) T handle HOL_ERR _ => false 3096 val _ = if sr_b orelse bagSyntax.is_empty split_sfb then () else raise UNCHANGED 3097 3098 val split_thm = var_res_prove___no_expn (mk_every (imprecise_t, split_sfb)) 3099 handle HOL_ERR _ => raise UNCHANGED 3100 3101 (*move strong_stack_propositions to *) 3102 val (thm1, precond_thm) = (if sr_b then 3103 VAR_RES_FRAME_SPLIT___strong_stack_proposition_to_split else I) 3104 (thm0, split_thm) 3105 3106 3107 (*combine it*) 3108 val thm2a = PART_MATCH (snd o dest_imp o snd o dest_imp) solve_thm (rhs (concl thm1)) 3109 val thm2b = MP thm2a precond_thm 3110 val thm2c = CONV_RULE ((RAND_CONV) (K (GSYM thm1))) thm2b 3111 3112 val c_opt = SOME (optionSyntax.dest_some (snd (pairSyntax.dest_pair sr))) handle HOL_ERR _ => NONE 3113 val comment_intro_CONV = if not has_bool orelse not (isSome c_opt) then ALL_CONV else 3114 (RATOR_CONV o RAND_CONV) (asl_comment_location_INTRO_CONV (asl_comment_modify_APPEND "condition" (valOf c_opt))) 3115 3116 val restP_conv = if not sr_b then (REWRITE_CONV [BAG_EVERY_THM]) else 3117 (DEPTH_CONV BETA_CONV THENC 3118 DEPTH_CONV SIMPLE_BAG_NORMALISE_CONV) 3119 val thm2d = CONV_RULE ((RATOR_CONV o RAND_CONV o 3120 (if preserve_fallback then RAND_CONV else I)) 3121 (comment_intro_CONV THENC restP_conv)) thm2c 3122 val thm2e = if preserve_fallback then CONV_RULE ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o RAND_CONV) 3123 (SIMPLE_BAG_NORMALISE_CONV)) thm2d else thm2d 3124 3125 val thm2 = CONV_RULE ((RATOR_CONV o RAND_CONV) imp_true_simp) thm2e handle HOL_ERR _ => thm2e; 3126in 3127 thm2 3128end; 3129 3130end; 3131 3132 3133(******************************************************************************) 3134(* Enrichment of instructions with implied properties *) 3135(******************************************************************************) 3136 3137(* 3138 val tt = find_term is_VAR_RES_COND_HOARE_TRIPLE (snd (top_goal ())) 3139*) 3140 3141fun var_res_prop_implies_COMBINE [] = Feedback.fail() 3142 | var_res_prop_implies_COMBINE [thm] = 3143 (CONV_RULE (RAND_CONV (bagLib.SIMPLE_BAG_NORMALISE_CONV)) thm handle HOL_ERR _ => thm) 3144 | var_res_prop_implies_COMBINE (thm1::thm2::thmL) = 3145 var_res_prop_implies_COMBINE ( 3146 (MATCH_MP var_res_prop_implies___UNION (CONJ thm1 thm2))::thmL) 3147 3148fun VAR_RES_COND_INFERENCE___enrich_precond___CONV el ss context tt = 3149let 3150 val (_,pre,prog,post) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 3151 val (f, wpb,rpb, sfb) = dest_var_res_prop pre 3152 3153 val implies_list = flatten ( 3154 map (fn ff => ff [] el ss context (f, wpb, rpb, sfb)) 3155 var_res_param.var_res_prop_implies___GENERATE) 3156 3157 val implies_thm = var_res_prop_implies_COMBINE implies_list; 3158 val sfb' = rand (concl implies_thm) 3159 val thm0 = ISPECL [f, wpb,rpb, sfb, sfb', prog, post] 3160 VAR_RES_COND_INFERENCE___prop_implies 3161 val thm1 = MP thm0 implies_thm 3162 val thm2 = CONV_RULE (RHS_CONV (VAR_RES_COND_HOARE_TRIPLE___PRECOND_CONV 3163 (RAND_CONV bagLib.SIMPLE_BAG_NORMALISE_CONV))) thm1 3164in 3165 thm2 3166end; 3167 3168 3169(* 3170 val tt = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 3171*) 3172fun VAR_RES_FRAME_SPLIT_INFERENCE___enrich_split___CONV el ss context tt = 3173let 3174 val (f, _, wr, _, context_sfb, split_sfb, imp_sfb, _) = 3175 dest_VAR_RES_FRAME_SPLIT tt 3176 val (wpb,rpb) = dest_pair wr 3177 val sfb = bagSyntax.mk_union (context_sfb, split_sfb) 3178 3179 val implies_list = flatten ( 3180 map (fn ff => ff [imp_sfb] el ss context (f, wpb, rpb, sfb)) 3181 var_res_param.var_res_prop_implies___GENERATE) 3182 3183 val implies_thm = var_res_prop_implies_COMBINE implies_list; 3184 val sfb = rand (concl implies_thm) 3185 val thm0 = PART_MATCH (lhs o snd o dest_imp) 3186 (ISPEC sfb VAR_RES_FRAME_SPLIT___var_res_prop_implies___split) tt 3187 3188 val thm1 = MP thm0 implies_thm 3189 3190 val thm2 = CONV_RULE (RHS_CONV (RATOR_CONV (RATOR_CONV ( 3191 (RAND_CONV bagLib.SIMPLE_BAG_NORMALISE_CONV))))) thm1 3192in 3193 thm2 3194end; 3195 3196 3197(******************************************************************************) 3198(* STRUCTURE_NORMALISE *) 3199(******************************************************************************) 3200 3201fun NO_MARKER___AND_IMP_INTRO t = 3202if ConseqConv.is_asm_marker ((fst o dest_imp) t) then Feedback.fail () else 3203(PART_MATCH lhs AND_IMP_INTRO) t 3204 3205fun NO_MARKER___RIGHT_IMP_FORALL_CONV t = 3206if ConseqConv.is_asm_marker ((rand o snd o strip_forall) t) then Feedback.fail () else 3207RIGHT_IMP_FORALL_CONV t 3208 3209val VAR_RES_STRUCTURE_NORMALISE_CONV = 3210 LIST_FORALL_SIMP_CONV ORELSEC 3211 LIST_FORALL_AND_CONV ORELSEC 3212 NO_MARKER___AND_IMP_INTRO ORELSEC 3213 NO_MARKER___RIGHT_IMP_FORALL_CONV ORELSEC 3214 (PART_MATCH lhs IMP_CONJ_THM) ORELSEC 3215 LIST_EXISTS_SIMP_CONV; 3216 3217 3218(******************************************************************************) 3219(* Quantifier instantiations *) 3220(******************************************************************************) 3221 3222fun QUANT_INSTANTIATE_HEURISTIC___VAR_RES_FRAME_SPLIT___bool (sys:quant_heuristic_base) v tt = 3223let 3224 val (_,_,_,_,_,_,sfb_imp,_) = dest_VAR_RES_FRAME_SPLIT tt 3225 handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 3226 3227 val (sfs,_) = bagSyntax.dest_bag sfb_imp; 3228 val sfs' = filter is_var_res_bool_proposition sfs; 3229 val sfs'' = map rand sfs'; 3230 3231 val gC = COMBINE_HEURISTIC_FUNS (map (fn t => (fn () => (sys v t))) sfs''); 3232 val relevant_guesses = #exists_gap gC; 3233 3234 fun mk_exists g = 3235 let 3236 val (i,fvL) = guess_extract g 3237 in 3238 mk_guess gty_exists v tt i fvL 3239 end; 3240 val guesses = map mk_exists relevant_guesses 3241in 3242 {rewrites = #rewrites gC, 3243 general = [], 3244 exists_point = [], 3245 forall_point = [], 3246 forall = [], 3247 exists = guesses, 3248 exists_gap = [], 3249 forall_gap = []}:guess_collection 3250end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 3251 3252val cache_ref = ref (mk_quant_heuristic_cache ()); 3253val var_res_main_qp = combine_qps [ 3254 rewrite_qp [asl_comments_ELIM], 3255 heuristics_qp [QUANT_INSTANTIATE_HEURISTIC___VAR_RES_FRAME_SPLIT___bool]] 3256val VAR_RES_QUANT_INSTANTIATE_CONSEQ_CONV___main = 3257 EXTENSIBLE_QUANT_INSTANTIATE_STEP_CONSEQ_CONV NONE false basic_qp 3258 (var_res_main_qp::list_no_len_qp::(var_res_param.quantifier_heuristicsL)); 3259 3260(* 3261val lref = ref [] 3262 3263val tt = el 1 (!lref) 3264 3265 3266val xthm0 = VAR_RES_QUANT_INSTANTIATE_CONSEQ_CONV___main CONSEQ_CONV_STRENGTHEN_direction tt 3267 3268set_trace "QUANT_INSTANTIATE_HEURISTIC" 3 3269traces () 3270 val _ = lref := tt::(!lref); 3271*) 3272fun VAR_RES_QUANT_INSTANTIATE_CONSEQ_CONV ss context tt = 3273let 3274 val thm0 = VAR_RES_QUANT_INSTANTIATE_CONSEQ_CONV___main CONSEQ_CONV_STRENGTHEN_direction tt 3275(* val c = (if (is_imp (concl thm0)) then (RATOR_CONV o RAND_CONV) else 3276 RAND_CONV) 3277 val thm1 = CONV_RULE (c (VAR_RES_PROP_REWRITE_CONV ss context)) thm0*) 3278in 3279 thm0 3280end; 3281 3282(* 3283fun FORALL_NORMALISE_CONV tt = 3284let 3285 val (v, body) = dest_forall tt; 3286in 3287 if (is_conj body) then 3288 HO_PART_MATCH lhs FORALL_AND_THM tt 3289 else if (is_imp_only body) then 3290 let 3291 val (b1,b2) = dest_imp_only body 3292 in 3293 if not (free_in v b1) then 3294 HO_PART_MATCH lhs RIGHT_FORALL_IMP_THM tt 3295 else if not (free_in v b2) then 3296 HO_PART_MATCH lhs LEFT_FORALL_OR_THM tt 3297 else Feedback.fail() 3298 end 3299 else if (is_disj body) then 3300 let 3301 val (b1,b2) = dest_disj body 3302 in 3303 if not (free_in v b2) then 3304 HO_PART_MATCH lhs LEFT_FORALL_OR_THM tt 3305 else if not (free_in v b1) then 3306 HO_PART_MATCH lhs RIGHT_FORALL_OR_THM tt 3307 else Feedback.fail() 3308 end 3309 else Feedback.fail() 3310end 3311 3312 SIMP_CONV std_ss [] tt 3313end; 3314*) 3315 3316 3317(* 3318fun VAR_RES_COND_INFERENCE___comment_quant_best_local_action___CONV var_res_param = 3319 asl_comment_location_CONSEQ_CONV 3320 (VAR_RES_COND_INFERENCE___quant_best_local_action___CONV var_res_param) 3321 3322 3323*) 3324 3325 3326 3327(* 3328 3329ONCE_DEPTH_CONSEQ_CONV_TAC (K (VAR_RES_COND_INFERENCE___assume var_res_param)) 3330 3331 3332 3333al exp = (intro_hoare_triples current_theorem; UNCHANGED) handle x => x 3334val resource_and_proc_call_free_PROVE___failed_expn(_, _, SOME tt) = exp 3335 3336open Profile 3337 3338 3339fun profile_program_abst s a abstL sys xenv penv = 3340 Profile.profile s (fn p => (a abstL sys xenv penv p) 3341 handle HOL_ERR _ => NONE 3342 handle UNCHANGED => NONE) 3343 3344 3345 3346reset_all (); 3347val _ = time (ASL_SPECIFICATION___CONSEQ_CONV (proc_call_free_CONV, abstrL)) t; 3348print_profile_results (results()); 3349 3350abstrL 3351 3352 3353 3354remove_holfoot_pp () 3355add_holfoot_pp () 3356thm 3357 3358 3359``!x. n + x + 3 = 8`` 3360 3361 3362 3363 3364*) 3365 3366 3367(* ========================================================================== *) 3368(* The inferences list consists of consequence conversions that are used to *) 3369(* make some kind of progress towards verifying an specification. They are *) 3370(* annotated with a string describing them and a level at which to excute. *) 3371(* This level is important for interactive steps later. If an inference of a *) 3372(* given or lower level has been sucessfully applied, this STEP_TAC stops. *) 3373(* ========================================================================== *) 3374 3375type var_res_inference_group = 3376 (* group name (used for debug) *) 3377 string * 3378 (* group guard, inferences are just applied to 3379 terms that satisfy this guard *) 3380 (term -> bool) * 3381 (* apply before working on subterms *) 3382 bool * 3383 (* use this inference group to clean up after a "bigger" step *) 3384 bool * 3385 (* the members of the group, each with a name for debugging *) 3386 (string * var_res_inference) list; 3387 3388 3389val VAR_RES_INFERENCES_LIST___simulate_command = ("simulate command", 3390 is_VAR_RES_COND_HOARE_TRIPLE, false, true, [ 3391 ("cond", 3392 no_context_strengthen_conseq_conv 3393 VAR_RES_COND_INFERENCE___cond___CONSEQ_CONV), 3394 ("assignment", 3395 no_context_strengthen_conseq_conv 3396 VAR_RES_COND_INFERENCE___assign___CONSEQ_CONV), 3397 ("local_vars_arg", 3398 no_context_strengthen_conseq_conv 3399 VAR_RES_COND_INFERENCE___local_vars_args___CONSEQ_CONV), 3400 ("while_invariant", 3401 no_context_strengthen_conseq_conv 3402 VAR_RES_COND_INFERENCE___while___invariant___CONSEQ_CONV), 3403 ("while_loop_spec", 3404 no_context_strengthen_conseq_conv 3405 VAR_RES_COND_INFERENCE___while___loop_spec___CONSEQ_CONV), 3406 ("while_unroll", 3407 no_context_strengthen_conseq_conv 3408 VAR_RES_COND_INFERENCE___while___loop_unroll___CONSEQ_CONV), 3409 ("abstractions", 3410 no_context_strengthen_conseq_conv 3411 VAR_RES_COND_INFERENCE___abstracted_code___CONV), 3412 ("hoare_triple_solve", 3413 no_context_strengthen_conseq_conv 3414 VAR_RES_COND_INFERENCE___final___CONSEQ_CONV), 3415 ("block_spec", 3416 no_context_strengthen_conseq_conv 3417 VAR_RES_COND_INFERENCE___block_spec___CONSEQ_CONV), 3418 ("diverge", 3419 no_context_strengthen_conseq_conv 3420 VAR_RES_COND_INFERENCE___diverge___CONV), 3421 ("assert", 3422 no_context_strengthen_conseq_conv 3423 VAR_RES_COND_INFERENCE___assert___CONSEQ_CONV)]@ 3424 var_res_param.INFERENCES_LIST___simulate_command):var_res_inference_group; 3425 3426 3427 3428val VAR_RES_INFERENCES_LIST___simulate_minor_command = ("simulate minor command", 3429 is_VAR_RES_COND_HOARE_TRIPLE, false, true, [ 3430 ("assume", 3431 no_context_strengthen_conseq_conv 3432 VAR_RES_COND_INFERENCE___assume___CONSEQ_CONV), 3433 ("eval_expressions", 3434 no_context_strengthen_conseq_conv 3435 VAR_RES_COND_INFERENCE___eval_expressions___CONV), 3436 ("quant_best_local_action", 3437 no_context_strengthen_conseq_conv 3438 VAR_RES_COND_INFERENCE___quant_best_local_action___CONSEQ_CONV), 3439 ("best_local_action", 3440 no_context_strengthen_conseq_conv 3441 VAR_RES_COND_INFERENCE___best_local_action___CONV), 3442 ("cond_best_local_action", 3443 no_context_strengthen_conseq_conv 3444 VAR_RES_COND_INFERENCE___cond_best_local_action___CONV), 3445 ("aquire_lock", 3446 no_context_strengthen_conseq_conv 3447 VAR_RES_COND_INFERENCE___aquire_lock___CONV), 3448 ("release_lock", 3449 no_context_strengthen_conseq_conv 3450 VAR_RES_COND_INFERENCE___release_lock___CONV), 3451 ("cond_best_local_action___cond_star", 3452 no_context_strengthen_conseq_conv 3453 VAR_RES_COND_INFERENCE___cond_best_local_action___asl_cond_star___CONSEQ_CONV)]@ 3454 var_res_param.INFERENCES_LIST___simulate_minor_command): 3455 var_res_inference_group; 3456 3457 3458val VAR_RES_INFERENCES_LIST___mayor_step = ("mayor step", 3459 K true, false, true, [ 3460 ("specification", 3461 no_context_strengthen_conseq_conv 3462 VAR_RES_SPECIFICATION___CONSEQ_CONV)]):var_res_inference_group; 3463 3464val VAR_RES_INFERENCES_LIST___entailment_steps = ("entailment", 3465 is_VAR_RES_FRAME_SPLIT, false, true, [ 3466 ("entailment_equality", 3467 no_context_strengthen_conseq_conv 3468 VAR_RES_FRAME_SPLIT_INFERENCE___VAR_EQ_CONST_TO_CONTEXT___CONV), 3469 ("frame", 3470 no_context_strengthen_conseq_conv 3471 VAR_RES_FRAME_SPLIT_INFERENCE___FRAME___CONV), 3472 ("simp___bool_pred", 3473 simpset_strengthen_conseq_conv 3474 VAR_RES_FRAME_SPLIT_INFERENCE___bool_pred___CONV)]@ 3475 var_res_param.INFERENCES_LIST___entailment_steps):var_res_inference_group; 3476 3477val VAR_RES_INFERENCES_LIST___entailment_solve = ("entailment", 3478 (K true), false, true, 3479 [("entailment_solve", 3480 fn p => (fn context => (K 3481 (VAR_RES_FRAME_SPLIT_INFERENCE___SOLVE___CONSEQ_CONV 3482 false (not (#fast p)) context))))]):var_res_inference_group; 3483 3484 3485val VAR_RES_INFERENCES_LIST___cheap_simplifications = ("cheap simps", 3486 (K true), false, true, [ 3487 ("precond_simp___false", 3488 no_context_strengthen_conseq_conv 3489 VAR_RES_COND_INFERENCE___PRECOND_false___CONV), 3490 ("entail_simp___false", 3491 no_context_strengthen_conseq_conv 3492 VAR_RES_FRAME_SPLIT_INFERENCE___asl_false___CONV), 3493 ("precond_simp___stack_true", 3494 no_context_strengthen_conseq_conv 3495 VAR_RES_COND_INFERENCE___PRECOND_stack_true___CONV), 3496 ("precond_simp___bool_pred", 3497 simpset_strengthen_conseq_conv 3498 VAR_RES_COND_INFERENCE___PRECOND_bool_pred___CONV), 3499 ("precond_simp___trivial_cond", 3500 no_context_strengthen_conseq_conv 3501 VAR_RES_COND_INFERENCE___PRECOND_trivial_cond___CONV), 3502 ("entailment_simp___stack_true", 3503 no_context_strengthen_conseq_conv 3504 VAR_RES_FRAME_SPLIT_INFERENCE___stack_true___CONV), 3505 ("precond_simp___asl_exists", 3506 no_context_strengthen_conseq_conv 3507 VAR_RES_COND_INFERENCE___PRECOND_asl_exists___CONV), 3508 ("precond_simp___strong_exists", 3509 no_context_strengthen_conseq_conv 3510 VAR_RES_COND_INFERENCE___EXISTS_PRE___CONSEQ_CONV), 3511 ("precond_simp___asl_star", 3512 no_context_strengthen_conseq_conv 3513 VAR_RES_COND_INFERENCE___PRECOND_asl_star___CONV), 3514 ("entail_simp___asl_star", 3515 no_context_strengthen_conseq_conv 3516 VAR_RES_FRAME_SPLIT_INFERENCE___asl_star___CONV), 3517 ("entail_simp___asl_trivial_cond", 3518 no_context_strengthen_conseq_conv 3519 VAR_RES_FRAME_SPLIT_INFERENCE___asl_trivial_cond___CONV), 3520 ("entail_simp___asl_exists", 3521 no_context_strengthen_conseq_conv 3522 VAR_RES_FRAME_SPLIT_INFERENCE___asl_exists___CONSEQ_CONV), 3523 ("comment_block", 3524 no_context_strengthen_conseq_conv 3525 VAR_RES_COND_INFERENCE___block_comment___CONV)]):var_res_inference_group 3526 3527(* 3528("quantifier instantiation", 3529 K VAR_RES_QUANT_INSTANTIATE_CONSEQ_CONV)*) 3530 3531val VAR_RES_INFERENCES_LIST___expensive_simplifications___general = ("expensive simps", 3532 (K true), false, true, [ 3533 ("eliminate_comment", 3534 no_context_strengthen_conseq_conv 3535 asl_comment_location___TF_ELIM___CONV), 3536 ("quantifier instantiation", 3537 simpset_strengthen_conseq_conv VAR_RES_QUANT_INSTANTIATE_CONSEQ_CONV)]@ 3538 var_res_param.INFERENCES_LIST___expensive_simplifications):var_res_inference_group 3539 3540val VAR_RES_INFERENCES_LIST___expensive_simplifications___hoare_triple = ("expensive simps", 3541 is_VAR_RES_COND_HOARE_TRIPLE, false, true, [ 3542 ("precond_simp___rewrites", 3543 simpset_strengthen_conseq_conv 3544 VAR_RES_COND_INFERENCE___PRECOND_REWRITE___CONV), 3545 ("precond_simp___propagate_eq", 3546 no_context_strengthen_conseq_conv 3547 (VAR_RES_COND_INFERENCE___CONST_INTRO_PROPAGATE_EQ___CONSEQ_CONV false)), 3548 ("flatten_block", 3549 no_context_strengthen_conseq_conv 3550 VAR_RES_COND_INFERENCE___block_flatten___CONSEQ_CONV)]):var_res_inference_group; 3551 3552 3553val VAR_RES_INFERENCES_LIST___expands = ("expands", 3554 (K true), false, false, [ 3555 ("precond_enrich", 3556 expands_strengthen_conseq_conv 3557 (VAR_RES_COND_INFERENCE___enrich_precond___CONV)), 3558 ("precond_simp___intro_constants", 3559 no_context_strengthen_conseq_conv 3560 VAR_RES_COND_INFERENCE___ALL_CONST_INTRO___CONV)]):var_res_inference_group; 3561 3562 3563val VAR_RES_INFERENCES_LIST___expands_entailment = ("expands_entailment", 3564 (K true), false, true, [ 3565 ("entailment_enrich", 3566 expands_strengthen_conseq_conv 3567 VAR_RES_FRAME_SPLIT_INFERENCE___enrich_split___CONV), 3568 ("entailment___intro_constants", 3569 no_context_strengthen_conseq_conv 3570 VAR_RES_FRAME_SPLIT_INFERENCE___ALL_CONST_INTRO___CONV)]):var_res_inference_group; 3571 3572val VAR_RES_INFERENCES_LIST___case_splits = ("case_splits", 3573 (K true), false, false, [ 3574 ("entailment_case_split", 3575 no_context_strengthen_conseq_conv 3576 VAR_RES_FRAME_SPLIT_INFERENCE___case_split___CONV), 3577 ("hoare_triple case split", 3578 no_context_strengthen_conseq_conv 3579 VAR_RES_COND_INFERENCE___case_split___CONV)]):var_res_inference_group; 3580 3581 3582val VAR_RES_INFERENCES_LIST___expensive_simplifications___frame_split = ("expensive simps", 3583 is_VAR_RES_FRAME_SPLIT, false, true, [ 3584 ("entailment_prop_rewrites", 3585 simpset_strengthen_conseq_conv 3586 VAR_RES_FRAME_SPLIT_INFERENCE___PROP_REWRITE___CONV)]):var_res_inference_group 3587 3588 3589fun VAR_RES_INFERENCES_LIST (ih, im, il) (do_expands, do_case_splits) = ih@[ 3590 (5, VAR_RES_INFERENCES_LIST___cheap_simplifications), 3591 (3, VAR_RES_INFERENCES_LIST___simulate_minor_command), 3592 (2, VAR_RES_INFERENCES_LIST___entailment_steps), 3593 (2, VAR_RES_INFERENCES_LIST___entailment_solve), 3594 (1, VAR_RES_INFERENCES_LIST___simulate_command), 3595 (1, VAR_RES_INFERENCES_LIST___mayor_step)]@ 3596 im@[ 3597 (5, VAR_RES_INFERENCES_LIST___expensive_simplifications___hoare_triple), 3598 (5, VAR_RES_INFERENCES_LIST___expensive_simplifications___frame_split), 3599 (5, VAR_RES_INFERENCES_LIST___expensive_simplifications___general)]@ 3600 (if do_expands then [(2, VAR_RES_INFERENCES_LIST___expands_entailment),(2, VAR_RES_INFERENCES_LIST___expands)] else [])@ 3601 (if do_case_splits then [(2, VAR_RES_INFERENCES_LIST___case_splits)] else [])@ 3602 il; 3603 3604type gen_step_param = 3605 {use_asms : bool, 3606 do_case_splits : bool, 3607 expands_level : int, 3608 generate_vcs : bool, 3609 fast : bool, 3610 prop_simp_level: int, 3611 stop_evals : (term -> bool) list, 3612 inferences : (int * var_res_inference_group) list * 3613 (int * var_res_inference_group) list * 3614 (int * var_res_inference_group) list}; 3615 3616 3617fun gen_step_param___update_stop_evals 3618 ({use_asms = asms, 3619 do_case_splits = cs, 3620 expands_level = ex, 3621 generate_vcs = vcs, 3622 fast = f, 3623 stop_evals = sel, 3624 inferences = inf, 3625 prop_simp_level = ps}:gen_step_param) l = 3626 ({use_asms = asms, 3627 do_case_splits = cs, 3628 expands_level = ex, 3629 generate_vcs = vcs, 3630 fast = f, 3631 prop_simp_level = ps, 3632 inferences = inf, 3633 stop_evals = l}:gen_step_param); 3634 3635 3636fun gen_step_param___update_use_asms 3637 ({use_asms = asms, 3638 do_case_splits = cs, 3639 expands_level = ex, 3640 generate_vcs = vcs, 3641 fast = f, 3642 stop_evals = sel, 3643 inferences = inf, 3644 prop_simp_level = ps}:gen_step_param) b = 3645 ({use_asms = b, 3646 do_case_splits = cs, 3647 expands_level = ex, 3648 generate_vcs = vcs, 3649 fast = f, 3650 stop_evals = sel, 3651 inferences = inf, 3652 prop_simp_level = ps}:gen_step_param); 3653 3654fun gen_step_param___update_cs 3655 ({use_asms = asms, 3656 do_case_splits = cs, 3657 expands_level = ex, 3658 generate_vcs = vcs, 3659 fast = f, 3660 stop_evals = sel, 3661 inferences = inf, 3662 prop_simp_level = ps}:gen_step_param) b = 3663 ({use_asms = asms, 3664 do_case_splits = b, 3665 expands_level = ex, 3666 generate_vcs = vcs, 3667 fast = f, 3668 stop_evals = sel, 3669 inferences = inf, 3670 prop_simp_level = ps}:gen_step_param); 3671 3672fun gen_step_param___update_vcs 3673 ({use_asms = asms, 3674 do_case_splits = cs, 3675 expands_level = ex, 3676 generate_vcs = vcs, 3677 fast = f, 3678 stop_evals = sel, 3679 inferences = inf, 3680 prop_simp_level = ps}:gen_step_param) b = 3681 ({use_asms = asms, 3682 do_case_splits = cs, 3683 expands_level = ex, 3684 generate_vcs = b, 3685 fast = f, 3686 stop_evals = sel, 3687 inferences = inf, 3688 prop_simp_level = ps}:gen_step_param); 3689 3690fun gen_step_param___update_expands 3691 ({use_asms = asms, 3692 do_case_splits = cs, 3693 expands_level = ex, 3694 generate_vcs = vcs, 3695 fast = f, 3696 stop_evals = sel, 3697 inferences = inf, 3698 prop_simp_level = ps}:gen_step_param) n = 3699 ({use_asms = asms, 3700 do_case_splits = cs, 3701 expands_level = n, 3702 generate_vcs = vcs, 3703 fast = f, 3704 stop_evals = sel, 3705 inferences = inf, 3706 prop_simp_level = ps}:gen_step_param); 3707 3708fun gen_step_param___update_fast 3709 ({use_asms = asms, 3710 do_case_splits = cs, 3711 expands_level = ex, 3712 generate_vcs = vcs, 3713 fast = f, 3714 stop_evals = sel, 3715 inferences = inf, 3716 prop_simp_level = ps}:gen_step_param) b = 3717 ({use_asms = asms, 3718 do_case_splits = cs, 3719 expands_level = ex, 3720 generate_vcs = vcs, 3721 fast = b, 3722 stop_evals = sel, 3723 inferences = inf, 3724 prop_simp_level = ps}:gen_step_param); 3725 3726fun gen_step_param___update_prop_simps 3727 ({use_asms = asms, 3728 do_case_splits = cs, 3729 expands_level = ex, 3730 generate_vcs = vcs, 3731 fast = f, 3732 stop_evals = sel, 3733 inferences = inf, 3734 prop_simp_level = ps}:gen_step_param) n = 3735 ({use_asms = asms, 3736 do_case_splits = cs, 3737 expands_level = ex, 3738 generate_vcs = vcs, 3739 fast = f, 3740 stop_evals = sel, 3741 inferences = inf, 3742 prop_simp_level = n}:gen_step_param); 3743 3744fun gen_step_param___update_inferences 3745 ({use_asms = asms, 3746 do_case_splits = cs, 3747 expands_level = ex, 3748 generate_vcs = vcs, 3749 fast = f, 3750 stop_evals = sel, 3751 inferences = inf, 3752 prop_simp_level = ps}:gen_step_param) inf' = 3753 ({use_asms = asms, 3754 do_case_splits = cs, 3755 expands_level = ex, 3756 generate_vcs = vcs, 3757 fast = f, 3758 stop_evals = sel, 3759 inferences = inf', 3760 prop_simp_level = ps}:gen_step_param); 3761 3762 3763fun gen_step_param___add_inferences p (inf_h', inf_m', inf_l') = 3764 let 3765 val (inf_h, inf_m, inf_l) = #inferences p; 3766 in 3767 gen_step_param___update_inferences p (inf_h'@inf_h, inf_m'@inf_m, inf_l'@inf_l) 3768 end; 3769 3770 3771local 3772 3773fun gen_step_conv_map_fun l s f = f; 3774 3775fun gen_step_conv_map_fun l s f = 3776 let 3777 fun f1 x = 3778 (((!(do_profile_ref ())) s (fn () => 3779 (f x))) ()) 3780 fun f2 x = if !verbose_level = 0 andalso !verbose_level_try = 0 then f1 x else 3781 let 3782 val _ = if (l < !verbose_level_try) then 3783 print ("trying "^ s ^ "\n") else () 3784 val y = f1 x; 3785 val _ = if (l < !verbose_level orelse l < !verbose_level_try) then 3786 print ("applying "^ s ^ "\n") else () 3787 in y end 3788 in f2 end 3789 3790fun step_conv_map_fun l s1 (s2, c:var_res_inference) = 3791 let 3792 val s = s1 ^ " - "^s2; 3793 fun f1 (p, context, dir, t) = c p context dir t; 3794 fun f2 p context dir t = 3795 gen_step_conv_map_fun l s f1 (p, context, dir, t); 3796 in 3797 f2 3798 end; 3799 3800fun convL p stops n list = 3801 let 3802 fun pre (l, (s1, guard, before_flag, continue_simp, cL)) = 3803 let 3804 val cL' = map (step_conv_map_fun l s1) cL 3805 fun conv context dir t = 3806 if (not (guard t) orelse (stops t)) then raise UNCHANGED else 3807 tryfind (fn c => c p context dir t) cL' 3808 val w = (if l <= n then SOME 1 else if continue_simp then NONE else SOME 0); 3809 in 3810 (before_flag, w, conv) 3811 end; 3812 in 3813 map pre list 3814 end; 3815 3816in 3817 3818(* 3819val cache_opt = SOME (mk_DEPTH_CONSEQ_CONV_CACHE, 3820 fn (t, (n, thm_opt)) => 3821 not ((isSome thm_opt) orelse 3822 (is_forall t) orelse (is_exists t) orelse 3823 (is_imp_only t) orelse (is_disj t) orelse 3824 (is_conj t) orelse (is_neg t))) 3825 3826val cache_opt = SOME (mk_DEPTH_CONSEQ_CONV_CACHE, K true) 3827val cache_opt = CONSEQ_CONV_default_cache_opt 3828val cache_opt = NONE 3829*) 3830 3831 3832type user_rewrite_param = (Abbrev.thm list * Abbrev.conv list * simpLib.ssfrag list); 3833 3834fun mk_ssfrag (thmL, convL, ssfragL) = 3835 let 3836 val ss1 = simpLib.rewrites thmL; 3837 val ss2 = simpLib.SSFRAG {name=NONE, convs = 3838 (map (fn c => {conv = K (K c), key = NONE, name = "user-conversion", trace = 2}) convL), 3839 filter = NONE, ac=[], dprocs=[], congs=[], rewrs = []}; 3840 in 3841 simpLib.merge_ss (ss1::ss2::ssfragL) 3842 end 3843 3844val CONSEQ_CONV_CONGRUENCE___var_res_list = 3845 (CONSEQ_CONV_get_context_congruences CONSEQ_CONV_IMP_CONTEXT) @ [ 3846 CONSEQ_CONV_CONGRUENCE___location_comment] 3847 3848 3849fun vc_conv vc step_opt = 3850 if not vc then (K (0, NONE)) else 3851 EXT_DEPTH_NUM_CONSEQ_CONV CONSEQ_CONV_CONGRUENCE___var_res_list NONE step_opt true 3852 [(true, SOME 1, fn context => 3853 (K (VAR_RES_FRAME_SPLIT_INFERENCE___SOLVE___CONSEQ_CONV true false context)))] [] 3854 CONSEQ_CONV_STRENGTHEN_direction; 3855 3856(* 3857 val ((fast, vc, cs), ssp, step_opt, n, context) = 3858 ((false, false, true), ([],[],[]), NONE, 2, []) 3859*) 3860 3861fun VAR_RES_GEN_STEP_CONSEQ_CONV (p:gen_step_param) ssp step_opt n context = 3862 let 3863 val list = VAR_RES_INFERENCES_LIST (#inferences p) (#expands_level p > 0, #do_case_splits p); 3864 val stops = if null (#stop_evals p) then K false else 3865 (fn t => (exists (fn pp => (pp t) handle Interrupt => raise Interrupt 3866 | _ => false) (#stop_evals p))) 3867 3868 val ssp0 = not (#prop_simp_level p = 0); 3869 val ssp1 = simpLib.merge_ss [var_res_param.predicate_ssfrag (#prop_simp_level p), 3870 (mk_ssfrag ssp)]; 3871 val prop_simp_CONV = VAR_RES_PROP_REWRITE_CONV (ssp0,ssp1) []; 3872 3873 val param = ({fast = #fast p, 3874 expands_level = #expands_level p, 3875 do_prop_simps = ssp0, 3876 prop_simp_ss = ssp1}:var_res_inference_param); 3877 3878 val cL = convL param stops n list; 3879 3880 fun mc step_opt = 3881 EXT_DEPTH_NUM_CONSEQ_CONV CONSEQ_CONV_CONGRUENCE___var_res_list NONE step_opt true 3882 cL context CONSEQ_CONV_STRENGTHEN_direction 3883 val vcc = vc_conv (#generate_vcs p); 3884 3885 fun fc step_opt t = 3886 let 3887 val (n1, thm1_opt) = mc step_opt t; 3888 val step_opt' = step_opt_sub step_opt n1; 3889 val t' = if (isSome thm1_opt) then ((fst o dest_imp o concl o valOf) thm1_opt) else t 3890 3891 fun apply_second_step s f (n2, thm2_opt) = 3892 if (isSome thm2_opt) then (n2, thm2_opt) else 3893 ((gen_step_conv_map_fun 1 ("toplevel - "^s) 3894 (fn x => let 3895 val (n, thm_opt) = f x; 3896 val _ = if isSome thm_opt then () else Feedback.fail() 3897 in (n, thm_opt) end) t') 3898 handle Interrupt => raise Interrupt 3899 | _ => (0, NONE)) 3900 3901 3902 val (n2, thm2_opt) = apply_second_step "Normalise Structure" 3903 (fn t' => ( 3904 (0, SOME (snd (EQ_IMP_RULE (((REDEPTH_CONV VAR_RES_STRUCTURE_NORMALISE_CONV) THENC 3905 REWRITE_CONV []) t')))))) (0, NONE); 3906 3907 val (n2, thm2_opt) = apply_second_step "Generate verification conditions" 3908 (fn t' => (if step_opt_allows_steps step_opt' 0 (SOME 1) then 3909 vcc step_opt' t' else (0, NONE))) (n2, thm2_opt); 3910 3911 val (n2, thm2_opt) = apply_second_step "Simplification" 3912 (fn t' => if not (step_opt_allows_steps step_opt' 0 (SOME 1)) then (0, NONE) else 3913 (1, SOME (snd (EQ_IMP_RULE (prop_simp_CONV t'))))) (n2, thm2_opt); 3914 3915 3916 val thm = 3917 if (isSome thm1_opt) then 3918 (if (isSome thm2_opt) then 3919 IMP_TRANS (valOf thm2_opt) (valOf thm1_opt) 3920 else valOf thm1_opt) 3921 else 3922 (if (isSome thm2_opt) then 3923 valOf thm2_opt 3924 else raise UNCHANGED) 3925 in 3926 if not (isSome thm2_opt) then thm else 3927 let 3928 val step_opt'' = step_opt_sub step_opt' n2; 3929 val t'' = (fst o dest_imp o concl) thm 3930 val thm3_opt = SOME (fc step_opt'' t'') handle UNCHANGED => NONE 3931 in 3932 if (isSome thm3_opt) then 3933 IMP_TRANS (valOf thm3_opt) thm 3934 else thm 3935 end 3936 end; 3937 in 3938 fc step_opt 3939 end; 3940 3941end; 3942 3943 3944fun VAR_RES_GEN_STEP_TAC (p:gen_step_param) ss step_opt n = 3945 if (#use_asms p) then 3946 (DISCH_ASM_CONSEQ_CONV_TAC (K (VAR_RES_GEN_STEP_CONSEQ_CONV p ss step_opt n []))) 3947 else 3948 (CONSEQ_CONV_TAC (K (VAR_RES_GEN_STEP_CONSEQ_CONV p ss step_opt n []))); 3949 3950 3951datatype gen_step_tac_opt = 3952 case_splits_flag of bool 3953 | expands_level of int 3954 | fast_flag of bool 3955 | prop_simp_level of int 3956 | use_asms_flag of bool 3957 | generate_vcs_flag of bool 3958 | add_rewrites of thm list 3959 | add_convs of conv list 3960 | add_ssfrags of simpLib.ssfrag list 3961 | stop_evals of (term -> bool) list 3962 | combined_gen_step_tac_opt of gen_step_tac_opt list 3963 | add_inference_groups of (int * var_res_inference_group) list * 3964 (int * var_res_inference_group) list * 3965 (int * var_res_inference_group) list; 3966 3967val no_case_splits = case_splits_flag false; 3968val no_expands = expands_level 0; 3969val no_case_split_expands = combined_gen_step_tac_opt [no_case_splits, no_expands] 3970val do_case_splits = case_splits_flag true; 3971val do_expands = expands_level 1; 3972val full_expands = expands_level 2; 3973val generate_vcs = generate_vcs_flag true; 3974val dont_generate_vcs = generate_vcs_flag false; 3975val no_asms = use_asms_flag false; 3976val use_asms = use_asms_flag true; 3977val no_prop_simps = prop_simp_level 0; 3978val simple_prop_simps = prop_simp_level 1; 3979val full_prop_simps = prop_simp_level 3; 3980val conservative = fast_flag false; 3981val careful = combined_gen_step_tac_opt [no_case_splits, no_expands, no_asms]; 3982 3983val stop_at_while = stop_evals [fn t => 3984 let 3985 val (p1_0,_,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location t; 3986 in 3987 is_asl_comment_loop_invariant p1_0 orelse 3988 is_asl_comment_loop_spec p1_0 orelse 3989 is_asl_prog_while p1_0 3990 end] 3991 3992val stop_at_cond = stop_evals [fn t => 3993 let 3994 val (p1_0,_,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location t; 3995 in 3996 is_asl_prog_cond p1_0 3997 end] 3998 3999val stop_at_abstraction = stop_evals [fn t => 4000 let 4001 val (p1_0,_,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location t; 4002 in 4003 is_asl_comment_abstraction p1_0 4004 end] 4005 4006val stop_at_block_spec = stop_evals [fn t => 4007 let 4008 val (p1_0,_,_,_,_,_) = dest_VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND_location t; 4009 in 4010 is_asl_comment_block_spec p1_0 4011 end] 4012 4013 4014val stop_at_frame_calc = stop_evals [is_VAR_RES_FRAME_SPLIT] 4015val stop_at_hoare_triple = stop_evals [is_VAR_RES_COND_HOARE_TRIPLE] 4016 4017 4018 4019fun gen_step_tac_opt_eval (p:gen_step_param, ssp) [] = (p, ssp) 4020 | gen_step_tac_opt_eval (p, (rw, cv, ss)) 4021 ((add_rewrites thmL)::gstoL) = 4022 gen_step_tac_opt_eval (p, (rw@thmL, cv, ss)) gstoL 4023 | gen_step_tac_opt_eval (p, (rw, cv, ss)) 4024 ((add_convs convL)::gstoL) = 4025 gen_step_tac_opt_eval (p, (rw, cv@convL, ss)) gstoL 4026 | gen_step_tac_opt_eval (p, (rw, cv, ss)) 4027 ((add_ssfrags ssfL)::gstoL) = 4028 gen_step_tac_opt_eval (p, (rw, cv, ss@ssfL)) gstoL 4029 | gen_step_tac_opt_eval (p, ssp) 4030 ((case_splits_flag b)::gstoL) = 4031 gen_step_tac_opt_eval (gen_step_param___update_cs p b, ssp) gstoL 4032 | gen_step_tac_opt_eval (p, ssp) 4033 ((expands_level n)::gstoL) = 4034 gen_step_tac_opt_eval (gen_step_param___update_expands p n, ssp) gstoL 4035 | gen_step_tac_opt_eval (p, ssp) 4036 ((fast_flag b)::gstoL) = 4037 gen_step_tac_opt_eval (gen_step_param___update_fast p b, ssp) gstoL 4038 | gen_step_tac_opt_eval (p, ssp) 4039 ((prop_simp_level n)::gstoL) = 4040 gen_step_tac_opt_eval (gen_step_param___update_prop_simps p n, ssp) gstoL 4041 | gen_step_tac_opt_eval (p, ssp) 4042 ((use_asms_flag b)::gstoL) = 4043 gen_step_tac_opt_eval (gen_step_param___update_use_asms p b, ssp) gstoL 4044 | gen_step_tac_opt_eval (p, ssp) 4045 ((generate_vcs_flag b)::gstoL) = 4046 gen_step_tac_opt_eval (gen_step_param___update_vcs p b, ssp) gstoL 4047 | gen_step_tac_opt_eval (p, ssp) 4048 ((stop_evals b)::gstoL) = 4049 gen_step_tac_opt_eval (gen_step_param___update_stop_evals p b, ssp) gstoL 4050 | gen_step_tac_opt_eval (p, ssp) 4051 ((add_inference_groups ipg)::gstoL) = 4052 gen_step_tac_opt_eval (gen_step_param___add_inferences p ipg, ssp) gstoL 4053 | gen_step_tac_opt_eval (p, ssp) 4054 ((combined_gen_step_tac_opt optL)::gstoL) = 4055 gen_step_tac_opt_eval (p, ssp) (optL@gstoL) 4056 4057 4058val default_params = ( 4059 {do_case_splits = true, 4060 expands_level = 1, 4061 fast = true, 4062 use_asms = true, 4063 prop_simp_level = 3, 4064 stop_evals = [], 4065 inferences = ([],[],[]), 4066 generate_vcs = false}, ([],[],[])); 4067 4068 4069fun xVAR_RES_GEN_STEP_TAC optL = 4070 let 4071 val (p,ssp) = gen_step_tac_opt_eval default_params optL; 4072 in 4073 VAR_RES_GEN_STEP_TAC p ssp 4074 end; 4075 4076 4077fun xVAR_RES_GEN_STEP_CONSEQ_CONV optL n m = 4078 let 4079 val (p,ssp) = gen_step_tac_opt_eval default_params optL 4080 in 4081 VAR_RES_GEN_STEP_CONSEQ_CONV p ssp n m [] 4082 end; 4083 4084 4085 4086val _ = Rewrite.add_implicit_rewrites [asl_comments_TF_ELIM]; 4087val VAR_RES_PURE_VC_TAC = 4088 CONSEQ_CONV_TAC (K (fn t => 4089 let 4090 val (_, thm_opt) = vc_conv true NONE t 4091 in 4092 if isSome thm_opt then valOf thm_opt else raise UNCHANGED 4093 end)) 4094 4095val VAR_RES_ELIM_COMMENTS_TAC = REWRITE_TAC [asl_comments_ELIM] 4096val VAR_RES_VC_TAC = (TRY VAR_RES_PURE_VC_TAC) THEN VAR_RES_ELIM_COMMENTS_TAC 4097 4098 4099 4100 4101val VAR_RES_SPECIFICATION_TAC = 4102 CONSEQ_CONV_TAC (K VAR_RES_SPECIFICATION___CONSEQ_CONV) 4103 4104 4105fun VAR_RES_SINGLE_ENTAILMENT_INIT_CONSEQ_CONV t = 4106 if (is_VAR_RES_FRAME_SPLIT t) then EVERY_CONSEQ_CONV [ 4107 TRY_CONV VAR_RES_FRAME_SPLIT_INFERENCE___ALL_CONST_INTRO___CONV, 4108 DEPTH_STRENGTHEN_CONSEQ_CONV VAR_RES_FRAME_SPLIT_INFERENCE___asl_exists___CONSEQ_CONV, 4109 DEPTH_CONV VAR_RES_FRAME_SPLIT_INFERENCE___asl_star___CONV] t 4110 else raise UNCHANGED 4111 4112val VAR_RES_ENTAILMENT_INIT___CONSEQ_CONV = 4113 DEPTH_STRENGTHEN_CONSEQ_CONV VAR_RES_SINGLE_ENTAILMENT_INIT_CONSEQ_CONV 4114 4115val VAR_RES_ENTAILMENT_INIT_TAC = 4116 CONSEQ_CONV_TAC (K VAR_RES_ENTAILMENT_INIT___CONSEQ_CONV); 4117 4118end 4119 4120 4121