theory SALTypeSafetyPlatform = VerificationConditionGenerator + SALSemantics:

section {*  SAL Safety Logic  *}

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

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

lemma [code]:
"provable prg f = term (provable (to_term prg) (to_term f))"
apply (simp add: term_def to_term_def)
done

constdefs
FalseF::"SALform"
"FalseF \<equiv> \<lambda> s. False"

lemma [code]:
"FalseF = term (\<lambda> s. False)"
apply (simp only: term_def FalseF_def)
done

constdefs
TrueF::"SALform"
"TrueF \<equiv> \<lambda> s. True"

lemma [code]:
"TrueF = term (\<lambda> s. True)"
apply (simp only: term_def TrueF_def)
done

constdefs
Conj::"SALform list \<Rightarrow> SALform"
"Conj fl \<equiv> \<lambda> s. \<forall> f\<in>set fl. f(s)"

constdefs
Impl::"SALform \<Rightarrow> SALform \<Rightarrow> SALform"
"Impl a b \<equiv> \<lambda> s. a(s) \<longrightarrow> b(s)"

(*<*)
lemma [code]:
"Conj [] = TrueF"
apply (unfold Conj_def)
apply simp
apply (fold TrueF_def)
by simp

lemma [code]:
"Conj (f#fl) = term (\<lambda> s.((to_term f) s \<and> (to_term (Conj fl)) s))"
apply (unfold Conj_def term_def to_term_def)
apply auto
done


lemma [code]:
"Impl a b = term (\<lambda> s. (to_term a) s \<longrightarrow> (to_term b) s)"
apply (unfold Impl_def term_def to_term_def)
apply auto
done
(*>*)

section {* Weakest Preconditions *}

constdefs
  wpF::"SALprogram \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> SALform \<Rightarrow> SALform"
 "wpF p i j Q \<equiv> case (cmd p i) of None \<Rightarrow> FalseF
  | Some ins \<Rightarrow> (case ins of
      SET x n \<Rightarrow> (\<lambda>(pc, m). Q (j, m[x \<mapsto> NAT n]))
    | ADD x y \<Rightarrow> (\<lambda>(pc, m). Q (j, m[x \<mapsto> lift (op +) (m x) (m y)]))
    | INC x  \<Rightarrow> (\<lambda>(pc, m). Q (j, m[x \<mapsto> lift (op +) (m x) (NAT 1)]))
    | JMPEQ x y t \<Rightarrow> (\<lambda>(pc, m). Q (j, m))
    | JMPB t \<Rightarrow> (\<lambda>(pc, m). Q (j, m)))"

lemma [code]:
 "wpF p i j Q = (case (cmd p i) of None \<Rightarrow> FalseF
  | Some ins \<Rightarrow> (case ins of
      SET x n \<Rightarrow> term (\<lambda>(pc, m). (to_term Q) (to_term j, m[(to_term x) \<mapsto> NAT (to_term n)]))
    | ADD x y \<Rightarrow> term (\<lambda>(pc, m). (to_term Q) (to_term j, m[(to_term x) \<mapsto> lift (op +) (m (to_term x)) (m (to_term y))]))
    | INC x  \<Rightarrow> term (\<lambda>(pc, m). (to_term Q) (to_term j, m[(to_term x) \<mapsto> lift (op +) (m (to_term x)) (NAT 1)]))
    | JMPEQ x y t \<Rightarrow> term (\<lambda>(pc, m). (to_term Q) (to_term j, m))
    | JMPB t \<Rightarrow> term (\<lambda>(pc, m). (to_term Q) (to_term j, m))))"
apply (simp only: wpF_def term_def to_term_def)
done

section {* Control Flow *}

constdefs
  succsF::"SALprogram \<Rightarrow> nat \<Rightarrow> (nat \<times> SALform) list"
 "succsF p i \<equiv>  case (cmd p i) of
    None \<Rightarrow> []
  | Some ins \<Rightarrow> (case ins of
      SET x n \<Rightarrow> [(i + 1, TrueF)]
    | ADD x y \<Rightarrow> [(i + 1, TrueF)]
    | INC x \<Rightarrow> [(i + 1, TrueF)]
    | JMPEQ x y t \<Rightarrow> [(i + t, \<lambda>(pc, m). m x = m y), (i + 1, \<lambda>(pc, m). m x \<noteq> m y)]
    | JMPB t \<Rightarrow> [(i - t, TrueF)])"

lemma [code]:
 "succsF p i = (case (cmd p i) of
    None \<Rightarrow> []
  | Some ins \<Rightarrow> (case ins of
      SET x n \<Rightarrow> [(i + 1, TrueF)]
    | ADD x y \<Rightarrow> [(i + 1, TrueF)]
    | INC x \<Rightarrow> [(i + 1, TrueF)]
    | JMPEQ x y t \<Rightarrow> [(i + t, term (\<lambda>(pc, m). (m (to_term x)) = (m (to_term y)))),
        (i + 1, term (\<lambda>(pc, m). (m (to_term x)) \<noteq> (m (to_term y))))]
    | JMPB t \<Rightarrow> [(i - t, TrueF)]))"
