theory Command

imports Main

keywords "foobar" "foobar_trace" :: thy_decl and

         "foobar_goal" "foobar_prove" :: thy_goal

begin

let

   val do_nothing = Scan.succeed (Local_Theory.background_theory I)

in

   Outer_Syntax.local_theory @{command_spec "foobar"} 

     "description of foobar" 

       do_nothing

end

let

  fun trace_prop str =

     Local_Theory.background_theory (fn lthy => (tracing str; lthy))

  val trace_prop_parser = Parse.prop >> trace_prop

in

  Outer_Syntax.local_theory @{command_spec "foobar_trace"} 

    "traces a proposition"

      trace_prop_parser

end

let

   fun prove_prop str lthy =

     let

       val prop = Syntax.read_prop lthy str

     in

       Proof.theorem NONE (K I) [[(prop,[])]] lthy

     end;

   val prove_prop_parser = Parse.prop >> prove_prop

in

   Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} 

     "proving a proposition"

       prove_prop_parser

end

structure Result = Proof_Data(

  type T = unit -> term

  fun init thy () = error "Result")

val result_cookie = (Result.get, Result.put, "Result.put")

let

   fun after_qed thm_name thms lthy =

        Local_Theory.note (thm_name, (flat thms)) lthy |> snd

   fun setup_proof (thm_name, {text, ...}) lthy =

   let

     val trm = Code_Runtime.value lthy result_cookie ("", text)

   in

     Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy

   end

   val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source

in

   Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"} 

     "proving a proposition" 

        (parser >> setup_proof)

end