(* Isabelle/HOL formalization of FJEU with strings, the semantics, the
   base region type system, its soundness proof, string operation
   contexts and their interpretation *)

(* This theory has been tested with Isabelle versions 2007 and 2009. *)

theory RegionTypeSystems imports Main begin

typedecl Var
typedecl Class
typedecl Method
typedecl Field


datatype Fjeu =
  FjNull
| FjVar Var
| FjNew Class
| FjString string (*constructor for class String*)
| FjLet Var Fjeu Fjeu
| FjCond Var Var Fjeu Fjeu
| FjIfinst Var Class Fjeu Fjeu
| FjGet Var Field
| FjGetQ Var Field
| FjPut Var Field Var
| FjPutQ Var Field Var
| FjInvoke Var Method "Var list"

typedecl Loc

datatype Val = 
  nullVal
| locVal Loc

datatype HeapObj = 
  Obj Class "Field ~=> Val"
| String string

types Heap = "Loc ~=> HeapObj"

types Store = "Var ~=> Val"

constdefs defaultObj::"Class => HeapObj"
"defaultObj C \<equiv> Obj C (\<lambda> f. Some nullVal)"

constdefs stringObj::"string => HeapObj"
"stringObj s \<equiv> String s"

inductive_set mkStore::"(('a ~=> 'b) \<times> ('c list) \<times> ('a list) \<times> ('c ~=> 'b)) set"
where
mkStoreNull:"\<lbrakk>t = (\<lambda> x . None) \<rbrakk>
             \<Longrightarrow> (s,[],[],t):mkStore"
|
mkStoreCons:"\<lbrakk>(s,pars,args,r):mkStore; s y = Some v; 
                      t = r(x:=Some v) \<rbrakk>
             \<Longrightarrow> (s,x#pars,y#args,t):mkStore"

lemma mkStore_determ[rule_format]:
  "(s, pars, args, t) : mkStore ==> \<forall> tt . (s, pars, args, tt) : mkStore --> tt=t"
apply (erule mkStore.induct)
apply clarsimp
  apply (erule mkStore.cases, clarsimp) apply clarsimp
apply clarify apply (erule thin_rl)
  apply (erule mkStore.cases, clarsimp) apply clarsimp
done

lemma mkStore_existsAux[rule_format]:
  "\<forall> pars args . length pars = N --> length args = N --> 
     (\<forall> n . n < length args --> (\<exists> v . s (args!n) = Some v)) --> 
     (\<exists> t . (s,pars,args,t):mkStore)"
apply (induct N)
apply clarsimp apply (rule, rule mkStoreNull) apply simp
apply clarsimp
  apply (case_tac pars, clarsimp, clarsimp) apply (rename_tac p pars)
  apply (case_tac args, clarsimp, clarsimp) apply (rename_tac a args)
  apply (erule_tac x=pars in allE, clarsimp)
  apply (erule_tac x=args in allE, clarsimp)
  apply (erule impE) apply clarsimp apply (erule_tac x="Suc n" in allE, clarsimp)
  apply (erule exE)
  apply (erule_tac x=0 in allE, clarsimp)
  apply (rule, erule mkStoreCons) apply assumption apply simp
done
lemma mkStore_exists:
  "[| length pars = length args;
      \<forall> n . n < length args --> (\<exists> v . s (args!n) = Some v)|]
   ==> \<exists> t . (s,pars,args,t):mkStore"
apply (rule mkStore_existsAux) apply simp apply simp apply fast
done

lemma mkStore_length:"(s, pars, args, t) : mkStore ==> length pars = length args"
apply (erule mkStore.induct)
apply simp
apply simp
done

lemma mkStore_dom_lookup[rule_format]:
  "(s, pars, args, t) : mkStore ==> \<forall> n . n < length args --> (\<exists> v . s (args!n) = Some v)"
apply (erule mkStore.induct)
apply simp
apply clarsimp apply (case_tac n, clarsimp) apply clarsimp
done

consts subclassOf::"Class => Class => bool"
       mbody::"Class => Method ~=> (Var list \<times> Fjeu)"

consts StringConcat::Method


(* operational semantics *)

inductive_set
  FjeuOpsem::"(Store \<times> Heap \<times> 
               Fjeu \<times> Val \<times> Heap) set"
where
OpsemNull:"\<lbrakk>v=nullVal; k=h\<rbrakk>
       \<Longrightarrow> (s,h,FjNull,v,k) : FjeuOpsem"
|
OpsemVar:"\<lbrakk> s x = Some v; k=h\<rbrakk>
       \<Longrightarrow> (s,h,FjVar x,v,k) : FjeuOpsem"
|
OpsemNew:"\<lbrakk> h a = None; v=locVal a; k=h(a:=Some (defaultObj C))\<rbrakk>
       \<Longrightarrow> (s,h,FjNew C,v,k) : FjeuOpsem"
|
OpsemString:"\<lbrakk> h a = None; v=locVal a; k=h(a:=Some (stringObj S))\<rbrakk>
       \<Longrightarrow> (s,h,FjString S,v,k) : FjeuOpsem"
|
OpsemLet:"\<lbrakk> (s,h,e1,v1,h1) : FjeuOpsem;
                 (s(x:=Some v1),h1,e2,v,k) : FjeuOpsem\<rbrakk>
       \<Longrightarrow> (s,h,FjLet x e1 e2,v,k) : FjeuOpsem"
|
OpsemCond:"\<lbrakk> ((s,h,e1,v,k) : FjeuOpsem \<and> s x = s y) \<or>
             ((s,h,e2,v,k) : FjeuOpsem \<and> \<not> s x = s y)\<rbrakk>
       \<Longrightarrow> (s,h,FjCond x y e1 e2,v,k) : FjeuOpsem"
|
OpsemIf:"\<lbrakk> s x = Some (locVal a); h a = Some (Obj C F);
                   ((s,h,e1,v,k) : FjeuOpsem \<and> subclassOf C E) \<or>
                   ((s,h,e2,v,k) : FjeuOpsem \<and> \<not> subclassOf C E)\<rbrakk>
       \<Longrightarrow> (s,h,FjIfinst x E e1 e2,v,k) : FjeuOpsem"
|
OpsemGet:"\<lbrakk> s x = Some (locVal a); h a = Some (Obj C F);
                    F f = Some v; k=h\<rbrakk>
       \<Longrightarrow> (s,h,FjGet x f,v,k) : FjeuOpsem"
|
OpsemGetQ:"\<lbrakk> s x = Some (locVal a); h a = Some (Obj C F);
                    F f = Some v; k=h\<rbrakk>
       \<Longrightarrow> (s,h,FjGetQ x f,v,k) : FjeuOpsem"
|
OpsemPut:"\<lbrakk> s x = Some (locVal a); h a = Some (Obj C F);
                    s y = Some v; G = F(f:=Some v); 
                    k=h(a:=Some (Obj C G))\<rbrakk>
       \<Longrightarrow> (s,h,FjPut x f y,v,k) : FjeuOpsem"
|
OpsemPutQ:"\<lbrakk> s x = Some (locVal a); h a = Some (Obj C F);
                    s y = Some v; G = F(f:=Some v); 
                    k=h(a:=Some (Obj C G))\<rbrakk>
       \<Longrightarrow> (s,h,FjPutQ x f y,v,k) : FjeuOpsem"
|
OpsemStringConcat: 
   "[| s x = Some(locVal Xa); h Xa = Some(String XString); 
       s y = Some(locVal Ya); h Ya = Some(String YString);
       h a = None; 
       case YString of 
          [] => (k=h \<and> v = locVal Xa)
        | c#str => (v=locVal a \<and> k=h(a:=Some (stringObj (XString @ YString))))  |]
    ==> (s,h,FjInvoke x StringConcat [y],v,k) : FjeuOpsem"
|
OpsemInvoke:"\<lbrakk> m ~= StringConcat; s x = Some (locVal a); h a = Some(Obj C F);
                       mbody C m = Some (pars,e); (s,pars,args,t):mkStore;
                       (t, h, e,v,k):FjeuOpsem\<rbrakk>
       \<Longrightarrow> (s,h,FjInvoke x m args,v,k) : FjeuOpsem"

inductive_cases NullOpsem[elim!]:"(s,h,FjNull,v,k):FjeuOpsem"
inductive_cases VarOpsem[elim!]:"(s,h,FjVar x,v,k):FjeuOpsem"
inductive_cases NewOpsem[elim!]:"(s,h,FjNew C,v,k):FjeuOpsem"
inductive_cases StringOpsem[elim!]:"(s,h,FjString S,v,k):FjeuOpsem"
inductive_cases GetOpsem[elim!]:"(s,h,FjGet x f,v,k):FjeuOpsem"
inductive_cases GetQOpsem[elim!]:"(s,h,FjGetQ x f,v,k):FjeuOpsem"
inductive_cases PutOpsem[elim!]:"(s,h,FjPut x f y,v,k):FjeuOpsem"
inductive_cases PutQOpsem[elim!]:"(s,h,FjPutQ x f y,v,k):FjeuOpsem"
inductive_cases IfOpsem[elim!]:"(s,h,FjIfinst x E e1 e2,v,k):FjeuOpsem"
inductive_cases CondOpsem[elim!]:"(s,h,FjCond x y e1 e2,v,k):FjeuOpsem"
inductive_cases InvokeOpsem[elim!]:"(s,h,FjInvoke x m args,v,k):FjeuOpsem"
inductive_cases LetOpsem[elim!]:"(s,h,FjLet x e1 e2,v,k):FjeuOpsem"


(* Region type environments *)

typedecl Region

datatype TP = 
  stringTP "Region set"
| objTP Class "Region set"

constdefs subtypeOf::"TP => TP => bool"
"subtypeOf \<tau> \<sigma> \<equiv>
  (case \<tau> of (stringTP R) => (case \<sigma> of stringTP S => (R \<subseteq> S)
                                                 | objTP D S => False)
                | (objTP C R) => (case \<sigma> of (stringTP S) => False
                                                 | objTP D S => subclassOf C D \<and> R \<subseteq> S))"

axioms subclassOf_refl:"subclassOf C C"
axioms subclassOf_trans:"[|subclassOf C D; subclassOf D E |] ==> subclassOf C E"

lemma subtypeOf_refl:"subtypeOf \<tau> \<tau>"
apply (simp add: subtypeOf_def)
apply (case_tac \<tau>, clarsimp) apply clarsimp
apply (rule subclassOf_refl) 
done

lemma subtypeOf_trans:
 "[|subtypeOf \<tau> \<sigma>; subtypeOf \<sigma> \<omega> |] ==> subtypeOf \<tau> \<omega>"
apply (simp add: subtypeOf_def)
apply (case_tac \<tau>, clarsimp) 
  apply (case_tac \<sigma>, clarsimp) 
    apply (case_tac \<omega>, clarsimp) apply fast apply clarsimp
  apply clarsimp
apply clarsimp apply (rename_tac C R)
  apply (case_tac \<sigma>, clarsimp) apply clarsimp apply (rename_tac E T)
  apply (case_tac \<omega>, clarsimp) apply clarsimp apply (rename_tac D S)
  apply rule apply (erule subclassOf_trans) apply assumption 
  apply fast
done

types VarEnv = "Var ~=> TP"

types MethodTyping = "TP list \<times> TP"

constdefs Meth_subtypeOf::"MethodTyping => MethodTyping => bool"
"Meth_subtypeOf \<alpha> \<beta> \<equiv>
  (case \<alpha> of (\<tau>s,\<tau>) =>
     (case \<beta> of (\<sigma>s,\<sigma>) =>
       length \<tau>s = length \<sigma>s \<and>
       (\<forall> n . n < length \<sigma>s --> subtypeOf (\<sigma>s!n) (\<tau>s!n)) \<and>
       subtypeOf \<tau> \<sigma>))"

lemma Meth_subtypeOf_trans:
  "[|  Meth_subtypeOf \<alpha> \<beta>;  Meth_subtypeOf \<beta> \<gamma>|]
   ==>  Meth_subtypeOf \<alpha> \<gamma>"
apply (simp add: Meth_subtypeOf_def) apply clarsimp
apply (rule, clarsimp) apply (erule_tac x=n in allE, clarsimp)
                       apply (erule_tac x=n in allE, clarsimp)
                       apply (erule subtypeOf_trans, assumption)
