1(*---------------------------------------------------------------------------* 2 * The "imperative" library. This provides a collection of proof tactics * 3 * that are called upon by imperativeTheory * 4 * * 5 *---------------------------------------------------------------------------*) 6 7structure imperativeLib :> imperativeLib = 8struct 9 10open HolKernel Parse boolLib bossLib ptopTheory ; 11 12fun APPLY_DEFINITIONS_TO_THEOREM definitions th = 13 ( 14 BETA_RULE 15 ( 16 GEN_ALL 17 ( 18 PURE_ONCE_REWRITE_RULE definitions th 19 ) 20 ) 21 ) 22; 23 24fun APPLY_DEFINITIONS_TAC definitions = 25 (PURE_ONCE_REWRITE_TAC definitions ) 26 THEN 27 (REPEAT GEN_TAC) 28 THEN 29 (BETA_TAC) 30; 31 32(* 33val REFINEMENT_RATOR = rator(rator(``u [=. v``)); 34 35val REFINEMENT_NOT_RATOR = rator(rator(``u [<>. v``)); 36*) 37 38val REFINEMENT_RATOR = ``$[=.``; 39 40val REFINEMENT_NOT_RATOR = ``$[<>.``; 41 42fun REFINEMENT_RULE th = APPLY_DEFINITIONS_TO_THEOREM [ptopTheory.bRefinement_def,ptopTheory.bRefinementNot_def] th ; 43 44val REFINEMENT_TAC = APPLY_DEFINITIONS_TAC [ptopTheory.bRefinement_def, ptopTheory.bRefinementNot_def]; 45 46 47fun SWAPLR_RULE th =(PURE_ONCE_REWRITE_RULE [EQ_SYM_EQ] th); 48 49fun EXHAUSTIVELY x = 50 (REPEAT (CHANGED_TAC x)) 51; 52 53val REP_EVAL_TAC = 54 (EXHAUSTIVELY EVAL_TAC) 55; 56 57fun USE_CONTEXT (asl:term list) (th:thm) = 58 if (null asl) then th else (UNDISCH (USE_CONTEXT (tl(asl)) th)) 59; 60 61fun VSUB (v:term) (e:term) (th:thm) = 62 USE_CONTEXT (hyp th) (SPEC e (GEN v (DISCH_ALL th))) 63; 64 65fun MAKE_IT_SO (th:thm) = 66 ((SUBST_TAC [(VSUB ``v:bool`` (concl th) PTOP_ACCEPT_IN_PLACE)]) THEN EVAL_TAC) 67; 68 69fun MAKE_IT_NO (th:thm) = 70 if(is_neg(concl th)) then 71 ((SUBST_TAC [(VSUB ``v:bool`` (dest_neg(concl th)) PTOP_REJECT_IN_PLACE)]) THEN EVAL_TAC) 72 else 73 ((SUBST_TAC [(VSUB ``v:bool`` (mk_neg(concl th)) PTOP_REJECT_IN_PLACE)]) THEN EVAL_TAC) 74; 75 76fun EVAL_FOR_STATEVARS valList = 77 if(null valList) then 78 ( 79 (REPEAT DISCH_TAC) 80 THEN 81 (REPEAT (FIRST_ASSUM (fn th => (CHANGED_TAC (SUBST_TAC [th]))) )) 82 ) 83 else 84 ( 85 (EVERY_ASSUM 86 (fn th => let val instance = (SPECL [(hd valList)] th) 87 in 88 ( 89 (ASSUME_TAC instance) THEN 90 (UNDISCH_TAC (concl instance)) THEN 91 (REP_EVAL_TAC) 92 ) 93 end 94 ) 95 ) 96 THEN 97 ( 98 EVAL_FOR_STATEVARS (tl valList) 99 ) 100 ) 101; 102 103fun DISTINCT_STATEVARS (boundVarAndType: term) (disjList: term) (asl : term list) = 104 if( is_disj(disjList) ) then ( 105 let val lhsRhs = (dest_disj(disjList)) in 106 let val asm = mk_forall ( boundVarAndType, ( mk_imp ( #2(lhsRhs), (mk_neg (#1(lhsRhs)) ) ) ) ) in 107 DISTINCT_STATEVARS boundVarAndType (#1(lhsRhs)) (asm :: asl) 108 end 109 end 110 ) else 111 asl 112; 113 114fun DECL_NEXT_DISJLIST (boundVarAndType:term) (stateVars: term list) (disjList: term) = 115 if(null stateVars) then ( 116 disjList 117 ) else ( 118 DECL_NEXT_DISJLIST boundVarAndType (tl stateVars) ( mk_disj ( disjList, (mk_eq ( boundVarAndType, (hd stateVars) ) ) ) ) 119 ) 120; 121 122fun DECL_DISJLIST (boundVarAndType:term) (stateVars: term list) = 123 if (null stateVars) then ( 124 mk_eq (boundVarAndType,boundVarAndType ) 125 ) else ( 126 DECL_NEXT_DISJLIST boundVarAndType (tl stateVars) ( mk_eq( boundVarAndType, (hd stateVars) ) ) 127 ) 128; 129 130fun DECL_STATEVARS (boundVarAndType : term) ( stateVars : term list) = 131 let val disjList = (DECL_DISJLIST boundVarAndType stateVars) 132 in ( 133 if (null stateVars) then ( 134 [] 135 ) else ( 136 DISTINCT_STATEVARS boundVarAndType disjList [ ( mk_forall (boundVarAndType,disjList) ) ] 137 ) 138 ) 139 end 140; 141 142end 143