Skip to content

Commit b378040

Browse files
tanyongkiamtanyongkiam
authored
Merge pull request #1186 from CakeML/mcandidate-fix
fixes for mcandidate changes
2 parents e1650fc + f8a75d8 commit b378040

File tree

128 files changed

+1303
-1835
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

128 files changed

+1303
-1835
lines changed

‎basis/ArrayProofScript.sml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -182,7 +182,7 @@ Proof
182182
\\ `xv = nv` by fs [NUM_def, INT_def]
183183
\\ instantiate \\ fs [])
184184
\\ xif >- (xret \\ xsimpl \\ `LENGTH rest = 0` by decide_tac \\ fs[] )
185-
\\ fs [NUM_def, INT_def] \\ rfs[])
185+
\\ gvs [NUM_def, INT_def] \\ Cases_on ‘rest’ >> gvs[])
186186
\\ rw[] \\ first_assum match_mp_tac
187187
\\ xlet `POSTv bv. & BOOL (xv = nv) bv * ARRAY av (l_pre ++ rest)`
188188
>- (xapp_spec eq_num_v_thm \\ xsimpl \\ instantiate \\ fs[BOOL_def, NUM_def, INT_def])

‎basis/TextIOProofScript.sml‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5724,8 +5724,7 @@ Theorem inputLines_spec:
57245724
Proof
57255725
Induct_on`splitlines (DROP pos content)` \\ rw[]
57265726
>- (
5727-
qpat_x_assum`[] = _`(assume_tac o SYM) \\ fs[DROP_NIL]
5728-
\\ `LENGTH content - pos = 0` by simp[]
5727+
`LENGTH content - pos = 0` by simp[]
57295728
\\ pop_assum SUBST1_TAC
57305729
\\ `DROP pos content = []` by fs[DROP_NIL]
57315730
\\ rpt strip_tac

‎basis/fsFFIPropsScript.sml‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1037,11 +1037,12 @@ Theorem concat_lines_of:
10371037
Proof
10381038
rw[lines_of_def] \\
10391039
`s = implode (explode s)` by fs [explode_implode] \\
1040-
qabbrev_tac `ls = explode s` \\ pop_assum kall_tac \\ rveq \\
1041-
Induct_on`splitlines ls` \\ rw[] \\
1042-
pop_assum(assume_tac o SYM) \\
1043-
fs[splitlines_eq_nil,concat_cons]
1040+
qabbrev_tac `ls = explode s`
1041+
\\ pop_assum kall_tac \\ rveq \\
1042+
Induct_on`splitlines ls` \\ rw[]
10441043
>- EVAL_TAC \\
1044+
pop_assum(assume_tac o SYM) \\
1045+
fs[splitlines_eq_nil,concat_cons] \\
10451046
imp_res_tac splitlines_next \\ rw[] \\
10461047
first_x_assum(qspec_then`DROP (SUC (LENGTH h)) ls`mp_tac) \\
10471048
rw[] \\ rw[]

‎basis/pure/typeDecToPPScript.sml‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -66,8 +66,6 @@ Definition pp_of_ast_t_def:
6666
pp_of_ast_t fixes (Attup ts) = (Fun "x" (App Opapp
6767
[Var (mod_pp (Short "tuple")); Mat (Var (Short "x"))
6868
[(con_x_i_pat NONE (LENGTH ts), x_i_list_f_apps (MAP (pp_of_ast_t fixes) ts))]]))
69-
Termination
70-
WF_REL_TAC `measure (ast_t_size o SND)`
7169
End
7270

7371
Definition mk_pps_for_type_def:

‎candle/overloading/ml_kernel/ml_hol_kernel_funsProgScript.sml‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -322,10 +322,6 @@ Definition type_compare_def:
322322
(case type_compare t1 t2 of
323323
| Equal => type_list_compare ts1 ts2
324324
| other => other))
325-
Termination
326-
WF_REL_TAC `measure (\x. case x of
327-
INR (x,_) => type1_size x
328-
| INL (x,_) => type_size x)`
329325
End
330326

