Inl and Inr now with authentic syntax
authorhaftmann
Fri Nov 27 08:42:50 2009 +0100 (2009-11-27)
changeset 33965f57c11db4ad4
parent 33964 26acbc11e8be
child 33966 b863967f23ea
Inl and Inr now with authentic syntax
src/HOL/Bali/AxExample.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/State.thy
src/HOL/Bali/WellType.thy
src/HOL/Tools/Datatype/datatype_data.ML
     1.1 --- a/src/HOL/Bali/AxExample.thy	Fri Nov 27 08:42:34 2009 +0100
     1.2 +++ b/src/HOL/Bali/AxExample.thy	Fri Nov 27 08:42:50 2009 +0100
     1.3 @@ -1,11 +1,12 @@
     1.4  (*  Title:      HOL/Bali/AxExample.thy
     1.5 -    ID:         $Id$
     1.6      Author:     David von Oheimb
     1.7  *)
     1.8  
     1.9  header {* Example of a proof based on the Bali axiomatic semantics *}
    1.10  
    1.11 -theory AxExample imports AxSem Example begin
    1.12 +theory AxExample
    1.13 +imports AxSem Example
    1.14 +begin
    1.15  
    1.16  constdefs
    1.17    arr_inv :: "st \<Rightarrow> bool"
     2.1 --- a/src/HOL/Bali/Basis.thy	Fri Nov 27 08:42:34 2009 +0100
     2.2 +++ b/src/HOL/Bali/Basis.thy	Fri Nov 27 08:42:50 2009 +0100
     2.3 @@ -216,8 +216,8 @@
     2.4           In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
     2.5           In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
     2.6  translations
     2.7 -        "In1l e" == "In1 (Inl e)"
     2.8 -        "In1r c" == "In1 (Inr c)"
     2.9 +        "In1l e" == "In1 (CONST Inl e)"
    2.10 +        "In1r c" == "In1 (CONST Inr c)"
    2.11  
    2.12  syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
    2.13         the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
    2.14 @@ -233,7 +233,7 @@
    2.15  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
    2.16  
    2.17  translations
    2.18 -  "option"<= (type) "Datatype.option"
    2.19 +  "option"<= (type) "Option.option"
    2.20    "list"  <= (type) "List.list"
    2.21    "sum3"  <= (type) "Basis.sum3"
    2.22  
     3.1 --- a/src/HOL/Bali/Example.thy	Fri Nov 27 08:42:34 2009 +0100
     3.2 +++ b/src/HOL/Bali/Example.thy	Fri Nov 27 08:42:50 2009 +0100
     3.3 @@ -1,10 +1,11 @@
     3.4  (*  Title:      HOL/Bali/Example.thy
     3.5 -    ID:         $Id$
     3.6      Author:     David von Oheimb
     3.7  *)
     3.8  header {* Example Bali program *}
     3.9  
    3.10 -theory Example imports Eval WellForm begin
    3.11 +theory Example
    3.12 +imports Eval WellForm
    3.13 +begin
    3.14  
    3.15  text {*
    3.16  The following example Bali program includes:
    3.17 @@ -1235,24 +1236,24 @@
    3.18  
    3.19  translations
    3.20    "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) (CONST two)
    3.21 -                ,values=CONST empty(Inr 0\<mapsto>Bool False)(Inr (CONST one)\<mapsto>Bool False)\<rparr>"
    3.22 +                ,values=CONST empty(CONST Inr 0\<mapsto>Bool False)(CONST Inr (CONST one)\<mapsto>Bool False)\<rparr>"
    3.23    "obj_b"   <= "\<lparr>tag=CInst (CONST Ext)
    3.24 -                ,values=(CONST empty(Inl (CONST vee, CONST Base)\<mapsto>Null   ) 
    3.25 -                              (Inl (CONST vee, CONST Ext )\<mapsto>Intg 0))\<rparr>"
    3.26 +                ,values=(CONST empty(CONST Inl (CONST vee, CONST Base)\<mapsto>Null   ) 
    3.27 +                              (CONST Inl (CONST vee, CONST Ext )\<mapsto>Intg 0))\<rparr>"
    3.28    "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
    3.29 -  "arr_N"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Null)"
    3.30 -  "arr_a"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
    3.31 -  "globs1"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    3.32 -                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
    3.33 -                     (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
    3.34 -  "globs2"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    3.35 -                     (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    3.36 -                     (Inl a\<mapsto>obj_a)
    3.37 -                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
    3.38 -  "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
    3.39 -  "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
    3.40 +  "arr_N"   == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Null)"
    3.41 +  "arr_a"   == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
    3.42 +  "globs1"  == "CONST empty(CONST Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    3.43 +                     (CONST Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
    3.44 +                     (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
    3.45 +  "globs2"  == "CONST empty(CONST Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    3.46 +                     (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    3.47 +                     (CONST Inl a\<mapsto>obj_a)
    3.48 +                     (CONST Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
    3.49 +  "globs3"  == "globs2(CONST Inl b\<mapsto>obj_b)"
    3.50 +  "globs8"  == "globs3(CONST Inl c\<mapsto>obj_c)"
    3.51    "locs3"   == "CONST empty(VName (CONST e)\<mapsto>Addr b)"
    3.52 -  "locs4"   == "CONST empty(VName (CONST z)\<mapsto>Null)(Inr()\<mapsto>Addr b)"
    3.53 +  "locs4"   == "CONST empty(VName (CONST z)\<mapsto>Null)(CONST Inr()\<mapsto>Addr b)"
    3.54    "locs8"   == "locs3(VName (CONST z)\<mapsto>Addr c)"
    3.55    "s0"  == "       st (CONST empty) (CONST empty)"
    3.56    "s0'" == " Norm  s0"
     4.1 --- a/src/HOL/Bali/State.thy	Fri Nov 27 08:42:34 2009 +0100
     4.2 +++ b/src/HOL/Bali/State.thy	Fri Nov 27 08:42:50 2009 +0100
     4.3 @@ -1,10 +1,11 @@
     4.4  (*  Title:      HOL/Bali/State.thy
     4.5 -    ID:         $Id$
     4.6      Author:     David von Oheimb
     4.7  *)
     4.8  header {* State for evaluation of Java expressions and statements *}
     4.9  
    4.10 -theory State imports DeclConcepts begin
    4.11 +theory State
    4.12 +imports DeclConcepts
    4.13 +begin
    4.14  
    4.15  text {*
    4.16  design issues:
    4.17 @@ -138,8 +139,8 @@
    4.18    Stat  :: "qtname \<Rightarrow> oref"
    4.19  
    4.20  translations
    4.21 -  "Heap" => "Inl"
    4.22 -  "Stat" => "Inr"
    4.23 +  "Heap" => "CONST Inl"
    4.24 +  "Stat" => "CONST Inr"
    4.25    "oref" <= (type) "loc + qtname"
    4.26  
    4.27  constdefs
    4.28 @@ -328,7 +329,7 @@
    4.29    init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
    4.30  
    4.31  translations
    4.32 - "init_class_obj G C" == "init_obj G CONST undefined (Inr C)"
    4.33 + "init_class_obj G C" == "init_obj G CONST undefined (CONST Inr C)"
    4.34  
    4.35  lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
    4.36  apply (unfold gupd_def)
     5.1 --- a/src/HOL/Bali/WellType.thy	Fri Nov 27 08:42:34 2009 +0100
     5.2 +++ b/src/HOL/Bali/WellType.thy	Fri Nov 27 08:42:50 2009 +0100
     5.3 @@ -1,10 +1,11 @@
     5.4  (*  Title:      HOL/Bali/WellType.thy
     5.5 -    ID:         $Id$
     5.6      Author:     David von Oheimb
     5.7  *)
     5.8  header {* Well-typedness of Java programs *}
     5.9  
    5.10 -theory WellType imports DeclConcepts begin
    5.11 +theory WellType
    5.12 +imports DeclConcepts
    5.13 +begin
    5.14  
    5.15  text {*
    5.16  improvements over Java Specification 1.0:
    5.17 @@ -443,10 +444,10 @@
    5.18  
    5.19  translations
    5.20          "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
    5.21 -        "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>Inl (PrimT Void)"
    5.22 -        "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>Inl T"
    5.23 -        "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>Inl T"
    5.24 -        "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>Inr T"
    5.25 +        "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>CONST Inl (PrimT Void)"
    5.26 +        "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>CONST Inl T"
    5.27 +        "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>CONST Inl T"
    5.28 +        "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>CONST Inr T"
    5.29  
    5.30  
    5.31  declare not_None_eq [simp del]