# HG changeset patch
# User wenzelm
# Date 1126980870 -7200
# Node ID ceb42ea2f223efb2365784a8d1142852880457d4
# Parent  315cb57e3dd73d210dad64f1618762d93a94d5d9
converted to Isar theory format;

diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Com.ML
--- a/src/HOL/IMPP/Com.ML	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Com.ML	Sat Sep 17 20:14:30 2005 +0200
@@ -1,3 +1,5 @@
+(* $Id$ *)
+
 val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
 
 Goalw [body_def] "finite (dom body)";
@@ -9,9 +11,4 @@
 by (Fast_tac 1);
 qed "WT_bodiesD";
 
-val WTs_elim_cases = map WTs.mk_cases
-   ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", 
-    "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
-    "WT (BODY P)", "WT (X:=CALL P(a))"];
-
 AddSEs WTs_elim_cases;
diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Com.thy
--- a/src/HOL/IMPP/Com.thy	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Com.thy	Sat Sep 17 20:14:30 2005 +0200
@@ -2,80 +2,89 @@
     ID:       $Id$
     Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     Copyright 1999 TUM
-
-Semantics of arithmetic and boolean expressions, Syntax of commands
 *)
 
-Com = Main +
+header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
 
-types	 val = nat   (* for the meta theory, this may be anything, but with
+theory Com
+imports Main
+begin
+
+types    val = nat   (* for the meta theory, this may be anything, but with
                         current Isabelle, types cannot be refined later *)
-types	 glb
-         loc
-arities	 (*val,*)glb,loc :: type
-consts   Arg, Res :: loc
+typedecl glb
+typedecl loc
+
+consts
+  Arg :: loc
+  Res :: loc
 
 datatype vname  = Glb glb | Loc loc
-types	 globs  = glb => val
-	 locals = loc => val
+types    globs  = "glb => val"
+         locals = "loc => val"
 datatype state  = st globs locals
 (* for the meta theory, the following would be sufficient:
-types    state
-arities  state::type
-consts   st:: [globs , locals] => state
+typedecl state
+consts   st :: "[globs , locals] => state"
 *)
-types	 aexp   = state => val
-	 bexp   = state => bool
+types    aexp   = "state => val"
+         bexp   = "state => bool"
 
-types	pname
-arities	pname  :: type
+typedecl pname
 
 datatype com
       = SKIP
-      | Ass   vname aexp	("_:==_"	        [65, 65    ] 60)
-      | Local loc aexp com	("LOCAL _:=_ IN _"	[65,  0, 61] 60)
-      | Semi  com  com		("_;; _"	        [59, 60    ] 59)
-      | Cond  bexp com com	("IF _ THEN _ ELSE _"	[65, 60, 61] 60)
-      | While bexp com		("WHILE _ DO _"		[65,     61] 60)
+      | Ass   vname aexp        ("_:==_"                [65, 65    ] 60)
+      | Local loc aexp com      ("LOCAL _:=_ IN _"      [65,  0, 61] 60)
+      | Semi  com  com          ("_;; _"                [59, 60    ] 59)
+      | Cond  bexp com com      ("IF _ THEN _ ELSE _"   [65, 60, 61] 60)
+      | While bexp com          ("WHILE _ DO _"         [65,     61] 60)
       | BODY  pname
-      | Call  vname pname aexp	("_:=CALL _'(_')"	[65, 65,  0] 60)
+      | Call  vname pname aexp  ("_:=CALL _'(_')"       [65, 65,  0] 60)
 
 consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
        body   :: " pname ~=> com"
-defs   body_def  "body == map_of bodies"
+defs   body_def: "body == map_of bodies"
 
 
 (* Well-typedness: all procedures called must exist *)
-consts WTs :: com set
-syntax WT  :: com => bool
+consts WTs :: "com set"
+syntax WT  :: "com => bool"
 translations "WT c" == "c : WTs"
 
-inductive WTs intrs
+inductive WTs intros
 
-    Skip    "WT SKIP"
+    Skip:    "WT SKIP"
 
-    Assign  "WT (X :== a)"
+    Assign:  "WT (X :== a)"
 
-    Local   "WT c ==>
-             WT (LOCAL Y := a IN c)"
+    Local:   "WT c ==>
+              WT (LOCAL Y := a IN c)"
 
-    Semi    "[| WT c0; WT c1 |] ==>
-             WT (c0;; c1)"
+    Semi:    "[| WT c0; WT c1 |] ==>
+              WT (c0;; c1)"
 
-    If      "[| WT c0; WT c1 |] ==>
-             WT (IF b THEN c0 ELSE c1)"
+    If:      "[| WT c0; WT c1 |] ==>
+              WT (IF b THEN c0 ELSE c1)"
 
-    While   "WT c ==>
-             WT (WHILE b DO c)"
+    While:   "WT c ==>
+              WT (WHILE b DO c)"
 
-    Body    "body pn ~= None ==>
-             WT (BODY pn)"
+    Body:    "body pn ~= None ==>
+              WT (BODY pn)"
 
-    Call    "WT (BODY pn) ==>
-             WT (X:=CALL pn(a))"
+    Call:    "WT (BODY pn) ==>
+              WT (X:=CALL pn(a))"
+
+inductive_cases WTs_elim_cases:
+  "WT SKIP"  "WT (X:==a)"  "WT (LOCAL Y:=a IN c)"
+  "WT (c1;;c2)"  "WT (IF b THEN c1 ELSE c2)"  "WT (WHILE b DO c)"
+  "WT (BODY P)"  "WT (X:=CALL P(a))"
 
 constdefs
   WT_bodies :: bool
- "WT_bodies == !(pn,b):set bodies. WT b"
+  "WT_bodies == !(pn,b):set bodies. WT b"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/EvenOdd.ML
--- a/src/HOL/IMPP/EvenOdd.ML	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/EvenOdd.ML	Sat Sep 17 20:14:30 2005 +0200
@@ -4,7 +4,7 @@
     Copyright   1999 TUM
 *)
 