apply (simp only: succsF_def term_def to_term_def)
done

constdefs anF::"SALprogram \<Rightarrow> nat \<Rightarrow> (SALform option)"
"anF prg p \<equiv> snd (prg ! p)"

constdefs
  domA :: "SALprogram \<Rightarrow> nat list"
 "domA \<equiv> \<lambda> prg. [pc\<in> domC prg. (anF prg pc) \<noteq> None]"

constdefs 
ipc :: "SALprogram \<Rightarrow> nat"
"ipc prg \<equiv> 0"

section {* Safety Policy *}

constdefs 
  safeF::"SALprogram \<Rightarrow> nat \<Rightarrow> SALform"
 "safeF prg p \<equiv> (case (cmd prg p) of
    None \<Rightarrow> FalseF
  | Some a \<Rightarrow> (case a of
   SET X n \<Rightarrow> TrueF
  | ADD X Y \<Rightarrow> (\<lambda> (p,m). m X \<noteq> ILLEGAL \<and> m Y \<noteq> ILLEGAL)
  | INC X \<Rightarrow> (\<lambda> (p,m). m X \<noteq> ILLEGAL)
  | JMPEQ X Y t \<Rightarrow> TrueF
  | JMPB t \<Rightarrow> TrueF))"

lemma [code]:
 "safeF prg p = (case (cmd prg p) of
    None \<Rightarrow> FalseF
  | Some ins \<Rightarrow> (case ins of
   SET X n \<Rightarrow> TrueF
  | ADD X Y \<Rightarrow> term (\<lambda> (p,m). m (to_term X) \<noteq> ILLEGAL \<and> m (to_term Y) \<noteq> ILLEGAL)
  | INC X \<Rightarrow> term (\<lambda> (p,m). m (to_term X) \<noteq> ILLEGAL)
  | JMPEQ X Y t \<Rightarrow> TrueF
  | JMPB t \<Rightarrow> TrueF))"
apply (simp only: term_def to_term_def safeF_def)
done

constdefs initF:: "SALprogram \<Rightarrow> SALform"
"initF prg \<equiv> \<lambda> (p,m). p=0 \<and> (\<forall> X. m X = ILLEGAL)"

lemma [code]:
"initF prg = term ( \<lambda> (p,m). p=0 \<and> (\<forall> X. m X = ILLEGAL))"
apply (simp only: term_def to_term_def initF_def)
done

subsection {* Wellformedness Checker *}

consts
  checkPos :: "SALprogram \<Rightarrow> (nat list) \<Rightarrow> bool"

primrec
 "checkPos prg [] = True"
 "checkPos prg (p # ps) = (if ((case  (cmd prg p) of
    None \<Rightarrow> False
  | Some c \<Rightarrow> (case c of
      SET x n \<Rightarrow> True
    | ADD x y \<Rightarrow> True
    | INC x \<Rightarrow> True
    | JMPEQ x y t \<Rightarrow> (t = 0) \<longrightarrow> ((anF prg p) \<noteq> None)
    | JMPB  t \<Rightarrow> ((anF prg (p - t)) \<noteq> None)
 ))) 
  then (checkPos prg ps)
  else False)"

constdefs
  wf :: "SALprogram \<Rightarrow> bool" 
 "wf prg \<equiv> checkPos prg (domC prg)"


section {* Instantiating the VCG *}


constdefs
vcgTSAL:: "SALprogram \<Rightarrow> SALform"
"vcgTSAL prg \<equiv> vcG Conj Impl FalseF ipc initF safeF succsF wpF domC domA anF prg"

(*<*)
types_code
  set ("(_ -> bool)")

consts_code
  "op :" ("(_ |> _)")
  "Collect" ("(_)")


ML {* fun term_of_fun_type _ _ _ _= error "term_of_fun_type applied" *} 

ML {* fun term_of_bool  _ = error "term_of_bool applied" *} 

generate_code ("vcgTSAL.ML") [term_of]
    prov = "provable"
    vcg = "vcgTSAL"
(*>*)



ML {*
fun prf_size () =
  let
    val proof_state = Toplevel.proof_of (Toplevel.get_state ());
    val (_, (_, st)) = Proof.get_goal proof_state;
    val {der = (_, prf), ...} = rep_thm st
  in Proofterm.size_of_proof (prf)
  end;
*}

ML {*
fun nprf_size () =
  let
    val proof_state = Toplevel.proof_of (Toplevel.get_state ());
    val (_, (_, st)) = Proof.get_goal proof_state;
    val {der = (_, prf), ...} = rep_thm st
  in Proofterm.size_of_proof (Proofterm.rewrite_proof_notypes ([],
ProofRewriteRules.rprocs false) prf)
  end;
*}


end