theory SALSafetyLogic_deep = SALSemantics_deep + VerificationConditionGenerator:

section {* SAL Safety Logic *}

text {* In this theory we instantiate huge parts of our PCC Framework. These include
the safety logic operators (connectives, judgements) , the safety policy (safeF)  and the VCG parameter functions (succsF
and wpF). *}

subsection {* Evaluation of expressions *}

types varint = "var \<Rightarrow> tval"


consts
eval::"varint \<Rightarrow> SALstate \<Rightarrow> expr \<Rightarrow> tval"


primrec 
"eval I s (V v) = (let (p,m,e)=s in m v)"
"eval I s (Lv v) = I v"
"eval I s (C tv) = tv"
"eval I s Pc = (let (p,m,e)=s in (POS p))"
"eval I s Rp = (let (p,m,e)=s in (case (length (cs e))
 of 0 \<Rightarrow> ILLEGAL | Suc n \<Rightarrow> (case n of 0 \<Rightarrow> (POS (0,0))
                             | Suc n' \<Rightarrow> POS (incA (callpc e)))))"
"eval I s Tm = (let (p,m,e)=s in NAT (length (h e)))"
"eval I s (Add e1 e2) = (lift (op +) (eval I s e1) (eval I s e2))"
"eval I s (Minus e1 e2) = (lift (op -) (eval I s e1) (eval I s e2))"
"eval I s (Mult e1 e2) = (lift (op *) (eval I s e1) (eval I s e2))"
"eval I s (Deref e') = (case (eval I s e')
                     of ILLEGAL \<Rightarrow> ILLEGAL
                     | NAT v \<Rightarrow> (let (p,m,e)=s in m v)
                     | POS r \<Rightarrow> ILLEGAL)"
"eval I s (Ifeq e0 e1 e2 e3) = (case ((eval I s e0)=(eval I s e1))
 of True \<Rightarrow> (eval I s e2) | False \<Rightarrow> (eval I s e3))"
"eval I s (Old e') = (let (p,m,e)=s in eval I (callstate e) e')"




subsection {* Validity of formulae *}

consts
validF :: "varint \<Rightarrow> SALstate \<Rightarrow> SALform \<Rightarrow> bool"   ("(_,_ \<Turnstile>  _)" [61,61,60] 60)
validFs :: "varint \<Rightarrow> SALstate \<Rightarrow> SALform list \<Rightarrow> bool"

primrec
"validFs I s [] = True"
"validFs I s (f#fs) = ((validF I s f) \<and> (validFs I s fs))"
"validF I s T = True"
"validF I s F = False"
"validF I s (And fs) = (validFs I s fs)"
"validF I s (Imp f1 f2) = (validF I s f1 \<longrightarrow> (validF I s f2))"
"validF I s (Neg f) = (\<not> validF I s f)"
"validF I s (Eq e1 e2) = ((eval I s e1) = (eval I s e2))"
"validF I s (Leq e1 e2) = (nv (eval I s e1) \<le> nv (eval I s e2))"
"validF I s (Less e1 e2) = (nv (eval I s e1) < nv (eval I s e2))"
"validF I s (Ty ex t) = (case (eval I s ex) of ILLEGAL \<Rightarrow> False | NAT n \<Rightarrow> t = Nat | POS p \<Rightarrow> t = Pos)"
"validF I s (Forall v f) = (\<forall> tv. validF (I[v::=tv]) s f)"
"validF I s (Yields ex vs) = ((eval I s ex) \<in> set vs)"


constdefs
valid :: "SALprogram \<Rightarrow> SALstate \<Rightarrow> SALform \<Rightarrow> bool" ("(_,_ \<Turnstile> _)" [61,61,60] 60)
"valid prg s f \<equiv> (\<forall> I. validF I s f)" 

subsection {* Instantiating the Safety Logic Framework *}

constdefs
FalseF :: "SALform"  ("\<FalseF>")
"FalseF \<equiv> F"

constdefs
TrueF :: "SALform" ("\<TrueF>")
"TrueF \<equiv> T"

constdefs
Conj :: "SALform list \<Rightarrow> SALform" ("\<Conj>_" [70]) 
"Conj fs \<equiv> And fs"

constdefs
Impl :: "SALform \<Rightarrow> SALform \<Rightarrow> SALform" ("_ \<Impl> _" [61,60] 60)
"Impl a b \<equiv> Imp a b" 

subsection {* Defining the VCG parameter functions succsF and wpF *}

constdefs
  isCall :: "(instr option) \<Rightarrow> pname \<Rightarrow> bool"
 "isCall instr pn' \<equiv> (case instr of
    None \<Rightarrow> False
  | Some c \<Rightarrow> (case c of
      SET x n \<Rightarrow> False
    | ADD x y \<Rightarrow> False
    | SUB x y \<Rightarrow> False
    | INC x   \<Rightarrow> False
    | JMPEQ x y t \<Rightarrow> False
    | JMPL x y t \<Rightarrow> False
    | JLE x y t \<Rightarrow> False
    | JMPB t \<Rightarrow> False
    | JMPI x \<Rightarrow> False
    | CALL x pn \<Rightarrow> (pn = pn')
    | RET x \<Rightarrow> False
    | MOV s t \<Rightarrow> False
    | HALT \<Rightarrow> False
    ))" 


constdefs
  callpoints :: "SALprogram \<Rightarrow> pname \<Rightarrow> pos list"
 "callpoints prg pn \<equiv> [cp \<in> (domC prg). isCall (cmd prg cp) pn]"


text {* The contextUp and -Dn functions are needed by wpF to express the effect of
procedure calls on the enironment (the callstack gets manipulated by these
instructions) *}

constdefs
contextUpE:: "expr \<Rightarrow> expr"
"contextUpE e \<equiv> Old e"

consts
contextUp:: "SALform \<Rightarrow> SALform"
contextUpL:: "SALform list \<Rightarrow> SALform list"

primrec
"contextUpL [] = []"
"contextUpL (f#fs) = (contextUp f)#(contextUpL fs)"
"contextUp T = T"
"contextUp F = F"
"contextUp (And fs) = (And (contextUpL fs))"
"contextUp (Imp f1 f2) = (Imp (contextUp f1) (contextUp f2))"
"contextUp (Neg f) = (Neg (contextUp f))"
"contextUp (Eq e1 e2) = (Eq (contextUpE e1) (contextUpE e2))"
"contextUp (Leq e1 e2) = (Leq (contextUpE e1) (contextUpE e2))"
"contextUp (Less e1 e2) = (Less (contextUpE e1) (contextUpE e2))"
"contextUp (Ty ex vt) = (Ty (contextUpE ex) vt)"
"contextUp (Forall x f) = (Forall x (contextUp f))"
"contextUp (Yields ex vs) = (Yields (contextUpE ex) vs)"

consts
contextDnE:: "expr \<Rightarrow> expr"

primrec
"contextDnE (V v) = V v"
"contextDnE (Lv v) = (Lv v)"
"contextDnE (C tv) = (C tv)"
"contextDnE Pc = Pc"
"contextDnE Rp = Rp"
"contextDnE Tm = Tm"
"contextDnE (Add e1 e2) = (Add (contextDnE e1) (contextDnE e2))"
"contextDnE (Minus e1 e2) = (Minus (contextDnE e1) (contextDnE e2))"
"contextDnE (Mult e1 e2) = (Mult (contextDnE e1) (contextDnE e2))"
"contextDnE (Deref e) = (Deref (contextDnE e))"
"contextDnE (Ifeq e0 e1 e2 e3) = (Ifeq (contextDnE e0) (contextDnE e1) (contextDnE e2) (contextDnE e3))"
"contextDnE (Old e) = e"

consts
contextDn:: "SALform \<Rightarrow> SALform"
contextDnL:: "SALform list \<Rightarrow> SALform list"

primrec
"contextDnL [] = []"
"contextDnL (f#fs) = (contextDn f)#(contextDnL fs)"
"contextDn T = T"
"contextDn F = F"
"contextDn (And fs) = (And (contextDnL fs))"
"contextDn (Imp f1 f2) = (Imp (contextDn f1) (contextDn f2))"
"contextDn (Neg f) = (Neg (contextDn f))"
"contextDn (Eq e1 e2) = (Eq (contextDnE e1) (contextDnE e2))"
"contextDn (Leq e1 e2) = (Leq (contextDnE e1) (contextDnE e2))"
"contextDn (Less e1 e2) = (Less (contextDnE e1) (contextDnE e2))"
"contextDn (Ty e vt) = (Ty (contextDnE e) vt)"
"contextDn (Forall n f) = (Forall n (contextDn f))"
"contextDn (Yields ex vs) = (Yields (contextDnE ex) vs)"

consts
contextOldUpE:: "expr \<Rightarrow> expr"

primrec
"contextOldUpE (V v) = V v"
"contextOldUpE (Lv v) = Lv v"
"contextOldUpE (C tv) = C tv"
"contextOldUpE Pc = Pc"
"contextOldUpE Rp = Old Rp"
"contextOldUpE Tm = Tm"
"contextOldUpE (Add e1 e2) = (Add (contextOldUpE e1) (contextOldUpE e2))"
"contextOldUpE (Minus e1 e2) = (Minus (contextOldUpE e1) (contextOldUpE e2))"
"contextOldUpE (Mult e1 e2) = (Mult (contextOldUpE e1) (contextOldUpE e2))"
"contextOldUpE (Deref e) = (Deref (contextOldUpE e))"
"contextOldUpE (Ifeq e0 e1 e2 e3) = (Ifeq (contextOldUpE e0) (contextOldUpE e1) (contextOldUpE e2) (contextOldUpE e3))"
"contextOldUpE (Old e) = (Old (Old e))"

consts
contextOldUp:: "SALform \<Rightarrow> SALform"
contextOldUpL:: "SALform list \<Rightarrow> SALform list"

