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''"
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 ?caseby auto metis next case IfTrue thus ?caseby auto blast next case IfFalse thus ?caseby 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 thenobtain 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.12 Sekunden
(vorverarbeitet)
¤
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.
