Merge remote-tracking branch 'origin/develop' into probability_dev

binghe · Sep 29, 2023 · 306cde7 · 306cde7
2 parents 0f242ef + 491f509
commit 306cde7
Show file tree

Hide file tree

Showing 22 changed files with 390 additions and 467 deletions.
diff --git a/examples/algebra/lib/jcLib.sml b/examples/algebra/lib/jcLib.sml
@@ -19,7 +19,4 @@ fun stripDup ths =
            disch_then (fn th => strip_assume_tac th >>
                                 strip_assume_tac (REWRITE_RULE ths th))]
 
-val _ = Feedback.set_trace "Theory.allow_rebinds" 1
-
-
 end
diff --git a/examples/computability/kolmog/boolListsScript.sml b/examples/computability/kolmog/boolListsScript.sml
@@ -1243,7 +1243,7 @@ Proof
        rw[primrec_rules, primrec_pr_nblsnd0, primrec_ell])
 QED
 
-Theorem checkpair_i_def[simp] = new_specification(
+Theorem checkpair_i_def[simp,allow_rebind] = new_specification(
   "checkpair_i_def", ["checkpair_i"],
   MATCH_MP unary_rec_fns_phi recfn_checkpair)
 

diff --git a/examples/computability/kolmog/kraft_ineqScript.sml b/examples/computability/kolmog/kraft_ineqScript.sml
@@ -360,12 +360,12 @@ Proof
   Cases_on‘y=e’>> fsr[] >> RES_TAC >> fsr[]
 QED
 
-Theorem maxr_set_def = new_specification(
+val maxr_set_def = new_specification(
   "maxr_set_def",["maxr_set"],
   SIMP_RULE(srw_ss() )[SKOLEM_THM,GSYM RIGHT_EXISTS_IMP_THM] max_rs_lemma
   );
 
-Theorem minr_set_def = new_specification(
+val minr_set_def = new_specification(
   "minr_set_def",["minr_set"],
   SIMP_RULE(srw_ss() )[SKOLEM_THM,GSYM RIGHT_EXISTS_IMP_THM] min_rs_lemma);
 

diff --git a/examples/computability/turing/turing_machine_primeqScript.sml b/examples/computability/turing/turing_machine_primeqScript.sml
@@ -1200,10 +1200,6 @@ rpt strip_tac >> qexists_tac`Cn (pr2 nel) [proj 0;Cn (pr1 (list_rec_comb c n)) [
 rpt conj_tac >- (rpt (irule primrec_cn >> rw[primrec_rules,primrec_nel,primrec_list_rec_comb]))>>
  simp[list_rec_comb_def] >> simp[list_rec_comb_corr,nel_nlist_of,LIST_REC_def] )
 
-val nleng_thm = new_specification("nleng_def", ["nleng"],
-list_num_rec_thm |> SPECL[``0n``,``Cn succ [proj 2]``]
-                 |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules])
-
 val nrev_thm = new_specification("nrev_def", ["nrev"],
 list_num_rec_thm |> SPECL[``0n``,``Cn (pr2 napp) [proj 2;Cn (pr2 ncons) [proj 0;zerof] ]``]
                  |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules])
@@ -1270,12 +1266,6 @@ val primrec_pr_INITIAL_TAPE_TM_NUM = Q.store_thm(
        rw[primrec_rules,primrec_pr_eq,primrec_nsnd,primrec_nfst]) >>
   fs[primrec_proj]);
 
-val pr_INITIAL_TM_NUM_def = Define`
-pr_INITIAL_TM_NUM = Cn (pr2 npair) [zerof;Cn tape_encode
- [Cn (pr1 nfst) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]];
-  Cn (pr1 nfst) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]];
-  Cn (pr1 nsnd) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]]]]`;
-
 val pr_ODD_def = Define`pr_ODD = pr_cond (Cn pr_eq [Cn pr_mod [proj 0;twof];onef]) onef zerof`
 
 val pr_ODD_corr = Q.store_thm("pr_ODD_corr",
@@ -1490,7 +1480,6 @@ Cases_on `A` >> fs[])
 val recfn_rulesl = CONJUNCTS recfn_rules
 val recfnCn = save_thm("recfnCn", List.nth(recfn_rulesl, 3))
 val recfnPr = save_thm("recfnPr", List.nth(recfn_rulesl, 4))
-val recfnMin = save_thm("recfnMin", List.nth(recfn_rulesl, 5))
 
 (* Probably need to include a 'tape reset' type function, ie tm_return_num *)
 val recfn_tm_def = Define`