primrec
"contextOldUpL [] = []"
"contextOldUpL (f#fs) = (contextOldUp f)#(contextOldUpL fs)"
"contextOldUp T = T"
"contextOldUp F = F"
"contextOldUp (And fs) = (And (contextOldUpL fs))"
"contextOldUp (Imp f1 f2) = (Imp (contextOldUp f1) (contextOldUp f2))"
"contextOldUp (Neg f) = (Neg (contextOldUp f))"
"contextOldUp (Eq e1 e2) = (Eq (contextOldUpE e1) (contextOldUpE e2))"
"contextOldUp (Leq e1 e2) = (Leq (contextOldUpE e1) (contextOldUpE e2))"
"contextOldUp (Less e1 e2) = (Less (contextOldUpE e1) (contextOldUpE e2))"
"contextOldUp (Ty e vt) = (Ty (contextOldUpE e) vt)"
"contextOldUp (Forall n f) = (Forall n (contextOldUp f))"
"contextOldUp (Yields ex vs) = (Yields (contextOldUpE ex) vs)"

consts 
  ret_succs :: "SALprogram \<Rightarrow> pos \<Rightarrow> loc \<Rightarrow> pos list \<Rightarrow> (pos \<times> SALform) list"
primrec
 "ret_succs prg pc x [] = []"
 "ret_succs prg pc x (cp # cps) =
  ((let
    (pn,  i) = pc; 
    (pn', j) = cp;
     an = (case (anF prg cp) of
            None \<Rightarrow> TrueF
            | Some f \<Rightarrow> (contextUp f)
          )
   in ((pn', Suc j), 
       Conj [(Eq (V x) (C (POS (pn', Suc j)))),(Eq Pc (C (POS (pn,i)))), an])
   )# (ret_succs prg pc x cps)
  )"

lemma ret_succs_split:
"ret_succs prg pc x (l1@l2) = (ret_succs prg pc x l1) @ (ret_succs prg pc x l2)"
(*<*)
apply (induct_tac l1)
apply simp
apply (simp add: ret_succs.simps)
(*>*)
done

consts 
jumptargets::"nat \<Rightarrow> loc \<Rightarrow> SALform \<Rightarrow> pos list"
jumptargetsL::"nat \<Rightarrow> loc \<Rightarrow> SALform list \<Rightarrow> pos list"

primrec 
"jumptargetsL pn v [] = []"
"jumptargetsL pn v (f#fs) = (jumptargets pn v f)@(jumptargetsL pn v fs)"
"jumptargets pn v T = []"
"jumptargets pn v F = []"
"jumptargets pn v (And fs) = jumptargetsL pn v fs"
"jumptargets pn v (Imp f1 f2) = []"
"jumptargets pn v (Neg f) = []"
"jumptargets pn v (Eq e1 e2) = []"
"jumptargets pn v (Leq e1 e2) = []"
"jumptargets pn v (Less e1 e2) = []"
"jumptargets pn v (Ty ex tp) = []"
"jumptargets pn v (Forall v' f) = []"
"jumptargets pn v (Yields ex vs) = (case ex of V v' \<Rightarrow> (case (v = v') 
                                                        of True \<Rightarrow> map (\<lambda> tv. (pn,nv tv)) vs 
                                                        | False \<Rightarrow> []) 
                                       | Lv v' \<Rightarrow> []
                                       | C tv \<Rightarrow> []
                                       | Pc \<Rightarrow> []
                                       | Rp \<Rightarrow> []
                                       | Tm \<Rightarrow> []
                                       | (Add e1 e2) \<Rightarrow> []
                                       | (Minus e1 e2) \<Rightarrow> []
                                       | (Mult e1 e2) \<Rightarrow> []
                                       | (Deref ex) \<Rightarrow> []
                                       | (Ifeq e1 e2 e3 e4) \<Rightarrow> []
                                       | (Old ex) \<Rightarrow> [])"
                                       
 

constdefs
  succsF::"SALprogram \<Rightarrow> pos \<Rightarrow> (pos \<times> SALform) list"
 "succsF prg pc \<equiv> (let (pn, i) = pc in (case (cmd prg pc) of 
    None \<Rightarrow> []
  | Some ins \<Rightarrow> (case ins of 
      SET x n \<Rightarrow> [((pn, i + 1), Eq Pc (C (POS (pn,i))))]
    | ADD x y \<Rightarrow> [((pn, i + 1), Eq Pc (C (POS (pn,i))))]
    | SUB x y \<Rightarrow> [((pn, i + 1), Eq Pc (C (POS (pn,i))))]
    | INC x \<Rightarrow> [((pn, i + 1),  Eq Pc (C (POS (pn,i))))]
    | JMPEQ x y t \<Rightarrow> [((pn, i + t), And [ (Ty (V x) Nat), (Ty (V y) Nat), (Eq (V x) (V y)), (Eq Pc (C (POS (pn,i))))]), ((pn, i + 1), And [ (Ty (V x) Nat), (Ty (V y) Nat), (Neg (Eq (V x) (V y))), (Eq Pc (C (POS (pn,i))))])
                     ]
    | JMPL x y t \<Rightarrow> [((pn, i + t), And [(Ty (V x) Nat), (Ty (V y) Nat), (Less (V x) (V y)), (Eq  Pc (C (POS (pn,i))))]), ((pn, i + 1), And [(Ty (V x) Nat), (Ty (V y) Nat), (Neg (Less (V x) (V y))), (Eq Pc (C (POS (pn,i))))])
                    ] 
    | JLE x y t \<Rightarrow> [((pn, i + t), And [(Ty (V x) Nat), (Ty (V y) Nat), (Leq (V x) (V y)), (Eq  Pc (C (POS (pn,i))))]), ((pn, i + 1), And [(Ty (V x) Nat), (Ty (V y) Nat), (Neg (Leq (V x) (V y))), (Eq Pc (C (POS (pn,i))))])
                    ]
    | JMPB t \<Rightarrow> [((pn, i - t), Eq Pc (C (POS (pn,i))))]
    | JMPI x \<Rightarrow> (case (anF prg pc) of None \<Rightarrow> [] | Some A \<Rightarrow> map (\<lambda> (pn',i'). ((pn',i'), Eq (V x) (C (NAT i')))) (jumptargets pn x A))
    | CALL x pn' \<Rightarrow> [((pn', 0), Eq Pc (C (POS (pn,i))))]
    | RET x \<Rightarrow> (ret_succs prg pc x (callpoints prg pn))
    | MOV s t \<Rightarrow> [((pn,i+1), Eq Pc (C (POS (pn,i))))]
    | HALT \<Rightarrow> []

)))"

constdefs
wpF :: "SALprogram \<Rightarrow> pos \<Rightarrow> pos \<Rightarrow> SALform \<Rightarrow> SALform"
"wpF prg pc1 pc2 Q \<equiv> let (pn, i) = pc1; (pn',j) = pc2 in 
    (case (cmd prg (pn,i)) of
      None \<Rightarrow> FalseF
    | Some ins \<Rightarrow> (case ins 
      of SET x n \<Rightarrow> substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2)),(V x,C (NAT n))] Q
      | ADD x y  \<Rightarrow> substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2)),(V x, Add (V x) (V y))] Q
      | SUB x y  \<Rightarrow> substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2)),(V x, Minus (V x) (V y))] Q
      | INC x    \<Rightarrow> substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2)),(V x, Add (V x) (C (NAT 1)))] Q
      | JMPEQ x y t \<Rightarrow> substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2))] Q
      | JMPL x y t  \<Rightarrow> substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2))] Q 
      | JLE x y t  \<Rightarrow> substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2))] Q
      | JMPB t      \<Rightarrow> substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2))] Q 
      | JMPI x      \<Rightarrow> substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2))] Q
      | CALL x pn'' \<Rightarrow> (contextDn (substF NoPt [(Tm,Add Tm (C (NAT 1))),(Rp,C (POS (pn,i+1))),(Pc,C (POS pc2)),(V x,C (POS (pn,i+1)))] Q))
      | RET x \<Rightarrow> contextOldUp (substF NoPt [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2))] Q)
      | MOV s t \<Rightarrow> substF (Mv s t) [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS pc2))] Q
      | HALT \<Rightarrow> TrueF
))"


subsection {* Instantiating the safety policy *}

constdefs 
safeF :: "SALprogram \<Rightarrow> pos \<Rightarrow> SALform"
"safeF prg pc \<equiv> (let (pn,i) = pc in (case (cmd prg pc) of
    None \<Rightarrow> FalseF
  | Some ins \<Rightarrow> (case ins of
      SET x n \<Rightarrow> Leq (C (NAT n)) (C (NAT MAX)) 
    | ADD x y \<Rightarrow> Leq (Add (V x) (V y)) (C (NAT MAX))
    | SUB x y \<Rightarrow> And [(Ty (V x) Nat), (Ty (V y) Nat)]
    | INC x  \<Rightarrow> Less (V x) (C (NAT MAX))
    | JMPEQ x y t \<Rightarrow> And [(Ty (V x) Nat), (Ty (V y) Nat)]
    | JMPL x y t \<Rightarrow> And [(Ty (V x) Nat), (Ty (V y) Nat)]  
    | JLE x y t \<Rightarrow> And [(Ty (V x) Nat), (Ty (V y) Nat)]
    | JMPB t \<Rightarrow> TrueF  
    | JMPI x \<Rightarrow> Ty (V x) Nat
    | CALL x pn' \<Rightarrow> TrueF
    | RET x \<Rightarrow> And [(Eq (V x) Rp), (Ty (V x) Pos)]
    | MOV s t \<Rightarrow> And [(Ty (V s) Nat), (Ty (V t) Nat)]
    | HALT \<Rightarrow> TrueF
)))"



constdefs
  ipc :: "SALprogram \<Rightarrow> pos"
  "ipc prg \<equiv> (0,0)"

constdefs
initF :: "SALprogram \<Rightarrow> SALform"
"initF prg \<equiv> And [(Eq Pc (C (POS (0,0)))),
                  (Forall 0 (Eq (Deref (Lv 0)) (C ILLEGAL))), 
                  (Forall 0 (Eq (Old (Deref (Lv 0))) (C ILLEGAL))),
                  (Eq Rp (C (POS (0,0)))),
                  (Eq Tm (C (NAT 0)))]"

