1 2%----------------------------------------------------------------------------% 3% The stuff in this file is just `doodlings` and does not work! % 4%----------------------------------------------------------------------------% 5 6new_theory`ITL`;; 7 8% Test if an interval function only depends on the start time 9 of the interval % 10 11new_definition 12 (`IS_SIG`, 13 "IS_SIG (X:num->num->*) = ?f. !m n. X m n = f m");; 14 15% Make an interval function out of a signal % 16 17new_definition 18 (`MK_SIG`, 19 "MK_SIG (f:num->*) = \m (n:num). f m");; 20 21% Test if an interval function is a constant function % 22 23new_definition 24 (`IS_STATIC`, 25 "IS_STATIC (X:num->num->*) = ?c. !m n. X m n = c");; 26 27% Make an interval function out of a constant % 28 29new_definition 30 (`MK_STATIC`, 31 "MK_STATIC (c:*) = \m:num.\n:num. c");; 32 33% The ITL next operator for expressions. This is called "O" in Ben's papers 34 but I use that name for the next operator for formulas (see below) % 35 36new_definition 37 (`NEXT`, 38 "NEXT (X:num->num->*) = \m n. X (m+1) n");; 39 40% ITL Equality % 41 42new_infix_definition 43 (`==`, 44 "== (X:num->num->*) (Y:num->num->*) = \m n. ((X m n) = (Y m n))");; 45 46% ITL negation % 47 48new_definition 49 (`NOT`, 50 "NOT (X:num->num->bool) = \m n. ~(X m n)");; 51 52% ITL conjunction % 53 54new_infix_definition 55 (`AND`, 56 "AND (X:num->num->bool) (Y:num->num->bool) = 57 \m n. (X m n) /\ (Y m n)");; 58 59% The ITL next operator for formulas % 60 61new_definition 62 (`O`, 63 "O X = \m n. (n > m) /\ X (m+1) n");; 64 65% The ITL always operator % 66 67new_definition 68 (`BOX`, 69 "BOX X = \m n. !i. (m <= i) /\ (i <= n) ==> X i n");; 70 71% ITL chop operator (";" in Ben's notation - HOL won't allow ";" to be 72 made an infix) % 73 74new_infix_definition 75 (`THEN`, 76 "THEN X Y = \m n. ?i. (m<=i) /\ (i<=n) /\ (X m i) /\ (Y i n)");; 77 78% ITL existential quantification % 79 80new_binder_definition 81 (`EXISTS`, 82 "EXISTS (P:(num->num->*)->num->num->bool) = \m n. ?X. (P X m n)");; 83 84% The ITL validity predicate ("|=" in standard notation) % 85 86new_definition 87 (`VALID`, 88 "VALID (X:num->num->bool) = !m n. X m n");; 89 90 91% Now for some derived constants and operators % 92 93new_definition(`TRUE` , "TRUE = MK_STATIC T");; 94new_definition(`FALSE`, "FALSE = MK_STATIC F");; 95 96new_definition(`ZERO`, "ZERO = MK_STATIC 0");; 97new_definition(`ONE` , "ONE = MK_STATIC 1");; 98new_definition(`TWO` , "TWO = MK_STATIC 2");; 99 100new_infix_definition 101 (`OR`, 102 "OR X Y = NOT(NOT X AND NOT Y)");; 103 104new_infix_definition 105 (`IMPLIES`, 106 "IMPLIES X Y = NOT X OR Y");; 107 108new_definition 109 (`EMPTY`, 110 "EMPTY = NOT(O TRUE)");; 111 112new_definition 113 (`SKIP`, 114 "SKIP = O EMPTY");; 115 116new_infix_definition 117 (`GETS`, 118 "GETS (X:num->num->*) (Y:num->num->*) = 119 BOX(NOT EMPTY IMPLIES (NEXT X == Y))");; 120 121% ITL stability operator % 122 123new_definition 124 (`STABLE`, 125 "STABLE(X:num->num->*) = X GETS X");; 126 127new_definition 128 (`FIN`, 129 "FIN X = BOX(EMPTY IMPLIES X)");; 130 131hide_constant `S`;; 132 133new_infix_definition 134 (`-->`, 135 "--> (X:num->num->*) (Y:num->num->*) = 136 EXISTS S. IS_STATIC S AND (S == X) AND FIN(S == Y)");; 137 138% Some useful lemmas % 139 140let defs = 141 maptok 142 (definition `ITL`) 143 `IS_SIG MK_SIG IS_STATIC MK_STATIC NEXT == NOT AND O BOX THEN 144 EXISTS VALID TRUE FALSE ZERO ONE TWO OR IMPLIES EMPTY GETS STABLE`;; 145 146let TRUE_SEM = prove_thm(`TRUE_SEM` , "TRUE = \m n. T", REWRITE_TAC defs) 147and FALSE_SEM = prove_thm(`FALSE_SEM`, "FALSE = \m n. F", REWRITE_TAC defs) 148and ZERO_SEM = prove_thm(`ZERO_SEM` , "ZERO = \m n. 0", REWRITE_TAC defs) 149and ONE_SEM = prove_thm(`ONE_SEM` , "ONE = \m n. 1", REWRITE_TAC defs) 150and TWO_SEM = prove_thm(`TWO_SEM` , "TWO = \m n. 2", REWRITE_TAC defs);; 151 152let OR_SEM = 153 prove_thm 154 (`OR_SEM`, 155 "OR (X:num->num->bool) (Y:num->num->bool) = \m n. (X m n) \/ (Y m n)", 156 REWRITE_TAC defs 157 THEN CONV_TAC(DEPTH_CONV BETA_CONV) 158 THEN REWRITE_TAC[DE_MORGAN_THM]);; 159 160let OR_IMP_THM = 161 prove_thm 162 (`OR_IMP_THM`, 163 "(~t1 \/ t2) = (t1 ==> t2)", 164 BOOL_CASES_TAC "t1:bool" 165 THEN REWRITE_TAC[]);; 166 167let IMPLIES_SEM = 168 prove_thm 169 (`IMPLIES_SEM`, 170 "IMPLIES (X:num->num->bool) (Y:num->num->bool) = 171 \m n. (X m n) ==> (Y m n)", 172 REWRITE_TAC(OR_SEM.defs) 173 THEN CONV_TAC(DEPTH_CONV BETA_CONV) 174 THEN REWRITE_TAC[OR_IMP_THM]);; 175 176let EMPTY_SEM = 177 prove_thm 178 (`EMPTY_SEM`, 179 "EMPTY = \m n. n<=m", 180 REWRITE_TAC(TRUE_SEM.defs) 181 THEN CONV_TAC(DEPTH_CONV BETA_CONV) 182 THEN REWRITE_TAC[NOT_LESS;GREATER]);; 183 184let IMP_CONJ_THM = 185prove_thm 186 (`IMP_CONJ_THM`, 187 "(t1 ==> t2 ==> t3) = (t1 /\ t2 ==> t3)", 188 BOOL_CASES_TAC "t1:bool" 189 THEN REWRITE_TAC[]);; 190 191let LESS_AND_LESS_EQ_THM = 192 prove_thm 193 (`LESS_AND_LESS_EQ_THM`, 194 "m <= n /\ m < n = m < n", 195 EQ_TAC 196 THEN REPEAT STRIP_TAC 197 THEN ASM_REWRITE_TAC[LESS_OR_EQ]);; 198 199let GETS_SEM = 200 prove_thm 201 (`GETS_SEM`, 202 "GETS (X:num->num->*) (Y:num->num->*) = 203 \m n. !i. (m<=i) /\ (i<n) ==> (X(SUC i)n = Y i n)", 204 REWRITE_TAC(EMPTY_SEM.IMPLIES_SEM.defs) 205 THEN CONV_TAC(DEPTH_CONV BETA_CONV) 206 THEN REWRITE_TAC 207 [ADD1;IMP_CONJ_THM; 208 GREATER;LESS_AND_LESS_EQ_THM;SYM(SPEC_ALL CONJ_ASSOC)]);; 209 210% The following is not yet done 211 212let STABLE_SEM_LEMMA 213 prove_thm 214 (`STABLE_SEM_LEMMA`, 215 "STABLE (X:num->num->*) m n = !i. (m<=i) /\ (i<=n) ==> (X i n = X m n)", 216 REWRITE_TAC [definition `ITL` `STABLE`;GETS_SEM] 217 THEN CONV_TAC(DEPTH_CONV BETA_CONV) 218 THEN EQ_TAC 219 THEN DISCH_TAC 220 THEN INDUCT_TAC 221 THEN REWRITE_TAC[LESS_OR_EQ;NOT_LESS_0] 222 THEN REPEAT STRIP_TAC 223 THEN ASM_REWRITE_TAC[] 224 225Need to prove: 226 227 2285 subgoals 229"X(SUC(SUC i))n = X(SUC i)n" 230 [ "!i. m <= i /\ i <= n ==> (X i n = X m n)" ] 231 [ "m <= i /\ i < n ==> (X(SUC i)n = X i n)" ] 232 [ "m = SUC i" ] 233 [ "(SUC i) < n" ] 234 235"X(SUC(SUC i))n = X(SUC i)n" 236 [ "!i. m <= i /\ i <= n ==> (X i n = X m n)" ] 237 [ "m <= i /\ i < n ==> (X(SUC i)n = X i n)" ] 238 [ "m < (SUC i)" ] 239 [ "(SUC i) < n" ] 240 241"X(SUC 0)n = X 0 n" 242 [ "!i. m <= i /\ i <= n ==> (X i n = X m n)" ] 243 [ "m = 0" ] 244 [ "0 < n" ] 245 246"X n n = X m n" 247 [ "!i. m <= i /\ i < n ==> (X(SUC i)n = X i n)" ] 248 [ "m <= i /\ i <= n ==> (X i n = X m n)" ] 249 [ "m < (SUC i)" ] 250 [ "SUC i = n" ] 251 252"X(SUC i)n = X m n" 253 [ "!i. m <= i /\ i < n ==> (X(SUC i)n = X i n)" ] 254 [ "m <= i /\ i <= n ==> (X i n = X m n)" ] 255 [ "m < (SUC i)" ] 256 [ "(SUC i) < n" ] 257 258 259let STABLE_SEM 260 prove_thm 261 (`STABLE_SEM`, 262 "STABLE (X:num->num->*) = \m n. !i. (m<=i) /\ (i<=n) ==> (X i n = X m n)", 263 REWRITE_TAC [definition `ITL` `STABLE`;GETS_SEM] 264 265must prove: 266 267"(\m n. !i. m <= i /\ i < n ==> (X(SUC i)n = X i n)) = 268 (\m n. !i. m <= i /\ i <= n ==> (X i n = X m n))" 269% 270 271 272% Now we prove a theorem suggested by Ben % 273 274let SUB_REFL = 275 prove_thm 276 (`SUB_REFL`, 277 "!m. (m - m) = 0", 278 INDUCT_TAC 279 THEN REWRITE_TAC[SUB;LESS_SUC_REFL]);; 280 281let SUC_SUB_LEMMA = 282 prove_thm 283 (`SUC_SUB_LEMMA`, 284 "(n <= m) ==> ((SUC m) - n = (m - n) + 1)", 285 REWRITE_TAC[SUB;ADD1;SYM(SPEC_ALL NOT_LESS)] 286 THEN STRIP_TAC 287 THEN ASM_REWRITE_TAC[]);; 288 289% Some arithmetic operators % 290 291new_infix_definition 292 (`++`, 293 "++ X Y = \m n. (X m n) + (Y m n)");; 294 295new_infix_definition 296 (`**`, 297 "** X Y = \m n. (X m n) * (Y m n)");; 298 299let defs_sem = 300 [IMPLIES_SEM;GETS_SEM] @ 301 subtract defs (maptok (definition `ITL`) `IMPLIES GETS`) @ 302 maptok (definition `ITL`) `++ **`;; 303 304prove_thm 305 (`BENS_THM`, 306 "VALID (EXISTS X. (X == ZERO) AND (X GETS (X ++ ONE)))", 307 REWRITE_TAC defs_sem 308 THEN CONV_TAC(DEPTH_CONV BETA_CONV) 309 THEN REPEAT GEN_TAC 310 THEN EXISTS_TAC"\m' n.(m'-m)" 311 THEN CONV_TAC(DEPTH_CONV BETA_CONV) 312 THEN REPEAT STRIP_TAC 313 THEN IMP_RES_TAC LESS_EQ_TRANS 314 THEN IMP_RES_TAC SUC_SUB_LEMMA 315 THEN REWRITE_TAC[SUB_REFL]);; 316 317let g:goal = 318 ([], "VALID(((I == ZERO) AND 319 (J == ZERO) AND 320 (I GETS (I ++ ONE)) AND 321 (J GETS (J ++ TWO))) IMPLIES 322 BOX(J == (TWO ** I)))");; 323 324% Proof not yet done ... feel free to finish it! 325 326prove_thm 327 (`ROGERS_THM`, 328 "VALID(((I == ZERO) AND 329 (J == ZERO) AND 330 (I GETS (I ++ ONE)) AND 331 (J GETS (J ++ TWO))) IMPLIES 332 BOX(J == (TWO ** I)))", 333 REWRITE_TAC defs_sem 334 THEN CONV_TAC(DEPTH_CONV BETA_CONV) 335 THEN REPEAT GEN_TAC 336 THEN REPEAT STRIP_TAC 337 THEN INDUCT_TAC 338 339% 340