Merge pull request #79 from CakeML/bye-triviality

Replace Triviality by local Theorem

Author: myreen

compiler/backend/languages/properties/env_cexp_lemmasScript.sml

@@ -48,7 +48,7 @@ Proof
   metis_tac[]
 QED
 
-Triviality MAPi_ID[simp]:
+Theorem MAPi_ID[local,simp]:
   ∀l. MAPi (λn v. v) l = l
 Proof
   Induct >> rw[combinTheory.o_DEF]

compiler/backend/languages/relations/pure_presScript.sml

@@ -807,7 +807,7 @@ Proof
     )
 QED
 
-Triviality ALOOKUP_MAP_3':
+Theorem ALOOKUP_MAP_3'[local]:
   ALOOKUP (MAP (λ(k,v1,v2). (k,v1,f v1 v2)) l) =
   OPTION_MAP (λ(v1,v2). (v1, f v1 v2)) o ALOOKUP l
 Proof

compiler/backend/languages/semantics/pureLangScript.sml

@@ -25,7 +25,7 @@ Definition rows_of_def:
       (lets_for cn v (MAPi (λi v. (i,v)) vs) b) (rows_of v k rest)
 End
 
-Triviality list_size_cepat_size_MAPi:
+Theorem list_size_cepat_size_MAPi[local]:
   list_size (λx. cepat_size (SND x)) (MAPi ( λi p. f i, p) ps) = list_size cepat_size ps
 Proof
   Induct_on ‘ps’ using SNOC_INDUCT >> rw[] >>

compiler/backend/languages/semantics/stateLangScript.sml

@@ -692,7 +692,7 @@ Proof
   Induct_on ‘n’ >> rw[step,ADD1,step_n_add]
 QED
 
-Triviality application_Action:
+Theorem application_Action[local]:
   application p vs st k = (Action channel content,st1,k1) ⇒
   p = FFI channel ∧ ∃st1. st = SOME st1
 Proof
@@ -1509,7 +1509,7 @@ Proof
   \\ drule_all step'_append_cont \\ rw [] \\ gvs []
 QED
 
-Triviality step'_not_ForceK1:
+Theorem step'_not_ForceK1[local]:
   v1 ∉ avoid ∧
   step' avoid s k x = (r0,r1,r2) ∧
   (∀ts. x = Val v1 ⇒ k ≠ ForceK1::ts) ⇒
@@ -1544,7 +1544,7 @@ Proof
   \\ gvs [GSYM ADD1, step'_n_def, FUNPOW]
 QED
 
-Triviality step'_n_not_halt_mul:
+Theorem step'_n_not_halt_mul[local]:
   ∀m n avoid x s k.
     (∀k1. ¬is_halt (x,s,k1)) ∧
     (∀k. ∃k1. step'_n n avoid (x,s,k) = (x,s,k1)) ⇒

compiler/backend/passes/env_to_stateScript.sml

@@ -44,7 +44,7 @@ Definition update_delay_def:
         App (UpdateMutThunk NotEvaluated) [Var v; Lam NONE y])
 End
 
-Triviality Letrec_split_MEM_funs:
+Theorem Letrec_split_MEM_funs[local]:
   ∀xs delays funs m n x.
     (delays,funs) = Letrec_split ns xs ∧ MEM (m,n,x) funs ⇒
     cexp_size x ≤ list_size (pair_size mlstring_size cexp_size) xs
@@ -58,7 +58,7 @@ Proof
   \\ Cases_on ‘h1’ \\ gvs [dest_Lam_def,env_cexpTheory.cexp_size_def]
 QED
 
-Triviality Letrec_split_MEM_delays:
+Theorem Letrec_split_MEM_delays[local]:
   ∀xs delays funs m n x.
     (delays,funs) = Letrec_split ns xs ∧ MEM (m,n,x) delays ⇒
     cexp_size x ≤ list_size (pair_size mlstring_size cexp_size) xs

compiler/backend/passes/proofs/env_to_state_2ProofScript.sml

@@ -49,7 +49,7 @@ Proof
   \\ rpt $ first_x_assum $ irule_at Any
 QED
 
-Triviality MEM_explode[simp]:
+Theorem MEM_explode[local,simp]:
   ∀xs x. MEM (explode x) (MAP explode xs) = MEM x xs
 Proof
   Induct \\ fs []
@@ -233,14 +233,14 @@ Proof
   \\ fs []
 QED
 
-Triviality Letrec_imm_0:
+Theorem Letrec_imm_0[local]:
   env_to_state$Letrec_imm ts m ⇒
   (∃v. m = Var v ∧ MEM v ts) ∨ ∃x y. m = Lam x y
 Proof
   Cases_on ‘m’ \\ fs [Letrec_imm_def]
 QED
 
-Triviality Letrec_imm_1:
+Theorem Letrec_imm_1[local]:
   state_unthunkProof$Letrec_imm ts m ⇒
   (∃v. m = Var v ∧ MEM v ts) ∨ ∃x y. m = Lam (SOME x) y
 Proof
@@ -249,7 +249,7 @@ Proof
   \\ fs [state_unthunkProofTheory.Letrec_imm_def]
 QED
 
-Triviality comp_Letrec_neq:
+Theorem comp_Letrec_neq[local]:
   comp_Letrec sfns se ≠ Var v ∧
   comp_Letrec sfns se ≠ Lam m n
 Proof
@@ -261,7 +261,7 @@ Proof
   \\ fs [state_unthunkProofTheory.Lets_def]
 QED
 
-Triviality expand_Case_neq:
+Theorem expand_Case_neq[local]:
   state_caseProof$expand_Case v ses se ≠ Lam x t ∧
   state_caseProof$expand_Case v ses se ≠ False
 Proof
@@ -270,7 +270,7 @@ Proof
   \\ PairCases_on ‘h’ \\ fs [state_caseProofTheory.rows_of_def]
 QED
 
-Triviality rows_of_neq:
+Theorem rows_of_neq[local]:
   rows_of x y z ≠ Lam a b ∧
   rows_of x y z ≠ Var c
 Proof

compiler/backend/passes/proofs/expof_caseProofScript.sml

@@ -273,7 +273,7 @@ Proof
     \\ irule_at Any PAIR)
 QED
 
