Move some lemmas

Author: hrutvik

language/pure_eval_oldScript.sml

@@ -2,7 +2,7 @@
 open HolKernel Parse boolLib bossLib term_tactic;
 open arithmeticTheory listTheory stringTheory alistTheory
      optionTheory pairTheory ltreeTheory llistTheory bagTheory;
-open pure_expTheory pure_valueTheory pure_limitTheory;
+open pure_expTheory pure_valueTheory pure_limitTheory pure_miscTheory;
 
 val _ = new_theory "pure_eval_old";
 
@@ -1266,22 +1266,6 @@ Proof
   \\ fs[v_rel'_refl]
 QED
 
-Triviality LIST_REL_SYM:
-  (∀x y. R x y ⇔ R y x) ⇒
-  ∀xs ys. LIST_REL R xs ys ⇔ LIST_REL R ys xs
-Proof
-  strip_tac \\ Induct
-  \\ fs [] \\ rw [] \\ eq_tac \\ rw [] \\ fs [] \\ metis_tac []
-QED
-
-Triviality LIST_REL_TRANS:
-  (∀x y z. R x y ∧ R y z ⇒ R x z) ⇒
-  ∀xs ys zs. LIST_REL R xs ys ∧ LIST_REL R ys zs ⇒ LIST_REL R xs zs
-Proof
-  strip_tac \\ Induct
-  \\ fs [] \\ rw [] \\ fs [] \\ rw [] \\ fs [] \\ metis_tac []
-QED
-
 Triviality v_rel'_sym:
   ∀n x y. v_rel' n x y ⇔ v_rel' n y x
 Proof

language/pure_valueScript.sml

@@ -2,7 +2,7 @@
 open HolKernel Parse boolLib bossLib term_tactic;
 open arithmeticTheory listTheory stringTheory alistTheory optionTheory
      ltreeTheory llistTheory quotient_llistTheory
-     pure_configTheory pure_expTheory;
+     pure_configTheory pure_expTheory pure_miscTheory;
 
 val _ = new_theory "pure_value";
 
@@ -104,16 +104,6 @@ Definition Error_def:
   Error = v_abs Error_rep
 End
 
-(*
- * TODO: Move to llist?
- *)
-Theorem LSET_fromList:
-  ∀l. LSET (fromList l) = set l
-Proof
-  Induct \\ rw [fromList_def]
-QED
-
-
 Theorem v_rep_ok_Atom[local]:
   ∀b. v_rep_ok (Atom_rep b)
 Proof
@@ -353,17 +343,6 @@ Proof
   rw [boolTheory.DATATYPE_TAG_THM]
 QED
 
-(* TODO: move to ltreeTheory *)
-Theorem ltree_lookup_APPEND:
-  ∀ path1 path2 t.
-    ltree_lookup t (path1 ++ path2) =
-    OPTION_BIND (ltree_lookup t path1) (λsubtree. ltree_lookup subtree path2)
-Proof
-  Induct >> rw[optionTheory.OPTION_BIND_def] >>
-  Cases_on `t` >> fs[ltree_lookup_def] >>
-  Cases_on `LNTH h ts` >> fs[optionTheory.OPTION_BIND_def]
-QED
-
 Theorem v_rep_ok_ltree_el:
   ∀ vtree subtree.
     v_rep_ok vtree ∧
@@ -590,24 +569,6 @@ Definition make_v_rep_def:
       | (Error', _) => (Error', SOME 0))
 End
 
-(* TODO move to ltreeTheory *)
-Theorem ltree_lookup_SOME_gen_ltree:
-  ∀ path f a ts.
-    ltree_lookup (gen_ltree f) path = SOME (Branch a ts)
-  ⇒ f path = (a, LLENGTH ts)
-Proof
-  Induct >> rw[]
-  >- (
-    Cases_on `f []` >> fs[] >>
-    gvs[Once gen_ltree, ltree_lookup_def]
-    ) >>
-  Cases_on `f []` >> fs[] >> rename1 `f [] = (e1, e2)` >>
-  gvs[Once gen_ltree, ltree_lookup_def] >>
-  fs[LNTH_LGENLIST] >>
-  Cases_on `e2` >> gvs[] >>
-  Cases_on `h < x` >> fs[]
-QED
-
 Triviality v_rep_ok_make_v_rep:
   ∀f. v_rep_ok (make_v_rep f)
 Proof

