1102 List.concat supp_thms))))), |
1102 List.concat supp_thms))))), |
1103 length new_type_names)) |
1103 length new_type_names)) |
1104 end) atoms; |
1104 end) atoms; |
1105 |
1105 |
1106 val simp_atts = replicate (length new_type_names) [Simplifier.simp_add]; |
1106 val simp_atts = replicate (length new_type_names) [Simplifier.simp_add]; |
|
1107 val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, EqvtRules.eqvt_add]; |
1107 |
1108 |
1108 val (_, thy9) = thy8 |> |
1109 val (_, thy9) = thy8 |> |
1109 Theory.add_path big_name |> |
1110 Theory.add_path big_name |> |
1110 PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] ||>> |
1111 PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] ||>> |
1111 PureThy.add_thmss [(("inducts_weak", projections dt_induct), [case_names_induct])] ||> |
1112 PureThy.add_thmss [(("inducts_weak", projections dt_induct), [case_names_induct])] ||> |
1112 Theory.parent_path ||>> |
1113 Theory.parent_path ||>> |
1113 DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>> |
1114 DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>> |
1114 DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>> |
1115 DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>> |
1115 DatatypeAux.store_thmss_atts "perm" new_type_names simp_atts perm_simps' ||>> |
1116 DatatypeAux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>> |
1116 DatatypeAux.store_thmss "inject" new_type_names inject_thms ||>> |
1117 DatatypeAux.store_thmss "inject" new_type_names inject_thms ||>> |
1117 DatatypeAux.store_thmss "supp" new_type_names supp_thms ||>> |
1118 DatatypeAux.store_thmss "supp" new_type_names supp_thms ||>> |
1118 DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||> |
1119 DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||> |
1119 fold (fn (atom, ths) => fn thy => |
1120 fold (fn (atom, ths) => fn thy => |
1120 let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom) |
1121 let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom) |