changeset 43158 686fa0a0696e
child 45015 fdac1e9880eb
equal deleted inserted replaced
43157:b505be6f029a 43158:686fa0a0696e
     1 (* Author: Tobias Nipkow *)
     3 theory Def_Ass_Sound_Big imports Def_Ass Def_Ass_Big
     4 begin
     7 subsection "Soundness wrt Big Steps"
     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"}: *}
    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
    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)
    41 end