# HG changeset patch
# User kleing
# Date 969621139 -7200
# Node ID 8c8d2d0d3ef8a87451f4b99bf5ab10079a2d1ae0
# Parent  9f84ffa4a8d07129bd52186281c0551a6151e9b1
converted to Isar, tuned

diff -r 9f84ffa4a8d0 -r 8c8d2d0d3ef8 src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Fri Sep 22 13:12:19 2000 +0200
@@ -2,30 +2,38 @@
     ID:         $Id$
     Author:     Cornelia Pusch
     Copyright   1999 Technische Universitaet Muenchen
-
-Execution of the JVM
 *)
 
-JVMExec = JVMExecInstr + 
+header {* Program Execution in the JVM *}
+
+theory JVMExec = JVMExecInstr :
+
 
 consts
- exec :: "jvm_prog \\<times> jvm_state => jvm_state option"
+  exec :: "jvm_prog \<times> jvm_state => jvm_state option"
+
 
 (** exec is not recursive. recdef is just used for pattern matching **)
 recdef exec "{}"
- "exec (G, xp, hp, []) = None"
+  "exec (G, xp, hp, []) = None"
 
- "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
+  "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
   (let 
      i = snd(snd(snd(the(method (G,C) sig)))) ! pc
    in
      Some (exec_instr i G hp stk loc C sig pc frs))"
 
- "exec (G, Some xp, hp, frs) = None" 
+  "exec (G, Some xp, hp, frs) = None" 
 
 
 constdefs
- exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  ("_ \\<turnstile> _ -jvm-> _" [61,61,61]60)
- "G \\<turnstile> s -jvm-> t == (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
+  exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
+              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
+  "G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
+
+
+syntax (HTML output)
+  exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
+              ("_ |- _ -jvm-> _" [61,61,61]60)
 
 end
diff -r 9f84ffa4a8d0 -r 8c8d2d0d3ef8 src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Fri Sep 22 13:12:19 2000 +0200
@@ -2,11 +2,14 @@
     ID:         $Id$
     Author:     Cornelia Pusch, Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
-
-Semantics of JVM instructions
 *)
 
-JVMExecInstr = JVMInstructions + JVMState +
+
+header {* JVM Instruction Semantics *}
+
+
+theory JVMExecInstr = JVMInstructions + JVMState:
+
 
 consts
   exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