-Triviality freevars_lets_for':
+Theorem freevars_lets_for'[local]:
   ∀xs n x y.
     freevars (exp_of' p_2) = freevars (exp_of p_2) ⇒
     freevars (lets_for' n x y xs (exp_of' p_2)) =

compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml

@@ -2642,7 +2642,7 @@ Proof
   simp[]
 QED
 
-Triviality find_IfDisj:
+Theorem find_IfDisj[local]:
   find e1 c ∅ ds e2 NONE ⇒
   find (IfDisj s p1 e1) c ∅ ds (IfDisj s p1 e2) NONE
 Proof
@@ -3611,7 +3611,7 @@ QED
 
 (********** Prove that analysis only inserts well-defined Seqs **********)
 
-Triviality empty_map_simps[simp]:
+Theorem empty_map_simps[local,simp]:
   map_ok (empty compare) ∧
   cmp_of (empty compare) = compare ∧
   to_fmap (empty compare) = FEMPTY ∧

compiler/backend/passes/proofs/pure_freshenProofScript.sml

@@ -156,7 +156,7 @@ Proof
   gvs[SUBSET_DEF] >> metis_tac[]
 QED
 
-Triviality boundvars_FOLDR_Let_SUBSET:
+Theorem boundvars_FOLDR_Let_SUBSET[local]:
   boundvars (FOLDR (λ(u,e) A. Let (explode u) e A) acc binds) ⊆
     boundvars acc ∪ IMAGE explode (set (MAP FST binds)) ∪
     BIGUNION (set $ MAP (boundvars o SND) binds)
@@ -200,7 +200,7 @@ Proof
   Induct_on `cnars` >> rw[IfDisj_def, letrecs_distinct_def]
 QED
 
-Triviality ALOOKUP_MAP_3':
+Theorem ALOOKUP_MAP_3'[local]:
   ALOOKUP (MAP (λ(k,v1,v2). (k,v1,f v1 v2)) l) =
   OPTION_MAP (λ(v1,v2). (v1, f v1 v2)) o ALOOKUP l
 Proof
@@ -962,7 +962,7 @@ Proof
   simp[freshen_bind_def, combinTheory.o_DEF, UNCURRY]
 QED
 
-Triviality freshen_aux_list_LENGTH:
+Theorem freshen_aux_list_LENGTH[local]:
   ∀l m avoid l' avoid'.
     freshen_aux_list m l avoid = (l', avoid')
   ⇒ LENGTH l' = LENGTH l
@@ -1640,7 +1640,7 @@ Definition varmap_rel_def:
       FLOOKUP fmap (explode k) = SOME (explode v))
 End
 