constdefs
isafeF::"SALprogram \<Rightarrow> pos \<Rightarrow> SALform"
"isafeF prg pc \<equiv> isafe(domC prg,prg,anF prg,pc,FalseF,Conj,Impl,safeF,succsF,wpF)"


constdefs
isafeP::"SALprogram \<Rightarrow> SALstate set" ("isafe\<^sub>\<box>_" [70])
"isafeP prg \<equiv> (isafeP' effS valid initF isafeF prg)"

lemma  isafeP_induct:
"\<lbrakk> s \<in> (isafeP prg); 
   \<And> s. \<lbrakk> valid prg s (initF prg) \<rbrakk> \<Longrightarrow> P s;
   \<And> s s'. \<lbrakk> s \<in> (isafeP prg); valid prg s (isafeF prg (fst s)); valid prg s' (isafeF prg (fst s')); (s,s') \<in> (effS prg); P s \<rbrakk> \<Longrightarrow> P s' \<rbrakk> \<Longrightarrow> P s"
(*<*)
apply (simp only: isafeP_def)
apply (rule isafeP'.induct)
apply simp
apply atomize
apply auto
(*>*)
done


lemma doubleAllI:
"(\<forall> x. P x = Q x) \<Longrightarrow> (\<forall> x. P x) = (\<forall> y. Q y)"
(*<*)
apply simp
(*>*)
done



(*
subsection {* Provability of formulae *}

text {* Instead of introducing derivation rules for form, we reuse Isabelle/HOL's
inference rules by defining provability with a HOL formula. *}

consts
  provable :: "SALprogram \<Rightarrow> SALform \<Rightarrow> bool" ("(_ \<turnstile> _)" [61,60] 60)


defs provable_def:
 "prg \<turnstile> f \<equiv> (\<forall> s \<in> isafeP prg. prg,s \<Turnstile> f)"

theorem correctSafetyLogic:
"\<lbrakk> prg \<turnstile> f; s \<in> (isafeP prg) \<rbrakk> \<Longrightarrow>  prg,s \<Turnstile> f"
by (simp add: provable_def valid_def)



*)

(* If you uncomment the provability definition above, the remainder of this theory is not needed and must
   be commented *)


subsection {* Provability of formulae *}

text {* In this section we define a proof calculus for our safety logic. We use natural deduction plus an extra rule
HOLprf that allows us to defer the remainder of a proof to the Isabelle/HOL proof calculus. *}

subsubsection {* Renaming and Instantiation for Integer Variables *}

text {* The following is only required for the elimination rule of the Forall quantifier *}

consts
minL::"nat list \<Rightarrow> nat"
minLe::"nat \<Rightarrow> nat list \<Rightarrow> nat"

primrec
"minLe n [] = n"
"minLe n (x#xs) = (case (x < n) 
                   of True \<Rightarrow> minLe x xs
                   | False \<Rightarrow> minLe n xs)"

defs minL_def:
"minL ns == minLe (hd ns) ns"



lemma minLe_le:
"\<And> n n'. \<lbrakk> n \<le> n' \<rbrakk> \<Longrightarrow> (minLe n ns = n \<or> ((minLe n ns = minLe n' ns) \<and> (minLe n ns < n))) \<and> (\<forall> n' \<in> set ns. minLe n ns \<le> n')"
(*<*)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (induct_tac ns)
apply simp
apply (rule allI)+
apply (rule impI)+
apply simp
apply (case_tac "a < n")
apply simp
apply (erule_tac x="a" in allE)
apply (erule_tac x="n" in allE)
apply (subgoal_tac "a \<le> n")
 prefer 2
 apply simp
apply simp
apply (erule conjE)
apply (erule disjE)
apply simp
apply (erule conjE)+
apply simp

apply simp
apply (case_tac "a < n'")
apply simp
apply (simp only: linorder_not_less)
apply (erule_tac x="n" in allE)
apply (erule_tac x="a" in allE)
apply (drule mp, assumption)
apply (erule conjE)
apply (erule disjE)
apply simp
apply (erule conjE)
apply simp

apply (case_tac "a < n'")
apply simp

apply simp
apply (simp only: linorder_not_less)
apply (subgoal_tac "n \<le> a")
 prefer 2
 apply simp
apply (erule_tac x="n" in allE)
apply (erule_tac x="a" in allE)
apply (drule mp, assumption)
apply (erule conjE)
apply (erule disjE)
apply simp
apply (erule conjE)
apply simp
(*>*)
done


lemma minL_in:
"ns\<noteq>[] \<Longrightarrow> minL ns \<in> set (ns)"
(*<*)
apply (induct ns)
apply simp
apply (case_tac list)
apply (simp add: minL_def)
apply simp
apply (case_tac "aa < a")
apply (simp add: minL_def)
apply (simp add: minL_def)
apply (simp only: linorder_not_less)
apply (drule_tac ns="lista" and n="a" and n'="aa" in minLe_le)
apply (erule conjE)
apply (erule_tac P="minLe a lista = a" in disjE)
apply simp
apply simp
(*>*)
done

lemma minL_sem:
"\<forall> n \<in> set ns. minL ns \<le> n"
(*<*)
apply (induct ns)
apply simp
apply (rule ballI)
apply (case_tac "list")
apply (simp add: minL_def)
apply (simp add: minL_def)
apply (erule conjE)
apply (erule disjE)
apply (case_tac "aa < a")
apply simp
apply simp
apply (simp only: linorder_not_less)
apply (drule_tac n="a" and n'="aa" and ns="lista" in minLe_le)
apply (erule conjE)
apply (erule disjE)
apply simp
apply (erule conjE)
apply simp

apply (case_tac "aa < a")
apply simp
apply (erule disjE)
apply simp
apply simp

apply simp
apply (simp only: linorder_not_less)
apply (frule_tac n="a" and n'="aa" and ns="lista" in minLe_le)
apply (erule conjE)
apply (erule disjE)
apply (erule disjE)
apply simp

apply simp

apply (erule_tac x="n" in ballE)
apply simp
apply simp
(*>*)
done

lemma minL_switch:
"minL (xs @ y#ys) = minL (y#xs @ ys)"
(*<*)
apply (subgoal_tac "minL (y#xs @ ys) \<le> minL (xs @ y#ys)")
 prefer 2
 apply (subgoal_tac "minL (xs @ y #ys) \<in> set (y#xs @ ys)")
  prefer 2
  apply (subgoal_tac "xs @ y # ys \<noteq> []")
   prefer 2
   apply simp
  apply (drule minL_in)
  apply simp
 apply (cut_tac ns="y # xs @ ys" in minL_sem)
 apply (erule_tac x="minL (xs @ y #ys)" in ballE)
 apply assumption
 apply simp

apply (subgoal_tac "minL (xs @ y#ys) \<le> minL (y#xs @ ys)")
 prefer 2
 apply (subgoal_tac "minL (y#xs @ ys) \<in> set (xs @ y#ys)")
  prefer 2
  apply (subgoal_tac "y # xs @ ys \<noteq> []")
   prefer 2
   apply simp
  apply (drule minL_in)
 apply simp
 apply (cut_tac ns="xs @ y#ys" in minL_sem)
 apply (erule_tac x="minL (y#xs @ ys)" in ballE)
 apply assumption
 apply simp
apply simp
(*>*)
done

lemma minL_subset:
"\<And> xs ys. ys \<noteq> [] \<Longrightarrow> set ys \<subseteq> set xs  \<Longrightarrow> minL xs \<le> minL ys"
(*<*)
apply (subgoal_tac "\<exists> k. k = length xs")
 prefer 2
 apply simp
apply (subgoal_tac "\<exists> l. l = length ys")
 prefer 2
 apply simp
apply (erule exE)+
apply (subgoal_tac "\<exists> m. m=k+l")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch5)
apply (rule allI)
apply (rule_tac n="m" in nat_less_induct) 
apply (rule allI)+
apply (rule impI)+
apply (case_tac "xs")
apply simp
apply (case_tac "ys")
apply simp
apply (drule_tac s="ys" in sym)
apply (simp only:)
apply (cut_tac ns="a # list" in minL_def)
apply (simp add: hd.simps del: minL_def minLe.simps)

apply (subgoal_tac "set ys \<subseteq> set list \<longrightarrow> ys \<noteq> [] \<longrightarrow> minL list \<le> minL ys")
 prefer 2
 apply (erule_tac x="length list + length ys" in allE)
 apply (subgoal_tac " length list + length ys < Suc (length list + length ys)")
  prefer 2
  apply simp
 apply (drule mp, assumption)
 apply (erule_tac x="list" in allE)
 apply (erule_tac x="ys" in allE)
 apply (subgoal_tac " length list + length ys = length list + length ys ")
  prefer 2
  apply simp
 apply (drule mp, assumption)
 apply assumption

apply (case_tac " set ys \<subseteq> set list")
apply (drule mp, assumption)
apply (drule mp, assumption)

apply simp
apply (case_tac "list")
apply simp

apply (simp add: minL_def)
apply (case_tac "ab < a")
apply simp

apply simp
apply (simp only: linorder_not_less)
apply (frule_tac n="a" and n'="ab" and ns="listb" in minLe_le)
apply (erule conjE)
apply (erule disjE)
apply (subgoal_tac "minLe ab listb \<in> set (ab#listb)")
 prefer 2
 apply (subgoal_tac "minLe ab listb = minL (ab#listb)")
  prefer 2 
  apply (simp add: minL_def)
 apply (simp only:)
 apply (subgoal_tac "ab # listb \<noteq> []")
  prefer 2
  apply simp
 apply (drule_tac ns="ab#listb" in minL_in)
 apply assumption
apply simp
apply (erule disjE)
apply simp

apply (erule_tac x="minLe ab listb" in ballE)
apply simp
apply simp

apply (erule conjE)
apply simp

--{* case not ys subseteq list *}
apply (subgoal_tac "a \<in> set ys")
 prefer 2
 apply (rule classical)
 apply (simp add: subset_insert_iff)
apply (subgoal_tac "a\<notin> set list")
 prefer 2
 apply (rule classical)
 apply (simp add: insert_absorb)

apply (simp only: in_set_conv_decomp)
 apply  (erule exE)+
 apply (subgoal_tac "minL (ysa @ a # zs) = minL (a # ysa @ zs)")
  prefer 2
  apply (rule minL_switch)
 apply (simp only:)

apply (subgoal_tac " set (ysa@zs) \<subseteq> set xs \<longrightarrow> (ysa@zs) \<noteq> [] \<longrightarrow> minL xs \<le> minL (ysa@zs)")
 prefer 2
 apply (erule_tac x="length xs + length (ysa @ zs)" in allE)
 apply (subgoal_tac " length xs + length (ysa @ zs) < Suc (length list + length (ysa @ a # zs))")
  prefer 2
  apply simp
 apply (drule mp,assumption)
 apply (erule_tac x="xs" in allE)
 apply (erule_tac x="ysa @ zs" in allE)
 apply simp
apply (subgoal_tac "set (ysa @ zs) \<subseteq> set xs")
 prefer 2
 apply simp
apply (drule mp, assumption)
apply (case_tac "ysa @ zs")
apply (subgoal_tac "a \<le> a")
 prefer 2
 apply simp
apply (drule_tac n="a" and n'="a" and ns="a #list" in minLe_le)
apply (erule conjE)
apply (erule_tac x="a" in ballE)
apply (simp add: minL_def)
apply simp

apply simp

apply (simp add: minL_def)
apply (case_tac "ab < a")
apply simp

apply simp
apply (simp only: linorder_not_less)
apply (drule_tac n="a" and n'="ab" and ns="listb" in minLe_le)
apply (erule conjE)+
apply (erule disjE)+
apply simp

apply (erule conjE)+
apply (rule_tac P="\<lambda> t. minLe a list \<le> t" and t="minLe a listb" and s="minLe ab listb" in subst)
apply (rule sym)
apply assumption
apply assumption

apply (erule disjE)
apply simp
apply (subgoal_tac "minLe a list = minLe a (a #list)")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "a \<le> a")
 prefer 2
 apply (simp (no_asm))
apply (drule_tac n="a" and n'="a" and ns="a #list" in minLe_le)
apply (erule conjE)+
apply (erule_tac x="a" and A="set (a # list)" in ballE)
apply assumption
apply (erule_tac P="a \<notin> set (a # list)" in rev_mp)
apply (simp (no_asm))
apply (erule conjE)
apply (rule_tac P="\<lambda> t. minLe a list \<le> t" and t="minLe a listb" and s="minLe ab listb" in subst)
apply (rule sym)
apply assumption
apply assumption
(*>*)
done

constdefs
delL::"'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
"delL a xs == [x\<in>xs. x \<noteq> a]"

lemma delL_length:
"\<And> a. a \<in> set xs \<Longrightarrow> length (delL a xs) < length xs"
(*<*)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (induct xs)
apply simp
apply (rule allI)
apply (case_tac "aa = a")
apply (simp add: delL_def)
apply (simp only: not_less_eq[THEN sym])
apply (simp only: linorder_not_less)
apply (rule length_filter)
apply (erule_tac x = "aa" in allE)
apply (rule impI)
apply (simp add: delL_def)
(*>*)
done

lemma delL_setdiff: "set (delL x xs) = (set xs) - {x}"
(*<*)
apply (simp add: delL_def)
apply auto
(*>*)
done

lemma setdiff_notin:
"x \<notin> B \<Longrightarrow> (x \<notin> (A - B)) = (x \<notin> A)"
by auto


lemma delL_subset:
"\<And> x. set (delL x xs) \<subseteq> set xs"
(*<*)
apply (simp add: delL_setdiff set_diff_def)
apply (rule subsetI)
apply simp
(*>*)
done

lemma newVar_hint:  "\<forall>v vs. v mem vs \<longrightarrow> length (delL (minL vs) vs) < length vs"
(*<*)
apply (rule allI)+
apply (rule impI)
apply (subgoal_tac "vs \<noteq> []")
 prefer 2
 apply (rule classical)
 apply simp
apply (drule minL_in)
apply (frule_tac a="minL vs" in  delL_length)
apply assumption
(*>*)
done

consts
newVar :: "var \<times> (var list) \<Rightarrow> var"

recdef newVar "measure (\<lambda> (v,vs). length vs)"
"newVar (v,vs) = (case v mem vs
                of True \<Rightarrow> newVar (Suc (minL vs),(delL (minL vs) vs))
                | False \<Rightarrow> v)"
(hints simp: newVar_hint)

lemma newVar_res:
"\<And> vs n v. \<lbrakk> vs \<noteq> [];  v = (newVar (n,vs)) \<rbrakk> \<Longrightarrow> (v = n) \<or> ((minL vs) < v)"
(*<*)
apply (subgoal_tac "\<exists> k. k = length vs")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch4)
apply (rule allI)
apply (rule "nat_less_induct")
apply (rule allI)+
apply (case_tac vs)
apply simp
apply (rule impI)+
apply (case_tac " na mem vs")
apply (erule_tac P="v = newVar (na, vs)" in rev_mp)
apply (simp (no_asm_simp) only:)
apply (subst newVar.simps)
apply (case_tac "na mem a # list")
apply (simp only: bool.cases)
apply (erule_tac x="length (delL (minL (a # list)) (a # list))" in allE)
apply (subgoal_tac "length (delL (minL (a # list)) (a # list)) < length (a # list)")
 prefer 2
 apply (subgoal_tac "minL (a # list) \<in> set (a # list)")
  prefer 2
  apply (subgoal_tac "a # list \<noteq> []")
   prefer 2
   apply simp
  apply (drule minL_in)
 apply assumption
 apply (drule_tac a="minL (a # list)" in delL_length)
 apply assumption
apply (drule mp, assumption)
apply (erule_tac x="Suc (minL (a # list))" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="delL (minL (a # list)) (a # list)" in allE)
apply (rule impI)
apply (subgoal_tac "length (delL (minL (a # list)) (a # list)) = length (delL (minL (a # list)) (a # list))")
 prefer 2 
 apply simp
apply (drule mp,assumption)
apply (drule mp,assumption)
apply (case_tac "delL (minL (a # list)) (a # list)")
apply simp
apply (subgoal_tac "delL (minL (a # list)) (a # list) \<noteq> []")
 prefer 2
 apply simp
apply (drule mp,assumption)
apply (erule disjE)
apply simp 
apply (subgoal_tac "minL (a # list) \<le> (minL (delL (minL (a # list)) (a # list)))")
 prefer 2
 apply (rule minL_subset)
 apply simp
 apply (rule delL_subset)
apply simp
--{* case na notin a list *}
apply simp

apply (simp add: minL_def delL_def newVar.simps)
(*>*)
done

lemma newVar_notin:
"\<forall> L n. newVar (n,L) \<notin> set L"
(*<*)
apply (rule allI)
apply (subgoal_tac "\<exists> k. k = length L")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch2) 
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)
apply (rule impI)
apply (rule allI)
apply (case_tac L)
apply simp

apply (subst newVar.simps)
apply (case_tac "na mem a # list")
apply (simp only: bool.cases)
apply (erule_tac x="length (delL (minL (a # list)) (a # list))" in allE)
apply (subgoal_tac "length (delL (minL (a # list)) (a # list)) < length (a # list)")
 prefer 2
 apply (subgoal_tac "a # list \<noteq> []")
  prefer 2
  apply simp
 apply (drule minL_in)
 apply (drule delL_length)
 apply assumption
apply (drule mp, assumption)
apply (erule_tac x="(delL (minL (a # list)) (a # list))" in allE)
apply (subgoal_tac "length (delL (minL (a # list)) (a # list)) = length (delL (minL (a # list)) (a # list))")
 prefer 2
 apply simp
apply (drule mp, assumption)
apply (erule_tac x="Suc (minL (a # list))" in allE)
apply (simp only: delL_setdiff)
apply (subgoal_tac "(newVar ((Suc (minL (a # list))), (delL (minL (a # list)) (a # list)))) \<notin> {(minL (a # list))}")
 prefer 2
 apply (simp (no_asm) del: newVar.simps)
 apply (erule_tac V="newVar (Suc (minL (a # list)), delL (minL (a # list)) (a # list)) \<notin> set (a # list) - {minL (a # list)}" in thin_rl)
 apply (case_tac "delL (minL (a # list)) (a # list)") 
 apply simp
 apply (subgoal_tac "delL (minL (a # list)) (a # list) \<noteq> []")
  prefer 2
  apply  simp
 apply (drule_tac vs="delL (minL (a # list)) (a # list)" and v="newVar (Suc (minL (a # list)), delL (minL (a # list)) (a # list))" and n="Suc (minL (a # list))" in newVar_res)
 apply simp
 apply (erule disjE)
 apply simp
 apply (case_tac "list")
 apply simp
 apply (subgoal_tac "minL (a # list) \<le> minL (delL (minL (a # list)) (a #list))")
  prefer 2
  apply (subgoal_tac "1 < length L")
   prefer 2
   apply simp
  apply (rule minL_subset)
  apply simp
  apply (rule delL_subset)

apply simp

apply (drule_tac A="set (a#list)" and B="{minL (a # list)}" in setdiff_notin)
apply simp

apply (simp add: set_mem_eq)
(*>*)
done

lemma newVarE:
"newVar (n,L) = v \<Longrightarrow> v\<notin> set L"
(*<*)
apply (cut_tac newVar_notin)
apply (erule_tac x="L" in allE)
apply (erule_tac x="n" in allE)
apply simp
(*>*)
done

consts 
renLvE:: "var \<Rightarrow> var \<Rightarrow> expr \<Rightarrow> expr" 

primrec renLvE:
"renLvE v v' (V v'') = V v''"
"renLvE v v' (Lv v'') = Lv (if v=v'' then v' else v'')"
"renLvE v v' (C tv) = C tv"
"renLvE v v' Pc = Pc"
"renLvE v v' Tm = Tm"
"renLvE v v' Rp = Rp"
"renLvE v v' (Add e1 e2) = Add (renLvE v v' e1) (renLvE v v' e2)"
"renLvE v v' (Minus e1 e2) = Minus (renLvE v v' e1) (renLvE v v' e2)"
"renLvE v v' (Mult e1 e2) = Mult (renLvE v v' e1) (renLvE v v' e2)"
"renLvE v v' (Deref ex) = Deref (renLvE v v' ex)"
"renLvE v v' (Ifeq e1 e2 e3 e4) = Ifeq (renLvE v v' e1) (renLvE v v' e2) (renLvE v v' e3) (renLvE v v' e4)"
"renLvE v v' (Old ex) = Old (renLvE v v' ex)"

consts 
renLvF:: "var \<Rightarrow> var \<Rightarrow> SALform \<Rightarrow> SALform" 
renLvFs:: "var \<Rightarrow> var \<Rightarrow> (SALform list) \<Rightarrow> (SALform list)"

primrec 
"renLvFs v v' [] = []"
"renLvFs v v' (f#fs) = (renLvF v v' f)#(renLvFs v v' fs)"
"renLvF v v' T = T"
"renLvF v v' F = F"
"renLvF v v' (And fs) = And (renLvFs v v' fs)"
"renLvF v v' (Imp f f') = Imp (renLvF v v' f) (renLvF v v' f')"
"renLvF v v' (Neg f) = Neg (renLvF v v' f)"
"renLvF v v' (Eq ex ex') = Eq (renLvE v v' ex) (renLvE v v' ex')"
"renLvF v v' (Leq ex ex') = Leq (renLvE v v' ex) (renLvE v v' ex')"
"renLvF v v' (Less ex ex') = Less (renLvE v v' ex) (renLvE v v' ex')"
"renLvF v v' (Ty ex tp) = Ty (renLvE v v' ex) tp"
"renLvF v v' (Forall x f) = (case x=v
                             of True \<Rightarrow> Forall x f
                             | False \<Rightarrow> Forall x (renLvF v v' f))"
"renLvF v v' (Yields ex vs) = Yields (renLvE v v' ex) vs"

consts 
intVarsF::"SALform \<Rightarrow> var list"
intVarsFs::"SALform list \<Rightarrow> var list"

primrec 
"intVarsFs [] = []"
"intVarsFs (f#fs) = (intVarsF f)@(intVarsFs fs)"
"intVarsF T = []"
"intVarsF F = []"
"intVarsF (And fs) = intVarsFs fs"
"intVarsF (Imp f f') = (intVarsF f) @ (intVarsF f')"
"intVarsF (Neg f) = (intVarsF f)"
"intVarsF (Eq ex ex') = (intVarsE ex) @ (intVarsE ex')" 
"intVarsF (Leq ex ex') = (intVarsE ex) @ (intVarsE ex')"
"intVarsF (Less ex ex') = (intVarsE ex) @ (intVarsE ex')"
"intVarsF (Ty ex tp) = (intVarsE ex)"
"intVarsF (Forall x f) = x#(intVarsF f)"
"intVarsF (Yields ex vs) = (intVarsE ex)"

consts instLvE:: "expr \<Rightarrow> expr \<Rightarrow> var \<Rightarrow> expr" ("_[_'/_]" [300, 0, 0] 300)

primrec instLvE:
"(V x)[ex/v] = (V x)"
"(Lv x)[ex/v] = (if (v=x) then ex else (Lv x))"
"(C tv)[ex/v] = C tv"
"Pc[ex/v] = Pc"
"Tm[ex/v] = Tm"
"Rp[ex/v] = Rp"
"(Add e1 e2)[ex/v] = Add (e1[ex/v]) (e2[ex/v])"
"(Minus e1 e2)[ex/v] = Minus (e1[ex/v]) (e2[ex/v])"              
"(Mult e1 e2)[ex/v] = Mult (e1[ex/v]) (e2[ex/v])"         
"(Deref ex')[ex/v] = Deref (ex'[ex/v])"
"(Ifeq e1 e2 e3 e4)[ex/v] = Ifeq (e1[ex/v]) (e2[ex/v]) (e3[ex/v]) (e4[ex/v])"
"(Old ex')[ex/v] = Old (ex'[ex/v])"

consts  instLvF:: "(SALform \<times> (var \<times> expr)) \<Rightarrow> SALform" 


syntax instLvF2 :: "SALform \<Rightarrow> expr \<Rightarrow> var \<Rightarrow> SALform" ("_[_'/_]" [300, 0, 0] 300)

translations
"instLvF2 f t v"  \<rightleftharpoons> "instLvF (f,v,t)" 


consts
sizeF::"SALform \<Rightarrow> nat"
sizeFs::"SALform list \<Rightarrow> nat"

primrec
"sizeFs [] = 0"
"sizeFs (f#fs) = (sizeF f) + (sizeFs fs)"
"sizeF T = 0"
"sizeF F = 0"
"sizeF (And fs) = Suc (sizeFs fs) + length fs"
"sizeF (Imp f1 f2) = Suc ((sizeF f1) + (sizeF f2))"
"sizeF (Neg f) = Suc (sizeF f)"
"sizeF (Eq e e') = 0"
"sizeF (Leq e e') = 0"
"sizeF (Less e e') = 0"
"sizeF (Ty e tp) = 0"
"sizeF (Forall n f) = Suc (sizeF f)"
"sizeF (Yields ex vs) = 0" 

lemma sizeF_sizeFs:
"\<forall> fs f. f \<in> set fs \<longrightarrow> sizeF f < Suc (sizeFs fs + length fs)"
apply (rule allI)
apply (induct_tac "fs")
apply auto
done

lemma renLvF_sizeF:
"sizeF (renLvF v v' f) = sizeF f"
apply (induct f)
apply simp
apply simp
apply simp
apply simp+
apply (case_tac "nat = v")
apply simp+
done

consts nV::"var \<Rightarrow> (var list) \<Rightarrow> var"
defs nV_def:
"nV == (\<lambda> v L. newVar (v,L))"
(* recdef loops when we use newVar directly *)

recdef instLvF "measure (\<lambda> (f,(v,t)). sizeF f)"
"T[ex/v] = T"
"F[ex/v] = F"
"(And fs)[ex/v] = And (map (\<lambda> f. f[ex/v]) fs)"
"(Imp f f')[ex/v] = Imp (f[ex/v]) (f'[ex/v])"
"(Neg f)[ex/v] = Neg (f[ex/v])"
"(Eq e1 e2)[ex/v] = Eq (e1[ex/v]) (e2[ex/v])"
"(Leq e1 e2)[ex/v] = Leq (e1[ex/v]) (e2[ex/v])"
"(Less e1 e2)[ex/v] = Less (e1[ex/v]) (e2[ex/v])"
"(Ty ex' tp)[ex/v] = Ty (ex'[ex/v]) tp"
"(Forall x f)[ex/v] = (case v=x 
                       of True \<Rightarrow> Forall x f
                       | False \<Rightarrow> let nv = nV x (intVarsF f @(intVarsE ex) @[v]) 
                                  in Forall nv (renLvF x nv f [ex/v]))"
"(Yields ex' vs)[ex/v] = Yields (ex'[ex/v]) vs"
(hints simp: sizeF_sizeFs renLvF_sizeF)

text {* \newpage *}

consts stateInv::"expr \<Rightarrow> bool"

primrec
"stateInv (V v) = False"
"stateInv (Lv v) = True"
"stateInv (C tv) = True"
"stateInv Pc = False"
"stateInv Tm = False"
"stateInv Rp = False"
"stateInv (Add e1 e2) = (stateInv e1 \<and> stateInv e2)"
"stateInv (Minus e1 e2) = (stateInv e1 \<and> stateInv e2)"
"stateInv (Mult e1 e2) = (stateInv e1 \<and> stateInv e2)"
"stateInv (Deref ex) = False"
"stateInv (Ifeq e1 e2 e3 e4) =(stateInv e1 \<and> stateInv e2 \<and> stateInv e3 \<and> stateInv e4)"
"stateInv (Old ex) = (stateInv ex)"

subsubsection {* The Proof Calculus *}


consts deriv :: "(SALprogram \<times> (SALform list) \<times> SALform) set"

syntax "_deriv" :: "SALprogram \<Rightarrow> (SALform list) \<Rightarrow> SALform \<Rightarrow> bool" ("(_,_ \<turnstile> _)" [61,61,60] 60)

translations
"prg,A \<turnstile> f"  \<rightleftharpoons> "(prg,A,f) \<in> deriv" 

inductive "deriv"
intros
HOLprf: "(\<forall> s \<in> (isafeP prg).  prg,s \<Turnstile> Imp (And A) f) \<Longrightarrow> prg,A \<turnstile> f"

Asm: "f \<in> (set A) \<Longrightarrow> prg,A \<turnstile> f"

And0: "prg,A \<turnstile> And []"

AndI:"prg,A \<turnstile> And fs \<Longrightarrow>  prg,A \<turnstile> f \<Longrightarrow> prg,A \<turnstile> And (f#fs)"

AndE:"f \<in> set fs \<Longrightarrow> prg,A \<turnstile> And fs \<Longrightarrow> prg,A \<turnstile> f"

ImpI:"prg,f#A \<turnstile> f' \<Longrightarrow> prg,A \<turnstile> Imp f f'"

ImpE:"prg,A \<turnstile> Imp f f' \<Longrightarrow>  prg,A \<turnstile> f \<Longrightarrow> prg,A \<turnstile> f'" 

AllI:"(\<forall> a\<in> (set A). x \<notin> set (freeIntVars a)) \<Longrightarrow> prg,A \<turnstile> f \<Longrightarrow> prg,A \<turnstile> Forall x f"

AllE:"stateInv ex \<Longrightarrow>  prg,A \<turnstile> Forall x f \<Longrightarrow> prg,A \<turnstile> f[ex/x]"
--{* In AllE we can only substitute expressions that are state independent. 
The variable Lv x, which we replace, might appear inside 
and outside of Old contexts.  State dependent parts in ex, for example variables, would
have a different meaning inside and outside of Old. *}

consts
  provable :: "SALprogram \<Rightarrow> SALform \<Rightarrow> bool" ("(_ \<turnstile> _)" [61,60] 60)

defs provable_def:
 "prg \<turnstile> f \<equiv> prg,[] \<turnstile> f"
(*<*)
lemmas ls = Impl_def TrueF_def FalseF_def Conj_def valid_def validF_validFs.simps
(*>*)
subsubsection {* Verifiy the correctness of the proof system.  *}

text {* Here we prove that the provability judegment is correct. That is provable formulae are
valid. The theorem correctSafetyLogic at the very bottom expresses this formally. It is one
of the requirements of the PcC Framework. *}


lemma stateInv_callstate_eval:
"\<And> s I. stateInv ex \<Longrightarrow> eval I (callstate (snd (snd s))) ex =  eval I s ex"
(*<*)
apply (induct ex)
apply simp+
--{* Ifeq case*}
apply (case_tac  "eval I s expr1 = eval I s expr2")
apply simp
apply simp
--{* Old *}
apply (simp add:Let_def split_def)
done
(*>*)

lemma intvar_upd_eval:
"\<And> s v I tv. v \<notin> set (intVarsE ex) \<Longrightarrow> eval (I[v ::= tv]) s ex = eval I s ex"
(*<*)
apply (induct ex)
--{* V nat *}
apply simp
--{* Lv nat *}
apply (simp add: update_def)
apply simp+
--{* Ifeq *}
apply (case_tac "eval I s expr1 = eval I s expr2 ")
apply simp
apply simp
--{* Old *}
apply (simp add: Let_def split_def)
done
(*>*)

lemma intvar_upd_validF:
"\<And> s v I tv. v \<notin> set (freeIntVars f) \<Longrightarrow> ((I[v::=tv]),s \<Turnstile> f) = (I,s \<Turnstile> f)"
(*<*)
apply (induct f)
--{* T *}
apply simp
--{* F *}
apply simp
--{* And *}
apply (drule_tac psi="(\<lambda> l. \<forall> s v I tv. (v \<notin> set (freeIntVars (\<Lambda> l))) \<longrightarrow> ((I[v ::= tv]),s \<Turnstile>  \<Lambda> l) = (I,s \<Turnstile>  \<Lambda> l)) list" in asm_rl)
apply (erule_tac x="s" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="tv" in allE)
apply simp
prefer 10
apply simp
prefer 9
apply simp
--{* Impl *}
apply simp
--{* Neg *}
apply simp
--{* Eq *}
apply (simp add: intvar_upd_eval)
--{* Leq *}
apply (simp add: intvar_upd_eval)
--{* Less *}
apply (simp add: intvar_upd_eval)
--{* Ty *}
apply (simp add: intvar_upd_eval)
--{* Forall *}
apply (case_tac "v = nat")
apply simp
apply (rule doubleAllI)
apply (rule allI)
apply (simp add: update_def)
--{* v ~= nat *}
apply atomize
apply (simp (no_asm_simp))
apply (rule doubleAllI)
apply (rule allI)
apply (subgoal_tac "I[v ::= tv][nat ::= tva] = I[nat ::= tva][v ::= tv]")
 prefer 2
 apply (simp (no_asm) add: update_def)
 apply (rule fun_upd_twist)
 apply assumption
apply (erule_tac x="s" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="I[nat ::= tva]" in allE)
apply (erule_tac x="tv" in allE)
apply simp
--{* Yields *}
apply (simp add: intvar_upd_eval)
done
(*>*)

lemma renLvE_id:
"\<And> x. renLvE x x ex = ex"
(*<*)
apply (induct ex)
apply simp+
done
(*>*)

lemma renLvF_id:
"\<And> x. renLvF x x f = f"
(*<*)
apply (induct f)
apply simp
apply simp
apply (drule_tac psi="(\<lambda> l. \<forall> x. renLvF x x (\<Lambda> l) = \<Lambda> l) list" in asm_rl)
apply (simp add: renLvE_id)+
apply (case_tac "nat = x")
apply simp
apply simp
apply (simp add: renLvE_id)
apply simp+
done
(*>*)

lemma freeIntVars_intVarsF:
"\<And> x. x \<in> set (freeIntVars f) \<Longrightarrow> x \<in> set (intVarsF f)"
(*<*)
apply (induct f)
apply simp
apply simp
apply (drule_tac psi="(\<lambda> l. \<forall> x. (x \<in> set (freeIntVars (\<Lambda> l))) \<longrightarrow> (x \<in> set (intVarsF (\<Lambda> l))) ) list" in asm_rl)
apply auto
done
(*>*)

lemma notin_intVarsF_freeIntVars:
"\<And> x. x \<notin> set (intVarsF f) \<Longrightarrow> x \<notin>  set (freeIntVars f)"
(*<*)
apply (induct f)
apply simp
apply simp
apply (drule_tac psi="(\<lambda> l. \<forall> x. (x \<notin> set (intVarsF (\<Lambda> l))) \<longrightarrow> (x \<notin>  set (freeIntVars (\<Lambda> l))) ) list" in asm_rl)
apply auto
done
(*>*)

lemma renLvE_upd:
"\<And> s. v' \<notin> (set (intVarsE ex)) \<Longrightarrow> (eval (I[v::=tv]) s ex) = (eval (I[v'::=tv]) s (renLvE v v' ex))"
(*<*)
apply (induct ex)
--{* V nat *}
apply simp
--{* Lv nat *}
apply (simp add: update_def)
--{* C tval *}
apply simp
--{* Pc *}
apply simp
--{* Rp *}
apply simp
--{* Tm *}
apply simp
--{* Add *}
apply simp
--{* Sub *}
apply simp
--{* Mult *}
apply simp
--{* Deref *}
apply simp
--{* Ifeq *}
apply simp
apply (case_tac "eval (I[v' ::= tv]) s (renLvE v v' expr1) = eval (I[v' ::= tv]) s (renLvE v v' expr2)")
apply simp
apply simp
--{* Old *}
apply atomize
apply (erule_tac x="callstate (snd (snd s))" in allE)
apply (simp add: Let_def split_def)
done
(*>*)

lemma renLvF_upd:
"\<And> f v v' I tv s. v' \<notin> (set (intVarsF f)) \<Longrightarrow> (I[v::=tv],s \<Turnstile> f) = ((I[v'::=tv]),s \<Turnstile> (renLvF v v' f))"
(*<*)
apply (subgoal_tac "\<exists> k. sizeF f = k")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch7)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI | rule impI)+
apply (case_tac "f")
--{* T *}
apply simp
--{* F *}
apply simp
--{* And *}
apply (simp only:)
apply (erule_tac V="f = And list" in thin_rl)
apply (erule rev_mp)
apply (rotate_tac -1)
apply (erule rev_mp)
apply (drule sym)
apply (simp only:)
apply (induct_tac list)
apply simp