-section "even"; 
+section "even";
 
 Goalw [even_def] "even 0";
 by (Simp_tac 1);
@@ -71,14 +71,14 @@
 by (res_inst_tac [("Q","%Z s. ?P Z s & Res_ok Z s")] hoare_derivs.Comp 1);
 by (rtac export_s 1);
 by  (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"),
-		   ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
+                   ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
 by (rtac (single_asm RS conseq2) 1);
 by   (clarsimp_tac Arg_Res_css 1);
 by  (force_tac Arg_Res_css 1);
 by (rtac export_s 1);
 by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"),
-		  ("Q1","%Z s. even Z = (s<Arg> = 0)")]
-		 (Call_invariant RS conseq12) 1);
+                  ("Q1","%Z s. even Z = (s<Arg> = 0)")]
+                 (Call_invariant RS conseq12) 1);
 by (rtac (single_asm RS conseq2) 1);
 by  (clarsimp_tac Arg_Res_css 1);
 by (force_tac Arg_Res_css 1);
@@ -97,7 +97,7 @@
 
 Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
 by (rtac conseq1 1);
-by  (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"), 
+by  (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"),
       ("P","%pn. Z=Arg+(if pn = Odd then 1 else 0)"),
       ("Q","%pn. Res_ok")] Body1 1);
 by    Auto_tac;
diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/EvenOdd.thy
--- a/src/HOL/IMPP/EvenOdd.thy	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy	Sat Sep 17 20:14:30 2005 +0200
@@ -2,20 +2,24 @@
     ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 TUM
-
-Example of mutually recursive procedures verified with Hoare logic
 *)
 
-EvenOdd = Misc +
+header {* Example of mutually recursive procedures verified with Hoare logic *}
 
-constdefs even :: nat => bool
+theory EvenOdd
+imports Misc
+begin
+
+constdefs
+  even :: "nat => bool"
   "even n == 2 dvd n"
 
 consts
