Theory J1

(*  Title:      Jinja/Compiler/J1.thy
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

chapter ‹Compilation \label{cha:comp}›

section ‹An Intermediate Language›

theory J1 imports "../J/BigStep" begin

type_synonym expr1 = "nat exp"
type_synonym J1_prog = "expr1 prog"
type_synonym state1 = "heap × (val list)"

primrec
  max_vars :: "'a exp  nat"
  and max_varss :: "'a exp list  nat"
where
  "max_vars(new C) = 0"
| "max_vars(Cast C e) = max_vars e"
| "max_vars(Val v) = 0"
| "max_vars(e1 «bop» e2) = max (max_vars e1) (max_vars e2)"
| "max_vars(Var V) = 0"
| "max_vars(V:=e) = max_vars e"
| "max_vars(eF{D}) = max_vars e"
| "max_vars(FAss e1 F D e2) = max (max_vars e1) (max_vars e2)"
| "max_vars(eM(es)) = max (max_vars e) (max_varss es)"
| "max_vars({V:T; e}) = max_vars e + 1"
| "max_vars(e1;;e2) = max (max_vars e1) (max_vars e2)"
| "max_vars(if (e) e1 else e2) =
   max (max_vars e) (max (max_vars e1) (max_vars e2))"
| "max_vars(while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars(throw e) = max_vars e"
| "max_vars(try e1 catch(C V) e2) = max (max_vars e1) (max_vars e2 + 1)"

| "max_varss [] = 0"
| "max_varss (e#es) = max (max_vars e) (max_varss es)"

inductive
  eval1 :: "J1_prog  expr1  state1  expr1  state1  bool"
          ("_ 1 ((1_,/_) / (1_,/_))" [51,0,0,0,0] 81)
  and evals1 :: "J1_prog  expr1 list  state1  expr1 list  state1  bool"
           ("_ 1 ((1_,/_) [⇒]/ (1_,/_))" [51,0,0,0,0] 81)
  for P :: J1_prog
where

  New1:
  " new_Addr h = Some a; P  C has_fields FDTs; h' = h(a(C,init_fields FDTs)) 
   P 1 new C,(h,l)  addr a,(h',l)"
| NewFail1:
  "new_Addr h = None 
  P 1 new C, (h,l)  THROW OutOfMemory,(h,l)"

| Cast1:
  " P 1 e,s0  addr a,(h,l); h a = Some(D,fs); P  D * C 
   P 1 Cast C e,s0  addr a,(h,l)"
| CastNull1:
  "P 1 e,s0  null,s1 
  P 1 Cast C e,s0  null,s1"
| CastFail1:
  " P 1 e,s0  addr a,(h,l); h a = Some(D,fs); ¬ P  D * C 
   P 1 Cast C e,s0  THROW ClassCast,(h,l)"
| CastThrow1:
  "P 1 e,s0  throw e',s1 
  P 1 Cast C e,s0  throw e',s1"

| Val1:
  "P 1 Val v,s  Val v,s"

| BinOp1:
  " P 1 e1,s0  Val v1,s1; P 1 e2,s1  Val v2,s2; binop(bop,v1,v2) = Some v 
   P 1 e1 «bop» e2,s0  Val v,s2"
| BinOpThrow11:
  "P 1 e1,s0  throw e,s1 
  P 1 e1 «bop» e2, s0  throw e,s1"
| BinOpThrow21:
  " P 1 e1,s0  Val v1,s1; P 1 e2,s1  throw e,s2 
   P 1 e1 «bop» e2,s0  throw e,s2"

| Var1:
  " ls!i = v; i < size ls  
  P 1 Var i,(h,ls)  Val v,(h,ls)"

| LAss1:
  " P 1 e,s0  Val v,(h,ls); i < size ls; ls' = ls[i := v] 
   P 1 i:= e,s0  unit,(h,ls')"
| LAssThrow1:
  "P 1 e,s0  throw e',s1 
  P 1 i:= e,s0  throw e',s1"

| FAcc1:
  " P 1 e,s0  addr a,(h,ls); h a = Some(C,fs); fs(F,D) = Some v 
   P 1 eF{D},s0  Val v,(h,ls)"
| FAccNull1:
  "P 1 e,s0  null,s1 
  P 1 eF{D},s0  THROW NullPointer,s1"
| FAccThrow1:
  "P 1 e,s0  throw e',s1 
  P 1 eF{D},s0  throw e',s1"

| FAss1:
  " P 1 e1,s0  addr a,s1; P 1 e2,s1  Val v,(h2,l2);
    h2 a = Some(C,fs); fs' = fs((F,D)v); h2' = h2(a(C,fs')) 
   P 1 e1F{D}:= e2,s0  unit,(h2',l2)"
| FAssNull1:
  " P 1 e1,s0  null,s1;  P 1 e2,s1  Val v,s2 
   P 1 e1F{D}:= e2,s0  THROW NullPointer,s2"
| FAssThrow11:
  "P 1 e1,s0  throw e',s1 
  P 1 e1F{D}:= e2,s0  throw e',s1"
| FAssThrow21:
  " P 1 e1,s0  Val v,s1; P 1 e2,s1  throw e',s2 
   P 1 e1F{D}:= e2,s0  throw e',s2"

| CallObjThrow1:
  "P 1 e,s0  throw e',s1 
  P 1 eM(es),s0  throw e',s1"
| CallNull1:
  " P 1 e,s0  null,s1; P 1 es,s1 [⇒] map Val vs,s2 
   P 1 eM(es),s0  THROW NullPointer,s2"
| Call1:
  " P 1 e,s0  addr a,s1; P 1 es,s1 [⇒] map Val vs,(h2,ls2);
    h2 a = Some(C,fs); P  C sees M:TsT = body in D;
    size vs = size Ts; ls2' = (Addr a) # vs @ replicate (max_vars body) undefined;
    P 1 body,(h2,ls2')  e',(h3,ls3) 
   P 1 eM(es),s0  e',(h3,ls2)"
| CallParamsThrow1:
  " P 1 e,s0  Val v,s1; P 1 es,s1 [⇒] es',s2;
     es' = map Val vs @ throw ex # es2 
    P 1 eM(es),s0  throw ex,s2"

| Block1:
  "P 1 e,s0  e',s1  P 1 Block i T e,s0  e',s1"

| Seq1:
  " P 1 e0,s0  Val v,s1; P 1 e1,s1  e2,s2 
   P 1 e0;;e1,s0  e2,s2"
| SeqThrow1:
  "P 1 e0,s0  throw e,s1 
  P 1 e0;;e1,s0  throw e,s1"

| CondT1:
  " P 1 e,s0  true,s1; P 1 e1,s1  e',s2 
   P 1 if (e) e1 else e2,s0  e',s2"
| CondF1:
  " P 1 e,s0  false,s1; P 1 e2,s1  e',s2 
   P 1 if (e) e1 else e2,s0  e',s2"
| CondThrow1:
  "P 1 e,s0  throw e',s1 
  P 1 if (e) e1 else e2, s0  throw e',s1"

| WhileF1:
  "P 1 e,s0  false,s1 
  P 1 while (e) c,s0  unit,s1"
| WhileT1:
  " P 1 e,s0  true,s1; P 1 c,s1  Val v1,s2;
    P 1 while (e) c,s2  e3,s3 
   P 1 while (e) c,s0  e3,s3"
| WhileCondThrow1:
  "P 1 e,s0  throw e',s1 
  P 1 while (e) c,s0  throw e',s1"
| WhileBodyThrow1:
  " P 1 e,s0  true,s1; P 1 c,s1  throw e',s2
   P 1 while (e) c,s0  throw e',s2"

| Throw1:
  "P 1 e,s0  addr a,s1 
  P 1 throw e,s0  Throw a,s1"
| ThrowNull1:
  "P 1 e,s0  null,s1 
  P 1 throw e,s0  THROW NullPointer,s1"
| ThrowThrow1:
  "P 1 e,s0  throw e',s1 
  P 1 throw e,s0  throw e',s1"

| Try1:
  "P 1 e1,s0  Val v1,s1 
  P 1 try e1 catch(C i) e2,s0  Val v1,s1"
| TryCatch1:
  " P 1 e1,s0  Throw a,(h1,ls1);
    h1 a = Some(D,fs); P  D * C; i < length ls1;
    P 1 e2,(h1,ls1[i:=Addr a])  e2',(h2,ls2) 
   P 1 try e1 catch(C i) e2,s0  e2',(h2,ls2)"
| TryThrow1:
  " P 1 e1,s0  Throw a,(h1,ls1); h1 a = Some(D,fs); ¬ P  D * C 
   P 1 try e1 catch(C i) e2,s0  Throw a,(h1,ls1)"

| Nil1:
  "P 1 [],s [⇒] [],s"

| Cons1:
  " P 1 e,s0  Val v,s1; P 1 es,s1 [⇒] es',s2 
   P 1 e#es,s0 [⇒] Val v # es',s2"
| ConsThrow1:
  "P 1 e,s0  throw e',s1 
  P 1 e#es,s0 [⇒] throw e' # es, s1"

(*<*)
lemmas eval1_evals1_induct = eval1_evals1.induct [split_format (complete)]
  and eval1_evals1_inducts = eval1_evals1.inducts [split_format (complete)]
(*>*)

lemma eval1_preserves_len:
  "P 1 e0,(h0,ls0)  e1,(h1,ls1)  length ls0 = length ls1"
and evals1_preserves_len:
  "P 1 es0,(h0,ls0) [⇒] es1,(h1,ls1)  length ls0 = length ls1"
(*<*)by (induct rule:eval1_evals1_inducts, simp_all)(*>*)


lemma evals1_preserves_elen:
  "es' s s'. P 1 es,s [⇒] es',s'  length es = length es'"
(*<*)by(induct es type:list) (auto elim:evals1.cases)(*>*)


lemma eval1_final: "P 1 e,s  e',s'  final e'"
 and evals1_final: "P 1 es,s [⇒] es',s'  finals es'"
(*<*)by(induct rule:eval1_evals1.inducts, simp_all)(*>*)


end