114 Pretty.brk 1, |
114 Pretty.brk 1, |
115 Pretty.str ("the correct raw type is " ^ quote rty_of_qty_name ^ ".")]) |
115 Pretty.str ("the correct raw type is " ^ quote rty_of_qty_name ^ ".")]) |
116 else |
116 else |
117 () |
117 () |
118 |
118 |
|
119 fun zip_Tvars ctxt type_name rty_Tvars qty_Tvars = |
|
120 case try (get_rel_quot_thm ctxt) type_name of |
|
121 NONE => rty_Tvars ~~ qty_Tvars |
|
122 | SOME rel_quot_thm => |
|
123 let |
|
124 fun quot_term_absT quot_term = |
|
125 let |
|
126 val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term |
|
127 in |
|
128 fastype_of abs |
|
129 end |
|
130 |
|
131 fun equiv_univ_err ctxt ty_pat ty = |
|
132 let |
|
133 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
134 val ty_str = Syntax.string_of_typ ctxt ty |
|
135 in |
|
136 raise QUOT_THM_INTERNAL (Pretty.block |
|
137 [Pretty.str ("The type " ^ quote ty_str), |
|
138 Pretty.brk 1, |
|
139 Pretty.str ("and the relator type pattern " ^ quote ty_pat_str), |
|
140 Pretty.brk 1, |
|
141 Pretty.str "don't unify."]) |
|
142 end |
|
143 |
|
144 fun raw_match (TVar (v, S), T) subs = |
|
145 (case Vartab.defined subs v of |
|
146 false => Vartab.update_new (v, (S, T)) subs |
|
147 | true => subs) |
|
148 | raw_match (Type (_, Ts), Type (_, Us)) subs = |
|
149 raw_matches (Ts, Us) subs |
|
150 | raw_match _ subs = subs |
|
151 and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs) |
|
152 | raw_matches _ subs = subs |
|
153 |
|
154 val rty = Type (type_name, rty_Tvars) |
|
155 val qty = Type (type_name, qty_Tvars) |
|
156 val rel_quot_thm_concl = (Logic.strip_imp_concl o prop_of) rel_quot_thm |
|
157 val schematic_rel_absT = quot_term_absT rel_quot_thm_concl; |
|
158 val ctxt' = Variable.declare_typ schematic_rel_absT ctxt |
|
159 val thy = Proof_Context.theory_of ctxt' |
|
160 val absT = rty --> qty |
|
161 val schematic_absT = Logic.type_map (singleton (Variable.polymorphic ctxt')) absT |
|
162 val _ = Sign.typ_unify thy (schematic_rel_absT, schematic_absT) (Vartab.empty,0) |
|
163 handle Type.TUNIFY => equiv_univ_err ctxt schematic_rel_absT schematic_absT |
|
164 val subs = raw_match (schematic_rel_absT, absT) Vartab.empty |
|
165 val rel_quot_thm_prems = (Logic.strip_imp_prems o prop_of) rel_quot_thm |
|
166 in |
|
167 map (dest_funT o |
|
168 Envir.subst_type subs o |
|
169 quot_term_absT) |
|
170 rel_quot_thm_prems |
|
171 end |
|
172 |
119 fun prove_schematic_quot_thm ctxt (rty, qty) = |
173 fun prove_schematic_quot_thm ctxt (rty, qty) = |
120 (case (rty, qty) of |
174 (case (rty, qty) of |
121 (Type (s, tys), Type (s', tys')) => |
175 (Type (s, tys), Type (s', tys')) => |
122 if s = s' |
176 if s = s' |
123 then |
177 then |
124 let |
178 let |
125 val args = map (prove_schematic_quot_thm ctxt) (tys ~~ tys') |
179 val args = map (prove_schematic_quot_thm ctxt) (zip_Tvars ctxt s tys tys') |
126 in |
180 in |
127 if forall is_id_quot args |
181 if forall is_id_quot args |
128 then |
182 then |
129 @{thm identity_quotient} |
183 @{thm identity_quotient} |
130 else |
184 else |