theory EX_SmartCardPurse_deep = VCOpt + AuxBox:

section {* Smart Card Purse *}

text {* This program adds a credit C to a balance B if the new balance B + C does not execeed an upper bound
MAX (the highest number the safety policy accepts). To check this condition a procedure is called  which
sets a flag F to NAT 0 if this condition is violated *}

--{* program variables *}
constdefs 
  b :: nat -- "balance"
 "b \<equiv> 0"
  c :: nat -- "credit"
 "c \<equiv> 1"
  m :: nat -- "maximum"
 "m \<equiv> 2"
  p :: nat -- "return address storage"
 "p \<equiv> 3"

--{* initial values *}
constdefs
  b0 :: nat
 "b0 \<equiv> 4"  -- "maximal intial balance"
  c0 :: nat
 "c0 \<equiv> 2" -- "initial credit"
 x::nat
 "x \<equiv> 5"

constdefs prog::"SALprogram"
"prog \<equiv>
[(0, [(SET b b0, None),
      (SET c c0, None),
      (CALL p 1, Some (\<Lambda> [V b \<doteq> C (NAT b0), V c \<doteq> C (NAT c0)])),
      (ADD b c , Some (\<Lambda> [V b \<doteq> C (NAT b0), Ty (V c) Nat,
                          (C (NAT 0) \<prec> V c) \<supset> 
                             \<Lambda> [(V b \<oplus> V c) \<preceq> C (NAT MAX), V c \<doteq> C (NAT c0)]])),
      (HALT, None)]),
(1, [(SET m MAX, Some (\<Lambda> [V p \<doteq> Rp, Ty (V b) Nat, Ty (V c) Nat,
                           \<Prod>x. Neg (Eq (Lv x) (C (NAT p))) \<supset> (Deref (Lv x) \<doteq> Old (Deref (Lv x)))])),
     (SUB m c, None), 
     (JMPL b m 2, None), 
     (SET c 0, None),
     (RET p, Some (\<Lambda> [(\<Prod>x. (\<Lambda> [Neg ((Lv x) \<doteq> (C (NAT c))), Neg ((Lv x) \<doteq> (C (NAT m))),
                              Neg ((Lv x) \<doteq> C (NAT p))]) \<supset>
                               (Deref (Lv x) \<doteq> Old (Deref (Lv x)))),
                       (Neg (V c \<doteq> C (NAT 0)) \<supset> (\<Lambda> [V c \<doteq> Old (V c), 
                                                   (V b \<oplus> V c) \<preceq> C (NAT MAX)]))]))])]"




text {* \clearpage *}


subsection {* The Verification Condition *}

generate_code [term_of]
  vcg = "vcgSALDeep"
  vcopt = "vcopt"
  prg = "prog" 


ML {* set show_brackets; *}

ML {* val vc = vcg prog; *}

ML {* File.write (Path.unpack "pvc.txt") (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_form vc))); *}

ML {* val vco = vcopt [] vc; *}

ML {* File.write (Path.unpack "opvc.txt") (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_form vco))); *}

ML {* val pvc = (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_form vco))); *}

ML {* reset show_brackets *}