apply (erule subtypeOf_trans, assumption)
done

consts fields :: "Class \<Rightarrow> Field set" 

consts getview::"Class => Region => Field ~=> TP"
axioms getviewObjTP:"getview C r f = Some \<tau> ==> (\<exists> D R . \<tau>= objTP D R)"

consts setview::"Class => Region => Field ~=> TP"
axioms setviewObjTP:"setview C r f = Some \<tau> ==> (\<exists> D R . \<tau>= objTP D R)"

consts MethViews::"Class => Region => Method => (MethodTyping set)"

constdefs argTypes::"VarEnv => Var list => TP list => bool"
"argTypes \<Gamma> args \<tau>s \<equiv> length args = length \<tau>s \<and>
            (\<forall> n . n < length args --> \<Gamma> (args!n) = Some (\<tau>s!n))"

constdefs VarEnvSubtyping::"VarEnv => VarEnv => bool"
"VarEnvSubtyping \<Gamma> \<Theta> \<equiv>
     \<forall> x \<omega> . \<Theta> x = Some \<omega> -->
              (\<exists> \<theta> . \<Gamma> x = Some \<theta> \<and> subtypeOf \<theta> \<omega>)"

consts LCS::"Class \<Rightarrow> Class \<Rightarrow> Class"
axioms LCS1:"subclassOf C (LCS C D)"
axioms LCS2:"subclassOf D (LCS C D)"
axioms LCS3:"\<lbrakk>subclassOf C E; subclassOf D E\<rbrakk> \<Longrightarrow> subclassOf (LCS C D) E"
axioms subclassOf_antisymm: "\<lbrakk>subclassOf C D; subclassOf D C\<rbrakk> \<Longrightarrow> C=D"
  

consts is_meet_of ::"TP \<Rightarrow> TP \<Rightarrow> TP \<Rightarrow> bool"
primrec
"is_meet_of (stringTP W) \<sigma> \<tau> = (\<exists> S R . \<sigma> = stringTP S \<and> \<tau> = stringTP R \<and> S \<union> R \<subseteq> W)" 
"is_meet_of (objTP E W) \<sigma> \<tau> = (\<exists> C S D R . \<sigma> = objTP C S \<and> \<tau> = objTP D R \<and> S \<union> R \<subseteq> W \<and> 
                                           subclassOf C E \<and> subclassOf D E)" 

constdefs meet:: "TP \<Rightarrow> TP \<Rightarrow> TP \<Rightarrow> bool"
"meet \<sigma> \<tau> \<omega> \<equiv> is_meet_of \<omega> \<sigma> \<tau> \<and> (\<forall> \<nu> .  is_meet_of \<nu> \<sigma> \<tau> \<longrightarrow> subtypeOf \<omega> \<nu>)"

constdefs vee::"TP \<Rightarrow> TP \<Rightarrow> TP option"
"vee \<sigma> \<tau> \<equiv> case \<sigma> of 
     stringTP S \<Rightarrow> (case \<tau> of stringTP R \<Rightarrow> Some (stringTP (S \<union> R))
                            | objTP D R \<Rightarrow> None)
   | objTP C S \<Rightarrow> (case \<tau> of stringTP R \<Rightarrow> None
                            | objTP D R \<Rightarrow> Some (objTP (LCS C D) (S \<union> R)))"

constdefs Meet::"TP set \<Rightarrow> TP \<Rightarrow> bool"
"Meet X \<omega> \<equiv>  (\<forall> \<sigma> \<tau> . \<sigma>:X \<longrightarrow> \<tau>:X \<longrightarrow> is_meet_of \<omega> \<sigma> \<tau>) \<and> 
             (\<forall> \<nu> . (\<forall> \<sigma> \<tau> . \<sigma>:X \<longrightarrow> \<tau>:X \<longrightarrow>  is_meet_of \<nu> \<sigma> \<tau>) \<longrightarrow> subtypeOf \<omega> \<nu>)" 
 
consts is_join_of ::"TP \<Rightarrow> TP \<Rightarrow> TP \<Rightarrow> bool"
primrec
"is_join_of (stringTP W) \<sigma> \<tau> = (\<exists> S R . \<sigma> = stringTP S \<and> \<tau> = stringTP R \<and> W \<subseteq> S \<inter> R)" 
"is_join_of (objTP C W) \<sigma> \<tau> = (\<exists> S R . \<sigma> = objTP C S \<and> \<tau> = objTP C R \<and> W \<subseteq> S \<inter> R)" 

constdefs join:: "TP \<Rightarrow> TP \<Rightarrow> TP \<Rightarrow> bool"
"join \<sigma> \<tau> \<omega> \<equiv> is_join_of \<omega> \<sigma> \<tau> \<and> (\<forall> \<nu> . is_join_of \<nu> \<sigma> \<tau> \<longrightarrow> subtypeOf \<nu> \<omega>)"

constdefs wedge::"TP \<Rightarrow> TP \<Rightarrow> TP option"
"wedge \<sigma> \<tau> \<equiv> case \<sigma> of 
     stringTP S \<Rightarrow> (case \<tau> of stringTP R \<Rightarrow> Some (stringTP (S \<inter> R))
                            | objTP D R \<Rightarrow> None)
   | objTP C S \<Rightarrow> (case \<tau> of stringTP R \<Rightarrow> None
                            | objTP D R \<Rightarrow> if C=D then Some (objTP C (S \<inter> R)) else None)"

constdefs Join::"TP set \<Rightarrow> TP \<Rightarrow> bool"
"Join X \<omega> \<equiv> (\<forall> \<sigma> \<tau> . \<sigma>:X \<longrightarrow> \<tau>:X \<longrightarrow> is_join_of \<omega> \<sigma> \<tau>) \<and> 
             (\<forall> \<nu> . (\<forall> \<sigma> \<tau> . \<sigma>:X \<longrightarrow> \<tau>:X \<longrightarrow>  is_join_of \<nu> \<sigma> \<tau>) \<longrightarrow> subtypeOf \<nu> \<omega>)" 
 
lemma "dom (\<lambda> x . None) = {}"
by simp
lemma "dom ((\<lambda> x. None)(x:=Some a)) = {x}"
by simp 

types "MkStringCond_TP" = "string \<Rightarrow> Region \<Rightarrow> bool"
types "ConcatCond_TP" = "Region set \<Rightarrow> Region set \<Rightarrow> Region \<Rightarrow> bool"

types "StringCond" = "MkStringCond_TP \<times> ConcatCond_TP"


(* Region type system *)

inductive_set FjeuTyping::"(VarEnv \<times> StringCond \<times> Fjeu \<times> TP) set"
where
TpNull:"\<lbrakk> \<tau> = objTP C R \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC, FjNull,\<tau>):FjeuTyping"
|
TpVar:"\<lbrakk> \<Gamma> x = Some \<tau> \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC, FjVar x,\<tau>):FjeuTyping"
|
TpNew:"\<lbrakk> \<tau> = objTP C {r}; \<forall> f . f: fields C \<longrightarrow> (\<exists>\<sigma>. getview C r f = Some \<sigma>)\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC, FjNew C,\<tau>):FjeuTyping"
|
TpString:"\<lbrakk> \<tau> = stringTP {r}; (fst SC) S r\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC, FjString S,\<tau>):FjeuTyping"
|
TpLet:"\<lbrakk> (\<Gamma>,SC,e1,\<sigma>):FjeuTyping;
                 (\<Gamma>(x:=Some \<sigma>),SC,e2,\<tau>):FjeuTyping  \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjLet x e1 e2,\<tau>):FjeuTyping"
|
TpIf:"\<lbrakk> \<Gamma> x = Some (objTP C R);
                (\<Gamma>,SC,e1,\<tau>):FjeuTyping;
                (\<Gamma>,SC,e2,\<tau>):FjeuTyping \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjIfinst x E e1 e2,\<tau>):FjeuTyping"
|
TpCond:"\<lbrakk> \<Gamma> x = Some (objTP C R);  \<Gamma> y = Some (objTP D S);
                ((\<Gamma>(x:=Some (objTP C (R \<inter> S))))(y:=Some (objTP D (R \<inter> S))),
                   SC,e1,\<tau>):FjeuTyping;
                (\<Gamma>,SC,e2,\<tau>):FjeuTyping \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjCond x y e1 e2,\<tau>):FjeuTyping"
|
TpGet:
  "\<lbrakk> \<Gamma> x = Some (objTP C R); f:fields C;
     Meet {\<sigma> . \<exists> r . r:R \<and> getview C r f = Some \<sigma>} \<tau>;
     \<forall> r . r:R \<longrightarrow> (\<exists> \<sigma>. getview C r f = Some \<sigma>)\<rbrakk>
     \<Longrightarrow> (\<Gamma>,SC,FjGet x f,\<tau>):FjeuTyping"
|
TpGetQuant:
  "\<lbrakk> \<Gamma> x = Some (objTP C R); f:fields C;
     \<forall> r . r:R \<longrightarrow> (\<exists> \<sigma>. getview C r f = Some \<sigma> \<and> subtypeOf \<sigma> \<tau>)\<rbrakk>
     \<Longrightarrow> (\<Gamma>,SC,FjGetQ x f,\<tau>):FjeuTyping"
|
TpPut:
   "\<lbrakk> \<Gamma> x = Some (objTP C R); \<Gamma> y = Some \<tau>; 
      Join {\<sigma> . \<exists> r . r:R \<and> setview C r f = Some \<sigma>} \<tau>;
       f:fields C; \<forall> r . r:R \<longrightarrow> (\<exists> \<sigma>. setview C r f = Some \<sigma>)\<rbrakk>
      \<Longrightarrow> (\<Gamma>,SC,FjPut x f y,\<tau>):FjeuTyping"
|
TpPutQuant:
   "\<lbrakk> \<Gamma> x = Some (objTP C R); \<Gamma> y = Some \<tau>; 
       f:fields C; 
       \<forall> r . r:R \<longrightarrow> (\<exists> \<sigma>. setview C r f = Some \<sigma> \<and> subtypeOf \<tau> \<sigma>)\<rbrakk>
      \<Longrightarrow> (\<Gamma>,SC,FjPutQ x f y,\<tau>):FjeuTyping"
|
TpStringConcat:
   "\<lbrakk> \<Gamma> x = Some (stringTP Rx); \<Gamma> y = Some (stringTP Ry); 
              \<tau> = (stringTP (Rx \<union> {r}));
       (snd SC) Rx Ry r\<rbrakk>
     \<Longrightarrow> (\<Gamma>,SC,FjInvoke x StringConcat [y],\<tau>):FjeuTyping"
|
TpInv:
   "\<lbrakk> m ~= StringConcat; \<Gamma> x = Some (objTP C R); 
      argTypes \<Gamma> args \<tau>s; 
      \<forall> r . r:R --> (\<exists> \<alpha> . \<alpha> : MethViews C r m \<and> 
                                Meth_subtypeOf \<alpha> (\<tau>s,\<tau>)) \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjInvoke x m args,\<tau>):FjeuTyping"
|
TpSub:
  "\<lbrakk> (\<Theta>,SC,e,\<sigma>):FjeuTyping;
             subtypeOf \<sigma> \<tau>;VarEnvSubtyping \<Gamma> \<Theta>\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,e,\<tau>):FjeuTyping"

types HeapTyping = "Loc ~=> (Region \<times> (Class option))"

lemma "subtypeOf (objTP D {r}) (objTP C R) ==> r:R \<and> subclassOf D C"
apply (simp add: subtypeOf_def) done

inductive_set wfVal::"(HeapTyping \<times> Val \<times> TP) set"
where
(*wfVal_Null:"\<tau> = objTP C R \<Longrightarrow> (\<Sigma>,nullVal,\<tau>):wfVal"*)
wfVal_Null:"(\<Sigma>,nullVal,\<tau>):wfVal"
|
wfVal_String:"\<lbrakk>\<Sigma> a = Some(r,None); \<tau> = stringTP {r} \<rbrakk>
          \<Longrightarrow> (\<Sigma>,locVal a,\<tau>):wfVal"
|
wfVal_Loc:"\<lbrakk>\<Sigma> a = Some(r,Some C); \<tau> = objTP C {r} \<rbrakk>
          \<Longrightarrow> (\<Sigma>,locVal a,\<tau>):wfVal"