-  Even, Odd :: pname
-rules 
-  Even_neq_Odd "Even ~= Odd"
-  Arg_neq_Res  "Arg  ~= Res"
+  Even :: pname
+  Odd :: pname
+axioms
+  Even_neq_Odd: "Even ~= Odd"
+  Arg_neq_Res:  "Arg  ~= Res"
 
 constdefs
   evn :: com
@@ -30,13 +34,15 @@
          ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
 
 defs
-  bodies_def "bodies == [(Even,evn),(Odd,odd)]"
-  
+  bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
+
 consts
-  Z_eq_Arg_plus   :: nat => nat assn ("Z=Arg+_" [50]50)
- "even_Z=(Res=0)" ::        nat assn ("Res'_ok")
+  Z_eq_Arg_plus   :: "nat => nat assn" ("Z=Arg+_" [50]50)
+ "even_Z=(Res=0)" ::        "nat assn" ("Res'_ok")
 defs
-  Z_eq_Arg_plus_def "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
-  Res_ok_def       "Res_ok   == %Z s. even Z = (s<Res> = 0)"
+  Z_eq_Arg_plus_def: "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
+  Res_ok_def:       "Res_ok   == %Z s. even Z = (s<Res> = 0)"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Hoare.ML
--- a/src/HOL/IMPP/Hoare.ML	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Hoare.ML	Sat Sep 17 20:14:30 2005 +0200
@@ -6,8 +6,8 @@
 Soundness and relative completeness of Hoare rules wrt operational semantics
 *)
 
-Goalw [state_not_singleton_def] 
-	"state_not_singleton ==> !t. (!s::state. s = t) --> False";
+Goalw [state_not_singleton_def]
+        "state_not_singleton ==> !t. (!s::state. s = t) --> False";
 by (Clarify_tac 1);
 by (case_tac "ta = t" 1);
 by  (ALLGOALS (blast_tac (HOL_cs addDs [not_sym])));
@@ -18,7 +18,7 @@
 
 section "validity";
 
-Goalw [triple_valid_def] 
+Goalw [triple_valid_def]
   "|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))";
 by Auto_tac;
 qed "triple_valid_def2";
@@ -105,16 +105,16 @@
 Goal "G'||-ts ==> !G. G' <= G --> G||-ts";
 by (etac hoare_derivs.induct 1);
 by                (ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]));
