121 |
121 |
122 (* main function for constructing a quotient type *) |
122 (* main function for constructing a quotient type *) |
123 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = |
123 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = |
124 let |
124 let |
125 (* generates the typedef *) |
125 (* generates the typedef *) |
126 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
126 val ((qty_full_name, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
127 |
127 |
128 (* abs and rep functions from the typedef *) |
128 (* abs and rep functions from the typedef *) |
129 val abs_ty = #abs_type typedef_info |
129 val Abs_ty = #abs_type typedef_info |
130 val rep_ty = #rep_type typedef_info |
130 val Rep_ty = #rep_type typedef_info |
131 val abs_name = #Abs_name typedef_info |
131 val Abs_name = #Abs_name typedef_info |
132 val rep_name = #Rep_name typedef_info |
132 val Rep_name = #Rep_name typedef_info |
133 val abs = Const (abs_name, rep_ty --> abs_ty) |
133 val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) |
134 val rep = Const (rep_name, abs_ty --> rep_ty) |
134 val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) |
135 |
135 |
136 (* more abstract ABS and REP definitions *) |
136 (* more abstract abs and rep definitions *) |
137 val ABS_const = Const (@{const_name "Quot_Type.abs"}, dummyT ) |
137 val abs_const = Const (@{const_name "Quot_Type.abs"}, dummyT ) |
138 val REP_const = Const (@{const_name "Quot_Type.rep"}, dummyT ) |
138 val rep_const = Const (@{const_name "Quot_Type.rep"}, dummyT ) |
139 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
139 val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const) |
140 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
140 val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const) |
141 val ABS_name = Binding.prefix_name "abs_" qty_name |
141 val abs_name = Binding.prefix_name "abs_" qty_name |
142 val REP_name = Binding.prefix_name "rep_" qty_name |
142 val rep_name = Binding.prefix_name "rep_" qty_name |
143 |
143 |
144 val ((ABS, ABS_def), lthy2) = define (ABS_name, NoSyn, ABS_trm) lthy1 |
144 val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 |
145 val ((REP, REP_def), lthy3) = define (REP_name, NoSyn, REP_trm) lthy2 |
145 val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 |
146 |
146 |
147 (* quot_type theorem - needed below *) |
147 (* quot_type theorem - needed below *) |
148 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy3 |
148 val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3 |
149 |
149 |
150 (* quotient theorem *) |
150 (* quotient theorem *) |
151 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy3 |
151 val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3 |
152 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
152 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
153 |
153 |
|
154 (* name equivalence theorem *) |
|
155 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
|
156 |
154 (* storing the quot-info *) |
157 (* storing the quot-info *) |
155 val qty_str = fst (Term.dest_Type abs_ty) |
158 val lthy4 = quotdata_update qty_full_name |
156 val lthy4 = quotdata_update qty_str |
159 (Logic.varifyT Abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy3 |
157 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy3 |
|
158 (* FIXME: varifyT should not be used *) |
160 (* FIXME: varifyT should not be used *) |
159 (* FIXME: the relation can be any term, that later maybe needs to be given *) |
161 (* FIXME: the relation can be any term, that later maybe needs to be given *) |
160 (* FIXME: a different type (in regularize_trm); how should tis be done? *) |
162 (* FIXME: a different type (in regularize_trm); how should this be done? *) |
161 |
|
162 in |
163 in |
163 lthy4 |
164 lthy4 |
164 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
165 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
165 ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add]) |
166 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
166 end |
167 end |
167 |
168 |
168 |
169 |
169 (* interface and syntax setup *) |
170 (* interface and syntax setup *) |
170 |
171 |