Fix remaining stuff

Author: ordinarymath

characteristic/cfMainScript.sml

@@ -55,7 +55,7 @@ Proof
   \\ asm_exists_tac \\ fs []
   \\ once_rewrite_tac [CONJ_COMM] \\ rewrite_tac [GSYM CONJ_ASSOC]
   \\ once_rewrite_tac [CONJ_COMM] \\ rewrite_tac [GSYM CONJ_ASSOC]
-  \\ once_rewrite_tac [EQ_SYM_EQ] \\ fs [evaluateTheory.dec_clock_def]
+  \\ fs [evaluateTheory.dec_clock_def]
   \\ `evaluate (st2 with clock := (ck + ck2 + 1) - 1) env [exp] =
         ((st' with clock := st2.clock) with clock := ck2 + st'.clock,
          Rval [Conv NONE []])` by fs []

pancake/proofs/panItreeSemEquivScript.sml

@@ -121,14 +121,13 @@ Theorem fbs_sem_div_compos_thm:
 Proof
   rpt strip_tac>>
   fs[fbs_semantics_beh_def,Once evaluate_def] >>
-  fs[bool_case_eq]>-
-  rpt (FULL_CASE_TAC>>fs[])>>
-  disj2_tac>>
+  fs[bool_case_eq] >>
+  fs[option_case_eq,pair_case_eq,result_case_eq] >>
   conj_tac>-
    (strip_tac>>first_x_assum $ qspec_then ‘k’ assume_tac>>
     FULL_CASE_TAC>>fs[]>>
     pairarg_tac>>fs[]>>gvs[panPropsTheory.eval_upd_clock_eq,panItreeSemTheory.reclock_def])>>
-  irule lprefix_lubTheory.IMP_build_lprefix_lub_EQ>>
+  rveq >> irule lprefix_lubTheory.IMP_build_lprefix_lub_EQ>>
   conj_asm1_tac>-
    (simp[lprefix_chain_def]>>
     rpt strip_tac>>fs[]>>
@@ -167,13 +166,13 @@ Proof
     simp[Once evaluate_def,
          panItreeSemTheory.reclock_def,
          panPropsTheory.eval_upd_clock_eq]>>
-    pairarg_tac>>fs[]>>
-    qexists_tac ‘k’>>fs[])>>
+    qexists_tac `k` >> fs[] >>
+    pairarg_tac>>fs[])>>
   simp[lprefix_rel_def]>>
   rpt strip_tac>>
   simp[PULL_EXISTS]>>
   simp[LPREFIX_def,from_toList]>>
-  simp[SimpR “isPREFIX”, Once evaluate_def,
+  simp[Once evaluate_def,
        panItreeSemTheory.reclock_def,
        panPropsTheory.eval_upd_clock_eq]>>
   qexists_tac ‘k’>>

translator/ml_optimiseScript.sml

@@ -148,7 +148,7 @@ Triviality BOTTOM_UP_OPT_THM1:
     eval_match_rel s env v (BOTTOM_UP_OPT_PAT f pats) w s1 r)
 Proof
   disch_tac
-  \\ ho_match_mp_tac (fetch "-" "BOTTOM_UP_OPT_ind")
+  \\ ho_match_mp_tac BOTTOM_UP_OPT_ind
   \\ rpt strip_tac
   \\ simp [eval_rel_def |> ONCE_REWRITE_RULE [CONJ_COMM],
            eval_list_rel_def |> ONCE_REWRITE_RULE [CONJ_COMM],
@@ -169,8 +169,6 @@ Proof
          bool_case_eq,option_case_eq,state_component_equality,
          REVERSE_BOTTOM_UP_OPT_LIST]
   \\ TRY (asm_exists_tac \\ fs [state_component_equality] \\ NO_TAC)
-  \\ TRY (qpat_x_assum `(_,_) = _` (assume_tac o GSYM)
-          \\ asm_exists_tac \\ fs [state_component_equality] \\ NO_TAC)
   THEN1 (* Con *)
    (rename1 `_ = (st1,Rval vs)`
     \\ `evaluate (s with clock := ck1) env (REVERSE xs) =
@@ -180,7 +178,7 @@ Proof
     \\ asm_exists_tac \\ fs [])
   THEN1 (* App Eval *)
    (
-    fs [evaluateTheory.do_eval_res_def, Q.ISPEC `(_, _)` EQ_SYM_EQ]
+    fs [evaluateTheory.do_eval_res_def]
     \\ fs [list_case_eq,option_case_eq,bool_case_eq,pair_case_eq,result_case_eq]
     \\ rveq \\ fs [PULL_EXISTS]
     \\ `? st_x ck_x. st' = (st_x with clock := ck_x) /\ st_x.clock = s.clock`
@@ -205,7 +203,7 @@ Proof
           ((st1 with clock := s1.clock) with clock := st1.clock,Rval vs)`
              by fs [state_component_equality]
     \\ first_x_assum drule \\ simp [] \\ strip_tac
-    \\ qpat_x_assum `(_,_) = _` (assume_tac o GSYM)
+    \\ qpat_x_assum `evaluate _ _ _  = (s1 with clock := _ ,_)` assume_tac
     \\ drule evaluate_add_to_clock \\ fs []
     \\ disch_then (qspec_then `ck2' + 1` assume_tac)
     \\ rfs [EVAL ``(dec_clock st1).clock``]
@@ -320,7 +318,7 @@ Proof
     imp_res_tac evaluate_sing \\ rveq \\ fs []
     \\ `? st_x ck_x. st' = (st_x with clock := ck_x) /\ st_x.clock = s.clock`
       by (qexists_tac `st' with clock := s.clock` \\ simp [state_component_equality])
-    \\ fs [Q.ISPEC `(_, _)` EQ_SYM_EQ]
+    \\ fs []
     \\ rpt (first_x_assum drule \\ rw [])
     \\ dxrule_then dxrule evaluate_and_match_clock
     \\ rw []
@@ -332,7 +330,7 @@ Proof
    (imp_res_tac evaluate_sing \\ rveq \\ fs [] \\ rveq \\ fs []
     \\ `? st_x ck_x. st' = (st_x with clock := ck_x) /\ st_x.clock = s.clock`
       by (qexists_tac `st' with clock := s.clock` \\ simp [state_component_equality])
-    \\ fs [Q.ISPEC `(_, _)` EQ_SYM_EQ]
+    \\ fs []
     \\ rpt (first_x_assum drule \\ rw [])
     \\ dxrule_then dxrule evaluate_two_steps_clock
     \\ rw []
@@ -368,7 +366,7 @@ Proof
    )
   THEN1 (* match *)
    (
-    fs [Q.ISPEC `(_, _)` EQ_SYM_EQ, match_result_case_eq]
+    fs [match_result_case_eq]
     \\ fsrw_tac [SATISFY_ss] []
    )
 QED
@@ -398,7 +396,6 @@ Proof
   \\ rveq \\ fs [] \\ rveq \\ fs [do_opapp_def,bool_case_eq,PULL_EXISTS]
   \\ fs [evaluateTheory.dec_clock_def,evaluate_def,abs2let_def]
   \\ qexists_tac `ck1` \\ fs []
-  \\ first_x_assum (assume_tac o SYM) \\ fs []
   \\ drule evaluate_add_to_clock \\ fs []
   \\ disch_then (qspec_then `1` mp_tac) \\ fs []
   \\ `(st' with clock := st'.clock) = st'` by fs [state_component_equality]