43158

1 
(* Author: Tobias Nipkow *)


2 


3 
theory Def_Ass_Sound_Big imports Def_Ass Def_Ass_Big


4 
begin


5 


6 


7 
subsection "Soundness wrt Big Steps"


8 


9 
text{* Note the special form of the induction because one of the arguments


10 
of the inductive predicate is not a variable but the term @{term"Some s"}: *}


11 


12 
theorem Sound:


13 
"\<lbrakk> (c,Some s) \<Rightarrow> s'; D A c A'; A \<subseteq> dom s \<rbrakk>


14 
\<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"


15 
proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct)


16 
case AssignNone thus ?case


17 
by auto (metis aval_Some option.simps(3) subset_trans)


18 
next


19 
case Semi thus ?case by auto metis


20 
next


21 
case IfTrue thus ?case by auto blast


22 
next


23 
case IfFalse thus ?case by auto blast


24 
next


25 
case IfNone thus ?case


26 
by auto (metis bval_Some option.simps(3) order_trans)


27 
next


28 
case WhileNone thus ?case


29 
by auto (metis bval_Some option.simps(3) order_trans)


30 
next


31 
case (WhileTrue b s c s' s'')


32 
from `D A (WHILE b DO c) A'` obtain A' where "D A c A'" by blast


33 
then obtain t' where "s' = Some t'" "A \<subseteq> dom t'"


34 
by (metis D_incr WhileTrue(3,7) subset_trans)


35 
from WhileTrue(5)[OF this(1) WhileTrue(6) this(2)] show ?case .


36 
qed auto


37 


38 
corollary sound: "\<lbrakk> D (dom s) c A'; (c,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> s' \<noteq> None"


39 
by (metis Sound not_Some_eq subset_refl)


40 


41 
end
