theory Method
imports Main
begin



section {* A simple method *}

ML {*
val q1_syntax = Scan.succeed
*}

ML {*
fun q1_method ctxt = SIMPLE_METHOD'
  (Simplifier.simp_tac (Simplifier.context ctxt HOL_ss))
*}

method_setup Q1 = {* q1_syntax q1_method *} "The Q method"

lemma True by Q1





section {* Select a Subgoal *}

ML {*
val q2_syntax = OuterParse.nat
*}

ML {*
fun q2_method i ctxt = SIMPLE_METHOD
  (Simplifier.simp_tac (Simplifier.context ctxt HOL_ss) i)
*}

method_setup Q2 = {* Scan.lift q2_syntax >> q2_method *}
  "The Q method"

lemma "True = (True \<and> True)"
  apply (intro iffI conjI)
  apply (Q2 3)
  sorry





section {* Adding Theorems *}

ML {*
val q3_syntax =
  Scan.lift (Args.add -- Args.colon) |-- Attrib.thms
*}

ML {*
fun q3_method thms _ = SIMPLE_METHOD'
  (Tactic.resolve_tac thms)
*}

method_setup Q3 = {* q3_syntax >> q3_method *}
  "The Q method"

lemma "t = t" by (Q3 add: refl)





section {* Using the Context *}

ML {*
structure Q4_Rules = NamedThmsFun
(
  val name = "q4"
  val description = "q4 rules"
)
*}
setup Q4_Rules.setup

ML {*
fun q4_method ctxt = SIMPLE_METHOD'
  (Tactic.resolve_tac (Q4_Rules.get ctxt))
*}

ML {*
Q4_Rules.add
*}

ML {*
val q4_syntax = Method.sections [
  Args.add -- Args.colon >> K (I, Q4_Rules.add)]
*}

method_setup Q4 = {* q4_syntax >> K q4_method *}
  "The Q method"

lemma "t = t" by (Q4 add: refl)
lemma "t = t" by (Q4 add: refl sym)
lemma "t = t" by (Q4 add: refl add: sym)

lemma "t = t" using refl[q4] by Q4





section {* A Method Option *}

ML {*
val q5_opts = Scan.optional
  (Args.parens (Args.$$$ "strict" >> K true))
  false

val q5_syntax =
  Scan.lift q5_opts --
  (Method.sections [
    Args.add -- Args.colon >> K (I, Q4_Rules.add)] >> flat)
*}

ML {*
fun q5_method (strict, thms) ctxt =
  let val ths = if strict then thms else Q4_Rules.get ctxt
  in SIMPLE_METHOD' (Tactic.resolve_tac ths) end
*}

method_setup Q5 = {* q5_syntax >> q5_method *}
  "The Q method"

lemma "t = t" by (Q5 add: refl)
lemma "t = t" using refl[q4] by Q5
(*
lemma "t = t" using refl[q4] by (Q5 (strict))
lemma "t = t" using refl[q4] by (Q5 (strict) add: conjI)
*)
lemma "t = t" by (Q5 (strict) add: refl)


end