Resolve merge conflicts with master

basis/ListProgScript.sml

@@ -218,7 +218,23 @@ end
 
 val result = translate collate_def;
 
-val result = translate ZIP_def;
+Theorem ZIP_ind:
+  ∀P. (∀v. (∀x4 x3 x2 x1. v = (x4::x3,x2::x1) ⇒ P (x3,x1)) ⇒ P v) ⇒ ∀v. P v
+Proof
+  simp [FORALL_PROD] \\ ntac 2 strip_tac \\ Induct \\ rw []
+QED
+
+Theorem ZIP_eq:
+  ZIP x =
+    case x of
+    | (x::xs,y::ys) => (x,y) :: ZIP (xs,ys)
+    | _ => []
+Proof
+  PairCases_on ‘x’ \\ fs [ZIP_def]
+  \\ Cases_on ‘x0’ \\ Cases_on ‘x1’ \\ fs [ZIP_def]
+QED
+
+val result = translate ZIP_eq;
 
 val result = translate MEMBER_def;
 
@@ -251,8 +267,23 @@ val nth_side_def = Q.prove(
   THEN FULL_SIMP_TAC (srw_ss()) [CONTAINER_def])
   |> update_precondition;
 
+Theorem LUPDATE_ind:
+  ∀P. (∀e n. P e n []) ∧ (∀e n x xs. (∀e n. P e n xs) ⇒ P e n (x::xs)) ⇒ ∀e n xs. P e n xs
+Proof
+  ntac 2 strip_tac \\ Induct_on ‘xs’ \\ fs []
+QED
+
+Theorem LUPDATE_eq:
+  LUPDATE e n xs =
+    case xs of
+    | [] => []
+    | y::ys => if n = 0 then e :: ys else y :: LUPDATE e (n-1) ys
+Proof
+  Cases_on ‘xs’ \\ fs [LUPDATE_DEF,PRE_SUB1]
+QED
+
 val _ = next_ml_names := ["update"];
-val result = translate LUPDATE_def;
+val result = translate LUPDATE_eq;
 
 val _ = (next_ml_names := ["compare"]);
 val _ = translate mllistTheory.list_compare_def;

candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml

@@ -559,9 +559,33 @@ val def = (INST_TYPE_def |> SIMP_RULE std_ss [LET_DEF]) |> check [‘theta’] |
 val def = (INST_def |> SIMP_RULE std_ss [LET_DEF]) |> check [‘theta’] |> m_translate
 val def = new_basic_type_definition_def |> check [‘tyname’,‘absname’,‘repname’]  |> m_translate
 
-val def = m_translate axioms_def;
-val def = m_translate types_def;
-val def = m_translate constants_def;
+val _ = ml_prog_update open_local_block;
+
+val def = list_to_hypset_def |> translate
+
+val _ = ml_prog_update open_local_in_block;
+
+Triviality axioms_eq:
+  axioms u = one_CASE u get_the_axioms
+Proof
+  fs [axioms_def]
+QED
+
+Triviality types_eq:
+  types u = one_CASE u get_the_type_constants
+Proof
+  fs [types_def]
+QED
+
+Triviality constants_eq:
+  constants u = one_CASE u get_the_term_constants
+Proof
+  fs [constants_def]
+QED
+
+val def = m_translate axioms_eq;
+val def = m_translate types_eq;
+val def = m_translate constants_eq;
 
 (* The kernel module is closed in subsequent script files:
    ml_hol_kernelProgScript.sml and candle_kernelProgScript.sml *)

compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml

@@ -10,6 +10,7 @@ val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
 val _ = new_theory"ag32_ffi_codeProof";
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
+val _ = temp_delsimps ["DIV_NUMERAL_THM"]
 val _ = diminish_srw_ss ["ABBREV"]
 val _ = set_trace "BasicProvers.var_eq_old" 1
 

compiler/backend/ag32/proofs/ag32_memoryProofScript.sml

@@ -251,7 +251,7 @@ Proof
       \\ fs[] )
   \\ DEP_REWRITE_TAC[ADD_DIV_RWT]
   \\ qspecl_then[`4`,`LENGTH ll`]mp_tac MULT_DIV