|
wfVal_sub:"\<lbrakk> (\<Sigma>,v,\<sigma>):wfVal; subtypeOf \<sigma> \<tau> \<rbrakk> \<Longrightarrow> (\<Sigma>,v,\<tau>):wfVal"

lemma wfValD:"(\<Sigma>,v,\<tau>):wfVal \<Longrightarrow>
                   v = nullVal \<or> (\<exists> a r. v = locVal a \<and> \<Sigma> a = Some(r,None) \<and> subtypeOf (stringTP {r}) \<tau>) \<or>
                   (\<exists> a r C. v = locVal a \<and> \<Sigma> a = Some(r,Some C) \<and> subtypeOf (objTP C {r}) \<tau>)"
apply (erule wfVal.induct)
apply clarsimp
apply clarsimp apply (rule subtypeOf_refl)
apply clarsimp apply (rule subtypeOf_refl)
apply clarsimp
  apply (erule disjE, clarsimp) apply (erule subtypeOf_trans, assumption)
  apply clarsimp apply (drule subtypeOf_trans, assumption) apply simp
done

constdefs store_wf::"HeapTyping \<Rightarrow> Store \<Rightarrow> VarEnv \<Rightarrow> bool"
"store_wf \<Sigma> s \<Gamma> \<equiv> \<forall> x \<tau> . \<Gamma> x = Some \<tau> \<longrightarrow> 
      (\<exists> v .  s x = Some v \<and> (\<Sigma>,v,\<tau>):wfVal)"

lemma storeD:"\<lbrakk> store_wf \<Sigma> s \<Gamma>; \<Gamma> x = Some \<tau>\<rbrakk> \<Longrightarrow>
              \<exists> v .  s x = Some v \<and> (\<Sigma>,v,\<tau>):wfVal"
apply (simp add: store_wf_def) done

types "PROP_TP" = "string \<Rightarrow> Region \<Rightarrow> bool"

consts obj_wt::"PROP_TP \<Rightarrow> HeapTyping \<Rightarrow> HeapObj \<Rightarrow> 
    (Region \<times> (Class option)) \<Rightarrow> bool"
primrec
"obj_wt P \<Sigma> (String w) X = (\<exists> r . X = (r,None) \<and> P w r)"
"obj_wt P \<Sigma> (Obj C F) X = 
    (\<exists> D r . X = (r,Some D) \<and> subclassOf C D \<and>
             (\<forall> f . f :fields C \<longrightarrow> 
                     (\<exists> v \<sigma> . F f = Some v \<and> getview C r f = Some \<sigma> \<and>
                              (\<Sigma>,v,\<sigma>):wfVal)))"

constdefs heap_wt::"Heap \<Rightarrow> PROP_TP \<Rightarrow> HeapTyping \<Rightarrow> bool"
"heap_wt h P \<Sigma> \<equiv> \<forall> l X . \<Sigma> l = Some X \<longrightarrow> 
              (\<exists> obj . h l = Some obj \<and> obj_wt P \<Sigma> obj X)"

lemma heapD: "\<lbrakk>heap_wt h P \<Sigma>; \<Sigma> l = Some X\<rbrakk> \<Longrightarrow>
               \<exists> obj . h l = Some obj \<and> obj_wt P \<Sigma> obj X"
apply (simp add:heap_wt_def) apply (case_tac X, clarsimp) done


(* Subtyping-rule-free version of the region type system, which is
later shown to be complete with respect to the region type system *)

inductive_set FjeuSD::"(VarEnv \<times> StringCond \<times> Fjeu \<times> TP) set"
where
SDNull:"\<lbrakk> subtypeOf (objTP C R) \<tau>\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjNull,\<tau>):FjeuSD"
|
SDVar:"\<lbrakk> \<Gamma> x = Some \<sigma>; subtypeOf \<sigma> \<tau> \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjVar x,\<tau>):FjeuSD"
|
SDNew:"\<lbrakk> subtypeOf (objTP C {r}) \<tau>; 
         \<forall> f . f: fields C \<longrightarrow> (\<exists>\<sigma>. getview C r f = Some \<sigma>)\<rbrakk>
        \<Longrightarrow> (\<Gamma>,SC,FjNew C,\<tau>):FjeuSD"
|
SDString:"\<lbrakk> subtypeOf (stringTP {r}) \<tau>; (fst SC) S r\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjString S,\<tau>):FjeuSD"
|
SDLet:"\<lbrakk> (\<Delta>,SC,e1,\<sigma>):FjeuTyping;
         (\<Delta>(x:=Some \<sigma>),SC,e2,\<omega>):FjeuTyping;
          VarEnvSubtyping \<Gamma> \<Delta>; subtypeOf \<omega> \<tau> \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjLet x e1 e2,\<tau>):FjeuSD"
|
SDIf:"\<lbrakk> \<Delta> x = Some (objTP C R);
        (\<Delta>,SC,e1,\<omega>):FjeuTyping; (\<Delta>,SC,e2,\<omega>):FjeuTyping;
         VarEnvSubtyping \<Gamma> \<Delta>; subtypeOf \<omega> \<tau>\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjIfinst x E e1 e2,\<tau>):FjeuSD"
|
SDCond:"\<lbrakk> \<Delta> x = Some (objTP C R); \<Delta> y = Some (objTP D S);
        ((\<Delta>(x:=Some(objTP C (R \<inter> S))))(y:=Some(objTP D (R \<inter> S))),
          SC,e1,\<omega>):FjeuTyping; 
        (\<Delta>,SC,e2,\<omega>):FjeuTyping;
         VarEnvSubtyping \<Gamma> \<Delta>; subtypeOf \<omega> \<tau>\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjCond x y e1 e2,\<tau>):FjeuSD"
|
SDGet:
  "\<lbrakk> \<Delta> x = Some (objTP C R); f: fields C;
     \<forall> r . r:R \<longrightarrow> (\<exists> \<sigma>. getview C r f = Some \<sigma>);
     Meet {\<sigma> . \<exists> r . r:R \<and> getview C r f = Some \<sigma>} \<omega>;
         VarEnvSubtyping \<Gamma> \<Delta>; subtypeOf \<omega> \<tau>\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjGet x f,\<tau>):FjeuSD"
|
SDGetQuant:
  "\<lbrakk> \<Delta> x = Some (objTP C R); f:fields C;
     \<forall> r . r:R \<longrightarrow> (\<exists> \<sigma>. getview C r f = Some \<sigma> \<and> subtypeOf \<sigma> \<tau>);
         VarEnvSubtyping \<Gamma> \<Delta>\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjGetQ x f,\<tau>):FjeuSD"
|
SDPut:
   "\<lbrakk> \<Delta> x = Some (objTP C R); \<Delta> y = Some \<tau>; f:fields C;
       \<forall> r . r:R \<longrightarrow> (\<exists> \<sigma>. setview C r f = Some \<sigma>);
      Join {\<sigma> . \<exists> r . r:R \<and> setview C r f = Some \<sigma>} \<tau>;
      subtypeOf \<tau> \<omega>; VarEnvSubtyping \<Gamma> \<Delta> \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjPut x f y,\<omega>):FjeuSD"
|
SDPutQuant:
   "\<lbrakk> \<Delta> x = Some (objTP C R); \<Delta> y = Some \<tau>; f:fields C; 
      \<forall> r . r:R \<longrightarrow> (\<exists> \<sigma>. setview C r f = Some \<sigma> \<and> subtypeOf \<tau> \<sigma>);
      subtypeOf \<tau> \<omega>; VarEnvSubtyping \<Gamma> \<Delta> \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjPutQ x f y,\<omega>):FjeuSD"
|
SDConcat:
   "\<lbrakk> \<Delta> x = Some (stringTP Rx); \<Delta> y = Some (stringTP Ry); 
      subtypeOf (stringTP (Rx \<union> {r})) \<tau>; VarEnvSubtyping \<Gamma> \<Delta>;
      (snd SC) Rx Ry r\<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC, FjInvoke x StringConcat [y],\<tau>):FjeuSD"
|
SDInv:
   "\<lbrakk> m ~= StringConcat; \<Delta> x = Some (objTP C R); 
      argTypes \<Delta> args \<tau>s; VarEnvSubtyping \<Gamma> \<Delta>; 
      \<forall> r . r:R --> (\<exists> \<alpha> . \<alpha> : MethViews C r m \<and> 
                                Meth_subtypeOf \<alpha> (\<tau>s,\<tau>)) \<rbrakk>
             \<Longrightarrow> (\<Gamma>,SC,FjInvoke x m args,\<tau>):FjeuSD"

inductive_cases TpSD_Null[elim!]:"(\<Gamma>,SC,FjNull,\<tau>):FjeuSD"
inductive_cases TpSD_Var[elim!]:"(\<Gamma>,SC,FjVar x,\<tau>):FjeuSD"
inductive_cases TpSD_New[elim!]:"(\<Gamma>,SC,FjNew C,\<tau>):FjeuSD"
inductive_cases TpSD_String[elim!]:"(\<Gamma>,SC,FjString S,\<tau>):FjeuSD"
inductive_cases TpSD_If[elim!]:"(\<Gamma>,SC,FjIfinst x C e1 e2,\<tau>):FjeuSD"
inductive_cases TpSD_Cond[elim!]:"(\<Gamma>,SC,FjCond x y e1 e2,\<tau>):FjeuSD"
inductive_cases TpSD_Let[elim!]:"(\<Gamma>,SC,FjLet x e1 e2,\<tau>):FjeuSD"
inductive_cases TpSD_Get[elim!]:"(\<Gamma>,SC,FjGet x f,\<tau>):FjeuSD"
inductive_cases TpSD_GetQ[elim!]:"(\<Gamma>,SC,FjGetQ x f,\<tau>):FjeuSD"
inductive_cases TpSD_Put[elim!]:"(\<Gamma>,SC,FjPut x f y,\<tau>):FjeuSD"
inductive_cases TpSD_PutQ[elim!]:"(\<Gamma>,SC,FjPutQ x f y,\<tau>):FjeuSD"
(*inductive_cases TpSD_StringConcat[elim!]:"(\<Gamma>,FjInvoke x StringConcat [y],\<tau>):FjeuTypingSD"
inductive_cases TpSD_Inv[elim!]:"(\<Gamma>,FjInvoke x m args,\<tau>):FjeuTypingSD"
*)