(*<*)
constdefs
vc::"SALform"
"vc \<equiv> (\<Lambda> [((\<Lambda> [(Pc \<doteq> (C (POS (0, 0)))), (\<Prod>0. ((Deref (Lv 0)) \<doteq> (C ILLEGAL))), (\<Prod>0. ((Old (Deref (Lv 0))) \<doteq> (C ILLEGAL))), (Rp \<doteq> (C (POS (0, 0)))), (Tm \<doteq> (C (NAT 0)))]) \<supset> (\<Lambda> [((C (NAT (Suc (Suc (Suc (Suc 0)))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((Pc \<doteq> (C (POS (0, 0)))) \<supset> (\<Lambda> [((C (NAT (Suc (Suc 0)))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (((C (POS (0, (Suc 0)))) \<doteq> (C (POS (0, (Suc 0))))) \<supset> (\<Lambda> [T, (\<Lambda> [((C (NAT (Suc (Suc (Suc (Suc 0)))))) \<doteq> 
(C (NAT (Suc (Suc (Suc (Suc 0))))))), ((C (NAT (Suc (Suc 0)))) \<doteq> (C (NAT (Suc (Suc 0)))))])]))]))])), (\<Lambda> [((\<Lambda> [(\<Lambda> [T, (\<Lambda> [((V 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0))))))), ((V (Suc 0)) \<doteq> (C (NAT (Suc (Suc 0)))))])]), (Pc \<doteq> (C (POS (0, (Suc (Suc 0))))))]) \<supset> (\<Lambda> [((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (\<Lambda> [((C (POS (0, (Suc (Suc (Suc 0)))))) \<doteq> (C (POS (0, (Suc (Suc (Suc 0))))))), (Ty (V 0) vtype.Nat), (Ty (V (Suc 0)) vtype.Nat), (\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))) \<supset> ((IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> 
(C (NAT (Suc (Suc (Suc 0))))) THEN (C (POS (0, (Suc (Suc (Suc 0)))))) ELSE (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))))])]))]), (\<Lambda> [((\<Lambda> [(\<Lambda> [(((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (\<Lambda> [((V 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0))))))), (Ty (V (Suc 0)) vtype.Nat), (((C (NAT 0)) \<prec> (V (Suc 0))) \<supset> (\<Lambda> [(((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc 0)) \<doteq> (C (NAT (Suc (Suc 0)))))]))])]), (Pc \<doteq> (C (POS (0, (Suc (Suc (Suc 0)))))))]) \<supset> (\<Lambda> [T]))]), (\<Lambda> [((\<Lambda> [(\<Lambda> [((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (\<Lambda> [((V (Suc (Suc (Suc 0)))) \<doteq> Rp), 
(Ty (V 0) vtype.Nat), (Ty (V (Suc 0)) vtype.Nat), (\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))) \<supset> ((Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (Old (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0)))))))))))])]), (Pc \<doteq> (C (POS ((Suc 0), 0))))]) \<supset> (\<Lambda> [(\<Lambda> [(Ty (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) vtype.Nat), (Ty (V (Suc 0)) vtype.Nat)]), (((C (POS ((Suc 0), (Suc 0)))) \<doteq> (C (POS ((Suc 0), (Suc 0))))) \<supset> (\<Lambda> [(\<Lambda> [(Ty (V 0) vtype.Nat), (Ty ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) vtype.Nat)]), ((\<Lambda> [(Ty (V 0) vtype.Nat), (Ty ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) vtype.Nat), ((V 0) \<prec> ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0)))), ((C (POS ((Suc 0), (Suc (Suc 0))))) \<doteq> (C (POS ((Suc 0), (Suc (Suc 0))))))]) \<supset> (\<Lambda> [(\<Lambda> [((V (Suc (Suc (Suc 0)))) \<doteq> Rp), 
(Ty (V (Suc (Suc (Suc 0)))) Pos)]), (\<Lambda> [(\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((\<Lambda> [(Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0)))))))]) \<supset> ((IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) ELSE (IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) ELSE (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))))), ((Neg ((V (Suc 0)) \<doteq> (C (NAT 0)))) \<supset> (\<Lambda> [((V (Suc 0)) \<doteq> (Old (V (Suc 0)))), (((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))]))])])), ((\<Lambda> [(Ty (V 0) vtype.Nat), (Ty ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) vtype.Nat), 
(Neg ((V 0) \<prec> ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))))), ((C (POS ((Suc 0), (Suc (Suc 0))))) \<doteq> (C (POS ((Suc 0), (Suc (Suc 0))))))]) \<supset> (\<Lambda> [((C (NAT 0)) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (((C (POS ((Suc 0), (Suc (Suc (Suc 0)))))) \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc 0))))))) \<supset> (\<Lambda> [(\<Lambda> [((V (Suc (Suc (Suc 0)))) \<doteq> Rp), (Ty (V (Suc (Suc (Suc 0)))) Pos)]), (\<Lambda> [(\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((\<Lambda> [(Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0)))))))]) \<supset> ((IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0))) THEN (C (NAT 0)) ELSE (IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) ELSE (IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) ELSE (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<doteq> (Old (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))))), 
((Neg ((C (NAT 0)) \<doteq> (C (NAT 0)))) \<supset> (\<Lambda> [((C (NAT 0)) \<doteq> (Old (V (Suc 0)))), (((V 0) \<oplus> (C (NAT 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))]))])]))]))]))]))]), (\<Lambda> [((\<Lambda> [(\<Lambda> [(\<Lambda> [((V (Suc (Suc (Suc 0)))) \<doteq> Rp), (Ty (V (Suc (Suc (Suc 0)))) Pos)]), (\<Lambda> [(\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((\<Lambda> [(Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0)))))))]) \<supset> ((Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (Old (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))))), ((Neg ((V (Suc 0)) \<doteq> (C (NAT 0)))) \<supset> (\<Lambda> [((V (Suc 0)) \<doteq> (Old (V (Suc 0)))), (((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))]))])]), (\<Lambda> [((V (Suc (Suc (Suc 0)))) \<doteq> (C (POS (0, (Suc (Suc (Suc 0))))))), (Pc \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc (Suc 0)))))))), (\<Lambda> [((Old (V 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc 0)))))))), ((Old (V (Suc 0))) \<doteq> (Old (C (NAT (Suc (Suc 0))))))])])]) \<supset> (\<Lambda> [(((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (\<Lambda> [((V 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0))))))), (Ty (V (Suc 0)) vtype.Nat), (((C (NAT 0)) \<prec> (V (Suc 0))) \<supset> (\<Lambda> [(((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc 0)) \<doteq> (C (NAT (Suc (Suc 0)))))]))])]))])])"
(*>*)

