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