apply (rule impI | rule allI)+
apply (subgoal_tac "v' \<notin> set (intVarsF (\<Lambda> lista))")
 prefer 2
 apply simp
apply (drule mp, assumption)+
apply (subgoal_tac "(I[v ::= tv],s \<Turnstile>  a) = (I[v' ::= tv],s \<Turnstile> renLvF v v' a)")
 prefer 2
 apply (erule_tac x="sizeF a" in allE)
 apply (subgoal_tac "sizeF a <  sizeF (\<Lambda> a # lista)") 
  prefer 2
  apply simp
 apply (drule mp,assumption)
 apply (erule_tac x="a" in allE)
 apply (erule_tac x="v" in allE)
 apply (erule_tac x="v'" in allE)
 apply (erule_tac x="I" in allE)
 apply (erule_tac x="tv" in allE)
 apply (erule_tac x="s" in allE)
 apply simp
apply (subgoal_tac "(I[v ::= tv],s \<Turnstile>  And lista) = (I[v' ::= tv],s \<Turnstile> renLvF v v' (And lista))")
 prefer 2
 apply (erule_tac x="sizeF (And lista)" in allE)
 apply (subgoal_tac "sizeF (And lista) <  sizeF (\<Lambda> a # lista)") 
  prefer 2
  apply simp
 apply (drule mp,assumption)
 apply (erule_tac x="And lista" in allE)
 apply (erule_tac x="v" in allE)
 apply (erule_tac x="v'" in allE)
 apply (erule_tac x="I" in allE)
 apply (erule_tac x="tv" in allE)
 apply (erule_tac x="s" in allE)
 apply simp
