--- a/src/HOL/Bali/AxExample.thy Fri Nov 27 08:42:34 2009 +0100
+++ b/src/HOL/Bali/AxExample.thy Fri Nov 27 08:42:50 2009 +0100
@@ -1,11 +1,12 @@
(* Title: HOL/Bali/AxExample.thy
- ID: $Id$
Author: David von Oheimb
*)
header {* Example of a proof based on the Bali axiomatic semantics *}
-theory AxExample imports AxSem Example begin
+theory AxExample
+imports AxSem Example
+begin
constdefs
arr_inv :: "st \<Rightarrow> bool"
--- a/src/HOL/Bali/Basis.thy Fri Nov 27 08:42:34 2009 +0100
+++ b/src/HOL/Bali/Basis.thy Fri Nov 27 08:42:50 2009 +0100
@@ -216,8 +216,8 @@
In1l :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
translations
- "In1l e" == "In1 (Inl e)"
- "In1r c" == "In1 (Inr c)"
+ "In1l e" == "In1 (CONST Inl e)"
+ "In1r c" == "In1 (CONST Inr c)"
syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
@@ -233,7 +233,7 @@
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
translations
- "option"<= (type) "Datatype.option"
+ "option"<= (type) "Option.option"
"list" <= (type) "List.list"
"sum3" <= (type) "Basis.sum3"
--- a/src/HOL/Bali/Example.thy Fri Nov 27 08:42:34 2009 +0100
+++ b/src/HOL/Bali/Example.thy Fri Nov 27 08:42:50 2009 +0100
@@ -1,10 +1,11 @@
(* Title: HOL/Bali/Example.thy
- ID: $Id$
Author: David von Oheimb
*)
header {* Example Bali program *}
-theory Example imports Eval WellForm begin
+theory Example
+imports Eval WellForm
+begin
text {*
The following example Bali program includes:
@@ -1235,24 +1236,24 @@
translations
"obj_a" <= "\<lparr>tag=Arr (PrimT Boolean) (CONST two)
- ,values=CONST empty(Inr 0\<mapsto>Bool False)(Inr (CONST one)\<mapsto>Bool False)\<rparr>"
+ ,values=CONST empty(CONST Inr 0\<mapsto>Bool False)(CONST Inr (CONST one)\<mapsto>Bool False)\<rparr>"
"obj_b" <= "\<lparr>tag=CInst (CONST Ext)
- ,values=(CONST empty(Inl (CONST vee, CONST Base)\<mapsto>Null )
- (Inl (CONST vee, CONST Ext )\<mapsto>Intg 0))\<rparr>"
+ ,values=(CONST empty(CONST Inl (CONST vee, CONST Base)\<mapsto>Null )
+ (CONST Inl (CONST vee, CONST Ext )\<mapsto>Intg 0))\<rparr>"
"obj_c" == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
- "arr_N" == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Null)"
- "arr_a" == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
- "globs1" == "CONST empty(Inr (CONST Ext) \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
- (Inr (CONST Base) \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
- (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
- "globs2" == "CONST empty(Inr (CONST Ext) \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
- (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
- (Inl a\<mapsto>obj_a)
- (Inr (CONST Base) \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
- "globs3" == "globs2(Inl b\<mapsto>obj_b)"
- "globs8" == "globs3(Inl c\<mapsto>obj_c)"
+ "arr_N" == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Null)"
+ "arr_a" == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
+ "globs1" == "CONST empty(CONST Inr (CONST Ext) \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
+ (CONST Inr (CONST Base) \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
+ (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
+ "globs2" == "CONST empty(CONST Inr (CONST Ext) \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
+ (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
+ (CONST Inl a\<mapsto>obj_a)
+ (CONST Inr (CONST Base) \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
+ "globs3" == "globs2(CONST Inl b\<mapsto>obj_b)"
+ "globs8" == "globs3(CONST Inl c\<mapsto>obj_c)"
"locs3" == "CONST empty(VName (CONST e)\<mapsto>Addr b)"
- "locs4" == "CONST empty(VName (CONST z)\<mapsto>Null)(Inr()\<mapsto>Addr b)"
+ "locs4" == "CONST empty(VName (CONST z)\<mapsto>Null)(CONST Inr()\<mapsto>Addr b)"
"locs8" == "locs3(VName (CONST z)\<mapsto>Addr c)"
"s0" == " st (CONST empty) (CONST empty)"
"s0'" == " Norm s0"
--- a/src/HOL/Bali/State.thy Fri Nov 27 08:42:34 2009 +0100
+++ b/src/HOL/Bali/State.thy Fri Nov 27 08:42:50 2009 +0100
@@ -1,10 +1,11 @@
(* Title: HOL/Bali/State.thy
- ID: $Id$
Author: David von Oheimb
*)
header {* State for evaluation of Java expressions and statements *}
-theory State imports DeclConcepts begin
+theory State
+imports DeclConcepts
+begin
text {*
design issues:
@@ -138,8 +139,8 @@
Stat :: "qtname \<Rightarrow> oref"
translations
- "Heap" => "Inl"
- "Stat" => "Inr"
+ "Heap" => "CONST Inl"
+ "Stat" => "CONST Inr"
"oref" <= (type) "loc + qtname"
constdefs
@@ -328,7 +329,7 @@
init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
translations
- "init_class_obj G C" == "init_obj G CONST undefined (Inr C)"
+ "init_class_obj G C" == "init_obj G CONST undefined (CONST Inr C)"
lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
apply (unfold gupd_def)
--- a/src/HOL/Bali/WellType.thy Fri Nov 27 08:42:34 2009 +0100
+++ b/src/HOL/Bali/WellType.thy Fri Nov 27 08:42:50 2009 +0100
@@ -1,10 +1,11 @@
(* Title: HOL/Bali/WellType.thy
- ID: $Id$
Author: David von Oheimb
*)
header {* Well-typedness of Java programs *}
-theory WellType imports DeclConcepts begin
+theory WellType
+imports DeclConcepts
+begin
text {*
improvements over Java Specification 1.0:
@@ -443,10 +444,10 @@
translations
"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
- "E\<turnstile>s\<Colon>\<surd>" == "E\<turnstile>In1r s\<Colon>Inl (PrimT Void)"
- "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>Inl T"
- "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2 e\<Colon>Inl T"
- "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3 e\<Colon>Inr T"
+ "E\<turnstile>s\<Colon>\<surd>" == "E\<turnstile>In1r s\<Colon>CONST Inl (PrimT Void)"
+ "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>CONST Inl T"
+ "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2 e\<Colon>CONST Inl T"
+ "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3 e\<Colon>CONST Inr T"
declare not_None_eq [simp del]