55 val Suml_name = "Datatype.Suml"; |
55 val Suml_name = "Datatype.Suml"; |
56 val Sumr_name = "Datatype.Sumr"; |
56 val Sumr_name = "Datatype.Sumr"; |
57 |
57 |
58 val [In0_inject, In1_inject, Scons_inject, Leaf_inject, |
58 val [In0_inject, In1_inject, Scons_inject, Leaf_inject, |
59 In0_eq, In1_eq, In0_not_In1, In1_not_In0, |
59 In0_eq, In1_eq, In0_not_In1, In1_not_In0, |
60 Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o rpair NONE) |
60 Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o Name) |
61 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", |
61 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", |
62 "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", |
62 "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", |
63 "Lim_inject", "Suml_inject", "Sumr_inject"]; |
63 "Lim_inject", "Suml_inject", "Sumr_inject"]; |
64 |
64 |
65 val descr' = List.concat descr; |
65 val descr' = List.concat descr; |
259 val _ = message "Proving isomorphism properties ..."; |
259 val _ = message "Proving isomorphism properties ..."; |
260 |
260 |
261 (* get axioms from theory *) |
261 (* get axioms from theory *) |
262 |
262 |
263 val newT_iso_axms = map (fn s => |
263 val newT_iso_axms = map (fn s => |
264 (get_thm thy4 ("Abs_" ^ s ^ "_inverse", NONE), |
264 (get_thm thy4 (Name ("Abs_" ^ s ^ "_inverse")), |
265 get_thm thy4 ("Rep_" ^ s ^ "_inverse", NONE), |
265 get_thm thy4 (Name ("Rep_" ^ s ^ "_inverse")), |
266 get_thm thy4 ("Rep_" ^ s, NONE))) new_type_names; |
266 get_thm thy4 (Name ("Rep_" ^ s)))) new_type_names; |
267 |
267 |
268 (*------------------------------------------------*) |
268 (*------------------------------------------------*) |
269 (* prove additional theorems: *) |
269 (* prove additional theorems: *) |
270 (* inj_on dt_Abs_i rep_set_i and inj dt_Rep_i *) |
270 (* inj_on dt_Abs_i rep_set_i and inj dt_Rep_i *) |
271 (*------------------------------------------------*) |
271 (*------------------------------------------------*) |