equal
deleted
inserted
replaced
535 val classes = Sign.all_classes thy; |
535 val classes = Sign.all_classes thy; |
536 val class_trivs = map (Thm.class_triv thy) classes; |
536 val class_trivs = map (Thm.class_triv thy) classes; |
537 val class_intros = these_intros thy; |
537 val class_intros = these_intros thy; |
538 val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; |
538 val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; |
539 in |
539 in |
540 (ALLGOALS (Method.insert_tac facts THEN' |
540 Method.intros_tac (class_trivs @ class_intros @ axclass_intros) facts st |
541 REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros))) |
|
542 THEN Tactic.distinct_subgoals_tac) st |
|
543 end; |
541 end; |
544 |
542 |
545 fun default_intro_classes_tac [] = intro_classes_tac [] |
543 fun default_intro_classes_tac [] = intro_classes_tac [] |
546 | default_intro_classes_tac _ = no_tac; |
544 | default_intro_classes_tac _ = no_tac; |
547 |
545 |
594 |> ClassData.map (Graph.add_edge (sub, sup)) |
592 |> ClassData.map (Graph.add_edge (sub, sup)) |
595 end; |
593 end; |
596 |
594 |
597 fun prove_subclass (sub, sup) thms ctxt thy = |
595 fun prove_subclass (sub, sup) thms ctxt thy = |
598 let |
596 let |
599 val supclasses = Sign.complete_sort thy [sup] |
597 val classes = ClassData.get thy; |
600 |> filter_out (fn class => Sign.subsort thy ([sub], [class])); |
598 val is_sup = not o null o curry (Graph.irreducible_paths classes) sub; |
|
599 val supclasses = Graph.all_succs classes [sup] |> filter_out is_sup; |
601 fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms); |
600 fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms); |
602 in |
601 in |
603 thy |
602 thy |
604 |> fold_rev (fn sup' => prove_single_subclass (sub, sup') |
603 |> fold_rev (fn sup' => prove_single_subclass (sub, sup') |
605 (transform sup') ctxt) supclasses |
604 (transform sup') ctxt) supclasses |
842 (map fst params ~~ consts, base_sort, |
841 (map fst params ~~ consts, base_sort, |
843 mk_inst class (map snd supconsts @ consts), |
842 mk_inst class (map snd supconsts @ consts), |
844 calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro)) |
843 calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro)) |
845 #> class_interpretation class axioms [] |
844 #> class_interpretation class axioms [] |
846 ))))) |
845 ))))) |
|
846 |> init class |
847 |> pair class |
847 |> pair class |
848 end; |
848 end; |
849 |
849 |
850 in |
850 in |
851 |
851 |