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