-by (rtac 		  hoare_derivs.empty 1);
+by (rtac                  hoare_derivs.empty 1);
 by               (eatac hoare_derivs.insert 1 1);
 by              (fast_tac (claset() addIs [hoare_derivs.asm]) 1);
 by             (fast_tac (claset() addIs [hoare_derivs.cut]) 1);
 by            (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
 by           (EVERY'[rtac hoare_derivs.conseq, strip_tac, smp_tac 2,Clarify_tac,
-	             smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1);
-by          (EVERY'[rtac hoare_derivs.Body,dtac spec,etac mp,Fast_tac] 7); 
-by         (ALLGOALS (resolve_tac ((funpow 5 tl) hoare_derivs.intrs)
-	              THEN_ALL_NEW Fast_tac));
+                     smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1);
+by          (EVERY'[rtac hoare_derivs.Body,dtac spec,etac mp,Fast_tac] 7);
+by         (ALLGOALS (resolve_tac ((funpow 5 tl) hoare_derivs.intros)
+                      THEN_ALL_NEW Fast_tac));
 qed_spec_mp "thin";
 
 Goal "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}";
@@ -178,8 +178,8 @@
 by          (Blast_tac 1); (* asm *)
 by         (Blast_tac 1); (* cut *)
 by        (Blast_tac 1); (* weaken *)
-by       (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs", 
-	                   Simp_tac, Clarify_tac, REPEAT o smp_tac 1]));
+by       (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs",
+                           Simp_tac, Clarify_tac, REPEAT o smp_tac 1]));
 by       (ALLGOALS (full_simp_tac (simpset() addsimps [triple_valid_def2])));
 by       (EVERY'[strip_tac, smp_tac 2, Blast_tac] 1); (* conseq *)
 by      (ALLGOALS Clarsimp_tac); (* Skip, Ass, Local *)
@@ -212,18 +212,13 @@
 by (Blast_tac 1);
 qed "MGT_alternD";
 
-Goalw [MGT_def] 
+Goalw [MGT_def]
  "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}";
 by (etac conseq12 1);
-by (clarsimp_tac (claset(), simpset() addsimps 
+by (clarsimp_tac (claset(), simpset() addsimps
   [hoare_valids_def,eval_eq,triple_valid_def2]) 1);
 qed "MGF_complete";
 
-val WTs_elim_cases = map WTs.mk_cases
-   ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", 
-    "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
-    "WT (BODY P)", "WT (X:=CALL P(a))"];
-
 AddSEs WTs_elim_cases;
 (* requires com_det, escape (i.e. hoare_derivs.conseq) *)
 Goal "state_not_singleton ==> \
@@ -234,15 +229,15 @@
 by (etac MGT_alternD 6);
 by       (rewtac MGT_def);
 by       (EVERY'[dtac bspec, etac (thm"domI")] 7);
-by       (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac 
-	     [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")]
-	     (hoare_derivs.Call RS conseq1), etac conseq12] 7);
+by       (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
+             [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")]
+             (hoare_derivs.Call RS conseq1), etac conseq12] 7);
 by        (ALLGOALS (etac thin_rl));
 by (rtac (hoare_derivs.Skip RS conseq2) 1);
 by (rtac (hoare_derivs.Ass RS conseq1) 2);
-by        (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac 
-	          [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")] 
-		  (hoare_derivs.Local RS conseq1), etac conseq12] 3);
+by        (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
+                  [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")]
+                  (hoare_derivs.Local RS conseq1), etac conseq12] 3);
 by         (EVERY'[etac hoare_derivs.Comp, etac conseq12] 5);
 by         ((rtac hoare_derivs.If THEN_ALL_NEW etac conseq12) 6);
 by          (EVERY'[rtac (hoare_derivs.Loop RS conseq2), etac conseq12] 8);
@@ -278,7 +273,7 @@
 by   (Fast_tac 1);
 by (dtac finite_subset 1);
 by (etac finite_imageI 1);
-by (Asm_simp_tac 1); 
+by (Asm_simp_tac 1);
 by (arith_tac 1);
 qed_spec_mp "nesting_lemma";
 
@@ -329,8 +324,8 @@
 by (make_imp_tac 1);
 by (etac finite_induct 1);
 by  (ALLGOALS (clarsimp_tac (
-	claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
-	simpset() delsimps [range_composition])));
+        claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
+        simpset() delsimps [range_composition])));
 by (etac MGF_lemma1 1);
 by  (fast_tac (claset() addDs [WT_bodiesD]) 2);
 by (Clarsimp_tac 1);
@@ -354,7 +349,7 @@
 qed "MGF'";
 
 (* requires Body+empty+insert / BodyN, com_det *)
-bind_thm ("hoare_complete", MGF' RS MGF_complete); 
+bind_thm ("hoare_complete", MGF' RS MGF_complete);
 
 section "unused derived rules";
 
diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Hoare.thy	Sat Sep 17 20:14:30 2005 +0200
@@ -2,98 +2,106 @@
     ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 TUM
-
-Inductive definition of Hoare logic for partial correctness
-Completeness is taken relative to completeness of the underlying logic
-Two versions of completeness proof:
-  nested single recursion vs. simultaneous recursion in call rule
 *)
 
-Hoare = Natural + 
+header {* Inductive definition of Hoare logic for partial correctness *}
+
+theory Hoare
+imports Natural
+begin
+
+text {*
+  Completeness is taken relative to completeness of the underlying logic.
+
+  Two versions of completeness proof: nested single recursion
+  vs. simultaneous recursion in call rule
+*}
 
 types 'a assn = "'a => state => bool"
 translations
-      "a assn"   <= (type)"a => state => bool"
+  "a assn"   <= (type)"a => state => bool"
 
 constdefs
   state_not_singleton :: bool
- "state_not_singleton == ? s t::state. s ~= t" (* at least two elements *)
+  "state_not_singleton == \<exists>s t::state. s ~= t" (* at least two elements *)
 
   peek_and    :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35)
- "peek_and P p == %Z s. P Z s & p s"
+  "peek_and P p == %Z s. P Z s & p s"
 
 datatype 'a triple =
-    triple ('a assn) com ('a assn)         ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
-  
+  triple "'a assn"  com  "'a assn"       ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
+
 consts
-  triple_valid ::            nat => 'a triple     => bool ( "|=_:_" [0 , 58] 57)
-  hoare_valids ::  'a triple set => 'a triple set => bool ("_||=_"  [58, 58] 57)
-  hoare_derivs ::"('a triple set *  'a triple set)   set"
+  triple_valid ::            "nat => 'a triple     => bool" ( "|=_:_" [0 , 58] 57)
+  hoare_valids ::  "'a triple set => 'a triple set => bool" ("_||=_"  [58, 58] 57)
+  hoare_derivs :: "('a triple set *  'a triple set)   set"
 syntax
-  triples_valid::            nat => 'a triple set => bool ("||=_:_" [0 , 58] 57)
-  hoare_valid  ::  'a triple set => 'a triple     => bool ("_|=_"   [58, 58] 57)
-"@hoare_derivs"::  'a triple set => 'a triple set => bool ("_||-_"  [58, 58] 57)
-"@hoare_deriv" ::  'a triple set => 'a triple     => bool ("_|-_"   [58, 58] 57)
+  triples_valid::            "nat => 'a triple set => bool" ("||=_:_" [0 , 58] 57)
+  hoare_valid  ::  "'a triple set => 'a triple     => bool" ("_|=_"   [58, 58] 57)
+"@hoare_derivs"::  "'a triple set => 'a triple set => bool" ("_||-_"  [58, 58] 57)
+"@hoare_deriv" ::  "'a triple set => 'a triple     => bool" ("_|-_"   [58, 58] 57)
 
-defs triple_valid_def  "|=n:t  ==  case t of {P}.c.{Q} =>
-		                !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')"
+defs triple_valid_def: "|=n:t  ==  case t of {P}.c.{Q} =>
+                                !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')"
 translations          "||=n:G" == "Ball G (triple_valid n)"
-defs hoare_valids_def"G||=ts   ==  !n. ||=n:G --> ||=n:ts"
+defs hoare_valids_def: "G||=ts   ==  !n. ||=n:G --> ||=n:ts"
 translations         "G |=t  " == " G||={t}"
                      "G||-ts"  == "(G,ts) : hoare_derivs"
                      "G |-t"   == " G||-{t}"
 
 (* Most General Triples *)
-constdefs MGT    :: com => state triple              ("{=}._.{->}" [60] 58)
+constdefs MGT    :: "com => state triple"            ("{=}._.{->}" [60] 58)
          "{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}"
 
-inductive hoare_derivs intrs
-  
-  empty    "G||-{}"
-  insert"[| G |-t;  G||-ts |]
-	==> G||-insert t ts"
+inductive hoare_derivs intros
+
+  empty:    "G||-{}"
+  insert: "[| G |-t;  G||-ts |]
+        ==> G||-insert t ts"
 
-  asm	   "ts <= G ==>
-	    G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *)
+  asm:      "ts <= G ==>
+             G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *)
 