331327
val type_cmp_thm = Q.prove(

‎candle/overloading/monadic/holKernelProofScript.sml‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2303,10 +2303,9 @@ Triviality first_dup_thm:
23032303
∀ls acc. (first_dup ls acc = NONE) ⇒ ALL_DISTINCT ls ∧ (∀x. MEM x ls ⇒ ¬MEM x acc)
23042304
Proof
23052305
Induct >> simp[Once first_dup_def] >>
2306-
rpt gen_tac >>
2307-
BasicProvers.CASE_TAC >>
2308-
strip_tac >> res_tac >>
2309-
fs[MEM] >> METIS_TAC[]
2306+
rpt (gen_tac ORELSE disch_then strip_assume_tac) >>
2307+
first_x_assum drule >>
2308+
fs[DISJ_IMP_THM,IMP_CONJ_THM,FORALL_AND_THM]
23102309
QED
23112310

23122311
Triviality first_dup_SOME:

‎candle/overloading/semantics/holSemanticsExtraScript.sml‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -678,10 +678,11 @@ Proof
678678
qunabbrev_tac`ls` >>
679679
simp[ALOOKUP_FILTER,Abbr`P`,Abbr`sw`,combinTheory.o_DEF,LAMBDA_PROD] >- (
680680
rw[combinTheory.APPLY_UPDATE_THM,APPLY_UPDATE_LIST_ALOOKUP] >>
681-
qmatch_assum_abbrev_tac`P ⇒ ALOOKUP ls vv = NONE` >>
681+
gvs[]>>
682+
qmatch_assum_abbrev_tac`ALOOKUP ls vv = NONE` >>
682683
Q.ISPECL_THEN[`ls`,`termsem δ γ v sigma`,`z`,`tyr`]mp_tac ALOOKUP_MAP_dest_var >>
683-
impl_tac >- (simp[EVERY_MAP,EVERY_MEM,FORALL_PROD,Abbr`ls`] >> metis_tac[]) >>
684-
rw[] >> fs[Abbr`P`] ) >>
684+
(impl_tac >- (simp[EVERY_MAP,EVERY_MEM,FORALL_PROD,Abbr`ls`] >> metis_tac[]) >>
685+
fs[]))>>
685686
simp[combinTheory.APPLY_UPDATE_THM,APPLY_UPDATE_LIST_ALOOKUP] >>
686687
rw[Abbr`f`] >>
687688
qmatch_assum_abbrev_tac`ALOOKUP ls vv = SOME zz` >>

‎candle/overloading/syntax/holSyntaxExtraScript.sml‎

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -8196,9 +8196,11 @@ Proof
81968196
fs[tyvars_def,MEM_FOLDR_LIST_UNION,EVERY_MEM] >>
81978197
res_tac >>
81988198
Cases_on `Tyvar a = y` >-
8199-
(rveq >> fs[MEM_SPLIT,type_size_def,type1_size_append]) >>
8199+
(rveq >> fs[MEM_SPLIT]>>
8200+
simp[list_size_APPEND]) >>
82008201
res_tac >>
8201-
fs[MEM_SPLIT,type_size_def,type1_size_append]) >>
8202+
fs[MEM_SPLIT,list_size_APPEND]
8203+
) >>
82028204
first_x_assum drule_all >>
82038205
`type_size(TYPE_SUBST s (Tyvar a)) = type_size(TYPE_SUBST s ty)`
82048206
by rw[] >>
@@ -14529,24 +14531,16 @@ Definition tymatch_def:
1452914531
(tymatch (Tyapp c1 a1::ps) (Tyapp c2 a2::obs) sids =
1453014532
if c1=c2 then tymatch (a1++ps) (a2++obs) sids else NONE) ∧
1453114533
(tymatch _ _ _ = NONE)
14532-
Termination
14533-
WF_REL_TAC`measure (λx. type1_size (FST x) + type1_size (FST(SND x)))`
14534-
>> simp[type1_size_append]
1453514534
End
1453614535

14537-
val tymatch_ind = theorem "tymatch_ind";
14538-
1453914536
Definition arities_match_def:
1454014537
(arities_match [] [] ⇔ T) ∧
1454114538
(arities_match [] _ ⇔ F) ∧
1454214539
(arities_match _ [] ⇔ F) ∧
1454314540
(arities_match (Tyapp c1 a1::xs) (Tyapp c2 a2::ys) ⇔
1454414541
((c1 = c2) ⇒ arities_match a1 a2) ∧ arities_match xs ys) ∧
1454514542
(arities_match (_::xs) (_::ys) ⇔ arities_match xs ys)
14546-
Termination
14547-
WF_REL_TAC`measure (λx. type1_size (FST x) + type1_size (SND x))`
1454814543
End
14549-
val arities_match_ind = theorem "arities_match_ind"
1455014544

