--- a/src/HOL/Bali/AxSem.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/AxSem.thy Wed Feb 10 00:45:16 2010 +0100
@@ -6,7 +6,6 @@
header {* Axiomatic semantics of Java expressions and statements
(see also Eval.thy)
*}
-
theory AxSem imports Evaln TypeSafe begin
text {*
@@ -39,14 +38,15 @@
*}
types res = vals --{* result entry *}
-syntax
- Val :: "val \<Rightarrow> res"
- Var :: "var \<Rightarrow> res"
- Vals :: "val list \<Rightarrow> res"
-translations
- "Val x" => "(In1 x)"
- "Var x" => "(In2 x)"
- "Vals x" => "(In3 x)"
+
+abbreviation (input)
+ Val where "Val x == In1 x"
+
+abbreviation (input)
+ Var where "Var x == In2 x"
+
+abbreviation (input)
+ Vals where "Vals x == In3 x"
syntax
"_Val" :: "[pttrn] => pttrn" ("Val:_" [951] 950)
@@ -54,9 +54,9 @@
"_Vals" :: "[pttrn] => pttrn" ("Vals:_" [951] 950)
translations
- "\<lambda>Val:v . b" == "(\<lambda>v. b) \<circ> the_In1"
- "\<lambda>Var:v . b" == "(\<lambda>v. b) \<circ> the_In2"
- "\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> the_In3"
+ "\<lambda>Val:v . b" == "(\<lambda>v. b) \<circ> CONST the_In1"
+ "\<lambda>Var:v . b" == "(\<lambda>v. b) \<circ> CONST the_In2"
+ "\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> CONST the_In3"
--{* relation on result values, state and auxiliary variables *}
types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
@@ -105,10 +105,9 @@
apply auto
done
-syntax
- Normal :: "'a assn \<Rightarrow> 'a assn"
-translations
- "Normal P" == "P \<and>. normal"
+abbreviation
+ Normal :: "'a assn \<Rightarrow> 'a assn"
+ where "Normal P == P \<and>. normal"
lemma peek_and_Normal [simp]: "peek_and (Normal P) p = Normal (peek_and P p)"
apply (rule ext)
@@ -207,9 +206,9 @@
"peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
syntax
-"@peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_:. _" [0,3] 3)
+ "_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_:. _" [0,3] 3)
translations
- "\<lambda>w:. P" == "peek_res (\<lambda>w. P)"
+ "\<lambda>w:. P" == "CONST peek_res (\<lambda>w. P)"
lemma peek_res_def2 [simp]: "peek_res P Y = P Y Y"
apply (unfold peek_res_def)
@@ -268,9 +267,9 @@
"peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
syntax
-"@peek_st" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_.. _" [0,3] 3)
+ "_peek_st" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_.. _" [0,3] 3)
translations
- "\<lambda>s.. P" == "peek_st (\<lambda>s. P)"
+ "\<lambda>s.. P" == "CONST peek_st (\<lambda>s. P)"
lemma peek_st_def2 [simp]: "(\<lambda>s.. Pf s) Y s = Pf (store s) Y s"
apply (unfold peek_st_def)
@@ -386,33 +385,31 @@
("{(1_)}/ _>/ {(1_)}" [3,65,3]75)
types 'a triples = "'a triple set"
-syntax
-
+abbreviation
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _=>/ {(1_)}" [3,80,3] 75)
+ where "{P} e=> {Q} == {P} In2 e> {Q}"
+
+abbreviation
expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _->/ {(1_)}" [3,80,3] 75)
+ where "{P} e-> {Q} == {P} In1l e> {Q}"
+
+abbreviation
exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _#>/ {(1_)}" [3,65,3] 75)
+ where "{P} e#> {Q} == {P} In3 e> {Q}"
+
+abbreviation
stmt_triple :: "['a assn, stmt, 'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ ._./ {(1_)}" [3,65,3] 75)
-
-syntax (xsymbols)
+ where "{P} .c. {Q} == {P} In1r c> {Q}"
- triple :: "['a assn, term ,'a assn] \<Rightarrow> 'a triple"
- ("{(1_)}/ _\<succ>/ {(1_)}" [3,65,3] 75)
- var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"
- ("{(1_)}/ _=\<succ>/ {(1_)}" [3,80,3] 75)
- expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple"
- ("{(1_)}/ _-\<succ>/ {(1_)}" [3,80,3] 75)
- exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple"
- ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}" [3,65,3] 75)
-
-translations
- "{P} e-\<succ> {Q}" == "{P} In1l e\<succ> {Q}"
- "{P} e=\<succ> {Q}" == "{P} In2 e\<succ> {Q}"
- "{P} e\<doteq>\<succ> {Q}" == "{P} In3 e\<succ> {Q}"
- "{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
+notation (xsymbols)
+ triple ("{(1_)}/ _\<succ>/ {(1_)}" [3,65,3] 75) and
+ var_triple ("{(1_)}/ _=\<succ>/ {(1_)}" [3,80,3] 75) and
+ expr_triple ("{(1_)}/ _-\<succ>/ {(1_)}" [3,80,3] 75) and
+ exprs_triple ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}" [3,65,3] 75)
lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
apply (rule inj_onI)
@@ -436,26 +433,25 @@
ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
("_,_|\<Turnstile>_" [61,58,58] 57)
-syntax
-
+abbreviation
triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"
( "_||=_:_" [61,0, 58] 57)
- ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"
- ( "_,_|=_" [61,58,58] 57)
-
-syntax (xsymbols)
+ where "G||=n:ts == Ball ts (triple_valid G n)"
- triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"
- ( "_|\<Turnstile>_:_" [61,0, 58] 57)
- ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"
- ( "_,_\<Turnstile>_" [61,58,58] 57)
+abbreviation
+ ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"
+ ( "_,_|=_" [61,58,58] 57)
+ where "G,A |=t == G,A|\<Turnstile>{t}"
+
+notation (xsymbols)
+ triples_valid ("_|\<Turnstile>_:_" [61,0, 58] 57) and
+ ax_valid ("_,_\<Turnstile>_" [61,58,58] 57)
defs triple_valid_def: "G\<Turnstile>n:t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
\<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
(\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
-translations "G|\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"
-defs ax_valids_def:"G,A|\<Turnstile>ts \<equiv> \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
-translations "G,A \<Turnstile>t" == "G,A|\<Turnstile>{t}"
+
+defs ax_valids_def:"G,A|\<Turnstile>ts \<equiv> \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =
(\<forall>Y s Z. P Y s Z