MinimalExample.thy

theory MinimalExample
imports Main "~~/src/HOL/Library/FSet" Map
begin

section {* Threads and Executions *}

text {* Every thread has a unique identifier *}

datatype ThreadId = UserThread nat

text {* An execution trace (currently) is just a list of the scheduling
decisions made and the threads runnable at each step. *}

type_synonym Trace = "(ThreadId * ThreadId fset) list"

text {* A well-formed Trace value has, at all steps, the thread which
ran next in the runnable set. *}

fun
  trace_well_formed :: "Trace ⇒ bool"
where
  "trace_well_formed [] = True" |

  "trace_well_formed ((t, run) # rest) =
    (t |∈| run ∧ trace_well_formed rest)"

section {* Partial-order Reduction *}

text {* POR runnable todo done *}

datatype POR = POR "ThreadId fset" "ThreadId fset" "ThreadId ⇀ POR"

text {* A well-formed POR value has the todo and domain of the
done as disjoint subsets of runnable, and no thread is both in the
todo list and done function. *}

definition por_well_formed
where
  "por_well_formed = rec_POR (λrunnable todo done.
     todo |⊆| runnable
   ∧ dom done ⊆ fset runnable
   ∧ fset todo ∩ dom done = {}
   ∧ (∀ p ∈ ran done. snd p))"

lemma por_well_formed_simps:
  "por_well_formed (POR runnable todo done) ⟷
   ( todo |⊆| runnable
   ∧ dom done ⊆ fset runnable
   ∧ fset todo ∩ dom done = {})
   ∧ (∀ p ∈ ran done. por_well_formed p)"
  unfolding por_well_formed_def by (simp add: dom_map_option ran_map_option o_def)

text {* A Trace agrees with a POR value if they agree on runnable threads
everywhere up until the end of the Trace, and the Trace is at least as
long as the POR. *}

fun
  trace_por_agree :: "Trace ⇒ POR ⇒ bool"
where
  "trace_por_agree [] (POR _ _ _) = False" |

  "trace_por_agree [(_, run)] (POR runnable _ done) =
    (run |⊆| runnable ∧ done = empty)" |

  "trace_por_agree ((t, run) # rest) (POR runnable todo done) =
    ( run |⊆| runnable
    ∧ (∃ p. done t = Some p ⟶ trace_por_agree rest p))"

lemma terminal_por_well_formed [simp]: "todo |⊆| run ⟶ por_well_formed (POR run todo empty)"
by (simp add: por_well_formed_def)

lemma terminal_por_well_formed2 [simp]: "por_well_formed (POR run todo empty) ⟶ todo |⊆| run"
by (simp add: por_well_formed_def)

text {* Once an execution has been performed, the POR state needs to be
extended with additional information *}

fun
  por_from :: "Trace ⇒ POR"
where
  "por_from [] = undefined" |

  "por_from [(_, run)] = POR run {||} empty" |

  "por_from ((t, run) # rest) =
    POR run {||} (map_of [(t, por_from rest)])"

lemma por_from_well_formed:
  assumes "trace ≠ []"
  assumes "trace_well_formed trace"
  shows   "por_well_formed (por_from trace)"
using assms
proof (induct trace rule: list_nonempty_induct)
  case (single x) thus ?case
    by (cases x, simp)
next
  case (cons x xs) thus ?case
  proof (induct xs rule: list_nonempty_induct)
    case (single y) thus ?case
      by (cases x, cases y, simp add: por_well_formed_simps fmember.rep_eq)
  next
    case (cons y ys) thus ?case
      by (cases x, cases y, simp add: por_well_formed_simps fmember.rep_eq)
  qed
qed

fun
  por_from_helper :: "Trace ⇒ POR option"
where
  "por_from_helper [] = None" |
  "por_from_helper ts = Some (por_from ts)"

lemma por_from_helper_well_formed:
  assumes "trace_well_formed trace"
  shows "(por_from_helper trace = Some p) ⟶ por_well_formed p"
using assms por_from_helper.elims por_from_well_formed by auto