apply simp
--{* Imp *}
apply (subgoal_tac "(I[v ::= tv],s \<Turnstile>  form1) = (I[v' ::= tv],s \<Turnstile> renLvF v v' form1)")
 prefer 2
 apply (erule_tac x="sizeF form1" in allE)
 apply (subgoal_tac "sizeF form1 < n")
  prefer 2
  apply simp
 apply (drule mp, assumption)
 apply (erule_tac x="form1" in allE)
 apply (erule_tac x="v" in allE)
 apply (erule_tac x="v'" in allE)
 apply (erule_tac x="I" in allE)
 apply (erule_tac x="tv" in allE)
 apply (erule_tac x="s" in allE)
 apply simp
apply (subgoal_tac "(I[v ::= tv],s \<Turnstile>  form2) = (I[v' ::= tv],s \<Turnstile> renLvF v v' form2)")
 prefer 2
 apply (erule_tac x="sizeF form2" in allE)
 apply (subgoal_tac "sizeF form2 < n")
  prefer 2
  apply simp
 apply (drule mp, assumption)
 apply (erule_tac x="form2" in allE)
 apply (erule_tac x="v" in allE)
 apply (erule_tac x="v'" in allE)
 apply (erule_tac x="I" in allE)
 apply (erule_tac x="tv" in allE)
 apply (erule_tac x="s" in allE)
 apply simp
