Cleanup, fixing typos, adding missing adjustments to symbexec after finishing work on retrofit sem

Author: didriklundberg

hol/p4_exec_semScript.sml

@@ -3358,7 +3358,7 @@ arch_multi_exec uninit (ab_list,pblock_map,ffblock_map,input_f,output_f,copyin_p
           ((i,io_list,io_list',ascope),g_scope_list',
            arch_frame_list_regular frame_list',status_running) ==>
 ?x el pbl_type x_d_list b_func_map decl_list pars_map tbl_map.
- EL i ab_list = arch_block_pbl x el /\
+ oEL i ab_list = SOME $ arch_block_pbl x el /\
  ALOOKUP pblock_map x =
           SOME (pbl_type,x_d_list,b_func_map,decl_list,pars_map,tbl_map)
 Proof
@@ -3409,10 +3409,7 @@ Cases_on ‘x5’ >- (
  ) >>
  gs[AllCaseEqs()]
 ) >>
-gvs[arch_exec_def, AllCaseEqs()] >- (
- metis_tac[listTheory.oEL_EQ_EL]
-) >>
-metis_tac[listTheory.oEL_EQ_EL]
+gvs[arch_exec_def, AllCaseEqs()]
 QED
 
 val _ = export_theory ();

hol/p4_exec_semSyntax.sig

@@ -7,4 +7,9 @@ val dest_arch_multi_exec : term -> term * term * term * term
 val is_arch_multi_exec : term -> bool
 val mk_arch_multi_exec : term * term * int -> term
 
+val dest_match_all_exec : term -> term
+val is_match_all_exec : term -> bool
+val match_all_exec_tm : term
+val mk_match_all_exec : term -> term
+
 end

hol/p4_exec_semSyntax.sml

@@ -8,7 +8,11 @@ open p4_exec_semTheory;
 
 val (arch_multi_exec_tm, _, dest_arch_multi_exec, is_arch_multi_exec) =
   syntax_fns4 "p4_exec_sem" "arch_multi_exec";
+(* TODO: Generalise *)
 val mk_arch_multi_exec =
  (fn (ctx, state, fuel) => (#2 (syntax_fns4 "p4_exec_sem" "arch_multi_exec")) (“uninit_zero”, ctx, state, term_of_int fuel));
 
+val (match_all_exec_tm, mk_match_all_exec, dest_match_all_exec, is_match_all_exec) =
+  syntax_fns1 "p4_exec_sem" "match_all_exec";
+
 end

hol/p4_testLib.sml

@@ -225,7 +225,7 @@ fun the_final_state_hyp_imp_n step_thm =
  let
   val (hyp, step_tm) = dest_imp $ concl step_thm
   val (exec, final_state) = dest_eq step_tm
-  val steps = #3 $ dest_arch_multi_exec exec
+  val steps = #4 $ dest_arch_multi_exec exec
  in
   (hyp, optionSyntax.dest_some final_state, steps)
  end
@@ -235,7 +235,7 @@ fun get_actx step_thm =
  let
   val step_thm_tm = concl step_thm
  in
-  #1 $ dest_arch_multi_exec $ fst $ dest_eq $ 
+  #2 $ dest_arch_multi_exec $ fst $ dest_eq $ 
    (if is_imp step_thm_tm
     then snd $ dest_imp $ step_thm_tm
     else step_thm_tm)