lemma por_from_helper_empty:
  shows "por_from_helper trace = None ⟷ trace = []"
using por_from_helper.elims by auto

fun
  grow_por :: "POR ⇒ Trace ⇒ POR"
where
  "grow_por (POR runnable todo done) ((t, run) # ts) =
    (case done t of
      Some p ⇒ POR runnable todo (done (t ↦ grow_por p ts)) |
      None   ⇒ POR runnable (todo |-| {| t |}) (done (t := por_from_helper ts)))" |
  "grow_por por _ = por"

lemma grow_por_well_formed:
  assumes "por_well_formed   por"
  assumes "trace_well_formed trace"
  assumes "trace_por_agree trace por"
  shows "por_well_formed (grow_por por trace)"
using assms
proof (induct trace)
  case Nil thus ?case
    by simp
next
  case (Cons x xs)
    obtain t run where "x = (t, run)" by (cases x)
    obtain runnable todo dne where "por = POR runnable todo dne" by (cases por)
    thus ?case
    proof (cases "dne t")
      case (Some p)
        obtain newPor  where "newPor = grow_por p xs" by simp
        obtain newDone where "newDone = dne (t ↦ newPor)" by simp
        have "por_well_formed p" by (metis Some `por = POR runnable todo dne` assms(1) por_well_formed_simps ranI)

        have TR: "todo |⊆| runnable"
        proof-
          show ?thesis by (metis `por = POR runnable todo dne` assms(1) por_well_formed_simps)
        qed

        have DR: "dom newDone ⊆ fset runnable"
        proof-
          show ?thesis by (metis Some `newDone = dne(t ↦ newPor)` `por = POR runnable todo dne` assms(1) dom_fun_upd insert_dom option.distinct(1) por_well_formed_simps)
        qed

        have TD: "fset todo ∩ dom newDone = {}"
        proof-
          show ?thesis by (metis Some `newDone = dne(t ↦ newPor)` `por = POR runnable todo dne` assms(1) dom_fun_upd insert_dom option.distinct(1) por_well_formed_simps)
        qed

        have P: "∀ p ∈ ran newDone. por_well_formed p"
        proof-
(* I can't figure out how to prove this. I feel like it should
be an induction hypothesis, but I'm inducting over trace,
not por. *)
          have "por_well_formed newPor" sorry

          hence "∀ p ∈ ran dne. por_well_formed p" by (metis `por = POR runnable todo dne` assms(1) por_well_formed_simps)
          hence "∀ p. newDone a = Some p ⟹ a = t ∨ p ∈ ran dne" by (meson Some ranI) 
          hence "∀ p. newDone a = Some p ⟹ por_well_formed p" by (metis (full_types) assms(1) option.sel)

(* This is a big scary sledgehammer-generated proof. I don't see
why this case is so different to the None case, which is way
simpler. *)
          thus ?thesis
proof -
  obtain keyOf :: "POR ⇒ (ThreadId ⇀ POR) ⇒ ThreadId" where
    "∀v m. (∃k. m k = Some v) = (m (keyOf v m) = Some v)"
    by moura
  hence f1: "(¬ (∃ta. newDone ta = Some p) ∨ newDone (keyOf p newDone) = Some p) ∧ ((∃ta. newDone ta = Some p) ∨ (∀ta. newDone ta ≠ Some p))"
    by blast
  obtain badPOR :: POR where
    "(∃p. p ∈ ran newDone ∧ ¬ por_well_formed p) = (badPOR ∈ ran newDone ∧ ¬ por_well_formed badPOR)"
    by moura
  moreover
  { assume "keyOf badPOR newDone ≠ t ∨ newPor ≠ badPOR"
    moreover
    { assume "(keyOf badPOR newDone ≠ t ∨ newPor ≠ badPOR) ∧ (keyOf badPOR newDone = t ∨ dne (keyOf badPOR newDone) ≠ Some badPOR)"
      hence "newDone (keyOf badPOR newDone) ≠ Some badPOR"
        using `newDone = dne(t ↦ newPor)` by auto
      hence "badPOR ∉ ran newDone ∨ por_well_formed badPOR"
        using f1
proof -
  have f1: "{p. ∃ta. newDone ta = Some p} = ran newDone"
    by (simp add: `newDone = dne(t ↦ newPor)` ran_def)
  have "¬ (∃ta. newDone ta = Some badPOR)"
    using `newDone (keyOf badPOR newDone) ≠ Some badPOR` `∀x0 x1. (∃v2. x1 v2 = Some x0) = (x1 (keyOf x0 x1) = Some x0)` by presburger
  thus ?thesis
    using f1 by blast
qed  }
    moreover
    { assume "∃t. dne t = Some badPOR"
      hence "badPOR ∈ ran dne"
        by (simp add: ran_def)
      hence "badPOR ∉ ran newDone ∨ por_well_formed badPOR"
        by (simp add: `∀p∈ran dne. por_well_formed p`) }
    ultimately have "badPOR ∉ ran newDone ∨ por_well_formed badPOR"
      by blast }
  ultimately show ?thesis
    using `por_well_formed newPor` by blast
