24 val print_shuffles: theory -> unit |
24 val print_shuffles: theory -> unit |
25 |
25 |
26 val add_shuffle_rule: thm -> theory -> theory |
26 val add_shuffle_rule: thm -> theory -> theory |
27 val shuffle_attr: theory attribute |
27 val shuffle_attr: theory attribute |
28 |
28 |
29 val setup : (theory -> theory) list |
29 val setup : theory -> theory |
30 end |
30 end |
31 |
31 |
32 structure Shuffler :> Shuffler = |
32 structure Shuffler :> Shuffler = |
33 struct |
33 struct |
34 |
34 |
682 else ShuffleData.put (thm::shuffles) thy |
682 else ShuffleData.put (thm::shuffles) thy |
683 end |
683 end |
684 |
684 |
685 fun shuffle_attr (thy,thm) = (add_shuffle_rule thm thy,thm) |
685 fun shuffle_attr (thy,thm) = (add_shuffle_rule thm thy,thm) |
686 |
686 |
687 val setup = [Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around"), |
687 val setup = |
688 Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems"), |
688 Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #> |
689 ShuffleData.init, |
689 Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems") #> |
690 add_shuffle_rule weaken, |
690 ShuffleData.init #> |
691 add_shuffle_rule equiv_comm, |
691 add_shuffle_rule weaken #> |
692 add_shuffle_rule imp_comm, |
692 add_shuffle_rule equiv_comm #> |
693 add_shuffle_rule Drule.norm_hhf_eq, |
693 add_shuffle_rule imp_comm #> |
694 add_shuffle_rule Drule.triv_forall_equality, |
694 add_shuffle_rule Drule.norm_hhf_eq #> |
695 Attrib.add_attributes [("shuffle_rule",(Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]] |
695 add_shuffle_rule Drule.triv_forall_equality #> |
|
696 Attrib.add_attributes [("shuffle_rule", (Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")] |
|
697 |
696 end |
698 end |