1(*  Title:      HOL/UNITY/Simple/Channel.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4
5Unordered Channel
6
7From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
8*)
9
10theory Channel imports "../UNITY_Main" begin
11
12type_synonym state = "nat set"
13
14consts
15  F :: "state program"
16
17definition minSet :: "nat set => nat option" where
18    "minSet A == if A={} then None else Some (LEAST x. x \<in> A)"
19
20axiomatization where
21
22  UC1:  "F \<in> (minSet -` {Some x}) co (minSet -` (Some`atLeast x))" and
23
24  (*  UC1  "F \<in> {s. minSet s = x} co {s. x \<subseteq> minSet s}"  *)
25
26  UC2:  "F \<in> (minSet -` {Some x}) leadsTo {s. x \<notin> s}"
27
28
29(*None represents "infinity" while Some represents proper integers*)
30lemma minSet_eq_SomeD: "minSet A = Some x ==> x \<in> A"
31apply (unfold minSet_def)
32apply (simp split: if_split_asm)
33apply (fast intro: LeastI)
34done
35
36lemma minSet_empty [simp]: " minSet{} = None"
37by (unfold minSet_def, simp)
38
39lemma minSet_nonempty: "x \<in> A ==> minSet A = Some (LEAST x. x \<in> A)"
40by (unfold minSet_def, auto)
41
42lemma minSet_greaterThan:
43     "F \<in> (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))"
44apply (rule leadsTo_weaken)
45apply (rule_tac x1=x in psp [OF UC2 UC1], safe)
46apply (auto dest: minSet_eq_SomeD simp add: linorder_neq_iff)
47done
48
49(*The induction*)
50lemma Channel_progress_lemma:
51     "F \<in> (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))"
52apply (rule leadsTo_weaken_R)
53apply (rule_tac l = y and f = "the o minSet" and B = "{}" 
54       in greaterThan_bounded_induct, safe)
55apply (simp_all (no_asm_simp))
56apply (drule_tac [2] minSet_nonempty)
57 prefer 2 apply simp 
58apply (rule minSet_greaterThan [THEN leadsTo_weaken], safe)
59apply simp_all
60apply (drule minSet_nonempty, simp)
61done
62
63
64lemma Channel_progress: "!!y::nat. F \<in> (UNIV-{{}}) leadsTo {s. y \<notin> s}"
65apply (rule Channel_progress_lemma [THEN leadsTo_weaken_R], clarify)
66apply (frule minSet_nonempty)
67apply (auto dest: Suc_le_lessD not_less_Least)
68done
69
70end
71