130 val rep_name = #Rep_name typedef_info |
130 val rep_name = #Rep_name typedef_info |
131 val abs = Const (abs_name, rep_ty --> abs_ty) |
131 val abs = Const (abs_name, rep_ty --> abs_ty) |
132 val rep = Const (rep_name, abs_ty --> rep_ty) |
132 val rep = Const (rep_name, abs_ty --> rep_ty) |
133 |
133 |
134 (* ABS and REP definitions *) |
134 (* ABS and REP definitions *) |
135 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
135 val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT ) |
136 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
136 val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT ) |
137 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
137 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
138 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
138 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
139 val ABS_name = Binding.prefix_name "ABS_" qty_name |
139 val ABS_name = Binding.prefix_name "abs_" qty_name |
140 val REP_name = Binding.prefix_name "REP_" qty_name |
140 val REP_name = Binding.prefix_name "rep_" qty_name |
141 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
141 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
142 lthy1 |> define (ABS_name, NoSyn, ABS_trm) |
142 lthy1 |> define (ABS_name, NoSyn, ABS_trm) |
143 ||>> define (REP_name, NoSyn, REP_trm) |
143 ||>> define (REP_name, NoSyn, REP_trm) |
144 |
144 |
145 (* quot_type theorem *) |
145 (* quot_type theorem *) |