|
1
|
1 data HTProof : Cond -> Comm -> Cond -> Set where
|
|
|
2 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
|
|
|
3 (pr : Axiom bPre pcm bPost) ->
|
|
|
4 HTProof bPre (PComm pcm) bPost
|
|
|
5 SkipRule : (b : Cond) -> HTProof b Skip b
|
|
|
6 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
|
|
|
7 HTProof bPre Abort bPost
|
|
|
8 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
|
|
|
9 {bPost' : Cond} -> {bPost : Cond} ->
|
|
|
10 Tautology bPre bPre' ->
|
|
|
11 HTProof bPre' cm bPost' ->
|
|
|
12 Tautology bPost' bPost ->
|
|
|
13 HTProof bPre cm bPost
|
|
|
14 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
|
|
|
15 {cm2 : Comm} -> {bPost : Cond} ->
|
|
|
16 HTProof bPre cm1 bMid ->
|
|
|
17 HTProof bMid cm2 bPost ->
|
|
|
18 HTProof bPre (Seq cm1 cm2) bPost
|
|
|
19 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
|
|
|
20 {bPre : Cond} -> {bPost : Cond} ->
|
|
|
21 {b : Cond} ->
|
|
|
22 HTProof (bPre /\ b) cmThen bPost ->
|
|
|
23 HTProof (bPre /\ neg b) cmElse bPost ->
|
|
|
24 HTProof bPre (If b cmThen cmElse) bPost
|
|
|
25 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
|
|
|
26 HTProof (bInv /\ b) cm bInv ->
|
|
|
27 HTProof bInv (While b cm) (bInv /\ neg b)
|
