edited the test cases calls according to the last commits and renamings

AnoudAlshnakat · AnoudAlshnakat · commit f981e1e51784 · 2025-12-22T11:20:20.000+01:00
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_10Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_10Script.sml
@@ -437,7 +437,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order); 
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_11Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_11Script.sml
@@ -476,7 +476,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order); 
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_12Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_12Script.sml
@@ -500,7 +500,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
                       
 val _ = export_theory ();
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_13Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_13Script.sml
@@ -530,7 +530,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
                       
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_14Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_14Script.sml
@@ -558,7 +558,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
                       
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_15Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_15Script.sml
@@ -586,7 +586,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
                       
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_16Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_16Script.sml
@@ -614,7 +614,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
                       
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_17Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_17Script.sml
@@ -643,7 +643,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
                       
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_18Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_18Script.sml
@@ -671,7 +671,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
                       
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_19Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_19Script.sml
@@ -692,7 +692,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
                       
 val _ = export_theory ();
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_1Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_1Script.sml
@@ -91,7 +91,7 @@ val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_dstPort
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 val _ = export_theory ();
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_20Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_20Script.sml
@@ -719,7 +719,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
                       
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_2Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_2Script.sml
@@ -174,7 +174,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_3Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_3Script.sml
@@ -217,7 +217,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order); 
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_4Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_4Script.sml
@@ -250,7 +250,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_5Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_5Script.sml
@@ -290,7 +290,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 val _ = export_theory ();
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_6Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_6Script.sml
@@ -318,7 +318,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_7Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_7Script.sml
@@ -339,7 +339,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order); 
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_8Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_8Script.sml
@@ -364,7 +364,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order); 
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 
diff --git a/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_9Script.sml b/hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_9Script.sml
@@ -405,7 +405,7 @@ val policy_full_order = ``[
 
 (* Cakeml sptrees *)
 
-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order); 
+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
 
 
 

Original file line number	Diff line number	Diff line change
@@ -437,7 +437,7 @@ val policy_full_order = ``[
`437`	`437`
`438`	`438`	`(* Cakeml sptrees *)`
`439`	`439`
`440`		`-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
	`440`	`+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
`441`	`441`
`442`	`442`
`443`	`443`
Original file line number	Diff line number	Diff line change
@@ -476,7 +476,7 @@ val policy_full_order = ``[
`476`	`476`
`477`	`477`	`(* Cakeml sptrees *)`
`478`	`478`
`479`		`-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
	`479`	`+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
`480`	`480`
`481`	`481`
`482`	`482`
Original file line number	Diff line number	Diff line change
@@ -530,7 +530,7 @@ val policy_full_order = ``[
`530`	`530`
`531`	`531`	`(* Cakeml sptrees *)`
`532`	`532`
`533`		`-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
	`533`	`+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
`534`	`534`
`535`	`535`
`536`	`536`
Original file line number	Diff line number	Diff line change
@@ -558,7 +558,7 @@ val policy_full_order = ``[
`558`	`558`
`559`	`559`	`(* Cakeml sptrees *)`
`560`	`560`
`561`		`-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
	`561`	`+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
`562`	`562`
`563`	`563`
`564`	`564`
Original file line number	Diff line number	Diff line change
@@ -586,7 +586,7 @@ val policy_full_order = ``[
`586`	`586`
`587`	`587`	`(* Cakeml sptrees *)`
`588`	`588`
`589`		`-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
	`589`	`+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
`590`	`590`
`591`	`591`
`592`	`592`
Original file line number	Diff line number	Diff line change
@@ -614,7 +614,7 @@ val policy_full_order = ``[
`614`	`614`
`615`	`615`	`(* Cakeml sptrees *)`
`616`	`616`
`617`		`-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
	`617`	`+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
`618`	`618`
`619`	`619`
`620`	`620`
Original file line number	Diff line number	Diff line change
@@ -643,7 +643,7 @@ val policy_full_order = ``[
`643`	`643`
`644`	`644`	`(* Cakeml sptrees *)`
`645`	`645`
`646`		`-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
	`646`	`+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
`647`	`647`
`648`	`648`
`649`	`649`
Original file line number	Diff line number	Diff line change
@@ -671,7 +671,7 @@ val policy_full_order = ``[
`671`	`671`
`672`	`672`	`(* Cakeml sptrees *)`
`673`	`673`
`674`		`-val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
	`674`	`+val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);`
`675`	`675`
`676`	`676`
`677`	`677`