equal
deleted
inserted
replaced
22 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |
22 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |
23 |
23 |
24 ML {* |
24 ML {* |
25 (* The commented-out type systems are too incomplete for our exhaustive |
25 (* The commented-out type systems are too incomplete for our exhaustive |
26 tests. *) |
26 tests. *) |
27 val type_syss = |
27 val type_encs = |
28 ["erased", |
28 ["erased", |
29 "poly_preds", |
29 "poly_preds", |
30 "poly_preds_heavy", |
30 "poly_preds_heavy", |
31 "poly_tags", |
31 "poly_tags", |
32 "poly_tags_heavy", |
32 "poly_tags_heavy", |
70 "simple!"] |
70 "simple!"] |
71 |
71 |
72 fun metis_exhaust_tac ctxt ths = |
72 fun metis_exhaust_tac ctxt ths = |
73 let |
73 let |
74 fun tac [] st = all_tac st |
74 fun tac [] st = all_tac st |
75 | tac (type_sys :: type_syss) st = |
75 | tac (type_enc :: type_encs) st = |
76 st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *) |
76 st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *) |
77 |> ((if null type_syss then all_tac else rtac @{thm fork} 1) |
77 |> ((if null type_encs then all_tac else rtac @{thm fork} 1) |
78 THEN Metis_Tactics.metis_tac [type_sys] ctxt ths 1 |
78 THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1 |
79 THEN COND (has_fewer_prems 2) all_tac no_tac |
79 THEN COND (has_fewer_prems 2) all_tac no_tac |
80 THEN tac type_syss) |
80 THEN tac type_encs) |
81 in tac end |
81 in tac end |
82 *} |
82 *} |
83 |
83 |
84 method_setup metis_exhaust = {* |
84 method_setup metis_exhaust = {* |
85 Attrib.thms >> |
85 Attrib.thms >> |
86 (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_syss)) |
86 (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_encs)) |
87 *} "exhaustively run the new Metis with all type encodings" |
87 *} "exhaustively run the new Metis with all type encodings" |
88 |
88 |
89 |
89 |
90 text {* Miscellaneous tests *} |
90 text {* Miscellaneous tests *} |
91 |
91 |