@@ -25,10 +28,10 @@
       (None, hp, (Null # stk, vars, Cl, sig, pc+1)#frs)"
 
  "exec_instr (New C) G hp stk vars Cl sig pc frs = 
-	(let xp'	= raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory;
+	(let xp'	= raise_xcpt (\<forall>x. hp x \<noteq> None) OutOfMemory;
 	     oref	= newref hp;
              fs		= init_vars (fields(G,C));
-	     hp'	= if xp'=None then hp(oref \\<mapsto> (C,fs)) else hp;
+	     hp'	= if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
 	     stk'	= if xp'=None then (Addr oref)#stk else stk
 	 in 
       (xp', hp', (stk', vars, Cl, sig, pc+1)#frs))"	
@@ -46,13 +49,13 @@
 	     xp'	= raise_xcpt (oref=Null) NullPointer;
 	     a		= the_Addr oref;
 	     (oc,fs)	= the(hp a);
-	     hp'	= if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp
+	     hp'	= if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp
 	 in
       (xp', hp', (tl (tl stk), vars, Cl, sig, pc+1)#frs))"
 
  "exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
 	(let oref	= hd stk;
-	     xp'	= raise_xcpt (\\<not> cast_ok G C hp oref) ClassCast; 
+	     xp'	= raise_xcpt (\<not> cast_ok G C hp oref) ClassCast; 
 	     stk'	= if xp'=None then stk else tl stk
 	 in
       (xp', hp, (stk', vars, Cl, sig, pc+1)#frs))"
diff -r 9f84ffa4a8d0 -r 8c8d2d0d3ef8 src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Fri Sep 22 13:12:19 2000 +0200
@@ -2,11 +2,12 @@
     ID:         $Id$
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
-
-Instructions of the JVM
 *)
 
-JVMInstructions = JVMState +
+header {* Instructions of the JVM *}
+
+
+theory JVMInstructions = JVMState:
 
 
 datatype 
@@ -19,19 +20,19 @@
         | Putfield vname cname		  (* Set field in object     *)
         | Checkcast cname	          (* Check whether object is of given type *)
         | Invoke cname mname "(ty list)"  (* inv. instance meth of an object *)
-        | Return
-        | Pop
-        | Dup
-        | Dup_x1
-        | Dup_x2
-        | Swap
-        | IAdd
-        | Goto int
+        | Return                    (* return from method *)
+        | Pop                       (* pop top element from opstack *)
+        | Dup                       (* duplicate top element of opstack *)
+        | Dup_x1                    (* duplicate next to top element *)
+        | Dup_x2                    (* duplicate 3rd element *)
+        | Swap                      (* swap top and next to top element *)
+        | IAdd                      (* integer addition *)
+        | Goto int                  (* goto relative address *)
         | Ifcmpeq int               (* Branch if int/ref comparison succeeds *)
 
 
 types
   bytecode = "instr list"
-  jvm_prog = "(nat \\<times> bytecode) prog" 
+  jvm_prog = "(nat \<times> bytecode) prog" 
 
 end
diff -r 9f84ffa4a8d0 -r 8c8d2d0d3ef8 src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Fri Sep 22 13:12:19 2000 +0200
@@ -2,25 +2,26 @@
     ID:         $Id$
     Author:     Cornelia Pusch
     Copyright   1999 Technische Universitaet Muenchen
-
-State of the JVM
 *)
 
-JVMState = Store +
+
+header {* State of the JVM *}
 
 
-(** frame stack **)
+theory JVMState = Store:
 
+
+text {* frame stack :*}
 types
  opstack 	 = "val list"
  locvars 	 = "val list" 
  p_count 	 = nat
 
- frame = "opstack \\<times>			
-	  locvars \\<times>		
-	  cname \\<times>			
-	  sig \\<times>			
-	  p_count"
+ frame = "opstack \<times>			
+          locvars \<times>		
+          cname \<times>			
+          sig \<times>			
+          p_count"
 
 	(* operand stack *)
 	(* local variables *)
@@ -29,22 +30,20 @@
 	(* program counter within frame *)
 
 
-(** exceptions **)
-
+text {* exceptions: *}
 constdefs
- raise_xcpt :: "bool => xcpt => xcpt option"
-"raise_xcpt c x == (if c then Some x else None)"
-
-(** runtime state **)
-
-types
- jvm_state = "xcpt option \\<times> aheap \\<times> frame list"	
+  raise_xcpt :: "bool => xcpt => xcpt option"
+  "raise_xcpt c x == (if c then Some x else None)"
 
 
+text {* runtime state: *}
+types
+  jvm_state = "xcpt option \<times> aheap \<times> frame list"	
 
-(** dynamic method lookup **)
 
+text {* dynamic method lookup: *}
 constdefs
- dyn_class	:: "'code prog \\<times> sig \\<times> cname => cname"
-"dyn_class == \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
+  dyn_class	:: "'code prog \<times> sig \<times> cname => cname"
+  "dyn_class == \<lambda>(G,sig,C). fst(the(method(G,C) sig))"
+
 end
diff -r 9f84ffa4a8d0 -r 8c8d2d0d3ef8 src/HOL/MicroJava/JVM/Store.thy
--- a/src/HOL/MicroJava/JVM/Store.thy	Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.thy	Fri Sep 22 13:12:19 2000 +0200
@@ -2,17 +2,25 @@
     ID:         $Id$
     Author:     Cornelia Pusch
     Copyright   1999 Technische Universitaet Muenchen
-
-The store.
-
-The JVM builds on many notions already defined in Java.
-Conform provides notions for the type safety proof of the Bytecode Verifier.
 *)
 
-Store = Conform +  
+header {* Store of the JVM *}
+
+theory Store = Conform:
+
+text {*
+The JVM builds on many notions already defined in Java.
+Conform provides notions for the type safety proof of the Bytecode Verifier.
+*}
+
 
 constdefs
- newref :: "('a \\<leadsto> 'b) => 'a"
+ newref :: "('a \<leadsto> 'b) => 'a"
  "newref s == SOME v. s v = None"
 
+
+lemma newref_None:
+  "hp x = None ==> hp (newref hp) = None"
+by (auto intro: someI2_ex simp add: newref_def)
+
 end