Homework 6_1

Definitions File

theory Defs
  imports "HOL-IMP.AExp" "HOL-Library.List_Lexorder" "HOL-Library.Char_ord" "HOL-IMP.Star"
begin

declare [[names_short]]

datatype action = 
  Up vname  \<comment> \<open>Increment\<close>
  | Down vname \<comment> \<open>Decrement\<close>
  | Other     \<comment> \<open>Unrelated operation\<close>

type_synonym config = "action list \<times> action list \<times> state"

datatype label = P1 action | P2 action

fun well_formed_aux :: "vname set \<Rightarrow> action list \<Rightarrow> bool" where
  "well_formed_aux A (Down x#l) \<longleftrightarrow> well_formed_aux (insert x A) l \<and> (\<forall>y\<in>A. x>y)"
|  "well_formed_aux A (Up x#l) \<longleftrightarrow> well_formed_aux (A-{x}) l \<and> x\<in>A"
|  "well_formed_aux A (Other#l) \<longleftrightarrow> well_formed_aux A l"  
|  "well_formed_aux A [] \<longleftrightarrow> A={}"

abbreviation "well_formed l \<equiv> well_formed_aux {} l"

abbreviation init :: state where "init \<equiv> \<lambda>_. 1" \<comment> \<open>Initial state\<close>


consts exec :: "action \<Rightarrow> state \<Rightarrow> state \<Rightarrow> bool"

consts step :: "config \<Rightarrow> label \<Rightarrow> config \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

inductive exec :: "action \<Rightarrow> state \<Rightarrow> state \<Rightarrow> bool" 

type_synonym config = "action list \<times> action list \<times> state"

inductive step :: "config \<Rightarrow> label \<Rightarrow> config \<Rightarrow> bool" 

lemma step_shift:
    assumes "step c1 (P1 (Down x)) c2"
      and "step c2 (P2 a) c3"
  shows "\<exists>ch. step c1 (P2 a) ch \<and> step ch (P1 (Down x)) c3"
  sorry

fun final where "final ([],[],_) \<longleftrightarrow> True" | "final _ \<longleftrightarrow> False"
definition "deadlocked c \<equiv> \<not>final c \<and> (\<forall>c' a. \<not>step c a c')"
abbreviation "step' c c' \<equiv> \<exists>a. step c a c'"

theorem deadlock_freedom:
    assumes WF1: "well_formed l1"
      and WF2: "well_formed l2"
      and STEPS: "star step' (l1,l2,init) c'"
  shows "\<not>deadlocked c'"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma step_shift: "(step c1 (P1 (Down x)) c2) \<Longrightarrow> (step c2 (P2 a) c3) \<Longrightarrow> \<exists>ch. step c1 (P2 a) ch \<and> step ch (P1 (Down x)) c3"
  by (rule Submission.step_shift)

theorem deadlock_freedom: "(well_formed l1) \<Longrightarrow> (well_formed l2) \<Longrightarrow> (star step' (l1,l2,init) c') \<Longrightarrow> \<not>deadlocked c'"
  by (rule Submission.deadlock_freedom)

end