1455114545
Theorem arities_match_length:
1455214546
∀l1 l2. arities_match l1 l2 ⇒ (LENGTH l1 = LENGTH l2)

‎candle/prover/ast_extrasScript.sml‎

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -54,9 +54,10 @@ Definition every_exp_def[simp]:
5454
(every_exp f e <=> f e)
5555
Termination
5656
WF_REL_TAC `measure (exp_size o SND)`
57-
\\ rw [exp_size_eq, MEM_MAP, EXISTS_PROD]
58-
\\ gvs [MEM_SPLIT, list_size_append, list_size_def,
59-
basicSizeTheory.pair_size_def]
57+
\\ rw [list_size_pair_size_MAP_FST_SND]
58+
\\ drule MEM_list_size
59+
\\ disch_then(qspec_then `exp_size` mp_tac)
60+
\\ simp[]
6061
End
6162

6263
Theorem every_exp_the[simp]:
@@ -79,8 +80,6 @@ Definition every_pat_def[simp]:
7980
every_pat f (Pas p s) = (f (Pas p s) ∧ every_pat f p) ∧
8081
every_pat f (Ptannot p t) = (f (Ptannot p t) ∧ every_pat f p) ∧
8182
every_pat f p = f p
82-
Termination
83-
wf_rel_tac ‘measure (pat_size o SND)’
8483
End
8584

8685
Theorem every_pat_the[simp]:
@@ -107,8 +106,6 @@ Definition every_dec_def[simp]:
107106
EVERY (every_dec f) ds2) /\
108107
(every_dec f d <=>
109108
f d)
110-
Termination
111-
WF_REL_TAC `measure (dec_size o SND)`
112109
End
113110

114111
Definition freevars_def[simp]:
@@ -136,8 +133,6 @@ Definition freevars_def[simp]:
136133
freevars (Tannot x t) = freevars x ∧
137134
freevars (Lannot x l) = freevars x ∧
138135
freevars (FpOptimise fpopt e) = freevars e
139-
Termination
140-
wf_rel_tac ‘measure exp_size’
141136
End
142137

143138
(* Partial applications of closures.

‎candle/prover/compute/compute_evalScript.sml‎

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -241,7 +241,13 @@ Termination
241241
wf_rel_tac ‘measure term_size_alt’ \\ rw []
242242
\\ drule_then assume_tac list_dest_comb_term_size
243243
\\ gs [list_term_size_alt_def, term_size_alt_def]
244-
\\ drule_then assume_tac list_term_size_MEM \\ gs []
244+
\\ pop_assum $ rewrite_tac o single o GSYM
245+
\\ pop_assum mp_tac
246+
\\ qid_spec_tac ‘a’
247+
\\ qid_spec_tac ‘args’
248+
\\ Induct \\ gvs [] \\ rw []
249+
\\ gvs [list_term_size_alt_def]
250+
\\ rw [] \\ res_tac \\ decide_tac
245251
End
246252

247253
(* TODO use term_size and list_size as measure instead *)
@@ -436,7 +442,7 @@ Definition compute_eval_def:
436442
Termination
437443
wf_rel_tac ‘inv_image ($< LEX $<)
438444
(λx. case x of INL (ck,_,cv) => (ck, compute_exp_size cv)
439-
| INR (ck,_,cv) => (ck, compute_exp1_size cv))’
445+
| INR (ck,_,cv) => (ck, list_size compute_exp_size cv))’
440446
End
441447

442448
(* Let and App cases are modified below to get a more useful ind theorem *)
@@ -492,7 +498,7 @@ Definition compute_eval_ind_def:
492498
Termination
493499
wf_rel_tac ‘inv_image ($< LEX $<)
494500
(λx. case x of INL (ck,_,cv) => (ck, compute_exp_size cv)
495-
| INR (ck,_,cv) => (ck, compute_exp1_size cv))’
501+
| INR (ck,_,cv) => (ck, list_size compute_exp_size cv))’
496502
End
497503

498504
val _ = Theory.delete_binding "compute_eval_ind_def"

0 commit comments

Comments
 (0)