src/HOL/TLA/Memory/ProcedureInterface.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 9517 f58863b1406a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:        ProcedureInterface.ML
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@6255
     6
    Procedure interface (theorems and proofs)
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@3807
     9
Addsimps [slice_def];
wenzelm@6255
    10
val mem_css = (claset(), simpset());
wenzelm@3807
    11
wenzelm@3807
    12
(* ---------------------------------------------------------------------------- *)
wenzelm@3807
    13
wenzelm@6255
    14
val Procedure_defs = [caller_def, rtrner_def, Calling_def, 
wenzelm@3807
    15
                      Call_def, Return_def,
wenzelm@3807
    16
		      PLegalCaller_def, LegalCaller_def,
wenzelm@3807
    17
		      PLegalReturner_def, LegalReturner_def];
wenzelm@3807
    18
wenzelm@3807
    19
(* sample theorems (not used in the proof):
wenzelm@3807
    20
   1. calls and returns are mutually exclusive
wenzelm@3807
    21
wenzelm@6255
    22
qed_goal "CallNotReturn" ProcedureInterface.thy
wenzelm@6255
    23
     "|- Call ch p v --> ~ Return ch p w"
wenzelm@6255
    24
  (fn prems => [ auto_tac (temp_css addsimps2 [Call_def,Return_def]) ]);
wenzelm@3807
    25
wenzelm@3807
    26
wenzelm@3807
    27
  2. enabledness of calls and returns
wenzelm@3807
    28
wenzelm@3807
    29
qed_goal "Call_enabled" ProcedureInterface.thy
wenzelm@6255
    30
   "!!p. basevars ((caller ch)!p) ==> |- ~ Calling ch p --> Enabled (Call ch p v)"
wenzelm@4089
    31
   (fn _ => [action_simp_tac (simpset() addsimps [caller_def, Call_def]) 
wenzelm@3807
    32
                             [] [base_enabled,Pair_inject] 1
wenzelm@3807
    33
            ]);
wenzelm@3807
    34
wenzelm@6255
    35
qed_goal "Call_enabled_rew" ProcedureInterface.thy
wenzelm@6255
    36
   "basevars ((caller ch)!p) ==> |- Enabled (Call ch p v) = (~Calling ch p)"
wenzelm@6255
    37
   (fn [prem] => [auto_tac (mem_css addsimps2 [Call_def]),
wenzelm@6255
    38
                  force_tac (mem_css addsimps2 [enabled_def]) 1,
wenzelm@6255
    39
                  enabled_tac prem 1,
wenzelm@6255
    40
                  action_simp_tac (simpset() addsimps [caller_def]) [] [Pair_inject] 1
wenzelm@6255
    41
            ]);
wenzelm@6255
    42
wenzelm@3807
    43
qed_goal "Return_enabled" ProcedureInterface.thy
wenzelm@6255
    44
   "!!p. basevars ((rtrner ch)!p) ==> |- Calling ch p --> Enabled (Return ch p v)"
wenzelm@4089
    45
   (fn _ => [action_simp_tac (simpset() addsimps [rtrner_def, Return_def]) 
wenzelm@3807
    46
                             [] [base_enabled,Pair_inject] 1
wenzelm@3807
    47
            ]);
wenzelm@3807
    48
wenzelm@3807
    49
*)
wenzelm@3807
    50
wenzelm@3807
    51
(* Calls and returns change their subchannel *)
wenzelm@3807
    52
qed_goal "Call_changed" ProcedureInterface.thy
wenzelm@6255
    53
   "|- Call ch p v --> <Call ch p v>_((caller ch)!p)"
wenzelm@6255
    54
   (fn _ => [ auto_tac (mem_css addsimps2 [angle_def,Call_def,caller_def,Calling_def]) ]);
wenzelm@3807
    55
wenzelm@3807
    56
qed_goal "Return_changed" ProcedureInterface.thy
wenzelm@6255
    57
   "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)"
wenzelm@6255
    58
   (fn _ => [ auto_tac (mem_css addsimps2 [angle_def,Return_def,rtrner_def,Calling_def]) ]);
wenzelm@3807
    59
wenzelm@3807
    60