--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/progtut/Tactical.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,64 @@
+theory Tactical
+imports Advanced
+begin
+
+ML {*
+fun my_print_tac ctxt thm =
+let
+   val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))
+in
+   Seq.single thm
+end
+*}
+
+ML {*
+let
+   val ctxt = @{context}
+   val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
+in
+   Goal.prove ctxt ["x", "y", "u", "v", "P", "Q"] [@{prop "x = y"}, @{prop "u = v"}] goal
+    (fn {prems = pms, context = ctxt} =>  
+              (my_print_tac ctxt)
+              THEN etac @{thm disjE} 1 THEN
+               (my_print_tac ctxt) 
+              THEN rtac @{thm disjI2} 1
+              THEN  (my_print_tac ctxt) 
+              THEN atac 1
+              THEN rtac @{thm disjI1} 1
+              THEN atac 1)
+end
+*}
+
+ML {*
+  Goal.prove
+*}
+
+ML {*
+fun pretty_cterms ctxt ctrms =
+  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))
+*}
+
+ML {*
+fun foc_tac {prems, params, asms, concl, context, schematics} =
+let
+  fun assgn1 f1 f2 xs =
+    let
+       val out = map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs
+    in
+       Pretty.list "" "" out
+    end
+  fun assgn2 f xs = assgn1 f f xs
+  val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp])
+    [("params: ", assgn1 Pretty.str (pretty_cterm context) params),
+     ("assumptions: ", pretty_cterms context asms),
+     ("conclusion: ", pretty_cterm context concl),
+     ("premises: ", pretty_thms_no_vars context prems),
+     ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))]
+in
+  tracing (Pretty.string_of (Pretty.chunks pps)); all_tac
+end
+*}
+
+notation (output) "prop"   ("#_" [1000] 1000)
+
+end