products/Sources/formale Sprachen/Coq/test-suite/bugs/closed/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: clock_shift.prf   Sprache: Isabelle

Original von: Isabelle©
(* Author: Tobias Nipkow *)

theory Def_Init_Big
imports Def_Init_Exp Def_Init
begin

subsection "Initialization-Sensitive Big Step Semantics"

inductive
  big_step :: "(com \ state option) \ state option \ bool" (infix "\" 55)
where
None: "(c,None) \ None" |
Skip: "(SKIP,s) \ s" |
AssignNone: "aval a s = None \ (x ::= a, Some s) \ None" |
Assign: "aval a s = Some i \ (x ::= a, Some s) \ Some(s(x := Some i))" |
Seq:    "(c\<^sub>1,s\<^sub>1) \ s\<^sub>2 \ (c\<^sub>2,s\<^sub>2) \ s\<^sub>3 \ (c\<^sub>1;;c\<^sub>2,s\<^sub>1) \ s\<^sub>3" |

IfNone:  "bval b s = None \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2,Some s) \ None" |
IfTrue:  "\ bval b s = Some True; (c\<^sub>1,Some s) \ s' \ \
  (IF b THEN c\<^sub>1 ELSE c\<^sub>2,Some s) \<Rightarrow> s'" |
IfFalse: "\ bval b s = Some False; (c\<^sub>2,Some s) \ s' \ \
  (IF b THEN c\<^sub>1 ELSE c\<^sub>2,Some s) \<Rightarrow> s'" |

WhileNone: "bval b s = None \ (WHILE b DO c,Some s) \ None" |
WhileFalse: "bval b s = Some False \ (WHILE b DO c,Some s) \ Some s" |
WhileTrue:
  "\ bval b s = Some True; (c,Some s) \ s'; (WHILE b DO c,s') \ s'' \ \
  (WHILE b DO c,Some s) \<Rightarrow> s''"

lemmas big_step_induct = big_step.induct[split_format(complete)]


subsection "Soundness wrt Big Steps"

text\<open>Note the special form of the induction because one of the arguments
of the inductive predicate is not a variable but the term \<^term>\<open>Some s\<close>:\<close>

theorem Sound:
  "\ (c,Some s) \ s'; D A c A'; A \ dom s \
  \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
  case AssignNone thus ?case
    by auto (metis aval_Some option.simps(3) subset_trans)
next
  case Seq thus ?case by auto metis
next
  case IfTrue thus ?case by auto blast
next
  case IfFalse thus ?case by auto blast
next
  case IfNone thus ?case
    by auto (metis bval_Some option.simps(3) order_trans)
next
  case WhileNone thus ?case
    by auto (metis bval_Some option.simps(3) order_trans)
next
  case (WhileTrue b s c s' s'')
  from \<open>D A (WHILE b DO c) A'\<close> obtain A' where "D A c A'" by blast
  then obtain t' where "s' = Some t'" "A \ dom t'"
    by (metis D_incr WhileTrue(3,7) subset_trans)
  from WhileTrue(5)[OF this(1) WhileTrue(6) this(2)] show ?case .
qed auto

corollary sound: "\ D (dom s) c A'; (c,Some s) \ s' \ \ s' \ None"
by (metis Sound not_Some_eq subset_refl)

end


¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

in der Quellcodebibliothek suchen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff