Skip to content

Commit 06de292

Browse files
didriklundbergdidriklundberg
committed
More progress on metatheory
1 parent 21f4af0 commit 06de292

File tree

3 files changed

+52
-35
lines changed

3 files changed

+52
-35
lines changed

‎hol/metatheory/p4_e_progressScript.sml‎

Lines changed: 44 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -42,15 +42,15 @@ val _ = new_theory "p4_e_progress";
4242
val prog_exp_def = Define `
4343
prog_exp (e) (ty:'a itself) =
4444
!gscope (scopest:scope list) t_scope_list t_scope_list_g
45-
T_e tau b (c:'a ctx) order delta_g delta_b (delta_t:delta_t) delta_x f Prs_n.
45+
T_e tau b (c:'a ectx) order delta_g delta_b (delta_t:delta_t) delta_x f Prs_n.
4646

4747
type_scopes_list gscope t_scope_list_g ∧
4848
type_scopes_list scopest t_scope_list ∧
4949
star_not_in_sl (scopest) ∧
5050
~(is_const e) ∧
5151
e_typ (t_scope_list_g,t_scope_list) T_e e tau b ∧
5252
(T_e = (order, f, (delta_g, delta_b, delta_x, delta_t))) /\
53-
WT_c c order t_scope_list_g delta_g delta_b delta_x delta_t Prs_n ==>
53+
WT_ec c order t_scope_list_g delta_g delta_b delta_x delta_t Prs_n ==>
5454
?e' framel. e_red c gscope scopest e e' framel
5555
`;
5656

@@ -1335,15 +1335,16 @@ gvs[]
13351335

13361336

13371337
val wf_imp_ci_abstract_single = prove ( ``
1338-
! e d x ss .
1339-
wf_arg d x e (ss) ==>
1340-
? scope . copyin_abstract [x] [d] [e] (ss) scope``,
1338+
!e d x ss oracle_index random_oracle.
1339+
wf_arg d x e ss ==>
1340+
?scope. copyin_abstract [x] [d] [e] ss scope oracle_index random_oracle``,
13411341

13421342
REPEAT STRIP_TAC >>
1343-
Q.EXISTS_TAC `[(varn_name x , THE (one_arg_val_for_newscope (d) (e) ss))]` >>
1343+
Q.EXISTS_TAC `[(varn_name x , (\ (a,b). (FST a, b)) $ THE (one_arg_val_for_newscope d e ss oracle_index random_oracle))]` >>
13441344

13451345
fs[copyin_abstract_def] >>
13461346
IMP_RES_TAC wf_imp_val_lval >>
1347+
Q.PAT_X_ASSUM ‘!random_oracle i. _’ (fn thm => assume_tac $ Q.SPECL [‘random_oracle’, ‘oracle_index’] thm) >>
13471348
gvs[]
13481349
);
13491350

@@ -1353,12 +1354,12 @@ gvs[]
13531354

13541355

