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