apply simp
--{* Neg *}
apply (subgoal_tac "(I[v ::= tv],s \<Turnstile>  form) = (I[v' ::= tv],s \<Turnstile> renLvF v v' form)")
 prefer 2
 apply (erule_tac x="sizeF form" in allE)
 apply (subgoal_tac "sizeF form < n")
  prefer 2
  apply simp
 apply (drule mp, assumption)
 apply (erule_tac x="form" in allE)
 apply (erule_tac x="v" in allE)
 apply (erule_tac x="v'" in allE)
 apply (erule_tac x="I" in allE)
 apply (erule_tac x="tv" in allE)
 apply (erule_tac x="s" in allE)
 apply simp
apply simp
--{* Eq *}
apply simp
apply (subgoal_tac "eval (I[v ::= tv]) s expr1 = (eval (I[v' ::= tv]) s (renLvE v v' expr1))")
 prefer 2
 apply (rule renLvE_upd)
 apply simp
apply (subgoal_tac "eval (I[v ::= tv]) s expr2 = (eval (I[v' ::= tv]) s (renLvE v v' expr2))")
 prefer 2
 apply (rule renLvE_upd)
 apply simp
apply simp
--{* Leq *}
apply simp
apply (subgoal_tac "eval (I[v ::= tv]) s expr1 = (eval (I[v' ::= tv]) s (renLvE v v' expr1))")
 prefer 2
 apply (rule renLvE_upd)
 apply simp