13551356
val wf_imp_new_vlval_list = prove ( ``
1356-
! i dl xl el ss.
1357+
! i dl xl el ss oracle_index random_oracle.
13571358
(LENGTH xl = LENGTH dl) /\
13581359
(LENGTH dl = LENGTH el) /\
13591360
(i < LENGTH dl ) /\
13601361
wf_arg_list (dl) (xl) (el) ss ==>
1361-
? vlval . one_arg_val_for_newscope (EL i (dl)) (EL i (el)) ss = SOME vlval``,
1362+
? vlval . one_arg_val_for_newscope (EL i (dl)) (EL i (el)) ss oracle_index random_oracle = SOME vlval``,
13621363

13631364
Induct_on `xl` >>
13641365
Induct_on `dl` >>
@@ -1372,7 +1373,7 @@ gvs[] >| [
13721373

13731374
IMP_RES_TAC wf_arg_normalization >>
13741375
IMP_RES_TAC wf_imp_val_lval >>
1375-
srw_tac [SatisfySimps.SATISFY_ss][]
1376+
metis_tac[]
13761377
,
13771378

13781379
IMP_RES_TAC wf_arg_normalization >>
@@ -1401,20 +1402,20 @@ gvs[] >| [
14011402

14021403

14031404
val wf_arg_list_NONE2 = prove (``
1404-
! dl xl el ss .
1405+
! dl xl el ss oracle_index random_oracle.
14051406
(LENGTH xl = LENGTH dl) /\
14061407
(LENGTH dl = LENGTH el) /\
14071408
wf_arg_list dl xl el ss /\
14081409
ALL_DISTINCT xl ==>
1409-
~ (all_arg_update_for_newscope xl dl el ss = NONE)``,
1410+
~ (all_arg_update_for_newscope xl dl el ss oracle_index random_oracle = NONE)``,
14101411

14111412
REPEAT STRIP_TAC >>
14121413
fs[all_arg_update_for_newscope_def] >>
14131414
ASSUME_TAC wf_arg_list_NONE >>
14141415

14151416
FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL [`ZIP (dl,ZIP (xl,el))`])) >>
14161417
gvs[] >>
1417-
FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL [`ss`])) >>
1418+
FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL [`ss`, ‘oracle_index’, ‘random_oracle’])) >>
14181419
gvs[] >| [
14191420

14201421
`(MAP (λ(d,x,e). x) (ZIP (dl,ZIP (xl,el)))) = xl` by gvs[GSYM map_distrub] >>
@@ -1434,21 +1435,21 @@ gvs[] >| [
14341435

14351436

14361437
val copyin_eq_rw = prove ( ``
1437-
! xl dl el gscope scopest scope.
1438+
! xl dl el gscope scopest scope oracle_index random_oracle.
14381439
(LENGTH xl = LENGTH dl) /\
14391440
(LENGTH dl = LENGTH el) /\
14401441
(ALL_DISTINCT xl) ∧
14411442
(wf_arg_list dl xl el (scopest ⧺ gscope)) ==>
1442-
( (SOME scope = copyin xl dl el gscope scopest)
1443+
((?i_opt. SOME (scope, i_opt) = copyin xl dl el gscope scopest oracle_index random_oracle)
14431444
<=>
1444-
copyin_abstract xl dl el (scopest ⧺ gscope) scope)
1445+
copyin_abstract xl dl el (scopest ⧺ gscope) scope oracle_index random_oracle)
14451446
``,
14461447

14471448
REPEAT STRIP_TAC >>
14481449
ASSUME_TAC copyin_eq >>
14491450
FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL
14501451
[`ZIP (el,ZIP (xl,dl))`, `gscope`,
1451-
`scopest`, `scope`])) >>
1452+
`scopest`, `scope`, ‘oracle_index’, ‘random_oracle’])) >>
14521453
gvs[] >>
14531454

14541455
`(MAP (λ(e,x,d). x) (ZIP (el,ZIP (xl,dl)))) = xl` by gvs[GSYM map_distrub] >>
@@ -1929,18 +1930,23 @@ gvs[is_const_def, clause_name_def] >>
19291930

19301931
(* the cases should be on if there is an element unreduced yet? *)
19311932
Cases_on ` (unred_arg_index (MAP (λ(e_,tau_,x_,d_,b_). d_) e_tau_x_d_b_list)
1932-
(MAP (λ(e_,tau_,x_,d_,b_). e_) e_tau_x_d_b_list) = NONE) ` >| [
1933+
(MAP (λ(e_,tau_,x_,d_,b_). e_) e_tau_x_d_b_list) = NONE)` >| [
19331934

19341935
DISJ1_TAC >>
19351936

19361937
IMP_RES_TAC unred_arg_index_NONE >>
19371938

19381939
ASSUME_TAC tfunn_imp_sig_body_lookup >>
19391940
FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL
1940-
[`c0`, `c1`, `c2`, `c3`, `c4`, `c5`, `order`, `t_scope_list_g`,
1941+
[`c0`, `c1`, `c2`, `c3`, `c4`, `c5`,
1942+
‘get_oracle_index’, ‘set_oracle_index’, ‘c7’,
1943+
`order`, `t_scope_list_g`,
19411944
`delta_g`, `delta_b`, `delta_x`,
19421945
`(MAP (λ(e_,tau_,x_,d_,b_).(tau_,x_,d_)) (e_tau_x_d_b_list : (e # tau # string # d # bool) list))`,
19431946
`tau'`, `f` , ‘delta_t’, ‘Prs_n’ ])) >> gvs[] >>
1947+
assume_tac $ Q.SPECL
1948+
[`c0`, `c1`, `c2`, `c3`, `c4`, `c5`, ‘get_oracle_index’, ‘set_oracle_index’, ‘c6’, ‘c7’] $ GSYM WT_c_ec >>
1949+
gs[] >>
19441950