-  cut   "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *)
+  cut:   "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *)
 
-  weaken"[| G||-ts' ; ts <= ts' |] ==> G||-ts"
+  weaken: "[| G||-ts' ; ts <= ts' |] ==> G||-ts"
 
-  conseq"!Z s. P  Z  s --> (? P' Q'. G|-{P'}.c.{Q'} &
-                                  (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s'))
-         ==> G|-{P}.c.{Q}"
+  conseq: "!Z s. P  Z  s --> (? P' Q'. G|-{P'}.c.{Q'} &
+                                   (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s'))
+          ==> G|-{P}.c.{Q}"
 
 
-  Skip	"G|-{P}. SKIP .{P}"
+  Skip:  "G|-{P}. SKIP .{P}"
 
-  Ass	"G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}"
+  Ass:   "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}"
 
-  Local	"G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])}
-     ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}"
+  Local: "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])}
+      ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}"
 
-  Comp	"[| G|-{P}.c.{Q};
-	    G|-{Q}.d.{R} |]
-	==> G|-{P}. (c;;d) .{R}"
+  Comp:  "[| G|-{P}.c.{Q};
+             G|-{Q}.d.{R} |]
+         ==> G|-{P}. (c;;d) .{R}"
 
-  If	"[| G|-{P &>        b }.c.{Q};
-	    G|-{P &> (Not o b)}.d.{Q} |]
-	==> G|-{P}. IF b THEN c ELSE d .{Q}"
+  If:    "[| G|-{P &>        b }.c.{Q};
+             G|-{P &> (Not o b)}.d.{Q} |]
+         ==> G|-{P}. IF b THEN c ELSE d .{Q}"
 
