theory EX_DoubleAddition_deep = VCOpt:

section {* Example - Double Addition *}

text {* We verify that a program computing four times x does not overflow. The annotation
at the HALT instruction is not necessary for the safety proof, but it demonstrates that
we can also do correctness proofs in our system. *}

subsection {* Variables *}

text {* The program computes 4 times x. *}

constdefs x::nat
"x\<equiv>1"
subsection {* Annotated Program *}

text {* We initialize x with 3 (any other value v such that 4*v <= MAX could also be used)
do two successive additions on it. The annoation in the end says that the result is NAT 12. *}

constdefs prog::"SALprogram"
"prog \<equiv> [(0,[
(SET x 3,None),
(ADD x x,None),
(ADD x x,None),
(JMPB 0, Some (V x \<doteq> C (NAT 12)))])]"

subsection {* Verification Condition *}

text {* We generate an executable ML program for the VCG *}

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

ML {* set show_brackets; *}
ML {* val vc = vcg prog; *}
ML {* val pvc = (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_form vc))); *}
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 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 (Suc 0)))) \<oplus> C (NAT (Suc (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> [((C (NAT (Suc (Suc (Suc 0)))) \<oplus> C (NAT (Suc (Suc (Suc 0))))) \<oplus> C (NAT (Suc (Suc (Suc 0)))) \<oplus> C (NAT (Suc (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 (Suc 0))) \<doteq> C (POS (0, Suc (Suc 0)))) \<supset> \<Lambda> [T, ((C (NAT (Suc (Suc (Suc 0)))) \<oplus> C (NAT (Suc (Suc (Suc 0))))) \<oplus> C (NAT (Suc (Suc (Suc 0)))) \<oplus> C (NAT (Suc (Suc (Suc 0))))) \<doteq> C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))]]]], \<Lambda> [\<Lambda> [\<Lambda> [T, V (Suc 0) \<doteq> C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))], Pc \<doteq> C (POS (0, Suc (Suc (Suc 0))))] \<supset> \<Lambda> [T, V (Suc 0) \<doteq> C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))]]]"

text {* The vc optimiser reduces this formula to T, so the proof becomes trivial *}

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

subsection {* Program Verification *}

text {* In this section we prove the vc (without optimisation) *}

text {* First, we check the program's wellformedness. *}

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. One simplifier call with definitions
of functions used in vc suffices. *}

lemma vc_prog_holds: "prog \<turnstile> vc"
apply (unfold provable_def)
apply (rule HOLprf)
apply (simp add: valid_def vc_def Let_def split_def fst_conv snd_conv id_lookup_def lift_def nv_def)
--{* nprfsize() = 4553 *}
done

text {* In the proof above we instantly shift to HOL by using the rule HOLprf. Instead we can also do large
parts of the proof inside our proof calculus and shift to HOL eventually. This technique results in
smaller proof objects, because we make less use of the simplifier. The simplifier produces extra load 
due to rewrites that are not necessary. For example it also simplifies assumptions that are not required for
a proof. *}

lemma vc_prog_holds_man: "prog \<turnstile> vc"
apply (unfold provable_def)
apply (unfold vc_def)
apply (rule AndI)
apply (rule AndSingle)
apply (rule AndSingle)
apply (rule ImpI)
apply (rule FlattenAsm)
apply (rule Asm)
apply simp
apply (rule ImpI)
apply (rule AndI)
apply (rule AndSingle)
apply (rule FlattenAsm)
apply (rule ImpI)
apply (rule AndI)
apply (rule AndSingle)
apply (rule ImpI)
apply (rule AndI)
apply (rule AndSingle)
apply (rule ImpI)
apply (rule AndI)
apply (rule AndSingle)
apply (rule HOLprf)
apply (rule ballI)
apply (simp (no_asm) add: valid_def validF_validFs.simps lift_def) 
apply (rule HOLprf)
apply (rule ballI)
apply (simp (no_asm) add: valid_def validF_validFs.simps lift_def) 
apply (rule HOLprf)
apply (rule ballI)
apply (simp (no_asm) add: valid_def validF_validFs.simps lift_def nv_def) 
apply (rule HOLprf)
apply (rule ballI)
apply (simp (no_asm) add: valid_def validF_validFs.simps lift_def nv_def) 
apply (rule HOLprf)
apply (rule ballI)
apply (simp (no_asm) add: valid_def validF_validFs.simps lift_def nv_def) 
(* nprfsize = 4555 *)
done

lemma vc_prog_holds_explict_rules: "prog \<turnstile> vc"
apply (unfold vc_def provable_def)
apply (safe intro!: AndI ImpI And0 FlattenAsm FlattenAsmSingle| simp only: append_Cons append_Nil)+
apply (rule HOLprf, simp add: valid_def vc_def Let_def split_def fst_conv snd_conv id_lookup_def lift_def nv_def)+
(* nprfsize = 7183 *)
done

end