Theory Data

section ‹Data›

text ‹This theory defines the data types and notations, and some preliminary results about them.›

theory Data
  imports Main
begin

subsection ‹Function notations›

abbreviation ε :: "'a ⇀ 'b" where
  "ε ≡ λx. None"

fun combine :: "('a ⇀ 'b) ⇒ ('a  ⇀ 'b) ⇒ ('a ⇀ 'b)" (‹_;;_› 20) where
  "(f ;; g) x = (if g x = None then f x else g x)"

lemma dom_combination_dom_union: "dom (τ;;τ') = dom τ ∪ dom τ'"
  by auto

subsection ‹Values, expressions and execution contexts›

datatype const = Unit | F | T

datatype (RIDV: 'r, LIDV: 'l,'v) val = 
  CV const
| Var 'v
| Loc 'l
| Rid 'r
| Lambda 'v "('r,'l,'v) expr"
and (RIDE: 'r, LIDE: 'l,'v) expr =
  VE "('r,'l,'v) val"
| Apply "('r,'l,'v) expr" "('r,'l,'v) expr"
| Ite "('r,'l,'v) expr" "('r,'l,'v) expr" "('r,'l,'v) expr"
| Ref "('r,'l,'v) expr"
| Read "('r,'l,'v) expr"
| Assign "('r,'l,'v) expr" "('r,'l,'v) expr"
| Rfork "('r,'l,'v) expr"
| Rjoin "('r,'l,'v) expr"

datatype (RIDC: 'r, LIDC: 'l,'v) cntxt = 
  Hole (‹□›)
| ApplyLℰ "('r,'l,'v) cntxt" "('r,'l,'v) expr" 
| ApplyRℰ "('r,'l,'v) val" "('r,'l,'v) cntxt"
| Iteℰ "('r,'l,'v) cntxt" "('r,'l,'v) expr" "('r,'l,'v) expr"
| Refℰ "('r,'l,'v) cntxt"
| Readℰ "('r,'l,'v) cntxt"
| AssignLℰ "('r,'l,'v) cntxt" "('r,'l,'v) expr"
| AssignRℰ 'l "('r,'l,'v) cntxt"
| Rjoinℰ "('r,'l,'v) cntxt"

subsection ‹Plugging and decomposing›

fun plug :: "('r,'l,'v) cntxt ⇒ ('r,'l,'v) expr ⇒ ('r,'l,'v) expr" (infix ‹⊲› 60) where
  "□ ⊲ e = e"
| "ApplyLℰ ℰ e1 ⊲ e = Apply (ℰ ⊲ e) e1"
| "ApplyRℰ val ℰ ⊲ e = Apply (VE val) (ℰ ⊲ e)"
| "Iteℰ ℰ e1 e2 ⊲ e = Ite (ℰ ⊲ e) e1 e2"
| "Refℰ ℰ ⊲ e = Ref (ℰ ⊲ e)"
| "Readℰ ℰ ⊲ e = Read (ℰ ⊲ e)"
| "AssignLℰ ℰ e1 ⊲ e = Assign (ℰ ⊲ e) e1"
| "AssignRℰ l ℰ ⊲ e = Assign (VE (Loc l)) (ℰ ⊲ e)"
| "Rjoinℰ ℰ ⊲ e = Rjoin (ℰ ⊲ e)"

translations
  "ℰ[x]" ⇌ "ℰ ⊲ x"

lemma injective_cntxt [simp]: "(ℰ[e1] = ℰ[e2]) = (e1 = e2)" by (induction ℰ) auto

lemma VE_empty_cntxt [simp]: "(VE v = ℰ[e]) = (ℰ = □ ∧ VE v = e)" by (cases ℰ, auto) 

inductive redex :: "('r,'l,'v) expr ⇒ bool" where
  app: "redex (Apply (VE (Lambda x e)) (VE v))"
| iteTrue: "redex (Ite (VE (CV T)) e1 e2)"
| iteFalse: "redex (Ite (VE (CV F)) e1 e2)"
| ref: "redex (Ref (VE v))"
| read: "redex (Read (VE (Loc l)))"
| assign: "redex (Assign (VE (Loc l)) (VE v))"
| rfork: "redex (Rfork e)"
| rjoin: "redex (Rjoin (VE (Rid r)))"

inductive_simps redex_simps [simp]: "redex e"
inductive_cases redexE [elim]: "redex e"

lemma plugged_redex_not_val [simp]: "redex r ⟹ (ℰ ⊲ r) ≠ (VE t)" by (cases ℰ) auto

inductive decompose :: "('r,'l,'v) expr ⇒ ('r,'l,'v) cntxt ⇒ ('r,'l,'v) expr ⇒ bool" where
  top_redex: "redex e ⟹ decompose e □ e"
| lapply: "⟦ ¬redex (Apply e1 e2); decompose e1 ℰ r ⟧ ⟹ decompose (Apply e1 e2) (ApplyLℰ ℰ e2) r"
| rapply: "⟦ ¬redex (Apply (VE v) e); decompose e ℰ r ⟧ ⟹ decompose (Apply (VE v) e) (ApplyRℰ v ℰ) r"
| ite: "⟦ ¬redex (Ite e1 e2 e3); decompose e1 ℰ r ⟧ ⟹ decompose (Ite e1 e2 e3) (Iteℰ ℰ e2 e3) r"
| ref: "⟦ ¬redex (Ref e); decompose e ℰ r ⟧ ⟹ decompose (Ref e) (Refℰ ℰ) r"
| read: "⟦ ¬redex (Read e); decompose e ℰ r ⟧ ⟹ decompose (Read e) (Readℰ ℰ) r"
| lassign: "⟦ ¬redex (Assign e1 e2); decompose e1 ℰ r ⟧ ⟹ decompose (Assign e1 e2) (AssignLℰ ℰ e2) r"
| rassign: "⟦ ¬redex (Assign (VE (Loc l)) e2); decompose e2 ℰ r ⟧ ⟹ decompose (Assign (VE (Loc l)) e2) (AssignRℰ l ℰ) r"
| rjoin:  "⟦ ¬redex (Rjoin e); decompose e ℰ r ⟧ ⟹ decompose (Rjoin e) (Rjoinℰ ℰ) r"

inductive_cases decomposeE [elim]: "decompose e ℰ r"

lemma plug_decomposition_equivalence: "redex r ⟹ decompose e ℰ r = (ℰ[r] = e)"
proof (rule iffI)
  assume x: "decompose e ℰ r"
  show "ℰ[r] = e" 
  proof (use x in ‹induct rule: decompose.induct›)
    case (top_redex e)
    thus "□[e] = e" by simp
  next
    case (lapply e1 e2 ℰ r)
    have "(ApplyLℰ ℰ e2) [r] = Apply (ℰ[r]) e2" by simp
    also have "... = Apply e1 e2" using ‹ℰ[r] = e1› by simp
    then show ?case by simp
  qed simp+
next
  assume red: "redex r" and  eq: "ℰ[r] = e"
  have "decompose (ℰ[r]) ℰ r" by (induct ℰ) (use red in ‹auto intro: decompose.intros›)
  thus "decompose e ℰ r" by (simp add: eq)
qed

lemma unique_decomposition: "decompose e ℰ1 r1 ⟹ decompose e ℰ2 r2 ⟹ ℰ1 = ℰ2 ∧ r1 = r2"
  by (induct arbitrary: ℰ2 rule: decompose.induct) auto

lemma completion_eq [simp]:
  assumes
    red_e: "redex r" and
    red_e': "redex r'"
  shows "(ℰ[r] = ℰ'[r']) = (ℰ = ℰ' ∧ r = r')"
proof (rule iffI)
  show "ℰ[r] = ℰ'[r'] ⟹ ℰ = ℰ' ∧ r = r'"
  proof (rule conjI)
    assume eq: "ℰ[r] = ℰ'[r']"
    have "decompose (ℰ[r]) ℰ r" using plug_decomposition_equivalence red_e by blast
    hence fst_decomp:"decompose (ℰ'[r']) ℰ r" by (simp add: eq)
    have snd_decomp: "decompose (ℰ'[r']) ℰ' r'" using plug_decomposition_equivalence red_e' by blast
    show cntxts_eq: "ℰ = ℰ'" using fst_decomp snd_decomp unique_decomposition by blast
    show "r = r'" using cntxts_eq eq by simp
  qed
qed simp

subsection ‹Stores and states›

type_synonym ('r,'l,'v) store = "'l ⇀ ('r,'l,'v) val"
type_synonym ('r,'l,'v) local_state = "('r,'l,'v) store × ('r,'l,'v) store × ('r,'l,'v) expr"
type_synonym ('r,'l,'v) global_state = "'r ⇀ ('r,'l,'v) local_state"

fun doms :: "('r,'l,'v) local_state ⇒ 'l set" where
  "doms (σ,τ,e) = dom σ ∪ dom τ"

fun LID_snapshot :: "('r,'l,'v) local_state ⇒ ('r,'l,'v) store" (‹_σ› 200) where
  "LID_snapshot (σ,τ,e) = σ"

fun LID_local_store :: "('r,'l,'v) local_state ⇒ ('r,'l,'v) store" (‹_τ› 200) where
  "LID_local_store (σ,τ,e) = τ"

fun LID_expression :: "('r,'l,'v) local_state ⇒ ('r,'l,'v) expr" (‹_e› 200) where
  "LID_expression (σ,τ,e) = e"

end