272 fun ext_inst_subclass prep_classrel raw_cc tac thy = |
272 fun ext_inst_subclass prep_classrel raw_cc tac thy = |
273 let |
273 let |
274 val (c1, c2) = prep_classrel thy raw_cc; |
274 val (c1, c2) = prep_classrel thy raw_cc; |
275 val txt = quote (Sign.string_of_classrel thy [c1, c2]); |
275 val txt = quote (Sign.string_of_classrel thy [c1, c2]); |
276 val _ = message ("Proving class inclusion " ^ txt ^ " ..."); |
276 val _ = message ("Proving class inclusion " ^ txt ^ " ..."); |
277 val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR_MESSAGE msg => |
277 val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR msg => |
278 error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt); |
278 cat_error msg ("The error(s) above occurred while trying to prove " ^ txt); |
279 in add_classrel_thms [th] thy end; |
279 in add_classrel_thms [th] thy end; |
280 |
280 |
281 fun ext_inst_arity prep_arity raw_arity tac thy = |
281 fun ext_inst_arity prep_arity raw_arity tac thy = |
282 let |
282 let |
283 val arity = prep_arity thy raw_arity; |
283 val arity = prep_arity thy raw_arity; |
284 val txt = quote (Sign.string_of_arity thy arity); |
284 val txt = quote (Sign.string_of_arity thy arity); |
285 val _ = message ("Proving type arity " ^ txt ^ " ..."); |
285 val _ = message ("Proving type arity " ^ txt ^ " ..."); |
286 val props = (mk_arities arity); |
286 val props = (mk_arities arity); |
287 val ths = Goal.prove_multi thy [] [] props |
287 val ths = Goal.prove_multi thy [] [] props |
288 (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) |
288 (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => |
289 handle ERROR_MESSAGE msg => |
289 cat_error msg ("\nThe error(s) above occurred while trying to prove " ^ txt); |
290 error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt); |
|
291 in add_arity_thms ths thy end; |
290 in add_arity_thms ths thy end; |
292 |
291 |
293 in |
292 in |
294 |
293 |
295 val add_inst_subclass = ext_inst_subclass read_classrel; |
294 val add_inst_subclass = ext_inst_subclass read_classrel; |