# HG changeset patch # User berghofe # Date 1165849574 -3600 # Node ID 89275a3ed7bea6cfbb291179624bbe1e3be0129f # Parent 720b0add52067e67f4a1767da6c2d64adae519e3 Adapted to new inductive definition package. diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/AxSem.thy Mon Dec 11 16:06:14 2006 +0100 @@ -435,7 +435,6 @@ ( "_\_:_" [61,0, 58] 57) ax_valids :: "prog \ 'b triples \ 'a triples \ bool" ("_,_|\_" [61,58,58] 57) - ax_derivs :: "prog \ ('a triples \ 'a triples) set" syntax @@ -443,10 +442,6 @@ ( "_||=_:_" [61,0, 58] 57) ax_valid :: "prog \ 'b triples \ 'a triple \ bool" ( "_,_|=_" [61,58,58] 57) - ax_Derivs:: "prog \ 'b triples \ 'a triples \ bool" - ("_,_||-_" [61,58,58] 57) - ax_Deriv :: "prog \ 'b triples \ 'a triple \ bool" - ( "_,_|-_" [61,58,58] 57) syntax (xsymbols) @@ -454,10 +449,6 @@ ( "_|\_:_" [61,0, 58] 57) ax_valid :: "prog \ 'b triples \ 'a triple \ bool" ( "_,_\_" [61,58,58] 57) - ax_Derivs:: "prog \ 'b triples \ 'a triples \ bool" - ("_,_|\_" [61,58,58] 57) - ax_Deriv :: "prog \ 'b triples \ 'a triple \ bool" - ( "_,_\_" [61,58,58] 57) defs triple_valid_def: "G\n:t \ case t of {P} t\ {Q} \ \Y s Z. P Y s Z \ type_ok G t s \ @@ -465,8 +456,6 @@ translations "G|\n:ts" == "Ball ts (triple_valid G n)" defs ax_valids_def:"G,A|\ts \ \n. G|\n:A \ G|\n:ts" translations "G,A \t" == "G,A|\{t}" - "G,A|\ts" == "(A,ts) \ ax_derivs G" - "G,A \t" == "G,A|\{t}" lemma triple_valid_def2: "G\n:{P} t\ {Q} = (\Y s Z. P Y s Z @@ -487,63 +476,69 @@ change_claset (fn cs => cs delSWrapper "split_all_tac"); *} -inductive "ax_derivs G" intros +inductive2 + ax_derivs :: "prog \ 'a triples \ 'a triples \ bool" ("_,_|\_" [61,58,58] 57) + and ax_deriv :: "prog \ 'a triples \ 'a triple \ bool" ("_,_\_" [61,58,58] 57) + for G :: prog +where - empty: " G,A|\{}" - insert:"\G,A\t; G,A|\ts\ \ + "G,A \t \ G,A|\{t}" + +| empty: " G,A|\{}" +| insert:"\G,A\t; G,A|\ts\ \ G,A|\insert t ts" - asm: "ts\A \ G,A|\ts" +| asm: "ts\A \ G,A|\ts" (* could be added for convenience and efficiency, but is not necessary cut: "\G,A'|\ts; G,A|\A'\ \ G,A |\ts" *) - weaken:"\G,A|\ts'; ts \ ts'\ \ G,A|\ts" +| weaken:"\G,A|\ts'; ts \ ts'\ \ G,A|\ts" - conseq:"\Y s Z . P Y s Z \ (\P' Q'. G,A\{P'} t\ {Q'} \ (\Y' s'. +| conseq:"\Y s Z . P Y s Z \ (\P' Q'. G,A\{P'} t\ {Q'} \ (\Y' s'. (\Y Z'. P' Y s Z' \ Q' Y' s' Z') \ Q Y' s' Z )) \ G,A\{P } t\ {Q }" - hazard:"G,A\{P \. Not \ type_ok G t} t\ {Q}" +| hazard:"G,A\{P \. Not \ type_ok G t} t\ {Q}" - Abrupt: "G,A\{P\(arbitrary3 t) \. Not \ normal} t\ {P}" +| Abrupt: "G,A\{P\(arbitrary3 t) \. Not \ normal} t\ {P}" --{* variables *} - LVar: " G,A\{Normal (\s.. P\Var (lvar vn s))} LVar vn=\ {P}" +| LVar: " G,A\{Normal (\s.. P\Var (lvar vn s))} LVar vn=\ {P}" - FVar: "\G,A\{Normal P} .Init C. {Q}; +| FVar: "\G,A\{Normal P} .Init C. {Q}; G,A\{Q} e-\ {\Val:a:. fvar C stat fn a ..; R}\ \ G,A\{Normal P} {accC,C,stat}e..fn=\ {R}" - AVar: "\G,A\{Normal P} e1-\ {Q}; +| AVar: "\G,A\{Normal P} e1-\ {Q}; \a. G,A\{Q\Val a} e2-\ {\Val:i:. avar G i a ..; R}\ \ G,A\{Normal P} e1.[e2]=\ {R}" --{* expressions *} - NewC: "\G,A\{Normal P} .Init C. {Alloc G (CInst C) Q}\ \ +| NewC: "\G,A\{Normal P} .Init C. {Alloc G (CInst C) Q}\ \ G,A\{Normal P} NewC C-\ {Q}" - NewA: "\G,A\{Normal P} .init_comp_ty T. {Q}; G,A\{Q} e-\ +| NewA: "\G,A\{Normal P} .init_comp_ty T. {Q}; G,A\{Q} e-\ {\Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\ \ G,A\{Normal P} New T[e]-\ {R}" - Cast: "\G,A\{Normal P} e-\ {\Val:v:. \s.. +| Cast: "\G,A\{Normal P} e-\ {\Val:v:. \s.. abupd (raise_if (\G,s\v fits T) ClassCast) .; Q\Val v}\ \ G,A\{Normal P} Cast T e-\ {Q}" - Inst: "\G,A\{Normal P} e-\ {\Val:v:. \s.. +| Inst: "\G,A\{Normal P} e-\ {\Val:v:. \s.. Q\Val (Bool (v\Null \ G,s\v fits RefT T))}\ \ G,A\{Normal P} e InstOf T-\ {Q}" - Lit: "G,A\{Normal (P\Val v)} Lit v-\ {P}" +| Lit: "G,A\{Normal (P\Val v)} Lit v-\ {P}" - UnOp: "\G,A\{Normal P} e-\ {\Val:v:. Q\Val (eval_unop unop v)}\ +| UnOp: "\G,A\{Normal P} e-\ {\Val:v:. Q\Val (eval_unop unop v)}\ \ G,A\{Normal P} UnOp unop e-\ {Q}" - BinOp: +| BinOp: "\G,A\{Normal P} e1-\ {Q}; \v1. G,A\{Q\Val v1} (if need_second_arg binop v1 then (In1l e2) else (In1r Skip))\ @@ -551,20 +546,20 @@ \ G,A\{Normal P} BinOp binop e1 e2-\ {R}" - Super:" G,A\{Normal (\s.. P\Val (val_this s))} Super-\ {P}" +| Super:" G,A\{Normal (\s.. P\Val (val_this s))} Super-\ {P}" - Acc: "\G,A\{Normal P} va=\ {\Var:(v,f):. Q\Val v}\ \ +| Acc: "\G,A\{Normal P} va=\ {\Var:(v,f):. Q\Val v}\ \ G,A\{Normal P} Acc va-\ {Q}" - Ass: "\G,A\{Normal P} va=\ {Q}; +| Ass: "\G,A\{Normal P} va=\ {Q}; \vf. G,A\{Q\Var vf} e-\ {\Val:v:. assign (snd vf) v .; R}\ \ G,A\{Normal P} va:=e-\ {R}" - Cond: "\G,A \{Normal P} e0-\ {P'}; +| Cond: "\G,A \{Normal P} e0-\ {P'}; \b. G,A\{P'\=b} (if b then e1 else e2)-\ {Q}\ \ G,A\{Normal P} e0 ? e1 : e2-\ {Q}" - Call: +| Call: "\G,A\{Normal P} e-\ {Q}; \a. G,A\{Q\Val a} args\\ {R a}; \a vs invC declC l. G,A\{(R a\Vals vs \. (\s. declC=invocation_declclass G mode (store s) a statT \name=mn,parTs=pTs\ \ @@ -575,37 +570,37 @@ Methd declC \name=mn,parTs=pTs\-\ {set_lvars l .; S}\ \ G,A\{Normal P} {accC,statT,mode}e\mn({pTs}args)-\ {S}" - Methd:"\G,A\ {{P} Methd-\ {Q} | ms} |\ {{P} body G-\ {Q} | ms}\ \ +| Methd:"\G,A\ {{P} Methd-\ {Q} | ms} |\ {{P} body G-\ {Q} | ms}\ \ G,A|\{{P} Methd-\ {Q} | ms}" - Body: "\G,A\{Normal P} .Init D. {Q}; +| Body: "\G,A\{Normal P} .Init D. {Q}; G,A\{Q} .c. {\s.. abupd (absorb Ret) .; R\(In1 (the (locals s Result)))}\ \ G,A\{Normal P} Body D c-\ {R}" --{* expression lists *} - Nil: "G,A\{Normal (P\Vals [])} []\\ {P}" +| Nil: "G,A\{Normal (P\Vals [])} []\\ {P}" - Cons: "\G,A\{Normal P} e-\ {Q}; +| Cons: "\G,A\{Normal P} e-\ {Q}; \v. G,A\{Q\Val v} es\\ {\Vals:vs:. R\Vals (v#vs)}\ \ G,A\{Normal P} e#es\\ {R}" --{* statements *} - Skip: "G,A\{Normal (P\\)} .Skip. {P}" +| Skip: "G,A\{Normal (P\\)} .Skip. {P}" - Expr: "\G,A\{Normal P} e-\ {Q\\}\ \ +| Expr: "\G,A\{Normal P} e-\ {Q\\}\ \ G,A\{Normal P} .Expr e. {Q}" - Lab: "\G,A\{Normal P} .c. {abupd (absorb l) .; Q}\ \ +| Lab: "\G,A\{Normal P} .c. {abupd (absorb l) .; Q}\ \ G,A\{Normal P} .l\ c. {Q}" - Comp: "\G,A\{Normal P} .c1. {Q}; +| Comp: "\G,A\{Normal P} .c1. {Q}; G,A\{Q} .c2. {R}\ \ G,A\{Normal P} .c1;;c2. {R}" - If: "\G,A \{Normal P} e-\ {P'}; +| If: "\G,A \{Normal P} e-\ {P'}; \b. G,A\{P'\=b} .(if b then c1 else c2). {Q}\ \ G,A\{Normal P} .If(e) c1 Else c2. {Q}" (* unfolding variant of Loop, not needed here @@ -613,28 +608,28 @@ \b. G,A\{P'\=b} .(if b then c;;While(e) c else Skip).{Q}\ \ G,A\{Normal P} .While(e) c. {Q}" *) - Loop: "\G,A\{P} e-\ {P'}; +| Loop: "\G,A\{P} e-\ {P'}; G,A\{Normal (P'\=True)} .c. {abupd (absorb (Cont l)) .; P}\ \ G,A\{P} .l\ While(e) c. {(P'\=False)\=\}" - Jmp: "G,A\{Normal (abupd (\a. (Some (Jump j))) .; P\\)} .Jmp j. {P}" +| Jmp: "G,A\{Normal (abupd (\a. (Some (Jump j))) .; P\\)} .Jmp j. {P}" - Throw:"\G,A\{Normal P} e-\ {\Val:a:. abupd (throw a) .; Q\\}\ \ +| Throw:"\G,A\{Normal P} e-\ {\Val:a:. abupd (throw a) .; Q\\}\ \ G,A\{Normal P} .Throw e. {Q}" - Try: "\G,A\{Normal P} .c1. {SXAlloc G Q}; +| Try: "\G,A\{Normal P} .c1. {SXAlloc G Q}; G,A\{Q \. (\s. G,s\catch C) ;. new_xcpt_var vn} .c2. {R}; (Q \. (\s. \G,s\catch C)) \ R\ \ G,A\{Normal P} .Try c1 Catch(C vn) c2. {R}" - Fin: "\G,A\{Normal P} .c1. {Q}; +| Fin: "\G,A\{Normal P} .c1. {Q}; \x. G,A\{Q \. (\s. x = fst s) ;. abupd (\x. None)} .c2. {abupd (abrupt_if (x\None) x) .; R}\ \ G,A\{Normal P} .c1 Finally c2. {R}" - Done: "G,A\{Normal (P\\ \. initd C)} .Init C. {P}" +| Done: "G,A\{Normal (P\\ \. initd C)} .Init C. {P}" - Init: "\the (class G C) = c; +| Init: "\the (class G C) = c; G,A\{Normal ((P \. Not \ initd C) ;. supd (init_class_obj G C))} .(if C = Object then Skip else Init (super c)). {Q}; \l. G,A\{Q \. (\s. l = locals (store s)) ;. set_lvars empty} @@ -645,10 +640,10 @@ @{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep semantics. *} - InsInitV: " G,A\{Normal P} InsInitV c v=\ {Q}" - InsInitE: " G,A\{Normal P} InsInitE c e-\ {Q}" - Callee: " G,A\{Normal P} Callee l e-\ {Q}" - FinA: " G,A\{Normal P} .FinA a c. {Q}" +| InsInitV: " G,A\{Normal P} InsInitV c v=\ {Q}" +| InsInitE: " G,A\{Normal P} InsInitE c e-\ {Q}" +| Callee: " G,A\{Normal P} Callee l e-\ {Q}" +| FinA: " G,A\{Normal P} .FinA a c. {Q}" (* axioms *) @@ -1032,7 +1027,7 @@ *} declare ax_Abrupts [intro!] -lemmas ax_Normal_cases = ax_cases [of _ _ normal] +lemmas ax_Normal_cases = ax_cases [of _ _ _ normal] lemma ax_Skip [intro!]: "G,(A::'a triple set)\{P\\} .Skip. {P::'a assn}" apply (rule ax_Normal_cases) diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/AxSound.thy --- a/src/HOL/Bali/AxSound.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/AxSound.thy Mon Dec 11 16:06:14 2006 +0100 @@ -375,18 +375,18 @@ thus ?case by (unfold ax_valids2_def) blast next - case (asm A ts) + case (asm ts A) have "ts \ A" . then show "G,A|\\ts" by (auto simp add: ax_valids2_def triple_valid2_def) next - case (weaken A ts ts') + case (weaken A ts' ts) have "G,A|\\ts'" . moreover have "ts \ ts'" . ultimately show "G,A|\\ts" by (unfold ax_valids2_def triple_valid2_def) blast next - case (conseq A P Q t) + case (conseq P A t Q) have con: "\Y s Z. P Y s Z \ (\P' Q'. (G,A\{P'} t\ {Q'} \ G,A|\\{ {P'} t\ {Q'} }) \ @@ -431,7 +431,7 @@ qed qed next - case (hazard A P Q t) + case (hazard A P t Q) show "G,A|\\{ {P \. Not \ type_ok G t} t\ {Q} }" by (simp add: ax_valids2_def triple_valid2_def2 type_ok_def) fast next @@ -474,7 +474,7 @@ qed qed next - case (FVar A statDeclC P Q R accC e fn stat) + case (FVar A P statDeclC Q e stat fn R accC) have valid_init: "G,A|\\{ {Normal P} .Init statDeclC. {Q} }" . have valid_e: "G,A|\\{ {Q} e-\ {\Val:a:. fvar statDeclC stat fn a ..; R} }" . show "G,A|\\{ {Normal P} {accC,statDeclC,stat}e..fn=\ {R} }" @@ -569,7 +569,7 @@ qed qed next - case (AVar A P Q R e1 e2) + case (AVar A P e1 Q e2 R) have valid_e1: "G,A|\\{ {Normal P} e1-\ {Q} }" . have valid_e2: "\ a. G,A|\\{ {Q\In1 a} e2-\ {\Val:i:. avar G i a ..; R} }" using AVar.hyps by simp @@ -633,7 +633,7 @@ qed qed next - case (NewC A C P Q) + case (NewC A P C Q) have valid_init: "G,A|\\{ {Normal P} .Init C. {Alloc G (CInst C) Q} }". show "G,A|\\{ {Normal P} NewC C-\ {Q} }" proof (rule valid_expr_NormalI) @@ -673,7 +673,7 @@ qed qed next - case (NewA A P Q R T e) + case (NewA A P T Q e R) have valid_init: "G,A|\\{ {Normal P} .init_comp_ty T. {Q} }" . have valid_e: "G,A|\\{ {Q} e-\ {\Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}}" . @@ -746,7 +746,7 @@ qed qed next - case (Cast A P Q T e) + case (Cast A P e T Q) have valid_e: "G,A|\\{ {Normal P} e-\ {\Val:v:. \s.. abupd (raise_if (\ G,s\v fits T) ClassCast) .; Q\In1 v} }" . @@ -786,7 +786,7 @@ qed qed next - case (Inst A P Q T e) + case (Inst A P e Q T) assume valid_e: "G,A|\\{ {Normal P} e-\ {\Val:v:. \s.. Q\In1 (Bool (v \ Null \ G,s\v fits RefT T))} }" show "G,A|\\{ {Normal P} e InstOf T-\ {Q} }" @@ -841,7 +841,7 @@ qed qed next - case (UnOp A P Q e unop) + case (UnOp A P e Q unop) assume valid_e: "G,A|\\{ {Normal P}e-\{\Val:v:. Q\In1 (eval_unop unop v)} }" show "G,A|\\{ {Normal P} UnOp unop e-\ {Q} }" proof (rule valid_expr_NormalI) @@ -878,7 +878,7 @@ qed qed next - case (BinOp A P Q R binop e1 e2) + case (BinOp A P e1 Q binop e2 R) assume valid_e1: "G,A|\\{ {Normal P} e1-\ {Q} }" have valid_e2: "\ v1. G,A|\\{ {Q\In1 v1} (if need_second_arg binop v1 then In1l e2 else In1r Skip)\ @@ -977,7 +977,7 @@ qed qed next - case (Acc A P Q var) + case (Acc A P var Q) have valid_var: "G,A|\\{ {Normal P} var=\ {\Var:(v, f):. Q\In1 v} }" . show "G,A|\\{ {Normal P} Acc var-\ {Q} }" proof (rule valid_expr_NormalI) @@ -1013,7 +1013,7 @@ qed qed next - case (Ass A P Q R e var) + case (Ass A P var Q e R) have valid_var: "G,A|\\{ {Normal P} var=\ {Q} }" . have valid_e: "\ vf. G,A|\\{ {Q\In2 vf} e-\ {\Val:v:. assign (snd vf) v .; R} }" @@ -1125,7 +1125,7 @@ qed qed next - case (Cond A P P' Q e0 e1 e2) + case (Cond A P e0 P' e1 e2 Q) have valid_e0: "G,A|\\{ {Normal P} e0-\ {P'} }" . have valid_then_else:"\ b. G,A|\\{ {P'\=b} (if b then e1 else e2)-\ {Q} }" using Cond.hyps by simp @@ -1215,7 +1215,7 @@ qed qed next - case (Call A P Q R S accC' args e mn mode pTs' statT) + case (Call A P e Q args R mode statT mn pTs' S accC') have valid_e: "G,A|\\{ {Normal P} e-\ {Q} }" . have valid_args: "\ a. G,A|\\{ {Q\In1 a} args\\ {R a} }" using Call.hyps by simp @@ -1604,7 +1604,7 @@ show "G,A|\\{{P} Methd-\ {Q} | ms}" by (rule Methd_sound) next - case (Body A D P Q R c) + case (Body A P D Q c R) have valid_init: "G,A|\\{ {Normal P} .Init D. {Q} }". have valid_c: "G,A|\\{ {Q} .c. {\s.. abupd (absorb Ret) .; R\In1 (the (locals s Result))} }". @@ -1697,7 +1697,7 @@ qed qed next - case (Cons A P Q R e es) + case (Cons A P e Q es R) have valid_e: "G,A|\\{ {Normal P} e-\ {Q} }". have valid_es: "\ v. G,A|\\{ {Q\\v\\<^sub>e} es\\ {\Vals:vs:. R\\(v # vs)\\<^sub>l} }" using Cons.hyps by simp @@ -1779,7 +1779,7 @@ qed qed next - case (Expr A P Q e) + case (Expr A P e Q) have valid_e: "G,A|\\{ {Normal P} e-\ {Q\\} }". show "G,A|\\{ {Normal P} .Expr e. {Q} }" proof (rule valid_stmt_NormalI) @@ -1809,7 +1809,7 @@ qed qed next - case (Lab A P Q c l) + case (Lab A P c l Q) have valid_c: "G,A|\\{ {Normal P} .c. {abupd (absorb l) .; Q} }". show "G,A|\\{ {Normal P} .l\ c. {Q} }" proof (rule valid_stmt_NormalI) @@ -1846,7 +1846,7 @@ qed qed next - case (Comp A P Q R c1 c2) + case (Comp A P c1 Q c2 R) have valid_c1: "G,A|\\{ {Normal P} .c1. {Q} }" . have valid_c2: "G,A|\\{ {Q} .c2. {R} }" . show "G,A|\\{ {Normal P} .c1;; c2. {R} }" @@ -1905,7 +1905,7 @@ qed qed next - case (If A P P' Q c1 c2 e) + case (If A P e P' c1 c2 Q) have valid_e: "G,A|\\{ {Normal P} e-\ {P'} }" . have valid_then_else: "\ b. G,A|\\{ {P'\=b} .(if b then c1 else c2). {Q} }" using If.hyps by simp @@ -1982,7 +1982,7 @@ qed qed next - case (Loop A P P' c e l) + case (Loop A P e P' c l) have valid_e: "G,A|\\{ {P} e-\ {P'} }". have valid_c: "G,A|\\{ {Normal (P'\=True)} .c. @@ -2020,7 +2020,7 @@ \\ (P'\=False\=\) v s' Z" (is "PROP ?Hyp n t s v s'") proof (induct) - case (Loop b c' e' l' n' s0' s1' s2' s3' Y' T E) + case (Loop s0' e' n' b s1' c' s2' l' s3' Y' T E) have while: "(\l'\ While(e') c'\\<^sub>s::term) = \l\ While(e) c\\<^sub>s" . hence eqs: "l'=l" "e'=e" "c'=c" by simp_all have valid_A: "\t\A. G\n'\t". @@ -2173,7 +2173,7 @@ qed qed next - case (Abrupt n' s t' abr Y' T E) + case (Abrupt abr s t' n' Y' T E) have t': "t' = \l\ While(e) c\\<^sub>s". have conf: "(Some abr, s)\\(G, L)". have P: "P Y' (Some abr, s) Z". @@ -2212,7 +2212,7 @@ qed qed next - case (Jmp A P j) + case (Jmp A j P) show "G,A|\\{ {Normal (abupd (\a. Some (Jump j)) .; P\\)} .Jmp j. {P} }" proof (rule valid_stmt_NormalI) fix n s0 L accC C s1 Y Z @@ -2239,7 +2239,7 @@ qed qed next - case (Throw A P Q e) + case (Throw A P e Q) have valid_e: "G,A|\\{ {Normal P} e-\ {\Val:a:. abupd (throw a) .; Q\\} }". show "G,A|\\{ {Normal P} .Throw e. {Q} }" proof (rule valid_stmt_NormalI) @@ -2277,7 +2277,7 @@ qed qed next - case (Try A C P Q R c1 c2 vn) + case (Try A P c1 Q C vn c2 R) have valid_c1: "G,A|\\{ {Normal P} .c1. {SXAlloc G Q} }". have valid_c2: "G,A|\\{ {Q \. (\s. G,s\catch C) ;. new_xcpt_var vn} .c2. @@ -2409,7 +2409,7 @@ qed qed next - case (Fin A P Q R c1 c2) + case (Fin A P c1 Q c2 R) have valid_c1: "G,A|\\{ {Normal P} .c1. {Q} }". have valid_c2: "\ abr. G,A|\\{ {Q \. (\s. abr = fst s) ;. abupd (\x. None)} .c2. @@ -2483,7 +2483,7 @@ qed qed next - case (Done A C P) + case (Done A P C) show "G,A|\\{ {Normal (P\\ \. initd C)} .Init C. {P} }" proof (rule valid_stmt_NormalI) fix n s0 L accC E s3 Y Z @@ -2506,7 +2506,7 @@ qed qed next - case (Init A C P Q R c) + case (Init C c A P Q R) have c: "the (class G C) = c". have valid_super: "G,A|\\{ {Normal (P \. Not \ initd C ;. supd (init_class_obj G C))} @@ -2618,7 +2618,7 @@ qed qed next - case (InsInitV A P Q c v) + case (InsInitV A P c v Q) show "G,A|\\{ {Normal P} InsInitV c v=\ {Q} }" proof (rule valid_var_NormalI) fix s0 vf n s1 L Z @@ -2630,7 +2630,7 @@ thus "Q \vf\\<^sub>v s1 Z \ s1\\(G, L)".. qed next - case (InsInitE A P Q c e) + case (InsInitE A P c e Q) show "G,A|\\{ {Normal P} InsInitE c e-\ {Q} }" proof (rule valid_expr_NormalI) fix s0 v n s1 L Z @@ -2642,7 +2642,7 @@ thus "Q \v\\<^sub>e s1 Z \ s1\\(G, L)".. qed next - case (Callee A P Q e l) + case (Callee A P l e Q) show "G,A|\\{ {Normal P} Callee l e-\ {Q} }" proof (rule valid_expr_NormalI) fix s0 v n s1 L Z @@ -2654,7 +2654,7 @@ thus "Q \v\\<^sub>e s1 Z \ s1\\(G, L)".. qed next - case (FinA A P Q a c) + case (FinA A P a c Q) show "G,A|\\{ {Normal P} .FinA a c. {Q} }" proof (rule valid_stmt_NormalI) fix s0 v n s1 L Z diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/DeclConcepts.thy Mon Dec 11 16:06:14 2006 +0100 @@ -536,26 +536,21 @@ subsubsection "members" -consts -members:: "prog \ (qtname \ (qtname \ memberdecl)) set" (* Can't just take a function: prog \ qtname \ memberdecl set because the class qtname changes to the superclass in the inductive definition below *) -syntax -member_of:: "prog \ (qtname \ memberdecl) \ qtname \ bool" - ("_ \ _ member'_of _" [61,61,61] 60) - -translations - "G\m member_of C" \ "(C,m) \ members G" +inductive2 + members :: "prog \ (qtname \ memberdecl) \ qtname \ bool" + ("_ \ _ member'_of _" [61,61,61] 60) + for G :: prog +where -inductive "members G" intros - -Immediate: "\G\mbr m declared_in C;declclass m = C\ \ G\m member_of C" -Inherited: "\G\m inheritable_in (pid C); G\memberid m undeclared_in C; - G\C \\<^sub>C\<^sub>1 S; G\(Class S) accessible_in (pid C);G\m member_of S - \ \ G\m member_of C" + Immediate: "\G\mbr m declared_in C;declclass m = C\ \ G\m member_of C" +| Inherited: "\G\m inheritable_in (pid C); G\memberid m undeclared_in C; + G\C \\<^sub>C\<^sub>1 S; G\(Class S) accessible_in (pid C);G\m member_of S + \ \ G\m member_of C" text {* Note that in the case of an inherited member only the members of the direct superclass are concerned. If a member of a superclass of the direct superclass isn't inherited in the direct superclass (not member of the @@ -619,9 +614,6 @@ translations "G\Methd s m member_in C" \ "G\(method s m) member_in C" -consts stat_overridesR:: - "prog \ ((qtname \ mdecl) \ (qtname \ mdecl)) set" - lemma member_inD: "G\m member_in C \ \ provC. G\ C \\<^sub>C provC \ G \ m member_of provC" by (auto simp add: member_in_def) @@ -641,48 +633,43 @@ *} text {* Static overriding (used during the typecheck of the compiler) *} -syntax -stat_overrides:: "prog \ (qtname \ mdecl) \ (qtname \ mdecl) \ bool" - ("_ \ _ overrides\<^sub>S _" [61,61,61] 60) -translations - "G\new overrides\<^sub>S old" == "(new,old) \ stat_overridesR G " -inductive "stat_overridesR G" intros +inductive2 + stat_overridesR :: "prog \ (qtname \ mdecl) \ (qtname \ mdecl) \ bool" + ("_ \ _ overrides\<^sub>S _" [61,61,61] 60) + for G :: prog +where -Direct: "\\ is_static new; msig new = msig old; - G\Method new declared_in (declclass new); - G\Method old declared_in (declclass old); - G\Method old inheritable_in pid (declclass new); - G\(declclass new) \\<^sub>C\<^sub>1 superNew; - G \Method old member_of superNew - \ \ G\new overrides\<^sub>S old" + Direct: "\\ is_static new; msig new = msig old; + G\Method new declared_in (declclass new); + G\Method old declared_in (declclass old); + G\Method old inheritable_in pid (declclass new); + G\(declclass new) \\<^sub>C\<^sub>1 superNew; + G \Method old member_of superNew + \ \ G\new overrides\<^sub>S old" -Indirect: "\G\new overrides\<^sub>S inter; G\inter overrides\<^sub>S old\ - \ G\new overrides\<^sub>S old" +| Indirect: "\G\new overrides\<^sub>S inter; G\inter overrides\<^sub>S old\ + \ G\new overrides\<^sub>S old" text {* Dynamic overriding (used during the typecheck of the compiler) *} -consts overridesR:: - "prog \ ((qtname \ mdecl) \ (qtname \ mdecl)) set" - -overrides:: "prog \ (qtname \ mdecl) \ (qtname \ mdecl) \ bool" - ("_ \ _ overrides _" [61,61,61] 60) -translations - "G\new overrides old" == "(new,old) \ overridesR G " - -inductive "overridesR G" intros +inductive2 + overridesR :: "prog \ (qtname \ mdecl) \ (qtname \ mdecl) \ bool" + ("_ \ _ overrides _" [61,61,61] 60) + for G :: prog +where -Direct: "\\ is_static new; \ is_static old; accmodi new \ Private; - msig new = msig old; - G\(declclass new) \\<^sub>C (declclass old); - G\Method new declared_in (declclass new); - G\Method old declared_in (declclass old); - G\Method old inheritable_in pid (declclass new); - G\resTy new \ resTy old - \ \ G\new overrides old" + Direct: "\\ is_static new; \ is_static old; accmodi new \ Private; + msig new = msig old; + G\(declclass new) \\<^sub>C (declclass old); + G\Method new declared_in (declclass new); + G\Method old declared_in (declclass old); + G\Method old inheritable_in pid (declclass new); + G\resTy new \ resTy old + \ \ G\new overrides old" -Indirect: "\G\new overrides inter; G\inter overrides old\ - \ G\new overrides old" +| Indirect: "\G\new overrides inter; G\inter overrides old\ + \ G\new overrides old" syntax sig_stat_overrides:: @@ -797,28 +784,31 @@ \end{itemize} *} - -consts -accessible_fromR:: - "prog \ qtname \ ((qtname \ memberdecl) \ qtname) set" +inductive2 + accessible_fromR :: "prog \ qtname \ (qtname \ memberdecl) \ qtname \ bool" + and accessible_from :: "prog \ (qtname \ memberdecl) \ qtname \ qtname \ bool" + ("_ \ _ of _ accessible'_from _" [61,61,61,61] 60) + and method_accessible_from :: "prog \ (qtname \ mdecl) \ qtname \ qtname \ bool" + ("_ \Method _ of _ accessible'_from _" [61,61,61,61] 60) + for G :: prog and accclass :: qtname +where + "G\membr of cls accessible_from accclass \ accessible_fromR G accclass membr cls" -syntax -accessible_from:: - "prog \ (qtname \ memberdecl) \ qtname \ qtname \ bool" - ("_ \ _ of _ accessible'_from _" [61,61,61,61] 60) +| "G\Method m of cls accessible_from accclass \ + G\methdMembr m of cls accessible_from accclass" -translations -"G\membr of cls accessible_from accclass" - \ "(membr,cls) \ accessible_fromR G accclass" +| Immediate: "\G\membr member_of class; + G\(Class class) accessible_in (pid accclass); + G\membr in class permits_acc_from accclass + \ \ G\membr of class accessible_from accclass" -syntax -method_accessible_from:: - "prog \ (qtname \ mdecl) \ qtname \ qtname \ bool" - ("_ \Method _ of _ accessible'_from _" [61,61,61,61] 60) - -translations -"G\Method m of cls accessible_from accclass" - \ "G\methdMembr m of cls accessible_from accclass" +| Overriding: "\G\membr member_of class; + G\(Class class) accessible_in (pid accclass); + membr=(C,mdecl new); + G\(C,new) overrides\<^sub>S old; + G\class \\<^sub>C sup; + G\Method old of sup accessible_from accclass + \\ G\membr of class accessible_from accclass" syntax methd_accessible_from:: @@ -838,41 +828,29 @@ "G\Field fn f of C accessible_from accclass" \ "G\(fieldm fn f) of C accessible_from accclass" -inductive "accessible_fromR G accclass" intros -Immediate: "\G\membr member_of class; - G\(Class class) accessible_in (pid accclass); - G\membr in class permits_acc_from accclass - \ \ G\membr of class accessible_from accclass" - -Overriding: "\G\membr member_of class; - G\(Class class) accessible_in (pid accclass); - membr=(C,mdecl new); - G\(C,new) overrides\<^sub>S old; - G\class \\<^sub>C sup; - G\Method old of sup accessible_from accclass - \\ G\membr of class accessible_from accclass" - -consts -dyn_accessible_fromR:: - "prog \ qtname \ ((qtname \ memberdecl) \ qtname) set" +inductive2 + dyn_accessible_fromR :: "prog \ qtname \ (qtname \ memberdecl) \ qtname \ bool" + and dyn_accessible_from' :: "prog \ (qtname \ memberdecl) \ qtname \ qtname \ bool" + ("_ \ _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) + and method_dyn_accessible_from :: "prog \ (qtname \ mdecl) \ qtname \ qtname \ bool" + ("_ \Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) + for G :: prog and accclass :: qtname +where + "G\membr in C dyn_accessible_from accC \ dyn_accessible_fromR G accC membr C" -syntax -dyn_accessible_from:: - "prog \ (qtname \ memberdecl) \ qtname \ qtname \ bool" - ("_ \ _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) +| "G\Method m in C dyn_accessible_from accC \ + G\methdMembr m in C dyn_accessible_from accC" -translations -"G\membr in C dyn_accessible_from accC" - \ "(membr,C) \ dyn_accessible_fromR G accC" +| Immediate: "\G\membr member_in class; + G\membr in class permits_acc_from accclass + \ \ G\membr in class dyn_accessible_from accclass" -syntax -method_dyn_accessible_from:: - "prog \ (qtname \ mdecl) \ qtname \ qtname \ bool" - ("_ \Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) - -translations -"G\Method m in C dyn_accessible_from accC" - \ "G\methdMembr m in C dyn_accessible_from accC" +| Overriding: "\G\membr member_in class; + membr=(C,mdecl new); + G\(C,new) overrides old; + G\class \\<^sub>C sup; + G\Method old in sup dyn_accessible_from accclass + \\ G\membr in class dyn_accessible_from accclass" syntax methd_dyn_accessible_from:: @@ -891,18 +869,6 @@ translations "G\Field fn f in dynC dyn_accessible_from accC" \ "G\(fieldm fn f) in dynC dyn_accessible_from accC" - -inductive "dyn_accessible_fromR G accclass" intros -Immediate: "\G\membr member_in class; - G\membr in class permits_acc_from accclass - \ \ G\membr in class dyn_accessible_from accclass" - -Overriding: "\G\membr member_in class; - membr=(C,mdecl new); - G\(C,new) overrides old; - G\class \\<^sub>C sup; - G\Method old in sup dyn_accessible_from accclass - \\ G\membr in class dyn_accessible_from accclass" lemma accessible_from_commonD: "G\m of C accessible_from S @@ -967,13 +933,13 @@ from n m eqid show "n=m" proof (induct) - case (Immediate C n) + case (Immediate n C) assume member_n: "G\ mbr n declared_in C" "declclass n = C" assume eqid: "memberid n = memberid m" assume "G \ m member_of C" then show "n=m" proof (cases) - case (Immediate _ m') + case (Immediate m' _) with eqid have "m=m'" "memberid n = memberid m" @@ -987,7 +953,7 @@ cdeclaredmethd_def cdeclaredfield_def split: memberdecl.splits) next - case (Inherited _ _ m') + case (Inherited m' _ _) then have "G\ memberid m undeclared_in C" by simp with eqid member_n @@ -995,7 +961,7 @@ by (cases n) (auto dest: declared_not_undeclared) qed next - case (Inherited C S n) + case (Inherited n C S) assume undecl: "G\ memberid n undeclared_in C" assume super: "G\C\\<^sub>C\<^sub>1S" assume hyp: "\G \ m member_of S; memberid n = memberid m\ \ n = m" @@ -1021,13 +987,13 @@ lemma member_of_is_classD: "G\m member_of C \ is_class G C" proof (induct set: members) - case (Immediate C m) + case (Immediate m C) assume "G\ mbr m declared_in C" then show "is_class G C" by (cases "mbr m") (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def) next - case (Inherited C S m) + case (Inherited m C S) assume "G\C\\<^sub>C\<^sub>1S" and "is_class G S" then show "is_class G C" by - (rule subcls_is_class2,auto) @@ -1046,10 +1012,10 @@ lemma member_of_class_relation: "G\m member_of C \ G\C \\<^sub>C declclass m" proof (induct set: members) - case (Immediate C m) + case (Immediate m C) then show "G\C \\<^sub>C declclass m" by simp next - case (Inherited C S m) + case (Inherited m C S) then show "G\C \\<^sub>C declclass m" by (auto dest: r_into_rtrancl intro: rtrancl_trans) qed @@ -1152,12 +1118,12 @@ from acc_C static show "G\m in (declclass m) dyn_accessible_from accC" proof (induct) - case (Immediate C m) + case (Immediate m C) then show ?case by (auto intro!: dyn_accessible_fromR.Immediate dest: member_in_declC permits_acc_static_declC) next - case (Overriding declCNew C m new old sup) + case (Overriding m C declCNew new old sup) then have "\ is_static m" by (auto dest: overrides_commonD) moreover @@ -1259,7 +1225,7 @@ from m subclseq_D_C subclseq_C_m show ?thesis proof (induct) - case (Immediate D m) + case (Immediate m D) assume "declclass m = D" and "G\D\\<^sub>C C" and "G\C\\<^sub>C declclass m" with ws have "D=C" @@ -1268,7 +1234,7 @@ show "G\m member_of C" by (auto intro: members.Immediate) next - case (Inherited D S m) + case (Inherited m D S) assume member_of_D_props: "G \ m inheritable_in pid D" "G\ memberid m undeclared_in D" @@ -1714,7 +1680,7 @@ from member_of show "?Methd C" proof (cases) - case (Immediate Ca membr) + case (Immediate membr Ca) then have "Ca=C" "membr = method sig m" and "G\Methd sig m declared_in C" "declclass m = C" by (cases m,auto) @@ -1727,7 +1693,7 @@ show ?thesis by (simp add: methd_rec) next - case (Inherited Ca S membr) + case (Inherited membr Ca S) with clsC have eq_Ca_C: "Ca=C" and undecl: "G\mid sig undeclared_in C" and diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/DefiniteAssignment.thy --- a/src/HOL/Bali/DefiniteAssignment.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/DefiniteAssignment.thy Mon Dec 11 16:06:14 2006 +0100 @@ -513,25 +513,6 @@ brk :: "breakass" --{* Definetly assigned variables for abrupt completion with a break *} -consts da :: "(env \ lname set \ term \ assigned) set" -text {* The environment @{term env} is only needed for the - conditional @{text "_ ? _ : _"}. - The definite assignment rules refer to the typing rules here to - distinguish boolean and other expressions. - *} - -syntax -da :: "env \ lname set \ term \ assigned \ bool" - ("_\ _ \_\ _" [65,65,65,65] 71) - -translations - "E\ B \t\ A" == "(E,B,t,A) \ da" - -text {* @{text B}: the ''assigned'' variables before evaluating term @{text t}; - @{text A}: the ''assigned'' variables after evaluating term @{text t} -*} - - constdefs rmlab :: "'a \ ('a,'b) tables \ ('a,'b) tables" "rmlab k A \ \ x. if x=k then UNIV else A x" @@ -543,35 +524,45 @@ constdefs range_inter_ts :: "('a,'b) tables \ 'b set" ("\\_" 80) "\\A \ {x |x. \ k. x \ A k}" -inductive "da" intros - - Skip: "Env\ B \\Skip\\ \nrm=B,brk=\ l. UNIV\" +text {* +In @{text "E\ B \t\ A"}, +@{text B} denotes the ''assigned'' variables before evaluating term @{text t}, +whereas @{text A} denotes the ''assigned'' variables after evaluating term @{text t}. +The environment @{term E} is only needed for the conditional @{text "_ ? _ : _"}. +The definite assignment rules refer to the typing rules here to +distinguish boolean and other expressions. +*} - Expr: "Env\ B \\e\\ A - \ - Env\ B \\Expr e\\ A" - Lab: "\Env\ B \\c\\ C; nrm A = nrm C \ (brk C) l; brk A = rmlab l (brk C)\ - \ - Env\ B \\Break l\ c\\ A" +inductive2 + da :: "env \ lname set \ term \ assigned \ bool" ("_\ _ \_\ _" [65,65,65,65] 71) +where + Skip: "Env\ B \\Skip\\ \nrm=B,brk=\ l. UNIV\" - Comp: "\Env\ B \\c1\\ C1; Env\ nrm C1 \\c2\\ C2; - nrm A = nrm C2; brk A = (brk C1) \\ (brk C2)\ - \ - Env\ B \\c1;; c2\\ A" +| Expr: "Env\ B \\e\\ A + \ + Env\ B \\Expr e\\ A" +| Lab: "\Env\ B \\c\\ C; nrm A = nrm C \ (brk C) l; brk A = rmlab l (brk C)\ + \ + Env\ B \\Break l\ c\\ A" - If: "\Env\ B \\e\\ E; - Env\ (B \ assigns_if True e) \\c1\\ C1; - Env\ (B \ assigns_if False e) \\c2\\ C2; - nrm A = nrm C1 \ nrm C2; - brk A = brk C1 \\ brk C2 \ - \ - Env\ B \\If(e) c1 Else c2\\ A" +| Comp: "\Env\ B \\c1\\ C1; Env\ nrm C1 \\c2\\ C2; + nrm A = nrm C2; brk A = (brk C1) \\ (brk C2)\ + \ + Env\ B \\c1;; c2\\ A" + +| If: "\Env\ B \\e\\ E; + Env\ (B \ assigns_if True e) \\c1\\ C1; + Env\ (B \ assigns_if False e) \\c2\\ C2; + nrm A = nrm C1 \ nrm C2; + brk A = brk C1 \\ brk C2 \ + \ + Env\ B \\If(e) c1 Else c2\\ A" --{* Note that @{term E} is not further used, because we take the specialized sets that also consider if the expression evaluates to true or false. Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break map of @{term E} will be the trivial one. So - @{term "Env\B \\e\\ E"} is just used to enshure the definite assignment in + @{term "Env\B \\e\\ E"} is just used to ensure the definite assignment in expression @{term e}. Notice the implicit analysis of a constant boolean expression @{term e} in this rule. For example, if @{term e} is constantly @{term True} then @@ -585,12 +576,12 @@ contribution. *} - Loop: "\Env\ B \\e\\ E; - Env\ (B \ assigns_if True e) \\c\\ C; - nrm A = nrm C \ (B \ assigns_if False e); - brk A = brk C\ - \ - Env\ B \\l\ While(e) c\\ A" +| Loop: "\Env\ B \\e\\ E; + Env\ (B \ assigns_if True e) \\c\\ C; + nrm A = nrm C \ (B \ assigns_if False e); + brk A = brk C\ + \ + Env\ B \\l\ While(e) c\\ A" --{* The @{text Loop} rule resembles some of the ideas of the @{text If} rule. For the @{term "nrm A"} the set @{term "B \ assigns_if False e"} will be @{term UNIV} if the condition is constantly true. To normally exit @@ -602,14 +593,14 @@ handle the breaks specially. *} - Jmp: "\jump=Ret \ Result \ B; - nrm A = UNIV; - brk A = (case jump of - Break l \ \ k. if k=l then B else UNIV - | Cont l \ \ k. UNIV - | Ret \ \ k. UNIV)\ - \ - Env\ B \\Jmp jump\\ A" +| Jmp: "\jump=Ret \ Result \ B; + nrm A = UNIV; + brk A = (case jump of + Break l \ \ k. if k=l then B else UNIV + | Cont l \ \ k. UNIV + | Ret \ \ k. UNIV)\ + \ + Env\ B \\Jmp jump\\ A" --{* In case of a break to label @{term l} the corresponding break set is all variables assigned before the break. The assigned variables for normal completion of the @{term Jmp} is @{term UNIV}, because the statement will @@ -618,21 +609,21 @@ assigned. *} - Throw: "\Env\ B \\e\\ E; nrm A = UNIV; brk A = (\ l. UNIV)\ - \ Env\ B \\Throw e\\ A" +| Throw: "\Env\ B \\e\\ E; nrm A = UNIV; brk A = (\ l. UNIV)\ + \ Env\ B \\Throw e\\ A" - Try: "\Env\ B \\c1\\ C1; - Env\lcl := lcl Env(VName vn\Class C)\\ (B \ {VName vn}) \\c2\\ C2; - nrm A = nrm C1 \ nrm C2; - brk A = brk C1 \\ brk C2\ - \ Env\ B \\Try c1 Catch(C vn) c2\\ A" +| Try: "\Env\ B \\c1\\ C1; + Env\lcl := lcl Env(VName vn\Class C)\\ (B \ {VName vn}) \\c2\\ C2; + nrm A = nrm C1 \ nrm C2; + brk A = brk C1 \\ brk C2\ + \ Env\ B \\Try c1 Catch(C vn) c2\\ A" - Fin: "\Env\ B \\c1\\ C1; - Env\ B \\c2\\ C2; - nrm A = nrm C1 \ nrm C2; - brk A = ((brk C1) \\\<^sub>\ (nrm C2)) \\ (brk C2)\ - \ - Env\ B \\c1 Finally c2\\ A" +| Fin: "\Env\ B \\c1\\ C1; + Env\ B \\c2\\ C2; + nrm A = nrm C1 \ nrm C2; + brk A = ((brk C1) \\\<^sub>\ (nrm C2)) \\ (brk C2)\ + \ + Env\ B \\c1 Finally c2\\ A" --{* The set of assigned variables before execution @{term c2} are the same as before execution @{term c1}, because @{term c1} could throw an exception and so we can't guarantee that any variable will be assigned in @{term c1}. @@ -671,7 +662,7 @@ and @{text NewA} *} - Init: "Env\ B \\Init C\\ \nrm=B,brk=\ l. UNIV\" +| Init: "Env\ B \\Init C\\ \nrm=B,brk=\ l. UNIV\" --{* Wellformedness of a program will ensure, that every static initialiser is definetly assigned and the jumps are nested correctly. The case here for @{term Init} is just for convenience, to get a proper precondition @@ -679,91 +670,91 @@ expand the initialisation on every point where it is triggerred by the evaluation rules. *} - NewC: "Env\ B \\NewC C\\ \nrm=B,brk=\ l. UNIV\" +| NewC: "Env\ B \\NewC C\\ \nrm=B,brk=\ l. UNIV\" + +| NewA: "Env\ B \\e\\ A + \ + Env\ B \\New T[e]\\ A" - NewA: "Env\ B \\e\\ A - \ - Env\ B \\New T[e]\\ A" +| Cast: "Env\ B \\e\\ A + \ + Env\ B \\Cast T e\\ A" - Cast: "Env\ B \\e\\ A - \ - Env\ B \\Cast T e\\ A" +| Inst: "Env\ B \\e\\ A + \ + Env\ B \\e InstOf T\\ A" - Inst: "Env\ B \\e\\ A - \ - Env\ B \\e InstOf T\\ A" +| Lit: "Env\ B \\Lit v\\ \nrm=B,brk=\ l. UNIV\" - Lit: "Env\ B \\Lit v\\ \nrm=B,brk=\ l. UNIV\" +| UnOp: "Env\ B \\e\\ A + \ + Env\ B \\UnOp unop e\\ A" - UnOp: "Env\ B \\e\\ A - \ - Env\ B \\UnOp unop e\\ A" +| CondAnd: "\Env\ B \\e1\\ E1; Env\ (B \ assigns_if True e1) \\e2\\ E2; + nrm A = B \ (assigns_if True (BinOp CondAnd e1 e2) \ + assigns_if False (BinOp CondAnd e1 e2)); + brk A = (\ l. UNIV) \ + \ + Env\ B \\BinOp CondAnd e1 e2\\ A" - CondAnd: "\Env\ B \\e1\\ E1; Env\ (B \ assigns_if True e1) \\e2\\ E2; - nrm A = B \ (assigns_if True (BinOp CondAnd e1 e2) \ - assigns_if False (BinOp CondAnd e1 e2)); +| CondOr: "\Env\ B \\e1\\ E1; Env\ (B \ assigns_if False e1) \\e2\\ E2; + nrm A = B \ (assigns_if True (BinOp CondOr e1 e2) \ + assigns_if False (BinOp CondOr e1 e2)); brk A = (\ l. UNIV) \ - \ - Env\ B \\BinOp CondAnd e1 e2\\ A" + \ + Env\ B \\BinOp CondOr e1 e2\\ A" - CondOr: "\Env\ B \\e1\\ E1; Env\ (B \ assigns_if False e1) \\e2\\ E2; - nrm A = B \ (assigns_if True (BinOp CondOr e1 e2) \ - assigns_if False (BinOp CondOr e1 e2)); - brk A = (\ l. UNIV) \ - \ - Env\ B \\BinOp CondOr e1 e2\\ A" +| BinOp: "\Env\ B \\e1\\ E1; Env\ nrm E1 \\e2\\ A; + binop \ CondAnd; binop \ CondOr\ + \ + Env\ B \\BinOp binop e1 e2\\ A" - BinOp: "\Env\ B \\e1\\ E1; Env\ nrm E1 \\e2\\ A; - binop \ CondAnd; binop \ CondOr\ - \ - Env\ B \\BinOp binop e1 e2\\ A" +| Super: "This \ B + \ + Env\ B \\Super\\ \nrm=B,brk=\ l. UNIV\" - Super: "This \ B - \ - Env\ B \\Super\\ \nrm=B,brk=\ l. UNIV\" - - AccLVar: "\vn \ B; - nrm A = B; brk A = (\ k. UNIV)\ - \ - Env\ B \\Acc (LVar vn)\\ A" +| AccLVar: "\vn \ B; + nrm A = B; brk A = (\ k. UNIV)\ + \ + Env\ B \\Acc (LVar vn)\\ A" --{* To properly access a local variable we have to test the definite assignment here. The variable must occur in the set @{term B} *} - Acc: "\\ vn. v \ LVar vn; - Env\ B \\v\\ A\ - \ - Env\ B \\Acc v\\ A" +| Acc: "\\ vn. v \ LVar vn; + Env\ B \\v\\ A\ + \ + Env\ B \\Acc v\\ A" - AssLVar: "\Env\ B \\e\\ E; nrm A = nrm E \ {vn}; brk A = brk E\ - \ - Env\ B \\(LVar vn) := e\\ A" +| AssLVar: "\Env\ B \\e\\ E; nrm A = nrm E \ {vn}; brk A = brk E\ + \ + Env\ B \\(LVar vn) := e\\ A" - Ass: "\\ vn. v \ LVar vn; Env\ B \\v\\ V; Env\ nrm V \\e\\ A\ - \ - Env\ B \\v := e\\ A" +| Ass: "\\ vn. v \ LVar vn; Env\ B \\v\\ V; Env\ nrm V \\e\\ A\ + \ + Env\ B \\v := e\\ A" - CondBool: "\Env\(c ? e1 : e2)\-(PrimT Boolean); - Env\ B \\c\\ C; - Env\ (B \ assigns_if True c) \\e1\\ E1; - Env\ (B \ assigns_if False c) \\e2\\ E2; - nrm A = B \ (assigns_if True (c ? e1 : e2) \ - assigns_if False (c ? e1 : e2)); - brk A = (\ l. UNIV)\ - \ - Env\ B \\c ? e1 : e2\\ A" +| CondBool: "\Env\(c ? e1 : e2)\-(PrimT Boolean); + Env\ B \\c\\ C; + Env\ (B \ assigns_if True c) \\e1\\ E1; + Env\ (B \ assigns_if False c) \\e2\\ E2; + nrm A = B \ (assigns_if True (c ? e1 : e2) \ + assigns_if False (c ? e1 : e2)); + brk A = (\ l. UNIV)\ + \ + Env\ B \\c ? e1 : e2\\ A" - Cond: "\\ Env\(c ? e1 : e2)\-(PrimT Boolean); - Env\ B \\c\\ C; - Env\ (B \ assigns_if True c) \\e1\\ E1; - Env\ (B \ assigns_if False c) \\e2\\ E2; - nrm A = nrm E1 \ nrm E2; brk A = (\ l. UNIV)\ - \ - Env\ B \\c ? e1 : e2\\ A" +| Cond: "\\ Env\(c ? e1 : e2)\-(PrimT Boolean); + Env\ B \\c\\ C; + Env\ (B \ assigns_if True c) \\e1\\ E1; + Env\ (B \ assigns_if False c) \\e2\\ E2; + nrm A = nrm E1 \ nrm E2; brk A = (\ l. UNIV)\ + \ + Env\ B \\c ? e1 : e2\\ A" - Call: "\Env\ B \\e\\ E; Env\ nrm E \\args\\ A\ - \ - Env\ B \\{accC,statT,mode}e\mn({pTs}args)\\ A" +| Call: "\Env\ B \\e\\ E; Env\ nrm E \\args\\ A\ + \ + Env\ B \\{accC,statT,mode}e\mn({pTs}args)\\ A" -- {* The interplay of @{term Call}, @{term Methd} and @{term Body}: Why rules for @{term Methd} and @{term Body} at all? Note that a @@ -786,16 +777,16 @@ also a precondition for type-safety and so we can omit some assertion that are already ensured by well-typedness. *} - Methd: "\methd (prg Env) D sig = Some m; - Env\ B \\Body (declclass m) (stmt (mbody (mthd m)))\\ A - \ +| Methd: "\methd (prg Env) D sig = Some m; + Env\ B \\Body (declclass m) (stmt (mbody (mthd m)))\\ A + \ + \ + Env\ B \\Methd D sig\\ A" + +| Body: "\Env\ B \\c\\ C; jumpNestingOkS {Ret} c; Result \ nrm C; + nrm A = B; brk A = (\ l. UNIV)\ \ - Env\ B \\Methd D sig\\ A" - - Body: "\Env\ B \\c\\ C; jumpNestingOkS {Ret} c; Result \ nrm C; - nrm A = B; brk A = (\ l. UNIV)\ - \ - Env\ B \\Body D c\\ A" + Env\ B \\Body D c\\ A" -- {* Note that @{term A} is not correlated to @{term C}. If the body statement returns abruptly with return, evaluation of @{term Body} will absorb this return and complete normally. So we cannot trivially @@ -809,21 +800,21 @@ set and then this information must be carried over to the @{term Body} rule by the conformance predicate of the state. *} - LVar: "Env\ B \\LVar vn\\ \nrm=B, brk=\ l. UNIV\" +| LVar: "Env\ B \\LVar vn\\ \nrm=B, brk=\ l. UNIV\" - FVar: "Env\ B \\e\\ A - \ - Env\ B \\{accC,statDeclC,stat}e..fn\\ A" - - AVar: "\Env\ B \\e1\\ E1; Env\ nrm E1 \\e2\\ A\ +| FVar: "Env\ B \\e\\ A \ - Env\ B \\e1.[e2]\\ A" + Env\ B \\{accC,statDeclC,stat}e..fn\\ A" - Nil: "Env\ B \\[]::expr list\\ \nrm=B, brk=\ l. UNIV\" +| AVar: "\Env\ B \\e1\\ E1; Env\ nrm E1 \\e2\\ A\ + \ + Env\ B \\e1.[e2]\\ A" - Cons: "\Env\ B \\e::expr\\ E; Env\ nrm E \\es\\ A\ - \ - Env\ B \\e#es\\ A" +| Nil: "Env\ B \\[]::expr list\\ \nrm=B, brk=\ l. UNIV\" + +| Cons: "\Env\ B \\e::expr\\ E; Env\ nrm E \\es\\ A\ + \ + Env\ B \\e#es\\ A" declare inj_term_sym_simps [simp] @@ -832,7 +823,7 @@ ML_setup {* change_simpset (fn ss => ss delloop "split_all_tac"); *} -inductive_cases da_elim_cases [cases set]: +inductive_cases2 da_elim_cases [cases set]: "Env\ B \\Skip\\ A" "Env\ B \In1r Skip\ A" "Env\ B \\Expr e\\ A" @@ -1076,7 +1067,7 @@ from Expr.prems Expr.hyps show ?case by cases simp next - case (Lab A B C Env c l B' A') + case (Lab Env B c C A l B' A') have A: "nrm A = nrm C \ brk C l" "brk A = rmlab l (brk C)" . have "PROP ?Hyp Env B \c\ C" . moreover @@ -1102,7 +1093,7 @@ ultimately show ?case by simp next - case (Comp A B C1 C2 Env c1 c2 B' A') + case (Comp Env B c1 C1 c2 C2 A B' A') have A: "nrm A = nrm C2" "brk A = brk C1 \\ brk C2" . have "Env\ B' \\c1;; c2\\ A'" . then obtain C1' C2' @@ -1123,7 +1114,7 @@ show ?case by auto next - case (If A B C1 C2 E Env c1 c2 e B' A') + case (If Env B e E c1 C1 c2 C2 A B' A') have A: "nrm A = nrm C1 \ nrm C2" "brk A = brk C1 \\ brk C2" . have "Env\ B' \\If(e) c1 Else c2\\ A'" . then obtain C1' C2' @@ -1144,7 +1135,7 @@ show ?case by auto next - case (Loop A B C E Env c e l B' A') + case (Loop Env B e E c C A l B' A') have A: "nrm A = nrm C \ (B \ assigns_if False e)" "brk A = brk C" . have "Env\ B' \\l\ While(e) c\\ A'" . @@ -1180,12 +1171,12 @@ ultimately show ?case by auto next - case (Jmp A B Env jump B' A') + case (Jmp jump B A Env B' A') thus ?case by (elim da_elim_cases) (auto split: jump.splits) next case Throw thus ?case by - (erule da_elim_cases, auto) next - case (Try A B C C1 C2 Env c1 c2 vn B' A') + case (Try Env B c1 C1 vn C c2 C2 A B' A') have A: "nrm A = nrm C1 \ nrm C2" "brk A = brk C1 \\ brk C2" . have "Env\ B' \\Try c1 Catch(C vn) c2\\ A'" . @@ -1210,7 +1201,7 @@ show ?case by auto next - case (Fin A B C1 C2 Env c1 c2 B' A') + case (Fin Env B c1 C1 c2 C2 A B' A') have A: "nrm A = nrm C1 \ nrm C2" "brk A = (brk C1 \\\<^sub>\ nrm C2) \\ (brk C2)" . have "Env\ B' \\c1 Finally c2\\ A'" . @@ -1247,7 +1238,7 @@ next case UnOp thus ?case by - (erule da_elim_cases, auto) next - case (CondAnd A B E1 E2 Env e1 e2 B' A') + case (CondAnd Env B e1 E1 e2 E2 A B' A') have A: "nrm A = B \ assigns_if True (BinOp CondAnd e1 e2) \ assigns_if False (BinOp CondAnd e1 e2)" @@ -1276,7 +1267,7 @@ next case Ass thus ?case by - (erule da_elim_cases, auto) next - case (CondBool A B C E1 E2 Env c e1 e2 B' A') + case (CondBool Env c e1 e2 B C E1 E2 A B' A') have A: "nrm A = B \ assigns_if True (c ? e1 : e2) \ assigns_if False (c ? e1 : e2)" @@ -1295,7 +1286,7 @@ with A A' show ?case by auto next - case (Cond A B C E1 E2 Env c e1 e2 B' A') + case (Cond Env c e1 e2 B C E1 E2 A B' A') have A: "nrm A = nrm E1 \ nrm E2" "brk A = (\l. UNIV)" . have not_bool: "\ Env\ (c ? e1 : e2)\- (PrimT Boolean)" . @@ -1354,7 +1345,7 @@ next case Expr thus ?case by (iprover intro: da.Expr) next - case (Lab A B C Env c l B') + case (Lab Env B c C A l B') have "PROP ?Hyp Env B \c\" . moreover have B': "B \ B'" . @@ -1364,7 +1355,7 @@ by (iprover intro: da.Lab) thus ?case .. next - case (Comp A B C1 C2 Env c1 c2 B') + case (Comp Env B c1 C1 c2 C2 A B') have da_c1: "Env\ B \\c1\\ C1" . have "PROP ?Hyp Env B \c1\" . moreover @@ -1383,7 +1374,7 @@ by (iprover intro: da.Comp) thus ?case .. next - case (If A B C1 C2 E Env c1 c2 e B') + case (If Env B e E c1 C1 c2 C2 A B') have B': "B \ B'" . obtain E' where "Env\ B' \\e\\ E'" proof - @@ -1417,7 +1408,7 @@ by (iprover intro: da.If) thus ?case .. next - case (Loop A B C E Env c e l B') + case (Loop Env B e E c C A l B') have B': "B \ B'" . obtain E' where "Env\ B' \\e\\ E'" proof - @@ -1441,7 +1432,7 @@ by (iprover intro: da.Loop ) thus ?case .. next - case (Jmp A B Env jump B') + case (Jmp jump B A Env B') have B': "B \ B'" . with Jmp.hyps have "jump = Ret \ Result \ B' " by auto @@ -1460,7 +1451,7 @@ next case Throw thus ?case by (iprover intro: da.Throw ) next - case (Try A B C C1 C2 Env c1 c2 vn B') + case (Try Env B c1 C1 vn C c2 C2 A B') have B': "B \ B'" . obtain C1' where "Env\ B' \\c1\\ C1'" proof - @@ -1485,7 +1476,7 @@ by (iprover intro: da.Try ) thus ?case .. next - case (Fin A B C1 C2 Env c1 c2 B') + case (Fin Env B c1 C1 c2 C2 A B') have B': "B \ B'" . obtain C1' where C1': "Env\ B' \\c1\\ C1'" proof - @@ -1519,7 +1510,7 @@ next case UnOp thus ?case by (iprover intro: da.UnOp) next - case (CondAnd A B E1 E2 Env e1 e2 B') + case (CondAnd Env B e1 E1 e2 E2 A B') have B': "B \ B'" . obtain E1' where "Env\ B' \\e1\\ E1'" proof - @@ -1541,7 +1532,7 @@ by (iprover intro: da.CondAnd) thus ?case .. next - case (CondOr A B E1 E2 Env e1 e2 B') + case (CondOr Env B e1 E1 e2 E2 A B') have B': "B \ B'" . obtain E1' where "Env\ B' \\e1\\ E1'" proof - @@ -1563,7 +1554,7 @@ by (iprover intro: da.CondOr) thus ?case .. next - case (BinOp A B E1 Env binop e1 e2 B') + case (BinOp Env B e1 E1 e2 A binop B') have B': "B \ B'" . obtain E1' where E1': "Env\ B' \\e1\\ E1'" proof - @@ -1593,7 +1584,7 @@ by auto thus ?case by (iprover intro: da.Super) next - case (AccLVar A B Env vn B') + case (AccLVar vn B A Env B') have "vn \ B" . moreover have "B \ B'" . @@ -1602,7 +1593,7 @@ next case Acc thus ?case by (iprover intro: da.Acc) next - case (AssLVar A B E Env e vn B') + case (AssLVar Env B e E A vn B') have B': "B \ B'" . then obtain E' where "Env\ B' \\e\\ E'" by (rule AssLVar.hyps [elim_format]) iprover @@ -1611,7 +1602,7 @@ by (iprover intro: da.AssLVar) thus ?case .. next - case (Ass A B Env V e v B') + case (Ass v Env B V e A B') have B': "B \ B'" . have "\vn. v \ LVar vn". moreover @@ -1637,7 +1628,7 @@ by (iprover intro: da.Ass) thus ?case .. next - case (CondBool A B C E1 E2 Env c e1 e2 B') + case (CondBool Env c e1 e2 B C E1 E2 A B') have B': "B \ B'" . have "Env\(c ? e1 : e2)\-(PrimT Boolean)" . moreover obtain C' where C': "Env\ B' \\c\\ C'" @@ -1673,7 +1664,7 @@ by (iprover intro: da.CondBool) thus ?case .. next - case (Cond A B C E1 E2 Env c e1 e2 B') + case (Cond Env c e1 e2 B C E1 E2 A B') have B': "B \ B'" . have "\ Env\(c ? e1 : e2)\-(PrimT Boolean)" . moreover obtain C' where C': "Env\ B' \\c\\ C'" @@ -1709,7 +1700,7 @@ by (iprover intro: da.Cond) thus ?case .. next - case (Call A B E Env accC args e mn mode pTs statT B') + case (Call Env B e E args A accC statT mode mn pTs B') have B': "B \ B'" . obtain E' where E': "Env\ B' \\e\\ E'" proof - @@ -1735,7 +1726,7 @@ next case Methd thus ?case by (iprover intro: da.Methd) next - case (Body A B C D Env c B') + case (Body Env B c C A D B') have B': "B \ B'" . obtain C' where C': "Env\ B' \\c\\ C'" and nrm_C': "nrm C \ nrm C'" proof - @@ -1763,7 +1754,7 @@ next case FVar thus ?case by (iprover intro: da.FVar) next - case (AVar A B E1 Env e1 e2 B') + case (AVar Env B e1 E1 e2 A B') have B': "B \ B'" . obtain E1' where E1': "Env\ B' \\e1\\ E1'" proof - @@ -1789,7 +1780,7 @@ next case Nil thus ?case by (iprover intro: da.Nil) next - case (Cons A B E Env e es B') + case (Cons Env B e E es A B') have B': "B \ B'" . obtain E' where E': "Env\ B' \\e\\ E'" proof - diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/DefiniteAssignmentCorrect.thy --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Dec 11 16:06:14 2006 +0100 @@ -309,7 +309,7 @@ next case Expr thus ?case by (elim wt_elim_cases) simp next - case (Lab c jmp s0 s1 jmps T Env) + case (Lab s0 c s1 jmp jmps T Env) have jmpOK: "jumpNestingOk jmps (In1r (jmp\ c))" . have G: "prg Env = G" . have wt_c: "Env\c\\" @@ -338,7 +338,7 @@ } thus ?case by simp next - case (Comp c1 c2 s0 s1 s2 jmps T Env) + case (Comp s0 c1 s1 c2 s2 jmps T Env) have jmpOk: "jumpNestingOk jmps (In1r (c1;; c2))" . have G: "prg Env = G" . from Comp.prems obtain @@ -363,7 +363,7 @@ qed } thus ?case by simp next - case (If b c1 c2 e s0 s1 s2 jmps T Env) + case (If s0 e b s1 c1 c2 s2 jmps T Env) have jmpOk: "jumpNestingOk jmps (In1r (If(e) c1 Else c2))" . have G: "prg Env = G" . from If.prems obtain @@ -389,7 +389,7 @@ } thus ?case by simp next - case (Loop b c e l s0 s1 s2 s3 jmps T Env) + case (Loop s0 e b s1 c s2 l s3 jmps T Env) have jmpOk: "jumpNestingOk jmps (In1r (l\ While(e) c))" . have G: "prg Env = G" . have wt: "Env\In1r (l\ While(e) c)\T" . @@ -467,9 +467,9 @@ } thus ?case by simp next - case (Jmp j s jmps T Env) thus ?case by simp + case (Jmp s j jmps T Env) thus ?case by simp next - case (Throw a e s0 s1 jmps T Env) + case (Throw s0 e a s1 jmps T Env) have jmpOk: "jumpNestingOk jmps (In1r (Throw e))" . have G: "prg Env = G" . from Throw.prems obtain Te where @@ -491,7 +491,7 @@ } thus ?case by simp next - case (Try C c1 c2 s0 s1 s2 s3 vn jmps T Env) + case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env) have jmpOk: "jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))" . have G: "prg Env = G" . from Try.prems obtain @@ -543,7 +543,7 @@ } thus ?case by simp next - case (Fin c1 c2 s0 s1 s2 s3 x1 jmps T Env) + case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env) have jmpOk: " jumpNestingOk jmps (In1r (c1 Finally c2))" . have G: "prg Env = G" . from Fin.prems obtain @@ -571,7 +571,7 @@ } thus ?case by simp next - case (Init C c s0 s1 s2 s3 jmps T Env) + case (Init C c s0 s3 s1 s2 jmps T Env) have "jumpNestingOk jmps (In1r (Init C))". have G: "prg Env = G" . have "the (class G C) = c" . @@ -636,7 +636,7 @@ } thus ?case by simp next - case (NewC C a s0 s1 s2 jmps T Env) + case (NewC s0 C s1 a s2 jmps T Env) { fix j assume jmp: "abrupt s2 = Some (Jump j)" @@ -660,7 +660,7 @@ } thus ?case by simp next - case (NewA elT a e i s0 s1 s2 s3 jmps T Env) + case (NewA s0 elT s1 e i s2 a s3 jmps T Env) { fix j assume jmp: "abrupt s3 = Some (Jump j)" @@ -692,7 +692,7 @@ } thus ?case by simp next - case (Cast cT e s0 s1 s2 v jmps T Env) + case (Cast s0 e v s1 s2 cT jmps T Env) { fix j assume jmp: "abrupt s2 = Some (Jump j)" @@ -715,7 +715,7 @@ } thus ?case by simp next - case (Inst eT b e s0 s1 v jmps T Env) + case (Inst s0 e v s1 b eT jmps T Env) { fix j assume jmp: "abrupt s1 = Some (Jump j)" @@ -734,7 +734,7 @@ next case Lit thus ?case by simp next - case (UnOp e s0 s1 unop v jmps T Env) + case (UnOp s0 e v s1 unop jmps T Env) { fix j assume jmp: "abrupt s1 = Some (Jump j)" @@ -751,7 +751,7 @@ } thus ?case by simp next - case (BinOp binop e1 e2 s0 s1 s2 v1 v2 jmps T Env) + case (BinOp s0 e1 v1 s1 binop e2 v2 s2 jmps T Env) { fix j assume jmp: "abrupt s2 = Some (Jump j)" @@ -784,7 +784,7 @@ next case Super thus ?case by simp next - case (Acc f s0 s1 v va jmps T Env) + case (Acc s0 va v f s1 jmps T Env) { fix j assume jmp: "abrupt s1 = Some (Jump j)" @@ -801,7 +801,7 @@ } thus ?case by simp next - case (Ass e f s0 s1 s2 v va w jmps T Env) + case (Ass s0 va w f s1 e v s2 jmps T Env) have G: "prg Env = G" . from Ass.prems obtain vT eT where @@ -841,7 +841,7 @@ } thus ?case by simp next - case (Cond b e0 e1 e2 s0 s1 s2 v jmps T Env) + case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env) have G: "prg Env = G" . have hyp_e0: "PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)" . have hyp_e1_e2: "PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) @@ -876,7 +876,7 @@ } thus ?case by simp next - case (Call D a accC args e mn mode pTs s0 s1 s2 s3 s3' s4 statT v vs + case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4 jmps T Env) have G: "prg Env = G" . from Call.prems @@ -919,14 +919,14 @@ } thus ?case by simp next - case (Methd D s0 s1 sig v jmps T Env) + case (Methd s0 D sig v s1 jmps T Env) have "G\Norm s0 \Methd D sig-\v\ s1" by (rule eval.Methd) hence "\ j. abrupt s1 \ Some (Jump j)" by (rule Methd_no_jump) simp thus ?case by simp next - case (Body D c s0 s1 s2 s3 jmps T Env) + case (Body s0 D s1 c s2 s3 jmps T Env) have "G\Norm s0 \Body D c-\the (locals (store s2) Result) \ abupd (absorb Ret) s3" by (rule eval.Body) @@ -937,7 +937,7 @@ case LVar thus ?case by (simp add: lvar_def Let_def) next - case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v jmps T Env) + case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env) have G: "prg Env = G" . from wf FVar.prems obtain statC f where @@ -996,7 +996,7 @@ } ultimately show ?case using v by simp next - case (AVar a e1 e2 i s0 s1 s2 s2' v jmps T Env) + case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env) have G: "prg Env = G" . from AVar.prems obtain e1T e2T where @@ -1042,7 +1042,7 @@ next case Nil thus ?case by simp next - case (Cons e es s0 s1 s2 v vs jmps T Env) + case (Cons s0 e v s1 es vs s2 jmps T Env) have G: "prg Env = G" . from Cons.prems obtain eT esT where wt_e: "Env\e\-eT" and wt_e2: "Env\es\\esT" @@ -1290,7 +1290,7 @@ next case Lab thus ?case by simp next - case (Comp c1 c2 s0 s1 s2) + case (Comp s0 c1 s1 c2 s2) from Comp.hyps have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" by simp @@ -1300,7 +1300,7 @@ by simp finally show ?case by simp next - case (If b c1 c2 e s0 s1 s2) + case (If s0 e b s1 c1 c2 s2) from If.hyps have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" by simp @@ -1310,7 +1310,7 @@ by simp finally show ?case by simp next - case (Loop b c e l s0 s1 s2 s3) + case (Loop s0 e b s1 c s2 l s3) show ?case proof (cases "the_Bool b") case True @@ -1334,7 +1334,7 @@ next case Throw thus ?case by simp next - case (Try C c1 c2 s0 s1 s2 s3 vn) + case (Try s0 c1 s1 s2 C vn c2 s3) then have s0_s1: "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" by simp @@ -1361,7 +1361,7 @@ using False Try.hyps by simp qed next - case (Fin c1 c2 s0 s1 s2 s3 x1) + case (Fin s0 c1 x1 s1 c2 s2 s3) show ?case proof (cases "\err. x1 = Some (Error err)") case True @@ -1384,7 +1384,7 @@ using Fin.hyps by simp qed next - case (Init C c s0 s1 s2 s3) + case (Init C c s0 s3 s1 s2) show ?case proof (cases "inited C (globs s0)") case True @@ -1405,7 +1405,7 @@ thus ?thesis by simp qed next - case (NewC C a s0 s1 s2) + case (NewC s0 C s1 a s2) have halloc: "G\s1 \halloc CInst C\a\ s2" . from NewC.hyps have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" @@ -1415,7 +1415,7 @@ have "\ \ dom (locals (store s2))" by (rule dom_locals_halloc_mono) finally show ?case by simp next - case (NewA T a e i s0 s1 s2 s3) + case (NewA s0 T s1 e i s2 a s3) have halloc: "G\abupd (check_neg i) s2 \halloc Arr T (the_Intg i)\a\ s3" . from NewA.hyps have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" @@ -1437,7 +1437,7 @@ next case UnOp thus ?case by simp next - case (BinOp binop e1 e2 s0 s1 s2 v1 v2) + case (BinOp s0 e1 v1 s1 binop e2 v2 s2) from BinOp.hyps have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" by simp @@ -1450,7 +1450,7 @@ next case Acc thus ?case by simp next - case (Ass e f s0 s1 s2 v va w) + case (Ass s0 va w f s1 e v s2) from Ass.hyps have s0_s1: "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" @@ -1486,7 +1486,7 @@ by simp qed next - case (Cond b e0 e1 e2 s0 s1 s2 v) + case (Cond s0 e0 b s1 e1 e2 v s2) from Cond.hyps have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" by simp @@ -1496,7 +1496,7 @@ by simp finally show ?case by simp next - case (Call D a' accC args e mn mode pTs s0 s1 s2 s3 s3' s4 statT v vs) + case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4) have s3: "s3 = init_lvars G D \name = mn, parTs = pTs\ mode a' vs s2" . from Call.hyps have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" @@ -1512,7 +1512,7 @@ next case Methd thus ?case by simp next - case (Body D c s0 s1 s2 s3) + case (Body s0 D s1 c s2 s3) from Body.hyps have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" by simp @@ -1540,7 +1540,7 @@ using dom_locals_lvar_mono by simp next - case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v) + case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC) from FVar.hyps obtain s2': "s2' = snd (fvar statDeclC stat fn a s2)" and v: "v = fst (fvar statDeclC stat fn a s2)" @@ -1572,7 +1572,7 @@ using v_ok by simp next - case (AVar a e1 e2 i s0 s1 s2 s2' v) + case (AVar s0 e1 a s1 e2 i s2 v s2') from AVar.hyps obtain s2': "s2' = snd (avar G i a s2)" and v: "v = fst (avar G i a s2)" @@ -1599,7 +1599,7 @@ next case Nil thus ?case by simp next - case (Cons e es s0 s1 s2 v vs) + case (Cons s0 e v s1 es vs s2) from Cons.hyps have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" by simp @@ -1689,7 +1689,7 @@ next case NewC show ?case by simp next - case (NewA T a e i s0 s1 s2 s3) + case (NewA s0 T s1 e i s2 a s3) have halloc: "G\abupd (check_neg i) s2 \halloc Arr T (the_Intg i)\a\ s3" . have "assigns (In1l e) \ dom (locals (store s2))" proof - @@ -1706,7 +1706,7 @@ by (rule dom_locals_halloc_mono [elim_format]) simp finally show ?case by simp next - case (Cast T e s0 s1 s2 v) + case (Cast s0 e v s1 s2 T) hence "normal s1" by (cases s1,simp) with Cast.hyps have "assigns (In1l e) \ dom (locals (store s1))" @@ -1725,7 +1725,7 @@ next case UnOp thus ?case by simp next - case (BinOp binop e1 e2 s0 s1 s2 v1 v2) + case (BinOp s0 e1 v1 s1 binop e2 v2 s2) hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) with BinOp.hyps have "assigns (In1l e1) \ dom (locals (store s1))" @@ -1756,7 +1756,7 @@ next case Acc thus ?case by simp next - case (Ass e f s0 s1 s2 v va w) + case (Ass s0 va w f s1 e v s2) have nrm_ass_s2: "normal (assign f v s2)" . hence nrm_s2: "normal s2" by (cases s2, simp add: assign_def Let_def) @@ -1808,7 +1808,7 @@ show ?thesis by (simp add: Un_assoc) qed next - case (Cond b e0 e1 e2 s0 s1 s2 v) + case (Cond s0 e0 b s1 e1 e2 v s2) hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) with Cond.hyps @@ -1845,7 +1845,7 @@ thus ?thesis using False by simp qed next - case (Call D a' accC args e mn mode pTs s0 s1 s2 s3 s3' s4 statT v vs) + case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4) have nrm_s2: "normal s2" proof - have "normal ((set_lvars (locals (snd s2))) s4)" . @@ -1887,7 +1887,7 @@ next case LVar thus ?case by simp next - case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v) + case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC) have s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" . have avar: "(v, s2') = fvar statDeclC stat fn a s2" . have nrm_s2: "normal s2" @@ -1916,7 +1916,7 @@ finally show ?case by simp next - case (AVar a e1 e2 i s0 s1 s2 s2' v) + case (AVar s0 e1 a s1 e2 i s2 v s2') have avar: "(v, s2') = avar G i a s2" . have nrm_s2: "normal s2" proof - @@ -1954,7 +1954,7 @@ next case Nil show ?case by simp next - case (Cons e es s0 s1 s2 v vs) + case (Cons s0 e v s1 es vs s2) have "assigns (In1l e) \ dom (locals (store s1))" proof - from Cons @@ -2254,19 +2254,19 @@ proof (induct) case Abrupt thus ?case by simp next - case (NewC C a s0 s1 s2) + case (NewC s0 C s1 a s2) have "Env\NewC C\-PrimT Boolean" . hence False by cases simp thus ?case .. next - case (NewA T a e i s0 s1 s2 s3) + case (NewA s0 T s1 e i s2 a s3) have "Env\New T[e]\-PrimT Boolean" . hence False by cases simp thus ?case .. next - case (Cast T e s0 s1 s2 b) + case (Cast s0 e b s1 s2 T) have s2: "s2 = abupd (raise_if (\ prg Env,snd s1\b fits T) ClassCast) s1". have "assigns_if (the_Bool b) e \ dom (locals (store s1))" proof - @@ -2285,7 +2285,7 @@ by simp finally show ?case by simp next - case (Inst T b e s0 s1 v) + case (Inst s0 e v s1 b T) have "prg Env\Norm s0 \e-\v\ s1" and "normal s1" . hence "assignsE e \ dom (locals (store s1))" by (rule assignsE_good_approx) @@ -2301,7 +2301,7 @@ thus ?case by simp next - case (UnOp e s0 s1 unop v) + case (UnOp s0 e v s1 unop) have bool: "Env\UnOp unop e\-PrimT Boolean" . hence bool_e: "Env\e\-PrimT Boolean" by cases (cases unop,simp_all) @@ -2341,7 +2341,7 @@ thus ?thesis by simp qed next - case (BinOp binop e1 e2 s0 s1 s2 v1 v2) + case (BinOp s0 e1 v1 s1 binop e2 v2 s2) have bool: "Env\BinOp binop e1 e2\-PrimT Boolean" . show ?case proof (cases "constVal (BinOp binop e1 e2)") @@ -2507,13 +2507,13 @@ by cases simp thus ?case .. next - case (Acc f s0 s1 v va) + case (Acc s0 va v f s1) have "prg Env\Norm s0 \va=\(v, f)\ s1" and "normal s1". hence "assignsV va \ dom (locals (store s1))" by (rule assignsV_good_approx) thus ?case by simp next - case (Ass e f s0 s1 s2 v va w) + case (Ass s0 va w f s1 e v s2) hence "prg Env\Norm s0 \va := e-\v\ assign f v s2" by - (rule eval.Ass) moreover have "normal (assign f v s2)" . @@ -2522,7 +2522,7 @@ by (rule assignsE_good_approx) thus ?case by simp next - case (Cond b e0 e1 e2 s0 s1 s2 v) + case (Cond s0 e0 b s1 e1 e2 v s2) have "Env\e0 ? e1 : e2\-PrimT Boolean" . then obtain wt_e1: "Env\e1\-PrimT Boolean" and wt_e2: "Env\e2\-PrimT Boolean" @@ -2599,7 +2599,7 @@ qed qed next - case (Call D a accC args e mn mode pTs s0 s1 s2 s3 s3' s4 statT v vs) + case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4) hence "prg Env\Norm s0 \({accC,statT,mode}e\mn( {pTs}args))-\v\ (set_lvars (locals (store s2)) s4)" @@ -2662,7 +2662,7 @@ from eval and wt da G show ?thesis proof (induct arbitrary: Env T A) - case (Abrupt s t xc Env T A) + case (Abrupt xc s t Env T A) have da: "Env\ dom (locals s) \t\ A" using Abrupt.prems by simp have "?NormalAssigned (Some xc,s) A" by simp @@ -2687,14 +2687,14 @@ by simp ultimately show ?case by (intro conjI) next - case (Expr e s0 s1 v Env T A) + case (Expr s0 e v s1 Env T A) from Expr.prems show "?NormalAssigned s1 A \ ?BreakAssigned (Norm s0) s1 A \ ?ResAssigned (Norm s0) s1" by (elim wt_elim_cases da_elim_cases) (rule Expr.hyps, auto) next - case (Lab c j s0 s1 Env T A) + case (Lab s0 c s1 j Env T A) have G: "prg Env = G" . from Lab.prems obtain C l where @@ -2753,7 +2753,7 @@ by (cases s1) (simp add: absorb_def) ultimately show ?case by (intro conjI) next - case (Comp c1 c2 s0 s1 s2 Env T A) + case (Comp s0 c1 s1 c2 s2 Env T A) have G: "prg Env = G" . from Comp.prems obtain C1 C2 @@ -2826,7 +2826,7 @@ ultimately show ?thesis by (intro conjI) qed next - case (If b c1 c2 e s0 s1 s2 Env T A) + case (If s0 e b s1 c1 c2 s2 Env T A) have G: "prg Env = G" . with If.hyps have eval_e: "prg Env \Norm s0 \e-\b\ s1" by simp from If.prems @@ -2930,7 +2930,7 @@ ultimately show ?thesis by simp qed next - case (Loop b c e l s0 s1 s2 s3 Env T A) + case (Loop s0 e b s1 c s2 l s3 Env T A) have G: "prg Env = G" . with Loop.hyps have eval_e: "prg Env\Norm s0 \e-\b\ s1" by (simp (no_asm_simp)) @@ -3118,7 +3118,7 @@ by simp qed next - case (Jmp j s Env T A) + case (Jmp s j Env T A) have "?NormalAssigned (Some (Jump j),s) A" by simp moreover from Jmp.prems @@ -3136,7 +3136,7 @@ by simp ultimately show ?case by (intro conjI) next - case (Throw a e s0 s1 Env T A) + case (Throw s0 e a s1 Env T A) have G: "prg Env = G" . from Throw.prems obtain E where da_e: "Env\ dom (locals (store ((Norm s0)::state))) \\e\\ E" @@ -3166,7 +3166,7 @@ by (cases s1) (simp add: throw_def abrupt_if_def) ultimately show ?case by (intro conjI) next - case (Try C c1 c2 s0 s1 s2 s3 vn Env T A) + case (Try s0 c1 s1 s2 C vn c2 s3 Env T A) have G: "prg Env = G" . from Try.prems obtain C1 C2 where da_c1: "Env\ dom (locals (store ((Norm s0)::state))) \\c1\\ C1" and @@ -3313,7 +3313,7 @@ qed qed next - case (Fin c1 c2 s0 s1 s2 s3 x1 Env T A) + case (Fin s0 c1 x1 s1 c2 s2 s3 Env T A) have G: "prg Env = G" . from Fin.prems obtain C1 C2 where da_C1: "Env\ dom (locals (store ((Norm s0)::state))) \\c1\\ C1" and @@ -3472,7 +3472,7 @@ by simp ultimately show ?case by (intro conjI) next - case (Init C c s0 s1 s2 s3 Env T A) + case (Init C c s0 s3 s1 s2 Env T A) have G: "prg Env = G" . from Init.hyps have eval: "prg Env\ Norm s0 \Init C\ s3" @@ -3528,7 +3528,7 @@ ultimately show ?thesis by (intro conjI) qed next - case (NewC C a s0 s1 s2 Env T A) + case (NewC s0 C s1 a s2 Env T A) have G: "prg Env = G" . from NewC.prems obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))" @@ -3568,7 +3568,7 @@ by simp_all ultimately show ?case by (intro conjI) next - case (NewA elT a e i s0 s1 s2 s3 Env T A) + case (NewA s0 elT s1 e i s2 a s3 Env T A) have G: "prg Env = G" . from NewA.prems obtain da_e: "Env\ dom (locals (store ((Norm s0)::state))) \\e\\ A" @@ -3633,7 +3633,7 @@ by simp_all ultimately show ?case by (intro conjI) next - case (Cast cT e s0 s1 s2 v Env T A) + case (Cast s0 e v s1 s2 cT Env T A) have G: "prg Env = G" . from Cast.prems obtain da_e: "Env\ dom (locals (store ((Norm s0)::state))) \\e\\ A" @@ -3678,7 +3678,7 @@ by simp_all ultimately show ?case by (intro conjI) next - case (Inst iT b e s0 s1 v Env T A) + case (Inst s0 e v s1 b iT Env T A) have G: "prg Env = G" . from Inst.prems obtain da_e: "Env\ dom (locals (store ((Norm s0)::state))) \\e\\ A" @@ -3700,7 +3700,7 @@ by (elim da_elim_cases) simp thus ?case by simp next - case (UnOp e s0 s1 unop v Env T A) + case (UnOp s0 e v s1 unop Env T A) have G: "prg Env = G" . from UnOp.prems obtain da_e: "Env\ dom (locals (store ((Norm s0)::state))) \\e\\ A" @@ -3716,7 +3716,7 @@ by simp thus ?case by (intro conjI) next - case (BinOp binop e1 e2 s0 s1 s2 v1 v2 Env T A) + case (BinOp s0 e1 v1 s1 binop e2 v2 s2 Env T A) have G: "prg Env = G". from BinOp.hyps have @@ -3875,7 +3875,7 @@ by (elim da_elim_cases) simp thus ?case by simp next - case (Acc upd s0 s1 w v Env T A) + case (Acc s0 v w upd s1 Env T A) show ?case proof (cases "\ vn. v = LVar vn") case True @@ -3905,7 +3905,7 @@ thus ?thesis by (intro conjI) qed next - case (Ass e upd s0 s1 s2 v var w Env T A) + case (Ass s0 var w upd s1 e v s2 Env T A) have G: "prg Env = G" . from Ass.prems obtain varT eT where wt_var: "Env\var\=varT" and @@ -4019,7 +4019,7 @@ by simp_all ultimately show ?case by (intro conjI) next - case (Cond b e0 e1 e2 s0 s1 s2 v Env T A) + case (Cond s0 e0 b s1 e1 e2 v s2 Env T A) have G: "prg Env = G" . have "?NormalAssigned s2 A" proof @@ -4140,7 +4140,7 @@ by simp_all ultimately show ?case by (intro conjI) next - case (Call D a accC args e mn mode pTs s0 s1 s2 s3 s3' s4 statT v vs + case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4 Env T A) have G: "prg Env = G" . have "?NormalAssigned (restore_lvars s2 s4) A" @@ -4213,7 +4213,7 @@ by simp_all ultimately show ?case by (intro conjI) next - case (Methd D s0 s1 sig v Env T A) + case (Methd s0 D sig v s1 Env T A) have G: "prg Env = G". from Methd.prems obtain m where m: "methd (prg Env) D sig = Some m" and @@ -4235,7 +4235,7 @@ ultimately show ?case using G by simp next - case (Body D c s0 s1 s2 s3 Env T A) + case (Body s0 D s1 c s2 s3 Env T A) have G: "prg Env = G" . from Body.prems have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))" @@ -4261,7 +4261,7 @@ by (elim da_elim_cases) simp thus ?case by simp next - case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v Env T A) + case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC Env T A) have G: "prg Env = G" . have "?NormalAssigned s3 A" proof @@ -4333,7 +4333,7 @@ by simp_all ultimately show ?case by (intro conjI) next - case (AVar a e1 e2 i s0 s1 s2 s2' v Env T A) + case (AVar s0 e1 a s1 e2 i s2 v s2' Env T A) have G: "prg Env = G" . have "?NormalAssigned s2' A" proof @@ -4405,7 +4405,7 @@ by (elim da_elim_cases) simp thus ?case by simp next - case (Cons e es s0 s1 s2 v vs Env T A) + case (Cons s0 e v s1 es vs s2 Env T A) have G: "prg Env = G" . have "?NormalAssigned s2 A" proof diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/Eval.thy Mon Dec 11 16:06:14 2006 +0100 @@ -474,104 +474,75 @@ section "evaluation judgments" -consts - eval :: "prog \ (state \ term \ vals \ state) set" - halloc:: "prog \ (state \ obj_tag \ loc \ state) set" - sxalloc:: "prog \ (state \ state) set" - - -syntax -eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _" [61,61,80, 61]60) -exec ::"[prog,state,stmt ,state]=>bool"("_|-_ -_-> _" [61,61,65, 61]60) -evar ::"[prog,state,var ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60) -eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60) -evals::"[prog,state,expr list , - val list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60) -hallo::"[prog,state,obj_tag, - loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60) -sallo::"[prog,state ,state]=>bool"("_|-_ -sxalloc-> _"[61,61, 61]60) - -syntax (xsymbols) -eval ::"[prog,state,term,vals\state]\bool" ("_\_ \_\\ _" [61,61,80, 61]60) -exec ::"[prog,state,stmt ,state]\bool"("_\_ \_\ _" [61,61,65, 61]60) -evar ::"[prog,state,var ,vvar,state]\bool"("_\_ \_=\_\ _"[61,61,90,61,61]60) -eval_::"[prog,state,expr ,val ,state]\bool"("_\_ \_-\_\ _"[61,61,80,61,61]60) -evals::"[prog,state,expr list , - val list ,state]\bool"("_\_ \_\\_\ _"[61,61,61,61,61]60) -hallo::"[prog,state,obj_tag, - loc,state]\bool"("_\_ \halloc _\_\ _"[61,61,61,61,61]60) -sallo::"[prog,state, state]\bool"("_\_ \sxalloc\ _"[61,61, 61]60) - -translations - "G\s \t \\ w___s' " == "(s,t,w___s') \ eval G" - "G\s \t \\ (w, s')" <= "(s,t,w, s') \ eval G" - "G\s \t \\ (w,x,s')" <= "(s,t,w,x,s') \ eval G" - "G\s \c \ (x,s')" <= "G\s \In1r c\\ (\,x,s')" - "G\s \c \ s' " == "G\s \In1r c\\ (\ , s')" - "G\s \e-\v \ (x,s')" <= "G\s \In1l e\\ (In1 v ,x,s')" - "G\s \e-\v \ s' " == "G\s \In1l e\\ (In1 v , s')" - "G\s \e=\vf\ (x,s')" <= "G\s \In2 e\\ (In2 vf,x,s')" - "G\s \e=\vf\ s' " == "G\s \In2 e\\ (In2 vf, s')" - "G\s \e\\v \ (x,s')" <= "G\s \In3 e\\ (In3 v ,x,s')" - "G\s \e\\v \ s' " == "G\s \In3 e\\ (In3 v , s')" - "G\s \halloc oi\a\ (x,s')" <= "(s,oi,a,x,s') \ halloc G" - "G\s \halloc oi\a\ s' " == "(s,oi,a, s') \ halloc G" - "G\s \sxalloc\ (x,s')" <= "(s ,x,s') \ sxalloc G" - "G\s \sxalloc\ s' " == "(s , s') \ sxalloc G" - -inductive "halloc G" intros --{* allocating objects on the heap, cf. 12.5 *} +inductive2 + halloc :: "[prog,state,obj_tag,loc,state]\bool" ("_\_ \halloc _\_\ _"[61,61,61,61,61]60) for G::prog +where --{* allocating objects on the heap, cf. 12.5 *} Abrupt: "G\(Some x,s) \halloc oi\arbitrary\ (Some x,s)" - New: "\new_Addr (heap s) = Some a; +| New: "\new_Addr (heap s) = Some a; (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi) else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\ \ G\Norm s \halloc oi\a\ (x,init_obj G oi' (Heap a) s)" -inductive "sxalloc G" intros --{* allocating exception objects for - standard exceptions (other than OutOfMemory) *} +inductive2 sxalloc :: "[prog,state,state]\bool" ("_\_ \sxalloc\ _"[61,61,61]60) for G::prog +where --{* allocating exception objects for + standard exceptions (other than OutOfMemory) *} Norm: "G\ Norm s \sxalloc\ Norm s" - Jmp: "G\(Some (Jump j), s) \sxalloc\ (Some (Jump j), s)" +| Jmp: "G\(Some (Jump j), s) \sxalloc\ (Some (Jump j), s)" - Error: "G\(Some (Error e), s) \sxalloc\ (Some (Error e), s)" +| Error: "G\(Some (Error e), s) \sxalloc\ (Some (Error e), s)" - XcptL: "G\(Some (Xcpt (Loc a) ),s) \sxalloc\ (Some (Xcpt (Loc a)),s)" +| XcptL: "G\(Some (Xcpt (Loc a) ),s) \sxalloc\ (Some (Xcpt (Loc a)),s)" - SXcpt: "\G\Norm s0 \halloc (CInst (SXcpt xn))\a\ (x,s1)\ \ +| SXcpt: "\G\Norm s0 \halloc (CInst (SXcpt xn))\a\ (x,s1)\ \ G\(Some (Xcpt (Std xn)),s0) \sxalloc\ (Some (Xcpt (Loc a)),s1)" -inductive "eval G" intros +inductive2 + eval :: "[prog,state,term,vals,state]\bool" ("_\_ \_\\ '(_, _')" [61,61,80,0,0]60) + and exec ::"[prog,state,stmt ,state]\bool"("_\_ \_\ _" [61,61,65, 61]60) + and evar ::"[prog,state,var ,vvar,state]\bool"("_\_ \_=\_\ _"[61,61,90,61,61]60) + and eval'::"[prog,state,expr ,val ,state]\bool"("_\_ \_-\_\ _"[61,61,80,61,61]60) + and evals::"[prog,state,expr list , + val list ,state]\bool"("_\_ \_\\_\ _"[61,61,61,61,61]60) + for G::prog +where + + "G\s \c \ s' \ G\s \In1r c\\ (\, s')" +| "G\s \e-\v \ s' \ G\s \In1l e\\ (In1 v, s')" +| "G\s \e=\vf\ s' \ G\s \In2 e\\ (In2 vf, s')" +| "G\s \e\\v \ s' \ G\s \In3 e\\ (In3 v, s')" --{* propagation of abrupt completion *} --{* cf. 14.1, 15.5 *} - Abrupt: - "G\(Some xc,s) \t\\ (arbitrary3 t,(Some xc,s))" +| Abrupt: + "G\(Some xc,s) \t\\ (arbitrary3 t, (Some xc, s))" --{* execution of statements *} --{* cf. 14.5 *} - Skip: "G\Norm s \Skip\ Norm s" +| Skip: "G\Norm s \Skip\ Norm s" --{* cf. 14.7 *} - Expr: "\G\Norm s0 \e-\v\ s1\ \ +| Expr: "\G\Norm s0 \e-\v\ s1\ \ G\Norm s0 \Expr e\ s1" - Lab: "\G\Norm s0 \c \ s1\ \ +| Lab: "\G\Norm s0 \c \ s1\ \ G\Norm s0 \l\ c\ abupd (absorb l) s1" --{* cf. 14.2 *} - Comp: "\G\Norm s0 \c1 \ s1; +| Comp: "\G\Norm s0 \c1 \ s1; G\ s1 \c2 \ s2\ \ G\Norm s0 \c1;; c2\ s2" --{* cf. 14.8.2 *} - If: "\G\Norm s0 \e-\b\ s1; +| If: "\G\Norm s0 \e-\b\ s1; G\ s1\(if the_Bool b then c1 else c2)\ s2\ \ G\Norm s0 \If(e) c1 Else c2 \ s2" @@ -583,26 +554,26 @@ the state before the iterative evaluation of the while statement. A break jump is handled by the Lab Statement @{text "Lab l (while\)"}. *} - Loop: "\G\Norm s0 \e-\b\ s1; +| Loop: "\G\Norm s0 \e-\b\ s1; if the_Bool b then (G\s1 \c\ s2 \ G\(abupd (absorb (Cont l)) s2) \l\ While(e) c\ s3) else s3 = s1\ \ G\Norm s0 \l\ While(e) c\ s3" - Jmp: "G\Norm s \Jmp j\ (Some (Jump j), s)" +| Jmp: "G\Norm s \Jmp j\ (Some (Jump j), s)" --{* cf. 14.16 *} - Throw: "\G\Norm s0 \e-\a'\ s1\ \ +| Throw: "\G\Norm s0 \e-\a'\ s1\ \ G\Norm s0 \Throw e\ abupd (throw a') s1" --{* cf. 14.18.1 *} - Try: "\G\Norm s0 \c1\ s1; G\s1 \sxalloc\ s2; +| Try: "\G\Norm s0 \c1\ s1; G\s1 \sxalloc\ s2; if G,s2\catch C then G\new_xcpt_var vn s2 \c2\ s3 else s3 = s2\ \ G\Norm s0 \Try c1 Catch(C vn) c2\ s3" --{* cf. 14.18.2 *} - Fin: "\G\Norm s0 \c1\ (x1,s1); +| Fin: "\G\Norm s0 \c1\ (x1,s1); G\Norm s1 \c2\ s2; s3=(if (\ err. x1=Some (Error err)) then (x1,s1) @@ -610,7 +581,7 @@ \ G\Norm s0 \c1 Finally c2\ s3" --{* cf. 12.4.2, 8.5 *} - Init: "\the (class G C) = c; +| Init: "\the (class G C) = c; if inited C (globs s0) then s3 = Norm s0 else (G\Norm (init_class_obj G C s0) \(if C = Object then Skip else Init (super c))\ s1 \ @@ -642,51 +613,51 @@ --{* evaluation of expressions *} --{* cf. 15.8.1, 12.4.1 *} - NewC: "\G\Norm s0 \Init C\ s1; +| NewC: "\G\Norm s0 \Init C\ s1; G\ s1 \halloc (CInst C)\a\ s2\ \ G\Norm s0 \NewC C-\Addr a\ s2" --{* cf. 15.9.1, 12.4.1 *} - NewA: "\G\Norm s0 \init_comp_ty T\ s1; G\s1 \e-\i'\ s2; +| NewA: "\G\Norm s0 \init_comp_ty T\ s1; G\s1 \e-\i'\ s2; G\abupd (check_neg i') s2 \halloc (Arr T (the_Intg i'))\a\ s3\ \ G\Norm s0 \New T[e]-\Addr a\ s3" --{* cf. 15.15 *} - Cast: "\G\Norm s0 \e-\v\ s1; +| Cast: "\G\Norm s0 \e-\v\ s1; s2 = abupd (raise_if (\G,store s1\v fits T) ClassCast) s1\ \ G\Norm s0 \Cast T e-\v\ s2" --{* cf. 15.19.2 *} - Inst: "\G\Norm s0 \e-\v\ s1; +| Inst: "\G\Norm s0 \e-\v\ s1; b = (v\Null \ G,store s1\v fits RefT T)\ \ G\Norm s0 \e InstOf T-\Bool b\ s1" --{* cf. 15.7.1 *} - Lit: "G\Norm s \Lit v-\v\ Norm s" +| Lit: "G\Norm s \Lit v-\v\ Norm s" - UnOp: "\G\Norm s0 \e-\v\ s1\ +| UnOp: "\G\Norm s0 \e-\v\ s1\ \ G\Norm s0 \UnOp unop e-\(eval_unop unop v)\ s1" - BinOp: "\G\Norm s0 \e1-\v1\ s1; +| BinOp: "\G\Norm s0 \e1-\v1\ s1; G\s1 \(if need_second_arg binop v1 then (In1l e2) else (In1r Skip)) - \\ (In1 v2,s2) + \\ (In1 v2, s2) \ \ G\Norm s0 \BinOp binop e1 e2-\(eval_binop binop v1 v2)\ s2" --{* cf. 15.10.2 *} - Super: "G\Norm s \Super-\val_this s\ Norm s" +| Super: "G\Norm s \Super-\val_this s\ Norm s" --{* cf. 15.2 *} - Acc: "\G\Norm s0 \va=\(v,f)\ s1\ \ +| Acc: "\G\Norm s0 \va=\(v,f)\ s1\ \ G\Norm s0 \Acc va-\v\ s1" --{* cf. 15.25.1 *} - Ass: "\G\Norm s0 \va=\(w,f)\ s1; +| Ass: "\G\Norm s0 \va=\(w,f)\ s1; G\ s1 \e-\v \ s2\ \ G\Norm s0 \va:=e-\v\ assign f v s2" --{* cf. 15.24 *} - Cond: "\G\Norm s0 \e0-\b\ s1; +| Cond: "\G\Norm s0 \e0-\b\ s1; G\ s1 \(if the_Bool b then e1 else e2)-\v\ s2\ \ G\Norm s0 \e0 ? e1 : e2-\v\ s2" @@ -710,7 +681,7 @@ \end{itemize} *} --{* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *} - Call: +| Call: "\G\Norm s0 \e-\a'\ s1; G\s1 \args\\vs\ s2; D = invocation_declclass G mode (store s2) a' statT \name=mn,parTs=pTs\; s3=init_lvars G D \name=mn,parTs=pTs\ mode a' vs s2; @@ -723,10 +694,10 @@ reference in case of an instance method invocation. *} - Methd: "\G\Norm s0 \body G D sig-\v\ s1\ \ +| Methd: "\G\Norm s0 \body G D sig-\v\ s1\ \ G\Norm s0 \Methd D sig-\v\ s1" - Body: "\G\Norm s0 \Init D\ s1; G\s1 \c\ s2; +| Body: "\G\Norm s0 \Init D\ s1; G\s1 \c\ s2; s3 = (if (\ l. abrupt s2 = Some (Jump (Break l)) \ abrupt s2 = Some (Jump (Cont l))) then abupd (\ x. Some (Error CrossMethodJump)) s2 @@ -742,10 +713,10 @@ --{* evaluation of variables *} --{* cf. 15.13.1, 15.7.2 *} - LVar: "G\Norm s \LVar vn=\lvar vn s\ Norm s" +| LVar: "G\Norm s \LVar vn=\lvar vn s\ Norm s" --{* cf. 15.10.1, 12.4.1 *} - FVar: "\G\Norm s0 \Init statDeclC\ s1; G\s1 \e-\a\ s2; +| FVar: "\G\Norm s0 \Init statDeclC\ s1; G\s1 \e-\a\ s2; (v,s2') = fvar statDeclC stat fn a s2; s3 = check_field_access G accC statDeclC fn stat a s2' \ \ G\Norm s0 \{accC,statDeclC,stat}e..fn=\v\ s3" @@ -755,7 +726,7 @@ *} --{* cf. 15.12.1, 15.25.1 *} - AVar: "\G\ Norm s0 \e1-\a\ s1; G\s1 \e2-\i\ s2; +| AVar: "\G\ Norm s0 \e1-\a\ s1; G\s1 \e2-\i\ s2; (v,s2') = avar G i a s2\ \ G\Norm s0 \e1.[e2]=\v\ s2'" @@ -763,11 +734,11 @@ --{* evaluation of expression lists *} --{* cf. 15.11.4.2 *} - Nil: +| Nil: "G\Norm s0 \[]\\[]\ Norm s0" --{* cf. 15.6.4 *} - Cons: "\G\Norm s0 \e -\ v \ s1; +| Cons: "\G\Norm s0 \e -\ v \ s1; G\ s1 \es\\vs\ s2\ \ G\Norm s0 \e#es\\v#vs\ s2" @@ -794,17 +765,17 @@ declare split_if [split del] split_if_asm [split del] option.split [split del] option.split_asm [split del] -inductive_cases halloc_elim_cases: +inductive_cases2 halloc_elim_cases: "G\(Some xc,s) \halloc oi\a\ s'" "G\(Norm s) \halloc oi\a\ s'" -inductive_cases sxalloc_elim_cases: +inductive_cases2 sxalloc_elim_cases: "G\ Norm s \sxalloc\ s'" "G\(Some (Jump j),s) \sxalloc\ s'" "G\(Some (Error e),s) \sxalloc\ s'" "G\(Some (Xcpt (Loc a )),s) \sxalloc\ s'" "G\(Some (Xcpt (Std xn)),s) \sxalloc\ s'" -inductive_cases sxalloc_cases: "G\s \sxalloc\ s'" +inductive_cases2 sxalloc_cases: "G\s \sxalloc\ s'" lemma sxalloc_elim_cases2: "\G\s \sxalloc\ s'; \s. \s' = Norm s\ \ P; @@ -822,40 +793,40 @@ ML_setup {* change_simpset (fn ss => ss delloop "split_all_tac"); *} -inductive_cases eval_cases: "G\s \t\\ vs'" +inductive_cases2 eval_cases: "G\s \t\\ (v, s')" -inductive_cases eval_elim_cases [cases set]: - "G\(Some xc,s) \t \\ vs'" - "G\Norm s \In1r Skip \\ xs'" - "G\Norm s \In1r (Jmp j) \\ xs'" - "G\Norm s \In1r (l\ c) \\ xs'" - "G\Norm s \In3 ([]) \\ vs'" - "G\Norm s \In3 (e#es) \\ vs'" - "G\Norm s \In1l (Lit w) \\ vs'" - "G\Norm s \In1l (UnOp unop e) \\ vs'" - "G\Norm s \In1l (BinOp binop e1 e2) \\ vs'" - "G\Norm s \In2 (LVar vn) \\ vs'" - "G\Norm s \In1l (Cast T e) \\ vs'" - "G\Norm s \In1l (e InstOf T) \\ vs'" - "G\Norm s \In1l (Super) \\ vs'" - "G\Norm s \In1l (Acc va) \\ vs'" - "G\Norm s \In1r (Expr e) \\ xs'" - "G\Norm s \In1r (c1;; c2) \\ xs'" - "G\Norm s \In1l (Methd C sig) \\ xs'" - "G\Norm s \In1l (Body D c) \\ xs'" - "G\Norm s \In1l (e0 ? e1 : e2) \\ vs'" - "G\Norm s \In1r (If(e) c1 Else c2) \\ xs'" - "G\Norm s \In1r (l\ While(e) c) \\ xs'" - "G\Norm s \In1r (c1 Finally c2) \\ xs'" - "G\Norm s \In1r (Throw e) \\ xs'" - "G\Norm s \In1l (NewC C) \\ vs'" - "G\Norm s \In1l (New T[e]) \\ vs'" - "G\Norm s \In1l (Ass va e) \\ vs'" - "G\Norm s \In1r (Try c1 Catch(tn vn) c2) \\ xs'" - "G\Norm s \In2 ({accC,statDeclC,stat}e..fn) \\ vs'" - "G\Norm s \In2 (e1.[e2]) \\ vs'" - "G\Norm s \In1l ({accC,statT,mode}e\mn({pT}p)) \\ vs'" - "G\Norm s \In1r (Init C) \\ xs'" +inductive_cases2 eval_elim_cases [cases set]: + "G\(Some xc,s) \t \\ (v, s')" + "G\Norm s \In1r Skip \\ (x, s')" + "G\Norm s \In1r (Jmp j) \\ (x, s')" + "G\Norm s \In1r (l\ c) \\ (x, s')" + "G\Norm s \In3 ([]) \\ (v, s')" + "G\Norm s \In3 (e#es) \\ (v, s')" + "G\Norm s \In1l (Lit w) \\ (v, s')" + "G\Norm s \In1l (UnOp unop e) \\ (v, s')" + "G\Norm s \In1l (BinOp binop e1 e2) \\ (v, s')" + "G\Norm s \In2 (LVar vn) \\ (v, s')" + "G\Norm s \In1l (Cast T e) \\ (v, s')" + "G\Norm s \In1l (e InstOf T) \\ (v, s')" + "G\Norm s \In1l (Super) \\ (v, s')" + "G\Norm s \In1l (Acc va) \\ (v, s')" + "G\Norm s \In1r (Expr e) \\ (x, s')" + "G\Norm s \In1r (c1;; c2) \\ (x, s')" + "G\Norm s \In1l (Methd C sig) \\ (x, s')" + "G\Norm s \In1l (Body D c) \\ (x, s')" + "G\Norm s \In1l (e0 ? e1 : e2) \\ (v, s')" + "G\Norm s \In1r (If(e) c1 Else c2) \\ (x, s')" + "G\Norm s \In1r (l\ While(e) c) \\ (x, s')" + "G\Norm s \In1r (c1 Finally c2) \\ (x, s')" + "G\Norm s \In1r (Throw e) \\ (x, s')" + "G\Norm s \In1l (NewC C) \\ (v, s')" + "G\Norm s \In1l (New T[e]) \\ (v, s')" + "G\Norm s \In1l (Ass va e) \\ (v, s')" + "G\Norm s \In1r (Try c1 Catch(tn vn) c2) \\ (x, s')" + "G\Norm s \In2 ({accC,statDeclC,stat}e..fn) \\ (v, s')" + "G\Norm s \In2 (e1.[e2]) \\ (v, s')" + "G\Norm s \In1l ({accC,statT,mode}e\mn({pT}p)) \\ (v, s')" + "G\Norm s \In1r (Init C) \\ (x, s')" declare not_None_eq [simp] (* IntDef.Zero_def [simp] *) declare split_paired_All [simp] split_paired_Ex [simp] ML_setup {* @@ -885,25 +856,33 @@ (injection @{term In1l} into terms) always evaluates to ordinary values (injection @{term In1} into generalised values @{term vals}). *} + +lemma eval_expr_eq: "G\s \In1l t\\ (w, s') = (\v. w=In1 v \ G\s \t-\v \ s')" + by (auto, frule eval_Inj_elim, auto) + +lemma eval_var_eq: "G\s \In2 t\\ (w, s') = (\vf. w=In2 vf \ G\s \t=\vf\ s')" + by (auto, frule eval_Inj_elim, auto) + +lemma eval_exprs_eq: "G\s \In3 t\\ (w, s') = (\vs. w=In3 vs \ G\s \t\\vs\ s')" + by (auto, frule eval_Inj_elim, auto) + +lemma eval_stmt_eq: "G\s \In1r t\\ (w, s') = (w=\ \ G\s \t \ s')" + by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto) + ML_setup {* -fun eval_fun nam inj rhs = +fun eval_fun name lhs = let - val name = "eval_" ^ nam ^ "_eq" - val lhs = "G\s \" ^ inj ^ " t\\ (w, s')" - val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") - (K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac]) fun is_Inj (Const (inj,_) $ _) = true | is_Inj _ = false - fun pred (_ $ (Const ("Pair",_) $ _ $ - (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x + fun pred (_ $ _ $ _ $ _ $ x $ _) = is_Inj x in cond_simproc name lhs pred (thm name) end -val eval_expr_proc =eval_fun "expr" "In1l" "\v. w=In1 v \ G\s \t-\v \ s'" -val eval_var_proc =eval_fun "var" "In2" "\vf. w=In2 vf \ G\s \t=\vf\ s'" -val eval_exprs_proc=eval_fun "exprs""In3" "\vs. w=In3 vs \ G\s \t\\vs\ s'" -val eval_stmt_proc =eval_fun "stmt" "In1r" " w=\ \ G\s \t \ s'"; +val eval_expr_proc = eval_fun "eval_expr_eq" "G\s \In1l t\\ (w, s')"; +val eval_var_proc = eval_fun "eval_var_eq" "G\s \In2 t\\ (w, s')"; +val eval_exprs_proc = eval_fun "eval_exprs_eq" "G\s \In3 t\\ (w, s')"; +val eval_stmt_proc = eval_fun "eval_stmt_eq" "G\s \In1r t\\ (w, s')"; Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc]; bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt")) *} @@ -922,9 +901,7 @@ assume eval: "G\s \t\\ (v,s')" and normal: "normal s" and callee: "t=In1l (Callee l e)" - then have "False" - proof (induct) - qed (auto) + then have "False" by induct auto } then show ?thesis by (cases s') fastsimp @@ -937,9 +914,7 @@ assume eval: "G\s \t\\ (v,s')" and normal: "normal s" and callee: "t=In1l (InsInitE c e)" - then have "False" - proof (induct) - qed (auto) + then have "False" by induct auto } then show ?thesis by (cases s') fastsimp @@ -951,9 +926,7 @@ assume eval: "G\s \t\\ (v,s')" and normal: "normal s" and callee: "t=In2 (InsInitV c w)" - then have "False" - proof (induct) - qed (auto) + then have "False" by induct auto } then show ?thesis by (cases s') fastsimp @@ -965,9 +938,7 @@ assume eval: "G\s \t\\ (v,s')" and normal: "normal s" and callee: "t=In1r (FinA a c)" - then have "False" - proof (induct) - qed (auto) + then have "False" by induct auto } then show ?thesis by (cases s') fastsimp @@ -988,8 +959,7 @@ local fun is_None (Const ("Datatype.option.None",_)) = true | is_None _ = false - fun pred (t as (_ $ (Const ("Pair",_) $ - (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x + fun pred (_ $ _ $ (Const ("Pair", _) $ x $ _) $ _ $ _ $ _) = is_None x in val eval_no_abrupt_proc = cond_simproc "eval_no_abrupt" "G\(x,s) \e\\ (w,Norm s')" pred @@ -1015,9 +985,7 @@ local fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true | is_Some _ = false - fun pred (_ $ (Const ("Pair",_) $ - _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $ - x))) $ _ ) = is_Some x + fun pred (_ $ _ $ _ $ _ $ _ $ x) = is_Some x in val eval_abrupt_proc = cond_simproc "eval_abrupt" @@ -1174,8 +1142,7 @@ section "single valued" lemma unique_halloc [rule_format (no_asm)]: - "\s as as'. (s,oi,as)\halloc G \ (s,oi,as')\halloc G \ as'=as" -apply (simp (no_asm_simp) only: split_tupled_all) + "G\s \halloc oi\a \ s' \ G\s \halloc oi\a' \ s'' \ a' = a \ s'' = s'" apply (erule halloc.induct) apply (auto elim!: halloc_elim_cases split del: split_if split_if_asm) apply (drule trans [THEN sym], erule sym) @@ -1192,8 +1159,7 @@ lemma unique_sxalloc [rule_format (no_asm)]: - "\s s'. G\s \sxalloc\ s' \ G\s \sxalloc\ s'' \ s'' = s'" -apply (simp (no_asm_simp) only: split_tupled_all) + "G\s \sxalloc\ s' \ G\s \sxalloc\ s'' \ s'' = s'" apply (erule sxalloc.induct) apply (auto dest: unique_halloc elim!: sxalloc_elim_cases split del: split_if split_if_asm) @@ -1210,9 +1176,7 @@ lemma unique_eval [rule_format (no_asm)]: - "G\s \t\\ ws \ (\ws'. G\s \t\\ ws' \ ws' = ws)" -apply (case_tac "ws") -apply hypsubst + "G\s \t\\ (w, s') \ (\w' s''. G\s \t\\ (w', s'') \ w' = w \ s'' = s')" apply (erule eval_induct) apply (tactic {* ALLGOALS (EVERY' [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *}) @@ -1221,19 +1185,16 @@ apply (simp (no_asm_use) only: split add: split_if_asm) (* 34 subgoals *) prefer 30 (* Init *) -apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+) +apply (case_tac "inited C (globs s0)", (simp only: if_True if_False simp_thms)+) prefer 26 (* While *) apply (simp (no_asm_use) only: split add: split_if_asm, blast) -apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp) -apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp) -apply blast -(* 33 subgoals *) +(* 36 subgoals *) apply (blast dest: unique_sxalloc unique_halloc split_pairD)+ done (* unused *) lemma single_valued_eval: - "single_valued {((s,t),vs'). G\s \t\\ vs'}" + "single_valued {((s, t), (v, s')). G\s \t\\ (v, s')}" apply (unfold single_valued_def) by (clarify, drule (1) unique_eval, auto) diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/Evaln.thy Mon Dec 11 16:06:14 2006 +0100 @@ -28,68 +28,40 @@ for welltyped, and definitely assigned terms. *} -consts - - evaln :: "prog \ (state \ term \ nat \ vals \ state) set" - -syntax - - evaln :: "[prog, state, term, nat, vals * state] => bool" - ("_|-_ -_>-_-> _" [61,61,80, 61,61] 60) - evarn :: "[prog, state, var , vvar , nat, state] => bool" - ("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60) - eval_n:: "[prog, state, expr , val , nat, state] => bool" - ("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60) - evalsn:: "[prog, state, expr list, val list, nat, state] => bool" - ("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60) - execn :: "[prog, state, stmt , nat, state] => bool" - ("_|-_ -_-_-> _" [61,61,65, 61,61] 60) - -syntax (xsymbols) +inductive2 + evaln :: "[prog, state, term, nat, vals, state] \ bool" + ("_\_ \_\\_\ '(_, _')" [61,61,80,61,0,0] 60) + and evarn :: "[prog, state, var, vvar, nat, state] \ bool" + ("_\_ \_=\_\_\ _" [61,61,90,61,61,61] 60) + and eval_n:: "[prog, state, expr, val, nat, state] \ bool" + ("_\_ \_-\_\_\ _" [61,61,80,61,61,61] 60) + and evalsn :: "[prog, state, expr list, val list, nat, state] \ bool" + ("_\_ \_\\_\_\ _" [61,61,61,61,61,61] 60) + and execn :: "[prog, state, stmt, nat, state] \ bool" + ("_\_ \_\_\ _" [61,61,65, 61,61] 60) + for G :: prog +where - evaln :: "[prog, state, term, nat, vals \ state] \ bool" - ("_\_ \_\\_\ _" [61,61,80, 61,61] 60) - evarn :: "[prog, state, var , vvar , nat, state] \ bool" - ("_\_ \_=\_\_\ _" [61,61,90,61,61,61] 60) - eval_n:: "[prog, state, expr , val , nat, state] \ bool" - ("_\_ \_-\_\_\ _" [61,61,80,61,61,61] 60) - evalsn:: "[prog, state, expr list, val list, nat, state] \ bool" - ("_\_ \_\\_\_\ _" [61,61,61,61,61,61] 60) - execn :: "[prog, state, stmt , nat, state] \ bool" - ("_\_ \_\_\ _" [61,61,65, 61,61] 60) - -translations - - "G\s \t \\n\ w___s' " == "(s,t,n,w___s') \ evaln G" - "G\s \t \\n\ (w, s')" <= "(s,t,n,w, s') \ evaln G" - "G\s \t \\n\ (w,x,s')" <= "(s,t,n,w,x,s') \ evaln G" - "G\s \c \n\ (x,s')" <= "G\s \In1r c\\n\ (\ ,x,s')" - "G\s \c \n\ s' " == "G\s \In1r c\\n\ (\ , s')" - "G\s \e-\v \n\ (x,s')" <= "G\s \In1l e\\n\ (In1 v ,x,s')" - "G\s \e-\v \n\ s' " == "G\s \In1l e\\n\ (In1 v , s')" - "G\s \e=\vf \n\ (x,s')" <= "G\s \In2 e\\n\ (In2 vf,x,s')" - "G\s \e=\vf \n\ s' " == "G\s \In2 e\\n\ (In2 vf, s')" - "G\s \e\\v \n\ (x,s')" <= "G\s \In3 e\\n\ (In3 v ,x,s')" - "G\s \e\\v \n\ s' " == "G\s \In3 e\\n\ (In3 v , s')" - - -inductive "evaln G" intros + "G\s \c \n\ s' \ G\s \In1r c\\n\ (\ , s')" +| "G\s \e-\v \n\ s' \ G\s \In1l e\\n\ (In1 v , s')" +| "G\s \e=\vf \n\ s' \ G\s \In2 e\\n\ (In2 vf, s')" +| "G\s \e\\v \n\ s' \ G\s \In3 e\\n\ (In3 v , s')" --{* propagation of abrupt completion *} - Abrupt: "G\(Some xc,s) \t\\n\ (arbitrary3 t,(Some xc,s))" +| Abrupt: "G\(Some xc,s) \t\\n\ (arbitrary3 t,(Some xc,s))" --{* evaluation of variables *} - LVar: "G\Norm s \LVar vn=\lvar vn s\n\ Norm s" +| LVar: "G\Norm s \LVar vn=\lvar vn s\n\ Norm s" - FVar: "\G\Norm s0 \Init statDeclC\n\ s1; G\s1 \e-\a\n\ s2; +| FVar: "\G\Norm s0 \Init statDeclC\n\ s1; G\s1 \e-\a\n\ s2; (v,s2') = fvar statDeclC stat fn a s2; s3 = check_field_access G accC statDeclC fn stat a s2'\ \ G\Norm s0 \{accC,statDeclC,stat}e..fn=\v\n\ s3" - AVar: "\G\ Norm s0 \e1-\a\n\ s1 ; G\s1 \e2-\i\n\ s2; +| AVar: "\G\ Norm s0 \e1-\a\n\ s1 ; G\s1 \e2-\i\n\ s2; (v,s2') = avar G i a s2\ \ G\Norm s0 \e1.[e2]=\v\n\ s2'" @@ -98,46 +70,46 @@ --{* evaluation of expressions *} - NewC: "\G\Norm s0 \Init C\n\ s1; +| NewC: "\G\Norm s0 \Init C\n\ s1; G\ s1 \halloc (CInst C)\a\ s2\ \ G\Norm s0 \NewC C-\Addr a\n\ s2" - NewA: "\G\Norm s0 \init_comp_ty T\n\ s1; G\s1 \e-\i'\n\ s2; +| NewA: "\G\Norm s0 \init_comp_ty T\n\ s1; G\s1 \e-\i'\n\ s2; G\abupd (check_neg i') s2 \halloc (Arr T (the_Intg i'))\a\ s3\ \ G\Norm s0 \New T[e]-\Addr a\n\ s3" - Cast: "\G\Norm s0 \e-\v\n\ s1; +| Cast: "\G\Norm s0 \e-\v\n\ s1; s2 = abupd (raise_if (\G,snd s1\v fits T) ClassCast) s1\ \ G\Norm s0 \Cast T e-\v\n\ s2" - Inst: "\G\Norm s0 \e-\v\n\ s1; +| Inst: "\G\Norm s0 \e-\v\n\ s1; b = (v\Null \ G,store s1\v fits RefT T)\ \ G\Norm s0 \e InstOf T-\Bool b\n\ s1" - Lit: "G\Norm s \Lit v-\v\n\ Norm s" +| Lit: "G\Norm s \Lit v-\v\n\ Norm s" - UnOp: "\G\Norm s0 \e-\v\n\ s1\ +| UnOp: "\G\Norm s0 \e-\v\n\ s1\ \ G\Norm s0 \UnOp unop e-\(eval_unop unop v)\n\ s1" - BinOp: "\G\Norm s0 \e1-\v1\n\ s1; +| BinOp: "\G\Norm s0 \e1-\v1\n\ s1; G\s1 \(if need_second_arg binop v1 then (In1l e2) else (In1r Skip)) \\n\ (In1 v2,s2)\ \ G\Norm s0 \BinOp binop e1 e2-\(eval_binop binop v1 v2)\n\ s2" - Super: "G\Norm s \Super-\val_this s\n\ Norm s" +| Super: "G\Norm s \Super-\val_this s\n\ Norm s" - Acc: "\G\Norm s0 \va=\(v,f)\n\ s1\ \ +| Acc: "\G\Norm s0 \va=\(v,f)\n\ s1\ \ G\Norm s0 \Acc va-\v\n\ s1" - Ass: "\G\Norm s0 \va=\(w,f)\n\ s1; +| Ass: "\G\Norm s0 \va=\(w,f)\n\ s1; G\ s1 \e-\v \n\ s2\ \ G\Norm s0 \va:=e-\v\n\ assign f v s2" - Cond: "\G\Norm s0 \e0-\b\n\ s1; +| Cond: "\G\Norm s0 \e0-\b\n\ s1; G\ s1 \(if the_Bool b then e1 else e2)-\v\n\ s2\ \ G\Norm s0 \e0 ? e1 : e2-\v\n\ s2" - Call: +| Call: "\G\Norm s0 \e-\a'\n\ s1; G\s1 \args\\vs\n\ s2; D = invocation_declclass G mode (store s2) a' statT \name=mn,parTs=pTs\; s3=init_lvars G D \name=mn,parTs=pTs\ mode a' vs s2; @@ -147,10 +119,10 @@ \ G\Norm s0 \{accC,statT,mode}e\mn({pTs}args)-\v\n\ (restore_lvars s2 s4)" - Methd:"\G\Norm s0 \body G D sig-\v\n\ s1\ \ +| Methd:"\G\Norm s0 \body G D sig-\v\n\ s1\ \ G\Norm s0 \Methd D sig-\v\Suc n\ s1" - Body: "\G\Norm s0\Init D\n\ s1; G\s1 \c\n\ s2; +| Body: "\G\Norm s0\Init D\n\ s1; G\s1 \c\n\ s2; s3 = (if (\ l. abrupt s2 = Some (Jump (Break l)) \ abrupt s2 = Some (Jump (Cont l))) then abupd (\ x. Some (Error CrossMethodJump)) s2 @@ -160,57 +132,57 @@ --{* evaluation of expression lists *} - Nil: +| Nil: "G\Norm s0 \[]\\[]\n\ Norm s0" - Cons: "\G\Norm s0 \e -\ v \n\ s1; +| Cons: "\G\Norm s0 \e -\ v \n\ s1; G\ s1 \es\\vs\n\ s2\ \ G\Norm s0 \e#es\\v#vs\n\ s2" --{* execution of statements *} - Skip: "G\Norm s \Skip\n\ Norm s" +| Skip: "G\Norm s \Skip\n\ Norm s" - Expr: "\G\Norm s0 \e-\v\n\ s1\ \ +| Expr: "\G\Norm s0 \e-\v\n\ s1\ \ G\Norm s0 \Expr e\n\ s1" - Lab: "\G\Norm s0 \c \n\ s1\ \ +| Lab: "\G\Norm s0 \c \n\ s1\ \ G\Norm s0 \l\ c\n\ abupd (absorb l) s1" - Comp: "\G\Norm s0 \c1 \n\ s1; +| Comp: "\G\Norm s0 \c1 \n\ s1; G\ s1 \c2 \n\ s2\ \ G\Norm s0 \c1;; c2\n\ s2" - If: "\G\Norm s0 \e-\b\n\ s1; +| If: "\G\Norm s0 \e-\b\n\ s1; G\ s1\(if the_Bool b then c1 else c2)\n\ s2\ \ G\Norm s0 \If(e) c1 Else c2 \n\ s2" - Loop: "\G\Norm s0 \e-\b\n\ s1; +| Loop: "\G\Norm s0 \e-\b\n\ s1; if the_Bool b then (G\s1 \c\n\ s2 \ G\(abupd (absorb (Cont l)) s2) \l\ While(e) c\n\ s3) else s3 = s1\ \ G\Norm s0 \l\ While(e) c\n\ s3" - Jmp: "G\Norm s \Jmp j\n\ (Some (Jump j), s)" +| Jmp: "G\Norm s \Jmp j\n\ (Some (Jump j), s)" - Throw:"\G\Norm s0 \e-\a'\n\ s1\ \ +| Throw:"\G\Norm s0 \e-\a'\n\ s1\ \ G\Norm s0 \Throw e\n\ abupd (throw a') s1" - Try: "\G\Norm s0 \c1\n\ s1; G\s1 \sxalloc\ s2; +| Try: "\G\Norm s0 \c1\n\ s1; G\s1 \sxalloc\ s2; if G,s2\catch tn then G\new_xcpt_var vn s2 \c2\n\ s3 else s3 = s2\ \ G\Norm s0 \Try c1 Catch(tn vn) c2\n\ s3" - Fin: "\G\Norm s0 \c1\n\ (x1,s1); +| Fin: "\G\Norm s0 \c1\n\ (x1,s1); G\Norm s1 \c2\n\ s2; s3=(if (\ err. x1=Some (Error err)) then (x1,s1) else abupd (abrupt_if (x1\None) x1) s2)\ \ G\Norm s0 \c1 Finally c2\n\ s3" - Init: "\the (class G C) = c; +| Init: "\the (class G C) = c; if inited C (globs s0) then s3 = Norm s0 else (G\Norm (init_class_obj G C s0) \(if C = Object then Skip else Init (super c))\n\ s1 \ @@ -229,41 +201,41 @@ ML_setup {* change_simpset (fn ss => ss delloop "split_all_tac"); *} -inductive_cases evaln_cases: "G\s \t\\n\ vs'" +inductive_cases2 evaln_cases: "G\s \t\\n\ (v, s')" -inductive_cases evaln_elim_cases: - "G\(Some xc, s) \t \\n\ vs'" - "G\Norm s \In1r Skip \\n\ xs'" - "G\Norm s \In1r (Jmp j) \\n\ xs'" - "G\Norm s \In1r (l\ c) \\n\ xs'" - "G\Norm s \In3 ([]) \\n\ vs'" - "G\Norm s \In3 (e#es) \\n\ vs'" - "G\Norm s \In1l (Lit w) \\n\ vs'" - "G\Norm s \In1l (UnOp unop e) \\n\ vs'" - "G\Norm s \In1l (BinOp binop e1 e2) \\n\ vs'" - "G\Norm s \In2 (LVar vn) \\n\ vs'" - "G\Norm s \In1l (Cast T e) \\n\ vs'" - "G\Norm s \In1l (e InstOf T) \\n\ vs'" - "G\Norm s \In1l (Super) \\n\ vs'" - "G\Norm s \In1l (Acc va) \\n\ vs'" - "G\Norm s \In1r (Expr e) \\n\ xs'" - "G\Norm s \In1r (c1;; c2) \\n\ xs'" - "G\Norm s \In1l (Methd C sig) \\n\ xs'" - "G\Norm s \In1l (Body D c) \\n\ xs'" - "G\Norm s \In1l (e0 ? e1 : e2) \\n\ vs'" - "G\Norm s \In1r (If(e) c1 Else c2) \\n\ xs'" - "G\Norm s \In1r (l\ While(e) c) \\n\ xs'" - "G\Norm s \In1r (c1 Finally c2) \\n\ xs'" - "G\Norm s \In1r (Throw e) \\n\ xs'" - "G\Norm s \In1l (NewC C) \\n\ vs'" - "G\Norm s \In1l (New T[e]) \\n\ vs'" - "G\Norm s \In1l (Ass va e) \\n\ vs'" - "G\Norm s \In1r (Try c1 Catch(tn vn) c2) \\n\ xs'" - "G\Norm s \In2 ({accC,statDeclC,stat}e..fn) \\n\ vs'" - "G\Norm s \In2 (e1.[e2]) \\n\ vs'" - "G\Norm s \In1l ({accC,statT,mode}e\mn({pT}p)) \\n\ vs'" - "G\Norm s \In1r (Init C) \\n\ xs'" - "G\Norm s \In1r (Init C) \\n\ xs'" +inductive_cases2 evaln_elim_cases: + "G\(Some xc, s) \t \\n\ (v, s')" + "G\Norm s \In1r Skip \\n\ (x, s')" + "G\Norm s \In1r (Jmp j) \\n\ (x, s')" + "G\Norm s \In1r (l\ c) \\n\ (x, s')" + "G\Norm s \In3 ([]) \\n\ (v, s')" + "G\Norm s \In3 (e#es) \\n\ (v, s')" + "G\Norm s \In1l (Lit w) \\n\ (v, s')" + "G\Norm s \In1l (UnOp unop e) \\n\ (v, s')" + "G\Norm s \In1l (BinOp binop e1 e2) \\n\ (v, s')" + "G\Norm s \In2 (LVar vn) \\n\ (v, s')" + "G\Norm s \In1l (Cast T e) \\n\ (v, s')" + "G\Norm s \In1l (e InstOf T) \\n\ (v, s')" + "G\Norm s \In1l (Super) \\n\ (v, s')" + "G\Norm s \In1l (Acc va) \\n\ (v, s')" + "G\Norm s \In1r (Expr e) \\n\ (x, s')" + "G\Norm s \In1r (c1;; c2) \\n\ (x, s')" + "G\Norm s \In1l (Methd C sig) \\n\ (x, s')" + "G\Norm s \In1l (Body D c) \\n\ (x, s')" + "G\Norm s \In1l (e0 ? e1 : e2) \\n\ (v, s')" + "G\Norm s \In1r (If(e) c1 Else c2) \\n\ (x, s')" + "G\Norm s \In1r (l\ While(e) c) \\n\ (x, s')" + "G\Norm s \In1r (c1 Finally c2) \\n\ (x, s')" + "G\Norm s \In1r (Throw e) \\n\ (x, s')" + "G\Norm s \In1l (NewC C) \\n\ (v, s')" + "G\Norm s \In1l (New T[e]) \\n\ (v, s')" + "G\Norm s \In1l (Ass va e) \\n\ (v, s')" + "G\Norm s \In1r (Try c1 Catch(tn vn) c2) \\n\ (x, s')" + "G\Norm s \In2 ({accC,statDeclC,stat}e..fn) \\n\ (v, s')" + "G\Norm s \In2 (e1.[e2]) \\n\ (v, s')" + "G\Norm s \In1l ({accC,statT,mode}e\mn({pT}p)) \\n\ (v, s')" + "G\Norm s \In1r (Init C) \\n\ (x, s')" + "G\Norm s \In1r (Init C) \\n\ (x, s')" declare split_if [split] split_if_asm [split] option.split [split] option.split_asm [split] @@ -288,25 +260,32 @@ (injection @{term In1} into generalised values @{term vals}). *} +lemma evaln_expr_eq: "G\s \In1l t\\n\ (w, s') = (\v. w=In1 v \ G\s \t-\v \n\ s')" + by (auto, frule evaln_Inj_elim, auto) + +lemma evaln_var_eq: "G\s \In2 t\\n\ (w, s') = (\vf. w=In2 vf \ G\s \t=\vf\n\ s')" + by (auto, frule evaln_Inj_elim, auto) + +lemma evaln_exprs_eq: "G\s \In3 t\\n\ (w, s') = (\vs. w=In3 vs \ G\s \t\\vs\n\ s')" + by (auto, frule evaln_Inj_elim, auto) + +lemma evaln_stmt_eq: "G\s \In1r t\\n\ (w, s') = (w=\ \ G\s \t \n\ s')" + by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto) + ML_setup {* -fun enf nam inj rhs = +fun enf name lhs = let - val name = "evaln_" ^ nam ^ "_eq" - val lhs = "G\s \" ^ inj ^ " t\\n\ (w, s')" - val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") - (K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac]) fun is_Inj (Const (inj,_) $ _) = true | is_Inj _ = false - fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ - (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x + fun pred (_ $ _ $ _ $ _ $ _ $ x $ _) = is_Inj x in cond_simproc name lhs pred (thm name) end; -val evaln_expr_proc = enf "expr" "In1l" "\v. w=In1 v \ G\s \t-\v \n\ s'"; -val evaln_var_proc = enf "var" "In2" "\vf. w=In2 vf \ G\s \t=\vf\n\ s'"; -val evaln_exprs_proc= enf "exprs""In3" "\vs. w=In3 vs \ G\s \t\\vs\n\ s'"; -val evaln_stmt_proc = enf "stmt" "In1r" " w=\ \ G\s \t \n\ s'"; +val evaln_expr_proc = enf "evaln_expr_eq" "G\s \In1l t\\n\ (w, s')"; +val evaln_var_proc = enf "evaln_var_eq" "G\s \In2 t\\n\ (w, s')"; +val evaln_exprs_proc = enf "evaln_exprs_eq" "G\s \In3 t\\n\ (w, s')"; +val evaln_stmt_proc = enf "evaln_stmt_eq" "G\s \In1r t\\n\ (w, s')"; Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc]; bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt")) @@ -319,9 +298,7 @@ assume eval: "G\s \t\\n\ (v,s')" and normal: "normal s" and callee: "t=In1l (Callee l e)" - then have "False" - proof (induct) - qed (auto) + then have "False" by induct auto } then show ?thesis by (cases s') fastsimp @@ -333,9 +310,7 @@ assume eval: "G\s \t\\n\ (v,s')" and normal: "normal s" and callee: "t=In1l (InsInitE c e)" - then have "False" - proof (induct) - qed (auto) + then have "False" by induct auto } then show ?thesis by (cases s') fastsimp @@ -347,9 +322,7 @@ assume eval: "G\s \t\\n\ (v,s')" and normal: "normal s" and callee: "t=In2 (InsInitV c w)" - then have "False" - proof (induct) - qed (auto) + then have "False" by induct auto } then show ?thesis by (cases s') fastsimp @@ -361,9 +334,7 @@ assume eval: "G\s \t\\n\ (v,s')" and normal: "normal s" and callee: "t=In1r (FinA a c)" - then have "False" - proof (induct) - qed (auto) + then have "False" by induct auto } then show ?thesis by (cases s') fastsimp @@ -385,9 +356,7 @@ local fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true | is_Some _ = false - fun pred (_ $ (Const ("Pair",_) $ - _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $ - (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x + fun pred (_ $ _ $ _ $ _ $ _ $ _ $ x) = is_Some x in val evaln_abrupt_proc = cond_simproc "evaln_abrupt" "G\(Some xc,s) \e\\n\ (w,s')" pred (thm "evaln_abrupt") @@ -440,7 +409,7 @@ shows "G\s0 \t\\ (v,s1)" using evaln proof (induct) - case (Loop b c e l n s0 s1 s2 s3) + case (Loop s0 e n b s1 c s2 l s3) have "G\Norm s0 \e-\b\ s1". moreover have "if the_Bool b @@ -450,7 +419,7 @@ using Loop.hyps by simp ultimately show ?case by (rule eval.Loop) next - case (Try c1 c2 n s0 s1 s2 s3 C vn) + case (Try s0 c1 n s1 s2 C vn c2 s3) have "G\Norm s0 \c1\ s1". moreover have "G\s1 \sxalloc\ s2". @@ -459,7 +428,7 @@ using Try.hyps by simp ultimately show ?case by (rule eval.Try) next - case (Init C c n s0 s1 s2 s3) + case (Init C c s0 s3 n s1 s2) have "the (class G C) = c". moreover have "if inited C (globs s0) @@ -478,8 +447,7 @@ done lemma evaln_nonstrict [rule_format (no_asm), elim]: - "\ws. G\s \t\\n\ ws \ \m. n\m \ G\s \t\\m\ ws" -apply (simp (no_asm_simp) only: split_tupled_all) + "G\s \t\\n\ (w, s') \ \m. n\m \ G\s \t\\m\ (w, s')" apply (erule evaln.induct) apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"), REPEAT o smp_tac 1, @@ -490,30 +458,30 @@ lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]] -lemma evaln_max2: "\G\s1 \t1\\n1\ ws1; G\s2 \t2\\n2\ ws2\ \ - G\s1 \t1\\max n1 n2\ ws1 \ G\s2 \t2\\max n1 n2\ ws2" +lemma evaln_max2: "\G\s1 \t1\\n1\ (w1, s1'); G\s2 \t2\\n2\ (w2, s2')\ \ + G\s1 \t1\\max n1 n2\ (w1, s1') \ G\s2 \t2\\max n1 n2\ (w2, s2')" by (fast intro: le_maxI1 le_maxI2) corollary evaln_max2E [consumes 2]: - "\G\s1 \t1\\n1\ ws1; G\s2 \t2\\n2\ ws2; - \G\s1 \t1\\max n1 n2\ ws1;G\s2 \t2\\max n1 n2\ ws2 \ \ P \ \ P" + "\G\s1 \t1\\n1\ (w1, s1'); G\s2 \t2\\n2\ (w2, s2'); + \G\s1 \t1\\max n1 n2\ (w1, s1');G\s2 \t2\\max n1 n2\ (w2, s2') \ \ P \ \ P" by (drule (1) evaln_max2) simp lemma evaln_max3: -"\G\s1 \t1\\n1\ ws1; G\s2 \t2\\n2\ ws2; G\s3 \t3\\n3\ ws3\ \ - G\s1 \t1\\max (max n1 n2) n3\ ws1 \ - G\s2 \t2\\max (max n1 n2) n3\ ws2 \ - G\s3 \t3\\max (max n1 n2) n3\ ws3" +"\G\s1 \t1\\n1\ (w1, s1'); G\s2 \t2\\n2\ (w2, s2'); G\s3 \t3\\n3\ (w3, s3')\ \ + G\s1 \t1\\max (max n1 n2) n3\ (w1, s1') \ + G\s2 \t2\\max (max n1 n2) n3\ (w2, s2') \ + G\s3 \t3\\max (max n1 n2) n3\ (w3, s3')" apply (drule (1) evaln_max2, erule thin_rl) apply (fast intro!: le_maxI1 le_maxI2) done corollary evaln_max3E: -"\G\s1 \t1\\n1\ ws1; G\s2 \t2\\n2\ ws2; G\s3 \t3\\n3\ ws3; - \G\s1 \t1\\max (max n1 n2) n3\ ws1; - G\s2 \t2\\max (max n1 n2) n3\ ws2; - G\s3 \t3\\max (max n1 n2) n3\ ws3 +"\G\s1 \t1\\n1\ (w1, s1'); G\s2 \t2\\n2\ (w2, s2'); G\s3 \t3\\n3\ (w3, s3'); + \G\s1 \t1\\max (max n1 n2) n3\ (w1, s1'); + G\s2 \t2\\max (max n1 n2) n3\ (w2, s2'); + G\s3 \t3\\max (max n1 n2) n3\ (w3, s3') \ \ P \ \ P" by (drule (2) evaln_max3) simp @@ -551,16 +519,16 @@ shows "\n. G\s0 \t\\n\ (v,s1)" using eval proof (induct) - case (Abrupt s t xc) + case (Abrupt xc s t) obtain n where - "G\(Some xc, s) \t\\n\ (arbitrary3 t, Some xc, s)" + "G\(Some xc, s) \t\\n\ (arbitrary3 t, (Some xc, s))" by (iprover intro: evaln.Abrupt) then show ?case .. next case Skip show ?case by (blast intro: evaln.Skip) next - case (Expr e s0 s1 v) + case (Expr s0 e v s1) then obtain n where "G\Norm s0 \e-\v\n\ s1" by (iprover) @@ -568,7 +536,7 @@ by (rule evaln.Expr) then show ?case .. next - case (Lab c l s0 s1) + case (Lab s0 c s1 l) then obtain n where "G\Norm s0 \c\n\ s1" by (iprover) @@ -576,7 +544,7 @@ by (rule evaln.Lab) then show ?case .. next - case (Comp c1 c2 s0 s1 s2) + case (Comp s0 c1 s1 c2 s2) then obtain n1 n2 where "G\Norm s0 \c1\n1\ s1" "G\s1 \c2\n2\ s2" @@ -585,7 +553,7 @@ by (blast intro: evaln.Comp dest: evaln_max2 ) then show ?case .. next - case (If b c1 c2 e s0 s1 s2) + case (If s0 e b s1 c1 c2 s2) then obtain n1 n2 where "G\Norm s0 \e-\b\n1\ s1" "G\s1 \(if the_Bool b then c1 else c2)\n2\ s2" @@ -594,7 +562,7 @@ by (blast intro: evaln.If dest: evaln_max2) then show ?case .. next - case (Loop b c e l s0 s1 s2 s3) + case (Loop s0 e b s1 c s2 l s3) from Loop.hyps obtain n1 where "G\Norm s0 \e-\b\n1\ s1" by (iprover) @@ -614,12 +582,12 @@ done then show ?case .. next - case (Jmp j s) + case (Jmp s j) have "G\Norm s \Jmp j\n\ (Some (Jump j), s)" by (rule evaln.Jmp) then show ?case .. next - case (Throw a e s0 s1) + case (Throw s0 e a s1) then obtain n where "G\Norm s0 \e-\a\n\ s1" by (iprover) @@ -627,7 +595,7 @@ by (rule evaln.Throw) then show ?case .. next - case (Try catchC c1 c2 s0 s1 s2 s3 vn) + case (Try s0 c1 s1 s2 catchC vn c2 s3) from Try.hyps obtain n1 where "G\Norm s0 \c1\n1\ s1" by (iprover) @@ -642,7 +610,7 @@ by (auto intro!: evaln.Try le_maxI1 le_maxI2) then show ?case .. next - case (Fin c1 c2 s0 s1 s2 s3 x1) + case (Fin s0 c1 x1 s1 c2 s2 s3) from Fin obtain n1 n2 where "G\Norm s0 \c1\n1\ (x1, s1)" "G\Norm s1 \c2\n2\ s2" @@ -657,7 +625,7 @@ by (blast intro: evaln.Fin dest: evaln_max2) then show ?case .. next - case (Init C c s0 s1 s2 s3) + case (Init C c s0 s3 s1 s2) have cls: "the (class G C) = c" . moreover from Init.hyps obtain n where "if inited C (globs s0) then s3 = Norm s0 @@ -670,7 +638,7 @@ by (rule evaln.Init) then show ?case .. next - case (NewC C a s0 s1 s2) + case (NewC s0 C s1 a s2) then obtain n where "G\Norm s0 \Init C\n\ s1" by (iprover) @@ -679,7 +647,7 @@ by (iprover intro: evaln.NewC) then show ?case .. next - case (NewA T a e i s0 s1 s2 s3) + case (NewA s0 T s1 e i s2 a s3) then obtain n1 n2 where "G\Norm s0 \init_comp_ty T\n1\ s1" "G\s1 \e-\i\n2\ s2" @@ -691,7 +659,7 @@ by (blast intro: evaln.NewA dest: evaln_max2) then show ?case .. next - case (Cast castT e s0 s1 s2 v) + case (Cast s0 e v s1 s2 castT) then obtain n where "G\Norm s0 \e-\v\n\ s1" by (iprover) @@ -702,7 +670,7 @@ by (rule evaln.Cast) then show ?case .. next - case (Inst T b e s0 s1 v) + case (Inst s0 e v s1 b T) then obtain n where "G\Norm s0 \e-\v\n\ s1" by (iprover) @@ -718,7 +686,7 @@ by (rule evaln.Lit) then show ?case .. next - case (UnOp e s0 s1 unop v ) + case (UnOp s0 e v s1 unop) then obtain n where "G\Norm s0 \e-\v\n\ s1" by (iprover) @@ -726,7 +694,7 @@ by (rule evaln.UnOp) then show ?case .. next - case (BinOp binop e1 e2 s0 s1 s2 v1 v2) + case (BinOp s0 e1 v1 s1 binop e2 v2 s2) then obtain n1 n2 where "G\Norm s0 \e1-\v1\n1\ s1" "G\s1 \(if need_second_arg binop v1 then In1l e2 @@ -742,7 +710,7 @@ by (rule evaln.Super) then show ?case .. next - case (Acc f s0 s1 v va) + case (Acc s0 va v f s1) then obtain n where "G\Norm s0 \va=\(v, f)\n\ s1" by (iprover) @@ -751,7 +719,7 @@ by (rule evaln.Acc) then show ?case .. next - case (Ass e f s0 s1 s2 v var w) + case (Ass s0 var w f s1 e v s2) then obtain n1 n2 where "G\Norm s0 \var=\(w, f)\n1\ s1" "G\s1 \e-\v\n2\ s2" @@ -761,7 +729,7 @@ by (blast intro: evaln.Ass dest: evaln_max2) then show ?case .. next - case (Cond b e0 e1 e2 s0 s1 s2 v) + case (Cond s0 e0 b s1 e1 e2 v s2) then obtain n1 n2 where "G\Norm s0 \e0-\b\n1\ s1" "G\s1 \(if the_Bool b then e1 else e2)-\v\n2\ s2" @@ -771,8 +739,7 @@ by (blast intro: evaln.Cond dest: evaln_max2) then show ?case .. next - case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT - v vs) + case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4) then obtain n1 n2 where "G\Norm s0 \e-\a'\n1\ s1" "G\s1 \args\\vs\n2\ s2" @@ -795,7 +762,7 @@ by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2) thus ?case .. next - case (Methd D s0 s1 sig v ) + case (Methd s0 D sig v s1) then obtain n where "G\Norm s0 \body G D sig-\v\n\ s1" by iprover @@ -803,7 +770,7 @@ by (rule evaln.Methd) then show ?case .. next - case (Body D c s0 s1 s2 s3 ) + case (Body s0 D s1 c s2 s3) from Body.hyps obtain n1 n2 where evaln_init: "G\Norm s0 \Init D\n1\ s1" and evaln_c: "G\s1 \c\n2\ s2" @@ -826,7 +793,7 @@ by (iprover intro: evaln.LVar) then show ?case .. next - case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v) + case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC) then obtain n1 n2 where "G\Norm s0 \Init statDeclC\n1\ s1" "G\s1 \e-\a\n2\ s2" @@ -839,7 +806,7 @@ by (iprover intro: evaln.FVar dest: evaln_max2) then show ?case .. next - case (AVar a e1 e2 i s0 s1 s2 s2' v ) + case (AVar s0 e1 a s1 e2 i s2 v s2') then obtain n1 n2 where "G\Norm s0 \e1-\a\n1\ s1" "G\s1 \e2-\i\n2\ s2" @@ -854,7 +821,7 @@ case (Nil s0) show ?case by (iprover intro: evaln.Nil) next - case (Cons e es s0 s1 s2 v vs) + case (Cons s0 e v s1 es vs s2) then obtain n1 n2 where "G\Norm s0 \e-\v\n1\ s1" "G\s1 \es\\vs\n2\ s2" diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/Trans.thy --- a/src/HOL/Bali/Trans.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/Trans.thy Mon Dec 11 16:06:14 2006 +0100 @@ -60,29 +60,22 @@ by (simp) declare the_var_AVar_def [simp del] -consts - step :: "prog \ ((term \ state) \ (term \ state)) set" - -syntax (symbols) - step :: "[prog,term \ state,term \ state] \ bool" ("_\_ \1 _"[61,82,82] 81) - stepn:: "[prog, term \ state,nat,term \ state] \ bool" - ("_\_ \_ _"[61,82,82] 81) -"step*":: "[prog,term \ state,term \ state] \ bool" ("_\_ \* _"[61,82,82] 81) +syntax (xsymbols) Ref :: "loc \ expr" SKIP :: "expr" translations - "G\p \1 p' " == "(p,p') \ step G" - "G\p \n p' " == "(p,p') \ (step G)^n" - "G\p \* p' " == "(p,p') \ (step G)\<^sup>*" "Ref a" == "Lit (Addr a)" "SKIP" == "Lit Unit" -inductive "step G" intros +inductive2 + step :: "[prog,term \ state,term \ state] \ bool" ("_\_ \1 _"[61,82,82] 81) + for G :: prog +where (* evaluation of expression *) (* cf. 15.5 *) -Abrupt: "\\v. t \ \Lit v\; + Abrupt: "\\v. t \ \Lit v\; \ t. t \ \l\ Skip\; \ C vn c. t \ \Try Skip Catch(C vn) c\; \ x c. t \ \Skip Finally c\ \ xc \ Xcpt x; @@ -90,19 +83,19 @@ \ G\(t,Some xc,s) \1 (\Lit arbitrary\,Some xc,s)" -InsInitE: "\G\(\c\,Norm s) \1 (\c'\, s')\ - \ - G\(\InsInitE c e\,Norm s) \1 (\InsInitE c' e\, s')" +| InsInitE: "\G\(\c\,Norm s) \1 (\c'\, s')\ + \ + G\(\InsInitE c e\,Norm s) \1 (\InsInitE c' e\, s')" (* SeqE: "G\(\Seq Skip e\,Norm s) \1 (\e\, Norm s)" *) (* Specialised rules to evaluate: InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *) (* cf. 15.8.1 *) -NewC: "G\(\NewC C\,Norm s) \1 (\InsInitE (Init C) (NewC C)\, Norm s)" -NewCInited: "\G\ Norm s \halloc (CInst C)\a\ s'\ - \ - G\(\InsInitE Skip (NewC C)\,Norm s) \1 (\Ref a\, s')" +| NewC: "G\(\NewC C\,Norm s) \1 (\InsInitE (Init C) (NewC C)\, Norm s)" +| NewCInited: "\G\ Norm s \halloc (CInst C)\a\ s'\ + \ + G\(\InsInitE Skip (NewC C)\,Norm s) \1 (\Ref a\, s')" @@ -119,68 +112,68 @@ *) (* cf. 15.9.1 *) -NewA: +| NewA: "G\(\New T[e]\,Norm s) \1 (\InsInitE (init_comp_ty T) (New T[e])\,Norm s)" -InsInitNewAIdx: +| InsInitNewAIdx: "\G\(\e\,Norm s) \1 (\e'\, s')\ \ G\(\InsInitE Skip (New T[e])\,Norm s) \1 (\InsInitE Skip (New T[e'])\,s')" -InsInitNewA: +| InsInitNewA: "\G\abupd (check_neg i) (Norm s) \halloc (Arr T (the_Intg i))\a\ s' \ \ G\(\InsInitE Skip (New T[Lit i])\,Norm s) \1 (\Ref a\,s')" (* cf. 15.15 *) -CastE: +| CastE: "\G\(\e\,Norm s) \1 (\e'\,s')\ \ G\(\Cast T e\,None,s) \1 (\Cast T e'\,s')" -Cast: +| Cast: "\s' = abupd (raise_if (\G,s\v fits T) ClassCast) (Norm s)\ \ G\(\Cast T (Lit v)\,Norm s) \1 (\Lit v\,s')" (* can be written without abupd, since we know Norm s *) -InstE: "\G\(\e\,Norm s) \1 (\e'::expr\,s')\ +| InstE: "\G\(\e\,Norm s) \1 (\e'::expr\,s')\ \ G\(\e InstOf T\,Norm s) \1 (\e'\,s')" -Inst: "\b = (v\Null \ G,s\v fits RefT T)\ - \ - G\(\(Lit v) InstOf T\,Norm s) \1 (\Lit (Bool b)\,s')" +| Inst: "\b = (v\Null \ G,s\v fits RefT T)\ + \ + G\(\(Lit v) InstOf T\,Norm s) \1 (\Lit (Bool b)\,s')" (* cf. 15.7.1 *) (*Lit "G\(Lit v,None,s) \1 (Lit v,None,s)"*) -UnOpE: "\G\(\e\,Norm s) \1 (\e'\,s') \ - \ - G\(\UnOp unop e\,Norm s) \1 (\UnOp unop e'\,s')" -UnOp: "G\(\UnOp unop (Lit v)\,Norm s) \1 (\Lit (eval_unop unop v)\,Norm s)" - -BinOpE1: "\G\(\e1\,Norm s) \1 (\e1'\,s') \ +| UnOpE: "\G\(\e\,Norm s) \1 (\e'\,s') \ \ - G\(\BinOp binop e1 e2\,Norm s) \1 (\BinOp binop e1' e2\,s')" -BinOpE2: "\need_second_arg binop v1; G\(\e2\,Norm s) \1 (\e2'\,s') \ - \ - G\(\BinOp binop (Lit v1) e2\,Norm s) - \1 (\BinOp binop (Lit v1) e2'\,s')" -BinOpTerm: "\\ need_second_arg binop v1\ + G\(\UnOp unop e\,Norm s) \1 (\UnOp unop e'\,s')" +| UnOp: "G\(\UnOp unop (Lit v)\,Norm s) \1 (\Lit (eval_unop unop v)\,Norm s)" + +| BinOpE1: "\G\(\e1\,Norm s) \1 (\e1'\,s') \ + \ + G\(\BinOp binop e1 e2\,Norm s) \1 (\BinOp binop e1' e2\,s')" +| BinOpE2: "\need_second_arg binop v1; G\(\e2\,Norm s) \1 (\e2'\,s') \ \ G\(\BinOp binop (Lit v1) e2\,Norm s) - \1 (\Lit v1\,Norm s)" -BinOp: "G\(\BinOp binop (Lit v1) (Lit v2)\,Norm s) - \1 (\Lit (eval_binop binop v1 v2)\,Norm s)" + \1 (\BinOp binop (Lit v1) e2'\,s')" +| BinOpTerm: "\\ need_second_arg binop v1\ + \ + G\(\BinOp binop (Lit v1) e2\,Norm s) + \1 (\Lit v1\,Norm s)" +| BinOp: "G\(\BinOp binop (Lit v1) (Lit v2)\,Norm s) + \1 (\Lit (eval_binop binop v1 v2)\,Norm s)" (* Maybe its more convenient to add: need_second_arg as precondition to BinOp to make the choice between BinOpTerm and BinOp deterministic *) -Super: "G\(\Super\,Norm s) \1 (\Lit (val_this s)\,Norm s)" +| Super: "G\(\Super\,Norm s) \1 (\Lit (val_this s)\,Norm s)" -AccVA: "\G\(\va\,Norm s) \1 (\va'\,s') \ - \ - G\(\Acc va\,Norm s) \1 (\Acc va'\,s')" -Acc: "\groundVar va; ((v,vf),s') = the_var G (Norm s) va\ - \ - G\(\Acc va\,Norm s) \1 (\Lit v\,s')" +| AccVA: "\G\(\va\,Norm s) \1 (\va'\,s') \ + \ + G\(\Acc va\,Norm s) \1 (\Acc va'\,s')" +| Acc: "\groundVar va; ((v,vf),s') = the_var G (Norm s) va\ + \ + G\(\Acc va\,Norm s) \1 (\Lit v\,s')" (* AccLVar: "G\(\Acc (LVar vn)\,Norm s) \1 (\Lit (fst (lvar vn s))\,Norm s)" @@ -192,68 +185,68 @@ \ G\(\Acc ((Lit a).[Lit i])\,Norm s) \1 (\Lit v\,s')" *) -AssVA: "\G\(\va\,Norm s) \1 (\va'\,s')\ - \ - G\(\va:=e\,Norm s) \1 (\va':=e\,s')" -AssE: "\groundVar va; G\(\e\,Norm s) \1 (\e'\,s')\ - \ - G\(\va:=e\,Norm s) \1 (\va:=e'\,s')" -Ass: "\groundVar va; ((w,f),s') = the_var G (Norm s) va\ - \ - G\(\va:=(Lit v)\,Norm s) \1 (\Lit v\,assign f v s')" +| AssVA: "\G\(\va\,Norm s) \1 (\va'\,s')\ + \ + G\(\va:=e\,Norm s) \1 (\va':=e\,s')" +| AssE: "\groundVar va; G\(\e\,Norm s) \1 (\e'\,s')\ + \ + G\(\va:=e\,Norm s) \1 (\va:=e'\,s')" +| Ass: "\groundVar va; ((w,f),s') = the_var G (Norm s) va\ + \ + G\(\va:=(Lit v)\,Norm s) \1 (\Lit v\,assign f v s')" -CondC: "\G\(\e0\,Norm s) \1 (\e0'\,s')\ - \ - G\(\e0? e1:e2\,Norm s) \1 (\e0'? e1:e2\,s')" -Cond: "G\(\Lit b? e1:e2\,Norm s) \1 (\if the_Bool b then e1 else e2\,Norm s)" +| CondC: "\G\(\e0\,Norm s) \1 (\e0'\,s')\ + \ + G\(\e0? e1:e2\,Norm s) \1 (\e0'? e1:e2\,s')" +| Cond: "G\(\Lit b? e1:e2\,Norm s) \1 (\if the_Bool b then e1 else e2\,Norm s)" -CallTarget: "\G\(\e\,Norm s) \1 (\e'\,s')\ - \ - G\(\{accC,statT,mode}e\mn({pTs}args)\,Norm s) - \1 (\{accC,statT,mode}e'\mn({pTs}args)\,s')" -CallArgs: "\G\(\args\,Norm s) \1 (\args'\,s')\ - \ - G\(\{accC,statT,mode}Lit a\mn({pTs}args)\,Norm s) - \1 (\{accC,statT,mode}Lit a\mn({pTs}args')\,s')" -Call: "\groundExprs args; vs = map the_val args; - D = invocation_declclass G mode s a statT \name=mn,parTs=pTs\; - s'=init_lvars G D \name=mn,parTs=pTs\ mode a' vs (Norm s)\ - \ - G\(\{accC,statT,mode}Lit a\mn({pTs}args)\,Norm s) - \1 (\Callee (locals s) (Methd D \name=mn,parTs=pTs\)\,s')" +| CallTarget: "\G\(\e\,Norm s) \1 (\e'\,s')\ + \ + G\(\{accC,statT,mode}e\mn({pTs}args)\,Norm s) + \1 (\{accC,statT,mode}e'\mn({pTs}args)\,s')" +| CallArgs: "\G\(\args\,Norm s) \1 (\args'\,s')\ + \ + G\(\{accC,statT,mode}Lit a\mn({pTs}args)\,Norm s) + \1 (\{accC,statT,mode}Lit a\mn({pTs}args')\,s')" +| Call: "\groundExprs args; vs = map the_val args; + D = invocation_declclass G mode s a statT \name=mn,parTs=pTs\; + s'=init_lvars G D \name=mn,parTs=pTs\ mode a' vs (Norm s)\ + \ + G\(\{accC,statT,mode}Lit a\mn({pTs}args)\,Norm s) + \1 (\Callee (locals s) (Methd D \name=mn,parTs=pTs\)\,s')" -Callee: "\G\(\e\,Norm s) \1 (\e'::expr\,s')\ - \ - G\(\Callee lcls_caller e\,Norm s) \1 (\e'\,s')" +| Callee: "\G\(\e\,Norm s) \1 (\e'::expr\,s')\ + \ + G\(\Callee lcls_caller e\,Norm s) \1 (\e'\,s')" -CalleeRet: "G\(\Callee lcls_caller (Lit v)\,Norm s) - \1 (\Lit v\,(set_lvars lcls_caller (Norm s)))" +| CalleeRet: "G\(\Callee lcls_caller (Lit v)\,Norm s) + \1 (\Lit v\,(set_lvars lcls_caller (Norm s)))" -Methd: "G\(\Methd D sig\,Norm s) \1 (\body G D sig\,Norm s)" +| Methd: "G\(\Methd D sig\,Norm s) \1 (\body G D sig\,Norm s)" -Body: "G\(\Body D c\,Norm s) \1 (\InsInitE (Init D) (Body D c)\,Norm s)" +| Body: "G\(\Body D c\,Norm s) \1 (\InsInitE (Init D) (Body D c)\,Norm s)" -InsInitBody: +| InsInitBody: "\G\(\c\,Norm s) \1 (\c'\,s')\ \ G\(\InsInitE Skip (Body D c)\,Norm s) \1(\InsInitE Skip (Body D c')\,s')" -InsInitBodyRet: +| InsInitBodyRet: "G\(\InsInitE Skip (Body D Skip)\,Norm s) \1 (\Lit (the ((locals s) Result))\,abupd (absorb Ret) (Norm s))" (* LVar: "G\(LVar vn,Norm s)" is already evaluated *) -FVar: "\\ inited statDeclC (globs s)\ - \ - G\(\{accC,statDeclC,stat}e..fn\,Norm s) - \1 (\InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\,Norm s)" -InsInitFVarE: +| FVar: "\\ inited statDeclC (globs s)\ + \ + G\(\{accC,statDeclC,stat}e..fn\,Norm s) + \1 (\InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\,Norm s)" +| InsInitFVarE: "\G\(\e\,Norm s) \1 (\e'\,s')\ \ G\(\InsInitV Skip ({accC,statDeclC,stat}e..fn)\,Norm s) \1 (\InsInitV Skip ({accC,statDeclC,stat}e'..fn)\,s')" -InsInitFVar: +| InsInitFVar: "G\(\InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\,Norm s) \1 (\{accC,statDeclC,stat}Lit a..fn\,Norm s)" -- {* Notice, that we do not have literal values for @{text vars}. @@ -266,13 +259,13 @@ *} -AVarE1: "\G\(\e1\,Norm s) \1 (\e1'\,s')\ - \ - G\(\e1.[e2]\,Norm s) \1 (\e1'.[e2]\,s')" +| AVarE1: "\G\(\e1\,Norm s) \1 (\e1'\,s')\ + \ + G\(\e1.[e2]\,Norm s) \1 (\e1'.[e2]\,s')" -AVarE2: "G\(\e2\,Norm s) \1 (\e2'\,s') - \ - G\(\Lit a.[e2]\,Norm s) \1 (\Lit a.[e2']\,s')" +| AVarE2: "G\(\e2\,Norm s) \1 (\e2'\,s') + \ + G\(\Lit a.[e2]\,Norm s) \1 (\Lit a.[e2']\,s')" (* AVar: \(Lit a).[Lit i]\ is fully evaluated *) @@ -280,89 +273,97 @@ -- {* @{text Nil} is fully evaluated *} -ConsHd: "\G\(\e::expr\,Norm s) \1 (\e'::expr\,s')\ - \ - G\(\e#es\,Norm s) \1 (\e'#es\,s')" +| ConsHd: "\G\(\e::expr\,Norm s) \1 (\e'::expr\,s')\ + \ + G\(\e#es\,Norm s) \1 (\e'#es\,s')" -ConsTl: "\G\(\es\,Norm s) \1 (\es'\,s')\ - \ - G\(\(Lit v)#es\,Norm s) \1 (\(Lit v)#es'\,s')" +| ConsTl: "\G\(\es\,Norm s) \1 (\es'\,s')\ + \ + G\(\(Lit v)#es\,Norm s) \1 (\(Lit v)#es'\,s')" (* execution of statements *) (* cf. 14.5 *) -Skip: "G\(\Skip\,Norm s) \1 (\SKIP\,Norm s)" +| Skip: "G\(\Skip\,Norm s) \1 (\SKIP\,Norm s)" -ExprE: "\G\(\e\,Norm s) \1 (\e'\,s')\ - \ - G\(\Expr e\,Norm s) \1 (\Expr e'\,s')" -Expr: "G\(\Expr (Lit v)\,Norm s) \1 (\Skip\,Norm s)" +| ExprE: "\G\(\e\,Norm s) \1 (\e'\,s')\ + \ + G\(\Expr e\,Norm s) \1 (\Expr e'\,s')" +| Expr: "G\(\Expr (Lit v)\,Norm s) \1 (\Skip\,Norm s)" -LabC: "\G\(\c\,Norm s) \1 (\c'\,s')\ - \ - G\(\l\ c\,Norm s) \1 (\l\ c'\,s')" -Lab: "G\(\l\ Skip\,s) \1 (\Skip\, abupd (absorb l) s)" +| LabC: "\G\(\c\,Norm s) \1 (\c'\,s')\ + \ + G\(\l\ c\,Norm s) \1 (\l\ c'\,s')" +| Lab: "G\(\l\ Skip\,s) \1 (\Skip\, abupd (absorb l) s)" (* cf. 14.2 *) -CompC1: "\G\(\c1\,Norm s) \1 (\c1'\,s')\ - \ - G\(\c1;; c2\,Norm s) \1 (\c1';; c2\,s')" +| CompC1: "\G\(\c1\,Norm s) \1 (\c1'\,s')\ + \ + G\(\c1;; c2\,Norm s) \1 (\c1';; c2\,s')" -Comp: "G\(\Skip;; c2\,Norm s) \1 (\c2\,Norm s)" +| Comp: "G\(\Skip;; c2\,Norm s) \1 (\c2\,Norm s)" (* cf. 14.8.2 *) -IfE: "\G\(\e\ ,Norm s) \1 (\e'\,s')\ - \ - G\(\If(e) s1 Else s2\,Norm s) \1 (\If(e') s1 Else s2\,s')" -If: "G\(\If(Lit v) s1 Else s2\,Norm s) - \1 (\if the_Bool v then s1 else s2\,Norm s)" +| IfE: "\G\(\e\ ,Norm s) \1 (\e'\,s')\ + \ + G\(\If(e) s1 Else s2\,Norm s) \1 (\If(e') s1 Else s2\,s')" +| If: "G\(\If(Lit v) s1 Else s2\,Norm s) + \1 (\if the_Bool v then s1 else s2\,Norm s)" (* cf. 14.10, 14.10.1 *) -Loop: "G\(\l\ While(e) c\,Norm s) - \1 (\If(e) (Cont l\c;; l\ While(e) c) Else Skip\,Norm s)" +| Loop: "G\(\l\ While(e) c\,Norm s) + \1 (\If(e) (Cont l\c;; l\ While(e) c) Else Skip\,Norm s)" -Jmp: "G\(\Jmp j\,Norm s) \1 (\Skip\,(Some (Jump j), s))" +| Jmp: "G\(\Jmp j\,Norm s) \1 (\Skip\,(Some (Jump j), s))" -ThrowE: "\G\(\e\,Norm s) \1 (\e'\,s')\ - \ - G\(\Throw e\,Norm s) \1 (\Throw e'\,s')" -Throw: "G\(\Throw (Lit a)\,Norm s) \1 (\Skip\,abupd (throw a) (Norm s))" +| ThrowE: "\G\(\e\,Norm s) \1 (\e'\,s')\ + \ + G\(\Throw e\,Norm s) \1 (\Throw e'\,s')" +| Throw: "G\(\Throw (Lit a)\,Norm s) \1 (\Skip\,abupd (throw a) (Norm s))" -TryC1: "\G\(\c1\,Norm s) \1 (\c1'\,s')\ - \ - G\(\Try c1 Catch(C vn) c2\, Norm s) \1 (\Try c1' Catch(C vn) c2\,s')" -Try: "\G\s \sxalloc\ s'\ - \ - G\(\Try Skip Catch(C vn) c2\, s) - \1 (if G,s'\catch C then (\c2\,new_xcpt_var vn s') - else (\Skip\,s'))" +| TryC1: "\G\(\c1\,Norm s) \1 (\c1'\,s')\ + \ + G\(\Try c1 Catch(C vn) c2\, Norm s) \1 (\Try c1' Catch(C vn) c2\,s')" +| Try: "\G\s \sxalloc\ s'\ + \ + G\(\Try Skip Catch(C vn) c2\, s) + \1 (if G,s'\catch C then (\c2\,new_xcpt_var vn s') + else (\Skip\,s'))" -FinC1: "\G\(\c1\,Norm s) \1 (\c1'\,s')\ - \ - G\(\c1 Finally c2\,Norm s) \1 (\c1' Finally c2\,s')" +| FinC1: "\G\(\c1\,Norm s) \1 (\c1'\,s')\ + \ + G\(\c1 Finally c2\,Norm s) \1 (\c1' Finally c2\,s')" -Fin: "G\(\Skip Finally c2\,(a,s)) \1 (\FinA a c2\,Norm s)" +| Fin: "G\(\Skip Finally c2\,(a,s)) \1 (\FinA a c2\,Norm s)" -FinAC: "\G\(\c\,s) \1 (\c'\,s')\ - \ - G\(\FinA a c\,s) \1 (\FinA a c'\,s')" -FinA: "G\(\FinA a Skip\,s) \1 (\Skip\,abupd (abrupt_if (a\None) a) s)" +| FinAC: "\G\(\c\,s) \1 (\c'\,s')\ + \ + G\(\FinA a c\,s) \1 (\FinA a c'\,s')" +| FinA: "G\(\FinA a Skip\,s) \1 (\Skip\,abupd (abrupt_if (a\None) a) s)" -Init1: "\inited C (globs s)\ - \ - G\(\Init C\,Norm s) \1 (\Skip\,Norm s)" -Init: "\the (class G C)=c; \ inited C (globs s)\ - \ - G\(\Init C\,Norm s) - \1 (\(if C = Object then Skip else (Init (super c)));; - Expr (Callee (locals s) (InsInitE (init c) SKIP))\ - ,Norm (init_class_obj G C s))" +| Init1: "\inited C (globs s)\ + \ + G\(\Init C\,Norm s) \1 (\Skip\,Norm s)" +| Init: "\the (class G C)=c; \ inited C (globs s)\ + \ + G\(\Init C\,Norm s) + \1 (\(if C = Object then Skip else (Init (super c)));; + Expr (Callee (locals s) (InsInitE (init c) SKIP))\ + ,Norm (init_class_obj G C s))" -- {* @{text InsInitE} is just used as trick to embed the statement @{text "init c"} into an expression*} -InsInitESKIP: - "G\(\InsInitE Skip SKIP\,Norm s) \1 (\SKIP\,Norm s)" +| InsInitESKIP: + "G\(\InsInitE Skip SKIP\,Norm s) \1 (\SKIP\,Norm s)" + +abbreviation + stepn:: "[prog, term \ state,nat,term \ state] \ bool" ("_\_ \_ _"[61,82,82] 81) + where "G\p \n p' \ (p,p') \ {(x, y). step G x y}^n" + +abbreviation + steptr:: "[prog,term \ state,term \ state] \ bool" ("_\_ \* _"[61,82,82] 81) + where "G\p \* p' \ (p,p') \ {(x, y). step G x y}\<^sup>*" (* Equivalenzen: Bigstep zu Smallstep komplett. diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/TypeRel.thy --- a/src/HOL/Bali/TypeRel.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/TypeRel.thy Mon Dec 11 16:06:14 2006 +0100 @@ -34,10 +34,6 @@ (*subcls , by translation*) (* subclass *) (*subclseq, by translation*) (* subclass + identity *) implmt1 :: "prog \ (qtname \ qtname) set" --{* direct implementation *} - implmt :: "prog \ (qtname \ qtname) set" --{* implementation *} - widen :: "prog \ (ty \ ty ) set" --{* widening *} - narrow :: "prog \ (ty \ ty ) set" --{* narrowing *} - cast :: "prog \ (ty \ ty ) set" --{* casting *} syntax @@ -49,12 +45,8 @@ "@subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70) *) "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_" [71,71,71] 70) - "@implmt" :: "prog => [qtname, qtname] => bool" ("_|-_~>_" [71,71,71] 70) - "@widen" :: "prog => [ty , ty ] => bool" ("_|-_<=:_" [71,71,71] 70) - "@narrow" :: "prog => [ty , ty ] => bool" ("_|-_:>_" [71,71,71] 70) - "@cast" :: "prog => [ty , ty ] => bool" ("_|-_<=:? _"[71,71,71] 70) -syntax (symbols) +syntax (xsymbols) "@subint1" :: "prog \ [qtname, qtname] \ bool" ("_\_\I1_" [71,71,71] 70) "@subint" :: "prog \ [qtname, qtname] \ bool" ("_\_\I _" [71,71,71] 70) @@ -64,10 +56,6 @@ "@subcls" :: "prog \ [qtname, qtname] \ bool" ("_\_\\<^sub>C _" [71,71,71] 70) *) "@implmt1" :: "prog \ [qtname, qtname] \ bool" ("_\_\1_" [71,71,71] 70) - "@implmt" :: "prog \ [qtname, qtname] \ bool" ("_\_\_" [71,71,71] 70) - "@widen" :: "prog \ [ty , ty ] \ bool" ("_\_\_" [71,71,71] 70) - "@narrow" :: "prog \ [ty , ty ] \ bool" ("_\_\_" [71,71,71] 70) - "@cast" :: "prog \ [ty , ty ] \ bool" ("_\_\? _" [71,71,71] 70) translations @@ -78,10 +66,6 @@ "G\C \\<^sub>C D" == "(C,D) \(subcls1 G)^*" *) "G\C \1 I" == "(C,I) \ implmt1 G" - "G\C \ I" == "(C,I) \ implmt G" - "G\S \ T" == "(S,T) \ widen G" - "G\S \ T" == "(S,T) \ narrow G" - "G\S \? T" == "(S,T) \ cast G" section "subclass and subinterface relations" @@ -367,11 +351,13 @@ done -inductive "implmt G" intros --{* cf. 8.1.4 *} - +inductive2 --{* implementation, cf. 8.1.4 *} + implmt :: "prog \ qtname \ qtname \ bool" ("_\_\_" [71,71,71] 70) + for G :: prog +where direct: "G\C\1J \\ \ G\C\J" - subint: "\G\C\1I; G\I\I J\ \ G\C\J" - subcls1: "\G\C\\<^sub>C\<^sub>1D; G\D\J \ \ G\C\J" +| subint: "\G\C\1I; G\I\I J\ \ G\C\J" +| subcls1: "\G\C\\<^sub>C\<^sub>1D; G\D\J \ \ G\C\J" lemma implmtD: "G\C\J \ (\I. G\C\1I \ G\I\I J) \ (\D. G\C\\<^sub>C\<^sub>1D \ G\D\J)" apply (erule implmt.induct) @@ -399,17 +385,20 @@ section "widening relation" -inductive "widen G" intros +inductive2 --{*widening, viz. method invocation conversion, cf. 5.3 i.e. kind of syntactic subtyping *} + widen :: "prog \ ty \ ty \ bool" ("_\_\_" [71,71,71] 70) + for G :: prog +where refl: "G\T\T" --{*identity conversion, cf. 5.1.1 *} - subint: "G\I\I J \ G\Iface I\ Iface J" --{*wid.ref.conv.,cf. 5.1.4 *} - int_obj: "G\Iface I\ Class Object" - subcls: "G\C\\<^sub>C D \ G\Class C\ Class D" - implmt: "G\C\I \ G\Class C\ Iface I" - null: "G\NT\ RefT R" - arr_obj: "G\T.[]\ Class Object" - array: "G\RefT S\RefT T \ G\RefT S.[]\ RefT T.[]" +| subint: "G\I\I J \ G\Iface I\ Iface J" --{*wid.ref.conv.,cf. 5.1.4 *} +| int_obj: "G\Iface I\ Class Object" +| subcls: "G\C\\<^sub>C D \ G\Class C\ Class D" +| implmt: "G\C\I \ G\Class C\ Iface I" +| null: "G\NT\ RefT R" +| arr_obj: "G\T.[]\ Class Object" +| array: "G\RefT S\RefT T \ G\RefT S.[]\ RefT T.[]" declare widen.refl [intro!] declare widen.intros [simp] @@ -418,14 +407,14 @@ lemma widen_PrimT: "G\PrimT x\T \ T = PrimT x" *) lemma widen_PrimT: "G\PrimT x\T \ (\y. T = PrimT y)" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\PrimT x\T") by auto (* too strong in general: lemma widen_PrimT2: "G\S\PrimT x \ S = PrimT x" *) lemma widen_PrimT2: "G\S\PrimT x \ \y. S = PrimT y" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\S\PrimT x") by auto text {* @@ -435,37 +424,37 @@ *} lemma widen_PrimT_strong: "G\PrimT x\T \ T = PrimT x" -by (ind_cases "G\S\T") simp_all +by (ind_cases2 "G\PrimT x\T") simp_all lemma widen_PrimT2_strong: "G\S\PrimT x \ S = PrimT x" -by (ind_cases "G\S\T") simp_all +by (ind_cases2 "G\S\PrimT x") simp_all text {* Specialized versions for booleans also would work for real Java *} lemma widen_Boolean: "G\PrimT Boolean\T \ T = PrimT Boolean" -by (ind_cases "G\S\T") simp_all +by (ind_cases2 "G\PrimT Boolean\T") simp_all lemma widen_Boolean2: "G\S\PrimT Boolean \ S = PrimT Boolean" -by (ind_cases "G\S\T") simp_all +by (ind_cases2 "G\S\PrimT Boolean") simp_all lemma widen_RefT: "G\RefT R\T \ \t. T=RefT t" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\RefT R\T") by auto lemma widen_RefT2: "G\S\RefT R \ \t. S=RefT t" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\S\RefT R") by auto lemma widen_Iface: "G\Iface I\T \ T=Class Object \ (\J. T=Iface J)" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\Iface I\T") by auto lemma widen_Iface2: "G\S\ Iface J \ S = NT \ (\I. S = Iface I) \ (\D. S = Class D)" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\S\ Iface J") by auto lemma widen_Iface_Iface: "G\Iface I\ Iface J \ G\I\I J" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\Iface I\ Iface J") by auto lemma widen_Iface_Iface_eq [simp]: "G\Iface I\ Iface J = G\I\I J" @@ -475,15 +464,15 @@ done lemma widen_Class: "G\Class C\T \ (\D. T=Class D) \ (\I. T=Iface I)" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\Class C\T") by auto lemma widen_Class2: "G\S\ Class C \ C = Object \ S = NT \ (\D. S = Class D)" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\S\ Class C") by auto lemma widen_Class_Class: "G\Class C\ Class cm \ G\C\\<^sub>C cm" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\Class C\ Class cm") by auto lemma widen_Class_Class_eq [simp]: "G\Class C\ Class cm = G\C\\<^sub>C cm" @@ -493,7 +482,7 @@ done lemma widen_Class_Iface: "G\Class C\ Iface I \ G\C\I" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\Class C\ Iface I") by auto lemma widen_Class_Iface_eq [simp]: "G\Class C\ Iface I = G\C\I" @@ -503,21 +492,21 @@ done lemma widen_Array: "G\S.[]\T \ T=Class Object \ (\T'. T=T'.[] \ G\S\T')" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\S.[]\T") by auto lemma widen_Array2: "G\S\T.[] \ S = NT \ (\S'. S=S'.[] \ G\S'\T)" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\S\T.[]") by auto lemma widen_ArrayPrimT: "G\PrimT t.[]\T \ T=Class Object \ T=PrimT t.[]" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\PrimT t.[]\T") by auto lemma widen_ArrayRefT: "G\RefT t.[]\T \ T=Class Object \ (\s. T=RefT s.[] \ G\RefT t\RefT s)" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\RefT t.[]\T") by auto lemma widen_ArrayRefT_ArrayRefT_eq [simp]: @@ -538,7 +527,7 @@ lemma widen_NT2: "G\S\NT \ S = NT" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\S\NT") by auto lemma widen_Object:"\isrtype G T;ws_prog G\ \ G\RefT T \ Class Object" @@ -621,35 +610,35 @@ *) (* more detailed than necessary for type-safety, see above rules. *) -inductive "narrow G" intros (* narrowing reference conversion, cf. 5.1.5 *) - +inductive2 --{* narrowing reference conversion, cf. 5.1.5 *} + narrow :: "prog \ ty \ ty \ bool" ("_\_\_" [71,71,71] 70) + for G :: prog +where subcls: "G\C\\<^sub>C D \ G\ Class D\Class C" - implmt: "\G\C\I \ G\ Class C\Iface I" - obj_arr: "G\Class Object\T.[]" - int_cls: "G\ Iface I\Class C" - subint: "imethds G I hidings imethds G J entails +| implmt: "\G\C\I \ G\ Class C\Iface I" +| obj_arr: "G\Class Object\T.[]" +| int_cls: "G\ Iface I\Class C" +| subint: "imethds G I hidings imethds G J entails (\(md, mh ) (md',mh').\G\mrt mh\mrt mh') \ \G\I\I J \\\\ G\ Iface I\Iface J" - array: "G\RefT S\RefT T \\ G\ RefT S.[]\RefT T.[]" +| array: "G\RefT S\RefT T \\ G\ RefT S.[]\RefT T.[]" (*unused*) lemma narrow_RefT: "G\RefT R\T \ \t. T=RefT t" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\RefT R\T") by auto lemma narrow_RefT2: "G\S\RefT R \ \t. S=RefT t" -apply (ind_cases "G\S\T") +apply (ind_cases2 "G\S\RefT R") by auto (*unused*) lemma narrow_PrimT: "G\PrimT pt\T \ \t. T=PrimT t" -apply (ind_cases "G\S\T") -by auto +by (ind_cases2 "G\PrimT pt\T") lemma narrow_PrimT2: "G\S\PrimT pt \ \t. S=PrimT t \ G\PrimT t\PrimT pt" -apply (ind_cases "G\S\T") -by auto +by (ind_cases2 "G\S\PrimT pt") text {* These narrowing lemmata hold in Bali but are to strong for ordinary @@ -657,42 +646,44 @@ long, int. These lemmata are just for documentation and are not used. *} lemma narrow_PrimT_strong: "G\PrimT pt\T \ T=PrimT pt" -by (ind_cases "G\S\T") simp_all +by (ind_cases2 "G\PrimT pt\T") lemma narrow_PrimT2_strong: "G\S\PrimT pt \ S=PrimT pt" -by (ind_cases "G\S\T") simp_all +by (ind_cases2 "G\S\PrimT pt") text {* Specialized versions for booleans also would work for real Java *} lemma narrow_Boolean: "G\PrimT Boolean\T \ T=PrimT Boolean" -by (ind_cases "G\S\T") simp_all +by (ind_cases2 "G\PrimT Boolean\T") lemma narrow_Boolean2: "G\S\PrimT Boolean \ S=PrimT Boolean" -by (ind_cases "G\S\T") simp_all +by (ind_cases2 "G\S\PrimT Boolean") section "casting relation" -inductive "cast G" intros --{* casting conversion, cf. 5.5 *} - +inductive2 --{* casting conversion, cf. 5.5 *} + cast :: "prog \ ty \ ty \ bool" ("_\_\? _" [71,71,71] 70) + for G :: prog +where widen: "G\S\T \ G\S\? T" - narrow: "G\S\T \ G\S\? T" +| narrow: "G\S\T \ G\S\? T" (*unused*) lemma cast_RefT: "G\RefT R\? T \ \t. T=RefT t" -apply (ind_cases "G\S\? T") +apply (ind_cases2 "G\RefT R\? T") by (auto dest: widen_RefT narrow_RefT) lemma cast_RefT2: "G\S\? RefT R \ \t. S=RefT t" -apply (ind_cases "G\S\? T") +apply (ind_cases2 "G\S\? RefT R") by (auto dest: widen_RefT2 narrow_RefT2) (*unused*) lemma cast_PrimT: "G\PrimT pt\? T \ \t. T=PrimT t" -apply (ind_cases "G\S\? T") +apply (ind_cases2 "G\PrimT pt\? T") by (auto dest: widen_PrimT narrow_PrimT) lemma cast_PrimT2: "G\S\? PrimT pt \ \t. S=PrimT t \ G\PrimT t\PrimT pt" -apply (ind_cases "G\S\? T") +apply (ind_cases2 "G\S\? PrimT pt") by (auto dest: widen_PrimT2 narrow_PrimT2) lemma cast_Boolean: diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/TypeSafe.thy --- a/src/HOL/Bali/TypeSafe.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/TypeSafe.thy Mon Dec 11 16:06:14 2006 +0100 @@ -226,7 +226,7 @@ lemmas eval_gext = eval_gext_lemma [THEN conjunct1] -lemma eval_gext': "G\(x1,s1) \t\\ (w,x2,s2) \ s1\|s2" +lemma eval_gext': "G\(x1,s1) \t\\ (w,(x2,s2)) \ s1\|s2" apply (drule eval_gext) apply auto done @@ -1735,7 +1735,7 @@ \ ?Conform L s1 \ ?ValueTyped L T s1 t v \ ?ErrorFree s0 s1") proof (induct) - case (Abrupt s t xc L accC T A) + case (Abrupt xc s t L accC T A) have "(Some xc, s)\\(G,L)" . then show "(Some xc, s)\\(G,L) \ (normal (Some xc, s) @@ -1751,7 +1751,7 @@ (error_free (Norm s) = error_free (Norm s))" by (simp) next - case (Expr e s0 s1 v L accC T A) + case (Expr s0 e v s1 L accC T A) have "G\Norm s0 \e-\v\ s1" . have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" . have conf_s0: "Norm s0\\(G, L)" . @@ -1773,7 +1773,7 @@ (error_free (Norm s0) = error_free s1)" by (simp) next - case (Lab c l s0 s1 L accC T A) + case (Lab s0 c s1 l L accC T A) have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r c) \" . have conf_s0: "Norm s0\\(G, L)" . moreover @@ -1796,7 +1796,7 @@ (error_free (Norm s0) = error_free (abupd (absorb l) s1))" by (simp) next - case (Comp c1 c2 s0 s1 s2 L accC T A) + case (Comp s0 c1 s1 c2 s2 L accC T A) have eval_c1: "G\Norm s0 \c1\ s1" . have eval_c2: "G\s1 \c2\ s2" . have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \" . @@ -1842,7 +1842,7 @@ using wt by simp qed next - case (If b c1 c2 e s0 s1 s2 L accC T) + case (If s0 e b s1 c1 c2 s2 L accC T A) have eval_e: "G\Norm s0 \e-\b\ s1" . have eval_then_else: "G\s1 \(if the_Bool b then c1 else c2)\ s2" . have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" . @@ -1917,7 +1917,7 @@ a boolean value is part of @{term hyp_e}. See also Loop *} next - case (Loop b c e l s0 s1 s2 s3 L accC T A) + case (Loop s0 e b s1 c s2 l s3 L accC T A) have eval_e: "G\Norm s0 \e-\b\ s1" . have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" . have conf_s0: "Norm s0\\(G, L)" . @@ -2048,7 +2048,7 @@ by simp qed next - case (Jmp j s L accC T A) + case (Jmp s j L accC T A) have "Norm s\\(G, L)" . moreover from Jmp.prems @@ -2062,7 +2062,7 @@ (error_free (Norm s) = error_free (Some (Jump j), s))" by simp next - case (Throw a e s0 s1 L accC T A) + case (Throw s0 e a s1 L accC T A) have "G\Norm s0 \e-\a\ s1" . have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" . have conf_s0: "Norm s0\\(G, L)" . @@ -2090,7 +2090,7 @@ (error_free (Norm s0) = error_free (abupd (throw a) s1))" by simp next - case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T A) + case (Try s0 c1 s1 s2 catchC vn c2 s3 L accC T A) have eval_c1: "G\Norm s0 \c1\ s1" . have sx_alloc: "G\s1 \sxalloc\ s2" . have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \" . @@ -2207,7 +2207,7 @@ qed qed next - case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T A) + case (Fin s0 c1 x1 s1 c2 s2 s3 L accC T A) have eval_c1: "G\Norm s0 \c1\ (x1, s1)" . have eval_c2: "G\Norm s1 \c2\ s2" . have s3: "s3= (if \err. x1 = Some (Error err) @@ -2276,7 +2276,7 @@ by (cases s2) auto qed next - case (Init C c s0 s1 s2 s3 L accC T) + case (Init C c s0 s3 s1 s2 L accC T A) have cls: "the (class G C) = c" . have conf_s0: "Norm s0\\(G, L)" . have wt: "\prg = G, cls = accC, lcl = L\\In1r (Init C)\T" . @@ -2382,7 +2382,7 @@ by simp qed next - case (NewC C a s0 s1 s2 L accC T A) + case (NewC s0 C s1 a s2 L accC T A) have "G\Norm s0 \Init C\ s1" . have halloc: "G\s1 \halloc CInst C\a\ s2" . have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \" . @@ -2414,7 +2414,7 @@ (error_free (Norm s0) = error_free s2)" by auto next - case (NewA elT a e i s0 s1 s2 s3 L accC T A) + case (NewA s0 elT s1 e i s2 a s3 L accC T A) have eval_init: "G\Norm s0 \init_comp_ty elT\ s1" . have eval_e: "G\s1 \e-\i\ s2" . have halloc: "G\abupd (check_neg i) s2\halloc Arr elT (the_Intg i)\a\ s3". @@ -2485,7 +2485,7 @@ (error_free (Norm s0) = error_free s3) " by simp next - case (Cast castT e s0 s1 s2 v L accC T A) + case (Cast s0 e v s1 s2 castT L accC T A) have "G\Norm s0 \e-\v\ s1" . have s2:"s2 = abupd (raise_if (\ G,store s1\v fits castT) ClassCast) s1" . have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" . @@ -2531,7 +2531,7 @@ (error_free (Norm s0) = error_free s2)" by blast next - case (Inst instT b e s0 s1 v L accC T A) + case (Inst s0 e v s1 b instT L accC T A) have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" . have conf_s0: "Norm s0\\(G, L)" . from Inst.prems obtain eT @@ -2555,7 +2555,7 @@ by (auto elim!: wt_elim_cases intro: conf_litval simp add: empty_dt_def) next - case (UnOp e s0 s1 unop v L accC T A) + case (UnOp s0 e v s1 unop L accC T A) have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" . have conf_s0: "Norm s0\\(G, L)" . have wt: "\prg = G, cls = accC, lcl = L\\In1l (UnOp unop e)\T" . @@ -2582,7 +2582,7 @@ error_free (Norm s0) = error_free s1" by simp next - case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T A) + case (BinOp s0 e1 v1 s1 binop e2 v2 s2 L accC T A) have eval_e1: "G\Norm s0 \e1-\v1\ s1" . have eval_e2: "G\s1 \(if need_second_arg binop v1 then In1l e2 else In1r Skip)\\ (In1 v2, s2)" . @@ -2698,7 +2698,7 @@ (error_free (Norm s) = error_free (Norm s))" by simp next - case (Acc upd s0 s1 w v L accC T A) + case (Acc s0 v w upd s1 L accC T A) have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" . have conf_s0: "Norm s0\\(G, L)" . from Acc.prems obtain vT where @@ -2738,7 +2738,7 @@ with conf_s1 error_free_s1 show ?case by simp next - case (Ass e upd s0 s1 s2 v var w L accC T A) + case (Ass s0 var w upd s1 e v s2 L accC T A) have eval_var: "G\Norm s0 \var=\(w, upd)\ s1" . have eval_e: "G\s1 \e-\v\ s2" . have hyp_var: "PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))" . @@ -2895,7 +2895,7 @@ qed qed next - case (Cond b e0 e1 e2 s0 s1 s2 v L accC T A) + case (Cond s0 e0 b s1 e1 e2 v s2 L accC T A) have eval_e0: "G\Norm s0 \e0-\b\ s1" . have eval_e1_e2: "G\s1 \(if the_Bool b then e1 else e2)-\v\ s2" . have hyp_e0: "PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)" . @@ -2988,8 +2988,8 @@ qed qed next - case (Call invDeclC a accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT - v vs L accC T A) + case (Call s0 e a s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' + v s4 L accC T A) have eval_e: "G\Norm s0 \e-\a\ s1" . have eval_args: "G\s1 \args\\vs\ s2" . have invDeclC: "invDeclC @@ -3332,7 +3332,7 @@ qed qed next - case (Methd D s0 s1 sig v L accC T A) + case (Methd s0 D sig v s1 L accC T A) have "G\Norm s0 \body G D sig-\v\ s1" . have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" . have conf_s0: "Norm s0\\(G, L)" . @@ -3357,7 +3357,7 @@ using hyp [of _ _ "(Inl bodyT)"] conf_s0 by (auto simp add: Let_def body_def) next - case (Body D c s0 s1 s2 s3 L accC T A) + case (Body s0 D s1 c s2 s3 L accC T A) have eval_init: "G\Norm s0 \Init D\ s1" . have eval_c: "G\s1 \c\ s2" . have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \" . @@ -3481,7 +3481,7 @@ (error_free (Norm s) = error_free (Norm s))" by (simp add: lvar_def) next - case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T A) + case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC L accC' T A) have eval_init: "G\Norm s0 \Init statDeclC\ s1" . have eval_e: "G\s1 \e-\a\ s2" . have fvar: "(v, s2') = fvar statDeclC stat fn a s2" . @@ -3597,7 +3597,7 @@ (error_free (Norm s0) = error_free s3)" by auto next - case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T A) + case (AVar s0 e1 a s1 e2 i s2 v s2' L accC T A) have eval_e1: "G\Norm s0 \e1-\a\ s1" . have eval_e2: "G\s1 \e2-\i\ s2" . have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)" . @@ -3697,7 +3697,7 @@ then show ?case by (auto elim!: wt_elim_cases) next - case (Cons e es s0 s1 s2 v vs L accC T A) + case (Cons s0 e v s1 es vs s2 L accC T A) have eval_e: "G\Norm s0 \e-\v\ s1" . have eval_es: "G\s1 \es\\vs\ s2" . have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" . @@ -3905,7 +3905,7 @@ next case Skip from skip show ?case by simp next - case (Expr e s0 s1 v L accC T A) + case (Expr s0 e v s1 L accC T A) from Expr.prems obtain eT where "\prg = G, cls = accC, lcl = L\\e\-eT" by (elim wt_elim_cases) @@ -3919,7 +3919,7 @@ ultimately show ?case by (rule expr) next - case (Lab c l s0 s1 L accC T A) + case (Lab s0 c s1 l L accC T A) from Lab.prems have "\prg = G, cls = accC, lcl = L\\c\\" by (elim wt_elim_cases) @@ -3933,7 +3933,7 @@ ultimately show ?case by (rule lab) next - case (Comp c1 c2 s0 s1 s2 L accC T A) + case (Comp s0 c1 s1 c2 s2 L accC T A) have eval_c1: "G\Norm s0 \c1\ s1" . have eval_c2: "G\s1 \c2\ s2" . from Comp.prems obtain @@ -3976,7 +3976,7 @@ show ?case by (rule comp) iprover+ next - case (If b c1 c2 e s0 s1 s2 L accC T A) + case (If s0 e b s1 c1 c2 s2 L accC T A) have eval_e: "G\Norm s0 \e-\b\ s1" . have eval_then_else: "G\s1 \(if the_Bool b then c1 else c2)\ s2" . from If.prems diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/WellForm.thy Mon Dec 11 16:06:14 2006 +0100 @@ -883,7 +883,7 @@ show "?Overrides new old" by (auto intro: overridesR.Direct stat_override_declclasses_relation) next - case (Indirect inter new old) + case (Indirect new inter old) then show "?Overrides new old" by (blast intro: overridesR.Indirect) qed @@ -1138,7 +1138,7 @@ qed qed next - case (Indirect inter new old) + case (Indirect new inter old) assume accmodi_old: "accmodi old \ Package" assume "accmodi old \ Package \ G \ inter overrides\<^sub>S old" with accmodi_old @@ -1244,7 +1244,7 @@ then show "pid (declclass old) = pid (declclass new)" by (auto simp add: inheritable_in_def) next - case (Indirect inter new old) + case (Indirect new inter old) assume accmodi_old: "accmodi old = Package" and accmodi_new: "accmodi new = Package" assume "G \ new overrides inter" @@ -1280,7 +1280,7 @@ show "?P new old" by (contradiction) next - case (Indirect inter new old) + case (Indirect new inter old) assume accmodi_old: "accmodi old = Package" assume outside_pack: "pid (declclass old) \ pid (declclass new)" assume override_new_inter: "G \ new overrides inter" @@ -2554,13 +2554,13 @@ from stat_acc subclseq show ?thesis (is "?Dyn_accessible m") proof (induct rule: accessible_fromR.induct) - case (Immediate statC m) + case (Immediate m statC) then show "?Dyn_accessible m" by (blast intro: dyn_accessible_fromR.Immediate member_inI permits_acc_inheritance) next - case (Overriding _ _ m) + case (Overriding m _ _) with wf show "?Dyn_accessible m" by (blast intro: dyn_accessible_fromR.Overriding member_inI @@ -2921,7 +2921,7 @@ from dyn_acc priv show ?thesis proof (induct) - case (Immediate C m) + case (Immediate m C) have "G \ m in C permits_acc_from accC" and "accmodi m = Private" . then show ?case by (simp add: permits_acc_def) @@ -2946,14 +2946,14 @@ \ pid accC = pid (declclass m)" (is "?Pack m \ ?P m") proof (induct rule: dyn_accessible_fromR.induct) - case (Immediate C m) + case (Immediate m C) assume "G\m member_in C" "G \ m in C permits_acc_from accC" "accmodi m = Package" then show "?P m" by (auto simp add: permits_acc_def) next - case (Overriding declC C new newm old Sup) + case (Overriding new C declC newm old Sup) assume member_new: "G \ new member_in C" and new: "new = (declC, mdecl newm)" and override: "G \ (declC, newm) overrides old" and @@ -2986,7 +2986,7 @@ from dyn_acc pack field show ?thesis proof (induct) - case (Immediate C f) + case (Immediate f C) have "G \ f in C permits_acc_from accC" and "accmodi f = Package" . then show ?case by (simp add: permits_acc_def) @@ -3010,7 +3010,7 @@ from dyn_acc prot field instance_field outside show ?thesis proof (induct) - case (Immediate C f) + case (Immediate f C) have "G \ f in C permits_acc_from accC" . moreover assume "accmodi f = Protected" and "is_field f" and "\ is_static f" and @@ -3035,7 +3035,7 @@ from dyn_acc prot field static_field outside show ?thesis proof (induct) - case (Immediate C f) + case (Immediate f C) assume "accmodi f = Protected" and "is_field f" and "is_static f" and "pid (declclass f) \ pid accC" moreover diff -r 720b0add5206 -r 89275a3ed7be src/HOL/Bali/WellType.thy --- a/src/HOL/Bali/WellType.thy Mon Dec 11 12:28:16 2006 +0100 +++ b/src/HOL/Bali/WellType.thy Mon Dec 11 16:06:14 2006 +0100 @@ -245,33 +245,185 @@ translations "tys" <= (type) "ty + ty list" -consts - wt :: "(env\ \ dyn_ty\ \ term \ tys) set" -(*wt :: " env \ dyn_ty \ (term \ tys) set" not feasible because of - \ changing env in Try stmt *) + +inductive2 + wt :: "env \ dyn_ty \ [term,tys] \ bool" ("_,_\_\_" [51,51,51,51] 50) + and wt_stmt :: "env \ dyn_ty \ stmt \ bool" ("_,_\_\\" [51,51,51 ] 50) + and ty_expr :: "env \ dyn_ty \ [expr ,ty ] \ bool" ("_,_\_\-_" [51,51,51,51] 50) + and ty_var :: "env \ dyn_ty \ [var ,ty ] \ bool" ("_,_\_\=_" [51,51,51,51] 50) + and ty_exprs :: "env \ dyn_ty \ [expr list, ty list] \ bool" + ("_,_\_\\_" [51,51,51,51] 50) +where + + "E,dt\s\\ \ E,dt\In1r s\Inl (PrimT Void)" +| "E,dt\e\-T \ E,dt\In1l e\Inl T" +| "E,dt\e\=T \ E,dt\In2 e\Inl T" +| "E,dt\e\\T \ E,dt\In3 e\Inr T" + +--{* well-typed statements *} + +| Skip: "E,dt\Skip\\" + +| Expr: "\E,dt\e\-T\ \ + E,dt\Expr e\\" + --{* cf. 14.6 *} +| Lab: "E,dt\c\\ \ + E,dt\l\ c\\" + +| Comp: "\E,dt\c1\\; + E,dt\c2\\\ \ + E,dt\c1;; c2\\" + + --{* cf. 14.8 *} +| If: "\E,dt\e\-PrimT Boolean; + E,dt\c1\\; + E,dt\c2\\\ \ + E,dt\If(e) c1 Else c2\\" + + --{* cf. 14.10 *} +| Loop: "\E,dt\e\-PrimT Boolean; + E,dt\c\\\ \ + E,dt\l\ While(e) c\\" + --{* cf. 14.13, 14.15, 14.16 *} +| Jmp: "E,dt\Jmp jump\\" -syntax -wt :: "env \ dyn_ty \ [term,tys] \ bool" ("_,_|=_::_" [51,51,51,51] 50) -wt_stmt :: "env \ dyn_ty \ stmt \ bool" ("_,_|=_:<>" [51,51,51 ] 50) -ty_expr :: "env \ dyn_ty \ [expr ,ty ] \ bool" ("_,_|=_:-_" [51,51,51,51] 50) -ty_var :: "env \ dyn_ty \ [var ,ty ] \ bool" ("_,_|=_:=_" [51,51,51,51] 50) -ty_exprs:: "env \ dyn_ty \ [expr list, - \ \ ty list] \ bool" ("_,_|=_:#_" [51,51,51,51] 50) + --{* cf. 14.16 *} +| Throw: "\E,dt\e\-Class tn; + prg E\tn\\<^sub>C SXcpt Throwable\ \ + E,dt\Throw e\\" + --{* cf. 14.18 *} +| Try: "\E,dt\c1\\; prg E\tn\\<^sub>C SXcpt Throwable; + lcl E (VName vn)=None; E \lcl := lcl E(VName vn\Class tn)\,dt\c2\\\ + \ + E,dt\Try c1 Catch(tn vn) c2\\" + + --{* cf. 14.18 *} +| Fin: "\E,dt\c1\\; E,dt\c2\\\ \ + E,dt\c1 Finally c2\\" + +| Init: "\is_class (prg E) C\ \ + E,dt\Init C\\" + --{* @{term Init} is created on the fly during evaluation (see Eval.thy). + The class isn't necessarily accessible from the points @{term Init} + is called. Therefor we only demand @{term is_class} and not + @{term is_acc_class} here. + *} + +--{* well-typed expressions *} + + --{* cf. 15.8 *} +| NewC: "\is_acc_class (prg E) (pkg E) C\ \ + E,dt\NewC C\-Class C" + --{* cf. 15.9 *} +| NewA: "\is_acc_type (prg E) (pkg E) T; + E,dt\i\-PrimT Integer\ \ + E,dt\New T[i]\-T.[]" + + --{* cf. 15.15 *} +| Cast: "\E,dt\e\-T; is_acc_type (prg E) (pkg E) T'; + prg E\T\? T'\ \ + E,dt\Cast T' e\-T'" + + --{* cf. 15.19.2 *} +| Inst: "\E,dt\e\-RefT T; is_acc_type (prg E) (pkg E) (RefT T'); + prg E\RefT T\? RefT T'\ \ + E,dt\e InstOf T'\-PrimT Boolean" + + --{* cf. 15.7.1 *} +| Lit: "\typeof dt x = Some T\ \ + E,dt\Lit x\-T" -syntax (xsymbols) -wt :: "env \ dyn_ty \ [term,tys] \ bool" ("_,_\_\_" [51,51,51,51] 50) -wt_stmt :: "env \ dyn_ty \ stmt \ bool" ("_,_\_\\" [51,51,51 ] 50) -ty_expr :: "env \ dyn_ty \ [expr ,ty ] \ bool" ("_,_\_\-_" [51,51,51,51] 50) -ty_var :: "env \ dyn_ty \ [var ,ty ] \ bool" ("_,_\_\=_" [51,51,51,51] 50) -ty_exprs:: "env \ dyn_ty \ [expr list, - \ \ ty list] \ bool"("_,_\_\\_" [51,51,51,51] 50) +| UnOp: "\E,dt\e\-Te; wt_unop unop Te; T=PrimT (unop_type unop)\ + \ + E,dt\UnOp unop e\-T" + +| BinOp: "\E,dt\e1\-T1; E,dt\e2\-T2; wt_binop (prg E) binop T1 T2; + T=PrimT (binop_type binop)\ + \ + E,dt\BinOp binop e1 e2\-T" + + --{* cf. 15.10.2, 15.11.1 *} +| Super: "\lcl E This = Some (Class C); C \ Object; + class (prg E) C = Some c\ \ + E,dt\Super\-Class (super c)" + + --{* cf. 15.13.1, 15.10.1, 15.12 *} +| Acc: "\E,dt\va\=T\ \ + E,dt\Acc va\-T" + + --{* cf. 15.25, 15.25.1 *} +| Ass: "\E,dt\va\=T; va \ LVar This; + E,dt\v \-T'; + prg E\T'\T\ \ + E,dt\va:=v\-T'" + + --{* cf. 15.24 *} +| Cond: "\E,dt\e0\-PrimT Boolean; + E,dt\e1\-T1; E,dt\e2\-T2; + prg E\T1\T2 \ T = T2 \ prg E\T2\T1 \ T = T1\ \ + E,dt\e0 ? e1 : e2\-T" + + --{* cf. 15.11.1, 15.11.2, 15.11.3 *} +| Call: "\E,dt\e\-RefT statT; + E,dt\ps\\pTs; + max_spec (prg E) (cls E) statT \name=mn,parTs=pTs\ + = {((statDeclT,m),pTs')} + \ \ + E,dt\{cls E,statT,invmode m e}e\mn({pTs'}ps)\-(resTy m)" -translations - "E,dt\t\T" == "(E,dt,t,T) \ wt" - "E,dt\s\\" == "E,dt\In1r s\Inl (PrimT Void)" - "E,dt\e\-T" == "E,dt\In1l e\Inl T" - "E,dt\e\=T" == "E,dt\In2 e\Inl T" - "E,dt\e\\T" == "E,dt\In3 e\Inr T" +| Methd: "\is_class (prg E) C; + methd (prg E) C sig = Some m; + E,dt\Body (declclass m) (stmt (mbody (mthd m)))\-T\ \ + E,dt\Methd C sig\-T" + --{* The class @{term C} is the dynamic class of the method call + (cf. Eval.thy). + It hasn't got to be directly accessible from the current package + @{term "(pkg E)"}. + Only the static class must be accessible (enshured indirectly by + @{term Call}). + Note that l is just a dummy value. It is only used in the smallstep + semantics. To proof typesafety directly for the smallstep semantics + we would have to assume conformance of l here! + *} + +| Body: "\is_class (prg E) D; + E,dt\blk\\; + (lcl E) Result = Some T; + is_type (prg E) T\ \ + E,dt\Body D blk\-T" +--{* The class @{term D} implementing the method must not directly be + accessible from the current package @{term "(pkg E)"}, but can also + be indirectly accessible due to inheritance (enshured in @{term Call}) + The result type hasn't got to be accessible in Java! (If it is not + accessible you can only assign it to Object). + For dummy value l see rule @{term Methd}. + *} + +--{* well-typed variables *} + + --{* cf. 15.13.1 *} +| LVar: "\lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\ \ + E,dt\LVar vn\=T" + --{* cf. 15.10.1 *} +| FVar: "\E,dt\e\-Class C; + accfield (prg E) (cls E) C fn = Some (statDeclC,f)\ \ + E,dt\{cls E,statDeclC,is_static f}e..fn\=(type f)" + --{* cf. 15.12 *} +| AVar: "\E,dt\e\-T.[]; + E,dt\i\-PrimT Integer\ \ + E,dt\e.[i]\=T" + + +--{* well-typed expression lists *} + + --{* cf. 15.11.??? *} +| Nil: "E,dt\[]\\[]" + + --{* cf. 15.11.??? *} +| Cons: "\E,dt\e \-T; + E,dt\es\\Ts\ \ + E,dt\e#es\\T#Ts" + syntax (* for purely static typing *) wt_ :: "env \ [term,tys] \ bool" ("_|-_::_" [51,51,51] 50) @@ -297,174 +449,6 @@ "E\e\\T" == "E\In3 e\Inr T" -inductive wt intros - - ---{* well-typed statements *} - - Skip: "E,dt\Skip\\" - - Expr: "\E,dt\e\-T\ \ - E,dt\Expr e\\" - --{* cf. 14.6 *} - Lab: "E,dt\c\\ \ - E,dt\l\ c\\" - - Comp: "\E,dt\c1\\; - E,dt\c2\\\ \ - E,dt\c1;; c2\\" - - --{* cf. 14.8 *} - If: "\E,dt\e\-PrimT Boolean; - E,dt\c1\\; - E,dt\c2\\\ \ - E,dt\If(e) c1 Else c2\\" - - --{* cf. 14.10 *} - Loop: "\E,dt\e\-PrimT Boolean; - E,dt\c\\\ \ - E,dt\l\ While(e) c\\" - --{* cf. 14.13, 14.15, 14.16 *} - Jmp: "E,dt\Jmp jump\\" - - --{* cf. 14.16 *} - Throw: "\E,dt\e\-Class tn; - prg E\tn\\<^sub>C SXcpt Throwable\ \ - E,dt\Throw e\\" - --{* cf. 14.18 *} - Try: "\E,dt\c1\\; prg E\tn\\<^sub>C SXcpt Throwable; - lcl E (VName vn)=None; E \lcl := lcl E(VName vn\Class tn)\,dt\c2\\\ - \ - E,dt\Try c1 Catch(tn vn) c2\\" - - --{* cf. 14.18 *} - Fin: "\E,dt\c1\\; E,dt\c2\\\ \ - E,dt\c1 Finally c2\\" - - Init: "\is_class (prg E) C\ \ - E,dt\Init C\\" - --{* @{term Init} is created on the fly during evaluation (see Eval.thy). - The class isn't necessarily accessible from the points @{term Init} - is called. Therefor we only demand @{term is_class} and not - @{term is_acc_class} here. - *} - ---{* well-typed expressions *} - - --{* cf. 15.8 *} - NewC: "\is_acc_class (prg E) (pkg E) C\ \ - E,dt\NewC C\-Class C" - --{* cf. 15.9 *} - NewA: "\is_acc_type (prg E) (pkg E) T; - E,dt\i\-PrimT Integer\ \ - E,dt\New T[i]\-T.[]" - - --{* cf. 15.15 *} - Cast: "\E,dt\e\-T; is_acc_type (prg E) (pkg E) T'; - prg E\T\? T'\ \ - E,dt\Cast T' e\-T'" - - --{* cf. 15.19.2 *} - Inst: "\E,dt\e\-RefT T; is_acc_type (prg E) (pkg E) (RefT T'); - prg E\RefT T\? RefT T'\ \ - E,dt\e InstOf T'\-PrimT Boolean" - - --{* cf. 15.7.1 *} - Lit: "\typeof dt x = Some T\ \ - E,dt\Lit x\-T" - - UnOp: "\E,dt\e\-Te; wt_unop unop Te; T=PrimT (unop_type unop)\ - \ - E,dt\UnOp unop e\-T" - - BinOp: "\E,dt\e1\-T1; E,dt\e2\-T2; wt_binop (prg E) binop T1 T2; - T=PrimT (binop_type binop)\ - \ - E,dt\BinOp binop e1 e2\-T" - - --{* cf. 15.10.2, 15.11.1 *} - Super: "\lcl E This = Some (Class C); C \ Object; - class (prg E) C = Some c\ \ - E,dt\Super\-Class (super c)" - - --{* cf. 15.13.1, 15.10.1, 15.12 *} - Acc: "\E,dt\va\=T\ \ - E,dt\Acc va\-T" - - --{* cf. 15.25, 15.25.1 *} - Ass: "\E,dt\va\=T; va \ LVar This; - E,dt\v \-T'; - prg E\T'\T\ \ - E,dt\va:=v\-T'" - - --{* cf. 15.24 *} - Cond: "\E,dt\e0\-PrimT Boolean; - E,dt\e1\-T1; E,dt\e2\-T2; - prg E\T1\T2 \ T = T2 \ prg E\T2\T1 \ T = T1\ \ - E,dt\e0 ? e1 : e2\-T" - - --{* cf. 15.11.1, 15.11.2, 15.11.3 *} - Call: "\E,dt\e\-RefT statT; - E,dt\ps\\pTs; - max_spec (prg E) (cls E) statT \name=mn,parTs=pTs\ - = {((statDeclT,m),pTs')} - \ \ - E,dt\{cls E,statT,invmode m e}e\mn({pTs'}ps)\-(resTy m)" - - Methd: "\is_class (prg E) C; - methd (prg E) C sig = Some m; - E,dt\Body (declclass m) (stmt (mbody (mthd m)))\-T\ \ - E,dt\Methd C sig\-T" - --{* The class @{term C} is the dynamic class of the method call - (cf. Eval.thy). - It hasn't got to be directly accessible from the current package - @{term "(pkg E)"}. - Only the static class must be accessible (enshured indirectly by - @{term Call}). - Note that l is just a dummy value. It is only used in the smallstep - semantics. To proof typesafety directly for the smallstep semantics - we would have to assume conformance of l here! - *} - - Body: "\is_class (prg E) D; - E,dt\blk\\; - (lcl E) Result = Some T; - is_type (prg E) T\ \ - E,dt\Body D blk\-T" ---{* The class @{term D} implementing the method must not directly be - accessible from the current package @{term "(pkg E)"}, but can also - be indirectly accessible due to inheritance (enshured in @{term Call}) - The result type hasn't got to be accessible in Java! (If it is not - accessible you can only assign it to Object). - For dummy value l see rule @{term Methd}. - *} - ---{* well-typed variables *} - - --{* cf. 15.13.1 *} - LVar: "\lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\ \ - E,dt\LVar vn\=T" - --{* cf. 15.10.1 *} - FVar: "\E,dt\e\-Class C; - accfield (prg E) (cls E) C fn = Some (statDeclC,f)\ \ - E,dt\{cls E,statDeclC,is_static f}e..fn\=(type f)" - --{* cf. 15.12 *} - AVar: "\E,dt\e\-T.[]; - E,dt\i\-PrimT Integer\ \ - E,dt\e.[i]\=T" - - ---{* well-typed expression lists *} - - --{* cf. 15.11.??? *} - Nil: "E,dt\[]\\[]" - - --{* cf. 15.11.??? *} - Cons: "\E,dt\e \-T; - E,dt\es\\Ts\ \ - E,dt\e#es\\T#Ts" - - declare not_None_eq [simp del] declare split_if [split del] split_if_asm [split del] declare split_paired_All [simp del] split_paired_Ex [simp del] @@ -472,7 +456,7 @@ change_simpset (fn ss => ss delloop "split_all_tac") *} -inductive_cases wt_elim_cases [cases set]: +inductive_cases2 wt_elim_cases [cases set]: "E,dt\In2 (LVar vn) \T" "E,dt\In2 ({accC,statDeclC,s}e..fn)\T" "E,dt\In2 (e.[i]) \T" @@ -610,25 +594,32 @@ correlation. *} +lemma wt_expr_eq: "E,dt\In1l t\U = (\T. U=Inl T \ E,dt\t\-T)" + by (auto, frule wt_Inj_elim, auto) + +lemma wt_var_eq: "E,dt\In2 t\U = (\T. U=Inl T \ E,dt\t\=T)" + by (auto, frule wt_Inj_elim, auto) + +lemma wt_exprs_eq: "E,dt\In3 t\U = (\Ts. U=Inr Ts \ E,dt\t\\Ts)" + by (auto, frule wt_Inj_elim, auto) + +lemma wt_stmt_eq: "E,dt\In1r t\U = (U=Inl(PrimT Void)\E,dt\t\\)" + by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto) + ML {* -fun wt_fun name inj rhs = +fun wt_fun name lhs = let - val lhs = "E,dt\" ^ inj ^ " t\U" - val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") - (K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac]) fun is_Inj (Const (inj,_) $ _) = true | is_Inj _ = false - fun pred (t as (_ $ (Const ("Pair",_) $ - _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $ - x))) $ _ )) = is_Inj x + fun pred (_ $ _ $ _ $ _ $ x) = is_Inj x in cond_simproc name lhs pred (thm name) end -val wt_expr_proc = wt_fun "wt_expr_eq" "In1l" "\T. U=Inl T \ E,dt\t\-T" -val wt_var_proc = wt_fun "wt_var_eq" "In2" "\T. U=Inl T \ E,dt\t\=T" -val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3" "\Ts. U=Inr Ts \ E,dt\t\\Ts" -val wt_stmt_proc = wt_fun "wt_stmt_eq" "In1r" "U=Inl(PrimT Void)\E,dt\t\\" +val wt_expr_proc = wt_fun "wt_expr_eq" "E,dt\In1l t\U"; +val wt_var_proc = wt_fun "wt_var_eq" "E,dt\In2 t\U"; +val wt_exprs_proc = wt_fun "wt_exprs_eq" "E,dt\In3 t\U"; +val wt_stmt_proc = wt_fun "wt_stmt_eq" "E,dt\In1r t\U"; *} ML {*