-  Loop  "G|-{P &> b}.c.{P} ==>
-	 G|-{P}. WHILE b DO c .{P &> (Not o b)}"
+  Loop:  "G|-{P &> b}.c.{P} ==>
+          G|-{P}. WHILE b DO c .{P &> (Not o b)}"
 
 (*
-  BodyN	"(insert ({P}. BODY pn  .{Q}) G)
-	  |-{P}.  the (body pn) .{Q} ==>
-	 G|-{P}.       BODY pn  .{Q}"
+  BodyN: "(insert ({P}. BODY pn  .{Q}) G)
+           |-{P}.  the (body pn) .{Q} ==>
+          G|-{P}.       BODY pn  .{Q}"
 *)
-  Body	"[| G Un (%p. {P p}.      BODY p  .{Q p})`Procs
-	      ||-(%p. {P p}. the (body p) .{Q p})`Procs |]
-	==>  G||-(%p. {P p}.      BODY p  .{Q p})`Procs"
+  Body:  "[| G Un (%p. {P p}.      BODY p  .{Q p})`Procs
+               ||-(%p. {P p}. the (body p) .{Q p})`Procs |]
+         ==>  G||-(%p. {P p}.      BODY p  .{Q p})`Procs"
 
-  Call	   "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
-	==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
-	    X:=CALL pn(a) .{Q}"
+  Call:     "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
+         ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
+             X:=CALL pn(a) .{Q}"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Misc.thy
--- a/src/HOL/IMPP/Misc.thy	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Misc.thy	Sat Sep 17 20:14:30 2005 +0200
@@ -2,18 +2,22 @@
     ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 TUM
+*)
 
-Several examples for Hoare logic
-*)
-Misc = Hoare +
+header {* Several examples for Hoare logic *}
+
+theory Misc
+imports Hoare
+begin
 
 defs
-  newlocs_def "newlocs       == %x. arbitrary"
-  setlocs_def "setlocs s l'  == case s of st g l => st g l'"
-  getlocs_def "getlocs s     == case s of st g l => l"
-   update_def "update s vn v == case vn of
-                              Glb gn => (case s of st g l => st (g(gn:=v)) l)
-                            | Loc ln => (case s of st g l => st g (l(ln:=v)))"
+  newlocs_def: "newlocs       == %x. arbitrary"
+  setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
+  getlocs_def: "getlocs s     == case s of st g l => l"
+   update_def: "update s vn v == case vn of
+                               Glb gn => (case s of st g l => st (g(gn:=v)) l)
+                             | Loc ln => (case s of st g l => st g (l(ln:=v)))"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
-  
\ No newline at end of file
diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Natural.ML
--- a/src/HOL/IMPP/Natural.ML	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Natural.ML	Sat Sep 17 20:14:30 2005 +0200
@@ -4,21 +4,8 @@
     Copyright   1999 TUM
 *)
 
