diff --git a/basis/ListProgScript.sml b/basis/ListProgScript.sml index 1c107d4fed..23c188a850 100644 --- a/basis/ListProgScript.sml +++ b/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; diff --git a/candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml b/candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml index b3bcd21216..cbddaffd0f 100644 --- a/candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml +++ b/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 *) diff --git a/compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml b/compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml index e8c7670e32..2e62870b38 100644 --- a/compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml +++ b/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 diff --git a/compiler/backend/ag32/proofs/ag32_memoryProofScript.sml b/compiler/backend/ag32/proofs/ag32_memoryProofScript.sml index 1f43ca825a..35228a5564 100644 --- a/compiler/backend/ag32/proofs/ag32_memoryProofScript.sml +++ b/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[] diff --git a/compiler/backend/proofs/data_to_word_assignProofScript.sml b/compiler/backend/proofs/data_to_word_assignProofScript.sml index 94bc36e9ce..b077a0abaa 100644 --- a/compiler/backend/proofs/data_to_word_assignProofScript.sml +++ b/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 diff --git a/compiler/backend/proofs/data_to_word_gcProofScript.sml b/compiler/backend/proofs/data_to_word_gcProofScript.sml index 449f355804..6c1f10378a 100644 --- a/compiler/backend/proofs/data_to_word_gcProofScript.sml +++ b/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: diff --git a/compiler/backend/proofs/source_evalProofScript.sml b/compiler/backend/proofs/source_evalProofScript.sml index cf8eb2cba7..b6f6c7c5a1 100644 --- a/compiler/backend/proofs/source_evalProofScript.sml +++ b/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 diff --git a/compiler/inference/unifyScript.sml b/compiler/inference/unifyScript.sml index 4d52ed4e70..e06603ac0f 100644 --- a/compiler/inference/unifyScript.sml +++ b/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 = diff --git a/examples/cost/cyesProgScript.sml b/examples/cost/cyesProgScript.sml index 3145b5b9bd..d707403e00 100644 --- a/examples/cost/cyesProgScript.sml +++ b/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) diff --git a/examples/cost/yesProgScript.sml b/examples/cost/yesProgScript.sml index 1a1fa1d317..8f43fdcccb 100644 --- a/examples/cost/yesProgScript.sml +++ b/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) diff --git a/examples/divScript.sml b/examples/divScript.sml index e2b86e88fe..1638234dab 100644 --- a/examples/divScript.sml +++ b/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) diff --git a/misc/Holmakefile b/misc/Holmakefile index 1393f51d0b..f01a823001 100644 --- a/misc/Holmakefile +++ b/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 diff --git a/misc/miscScript.sml b/misc/miscScript.sml index 5aefca0509..f9b8cb85b7 100644 --- a/misc/miscScript.sml +++ b/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: diff --git a/pancake/proofs/loop_to_wordProofScript.sml b/pancake/proofs/loop_to_wordProofScript.sml index d0656ac730..bdbdbc78d9 100644 --- a/pancake/proofs/loop_to_wordProofScript.sml +++ b/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: diff --git a/semantics/Holmakefile b/semantics/Holmakefile index b2cda06e86..72475f54c9 100644 --- a/semantics/Holmakefile +++ b/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 diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml index 36714aa8c6..e33debce3d 100644 --- a/translator/ml_translatorLib.sml +++ b/translator/ml_translatorLib.sml @@ -2654,11 +2654,6 @@ 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) @@ -2666,33 +2661,7 @@ fun single_line_def def = let |> 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.") diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml index bc68cbccbf..003275e514 100644 --- a/translator/ml_translatorScript.sml +++ b/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)