Theory Program_Graph

theory Program_Graph imports Labeled_Transition_Systems.LTS Datalog begin


section ‹Actions›

datatype (fv_arith: 'v) arith =
  Integer int
  | Arith_Var 'v
  | Arith_Op "'v arith" "int ⇒ int ⇒ int" "'v arith"
  | Minus "'v arith"

datatype (fv_boolean: 'v) boolean =
  true
  | false
  | Rel_Op "'v arith" "int ⇒ int ⇒ bool" "'v arith"
  | Bool_Op "'v boolean" "bool ⇒ bool ⇒ bool" "'v boolean"
  | Neg "'v boolean"

datatype 'v action =
  Asg 'v "'v arith" ("_ ::= _" [1000, 61] 61)
  | Bool "'v boolean"
  | Skip


section ‹Memories›

type_synonym 'v memory = "'v ⇒ int"


section ‹Semantics›

fun sem_arith :: "'v arith ⇒ 'v memory ⇒ int" where
  "sem_arith (Integer n) σ = n"
| "sem_arith (Arith_Var x) σ = σ x"
| "sem_arith (Arith_Op a1 op a2) σ = op (sem_arith a1 σ) (sem_arith a2 σ)"
| "sem_arith (Minus a) σ = - (sem_arith a σ)"

fun sem_bool :: "'v boolean ⇒ 'v memory ⇒ bool" where
  "sem_bool true σ = True"
| "sem_bool false σ = False"
| "sem_bool (Rel_Op a1 op a2) σ = op (sem_arith a1 σ) (sem_arith a2 σ)"
| "sem_bool (Bool_Op b1 op b2) σ = op (sem_bool b1 σ) (sem_bool b2 σ)"
| "sem_bool (Neg b) σ = (¬(sem_bool b σ))"

fun sem_action :: "'v action ⇒ 'v memory ⇀ 'v memory" where
  "sem_action (x ::= a) σ = Some (σ(x := sem_arith a σ))"
| "sem_action (Bool b) σ = (if sem_bool b σ then Some σ else None)"
| "sem_action Skip σ = Some σ"


section ‹Program Graphs›


subsection ‹Types›

type_synonym ('n,'a) edge = "'n × 'a × 'n"

type_synonym ('n,'a) program_graph = "('n,'a) edge set × 'n × 'n"

type_synonym ('n,'v) config = "'n * 'v memory"


subsection ‹Program Graph Locale›

locale program_graph = 
  fixes pg :: "('n,'a) program_graph"
begin

definition edges where 
  "edges = fst pg"

definition start where
  "start = fst (snd pg)"

definition "end" where
  "end = snd (snd pg)"

definition pg_rev :: "('n,'a) program_graph" where
  "pg_rev = (rev_edge ` edges, end, start)"

end

subsection ‹Finite Program Graph Locale›

locale finite_program_graph = program_graph pg
  for pg :: "('n::finite,'v) program_graph" +
  assumes "finite edges"
begin

lemma finite_pg_rev: "finite (fst pg_rev)"
  by (metis finite_program_graph_axioms finite_program_graph_def finite_imageI fst_conv pg_rev_def)

end

locale finite_action_program_graph = 
  fixes pg :: "('n,'v action) program_graph"
begin

interpretation program_graph pg .

― ‹Execution Sequences:›

fun initial_config_of :: "('n,'v) config ⇒ bool" where
  "initial_config_of (q,σ) ⟷ q = start"

fun final_config_of :: "('n,'v) config ⇒ bool" where
  "final_config_of (q,σ) ⟷ q = end"

inductive exe_step :: "('n,'v) config ⇒ 'v action ⇒ ('n,'v) config ⇒ bool" where
  "(q1, α, q2) ∈ edges ⟹ sem_action α σ = Some σ' ⟹ exe_step (q1,σ) α (q2,σ')"

end


end