lemma Meet_subset: "\<lbrakk>Meet X \<tau>; Meet Y \<sigma>; Y \<subseteq> X; Y\<noteq>{}\<rbrakk> \<Longrightarrow> subtypeOf \<sigma> \<tau>"
apply (simp add: Meet_def) apply clarsimp
apply (subgoal_tac "\<exists> y. y:Y", erule exE)
  apply (rotate_tac -2, erule_tac x=\<tau> in allE, erule mp) apply clarsimp
  apply (erule_tac x=\<sigma>' in allE, erule impE) apply fast
  apply (erule_tac x=\<tau>' in allE, erule mp) apply fast
apply fast
done

lemma VarEnvSubtyping_refl:"VarEnvSubtyping \<Gamma> \<Gamma>"
apply (simp add: VarEnvSubtyping_def subtypeOf_refl)
done

lemma VarEnvSubtyping_trans:"[|VarEnvSubtyping \<Delta> \<Gamma>;VarEnvSubtyping \<Gamma> \<Pi> |]
       ==> VarEnvSubtyping \<Delta> \<Pi>"
apply (simp add: VarEnvSubtyping_def, clarsimp)
apply (erule_tac x=x in allE, clarsimp)
apply (erule_tac x=x in allE, clarsimp)
apply (erule subtypeOf_trans, assumption)
done

lemma VarEnvSubtypingD:
  "[| VarEnvSubtyping \<Delta> \<Gamma>; \<Gamma> x = Some \<sigma> |] 
  ==> \<exists> \<tau> . \<Delta> x = Some \<tau> \<and> subtypeOf \<tau> \<sigma>"
apply (simp only: VarEnvSubtyping_def) 
done

lemma argTypes_VarEnvSub[rule_format]:
"\<forall> \<tau>s . (argTypes \<Gamma> vars \<tau>s -->
          VarEnvSubtyping \<Delta> \<Gamma> -->
       (\<exists> \<sigma>s .  length \<tau>s = length \<sigma>s \<and>
           argTypes \<Delta> vars \<sigma>s \<and>
           (\<forall> n . n < length \<sigma>s --> subtypeOf (\<sigma>s!n) (\<tau>s!n))))"
apply (induct vars)
apply (simp add: argTypes_def, clarsimp)
apply (rename_tac x vars \<tau>s)
apply (simp add: argTypes_def, clarsimp)
  apply (case_tac \<tau>s, clarsimp,clarsimp)
  apply (rename_tac x vars \<tau> \<tau>s)
  apply (drule_tac x=x and \<sigma>=\<tau> in VarEnvSubtypingD) apply (erule_tac x=0 in allE, clarsimp)
  apply clarsimp 
  apply (rename_tac \<sigma>)
  apply (erule_tac x=\<tau>s in allE, clarsimp)
  apply (erule impE) apply clarsimp apply (erule_tac x="Suc n" in allE, clarsimp)
  apply clarsimp
  apply (rule_tac x="\<sigma>#\<sigma>s" in exI, clarsimp)
  apply (rule, clarsimp) apply (case_tac n, clarsimp) apply clarsimp
  apply (clarsimp) apply (case_tac n, clarsimp) apply clarsimp
done

lemma FjeuSD_subtyping[rule_format]:
  "\<forall> \<Delta> \<sigma> \<Gamma> \<tau> .
       (\<Delta>,SC,e,\<sigma>):FjeuSD -->
       VarEnvSubtyping  \<Gamma> \<Delta> --> subtypeOf \<sigma> \<tau> -->
       (\<Gamma>,SC,e,\<tau>):FjeuSD"
apply (induct e)
apply clarsimp  apply (rule_tac C=C in SDNull) apply (erule subtypeOf_trans, assumption)
apply clarsimp apply (drule VarEnvSubtypingD, assumption) apply clarsimp 
  apply (erule SDVar) apply (erule subtypeOf_trans, erule subtypeOf_trans, assumption)
apply clarsimp  apply (rule SDNew) apply (erule subtypeOf_trans, assumption) apply assumption
apply clarsimp  apply (rule SDString) apply (erule subtypeOf_trans, assumption)
                apply assumption
apply clarsimp  apply (rule SDLet) apply assumption apply assumption
   apply (erule VarEnvSubtyping_trans, assumption) apply (erule subtypeOf_trans, assumption)
apply clarsimp  apply (erule SDCond) apply assumption apply assumption apply assumption 
   apply (erule VarEnvSubtyping_trans, assumption) apply (erule subtypeOf_trans, assumption) 
apply clarsimp  apply (erule SDIf) apply assumption apply assumption 
   apply (erule VarEnvSubtyping_trans, assumption) apply (erule subtypeOf_trans, assumption) 
apply clarsimp apply (rename_tac x f \<Delta> \<sigma> \<Delta>' C R \<omega> \<Gamma> \<tau>)
  apply (frule VarEnvSubtypingD, assumption) apply clarsimp 
  apply (case_tac \<tau>', clarsimp) apply (simp add: subtypeOf_def) apply clarsimp
  apply (rename_tac D S)
  apply (rule_tac \<Delta>=\<Delta>' in SDGet) apply assumption apply assumption apply assumption apply assumption?
    apply (erule VarEnvSubtyping_trans) apply assumption apply (erule subtypeOf_trans, assumption)
apply clarsimp apply (rename_tac x f \<Delta> \<sigma> \<Delta>' C R \<Gamma> \<tau>)
  apply (frule VarEnvSubtypingD, assumption) apply clarsimp 
  apply (case_tac \<tau>', clarsimp) apply (simp add: subtypeOf_def) apply clarsimp
  apply (rename_tac D S)
  apply (rule_tac \<Delta>=\<Delta>' in SDGetQuant) apply assumption apply assumption? 
    apply clarsimp apply (erule_tac x=r in allE, clarsimp) apply (erule subtypeOf_trans,assumption) 
    apply (erule VarEnvSubtyping_trans) apply assumption 
apply clarsimp apply (rename_tac x f y  \<Delta> \<sigma> \<Delta>' C R \<tau> \<Gamma> \<tau>')
  apply (frule_tac x=x in VarEnvSubtypingD, assumption) apply clarsimp 
  apply (case_tac \<tau>'', clarsimp) apply (simp add: subtypeOf_def) apply clarsimp
  apply (rename_tac D S)
  apply (frule_tac x=y in VarEnvSubtypingD, assumption) apply clarsimp 
  apply (rule_tac \<Delta>=\<Delta>' in SDPut) apply assumption apply assumption apply assumption apply assumption apply assumption?
    apply (erule subtypeOf_trans, assumption)
    apply (erule VarEnvSubtyping_trans) apply assumption
apply clarsimp apply (rename_tac x f y \<Delta> \<sigma> \<Delta>' C R \<tau> \<Gamma> \<tau>')
  apply (frule_tac x=x in VarEnvSubtypingD, assumption) apply clarsimp 
  apply (case_tac \<tau>'', clarsimp) apply (simp add: subtypeOf_def) apply clarsimp
  apply (rename_tac D S)
  apply (frule_tac x=y in VarEnvSubtypingD, assumption) apply clarsimp 
  apply (rule_tac \<Delta>=\<Delta>' in SDPutQuant) apply assumption apply assumption apply assumption 
    apply clarsimp apply (erule subtypeOf_trans,assumption) 
    apply (erule VarEnvSubtyping_trans) apply assumption
apply clarsimp  
apply (erule FjeuSD.cases) apply (simp_all) apply clarsimp
  apply (frule_tac x=x in VarEnvSubtypingD, assumption) apply clarsimp
  apply (case_tac \<tau>'') prefer 2 apply (simp add: subtypeOf_def)
  apply clarsimp
  apply (frule_tac x=y in VarEnvSubtypingD, assumption) apply clarsimp
  apply (case_tac \<tau>'') prefer 2 apply (simp add: subtypeOf_def)
  apply clarsimp
  apply (rule_tac r=r and \<Delta>=\<Delta>' in SDConcat) apply assumption apply assumption   
  apply clarsimp apply (erule subtypeOf_trans,assumption)
  apply (erule VarEnvSubtyping_trans) apply assumption
  apply simp
apply (frule_tac x=x in VarEnvSubtypingD, assumption) apply clarsimp
  apply (frule argTypes_VarEnvSub) apply assumption apply clarsimp
  apply (rename_tac \<Gamma> \<tau> m \<Delta>' x C R args \<tau>s \<Delta> \<sigma> cond1 cond2 \<tau>' \<sigma>s)
  apply (case_tac \<tau>', clarsimp) apply (simp add: subtypeOf_def)
  apply clarsimp apply (rename_tac D S)
  apply (erule_tac \<Delta>=\<Delta>' in SDInv) apply assumption apply assumption
    apply (erule VarEnvSubtyping_trans, assumption)
    apply clarsimp apply (erule_tac x=r in allE, clarsimp)
    apply (rule_tac x=a in exI, rule_tac x=b in exI,simp add: Meth_subtypeOf_def) apply clarsimp
    apply (erule subtypeOf_trans, assumption)
done

lemma FjeuSD_complete:"(\<Delta>,SC,e,\<tau>):FjeuTyping ==> (\<Delta>,SC,e,\<tau>):FjeuSD"
apply (erule FjeuTyping.induct)
apply clarsimp apply (rule_tac C=C in SDNull) 
  apply (rule subtypeOf_refl) 
apply (erule SDVar) apply (rule subtypeOf_refl)
apply (rule SDNew) apply clarsimp apply (rule subtypeOf_refl) apply assumption 
apply (rule SDString) apply clarsimp apply (rule subtypeOf_refl) apply assumption
apply (rule SDLet) apply assumption apply assumption apply (rule VarEnvSubtyping_refl) apply (rule subtypeOf_refl)
apply (erule SDIf) apply assumption apply assumption apply (rule VarEnvSubtyping_refl) apply (rule subtypeOf_refl)
apply (erule SDCond) apply assumption apply assumption apply assumption
  apply (rule VarEnvSubtyping_refl) apply (rule subtypeOf_refl)
apply (erule SDGet)
  apply assumption  apply assumption apply assumption+
  apply (rule VarEnvSubtyping_refl)
  apply (rule subtypeOf_refl)
apply (erule SDGetQuant)
  apply assumption  apply assumption? 
  apply (rule VarEnvSubtyping_refl)
apply clarsimp apply (erule SDPut) apply assumption apply assumption apply assumption apply assumption?
  apply (rule subtypeOf_refl) 
  apply (rule VarEnvSubtyping_refl) 
apply clarsimp apply (erule SDPutQuant) apply assumption apply assumption apply assumption 
  apply (rule subtypeOf_refl) 
  apply (rule VarEnvSubtyping_refl) 
apply (erule_tac r=r in SDConcat) apply assumption apply clarsimp apply (rule subtypeOf_refl)
  apply (rule VarEnvSubtyping_refl) 
  apply assumption
apply (erule SDInv) apply assumption apply assumption 
  apply (rule VarEnvSubtyping_refl)
  apply assumption
apply (erule FjeuSD_subtyping) apply assumption apply assumption
done

constdefs HT_extends::"HeapTyping => HeapTyping => bool"
"HT_extends \<Pi> \<Sigma> \<equiv> \<forall> a r \<tau> . \<Sigma> a = Some (r,\<tau>) -->
  \<Pi> a = Some (r,\<tau>)"

lemma HT_extends_refl:"HT_extends \<Sigma> \<Sigma>"
apply (simp add: HT_extends_def subtypeOf_refl)
done

lemma HT_extends_trans:
  "[|HT_extends \<Pi> \<Sigma>; HT_extends \<Omega> \<Pi>|] ==> HT_extends \<Omega> \<Sigma>"
apply (simp add: HT_extends_def subtypeOf_trans)
done

lemma HT_extendsD:"[| HT_extends \<Pi> \<Sigma>;\<Sigma> a = Some X|] ==>  \<Pi> a = Some X"
apply (simp add: HT_extends_def) apply (case_tac X, clarsimp) 
done

lemma HT_extendsE:"[| HT_extends \<Pi> \<Sigma>;\<Pi> a = None|] ==>  \<Sigma> a = None"
apply (simp add: HT_extends_def) 
apply (case_tac "\<Sigma> a", assumption, clarsimp) apply (erule_tac x=a in allE, clarsimp) apply fast 
done

lemma wfVal_HTextends[rule_format]:
  "(\<Sigma>,v,\<tau>):wfVal ==> \<forall> \<Pi> . HT_extends \<Pi> \<Sigma> --> (\<Pi>,v,\<tau>):wfVal"
apply (erule wfVal.induct)
apply clarsimp apply (rule wfVal_Null) (*apply fastsimp*)
apply clarsimp apply (drule HT_extendsD, assumption)
  apply (erule wfVal_String) apply simp
apply clarsimp apply (drule HT_extendsD, assumption)
  apply (erule wfVal_Loc) apply simp
apply clarsimp apply (erule_tac x=\<Pi> in allE, clarsimp)
  apply (erule wfVal_sub) apply assumption
done

lemma objwt_HTextends[rule_format]:
  "obj_wt P \<Sigma> obj X ==> \<forall> \<Pi> . HT_extends \<Pi> \<Sigma> \<longrightarrow> obj_wt P \<Pi> obj X"
apply (case_tac obj,clarsimp) 
  apply (rename_tac C F D r \<Pi> f)
  apply (erule_tac x=f in allE, clarsimp)
  apply (erule wfVal_HTextends, assumption)
apply clarsimp
done

inductive_set mkEnv::"(Var list \<times> TP list \<times> VarEnv) set"
where
mkEnvNull:"\<lbrakk>t = (\<lambda> x . None) \<rbrakk>
             \<Longrightarrow> ([],[],t):mkEnv"
|
mkEnvCons:"\<lbrakk>(vars,\<sigma>s,r):mkEnv; 
                      t = r(x:=Some \<sigma>) \<rbrakk>
             \<Longrightarrow> (x#vars,\<sigma>#\<sigma>s,t):mkEnv"

lemma mkEnv_existsAux[rule_format]:
  "\<forall> vars \<tau>s . length vars = N --> length \<tau>s = N -->  
     (\<exists> t . (vars,\<tau>s,t):mkEnv)"
apply (induct N)
apply clarsimp apply (rule, rule mkEnvNull) apply simp
apply clarsimp
  apply (case_tac \<tau>s, clarsimp, clarsimp) apply (rename_tac \<tau> \<tau>s)
  apply (case_tac vars, clarsimp, clarsimp) apply (rename_tac x vars)
  apply (erule_tac x=vars in allE, clarsimp)
  apply (erule_tac x=\<tau>s in allE, clarsimp)
  apply (rule, erule mkEnvCons) apply simp
done

lemma mkEnv_exists:
  "length vars = length \<tau>s
   ==> \<exists> t . (vars,\<tau>s,t):mkEnv"
apply (rule mkEnv_existsAux) apply simp apply simp 
done

lemma mkEnv_length:"(vars,\<tau>s, t) : mkEnv ==> length vars = length \<tau>s"
apply (erule mkEnv.induct)
apply simp
apply simp
done

lemma mkEnv_dom[rule_format]:
  "(vars, \<sigma>s, \<Gamma>) : mkEnv ==> \<forall> x \<tau> . \<Gamma> x = Some \<tau> --> x:set vars"
apply (erule mkEnv.induct) apply clarsimp
apply clarsimp
done

lemma Meth_subtypeOf_wfEnv[rule_format]:
  "\<forall> \<tau>s vars \<Gamma>  \<Delta>.
      Meth_subtypeOf (\<sigma>s, \<sigma>) (\<tau>s, \<tau>) --> distinct vars -->
      (vars, \<tau>s, \<Gamma>) : mkEnv --> (vars, \<sigma>s, \<Delta>) : mkEnv -->
      store_wf \<Sigma> s \<Gamma> --> store_wf \<Sigma> s \<Delta>"
apply (induct \<sigma>s)
apply (simp add: Meth_subtypeOf_def, clarsimp)
  apply (erule mkEnv.cases, clarsimp) prefer 2 apply clarsimp
  apply (erule mkEnv.cases, clarsimp) apply clarsimp
apply (simp add: Meth_subtypeOf_def, clarsimp)
  apply (erule mkEnv.cases, clarsimp, clarsimp)
  apply (erule mkEnv.cases, clarsimp, clarsimp)
  apply (rename_tac \<omega>s \<Gamma> \<omega> vars \<psi>s \<Delta> x \<psi>)
  apply (erule_tac x=\<omega>s in allE, clarsimp)
  apply (erule impE) apply clarsimp apply (erule_tac x="Suc n" in allE, clarsimp) 
  apply (erule_tac x=vars in allE, erule impE, assumption)
  apply (case_tac "\<Gamma> x") prefer 2 apply (drule mkEnv_dom, assumption) apply simp
  apply (erule_tac x=\<Gamma> in allE, erule impE) apply assumption
  apply (erule_tac x=\<Delta> in allE, erule impE) apply assumption

  apply (erule impE) apply (simp add: store_wf_def) apply clarsimp
    apply (case_tac "x=xa", clarsimp) apply (erule_tac x=xa in allE, clarsimp)
  apply (simp add: store_wf_def) 
    apply (erule_tac x=x in allE, clarsimp)  
    apply (erule wfVal_sub) apply (erule_tac x=0 in allE, clarsimp)
done    

lemma mkStore_mkEnv[rule_format]:
  "(\<Gamma>, pars, args, \<Delta>) : mkStore ==>
       \<forall> \<tau>s . argTypes \<Gamma> args \<tau>s -->
       (pars, \<tau>s, \<Delta>) : mkEnv"
apply (erule mkStore.induct)
apply clarsimp apply (simp add: argTypes_def) apply (rule mkEnvNull) apply simp
apply clarsimp apply (simp add: argTypes_def) apply (case_tac \<tau>s, clarsimp) apply clarsimp
  apply (rename_tac s pars args r y v x \<tau> \<tau>s)
  apply (erule_tac x=\<tau>s in allE, erule impE, clarsimp) 
    apply (erule_tac x="Suc n" in allE, clarsimp)
  apply (erule mkEnvCons) 
    apply (erule_tac x=0 in allE)
    apply rule apply simp
done

lemma  mkStore_VarEnvSubtyping[rule_format]:
 "(\<Gamma>, pars, args, \<Delta>) : mkStore ==> 
       \<forall> \<Gamma>' \<Delta>' . 
           (\<Gamma>', pars, args, \<Delta>') : mkStore -->
          VarEnvSubtyping \<Gamma> \<Gamma>' --> VarEnvSubtyping \<Delta> \<Delta>'" 
apply (erule mkStore.induct)
apply clarsimp apply (erule mkStore.cases, clarsimp) apply (simp add: VarEnvSubtyping_def) apply clarsimp
apply clarsimp apply (erule mkStore.cases, clarsimp, clarsimp) 
  apply (erule_tac x=sa in allE, erule_tac x=ra in allE, clarsimp) 
  apply (simp add: VarEnvSubtyping_def) apply (erule_tac x=ya in allE, clarsimp)
done

lemma mkStore_mkEnv_sub[rule_format]:
  "(\<Gamma>', pars, args, \<Delta>') : mkStore ==>
    \<forall> \<sigma>s \<Phi> \<tau>s . 
        (pars, \<sigma>s, \<Phi>) : mkEnv --> argTypes \<Gamma>' args \<tau>s -->
          Meth_subtypeOf (\<sigma>s, \<sigma>) (\<tau>s, \<tau>) -->
          VarEnvSubtyping \<Delta>' \<Phi>"
apply (erule mkStore.induct)
apply clarsimp
  apply (erule mkEnv.cases, clarsimp) prefer 2 apply clarsimp
  apply (simp add: VarEnvSubtyping_def)
apply clarsimp
  apply (erule mkEnv.cases, clarsimp, clarsimp)
  apply (rename_tac s args r y v \<tau>s vars \<sigma>s \<Gamma> x \<omega>)
  apply (erule_tac x=\<sigma>s in allE, erule_tac x=\<Gamma> in allE, clarsimp)
  apply (simp add: argTypes_def) apply (case_tac \<tau>s, clarsimp, clarsimp)
  apply (erule_tac x=list in allE, clarsimp)
  apply (erule impE) apply clarsimp apply (erule_tac x="Suc n" in allE, clarsimp)
  apply (erule impE) apply (simp add: Meth_subtypeOf_def, clarsimp)
                     apply (rotate_tac -3, erule_tac x="Suc n" in allE, clarsimp)
  apply (simp add: VarEnvSubtyping_def Meth_subtypeOf_def, clarsimp)
                     apply (erule_tac x=0 in allE, clarsimp)
                     apply (erule_tac x=0 in allE, clarsimp)
done

constdefs Methods_welltyped::"StringCond \<Rightarrow> bool"
"Methods_welltyped SC \<equiv>
  (\<forall> C r m \<tau>s \<tau> pars e. 
    (\<tau>s,\<tau>) : MethViews C r m --> 
    mbody C m = Some (pars,e) --> 
    (length pars = length \<tau>s \<and> distinct pars \<and>
       (\<forall> \<Gamma> . (pars,\<tau>s, \<Gamma>) : mkEnv --> (\<Gamma>, SC, e, \<tau>):FjeuTyping)))"

constdefs StringCond_implies_Policy::"StringCond \<Rightarrow> PROP_TP \<Rightarrow> bool"
"StringCond_implies_Policy SC P \<equiv>
     (\<forall> w r . (fst SC) w r \<longrightarrow> P w r) \<and>
     (\<forall> R S t r s w1 w2. 
        (snd SC) R S t \<longrightarrow> r:R \<longrightarrow> s:S \<longrightarrow> 
        P w1 r \<longrightarrow> P w2 s \<longrightarrow> P (w1 @ w2) t)"

constdefs inter::"StringCond \<Rightarrow> PROP_TP \<Rightarrow> Store \<Rightarrow> 
                  Heap \<Rightarrow> Fjeu \<Rightarrow> Val \<Rightarrow> Heap \<Rightarrow> bool"
"inter SC P s h e v k \<equiv> StringCond_implies_Policy SC P \<longrightarrow>
    (\<forall> \<Gamma> \<tau> \<Sigma> . (\<Gamma>,SC,e,\<tau>):FjeuTyping \<longrightarrow> store_wf \<Sigma> s \<Gamma> \<longrightarrow> 
               heap_wt h P \<Sigma> \<longrightarrow> Methods_welltyped SC \<longrightarrow>
               (\<exists> \<Pi> . HT_extends \<Pi> \<Sigma> \<and> heap_wt k P \<Pi> \<and> (\<Pi>,v,\<tau>): wfVal))"
(*
axioms field_getr:"f \<in> fields C \<Longrightarrow> \<exists> \<sigma>. getview C r f = Some \<sigma>" 
axioms field_putr:"f \<in> fields C \<Longrightarrow> \<exists> \<sigma>. setview C r f = Some \<sigma>" 
*)
lemma storewf_sub:
  "[|VarEnvSubtyping \<Gamma> \<Delta>; store_wf \<Sigma> s \<Gamma> |] ==> store_wf \<Sigma> s \<Delta>"
apply (simp add: store_wf_def VarEnvSubtyping_def, clarsimp)
apply (erule_tac x=x in allE, clarsimp)
apply (erule_tac x=x in allE, clarsimp)
apply (erule wfVal_sub) apply assumption
done

lemma ismeet_subtypeOf1: "is_meet_of \<tau> \<sigma> \<omega> \<Longrightarrow> subtypeOf \<sigma> \<tau>"
apply (simp add: subtypeOf_def)
apply (case_tac \<tau>, clarsimp) apply clarsimp
done

lemma ismeet_subtypeOf2: "is_meet_of \<tau> \<sigma> \<omega> \<Longrightarrow> subtypeOf \<omega> \<tau>"
apply (simp add: subtypeOf_def)
apply (case_tac \<tau>, clarsimp) apply clarsimp
done

lemma isjoin_subtypeOf1: "is_join_of \<tau> \<sigma> \<omega> \<Longrightarrow> subtypeOf \<tau> \<sigma>"
apply (simp add: subtypeOf_def)
apply (case_tac \<tau>, clarsimp) apply clarsimp apply (rule subclassOf_refl)
done

lemma isjoin_subtypeOf2: "is_join_of \<tau> \<sigma> \<omega> \<Longrightarrow> subtypeOf \<tau> \<omega>"
apply (simp add: subtypeOf_def)
apply (case_tac \<tau>, clarsimp) apply clarsimp apply (rule subclassOf_refl)
done

lemma Meet_D: "\<lbrakk> Meet {\<sigma>. \<exists>r. r \<in> R \<and> getview D r f = Some \<sigma>} \<tau>; getview D r f = Some \<sigma>; r:R\<rbrakk>
       \<Longrightarrow> subtypeOf \<sigma> \<tau>"
apply (simp add: Meet_def) apply clarsimp
apply (erule_tac x=\<sigma> in allE, erule impE) apply (rule_tac x=r in exI, simp)
apply (rotate_tac -1, erule_tac x=\<sigma> in allE, erule impE) apply (rule_tac x=r in exI, simp)
apply (erule ismeet_subtypeOf1)
done

lemma Join_D: "\<lbrakk> Join {\<sigma>. \<exists>r. r \<in> R \<and> setview D r f = Some \<sigma>} \<tau>; setview D r f = Some \<sigma>; r:R \<rbrakk>
       \<Longrightarrow> subtypeOf \<tau> \<sigma>"
apply (simp add: Join_def) apply clarsimp
apply (erule_tac x=\<sigma> in allE, erule impE) apply (rule_tac x=r in exI, simp)
apply (rotate_tac -1, erule_tac x=\<sigma> in allE, erule impE) apply (rule_tac x=r in exI, simp)
apply (erule isjoin_subtypeOf1)
done

axioms condition1:"[|getview D r f = Some \<sigma>; subclassOf C D|]
       ==> EX \<tau>. getview C r f = Some \<tau> & subtypeOf \<tau> \<sigma>"
axioms condition2:"[|setview D r f = Some \<sigma>; subclassOf C D |]
       ==> EX \<tau>. setview C r f = Some \<tau> \<and>  subtypeOf \<sigma> \<tau>"
axioms condition3:"[| subtypeOf (objTP C R) (objTP D S); r:R; Dspec : MethViews D r m |] ==>
     \<exists> Cspec . Cspec : MethViews C r m \<and> Meth_subtypeOf Cspec Dspec"
axioms condition4:"[|setview D r f = Some \<sigma>; getview D r f = Some \<tau>|]
       ==> subtypeOf \<sigma> \<tau>"

axioms fields_sub:"subclassOf C D \<Longrightarrow> fields D \<subseteq> fields C"

lemma wfVal_Cond:
 "\<lbrakk>(\<Sigma>, v, objTP D S) : wfVal; (\<Sigma>, v, objTP C R) \<in> wfVal\<rbrakk> 
  \<Longrightarrow> (\<Sigma>, v, objTP C (R \<inter> S)) \<in> wfVal"
apply (drule wfValD)
apply (drule wfValD)
apply safe
apply (rule wfVal_Null)
apply clarsimp apply (simp add: subtypeOf_def)
apply clarsimp 
apply clarsimp 
apply clarsimp
  apply (rule wfVal_sub) apply (erule wfVal_Loc) apply simp 
  apply (simp add: subtypeOf_def) 
done

lemma mkStore_wfEnv[rule_format]:
"(s, pars, args, t) : mkStore ==> 
  \<forall> \<Delta> . store_wf \<Sigma> s \<Gamma> --> 
           (\<Gamma>, pars, args, \<Delta>) : mkStore --> 
           store_wf \<Sigma> t \<Delta>"
apply (erule mkStore.induct)
apply clarsimp
  apply (erule mkStore.cases, clarsimp) apply (simp add: store_wf_def)
  apply clarsimp
apply clarsimp
  apply (rotate_tac 1, erule mkStore.cases, clarsimp) 
  apply clarsimp apply (erule_tac x=ra in allE, erule impE, assumption)
  apply (simp add: store_wf_def) apply (erule_tac x=ya in allE, clarsimp)
done

lemma SoundAux:"(s,h,e,v,k):FjeuOpsem \<Longrightarrow> inter SC P s h e v k" 
apply (erule FjeuOpsem.induct) apply (simp_all add: inter_def)
(*Null*)
apply clarsimp
  apply (drule FjeuSD_complete) apply clarsimp
  apply (rule_tac x=\<Sigma> in exI, simp)
  apply rule apply (rule HT_extends_refl)
  apply (simp add: subtypeOf_def) apply (case_tac \<tau>, clarsimp, clarsimp)
  apply (rule wfVal_Null) (*apply fastsimp*)
(*Var*)
apply clarsimp
  apply (drule FjeuSD_complete) apply clarsimp
  apply (rule_tac x=\<Sigma> in exI, simp)
  apply rule apply (rule HT_extends_refl)
  apply (drule_tac x=x in storeD, assumption) apply clarsimp
  apply (erule wfVal_sub) apply assumption
(*New*)
apply clarsimp 
  apply (drule FjeuSD_complete) apply clarsimp
  apply (rule_tac x="\<Sigma>(a:=Some(r,Some C))" in exI)
  apply (subgoal_tac "HT_extends (\<Sigma>(a \<mapsto> (r, Some C))) \<Sigma>", simp)
  prefer 2 apply (simp add: HT_extends_def, clarsimp)
    apply (drule heapD, assumption)  apply clarsimp
  apply (subgoal_tac "(\<Sigma>(a:=Some (r, Some C)), locVal a, objTP C {r}) \<in> wfVal")
  prefer 2 apply (rule wfVal_Loc) apply fastsimp apply simp
  apply (simp (no_asm) only: heap_wt_def) 
    apply (rule, clarsimp)
      apply (rule, clarsimp) apply (simp add: defaultObj_def)
        apply (rule,rule subclassOf_refl) apply clarsimp 
            apply (erule_tac x=f in allE,clarsimp) (*apply (drule_tac r=r in field_getr) apply clarsimp*)
        apply (rule wfVal_Null) 
      apply clarsimp apply (drule heapD,assumption) apply clarsimp
        apply (erule objwt_HTextends) apply assumption
    apply (erule wfVal_sub) apply assumption
(*mkString*)
apply clarsimp 
  apply (drule FjeuSD_complete) apply clarsimp
  apply (rule_tac x="\<Sigma>(a:=Some(r,None))" in exI)
  apply (subgoal_tac "HT_extends (\<Sigma>(a \<mapsto> (r, None))) \<Sigma>", simp)
  prefer 2 apply (simp add: HT_extends_def, clarsimp)
    apply (drule heapD, assumption)  apply clarsimp
  apply (subgoal_tac "(\<Sigma>(a:=Some (r, None)), locVal a, stringTP {r}) \<in> wfVal")
  prefer 2 apply (rule wfVal_String) apply fastsimp apply simp
  apply (simp (no_asm) only: heap_wt_def) 
    apply (rule, clarsimp)
      apply (rule, clarsimp) apply (simp add: stringObj_def)
                             apply (simp add: StringCond_implies_Policy_def)
      apply clarsimp apply (drule heapD,assumption) apply clarsimp
        apply (erule objwt_HTextends) apply assumption
    apply (erule wfVal_sub) apply assumption
(*Let*)
apply clarsimp
  apply (drule FjeuSD_complete) apply clarsimp
  apply (erule_tac x=\<Delta> in allE, erule_tac x=\<sigma> in allE, clarsimp)
  apply (erule_tac x=\<Sigma> in allE, erule impE) apply (erule storewf_sub) apply assumption 
  apply clarsimp
  apply (erule_tac x="\<Delta>(x:=Some \<sigma>)" in allE, erule_tac x=\<omega> in allE, clarsimp)
  apply (erule_tac x=\<Pi> in allE, erule impE)
    apply (simp (no_asm) add: store_wf_def) apply clarsimp 
    apply (drule VarEnvSubtypingD) apply assumption apply clarsimp
    apply (drule storeD, assumption) apply clarsimp
    apply (rule wfVal_sub) apply (erule wfVal_HTextends) apply assumption apply assumption
  apply clarsimp
  apply (rule_tac x=\<Pi>' in exI, simp)
  apply rule apply (erule HT_extends_trans) apply assumption
  apply (erule wfVal_sub) apply assumption
(*Cond*)
apply clarsimp
  apply (drule FjeuSD_complete) apply clarsimp
  apply (erule disjE)
    apply clarsimp  
     apply (erule_tac x="\<Delta>(x \<mapsto> objTP C (R \<inter> S), y \<mapsto> objTP D (R \<inter> S))" in allE, 
            erule_tac x=\<omega> in allE, clarsimp)
      apply (erule_tac x=\<Sigma> in allE, erule impE) 
        apply (subgoal_tac "store_wf \<Sigma> s \<Delta>")
          prefer 2 apply (erule storewf_sub) apply assumption 
        apply (rotate_tac 1, erule thin_rl)
        apply (simp add: store_wf_def, clarsimp)
        apply (rule, clarsimp)
          apply (rule, clarsimp) apply clarsimp 
            apply (subgoal_tac "\<exists>v. s y = Some v \<and> (\<Sigma>, v, objTP D S) \<in> wfVal")
              apply (erule_tac x=x in allE, erule_tac x="objTP C R" in allE, erule impE,assumption)
              apply clarsimp
              apply (erule wfVal_Cond) apply assumption
            apply (erule_tac x=y in allE, erule_tac x="objTP D S" in allE, erule mp) apply assumption
          apply clarsimp 
            apply (subgoal_tac "\<exists>v. s y = Some v \<and> (\<Sigma>, v, objTP D S) \<in> wfVal")
              apply (erule_tac x=x in allE, erule_tac x="objTP C R" in allE, erule impE,assumption)
              apply clarsimp
              apply (subgoal_tac "R \<inter> S = S \<inter> R", clarsimp)
              apply (erule wfVal_Cond) apply assumption apply fast
            apply (erule_tac x=y in allE, erule_tac x="objTP D S" in allE, erule mp) apply assumption
      apply clarsimp
      apply (rule_tac x=\<Pi> in exI, simp) apply (erule wfVal_sub) apply assumption
    apply clarsimp apply (erule_tac x=\<Delta> in allE, erule_tac x=\<omega> in allE, clarsimp)
      apply (erule_tac x=\<Sigma> in allE, erule impE) apply (erule storewf_sub) apply assumption 
      apply clarsimp
      apply (rule_tac x=\<Pi> in exI, simp) apply (erule wfVal_sub) apply assumption
(*Ifinst*)
apply clarsimp
  apply (drule FjeuSD_complete) apply clarsimp
  apply (erule disjE)
    apply clarsimp  apply (erule_tac x=\<Delta> in allE, erule_tac x=\<omega> in allE, clarsimp)
      apply (erule_tac x=\<Sigma> in allE, erule impE) apply (erule storewf_sub) apply assumption 
      apply clarsimp
      apply (rule_tac x=\<Pi> in exI, simp) apply (erule wfVal_sub) apply assumption
    apply clarsimp apply (erule_tac x=\<Delta> in allE, erule_tac x=\<omega> in allE, clarsimp)
      apply (erule_tac x=\<Sigma> in allE, erule impE) apply (erule storewf_sub) apply assumption 
      apply clarsimp
      apply (rule_tac x=\<Pi> in exI, simp) apply (erule wfVal_sub) apply assumption
(*Get*)
apply clarsimp 
  apply (drule FjeuSD_complete) apply clarsimp
  apply (rule_tac x=\<Sigma> in exI, simp, rule, rule HT_extends_refl)
  apply (drule storewf_sub) apply assumption
  apply (rotate_tac -1)
  apply (rename_tac s x a h C F f v \<Gamma> \<tau> \<Sigma> \<Delta> D R \<omega>)
  apply (drule storeD, assumption) apply clarsimp 
  apply (drule wfValD) 
  apply (erule disjE, clarsimp)
  apply (erule disjE, clarsimp) apply (simp add: subtypeOf_def)
  apply clarsimp
    apply (drule heapD, assumption) apply clarsimp
    apply (erule_tac x=r in allE, erule impE) apply (simp add: subtypeOf_def) apply clarsimp 
       (*apply (frule_tac r=r in field_getr) apply (erule exE)*) 
    apply (subgoal_tac "subclassOf C D")
    prefer 2 apply (erule subclassOf_trans) apply (simp add: subtypeOf_def)
    apply (erule_tac x=f in allE, erule impE) apply (drule_tac C=C and D=D in fields_sub) apply fast
    apply clarsimp apply (erule wfVal_sub) apply (rule_tac \<sigma>=\<omega> in subtypeOf_trans)  
      apply (frule_tac C=C and D=D in condition1) apply assumption apply clarsimp
      apply (erule subtypeOf_trans) apply (erule Meet_D) apply assumption apply (simp add: subtypeOf_def)
        apply assumption
(*GetQ*)
apply clarsimp 
  apply (drule FjeuSD_complete) apply clarsimp
  apply (rule_tac x=\<Sigma> in exI, simp, rule, rule HT_extends_refl)
  apply (drule storewf_sub) apply assumption
  apply (rotate_tac -1)
  apply (rename_tac s x a h C F f v \<Gamma> \<tau> \<Sigma> \<Delta> D R)
  apply (drule storeD, assumption) apply clarsimp 
  apply (drule wfValD) 
  apply (erule disjE, clarsimp)
  apply (erule disjE, clarsimp) apply (simp add: subtypeOf_def)
  apply clarsimp apply (rename_tac E)
    apply (drule heapD, assumption) apply clarsimp
    apply (erule_tac x=r in allE, erule impE) apply (simp add: subtypeOf_def) apply clarsimp 
       (*apply (frule_tac r=r in field_getr) apply (erule exE)*) 
    apply (subgoal_tac "subclassOf C D")
    prefer 2 apply (erule subclassOf_trans) apply (simp add: subtypeOf_def)
    apply (erule_tac x=f in allE, erule impE) apply (drule_tac C=C and D=D in fields_sub) apply fast
    apply clarsimp apply (erule wfVal_sub) apply (rule_tac \<sigma>=\<sigma> in subtypeOf_trans)  
      apply (frule_tac C=C and D=D in condition1) apply assumption apply clarsimp apply assumption
(*Put*)
apply clarsimp 
  apply (drule FjeuSD_complete) apply clarsimp
  apply (rule_tac x=\<Sigma> in exI, rule, rule HT_extends_refl)
  apply (frule_tac x=x in VarEnvSubtypingD) apply assumption apply clarsimp
  apply (frule_tac x=x in storeD) apply assumption apply clarsimp
  apply (frule_tac x=y in VarEnvSubtypingD) apply assumption apply clarsimp
  apply (frule_tac x=y in storeD) apply assumption apply clarsimp
  apply rule prefer 2 apply (erule wfVal_sub) apply (erule subtypeOf_trans) apply assumption
  apply (drule wfValD) 
  apply (erule disjE, clarsimp) 
  apply (erule disjE, clarsimp) apply (drule_tac \<sigma>=\<tau>'' in subtypeOf_trans,assumption) apply (simp add: subtypeOf_def)
  apply clarsimp
  apply (rename_tac s x a h C F y w f \<Gamma> \<tau> \<Sigma> \<Delta> D R \<tau>' \<tau>'' \<tau>''' r E)
  apply (erule_tac x=r in allE,erule impE) apply (drule_tac \<sigma>=\<tau>'' in subtypeOf_trans, assumption) 
         apply (simp add: subtypeOf_def) apply clarsimp
     (*apply (drule_tac r=r in field_putr) apply (erule exE)*)
  apply (simp add: heap_wt_def) 
    apply (erule_tac x=a in allE, clarsimp)
    apply (erule_tac x=f in allE, erule impE, assumption) apply clarsimp
(*    apply (frule_tac x=y in VarEnvSubtypingD) apply assumption apply clarsimp
    apply (drule_tac x=y in storeD,assumption) apply clarsimp*)
    apply (drule_tac \<sigma>=\<tau>'' in subtypeOf_trans,assumption)
    apply (erule wfVal_sub) apply (erule subtypeOf_trans)
      apply (rule subtypeOf_trans) apply (erule Join_D) apply assumption apply (simp add: subtypeOf_def)
      apply (drule_tac C=C in condition2) 
        apply (erule subclassOf_trans) apply (simp add: subtypeOf_def)
      apply clarsimp apply (erule subtypeOf_trans) apply (erule condition4, assumption)
(*PutQ*)
apply clarsimp 
  apply (drule FjeuSD_complete) apply clarsimp
  apply (rule_tac x=\<Sigma> in exI, rule, rule HT_extends_refl)
  apply (frule_tac x=x in VarEnvSubtypingD) apply assumption apply clarsimp
  apply (frule_tac x=x in storeD) apply assumption apply clarsimp
  apply (frule_tac x=y in VarEnvSubtypingD) apply assumption apply clarsimp
  apply (frule_tac x=y in storeD) apply assumption apply clarsimp
  apply rule prefer 2 apply (erule wfVal_sub) apply (erule subtypeOf_trans) apply assumption
  apply (drule wfValD) 
  apply (erule disjE, clarsimp) 
  apply (erule disjE, clarsimp) apply (drule_tac \<sigma>=\<tau>'' in subtypeOf_trans,assumption) apply (simp add: subtypeOf_def)
  apply clarsimp
  apply (rename_tac s x a h C F y w f \<Gamma> \<tau> \<Sigma> \<Delta> D R \<tau>' \<tau>'' \<tau>''' r E)
  apply (erule_tac x=r in allE,erule impE) apply (drule_tac \<sigma>=\<tau>'' in subtypeOf_trans, assumption) 
         apply (simp add: subtypeOf_def) apply clarsimp
     (*apply (drule_tac r=r in field_putr) apply (erule exE)*)
  apply (simp add: heap_wt_def) 
    apply (erule_tac x=a in allE, clarsimp)
    apply (erule_tac x=f in allE, erule impE, assumption) apply clarsimp
(*    apply (frule_tac x=y in VarEnvSubtypingD) apply assumption apply clarsimp
    apply (drule_tac x=y in storeD,assumption) apply clarsimp*)
    apply (drule_tac \<sigma>=\<tau>'' in subtypeOf_trans,assumption)
    apply (erule wfVal_sub) apply (erule subtypeOf_trans)
      apply (erule_tac \<sigma>=\<sigma> in subtypeOf_trans) 
      apply (drule_tac C=C in condition2) 
        apply (erule subclassOf_trans) apply (simp add: subtypeOf_def)
      apply clarsimp apply (erule subtypeOf_trans) apply (erule condition4, assumption)
(*StringConcat*)
apply clarsimp 
  apply (drule FjeuSD_complete) 
  apply (erule FjeuSD.cases) apply (simp_all) apply clarsimp
apply (rename_tac s X h XString Y YString a k v \<Sigma> \<Delta> x Rx y Ry r \<tau>' \<Gamma>' SC1 SC2)
apply (frule VarEnvSubtypingD) apply assumption apply clarsimp
apply (frule storewf_sub) apply assumption
apply (case_tac YString, clarsimp)
  apply (rule_tac x=\<Sigma> in exI)
  apply (rule, rule HT_extends_refl) 
  apply rule apply (frule storeD) apply assumption apply assumption
  apply (drule_tac x=x in storeD) apply assumption apply clarsimp
  apply (erule wfVal_sub) apply (erule subtypeOf_trans) apply (rule subtypeOf_trans) prefer 2 apply assumption
     apply (simp add: subtypeOf_def) apply fast
apply clarsimp
  apply (rename_tac chr chars)
  apply (rule_tac x="\<Sigma>(a:=Some(r,None))" in exI)
  apply (subgoal_tac "HT_extends (\<Sigma>(a \<mapsto> (r, None))) \<Sigma>",simp) 
  prefer 2 apply (simp add: HT_extends_def, clarsimp) 
           apply (drule heapD) apply assumption apply clarsimp
  apply (subgoal_tac "(\<Sigma>(a:=Some (r, None)), locVal a, stringTP {r}) \<in> wfVal")
  prefer 2 apply (rule wfVal_String) apply fastsimp apply simp
  apply rule prefer 2 apply (erule wfVal_sub) apply (rule subtypeOf_trans) prefer 2 apply assumption
                                apply (simp add: subtypeOf_def)
  apply (simp (no_asm) only: heap_wt_def) apply clarsimp 
  apply rule apply clarsimp apply (simp add: stringObj_def)
             apply (simp add: StringCond_implies_Policy_def) apply clarsimp
               apply (erule_tac x=Rx in allE,erule_tac x=Ry in allE,
                      erule_tac x=r in allE, clarsimp)
               apply (frule_tac \<Gamma>=\<Delta> and x=x in storeD, assumption) apply clarsimp 
                 apply (drule_tac v="locVal X" in wfValD) apply clarsimp apply (simp add: subtypeOf_def)
                 apply clarsimp apply (rename_tac rx)
               apply (frule_tac \<Gamma>=\<Delta> and x=y in storeD, assumption) apply clarsimp 
                 apply (drule_tac v="locVal Y" in wfValD) apply clarsimp apply (simp add: subtypeOf_def)
                 apply clarsimp apply (rename_tac ry)
               apply (erule_tac x=rx in allE, erule impE, assumption)
               apply (erule_tac x=ry in allE, erule impE, assumption)
               apply (erule_tac x=XString in allE, erule impE)
                 apply (drule_tac l=X in heapD, assumption) apply clarsimp 
               apply (erule_tac x="chr # chars" in allE, erule impE)
                 apply (drule_tac l=Y in heapD, assumption) apply clarsimp 
               apply assumption 
  apply clarsimp apply (drule heapD,assumption) apply clarsimp 
    apply (erule objwt_HTextends) apply assumption
(*Invoke*)
apply clarsimp 
  apply (drule FjeuSD_complete) 
  apply (erule FjeuSD.cases) apply (simp_all) apply clarsimp 
apply (frule VarEnvSubtypingD) apply assumption apply clarsimp
apply (frule storewf_sub) apply assumption
apply (rename_tac m \<Gamma>' x D R args \<tau>s \<Gamma> \<tau>' SC1 SC2 \<tau>)
apply (subgoal_tac "(\<Sigma>, locVal a, \<tau>) : wfVal")
prefer 2 apply (drule storeD) apply assumption apply clarsimp
apply (frule wfValD) apply (erule disjE, clarsimp) 
  apply (erule disjE, clarsimp) apply (drule subtypeOf_trans,assumption) apply (simp add: subtypeOf_def)
apply clarsimp
apply (frule subtypeOf_trans,assumption) 
apply (frule_tac l=a in heapD) apply assumption apply clarsimp
apply (erule_tac x=r in allE, erule impE) apply (simp add: subtypeOf_def) 
apply clarsimp 
apply (rename_tac E \<sigma>s \<sigma>)
apply (subgoal_tac "\<exists> \<Delta> . (\<Gamma>, pars, args, \<Delta>):mkStore", erule exE)
prefer 2 apply (rule mkStore_exists) apply (erule mkStore_length) 
         apply (simp add: argTypes_def) apply clarsimp
         apply (simp add: VarEnvSubtyping_def) apply (erule_tac x=n in allE, clarsimp)
         apply (case_tac "\<tau>s ! n", clarsimp)
         apply (erule_tac x="args!n" in allE, clarsimp)
         apply (erule_tac x="args!n" in allE, clarsimp)
apply (subgoal_tac "store_wf \<Sigma> t \<Delta>")
prefer 2 apply (erule mkStore_wfEnv) apply assumption apply assumption
apply (subgoal_tac "subtypeOf (objTP C {r}) (objTP D R)")
prefer 2 apply (rule_tac \<sigma>="objTP E {r}" in subtypeOf_trans) apply (simp add: subtypeOf_def) apply assumption 
apply (frule_tac C=C and D=D in condition3) apply fast apply assumption apply clarsimp
apply (rename_tac \<omega>s \<omega>)
apply (subgoal_tac "distinct pars")
prefer 2 apply (simp add: Methods_welltyped_def)
apply (subgoal_tac "(\<Delta>, (SC1,SC2), e, \<omega>) : FjeuTyping")
  apply (erule_tac x=\<Delta> in allE, erule_tac x=\<omega> in allE, clarsimp)
  apply (erule_tac x=\<Sigma> in allE, clarsimp)
  apply (rule_tac x=\<Pi> in exI, simp)
  apply (erule wfVal_sub) apply (simp add: Meth_subtypeOf_def, clarsimp)
    apply (erule subtypeOf_trans) apply assumption
apply (simp add: Methods_welltyped_def)
apply (erule_tac x=C in allE, erule_tac x=r in allE, erule_tac x=m in allE)
apply (erule_tac x=\<omega>s in allE, erule_tac x=\<omega> in allE) apply clarsimp
apply (subgoal_tac "\<exists> \<Phi> . (pars, \<omega>s, \<Phi>):mkEnv", erule exE)
prefer 2 apply (erule mkEnv_exists)
apply (erule_tac x=\<Phi> in allE, erule impE, assumption)
apply (erule TpSub) apply (rule subtypeOf_refl)
apply (subgoal_tac "\<exists> \<Delta>' . (\<Gamma>', pars, args, \<Delta>') : mkStore")
prefer 2 apply (rule mkStore_exists)  apply (erule mkStore_length) 
         apply clarsimp  apply (simp add: argTypes_def) 
apply (erule exE)  
apply (rule VarEnvSubtyping_trans) 
  apply (erule_tac \<Gamma>'=\<Gamma>' in mkStore_VarEnvSubtyping) apply assumption apply assumption
apply (erule mkStore_mkEnv_sub) apply assumption apply assumption 
  apply (erule Meth_subtypeOf_trans, assumption)
done

theorem Sound:
  "\<lbrakk> (\<Gamma>,SC,e,\<tau>):FjeuTyping ; store_wf \<Sigma> s \<Gamma>;  Methods_welltyped SC; StringCond_implies_Policy SC P;
      heap_wt h P \<Sigma>; (s,h,e,v,k) : FjeuOpsem \<rbrakk>
  \<Longrightarrow> \<exists> \<Pi> . HT_extends \<Pi> \<Sigma> \<and> heap_wt k P \<Pi> \<and> (\<Pi>,v,\<tau>): wfVal"
apply (drule_tac SC=SC and P=P in SoundAux)
apply (simp add: inter_def)
done

constdefs mkSC::"PROP_TP \<Rightarrow> StringCond"
"mkSC P \<equiv> (P, \<lambda> R S t . \<forall> r s w1 w2 . r:R \<longrightarrow> s:S \<longrightarrow> P w1 r \<longrightarrow> P w2 s \<longrightarrow> P (w1 @ w2) t)" 

lemma mkSCP_implies_P: "StringCond_implies_Policy (mkSC P) P"
apply (simp add: StringCond_implies_Policy_def mkSC_def)
done

theorem SoundForPolicy:
  "\<lbrakk> (\<Gamma>,mkSC P,e,\<tau>):FjeuTyping ; store_wf \<Sigma> s \<Gamma>;  Methods_welltyped (mkSC P);
      heap_wt h P \<Sigma>; (s,h,e,v,k) : FjeuOpsem \<rbrakk>
  \<Longrightarrow> \<exists> \<Pi> . HT_extends \<Pi> \<Sigma> \<and> heap_wt k P \<Pi> \<and> (\<Pi>,v,\<tau>): wfVal"
apply (erule Sound) apply assumption+
apply (rule mkSCP_implies_P)
apply assumption+
done

(*Before we move to string operation contexts, let's first look at an
  easier type of policy: string tables.  They map each region r to the
  set of allowed values for string objects in r.  (Essentially, we
  have done all the work for string tables already.)  *)

types "StringTable" = "Region \<Rightarrow> string set"

(*Of course,this is essentially the same type as the type PROP_TP 
of policies, so we can easliy convert a table into a policy*)
constdefs ST_2_PROP:: "StringTable \<Rightarrow> PROP_TP"
"ST_2_PROP \<Theta> \<equiv> \<lambda> w r . w : \<Theta> r"

(*Also, we could easily define the syntactic conditions for the typing system 
  explicitly: *)

constdefs TableCond::"StringTable \<Rightarrow> StringCond"
"TableCond \<Theta> \<equiv>
   (\<lambda> w r . w \<in> \<Theta> r,
    \<lambda> R S t . \<forall> r s w1 w2 . r:R \<longrightarrow> s:S \<longrightarrow> 
                             w1 : \<Theta> r \<longrightarrow> w2 : \<Theta> s \<longrightarrow> 
                             (w1 @ w2) : \<Theta> t)"

(*Trivially, this results in the same conditions as going via policies:*)

lemma TableCond_is_mkSC: "TableCond \<Theta> = mkSC (ST_2_PROP \<Theta>)"
apply (simp add: TableCond_def ST_2_PROP_def mkSC_def)
done

(*Here is the specialisation of the soundess-for-polies-theorem to
string tables.*)

theorem SoundForStringTables:
  "\<lbrakk> (\<Gamma>,TableCond \<Theta>,e,\<tau>):FjeuTyping ; store_wf \<Sigma> s \<Gamma>;  Methods_welltyped (TableCond \<Theta>);
      heap_wt h (ST_2_PROP \<Theta>) \<Sigma>; (s,h,e,v,k) : FjeuOpsem \<rbrakk>
  \<Longrightarrow> \<exists> \<Pi> . HT_extends \<Pi> \<Sigma> \<and> heap_wt k (ST_2_PROP \<Theta>) \<Pi> \<and> (\<Pi>,v,\<tau>): wfVal"
apply (insert TableCond_is_mkSC [of \<Theta>])
apply (erule Sound) apply assumption+ 
apply clarsimp apply (rule mkSCP_implies_P)
apply assumption+
done

(*Let's now do stringopcontexts*)

datatype StringOp =
  newstring string Region
| concat Region Region Region
| unknown "string set" Region

types "StringOpCtxt" = "StringOp set"

(*Can we define again a policy - of course! It's the least
interpretation as given in the paper. In order to model the
construction in Isabelle, we first define when an interpretation
satisfies the 3 conditions.*)

types "Interpretation" = "Region \<Rightarrow> string set"

constdefs Cond1 :: "StringOpCtxt \<Rightarrow> Interpretation \<Rightarrow> bool"
"Cond1 \<Omega> interp \<equiv> \<forall> w r . newstring w r : \<Omega> \<longrightarrow> w : interp r"

constdefs Cond2 :: "StringOpCtxt \<Rightarrow> Interpretation \<Rightarrow> bool"
"Cond2 \<Omega> interp \<equiv> \<forall> r s t. concat r s t : \<Omega> \<longrightarrow>
                         (\<forall> w1 w2 . w1 : interp r \<longrightarrow>
                                    w2 : interp s \<longrightarrow>
                                    w1 @ w2 : interp t)"

constdefs Cond3 :: "StringOpCtxt \<Rightarrow> Interpretation \<Rightarrow> bool"
"Cond3 \<Omega> interp \<equiv> \<forall> W r . unknown W r : \<Omega> \<longrightarrow> W \<subseteq> interp r"

constdefs Inter_good::"StringOpCtxt \<Rightarrow> Interpretation \<Rightarrow> bool"
"Inter_good \<Omega> interp \<equiv> Cond1 \<Omega> interp \<and> Cond2 \<Omega> interp \<and> Cond3 \<Omega> interp"

(*We then define the interpretation of interest as the (pointwise)
intersection of all good intepretations.*)

constdefs LeastInter :: "StringOpCtxt \<Rightarrow> Interpretation"
"LeastInter \<equiv> \<lambda> \<Omega> r . { w . \<forall> interp . Inter_good \<Omega> interp \<longrightarrow> w : interp r}"

(*Indeed, this interpretation is good itself*)

lemma LeastInter_is_good: "Inter_good \<Omega> (LeastInter \<Omega>)"
apply (unfold Inter_good_def LeastInter_def)
apply rule apply (simp add: Cond1_def)
apply rule apply (simp add: Cond2_def)
apply (simp add: Cond3_def) apply fast
done

constdefs SOC_2_PROP::"StringOpCtxt \<Rightarrow> PROP_TP"
"SOC_2_PROP \<equiv> \<lambda> \<Omega> w r . w : LeastInter \<Omega> r" 

(*In fact, ANY interpretation IS a policy -- again the types are
essentially the same:*)

constdefs interp_2_PROP::"Interpretation \<Rightarrow> PROP_TP"
"interp_2_PROP \<equiv> \<lambda> interp w r . w : interp r"

lemma "SOC_2_PROP \<Omega> = interp_2_PROP (LeastInter \<Omega>)"
apply (simp add: SOC_2_PROP_def interp_2_PROP_def) done

(*We may also generate the typing conditions for ANY intepretation:*)

constdefs interp_2_SC::"Interpretation \<Rightarrow> StringCond"
"interp_2_SC interp \<equiv> 
   (\<lambda> w r . w \<in> interp r,
    \<lambda> R S t . \<forall> r s w1 w2 . r:R \<longrightarrow> s:S \<longrightarrow> 
                             w1 : interp r \<longrightarrow> w2 : interp s \<longrightarrow> 
                             (w1 @ w2) : interp t)"

(*Note that these side conditions involve the INTERPRETATIONS. Again,
this construction trivially yields the same conditions as going via
policies:*)

lemma interp_is_mkSC: "interp_2_SC interp = mkSC (interp_2_PROP interp)"
apply (simp add: interp_2_SC_def interp_2_PROP_def mkSC_def)
done

(*Here is the specialisation of the soundness-for-policies theoremfor
arbitrary intepretations - again the type side conditions are semantic*)
 
theorem SoundForStringContext_semSCs:
  "\<lbrakk> (\<Gamma>,interp_2_SC interp,e,\<tau>):FjeuTyping ; store_wf \<Sigma> s \<Gamma>;  Methods_welltyped (interp_2_SC interp);
      heap_wt h (interp_2_PROP interp) \<Sigma>; (s,h,e,v,k) : FjeuOpsem \<rbrakk>
  \<Longrightarrow> \<exists> \<Pi> . HT_extends \<Pi> \<Sigma> \<and> heap_wt k (interp_2_PROP interp) \<Pi> \<and> (\<Pi>,v,\<tau>): wfVal"
apply (insert  interp_is_mkSC) apply clarsimp 
apply (erule Sound) apply assumption+ 
apply (rule mkSCP_implies_P)
apply assumption+
done

(*What about the syntactic conditions given in the paper:*)

constdefs StrCtxt_Conds::"StringOpCtxt \<Rightarrow> StringCond"
"StrCtxt_Conds \<Omega> \<equiv>
   (\<lambda> w r . newstring w r : \<Omega>,
    \<lambda> R S t . \<forall> r s. r:R \<longrightarrow> s : S \<longrightarrow> concat r s t : \<Omega>)"

(*They (of course) imply the least policy - because the latter is good*)

lemma StrCtxt_Conds_imply_policy: "StringCond_implies_Policy (StrCtxt_Conds \<Omega>) (SOC_2_PROP \<Omega>)"
apply (simp add: StringCond_implies_Policy_def)
apply (simp add: SOC_2_PROP_def)
apply (simp add: StrCtxt_Conds_def)
apply (insert LeastInter_is_good [of \<Omega>])
apply (simp add: Inter_good_def)
apply rule apply (simp add: Cond1_def)
apply clarsimp apply (simp add: Cond2_def) apply fast
done

theorem SoundForStringContext_syntSCs:
  "\<lbrakk> (\<Gamma>,StrCtxt_Conds \<Omega>,e,\<tau>):FjeuTyping ; store_wf \<Sigma> s \<Gamma>;  Methods_welltyped (StrCtxt_Conds \<Omega>);
      heap_wt h (SOC_2_PROP \<Omega>) \<Sigma>; (s,h,e,v,k) : FjeuOpsem \<rbrakk>
  \<Longrightarrow> \<exists> \<Pi> . HT_extends \<Pi> \<Sigma> \<and> heap_wt k (SOC_2_PROP \<Omega>) \<Pi> \<and> (\<Pi>,v,\<tau>): wfVal"
apply (erule Sound) apply assumption+ 
apply (rule StrCtxt_Conds_imply_policy)
apply assumption+
done

(*Of course, the trivial interpretation is also good.*)
constdefs FullInter :: "StringOpCtxt \<Rightarrow> Interpretation"
"FullInter \<equiv> \<lambda> \<Omega> r . {w . True}"

lemma FullInter_is_good: "Inter_good \<Omega> (FullInter \<Omega>)"
apply (simp add: Inter_good_def FullInter_def)
apply rule apply (simp add: Cond1_def)
apply rule apply (simp add: Cond2_def)
apply (simp add: Cond3_def)
done

(*The crucial property of the least solution is that each set contains ONLY strings
  construcated by the three operations. I.e. we can track where
  components of COMPOSITE strings came from. In order to prove this,
  we show that simple fact that the above construction yields indeed
  the least GOOD solution w.r.t. pointwise inclusion.*)

constdefs leq::"Interpretation \<Rightarrow> Interpretation \<Rightarrow> bool"
"leq \<equiv> \<lambda> I J . \<forall> r . I r \<subseteq> J r"

lemma Least_minimal_good: "(Inter_good \<Omega> interp) \<Longrightarrow> leq (LeastInter \<Omega>) interp"
apply (simp add:leq_def,clarsimp)
apply (simp add: LeastInter_def)
done

(*From this, we show the following elimination result, which shows
that Omega contains all information to destruct strings in the
solution.*)

lemma LeastElim:
      "w : LeastInter \<Omega> t \<Longrightarrow>
       newstring w t : \<Omega> \<or> 
       (\<exists> r s w1 w2 . concat r s t : \<Omega> \<and> w1: LeastInter \<Omega> r \<and> w2 : LeastInter \<Omega> s \<and> w = w1 @ w2)
       \<or> (\<exists> W . unknown W t : \<Omega> \<and> w: W)"
apply clarsimp
apply (case_tac "\<exists>r s. StringOp.concat r s t \<in> \<Omega> \<and> (\<exists>w1. w1 \<in> LeastInter \<Omega> r \<and> 
                       (\<exists>w2. w2 \<in> LeastInter \<Omega> s \<and> w = w1 @ w2))", assumption)
apply clarsimp
apply (subgoal_tac "Inter_good \<Omega> (\<lambda> r . if r = t then (LeastInter \<Omega> r) - {w} else (LeastInter \<Omega> r))")
  apply (drule Least_minimal_good) apply (simp add: leq_def) 
  apply (rotate_tac -1, erule_tac x=t in allE, clarsimp) apply fast
apply (insert LeastInter_is_good [of \<Omega>])
apply (simp add: Inter_good_def)
apply (rule, simp add: Cond1_def, clarsimp)
apply rule
  prefer 2 apply (simp add: Cond3_def) apply clarsimp apply fast
apply (simp add: Cond2_def, clarsimp) apply fast
done

end