author blanchet Mon, 06 Jun 2011 20:36:35 +0200 changeset 43172 ea57961db57e parent 43171 37e1431cc213 child 43173 b98daa96d043
tuning
```--- a/src/HOL/Metis_Examples/Typings.thy	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/Typings.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -8,7 +8,6 @@
imports Main
begin

-
text {* Setup for testing Metis exhaustively *}

lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
@@ -28,46 +27,47 @@
constr (poly, level, heaviness))
[Preds, Tags])

-fun metis_exhaust_tac ctxt ths =
+fun metis_eXhaust_tac ctxt ths =
let
-    fun tac [] = all_tac
-      | tac (type_sys :: type_syss) =
-        (if null type_syss then all_tac else rtac @{thm fork} 1)
-        THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1
-        THEN COND (has_fewer_prems 2) all_tac no_tac
-        THEN tac type_syss
+    fun tac [] st = all_tac st
+      | tac (type_sys :: type_syss) st =
+        st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
+           |> ((if null type_syss then all_tac else rtac @{thm fork} 1)
+               THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1
+               THEN COND (has_fewer_prems 2) all_tac no_tac
+               THEN tac type_syss)
in tac end
*}

-method_setup metis_exhaust = {*
+method_setup metis_eXhaust = {*
Attrib.thms >>
-    (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_syss))
+    (fn ths => fn ctxt => SIMPLE_METHOD (metis_eXhaust_tac ctxt ths type_syss))
*} "exhaustively run the new Metis with all type encodings"

text {* Metis tests *}

lemma "x = y \<Longrightarrow> y = x"
-by metis_exhaust
+by metis_eXhaust

lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
-by (metis_exhaust last.simps)
+by (metis_eXhaust last.simps)

lemma "map Suc [0] = [Suc 0]"
-by (metis_exhaust map.simps)
+by (metis_eXhaust map.simps)

lemma "map Suc [1 + 1] = [Suc 2]"

lemma "map Suc [2] = [Suc (1 + 1)]"