header {* 
  \isaheader{Program Semantics} 
*}

theory Semantics = Main:

text {* Here we declare a framework for program semantics in form of a state transition relation. A state consists of
a position and a memory component. Note that we use type variables, hence one can instantiate programs, positions and
memories with arbitrary types.  *}

consts ReachableFrom:: "('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> 'a set"
inductive "ReachableFrom R S"
intros
init: "a \<in> S \<Longrightarrow> a \<in> ReachableFrom R S"
step: "a \<in> ReachableFrom R S \<Longrightarrow> (a,b) \<in> R \<Longrightarrow> b \<in> ReachableFrom R S"

consts ReachableFromInv:: "('a \<times> 'a) set \<Rightarrow> ('a set) \<Rightarrow> ('a set) \<Rightarrow> 'a set"
inductive "ReachableFromInv R S I"
intros
init: "a \<in> S \<Longrightarrow> a \<in> ReachableFromInv R S I"
step: "a \<in> ReachableFromInv R S I \<Longrightarrow> (a,b) \<in> R \<Longrightarrow> a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> b \<in> ReachableFromInv R S I"

locale Semantics =  

fixes initS:: "'prog \<Rightarrow> ('pos \<times> 'mem) set"
fixes effS:: " 'prog  \<Rightarrow> (('pos \<times> 'mem) \<times> ('pos \<times> 'mem)) set" 

fixes Reachables:: "'prog \<Rightarrow> ('pos \<times> 'mem) set"
defines
"Reachables \<equiv> \<lambda> \<Pi>. ReachableFrom (effS \<Pi>) (initS \<Pi>)"



lemma ReachableFromInv_ReachableFrom:
"s \<in> ReachableFromInv R S I \<Longrightarrow> s \<in> ReachableFrom R S" 
(*<*)
apply (erule ReachableFromInv.induct)
apply (rule ReachableFrom.init)
apply assumption

apply (rule ReachableFrom.step)
apply simp
apply simp
done
(*>*)

lemma ReachableFrom_conv:
"s \<in> ReachableFrom R S = (\<exists> s0. s0 \<in> S \<and> (s0,s) \<in> R\<^sup>*)"
(*<*)
apply (rule iffI)
-- {* if *}
apply (erule ReachableFrom.induct)
apply (rule_tac x="a" in exI)
apply simp

apply (erule exE | erule conjE)+
apply (rule_tac x="s0" in exI)
apply (rule conjI)
apply assumption

apply (rule_tac b="a" in rtrancl_into_rtrancl)
apply assumption
apply assumption

--{* only if *}
apply (erule exE | erule conjE)+
apply (erule rev_mp)
apply (erule  rtrancl.induct)
apply (rule impI)
apply (rule ReachableFrom.init)
apply assumption

apply (rule impI)
apply (drule mp, assumption)
apply (rule ReachableFrom.step)
apply assumption
apply assumption
done
(*>*)

lemma (in Semantics) Reachables_conv:
"Reachables \<Pi> = {s. \<exists> s0. s0 \<in> initS \<Pi> \<and> (s0,s) \<in> (effS \<Pi>)\<^sup>*}"
(*<*)
by (rule set_ext, simp only: mem_Collect_eq Reachables_def ReachableFrom_conv)
(*>*)

lemma (in Semantics) Reachables_induct [consumes 1, case_names init step]:
"\<lbrakk> x \<in> Reachables \<Pi>; \<And> s. s \<in> (initS \<Pi>) \<Longrightarrow> P s; \<And> s s'. \<lbrakk> s \<in> Reachables \<Pi>; P s; (s,s') \<in> (effS \<Pi>) \<rbrakk> \<Longrightarrow> P s' \<rbrakk> \<Longrightarrow> P x"
(*<*)
apply (rule_tac R="effS \<Pi>" and S="initS \<Pi>" in  ReachableFrom.induct)
apply (unfold Reachables_def)
apply assumption

apply atomize
apply (erule_tac x="a" in allE)+
apply simp

apply atomize
apply (erule_tac x="a" in allE)
apply (erule_tac x="a" in allE)
apply (erule_tac x="b" in allE)
apply simp
done
(*>*)

end