Quelle Init.thy Sprache: Isabelle

(*  Title:      HOL/TLA/Init.thy
    Author:     Stephan Merz
    Copyright:  1998 University of Munich

Introduces type of temporal formulas.  Defines interface between
temporal formulas and its "subformulas" (state predicates and
actions).
*)

theory Init
imports Action
begin

typedecl behavior
instance behavior :: world ..

type_synonym temporal = "behavior form"

consts
  first_world :: "behavior \ ('w::world)"
  st1         :: "behavior \ state"
  st2         :: "behavior \ state"

definition Initial :: "('w::world \ bool) \ temporal"
  where Init_def: "Initial F sigma = F (first_world sigma)"

syntax
  "_TEMP"    :: "lift \ 'a" ($TEMP _)$
  "_Init"    :: "lift \ lift" (\(Init _)\[40] 50)
translations
  "TEMP F"   => "(F::behavior \ _)"
  "_Init"    == "CONST Initial"
  "sigma \ Init F" <= "_Init F sigma"

overloading
  fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
  fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
  fw_act \<equiv> "first_world :: behavior \<Rightarrow> state \<times> state"
begin

definition "first_world == \sigma. sigma"
definition "first_world == st1"
definition "first_world == \sigma. (st1 sigma, st2 sigma)"

end

lemma const_simps [int_rewrite, simp]:
  "\ (Init #True) = #True"
  "\ (Init #False) = #False"
  by (auto simp: Init_def)

lemma Init_simps1 [int_rewrite]:
  "\F. \ (Init \F) = (\ Init F)"
  "\ (Init (P \ Q)) = (Init P \ Init Q)"
  "\ (Init (P \ Q)) = (Init P \ Init Q)"
  "\ (Init (P \ Q)) = (Init P \ Init Q)"
  "\ (Init (P = Q)) = ((Init P) = (Init Q))"
  "\ (Init (\x. F x)) = (\x. (Init F x))"
  "\ (Init (\x. F x)) = (\x. (Init F x))"
  "\ (Init (\!x. F x)) = (\!x. (Init F x))"
  by (auto simp: Init_def)

lemma Init_stp_act: "\ (Init $P) = (Init P)"
  by (auto simp add: Init_def fw_act_def fw_stp_def)

lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]

lemma Init_temp: "\ (Init F) = F"
  by (auto simp add: Init_def fw_temp_def)

lemmas Init_simps = Init_temp [int_rewrite] Init_simps2

(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
lemma Init_stp: "(sigma \ Init P) = P (st1 sigma)"
  by (simp add: Init_def fw_stp_def)

lemma Init_act: "(sigma \ Init A) = A (st1 sigma, st2 sigma)"
  by (simp add: Init_def fw_act_def)

lemmas Init_defs = Init_stp Init_act Init_temp [int_use]

end

quality95%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.