SSL Channel.thy

(*  Title:      HOL/UNITY/Simple/Channel.thy
  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

type_synonym state = "nat set"

consts
  F :: "state program"

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

axiomatization where

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

  (*  UC1  "F \<in> {s. minSet s = x} co {s. x \<subseteq> 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: if_split_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