-  \\ simp[Abbr`x`] \\ disch_then kall_tac
+  \\ simp[Abbr`x`]
   \\ rewrite_tac[GSYM APPEND_ASSOC]
   \\ DEP_ONCE_REWRITE_TAC[EL_APPEND2]
   \\ simp[]

compiler/backend/proofs/data_to_word_assignProofScript.sml

@@ -14,6 +14,7 @@ val _ = new_theory "data_to_word_assignProof";
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+val _ = temp_delsimps ["DIV_NUMERAL_THM"]
 val _ = diminish_srw_ss ["ABBREV"]
 val _ = set_trace "BasicProvers.var_eq_old" 1
 

compiler/backend/proofs/data_to_word_gcProofScript.sml

@@ -4946,10 +4946,8 @@ QED
 Theorem lookup_adjust_var_fromList2:
    lookup (adjust_var n) (fromList2 (w::ws)) = lookup n (fromList ws)
 Proof
-  full_simp_tac(srw_ss())[lookup_fromList2,EVEN_adjust_var,lookup_fromList]
-  \\ full_simp_tac(srw_ss())[adjust_var_def]
-  \\ once_rewrite_tac [MULT_COMM]
-  \\ full_simp_tac(srw_ss())[GSYM MULT_CLAUSES,MULT_DIV]
+  simp[lookup_fromList2,EVEN_adjust_var,lookup_fromList, adjust_var_def,
+       GSYM ADD1]
 QED
 
 Theorem stack_rel_IMP_size_of_stack:

compiler/backend/proofs/source_evalProofScript.sml

@@ -1343,6 +1343,7 @@ Proof
   )
 QED
 
+Overload shift_seq = “misc$shift_seq”
 Definition do_eval_oracle_def:
   do_eval_oracle (f : compiler_fun) vs (orac : eval_oracle_fun) =
   case vs of

compiler/inference/unifyScript.sml

@@ -12,6 +12,8 @@ open infer_tTheory;
 
 val _ = patternMatchesLib.ENABLE_PMATCH_CASES();
 
+val _ = new_theory "unify";
+
 val option_map_case = Q.prove (
   `!f opt.
     OPTION_MAP f opt =
@@ -20,8 +22,7 @@ val option_map_case = Q.prove (
        | SOME a => SOME (f a)`,
   simp[FUN_EQ_THM] >>
   gen_tac >> Cases >>
-  rw[OPTION_MAP_DEF])
-
+  rw[OPTION_MAP_DEF]);
 
 val option_bind_thm = Q.prove (
 `!x f. OPTION_BIND x f =
@@ -35,8 +36,6 @@ val I_o_f = Q.prove (
 `!m. I o_f m = m`,
 rw [GSYM fmap_EQ_THM]);
 
-val _ = new_theory "unify";
-
 Datatype:
   atom
   = TC_tag type_ident
@@ -57,19 +56,20 @@ val encode_infer_t_def = Define `
 (encode_infer_ts (t::ts) =
   Pair (encode_infer_t t) (encode_infer_ts ts))`;
 
-val decode_infer_t_def = Define `
+Definition decode_infer_t_def:
 (decode_infer_t (Var n) =
   Infer_Tuvar n) ∧
 (decode_infer_t (Const (DB_tag n)) =
   Infer_Tvar_db n) ∧
 (decode_infer_t (Pair (Const Tapp_tag) (Pair (Const (TC_tag tc)) s)) =
   Infer_Tapp (decode_infer_ts s) tc) ∧
+(decode_infer_t _ = Infer_Tuvar 5) ∧
 (decode_infer_ts (Const Null_tag) =
   []) ∧
 (decode_infer_ts (Pair s1 s2) =
   decode_infer_t s1 :: decode_infer_ts s2) ∧
-(decode_infer_t _ = Infer_Tuvar 5) ∧
-(decode_infer_ts _ = [])`;
+(decode_infer_ts _ = [])
+End
 
 Theorem decode_infer_t_pmatch:
     (!t. decode_infer_t t =

examples/cost/cyesProgScript.sml

@@ -104,8 +104,8 @@ QED
          this is copypasted from divScript *)
 
 val REPLICATE_LIST_def = Define `
-  (!l. REPLICATE_LIST l 0 = []) /\
-  (!l n. REPLICATE_LIST l (SUC n) = REPLICATE_LIST l n ++ l)`
+  (REPLICATE_LIST l 0 = []) /\
+  (REPLICATE_LIST l (SUC n) = REPLICATE_LIST l n ++ l)`
 
 Theorem REPLICATE_LIST_SNOC:
   !x n. SNOC x (REPLICATE_LIST [x] n) = REPLICATE_LIST [x] (SUC n)

examples/cost/yesProgScript.sml

@@ -104,8 +104,8 @@ QED
          this is copypasted from divScript *)
 
 val REPLICATE_LIST_def = Define `
-  (!l. REPLICATE_LIST l 0 = []) /\
-  (!l n. REPLICATE_LIST l (SUC n) = REPLICATE_LIST l n ++ l)`
+  (REPLICATE_LIST l 0 = []) /\
+  (REPLICATE_LIST l (SUC n) = REPLICATE_LIST l n ++ l)`
 
 Theorem REPLICATE_LIST_SNOC:
   !x n. SNOC x (REPLICATE_LIST [x] n) = REPLICATE_LIST [x] (SUC n)

examples/divScript.sml

@@ -318,8 +318,8 @@ QED
 (* TODO: Move REPLICATE_LIST and lemmas to an appropriate theory *)
 
 val REPLICATE_LIST_def = Define `
