src/HOL/Bali/Evaln.thy
author berghofe
Mon, 11 Dec 2006 16:06:14 +0100
changeset 21765 89275a3ed7be
parent 18249 4398f0f12579
child 22218 30a8890d2967
permissions -rw-r--r--
Adapted to new inductive definition package.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Evaln.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
     3
    Author:     David von Oheimb and Norbert Schirmer
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
header {* Operational evaluation (big-step) semantics of Java expressions and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
          statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     9
theory Evaln imports TypeSafe begin
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    10
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
text {*
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    13
Variant of @{term eval} relation with counter for bounded recursive depth. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    14
In principal @{term evaln} could replace @{term eval}.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    15
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    16
Validity of the axiomatic semantics builds on @{term evaln}. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    17
For recursive method calls the axiomatic semantics rule assumes the method ok 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    18
to derive a proof for the body. To prove the method rule sound we need to 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    19
perform induction on the recursion depth. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    20
For the completeness proof of the axiomatic semantics the notion of the most
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    21
general formula is used. The most general formula right now builds on the 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    22
ordinary evaluation relation @{term eval}. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    23
So sometimes we have to switch between @{term evaln} and @{term eval} and vice 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    24
versa. To make
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    25
this switch easy @{term evaln} also does all the technical accessibility tests 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    26
@{term check_field_access} and @{term check_method_access} like @{term eval}. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    27
If it would omit them @{term evaln} and @{term eval} would only be equivalent 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    28
for welltyped, and definitely assigned terms.
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    31
inductive2
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    32
  evaln	:: "[prog, state, term, nat, vals, state] \<Rightarrow> bool"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    33
    ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    34
  and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    35
    ("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    36
  and eval_n:: "[prog, state, expr, val, nat, state] \<Rightarrow> bool"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    37
    ("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    38
  and evalsn :: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    39
    ("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    40
  and execn	:: "[prog, state, stmt, nat, state] \<Rightarrow> bool"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    41
    ("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    42
  for G :: prog
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    43
where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    45
  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    46
| "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,  s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    47
| "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,  s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    48
| "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,  s')"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    50
--{* propagation of abrupt completion *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    52
| Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    55
--{* evaluation of variables *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    57
| LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    59
| FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    60
	  (v,s2') = fvar statDeclC stat fn a s2;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    61
          s3 = check_field_access G accC statDeclC fn stat a s2'\<rbrakk> \<Longrightarrow>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    62
	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s3"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    64
| AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1 ; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2; 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    71
--{* evaluation of expressions *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    73
| NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    77
| NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<midarrow>n\<rightarrow> s2; 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    81
| Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
	  s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    85
| Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    89
| Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    91
| UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
    92
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
    93
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    94
| BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; 
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
    95
           G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
    96
            \<succ>\<midarrow>n\<rightarrow> (In1 v2,s2)\<rbrakk> 
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
    97
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
    98
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
    99
| Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   101
| Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   104
| Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
          G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   108
| Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
          G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   112
| Call:	
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   115
    s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   116
    s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   117
    G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   118
   \<rbrakk>
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   119
   \<Longrightarrow> 
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   120
    G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s4)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   122
| Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   125
| Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   126
          s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   127
                         abrupt s2 = Some (Jump (Cont l)))
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   128
                  then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   129
                  else s2)\<rbrakk>\<Longrightarrow>
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   130
         G\<turnstile>Norm s0 \<midarrow>Body D c
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   131
          -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s3"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   133
--{* evaluation of expression lists *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   135
| Nil:
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   138
| Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   143
--{* execution of statements *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   145
| Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   147
| Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   150
| Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   151
                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   153
| Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   157
| If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   161
| Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   162
	  if the_Bool b 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
             then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
	     else s3 = s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
  
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   168
| Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
  
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   170
| Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   173
| Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
	  if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
          \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   178
| Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   179
	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   180
          s3=(if (\<exists> err. x1=Some (Error err)) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   181
              then (x1,s1) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   182
              else abupd (abrupt_if (x1\<noteq>None) x1) s2)\<rbrakk> \<Longrightarrow>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   183
              G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
  
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   185
| Init:	"\<lbrakk>the (class G C) = c;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
	  if inited C (globs s0) then s3 = Norm s0
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
	  else (G\<turnstile>Norm (init_class_obj G C s0)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
	          \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
	        G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
                s3 = restore_lvars s1 s2)\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
          \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
monos
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
  if_def2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
declare split_if     [split del] split_if_asm     [split del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
        option.split [split del] option.split_asm [split del]
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   199
        not_None_eq [simp del] 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   200
        split_paired_All [simp del] split_paired_Ex [simp del]
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   201
ML_setup {*
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17589
diff changeset
   202
change_simpset (fn ss => ss delloop "split_all_tac");
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   203
*}
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   204
inductive_cases2 evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   206
inductive_cases2 evaln_elim_cases:
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   207
	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   208
	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   209
        "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   210
        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   211
	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   212
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   213
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   214
        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   215
        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   216
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   217
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   218
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   219
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   220
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   221
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   222
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   223
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   224
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   225
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   226
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   227
	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   228
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   229
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   230
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   231
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   232
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   233
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   234
	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   235
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   236
	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   237
	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   238
        "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   239
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
declare split_if     [split] split_if_asm     [split] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
        option.split [split] option.split_asm [split]
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   242
        not_None_eq [simp] 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   243
        split_paired_All [simp] split_paired_Ex [simp]
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   244
ML_setup {*
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17589
diff changeset
   245
change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   246
*}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
  (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
  | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
apply (erule evaln_cases , auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
apply   (induct_tac "a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   256
text {* The following simplification procedures set up the proper injections of
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   257
 terms and their corresponding values in the evaluation relation:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   258
 E.g. an expression 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   259
 (injection @{term In1l} into terms) always evaluates to ordinary values 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   260
 (injection @{term In1} into generalised values @{term vals}). 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   261
*}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   262
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   263
lemma evaln_expr_eq: "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   264
  by (auto, frule evaln_Inj_elim, auto)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   265
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   266
lemma evaln_var_eq: "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   267
  by (auto, frule evaln_Inj_elim, auto)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   268
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   269
lemma evaln_exprs_eq: "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   270
  by (auto, frule evaln_Inj_elim, auto)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   271
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   272
lemma evaln_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<midarrow>n\<rightarrow> s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   273
  by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   274
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
ML_setup {*
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   276
fun enf name lhs =
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
let
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
  fun is_Inj (Const (inj,_) $ _) = true
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
    | is_Inj _                   = false
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   280
  fun pred (_ $ _ $ _ $ _ $ _ $ x $ _) = is_Inj x
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
in
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 13384
diff changeset
   282
  cond_simproc name lhs pred (thm name)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
end;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   285
val evaln_expr_proc  = enf "evaln_expr_eq"  "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')";
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   286
val evaln_var_proc   = enf "evaln_var_eq"   "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   287
val evaln_exprs_proc = enf "evaln_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   288
val evaln_stmt_proc  = enf "evaln_stmt_eq"  "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')";
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
declare evaln_AbruptIs [intro!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   295
lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   296
proof -
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   297
  { fix s t v s'
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   298
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   299
         normal: "normal s" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   300
         callee: "t=In1l (Callee l e)"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   301
    then have "False" by induct auto
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   302
  }
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   303
  then show ?thesis
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   304
    by (cases s') fastsimp 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   305
qed
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   306
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   307
lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   308
proof -
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   309
  { fix s t v s'
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   310
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   311
         normal: "normal s" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   312
         callee: "t=In1l (InsInitE c e)"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   313
    then have "False" by induct auto
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   314
  }
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   315
  then show ?thesis
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   316
    by (cases s') fastsimp
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   317
qed
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   318
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   319
lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   320
proof -
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   321
  { fix s t v s'
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   322
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   323
         normal: "normal s" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   324
         callee: "t=In2 (InsInitV c w)"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   325
    then have "False" by induct auto
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   326
  }  
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   327
  then show ?thesis
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   328
    by (cases s') fastsimp
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   329
qed
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   330
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   331
lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   332
proof -
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   333
  { fix s t v s'
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   334
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   335
         normal: "normal s" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   336
         callee: "t=In1r (FinA a c)"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   337
    then have "False" by induct auto
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   338
  } 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   339
  then show ?thesis
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   340
    by (cases s') fastsimp
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   341
qed
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   342
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
 fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
apply (erule evaln_cases , auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
lemma evaln_abrupt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
 "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
  w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
apply (frule evaln_abrupt_lemma, auto)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
local
12919
d6a0d168291e removed theory Option;
wenzelm
parents: 12859
diff changeset
   357
  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
    | is_Some _ = false
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   359
  fun pred (_ $ _ $ _ $ _ $ _ $ _ $ x) = is_Some x
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
  val evaln_abrupt_proc = 
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 13384
diff changeset
   362
 cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
end;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
Addsimprocs [evaln_abrupt_proc]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
by (auto intro!: evaln.Lit)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
lemma CondI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
 "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
  G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
by (auto intro!: evaln.Cond)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
by (auto intro!: evaln.Skip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
lemma evaln_ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<midarrow>n\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
by (auto intro!: evaln.Expr)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
lemma evaln_CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
by (auto intro!: evaln.Comp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
lemma evaln_IfI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
 "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
  G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
by (auto intro!: evaln.If)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
by (erule evaln_cases, auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   402
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   403
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   404
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   405
section {* evaln implies eval *}
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   406
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   407
lemma evaln_eval:  
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   408
  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   409
  shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   410
using evaln 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   411
proof (induct)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   412
  case (Loop s0 e n b s1 c s2 l s3)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   413
  have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   414
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   415
  have "if the_Bool b
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   416
        then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   417
             G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   418
        else s3 = s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   419
    using Loop.hyps by simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   420
  ultimately show ?case by (rule eval.Loop)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   421
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   422
  case (Try s0 c1 n s1 s2 C vn c2 s3)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   423
  have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   424
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   425
  have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   426
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   427
  have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   428
    using Try.hyps by simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   429
  ultimately show ?case by (rule eval.Try)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   430
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   431
  case (Init C c s0 s3 n s1 s2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   432
  have "the (class G C) = c".
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   433
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   434
  have "if inited C (globs s0) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   435
           then s3 = Norm s0
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   436
           else G\<turnstile>Norm ((init_class_obj G C) s0) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   437
                  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   438
                G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   439
                s3 = (set_lvars (locals (store s1))) s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   440
    using Init.hyps by simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   441
  ultimately show ?case by (rule eval.Init)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   442
qed (rule eval.intros,(assumption+ | assumption?))+
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   443
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   444
lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   445
apply (frule Suc_le_D)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   446
apply fast
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   447
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   448
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   449
lemma evaln_nonstrict [rule_format (no_asm), elim]: 
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   450
  "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   451
apply (erule evaln.induct)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   452
apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   453
  REPEAT o smp_tac 1, 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   454
  resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   455
(* 3 subgoals *)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   456
apply (auto split del: split_if)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   457
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   458
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   459
lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   460
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   461
lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2')\<rbrakk> \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   462
             G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1') \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2')"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   463
by (fast intro: le_maxI1 le_maxI2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   464
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   465
corollary evaln_max2E [consumes 2]:
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   466
  "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   467
    \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1');G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2') \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   468
by (drule (1) evaln_max2) simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   469
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   470
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   471
lemma evaln_max3: 
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   472
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3')\<rbrakk> \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   473
 G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1') \<and>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   474
 G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   475
 G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   476
apply (drule (1) evaln_max2, erule thin_rl)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   477
apply (fast intro!: le_maxI1 le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   478
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   479
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   480
corollary evaln_max3E: 
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   481
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3');
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   482
   \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1');
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   483
    G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2'); 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   484
    G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   485
   \<rbrakk> \<Longrightarrow> P
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   486
  \<rbrakk> \<Longrightarrow> P"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   487
by (drule (2) evaln_max3) simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   488
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   489
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   490
lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   491
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   492
  have "n2 \<le> max n2 n3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   493
    by (rule le_maxI1)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   494
  also
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   495
  have "max n2 n3 \<le> max n1 (max n2 n3)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   496
    by (rule le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   497
  finally
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   498
  show ?thesis .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   499
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   500
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   501
lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   502
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   503
  have "n3 \<le> max n2 n3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   504
    by (rule le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   505
  also
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   506
  have "max n2 n3 \<le> max n1 (max n2 n3)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   507
    by (rule le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   508
  finally
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   509
  show ?thesis .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   510
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   511
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   512
ML {*
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   513
Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   514
*}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   515
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   516
section {* eval implies evaln *}
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   517
lemma eval_evaln: 
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   518
  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   519
  shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   520
using eval 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   521
proof (induct)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   522
  case (Abrupt xc s t)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   523
  obtain n where
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   524
    "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, (Some xc, s))"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   525
    by (iprover intro: evaln.Abrupt)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   526
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   527
next
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   528
  case Skip
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   529
  show ?case by (blast intro: evaln.Skip)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   530
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   531
  case (Expr s0 e v s1)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   532
  then obtain n where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   533
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   534
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   535
  then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   536
    by (rule evaln.Expr) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   537
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   538
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   539
  case (Lab s0 c s1 l)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   540
  then obtain n where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   541
    "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   542
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   543
  then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   544
    by (rule evaln.Lab)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   545
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   546
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   547
  case (Comp s0 c1 s1 c2 s2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   548
  then obtain n1 n2 where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   549
    "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   550
    "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   551
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   552
  then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   553
    by (blast intro: evaln.Comp dest: evaln_max2 )
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   554
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   555
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   556
  case (If s0 e b s1 c1 c2 s2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   557
  then obtain n1 n2 where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   558
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   559
    "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   560
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   561
  then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   562
    by (blast intro: evaln.If dest: evaln_max2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   563
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   564
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   565
  case (Loop s0 e b s1 c s2 l s3)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   566
  from Loop.hyps obtain n1 where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   567
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   568
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   569
  moreover from Loop.hyps obtain n2 where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   570
    "if the_Bool b 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   571
        then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   572
              G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   573
	else s3 = s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   574
    by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   575
  ultimately
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   576
  have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   577
    apply -
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   578
    apply (rule evaln.Loop)
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   579
    apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   580
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   581
    apply   (auto intro: evaln_nonstrict intro: le_maxI2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   582
    done
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   583
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   584
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   585
  case (Jmp s j)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   586
  have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   587
    by (rule evaln.Jmp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   588
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   589
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   590
  case (Throw s0 e a s1)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   591
  then obtain n where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   592
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   593
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   594
  then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   595
    by (rule evaln.Throw)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   596
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   597
next 
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   598
  case (Try s0 c1 s1 s2 catchC vn c2 s3)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   599
  from Try.hyps obtain n1 where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   600
    "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   601
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   602
  moreover 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   603
  have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   604
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   605
  from Try.hyps obtain n2 where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   606
    "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   607
    by fastsimp 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   608
  ultimately
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   609
  have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   610
    by (auto intro!: evaln.Try le_maxI1 le_maxI2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   611
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   612
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   613
  case (Fin s0 c1 x1 s1 c2 s2 s3)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   614
  from Fin obtain n1 n2 where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   615
    "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   616
    "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   617
    by iprover
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   618
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   619
  have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   620
                     then (x1, s1)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   621
                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   622
  ultimately 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   623
  have 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   624
    "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   625
    by (blast intro: evaln.Fin dest: evaln_max2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   626
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   627
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   628
  case (Init C c s0 s3 s1 s2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   629
  have     cls: "the (class G C) = c" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   630
  moreover from Init.hyps obtain n where
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   631
      "if inited C (globs s0) then s3 = Norm s0
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   632
       else (G\<turnstile>Norm (init_class_obj G C s0)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   633
	      \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   634
	           G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   635
                   s3 = restore_lvars s1 s2)"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   636
    by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   637
  ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   638
    by (rule evaln.Init)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   639
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   640
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   641
  case (NewC s0 C s1 a s2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   642
  then obtain n where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   643
    "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   644
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   645
  with NewC 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   646
  have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   647
    by (iprover intro: evaln.NewC)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   648
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   649
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   650
  case (NewA s0 T s1 e i s2 a s3)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   651
  then obtain n1 n2 where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   652
    "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   653
    "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   654
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   655
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   656
  have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   657
  ultimately
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   658
  have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   659
    by (blast intro: evaln.NewA dest: evaln_max2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   660
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   661
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   662
  case (Cast s0 e v s1 s2 castT)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   663
  then obtain n where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   664
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   665
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   666
  moreover 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   667
  have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   668
  ultimately
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   669
  have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   670
    by (rule evaln.Cast)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   671
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   672
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   673
  case (Inst s0 e v s1 b T)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   674
  then obtain n where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   675
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   676
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   677
  moreover 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   678
  have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   679
  ultimately
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   680
  have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   681
    by (rule evaln.Inst)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   682
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   683
next
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   684
  case (Lit s v)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   685
  have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   686
    by (rule evaln.Lit)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   687
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   688
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   689
  case (UnOp s0 e v s1 unop)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   690
  then obtain n where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   691
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   692
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   693
  hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   694
    by (rule evaln.UnOp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   695
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   696
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   697
  case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   698
  then obtain n1 n2 where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   699
    "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   700
    "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   701
               else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   702
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   703
  hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   704
          \<rightarrow> s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   705
    by (blast intro!: evaln.BinOp dest: evaln_max2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   706
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   707
next
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   708
  case (Super s )
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   709
  have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   710
    by (rule evaln.Super)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   711
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   712
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   713
  case (Acc s0 va v f s1)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   714
  then obtain n where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   715
    "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   716
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   717
  then
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   718
  have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   719
    by (rule evaln.Acc)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   720
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   721
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   722
  case (Ass s0 var w f s1 e v s2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   723
  then obtain n1 n2 where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   724
    "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   725
    "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   726
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   727
  then
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   728
  have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   729
    by (blast intro: evaln.Ass dest: evaln_max2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   730
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   731
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   732
  case (Cond s0 e0 b s1 e1 e2 v s2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   733
  then obtain n1 n2 where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   734
    "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   735
    "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   736
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   737
  then
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   738
  have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   739
    by (blast intro: evaln.Cond dest: evaln_max2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   740
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   741
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   742
  case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   743
  then obtain n1 n2 where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   744
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   745
    "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   746
    by iprover
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   747
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   748
  have "invDeclC = invocation_declclass G mode (store s2) a' statT 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   749
                       \<lparr>name=mn,parTs=pTs'\<rparr>" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   750
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   751
  have "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   752
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   753
  have "s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3".
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   754
  moreover 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   755
  from Call.hyps
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   756
  obtain m where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   757
    "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   758
    by iprover
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   759
  ultimately
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   760
  have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   761
            (set_lvars (locals (store s2))) s4"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   762
    by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   763
  thus ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   764
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   765
  case (Methd s0 D sig v s1)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   766
  then obtain n where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   767
    "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   768
    by iprover
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   769
  then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   770
    by (rule evaln.Methd)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   771
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   772
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   773
  case (Body s0 D s1 c s2 s3)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   774
  from Body.hyps obtain n1 n2 where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   775
    evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   776
    evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   777
    by (iprover)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   778
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   779
  have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   780
                     fst s2 = Some (Jump (Cont l))
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   781
                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   782
                 else s2)".
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   783
  ultimately
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   784
  have
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   785
     "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   786
       \<rightarrow> abupd (absorb Ret) s3"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   787
    by (iprover intro: evaln.Body dest: evaln_max2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   788
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   789
next
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   790
  case (LVar s vn )
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   791
  obtain n where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   792
    "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   793
    by (iprover intro: evaln.LVar)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   794
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   795
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   796
  case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   797
  then obtain n1 n2 where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   798
    "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   799
    "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   800
    by iprover
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   801
  moreover
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   802
  have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   803
       "(v, s2') = fvar statDeclC stat fn a s2" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   804
  ultimately
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   805
  have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   806
    by (iprover intro: evaln.FVar dest: evaln_max2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   807
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   808
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   809
  case (AVar s0 e1 a s1 e2 i s2 v s2')
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   810
  then obtain n1 n2 where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   811
    "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   812
    "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   813
    by iprover
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   814
  moreover 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   815
  have "(v, s2') = avar G i a s2" .
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   816
  ultimately 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   817
  have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   818
    by (blast intro!: evaln.AVar dest: evaln_max2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   819
  then show ?case ..
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   820
next
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   821
  case (Nil s0)
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   822
  show ?case by (iprover intro: evaln.Nil)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   823
next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18249
diff changeset
   824
  case (Cons s0 e v s1 es vs s2)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   825
  then obtain n1 n2 where 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   826
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   827
    "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   828
    by iprover
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   829
  then
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   830
  have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   831
    by (blast intro!: evaln.Cons dest: evaln_max2)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   832
  then show ?case ..
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   833
qed
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   834
       
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   835
end