936 fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs |
936 fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs |
937 in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end |
937 in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end |
938 |
938 |
939 (** Axiom selection **) |
939 (** Axiom selection **) |
940 |
940 |
941 (* Similar to "Refute.specialize_type" but returns all matches rather than only |
|
942 the first (preorder) match. *) |
|
943 (* theory -> styp -> term -> term list *) |
|
944 fun multi_specialize_type thy slack (s, T) t = |
|
945 let |
|
946 (* term -> (typ * term) list -> (typ * term) list *) |
|
947 fun aux (Const (s', T')) ys = |
|
948 if s = s' then |
|
949 ys |> (if AList.defined (op =) ys T' then |
|
950 I |
|
951 else |
|
952 cons (T', Refute.monomorphic_term |
|
953 (Sign.typ_match thy (T', T) Vartab.empty) t) |
|
954 handle Type.TYPE_MATCH => I |
|
955 | Refute.REFUTE _ => |
|
956 if slack then |
|
957 I |
|
958 else |
|
959 raise NOT_SUPPORTED ("too much polymorphism in \ |
|
960 \axiom involving " ^ quote s)) |
|
961 else |
|
962 ys |
|
963 | aux _ ys = ys |
|
964 in map snd (fold_aterms aux t []) end |
|
965 |
|
966 (* theory -> bool -> const_table -> styp -> term list *) |
|
967 fun nondef_props_for_const thy slack table (x as (s, _)) = |
|
968 these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) |
|
969 |
|
970 (* 'a Symtab.table -> 'a list *) |
941 (* 'a Symtab.table -> 'a list *) |
971 fun all_table_entries table = Symtab.fold (append o snd) table [] |
942 fun all_table_entries table = Symtab.fold (append o snd) table [] |
972 (* const_table -> string -> const_table *) |
943 (* const_table -> string -> const_table *) |
973 fun extra_table table s = Symtab.make [(s, all_table_entries table)] |
944 fun extra_table table s = Symtab.make [(s, all_table_entries table)] |
974 |
945 |
983 val axioms_max_depth = 255 |
954 val axioms_max_depth = 255 |
984 |
955 |
985 (* hol_context -> term -> term list * term list * bool * bool *) |
956 (* hol_context -> term -> term list * term list * bool * bool *) |
986 fun axioms_for_term |
957 fun axioms_for_term |
987 (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms, |
958 (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms, |
988 fast_descrs, evals, def_table, nondef_table, user_nondefs, |
959 fast_descrs, evals, def_table, nondef_table, |
989 ...}) t = |
960 choice_spec_table, user_nondefs, ...}) t = |
990 let |
961 let |
991 type accumulator = styp list * (term list * term list) |
962 type accumulator = styp list * (term list * term list) |
992 (* (term list * term list -> term list) |
963 (* (term list * term list -> term list) |
993 -> ((term list -> term list) -> term list * term list |
964 -> ((term list -> term list) -> term list * term list |
994 -> term list * term list) |
965 -> term list * term list) |
1045 else if is_constr thy stds x then |
1016 else if is_constr thy stds x then |
1046 accum |
1017 accum |
1047 else if is_equational_fun hol_ctxt x then |
1018 else if is_equational_fun hol_ctxt x then |
1048 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) |
1019 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) |
1049 accum |
1020 accum |
|
1021 else if is_choice_spec_fun hol_ctxt x then |
|
1022 fold (add_nondef_axiom depth) |
|
1023 (nondef_props_for_const thy true choice_spec_table x) accum |
1050 else if is_abs_fun thy x then |
1024 else if is_abs_fun thy x then |
1051 if is_quot_type thy (range_type T) then |
1025 if is_quot_type thy (range_type T) then |
1052 raise NOT_SUPPORTED "\"Abs_\" function of quotient type" |
1026 raise NOT_SUPPORTED "\"Abs_\" function of quotient type" |
1053 else |
1027 else |
1054 accum |> fold (add_nondef_axiom depth) |
1028 accum |> fold (add_nondef_axiom depth) |