diff --git a/examples/decidable_separationLogic/src/decidable_separationLogicLibScript.sml b/examples/decidable_separationLogic/src/decidable_separationLogicLibScript.sml
@@ -1341,47 +1341,23 @@ REPEAT STRIP_TAC THEN (
 
 
 
-val INFERENCE_STAR_INTRODUCTION___EVAL1 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL1",
- ``!sfL'' c1 c2 pfL sfL pfL' sfL'.
-         (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==>
-         LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL''))``,
-
-
-REPEAT STRIP_TAC THEN
-`LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') =
- LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')` by (
-   MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN
-   SIMP_TAC std_ss [PERM_REFL, PERM_APPEND]
-) THEN
-ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
-
-Induct_on `sfL''` THENL [
-   ASM_SIMP_TAC list_ss [],
-   ASM_SIMP_TAC list_ss [INFERENCE_STAR_INTRODUCTION___IMPL]
-])
-
-
-
-
-val INFERENCE_STAR_INTRODUCTION___EVAL1 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL1",
- ``!sfL'' c1 c2 pfL sfL pfL' sfL'.
-         (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==>
-         LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL''))``,
-
-
-REPEAT STRIP_TAC THEN
-`LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') =
- LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')` by (
-   MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN
-   SIMP_TAC std_ss [PERM_REFL, PERM_APPEND]
-) THEN
-ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
-
-Induct_on `sfL''` THENL [
+Theorem INFERENCE_STAR_INTRODUCTION___EVAL1:
+ !sfL'' c1 c2 pfL sfL pfL' sfL'.
+   LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==>
+   LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'')
+Proof
+  REPEAT STRIP_TAC THEN
+  ‘LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') =
+   LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')’
+    by (MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN
+        SIMP_TAC std_ss [PERM_REFL, PERM_APPEND]
+       ) THEN
+  ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
+  Induct_on ‘sfL''’ THENL [
    ASM_SIMP_TAC list_ss [],
    ASM_SIMP_TAC list_ss [INFERENCE_STAR_INTRODUCTION___IMPL]
-])
-
+  ]
+QED
 
 val INFERENCE_STAR_INTRODUCTION___EVAL2 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL2",
  ``!x n1 n2 c1 c2 pfL sfL pfL' sfL'.

