Skip to content

Commit 2015790

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
ported the project to the newest HOL4 version, and eliminated the last two cheats in merge and elim theory
1 parent a0413e3 commit 2015790

File tree

5 files changed

+59
-62
lines changed

5 files changed

+59
-62
lines changed

‎hol/bdd_auxScript.sml‎

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -503,12 +503,9 @@ Proof
503503
gvs[mk_new_labels_def] >>
504504
rpt strip_tac >>
505505
PairCases_on ‘h’ >>
506-
gvs[mk_new_labels_def] >| [
507-
qexists_tac ‘0’ >> gvs[]
508-
,
509-
res_tac >>
510-
qexists_tac ‘2+i’ >> gvs[]
511-
]
506+
gvs[mk_new_labels_def] >>
507+
res_tac >>
508+
qexists_tac ‘2+i’ >> gvs[]
512509
QED
513510

514511

@@ -1514,12 +1511,7 @@ Proof
15141511
]
15151512
QED
15161513

1517-
1518-
1519-
1520-
1521-
1522-
1514+
15231515

15241516
Theorem not_mem_imp_adelkey_mem:
15251517
∀ l n'' n'.

‎hol/bdd_gen_eliminateScript.sml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -633,7 +633,6 @@ Theorem eliminate_dom_range_edges3_imp_adel_key_mem:
633633
MEM n'' (dom_range_edges3 (ADELKEY n' (merge_edges edges n n')))
634634
Proof
635635
rpt strip_tac >>
636-
‘(n ≠ a ∧ n ≠ b ∧ n'' ≠ a ∧ n'' ≠ b)’ by cheat >>
637636
‘ ALL_DISTINCT (MAP FST (merge_edges edges n n')) ’ by metis_tac [all_distinct_fst_merge_edges] >>
638637

639638

@@ -802,7 +801,8 @@ QED
802801

803802
Theorem eliminate_dom_range_edges_imp_adel_key_mem:
804803
∀edges root labels vars n n' n'' a b.
805-
n'' ≠ n' ∧ n ≠ n' ∧ BDD_ordered (root,edges,labels) vars ∧
804+
n'' ≠ n' ∧ n ≠ n' ∧
805+
BDD_ordered (root,edges,labels) vars ∧
806806
ALL_DISTINCT (MAP FST edges) ∧
807807
MEM (n',n,n) edges ∧ MEM (n,a,b) edges ∧
808808
MEM n (dom_range_edges edges) ∧

‎hol/bdd_gen_mergeScript.sml‎

Lines changed: 20 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -45,9 +45,8 @@ Proof
4545

4646
PairCases_on ‘h’ >>
4747
gvs[] >>
48-
rpt (BasicProvers.FULL_CASE_TAC >> gvs[]) >>
4948
res_tac >>
50-
gvs[merge_edges_def]
49+
metis_tac[merge_edges_def]
5150
QED
5251

5352

@@ -1539,12 +1538,11 @@ Proof
15391538
QED
15401539

15411540

1542-
1543-
1541+
15441542
Theorem dom_range_edges3_imp_adel_key_mem:
15451543
∀ edges root labels vars n n' n'' a b.
15461544
n'' ≠ n' ∧ n ≠ n' ∧
1547-
BDD_ordered (root,edges,labels) vars ∧
1545+
(n ≠ a ∧ n' ≠ a ∧ n ≠ b ∧ n' ≠ b) ∧
15481546
ALL_DISTINCT (MAP FST edges) ∧
15491547
MEM (n,a,b) edges ∧
15501548
MEM (n',a,b) edges ∧
@@ -1555,8 +1553,7 @@ Proof
15551553

15561554
rpt strip_tac >>
15571555

1558-
‘(n ≠ a ∧ n' ≠ a ∧ n ≠ b ∧ n' ≠ b)’ by cheat >>
1559-
‘ ALL_DISTINCT (MAP FST (merge_edges edges n n')) ’ by metis_tac [all_distinct_fst_merge_edges] >>
1556+
‘ALL_DISTINCT (MAP FST (merge_edges edges n n')) ’ by metis_tac [all_distinct_fst_merge_edges] >>
15601557

15611558
gvs[dom_range_edges3_def] >>
15621559

@@ -2124,7 +2121,9 @@ QED
21242121

21252122
Theorem dom_range_edges_imp_adel_key_mem:
21262123
∀edges root labels vars n n' n'' a b.
2127-
n'' ≠ n' ∧ n ≠ n' ∧ BDD_ordered (root,edges,labels) vars ∧
2124+
n'' ≠ n' ∧ n ≠ n' ∧
2125+
(n ≠ a ∧ n' ≠ a ∧ n ≠ b ∧ n' ≠ b) ∧
2126+
BDD_ordered (root,edges,labels) vars ∧
21282127
ALL_DISTINCT (MAP FST edges) ∧
21292128
MEM (n,a,b) edges ∧ MEM (n',a,b) edges ∧
21302129
MEM n (dom_range_edges edges) ∧
@@ -2140,25 +2139,28 @@ QED
21402139
Theorem merge_edges_preserve_nodes:
21412140
∀ edges n n' n'' root labels vars.
21422141
n'' ≠ n' ∧ n ≠ n' ∧
2142+
BDD_WF (root,edges,labels) ∧
2143+
consumed_dom_bdd vars (root,edges,labels) ∧
21432144
BDD_ordered (root,edges,labels) vars ∧
2144-
ALL_DISTINCT (MAP FST edges) ∧
21452145
ALOOKUP edges n = ALOOKUP edges n' ∧
21462146
MEM n (dom_range_edges edges) ∧
21472147
MEM n'' (dom_range_edges (merge_edges edges n n')) ⇒
21482148
MEM n'' (dom_range_edges (ADELKEY n' (merge_edges edges n n')))
21492149
Proof
2150-
21512150
rpt strip_tac >>
21522151
Cases_on ‘ALOOKUP edges n’ >|[
2153-
2152+
‘ALL_DISTINCT (MAP FST edges) ’ by gvs[BDD_WF_def] >>
21542153
irule dom_range_edges_imp_adel_key_mem_none >>
21552154
gvs[]
21562155
,
2157-
2156+
2157+
‘ALL_DISTINCT (MAP FST edges) ’ by gvs[BDD_WF_def] >>
21582158
‘ALL_DISTINCT (MAP FST (merge_edges edges n n'))’ by gvs[GSYM all_distinct_fst_merge_edges] >>
21592159
PairCases_on ‘x’ >>
21602160
‘MEM (n,x0,x1) edges’ by gvs[ALOOKUP_MEM] >>
21612161
‘MEM (n',x0,x1) edges’ by gvs[ALOOKUP_MEM] >>
2162+
‘n ≠ x0 ∧ n ≠ x1’ by metis_tac[lookup_edges_not_parent] >>
2163+
‘n' ≠ x0 ∧ n' ≠ x1’ by metis_tac[lookup_edges_not_parent] >>
21622164
metis_tac[dom_range_edges_imp_adel_key_mem]
21632165
]
21642166
QED
@@ -2169,14 +2171,16 @@ QED
21692171

21702172
Theorem mergable_wf_labels_edges_same:
21712173
∀ r edges labels n n' vars_consumed.
2172-
ALL_DISTINCT (MAP FST edges) ∧
2174+
BDD_WF (r,edges,labels) ∧
21732175
BDD_ordered (r,edges,labels) vars_consumed ∧
2176+
consumed_dom_bdd vars_consumed (r,edges,labels) ∧
21742177
mergable (r,edges,labels) n n' ∧
21752178
( ∀n. MEM n (dom_range_edges edges) ⇔ MEM n (MAP FST labels)) ⇒
21762179
(∀n''. MEM n'' (dom_range_edges (ADELKEY n' (merge_edges edges n n'))) ⇔
21772180
MEM n'' (MAP FST (ADELKEY n' labels)))
21782181
Proof
21792182
rw[mergable_def] >>
2183+
‘ALL_DISTINCT (MAP FST edges)’ by gvs[BDD_WF_def] >>
21802184
Cases_on ‘n'' = n'’ >> gvs[] >|[
21812185
gvs[merge_no_effect_on_unrelated_node_mem] >>
21822186
gvs[ADELKEY_def, MEM_MAP, MEM_FILTER]
@@ -2221,7 +2225,8 @@ Proof
22212225

22222226
‘¬MEM n'' (MAP FST (ADELKEY n' labels))’ by metis_tac[not_mem_imp_adelkey_mem]
22232227
]
2224-
) ]
2228+
)
2229+
]
22252230
QED
22262231

22272232

@@ -2465,7 +2470,7 @@ Proof
24652470
by imp_res_tac ALL_DISTINCT_MAP_ADELKEY >> gvs[] >>
24662471

24672472
‘∀n''. MEM n'' (dom_range_edges (ADELKEY n' (merge_edges edges n n'))) ⇔
2468-
MEM n'' (MAP FST (ADELKEY n' labels))’ by imp_res_tac mergable_wf_labels_edges_same >> gvs[] >>
2473+
MEM n'' (MAP FST (ADELKEY n' labels))’ by (imp_res_tac mergable_wf_labels_edges_same >> gvs[BDD_WF_def]) >>
24692474

24702475
imp_res_tac mergable_wf_internals_some >> gvs[] >>
24712476

‎hol/table_arith_to_intervalScript.sml‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1148,8 +1148,8 @@ Theorem if_bs_ge_not_gt_max_then_eq:
11481148
bitv_binpred binop_ge (a,len) (fixwidth len (n2v (max_from_type len)),len) = SOME T ⇒
11491149
a = fixwidth len (n2v (max_from_type len))
11501150
Proof
1151-
RW.ONCE_RW_TAC [bitv_binpred_def] >>
1152-
RW.ONCE_RW_TAC [bitv_binpred_inner_def] >>
1151+
Rewrite.ONCE_REWRITE_TAC [bitv_binpred_def] >>
1152+
Rewrite.ONCE_REWRITE_TAC [bitv_binpred_inner_def] >>
11531153
rpt strip_tac >>
11541154

11551155
rpt(
@@ -1175,8 +1175,8 @@ Theorem if_bs_le_ge_max_then_eq:
11751175
bitv_binpred binop_le (a,len) (n2v (max_from_type len),len) = SOME T ⇒
11761176
a = fixwidth len (n2v (max_from_type len))
11771177
Proof
1178-
RW.ONCE_RW_TAC [bitv_binpred_def] >>
1179-
RW.ONCE_RW_TAC [bitv_binpred_inner_def] >>
1178+
Rewrite.ONCE_REWRITE_TAC [bitv_binpred_def] >>
1179+
Rewrite.ONCE_REWRITE_TAC [bitv_binpred_inner_def] >>
11801180
rpt strip_tac >>
11811181

11821182
rpt(
@@ -1523,7 +1523,7 @@ Theorem transitive_binpred2:
15231523
bitv_binpred binop_le (c,len) (a,len) = SOME T
15241524
Proof
15251525
rw[bitv_binpred_def] >>
1526-
RW.ONCE_RW_TAC [bitv_binpred_inner_def, get_word_binpred_def] >>
1526+
Rewrite.ONCE_REWRITE_TAC [bitv_binpred_inner_def, get_word_binpred_def] >>
15271527
rpt strip_tac >>
15281528

15291529
rpt(
@@ -1547,7 +1547,7 @@ Theorem transitive_binpred3:
15471547
bitv_binpred binop_ge (c,len) (b,len) = SOME T
15481548
Proof
15491549
rw[bitv_binpred_def] >>
1550-
RW.ONCE_RW_TAC [bitv_binpred_inner_def, get_word_binpred_def] >>
1550+
Rewrite.ONCE_REWRITE_TAC [bitv_binpred_inner_def, get_word_binpred_def] >>
15511551
rpt strip_tac >>
15521552

15531553
rpt(
@@ -1569,7 +1569,7 @@ Theorem transitive_binpred4:
15691569
bitv_binpred binop_ge (c,len) (b,len) = SOME F
15701570
Proof
15711571
rw[bitv_binpred_def] >>
1572-
RW.ONCE_RW_TAC [bitv_binpred_inner_def, get_word_binpred_def] >>
1572+
Rewrite.ONCE_REWRITE_TAC [bitv_binpred_inner_def, get_word_binpred_def] >>
15731573
rpt strip_tac >>
15741574

15751575
rpt(
@@ -1592,7 +1592,7 @@ Theorem transitive_binpred5:
15921592
Proof
15931593

15941594
rw[bitv_binpred_def] >>
1595-
RW.ONCE_RW_TAC [bitv_binpred_inner_def, get_word_binpred_def] >>
1595+
Rewrite.ONCE_REWRITE_TAC [bitv_binpred_inner_def, get_word_binpred_def] >>
15961596
rpt strip_tac >>
15971597

15981598
rpt(

0 commit comments

Comments
 (0)