decidable_separationLogic/src/decidable_separationLogicLib.sml

455 fun GEN_SWAP_CONV n1 m1 n2 m2 n3 m3 n4 m4 n5 m5 n6 m6 =
457       val argsL = [n1, m1, n2, m2, n3, m3, n4, m4, n5, m5, n6, m6];
895          val n2 = valOf (find_entry 0 e2 cL);
897          SOME (list_mk_comb (``hyp_c_unequal``, [numLib.term_of_int n1, numLib.term_of_int n2]))
976    fun find_pairs_helper P n1 n2 l [] l2 r = r
977    | find_pairs_helper P n1 n2 l (e::l1) [] r =
979    | find_pairs_helper P n1 n2 l (e1::l1) (e2::l2) r =
981             find_pairs_helper P n1 (n2+1) l (e1::l1) l2 ((n1, e1, n2, e2)::r)
983             find_pairs_helper P n1 (n2+1) l (e1::l1) l2 r
991    fun adapt_pair_list_to_deletes___map n1 n2 [] = [] |
992        adapt_pair_list_to_deletes___map n1 n2 ((n1', e1, n2', e2)::l) =
993          let val l' = adapt_pair_list_to_deletes___map n1 n2 l in
994          if (n1 = n1') orelse (n2 = n2') then
998              if n2' > n2 then (n2'-1) else n2', e2)::l'
1002        adapt_pair_list_to_deletes___helper l1 ((n1, e1, n2, e2)::l) =
1003        adapt_pair_list_to_deletes___helper ((n1, e1, n2, e2)::l1) (adapt_pair_list_to_deletes___map n1 n2 l);
1029 fun ds_inference_FRAME___SINGLE_CONV___sf_points_to (n1, sf1, n2, sf2) t =
1035       val thm = ISPECL [e1, numLib.term_of_int n1, a1, numLib.term_of_int n2, a2, c1, c2, pf, sf, pf', sf']
1063 fun ds_inference_FRAME___SINGLE_CONV___sf_ls (n1, sf1, n2, sf2) t =
1068       val thm = ISPECL [f, e1, e2, numLib.term_of_int n1, numLib.term_of_int n2, c1, c2, pf, sf, pf', sf']
1105 fun ds_inference_FRAME___SINGLE_CONV___sf_bin_tree (n1, sf1, n2, sf2) t =
1111       val thm = ISPECL [e1, f11, f12, f21, f22, numLib.term_of_int n1, numLib.term_of_int n2, c1, c2, pf, sf, pf', sf']
1162 fun ds_inference_FRAME___IMPL_CONV___single_step ((n1, x, n2, _),in_thm) =
1168    val thm = ISPECL [x, numLib.term_of_int n1, numLib.term_of_int n2, c1, c2, pf, sf, pf', sf'] INFERENCE_STAR_INTRODUCTION___EVAL2;
1402 fun find_strengthen_uneq_pairs___helper accu n1 n2 pfLorg [] pfL = accu
1403   | find_strengthen_uneq_pairs___helper accu n1 n2 pfLorg ((e1,e2)::cL) [] =
1405   | find_strengthen_uneq_pairs___helper accu n1 n2 pfLorg ((e1,e2)::cL) (pf::pfL) =
1409       if ((e1 = e1') andalso (e2 = e2')) then (n1,n2,false,e1,e2)::accu else
1410       if ((e2 = e1') andalso (e1 = e2')) then (n1,n2,true,e1,e2)::accu else
1413       find_strengthen_uneq_pairs___helper accu' n1 (n2+1) pfLorg ((e1,e2)::cL) pfL
1423 fun ds_inference_PRECONDITION_STRENGTHEN___SINGLE_CONV (n1,n2,turn,e1,e2) t =
1430       val thm = ISPECL [numLib.term_of_int n2, numLib.term_of_int n1, e1, e2, c1, c2, pf, sf, pf', sf'] inf;
1455 fun find_strengthen_eq_pair___helper n1 n2 pfL [] cfL = NONE
1456   | find_strengthen_eq_pair___helper n1 n2 pfL ((e1,e2)::cL) [] =
1458   | find_strengthen_eq_pair___helper n1 n2 pfL ((e1,e2)::cL) ((e1',e2')::cL') =
1463       if cond then SOME (n1, n2, e1, e2) else
1464          find_strengthen_eq_pair___helper n1 (n2+1) pfL ((e1,e2)::cL) cL'
1478       val (n1,n2,e1,e2) = find_strengthen_eq_pair cL pfL handle _ =>
1481       val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, c1, c2, pf, sf, pf', sf']
1511       val (n1,n2,e1,e2) = find_strengthen_eq_precondition cL1 cL2 handle _ =>
1515       val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, c1, c2, pf, sf, pf', sf']
1617          val (n2, uneq) = valOf (find_in_list (is_uneq_2 e1 e3) pfL);
1621          SOME (n, n2, n3, turn, e1, e2,e3, f, a)
1628          val (n2, pointer) = valOf (find_in_list (is_sf_points_to_ex ex) sfL);
1633          SOME (n, n2, ex, e1, e2, f1, f2, a)
1647       val (n1, n2, n3, turn, e1, e2,e3, f, a) = valOf searchOpt;
1649       val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, numLib.term_of_int n3,
1669       val (n, n2, ex, e1, e2, f1, f2, a) = valOf searchOpt;
1670       val thm = ISPECL [numLib.term_of_int n, numLib.term_of_int n2,
1716          val (n2, uneq) = valOf (find_in_list (is_uneq_2 e1 e2) pfL);
1720          SOME (n, n2, turn, e1, e2, f)
1733       val (n, n2, turn, e1, e2, f) = valOf searchOpt;
1735       val thm = ISPECL [numLib.term_of_int n, numLib.term_of_int n2,
1859 fun find_list_append_instance_nil n1 n2 e1 e2 e3 f =
1862       val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, f] INFERENCE_APPEND_LIST___nil___EVAL
1867 fun find_list_append_instance_precond n1 n2 e1 e2 e3 f n3 b1 c1L =
1870       val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, f, e3, numLib.term_of_int n4, numLib.term_of_int n3, if b1 then T else F] INFERENCE_APPEND_LIST___precond___EVAL
1876 fun find_list_append_instance_points_to n1 n2 e1 e2 e3 f n3 b1 sfL =
1881       val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, f, e3, numLib.term_of_int n4, a, numLib.term_of_int n3, if b1 then T else F] INFERENCE_APPEND_LIST___points_to___EVAL
1891 fun find_list_append_instance_tree n1 n2 e1 e2 e3 f n3 b1 pfL sfL =
1905       val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2,
1914 fun find_list_append_instance n2 c1L pfL sfL [] = NONE |
1915     find_list_append_instance n2 c1L pfL sfL (sf'::sfL') =
1920       val thm = find_list_append_instance_nil n1 n2 e1 e2 e3 f handle _ =>
1924                    find_list_append_instance_precond n1 n2 e1 e2 e3 f n3 b1 c1L handle _ =>
1925                    find_list_append_instance_points_to n1 n2 e1 e2 e3 f n3 b1 sfL handle _ =>
1926                    find_list_append_instance_tree n1 n2 e1 e2 e3 f n3 b1 pfL sfL
1930     end handle _ => find_list_append_instance (n2+1) c1L pfL sfL sfL';