# File ProcedureInterface.ML

    (*
        File:        ProcedureInterface.ML
        ID:          $Id: ProcedureInterface.ML,v 1.5 2005/09/07 18:22:42 wenzelm Exp $
        Author:      Stephan Merz
        Copyright:   1997 University of Munich

        Procedure interface (theorems and proofs)
    *)

    Addsimps [slice_def];
    val mem_css = (claset(), simpset());

    (* ---------------------------------------------------------------------------- *)

    val Procedure_defs = [caller_def, rtrner_def, Calling_def,
                          Call_def, Return_def,
                          PLegalCaller_def, LegalCaller_def,
                          PLegalReturner_def, LegalReturner_def];

    (* Calls and returns change their subchannel *)
    Goal "|- Call ch p v --> <Call ch p v>_((caller ch)!p)";
    by (auto_tac (mem_css addsimps2 [angle_def,Call_def,caller_def,Calling_def]));
    qed "Call_changed";

    Goal "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)";
    by (auto_tac (mem_css addsimps2 [angle_def,Return_def,rtrner_def,Calling_def]));
    qed "Return_changed";