Small fixes and cleanup

src/theory/tools/symbexec/birs_rulesScript.sml

@@ -315,6 +315,29 @@ QED
 (* ******************************************************* *)
 (*      SUBST rule                                         *)
 (* ******************************************************* *)
+Theorem symb_rule_SUBST_thm[local]:
+  !sr.
+!sys L sys2 var symbexp symbexp' Pi.
+  (symb_symbols_f_sound sr) ==>
+  (symb_ARB_val_sound sr) ==>
+
+  (symb_hl_step_in_L_sound sr (sys, L, sys2 INSERT Pi)) ==>
+  ((symb_symbst_store sys2) var = SOME symbexp) ==>
+
+  (symb_simplification sr (symb_symbst_pcond sys2) symbexp symbexp') ==>
+
+  (symb_hl_step_in_L_sound sr (sys, L, (symb_symbst_store_update var symbexp' sys2) INSERT (Pi DELETE sys2)))
+Proof
+REPEAT STRIP_TAC >>
+
+`!B.((sys2 INSERT Pi) DIFF {sys2}) UNION {B} = B INSERT (Pi DELETE sys2)` by (
+    fs [] >>
+    METIS_TAC [INSERT_SING_UNION, UNION_COMM, DELETE_DEF]
+  ) >>
+
+  METIS_TAC [symb_rulesTheory.symb_rule_SUBST_thm]
+QED
+
 Theorem symb_rule_SUBST_SING_thm[local]:
   !sr.
 !sys L sys2 var symbexp symbexp'.
@@ -328,17 +351,23 @@ Theorem symb_rule_SUBST_SING_thm[local]:
 
   (symb_hl_step_in_L_sound sr (sys, L, {symb_symbst_store_update var symbexp' sys2}))
 Proof
-REPEAT STRIP_TAC >>
+  REPEAT STRIP_TAC >>
 
-  `({sys2} DIFF {sys2}) UNION {symb_symbst_store_update var symbexp' sys2} = {symb_symbst_store_update var symbexp' sys2}` by (
-    METIS_TAC [pred_setTheory.DIFF_EQ_EMPTY, pred_setTheory.UNION_EMPTY]
-  ) >>
+  METIS_TAC [symb_rule_SUBST_thm, EMPTY_DELETE]
+QED
 
-  METIS_TAC [symb_rulesTheory.symb_rule_SUBST_thm]
+(* TODO: move to bir_symbScript.sml *)
+Theorem birs_symb_to_symbst_IMAGE_DELETE_thm:
+!x s.
+  IMAGE birs_symb_to_symbst s DELETE birs_symb_to_symbst x =
+  IMAGE birs_symb_to_symbst (s DELETE x)
+Proof
+  simp_tac std_ss [EXTENSION, IN_DELETE, IN_IMAGE] >>
+  metis_tac [birs_symb_to_symbst_EXISTS_thm, birs_symb_from_symbst_EXISTS_thm, birs_symb_to_from_symbst_thm]
 QED
 
-Theorem birs_rule_SUBST_spec_thm:
-  !prog bs L bs2 bs2' lbl envl status pcond vn symbexp symbexp'.
+Theorem birs_rule_SUBST_thm:
+  !prog bs L bs2 bs2' lbl envl status pcond vn symbexp symbexp' Pi.
            (bs2 =
              <|bsst_pc := lbl;
                bsst_environ := birs_gen_env ((vn, symbexp)::envl);
@@ -349,26 +378,47 @@ Theorem birs_rule_SUBST_spec_thm:
                bsst_environ := birs_gen_env ((vn, symbexp')::envl);
                bsst_status := status;
                bsst_pcond := pcond|>) ==>
-           birs_symb_exec prog (bs, L, {bs2}) ==>
+           birs_symb_exec prog (bs, L, bs2 INSERT Pi) ==>
            birs_simplification pcond symbexp symbexp' ==>
-           birs_symb_exec prog (bs, L, {bs2'})
+           birs_symb_exec prog (bs, L, bs2' INSERT (Pi DELETE bs2))
 Proof
-  REWRITE_TAC [birs_symb_exec_def] >>
+  REWRITE_TAC [birs_symb_exec_def, IMAGE_INSERT] >>
   REPEAT STRIP_TAC >>
   ASSUME_TAC (
-    (Q.SPECL [`birs_symb_to_symbst bs`, `L`, `birs_symb_to_symbst bs2`, `vn`, `symbexp`, `symbexp'`] o
+    (Q.SPECL [`birs_symb_to_symbst bs`, `L`, `birs_symb_to_symbst bs2`, `vn`, `symbexp`, `symbexp'`, `IMAGE birs_symb_to_symbst Pi`] o
      SIMP_RULE std_ss [bir_symb_soundTheory.birs_symb_ARB_val_sound_thm] o
-     MATCH_MP symb_rule_SUBST_SING_thm o
+     MATCH_MP symb_rule_SUBST_thm o
      Q.SPEC `prog`)
        bir_symb_soundTheory.birs_symb_symbols_f_sound_thm) >>
 
+  FULL_SIMP_TAC std_ss [birs_symb_to_symbst_IMAGE_DELETE_thm] >>
+
   REV_FULL_SIMP_TAC (std_ss++birs_state_ss)
     [IMAGE_SING, birs_symb_to_symbst_def, symb_symbst_store_def, symb_symbst_pcond_def,
      bir_symb_simpTheory.birs_simplification_thm,
      symb_symbst_store_update_def, birs_auxTheory.birs_gen_env_thm,
      combinTheory.UPDATE_APPLY]
 QED
 
+Theorem birs_rule_SUBST_spec_thm:
+  !prog bs L bs2 bs2' lbl envl status pcond vn symbexp symbexp'.
+           (bs2 =
+             <|bsst_pc := lbl;
+               bsst_environ := birs_gen_env ((vn, symbexp)::envl);
+               bsst_status := status;
+               bsst_pcond := pcond|>) ==>
+           (bs2' =
+             <|bsst_pc := lbl;
+               bsst_environ := birs_gen_env ((vn, symbexp')::envl);
+               bsst_status := status;
+               bsst_pcond := pcond|>) ==>
+           birs_symb_exec prog (bs, L, {bs2}) ==>
+           birs_simplification pcond symbexp symbexp' ==>
+           birs_symb_exec prog (bs, L, {bs2'})
+Proof
+  metis_tac [birs_rule_SUBST_thm, EMPTY_DELETE]
+QED
+
 
 
 

src/tools/symbexec/birs_composeLib.sml

@@ -9,6 +9,10 @@ local
 
   open birsSyntax;
   open birs_auxTheory;
+
+  open aux_setLib;
+  open birs_utilsLib;
+
   val birs_state_ss = rewrites (type_rws ``:birs_state_t``);
 
   (* error handling *)
@@ -42,30 +46,14 @@ in
       (fn (al,g) => (print_term g; ([(al,g)], fn ([t]) => t))) >>
       (fn x => (print "starting to compute concrete set of free symbols\n"; ALL_TAC x)) >>
       *)
-      CONV_TAC (LAND_CONV (aux_setLib.varset_INTER_CONV)) >>
+      CONV_TAC (LAND_CONV (varset_INTER_CONV)) >>
 
       REWRITE_TAC [pred_setTheory.EMPTY_SUBSET]
     );
    in
     freesymbols_thm
    end;
 
-  fun tidyup_birs_symb_exec_CONV stateset_conv labelset_conv tm =
-    let
-      val _ = if is_birs_symb_exec tm then () else
-              raise ERR "tidyup_birs_symb_exec_CONV" "cannot handle term";
-
-      val struct_CONV =
-        RAND_CONV;
-      fun Pi_CONV conv =
-        RAND_CONV (RAND_CONV conv);
-      fun L_CONV conv =
-        RAND_CONV (LAND_CONV conv);
-    in
-      (struct_CONV (Pi_CONV stateset_conv) THENC
-       struct_CONV (L_CONV labelset_conv)) tm
-    end;
-
   (*
   val step_A_thm = single_step_A_thm;
   val step_B_thm = single_step_B_thm;
@@ -86,14 +74,17 @@ in
       val _ = print "composed\n";
 
       (* tidy up set operations to not accumulate (in both, post state set and label set) *)
-      val bprog_L_fixed_thm = CONV_RULE (tidyup_birs_symb_exec_CONV aux_setLib.birs_state_DIFF_UNION_CONV aux_setLib.labelset_UNION_CONV) bprog_composed_thm
+      val bprog_fixed_thm = CONV_RULE
+         (birs_Pi_CONV birs_state_DIFF_UNION_CONV THENC
+          birs_L_CONV labelset_UNION_CONV)
+         bprog_composed_thm
         handle e => (print "\n\n"; print_thm bprog_composed_thm; print "tidy up Pi and labelset failed\n"; raise e);
 
-      val _ = if symb_sound_struct_is_normform (concl bprog_L_fixed_thm) then () else
-              (print_term (concl bprog_L_fixed_thm);
+      val _ = if symb_sound_struct_is_normform (concl bprog_fixed_thm) then () else
+              (print_term (concl bprog_fixed_thm);
               raise ERR "birs_rule_SEQ_fun" "something is not right, the produced theorem is not evaluated enough");
     in
-      bprog_L_fixed_thm
+      bprog_fixed_thm
     end;
 
 

src/tools/symbexec/birs_execLib.sml

@@ -255,20 +255,21 @@ fun birs_rule_SUBST_prog_fun bprog_tm =
       ``,
         cheat (* TODO: connect this with prep_thm from above *)
       );*)
-    val inst_thm = SIMP_RULE std_ss [] ((SPEC bprog_tm o INST_TYPE [Type.alpha |-> prog_type]) birs_rule_SUBST_spec_thm);
+    val inst_thm1 = SIMP_RULE std_ss [] ((SPEC bprog_tm o INST_TYPE [Type.alpha |-> prog_type]) birs_rule_SUBST_thm);
+    val inst_thm2 = SIMP_RULE std_ss [] ((SPEC bprog_tm o INST_TYPE [Type.alpha |-> prog_type]) birs_rule_SUBST_spec_thm);
     (*val _ = (print_term o concl) inst_thm;*)
   in
-    inst_thm
+    (inst_thm1,inst_thm2)
   end;
 
 
 (*
-val single_step_prog_thm = result;
+val thm = result;
 *)
-fun birs_rule_SUBST_trysimp_fun birs_rule_SUBST_thm birs_simp_fun single_step_prog_thm =
+fun birs_rule_SUBST_trysimp_SING_fun (_,birs_rule_SUBST_thm) birs_simp_fun thm =
   let
     val assignment_thm_o =
-      SOME (MATCH_MP birs_rule_SUBST_thm single_step_prog_thm)
+      SOME (MATCH_MP birs_rule_SUBST_thm thm)
       handle _ => NONE;
 
     val simp_t_o = Option.mapPartial (fn assignment_thm =>
@@ -286,9 +287,46 @@ fun birs_rule_SUBST_trysimp_fun birs_rule_SUBST_thm birs_simp_fun single_step_pr
   in
     case simp_t_o of
        SOME (simp_t, assignment_thm) => MATCH_MP assignment_thm simp_t
-     | NONE => single_step_prog_thm
+     | NONE => thm
   end;
-val birs_rule_SUBST_trysimp_fun = fn x => Profile.profile "birs_rule_SUBST_trysimp_fun" (birs_rule_SUBST_trysimp_fun x);
+val birs_rule_SUBST_trysimp_SING_fun = fn x => Profile.profile "birs_rule_SUBST_trysimp_SING_fun" (birs_rule_SUBST_trysimp_SING_fun x);
+
+fun birs_rule_SUBST_trysimp_first_fun (birs_rule_SUBST_thm,_) birs_simp_fun thm =
+  let
+    val assignment_thm_o =
+      SOME (MATCH_MP birs_rule_SUBST_thm thm)
+      handle _ => NONE;
+
+    val simp_t_o = Option.mapPartial (fn assignment_thm =>
+      let
+        val simp_tm = (fst o dest_imp o (*snd o strip_binder (SOME boolSyntax.universal) o*) concl o Q.SPEC `symbexp'`) assignment_thm;
+        (*val _ = print_term simp_tm;*)
+    val timer_exec_step_p3 = holba_miscLib.timer_start 0;
+        val simp_t = birs_simp_fun simp_tm;
+        (* TODO: need to remove the following line later and enable the simp function above *)
+        (*val simp_t_o = NONE;*)
+    val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> SUBST in " ^ delta_s ^ "\n")) timer_exec_step_p3;
+      in
+        SOME (simp_t, assignment_thm)
+      end) assignment_thm_o;
+    (* Pi is "bs2' INSERT (Pi DELETE bs2)"*)
+    val cleanup_Pi_conv =
+      let
+        open pred_setLib;
+        open aux_setLib;
+      in
+        RAND_CONV (DELETE_CONV birs_state_EQ_CONV)
+      end;
+    val cleanup_RULE = CONV_RULE (birs_utilsLib.birs_Pi_CONV cleanup_Pi_conv);
+  in
+    case simp_t_o of
+       SOME (simp_t, assignment_thm) => cleanup_RULE (MATCH_MP assignment_thm simp_t)
+     | NONE => thm
+  end;
+val birs_rule_SUBST_trysimp_first_fun = fn x => Profile.profile "birs_rule_SUBST_trysimp_first_fun" (birs_rule_SUBST_trysimp_first_fun x);
+
+(* TODO: check if there is performance difference between this version and the one that applies the single item case, probably don't need special case... *)
+fun birs_rule_SUBST_trysimp_fun x y = birs_utilsLib.birs_Pi_each_RULE (birs_rule_SUBST_trysimp_first_fun x y);
 
 end (* local *)
 

src/tools/symbexec/birs_intervalLib.sml

@@ -198,7 +198,8 @@ in (* local *)
           val _ = print_term (hd refsymbs);
           *)
           val _ = if length refsymbs = 1 then () else
-            raise ERR "birs_intervals_Pi_first_unify_RULE::get_ref_symb" "unexpected";
+            (print "\n\n"; print_term env_symbol; print_term intervaltm_; print "\n\n";
+             raise ERR "birs_intervals_Pi_first_unify_RULE::get_ref_symb" "unexpected");
         in
           hd refsymbs
         end;

src/tools/symbexec/birs_utilsLib.sml

@@ -326,6 +326,8 @@ in (* local *)
       RAND_CONV;
     fun sys_CONV conv =
       LAND_CONV conv;
+    fun L_CONV conv =
+      RAND_CONV (LAND_CONV conv);
     fun Pi_CONV conv =
       RAND_CONV (RAND_CONV conv);
     val first_CONV =
@@ -335,11 +337,13 @@ in (* local *)
 
     local
       open pred_setSyntax;
+      open pred_setTheory;
       val rotate_first_INSERTs_thm = prove(``
         !x1 x2 xs.
         (x1 INSERT x2 INSERT xs) = (x2 INSERT x1 INSERT xs)
       ``,
-        cheat
+        fs [EXTENSION] >>
+        metis_tac []
       );
       fun is_two_INSERTs tm = (is_insert tm) andalso ((is_insert o snd o dest_insert) tm);
     in
@@ -351,8 +355,7 @@ in (* local *)
           val (x2_tm, xs_tm) = dest_insert x2xs_tm;
           val inst_thm = ISPECL [x1_tm, x2_tm, xs_tm] rotate_first_INSERTs_thm;
         in
-          (* TODO: the result of this should actually just be inst_thm *)
-          REWRITE_CONV [Once inst_thm] tm
+          inst_thm
         end;
 
       fun rotate_INSERTs_conv tm =
@@ -364,21 +367,30 @@ in (* local *)
     (* apply state transformer to sys *)
     fun birs_sys_CONV conv tm =
       let
-        val _ = if symb_sound_struct_is_normform tm then () else
-                raise ERR "birs_sys_CONV" "term is not a standard birs_symb_exec";
+        val _ = if is_birs_symb_exec tm then () else
+                raise ERR "birs_sys_CONV" "cannot handle term";
       in
         (struct_CONV (sys_CONV conv)) tm
       end;
 
     (* apply state transformer to Pi *)
     fun birs_Pi_CONV conv tm =
       let
-        val _ = if symb_sound_struct_is_normform tm then () else
-                raise ERR "birs_Pi_CONV" "term is not a standard birs_symb_exec";
+        val _ = if is_birs_symb_exec tm then () else
+                raise ERR "birs_Pi_CONV" "cannot handle term";
       in
         (struct_CONV (Pi_CONV conv)) tm
       end;
 
+    (* apply state transformer to L *)
+    fun birs_L_CONV conv tm =
+      let
+        val _ = if is_birs_symb_exec tm then () else
+                raise ERR "birs_L_CONV" "cannot handle term";
+      in
+        struct_CONV (L_CONV conv) tm
+      end;
+
     (* apply state transformer to first state in Pi *)
     fun birs_Pi_first_CONV conv =
       birs_Pi_CONV (first_CONV conv);