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