19451951
Q.EXISTS_TAC `ZIP ((MAP (λ(e_,tau_,x_,d_,b_). e_) e_tau_x_d_b_list),
19461952
ZIP(MAP FST xdl,MAP SND xdl))` >>
@@ -1978,19 +1984,21 @@ Cases_on ` (unred_arg_index (MAP (λ(e_,tau_,x_,d_,b_). d_) e_tau_x_d_b_list)
19781984
`gscope`, `scopest`, `scope`])) >>
19791985
gvs[] >>
19801986
gvs[] >>
1981-
1982-
Q.EXISTS_TAC `THE(copyin (MAP FST xdl) (MAP (λ(e_,tau_,x_,d_,b_). d_) e_tau_x_d_b_list)
1983-
(MAP (λ(e_,tau_,x_,d_,b_). e_) e_tau_x_d_b_list) gscope scopest)` >>
1987+
qpat_x_assum ‘!oracle_index. _’ (fn thm => assume_tac $ Q.SPECL [‘c6’, ‘c7’] thm) >>
1988+
Q.EXISTS_TAC `FST $ THE(copyin (MAP FST xdl) (MAP (λ(e_,tau_,x_,d_,b_). d_) e_tau_x_d_b_list)
1989+
(MAP (λ(e_,tau_,x_,d_,b_). e_) e_tau_x_d_b_list) gscope scopest c6 c7)` >>
19841990
gvs[] >>
19851991

19861992
Cases_on ` copyin (MAP FST xdl) (MAP (λ(e_,tau_,x_,d_,b_). d_) e_tau_x_d_b_list)
1987-
(MAP (λ(e_,tau_,x_,d_,b_). e_) e_tau_x_d_b_list) gscope scopest` >| [
1993+
(MAP (λ(e_,tau_,x_,d_,b_). e_) e_tau_x_d_b_list) gscope scopest c6 c7` >| [
19881994

19891995
IMP_RES_TAC wf_arg_list_NONE2 >>
19901996
gvs[] >>
1991-
fs[copyin_def]
1997+
gvs[copyin_def, AllCaseEqs()]
19921998
,
1993-
gvs[]
1999+
gvs[] >>
2000+
qexists_tac ‘SND x’ >>
2001+
gs[]
19942002
]
19952003
,
19962004

