# Theory Channel

Up to index of Isabelle/HOL/UNITY

theory Channel
imports UNITY_Main
begin

    (*  Title:      HOL/UNITY/Channel
        ID:         $Id: Channel.thy,v 1.5 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

    Unordered Channel

    From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
    *)

    theory Channel imports UNITY_Main begin

    types state = "nat set"

    consts
      F :: "state program"

    constdefs
      minSet :: "nat set => nat option"
        "minSet A == if A={} then None else Some (LEAST x. x ∈ A)"

    axioms

      UC1:  "F ∈ (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"

      (*  UC1  "F ∈ {s. minSet s = x} co {s. x ⊆ minSet s}"  *)

      UC2:  "F ∈ (minSet -` {Some x}) leadsTo {s. x ∉ s}"

    (*None represents "infinity" while Some represents proper integers*)
    lemma minSet_eq_SomeD: "minSet A = Some x ==> x ∈ A"
    apply (unfold minSet_def)
    apply (simp split: split_if_asm)
    apply (fast intro: LeastI)
    done

    lemma minSet_empty [simp]: " minSet{} = None"
    by (unfold minSet_def, simp)

    lemma minSet_nonempty: "x ∈ A ==> minSet A = Some (LEAST x. x ∈ A)"
    by (unfold minSet_def, auto)

    lemma minSet_greaterThan:
         "F ∈ (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))"
    apply (rule leadsTo_weaken)
    apply (rule_tac x1=x in psp [OF UC2 UC1], safe)
    apply (auto dest: minSet_eq_SomeD simp add: linorder_neq_iff)
    done

    (*The induction*)
    lemma Channel_progress_lemma:
         "F ∈ (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))"
    apply (rule leadsTo_weaken_R)
    apply (rule_tac l = y and f = "the o minSet" and B = "{}"
           in greaterThan_bounded_induct, safe)
    apply (simp_all (no_asm_simp))
    apply (drule_tac [2] minSet_nonempty)
     prefer 2 apply simp
    apply (rule minSet_greaterThan [THEN leadsTo_weaken], safe)
    apply simp_all
    apply (drule minSet_nonempty, simp)
    done

    lemma Channel_progress: "!!y::nat. F ∈ (UNIV-{{}}) leadsTo {s. y ∉ s}"
    apply (rule Channel_progress_lemma [THEN leadsTo_weaken_R], clarify)
    apply (frule minSet_nonempty)
    apply (auto dest: Suc_le_lessD not_less_Least)
    done

    end

lemma minSet_eq_SomeD:

      minSet A = Some x ==> x ∈ A

lemma minSet_empty:

      minSet {} = None

lemma minSet_nonempty:

      x ∈ A ==> minSet A = Some (LEAST x. x ∈ A)

lemma minSet_greaterThan:

      F ∈ minSet -` {Some x} leadsTo minSet -` Some ` {x<..}

lemma Channel_progress_lemma:

      F ∈ UNIV - {{}} leadsTo minSet -` Some ` {y..}

lemma Channel_progress:

      F ∈ UNIV - {{}} leadsTo {s. y ∉ s}