100 end |
100 end |
101 |
101 |
102 (* proves the quotient theorem *) |
102 (* proves the quotient theorem *) |
103 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
103 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
104 let |
104 let |
105 val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) |
105 val quotient_const = Const (@{const_name "Quotient"}, dummyT) |
106 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
106 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
107 |> Syntax.check_term lthy |
107 |> Syntax.check_term lthy |
108 |
108 |
109 val typedef_quotient_thm_tac = |
109 val typedef_quotient_thm_tac = |
110 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), |
110 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), |
111 rtac @{thm QUOT_TYPE.QUOTIENT}, |
111 rtac @{thm QUOT_TYPE.Quotient}, |
112 rtac quot_type_thm] |
112 rtac quot_type_thm] |
113 in |
113 in |
114 Goal.prove lthy [] [] goal |
114 Goal.prove lthy [] [] goal |
115 (K typedef_quotient_thm_tac) |
115 (K typedef_quotient_thm_tac) |
116 end |
116 end |
144 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
144 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
145 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
145 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
146 |
146 |
147 (* quotient theorem *) |
147 (* quotient theorem *) |
148 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
148 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
149 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
149 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
150 |
150 |
151 (* storing the quot-info *) |
151 (* storing the quot-info *) |
152 val qty_str = fst (Term.dest_Type abs_ty) |
152 val qty_str = fst (Term.dest_Type abs_ty) |
153 val lthy3 = quotdata_update qty_str |
153 val lthy3 = quotdata_update qty_str |
154 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
154 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
155 (* FIXME: varifyT should not be used *) |
155 (* FIXME: varifyT should not be used *) |
156 (* FIXME: the relation needs to be a string, since its type needs *) |
156 (* FIXME: the relation needs to be a string, since its type needs *) |
157 (* FIXME: to recalculated in for example REGULARIZE *) |
157 (* FIXME: to recalculated in for example REGULARIZE *) |
158 |
158 |
159 (* storing of the equiv_thm under a name *) |
159 (* storing of the equiv_thm under a name *) |
160 val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm, []) lthy3 |
160 val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, []) lthy3 |
161 |
161 |
162 (* interpretation *) |
162 (* interpretation *) |
163 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
163 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
164 val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; |
164 val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; |
165 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
165 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
203 |
203 |
204 fun quotient_type quot_list lthy = |
204 fun quotient_type quot_list lthy = |
205 let |
205 let |
206 fun mk_goal (rty, rel) = |
206 fun mk_goal (rty, rel) = |
207 let |
207 let |
208 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
208 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
209 in |
209 in |
210 HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel) |
210 HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) |
211 end |
211 end |
212 |
212 |
213 val goals = map (mk_goal o snd) quot_list |
213 val goals = map (mk_goal o snd) quot_list |
214 |
214 |
215 fun after_qed thms lthy = |
215 fun after_qed thms lthy = |