modernized syntax translations, using mostly abbreviation/notation;
minor tuning;
--- a/src/HOL/Bali/AxExample.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/AxExample.thy Wed Feb 10 00:45:16 2010 +0100
@@ -166,7 +166,7 @@
apply (tactic "ax_tac 1" (* NewC *))
apply (tactic "ax_tac 1" (* ax_Alloc *))
(* just for clarification: *)
-apply (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free tree \<and>. initd Ext)" in conseq2)
+apply (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free three \<and>. initd Ext)" in conseq2)
prefer 2
apply (simp add: invocation_declclass_def dynmethd_def)
apply (unfold dynlookup_def)
--- 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
--- a/src/HOL/Bali/Basis.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Basis.thy Wed Feb 10 00:45:16 2010 +0100
@@ -27,12 +27,8 @@
apply fast+
done
-syntax
- "3" :: nat ("3")
- "4" :: nat ("4")
-translations
- "3" == "Suc 2"
- "4" == "Suc 3"
+abbreviation nat3 :: nat ("3") where "3 == Suc 2"
+abbreviation nat4 :: nat ("4") where "4 == Suc 3"
(*unused*)
lemma range_bool_domain: "range f = {f True, f False}"
@@ -182,10 +178,7 @@
hide const In0 In1
-syntax
- fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
-translations
- "fun_sum" == "CONST sum_case"
+notation sum_case (infixr "'(+')"80)
consts the_Inl :: "'a + 'b \<Rightarrow> 'a"
the_Inr :: "'a + 'b \<Rightarrow> 'b"
@@ -201,18 +194,17 @@
primrec "the_In2 (In2 b) = b"
primrec "the_In3 (In3 c) = c"
-syntax
- In1l :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
- In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
-translations
- "In1l e" == "In1 (CONST Inl e)"
- "In1r c" == "In1 (CONST Inr c)"
+abbreviation In1l :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
+ where "In1l e == In1 (Inl e)"
+
+abbreviation In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
+ where "In1r c == In1 (Inr c)"
-syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
- the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
-translations
- "the_In1l" == "the_Inl \<circ> the_In1"
- "the_In1r" == "the_Inr \<circ> the_In1"
+abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
+ where "the_In1l == the_Inl \<circ> the_In1"
+
+abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
+ where "the_In1r == the_Inr \<circ> the_In1"
ML {*
fun sum3_instantiate ctxt thm = map (fn s =>
@@ -319,8 +311,8 @@
syntax
"_lpttrn" :: "[pttrn,pttrn] => pttrn" ("_#/_" [901,900] 900)
translations
- "%y#x#xs. b" == "lsplit (%y x#xs. b)"
- "%x#xs . b" == "lsplit (%x xs . b)"
+ "%y#x#xs. b" == "CONST lsplit (%y x#xs. b)"
+ "%x#xs . b" == "CONST lsplit (%x xs . b)"
lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
apply (unfold lsplit_def)
--- a/src/HOL/Bali/Decl.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Decl.thy Wed Feb 10 00:45:16 2010 +0100
@@ -402,17 +402,21 @@
"prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
"prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
-syntax
- iface :: "prog \<Rightarrow> (qtname, iface) table"
- "class" :: "prog \<Rightarrow> (qtname, class) table"
- is_iface :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
- is_class :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
+abbreviation
+ iface :: "prog \<Rightarrow> (qtname, iface) table"
+ where "iface G I == table_of (ifaces G) I"
+
+abbreviation
+ "class" :: "prog \<Rightarrow> (qtname, class) table"
+ where "class G C == table_of (classes G) C"
-translations
- "iface G I" == "table_of (ifaces G) I"
- "class G C" == "table_of (classes G) C"
- "is_iface G I" == "iface G I \<noteq> None"
- "is_class G C" == "class G C \<noteq> None"
+abbreviation
+ is_iface :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
+ where "is_iface G I == iface G I \<noteq> None"
+
+abbreviation
+ is_class :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
+ where "is_class G C == class G C \<noteq> None"
section "is type"
@@ -445,21 +449,22 @@
subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
-syntax
- "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
- "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- "_subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
+abbreviation
+ subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
+ where "G|-C <:C1 D == (C,D) \<in> subcls1 G"
+
+abbreviation
+ subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
+ where "G|-C <=:C D == (C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
-syntax (xsymbols)
- "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70)
- "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70)
- "_subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
+abbreviation
+ subcls_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
+ where "G|-C <:C D == (C,D) \<in>(subcls1 G)^+"
-translations
- "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
- "G\<turnstile>C \<preceq>\<^sub>C D" == "(C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
- "G\<turnstile>C \<prec>\<^sub>C D" == "(C,D) \<in>(subcls1 G)^+"
-
+notation (xsymbols)
+ subcls1_syntax ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70) and
+ subclseq_syntax ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70) and
+ subcls_syntax ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk>
\<Longrightarrow> (I,J) \<in> subint1 G"
--- a/src/HOL/Bali/DeclConcepts.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Wed Feb 10 00:45:16 2010 +0100
@@ -13,8 +13,8 @@
"is_public G qn \<equiv> (case class G qn of
None \<Rightarrow> (case iface G qn of
None \<Rightarrow> False
- | Some iface \<Rightarrow> access iface = Public)
- | Some class \<Rightarrow> access class = Public)"
+ | Some i \<Rightarrow> access i = Public)
+ | Some c \<Rightarrow> access c = Public)"
subsection "accessibility of types (cf. 6.6.1)"
text {*
@@ -445,21 +445,17 @@
| Protected \<Rightarrow> True
| Public \<Rightarrow> True)"
-syntax
-Method_inheritable_in::
+abbreviation
+Method_inheritable_in_syntax::
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool"
("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60)
+ where "G\<turnstile>Method m inheritable_in p == G\<turnstile>methdMembr m inheritable_in p"
-translations
-"G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p"
-
-syntax
+abbreviation
Methd_inheritable_in::
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool"
("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60)
-
-translations
-"G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p"
+ where "G\<turnstile>Methd s m inheritable_in p == G\<turnstile>(method s m) inheritable_in p"
subsubsection "declared-in/undeclared-in"
@@ -486,17 +482,15 @@
fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn = Some f
| mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
-syntax
+abbreviation
method_declared_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
("_\<turnstile>Method _ declared'_in _" [61,61,61] 60)
-translations
-"G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C"
+ where "G\<turnstile>Method m declared_in C == G\<turnstile>mdecl (mthd m) declared_in C"
-syntax
+abbreviation
methd_declared_in:: "prog \<Rightarrow> sig \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
("_\<turnstile>Methd _ _ declared'_in _" [61,61,61,61] 60)
-translations
-"G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C"
+ where "G\<turnstile>Methd s m declared_in C == G\<turnstile>mdecl (s,mthd m) declared_in C"
lemma declared_in_classD:
"G\<turnstile>m declared_in C \<Longrightarrow> is_class G C"
@@ -538,26 +532,20 @@
of S will not inherit the member, regardless if they are in the same
package as A or not.*}
-syntax
+abbreviation
method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile>Method _ member'_of _" [61,61,61] 60)
+ where "G\<turnstile>Method m member_of C == G\<turnstile>(methdMembr m) member_of C"
-translations
- "G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C"
-
-syntax
+abbreviation
methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60)
+ where "G\<turnstile>Methd s m member_of C == G\<turnstile>(method s m) member_of C"
-translations
- "G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C"
-
-syntax
+abbreviation
fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile>Field _ _ member'_of _" [61,61,61] 60)
-
-translations
- "G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C"
+ where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C"
constdefs
inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool"
@@ -578,19 +566,15 @@
is necessary since not all members are inherited to subclasses. So such
members are not member-of the subclass but member-in the subclass.*}
-syntax
+abbreviation
method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile>Method _ member'_in _" [61,61,61] 60)
+ where "G\<turnstile>Method m member_in C == G\<turnstile>(methdMembr m) member_in C"
-translations
- "G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C"
-
-syntax
+abbreviation
methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60)
-
-translations
- "G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C"
+ where "G\<turnstile>Methd s m member_in C == G\<turnstile>(method s m) member_in C"
lemma member_inD: "G\<turnstile>m member_in C
\<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
@@ -649,18 +633,16 @@
| Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk>
\<Longrightarrow> G\<turnstile>new overrides old"
-syntax
+abbreviation (input)
sig_stat_overrides::
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool"
("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60)
-translations
- "G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)"
+ where "G,s\<turnstile>new overrides\<^sub>S old == G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)"
-syntax
+abbreviation (input)
sig_overrides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool"
("_,_\<turnstile> _ overrides _" [61,61,61,61] 60)
-translations
- "G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)"
+ where "G,s\<turnstile>new overrides old == G\<turnstile>(qmdecl s new) overrides (qmdecl s old)"
subsubsection "Hiding"
@@ -674,11 +656,10 @@
G\<turnstile>Method old declared_in (declclass old) \<and>
G\<turnstile>Method old inheritable_in pid (declclass new)"
-syntax
-sig_hides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
+abbreviation
+sig_hides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool"
("_,_\<turnstile> _ hides _" [61,61,61,61] 60)
-translations
- "G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)"
+ where "G,s\<turnstile>new hides old == G\<turnstile>(qmdecl s new) hides (qmdecl s old)"
lemma hidesI:
"\<lbrakk>is_static new; msig new = msig old;
@@ -731,14 +712,14 @@
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
-"G\<turnstile>membr in class permits_acc_from accclass
+"G\<turnstile>membr in cls permits_acc_from accclass
\<equiv> (case (accmodi membr) of
Private \<Rightarrow> (declclass membr = accclass)
| Package \<Rightarrow> (pid (declclass membr) = pid accclass)
| Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
\<or>
(G\<turnstile>accclass \<prec>\<^sub>C declclass membr
- \<and> (G\<turnstile>class \<preceq>\<^sub>C accclass \<or> is_static membr))
+ \<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr))
| Public \<Rightarrow> True)"
text {*
The subcondition of the @{term "Protected"} case:
@@ -774,12 +755,14 @@
| "G\<turnstile>Method m of cls accessible_from accclass \<equiv> accessible_fromR G accclass (methdMembr m) cls"
-| Immediate: "\<lbrakk>G\<turnstile>membr member_of class;
+| Immediate: "!!membr class.
+ \<lbrakk>G\<turnstile>membr member_of class;
G\<turnstile>(Class class) accessible_in (pid accclass);
G\<turnstile>membr in class permits_acc_from accclass
\<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
-| Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
+| Overriding: "!!membr class C new old supr.
+ \<lbrakk>G\<turnstile>membr member_of class;
G\<turnstile>(Class class) accessible_in (pid accclass);
membr=(C,mdecl new);
G\<turnstile>(C,new) overrides\<^sub>S old;
@@ -787,23 +770,21 @@
G\<turnstile>Method old of supr accessible_from accclass
\<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
-syntax
+abbreviation
methd_accessible_from::
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
+ where
+ "G\<turnstile>Methd s m of cls accessible_from accclass ==
+ G\<turnstile>(method s m) of cls accessible_from accclass"
-translations
-"G\<turnstile>Methd s m of cls accessible_from accclass"
- \<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass"
-
-syntax
+abbreviation
field_accessible_from::
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile>Field _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
-
-translations
-"G\<turnstile>Field fn f of C accessible_from accclass"
- \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass"
+ where
+ "G\<turnstile>Field fn f of C accessible_from accclass ==
+ G\<turnstile>(fieldm fn f) of C accessible_from accclass"
inductive
dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
@@ -817,34 +798,32 @@
| "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC (methdMembr m) C"
-| Immediate: "\<lbrakk>G\<turnstile>membr member_in class;
+| Immediate: "!!class. \<lbrakk>G\<turnstile>membr member_in class;
G\<turnstile>membr in class permits_acc_from accclass
\<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
-| Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
+| Overriding: "!!class. \<lbrakk>G\<turnstile>membr member_in class;
membr=(C,mdecl new);
G\<turnstile>(C,new) overrides old;
G\<turnstile>class \<prec>\<^sub>C supr;
G\<turnstile>Method old in supr dyn_accessible_from accclass
\<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
-syntax
+abbreviation
methd_dyn_accessible_from::
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
+ where
+ "G\<turnstile>Methd s m in C dyn_accessible_from accC ==
+ G\<turnstile>(method s m) in C dyn_accessible_from accC"
-translations
-"G\<turnstile>Methd s m in C dyn_accessible_from accC"
- \<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC"
-
-syntax
+abbreviation
field_dyn_accessible_from::
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
-
-translations
-"G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
- \<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
+ where
+ "G\<turnstile>Field fn f in dynC dyn_accessible_from accC ==
+ G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S
--- a/src/HOL/Bali/Eval.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Eval.thy Wed Feb 10 00:45:16 2010 +0100
@@ -125,20 +125,21 @@
assignment.
*}
-syntax (xsymbols)
+abbreviation (xsymbols)
dummy_res :: "vals" ("\<diamondsuit>")
-translations
- "\<diamondsuit>" == "In1 Unit"
+ where "\<diamondsuit> == In1 Unit"
+
+abbreviation (input)
+ val_inj_vals ("\<lfloor>_\<rfloor>\<^sub>e" 1000)
+ where "\<lfloor>e\<rfloor>\<^sub>e == In1 e"
-syntax
- val_inj_vals:: "expr \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>e" 1000)
- var_inj_vals:: "var \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>v" 1000)
- lst_inj_vals:: "expr list \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>l" 1000)
+abbreviation (input)
+ var_inj_vals ("\<lfloor>_\<rfloor>\<^sub>v" 1000)
+ where "\<lfloor>v\<rfloor>\<^sub>v == In2 v"
-translations
- "\<lfloor>e\<rfloor>\<^sub>e" \<rightharpoonup> "In1 e"
- "\<lfloor>v\<rfloor>\<^sub>v" \<rightharpoonup> "In2 v"
- "\<lfloor>es\<rfloor>\<^sub>l" \<rightharpoonup> "In3 es"
+abbreviation (input)
+ lst_inj_vals ("\<lfloor>_\<rfloor>\<^sub>l" 1000)
+ where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
constdefs
undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
--- a/src/HOL/Bali/Example.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Example.thy Wed Feb 10 00:45:16 2010 +0100
@@ -1202,74 +1202,52 @@
abbreviation "one == Suc 0"
abbreviation "two == Suc one"
-abbreviation "tree == Suc two"
-abbreviation "four == Suc tree"
+abbreviation "three == Suc two"
+abbreviation "four == Suc three"
+
+abbreviation
+ "obj_a == \<lparr>tag=Arr (PrimT Boolean) 2
+ ,values= empty(Inr 0\<mapsto>Bool False)(Inr 1\<mapsto>Bool False)\<rparr>"
-syntax
- obj_a :: obj
- obj_b :: obj
- obj_c :: obj
- arr_N :: "(vn, val) table"
- arr_a :: "(vn, val) table"
- globs1 :: globs
- globs2 :: globs
- globs3 :: globs
- globs8 :: globs
- locs3 :: locals
- locs4 :: locals
- locs8 :: locals
- s0 :: state
- s0' :: state
- s9' :: state
- s1 :: state
- s1' :: state
- s2 :: state
- s2' :: state
- s3 :: state
- s3' :: state
- s4 :: state
- s4' :: state
- s6' :: state
- s7' :: state
- s8 :: state
- s8' :: state
+abbreviation
+ "obj_b == \<lparr>tag=CInst Ext
+ ,values=(empty(Inl (vee, Base)\<mapsto>Null )
+ (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
+
+abbreviation
+ "obj_c == \<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
+
+abbreviation "arr_N == empty(Inl (arr, Base)\<mapsto>Null)"
+abbreviation "arr_a == empty(Inl (arr, Base)\<mapsto>Addr a)"
+
+abbreviation
+ "globs1 == empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
+ (Inr Base \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>)
+ (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)"
-translations
- "obj_a" <= "\<lparr>tag=Arr (PrimT Boolean) (CONST two)
- ,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(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(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)(CONST Inr()\<mapsto>Addr b)"
- "locs8" == "locs3(VName (CONST z)\<mapsto>Addr c)"
- "s0" == " st (CONST empty) (CONST empty)"
- "s0'" == " Norm s0"
- "s1" == " st globs1 (CONST empty)"
- "s1'" == " Norm s1"
- "s2" == " st globs2 (CONST empty)"
- "s2'" == " Norm s2"
- "s3" == " st globs3 locs3 "
- "s3'" == " Norm s3"
- "s4" == " st globs3 locs4"
- "s4'" == " Norm s4"
- "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
- "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
- "s8" == " st globs8 locs8"
- "s8'" == " Norm s8"
- "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
+abbreviation
+ "globs2 == empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
+ (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
+ (Inl a\<mapsto>obj_a)
+ (Inr Base \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)"
+
+abbreviation "globs3 == globs2(Inl b\<mapsto>obj_b)"
+abbreviation "globs8 == globs3(Inl c\<mapsto>obj_c)"
+abbreviation "locs3 == empty(VName e\<mapsto>Addr b)"
+abbreviation "locs8 == locs3(VName z\<mapsto>Addr c)"
+
+abbreviation "s0 == st empty empty"
+abbreviation "s0' == Norm s0"
+abbreviation "s1 == st globs1 empty"
+abbreviation "s1' == Norm s1"
+abbreviation "s2 == st globs2 empty"
+abbreviation "s2' == Norm s2"
+abbreviation "s3 == st globs3 locs3"
+abbreviation "s3' == Norm s3"
+abbreviation "s7' == (Some (Xcpt (Std NullPointer)), s3)"
+abbreviation "s8 == st globs8 locs8"
+abbreviation "s8' == Norm s8"
+abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)"
declare Pair_eq [simp del]
@@ -1293,7 +1271,7 @@
apply (rule eval_Is (* NewC *))
(* begin init Ext *)
apply (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
-apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
+apply (erule_tac V = "atleast_free ?h three" in thin_rl)
apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
apply (rule eval_Is (* Init Ext *))
@@ -1336,7 +1314,7 @@
apply (drule alloc_one)
apply (simp (no_asm_simp))
apply clarsimp
-apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
+apply (erule_tac V = "atleast_free ?h three" in thin_rl)
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
apply (simp (no_asm_use))
apply (rule eval_Is (* Try *))
--- a/src/HOL/Bali/Name.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Name.thy Wed Feb 10 00:45:16 2010 +0100
@@ -20,13 +20,11 @@
datatype lname --{* names for local variables and the This pointer *}
= EName ename
| This
-syntax
- VName :: "vname \<Rightarrow> lname"
- Result :: lname
+abbreviation VName :: "vname \<Rightarrow> lname"
+ where "VName n == EName (VNam n)"
-translations
- "VName n" == "EName (VNam n)"
- "Result" == "EName Res"
+abbreviation Result :: lname
+ where "Result == EName Res"
datatype xname --{* names of standard exceptions *}
= Throwable
--- a/src/HOL/Bali/State.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/State.thy Wed Feb 10 00:45:16 2010 +0100
@@ -254,13 +254,11 @@
by (simp add: heap_def)
-syntax
- val_this :: "st \<Rightarrow> val"
- lookup_obj :: "st \<Rightarrow> val \<Rightarrow> obj"
+abbreviation val_this :: "st \<Rightarrow> val"
+ where "val_this s == the (locals s This)"
-translations
- "val_this s" == "CONST the (locals s This)"
- "lookup_obj s a'" == "CONST the (heap s (the_Addr a'))"
+abbreviation lookup_obj :: "st \<Rightarrow> val \<Rightarrow> obj"
+ where "lookup_obj s a' == the (heap s (the_Addr a'))"
subsection "memory allocation"
@@ -286,12 +284,8 @@
subsection "initialization"
-syntax
-
- init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
-
-translations
- "init_vals vs" == "CONST Option.map default_val \<circ> vs"
+abbreviation init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
+ where "init_vals vs == Option.map default_val \<circ> vs"
lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
apply (unfold arr_comps_def in_bounds_def)
@@ -325,11 +319,9 @@
init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
"init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
-syntax
+abbreviation
init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
-
-translations
- "init_class_obj G C" == "init_obj G CONST undefined (CONST Inr C)"
+ where "init_class_obj G C == init_obj G undefined (Inr C)"
lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
apply (unfold gupd_def)
@@ -513,19 +505,17 @@
apply auto
done
-syntax
+abbreviation raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
+ where "raise_if c xn == abrupt_if c (Some (Xcpt (Std xn)))"
+
+abbreviation np :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
+ where "np v == raise_if (v = Null) NullPointer"
- raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
- np :: "val \<spacespace> \<Rightarrow> abopt \<Rightarrow> abopt"
- check_neg:: "val \<spacespace> \<Rightarrow> abopt \<Rightarrow> abopt"
- error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt"
-
-translations
+abbreviation check_neg :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
+ where "check_neg i' == raise_if (the_Intg i'<0) NegArrSize"
- "raise_if c xn" == "abrupt_if c (Some (Xcpt (Std xn)))"
- "np v" == "raise_if (v = Null) NullPointer"
- "check_neg i'" == "raise_if (the_Intg i'<0) NegArrSize"
- "error_if c e" == "abrupt_if c (Some (Error e))"
+abbreviation error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt"
+ where "error_if c e == abrupt_if c (Some (Error e))"
lemma raise_if_None [simp]: "(raise_if c x y = None) = (\<not>c \<and> y = None)"
apply (simp add: abrupt_if_def)
@@ -592,22 +582,23 @@
types
state = "abopt \<times> st" --{* state including abruption information *}
-syntax
- Norm :: "st \<Rightarrow> state"
- abrupt :: "state \<Rightarrow> abopt"
- store :: "state \<Rightarrow> st"
-
translations
-
- "Norm s" == "(None,s)"
- "abrupt" => "fst"
- "store" => "snd"
"abopt" <= (type) "State.abrupt option"
"abopt" <= (type) "abrupt option"
"state" <= (type) "abopt \<times> State.st"
"state" <= (type) "abopt \<times> st"
+abbreviation
+ Norm :: "st \<Rightarrow> state"
+ where "Norm s == (None, s)"
+abbreviation (input)
+ abrupt :: "state \<Rightarrow> abopt"
+ where "abrupt == fst"
+
+abbreviation (input)
+ store :: "state \<Rightarrow> st"
+ where "store == snd"
lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False"
apply (erule_tac x = "(Some k,y)" in all_dupE)
@@ -683,15 +674,11 @@
lemma supd_abrupt_invariant [simp]: "abrupt (supd f s) = abrupt s"
by (cases s) simp
-syntax
+abbreviation set_lvars :: "locals \<Rightarrow> state \<Rightarrow> state"
+ where "set_lvars l == supd (set_locals l)"
- set_lvars :: "locals \<Rightarrow> state \<Rightarrow> state"
- restore_lvars :: "state \<Rightarrow> state \<Rightarrow> state"
-
-translations
-
- "set_lvars l" == "supd (set_locals l)"
- "restore_lvars s' s" == "set_lvars (locals (store s')) s"
+abbreviation restore_lvars :: "state \<Rightarrow> state \<Rightarrow> state"
+ where "restore_lvars s' s == set_lvars (locals (store s')) s"
lemma set_set_lvars [simp]: "\<And> s. set_lvars l (set_lvars l' s) = set_lvars l s"
apply (simp (no_asm_simp) only: split_tupled_all)
--- a/src/HOL/Bali/Term.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Term.thy Wed Feb 10 00:45:16 2010 +0100
@@ -244,22 +244,23 @@
"stmt" <= (type) "Term.stmt"
"term" <= (type) "(expr+stmt,var,expr list) sum3"
-syntax
-
- this :: expr
- LAcc :: "vname \<Rightarrow> expr" ("!!")
- LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
- Return :: "expr \<Rightarrow> stmt"
- StatRef :: "ref_ty \<Rightarrow> expr"
+abbreviation this :: expr
+ where "this == Acc (LVar This)"
+
+abbreviation LAcc :: "vname \<Rightarrow> expr" ("!!")
+ where "!!v == Acc (LVar (EName (VNam v)))"
-translations
-
- "this" == "Acc (LVar This)"
- "!!v" == "Acc (LVar (EName (VNam v)))"
- "v:==e" == "Expr (Ass (LVar (EName (VNam v))) e)"
- "Return e" == "Expr (Ass (LVar (EName Res)) e);; Jmp Ret"
- --{* \tt Res := e;; Jmp Ret *}
- "StatRef rt" == "Cast (RefT rt) (Lit Null)"
+abbreviation
+ LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
+ where "v:==e == Expr (Ass (LVar (EName (VNam v))) e)"
+
+abbreviation
+ Return :: "expr \<Rightarrow> stmt"
+ where "Return e == Expr (Ass (LVar (EName Res)) e);; Jmp Ret" --{* \tt Res := e;; Jmp Ret *}
+
+abbreviation
+ StatRef :: "ref_ty \<Rightarrow> expr"
+ where "StatRef rt == Cast (RefT rt) (Lit Null)"
constdefs
@@ -275,17 +276,21 @@
expressions, variables and expression lists into general terms.
*}
-syntax
- expr_inj_term:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
- stmt_inj_term:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
- var_inj_term:: "var \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>v" 1000)
- lst_inj_term:: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
+abbreviation (input)
+ expr_inj_term :: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
+ where "\<langle>e\<rangle>\<^sub>e == In1l e"
+
+abbreviation (input)
+ stmt_inj_term :: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
+ where "\<langle>c\<rangle>\<^sub>s == In1r c"
-translations
- "\<langle>e\<rangle>\<^sub>e" \<rightharpoonup> "In1l e"
- "\<langle>c\<rangle>\<^sub>s" \<rightharpoonup> "In1r c"
- "\<langle>v\<rangle>\<^sub>v" \<rightharpoonup> "In2 v"
- "\<langle>es\<rangle>\<^sub>l" \<rightharpoonup> "In3 es"
+abbreviation (input)
+ var_inj_term :: "var \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>v" 1000)
+ where "\<langle>v\<rangle>\<^sub>v == In2 v"
+
+abbreviation (input)
+ lst_inj_term :: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
+ where "\<langle>es\<rangle>\<^sub>l == In3 es"
text {* It seems to be more elegant to have an overloaded injection like the
following.
@@ -300,7 +305,7 @@
@{text AxSem} don't follow this convention right now, but introduce subtle
syntactic sugar in the relations themselves to make a distinction on
expressions, statements and so on. So unfortunately you will encounter a
-mixture of dealing with these injections. The translations above are used
+mixture of dealing with these injections. The abbreviations above are used
as bridge between the different conventions.
*}
--- a/src/HOL/Bali/Trans.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Trans.thy Wed Feb 10 00:45:16 2010 +0100
@@ -60,13 +60,13 @@
by (simp)
declare the_var_AVar_def [simp del]
-syntax (xsymbols)
- Ref :: "loc \<Rightarrow> expr"
- SKIP :: "expr"
+abbreviation
+ Ref :: "loc \<Rightarrow> expr"
+ where "Ref a == Lit (Addr a)"
-translations
- "Ref a" == "Lit (Addr a)"
- "SKIP" == "Lit Unit"
+abbreviation
+ SKIP :: "expr"
+ where "SKIP == Lit Unit"
inductive
step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
--- a/src/HOL/Bali/Type.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Type.thy Wed Feb 10 00:45:16 2010 +0100
@@ -36,17 +36,11 @@
"ref_ty" <= (type) "Type.ref_ty"
"ty" <= (type) "Type.ty"
-syntax
- NT :: " \<spacespace> ty"
- Iface :: "qtname \<Rightarrow> ty"
- Class :: "qtname \<Rightarrow> ty"
- Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90)
-
-translations
- "NT" == "RefT NullT"
- "Iface I" == "RefT (IfaceT I)"
- "Class C" == "RefT (ClassT C)"
- "T.[]" == "RefT (ArrayT T)"
+abbreviation "NT == RefT NullT"
+abbreviation "Iface I == RefT (IfaceT I)"
+abbreviation "Class C == RefT (ClassT C)"
+abbreviation Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90)
+ where "T.[] == RefT (ArrayT T)"
constdefs
the_Class :: "ty \<Rightarrow> qtname"
--- a/src/HOL/Bali/TypeRel.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/TypeRel.thy Wed Feb 10 00:45:16 2010 +0100
@@ -35,37 +35,22 @@
(*subclseq, by translation*) (* subclass + identity *)
implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
-syntax
+abbreviation
+ subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
+ where "G|-I <:I1 J == (I,J) \<in> subint1 G"
- "_subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
- "_subint" :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
- (* Defined in Decl.thy:
- "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
- "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- "_subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
- *)
- "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_" [71,71,71] 70)
-
-syntax (xsymbols)
+abbreviation
+ subint_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
+ where "G|-I <=:I J == (I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
- "_subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_" [71,71,71] 70)
- "_subint" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _" [71,71,71] 70)
- (* Defined in Decl.thy:
-\ "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70)
- "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70)
- "_subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
- *)
- "_implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70)
+abbreviation
+ implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_~>1_" [71,71,71] 70)
+ where "G|-C ~>1 I == (C,I) \<in> implmt1 G"
-translations
-
- "G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G"
- "G\<turnstile>I \<preceq>I J" == "(I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
- (* Defined in Decl.thy:
- "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
- "G\<turnstile>C \<preceq>\<^sub>C D" == "(C,D) \<in>(subcls1 G)^*"
- *)
- "G\<turnstile>C \<leadsto>1 I" == "(C,I) \<in> implmt1 G"
+notation (xsymbols)
+ subint1_syntax ("_\<turnstile>_\<prec>I1_" [71,71,71] 70) and
+ subint_syntax ("_\<turnstile>_\<preceq>I _" [71,71,71] 70) and
+ implmt1_syntax ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70)
section "subclass and subinterface relations"
--- a/src/HOL/Bali/WellForm.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/WellForm.thy Wed Feb 10 00:45:16 2010 +0100
@@ -2925,7 +2925,7 @@
then show "?P m"
by (auto simp add: permits_acc_def)
next
- case (Overriding new C declC newm old Sup)
+ case (Overriding new declC newm old Sup C)
assume member_new: "G \<turnstile> new member_in C" and
new: "new = (declC, mdecl newm)" and
override: "G \<turnstile> (declC, newm) overrides old" and
--- a/src/HOL/Bali/WellType.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/WellType.thy Wed Feb 10 00:45:16 2010 +0100
@@ -43,11 +43,9 @@
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
-
-syntax
+abbreviation
pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
-translations
- "pkg e" == "pid (cls e)"
+ where "pkg e == pid (cls e)"
section "Static overloading: maximally specific methods "
@@ -426,29 +424,33 @@
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
-syntax (* for purely static typing *)
- "_wt" :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
- "_wt_stmt" :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
- "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
- "_ty_var" :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
- "_ty_exprs":: "env \<Rightarrow> [expr list,
- \<spacespace> ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
+(* for purely static typing *)
+abbreviation
+ wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
+ where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
+
+abbreviation
+ wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
+ where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
+
+abbreviation
+ ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
+ where "E|-e:-T == E|-In1l e :: Inl T"
-syntax (xsymbols)
- "_wt" :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50)
- "_wt_stmt" :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50)
- "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
- "_ty_var" :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
- "_ty_exprs" :: "env \<Rightarrow> [expr list,
- \<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
+abbreviation
+ ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
+ where "E|-e:=T == E|-In2 e :: Inl T"
-translations
- "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> 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"
+abbreviation
+ ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
+ where "E|-e:#T == E|-In3 e :: Inr T"
+notation (xsymbols)
+ wt_syntax ("_\<turnstile>_\<Colon>_" [51,51,51] 50) and
+ wt_stmt_syntax ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) and
+ ty_expr_syntax ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
+ ty_var_syntax ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
+ ty_exprs_syntax ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
declare not_None_eq [simp del]
declare split_if [split del] split_if_asm [split del]