Skip to content

Commit 4f582db

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
removed some comments chunks
1 parent 618771c commit 4f582db

File tree

5 files changed

+26
-595
lines changed

5 files changed

+26
-595
lines changed

‎hol/policy_to_table/bdd_end_to_endScript.sml‎

Lines changed: 0 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -769,31 +769,6 @@ Definition correct_var_policy_var_tables_exec_def:
769769
T
770770
End
771771

772-
(*
773-
Definition correct_var_policy_var_tables_exec2_def:
774-
correct_var_policy_var_tables_exec2 var_policy var_table vars I =
775-
let BDD1_opt = mk_BDDPred_opt_new policy_structure (0,[],[(0, non_termn (NONE, var_policy))]) [] vars 1 in
776-
let BDD2_opt = mk_BDDPred_opt_new table_structure_new (0,[],[(0, non_termn (NONE, var_table ))]) [] vars 1 in
777-
if ~ IS_SOME(BDD1_opt) \/ ~ IS_SOME (BDD2_opt) then
778-
T
779-
else let BDD1 = THE BDD1_opt in let BDD2 = THE BDD2_opt in
780-
if (isIsomorph_exec (I: (num #num) list) BDD1 BDD2 ∧
781-
ALOOKUP I 0 = SOME 0 ∧
782-
node_in_BDD 0 BDD1 ∧
783-
node_in_BDD 0 BDD2 ∧
784-
prop_in_BDD 0 BDD1 = SOME var_policy ∧
785-
prop_in_BDD 0 BDD2 = SOME var_table ∧
786-
fv_in_vars_exec table_structure_new var_table vars ∧
787-
fv_in_vars_exec policy_structure var_policy vars ∧
788-
ALL_DISTINCT vars ∧
789-
vars ≠ []) then
790-
791-
(! mv. mv_dom_vars mv vars ⇒
792-
sem_policy var_policy mv = sem_tables var_table mv)
793-
else
794-
T
795-
End
796-
*)
797772

798773

799774

@@ -870,15 +845,6 @@ Proof
870845
QED
871846

872847

873-
(*
874-
Theorem correct_var_policy_var_tables_exec2_thm1:
875-
∀ var_policy var_table vars I.
876-
correct_var_policy_var_tables_exec2 var_policy var_table vars I
877-
Proof
878-
cheat
879-
QED
880-
*)
881-
882848
(******************************************
883849
884850
arith policy to interval table requirement for gluing all assumtions of equiality theorems:

‎hol/policy_to_table/bdd_gen_eliminateScript.sml‎

Lines changed: 0 additions & 102 deletions
Original file line numberDiff line numberDiff line change
@@ -1481,108 +1481,6 @@ Proof
14811481
QED
14821482

14831483

1484-
1485-
1486-
1487-
(*
1488-
Theorem eliminate_BDD_preserves_valid_and_correctness_verbose:
1489-
∀BDD n nl vars rec.
1490-
1491-
BDD_WF BDD ∧
1492-
BDD_ordered BDD vars ∧
1493-
fv_in_BDD rec BDD vars ∧
1494-
consumed_dom_bdd vars BDD ∧
1495-
correct_sem rec BDD vars ⇒
1496-
1497-
(
1498-
BDD_WF (eliminate_BDD BDD nl) ∧
1499-
BDD_ordered (eliminate_BDD BDD nl) vars ∧
1500-
fv_in_BDD rec (eliminate_BDD BDD nl) vars ∧
1501-
consumed_dom_bdd vars (eliminate_BDD BDD nl) ∧
1502-
correct_sem rec (eliminate_BDD BDD nl) vars
1503-
)
1504-
Proof
1505-
Induct_on ‘nl’ >-
1506-
(* Base case: empty list *)
1507-
fs [eliminate_BDD_def] >>
1508-
1509-
(* Inductive case *)
1510-
rpt gen_tac >> strip_tac >>
1511-
fs [eliminate_BDD_def] >>
1512-
1513-
Cases_on ‘eliminable BDD h’ >> gvs[] >|[
1514-
metis_tac[]
1515-
,
1516-
gvs[] >>
1517-
assume_tac eliminate_correct >>
1518-
first_x_assum (strip_assume_tac o (Q.SPECL [‘BDD’, ‘[]’, ‘vars’, ‘x’, ‘h’, ‘rec’])) >>
1519-
gvs[] >>
1520-
(*res_tac >>*)
1521-
‘BDD_WF (merge BDD x h)’ by imp_res_tac eliminate_wf_preservation >>
1522-
‘BDD_ordered (merge BDD x h) vars’ by imp_res_tac eliminate_order_preservation >>
1523-
‘fv_in_BDD rec (merge BDD x h) vars’ by (imp_res_tac merge_fv_final_preservation >>
1524-
first_x_assum (strip_assume_tac o (Q.SPECL [‘h’, ‘x’]))) >>
1525-
imp_res_tac merge_consumed_dom_final_preservation >>
1526-
first_x_assum (strip_assume_tac o (Q.SPECL [‘h’, ‘x’]) ) >>
1527-
gvs[]>>
1528-
1529-
1530-
res_tac >>
1531-
gvs[]
1532-
]
1533-
QED
1534-
*)
1535-
1536-
1537-
(*)
1538-
Theorem eliminate_BDD_preserves_valid_and_correctness:
1539-
∀BDD nl vars vars_consumed rec.
1540-
valid_BDD rec BDD vars vars_consumed ∧
1541-
correct_sem rec BDD (vars ⧺ vars_consumed) ⇒
1542-
(
1543-
valid_BDD rec (eliminate_BDD BDD nl) vars vars_consumed ∧
1544-
correct_sem rec (eliminate_BDD BDD nl) (vars ⧺ vars_consumed)
1545-
)
1546-
1547-
Proof
1548-
1549-
Induct_on ‘nl’ >-
1550-
(* Base case: empty list *)
1551-
fs [eliminate_BDD_def] >>
1552-
1553-
(* Inductive case *)
1554-
rpt gen_tac >> strip_tac >>
1555-
fs [eliminate_BDD_def] >>
1556-
1557-
Cases_on ‘eliminable BDD h’ >> gvs[] >>
1558-
1559-
gvs[valid_BDD_def] >>
1560-
1561-
assume_tac eliminate_correct >>
1562-
first_x_assum (strip_assume_tac o (Q.SPECL [‘BDD’, ‘vars’, ‘vars_consumed’,‘x’, ‘h’, ‘rec’])) >>
1563-
gvs[] >>
1564-
1565-
‘fv_in_BDD rec BDD (vars ⧺ vars_consumed)’ by imp_res_tac fv_in_BDD_reverse_triv >>
1566-
gvs[] >>
1567-
1568-
(*res_tac >>*)
1569-
‘BDD_WF (merge BDD x h)’ by imp_res_tac eliminate_wf_preservation >>
1570-
‘BDD_ordered (merge BDD x h) vars_consumed’ by imp_res_tac eliminate_order_preservation >>
1571-
1572-
‘consumed_dom_bdd vars_consumed (merge BDD x h)’ by (imp_res_tac merge_consumed_dom_final_preservation >>
1573-
first_x_assum (strip_assume_tac o (Q.SPECL [‘h’, ‘x’]))) >>
1574-
1575-
imp_res_tac merge_fv_final_preservation >>
1576-
first_x_assum (strip_assume_tac o (Q.SPECL [‘h’, ‘x’]) ) >>
1577-
gvs[]>>
1578-
1579-
1580-
1581-
res_tac >>
1582-
gvs[]
1583-
QED
1584-
*)
1585-
15861484

15871485
val _ = export_theory ();
15881486

‎hol/policy_to_table/bdd_gen_mergeScript.sml‎

Lines changed: 1 addition & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -2646,56 +2646,6 @@ QED
26462646

26472647

26482648

2649-
(*
2650-
(* nerging a node n with a a list of nodes nl then enduce a valid BDD *)
2651-
Theorem merge_BDD_preserves_valid_and_correctness_verbose:
2652-
∀BDD n nl vars rec.
2653-
2654-
BDD_WF BDD ∧
2655-
BDD_ordered BDD vars ∧
2656-
fv_in_BDD rec BDD vars ∧
2657-
consumed_dom_bdd vars BDD ∧
2658-
correct_sem rec BDD vars ⇒
2659-
2660-
(
2661-
BDD_WF (merge_BDD BDD n nl) ∧
2662-
BDD_ordered (merge_BDD BDD n nl) vars ∧
2663-
fv_in_BDD rec (merge_BDD BDD n nl) vars ∧
2664-
consumed_dom_bdd vars (merge_BDD BDD n nl) ∧
2665-
correct_sem rec (merge_BDD BDD n nl) vars
2666-
)
2667-
Proof
2668-
Induct_on ‘nl’ >-
2669-
(* Base case: empty list *)
2670-
fs [merge_BDD_def] >>
2671-
2672-
(* Inductive case *)
2673-
rpt gen_tac >> strip_tac >>
2674-
fs [merge_BDD_def] >>
2675-
2676-
(* Case analysis on mergable BDD n h *)
2677-
Cases_on ‘mergable BDD n h’ >> gvs[] >|[
2678-
gvs[] >>
2679-
assume_tac merge_correct >>
2680-
first_x_assum (strip_assume_tac o (Q.SPECL [‘BDD’, ‘[]’, ‘vars’, ‘n’, ‘h’, ‘rec’])) >>
2681-
gvs[] >>
2682-
(*res_tac >>*)
2683-
‘BDD_WF (merge BDD n h)’ by imp_res_tac merge_wf_preservation >>
2684-
‘BDD_ordered (merge BDD n h) vars’ by imp_res_tac merge_order_preservation >>
2685-
‘fv_in_BDD rec (merge BDD n h) vars’ by (imp_res_tac merge_fv_final_preservation >>
2686-
first_x_assum (strip_assume_tac o (Q.SPECL [‘h’, ‘n’]))) >>
2687-
‘consumed_dom_bdd vars (merge BDD n h)’ by (imp_res_tac merge_consumed_dom_final_preservation >>
2688-
first_x_assum (strip_assume_tac o (Q.SPECL [‘h’, ‘n’]))) >>
2689-
res_tac >>
2690-
gvs[]
2691-
,
2692-
metis_tac[]
2693-
]
2694-
QED
2695-
*)
2696-
2697-
2698-
26992649
Theorem fv_in_BDD_reverse_triv:
27002650
∀ BDD vars vars_consumed rec.
27012651
fv_in_BDD rec BDD (REVERSE vars ⧺ vars_consumed) ⇒
@@ -2710,51 +2660,7 @@ Proof
27102660
res_tac >>
27112661
fs[fv_in_vars_def]
27122662
QED
2713-
2714-
2715-
(*
2716-
Theorem merge_BDD_preserves_valid_and_correctness:
2717-
∀BDD n nl vars vars_consumed rec.
2718-
valid_BDD rec BDD vars vars_consumed ∧
2719-
correct_sem rec BDD (vars ⧺ vars_consumed) ⇒
2720-
(
2721-
valid_BDD rec (merge_BDD BDD n nl) vars vars_consumed∧
2722-
correct_sem rec (merge_BDD BDD n nl) (vars ⧺ vars_consumed)
2723-
)
2724-
Proof
2725-
Induct_on ‘nl’ >-
2726-
fs [merge_BDD_def] >>
2727-
2728-
rpt gen_tac >> strip_tac >>
2729-
fs [merge_BDD_def] >>
2730-
2731-
Cases_on ‘mergable BDD n h’ >> gvs[] >>
2732-
2733-
gvs[valid_BDD_def] >>
2734-
2735-
assume_tac merge_correct >>
2736-
first_x_assum (strip_assume_tac o (Q.SPECL [‘BDD’, ‘vars’, ‘vars_consumed’,‘n’, ‘h’, ‘rec’])) >>
2737-
gvs[] >>
2738-
2739-
‘fv_in_BDD rec BDD (vars ⧺ vars_consumed)’ by imp_res_tac fv_in_BDD_reverse_triv >>
2740-
2741-
(*res_tac >>*)
2742-
‘BDD_WF (merge BDD n h)’ by imp_res_tac merge_wf_preservation >>
2743-
‘BDD_ordered (merge BDD n h) vars_consumed’ by imp_res_tac merge_order_preservation >>
2744-
2745-
‘consumed_dom_bdd vars_consumed (merge BDD n h)’ by (imp_res_tac merge_consumed_dom_final_preservation >>
2746-
first_x_assum (strip_assume_tac o (Q.SPECL [‘h’, ‘n’]))) >>
2747-
2748-
2749-
‘fv_in_BDD rec (merge BDD n h) (REVERSE vars ⧺ vars_consumed)’ by (imp_res_tac merge_fv_final_preservation >>
2750-
first_x_assum (strip_assume_tac o (Q.SPECL [‘h’, ‘n’]))) >>
2751-
2752-
res_tac >>
2753-
gvs[]
2754-
QED
2755-
*)
2756-
2757-
2663+
27582664

27592665

27602666
val _ = export_theory ();

0 commit comments

Comments
 (0)