Skip to content

Commit 227f023

Browse files
hrutvikhrutvik
committed
Update for changes in CakeML
1 parent c24db64 commit 227f023

File tree

1 file changed

+65
-68
lines changed

1 file changed

+65
-68
lines changed

‎compiler/backend/passes/proofs/state_to_cakeProofScript.sml‎

Lines changed: 65 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -124,42 +124,40 @@ QED
124124

125125
Theorem cstep_n_to_dstep_n:
126126
∀n env dst eve k benv locs p dk cres.
127-
cstep_n n (Estep (env,dst.refs,dst.fp_state,eve,k)) = cres ∧ cres ≠ Edone ⇒
128-
∃fp'.
127+
cstep_n n (Estep (env,dst.refs,eve,k)) = cres ∧ cres ≠ Edone ⇒
129128
step_n benv n (Dstep dst (ExpVal env eve k locs p) dk) =
130129
case cres of
131-
| Estep (env',refs',fp',eve',k') =>
132-
Dstep (dst with <| refs := refs'; fp_state := fp' |>)
130+
| Estep (env',refs',eve',k') =>
131+
Dstep (dst with <| refs := refs' |>)
133132
(ExpVal env' eve' k' locs p) dk
134-
| Etype_error fp' => Dtype_error fp'
133+
| Etype_error => Dtype_error
135134
| Effi ch ws1 ws2 n env' refs' k' =>
136-
Dffi (dst with <| refs := refs'; fp_state := fp' |>)
135+
Dffi (dst with <| refs := refs' |>)
137136
(ch,ws1,ws2,n,env',k') locs p dk
138137
Proof
139138
Induct >> rw[]
140139
>- simp[itree_semanticsTheory.step_n_def, dstate_component_equality] >>
141140
gvs[cstep_n_alt] >>
142-
`cstep_n n (Estep (env,dst.refs,dst.fp_state,eve,k)) ≠ Edone` by gvs[AllCaseEqs()] >>
141+
`cstep_n n (Estep (env,dst.refs,eve,k)) ≠ Edone` by gvs[AllCaseEqs()] >>
143142
last_x_assum drule >>
144143
disch_then $ qspecl_then [`benv`,`locs`,`p`,`dk`] assume_tac >> gvs[] >>
145144
simp[itree_semanticsPropsTheory.step_n_alt_def] >>
146-
reverse $ Cases_on `cstep_n n (Estep (env,dst.refs,dst.fp_state,eve,k))` >> gvs[]
147-
>- irule_at Any EQ_REFL >>
145+
Cases_on `cstep_n n (Estep (env,dst.refs,eve,k))` >> gvs[] >>
148146
rename1 `estep st` >> PairCases_on `st` >> gvs[] >> gvs[estep_to_Edone] >>
149-
Cases_on `st3` >> gvs[] >> Cases_on `st4` >> gvs[] >> simp[dstep_def] >>
147+
Cases_on `st2` >> gvs[] >> Cases_on `st3` >> gvs[] >> simp[dstep_def] >>
150148
TOP_CASE_TAC >> gvs[estep_to_Edone] >> irule_at Any EQ_REFL
151149
QED
152150

153151
Triviality dstep_ExpVal_Exp:
154152
dstep benv st (ExpVal env (Exp e) k locs p) dk =
155-
case estep (env,st.refs,st.fp_state,Exp e,k) of
156-
| Estep (env',refs',fp',ev',ec') =>
157-
dreturn (st with <| refs := refs'; fp_state := fp' |>)
153+
case estep (env,st.refs,Exp e,k) of
154+
| Estep (env',refs',ev',ec') =>
155+
dreturn (st with <| refs := refs' |>)
158156
dk (ExpVal env' ev' ec' locs p)
159157
| Effi s ws1 ws2 n env'' refs'' ec'' =>
160158
Dffi (st with refs := refs'') (s,ws1,ws2,n,env'',ec'') locs p dk
161159
| Edone => Ddone
162-
| Etype_error fp => Dtype_error fp
160+
| Etype_error => Dtype_error
163161
Proof
164162
Cases_on `k` >> simp[dstep_def]
165163
QED
@@ -617,13 +615,13 @@ QED
617615
Inductive step_rel:
618616
(compile_rel cnenv se ce ∧ cont_rel cnenv sk ck ∧
619617
env_rel cnenv senv cenv ∧ state_rel cnenv sst cst ∧ env_ok cenv
620-
⇒ step_rel (Exp senv se, SOME sst, sk) (Estep (cenv, cst, fp, Exp ce, ck))) ∧
618+
⇒ step_rel (Exp senv se, SOME sst, sk) (Estep (cenv, cst, Exp ce, ck))) ∧
621619

622620
(v_rel cnenv sv cv ∧ cont_rel cnenv sk ck ∧ state_rel cnenv sst cst
623-
⇒ step_rel (Val sv, SOME sst, sk) (Estep (cenv, cst, fp, Val cv, ck))) ∧
621+
⇒ step_rel (Val sv, SOME sst, sk) (Estep (cenv, cst, Val cv, ck))) ∧
624622

625623
(v_rel cnenv sv cv ∧ cont_rel cnenv sk ck ∧ state_rel cnenv sst cst
626-
⇒ step_rel (Exn sv, SOME sst, sk) (Estep (cenv, cst, fp, Exn cv, ck))) ∧
624+
⇒ step_rel (Exn sv, SOME sst, sk) (Estep (cenv, cst, Exn cv, ck))) ∧
627625

628626
(cont_rel cnenv sk ck ∧ state_rel cnenv sst cst ∧ env_ok cenv ∧
629627
ws1 = MAP (λc. n2w $ ORD c) (EXPLODE conf) ∧
@@ -633,15 +631,15 @@ Inductive step_rel:
633631
End
634632

635633
Inductive dstep_rel:
636-
(step_rel (seve, SOME sst, sk) (Estep (cenv,dst.refs,dst.fp_state,ceve,ck)) ∧
634+
(step_rel (seve, SOME sst, sk) (Estep (cenv,dst.refs,ceve,ck)) ∧
637635
¬is_halt (seve, SOME sst, sk)
638636
⇒ dstep_rel (seve, SOME sst, sk)
639637
(Dstep dst (ExpVal cenv ceve ck locs (Pvar "prog")) [CdlocalG lenv genv (final_gc flag)])) ∧
640638

641639
dstep_rel (Val sv, SOME sst, []) Ddone ∧
642640

643641
(v_rel cnenv sv cv ⇒
644-
dstep_rel (Exn sv, SOME sst, []) (Draise (fp,cv))) ∧
642+
dstep_rel (Exn sv, SOME sst, []) (Draise cv)) ∧
645643

646644
(step_rel (Action ch conf, SOME sst, sk)
647645
(Effi (ExtCall ch) ws1 ws2 0 cenv' dst.refs ck)
@@ -714,28 +712,27 @@ Definition get_ffi_args_def[simp]:
714712
End
715713

716714
Theorem capplication_thm:
717-
∀op env s fp vs c.
718-
getOpClass op ≠ Icing ∧ getOpClass op ≠ Reals ⇒
719-
application op env s fp vs c =
715+
∀op env s vs c.
716+
application op env s vs c =
720717
if op = Opapp then
721718
case do_opapp vs of
722-
| NONE => Etype_error (fix_fp_state c fp)
723-
| SOME (env,e) => Estep (env,s,fp,Exp e,c)
719+
| NONE => Etype_error
720+
| SOME (env,e) => Estep (env,s,Exp e,c)
724721
else case get_ffi_ch op of
725722
| SOME n => (
726723
case get_ffi_args vs of
727724
| SOME (conf, lnum) => (
728725
case store_lookup lnum s of
729726
SOME (W8array ws) =>
730-
if n = "" then Estep (env, s, fp, Val $ Conv NONE [], c)
727+
if n = "" then Estep (env, s, Val $ Conv NONE [], c)
731728
else Effi (ExtCall n) (MAP (λc. n2w $ ORD c) (EXPLODE conf)) ws lnum env s c
732-
| _ => Etype_error (fix_fp_state c fp))
733-
| NONE => Etype_error (fix_fp_state c fp))
729+
| _ => Etype_error)
730+
| NONE => Etype_error)
734731
| NONE => (
735732
case do_app s op vs of
736-
| NONE => Etype_error (fix_fp_state c fp)
737-
| SOME (v1,Rval v') => return env v1 fp v' c
738-
| SOME (v1,Rraise v) => Estep (env,v1,fp,Exn v,c))
733+
| NONE => Etype_error
734+
| SOME (v1,Rval v') => return env v1 v' c
735+
| SOME (v1,Rraise v) => Estep (env,v1,Exn v,c))
739736
Proof
740737
rw[application_thm] >> simp[] >> gvs[]
741738
>- gvs[AllCaseEqs()]
@@ -809,9 +806,9 @@ Proof
809806
QED
810807

811808
Triviality cstep_Exn_over_list_to_cont:
812-
∀es cenv cst fp cv cenv' env ck'.
813-
cstep_n (LENGTH es) (Estep (cenv,cst,fp,Exn cv, (list_to_cont env es ++ ck'))) =
814-
(Estep (cenv,cst,fp,Exn cv,ck'))
809+
∀es cenv cst cv cenv' env ck'.
810+
cstep_n (LENGTH es) (Estep (cenv,cst,Exn cv, (list_to_cont env es ++ ck'))) =
811+
(Estep (cenv,cst,Exn cv,ck'))
815812
Proof
816813
Induct >> rw[list_to_cont_def] >> simp[cstep] >> CASE_TAC >> gvs[]
817814
QED
@@ -823,9 +820,9 @@ Proof
823820
QED
824821

825822
Theorem cstep_list_to_exp:
826-
∀ces cnenv cenv cst fp ck. cnenv_rel cnenv cenv.c ⇒
827-
∃n. cstep_n n (Estep (cenv,cst,fp,Exp (list_to_exp ces), ck)) =
828-
Estep (cenv,cst,fp,Val (Conv (SOME (TypeStamp "[]" 1)) []),
823+
∀ces cnenv cenv cst ck. cnenv_rel cnenv cenv.c ⇒
824+
∃n. cstep_n n (Estep (cenv,cst,Exp (list_to_exp ces), ck)) =
825+
Estep (cenv,cst,Val (Conv (SOME (TypeStamp "[]" 1)) []),
829826
list_to_cont cenv (REVERSE ces) ++ ck)
830827
Proof
831828
Induct >> rw[] >> gvs[env_ok_def] >> simp[list_to_exp_def, list_to_cont_def]
@@ -841,7 +838,7 @@ Proof
841838
simp[] >>
842839
last_x_assum $ drule_all_then assume_tac >>
843840
pop_assum $ qspecl_then
844-
[`cst`,`fp`,`(Ccon (SOME (Short "::")) [] [h],cenv)::ck`] assume_tac >> gvs[] >>
841+
[`cst`,`(Ccon (SOME (Short "::")) [] [h],cenv)::ck`] assume_tac >> gvs[] >>
845842
qrefine `m + n` >> simp[cstep_n_add] >>
846843
qexists0 >> simp[list_to_cont_APPEND, list_to_cont_def]
847844
QED
@@ -1208,11 +1205,11 @@ Theorem step1_rel_Case_match:
12081205
ALOOKUP cnenv cn = SOME (tyid, LENGTH pvs) ∧
12091206
LENGTH pvs = LENGTH cvs ∧
12101207
cnenv_rel cnenv cenv.c
1211-
⇒ ∃n cce. cstep_n n (Estep (cenv,cst,fp,Val (Conv (SOME tyid) cvs),
1208+
⇒ ∃n cce. cstep_n n (Estep (cenv,cst,Val (Conv (SOME tyid) cvs),
12121209
(Cmat (ccss ++ any) bind_exn_v,cenv)::ck)) =
12131210
Estep (cenv with v := nsAppend
12141211
(alist_to_ns (REVERSE (ZIP (MAP var_prefix pvs, cvs)))) cenv.v,
1215-
cst,fp,Exp cce,ck) ∧
1212+
cst,Exp cce,ck) ∧
12161213
compile_rel cnenv sce cce
12171214
Proof
12181215
Induct_on `LIST_REL` >> rw[] >> ntac 2 (pairarg_tac >> gvs[]) >>
@@ -1237,9 +1234,9 @@ Theorem step1_rel_Case_underscore:
12371234
ALOOKUP scss cn = NONE ∧
12381235
ALOOKUP cnenv cn = SOME (tyid, LENGTH cvs) ∧
12391236
cnenv_rel cnenv cenv.c
1240-
⇒ ∃n. cstep_n n (Estep (cenv,cst,fp,Val (Conv (SOME tyid) cvs),
1237+
⇒ ∃n. cstep_n n (Estep (cenv,cst,Val (Conv (SOME tyid) cvs),
12411238
(Cmat (ccss ++ [Pany,cuse]) bind_exn_v,cenv)::ck)) =
1242-
Estep (cenv,cst,fp,Exp cuse,ck)
1239+
Estep (cenv,cst,Exp cuse,ck)
12431240
Proof
12441241
Induct_on `LIST_REL` >> rw[]
12451242
>- (
@@ -1307,18 +1304,18 @@ QED
13071304
(***** primitive operations *****)
13081305

13091306
Theorem strle_lemma:
1310-
∀n s1 s2 len1 len2 env env' st fp c.
1307+
∀n s1 s2 len1 len2 env env' st c.
13111308
nsLookup env.v (Short "strle") = SOME $ strle_v env' ∧
13121309
nsLookup env'.c (Short $ "True") = SOME (0n, TypeStamp "True" bool_type_num) ∧
13131310
nsLookup env'.c (Short $ "False") = SOME (0n, TypeStamp "False" bool_type_num) ∧
13141311
len1 = LENGTH s1 ∧ len2 = LENGTH s2
1315-
⇒ ∃k env'. cstep_n k (Estep (env,st,fp, Exp (var "strle"),
1312+
⇒ ∃k env'. cstep_n k (Estep (env,st,Exp (var "strle"),
13161313
(Capp Opapp [Litv (IntLit &n)] [], env)::
13171314
(Capp Opapp [Litv (StrLit s1)] [], env)::
13181315
(Capp Opapp [Litv (StrLit s2)] [], env)::
13191316
(Capp Opapp [Litv (IntLit &len1)] [], env)::
13201317
(Capp Opapp [Litv (IntLit &len2)] [], env)::c)) =
1321-
Estep (env',st,fp,Val (Boolv (DROP n s1 ≤ DROP n s2)),c)
1318+
Estep (env',st,Val (Boolv (DROP n s1 ≤ DROP n s2)),c)
13221319
Proof
13231320
recInduct strle_ind >> rw[] >>
13241321
ntac 2 (qrefine `SUC k` >> simp[cstep]) >>
@@ -1363,30 +1360,30 @@ Proof
13631360
QED
13641361

13651362
Theorem strle:
1366-
∀s1 s2 env env' st fp c.
1363+
∀s1 s2 env env' st c.
13671364
nsLookup env.v (Short "strle") = SOME $ strle_v env' ∧
13681365
nsLookup env'.c (Short $ "True") = SOME (0n, TypeStamp "True" bool_type_num) ∧
13691366
nsLookup env'.c (Short $ "False") = SOME (0n, TypeStamp "False" bool_type_num)
1370-
⇒ ∃k env'. cstep_n k (Estep (env,st,fp, Exp (var "strle"),
1367+
⇒ ∃k env'. cstep_n k (Estep (env,st,Exp (var "strle"),
13711368
(Capp Opapp [Litv (IntLit 0)] [], env)::
13721369
(Capp Opapp [Litv (StrLit s1)] [], env)::
13731370
(Capp Opapp [Litv (StrLit s2)] [], env)::
13741371
(Capp Opapp [Litv (IntLit &LENGTH s1)] [], env)::
13751372
(Capp Opapp [Litv (IntLit &LENGTH s2)] [], env)::c)) =
1376-
Estep (env',st,fp,Val (Boolv (s1 ≤ s2)),c)
1373+
Estep (env',st,Val (Boolv (s1 ≤ s2)),c)
13771374
Proof
13781375
rw[] >> drule_all $ SRULE [] strle_lemma >>
13791376
disch_then $ qspec_then `0` mp_tac >> simp[]
13801377
QED
13811378

13821379
Theorem char_list:
1383-
∀l env env' st fp c.
1380+
∀l env env' st c.
13841381
nsLookup env.v (Short "char_list") = SOME $ char_list_v env' ∧
13851382
nsLookup env'.c (Short $ "[]") = SOME (0n, TypeStamp "[]" list_type_num) ∧
13861383
nsLookup env'.c (Short $ "::") = SOME (2n, TypeStamp "::" list_type_num)
1387-
⇒ ∃k env'. cstep_n k (Estep (env,st,fp, Exp (var "char_list"),
1384+
⇒ ∃k env'. cstep_n k (Estep (env,st,Exp (var "char_list"),
13881385
(Capp Opapp [list_to_v (MAP (Litv o IntLit) l)] [], env)::c)) =
1389-
Estep (env',st,fp,
1386+
Estep (env',st,
13901387
Val (list_to_v (MAP (λi. Litv $ Char $ CHR $ Num $ i % 256) l)),c)
13911388
Proof
13921389
Induct >> rw[list_to_v_def]
@@ -1412,8 +1409,8 @@ Proof
14121409
ntac 1 (qrefine `SUC k` >> simp[cstep]) >>
14131410
simp[do_con_check_def, build_conv_def] >>
14141411
ntac 3 (qrefine `SUC k` >> simp[cstep]) >>
1415-
qmatch_goalsub_abbrev_tac `(env' with v := new_env, _, _, _, _::c')` >>
1416-
last_x_assum $ qspecl_then [`env' with v := new_env`,`env'`,`st`,`fp`,`c'`] mp_tac >>
1412+
qmatch_goalsub_abbrev_tac `(env' with v := new_env, _, _, _::c')` >>
1413+
last_x_assum $ qspecl_then [`env' with v := new_env`,`env'`,`st`,`c'`] mp_tac >>
14171414
simp[] >> impl_tac >- (unabbrev_all_tac >> simp[char_list_v_def]) >>
14181415
strip_tac >> gvs[] >> qrefine `n + k` >> simp[cstep_n_add] >>
14191416
pop_assum kall_tac >> unabbrev_all_tac >>
@@ -1470,7 +1467,7 @@ Proof
14701467
qexists0 >> simp[step_rel_cases, SF SFY_ss]
14711468
) >>
14721469
gvs[SWAP_REVERSE_SYM, LIST_REL_SPLIT1, REVERSE_APPEND] >>
1473-
qspecl_then [`ys1 ++ [y]`,`cnenv`,`cenv`,`cst`,`fp`,`(Capp Strcat [] [],cenv)::ck`]
1470+
qspecl_then [`ys1 ++ [y]`,`cnenv`,`cenv`,`cst`,`(Capp Strcat [] [],cenv)::ck`]
14741471
assume_tac cstep_list_to_exp >> gvs[] >>
14751472
qrefine `m + n` >> simp[cstep_n_add, REVERSE_APPEND] >>
14761473
qrefine `SUC m` >> simp[cstep, list_to_cont_def] >>
@@ -1489,16 +1486,16 @@ Proof
14891486
drule $ cj 3 env_ok_imps >> strip_tac >> gvs[] >>
14901487
drule_all char_list >>
14911488
disch_then $ qspecl_then
1492-
[`[]`,`cst`,`fp`,`(Capp Implode [] [], cenv)::ck`] assume_tac >> gvs[] >>
1489+
[`[]`,`cst`,`(Capp Implode [] [], cenv)::ck`] assume_tac >> gvs[] >>
14931490
qrefine `n + k` >> simp[cstep_n_add] >> gvs[list_to_v_def, list_type_num_def] >>
14941491
ntac 1 (qrefine `SUC n` >> simp[cstep]) >>
14951492
simp[do_app_def, v_to_char_list_def, list_type_num_def] >>
14961493
qexists0 >> simp[step_rel_cases, SF SFY_ss]
14971494
) >>
14981495
gvs[SWAP_REVERSE_SYM, LIST_REL_SPLIT1, REVERSE_APPEND] >>
14991496
ntac 1 (qrefine `SUC n` >> simp[cstep]) >>
1500-
qmatch_goalsub_abbrev_tac `Estep (_,_,_,_,ck')` >>
1501-
qspecl_then [`ys1 ++ [y]`,`cnenv`,`cenv`,`cst`,`fp`,`ck'`]
1497+
qmatch_goalsub_abbrev_tac `Estep (_,_,_,ck')` >>
1498+
qspecl_then [`ys1 ++ [y]`,`cnenv`,`cenv`,`cst`,`ck'`]
15021499
assume_tac cstep_list_to_exp >> gvs[] >>
15031500
qrefine `m + n` >> simp[cstep_n_add, REVERSE_APPEND] >>
15041501
qrefine `SUC m` >> simp[cstep, list_to_cont_def] >> unabbrev_all_tac >>
@@ -1533,7 +1530,7 @@ Proof
15331530
impl_keep_tac >- gvs[env_rel_def] >> strip_tac >> gvs[] >>
15341531
qrefine `SUC n` >> simp[cstep] >>
15351532
drule step1_rel_Case_match >> rpt $ disch_then $ drule_at Any >>
1536-
disch_then $ qspecl_then [`fp`,`cvs`,`cst`,`ck`,`[]`] mp_tac >>
1533+
disch_then $ qspecl_then [`cvs`,`cst`,`ck`,`[]`] mp_tac >>
15371534
imp_res_tac LIST_REL_LENGTH >> gvs[] >> strip_tac >> gvs[] >>
15381535
qexists `n` >> simp[step_rel_cases] >> rpt $ goal_assum $ drule_at Any >>
15391536
irule_at Any env_rel_pmatch >> irule_at Any env_ok_pmatch >> simp[]
@@ -1567,7 +1564,7 @@ Proof
15671564
impl_keep_tac >- gvs[env_rel_def] >> strip_tac >> gvs[] >>
15681565
qrefine `SUC n` >> simp[cstep] >>
15691566
drule step1_rel_Case_match >> rpt $ disch_then $ drule_at Any >>
1570-
disch_then $ qspecl_then [`fp`,`cvs`,`cst`,`ck`,`[Pany,cuse]`] mp_tac >>
1567+
disch_then $ qspecl_then [`cvs`,`cst`,`ck`,`[Pany,cuse]`] mp_tac >>
15711568
imp_res_tac LIST_REL_LENGTH >> gvs[] >> strip_tac >> gvs[] >>
15721569
qexists `n` >> simp[step_rel_cases] >> rpt $ goal_assum $ drule_at Any >>
15731570
irule_at Any env_rel_pmatch >> irule_at Any env_ok_pmatch >> simp[]
@@ -1590,7 +1587,7 @@ Proof
15901587
impl_keep_tac >- gvs[env_rel_def] >> strip_tac >> gvs[] >>
15911588
qrefine `SUC n` >> simp[cstep] >>
15921589
drule step1_rel_Case_underscore >> rpt $ disch_then $ drule_at Any >>
1593-
disch_then $ qspecl_then [`fp`,`cvs`,`cuse`,`cst`,`ck`] mp_tac >>
1590+
disch_then $ qspecl_then [`cvs`,`cuse`,`cst`,`ck`] mp_tac >>
15941591
imp_res_tac LIST_REL_LENGTH >> gvs[] >> strip_tac >> gvs[] >>
15951592
qexists `n` >> simp[step_rel_cases] >> rpt $ goal_assum $ drule_at Any
15961593
)
@@ -1850,7 +1847,7 @@ Proof
18501847
)
18511848
>- ( (* out of bounds *)
18521849
qmatch_goalsub_abbrev_tac `cstep_n _ foo` >>
1853-
`foo = Estep (cenv',cst,fp,Exn sub_exn_v,ck')` by (
1850+
`foo = Estep (cenv',cst,Exn sub_exn_v,ck')` by (
18541851
unabbrev_all_tac >> simp[AllCaseEqs()] >> ARITH_TAC) >>
18551852
simp[] >> ntac 2 $ pop_assum kall_tac >>
18561853
qexists0 >> simp[step_rel_cases] >> rpt $ goal_assum $ drule_at Any >>
@@ -1888,7 +1885,7 @@ Proof
18881885
)
18891886
>- ( (* out of bounds *)
18901887
qmatch_goalsub_abbrev_tac `cstep_n _ foo` >>
1891-
`foo = Estep (cenv',cst,fp,Exn sub_exn_v,ck')` by (
1888+
`foo = Estep (cenv',cst,Exn sub_exn_v,ck')` by (
18921889
unabbrev_all_tac >> simp[AllCaseEqs()] >> ARITH_TAC) >>
18931890
simp[] >> ntac 2 $ pop_assum kall_tac >>
18941891
qexists0 >> simp[step_rel_cases] >> rpt $ goal_assum $ drule_at Any >>
@@ -2044,7 +2041,7 @@ Proof
20442041
unabbrev_all_tac >> gvs[env_ok_def] >> rpt (irule_at Any EQ_REFL >> simp[])) >>
20452042
drule $ cj 2 env_ok_imps >> strip_tac >>
20462043
drule_all strle >>
2047-
disch_then $ qspecl_then [`s1`,`s2`,`cst`,`fp`,`ck'`] assume_tac >> gvs[] >>
2044+
disch_then $ qspecl_then [`s1`,`s2`,`cst`,`ck'`] assume_tac >> gvs[] >>
20482045
qrefine `n + k` >> simp[cstep_n_add] >>
20492046
qexists0 >> simp[] >> IF_CASES_TAC >> simp[step_rel_cases] >>
20502047
rpt $ goal_assum $ drule_at Any >>
@@ -2071,7 +2068,7 @@ Proof
20712068
unabbrev_all_tac >> gvs[env_ok_def] >> rpt (irule_at Any EQ_REFL >> simp[])) >>
20722069
drule $ cj 2 env_ok_imps >> strip_tac >>
20732070
drule_all strle >>
2074-
disch_then $ qspecl_then [`s1`,`s2`,`cst`,`fp`,`ck'`] assume_tac >> gvs[] >>
2071+
disch_then $ qspecl_then [`s1`,`s2`,`cst`,`ck'`] assume_tac >> gvs[] >>
20752072
qrefine `n + k` >> simp[cstep_n_add] >>
20762073
qexists0 >> simp[step_rel_cases] >> rpt $ goal_assum $ drule_at Any >>
20772074
simp[stringTheory.string_le_def] >> IF_CASES_TAC >> gvs[] >>
@@ -2085,7 +2082,7 @@ Proof
20852082
unabbrev_all_tac >> gvs[env_ok_def] >> rpt (irule_at Any EQ_REFL >> simp[])) >>
20862083
drule $ cj 2 env_ok_imps >> strip_tac >>
20872084
drule_all strle >>
2088-
disch_then $ qspecl_then [`s2`,`s1`,`cst`,`fp`,`ck'`] assume_tac >> gvs[] >>
2085+
disch_then $ qspecl_then [`s2`,`s1`,`cst`,`ck'`] assume_tac >> gvs[] >>
20892086
qrefine `n + k` >> simp[cstep_n_add] >>
20902087
qexists0 >> simp[step_rel_cases] >> rpt $ goal_assum $ drule_at Any >>
20912088
simp[string_ge_def] >> IF_CASES_TAC >> gvs[] >>
@@ -2099,7 +2096,7 @@ Proof
20992096
unabbrev_all_tac >> gvs[env_ok_def] >> rpt (irule_at Any EQ_REFL >> simp[])) >>
21002097
drule $ cj 2 env_ok_imps >> strip_tac >>
21012098
qmatch_goalsub_abbrev_tac `cif::ck'` >> drule_all strle >>
2102-
disch_then $ qspecl_then [`s1`,`s2`,`cst`,`fp`,`cif::ck'`] assume_tac >> gvs[] >>
2099+
disch_then $ qspecl_then [`s1`,`s2`,`cst`,`cif::ck'`] assume_tac >> gvs[] >>
21032100
qrefine `n + k` >> simp[cstep_n_add] >> unabbrev_all_tac >>
21042101
qrefine `SUC n` >> simp[cstep_n_def, cstep, do_if_def] >>
21052102
`nsLookup cenv'.c (Short "False") = SOME (0,TypeStamp "False" 0) ∧
@@ -2170,7 +2167,7 @@ Proof
21702167
gvs[] >> drule $ cj 3 env_ok_imps >> strip_tac >> gvs[] >>
21712168
drule_all char_list >>
21722169
disch_then $ qspecl_then
2173-
[`il`,`cst`,`fp`,`(Capp Implode [] [],cenv')::ck'`] assume_tac >> gvs[] >>
2170+
[`il`,`cst`,`(Capp Implode [] [],cenv')::ck'`] assume_tac >> gvs[] >>
21742171
qrefine `n + k` >> simp[cstep_n_add] >>
21752172
qrefine `SUC n` >> simp[cstep, do_app_def] >>
21762173
simp[GSYM implode_v_to_char_list_list_to_v, IMPLODE_EXPLODE_I] >>
@@ -2296,15 +2293,15 @@ Proof
22962293
>- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL)
22972294
>- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL) >>
22982295
drule step1_rel >> simp[] >> strip_tac >> gvs[] >>
2299-
`cstep_n (SUC n) (Estep (cenv,dst.refs,dst.fp_state,ceve,ck)) ≠ Edone` by (
2296+
`cstep_n (SUC n) (Estep (cenv,dst.refs,ceve,ck)) ≠ Edone` by (
23002297
CCONTR_TAC >> gvs[step_rel_cases]) >>
23012298
qrefine `m + n` >> simp[SUC_ADD_SYM, itree_semanticsPropsTheory.step_n_add] >>
23022299
drule $ SRULE [] cstep_n_to_dstep_n >>
23032300
disch_then $ qspecl_then
23042301
[`benv`,`locs`,`Pvar "prog"`,`[CdlocalG lenv genv (final_gc flag)]`] assume_tac >>
23052302
gvs[] >> pop_assum kall_tac >>
23062303
reverse $ Cases_on
2307-
`cstep_n (SUC n) (Estep (cenv,dst.refs,dst.fp_state,ceve,ck))` >> gvs[]
2304+
`cstep_n (SUC n) (Estep (cenv,dst.refs,ceve,ck))` >> gvs[]
23082305
>- fs[Once step_rel_cases]
23092306
>- (
23102307
qpat_x_assum `step_rel _ _` mp_tac >>

0 commit comments

Comments
 (0)