(*<*)
lemma domC_prog:"domC prog = [(0,0),(0,1),(0,2),(0,3),(0,4),(1,0),(1,1),(1,2),(1,3),(1,4)]"
apply (simp add: domC.simps prog_def Let_def fst_conv snd_conv)
done

lemma anF_prog:"domA prog = [(0,2),(0,3),(1,0),(1,4)]"
apply (simp only: domA_def domC_prog)
apply (simp add: anF.simps prog_def noProc.simps Let_def fst_conv snd_conv split_def filter.simps)
done
(*>*)

subsection {*  Program Verification *}

text {* First we ensure that the program is wellformed. *}

lemma wf_prog:
"wf prog"
apply (simp add: wf_def checkPos.simps prog_def Let_def split_def fst_conv snd_conv cmd.simps domC.simps ret_succs.simps callpoints_def isCall_def anF.simps)
done

text {* Then, we prove the verification condition *}

subsubsection {* Automated Proof *}

(*<*)
lemmas vc_simps = nat_number split_def Let_def fst_conv snd_conv b_def MAX_def b0_def c_def c0_def m_def p_def update_def fun_upd_apply callpc_def callmem_def callenv_def incA_def nth_append lift_def validF_validFs.simps nv_def 
(*>*)

lemma vc_prog_holds:
"provable prog vc"
apply (simp only: provable_def valid_def split_paired_all | rule HOLprf | rule ballI | rule allI | rule impI)+
apply (rename_tac "pn" "i" "m" "e" "I")
apply (cut_tac wf_prog, drule vc_proof_startup,assumption, (erule conjE | erule exE)+, (simp only: fst_conv snd_conv))

--{* Now, the prelude is finished. The main proof starts . . . *}
apply (simp only: vc_def)
apply (auto simp add: vc_simps)
apply (simp add: vc_simps split add: tval.split tval.split_asm)

apply (simp  add: vc_simps split add: nat.split)

apply (fastsimp simp add: vc_simps)

apply (simp add: vc_simps split add: tval.split tval.split_asm)
apply arith

apply (simp split add: nat.split)
--{* nprfsize = 51.204 *}
done

subsubsection {* Manual Proof *}

--{* Lemmas about validity of formulae *}
lemma validF_True: "validF I s T = True" 
by simp

lemma validF_False: "validF I s F = False" 
by simp

lemma validF_And_Nil: "validF I s (\<Lambda> []) = True" 
by simp

lemma validF_And_Cons: "validF I s (\<Lambda> (f # fs)) = ((validF I s f) \<and> (validF I s (\<Lambda> fs)))"
by simp

lemma validF_And_Cons_Nil: "valid' (?s, (\<Lambda> [f])) = (valid' (?s, ?f))"
by simp 

lemma validF_Imp: "validF I s (f1 \<supset> f2) = ((validF I s f1) \<longrightarrow> (validF I s f2))" 
by simp

lemma validF_Neg: "validF I s (Neg f) = (\<not> (validF I s f))" 
by simp

lemma validF_Eq: "validF I s (e1 \<doteq> e2) = ((eval I s e1) = (eval I s e2))" 
by simp

lemma validF_Leq: "validF I s (e1 \<preceq> e2) = ((nv (eval I s e1)) \<le> (nv (eval I s e2)))" 
by simp

lemma validF_Less: "validF I s (e1 \<prec> e2) = ((nv (eval I s e1)) < (nv (eval I s e2)))" 
by simp

lemma validF_Forall: "validF I s (\<Prod>v. f) = (\<forall>tv. (validF (I[v::=tv]) s f))"
by (simp add: Let_def)
      