meta-theory/pure_alpha_equivScript.sml

@@ -7,7 +7,7 @@ open fixedPointTheory arithmeticTheory listTheory stringTheory alistTheory
      BasicProvers pred_setTheory relationTheory rich_listTheory finite_mapTheory
      dep_rewrite;
 open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
-     pure_exp_lemmasTheory pure_limitTheory pure_exp_relTheory;
+     pure_exp_lemmasTheory pure_limitTheory pure_exp_relTheory pure_miscTheory;
 
 val _ = new_theory "pure_alpha_equiv";
 
@@ -743,13 +743,6 @@ Inductive exp_alpha:
                (Letrec (funs1 ++ (y,perm_exp x y e)::funs2) e1))
 End
 
-Triviality MAP_PAIR_MAP:
-  MAP FST (MAP (f ## g) l) = MAP f (MAP FST l) ∧
-  MAP SND (MAP (f ## g) l) = MAP g (MAP SND l)
-Proof
-  rw[MAP_MAP_o,combinTheory.o_DEF,MAP_EQ_f]
-QED
-
 Triviality MAP_PAIR_MAP':
   MAP (λ(x,y). h x) (MAP (f ## g) l) = MAP h (MAP f (MAP FST l)) ∧
   MAP (λ(x,y). h y) (MAP (f ## g) l) = MAP h (MAP g (MAP SND l))
@@ -777,29 +770,6 @@ Proof
   Induct_on ‘l’ >> rw[]
 QED
 
-Theorem closed_subst_freevars:
-  ∀s x y.
-    closed x ∧ closed(subst s x y) ⇒
-    set(freevars y) ⊆ {s}
-Proof
-  rw[] >> pop_assum mp_tac >> drule freevars_subst_single >>
-  disch_then(qspecl_then [‘s’,‘y’] mp_tac) >> rw[] >>
-  gvs[closed_def, DELETE_DEF, SUBSET_DIFF_EMPTY]
-QED
-
-Theorem closed_freevars_subst:
-  ∀s x y.
-    closed x ∧ set(freevars y) ⊆ {s} ⇒
-    closed(subst s x y)
-Proof
-  rw[] >>
-  drule freevars_subst_single >> disch_then (qspecl_then [‘s’,‘y’] mp_tac) >>
-  gvs[DELETE_DEF, closed_def] >> rw[] >>
-  `freevars (subst s x y) = {}` suffices_by gvs[] >>
-  pop_assum SUBST_ALL_TAC >>
-  rw[SUBSET_DIFF_EMPTY]
-QED
-
 Theorem perm1_simps:
   perm1 x y x = y ∧
   perm1 x x y = y ∧
@@ -882,20 +852,6 @@ Proof
   rw[]
 QED
 
-Theorem EVERY2_refl_EQ:
-  LIST_REL R ls ls ⇔ (∀x. MEM x ls ⇒ R x x)
-Proof
-  simp[EQ_IMP_THM,EVERY2_refl] >>
-  Induct_on ‘ls’ >> rw[] >>
-  metis_tac[]
-QED
-
-Theorem MAP_ID_ON:
-  (∀x. MEM x l ⇒ f x = x) ⇒ MAP f l = l
-Proof
-  Induct_on ‘l’ >> rw[]
-QED
-
 Theorem MEM_PERM_IMP:
   MEM x l ⇒
   MEM y (MAP (perm1 x y) l)
@@ -1170,12 +1126,6 @@ Proof
       metis_tac[PAIR,FST,SND])
 QED
 
-Theorem fresh_list:
-  ∀s. FINITE s ⇒ ∃x. x ∉ s:('a list set)
-Proof
-  metis_tac[GSYM INFINITE_LIST_UNIV,NOT_IN_FINITE]
-QED
-
 Theorem exp_alpha_sym:
   ∀e e'.
     exp_alpha e e' ⇒ exp_alpha e' e
@@ -1508,20 +1458,6 @@ Proof
   simp[FORALL_PROD,perm1_simps,perm_exp_id]
 QED
 
-Theorem FDIFF_MAP_KEYS_BIJ:
-  BIJ f 𝕌(:α) 𝕌(:β) ⇒
-  FDIFF (MAP_KEYS f fm) (IMAGE f s) = MAP_KEYS f (FDIFF fm s)
-Proof
-  rpt strip_tac >>
-  simp[FDIFF_def] >>
-  ‘COMPL(IMAGE f s) = IMAGE f (COMPL s)’
-    by(rw[COMPL_DEF,IMAGE_DEF,SET_EQ_SUBSET,SUBSET_DEF] >>
-       gvs[BIJ_DEF,INJ_DEF,SURJ_DEF] >> metis_tac[]) >>
-  pop_assum SUBST_ALL_TAC >>
-  gvs[BIJ_DEF] >>
-  simp[DRESTRICT_MAP_KEYS_IMAGE]
-QED
-
 Theorem exp_alpha_subst_closed:
   ∀x y s e.
     x ≠ y ∧ y ∉ freevars e ∧
@@ -3572,13 +3508,6 @@ Proof
   goal_assum drule >> fs[] >> goal_assum drule >> fs[]
 QED
 
-Triviality LIST_REL_mono:
-  (∀x y. R x y ∧ MEM x xs ∧ MEM y ys ⇒ R1 x y) ==>
-  LIST_REL R xs ys ⇒ LIST_REL R1 xs ys
-Proof
-  qid_spec_tac ‘ys’ \\ Induct_on ‘xs’ \\ fs [] \\ rw []
-QED
-
 Theorem eval_wh_Closure_closed:
   eval_wh e = wh_Closure v body ∧ closed e ⇒ freevars body SUBSET {v}
 Proof

meta-theory/pure_congruenceScript.sml

@@ -8,8 +8,8 @@ open fixedPointTheory arithmeticTheory listTheory stringTheory alistTheory
      BasicProvers pred_setTheory relationTheory rich_listTheory finite_mapTheory
      dep_rewrite;
 open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
-     pure_exp_lemmasTheory pure_limitTheory
-     pure_exp_relTheory pure_alpha_equivTheory;
+     pure_exp_lemmasTheory pure_limitTheory pure_exp_relTheory
+     pure_alpha_equivTheory pure_miscTheory;
 
 val _ = new_theory "pure_congruence";
 
@@ -513,13 +513,6 @@ Proof
   \\ fs [Cus_def,open_bisimilarity_eq]
 QED
 
-Triviality DIFF_SUBSET:
-  a DIFF b ⊆ c ⇔ a ⊆ b ∪ c
-Proof
-  rw[SUBSET_DEF, EXTENSION] >>
-  eq_tac >> rw[] >> metis_tac[]
-QED
-
 Theorem IMP_Howe_Sub: (* 5.5.3 *)
   Ref R ∧ Tra R ∧ Cus R ∧ term_rel R ⇒ Sub (Howe R)
 Proof
@@ -801,19 +794,6 @@ Proof
   \\ fs [closed_def]
 QED
 
-Triviality SUBSET_SINGLETON:
-  x ⊆ {y} ⇒ (x = {y} ∨ x = {})
-Proof
-  rw[EXTENSION, SUBSET_DEF] >>
-  metis_tac[]
-QED
-
-Triviality DISJOINT_DRESTRICT_FEMPTY:
-  ∀m s. DISJOINT s (FDOM m) ⇒ DRESTRICT m s = FEMPTY
-Proof
-  Induct >> rw[]
-QED
-
 Theorem Sub_lift:
   ∀R. Sub R ⇒
     ∀f f' e1 e1' e2 e2' vars.
@@ -901,18 +881,6 @@ Proof
   >- (gvs[] >> metis_tac[UNION_COMM, UNION_ASSOC, INSERT_SING_UNION])
 QED
 
-Triviality UNION_DIFF_DISTRIBUTE:
-  ∀A B C. A ∪ B DIFF C = (A DIFF C) ∪ (B DIFF C)
-Proof
-  rw[EXTENSION] >> metis_tac[]
-QED
-
-Triviality UNION_DIFF_EMPTY:
-  ∀A B C. A ∪ B DIFF C = {} ⇒ B DIFF C = {}
-Proof
-  rw[EXTENSION] >> metis_tac[]
-QED
-
 Triviality closed_Letrec_funs:
   ∀ fs e f.
     closed (Letrec fs e) ∧
@@ -923,12 +891,6 @@ Proof
   gvs[MEM_MAP, PULL_EXISTS]
 QED
 
-Triviality FST_THM:
-  FST = λ(x,y). x
-Proof
-  irule EQ_EXT >> Cases >> simp[]
-QED
-
 Theorem open_similarity_larger:
   ∀vars e1 e2 vars1.
     open_similarity vars e1 e2 ∧ vars SUBSET vars1 ⇒ open_similarity vars1 e1 e2
@@ -1065,38 +1027,6 @@ Proof
   goal_assum drule >> simp[]
 QED
 
-Theorem ALOOKUP_SOME_EL:
-  ∀l k v. ALOOKUP l k = SOME v ⇒ ∃n. n < LENGTH l ∧ EL n l = (k,v)
-Proof
-  Induct >> rw[] >>
-  PairCases_on `h` >> gvs[] >>
-  FULL_CASE_TAC >> gvs[]
-  >- (qexists_tac `0` >> gvs[]) >>
-  first_x_assum drule >> strip_tac >>
-  qexists_tac `SUC n` >> gvs[]
-QED
-
-Theorem ALOOKUP_SOME_EL_2:
-  ∀l1 l2 k (v:'a).
-    ALOOKUP l1 k = SOME v ∧
-    MAP FST l1 = MAP FST l2
-  ⇒ ∃v'. ALOOKUP l2 k = SOME (v':'a) ∧
-      ∃n. n < LENGTH l1 ∧ EL n l1 = (k,v) ∧ EL n l2 = (k,v')
-Proof
-  Induct >> rw[] >>
-  PairCases_on `h` >> gvs[] >>
-  FULL_CASE_TAC >> gvs[]
-  >- (
-    qexists_tac `SND (EL 0 l2)` >>
-    Cases_on `l2` >> gvs[] >> PairCases_on `h` >> gvs[] >>
-    qexists_tac `0` >> gvs[]
-    ) >>
-  first_x_assum drule >> Cases_on `l2` >> gvs[] >>
-  disch_then (qspec_then `t` assume_tac) >> gvs[] >>
-  PairCases_on `h` >> gvs[] >>
-  qexists_tac `SUC n` >> gvs[]
-QED
-
 Theorem Sub_subst_funs:
   ∀R f1 f2 e1 e2.
     Sub R ∧

meta-theory/pure_eval_surjScript.sml

@@ -6,7 +6,8 @@ open HolKernel Parse boolLib bossLib term_tactic BasicProvers dep_rewrite;
 open arithmeticTheory listTheory stringTheory alistTheory optionTheory
      pairTheory ltreeTheory llistTheory bagTheory cardinalTheory
      pred_setTheory rich_listTheory combinTheory finite_mapTheory
-open pure_evalTheory pure_expTheory pure_valueTheory pure_exp_lemmasTheory;
+open pure_evalTheory pure_expTheory pure_valueTheory pure_exp_lemmasTheory
+     pure_miscTheory;
 
 val _ = new_theory "pure_eval_surj";
 
@@ -302,20 +303,6 @@ Proof
   first_x_assum (qspec_then `h::path'` assume_tac) >> gvs[]
 QED
 
-Theorem IS_PREFIX_NOT_EQ:
-  ∀x y.
-    IS_PREFIX x y ∧
-    x ≠ y ⇒
-    LENGTH y < LENGTH x
-Proof
-  rpt strip_tac >>
-  spose_not_then strip_assume_tac >>
-  gvs[NOT_LESS] >>
-  imp_res_tac IS_PREFIX_LENGTH >>
-  ‘LENGTH x = LENGTH y’ by DECIDE_TAC >>
-  metis_tac[IS_PREFIX_LENGTH_ANTI]
-QED
-
 Theorem v_uncountable:
   𝕌(:num -> bool) ≼ 𝕌(:v)
 Proof
@@ -577,14 +564,6 @@ Proof
   Cases_on `path` >> gvs[v_lookup]
 QED
 
-Triviality REPLICATE_11:
-  ∀n m e. REPLICATE n e = REPLICATE m e ⇒ n = m
-Proof
-  Induct >> rw[] >>
-  Cases_on `m` >> gvs[] >>
-  first_x_assum irule >> goal_assum drule
-QED
-
 Theorem cons_names_v_exists_INFINITE:
   ∃v. INFINITE (cons_names_v v)
 Proof