equal
deleted
inserted
replaced
189 else |
189 else |
190 (false, |
190 (false, |
191 thy2 |
191 thy2 |
192 |> update_classrel ((c1, c2), |
192 |> update_classrel ((c1, c2), |
193 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) |
193 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) |
194 |> Drule.instantiate' [SOME (ctyp_of thy2 (TVar ((Name.aT, 0), [])))] [] |
194 |> Drule.instantiate' [SOME (Thm.ctyp_of thy2 (TVar ((Name.aT, 0), [])))] [] |
195 |> Thm.close_derivation)); |
195 |> Thm.close_derivation)); |
196 |
196 |
197 val proven = is_classrel thy1; |
197 val proven = is_classrel thy1; |
198 val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds []; |
198 val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds []; |
199 val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs []; |
199 val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs []; |
226 Sign.super_classes thy c |
226 Sign.super_classes thy c |
227 |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => |
227 |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => |
228 c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars); |
228 c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars); |
229 |
229 |
230 val names = Name.invent Name.context Name.aT (length Ss); |
230 val names = Name.invent Name.context Name.aT (length Ss); |
231 val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names; |
231 val std_vars = map (fn a => SOME (Thm.ctyp_of thy (TVar ((a, 0), [])))) names; |
232 |
232 |
233 val completions = super_class_completions |> map (fn c1 => |
233 val completions = super_class_completions |> map (fn c1 => |
234 let |
234 let |
235 val th1 = |
235 val th1 = |
236 (th RS the_classrel thy (c, c1)) |
236 (th RS the_classrel thy (c, c1)) |
394 val binding = |
394 val binding = |
395 Binding.conceal (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2)))); |
395 Binding.conceal (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2)))); |
396 val (th', thy') = Global_Theory.store_thm (binding, th) thy; |
396 val (th', thy') = Global_Theory.store_thm (binding, th) thy; |
397 val th'' = th' |
397 val th'' = th' |
398 |> Thm.unconstrainT |
398 |> Thm.unconstrainT |
399 |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] []; |
399 |> Drule.instantiate' [SOME (Thm.ctyp_of thy' (TVar ((Name.aT, 0), [])))] []; |
400 in |
400 in |
401 thy' |
401 thy' |
402 |> Sign.primitive_classrel (c1, c2) |
402 |> Sign.primitive_classrel (c1, c2) |
403 |> map_proven_classrels (Symreltab.update ((c1, c2), th'')) |
403 |> map_proven_classrels (Symreltab.update ((c1, c2), th'')) |
404 |> perhaps complete_classrels |
404 |> perhaps complete_classrels |
416 Binding.conceal (Binding.name (prefix arity_prefix (Logic.name_arity arity))); |
416 Binding.conceal (Binding.name (prefix arity_prefix (Logic.name_arity arity))); |
417 val (th', thy') = Global_Theory.store_thm (binding, th) thy; |
417 val (th', thy') = Global_Theory.store_thm (binding, th) thy; |
418 |
418 |
419 val args = Name.invent_names Name.context Name.aT Ss; |
419 val args = Name.invent_names Name.context Name.aT Ss; |
420 val T = Type (t, map TFree args); |
420 val T = Type (t, map TFree args); |
421 val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args; |
421 val std_vars = map (fn (a, S) => SOME (Thm.ctyp_of thy' (TVar ((a, 0), [])))) args; |
422 |
422 |
423 val missing_params = Sign.complete_sort thy' [c] |
423 val missing_params = Sign.complete_sort thy' [c] |
424 |> maps (these o Option.map #params o try (get_info thy')) |
424 |> maps (these o Option.map #params o try (get_info thy')) |
425 |> filter_out (fn (const, _) => can (get_inst_param thy') (const, t)) |
425 |> filter_out (fn (const, _) => can (get_inst_param thy') (const, t)) |
426 |> (map o apsnd o map_atyps) (K T); |
426 |> (map o apsnd o map_atyps) (K T); |