-  (!l. REPLICATE_LIST l 0 = []) /\
-  (!l n. REPLICATE_LIST l (SUC n) = REPLICATE_LIST l n ++ l)`
+  (REPLICATE_LIST l 0 = []) /\
+  (REPLICATE_LIST l (SUC n) = REPLICATE_LIST l n ++ l)`
 
 Theorem REPLICATE_LIST_SNOC:
   !x n. SNOC x (REPLICATE_LIST [x] n) = REPLICATE_LIST [x] (SUC n)

misc/Holmakefile

@@ -8,3 +8,12 @@ README_SOURCES = preamble.sml $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wil
 DIRS = $(wildcard */)
 README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
 	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
+
+EXTRA_CLEANS = cakeml-heap
+
+ifdef POLY
+all: cakeml-heap
+
+cakeml-heap: preamble.uo
+	$(HOLDIR)/bin/buildheap -o $@ $<
+endif

misc/miscScript.sml

@@ -2209,9 +2209,8 @@ Theorem domain_fromList2:
    ∀q. domain(fromList2 q) = set(GENLIST (λx. 2n*x) (LENGTH q))
 Proof
   rw[EXTENSION,domain_lookup,lookup_fromList2,MEM_GENLIST,
-     lookup_fromList,EVEN_EXISTS]
-  \\ rw[EQ_IMP_THM] \\ rename1`2 * m`
-  \\ qspecl_then[`2`,`m`]mp_tac MULT_DIV \\ simp[]
+     lookup_fromList,EVEN_EXISTS, PULL_EXISTS, SF CONJ_ss] \\
+  metis_tac[]
 QED
 
 Theorem UNCURRY_eq_pair:

pancake/proofs/loop_to_wordProofScript.sml

@@ -263,6 +263,7 @@ Proof
   >> ‘2 * k + 2 = (SUC k) * 2’ by fs []
   >> asm_rewrite_tac [MATCH_MP MULT_DIV (DECIDE “0 < 2:num”)]
   >> fs [lookup_fromList]
+  >> rewrite_tac [GSYM ADD1,EL,TL]
 QED
 
 Theorem domain_mk_new_cutset_not_empty:

semantics/Holmakefile

@@ -10,3 +10,7 @@ README_SOURCES = grammar.txt astPP.sml $(wildcard *Script.sml) $(wildcard *Lib.s
 DIRS = $(wildcard */)
 README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
 	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
+
+ifdef POLY
+HOLHEAP = $(CAKEMLDIR)/misc/cakeml-heap
+endif

translator/ml_translatorLib.sml

@@ -2654,45 +2654,14 @@ fun single_line_def def = let
   fun find_def name =
     Theory.current_definitions ()
     |> first (fn (s,_) => s = name) |> snd
-  val curried = find_def "generated_definition_curried_def"
-  val c = curried |> SPEC_ALL |> concl |> dest_eq |> snd |> rand
-  val c2 = curried |> SPEC_ALL |> concl |> dest_eq |> fst
-  val c1 = curried |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator
-  val tupled = find_def "generated_definition_tupled_primitive_def"
   val ind = fetch "-" "generated_definition_ind"
   val tys = ind |> concl |> dest_forall |> fst |> type_of |> dest_type |> snd
   val vv = mk_var("very unlikely name",el 2 tys)
   val ind = ind |> SPEC (mk_abs(mk_var("x",hd tys),vv))
                 |> CONV_RULE (DEPTH_CONV BETA_CONV)
                 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss []))
                 |> GEN vv
