# HG changeset patch # User haftmann # Date 1259307770 -3600 # Node ID f57c11db4ad4efdb27b30ee91e3fc375fa2236a5 # Parent 26acbc11e8be56383314c8372287dd70aca3bb3a Inl and Inr now with authentic syntax diff -r 26acbc11e8be -r f57c11db4ad4 src/HOL/Bali/AxExample.thy --- 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 \ bool" diff -r 26acbc11e8be -r f57c11db4ad4 src/HOL/Bali/Basis.thy --- 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 \ ('al + 'ar, 'b, 'c) sum3" In1r :: "'ar \ ('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 \ 'al" the_In1r :: "('al + 'ar, 'b, 'c) sum3 \ '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" diff -r 26acbc11e8be -r f57c11db4ad4 src/HOL/Bali/Example.thy --- 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" <= "\tag=Arr (PrimT Boolean) (CONST two) - ,values=CONST empty(Inr 0\Bool False)(Inr (CONST one)\Bool False)\" + ,values=CONST empty(CONST Inr 0\Bool False)(CONST Inr (CONST one)\Bool False)\" "obj_b" <= "\tag=CInst (CONST Ext) - ,values=(CONST empty(Inl (CONST vee, CONST Base)\Null ) - (Inl (CONST vee, CONST Ext )\Intg 0))\" + ,values=(CONST empty(CONST Inl (CONST vee, CONST Base)\Null ) + (CONST Inl (CONST vee, CONST Ext )\Intg 0))\" "obj_c" == "\tag=CInst (SXcpt NullPointer),values=CONST empty\" - "arr_N" == "CONST empty(Inl (CONST arr, CONST Base)\Null)" - "arr_a" == "CONST empty(Inl (CONST arr, CONST Base)\Addr a)" - "globs1" == "CONST empty(Inr (CONST Ext) \\tag=CONST undefined, values=CONST empty\) - (Inr (CONST Base) \\tag=CONST undefined, values=arr_N\) - (Inr Object\\tag=CONST undefined, values=CONST empty\)" - "globs2" == "CONST empty(Inr (CONST Ext) \\tag=CONST undefined, values=CONST empty\) - (Inr Object\\tag=CONST undefined, values=CONST empty\) - (Inl a\obj_a) - (Inr (CONST Base) \\tag=CONST undefined, values=arr_a\)" - "globs3" == "globs2(Inl b\obj_b)" - "globs8" == "globs3(Inl c\obj_c)" + "arr_N" == "CONST empty(CONST Inl (CONST arr, CONST Base)\Null)" + "arr_a" == "CONST empty(CONST Inl (CONST arr, CONST Base)\Addr a)" + "globs1" == "CONST empty(CONST Inr (CONST Ext) \\tag=CONST undefined, values=CONST empty\) + (CONST Inr (CONST Base) \\tag=CONST undefined, values=arr_N\) + (CONST Inr Object\\tag=CONST undefined, values=CONST empty\)" + "globs2" == "CONST empty(CONST Inr (CONST Ext) \\tag=CONST undefined, values=CONST empty\) + (CONST Inr Object\\tag=CONST undefined, values=CONST empty\) + (CONST Inl a\obj_a) + (CONST Inr (CONST Base) \\tag=CONST undefined, values=arr_a\)" + "globs3" == "globs2(CONST Inl b\obj_b)" + "globs8" == "globs3(CONST Inl c\obj_c)" "locs3" == "CONST empty(VName (CONST e)\Addr b)" - "locs4" == "CONST empty(VName (CONST z)\Null)(Inr()\Addr b)" + "locs4" == "CONST empty(VName (CONST z)\Null)(CONST Inr()\Addr b)" "locs8" == "locs3(VName (CONST z)\Addr c)" "s0" == " st (CONST empty) (CONST empty)" "s0'" == " Norm s0" diff -r 26acbc11e8be -r f57c11db4ad4 src/HOL/Bali/State.thy --- 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 \ 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 \ qtname \ st \ 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\obj) (st g l) = st (g(r\obj)) l" apply (unfold gupd_def) diff -r 26acbc11e8be -r f57c11db4ad4 src/HOL/Bali/WellType.thy --- 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\t\ T" == "E,empty_dt\t\ T" - "E\s\\" == "E\In1r s\Inl (PrimT Void)" - "E\e\-T" == "E\In1l e\Inl T" - "E\e\=T" == "E\In2 e\Inl T" - "E\e\\T" == "E\In3 e\Inr T" + "E\s\\" == "E\In1r s\CONST Inl (PrimT Void)" + "E\e\-T" == "E\In1l e\CONST Inl T" + "E\e\=T" == "E\In2 e\CONST Inl T" + "E\e\\T" == "E\In3 e\CONST Inr T" declare not_None_eq [simp del]