apply (subgoal_tac "eval (I[v ::= tv]) s expr2 = (eval (I[v' ::= tv]) s (renLvE v v' expr2))")
 prefer 2
 apply (rule renLvE_upd)
 apply simp
apply simp
--{* Less *}
apply simp
apply (subgoal_tac "eval (I[v ::= tv]) s expr1 = (eval (I[v' ::= tv]) s (renLvE v v' expr1))")
 prefer 2
 apply (rule renLvE_upd)
 apply simp
apply (subgoal_tac "eval (I[v ::= tv]) s expr2 = (eval (I[v' ::= tv]) s (renLvE v v' expr2))")
 prefer 2
 apply (rule renLvE_upd)
 apply simp
apply simp
--{* Tp *}
apply simp
apply (subgoal_tac "eval (I[v ::= tv]) s expr = (eval (I[v' ::= tv]) s (renLvE v v' expr))")
 prefer 2
 apply (rule renLvE_upd)
 apply simp
apply simp
--{* Forall *}
apply (case_tac "v' = nat")
apply simp
--{* v' ~= nat *}
apply (case_tac "v = nat")
apply (simp only:)
apply (simp only: renLvF_renLvFs.simps)
apply (simp (no_asm_simp))
apply (rule doubleAllI)
apply (rule allI)
apply (subgoal_tac " I[v' ::= tv][nat ::= tva] = I[nat ::= tva][v' ::= tv]")
 prefer 2
 apply (simp add: update_def)
 apply (rule fun_upd_twist)
 apply assumption
apply (subgoal_tac "I[nat ::= tv][nat ::= tva] = I[nat ::= tva]")
 prefer 2
 apply (simp (no_asm) add: update_def)
apply (simp (no_asm_simp))
apply (drule notin_intVarsF_freeIntVars)
apply simp
apply (drule_tac v="v'" and tv="tv" and s="s" and I="I[nat ::= tva]" in intvar_upd_validF)
apply simp

--{* v ~= nat *}
apply (simp (no_asm_simp))
apply (rule doubleAllI)
apply (rule allI)
apply (erule_tac x="sizeF form" in allE)
apply (subgoal_tac "sizeF form < n")
 prefer 2
 apply (simp add: renLvF_sizeF)
apply (drule mp, assumption)
apply (erule_tac x="form" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="v'" in allE)
apply (erule_tac x="I[nat ::= tva]" in allE)
apply (erule_tac x="tv" in allE)
apply (erule_tac x="s" in allE)
apply (subgoal_tac " I[v ::= tv][nat ::= tva] =  I[nat ::= tva][v ::= tv]")
 prefer 2
 apply (simp (no_asm) add: update_def)
 apply (rule fun_upd_twist)
 apply assumption
apply (subgoal_tac " I[v' ::= tv][nat ::= tva] =  I[nat ::= tva][v' ::= tv]")
 prefer 2
 apply (simp (no_asm) add: update_def)
 apply (rule fun_upd_twist)
 apply assumption
apply simp
--{* Yields *}
apply simp
apply (subgoal_tac "eval (I[v ::= tv]) s expr = (eval (I[v' ::= tv]) s (renLvE v v' expr))")
 prefer 2
 apply (rule renLvE_upd)
 apply simp
apply simp
done
(*>*)

lemma instLvE_eval:
"\<And> s I x ex'. stateInv ex' \<Longrightarrow> (eval (I[x ::=(eval I s ex')]) s ex) = eval I s (ex[ex'/x])"
(*<*)
apply (induct ex)
--{* V nat *}
apply simp
--{* Lv nat *}
apply (simp add: update_def)
--{* C tval *}
apply simp
--{* Pc *}
apply simp
--{* Tm *}
apply simp
--{* Rp *}
apply simp
--{* Add *}
apply simp
--{* Minus *}
apply simp
--{* Mult *}
apply simp
--{* Deref *}
apply simp
--{* Ifeq *}
apply simp
apply (case_tac " eval I s (expr1[ex'/x]) = eval I s (expr2[ex'/x])")
apply simp
apply simp
--{* Old *}
apply (simp add: Let_def split_def fst_conv snd_conv)
apply atomize
apply (erule_tac x="callstate (snd (snd s))" in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="x" in allE)
apply (erule_tac x="ex'" in allE)
apply (simp add: stateInv_callstate_eval)
done
(*>*)

lemma eval_intvar_update:
"\<And> I s. x \<notin> set (intVarsE ex)  \<Longrightarrow> eval (I[x ::= tv]) s ex = eval I s ex"
(*<*)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (induct ex)
--{* V nat *}
apply simp
--{* Lv nat *}
apply (simp add: update_def)
--{* C tval*}
apply simp
--{* Pc *}
apply simp
--{* Rp *}
apply simp
--{* Tm *}
apply simp
--{* Add *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (simp add: intVarsE.simps)
--{* Minus *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (simp add: intVarsE.simps)
--{* Mult *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (simp add: intVarsE.simps)
--{* Deref *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply simp
--{* Ifeq *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (rule allI)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (simp add: intVarsE.simps)
apply (case_tac " eval I s expr1 = eval I s expr2")
apply simp
apply simp
--{* Old expr *}
apply (rule allI)+
apply (erule_tac x="I" in allE)
apply (erule_tac x="callstate (snd (snd s))" in allE)
apply (simp add: Let_def split_def)
done
(*>*)

lemma validF_intvar_update:
"\<And> I s. x \<notin> set (freeIntVars f)  \<Longrightarrow> validF (I[x ::= tv]) s f = validF I s f"
(*<*)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (induct f)
--{* T *}
apply (simp add: ls)
--{* F *}
apply (simp add: ls)
--{* And *}
apply (drule_tac psi="(\<lambda> l. \<forall> I s. x \<notin> set (freeIntVars (\<Lambda> list)) \<longrightarrow> (I[x ::= tv],s \<Turnstile>  \<Lambda> l) = (I,s \<Turnstile>  \<Lambda> l)) list" in asm_rl)
apply assumption
prefer 10
apply ((rule allI)+,rule impI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply simp
prefer 9
apply (simp add: ls)
--{* Impl *}
apply ((rule allI)+, rule impI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply simp
--{* Neg *}
apply ((rule allI)+, rule impI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="s" in allE)
apply simp
--{* Eq *}
apply ((rule allI)+, rule impI)
apply simp
apply (subgoal_tac " (eval (I[x ::= tv]) s expr1) = eval I s expr1")
 prefer 2
 apply (rule  eval_intvar_update, simp)
apply (subgoal_tac "(eval (I[x ::= tv]) s expr2) = eval I s expr2")
 prefer 2
 apply (rule  eval_intvar_update, simp)
apply simp
--{* Leq *}
apply ((rule allI)+, rule impI)
apply simp
apply (subgoal_tac " (eval (I[x ::= tv]) s expr1) = eval I s expr1")
 prefer 2
 apply (rule  eval_intvar_update, simp)
apply (subgoal_tac "(eval (I[x ::= tv]) s expr2) = eval I s expr2")
 prefer 2
 apply (rule  eval_intvar_update, simp)
apply simp
--{* Less *}
apply ((rule allI)+, rule impI)
apply simp
apply (subgoal_tac " (eval (I[x ::= tv]) s expr1) = eval I s expr1")
 prefer 2
 apply (rule  eval_intvar_update, simp)
apply (subgoal_tac "(eval (I[x ::= tv]) s expr2) = eval I s expr2")
 prefer 2
 apply (rule  eval_intvar_update, simp)
apply simp
--{* Ty *}
apply ((rule allI)+, rule impI)
apply simp
apply (subgoal_tac " (eval (I[x ::= tv]) s expr) = eval I s expr")
 prefer 2
 apply (rule  eval_intvar_update, simp)
apply simp
--{* Forall *}
apply ((rule allI)+,rule impI)
apply (simp (no_asm))
apply (rule doubleAllI)
apply (rule allI)
apply (erule_tac x="I[nat ::= tva]" in allE)
apply (erule_tac x="s" in allE)
apply simp
apply (case_tac "x \<in> set (freeIntVars form)")
apply (simp add: update_def)
apply simp
apply (case_tac "x = nat")
apply (simp add: update_def)
apply (simp add: update_def)
apply (subgoal_tac " I(nat := tva, x := tv) = I(x := tv, nat := tva)")
 prefer 2
 apply (rule fun_upd_twist)
 apply simp
apply simp
--{* Yields *}
apply ((rule allI)+, rule impI)
apply simp
apply (subgoal_tac " (eval (I[x ::= tv]) s expr) = eval I s expr")
 prefer 2
 apply (rule  eval_intvar_update, simp)
apply simp
done
(*>*)

lemma instLvF_validF:
"\<And> f I x ex. stateInv ex \<Longrightarrow> ((I[x ::=(eval I s ex)]),s \<Turnstile>  f) = (I,s \<Turnstile> f[ex/x])"
(*<*)
apply (subgoal_tac "\<exists> k. sizeF f = k")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch5)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI | rule impI)+
apply (case_tac "f")
--{* T *}
apply simp
--{* F *}
apply simp
--{* And *}
apply simp
apply (erule_tac V="f = And list" in thin_rl)
apply (erule rev_mp)+
apply (induct_tac list)
apply simp

apply simp
apply (rule impI)+
apply simp
apply (subgoal_tac "(I[x ::= eval I s ex],s \<Turnstile>  a) = (I,s \<Turnstile>  a[ex/x])")
 prefer 2
 apply (erule_tac x="sizeF a" in allE)
 apply simp
apply (subgoal_tac "((I[x ::= eval I s ex]),s \<Turnstile> (And lista)) = (I,s \<Turnstile> And (map (\<lambda>f. f[ex/x]) lista))")
 prefer 2
 apply (erule_tac x="sizeF (And lista)" in allE)
 apply simp
 apply (erule_tac x="And lista" in allE)
 apply simp
apply simp
--{* Imp *}
apply simp
apply (subgoal_tac "(I[x ::= eval I s ex],s \<Turnstile>  form1) = (I,s \<Turnstile>  form1[ex/x])")
 prefer 2
 apply (erule_tac x="sizeF form1" in allE)
 apply simp
apply (subgoal_tac "(I[x ::= eval I s ex],s \<Turnstile>  form2) = (I,s \<Turnstile>  form2[ex/x])")
 prefer 2
 apply (erule_tac x="sizeF form2" in allE)
 apply simp
apply simp
--{* Neg *}
apply simp
apply (subgoal_tac "(I[x ::= eval I s ex],s \<Turnstile>  form) = (I,s \<Turnstile>  form[ex/x])")
 prefer 2
 apply (erule_tac x="sizeF form" in allE)
 apply simp
apply simp
--{* Eq *}
apply (simp add: instLvE_eval)
--{* Leq *}
apply (simp add: instLvE_eval)
--{* Less *}
apply (simp add: instLvE_eval)
--{* Ty *}
apply (simp add: instLvE_eval)
--{* Forall *}
apply simp
apply (case_tac "x = nat")
apply simp
apply (rule doubleAllI)
apply (rule allI)
apply (simp add: update_def)
--{* x ~= nat *}
apply simp
apply (subgoal_tac "\<exists> v'. nV nat (intVarsF form @ intVarsE ex @ [x]) = v'")
 prefer 2
 apply simp
apply (erule exE)
apply (simp add: Let_def)
apply (rule doubleAllI)
apply (rule allI)
apply (case_tac "nat = v'")
apply (simp add: renLvF_id)
apply (erule_tac x="sizeF form" in allE)
apply simp
apply (erule_tac x="form" in allE)
apply simp
apply (erule_tac x="I[v' ::= tv]" in allE)
apply (erule_tac x="x" in allE)
apply (erule_tac x="ex" in allE)
apply simp
apply (subgoal_tac "eval (I[v' ::= tv]) s ex = eval I s ex")
 prefer 2
 apply (subgoal_tac "v' \<notin> set (intVarsE ex)")
  prefer 2
  apply (simp only: nV_def)
  apply (drule newVarE)
  apply simp
 apply (rule intvar_upd_eval)
 apply assumption
apply simp
apply (subgoal_tac "I[v' ::= tv][x ::= eval I s ex] = I[x ::= eval I s ex][v' ::= tv]")
 prefer 2
 apply (simp add: update_def)
 apply (rule fun_upd_twist)
 apply simp
apply simp

--{* nat ~= v' *}
apply (subgoal_tac "v' \<notin> set (intVarsF form)")
 prefer 2
 apply  (simp only: nV_def)
 apply (frule newVarE)
 apply simp
apply (frule_tac v="nat" and v'="v'" and I="I[x ::= eval I s ex]" and tv="tv" and f="form" and s="s" in renLvF_upd)
apply simp
apply (erule_tac x="sizeF (renLvF nat v' form)" in allE)
apply (simp add: renLvF_sizeF)
apply (erule_tac x="(renLvF nat v' form)" in allE)
apply (simp add: renLvF_sizeF)
apply (erule_tac x="I[v' ::= tv]" in allE)
apply (erule_tac x="x" in allE)
apply (erule_tac x="ex" in allE)
apply simp
apply (subgoal_tac " eval (I[v' ::= tv]) s ex = eval I s ex")
 prefer 2
 apply (subgoal_tac "v' \<notin> set (intVarsE ex)")
  prefer 2 
  apply (simp only: nV_def)
  apply (drule newVarE)
  apply simp
 apply (rule intvar_upd_eval)
 apply simp
apply simp
apply (case_tac "x = v'")
apply (simp only: nV_def)
apply (drule newVarE)
apply simp
--{* x ~= v' *}
apply (subgoal_tac "I[v' ::= tv][x ::= eval I s ex] = I[x ::= eval I s ex][v' ::= tv]") 
 prefer 2
 apply (simp add: update_def)
 apply (rule fun_upd_twist)
 apply simp
apply simp
--{* Yields *}
apply (simp add: instLvE_eval)
done
(*>*)

lemma validFAndE: "f \<in> set fs \<Longrightarrow> validF I s (And fs) \<Longrightarrow> validF I s f"
(*<*)
apply (induct fs)
apply simp+
apply (erule disjE)
apply simp+
(*>*)
done

lemma validFs_validF_All:
"validFs I s fs = (\<forall>f\<in> set fs. validF I s f)"
(*<*)
apply (induct fs)
apply auto
done
(*>*)

lemma provable_validF:
"\<And> A prg. \<lbrakk> s \<in> (isafeP prg);  prg,A \<turnstile> f \<rbrakk>  \<Longrightarrow> (\<forall> I. (\<forall> a\<in> (set A). validF I s a) \<longrightarrow>  validF I s f)"
(*<*)
apply (erule rev_mp)
apply (erule deriv.induct)
--{* HOLprf *}
apply (rule impI)+
apply (erule_tac x="s" in ballE)
apply (simp add: valid_def)
apply (rule allI)
apply (rule impI)
apply (erule_tac x="I" in allE)
 apply (subgoal_tac "validFs I s Aa = (\<forall>f\<in> set Aa. validF I s f)")
  prefer 2
  apply (simp only: validFs_validF_All)
apply simp
apply simp
--{* Asm *}
apply (rule impI | rule allI)+
apply (erule_tac x="f" in ballE)
apply simp
apply simp
--{* And0 *}
apply simp
--{* AndI *}
apply simp
--{* AndE *}
apply (rule impI | rule allI)+
apply (drule mp, assumption)
apply (erule_tac x="I" in allE)
apply (drule mp, assumption)
apply (rule validFAndE, simp, simp)
--{* ImplI *}
apply (rule impI | rule allI)+
apply (simp add: ls)
--{* ImplE *}
apply (rule impI | rule allI)+
apply (simp add: ls)
--{* AllI *}
apply (rule impI | rule allI)+
apply (simp add: ls)
apply (rule allI)
apply (erule_tac x="I[x ::= tv]" in allE)
apply (subgoal_tac "\<forall>a\<in>(set Aa). validF (I[x::=tv]) s a")
 prefer 2
 apply (rule ballI)
 apply (erule_tac x="a" in ballE)
 apply (erule_tac x="a" in ballE)
 apply (simp add: validF_intvar_update)
 apply simp
 apply simp
apply simp
--{* AllE *}
apply (rule impI | rule allI)+
apply (drule mp,assumption)
apply (erule_tac x="I" in allE)
apply (simp add: ls)
apply simp
apply (erule_tac x="eval I s ex" in allE)
apply (drule_tac x="x" and ex="ex" and I="I" and s="s" and f="f" in instLvF_validF)
apply simp
done
(*>*)

theorem correctSafetyLogic:
"\<lbrakk> prg \<turnstile> f; s \<in> (isafeP prg) \<rbrakk> \<Longrightarrow>  prg,s \<Turnstile> f"
(*<*)
apply (simp add: provable_def valid_def)
apply (rule allI)
apply (drule_tac A="[]" and f="f" in provable_validF)
apply assumption
apply (erule_tac x="I" in allE)
apply simp
done
(*>*)

subsection {* Some derived proof rules *}

lemma AndSingle:
"prg,A \<turnstile> f \<Longrightarrow> prg,A \<turnstile> And [f]"
apply (rule AndI)
apply (rule And0)
apply assumption
done

lemma FlattenAsm:
"prg,(fs'@fs) \<turnstile> f \<Longrightarrow>  prg,((And fs)#fs') \<turnstile> f"
apply (rule HOLprf)
apply (rule ballI)
apply (drule provable_validF)
apply simp
apply (simp add: valid_def validF_validFs.simps)
apply (rule allI)
apply (rule impI)
apply (erule conjE)
apply (erule_tac x="I" in allE)
apply (subgoal_tac "(\<forall>a\<in>set fs' \<union> set fs. I,s \<Turnstile>  a)")
 prefer 2
 apply (rule ballI)
 apply (simp add: validFs_validF_All)
 apply (erule disjE)
 apply (erule_tac x="a" and A="set fs'" in ballE)
 apply assumption
 apply simp
 apply (erule_tac x="a" and A="set fs" in ballE)
 apply assumption
 apply simp
apply simp
done

lemma FlattenAsmSingle:
"prg,fs \<turnstile> f \<Longrightarrow>  prg,[And fs] \<turnstile> f"
apply (simp add: FlattenAsm)
done

lemma AsmSwap:
"prg,(fs@[f]) \<turnstile> f' \<Longrightarrow> prg,(f#fs) \<turnstile> f'"
apply (rule HOLprf)
apply (rule ballI)
apply (drule provable_validF)
apply simp
apply (simp add: valid_def validF_validFs.simps)
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (rule impI)
apply (simp add: validFs_validF_All)
done

end