1246 |
1246 |
1247 |
1247 |
1248 (* NOT DONE YET *) |
1248 (* NOT DONE YET *) |
1249 |
1249 |
1250 section {* Sulzmann's Ordering of values *} |
1250 section {* Sulzmann's Ordering of values *} |
1251 |
|
1252 thm PMatch.intros |
|
1253 |
|
1254 (* |
|
1255 inductive ValOrd :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_ _" [100, 100, 100, 100] 100) |
|
1256 where |
|
1257 "\<lbrakk>s2 \<turnstile> v2 \<succ>r2 v2'; flat v1 = s1\<rbrakk> \<Longrightarrow> (s1 @ s2) \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
|
1258 | "\<lbrakk>s1 \<turnstile> v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
|
1259 | "\<lbrakk>flat v1 \<sqsubseteq> s; flat v2 \<sqsubseteq> flat v1\<rbrakk> \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
|
1260 | "\<lbrakk>flat v2 \<sqsubseteq> s; flat v1 \<sqsubset> flat v2\<rbrakk> \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Left v1)" |
|
1261 | "s \<turnstile> v2 \<succ>r2 v2' \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
|
1262 | "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
|
1263 | "s \<turnstile> Void \<succ>EMPTY Void" |
|
1264 | "(c#s) \<turnstile> (Char c) \<succ>(CHAR c) (Char c)" |
|
1265 *) |
|
1266 |
1251 |
1267 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
1252 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
1268 where |
1253 where |
1269 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
1254 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
1270 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
1255 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
1278 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])" |
1263 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])" |
1279 | "v1 \<succ>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))" |
1264 | "v1 \<succ>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))" |
1280 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))" |
1265 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))" |
1281 | "(Stars []) \<succ>(STAR r) (Stars [])" |
1266 | "(Stars []) \<succ>(STAR r) (Stars [])" |
1282 |
1267 |
|
1268 lemma ValOrd_refl: |
|
1269 assumes "\<turnstile> v : r" |
|
1270 shows "v \<succ>r v" |
|
1271 using assms |
|
1272 apply(induct) |
|
1273 apply(auto intro: ValOrd.intros) |
|
1274 done |
|
1275 |
|
1276 lemma ValOrd_total: |
|
1277 shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1" |
|
1278 apply(induct r arbitrary: v1 v2) |
|
1279 apply(auto) |
|
1280 apply(erule Prf.cases) |
|
1281 apply(simp_all)[7] |
|
1282 apply(erule Prf.cases) |
|
1283 apply(simp_all)[7] |
|
1284 apply(erule Prf.cases) |
|
1285 apply(simp_all)[7] |
|
1286 apply (metis ValOrd.intros(7)) |
|
1287 apply(erule Prf.cases) |
|
1288 apply(simp_all)[7] |
|
1289 apply(erule Prf.cases) |
|
1290 apply(simp_all)[7] |
|
1291 apply (metis ValOrd.intros(8)) |
|
1292 apply(erule Prf.cases) |
|
1293 apply(simp_all)[7] |
|
1294 apply(erule Prf.cases) |
|
1295 apply(simp_all)[7] |
|
1296 apply(clarify) |
|
1297 apply(case_tac "v1a = v1b") |
|
1298 apply(simp) |
|
1299 apply(rule ValOrd.intros(1)) |
|
1300 apply (metis ValOrd.intros(1)) |
|
1301 apply(rule ValOrd.intros(2)) |
|
1302 apply(auto)[2] |
|
1303 apply(erule contrapos_np) |
|
1304 apply(rule ValOrd.intros(2)) |
|
1305 apply(auto) |
|
1306 apply(erule Prf.cases) |
|
1307 apply(simp_all)[7] |
|
1308 apply(erule Prf.cases) |
|
1309 apply(simp_all)[7] |
|
1310 apply(clarify) |
|
1311 apply (metis ValOrd.intros(6)) |
|
1312 apply(rule ValOrd.intros) |
|
1313 apply(erule contrapos_np) |
|
1314 apply(rule ValOrd.intros) |
|
1315 apply (metis le_eq_less_or_eq neq_iff) |
|
1316 apply(erule Prf.cases) |
|
1317 apply(simp_all)[7] |
|
1318 apply(rule ValOrd.intros) |
|
1319 apply(erule contrapos_np) |
|
1320 apply(rule ValOrd.intros) |
|
1321 apply (metis le_eq_less_or_eq neq_iff) |
|
1322 apply(rule ValOrd.intros) |
|
1323 apply(erule contrapos_np) |
|
1324 apply(rule ValOrd.intros) |
|
1325 apply(metis) |
|
1326 apply(erule Prf.cases) |
|
1327 apply(simp_all)[7] |
|
1328 apply(erule Prf.cases) |
|
1329 apply(simp_all)[7] |
|
1330 apply(auto) |
|
1331 apply (metis ValOrd.intros(13)) |
|
1332 apply (metis ValOrd.intros(10) ValOrd.intros(9)) |
|
1333 apply(erule Prf.cases) |
|
1334 apply(simp_all)[7] |
|
1335 apply(auto) |
|
1336 apply (metis ValOrd.intros(10) ValOrd.intros(9)) |
|
1337 by (metis ValOrd.intros(11)) |
|
1338 |
|
1339 lemma ValOrd_anti: |
|
1340 shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2" |
|
1341 and "\<lbrakk>\<turnstile> Stars vs1 : r; \<turnstile> Stars vs2 : r; Stars vs1 \<succ>r Stars vs2; Stars vs2 \<succ>r Stars vs1\<rbrakk> \<Longrightarrow> vs1 = vs2" |
|
1342 apply(induct v1 and vs1 arbitrary: r v2 and r vs2 rule: val.inducts) |
|
1343 apply(erule Prf.cases) |
|
1344 apply(simp_all)[7] |
|
1345 apply(erule Prf.cases) |
|
1346 apply(simp_all)[7] |
|
1347 apply(erule Prf.cases) |
|
1348 apply(simp_all)[7] |
|
1349 apply(erule Prf.cases) |
|
1350 apply(simp_all)[7] |
|
1351 apply(erule Prf.cases) |
|
1352 apply(simp_all)[7] |
|
1353 apply(erule Prf.cases) |
|
1354 apply(simp_all)[7] |
|
1355 apply(erule ValOrd.cases) |
|
1356 apply(simp_all) |
|
1357 apply(erule ValOrd.cases) |
|
1358 apply(simp_all) |
|
1359 apply(erule ValOrd.cases) |
|
1360 apply(simp_all) |
|
1361 apply(erule Prf.cases) |
|
1362 apply(simp_all)[7] |
|
1363 apply(erule Prf.cases) |
|
1364 apply(simp_all)[7] |
|
1365 apply(erule ValOrd.cases) |
|
1366 apply(simp_all) |
|
1367 apply(erule ValOrd.cases) |
|
1368 apply(simp_all) |
|
1369 apply(erule ValOrd.cases) |
|
1370 apply(simp_all) |
|
1371 apply(erule ValOrd.cases) |
|
1372 apply(simp_all) |
|
1373 apply(erule Prf.cases) |
|
1374 apply(simp_all)[7] |
|
1375 apply(erule Prf.cases) |
|
1376 apply(simp_all)[7] |
|
1377 apply(erule ValOrd.cases) |
|
1378 apply(simp_all) |
|
1379 apply(erule ValOrd.cases) |
|
1380 apply(simp_all) |
|
1381 apply(erule ValOrd.cases) |
|
1382 apply(simp_all) |
|
1383 apply(erule ValOrd.cases) |
|
1384 apply(simp_all) |
|
1385 apply(erule Prf.cases) |
|
1386 apply(simp_all)[7] |
|
1387 apply(erule Prf.cases) |
|
1388 apply(simp_all)[7] |
|
1389 apply(erule ValOrd.cases) |
|
1390 apply(simp_all) |
|
1391 apply(erule ValOrd.cases) |
|
1392 apply(simp_all) |
|
1393 apply(erule Prf.cases) |
|
1394 apply(simp_all)[7] |
|
1395 apply(erule ValOrd.cases) |
|
1396 apply(simp_all) |
|
1397 apply(erule ValOrd.cases) |
|
1398 apply(simp_all) |
|
1399 apply(erule ValOrd.cases) |
|
1400 apply(simp_all) |
|
1401 apply(erule ValOrd.cases) |
|
1402 apply(simp_all) |
|
1403 apply(auto)[1] |
|
1404 prefer 2 |
|
1405 apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2) |
|
1406 prefer 2 |
|
1407 apply(auto)[1] |
|
1408 apply(rotate_tac 5) |
|
1409 apply(erule ValOrd.cases) |
|
1410 apply(simp_all) |
|
1411 apply (metis (no_types) Prf.intros(7) ValOrd.intros(11) not_Cons_self2) |
|
1412 apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2) |
|
1413 apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2) |
|
1414 apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2) |
|
1415 apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2) |
|
1416 apply (metis Prf.intros(7) ValOrd.intros(11) ValOrd_refl not_Cons_self2) |
|
1417 apply(erule ValOrd.cases) |
|
1418 apply(simp_all) |
|
1419 apply(erule ValOrd.cases) |
|
1420 apply(simp_all) |
|
1421 apply(erule ValOrd.cases) |
|
1422 apply(simp_all) |
|
1423 apply(erule ValOrd.cases) |
|
1424 apply(simp_all) |
|
1425 apply(erule ValOrd.cases) |
|
1426 apply(simp_all) |
|
1427 |
|
1428 |
|
1429 oops |
|
1430 |
|
1431 |
1283 (* |
1432 (* |
1284 |
1433 |
1285 lemma ValOrd_PMatch: |
1434 lemma ValOrd_PMatch: |
1286 assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 \<sqsubseteq> s" |
1435 assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 \<sqsubseteq> s" |
1287 shows "v1 \<succ>r v2" |
1436 shows "v1 \<succ>r v2" |