header {* 
  \isaheader{Safety Logic} 
*}

theory SafetyLogic = Main:

text {* The Safety Logic defines how to formulate and prove safety properties of programs. In order to use this framework one needs to come up with a formula language and judgements for provability and validity of formulas. *}

locale SafetyLogic =
fixes TrueF:: "'form" ("\<TrueF>")
fixes FalseF:: "'form" ("\<FalseF>")
fixes Conj:: "'form list \<Rightarrow> 'form" ("\<Conj>_" [70]) 
fixes Impl:: "'form \<Rightarrow> 'form \<Rightarrow> 'form" ("_ \<Impl> _" [61,60] 60) 
fixes valid:: "'prog \<Rightarrow> ('pos \<times> 'mem) \<Rightarrow> 'form \<Rightarrow> bool" ("(_,_ \<Turnstile> _)" [61,61,60] 60)
fixes provable :: "'prog \<Rightarrow> 'form \<Rightarrow> bool" ("(_ \<turnstile> _)" [61,60] 60)
assumes semConj: " \<Pi>,s \<Turnstile> \<Conj> L = (\<forall>f\<in>set L. \<Pi>,s \<Turnstile> f)"
assumes semImpE: " \<Pi>,s \<Turnstile> (f1 \<Impl> f2) \<Longrightarrow>  (\<Pi>,s \<Turnstile> f1 \<longrightarrow> \<Pi>,s \<Turnstile> f2)"
assumes semTrue: "\<Pi>,s \<Turnstile> \<TrueF>"
assumes semFalse: "\<not> (\<Pi>,s \<Turnstile> \<FalseF>)"

(*<*)
lemma (in SafetyLogic)  semConjE: 
"\<lbrakk>  \<Pi>,s \<Turnstile> Conj L; f\<in>set L \<rbrakk> \<Longrightarrow> \<Pi> ,s \<Turnstile> f"
by (simp add: semConj)

lemma (in SafetyLogic)  semConjI: 
"\<lbrakk> \<Pi> ,s \<Turnstile> A; \<Pi> ,s \<Turnstile> B \<rbrakk> \<Longrightarrow> \<Pi> ,s \<Turnstile>  Conj [A,B]"
by (simp add: semConj)

lemma (in SafetyLogic) semConjIM: 
"\<lbrakk> \<forall> f\<in> set l. \<Pi> ,s \<Turnstile> f \<rbrakk> \<Longrightarrow> \<Pi>,s \<Turnstile> Conj l"
by (simp add: semConj)

lemma (in SafetyLogic) semMP: 
"\<lbrakk> \<Pi> ,s \<Turnstile> Impl A B; \<Pi> ,s \<Turnstile> A\<rbrakk> \<Longrightarrow> \<Pi> ,s \<Turnstile>  B"
by (drule_tac ?f2.0="B" in semImpE,simp)

lemma (in SafetyLogic) ImplEq:
"\<lbrakk> A = A'; B = B' \<rbrakk> \<Longrightarrow> (Impl A B) = (Impl A' B')"
by auto

lemma (in SafetyLogic) ConjEq:
"\<lbrakk> l1 = l2 \<rbrakk> \<Longrightarrow> (Conj l1 = Conj l2)"
by auto
(*>*)

end