Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: TimerArray.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/UNITY/Comp/TimerArray.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

A trivial example of reasoning about an array of processes
*)

theory TimerArray imports "../UNITY_Main" begin

type_synonym 'a state = "nat * 'a" (*second component allows new variables*)

definition count :: "'a state => nat"
  where "count s = fst s"

definition decr  :: "('a state * 'a state) set"
  where "decr = (UN n uu. {((Suc n, uu), (n,uu))})"

definition Timer :: "'a state program"
  where "Timer = mk_total_program (UNIV, {decr}, UNIV)"

declare Timer_def [THEN def_prg_Init, simp]

declare count_def [simp] decr_def [simp]

(*Demonstrates induction, but not used in the following proof*)
lemma Timer_leadsTo_zero: "Timer \ UNIV leadsTo {s. count s = 0}"
apply (rule_tac f = count in lessThan_induct, simp)
apply (case_tac "m")
apply (force intro!: subset_imp_leadsTo)
apply (unfold Timer_def, ensures_tac "decr")
done

lemma Timer_preserves_snd [iff]: "Timer \ preserves snd"
apply (rule preservesI)
apply (unfold Timer_def, safety)
done

declare PLam_stable [simp]

lemma TimerArray_leadsTo_zero:
     "finite I
      \<Longrightarrow> (plam i: I. Timer) \<in> UNIV leadsTo {(s,uu). \<forall>i\<in>I. s i = 0}"
apply (erule_tac A'1 = "\i. lift_set i ({0} \ UNIV)"
       in finite_stable_completion [THEN leadsTo_weaken])
apply auto
(*Safety property, already reduced to the single Timer case*)
prefer 2
apply (simp add: Timer_def, safety)
(*Progress property for the array of Timers*)
apply (rule_tac f = "sub i o fst" in lessThan_induct)
apply (case_tac "m")
(*Annoying need to massage the conditions to have the form (... \<times> UNIV)*)
apply (auto intro: subset_imp_leadsTo
        simp add: insert_absorb
                  lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric]
               Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
apply (rename_tac "n")
apply (rule PLam_leadsTo_Basis)
apply (auto simp add: lessThan_Suc [symmetric])
apply (unfold Timer_def mk_total_program_def, safety)
apply (rule_tac act = decr in totalize_transientI, auto)
done

end

¤ Dauer der Verarbeitung: 0.14 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.