@@ -2002,7 +2010,9 @@ Cases_on ` (unred_arg_index (MAP (λ(e_,tau_,x_,d_,b_). d_) e_tau_x_d_b_list)
20022010
(* first show that we can indeed find a map for the function f in the context *)
20032011
ASSUME_TAC tfunn_imp_sig_lookup >>
20042012
FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL
2005-
[`c0`, `c1`, `c2`, `c3`, `c4`, `c5`, `order`, `t_scope_list_g`,
2013+
[`c0`, `c1`, `c2`, `c3`, `c4`, `c5`,
2014+
‘get_oracle_index’, ‘set_oracle_index’, ‘c7’,
2015+
`order`, `t_scope_list_g`,
20062016
`delta_g`, `delta_b`, `delta_x`,
20072017
`(MAP (λ(e_,tau_,x_,d_,b_).(tau_,x_,d_)) (e_tau_x_d_b_list : (e # tau # string # d # bool) list))`,
20082018
`tau'`, `f`, ‘delta_t’, ‘Prs_n’])) >> gvs[] >>
@@ -2027,11 +2037,14 @@ Cases_on ` (unred_arg_index (MAP (λ(e_,tau_,x_,d_,b_). d_) e_tau_x_d_b_list)
20272037
[`gscope`, `scopest`, `t_scope_list`, `t_scope_list_g`,
20282038
`(t_tau (EL i (MAP (λ(e_,tau_,x_,d_,b_). tau_) (e_tau_x_d_b_list : (e # tau # string # d # bool) list))))`,
20292039
`(EL i (MAP (λ(e_,tau_,x_,d_,b_). b_) (e_tau_x_d_b_list : (e # tau # string # d # bool) list)))`,
2030-
`(c0,c1,c2,c3,c4,c5)`, `order`, `delta_g`, `delta_b`, `delta_t`, `delta_x`, `f'`, ‘Prs_n’])) >> gvs[] >>
2031-
2040+
`(c0,c1,c2,c3,c4,c5,c6,c7)`, `order`, `delta_g`, `delta_b`, `delta_t`, `delta_x`, `f'`, ‘Prs_n’])) >> gvs[] >>
20322041
IMP_RES_TAC unred_arg_index_result >| [
20332042
(* if d is in/none, then it shouldn't be a constant in order to reduce it *)
20342043
gvs[] >>
2044+
(* TODO: Why doesn't it work to rewrite? *)
2045+
assume_tac $ Q.SPECL
2046+
[`c0`, `c1`, `c2`, `c3`, `c4`, `c5`, ‘get_oracle_index’, ‘set_oracle_index’, ‘c6’, ‘c7’] $ GSYM WT_c_ec >>
2047+
gs[] >>
20352048

20362049
Q.EXISTS_TAC `framel` >>
20372050
Q.EXISTS_TAC `ZIP ( MAP (λ(e_,tau_,x_,d_,b_). e_) e_tau_x_d_b_list ,
@@ -2064,6 +2077,10 @@ Cases_on ` (unred_arg_index (MAP (λ(e_,tau_,x_,d_,b_). d_) e_tau_x_d_b_list)
20642077

20652078
IMP_RES_TAC notlval_case >| [
20662079
gvs[] >>
2080+
(* TODO: Why doesn't it work to rewrite? *)
2081+
assume_tac $ Q.SPECL
2082+
[`c0`, `c1`, `c2`, `c3`, `c4`, `c5`, ‘get_oracle_index’, ‘set_oracle_index’, ‘c6’, ‘c7’] $ GSYM WT_c_ec >>
2083+
gs[] >>
20672084

20682085
Q.EXISTS_TAC `framel` >>
20692086
Q.EXISTS_TAC `ZIP ( MAP (λ(e_,tau_,x_,d_,b_). e_) e_tau_x_d_b_list ,

‎hol/metatheory/p4_e_subject_reductionScript.sml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1380,10 +1380,10 @@ QED
13801380

13811381

13821382
Theorem tfunn_imp_sig_body_lookup:
1383-
! apply_table_f ext_map func_map b_func_map pars_map tbl_map
1383+
! apply_table_f ext_map func_map b_func_map pars_map tbl_map get_oracle_index set_oracle_index random_oracle
13841384
order t_scope_list_g delta_g delta_b delta_x txdl tau f delta_t Prs_n.
1385-
WT_c (apply_table_f,ext_map,func_map,b_func_map,pars_map,tbl_map)
1386-
order t_scope_list_g delta_g delta_b delta_x delta_t Prs_n/\
1385+
WT_c (apply_table_f,ext_map,func_map,b_func_map,pars_map,tbl_map,get_oracle_index,set_oracle_index,random_oracle)
1386+
order t_scope_list_g delta_g delta_b delta_x delta_t Prs_n /\
13871387
SOME (txdl,tau) = t_lookup_funn f delta_g delta_b delta_x ==>
13881388
?stmt xdl.
13891389
SOME (stmt,xdl) =
@@ -1520,9 +1520,9 @@ QED
15201520

15211521

15221522
Theorem tfunn_imp_sig_lookup:
1523-
! apply_table_f ext_map func_map b_func_map pars_map tbl_map
1523+
! apply_table_f ext_map func_map b_func_map pars_map tbl_map get_oracle_index set_oracle_index random_oracle
15241524
order t_scope_list_g delta_g delta_b delta_x txdl tau f delta_t Prs_n .
1525-
WT_c (apply_table_f,ext_map,func_map,b_func_map,pars_map,tbl_map)
1525+
WT_c (apply_table_f,ext_map,func_map,b_func_map,pars_map,tbl_map,get_oracle_index,set_oracle_index,random_oracle)
15261526
order t_scope_list_g delta_g delta_b delta_x delta_t Prs_n /\
15271527
SOME (txdl,tau) = t_lookup_funn f delta_g delta_b delta_x ==>
15281528
? xdl.

‎hol/metatheory/p4_stmt_subject_reductionScript.sml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -125,9 +125,9 @@ apply_table_f ext_map func_map b_func_map pars_map tbl_map.
125125

126126

127127
val fr_len_exp_def = Define `
128-
fr_len_exp (e) (ty:'a itself) =
129-
∀ e' gscope (scopest:scope list) framel (c:'a ctx).
130-
e_red c gscope scopest e e' framel ⇒
128+
fr_len_exp e (ty:'a itself) =
129+
∀e' gscope (scopest:scope list) framel i_opt (c:'a ectx).
130+
e_red c gscope scopest e e' (framel, i_opt) ⇒
131131
((LENGTH framel = 1 ∧ ∃f_called stmt_called copied_in_scope. framel = [(f_called,[stmt_called],copied_in_scope)]) ∨
132132
(LENGTH framel = 0))
133133
`;

0 commit comments

Comments
 (0)