1open HolKernel Parse boolLib bossLib
2open arithmeticTheory whileTheory pairTheory pred_setTheory progTheory;
3
4val _ = new_theory "triple";
5
6infix \\
7val op \\ = op THEN;
8
9(* we define a total-correctness machine-code Hoare triple *)
10
11val TRIPLE_def = Define`
12   TRIPLE (assert,model) pre code post =
13     FST post ==> FST pre /\
14     SPEC model (assert (SND pre)) code (assert (SND post))`
15
16val TERM_TAILREC_def = zDefine`
17   TERM_TAILREC f g (d:'a -> bool # 'b) x =
18    let (cond,y) = d (WHILE g f x) in
19      (cond /\ (?n. ~g (FUNPOW f n x)),y)`
20
21val SHORT_TERM_TAILREC_def = Define`
22   SHORT_TERM_TAILREC (f:'a -> 'a + (bool # 'b)) =
23    TERM_TAILREC (OUTL o f) (ISL o f) (OUTR o f)`
24
25val case_sum_def = Define`
26   case_sum f1 f2 x = case x of INL y => f1 y | INR y => f2 y`
27
28(* theorems about this Hoare triple *)
29
30val TRIPLE_COMPOSE = Q.store_thm("TRIPLE_COMPOSE",
31   `!i p c m q. TRIPLE i p c m /\ TRIPLE i m c q ==> TRIPLE i p c q`,
32   simp [TRIPLE_def, FORALL_PROD]
33   \\ REPEAT strip_tac
34   \\ metis_tac [SPEC_COMPOSE, UNION_IDEMPOT]
35   )
36
37val TRIPLE_EXTEND = Q.store_thm("TRIPLE_EXTEND",
38   `!i p c q c'. TRIPLE i p c q ==> c SUBSET c' ==> TRIPLE i p c' q`,
39   simp [TRIPLE_def, FORALL_PROD]
40   \\ REPEAT strip_tac
41   \\ metis_tac [SPEC_SUBSET_CODE]
42   )
43
44val TRIPLE_REFL = Q.store_thm("TRIPLE_REFL",
45   `!i c p. TRIPLE i p c p`,
46   simp [FORALL_PROD, TRIPLE_def, SPEC_REFL]
47   )
48
49val TRIPLE_COMPOSE_ALT = Q.store_thm("TRIPLE_COMPOSE_ALT",
50   `!i p c m q. TRIPLE i m c q ==> TRIPLE i p c m ==> TRIPLE i p c q`,
51   metis_tac [TRIPLE_COMPOSE]
52   )
53
54val COND_MERGE = Q.store_thm("COND_MERGE",
55   `(x1 ==> f (g x2)) /\ (~x1 ==> f (g y2)) ==> f (g (if x1 then x2 else y2))`,
56   Cases_on `x1` \\ fs []
57   )
58
59val TERM_TAILREC_THM = Q.store_thm("TERM_TAILREC_THM",
60   `TERM_TAILREC f g d x = if g x then TERM_TAILREC f g d (f x) else d x`,
61   REVERSE (Cases_on `g x`)
62   \\ fs [TERM_TAILREC_def, LET_DEF]
63   \\ simp [Once WHILE]
64   >- (Cases_on `d x`
65       \\ Cases_on `q`
66       \\ fs []
67       \\ qexists_tac `0`
68       \\ fs [FUNPOW])
69   \\ Cases_on `(d (WHILE g f (f x)))`
70   \\ fs []
71   \\ Cases_on `q`
72   \\ fs []
73   \\ REPEAT strip_tac
74   \\ eq_tac
75   \\ REPEAT strip_tac
76   >- (Cases_on `n` \\ fs [FUNPOW] \\ metis_tac [])
77   \\ qexists_tac `SUC n`
78   \\ fs [FUNPOW]
79   )
80
81val () = computeLib.add_persistent_funs ["TERM_TAILREC_THM"]
82
83val TRIPLE_TERM_TAILREC = Q.prove(
84   `(!x. ~FST (post (F,x))) ==>
85    (!x. TRIPLE i (pre x) c (if g x then pre (f x) else post (d x))) ==>
86    (!x. TRIPLE i (pre x) c (post (TERM_TAILREC f g d x)))`,
87   Cases_on `i`
88   \\ simp [TERM_TAILREC_def, LET_DEF]
89   \\ REPEAT strip_tac
90   \\ REVERSE (Cases_on `?n. ~g (FUNPOW f n x)`)
91   >- (fs []
92       \\ Cases_on `d (WHILE g f x)`
93       \\ fs [TRIPLE_def])
94   \\ qpat_x_assum `!c. ~bbb` kall_tac
95   \\ fs []
96   \\ pop_assum mp_tac
97   \\ Q.SPEC_TAC (`x`, `x`)
98   \\ Induct_on `n`
99   \\ fs [FUNPOW]
100   \\ REPEAT strip_tac
101   >- (qpat_x_assum `!x.bbb` (MP_TAC o Q.SPEC `x`)
102       \\ once_rewrite_tac [WHILE]
103       \\ fs []
104       \\ Cases_on `d x`
105       \\ fs []
106       \\ REPEAT strip_tac
107       \\ fs []
108       \\ REVERSE (sg `q' /\ (?n. ~g (FUNPOW f n x)) = q'`)
109       \\ fs []
110       \\ Cases_on `q'`
111       \\ fs []
112       \\ qexists_tac `0`
113       \\ fs [FUNPOW])
114   \\ REPEAT strip_tac
115   \\ REVERSE (Cases_on `g x`)
116   >- (pop_assum mp_tac
117       \\ pop_assum kall_tac
118       \\ pop_assum kall_tac
119       \\ qpat_x_assum `!x.bbb` (MP_TAC o Q.SPEC `x`)
120       \\ once_rewrite_tac [WHILE]
121       \\ fs []
122       \\ Cases_on `d x`
123       \\ fs []
124       \\ REPEAT strip_tac
125       \\ fs []
126       \\ REVERSE (sg `q' /\ (?n. ~g (FUNPOW f n x)) = q'`)
127       \\ fs []
128       \\ Cases_on `q'`
129       \\ fs []
130       \\ qexists_tac `0`
131       \\ fs [FUNPOW])
132   \\ match_mp_tac TRIPLE_COMPOSE
133   \\ qexists_tac `pre (f x)`
134   \\ strip_tac
135   >- metis_tac []
136   \\ res_tac
137   \\ once_rewrite_tac [WHILE]
138   \\ fs []
139   \\ `(?n. ~g (FUNPOW f n (f x))) = (?n. ~g (FUNPOW f n x))` by (REPEAT strip_tac
140       \\ eq_tac
141       \\ REPEAT strip_tac
142       >- (qexists_tac `SUC n'` \\ fs [FUNPOW])
143       \\ Cases_on `n'`
144       \\ fs [FUNPOW]
145       \\ metis_tac [])
146   \\ fs []
147   )
148
149val case_sum_thm = Q.prove(
150   `!x. case_sum pre post x = if ISL x then pre (OUTL x) else post (OUTR x)`,
151   Cases \\ SRW_TAC [] [case_sum_def])
152
153val SHORT_TERM_TAILREC = Q.store_thm("SHORT_TERM_TAILREC",
154   `(!x. TRIPLE i (pre x) c (case_sum pre post (f x))) ==>
155    (!c x state. ~(FST (post (F,x)))) ==>
156    (!x. TRIPLE i (pre x) c (post (SHORT_TERM_TAILREC f x)))`,
157   simp [SHORT_TERM_TAILREC_def, LET_DEF]
158   \\ REPEAT strip_tac
159   \\ match_mp_tac (REWRITE_RULE [AND_IMP_INTRO] TRIPLE_TERM_TAILREC)
160   \\ fs [case_sum_thm]
161   )
162
163val TRIPLE_FRAME_BOOL = Q.store_thm("TRIPLE_FRAME_BOOL",
164   `!i. TRIPLE i (c1,pre) code (c2,post) ==>
165        !c. TRIPLE i (c /\ c1,pre) code (c /\ c2,post)`,
166   simp [TRIPLE_def, FORALL_PROD]
167   \\ REPEAT strip_tac
168   \\ Cases_on `c`
169   \\ fs []
170   )
171
172val INTRO_TRIPLE = Q.store_thm("INTRO_TRIPLE",
173   `!M. (side ==> SPEC (SND M) (FST M pre) code (FST M post)) ==>
174        !c. TRIPLE M (c, pre) code (c /\ side, post)`,
175   Cases \\ SIMP_TAC std_ss [TRIPLE_def]
176   )
177
178val _ = export_theory()
179