diff --git a/examples/formal-languages/regular/regexpScript.sml b/examples/formal-languages/regular/regexpScript.sml
@@ -130,15 +130,15 @@ Datatype
     | Neg regexp`
 ;
 
-Theorem regexp_induction :
+Theorem regexp_induction[allow_rebind] :
  !P Q.
      (!cs. P (Chset cs)) /\
      (!r r0. P r /\ P r0 ==> P (Cat r r0)) /\
      (!r. P r ==> P (Star r)) /\ (!l. Q l ==> P (Or l)) /\
      (!r. P r ==> P (Neg r)) /\ Q [] /\ (!r l. P r /\ Q l ==> Q (r::l)) ==>
      (!r. P r) /\ !l. Q l
 Proof
- ACCEPT_TAC (fetch "-" "regexp_induction")
+  ACCEPT_TAC (fetch "-" "regexp_induction")
 QED
 
 Triviality regexp_distinct = fetch "-" "regexp_distinct";

diff --git a/examples/fun-op-sem/cbv-lc/logrelScript.sml b/examples/fun-op-sem/cbv-lc/logrelScript.sml
@@ -119,7 +119,7 @@ val state_rel_rw =
 Theorem state_rel_rw = state_rel_rw
 
 (* Convert the if-then-else to ⇒ *)
-Theorem val_rel_def = SIMP_RULE (srw_ss()) [] val_rel_def
+Theorem val_rel_def[allow_rebind] = SIMP_RULE (srw_ss()) [] val_rel_def
 
 (* Package up exec_rel nicely in terms of res_rel. *)
 Theorem exec_rel_rw:

diff --git a/examples/fun-op-sem/ml/typeSoundScript.sml b/examples/fun-op-sem/ml/typeSoundScript.sml
@@ -280,8 +280,9 @@ val sem_clock = store_thm("sem_clock",
 val r = term_rewrite [``check_clock s1 s = s1``,
     ``s.clock <> 0 /\ s1.clock <> 0 <=> s1.clock <> 0``]
 
-val sem_def = store_thm("sem_def",
-  sem_def |> concl |> r,
+Theorem sem_def[allow_rebind]:
+  ^(sem_def |> concl |> r)
+Proof
   rpt strip_tac >>
   rw[Once sem_def] >>
   BasicProvers.CASE_TAC >>
@@ -294,10 +295,12 @@ val sem_def = store_thm("sem_def",
   imp_res_tac sem_clock >>
   simp[check_clock_id] >>
   `F` suffices_by rw[] >>
-  DECIDE_TAC)
+  DECIDE_TAC
+QED
 
-val sem_ind = store_thm("sem_ind",
-  sem_ind |> concl |> r,
+Theorem sem_ind[allow_rebind]:
+  ^(sem_ind |> concl |> r)
+Proof
   ntac 2 strip_tac >>
   ho_match_mp_tac sem_ind >>
   rw[] >>
@@ -306,7 +309,8 @@ val sem_ind = store_thm("sem_ind",
   res_tac >>
   imp_res_tac sem_clock >>
   fsrw_tac[ARITH_ss][check_clock_id] >> rfs[] >>
-  fsrw_tac[ARITH_ss][check_clock_id])
+  fsrw_tac[ARITH_ss][check_clock_id]
+QED
 
 (* alternative un-clocked relational big-step semantics for comparison *)
 

diff --git a/examples/l3-machine-code/arm/decompiler/arm_decomp_demoScript.sml b/examples/l3-machine-code/arm/decompiler/arm_decomp_demoScript.sml
@@ -283,7 +283,6 @@ val (PID_C2_cert, PID_C2_def) = core_decompilerLib.core_decompile "PID_C2" `
     edc37a00             (* vstr       s15, [r3]                *)
     e8bd0010             (* pop        {r4}                     *)`;
 
-val _ = save_thm("PID_C2_def",PID_C2_def);
 val _ = save_thm("PID_C2_cert",PID_C2_cert);
 
 val () = export_theory()
diff --git a/examples/l3-machine-code/m0/step/m0_stepScript.sml b/examples/l3-machine-code/m0/step/m0_stepScript.sml
@@ -741,13 +741,6 @@ val Decode_simps = save_thm("Decode_simps",
                      blastLib.BBLAST_CONV ``v2w [a; b; c] = ^w``
                   end)) |> Drule.LIST_CONJ);
 
-val Shift_C_LSL_rwt = Q.store_thm("Shift_C_LSL_rwt",
-   `!imm2 w C s.
-        Shift_C (w: word32, SRType_LSL, imm2, C) s =
-        ((w << imm2, if imm2 = 0 then C else testbit 32 (shiftl (w2v w) imm2)),
-         s)`,
-   lrw [Shift_C_def, LSL_C_def, bitstringTheory.shiftl_replicate_F])
-
 local
    val lem =
     (SIMP_RULE (srw_ss()) [] o Q.SPECL [`v`, `32`] o

diff --git a/examples/l3-machine-code/x64/decompiler/x64_decomp_demoScript.sml b/examples/l3-machine-code/x64/decompiler/x64_decomp_demoScript.sml
@@ -38,7 +38,10 @@ val _ = save_thm("decomp_cert",decomp_cert);
 
 val () = Feedback.set_trace "x64 spec" 2
 
-val (decomp1_cert,decomp1_def) = x64_decompLib.x64_decompile "decomp1" `
+val (decomp1_cert,decomp1_def) =
+  Feedback.trace ("Theory.allow_rebinds", 1)
+     (x64_decompLib.x64_decompile "decomp1")
+  ‘
   (*  0: *) 55              (* push   %rbp *)
   (*  1: *) 4889e5          (* mov    %rsp,%rbp *)
   (*  4: *) 4883ec20        (* sub    $0x20,%rsp *)
@@ -62,7 +65,7 @@ val (decomp1_cert,decomp1_def) = x64_decompLib.x64_decompile "decomp1" `
   (* 3b: *) 84c0            (* test   %al,%al *)
   (* 3d: *) 75d7            (* jne    16 <transform+0x16> *)
   (* 3f: *) 488b45e8        (* mov    -0x18(%rbp),%rax *)
-  (* 43: *) c9              (* leaveq  *) `
+  (* 43: *) c9              (* leaveq  *) ’
 
 val _ = save_thm("decomp1_cert",decomp1_cert);
 

diff --git a/examples/lambda/Holmakefile b/examples/lambda/Holmakefile
@@ -1,2 +1,2 @@
 CLINE_OPTIONS = -r
-INCLUDES = barendregt basics other-models typing wcbv-reasonable
+INCLUDES = barendregt basics other-models typing wcbv-reasonable examples