converted to Isar theory format;
authorwenzelm
Sat Sep 17 20:14:30 2005 +0200 (2005-09-17)
changeset 17477ceb42ea2f223
parent 17476 315cb57e3dd7
child 17478 1865064ca82a
converted to Isar theory format;
src/HOL/IMPP/Com.ML
src/HOL/IMPP/Com.thy
src/HOL/IMPP/EvenOdd.ML
src/HOL/IMPP/EvenOdd.thy
src/HOL/IMPP/Hoare.ML
src/HOL/IMPP/Hoare.thy
src/HOL/IMPP/Misc.thy
src/HOL/IMPP/Natural.ML
src/HOL/IMPP/Natural.thy
     1.1 --- a/src/HOL/IMPP/Com.ML	Sat Sep 17 19:17:35 2005 +0200
     1.2 +++ b/src/HOL/IMPP/Com.ML	Sat Sep 17 20:14:30 2005 +0200
     1.3 @@ -1,3 +1,5 @@
     1.4 +(* $Id$ *)
     1.5 +
     1.6  val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
     1.7  
     1.8  Goalw [body_def] "finite (dom body)";
     1.9 @@ -9,9 +11,4 @@
    1.10  by (Fast_tac 1);
    1.11  qed "WT_bodiesD";
    1.12  
    1.13 -val WTs_elim_cases = map WTs.mk_cases
    1.14 -   ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", 
    1.15 -    "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
    1.16 -    "WT (BODY P)", "WT (X:=CALL P(a))"];
    1.17 -
    1.18  AddSEs WTs_elim_cases;
     2.1 --- a/src/HOL/IMPP/Com.thy	Sat Sep 17 19:17:35 2005 +0200
     2.2 +++ b/src/HOL/IMPP/Com.thy	Sat Sep 17 20:14:30 2005 +0200
     2.3 @@ -2,80 +2,89 @@
     2.4      ID:       $Id$
     2.5      Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     2.6      Copyright 1999 TUM
     2.7 -
     2.8 -Semantics of arithmetic and boolean expressions, Syntax of commands
     2.9  *)
    2.10  
    2.11 -Com = Main +
    2.12 +header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
    2.13  
    2.14 -types	 val = nat   (* for the meta theory, this may be anything, but with
    2.15 +theory Com
    2.16 +imports Main
    2.17 +begin
    2.18 +
    2.19 +types    val = nat   (* for the meta theory, this may be anything, but with
    2.20                          current Isabelle, types cannot be refined later *)
    2.21 -types	 glb
    2.22 -         loc
    2.23 -arities	 (*val,*)glb,loc :: type
    2.24 -consts   Arg, Res :: loc
    2.25 +typedecl glb
    2.26 +typedecl loc
    2.27 +
    2.28 +consts
    2.29 +  Arg :: loc
    2.30 +  Res :: loc
    2.31  
    2.32  datatype vname  = Glb glb | Loc loc
    2.33 -types	 globs  = glb => val
    2.34 -	 locals = loc => val
    2.35 +types    globs  = "glb => val"
    2.36 +         locals = "loc => val"
    2.37  datatype state  = st globs locals
    2.38  (* for the meta theory, the following would be sufficient:
    2.39 -types    state
    2.40 -arities  state::type
    2.41 -consts   st:: [globs , locals] => state
    2.42 +typedecl state
    2.43 +consts   st :: "[globs , locals] => state"
    2.44  *)
    2.45 -types	 aexp   = state => val
    2.46 -	 bexp   = state => bool
    2.47 +types    aexp   = "state => val"
    2.48 +         bexp   = "state => bool"
    2.49  
    2.50 -types	pname
    2.51 -arities	pname  :: type
    2.52 +typedecl pname
    2.53  
    2.54  datatype com
    2.55        = SKIP
    2.56 -      | Ass   vname aexp	("_:==_"	        [65, 65    ] 60)
    2.57 -      | Local loc aexp com	("LOCAL _:=_ IN _"	[65,  0, 61] 60)
    2.58 -      | Semi  com  com		("_;; _"	        [59, 60    ] 59)
    2.59 -      | Cond  bexp com com	("IF _ THEN _ ELSE _"	[65, 60, 61] 60)
    2.60 -      | While bexp com		("WHILE _ DO _"		[65,     61] 60)
    2.61 +      | Ass   vname aexp        ("_:==_"                [65, 65    ] 60)
    2.62 +      | Local loc aexp com      ("LOCAL _:=_ IN _"      [65,  0, 61] 60)
    2.63 +      | Semi  com  com          ("_;; _"                [59, 60    ] 59)
    2.64 +      | Cond  bexp com com      ("IF _ THEN _ ELSE _"   [65, 60, 61] 60)
    2.65 +      | While bexp com          ("WHILE _ DO _"         [65,     61] 60)
    2.66        | BODY  pname
    2.67 -      | Call  vname pname aexp	("_:=CALL _'(_')"	[65, 65,  0] 60)
    2.68 +      | Call  vname pname aexp  ("_:=CALL _'(_')"       [65, 65,  0] 60)
    2.69  
    2.70  consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
    2.71         body   :: " pname ~=> com"
    2.72 -defs   body_def  "body == map_of bodies"
    2.73 +defs   body_def: "body == map_of bodies"
    2.74  
    2.75  
    2.76  (* Well-typedness: all procedures called must exist *)
    2.77 -consts WTs :: com set
    2.78 -syntax WT  :: com => bool
    2.79 +consts WTs :: "com set"
    2.80 +syntax WT  :: "com => bool"
    2.81  translations "WT c" == "c : WTs"
    2.82  
    2.83 -inductive WTs intrs
    2.84 +inductive WTs intros
    2.85  
    2.86 -    Skip    "WT SKIP"
    2.87 +    Skip:    "WT SKIP"
    2.88  
    2.89 -    Assign  "WT (X :== a)"
    2.90 +    Assign:  "WT (X :== a)"
    2.91  
    2.92 -    Local   "WT c ==>
    2.93 -             WT (LOCAL Y := a IN c)"
    2.94 +    Local:   "WT c ==>
    2.95 +              WT (LOCAL Y := a IN c)"
    2.96  
    2.97 -    Semi    "[| WT c0; WT c1 |] ==>
    2.98 -             WT (c0;; c1)"
    2.99 +    Semi:    "[| WT c0; WT c1 |] ==>
   2.100 +              WT (c0;; c1)"
   2.101  
   2.102 -    If      "[| WT c0; WT c1 |] ==>
   2.103 -             WT (IF b THEN c0 ELSE c1)"
   2.104 +    If:      "[| WT c0; WT c1 |] ==>
   2.105 +              WT (IF b THEN c0 ELSE c1)"
   2.106  
   2.107 -    While   "WT c ==>
   2.108 -             WT (WHILE b DO c)"
   2.109 +    While:   "WT c ==>
   2.110 +              WT (WHILE b DO c)"
   2.111  
   2.112 -    Body    "body pn ~= None ==>
   2.113 -             WT (BODY pn)"
   2.114 +    Body:    "body pn ~= None ==>
   2.115 +              WT (BODY pn)"
   2.116  
   2.117 -    Call    "WT (BODY pn) ==>
   2.118 -             WT (X:=CALL pn(a))"
   2.119 +    Call:    "WT (BODY pn) ==>
   2.120 +              WT (X:=CALL pn(a))"
   2.121 +
   2.122 +inductive_cases WTs_elim_cases:
   2.123 +  "WT SKIP"  "WT (X:==a)"  "WT (LOCAL Y:=a IN c)"
   2.124 +  "WT (c1;;c2)"  "WT (IF b THEN c1 ELSE c2)"  "WT (WHILE b DO c)"
   2.125 +  "WT (BODY P)"  "WT (X:=CALL P(a))"
   2.126  
   2.127  constdefs
   2.128    WT_bodies :: bool
   2.129 - "WT_bodies == !(pn,b):set bodies. WT b"
   2.130 +  "WT_bodies == !(pn,b):set bodies. WT b"
   2.131 +
   2.132 +ML {* use_legacy_bindings (the_context ()) *}
   2.133  
   2.134  end
     3.1 --- a/src/HOL/IMPP/EvenOdd.ML	Sat Sep 17 19:17:35 2005 +0200
     3.2 +++ b/src/HOL/IMPP/EvenOdd.ML	Sat Sep 17 20:14:30 2005 +0200
     3.3 @@ -4,7 +4,7 @@
     3.4      Copyright   1999 TUM
     3.5  *)
     3.6  
     3.7 -section "even"; 
     3.8 +section "even";
     3.9  
    3.10  Goalw [even_def] "even 0";
    3.11  by (Simp_tac 1);
    3.12 @@ -71,14 +71,14 @@
    3.13  by (res_inst_tac [("Q","%Z s. ?P Z s & Res_ok Z s")] hoare_derivs.Comp 1);
    3.14  by (rtac export_s 1);
    3.15  by  (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"),
    3.16 -		   ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
    3.17 +                   ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
    3.18  by (rtac (single_asm RS conseq2) 1);
    3.19  by   (clarsimp_tac Arg_Res_css 1);
    3.20  by  (force_tac Arg_Res_css 1);
    3.21  by (rtac export_s 1);
    3.22  by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"),
    3.23 -		  ("Q1","%Z s. even Z = (s<Arg> = 0)")]
    3.24 -		 (Call_invariant RS conseq12) 1);
    3.25 +                  ("Q1","%Z s. even Z = (s<Arg> = 0)")]
    3.26 +                 (Call_invariant RS conseq12) 1);
    3.27  by (rtac (single_asm RS conseq2) 1);
    3.28  by  (clarsimp_tac Arg_Res_css 1);
    3.29  by (force_tac Arg_Res_css 1);
    3.30 @@ -97,7 +97,7 @@
    3.31  
    3.32  Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
    3.33  by (rtac conseq1 1);
    3.34 -by  (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"), 
    3.35 +by  (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"),
    3.36        ("P","%pn. Z=Arg+(if pn = Odd then 1 else 0)"),
    3.37        ("Q","%pn. Res_ok")] Body1 1);
    3.38  by    Auto_tac;
     4.1 --- a/src/HOL/IMPP/EvenOdd.thy	Sat Sep 17 19:17:35 2005 +0200
     4.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Sat Sep 17 20:14:30 2005 +0200
     4.3 @@ -2,20 +2,24 @@
     4.4      ID:         $Id$
     4.5      Author:     David von Oheimb
     4.6      Copyright   1999 TUM
     4.7 -
     4.8 -Example of mutually recursive procedures verified with Hoare logic
     4.9  *)
    4.10  
    4.11 -EvenOdd = Misc +
    4.12 +header {* Example of mutually recursive procedures verified with Hoare logic *}
    4.13  
    4.14 -constdefs even :: nat => bool
    4.15 +theory EvenOdd
    4.16 +imports Misc
    4.17 +begin
    4.18 +
    4.19 +constdefs
    4.20 +  even :: "nat => bool"
    4.21    "even n == 2 dvd n"
    4.22  
    4.23  consts
    4.24 -  Even, Odd :: pname
    4.25 -rules 
    4.26 -  Even_neq_Odd "Even ~= Odd"
    4.27 -  Arg_neq_Res  "Arg  ~= Res"
    4.28 +  Even :: pname
    4.29 +  Odd :: pname
    4.30 +axioms
    4.31 +  Even_neq_Odd: "Even ~= Odd"
    4.32 +  Arg_neq_Res:  "Arg  ~= Res"
    4.33  
    4.34  constdefs
    4.35    evn :: com
    4.36 @@ -30,13 +34,15 @@
    4.37           ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
    4.38  
    4.39  defs
    4.40 -  bodies_def "bodies == [(Even,evn),(Odd,odd)]"
    4.41 -  
    4.42 +  bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
    4.43 +
    4.44  consts
    4.45 -  Z_eq_Arg_plus   :: nat => nat assn ("Z=Arg+_" [50]50)
    4.46 - "even_Z=(Res=0)" ::        nat assn ("Res'_ok")
    4.47 +  Z_eq_Arg_plus   :: "nat => nat assn" ("Z=Arg+_" [50]50)
    4.48 + "even_Z=(Res=0)" ::        "nat assn" ("Res'_ok")
    4.49  defs
    4.50 -  Z_eq_Arg_plus_def "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
    4.51 -  Res_ok_def       "Res_ok   == %Z s. even Z = (s<Res> = 0)"
    4.52 +  Z_eq_Arg_plus_def: "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
    4.53 +  Res_ok_def:       "Res_ok   == %Z s. even Z = (s<Res> = 0)"
    4.54 +
    4.55 +ML {* use_legacy_bindings (the_context ()) *}
    4.56  
    4.57  end
     5.1 --- a/src/HOL/IMPP/Hoare.ML	Sat Sep 17 19:17:35 2005 +0200
     5.2 +++ b/src/HOL/IMPP/Hoare.ML	Sat Sep 17 20:14:30 2005 +0200
     5.3 @@ -6,8 +6,8 @@
     5.4  Soundness and relative completeness of Hoare rules wrt operational semantics
     5.5  *)
     5.6  
     5.7 -Goalw [state_not_singleton_def] 
     5.8 -	"state_not_singleton ==> !t. (!s::state. s = t) --> False";
     5.9 +Goalw [state_not_singleton_def]
    5.10 +        "state_not_singleton ==> !t. (!s::state. s = t) --> False";
    5.11  by (Clarify_tac 1);
    5.12  by (case_tac "ta = t" 1);
    5.13  by  (ALLGOALS (blast_tac (HOL_cs addDs [not_sym])));
    5.14 @@ -18,7 +18,7 @@
    5.15  
    5.16  section "validity";
    5.17  
    5.18 -Goalw [triple_valid_def] 
    5.19 +Goalw [triple_valid_def]
    5.20    "|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))";
    5.21  by Auto_tac;
    5.22  qed "triple_valid_def2";
    5.23 @@ -105,16 +105,16 @@
    5.24  Goal "G'||-ts ==> !G. G' <= G --> G||-ts";
    5.25  by (etac hoare_derivs.induct 1);
    5.26  by                (ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]));
    5.27 -by (rtac 		  hoare_derivs.empty 1);
    5.28 +by (rtac                  hoare_derivs.empty 1);
    5.29  by               (eatac hoare_derivs.insert 1 1);
    5.30  by              (fast_tac (claset() addIs [hoare_derivs.asm]) 1);
    5.31  by             (fast_tac (claset() addIs [hoare_derivs.cut]) 1);
    5.32  by            (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
    5.33  by           (EVERY'[rtac hoare_derivs.conseq, strip_tac, smp_tac 2,Clarify_tac,
    5.34 -	             smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1);
    5.35 -by          (EVERY'[rtac hoare_derivs.Body,dtac spec,etac mp,Fast_tac] 7); 
    5.36 -by         (ALLGOALS (resolve_tac ((funpow 5 tl) hoare_derivs.intrs)
    5.37 -	              THEN_ALL_NEW Fast_tac));
    5.38 +                     smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1);
    5.39 +by          (EVERY'[rtac hoare_derivs.Body,dtac spec,etac mp,Fast_tac] 7);
    5.40 +by         (ALLGOALS (resolve_tac ((funpow 5 tl) hoare_derivs.intros)
    5.41 +                      THEN_ALL_NEW Fast_tac));
    5.42  qed_spec_mp "thin";
    5.43  
    5.44  Goal "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}";
    5.45 @@ -178,8 +178,8 @@
    5.46  by          (Blast_tac 1); (* asm *)
    5.47  by         (Blast_tac 1); (* cut *)
    5.48  by        (Blast_tac 1); (* weaken *)
    5.49 -by       (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs", 
    5.50 -	                   Simp_tac, Clarify_tac, REPEAT o smp_tac 1]));
    5.51 +by       (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs",
    5.52 +                           Simp_tac, Clarify_tac, REPEAT o smp_tac 1]));
    5.53  by       (ALLGOALS (full_simp_tac (simpset() addsimps [triple_valid_def2])));
    5.54  by       (EVERY'[strip_tac, smp_tac 2, Blast_tac] 1); (* conseq *)
    5.55  by      (ALLGOALS Clarsimp_tac); (* Skip, Ass, Local *)
    5.56 @@ -212,18 +212,13 @@
    5.57  by (Blast_tac 1);
    5.58  qed "MGT_alternD";
    5.59  
    5.60 -Goalw [MGT_def] 
    5.61 +Goalw [MGT_def]
    5.62   "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}";
    5.63  by (etac conseq12 1);
    5.64 -by (clarsimp_tac (claset(), simpset() addsimps 
    5.65 +by (clarsimp_tac (claset(), simpset() addsimps
    5.66    [hoare_valids_def,eval_eq,triple_valid_def2]) 1);
    5.67  qed "MGF_complete";
    5.68  
    5.69 -val WTs_elim_cases = map WTs.mk_cases
    5.70 -   ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", 
    5.71 -    "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
    5.72 -    "WT (BODY P)", "WT (X:=CALL P(a))"];
    5.73 -
    5.74  AddSEs WTs_elim_cases;
    5.75  (* requires com_det, escape (i.e. hoare_derivs.conseq) *)
    5.76  Goal "state_not_singleton ==> \
    5.77 @@ -234,15 +229,15 @@
    5.78  by (etac MGT_alternD 6);
    5.79  by       (rewtac MGT_def);
    5.80  by       (EVERY'[dtac bspec, etac (thm"domI")] 7);
    5.81 -by       (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac 
    5.82 -	     [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")]
    5.83 -	     (hoare_derivs.Call RS conseq1), etac conseq12] 7);
    5.84 +by       (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
    5.85 +             [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")]
    5.86 +             (hoare_derivs.Call RS conseq1), etac conseq12] 7);
    5.87  by        (ALLGOALS (etac thin_rl));
    5.88  by (rtac (hoare_derivs.Skip RS conseq2) 1);
    5.89  by (rtac (hoare_derivs.Ass RS conseq1) 2);
    5.90 -by        (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac 
    5.91 -	          [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")] 
    5.92 -		  (hoare_derivs.Local RS conseq1), etac conseq12] 3);
    5.93 +by        (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
    5.94 +                  [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")]
    5.95 +                  (hoare_derivs.Local RS conseq1), etac conseq12] 3);
    5.96  by         (EVERY'[etac hoare_derivs.Comp, etac conseq12] 5);
    5.97  by         ((rtac hoare_derivs.If THEN_ALL_NEW etac conseq12) 6);
    5.98  by          (EVERY'[rtac (hoare_derivs.Loop RS conseq2), etac conseq12] 8);
    5.99 @@ -278,7 +273,7 @@
   5.100  by   (Fast_tac 1);
   5.101  by (dtac finite_subset 1);
   5.102  by (etac finite_imageI 1);
   5.103 -by (Asm_simp_tac 1); 
   5.104 +by (Asm_simp_tac 1);
   5.105  by (arith_tac 1);
   5.106  qed_spec_mp "nesting_lemma";
   5.107  
   5.108 @@ -329,8 +324,8 @@
   5.109  by (make_imp_tac 1);
   5.110  by (etac finite_induct 1);
   5.111  by  (ALLGOALS (clarsimp_tac (
   5.112 -	claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
   5.113 -	simpset() delsimps [range_composition])));
   5.114 +        claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
   5.115 +        simpset() delsimps [range_composition])));
   5.116  by (etac MGF_lemma1 1);
   5.117  by  (fast_tac (claset() addDs [WT_bodiesD]) 2);
   5.118  by (Clarsimp_tac 1);
   5.119 @@ -354,7 +349,7 @@
   5.120  qed "MGF'";
   5.121  
   5.122  (* requires Body+empty+insert / BodyN, com_det *)
   5.123 -bind_thm ("hoare_complete", MGF' RS MGF_complete); 
   5.124 +bind_thm ("hoare_complete", MGF' RS MGF_complete);
   5.125  
   5.126  section "unused derived rules";
   5.127  
     6.1 --- a/src/HOL/IMPP/Hoare.thy	Sat Sep 17 19:17:35 2005 +0200
     6.2 +++ b/src/HOL/IMPP/Hoare.thy	Sat Sep 17 20:14:30 2005 +0200
     6.3 @@ -2,98 +2,106 @@
     6.4      ID:         $Id$
     6.5      Author:     David von Oheimb
     6.6      Copyright   1999 TUM
     6.7 -
     6.8 -Inductive definition of Hoare logic for partial correctness
     6.9 -Completeness is taken relative to completeness of the underlying logic
    6.10 -Two versions of completeness proof:
    6.11 -  nested single recursion vs. simultaneous recursion in call rule
    6.12  *)
    6.13  
    6.14 -Hoare = Natural + 
    6.15 +header {* Inductive definition of Hoare logic for partial correctness *}
    6.16 +
    6.17 +theory Hoare
    6.18 +imports Natural
    6.19 +begin
    6.20 +
    6.21 +text {*
    6.22 +  Completeness is taken relative to completeness of the underlying logic.
    6.23 +
    6.24 +  Two versions of completeness proof: nested single recursion
    6.25 +  vs. simultaneous recursion in call rule
    6.26 +*}
    6.27  
    6.28  types 'a assn = "'a => state => bool"
    6.29  translations
    6.30 -      "a assn"   <= (type)"a => state => bool"
    6.31 +  "a assn"   <= (type)"a => state => bool"
    6.32  
    6.33  constdefs
    6.34    state_not_singleton :: bool
    6.35 - "state_not_singleton == ? s t::state. s ~= t" (* at least two elements *)
    6.36 +  "state_not_singleton == \<exists>s t::state. s ~= t" (* at least two elements *)
    6.37  
    6.38    peek_and    :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35)
    6.39 - "peek_and P p == %Z s. P Z s & p s"
    6.40 +  "peek_and P p == %Z s. P Z s & p s"
    6.41  
    6.42  datatype 'a triple =
    6.43 -    triple ('a assn) com ('a assn)         ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
    6.44 -  
    6.45 +  triple "'a assn"  com  "'a assn"       ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
    6.46 +
    6.47  consts
    6.48 -  triple_valid ::            nat => 'a triple     => bool ( "|=_:_" [0 , 58] 57)
    6.49 -  hoare_valids ::  'a triple set => 'a triple set => bool ("_||=_"  [58, 58] 57)
    6.50 -  hoare_derivs ::"('a triple set *  'a triple set)   set"
    6.51 +  triple_valid ::            "nat => 'a triple     => bool" ( "|=_:_" [0 , 58] 57)
    6.52 +  hoare_valids ::  "'a triple set => 'a triple set => bool" ("_||=_"  [58, 58] 57)
    6.53 +  hoare_derivs :: "('a triple set *  'a triple set)   set"
    6.54  syntax
    6.55 -  triples_valid::            nat => 'a triple set => bool ("||=_:_" [0 , 58] 57)
    6.56 -  hoare_valid  ::  'a triple set => 'a triple     => bool ("_|=_"   [58, 58] 57)
    6.57 -"@hoare_derivs"::  'a triple set => 'a triple set => bool ("_||-_"  [58, 58] 57)
    6.58 -"@hoare_deriv" ::  'a triple set => 'a triple     => bool ("_|-_"   [58, 58] 57)
    6.59 +  triples_valid::            "nat => 'a triple set => bool" ("||=_:_" [0 , 58] 57)
    6.60 +  hoare_valid  ::  "'a triple set => 'a triple     => bool" ("_|=_"   [58, 58] 57)
    6.61 +"@hoare_derivs"::  "'a triple set => 'a triple set => bool" ("_||-_"  [58, 58] 57)
    6.62 +"@hoare_deriv" ::  "'a triple set => 'a triple     => bool" ("_|-_"   [58, 58] 57)
    6.63  
    6.64 -defs triple_valid_def  "|=n:t  ==  case t of {P}.c.{Q} =>
    6.65 -		                !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')"
    6.66 +defs triple_valid_def: "|=n:t  ==  case t of {P}.c.{Q} =>
    6.67 +                                !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')"
    6.68  translations          "||=n:G" == "Ball G (triple_valid n)"
    6.69 -defs hoare_valids_def"G||=ts   ==  !n. ||=n:G --> ||=n:ts"
    6.70 +defs hoare_valids_def: "G||=ts   ==  !n. ||=n:G --> ||=n:ts"
    6.71  translations         "G |=t  " == " G||={t}"
    6.72                       "G||-ts"  == "(G,ts) : hoare_derivs"
    6.73                       "G |-t"   == " G||-{t}"
    6.74  
    6.75  (* Most General Triples *)
    6.76 -constdefs MGT    :: com => state triple              ("{=}._.{->}" [60] 58)
    6.77 +constdefs MGT    :: "com => state triple"            ("{=}._.{->}" [60] 58)
    6.78           "{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}"
    6.79  
    6.80 -inductive hoare_derivs intrs
    6.81 -  
    6.82 -  empty    "G||-{}"
    6.83 -  insert"[| G |-t;  G||-ts |]
    6.84 -	==> G||-insert t ts"
    6.85 +inductive hoare_derivs intros
    6.86 +
    6.87 +  empty:    "G||-{}"
    6.88 +  insert: "[| G |-t;  G||-ts |]
    6.89 +        ==> G||-insert t ts"
    6.90  
    6.91 -  asm	   "ts <= G ==>
    6.92 -	    G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *)
    6.93 +  asm:      "ts <= G ==>
    6.94 +             G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *)
    6.95  
    6.96 -  cut   "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *)
    6.97 +  cut:   "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *)
    6.98  
    6.99 -  weaken"[| G||-ts' ; ts <= ts' |] ==> G||-ts"
   6.100 +  weaken: "[| G||-ts' ; ts <= ts' |] ==> G||-ts"
   6.101  
   6.102 -  conseq"!Z s. P  Z  s --> (? P' Q'. G|-{P'}.c.{Q'} &
   6.103 -                                  (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s'))
   6.104 -         ==> G|-{P}.c.{Q}"
   6.105 +  conseq: "!Z s. P  Z  s --> (? P' Q'. G|-{P'}.c.{Q'} &
   6.106 +                                   (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s'))
   6.107 +          ==> G|-{P}.c.{Q}"
   6.108  
   6.109  
   6.110 -  Skip	"G|-{P}. SKIP .{P}"
   6.111 +  Skip:  "G|-{P}. SKIP .{P}"
   6.112  
   6.113 -  Ass	"G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}"
   6.114 +  Ass:   "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}"
   6.115  
   6.116 -  Local	"G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])}
   6.117 -     ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}"
   6.118 +  Local: "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])}
   6.119 +      ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}"
   6.120  
   6.121 -  Comp	"[| G|-{P}.c.{Q};
   6.122 -	    G|-{Q}.d.{R} |]
   6.123 -	==> G|-{P}. (c;;d) .{R}"
   6.124 +  Comp:  "[| G|-{P}.c.{Q};
   6.125 +             G|-{Q}.d.{R} |]
   6.126 +         ==> G|-{P}. (c;;d) .{R}"
   6.127  
   6.128 -  If	"[| G|-{P &>        b }.c.{Q};
   6.129 -	    G|-{P &> (Not o b)}.d.{Q} |]
   6.130 -	==> G|-{P}. IF b THEN c ELSE d .{Q}"
   6.131 +  If:    "[| G|-{P &>        b }.c.{Q};
   6.132 +             G|-{P &> (Not o b)}.d.{Q} |]
   6.133 +         ==> G|-{P}. IF b THEN c ELSE d .{Q}"
   6.134  
   6.135 -  Loop  "G|-{P &> b}.c.{P} ==>
   6.136 -	 G|-{P}. WHILE b DO c .{P &> (Not o b)}"
   6.137 +  Loop:  "G|-{P &> b}.c.{P} ==>
   6.138 +          G|-{P}. WHILE b DO c .{P &> (Not o b)}"
   6.139  
   6.140  (*
   6.141 -  BodyN	"(insert ({P}. BODY pn  .{Q}) G)
   6.142 -	  |-{P}.  the (body pn) .{Q} ==>
   6.143 -	 G|-{P}.       BODY pn  .{Q}"
   6.144 +  BodyN: "(insert ({P}. BODY pn  .{Q}) G)
   6.145 +           |-{P}.  the (body pn) .{Q} ==>
   6.146 +          G|-{P}.       BODY pn  .{Q}"
   6.147  *)
   6.148 -  Body	"[| G Un (%p. {P p}.      BODY p  .{Q p})`Procs
   6.149 -	      ||-(%p. {P p}. the (body p) .{Q p})`Procs |]
   6.150 -	==>  G||-(%p. {P p}.      BODY p  .{Q p})`Procs"
   6.151 +  Body:  "[| G Un (%p. {P p}.      BODY p  .{Q p})`Procs
   6.152 +               ||-(%p. {P p}. the (body p) .{Q p})`Procs |]
   6.153 +         ==>  G||-(%p. {P p}.      BODY p  .{Q p})`Procs"
   6.154  
   6.155 -  Call	   "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
   6.156 -	==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
   6.157 -	    X:=CALL pn(a) .{Q}"
   6.158 +  Call:     "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
   6.159 +         ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
   6.160 +             X:=CALL pn(a) .{Q}"
   6.161 +
   6.162 +ML {* use_legacy_bindings (the_context ()) *}
   6.163  
   6.164  end
     7.1 --- a/src/HOL/IMPP/Misc.thy	Sat Sep 17 19:17:35 2005 +0200
     7.2 +++ b/src/HOL/IMPP/Misc.thy	Sat Sep 17 20:14:30 2005 +0200
     7.3 @@ -2,18 +2,22 @@
     7.4      ID:         $Id$
     7.5      Author:     David von Oheimb
     7.6      Copyright   1999 TUM
     7.7 +*)
     7.8  
     7.9 -Several examples for Hoare logic
    7.10 -*)
    7.11 -Misc = Hoare +
    7.12 +header {* Several examples for Hoare logic *}
    7.13 +
    7.14 +theory Misc
    7.15 +imports Hoare
    7.16 +begin
    7.17  
    7.18  defs
    7.19 -  newlocs_def "newlocs       == %x. arbitrary"
    7.20 -  setlocs_def "setlocs s l'  == case s of st g l => st g l'"
    7.21 -  getlocs_def "getlocs s     == case s of st g l => l"
    7.22 -   update_def "update s vn v == case vn of
    7.23 -                              Glb gn => (case s of st g l => st (g(gn:=v)) l)
    7.24 -                            | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    7.25 +  newlocs_def: "newlocs       == %x. arbitrary"
    7.26 +  setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
    7.27 +  getlocs_def: "getlocs s     == case s of st g l => l"
    7.28 +   update_def: "update s vn v == case vn of
    7.29 +                               Glb gn => (case s of st g l => st (g(gn:=v)) l)
    7.30 +                             | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    7.31 +
    7.32 +ML {* use_legacy_bindings (the_context ()) *}
    7.33  
    7.34  end
    7.35 -  
    7.36 \ No newline at end of file
     8.1 --- a/src/HOL/IMPP/Natural.ML	Sat Sep 17 19:17:35 2005 +0200
     8.2 +++ b/src/HOL/IMPP/Natural.ML	Sat Sep 17 20:14:30 2005 +0200
     8.3 @@ -4,21 +4,8 @@
     8.4      Copyright   1999 TUM
     8.5  *)
     8.6  
     8.7 -open Natural;
     8.8 -
     8.9 -AddIs evalc.intrs;
    8.10 -AddIs evaln.intrs;
    8.11 -
    8.12 -val evalc_elim_cases = map evalc.mk_cases
    8.13 -   ["<SKIP,s> -c-> t", "<X:==a,s> -c-> t", "<LOCAL Y:=a IN c,s> -c-> t", 
    8.14 -    "<c1;;c2,s> -c-> t","<IF b THEN c1 ELSE c2,s> -c-> t",
    8.15 -    "<BODY P,s> -c-> s1", "<X:=CALL P(a),s> -c-> s1"];
    8.16 -val evaln_elim_cases = map evaln.mk_cases
    8.17 -   ["<SKIP,s> -n-> t", "<X:==a,s> -n-> t", "<LOCAL Y:=a IN c,s> -n-> t",
    8.18 -    "<c1;;c2,s> -n-> t","<IF b THEN c1 ELSE c2,s> -n-> t",
    8.19 -    "<BODY P,s> -n-> s1", "<X:=CALL P(a),s> -n-> s1"];
    8.20 -val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
    8.21 -val evaln_WHILE_case = evaln.mk_cases "<WHILE b DO c,s> -n-> t";
    8.22 +AddIs evalc.intros;
    8.23 +AddIs evaln.intros;
    8.24  
    8.25  AddSEs evalc_elim_cases;
    8.26  AddSEs evaln_elim_cases;
    8.27 @@ -33,7 +20,7 @@
    8.28  
    8.29  Goal "<c,s> -n-> t ==> <c,s> -c-> t";
    8.30  by (etac evaln.induct 1);
    8.31 -by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac));
    8.32 +by (ALLGOALS (resolve_tac evalc.intros THEN_ALL_NEW atac));
    8.33  qed "evaln_evalc";
    8.34  
    8.35  Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";
    8.36 @@ -46,7 +33,7 @@
    8.37  Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t";
    8.38  by (etac evaln.induct 1);
    8.39  by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1]));
    8.40 -by (ALLGOALS (resolve_tac evaln.intrs THEN_ALL_NEW atac));
    8.41 +by (ALLGOALS (resolve_tac evaln.intros THEN_ALL_NEW atac));
    8.42  qed_spec_mp "evaln_nonstrict";
    8.43  
    8.44  Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'";
    8.45 @@ -64,7 +51,7 @@
    8.46  by (etac evalc.induct 1);
    8.47  by (ALLGOALS (REPEAT o etac exE));
    8.48  by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]]));
    8.49 -by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intrs THEN_ALL_NEW atac));
    8.50 +by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intros THEN_ALL_NEW atac));
    8.51  qed "evalc_evaln";
    8.52  
    8.53  Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)";
     9.1 --- a/src/HOL/IMPP/Natural.thy	Sat Sep 17 19:17:35 2005 +0200
     9.2 +++ b/src/HOL/IMPP/Natural.thy	Sat Sep 17 20:14:30 2005 +0200
     9.3 @@ -2,88 +2,111 @@
     9.4      ID:         $Id$
     9.5      Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     9.6      Copyright   1999 TUM
     9.7 -
     9.8 -Natural semantics of commands
     9.9  *)
    9.10  
    9.11 -Natural = Com + 
    9.12 +header {* Natural semantics of commands *}
    9.13 +
    9.14 +theory Natural
    9.15 +imports Com
    9.16 +begin
    9.17  
    9.18  (** Execution of commands **)
    9.19 -consts	 evalc :: "(com * state *       state) set"
    9.20 -       "@evalc":: [com,state,    state] => bool	("<_,_>/ -c-> _" [0,0,  51] 51)
    9.21 -	 evaln :: "(com * state * nat * state) set"
    9.22 -       "@evaln":: [com,state,nat,state] => bool	("<_,_>/ -_-> _" [0,0,0,51] 51)
    9.23 +consts
    9.24 +  evalc :: "(com * state *       state) set"
    9.25 +  evaln :: "(com * state * nat * state) set"
    9.26  
    9.27 -translations  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
    9.28 -              "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
    9.29 +syntax
    9.30 +  "@evalc":: "[com,state,    state] => bool"  ("<_,_>/ -c-> _" [0,0,  51] 51)
    9.31 +  "@evaln":: "[com,state,nat,state] => bool"  ("<_,_>/ -_-> _" [0,0,0,51] 51)
    9.32 +
    9.33 +translations
    9.34 +  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
    9.35 +  "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
    9.36  
    9.37  consts
    9.38    newlocs :: locals
    9.39 -  setlocs :: state => locals => state
    9.40 -  getlocs :: state => locals
    9.41 -  update  :: state => vname => val => state	("_/[_/::=/_]" [900,0,0] 900)
    9.42 +  setlocs :: "state => locals => state"
    9.43 +  getlocs :: "state => locals"
    9.44 +  update  :: "state => vname => val => state"     ("_/[_/::=/_]" [900,0,0] 900)
    9.45  syntax (* IN Natural.thy *)
    9.46 -  loc :: state => locals    ("_<_>" [75,0] 75)
    9.47 +  loc :: "state => locals"    ("_<_>" [75,0] 75)
    9.48  translations
    9.49    "s<X>" == "getlocs s X"
    9.50  
    9.51  inductive evalc
    9.52 -  intrs
    9.53 -    Skip    "<SKIP,s> -c-> s"
    9.54 +  intros
    9.55 +    Skip:    "<SKIP,s> -c-> s"
    9.56  
    9.57 -    Assign  "<X :== a,s> -c-> s[X::=a s]"
    9.58 +    Assign:  "<X :== a,s> -c-> s[X::=a s]"
    9.59  
    9.60 -    Local   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
    9.61 -             <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
    9.62 +    Local:   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
    9.63 +              <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
    9.64  
    9.65 -    Semi    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
    9.66 -             <c0;; c1, s0> -c-> s2"
    9.67 +    Semi:    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
    9.68 +              <c0;; c1, s0> -c-> s2"
    9.69  
    9.70 -    IfTrue  "[| b s; <c0,s> -c-> s1 |] ==>
    9.71 -             <IF b THEN c0 ELSE c1, s> -c-> s1"
    9.72 +    IfTrue:  "[| b s; <c0,s> -c-> s1 |] ==>
    9.73 +              <IF b THEN c0 ELSE c1, s> -c-> s1"
    9.74  
    9.75 -    IfFalse "[| ~b s; <c1,s> -c-> s1 |] ==>
    9.76 -             <IF b THEN c0 ELSE c1, s> -c-> s1"
    9.77 +    IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==>
    9.78 +              <IF b THEN c0 ELSE c1, s> -c-> s1"
    9.79  
    9.80 -    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
    9.81 +    WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
    9.82  
    9.83 -    WhileTrue  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
    9.84 -                <WHILE b DO c, s0> -c-> s2"
    9.85 +    WhileTrue:  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
    9.86 +                 <WHILE b DO c, s0> -c-> s2"
    9.87  
    9.88 -    Body       "<the (body pn), s0> -c-> s1 ==>
    9.89 -                <BODY pn, s0> -c-> s1"
    9.90 +    Body:       "<the (body pn), s0> -c-> s1 ==>
    9.91 +                 <BODY pn, s0> -c-> s1"
    9.92  
    9.93 -    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
    9.94 -                <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
    9.95 -                                         [X::=s1<Res>]"
    9.96 +    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
    9.97 +                 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
    9.98 +                                          [X::=s1<Res>]"
    9.99  
   9.100  inductive evaln
   9.101 -  intrs
   9.102 -    Skip    "<SKIP,s> -n-> s"
   9.103 +  intros
   9.104 +    Skip:    "<SKIP,s> -n-> s"
   9.105 +
   9.106 +    Assign:  "<X :== a,s> -n-> s[X::=a s]"
   9.107  
   9.108 -    Assign  "<X :== a,s> -n-> s[X::=a s]"
   9.109 +    Local:   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
   9.110 +              <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
   9.111 +
   9.112 +    Semi:    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
   9.113 +              <c0;; c1, s0> -n-> s2"
   9.114  
   9.115 -    Local   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
   9.116 -             <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
   9.117 +    IfTrue:  "[| b s; <c0,s> -n-> s1 |] ==>
   9.118 +              <IF b THEN c0 ELSE c1, s> -n-> s1"
   9.119  
   9.120 -    Semi    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
   9.121 -             <c0;; c1, s0> -n-> s2"
   9.122 +    IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
   9.123 +              <IF b THEN c0 ELSE c1, s> -n-> s1"
   9.124  
   9.125 -    IfTrue  "[| b s; <c0,s> -n-> s1 |] ==>
   9.126 -             <IF b THEN c0 ELSE c1, s> -n-> s1"
   9.127 +    WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
   9.128 +
   9.129 +    WhileTrue:  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
   9.130 +                 <WHILE b DO c, s0> -n-> s2"
   9.131  
   9.132 -    IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
   9.133 -             <IF b THEN c0 ELSE c1, s> -n-> s1"
   9.134 +    Body:       "<the (body pn), s0> -    n-> s1 ==>
   9.135 +                 <BODY pn, s0> -Suc n-> s1"
   9.136  
   9.137 -    WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"
   9.138 +    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
   9.139 +                 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
   9.140 +                                          [X::=s1<Res>]"
   9.141  
   9.142 -    WhileTrue  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
   9.143 -                <WHILE b DO c, s0> -n-> s2"
   9.144  
   9.145 -    Body       "<the (body pn), s0> -    n-> s1 ==>
   9.146 -                <BODY pn, s0> -Suc n-> s1"
   9.147 +inductive_cases evalc_elim_cases:
   9.148 +  "<SKIP,s> -c-> t"  "<X:==a,s> -c-> t"  "<LOCAL Y:=a IN c,s> -c-> t"
   9.149 +  "<c1;;c2,s> -c-> t"  "<IF b THEN c1 ELSE c2,s> -c-> t"
   9.150 +  "<BODY P,s> -c-> s1"  "<X:=CALL P(a),s> -c-> s1"
   9.151  
   9.152 -    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
   9.153 -                <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
   9.154 -                                         [X::=s1<Res>]"
   9.155 +inductive_cases evaln_elim_cases:
   9.156 +  "<SKIP,s> -n-> t"  "<X:==a,s> -n-> t"  "<LOCAL Y:=a IN c,s> -n-> t"
   9.157 +  "<c1;;c2,s> -n-> t"  "<IF b THEN c1 ELSE c2,s> -n-> t"
   9.158 +  "<BODY P,s> -n-> s1"  "<X:=CALL P(a),s> -n-> s1"
   9.159 +
   9.160 +inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
   9.161 +inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
   9.162 +
   9.163 +ML {* use_legacy_bindings (the_context ()) *}
   9.164 +
   9.165  end