48 |
48 |
49 val satisfy_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model for a formula *) |
49 val satisfy_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model for a formula *) |
50 val refute_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model that refutes a formula *) |
50 val refute_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model that refutes a formula *) |
51 val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit |
51 val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit |
52 |
52 |
53 val setup : (theory -> theory) list |
53 val setup : theory -> theory |
54 end; |
54 end; |
55 |
55 |
56 structure Refute : REFUTE = |
56 structure Refute : REFUTE = |
57 struct |
57 struct |
58 |
58 |
2603 (* ------------------------------------------------------------------------- *) |
2603 (* ------------------------------------------------------------------------- *) |
2604 |
2604 |
2605 (* (theory -> theory) list *) |
2605 (* (theory -> theory) list *) |
2606 |
2606 |
2607 val setup = |
2607 val setup = |
2608 [RefuteData.init, |
2608 RefuteData.init #> |
2609 add_interpreter "stlc" stlc_interpreter, |
2609 add_interpreter "stlc" stlc_interpreter #> |
2610 add_interpreter "Pure" Pure_interpreter, |
2610 add_interpreter "Pure" Pure_interpreter #> |
2611 add_interpreter "HOLogic" HOLogic_interpreter, |
2611 add_interpreter "HOLogic" HOLogic_interpreter #> |
2612 add_interpreter "set" set_interpreter, |
2612 add_interpreter "set" set_interpreter #> |
2613 add_interpreter "IDT" IDT_interpreter, |
2613 add_interpreter "IDT" IDT_interpreter #> |
2614 add_interpreter "IDT_constructor" IDT_constructor_interpreter, |
2614 add_interpreter "IDT_constructor" IDT_constructor_interpreter #> |
2615 add_interpreter "IDT_recursion" IDT_recursion_interpreter, |
2615 add_interpreter "IDT_recursion" IDT_recursion_interpreter #> |
2616 add_interpreter "Finite_Set.card" Finite_Set_card_interpreter, |
2616 add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #> |
2617 add_interpreter "Finite_Set.Finites" Finite_Set_Finites_interpreter, |
2617 add_interpreter "Finite_Set.Finites" Finite_Set_Finites_interpreter #> |
2618 add_interpreter "Nat.op <" Nat_less_interpreter, |
2618 add_interpreter "Nat.op <" Nat_less_interpreter #> |
2619 add_interpreter "Nat.op +" Nat_plus_interpreter, |
2619 add_interpreter "Nat.op +" Nat_plus_interpreter #> |
2620 add_interpreter "Nat.op -" Nat_minus_interpreter, |
2620 add_interpreter "Nat.op -" Nat_minus_interpreter #> |
2621 add_interpreter "Nat.op *" Nat_mult_interpreter, |
2621 add_interpreter "Nat.op *" Nat_mult_interpreter #> |
2622 add_interpreter "List.op @" List_append_interpreter, |
2622 add_interpreter "List.op @" List_append_interpreter #> |
2623 add_interpreter "Lfp.lfp" Lfp_lfp_interpreter, |
2623 add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #> |
2624 add_interpreter "Gfp.gfp" Gfp_gfp_interpreter, |
2624 add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #> |
2625 add_printer "stlc" stlc_printer, |
2625 add_printer "stlc" stlc_printer #> |
2626 add_printer "set" set_printer, |
2626 add_printer "set" set_printer #> |
2627 add_printer "IDT" IDT_printer]; |
2627 add_printer "IDT" IDT_printer; |
2628 |
2628 |
2629 end |
2629 end |