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