Theory ML_Util

theory ML_Util
  imports Main
begin

(* Printing util *)
ML ‹
  fun pretty_cterm ctxt ctm = Syntax.pretty_term ctxt (Thm.term_of ctm)
  val string_of_cterm = Pretty.string_of oo pretty_cterm
  val string_of_term = Pretty.string_of oo Syntax.pretty_term
›

(* Printing util *)
ML ‹
  fun string_of_thm ctxt = string_of_cterm ctxt o Thm.cprop_of
›

ML ‹
val term_pat_setup =
  let
    val parser = Args.context -- Scan.lift Args.name
      fun term_pat (ctxt, str) =
        str
        |> Proof_Context.read_term_pattern ctxt
        |> ML_Syntax.print_term
        |> ML_Syntax.atomic
in
  ML_Antiquotation.inline @{binding "term_pat"} (parser >> term_pat) end
›

setup ‹term_pat_setup›

ML ‹
fun match_resolve ctxt concl goal thm =
  let
      val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm)
      val insts = Thm.first_order_match (concl, concl_pat)
    in
      (Drule.instantiate_normalize insts goal |> resolve_tac ctxt [thm] 1)
    end handle Pattern.MATCH => Seq.empty
val fo_assm_tac = Subgoal.FOCUS_PREMS (
    fn {context = ctxt, concl, prems, ...} => fn goal =>
      Seq.maps (match_resolve ctxt concl goal) (Seq.of_list prems)
  )
›

schematic_goal "c s ⟹ c ?x"
  apply (tactic ‹fo_assm_tac @{context} 1›)
  done

schematic_goal "c s ⟹ ?P s"
  apply (tactic ‹fo_assm_tac @{context} 1›)
  done

ML ‹
fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct)
val refl_match_tac = Subgoal.FOCUS_PREMS (
  fn {context = ctxt, concl, ...} =>
    let
      val stripped = Thm.dest_arg concl
      val (l, r) = dest_binop stripped
      val insts =
        Thm.first_order_match (r, l)
        handle Pattern.MATCH => Thm.first_order_match (l, r)
    in
      Seq.single o Drule.instantiate_normalize insts THEN
      resolve_tac ctxt [@{thm HOL.refl}] 1
    end
    handle CTERM _ => no_tac | Pattern.MATCH => no_tac
  )
›

schematic_goal
  "x = ?x"
  by (tactic ‹refl_match_tac @{context} 1›)

schematic_goal
  "?x = x"
  by (tactic ‹refl_match_tac @{context} 1›)

ML ‹fun assumption ctxt = SIMPLE_METHOD (fo_assm_tac ctxt 1)›
ML ‹fun refl_match ctxt = SIMPLE_METHOD (refl_match_tac ctxt 1)›

method_setup fo_assumption =
  ‹Scan.succeed assumption› ‹Prove by assumption with first-order matching›

method_setup refl_match =
  ‹Scan.succeed refl_match› ‹Prove equality by reflexivity with first-order matching›

end