Theory Refine_Imperative_HOL.Term_Synth

section ‹Rule-Based Synthesis of Terms›
theory Term_Synth
imports Sepref_Misc
begin
  definition SYNTH_TERM :: "'a::{} ⇒ 'b::{} ⇒ bool"
    ― ‹Indicate synthesis of @{term y} from @{term x}.›
    where [simp]: "SYNTH_TERM x y ≡ True"
  consts SDUMMY :: "'a :: {}"
    ― ‹After synthesis has been completed, these are replaced by fresh schematic variable›

  named_theorems_rev synth_rules ‹Term synthesis rules›

  text ‹Term synthesis works by proving @{term "SYNTH_TERM t v"}, by repeatedly applying the 
    first matching intro-rule from ‹synth_rules›.  ›


ML ‹
  signature TERM_SYNTH = sig
    (* Synthesize something from term t. The initial list of theorems is
      added to beginning of synth_rules, and can be used to install intro-rules
      for SYNTH_TERM.*)
    val synth_term: thm list -> Proof.context -> term -> term
  end


  structure Term_Synth : TERM_SYNTH = struct

    (* Assumption: Term does not contain dummy variables *)
    fun replace_sdummies t = let
      fun r (t1$t2) n = let
              val (t1,n) = r t1 n
              val (t2,n) = r t2 n
            in (t1$t2,n) end
        | r (Abs (x,T,t)) n = let
              val (t,n) = r t n
            in (Abs (x,T,t),n) end
        | r @{mpat (typs) "SDUMMY::?'v_T"} n = (Var (("_dummy",n),T),n+1)
        | r (t' as (Var ((name,_),_))) n = if String.isPrefix "_" name then raise TERM ("replace_sdummies: Term already contains dummy patterns",[t',t]) else (t',n)
        | r t n = (t,n)
    in
      fst (r t 0)
    end    

    (* Use synthesis rules to transform the given term *)
    fun synth_term thms ctxt t = let
      val orig_ctxt = ctxt
      val (t,ctxt) = yield_singleton (Variable.import_terms true) t ctxt
      val v = Var (("result",0),TVar (("T",0),[]))
      val goal = @{mk_term "Trueprop (SYNTH_TERM ?t ?v)"} |> Thm.cterm_of ctxt
  
      val rules = thms @ Named_Theorems_Rev.get ctxt @{named_theorems_rev synth_rules}
        |> Tactic.build_net
      fun tac ctxt = ALLGOALS (TRY_SOLVED' (
        REPEAT_DETERM' (CHANGED o resolve_from_net_tac ctxt rules)))
      
      val thm = Goal.prove_internal ctxt [] goal (fn _ => tac ctxt)

      val res = case Thm.concl_of thm of
          @{mpat "Trueprop (SYNTH_TERM _ ?res)"} => res 
        | _ => raise THM("Synth_Term: Proved a different theorem?",~1,[thm])

      val res = singleton (Variable.export_terms ctxt orig_ctxt) res
        |> replace_sdummies
  
    in
      res
    end
  end  
›



end