qed 
        qed

        have "?thesis = por_well_formed (POR runnable todo newDone)" by (simp add: Some `newDone = dne(t ↦ newPor)` `newPor = grow_por p xs` `por = POR runnable todo dne` `x = (t, run)`)
        thus ?thesis using TR DR TD P by (simp add: TR `por_well_formed (grow_por por (x # xs)) = por_well_formed (POR runnable todo newDone)` por_well_formed_simps)
    next
      case None
        obtain newTodo where "newTodo = todo |-| {|t|}" by simp
        obtain newPor  where "newPor = por_from_helper xs" by simp
        obtain newDone where "newDone = dne (t := newPor)" by simp

        have TR: "newTodo  |⊆| runnable"
        proof-
          show ?thesis by (metis `newTodo = todo |-| {|t|}` `por = POR runnable todo dne` assms(1) fminus_fsubset order.trans por_well_formed_simps)
        qed

        have DR: "dom newDone ⊆ fset runnable"
        proof-
          have "t |∈| runnable" by (metis Cons.prems(2) Cons.prems(3) `por = POR runnable todo dne` `x = (t, run)` fset_rev_mp trace_por_agree.simps(2) trace_por_agree.simps(3) trace_well_formed.elims(2) trace_well_formed.simps(2))
          thus ?thesis by (metis (full_types) `newDone = dne(t := newPor)` `por = POR runnable todo dne` assms(1) contra_subsetD domIff fun_upd_other notin_fset por_well_formed_simps subsetI)
        qed

        have TD: "fset newTodo ∩ dom newDone = {}"
        proof-
          have "fset todo ∩ dom dne = {}" using `por = POR runnable todo dne` assms(1) por_well_formed_simps by blast
          thus ?thesis using `newDone = dne(t := newPor)` `newTodo = todo |-| {|t|}` by fastforce
        qed

        have P: "∀ p ∈ ran newDone. por_well_formed p"
        proof-
          have P1: "newPor = None   ⟶ newDone = dne" using None `newDone = dne(t := newPor)` by auto
          have P2: "newPor = Some p ⟶ por_well_formed p" using Cons.prems(2) `newPor = por_from_helper xs` `x = (t, run)` por_from_helper_well_formed by auto
          show ?thesis using P1 P2 by (metis Cons.prems(2) None `newDone = dne(t := newPor)` `newPor = por_from_helper xs` `por = POR runnable todo dne` `x = (t, run)` assms(1) insertE por_from_helper.elims por_from_helper_empty por_from_well_formed por_well_formed_simps ran_map_upd trace_well_formed.simps(2))
        qed

        have "?thesis = por_well_formed (POR runnable newTodo newDone)" by (simp add: None `newDone = dne(t := newPor)` `newPor = por_from_helper xs` `newTodo = todo |-| {|t|}` `por = POR runnable todo dne` `x = (t, run)`)
        thus ?thesis using TR DR TD P by (simp add: TR `por_well_formed (grow_por por (x # xs)) = por_well_formed (POR runnable newTodo newDone)` por_well_formed_simps)
    qed
qed

end