-Triviality fresh_boundvar_rel:
+Theorem fresh_boundvar_rel[local]:
   varmap_rel varmap m ∧
   vars_ok avoid ∧
   fresh_boundvar x varmap avoid = ((y,varmap'), avoid')
@@ -1654,14 +1654,14 @@ Proof
   drule_all fresh_boundvar_varmap >> strip_tac >> simp[FLOOKUP_SIMP] >> rw[]
 QED
 
-Triviality ALOOKUP_MAP_explode_FST:
+Theorem ALOOKUP_MAP_explode_FST[local]:
   ALOOKUP (MAP (λ(a,b). (explode a,b)) l) (explode k) = ALOOKUP l k
 Proof
   Induct_on `l` >> rw[] >>
   pairarg_tac >> gvs[]
 QED
 
-Triviality fresh_boundvars_rel:
+Theorem fresh_boundvars_rel[local]:
   ∀xs varmap avoid ys varmap' avoid' m.
   varmap_rel varmap m ∧
   vars_ok avoid ∧

compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml

@@ -355,7 +355,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality NOT_NONE_UNIT:
+Theorem NOT_NONE_UNIT[local]:
   (x ≠ NONE) ⇔ x = SOME ()
 Proof
   Cases_on ‘x’ \\ fs []
@@ -629,7 +629,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality App_Lam_to_Lets_allvars:
+Theorem App_Lam_to_Lets_allvars[local]:
   App_Lam_to_Lets exp = SOME exp1 ⇒
   allvars (exp_of exp) = allvars (exp_of exp1)
 Proof
@@ -655,7 +655,7 @@ Proof
   \\ res_tac \\ fs []
 QED
 
-Triviality MAP2_lemma:
+Theorem MAP2_lemma[local]:
   ∀vbs vbs1.
     LENGTH vbs = LENGTH vbs1 ⇒
     MAP FST (MAP2 (λ(v,_) x. (v,x)) vbs vbs1) = MAP FST vbs ∧
@@ -832,7 +832,7 @@ Definition wf_mem_def:
                cexp_wf ce ∧ letrecs_distinct (exp_of ce)
 End
 
-Triviality BIGUNION_set_SUBSET:
+Theorem BIGUNION_set_SUBSET[local]:
   BIGUNION (set xs) ⊆ z ⇔ EVERY (λx. x ⊆ z) xs
 Proof
   Induct_on ‘xs’ \\ gvs []
@@ -847,7 +847,7 @@ Proof
   \\ gvs [AC UNION_COMM UNION_ASSOC]
 QED
 
-Triviality cexp_Lets_append:
+Theorem cexp_Lets_append[local]:
   ∀xs ys x. Lets a (xs ++ ys) x = Lets a xs (Lets a ys x)
 Proof
   Induct \\ gvs [Lets_def,FORALL_PROD]
@@ -946,7 +946,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality freevars_Disj:
+Theorem freevars_Disj[local]:
   freevars (Disj v xs) ⊆ {v}
 Proof
   Induct_on ‘xs’ \\ gvs [Disj_def]
@@ -970,7 +970,7 @@ Proof
   metis_tac[avoid_set_ok_subset]
 QED
 
-Triviality App_Lam_to_Lets_avoid_set_ok:
+Theorem App_Lam_to_Lets_avoid_set_ok[local]:
   App_Lam_to_Lets e = SOME e' ⇒
   avoid_set_ok vars e = avoid_set_ok vars e'
 Proof
@@ -1627,7 +1627,7 @@ Proof
   dxrule_all freshen_global_boundvars >> simp[]
 QED
 
-Triviality freshen_cexp_disjoint_lemma:
+Theorem freshen_cexp_disjoint_lemma[local]:
   freshen_cexp e ns = (e1,ns1) ∧ avoid_set_ok ns e ∧
   cexp_wf e ∧ NestedCase_free e ∧ letrecs_distinct (exp_of e) ∧
   s ⊆ set_of ns
@@ -1647,7 +1647,7 @@ Proof
   \\ gvs [cexp_wf_def]
 QED
 
-Triviality if_lemma:
+Theorem if_lemma[local]:
   boundvars (if b then Seq Fail x else x) = boundvars x ∧
   barendregt (if b then Seq Fail x else x) = barendregt x ∧
   letrecs_distinct (if b then Seq Fail x else x) = letrecs_distinct x
@@ -1666,7 +1666,7 @@ Proof
   rw [] \\ irule inline_rel_Prim \\ gvs [inline_rel_refl]
 QED
 
-Triviality inline_rel_rows_of:
+Theorem inline_rel_rows_of[local]:
   ∀xs1 ys1.
     inline_rel xs x y ∧
     MAP FST xs1 = MAP FST ys1 ∧