-open Natural;
-
-AddIs evalc.intrs;
-AddIs evaln.intrs;
-
-val evalc_elim_cases = map evalc.mk_cases
-   ["<SKIP,s> -c-> t", "<X:==a,s> -c-> t", "<LOCAL Y:=a IN c,s> -c-> t", 
-    "<c1;;c2,s> -c-> t","<IF b THEN c1 ELSE c2,s> -c-> t",
-    "<BODY P,s> -c-> s1", "<X:=CALL P(a),s> -c-> s1"];
-val evaln_elim_cases = map evaln.mk_cases
-   ["<SKIP,s> -n-> t", "<X:==a,s> -n-> t", "<LOCAL Y:=a IN c,s> -n-> t",
-    "<c1;;c2,s> -n-> t","<IF b THEN c1 ELSE c2,s> -n-> t",
-    "<BODY P,s> -n-> s1", "<X:=CALL P(a),s> -n-> s1"];
-val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
-val evaln_WHILE_case = evaln.mk_cases "<WHILE b DO c,s> -n-> t";
+AddIs evalc.intros;
+AddIs evaln.intros;
 
 AddSEs evalc_elim_cases;
 AddSEs evaln_elim_cases;
@@ -33,7 +20,7 @@
 
 Goal "<c,s> -n-> t ==> <c,s> -c-> t";
 by (etac evaln.induct 1);
-by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac));
+by (ALLGOALS (resolve_tac evalc.intros THEN_ALL_NEW atac));
 qed "evaln_evalc";
 
 Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";
@@ -46,7 +33,7 @@
 Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t";
 by (etac evaln.induct 1);
 by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1]));
-by (ALLGOALS (resolve_tac evaln.intrs THEN_ALL_NEW atac));
+by (ALLGOALS (resolve_tac evaln.intros THEN_ALL_NEW atac));
 qed_spec_mp "evaln_nonstrict";
 
 Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'";
@@ -64,7 +51,7 @@
 by (etac evalc.induct 1);
 by (ALLGOALS (REPEAT o etac exE));
 by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]]));
-by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intrs THEN_ALL_NEW atac));
+by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intros THEN_ALL_NEW atac));
 qed "evalc_evaln";
 
 Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)";
diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Natural.thy
--- a/src/HOL/IMPP/Natural.thy	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Natural.thy	Sat Sep 17 20:14:30 2005 +0200
@@ -2,88 +2,111 @@
     ID:         $Id$
     Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     Copyright   1999 TUM
-
-Natural semantics of commands
 *)
 
-Natural = Com + 
+header {* Natural semantics of commands *}
+
+theory Natural
+imports Com
+begin
 
 (** Execution of commands **)
-consts	 evalc :: "(com * state *       state) set"
-       "@evalc":: [com,state,    state] => bool	("<_,_>/ -c-> _" [0,0,  51] 51)
-	 evaln :: "(com * state * nat * state) set"
-       "@evaln":: [com,state,nat,state] => bool	("<_,_>/ -_-> _" [0,0,0,51] 51)
+consts
+  evalc :: "(com * state *       state) set"
+  evaln :: "(com * state * nat * state) set"
 
-translations  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
-              "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
+syntax
+  "@evalc":: "[com,state,    state] => bool"  ("<_,_>/ -c-> _" [0,0,  51] 51)
+  "@evaln":: "[com,state,nat,state] => bool"  ("<_,_>/ -_-> _" [0,0,0,51] 51)
+
+translations
+  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
+  "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
 
 consts
   newlocs :: locals
-  setlocs :: state => locals => state
-  getlocs :: state => locals
-  update  :: state => vname => val => state	("_/[_/::=/_]" [900,0,0] 900)
+  setlocs :: "state => locals => state"
+  getlocs :: "state => locals"
+  update  :: "state => vname => val => state"     ("_/[_/::=/_]" [900,0,0] 900)
 syntax (* IN Natural.thy *)
-  loc :: state => locals    ("_<_>" [75,0] 75)
+  loc :: "state => locals"    ("_<_>" [75,0] 75)
 translations
   "s<X>" == "getlocs s X"
 
 inductive evalc
-  intrs
-    Skip    "<SKIP,s> -c-> s"
+  intros
+    Skip:    "<SKIP,s> -c-> s"
 
