# Theory Def_Init_Sound_Big

Up to index of Isabelle/HOL/HOL-IMP

theory Def_Init_Sound_Big
imports Def_Init Def_Init_Big
`(* Author: Tobias Nipkow *)theory Def_Init_Sound_Bigimports Def_Init Def_Init_Bigbeginsubsection "Soundness wrt Big Steps"text{* Note the special form of the induction because one of the argumentsof the inductive predicate is not a variable but the term @{term"Some s"}: *}theorem Sound:  "[| (c,Some s) => s';  D A c A';  A ⊆ dom s |]  ==> ∃ t. s' = Some t ∧ A' ⊆ 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 metisnext  case IfTrue thus ?case by auto blastnext  case IfFalse thus ?case by auto blastnext  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 `D A (WHILE b DO c) A'` 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 autocorollary sound: "[|  D (dom s) c A';  (c,Some s) => s' |] ==> s' ≠ None"by (metis Sound not_Some_eq subset_refl)end`