-  val cc = tupled |> concl |> dest_eq |> fst
-  val (v,tm) = tupled |> concl |> rand |> rand |> dest_abs
-  val (a,tm) = dest_abs tm
-  val tm = (REWRITE_CONV [GSYM FALSE_def,GSYM TRUE_def] THENC
-            SIMP_CONV std_ss [Once pair_case_def,GSYM curried]) (subst [a|->c,v|->cc] tm)
-           |> concl |> rand |> rand
-  val vs = free_vars tm
-  val goal = mk_eq(mk_CONTAINER c2, mk_CONTAINER tm)
-  val pre_tm =
-    if not (can (find_term is_arb) goal) then T else let
-      val vs = curried |> SPEC_ALL |> concl |> dest_eq |> fst |> dest_args |> tl
-      val pre_tm = pattern_complete def vs
-      in pre_tm end
-  val vs = filter (fn x => not (tmem x vs)) (free_vars goal)
-  val goal = subst (map (fn v => v |-> oneSyntax.one_tm) vs) goal
-  val goal = subst [mk_comb(c1,oneSyntax.one_tm)|->const] goal
-  val goal = mk_imp(pre_tm,goal)
-  val lemma = auto_prove "single_line_def-2" (goal,
-    SIMP_TAC std_ss [FUN_EQ_THM,FORALL_PROD,TRUE_def,FALSE_def] \\ SRW_TAC [] []
-    \\ BasicProvers.EVERY_CASE_TAC
-    \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [def]))
-    \\ SIMP_TAC std_ss [FUN_EQ_THM,FORALL_PROD,TRUE_def,FALSE_def]
-    \\ SRW_TAC [] [LET_THM]
-    \\ CONV_TAC (DEPTH_CONV ETA_CONV)
-    \\ POP_ASSUM MP_TAC \\ REWRITE_TAC [PRECONDITION_def])
-    |> REWRITE_RULE [EVAL (mk_PRECONDITION T)]
-    |> UNDISCH_ALL |> CONV_RULE (BINOP_CONV (REWR_CONV CONTAINER_def))
+  val lemma = DefnBase.one_line_ify NONE def
   in (lemma,SOME ind) end end
   handle HOL_ERR _ => failwith("Preprocessor failed: unable to reduce definition to single line.")
 

translator/ml_translatorScript.sml

@@ -1601,13 +1601,14 @@ end;
 
 (* list definition *)
 
-val LIST_TYPE_def = Define `
-     (LIST_TYPE a (x_2::x_1) v <=>
+Definition LIST_TYPE_def:
+  (LIST_TYPE a (x_2::x_1) v <=>
      ?v2_1 v2_2.
        v = Conv (SOME (TypeStamp "::" 1)) [v2_1; v2_2] /\
        a x_2 v2_1 /\ LIST_TYPE a x_1 v2_2) /\
-     (LIST_TYPE a [] v <=>
-      v = Conv (SOME (TypeStamp "[]" 1)) [])`
+  (LIST_TYPE a [] v <=>
+     v = Conv (SOME (TypeStamp "[]" 1)) [])
+End
 
 val LIST_TYPE_SIMP' = Q.prove(
   `!xs b. CONTAINER LIST_TYPE
@@ -1654,9 +1655,10 @@ QED
 
 (* pair definition *)
 
-val PAIR_TYPE_def = Define `
+Definition PAIR_TYPE_def:
     PAIR_TYPE b c (x_2:'b,x_1:'c) v <=>
-    ?v1_1 v1_2. v = Conv NONE [v1_1; v1_2] /\ b x_2 v1_1 /\ c x_1 v1_2`;
+    ?v1_1 v1_2. v = Conv NONE [v1_1; v1_2] /\ b x_2 v1_1 /\ c x_1 v1_2
+End
 
 val PAIR_TYPE_SIMP = Q.prove(
   `!x. CONTAINER PAIR_TYPE (\y v. if y = FST x then a y v else ARB)