(*File: OBJ.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory OBJ imports Main begin

section‹Base-line non-interference with objects›

text‹\label{sec:Objects} We now extend the encoding for base-line
 -interference to a language with objects. The development follows
  structure of Sections \ref{sec:IMP} to
 ref{sec:BaseLineNI}. Syntax and operational semantics are defined in
  \ref{sec:ObjLanguage}, the axiomatic semantics in Section
 ref{sec:ObjLogic}. The generalised definition of non-interference is
  in \ref{sec:ObjNI}, the derived proof rules in Section
 ref{sec:ObjDerivedRules}, and a type system in the style of Volpano
  al.~in Section \ref{sec:ObjTypeSystem}. Finally, Section
 ref{sec:contextObj} concludes with results on contextual closure.›

subsection ‹Syntax and operational semantics›
text‹\label{sec:ObjLanguage}›

text‹First, some operations for association lists›

primrec lookup :: "('a × 'b) list → 'a → 'b option"
where
"lookup [] l = None" |
"lookup (h # t) l = (if (fst h)=l then Some (snd h) else lookup t l)" 

definition Dom::"('a × 'b) list → 'a set"
where "Dom L = {l . ∃ a . lookup L l = Some a}"

(*<*)
lemma lookupNoneAppend[rule_format]: 
"∀ l L2. (lookup L1 l = None ⟶ lookup L2 l = None ⟶ lookup (L1 @ L2) l = None)"
by (induct L1, simp+)

lemma DomAppendUnion[rule_format]: "∀ ab. Dom (a @ ab) = Dom a ∪ Dom ab"
apply (induct a)
apply (simp add: Dom_def)
apply (simp add: Dom_def)
apply clarsimp apply fast
done

lemma DomAppend: "Dom L ⊆ Dom((a, b) # L)"
by (simp add: Dom_def, auto)

lemma lookupSomeAppend1[rule_format]:
"∀ L2 l c . lookup L1 l = Some c ⟶ lookup (L1 @ L2) l = Some c"
by (induct L1, simp, simp)

lemma DomUnion[rule_format]:"Dom ((a,b) # L) = {a} ∪ Dom L"
by (simp add: Dom_def DomAppendUnion, fast)

lemma lookupSomeAppend2[rule_format]:
"∀ l c L2 . lookup L2 l = Some c ⟶ Dom L1 ∩ Dom L2 = {} ⟶ lookup (L1 @ L2) l = Some c"
apply (induct L1)
apply (simp add: Dom_def)
apply clarsimp
  apply rule
    apply clarsimp apply (subgoal_tac "l:Dom L2") apply (simp add: DomUnion) 
   apply (simp add: Dom_def) 
apply clarsimp
  apply (erule_tac x=l in allE)
  apply (erule_tac x=c in allE)
  apply (erule_tac x=L2 in allE)
  apply simp apply (erule impE) apply (simp add: DomUnion) 
  apply simp
done
(*>*)

text‹Abstract types of variables, class names, field names, and
 .›

typedecl Var
typedecl Class
typedecl Field
typedecl Location

text‹References are either null or a location. Values are either
  or references.›

datatype Ref = Nullref | Loc Location

datatype Val = RVal Ref | IVal int 

text‹The heap is a finite map from locations to objects. Objects have
  dynamic class and a field map.›

type_synonym Object = "Class × ((Field × Val) list)"
type_synonym Heap = "(Location × Object) list"

text‹Stores contain values for all variables, and states are pairs of
  and heaps.›

type_synonym Store = "Var → Val"

definition update :: "Store → Var → Val → Store"
where "update s x v = (λ y . if x=y then v else s y)"

type_synonym State = "Store × Heap"

text‹Arithmetic and boolean expressions are as before.›

datatype Expr = 
    varE Var 
  | valE Val
  | opE "Val → Val → Val" Expr Expr

datatype BExpr = compB "Val → Val → bool" Expr Expr

text‹The same applies to their semantics.›

primrec evalE::"Expr → Store → Val"
where
"evalE (varE x) s = s x" |
"evalE (valE v) s = v" |
"evalE (opE f e1 e2) s = f (evalE e1 s) (evalE e2 s)"

primrec evalB::"BExpr → Store → bool"
where
"evalB (compB f e1 e2) s = f (evalE e1 s) (evalE e2 s)"

text‹The category of commands is extended by instructions for
  a fresh object, obtaining a value from a field and assigning
  value to a field.›

datatype OBJ =
    Skip 
  | Assign Var Expr
  | New Var Class
  | Get Var Var Field
  | Put Var Field Expr
  | Comp OBJ OBJ
  | While BExpr OBJ
  | Iff BExpr OBJ OBJ
  | Call

text‹The body of the procedure is identified by the same constant as
 .›

consts body :: OBJ

text‹The operational semantics is again a standard big-step
 .›

inductive_set Semn :: "(State × OBJ × nat × State) set"
where
SemSkip: "s=t ==> (s,Skip,1, t):Semn"

| SemAssign:
  "[ t = (update (fst s) x (evalE e (fst s)), snd s)]
  ==> (s, Assign x e, 1, t):Semn"

| SemNew:
  "[l ∉ Dom (snd s);
       t = (update (fst s) x (RVal (Loc l)), (l,(C,[])) # (snd s))]
  ==> (s, New x C, 1, t):Semn"

| SemGet:
  "[(fst s) y = RVal(Loc l); lookup (snd s) l = Some(C,Flds);
       lookup Flds F = Some v; t = (update (fst s) x v, snd s)]
  ==> (s, Get x y F, 1, t):Semn"

| SemPut:
  "[(fst s) x = RVal(Loc l); lookup (snd s) l = Some(C,Flds);
       t = (fst s, (l,(C,(F,evalE e (fst s)) # Flds)) # (snd s))]
  ==> (s, Put x F e, 1, t):Semn"

| SemComp:
  "[ (s, c, n, r):Semn; (r,d, m, t):Semn; k=(max n m)+1]
  ==> (s, Comp c d, k, t):Semn"

| SemWhileT:
  "[evalB b (fst s); (s,c, n, r):Semn; (r, While b c, m, t):Semn; k=((max n m)+1)]
  ==> (s, While b c, k, t):Semn"

| SemWhileF:
  "[¬ (evalB b (fst s)); t=s] ==> (s, While b c, 1, t):Semn"

| SemTrue:
  "[evalB b (fst s); (s,c1, n, t):Semn]
  ==> (s, Iff b c1 c2, n+1, t):Semn"

| SemFalse:
  "[¬ (evalB b (fst s)); (s,c2, n, t):Semn]
  ==> (s, Iff b c1 c2, n+1, t):Semn"

| SemCall: "[ (s,body,n, t):Semn] ==> (s,Call,n+1, t):Semn"

abbreviation
  SemN  :: "[State, OBJ, nat, State] → bool"   (‹ _ , _ →_{_} _ ›)
where
"s,c →_n t == (s,c,n,t) : Semn"

text‹Often, the height index does not matter, so we define a notion
  it.›

definition
Sem :: "[State, OBJ, State] → bool" (‹_ , _ ⇓ _ › 1000)
where "s,c ⇓ t = (∃ n. s,c →_n t)"

inductive_cases Sem_eval_cases: 
 "s,Skip →_n t"
 "s,(Assign x e) →_n t"
 "s,(New x C) →_n t"
 "s,(Get x y F) →_n t"
 "s,(Put x F e) →_n t"
 "s,(Comp c1 c2) →_n t"
 "s,(While b c) →_n t"
 "s,(Iff b c1 c2) →_n t"
 "s, Call →_n t"

(*<*)
lemma Sem_no_zero_height_derivsAux: "∀ s t. ((s, c →₀ t) ⟶ False)"
by (induct_tac c, auto elim: Sem_eval_cases)
(*>*)
lemma Sem_no_zero_height_derivs: "(s, c →₀ t) ==> False"
(*<*)by (insert Sem_no_zero_height_derivsAux, fastforce)(*>*)

text‹Determinism does not hold as allocation is nondeterministic.›

text‹End of theory OBJ›
end