equal
deleted
inserted
replaced
60 |
60 |
61 (* makes the new type definitions and proves non-emptyness *) |
61 (* makes the new type definitions and proves non-emptyness *) |
62 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
62 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
63 let |
63 let |
64 val typedef_tac = |
64 val typedef_tac = |
65 EVERY1 [rtac @{thm exI}, |
65 EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) |
66 rtac mem_def2, |
|
67 rtac @{thm exI}, |
|
68 rtac @{thm refl}] |
|
69 in |
66 in |
70 Local_Theory.theory_result |
67 Local_Theory.theory_result |
71 (Typedef.add_typedef false NONE |
68 (Typedef.add_typedef false NONE |
72 (qty_name, vs, mx) |
69 (qty_name, vs, mx) |
73 (typedef_term rel rty lthy) |
70 (typedef_term rel rty lthy) |
85 in |
82 in |
86 (rtac @{thm Quot_Type.intro} THEN' |
83 (rtac @{thm Quot_Type.intro} THEN' |
87 RANGE [rtac equiv_thm, |
84 RANGE [rtac equiv_thm, |
88 rtac rep_thm, |
85 rtac rep_thm, |
89 rtac rep_inv, |
86 rtac rep_inv, |
90 EVERY' [rtac abs_inv, rtac @{thm exI}, rtac @{thm refl}], |
87 EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), |
91 rtac rep_inj]) 1 |
88 rtac rep_inj]) 1 |
92 end |
89 end |
93 |
90 |
94 |
91 |
95 (* proves the Quot_Type theorem *) |
92 (* proves the Quot_Type theorem *) |
132 val Abs_name = #Abs_name typedef_info |
129 val Abs_name = #Abs_name typedef_info |
133 val Rep_name = #Rep_name typedef_info |
130 val Rep_name = #Rep_name typedef_info |
134 val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) |
131 val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) |
135 val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) |
132 val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) |
136 |
133 |
137 (* more abstract abs and rep definitions *) |
134 (* more useful abs and rep definitions *) |
138 val abs_const = Const (@{const_name "Quot_Type.abs"}, dummyT ) |
135 val abs_const = Const (@{const_name "Quot_Type.abs"}, dummyT ) |
139 val rep_const = Const (@{const_name "Quot_Type.rep"}, dummyT ) |
136 val rep_const = Const (@{const_name "Quot_Type.rep"}, dummyT ) |
140 val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const) |
137 val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const) |
141 val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const) |
138 val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const) |
142 val abs_name = Binding.prefix_name "abs_" qty_name |
139 val abs_name = Binding.prefix_name "abs_" qty_name |