Skip to content

Commit 513a1da

Browse files
ordinarymathordinarymath
committed
Fix pull_wordsTheory
1 parent 4b7f7e0 commit 513a1da

File tree

1 file changed

+192
-137
lines changed

1 file changed

+192
-137
lines changed

‎icing/pull_wordsScript.sml

Lines changed: 192 additions & 137 deletions
Original file line numberDiff line numberDiff line change
@@ -1279,149 +1279,204 @@ val mem_tac =
12791279
>> first_x_assum $ qspec_then ‘n’ assume_tac >> gs[]
12801280
>> Cases_on ‘EL n refs2’ >> gs[ref_rel_def];
12811281

1282+
Triviality v_rel_do_eq':
1283+
do_eq a b = A ==>
1284+
v_rel a c /\ v_rel b d ==>
1285+
do_eq c d = A
1286+
Proof
1287+
rw[] >> imp_res_tac v_rel_do_eq >> fs[]
1288+
QED
1289+
1290+
Triviality v_rel_store_assign':
1291+
store_assign lnum a refs1 = A ==>
1292+
ref_rel a b /\ LIST_REL ref_rel refs1 refs2 ==>
1293+
?B. store_assign lnum b refs2 = B /\
1294+
OPTREL (LIST_REL ref_rel) A B
1295+
Proof
1296+
rw[] >>
1297+
imp_res_tac LIST_REL_LENGTH >> gs[] >>
1298+
imp_res_tac LIST_REL_EL_EQN >> gs[] >>
1299+
first_x_assum $ qspec_then `lnum` assume_tac >> gs[] >>
1300+
gs[store_assign_def] >>
1301+
Cases_on `lnum < LENGTH refs2` >> gs[] >>
1302+
IF_CASES_TAC >> fs[] >>
1303+
gs[oneline store_v_same_type_def,AllCasePreds()] >>
1304+
gs[oneline ref_rel_def,AllCasePreds()] >>
1305+
fs[LIST_REL_EL_EQN,EL_LUPDATE] >>
1306+
rw[] >>
1307+
fs[LIST_REL_EL_EQN]
1308+
QED
1309+
1310+
Triviality v_rel_store_lookup':
1311+
store_lookup lnum refs1 = A ==>
1312+
LIST_REL ref_rel refs1 refs2 ==>
1313+
?B. store_lookup lnum refs2 = B /\
1314+
OPTREL (ref_rel) A B
1315+
Proof
1316+
rw[] >>
1317+
imp_res_tac LIST_REL_LENGTH >> gs[] >>
1318+
imp_res_tac LIST_REL_EL_EQN >> gs[] >>
1319+
first_x_assum $ qspec_then `lnum` assume_tac >> gs[] >>
1320+
gs[store_lookup_def] >>
1321+
Cases_on `lnum < LENGTH refs2` >> gs[] >>
1322+
IF_CASES_TAC >> fs[]
1323+
QED
1324+
1325+
Triviality v_rel_fp_translate':
1326+
fp_translate a = A ==>
1327+
v_rel a b ==>
1328+
fp_translate b = A
1329+
Proof
1330+
rw[] >> imp_res_tac v_rel_fp_translate >> simp[]
1331+
QED
1332+
1333+
val RESTR_EVAL_TAC = computeLib.RESTR_EVAL_TAC;
1334+
val LENGTH_EQ_NUM_compute' = LIST_CONJ $ map (GEN_ALL o CONV_RULE (LHS_CONV SYM_CONV) o SPEC_ALL) (CONJUNCTS LENGTH_EQ_NUM_compute)
1335+
val trivial_tac = gs[AllCaseEqs(),UNCURRY_EQ,Once $ oneline do_app_def,
1336+
Excl "IF_NONE_EQUALS_OPTION"] >>
1337+
strip_tac >>
1338+
rveq >> gs[LENGTH_EQ_NUM_compute,LENGTH_EQ_NUM_compute'] >>
1339+
RESTR_EVAL_TAC[``store_assign``,``store_lookup``,
1340+
``store_alloc``,
1341+
``copy_array``,``ws_to_chars``,``chars_to_ws``,
1342+
``EXPLODE``,``call_FFI``];
1343+
12821344
Theorem do_app_thm:
12831345
∀op a1 a2 refs1 refs2 ffi.
12841346
LIST_REL v_rel a1 a2 ∧ LIST_REL ref_rel refs1 refs2 ⇒
12851347
OPTREL (λ((r1,f1),v1) ((r2,f2),v2).
12861348
f1 = f2 ∧ res1_rel v1 v2 ∧ LIST_REL ref_rel r1 r2)
12871349
(do_app (refs1,ffi) op a1) (do_app (refs2,ffi) op a2)
1288-
Proof
1289-
Cases_on ‘op’ >> gs[Once do_app_def, OPTREL_def]
1290-
>- trivial_tac
1291-
>- trivial_tac
1292-
>- trivial_tac
1293-
>- trivial_tac
1294-
>- (
1295-
rpt strip_tac
1296-
>> ‘LENGTH a1 = LENGTH a2’ by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[])
1297-
>> ntac 3 (TOP_CASE_TAC >> gs[do_app_def])
1298-
>> imp_res_tac $ GSYM v_rel_do_eq
1299-
>> TOP_CASE_TAC >> gs[Boolv_def]
1300-
>> COND_CASES_TAC >> gs[])
1301-
>- fp_tac
1302-
>- fp_tac
1303-
>- fp_tac
1304-
>- fp_tac
1305-
>- trivial_tac
1306-
>- trivial_tac
1307-
>- trivial_tac
1308-
>- trivial_tac
1309-
>- trivial_tac
1310-
>- trivial_tac
1311-
>- trivial_tac
1312-
>- (
1313-
rpt strip_tac
1314-
>> ‘LENGTH a1 = LENGTH a2’ by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[])
1315-
>> ‘LENGTH refs1 = LENGTH refs2’ by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[])
1316-
>> rpt (TOP_CASE_TAC >> gs[])
1317-
>> gs[do_app_def]
1318-
>> gs[store_assign_def, store_v_same_type_def]
1319-
>> Cases_on ‘n < LENGTH refs2’ >> gs[]
1320-
>> Cases_on ‘EL n refs1’ >> gs[]
1321-
>> imp_res_tac LIST_REL_EL_EQN
1322-
>> first_x_assum $ qspec_then ‘n’ assume_tac
1323-
>> Cases_on ‘EL n refs2’ >> rveq >> gs[ref_rel_def]
1324-
>> irule EVERY2_LUPDATE_same
1325-
>> gs[ref_rel_def])
1326-
>- mem_tac
1327-
>- mem_tac
1328-
>- mem_tac
1329-
>- mem_tac
1330-
>- mem_tac
1331-
>- (
1332-
mem_tac
1333-
>> rveq >> irule EVERY2_LUPDATE_same >> gs[ref_rel_def])
1334-
>- trivial_tac
1335-
>- trivial_tac
1336-
>- mem_tac
1337-
>- (
1338-
mem_tac
1339-
>> rveq >> irule EVERY2_LUPDATE_same >> gs[ref_rel_def])
1340-
>- mem_tac
1341-
>- (
1342-
mem_tac
1343-
>> imp_res_tac LIST_REL_EL_EQN
1344-
>> first_x_assum $ qspec_then ‘n'’ assume_tac >> gs[]
1345-
>> Cases_on ‘EL n' refs2’ >> gs[ref_rel_def]
1346-
>> rveq >> irule EVERY2_LUPDATE_same >> gs[ref_rel_def])
1347-
>- trivial_tac
1348-
>- trivial_tac
1349-
>- trivial_tac
1350-
>- (
1351-
mem_tac
1352-
>> imp_res_tac $ GSYM v_rel_v_to_char_list >> gs[])
1353-
>- mem_tac
1354-
>- mem_tac
1355-
>- mem_tac
1356-
>- (
1357-
mem_tac
1358-
>> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def]
1359-
>> imp_res_tac $ GSYM v_rel_vs_to_string >> gs[])
1360-
>- (
1361-
mem_tac
1362-
>> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def])
1363-
>- (
1364-
mem_tac
1365-
>> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def])
1366-
>- (
1367-
mem_tac
1368-
>> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def])
1369-
>- (
1370-
mem_tac
1371-
>> rewrite_tac $ single LIST_REL_REPLICATE_same
1372-
>> strip_tac >> gs[])
1373-
>- mem_tac
1374-
>- mem_tac
1375-
>- (
1376-
mem_tac
1377-
>> TOP_CASE_TAC >> gs[]
1378-
>> ‘LENGTH l = LENGTH l'’
1379-
by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[])
1380-
>> gs $ single LIST_REL_EL_EQN)
1381-
>- ( mem_tac >> gs $ single LIST_REL_EL_EQN)
1382-
>- (
1383-
mem_tac
1384-
>> ‘LIST_REL v_rel l l'’ by (gs $ single LIST_REL_EL_EQN)
1385-
>> ‘LENGTH l = LENGTH l'’
1386-
by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[])
1387-
>> TOP_CASE_TAC >> gs[store_v_same_type_def]
1388-
>> rveq >> irule EVERY2_LUPDATE_same >> gs[]
1389-
>> irule EVERY2_LUPDATE_same >> gs[])
1390-
>- (
1391-
mem_tac >> TOP_CASE_TAC >> gs[]
1392-
>> ‘LENGTH l = LENGTH l'’
1393-
by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[])
1394-
>> gs[LIST_REL_EL_EQN])
1395-
>- (
1396-
mem_tac >> TOP_CASE_TAC >> gs[]
1397-
>> ‘LENGTH l = LENGTH l'’
1398-
by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[])
1399-
>> gs[LIST_REL_EL_EQN]
1400-
>> COND_CASES_TAC >> gs[store_v_same_type_def]
1401-
>> Cases_on ‘i < 0’ >> gs[] >> rveq
1402-
>> gs[LENGTH_LUPDATE]
1403-
>> rpt strip_tac >> gs[LIST_REL_EL_EQN]
1404-
>> res_tac >> rewrite_tac [EL_LUPDATE]
1405-
>> COND_CASES_TAC >> gs[]
1406-
>> irule EVERY2_LUPDATE_same >> gs[]
1407-
>> res_tac >> pop_assum $ mp_tac
1408-
>> asm_rewrite_tac [] >> gs[ref_rel_def])
1409-
>- mem_tac
1410-
>- (
1411-
mem_tac
1412-
>> Cases_on ‘i < 0’ >> gs[]
1413-
>> rveq >> gs[LIST_REL_EL_EQN]
1414-
>> rpt strip_tac
1415-
>> res_tac >> rewrite_tac [EL_LUPDATE]
1416-
>> COND_CASES_TAC >> gs[])
1350+
Proof[exclude_simps = IF_NONE_EQUALS_OPTION]
1351+
rpt strip_tac >> imp_res_tac LIST_REL_LENGTH >>
1352+
Cases_on `(do_app (refs1,ffi) op a1)` >> gs[OPTREL_SOME] >>
1353+
pop_assum mp_tac
1354+
(*NONE Case*)
1355+
>- (
1356+
trivial_tac
1357+
>>~ [`do_eq`]
1358+
>- (
1359+
dxrule_then (drule_all_then SUBST_ALL_TAC) v_rel_do_eq' >>
1360+
EVAL_TAC)
1361+
>>~-([`fp_translate`],
1362+
rpt $ dxrule_then (drule_all_then SUBST_ALL_TAC) v_rel_fp_translate' >>
1363+
EVAL_TAC)
1364+
>> rpt (dxrule_then (drule_all_then strip_assume_tac)
1365+
v_rel_store_lookup' >>
1366+
gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(),
1367+
Excl "IF_NONE_EQUALS_OPTION"])
1368+
>> rpt (dxrule v_rel_store_assign' >>
1369+
gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(),
1370+
Excl "IF_NONE_EQUALS_OPTION"])
1371+
>- (imp_res_tac $ GSYM v_rel_v_to_char_list >> gs[])
1372+
>- (imp_res_tac v_rel_v_to_list >> gs[])
1373+
>- (
1374+
imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME] >>
1375+
imp_res_tac v_rel_vs_to_string >> gs[])
1376+
>- (imp_res_tac v_rel_v_to_list >> gs[])
1377+
>- (
1378+
imp_res_tac LIST_REL_LENGTH >> fs[] >>
1379+
qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >>
1380+
disch_then (drule_at (Pos (el 2))) >>
1381+
simp[oneline ref_rel_def,AllCasePreds()] >>
1382+
disch_then (qspec_then `VARRAY` mp_tac) >>
1383+
simp[Abbr `VARRAY`] >>
1384+
impl_tac >- (irule EVERY2_LUPDATE_same >> fs[]) >>
1385+
fs[])
1386+
>- (imp_res_tac LIST_REL_LENGTH >> fs[])
1387+
>- (imp_res_tac LIST_REL_LENGTH >> fs[])
1388+
>- (
1389+
imp_res_tac LIST_REL_LENGTH >> fs[] >>
1390+
qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >>
1391+
disch_then (drule_at (Pos (el 2))) >>
1392+
simp[oneline ref_rel_def,AllCasePreds()] >>
1393+
disch_then (qspec_then `VARRAY` mp_tac) >>
1394+
simp[Abbr `VARRAY`] >>
1395+
impl_tac >- (irule EVERY2_LUPDATE_same >> fs[]) >>
1396+
fs[])
1397+
>- (imp_res_tac v_rel_v_to_list >> gs[])
1398+
>- (
1399+
imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME] >>
1400+
imp_res_tac v_rel_vs_to_string >> gs[]))
14171401
>- (
1418-
mem_tac
1419-
>> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def]
1420-
>> irule v_rel_list_to_v_app >> gs[])
1421-
>- trivial_tac
1422-
>- (mem_tac >> rveq >> irule EVERY2_LUPDATE_same >> gs[])
1423-
>- (mem_tac >> rveq >> irule EVERY2_LUPDATE_same >> gs[])
1424-
>> fp_tac >> simp[nat_to_v_def]
1402+
trivial_tac >> fs[]
1403+
>>~ [`do_eq`]
1404+
>- (
1405+
imp_res_tac v_rel_do_eq >> fs[]
1406+
>> fs[COND_RAND])
1407+
>>~-([`fp_translate`],
1408+
rpt $ dxrule_then (drule_all_then SUBST_ALL_TAC) v_rel_fp_translate' >>
1409+
EVAL_TAC >>
1410+
fs[])
1411+
>>~-([`store_alloc`],
1412+
gvs[store_alloc_def] >>
1413+
fs[LIST_REL_REPLICATE_same])
1414+
>> rpt (dxrule_then (drule_all_then strip_assume_tac)
1415+
v_rel_store_lookup' >>
1416+
gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(),
1417+
Excl "IF_NONE_EQUALS_OPTION"])
1418+
>> rpt (dxrule_then (drule_at_then (Pos (el 2)) mp_tac)
1419+
v_rel_store_assign' >>
1420+
gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(),
1421+
Excl "IF_NONE_EQUALS_OPTION"])
1422+
>>~ [`store_assign`]
1423+
>- (
1424+
qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >>
1425+
disch_then (qspec_then `VARRAY` mp_tac) >>
1426+
simp[Abbr `VARRAY`] >>
1427+
strip_tac >> fs[])
1428+
>- (fs[PULL_EXISTS])
1429+
>- (fs[PULL_EXISTS])
1430+
>- (fs[PULL_EXISTS])
1431+
>- (imp_res_tac LIST_REL_LENGTH >> fs[])
1432+
>- (
1433+
imp_res_tac LIST_REL_LENGTH >> fs[] >>
1434+
qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >>
1435+
disch_then (qspec_then `VARRAY` mp_tac) >>
1436+
simp[Abbr `VARRAY`] >>
1437+
impl_tac >- (irule EVERY2_LUPDATE_same >> fs[]) >>
1438+
strip_tac >> fs[])
1439+
>- (
1440+
imp_res_tac LIST_REL_LENGTH >> fs[] >>
1441+
qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >>
1442+
disch_then (qspec_then `VARRAY` mp_tac) >>
1443+
simp[Abbr `VARRAY`] >>
1444+
impl_tac >- (irule EVERY2_LUPDATE_same >> fs[]) >>
1445+
strip_tac >> fs[])
1446+
>- (fs[PULL_EXISTS])
1447+
>- (fs[PULL_EXISTS])
1448+
>>~ [`v_to_char_list`]
1449+
>- (imp_res_tac $ GSYM v_rel_v_to_char_list >> gs[])
1450+
>>~ [`v_to_list`,`vs_to_string`]
1451+
>- (
1452+
imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME] >>
1453+
imp_res_tac v_rel_vs_to_string >> gs[])
1454+
>>~ [`v_to_list`,`list_to_v`]
1455+
>- (imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME]
1456+
>> irule v_rel_list_to_v >> fs[]
1457+
>> irule LIST_REL_APPEND_suff >> fs[])
1458+
>>~ [`v_to_list`]
1459+
>- (imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME])
1460+
>>~ [`list_to_v`]
1461+
>- fs[v_rel_list_to_v_char]
1462+
(*TODO figure out a way to automate this*)
1463+
>- (Cases_on `n2 = 0` >> gvs[])
1464+
>- (fs[COND_RAND])
1465+
>- (fs[COND_RAND])
1466+
>- (TOP_CASE_TAC >> fs[])
1467+
>- (TOP_CASE_TAC >> fs[])
1468+
>- (TOP_CASE_TAC >> fs[])
1469+
>- (TOP_CASE_TAC >> fs[])
1470+
>- (imp_res_tac LIST_REL_LENGTH >> fs[])
1471+
>- (imp_res_tac LIST_REL_LENGTH >> fs[] >>
1472+
fs[LIST_REL_EL_EQN])
1473+
>- (imp_res_tac LIST_REL_LENGTH >> fs[])
1474+
>- (imp_res_tac LIST_REL_LENGTH >> fs[])
1475+
>- (imp_res_tac LIST_REL_LENGTH >> fs[] >>
1476+
fs[LIST_REL_EL_EQN])
1477+
>- (imp_res_tac LIST_REL_LENGTH >> fs[])
1478+
>- (imp_res_tac LIST_REL_LENGTH >> fs[] >>
1479+
fs[LIST_REL_EL_EQN]))
14251480
QED
14261481

14271482

@@ -1942,7 +1997,7 @@ Theorem ALL_DISTINCT_MAP:
19421997
Proof
19431998
Induct_on ‘funs’ >> gs[]
19441999
>> rpt strip_tac >> Cases_on ‘h’ >> gs[]
1945-
>> Cases_on ‘r’ >> gs[MEM_MAP] >> EQ_TAC >> rpt strip_tac
2000+
>> gs[MEM_MAP] >> EQ_TAC >> rpt strip_tac
19462001
>- (rveq >> Cases_on ‘y'’ >> gs[]
19472002
>> Cases_on ‘r’ >> gs[])
19482003
>- (gs[])

0 commit comments

Comments
 (0)