Better simplification of preconditions for eq_lemmas

[ordinarymath]

Looking at the result of eq_lemmas after calling val _ = translation_extends "decProg"; in the front of to_flatProgTheory it seems some theorems stored have unnecessary T in the implication

T ⇒ EqualityType LISP_VALUES_LISP_V_TYPE

Another example of preconditions not being simplified.

    ⊢ T ⇒ EqualityType STRING_TYPE ⇒ EqualityType TERM_TYPE,

      T ⇒
      EqualityType NUM ⇒
      EqualityType STRING_TYPE ⇒
      EqualityType TERM_TYPE ⇒
      EqualityType (LIST_TYPE (PAIR_TYPE STRING_TYPE TERM_TYPE)) ⇒
      EqualityType UPDATE_TYPE

[ordinarymath]

the full list if anyone's interested

[⊢ IsTypeRep AST_EXP_v AST_EXP_TYPE ∧ IsTypeRep (LIST_v (PAIR_v HOL_STRING_v (PAIR_v HOL_STRING_v AST_EXP_v))) (LIST_TYPE (PAIR_TYPE HOL_STRING_TYPE (PAIR_TYPE HOL_STRING_TYPE AST_EXP_TYPE))) ∧ IsTypeRep AST_PAT_v AST_PAT_TYPE ⇒ IsTypeRep AST_DEC_v AST_DEC_TYPE, ⊢ T ⇒ EqualityType AST_AST_T_TYPE ⇒ EqualityType HOL_STRING_TYPE ⇒ EqualityType (LIST_TYPE HOL_STRING_TYPE) ⇒ EqualityType (LIST_TYPE (PAIR_TYPE (LIST_TYPE HOL_STRING_TYPE) (PAIR_TYPE HOL_STRING_TYPE (LIST_TYPE (PAIR_TYPE HOL_STRING_TYPE (LIST_TYPE AST_AST_T_TYPE)))))) ⇒ EqualityType (LIST_TYPE (PAIR_TYPE HOL_STRING_TYPE (PAIR_TYPE HOL_STRING_TYPE AST_EXP_TYPE))) ⇒ EqualityType AST_EXP_TYPE ⇒ EqualityType AST_PAT_TYPE ⇒ EqualityType LOCATION_LOCS_TYPE ⇒ EqualityType AST_DEC_TYPE, ⊢ IsTypeRep AST_LIT_v AST_LIT_TYPE ∧ IsTypeRep AST_PAT_v AST_PAT_TYPE ⇒ IsTypeRep AST_EXP_v AST_EXP_TYPE, ⊢ T ⇒ EqualityType LOCATION_LOCS_TYPE ⇒ EqualityType AST_AST_T_TYPE ⇒ EqualityType (OPTION_TYPE HOL_STRING_TYPE) ⇒ EqualityType AST_LOP_TYPE ⇒ EqualityType AST_OP_TYPE ⇒ EqualityType HOL_STRING_TYPE ⇒ EqualityType (NAMESPACE_ID_TYPE HOL_STRING_TYPE HOL_STRING_TYPE) ⇒ EqualityType (OPTION_TYPE (NAMESPACE_ID_TYPE HOL_STRING_TYPE HOL_STRING_TYPE)) ⇒ EqualityType AST_LIT_TYPE ⇒ EqualityType AST_EXP_TYPE, ⊢ T ⇒ IsTypeRep LOCATION_LOCS_v LOCATION_LOCS_TYPE, ⊢ T ⇒ EqualityType LOCATION_LOCS_TYPE, ⊢ T ⇒ IsTypeRep LOCATION_LOCN_v LOCATION_LOCN_TYPE, ⊢ T ⇒ EqualityType LOCATION_LOCN_TYPE, ⊢ T ⇒ IsTypeRep AST_OP_v AST_OP_TYPE, ⊢ T ⇒ EqualityType AST_THUNK_OP_TYPE ⇒ EqualityType AST_FP_TOP_TYPE ⇒ EqualityType AST_FP_BOP_TYPE ⇒ EqualityType AST_FP_UOP_TYPE ⇒ EqualityType AST_FP_CMP_TYPE ⇒ EqualityType AST_PRIM_TYPE_TYPE ⇒ EqualityType AST_TEST_TYPE ⇒ EqualityType NUM ⇒ EqualityType AST_SHIFT_TYPE ⇒ EqualityType AST_OPW_TYPE ⇒ EqualityType AST_WORD_SIZE_TYPE ⇒ EqualityType AST_OPB_TYPE ⇒ EqualityType AST_OPN_TYPE ⇒ EqualityType AST_OP_TYPE, ⊢ T ⇒ IsTypeRep AST_PRIM_v_v AST_PRIM_TYPE_TYPE, ⊢ T ⇒ EqualityType AST_PRIM_TYPE_TYPE, ⊢ T ⇒ IsTypeRep AST_TEST_v AST_TEST_TYPE, ⊢ EqualityType AST_TEST_TYPE, ⊢ T ⇒ IsTypeRep AST_THUNK_OP_v AST_THUNK_OP_TYPE, ⊢ T ⇒ EqualityType AST_THUNK_OP_TYPE, ⊢ T ⇒ IsTypeRep AST_THUNK_MODE_v AST_THUNK_MODE_TYPE, ⊢ EqualityType AST_THUNK_MODE_TYPE, ⊢ T ⇒ IsTypeRep AST_FP_CMP_v AST_FP_CMP_TYPE, ⊢ EqualityType AST_FP_CMP_TYPE, ⊢ T ⇒ IsTypeRep AST_FP_TOP_v AST_FP_TOP_TYPE, ⊢ EqualityType AST_FP_TOP_TYPE, ⊢ T ⇒ IsTypeRep AST_FP_BOP_v AST_FP_BOP_TYPE, ⊢ EqualityType AST_FP_BOP_TYPE, ⊢ T ⇒ IsTypeRep AST_FP_UOP_v AST_FP_UOP_TYPE, ⊢ EqualityType AST_FP_UOP_TYPE, ⊢ T ⇒ IsTypeRep AST_WORD_SIZE_v AST_WORD_SIZE_TYPE, ⊢ EqualityType AST_WORD_SIZE_TYPE, ⊢ T ⇒ IsTypeRep AST_SHIFT_v AST_SHIFT_TYPE, ⊢ EqualityType AST_SHIFT_TYPE, ⊢ T ⇒ IsTypeRep AST_OPW_v AST_OPW_TYPE, ⊢ EqualityType AST_OPW_TYPE, ⊢ T ⇒ IsTypeRep AST_OPB_v AST_OPB_TYPE, ⊢ EqualityType AST_OPB_TYPE, ⊢ T ⇒ IsTypeRep AST_OPN_v AST_OPN_TYPE, ⊢ EqualityType AST_OPN_TYPE, ⊢ T ⇒ IsTypeRep AST_LOP_v AST_LOP_TYPE, ⊢ EqualityType AST_LOP_TYPE, ⊢ IsTypeRep AST_LIT_v AST_LIT_TYPE ⇒ IsTypeRep AST_PAT_v AST_PAT_TYPE, ⊢ T ⇒ EqualityType (OPTION_TYPE (NAMESPACE_ID_TYPE HOL_STRING_TYPE HOL_STRING_TYPE)) ⇒ EqualityType AST_LIT_TYPE ⇒ EqualityType HOL_STRING_TYPE ⇒ EqualityType AST_PAT_TYPE, ⊢ T ⇒ IsTypeRep AST_AST_T_v AST_AST_T_TYPE, ⊢ T ⇒ EqualityType HOL_STRING_TYPE ⇒ EqualityType AST_AST_T_TYPE, ⊢ IsTypeRep t_'m_v m ∧ IsTypeRep t_'n_v n ⇒ IsTypeRep (NAMESPACE_ID_v t_'m_v t_'n_v) (NAMESPACE_ID_TYPE m n), ⊢ EqualityType m ⇒ EqualityType n ⇒ EqualityType (NAMESPACE_ID_TYPE m n), ⊢ IsTypeRep WORD_v WORD ∧ IsTypeRep WORD_v WORD8 ⇒ IsTypeRep AST_LIT_v AST_LIT_TYPE, ⊢ T ⇒ EqualityType WORD8 ⇒ EqualityType HOL_STRING_TYPE ⇒ EqualityType CHAR ⇒ EqualityType INT ⇒ EqualityType AST_LIT_TYPE, ⊢ T ⇒ IsTypeRep DECPROG_DUMMY_v DECPROG_DUMMY_TYPE, ⊢ EqualityType DECPROG_DUMMY_TYPE, ⊢ IsTypeRep DUMMY_TYPE_REP_v (COMPUTE_EXEC_CV_TYPE --> COMPUTE_EXEC_CV_TYPE) ∧ IsTypeRep DUMMY_TYPE_REP_v (COMPUTE_EXEC_CV_TYPE --> COMPUTE_EXEC_CV_TYPE --> COMPUTE_EXEC_CV_TYPE) ⇒ IsTypeRep COMPUTE_EXEC_CE_v COMPUTE_EXEC_CE_TYPE, ⊢ EqualityType (COMPUTE_EXEC_CV_TYPE --> COMPUTE_EXEC_CV_TYPE --> COMPUTE_EXEC_CV_TYPE) ⇒ EqualityType (COMPUTE_EXEC_CV_TYPE --> COMPUTE_EXEC_CV_TYPE) ⇒ EqualityType NUM ⇒ EqualityType COMPUTE_EXEC_CE_TYPE, ⊢ T ⇒ IsTypeRep COMPUTE_EXEC_CV_v COMPUTE_EXEC_CV_TYPE, ⊢ T ⇒ EqualityType COMPUTE_EXEC_CV_TYPE, ⊢ T ⇒ IsTypeRep COMPUTE_SYNTAX_COMPUTE_EXP_v COMPUTE_SYNTAX_COMPUTE_EXP_TYPE, ⊢ T ⇒ EqualityType COMPUTE_SYNTAX_UOP_TYPE ⇒ EqualityType STRING_TYPE ⇒ EqualityType NUM ⇒ EqualityType COMPUTE_SYNTAX_COMPUTE_EXP_TYPE, ⊢ T ⇒ IsTypeRep COMPUTE_SYNTAX_UOP_v COMPUTE_SYNTAX_UOP_TYPE, ⊢ EqualityType COMPUTE_SYNTAX_UOP_TYPE, ⊢ T ⇒ IsTypeRep COMPUTE_SYNTAX_BINOP_v COMPUTE_SYNTAX_BINOP_TYPE, ⊢ EqualityType COMPUTE_SYNTAX_BINOP_TYPE, ⊢ T ⇒ IsTypeRep LISP_PRINTING_PRETTY_v LISP_PRINTING_PRETTY_TYPE, ⊢ T ⇒ EqualityType BOOL ⇒ EqualityType (LIST_TYPE CHAR) ⇒ EqualityType LISP_PRINTING_PRETTY_TYPE, ⊢ T ⇒ IsTypeRep LISP_VALUES_LISP_V_v LISP_VALUES_LISP_V_TYPE, ⊢ T ⇒ EqualityType LISP_VALUES_LISP_V_TYPE, ⊢ T ⇒ IsTypeRep UPDATE_v UPDATE_TYPE, ⊢ T ⇒ EqualityType NUM ⇒ EqualityType STRING_TYPE ⇒ EqualityType TERM_TYPE ⇒ EqualityType (LIST_TYPE (PAIR_TYPE STRING_TYPE TERM_TYPE)) ⇒ EqualityType UPDATE_TYPE, ⊢ T ⇒ IsTypeRep HOL_EXN_v HOL_EXN_TYPE, ⊢ T ⇒ EqualityType STRING_TYPE ⇒ EqualityType HOL_EXN_TYPE, ⊢ T ⇒ IsTypeRep THM_v THM_TYPE, ⊢ T ⇒ EqualityType (LIST_TYPE TERM_TYPE) ⇒ EqualityType THM_TYPE, ⊢ T ⇒ IsTypeRep TERM_v TERM_TYPE, ⊢ T ⇒ EqualityType STRING_TYPE ⇒ EqualityType TERM_TYPE, ⊢ T ⇒ IsTypeRep TYPE_v TYPE_TYPE, ⊢ T ⇒ EqualityType TYPE_TYPE, ⊢ IsTypeRep (APP_LIST_v t_'a_v) (APP_LIST_TYPE a) ∧ IsTypeRep (LIST_v t_'a_v) (LIST_TYPE a) ⇒ IsTypeRep (APP_LIST_ANN_v t_'a_v) (APP_LIST_ANN_TYPE a), ⊢ EqualityType (APP_LIST_TYPE a) ⇒ EqualityType (LIST_TYPE a) ⇒ EqualityType (APP_LIST_ANN_TYPE a), ⊢ T ⇒ IsTypeRep OUTSTREAM_v OUTSTREAM_TYPE, ⊢ T ⇒ EqualityType OUTSTREAM_TYPE, ⊢ T ⇒ IsTypeRep INSTREAM_v INSTREAM_TYPE, ⊢ T ⇒ EqualityType INSTREAM_TYPE, ⊢ IsTypeRep (BALANCED_MAP_v t_'a_v UNIT_v) (BALANCED_MAP_TYPE a UNIT_TYPE) ∧ IsTypeRep DUMMY_TYPE_REP_v (a --> a --> ORDERING_TYPE) ⇒ IsTypeRep (MLSET_v t_'a_v) (MLSET_TYPE a), ⊢ EqualityType (BALANCED_MAP_TYPE a UNIT_TYPE) ⇒ EqualityType (a --> a --> ORDERING_TYPE) ⇒ EqualityType (MLSET_TYPE a), ⊢ IsTypeRep (BALANCED_MAP_v t_'a_v t_'b_v) (BALANCED_MAP_TYPE a b) ∧ IsTypeRep DUMMY_TYPE_REP_v (a --> a --> ORDERING_TYPE) ⇒ IsTypeRep (MAP_v t_'a_v t_'b_v) (MAP_TYPE a b), ⊢ EqualityType (BALANCED_MAP_TYPE a b) ⇒ EqualityType (a --> a --> ORDERING_TYPE) ⇒ EqualityType (MAP_TYPE a b), ⊢ IsTypeRep t_'k_v k ∧ IsTypeRep t_'w_v w ⇒ IsTypeRep (BALANCED_MAP_v t_'k_v t_'w_v) (BALANCED_MAP_TYPE k w), ⊢ T ⇒ EqualityType k ⇒ EqualityType w ⇒ EqualityType (BALANCED_MAP_TYPE k w), ⊢ EqualityType REAL_TYPE, ⊢ EqualityType RAT_TYPE, ⊢ T ⇒ IsTypeRep RATIONAL_v RATIONAL_TYPE, ⊢ T ⇒ EqualityType INT ⇒ EqualityType RATIONAL_TYPE, ⊢ T ⇒ IsTypeRep DEFAULT_v_v DEFAULT_TYPE_TYPE, ⊢ EqualityType DEFAULT_TYPE_TYPE, ⊢ T ⇒ IsTypeRep PP_DATA_v PP_DATA_TYPE, ⊢ T ⇒ EqualityType BOOL ⇒ EqualityType PP_DATA_TYPE, ⊢ EqualityType UNIT_TYPE, ⊢ IsTypeRep (LIST_v t_'a_v) (LIST_TYPE a) ⇒ IsTypeRep (APP_LIST_v t_'a_v) (APP_LIST_TYPE a), ⊢ EqualityType (LIST_TYPE a) ⇒ EqualityType (APP_LIST_TYPE a), ⊢ IsTypeRep t_'a_v a ∧ IsTypeRep t_'b_v b ⇒ IsTypeRep (SUM_v t_'a_v t_'b_v) (SUM_TYPE a b), ⊢ EqualityType b ⇒ EqualityType a ⇒ EqualityType (SUM_TYPE a b), ⊢ EqualityType b ⇒ EqualityType a ⇒ EqualityType (PAIR_TYPE a b), ⊢ EqualityType a ⇒ EqualityType (LIST_TYPE a), ⊢ T ⇒ IsTypeRep ORDERING_v ORDERING_TYPE, ⊢ EqualityType ORDERING_TYPE, ⊢ IsTypeRep t_'a_v a ⇒ IsTypeRep (OPTION_v t_'a_v) (OPTION_TYPE a), ⊢ EqualityType a ⇒ EqualityType (OPTION_TYPE a), ⊢ EqualityType NUM, ⊢ EqualityType INT, ⊢ EqualityType BOOL, ⊢ EqualityType WORD, ⊢ EqualityType CHAR, ⊢ EqualityType STRING_TYPE, ⊢ EqualityType UNIT_TYPE, ⊢ EqualityType HOL_STRING_TYPE, ⊢ EqualityType WORD, ⊢ EqualityType FLOAT64, ⊢ IsTypeRep NUM_v NUM, ⊢ IsTypeRep INT_v INT, ⊢ IsTypeRep BOOL_v BOOL, ⊢ IsTypeRep CHAR_v CHAR, ⊢ IsTypeRep UNIT_v UNIT_TYPE, ⊢ IsTypeRep STRING_v STRING_TYPE, ⊢ IsTypeRep HOL_STRING_v HOL_STRING_TYPE, ⊢ dimindex (:α) ≤ 64 ⇒ IsTypeRep WORD_v WORD, ⊢ IsTypeRep a_v a ∧ IsTypeRep b_v b ⇒ IsTypeRep (PAIR_v a_v b_v) (PAIR_TYPE a b), ⊢ IsTypeRep a_v a ⇒ IsTypeRep (LIST_v a_v) (LIST_TYPE a), ⊢ IsTypeRep v_a a ⇒ IsTypeRep (VECTOR_v v_a) (VECTOR_TYPE a)]: thm list