35 def_table: const_table, |
35 def_table: const_table, |
36 nondef_table: const_table, |
36 nondef_table: const_table, |
37 user_nondefs: term list, |
37 user_nondefs: term list, |
38 simp_table: const_table Unsynchronized.ref, |
38 simp_table: const_table Unsynchronized.ref, |
39 psimp_table: const_table, |
39 psimp_table: const_table, |
|
40 choice_spec_table: const_table, |
40 intro_table: const_table, |
41 intro_table: const_table, |
41 ground_thm_table: term list Inttab.table, |
42 ground_thm_table: term list Inttab.table, |
42 ersatz_table: (string * string) list, |
43 ersatz_table: (string * string) list, |
43 skolems: (string * string list) list Unsynchronized.ref, |
44 skolems: (string * string list) list Unsynchronized.ref, |
44 special_funs: special_fun list Unsynchronized.ref, |
45 special_funs: special_fun list Unsynchronized.ref, |
178 val const_def_table : |
179 val const_def_table : |
179 Proof.context -> (term * term) list -> term list -> const_table |
180 Proof.context -> (term * term) list -> term list -> const_table |
180 val const_nondef_table : term list -> const_table |
181 val const_nondef_table : term list -> const_table |
181 val const_simp_table : Proof.context -> (term * term) list -> const_table |
182 val const_simp_table : Proof.context -> (term * term) list -> const_table |
182 val const_psimp_table : Proof.context -> (term * term) list -> const_table |
183 val const_psimp_table : Proof.context -> (term * term) list -> const_table |
|
184 val const_choice_spec_table : |
|
185 Proof.context -> (term * term) list -> const_table |
183 val inductive_intro_table : |
186 val inductive_intro_table : |
184 Proof.context -> (term * term) list -> const_table -> const_table |
187 Proof.context -> (term * term) list -> const_table -> const_table |
185 val ground_theorem_table : theory -> term list Inttab.table |
188 val ground_theorem_table : theory -> term list Inttab.table |
186 val ersatz_table : theory -> (string * string) list |
189 val ersatz_table : theory -> (string * string) list |
187 val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit |
190 val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit |
195 theory -> const_table -> string * typ -> fixpoint_kind |
198 theory -> const_table -> string * typ -> fixpoint_kind |
196 val is_inductive_pred : hol_context -> styp -> bool |
199 val is_inductive_pred : hol_context -> styp -> bool |
197 val is_equational_fun : hol_context -> styp -> bool |
200 val is_equational_fun : hol_context -> styp -> bool |
198 val is_constr_pattern_lhs : theory -> term -> bool |
201 val is_constr_pattern_lhs : theory -> term -> bool |
199 val is_constr_pattern_formula : theory -> term -> bool |
202 val is_constr_pattern_formula : theory -> term -> bool |
|
203 val nondef_props_for_const : |
|
204 theory -> bool -> const_table -> styp -> term list |
|
205 val is_choice_spec_fun : hol_context -> styp -> bool |
|
206 val is_choice_spec_axiom : theory -> const_table -> term -> bool |
200 val codatatype_bisim_axioms : hol_context -> typ -> term list |
207 val codatatype_bisim_axioms : hol_context -> typ -> term list |
201 val is_well_founded_inductive_pred : hol_context -> styp -> bool |
208 val is_well_founded_inductive_pred : hol_context -> styp -> bool |
202 val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term |
209 val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term |
203 val equational_fun_axioms : hol_context -> styp -> term list |
210 val equational_fun_axioms : hol_context -> styp -> term list |
204 val is_equational_fun_surely_complete : hol_context -> styp -> bool |
211 val is_equational_fun_surely_complete : hol_context -> styp -> bool |
239 def_table: const_table, |
246 def_table: const_table, |
240 nondef_table: const_table, |
247 nondef_table: const_table, |
241 user_nondefs: term list, |
248 user_nondefs: term list, |
242 simp_table: const_table Unsynchronized.ref, |
249 simp_table: const_table Unsynchronized.ref, |
243 psimp_table: const_table, |
250 psimp_table: const_table, |
|
251 choice_spec_table: const_table, |
244 intro_table: const_table, |
252 intro_table: const_table, |
245 ground_thm_table: term list Inttab.table, |
253 ground_thm_table: term list Inttab.table, |
246 ersatz_table: (string * string) list, |
254 ersatz_table: (string * string) list, |
247 skolems: (string * string list) list Unsynchronized.ref, |
255 skolems: (string * string list) list Unsynchronized.ref, |
248 special_funs: special_fun list Unsynchronized.ref, |
256 special_funs: special_fun list Unsynchronized.ref, |
1439 else t |
1447 else t |
1440 end |
1448 end |
1441 | NONE => t) |
1449 | NONE => t) |
1442 | t => t) |
1450 | t => t) |
1443 |
1451 |
1444 (* term -> string * term *) |
|
1445 fun pair_for_prop t = |
|
1446 case term_under_def t of |
|
1447 Const (s, _) => (s, t) |
|
1448 | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) |
|
1449 |
|
1450 (* (Proof.context -> term list) -> Proof.context -> (term * term) list |
|
1451 -> const_table *) |
|
1452 fun table_for get ctxt subst = |
|
1453 ctxt |> get |> map (pair_for_prop o subst_atomic subst) |
|
1454 |> AList.group (op =) |> Symtab.make |
|
1455 |
|
1456 (* theory -> (typ option * bool) list -> (string * int) list *) |
1452 (* theory -> (typ option * bool) list -> (string * int) list *) |
1457 fun case_const_names thy stds = |
1453 fun case_const_names thy stds = |
1458 Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) => |
1454 Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) => |
1459 if is_basic_datatype thy stds dtype_s then |
1455 if is_basic_datatype thy stds dtype_s then |
1460 I |
1456 I |
1511 forall (is_constr_pattern thy) (snd (strip_comb t)) |
1507 forall (is_constr_pattern thy) (snd (strip_comb t)) |
1512 fun is_constr_pattern_formula thy t = |
1508 fun is_constr_pattern_formula thy t = |
1513 case lhs_of_equation t of |
1509 case lhs_of_equation t of |
1514 SOME t' => is_constr_pattern_lhs thy t' |
1510 SOME t' => is_constr_pattern_lhs thy t' |
1515 | NONE => false |
1511 | NONE => false |
|
1512 |
|
1513 (* Similar to "Refute.specialize_type" but returns all matches rather than only |
|
1514 the first (preorder) match. *) |
|
1515 (* theory -> styp -> term -> term list *) |
|
1516 fun multi_specialize_type thy slack (s, T) t = |
|
1517 let |
|
1518 (* term -> (typ * term) list -> (typ * term) list *) |
|
1519 fun aux (Const (s', T')) ys = |
|
1520 if s = s' then |
|
1521 ys |> (if AList.defined (op =) ys T' then |
|
1522 I |
|
1523 else |
|
1524 cons (T', Refute.monomorphic_term |
|
1525 (Sign.typ_match thy (T', T) Vartab.empty) t) |
|
1526 handle Type.TYPE_MATCH => I |
|
1527 | Refute.REFUTE _ => |
|
1528 if slack then |
|
1529 I |
|
1530 else |
|
1531 raise NOT_SUPPORTED ("too much polymorphism in \ |
|
1532 \axiom involving " ^ quote s)) |
|
1533 else |
|
1534 ys |
|
1535 | aux _ ys = ys |
|
1536 in map snd (fold_aterms aux t []) end |
|
1537 (* theory -> bool -> const_table -> styp -> term list *) |
|
1538 fun nondef_props_for_const thy slack table (x as (s, _)) = |
|
1539 these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) |
|
1540 |
|
1541 (* term -> term *) |
|
1542 fun unvarify_term (t1 $ t2) = unvarify_term t1 $ unvarify_term t2 |
|
1543 | unvarify_term (Var ((s, 0), T)) = Free (s, T) |
|
1544 | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t') |
|
1545 | unvarify_term t = t |
|
1546 (* theory -> term -> term *) |
|
1547 fun axiom_for_choice_spec thy = |
|
1548 unvarify_term |
|
1549 #> Object_Logic.atomize_term thy |
|
1550 #> Choice_Specification.close_form |
|
1551 #> HOLogic.mk_Trueprop |
|
1552 (* hol_context -> styp -> bool *) |
|
1553 fun is_choice_spec_fun ({thy, def_table, nondef_table, choice_spec_table, ...} |
|
1554 : hol_context) x = |
|
1555 case nondef_props_for_const thy true choice_spec_table x of |
|
1556 [] => false |
|
1557 | ts => case def_of_const thy def_table x of |
|
1558 SOME (Const (@{const_name Eps}, _) $ _) => true |
|
1559 | SOME _ => false |
|
1560 | NONE => |
|
1561 let val ts' = nondef_props_for_const thy true nondef_table x in |
|
1562 length ts' = length ts andalso |
|
1563 forall (fn t => |
|
1564 exists (curry (op aconv) (axiom_for_choice_spec thy t)) |
|
1565 ts') ts |
|
1566 end |
|
1567 |
|
1568 (* theory -> const_table -> term -> bool *) |
|
1569 fun is_choice_spec_axiom thy choice_spec_table t = |
|
1570 Symtab.exists (fn (_, ts) => |
|
1571 exists (curry (op aconv) t o axiom_for_choice_spec thy) ts) |
|
1572 choice_spec_table |
1516 |
1573 |
1517 (** Constant unfolding **) |
1574 (** Constant unfolding **) |
1518 |
1575 |
1519 (* theory -> (typ option * bool) list -> int * styp -> term *) |
1576 (* theory -> (typ option * bool) list -> int * styp -> term *) |
1520 fun constr_case_body thy stds (j, (x as (_, T))) = |
1577 fun constr_case_body thy stds (j, (x as (_, T))) = |
1717 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end |
1775 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end |
1718 in do_term 0 [] end |
1776 in do_term 0 [] end |
1719 |
1777 |
1720 (** Axiom extraction/generation **) |
1778 (** Axiom extraction/generation **) |
1721 |
1779 |
|
1780 (* term -> string * term *) |
|
1781 fun pair_for_prop t = |
|
1782 case term_under_def t of |
|
1783 Const (s, _) => (s, t) |
|
1784 | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) |
|
1785 (* (Proof.context -> term list) -> Proof.context -> (term * term) list |
|
1786 -> const_table *) |
|
1787 fun def_table_for get ctxt subst = |
|
1788 ctxt |> get |> map (pair_for_prop o subst_atomic subst) |
|
1789 |> AList.group (op =) |> Symtab.make |
|
1790 (* term -> string * term *) |
|
1791 fun paired_with_consts t = map (rpair t) (Term.add_const_names t []) |
1722 (* Proof.context -> (term * term) list -> term list -> const_table *) |
1792 (* Proof.context -> (term * term) list -> term list -> const_table *) |
1723 fun const_def_table ctxt subst ts = |
1793 fun const_def_table ctxt subst ts = |
1724 table_for (map prop_of o Nitpick_Defs.get) ctxt subst |
1794 def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst |
1725 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) |
1795 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) |
1726 (map pair_for_prop ts) |
1796 (map pair_for_prop ts) |
1727 (* term list -> const_table *) |
1797 (* term list -> const_table *) |
1728 fun const_nondef_table ts = |
1798 fun const_nondef_table ts = |
1729 fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts [] |
1799 fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make |
1730 |> AList.group (op =) |> Symtab.make |
|
1731 (* Proof.context -> (term * term) list -> const_table *) |
1800 (* Proof.context -> (term * term) list -> const_table *) |
1732 val const_simp_table = table_for (map prop_of o Nitpick_Simps.get) |
1801 val const_simp_table = def_table_for (map prop_of o Nitpick_Simps.get) |
1733 val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get) |
1802 val const_psimp_table = def_table_for (map prop_of o Nitpick_Psimps.get) |
|
1803 fun const_choice_spec_table ctxt subst = |
|
1804 map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt) |
|
1805 |> const_nondef_table |
1734 (* Proof.context -> (term * term) list -> const_table -> const_table *) |
1806 (* Proof.context -> (term * term) list -> const_table -> const_table *) |
1735 fun inductive_intro_table ctxt subst def_table = |
1807 fun inductive_intro_table ctxt subst def_table = |
1736 table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) |
1808 def_table_for |
1737 def_table o prop_of) |
1809 (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) |
1738 o Nitpick_Intros.get) ctxt subst |
1810 def_table o prop_of) |
|
1811 o Nitpick_Intros.get) ctxt subst |
1739 (* theory -> term list Inttab.table *) |
1812 (* theory -> term list Inttab.table *) |
1740 fun ground_theorem_table thy = |
1813 fun ground_theorem_table thy = |
1741 fold ((fn @{const Trueprop} $ t1 => |
1814 fold ((fn @{const Trueprop} $ t1 => |
1742 is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) |
1815 is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) |
1743 | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty |
1816 | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty |
1744 |
1817 |
|
1818 (* TODO: Move to "Nitpick.thy" *) |
1745 val basic_ersatz_table = |
1819 val basic_ersatz_table = |
1746 [(@{const_name prod_case}, @{const_name split}), |
1820 [(@{const_name prod_case}, @{const_name split}), |
1747 (@{const_name card}, @{const_name card'}), |
1821 (@{const_name card}, @{const_name card'}), |
1748 (@{const_name setsum}, @{const_name setsum'}), |
1822 (@{const_name setsum}, @{const_name setsum'}), |
1749 (@{const_name fold_graph}, @{const_name fold_graph'}), |
1823 (@{const_name fold_graph}, @{const_name fold_graph'}), |