Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Channel.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.