-    Assign  "<X :== a,s> -c-> s[X::=a s]"
+    Assign:  "<X :== a,s> -c-> s[X::=a s]"
 
-    Local   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
-             <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
+    Local:   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
+              <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
 
-    Semi    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
-             <c0;; c1, s0> -c-> s2"
+    Semi:    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
+              <c0;; c1, s0> -c-> s2"
 
-    IfTrue  "[| b s; <c0,s> -c-> s1 |] ==>
-             <IF b THEN c0 ELSE c1, s> -c-> s1"
+    IfTrue:  "[| b s; <c0,s> -c-> s1 |] ==>
+              <IF b THEN c0 ELSE c1, s> -c-> s1"
 
-    IfFalse "[| ~b s; <c1,s> -c-> s1 |] ==>
-             <IF b THEN c0 ELSE c1, s> -c-> s1"
+    IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==>
+              <IF b THEN c0 ELSE c1, s> -c-> s1"
 
-    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
+    WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
 
-    WhileTrue  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
-                <WHILE b DO c, s0> -c-> s2"
+    WhileTrue:  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
+                 <WHILE b DO c, s0> -c-> s2"
 
-    Body       "<the (body pn), s0> -c-> s1 ==>
-                <BODY pn, s0> -c-> s1"
+    Body:       "<the (body pn), s0> -c-> s1 ==>
+                 <BODY pn, s0> -c-> s1"
 
-    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
-                <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
-                                         [X::=s1<Res>]"
+    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
+                 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
+                                          [X::=s1<Res>]"
 
 inductive evaln
-  intrs
-    Skip    "<SKIP,s> -n-> s"
+  intros
+    Skip:    "<SKIP,s> -n-> s"
+
+    Assign:  "<X :== a,s> -n-> s[X::=a s]"
 
-    Assign  "<X :== a,s> -n-> s[X::=a s]"
+    Local:   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
+              <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
+
+    Semi:    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
+              <c0;; c1, s0> -n-> s2"
 
-    Local   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
-             <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
+    IfTrue:  "[| b s; <c0,s> -n-> s1 |] ==>
+              <IF b THEN c0 ELSE c1, s> -n-> s1"
 
-    Semi    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
-             <c0;; c1, s0> -n-> s2"
+    IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
+              <IF b THEN c0 ELSE c1, s> -n-> s1"
 
-    IfTrue  "[| b s; <c0,s> -n-> s1 |] ==>
-             <IF b THEN c0 ELSE c1, s> -n-> s1"
+    WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
+
+    WhileTrue:  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
+                 <WHILE b DO c, s0> -n-> s2"
 
-    IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
-             <IF b THEN c0 ELSE c1, s> -n-> s1"
+    Body:       "<the (body pn), s0> -    n-> s1 ==>
+                 <BODY pn, s0> -Suc n-> s1"
 
-    WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"
+    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
+                 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
+                                          [X::=s1<Res>]"
 
-    WhileTrue  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
-                <WHILE b DO c, s0> -n-> s2"
 
-    Body       "<the (body pn), s0> -    n-> s1 ==>
-                <BODY pn, s0> -Suc n-> s1"
+inductive_cases evalc_elim_cases:
+  "<SKIP,s> -c-> t"  "<X:==a,s> -c-> t"  "<LOCAL Y:=a IN c,s> -c-> t"
+  "<c1;;c2,s> -c-> t"  "<IF b THEN c1 ELSE c2,s> -c-> t"
+  "<BODY P,s> -c-> s1"  "<X:=CALL P(a),s> -c-> s1"
 
-    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
-                <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
-                                         [X::=s1<Res>]"
+inductive_cases evaln_elim_cases:
+  "<SKIP,s> -n-> t"  "<X:==a,s> -n-> t"  "<LOCAL Y:=a IN c,s> -n-> t"
+  "<c1;;c2,s> -n-> t"  "<IF b THEN c1 ELSE c2,s> -n-> t"
+  "<BODY P,s> -n-> s1"  "<X:=CALL P(a),s> -n-> s1"
+
+inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
+inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end