equal
deleted
inserted
replaced
40 |
40 |
41 fun is_div_mod @{const div (int)} = true |
41 fun is_div_mod @{const div (int)} = true |
42 | is_div_mod @{const mod (int)} = true |
42 | is_div_mod @{const mod (int)} = true |
43 | is_div_mod _ = false |
43 | is_div_mod _ = false |
44 |
44 |
45 val have_int_div_mod = |
45 val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of) |
46 exists (Term.exists_subterm is_div_mod o Thm.prop_of) |
|
47 |
46 |
48 fun add_div_mod _ (thms, extra_thms) = |
47 fun add_div_mod _ (thms, extra_thms) = |
49 if have_int_div_mod thms orelse have_int_div_mod extra_thms then |
48 if have_int_div_mod thms orelse have_int_div_mod extra_thms then |
50 (thms, @{thms div_as_z3div mod_as_z3mod} @ extra_thms) |
49 (thms, @{thms div_as_z3div mod_as_z3mod} @ extra_thms) |
51 else (thms, extra_thms) |
50 else (thms, extra_thms) |
99 val empty = [] |
98 val empty = [] |
100 val extend = I |
99 val extend = I |
101 fun merge data = Ord_List.merge fst_int_ord data |
100 fun merge data = Ord_List.merge fst_int_ord data |
102 ) |
101 ) |
103 |
102 |
104 fun add_mk_builtins mk = |
103 fun add_mk_builtins mk = Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) |
105 Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) |
|
106 |
104 |
107 fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt)) |
105 fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt)) |
108 |
106 |
109 |
107 |
110 (** basic and additional constructors **) |
108 (** basic and additional constructors **) |