src/HOL/IMP/Def_Ass_Sound_Big.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45015 fdac1e9880eb
child 47818 151d137f1095
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     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 (induction 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