--- a/src/HOL/MicroJava/J/Conform.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Sep 22 16:28:53 2000 +0200
@@ -12,23 +12,43 @@
constdefs
- hext :: "aheap => aheap => bool" ( "_\\<le>|_" [51,51] 50)
+ hext :: "aheap => aheap => bool" ("_ \\<le>| _" [51,51] 50)
"h\\<le>|h' == \\<forall>a C fs. h a = Some(C,fs) --> (\\<exists>fs'. h' a = Some(C,fs'))"
- conf :: "'c prog => aheap => val => ty => bool" ( "_,_\\<turnstile>_::\\<preceq>_" [51,51,51,51] 50)
+ conf :: "'c prog => aheap => val => ty => bool" ("_,_ \\<turnstile> _ ::\\<preceq> _" [51,51,51,51] 50)
"G,h\\<turnstile>v::\\<preceq>T == \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
- ("_,_\\<turnstile>_[::\\<preceq>]_" [51,51,51,51] 50)
+ ("_,_ \\<turnstile> _ [::\\<preceq>] _" [51,51,51,51] 50)
"G,h\\<turnstile>vs[::\\<preceq>]Ts == \\<forall>n T. Ts n = Some T --> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T)"
- oconf :: "'c prog => aheap => obj => bool" ("_,_\\<turnstile>_\\<surd>" [51,51,51] 50)
+ oconf :: "'c prog => aheap => obj => bool" ("_,_ \\<turnstile> _ \\<surd>" [51,51,51] 50)
"G,h\\<turnstile>obj\\<surd> == G,h\\<turnstile>snd obj[::\\<preceq>]map_of (fields (G,fst obj))"
- hconf :: "'c prog => aheap => bool" ("_\\<turnstile>h _\\<surd>" [51,51] 50)
+ hconf :: "'c prog => aheap => bool" ("_ \\<turnstile>h _ \\<surd>" [51,51] 50)
"G\\<turnstile>h h\\<surd> == \\<forall>a obj. h a = Some obj --> G,h\\<turnstile>obj\\<surd>"
- conforms :: "state => java_mb env_ => bool" ("_::\\<preceq>_" [51,51] 50)
+ conforms :: "state => java_mb env_ => bool" ("_ ::\\<preceq> _" [51,51] 50)
"s::\\<preceq>E == prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[::\\<preceq>]localT E"
+
+syntax (HTML)
+ hext :: "aheap => aheap => bool"
+ ("_ <=| _" [51,51] 50)
+
+ conf :: "'c prog => aheap => val => ty => bool"
+ ("_,_ |- _ ::<= _" [51,51,51,51] 50)
+
+ lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
+ ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
+
+ oconf :: "'c prog => aheap => obj => bool"
+ ("_,_ |- _ [ok]" [51,51,51] 50)
+
+ hconf :: "'c prog => aheap => bool"
+ ("_ |-h _ [ok]" [51,51] 50)
+
+ conforms :: "state => java_mb env_ => bool"
+ ("_ ::<= _" [51,51] 50)
+
end
--- a/src/HOL/MicroJava/J/Eval.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Fri Sep 22 16:28:53 2000 +0200
@@ -16,12 +16,22 @@
syntax
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
- ("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
+ ("_ \\<turnstile> _ -_\\<succ>_-> _" [51,82,82,82,82] 81)
evals:: "[java_mb prog,xstate,expr list,
val list,xstate] => bool "
- ("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
+ ("_ \\<turnstile> _ -_[\\<succ>]_-> _" [51,82,51,51,82] 81)
exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
- ("_\\<turnstile>_ -_-> _" [51,82,82, 82]81)
+ ("_ \\<turnstile> _ -_-> _" [51,82,82,82] 81)
+
+syntax (HTML)
+ eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
+ ("_ |- _ -_>_-> _" [51,82,82,82,82] 81)
+ evals:: "[java_mb prog,xstate,expr list,
+ val list,xstate] => bool "
+ ("_ |- _ -_[>]_-> _" [51,82,51,51,82] 81)
+ exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
+ ("_ |- _ -_-> _" [51,82,82,82] 81)
+
translations
"G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval G"
--- a/src/HOL/MicroJava/J/State.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy Fri Sep 22 16:28:53 2000 +0200
@@ -14,7 +14,6 @@
obj = "cname \\<times> fields_" (* class instance with class name and fields *)
constdefs
-
obj_ty :: "obj => ty"
"obj_ty obj == Class (fst obj)"
@@ -42,9 +41,9 @@
Norm :: "state => xstate"
translations
- "heap" => "fst"
- "locals" => "snd"
- "Norm s" == "(None,s)"
+ "heap" => "fst"
+ "locals" => "snd"
+ "Norm s" == "(None,s)"
constdefs
--- a/src/HOL/MicroJava/J/Term.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Fri Sep 22 16:28:53 2000 +0200
@@ -11,21 +11,23 @@
datatype binop = Eq | Add (* function codes for binary operation *)
datatype expr
- = NewC cname (* class instance creation *)
- | Cast cname expr (* type cast *)
- | Lit val (* literal value, also references *)
- | BinOp binop expr expr (* binary operation *)
- | LAcc vname (* local (incl. parameter) access *)
- | LAss vname expr (* local assign *) ("_::=_" [ 90,90]90)
- | FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90)
+ = NewC cname (* class instance creation *)
+ | Cast cname expr (* type cast *)
+ | Lit val (* literal value, also references *)
+ | BinOp binop expr expr (* binary operation *)
+ | LAcc vname (* local (incl. parameter) access *)
+ | LAss vname expr (* local assign *) ("_::=_" [ 90,90]90)
+ | FAcc cname expr vname (* field access *) ("{_}_.._" [10,90,99 ]90)
| FAss cname expr vname
- expr (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
- | Call expr mname (ty list) (expr list)(* method call*)
- ("_.._'({_}_')" [90,99,10,10] 90)
+ expr (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
+ | Call expr mname
+ (ty list) (expr list) (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
+
and stmt
- = Skip (* empty statement *)
- | Expr expr (* expression statement *)
- | Comp stmt stmt ("_;; _" [ 61,60]60)
- | Cond expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
- | Loop expr stmt ("While'(_') _" [ 80,79]70)
+ = Skip (* empty statement *)
+ | Expr expr (* expression statement *)
+ | Comp stmt stmt ("_;; _" [61,60]60)
+ | Cond expr stmt stmt ("If '(_') _ Else _" [80,79,79]70)
+ | Loop expr stmt ("While '(_') _" [80,79]70)
+
end
--- a/src/HOL/MicroJava/J/Type.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Fri Sep 22 16:28:53 2000 +0200
@@ -8,32 +8,35 @@
Type = JBasis +
-types cname (* class name *)
- vnam (* variable or field name *)
- mname (* method name *)
+types cname (* class name *)
+ vnam (* variable or field name *)
+ mname (* method name *)
+
arities cname, vnam, mname :: term
datatype vname (* names for This pointer and local/field variables *)
- = This
- | VName vnam
+ = This
+ | VName vnam
-datatype prim_ty (* primitive type, cf. 4.2 *)
- = Void (* 'result type' of void methods *)
- | Boolean
- | Integer
+datatype prim_ty (* primitive type, cf. 4.2 *)
+ = Void (* 'result type' of void methods *)
+ | Boolean
+ | Integer
datatype ref_ty (* reference type, cf. 4.3 *)
- = NullT (* null type, cf. 4.1 *)
- | ClassT cname (* class type *)
-datatype ty (* any type, cf. 4.1 *)
- = PrimT prim_ty (* primitive type *)
- | RefT ref_ty (* reference type *)
+ = NullT (* null type, cf. 4.1 *)
+ | ClassT cname (* class type *)
+
+datatype ty (* any type, cf. 4.1 *)
+ = PrimT prim_ty (* primitive type *)
+ | RefT ref_ty (* reference type *)
syntax
- NT :: " ty"
- Class :: "cname => ty"
+ NT :: " ty"
+ Class :: "cname => ty"
+
translations
- "NT" == "RefT NullT"
+ "NT" == "RefT NullT"
"Class C" == "RefT (ClassT C)"
end
--- a/src/HOL/MicroJava/J/TypeRel.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Sep 22 16:28:53 2000 +0200
@@ -9,21 +9,27 @@
TypeRel = Decl +
consts
- subcls1 :: "'c prog => (cname \\<times> cname) set" (* subclass *)
- widen :: "'c prog => (ty \\<times> ty ) set" (* widening *)
- cast :: "'c prog => (cname \\<times> cname) set" (* casting *)
+ subcls1 :: "'c prog => (cname \\<times> cname) set" (* subclass *)
+ widen :: "'c prog => (ty \\<times> ty ) set" (* widening *)
+ cast :: "'c prog => (cname \\<times> cname) set" (* casting *)
syntax
- subcls1 :: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<prec>C1_" [71,71,71] 70)
- subcls :: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>C _" [71,71,71] 70)
- widen :: "'c prog => [ty , ty ] => bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70)
- cast :: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
+ subcls1 :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<prec>C1 _" [71,71,71] 70)
+ subcls :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>C _" [71,71,71] 70)
+ widen :: "'c prog => [ty , ty ] => bool" ("_ \\<turnstile> _ \\<preceq> _" [71,71,71] 70)
+ cast :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>? _" [71,71,71] 70)
+
+syntax (HTML)
+ subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
+ subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
+ widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70)
+ cast :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
translations
- "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
- "G\\<turnstile>C \\<preceq>C D" == "(C,D) \\<in> (subcls1 G)^*"
- "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G"
- "G\\<turnstile>C \\<preceq>? D" == "(C,D) \\<in> cast G"
+ "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
+ "G\\<turnstile>C \\<preceq>C D" == "(C,D) \\<in> (subcls1 G)^*"
+ "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G"
+ "G\\<turnstile>C \\<preceq>? D" == "(C,D) \\<in> cast G"
defs
--- a/src/HOL/MicroJava/J/Value.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Fri Sep 22 16:28:53 2000 +0200
@@ -8,44 +8,45 @@
Value = Type +
-types loc (* locations, i.e. abstract references on objects *)
+types loc (* locations, i.e. abstract references on objects *)
arities loc :: term
-datatype val_ (* name non 'val' because of clash with ML token *)
- = Unit (* dummy result value of void methods *)
- | Null (* null reference *)
- | Bool bool (* Boolean value *)
- | Intg int (* integer value *) (* Name Intg instead of Int because
- of clash with HOL/Set.thy *)
- | Addr loc (* addresses, i.e. locations of objects *)
+datatype val_ (* name non 'val' because of clash with ML token *)
+ = Unit (* dummy result value of void methods *)
+ | Null (* null reference *)
+ | Bool bool (* Boolean value *)
+ | Intg int (* integer value, name Intg instead of Int because
+ of clash with HOL/Set.thy *)
+ | Addr loc (* addresses, i.e. locations of objects *)
+
types val = val_
translations "val" <= (type) "val_"
consts
- the_Bool :: "val => bool"
- the_Intg :: "val => int"
- the_Addr :: "val => loc"
+ the_Bool :: "val => bool"
+ the_Intg :: "val => int"
+ the_Addr :: "val => loc"
primrec
- "the_Bool (Bool b) = b"
+ "the_Bool (Bool b) = b"
primrec
- "the_Intg (Intg i) = i"
+ "the_Intg (Intg i) = i"
primrec
- "the_Addr (Addr a) = a"
+ "the_Addr (Addr a) = a"
consts
- defpval :: "prim_ty => val" (* default value for primitive types *)
- default_val :: "ty => val" (* default value for all types *)
+ defpval :: "prim_ty => val" (* default value for primitive types *)
+ default_val :: "ty => val" (* default value for all types *)
primrec
- "defpval Void = Unit"
- "defpval Boolean = Bool False"
- "defpval Integer = Intg (#0)"
+ "defpval Void = Unit"
+ "defpval Boolean = Bool False"
+ "defpval Integer = Intg (#0)"
primrec
- "default_val (PrimT pt) = defpval pt"
- "default_val (RefT r ) = Null"
+ "default_val (PrimT pt) = defpval pt"
+ "default_val (RefT r ) = Null"
end
--- a/src/HOL/MicroJava/J/WellForm.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Fri Sep 22 16:28:53 2000 +0200
@@ -19,17 +19,16 @@
types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
constdefs
-
- wf_fdecl :: "'c prog => fdecl => bool"
+ wf_fdecl :: "'c prog => fdecl => bool"
"wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
- wf_mhead :: "'c prog => sig => ty => bool"
+ wf_mhead :: "'c prog => sig => ty => bool"
"wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
- wf_mdecl :: "'c wf_mb => 'c wf_mb"
+ wf_mdecl :: "'c wf_mb => 'c wf_mb"
"wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
- wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
+ wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
"wf_cdecl wf_mb G ==
\\<lambda>(C,(sc,fs,ms)).
(\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and>
@@ -40,7 +39,7 @@
(\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
- wf_prog :: "'c wf_mb => 'c prog => bool"
+ wf_prog :: "'c wf_mb => 'c prog => bool"
"wf_prog wf_mb G ==
let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
--- a/src/HOL/MicroJava/J/WellType.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Fri Sep 22 16:28:53 2000 +0200
@@ -23,26 +23,22 @@
= "'c prog \\<times> lenv"
syntax
-
- prg :: "'c env => 'c prog"
- localT :: "'c env => (vname \\<leadsto> ty)"
+ prg :: "'c env => 'c prog"
+ localT :: "'c env => (vname \\<leadsto> ty)"
translations
-
- "prg" => "fst"
- "localT" => "snd"
+ "prg" => "fst"
+ "localT" => "snd"
consts
-
- more_spec :: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
- (ty \\<times> 'x) \\<times> ty list => bool"
- appl_methds :: "'c prog => cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
- max_spec :: "'c prog => cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
+ more_spec :: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
+ (ty \\<times> 'x) \\<times> ty list => bool"
+ appl_methds :: "'c prog => cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
+ max_spec :: "'c prog => cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
defs
-
- more_spec_def "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
- list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
+ more_spec_def "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
+ list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
(* applicable methods, cf. 15.11.2.1 *)
appl_methds_def "appl_methds G C == \\<lambda>(mn, pTs).
@@ -51,11 +47,11 @@
list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
(* maximally specific methods, cf. 15.11.2.2 *)
- max_spec_def "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and>
- (\\<forall>m'\\<in>appl_methds G C sig.
- more_spec G m' m --> m' = m)}"
+ max_spec_def "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and>
+ (\\<forall>m'\\<in>appl_methds G C sig.
+ more_spec G m' m --> m' = m)}"
+
consts
-
typeof :: "(loc => ty option) => val => ty option"
primrec
@@ -70,16 +66,20 @@
(* method body with parameter names, local variables, block, result expression *)
consts
-
ty_expr :: "java_mb env => (expr \\<times> ty ) set"
ty_exprs:: "java_mb env => (expr list \\<times> ty list) set"
wt_stmt :: "java_mb env => stmt set"
syntax
+ ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ \\<turnstile> _ :: _" [51,51,51]50)
+ ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \\<turnstile> _ [::] _" [51,51,51]50)
+ wt_stmt :: "java_mb env => stmt => bool" ("_ \\<turnstile> _ \\<surd>" [51,51 ]50)
-ty_expr :: "java_mb env => [expr , ty ] => bool" ("_\\<turnstile>_::_" [51,51,51]50)
-ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_\\<turnstile>_[::]_"[51,51,51]50)
-wt_stmt :: "java_mb env => stmt => bool" ("_\\<turnstile>_ \\<surd>" [51,51 ]50)
+syntax (HTML)
+ ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ |- _ :: _" [51,51,51]50)
+ ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
+ wt_stmt :: "java_mb env => stmt => bool" ("_ |- _ [ok]" [51,51 ]50)
+
translations
"E\\<turnstile>e :: T" == "(e,T) \\<in> ty_expr E"
@@ -91,84 +91,84 @@
(* well-typed expressions *)
(* cf. 15.8 *)
- NewC "[|is_class (prg E) C|] ==>
- E\\<turnstile>NewC C::Class C"
+ NewC "[| is_class (prg E) C |] ==>
+ E\\<turnstile>NewC C::Class C"
(* cf. 15.15 *)
- Cast "[|E\\<turnstile>e::Class C;
- prg E\\<turnstile>C\\<preceq>? D|] ==>
- E\\<turnstile>Cast D e::Class D"
+ Cast "[| E\\<turnstile>e::Class C;
+ prg E\\<turnstile>C\\<preceq>? D |] ==>
+ E\\<turnstile>Cast D e::Class D"
(* cf. 15.7.1 *)
- Lit "[|typeof (\\<lambda>v. None) x = Some T|] ==>
- E\\<turnstile>Lit x::T"
+ Lit "[| typeof (\\<lambda>v. None) x = Some T |] ==>
+ E\\<turnstile>Lit x::T"
(* cf. 15.13.1 *)
- LAcc "[|localT E v = Some T; is_type (prg E) T|] ==>
- E\\<turnstile>LAcc v::T"
+ LAcc "[| localT E v = Some T; is_type (prg E) T |] ==>
+ E\\<turnstile>LAcc v::T"
- BinOp "[|E\\<turnstile>e1::T;
- E\\<turnstile>e2::T;
- if bop = Eq then T' = PrimT Boolean
- else T' = T \\<and> T = PrimT Integer|] ==>
- E\\<turnstile>BinOp bop e1 e2::T'"
+ BinOp "[| E\\<turnstile>e1::T;
+ E\\<turnstile>e2::T;
+ if bop = Eq then T' = PrimT Boolean
+ else T' = T \\<and> T = PrimT Integer|] ==>
+ E\\<turnstile>BinOp bop e1 e2::T'"
(* cf. 15.25, 15.25.1 *)
- LAss "[|E\\<turnstile>LAcc v::T;
- E\\<turnstile>e::T';
- prg E\\<turnstile>T'\\<preceq>T|] ==>
- E\\<turnstile>v::=e::T'"
+ LAss "[| E\\<turnstile>LAcc v::T;
+ E\\<turnstile>e::T';
+ prg E\\<turnstile>T'\\<preceq>T |] ==>
+ E\\<turnstile>v::=e::T'"
(* cf. 15.10.1 *)
- FAcc "[|E\\<turnstile>a::Class C;
- field (prg E,C) fn = Some (fd,fT)|] ==>
- E\\<turnstile>{fd}a..fn::fT"
+ FAcc "[| E\\<turnstile>a::Class C;
+ field (prg E,C) fn = Some (fd,fT) |] ==>
+ E\\<turnstile>{fd}a..fn::fT"
(* cf. 15.25, 15.25.1 *)
- FAss "[|E\\<turnstile>{fd}a..fn::T;
- E\\<turnstile>v ::T';
- prg E\\<turnstile>T'\\<preceq>T|] ==>
- E\\<turnstile>{fd}a..fn:=v::T'"
+ FAss "[| E\\<turnstile>{fd}a..fn::T;
+ E\\<turnstile>v ::T';
+ prg E\\<turnstile>T'\\<preceq>T |] ==>
+ E\\<turnstile>{fd}a..fn:=v::T'"
(* cf. 15.11.1, 15.11.2, 15.11.3 *)
- Call "[|E\\<turnstile>a::Class C;
- E\\<turnstile>ps[::]pTs;
- max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}|] ==>
- E\\<turnstile>a..mn({pTs'}ps)::rT"
+ Call "[| E\\<turnstile>a::Class C;
+ E\\<turnstile>ps[::]pTs;
+ max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
+ E\\<turnstile>a..mn({pTs'}ps)::rT"
(* well-typed expression lists *)
(* cf. 15.11.??? *)
- Nil "E\\<turnstile>[][::][]"
+ Nil "E\\<turnstile>[][::][]"
(* cf. 15.11.??? *)
- Cons "[|E\\<turnstile>e::T;
- E\\<turnstile>es[::]Ts|] ==>
- E\\<turnstile>e#es[::]T#Ts"
+ Cons "[| E\\<turnstile>e::T;
+ E\\<turnstile>es[::]Ts |] ==>
+ E\\<turnstile>e#es[::]T#Ts"
(* well-typed statements *)
- Skip "E\\<turnstile>Skip\\<surd>"
+ Skip "E\\<turnstile>Skip\\<surd>"
- Expr "[|E\\<turnstile>e::T|] ==>
- E\\<turnstile>Expr e\\<surd>"
+ Expr "[| E\\<turnstile>e::T |] ==>
+ E\\<turnstile>Expr e\\<surd>"
- Comp "[|E\\<turnstile>s1\\<surd>;
- E\\<turnstile>s2\\<surd>|] ==>
- E\\<turnstile>s1;; s2\\<surd>"
+ Comp "[| E\\<turnstile>s1\\<surd>;
+ E\\<turnstile>s2\\<surd> |] ==>
+ E\\<turnstile>s1;; s2\\<surd>"
(* cf. 14.8 *)
- Cond "[|E\\<turnstile>e::PrimT Boolean;
- E\\<turnstile>s1\\<surd>;
- E\\<turnstile>s2\\<surd>|] ==>
- E\\<turnstile>If(e) s1 Else s2\\<surd>"
+ Cond "[| E\\<turnstile>e::PrimT Boolean;
+ E\\<turnstile>s1\\<surd>;
+ E\\<turnstile>s2\\<surd> |] ==>
+ E\\<turnstile>If(e) s1 Else s2\\<surd>"
(* cf. 14.10 *)
- Loop "[|E\\<turnstile>e::PrimT Boolean;
- E\\<turnstile>s\\<surd>|] ==>
- E\\<turnstile>While(e) s\\<surd>"
+ Loop "[| E\\<turnstile>e::PrimT Boolean;
+ E\\<turnstile>s\\<surd> |] ==>
+ E\\<turnstile>While(e) s\\<surd>"
constdefs