958 accum |
958 accum |
959 else if is_choice_spec_fun hol_ctxt x then |
959 else if is_choice_spec_fun hol_ctxt x then |
960 fold (add_nondef_axiom depth) |
960 fold (add_nondef_axiom depth) |
961 (nondef_props_for_const thy true choice_spec_table x) accum |
961 (nondef_props_for_const thy true choice_spec_table x) accum |
962 else if is_abs_fun ctxt x then |
962 else if is_abs_fun ctxt x then |
963 if is_quot_type thy (range_type T) then |
963 accum |> fold (add_nondef_axiom depth) |
964 accum |
964 (nondef_props_for_const thy false nondef_table x) |
965 else |
965 |> (is_funky_typedef thy (range_type T) orelse |
966 accum |> fold (add_nondef_axiom depth) |
966 range_type T = nat_T) |
967 (nondef_props_for_const thy false nondef_table x) |
967 ? fold (add_maybe_def_axiom depth) |
968 |> (is_funky_typedef thy (range_type T) orelse |
968 (nondef_props_for_const thy true |
969 range_type T = nat_T) |
|
970 ? fold (add_maybe_def_axiom depth) |
|
971 (nondef_props_for_const thy true |
|
972 (extra_table def_table s) x) |
969 (extra_table def_table s) x) |
973 else if is_rep_fun ctxt x then |
970 else if is_rep_fun ctxt x then |
974 if is_quot_type thy (domain_type T) then |
971 accum |> fold (add_nondef_axiom depth) |
975 accum |
972 (nondef_props_for_const thy false nondef_table x) |
976 else |
973 |> (is_funky_typedef thy (range_type T) orelse |
977 accum |> fold (add_nondef_axiom depth) |
974 range_type T = nat_T) |
978 (nondef_props_for_const thy false nondef_table x) |
975 ? fold (add_maybe_def_axiom depth) |
979 |> (is_funky_typedef thy (range_type T) orelse |
976 (nondef_props_for_const thy true |
980 range_type T = nat_T) |
|
981 ? fold (add_maybe_def_axiom depth) |
|
982 (nondef_props_for_const thy true |
|
983 (extra_table def_table s) x) |
977 (extra_table def_table s) x) |
984 |> add_axioms_for_term depth |
978 |> add_axioms_for_term depth |
985 (Const (mate_of_rep_fun ctxt x)) |
979 (Const (mate_of_rep_fun ctxt x)) |
986 |> fold (add_def_axiom depth) |
980 |> fold (add_def_axiom depth) |
987 (inverse_axioms_for_rep_fun ctxt x) |
981 (inverse_axioms_for_rep_fun ctxt x) |
988 else if s = @{const_name TYPE} then |
982 else if s = @{const_name TYPE} then |
989 accum |
983 accum |
990 else case def_of_const thy def_table x of |
984 else case def_of_const thy def_table x of |
991 SOME def => |
985 SOME def => |
992 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) |
986 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) |