1 theory MLs

     2 imports Pure

     3 keywords "ML_psf" :: prf_script and

     4          "ML_goal" :: thy_goal

     5 begin

     6 

     7 section {* ML for proof state transformation *}

     8 

     9 ML {*

    10   structure ML_psf = Proof_Data (

    11     type T = Proof.state -> Proof.state

    12     fun init _ = undefined

    13   )

    14 *}

    15 

    16 

    17 ML {*

    18  fun ml_psf (txt, pos) state =   

    19         (((Proof.context_of state) |>

    20          Context.proof_map (ML_Context.expression Position.none 

    21                  "val psf : Proof.state -> Proof.state"

    22                   "Context.map_proof (ML_psf.put psf)"  (ML_Lex.read pos txt)) |>

    23          ML_psf.get) state):Proof.state

    24 *}

    25 

    26 ML {*

    27 val _ =

    28   Outer_Syntax.command @{command_spec "ML_psf"} "ML state transfer function"

    29     (Parse.ML_source >> (Toplevel.print oo (Toplevel.proof o ml_psf)))

    30 *}

    31 

    32 section {* ML for global goal establishment *}

    33 

    34 ML {*

    35   structure ML_goal = Proof_Data (

    36     type T = local_theory -> Proof.state

    37     fun init _ = undefined

    38   )

    39 *}

    40 

    41 ML {*

    42  fun ml_goal (txt, pos) ctxt =   

    43         ((ctxt |>

    44          Context.proof_map (ML_Context.expression Position.none 

    45                  "val goalf : local_theory -> Proof.state"

    46                   "Context.map_proof (ML_goal.put goalf)"  (ML_Lex.read pos txt)) |>

    47          ML_goal.get) ctxt) :Proof.state

    48 *}

    49 

    50 ML {*

    51 val _ =

    52   Outer_Syntax.local_theory_to_proof @{command_spec "ML_goal"} "ML goal function"

    53     (Parse.ML_source >> ml_goal)

    54 *}

    55 

    56 ML {*

    57   fun start_theorem prop = Proof.theorem NONE (K I) [[(prop, [])]]

    58 *}

    59 

    60 end

    61