lemma length_cons:
"length (a#as) = Suc (length as)"
by simp

lemma vc_prog_holds2:
"provable prog vc"
apply (simp only: provable_def valid_def split_paired_all | rule HOLprf | rule ballI | rule allI | rule impI)+
apply (rename_tac "pn" "i" "m" "e" "I")
apply (cut_tac wf_prog, drule vc_proof_startup,assumption, (erule conjE | erule exE)+, (simp only: fst_conv snd_conv))
apply (simp add: vc_def validF_validFs.simps del: sysinv.simps sysinv2.simps)
(* txt {* \newpage @{subgoals [display, indent=0, margin=130]} *} *)

--{* Now, the prelude is finished. The main proof starts . . . *}
apply (case_tac "prog,((pn,i),m,e) \<Turnstile> (initF prog)")
--{* (initF prg) implies (isafeF prg (ipc prg)) *}
apply (simp add: initF_def valid_def b_def MAX_def b0_def  c_def c0_def update_def fun_upd_apply nv_def)
--{* case not (initF prg) *}
apply (erule isafeP_elims)
apply (simp only: simp_thms)
apply (drule_tac t="s''" in sym)
apply (simp only: fst_conv snd_conv)
--{* now we know that ((pn,i),m,e) is inductively safe *}

apply (rule conjI)
--{* initF impliziert isafeF (0,0) *}
apply (simp add: validF_validFs.simps Let_def split_def fst_conv snd_conv nv_def)

apply (simp only: Let_def split_def fst_conv snd_conv)


apply (rule conjI)
--{* (1,0) nach (1,4), prozedurbody, zwei wege *}
apply (case_tac "css")
apply (simp only:)
apply (drule_tac P="\<lambda> s. s" in subst[OF sysinv.simps])
apply (simp add: validF_validFs.simps Let_def split_def fst_conv snd_conv nv_def lift_def)

--{* case "css = a  list" *}
apply (simp add: validF_validFs.simps Let_def split_def fst_conv snd_conv nv_def lift_def tval.cases id_lookup_def)
apply (rule impI)
apply (simp add: validF_validFs.simps Let_def split_def fst_conv snd_conv nv_def lift_def tval.cases id_lookup_def update_def split add: tval.split tval.split_asm)
apply (rule conjI | rule impI)+

apply (erule_tac x="NAT (Suc 0)" in allE)
apply (erule conjE)+
apply (erule_tac x="Suc 0" in allE)
apply simp

apply arith

--{* Sprungbedingung gilt nicht *}

apply (rule impI | rule allI | erule conjE)+
apply (rule conjI)
apply (simp add: lift_def nv_def update_def)
apply (erule_tac x="NAT 0" in allE)
apply simp
apply (case_tac "m (Suc 0)")
apply (simp add: MAX_def)
apply simp
apply (case_tac "0 < nat")
apply simp
apply simp
apply simp

apply (rule conjI)
apply (erule_tac x="NAT 0" in allE)
apply (simp add: update_def)

apply (rule conjI)
apply simp 
apply (case_tac "m (Suc 0)")
apply simp
apply simp
apply simp

apply (rule impI)
apply (simp add: nv_def lift_def)
apply (erule_tac x="NAT 0" in allE)
apply (simp add: update_def)

apply (case_tac "m (Suc 0)")
apply simp
apply simp
apply simp
(* nprfsize (frueher) = 148.293 *)
(* nprfsize (ohne simp einschraenkung) = 373.836 *)
(* nprfsize (alle Zweige manuell: 175.447 *)
(* nprfsize 85473 *)
done

subsubsection {* Optimised VC *}

text{* 
Vereinfachungen: \\
\begin{itemize}
\item verschachtelte Ands aufloesen ( And [ And [A1,..,An], ..] = And [A1,..,An, ..])
\item konstante arithmetische Ausdruecke auswerten: Plus (C (NAT 3)) (C (NAT 3)) = C (NAT 6)
\item Implikationen mit T,F vereinfachen: Imp F A = T, Imp T A = A, Imp A T = T
\item Ands mit T,F vereinfachen: And [..,T,..] = And [..,..], And [..,F,..] = F, And [] = T
\item Goals die direkt aus Assumptions folgen, herausnehmen, Imp And [..,A,..] And [..,A,..] = Imp And [..,..] And [..,..]
\item von (V x) = (C (NAT 5)) auf Ty (V x) Nat schliessen (nicht implementiert) 
\item Ty (C (NAT 15) Nat) = T 
\item einelementige Ands aufloesen And [A] = A
\end{itemize} *}

constdefs vco :: "SALform"
"vco \<equiv> (\<Lambda> [((\<Lambda> [((V 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0))))))), ((V (Suc 0)) \<doteq> (C (NAT (Suc (Suc 0))))), (Pc \<doteq> (C (POS (0, (Suc (Suc 0))))))]) \<supset> (\<Lambda> [(Ty (V 0) vtype.Nat), (Ty (V (Suc 0)) vtype.Nat), (\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))) \<supset> ((IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (C (POS (0, (Suc (Suc (Suc 0)))))) ELSE (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))))])), ((\<Lambda> [((V (Suc (Suc (Suc 0)))) \<doteq> Rp), (Ty (V 0) vtype.Nat), (Ty (V (Suc 0)) vtype.Nat), (\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))) \<supset> ((Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (Old (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))))), (Pc \<doteq> (C (POS ((Suc 0), 0))))]) \<supset> (\<Lambda> [(Ty ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) vtype.Nat), ((\<Lambda> [(Ty ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) vtype.Nat), ((V 0) \<prec> ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))))]) \<supset> (\<Lambda> [(Ty (V (Suc (Suc (Suc 0)))) Pos), (\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((\<Lambda> [(Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0)))))))]) \<supset> ((IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) ELSE (IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) ELSE (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))))), ((Neg ((V (Suc 0)) \<doteq> (C (NAT 0)))) \<supset> (\<Lambda> [((V (Suc 0)) \<doteq> (Old (V (Suc 0)))), (((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))]))])), ((\<Lambda> [(Ty ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) vtype.Nat), (Neg ((V 0) \<prec> ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0)))))]) \<supset> (\<Lambda> [(Ty (V (Suc (Suc (Suc 0)))) Pos), (\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((\<Lambda> [(Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0)))))))]) \<supset> ((IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0))) THEN (C (NAT 0)) ELSE (IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<ominus> (V (Suc 0))) ELSE (IF (Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) ELSE (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<doteq> (Old (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0)))))))))))]))])), ((\<Lambda> [((V (Suc (Suc (Suc 0)))) \<doteq> Rp), (Ty (V (Suc (Suc (Suc 0)))) Pos), (\<Prod>(Suc (Suc (Suc (Suc (Suc 0))))). ((\<Lambda> [(Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc 0)))))), (Neg ((Lv (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc (Suc (Suc 0)))))))]) \<supset> ((Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (Old (Deref (Lv (Suc (Suc (Suc (Suc (Suc 0))))))))))), ((Neg ((V (Suc 0)) \<doteq> (C (NAT 0)))) \<supset> (\<Lambda> [((V (Suc 0)) \<doteq> (Old (V (Suc 0)))), (((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))])), ((V (Suc (Suc (Suc 0)))) \<doteq> (C (POS (0, (Suc (Suc (Suc 0))))))), (Pc \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc (Suc 0)))))))), ((Old (V 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc 0)))))))), ((Old (V (Suc 0))) \<doteq> (Old (C (NAT (Suc (Suc 0))))))]) \<supset> (\<Lambda> [(((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0))))))), (Ty (V (Suc 0)) vtype.Nat), (((C (NAT 0)) \<prec> (V (Suc 0))) \<supset> (\<Lambda> [(((V 0) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc 0)) \<doteq> (C (NAT (Suc (Suc 0)))))]))]))])"

text {* Now we prove the optimized verification condition *}

lemma vco_prog_holds: 
"provable prog vco"
apply (simp only: provable_def valid_def split_paired_all | rule HOLprf | rule ballI | rule allI | rule impI)+
apply (rename_tac "pn" "i" "m" "e" "I")
apply (cut_tac wf_prog, drule vc_proof_startup,assumption, (erule conjE | erule exE)+, (simp only: fst_conv snd_conv))

--{* Now, the prelude is finished. The main proof starts . . . *}
apply (simp only: vco_def)
apply (auto simp add: vc_simps)
apply (simp add: vc_simps split add: tval.split tval.split_asm)

apply (simp  add: vc_simps split add: nat.split)

apply (fastsimp simp add: vc_simps)

apply (simp add: vc_simps split add: tval.split tval.split_asm)
apply arith

apply (simp split add: nat.split)
(* nprfsize = 43.411 *)
(* deprecated: (fuer manuellen Beweis der optimierten VC: nprfsize =  110598) *)
done



end